[isabelle] About contradiction method
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] About contradiction method
- From: "Glauber Cabral" <glauber.sp at gmail.com>
- Date: Tue, 17 Jun 2008 17:30:28 -0300
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
I'm using Isabelle to prove HasCASL specifications and I'm still learning
how to use both "technologies" to my master thesis. Sorry if this question
is too newbie, but I couldn't find any solution by myself.
I've been writing proofs only with apply (method) because Isabelle is not
the main focus right now and I thought it should be enough at this moment to
write proofs this way.
The problem is that I could not find any example or explanation about how to
use contradiction method. When I use it, I got 2 goals: P x y and not P x y,
and I couldn't find how to make Isabelle relates P with a function I've
already created. Can anyone tell me where do I found any explanation or
example to understand how it works?
I'd like to ask something else that I'm not sure. If I escape a proof of a
theorem/lemma with oops, I cannot use this thm/lemma in the next proofs,
right?Just to be sure, although I know using this without proving it would
not make sense...
Thanks in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and