[isabelle] About contradiction method



Hi everybody.

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,
Glauber Cabral




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