*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Unable to prove easy existential "directly"*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 19 Jul 2013 13:30:05 +0200*In-reply-to*: <6c9a-51e80c80-1-5d76dd8@90856565>*References*: <6c9a-51e80c80-1-5d76dd8@90856565>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

Hallo, the behaviour of "rule" in the presence of premises is something that I have not and will probably never understand. You can replace the ".." with a "by (rule_tac exI)" or a "by (intro exI)" and that works fine. Personally, I usually prefer the good old "by blast" in these cases. Another thing that would work is "from exI[OF this] show "∃b.(P b)" ." As for the reason that rule fails here but rule_tac works, that is something from the depths of the internals of Isabelle that are far outside my area of expertise. Cheers, Manuel On 07/18/2013 05:41 PM, Wilmer RICCIOTTI wrote: > Hi all, > > as a beginner in the use of Isabelle/Isar, I have every day numerous clashes with the Isar way of proving theorems. The strangest one to date is related to proving an existentially quantified formula when you have the same formula with an explicit witness as a hypothesis. That is to say, something similar to this lemma: > > lemma fie : "P a ⟶ (∃b.(P b))" > proof > assume ha : "P a" > thus "∃b.(P b)".. > qed > > Unsurprisingly, this proof doesn't pose any challenge at all. However I can slightly complicate the formula by means of a definition, and this obvious proof technique won't work any more. Specifically, I define > > definition bijection :: "('a ⇒ 'b) ⇒ bool" where > "bijection f = (∀y::'b.∃!x::'a. y = f x)" > > and then the same proof as before, with bijection in place of a generic P, fails: > > lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))" > proof > assume hg : "bijection (g::'a ⇒ 'b)" > thus "∃f.(bijection f)".. > qed > > replacing the implicit ".." with an explicit "proof (rule exI)" fails similarly, leaving me quite puzzled. > (Un)Interestingly, since "foo" is an instance of "fie", we can easily prove it using "by (rule fie)" and nothing else. However this feels more like a trick to make things work than a solution. > > What am I doing wrong? > > Best, > -- > Wilmer Ricciotti >

**References**:**[isabelle] Unable to prove easy existential "directly"***From:*Wilmer RICCIOTTI

- Previous by Date: [isabelle] Unable to prove easy existential "directly"
- Next by Date: Re: [isabelle] Unable to prove easy existential "directly"
- Previous by Thread: [isabelle] Unable to prove easy existential "directly"
- Next by Thread: Re: [isabelle] Unable to prove easy existential "directly"
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list