Re: [isabelle] Proving a simple lemma

This is not true. "EX k : S . P K" is equivalent to "EX k. ((k : S) & (P k))" , which is stronger than "EX k. k : S --> P k". If S is empty, "EX k. k : S --> P k" is true, but "EX k : S . P K" is false.

On 7/26/12 2:10 PM, 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. However, I can't
find a proof using sledgehammer.

Any help will be appreciated. Thanks.


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