Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Instantiating a quantifier in a tactic

view this post on Zulip Email Gateway (Aug 18 2022 at 15:56):

From: John Munroe <munddr@gmail.com>
Hi,

I have a quick question regarding instantiating a quantifier
explicitly in a tactic. For example, how would the following line be
translated into a tactic:

lemma "EX z. z > a"
apply (rule exI [where x = "c"])
..

where a and c are constants. Would Drule.instantiate need to be used?

TIA

John

view this post on Zulip Email Gateway (Aug 18 2022 at 15:57):

From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
John,

I think it should be

res_inst_tac [("x", "c")] exI 1

Jeremy

Last updated: Nov 21 2024 at 12:39 UTC