Re: [isabelle] Stuck with existential quantifier



Hi,

the nth function on lists (xs ! n) is undefined when n is outside the bounds of xs. That means that we do not know anything about the result. Since we do not know anything, we do in particular not know whether the result is 0 or not. Thus your statement is not provable.

I hope this helps.

cheers

chris


On 07/25/2011 10:17 PM, Christian Kühnel wrote:

Dear isabelle users,


I'm trying to prove this obvious lemma:


   "~ (EX t. [1::nat,1,1] ! t = 0 )"


I've been trying for a while but could not figure it out. Can you please
give me a hint, how I can prove this?


Is there more documatation on prooving terms with existential and universal
quantifiers? The isabelle tutorial did not help me there.



Best regards,
Christian Kühnel







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