Re: [isabelle] Proving a simple lemma



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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.