Re: [isabelle] Stuck with existential quantifier
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,
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.
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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