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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and