Re: [isabelle] Stuck with existential quantifier



Dear Christian,

your lemma is not provable, because t is not constrained to the length of the list. It could be, say, 42, and you can hardly prove anything about what you get if you take an element beyond the list.

Here's the provable version:

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

If you apply the simplifier to this goal, it will pull the negation in, turning the existential quantifier into a universal one, so this is no longer a problem of existential quantifiers. You can prove the statement in by trying every possible value -- which is feasible for such small lists, but impractical for larger ones. If you want to split the cases for t automatically, feed nth_Cons' to the simplifier:

by(simp add: nth_Cons')

Hope this helps,
Andreas

Am 25.07.2011 22:17, schrieb Christian Kühnel:

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

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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