Re: [isabelle] Stuck with existential quantifier


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.



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.