*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proving a simple lemma*From*: Tjark Weber <webertj at in.tum.de>*Date*: Thu, 26 Jul 2012 22:02:33 +0200*In-reply-to*: <CAFU+7wPf+zDYTjn63g3UEJvBAH=zPpBnK=mdp10YOqvw2dBO5A@mail.gmail.com>*References*: <CAFU+7wPf+zDYTjn63g3UEJvBAH=zPpBnK=mdp10YOqvw2dBO5A@mail.gmail.com>

On Thu, 2012-07-26 at 20:10 +0100, Steve Wong wrote: > I'm struggling to prove the following lemma: > > lemma "EX k:S. P k == EX k. k : S --> P k" > > If my understand is right, the lemma should be correct. If you try nitpick, it will quickly show you a counterexample. > However, I can't find a proof using sledgehammer. A correct version of the lemma is lemma "EX k:S. P k == EX k. k : S ∧ P k" by (rule eq_reflection) metis eq_reflection (in HOL.thy) states that object equality (=) implies meta-equality (==). You might want to use = in your lemma in the first place; then sledgehammer will succeed. Best regards, Tjark

**References**:**[isabelle] Proving a simple lemma***From:*Steve Wong

- Previous by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Next by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Previous by Thread: Re: [isabelle] Proving a simple lemma
- Next by Thread: [isabelle] "Illegal equation head" ---an error in func definition
- Cl-isabelle-users July 2012 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