# Re: [isabelle] About contradiction method

Quoting Glauber Cabral <glauber.sp at gmail.com>:

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?

The "contradiction" method simply applies the not-elimination rule, notE:
lemma notE: "[| ~P; P |] ==> R"

`Note that unlike most lemmas, the conclusion is totally unrelated to
``the assumptions. If you write "apply contradiction" in an apply-style
``proof, Isabelle matches "R" against your current subgoal, but "P" is
``still totally unconstrained, so your new subgoals will have schematic
``variables (usually shown with question marks, like "?P"). In your
``case, the "?P" schematic variable is parametrized over x and y because
``your subgoal is universally quantified over those variables, and ?P is
``allowed to depend on them.
`

`Schematic variables can be instantiated at any time by matching them
``with other rules or assumptions. For example, if you have a subgoal
``that looks like "~ foo ==> ~ ?P", you can discharge it by typing
``"apply assumption" which will instantiate ?P to foo. All occurrences
``of ?P in other subgoals will then be replaced by foo.
`

`Schematic variables can be awkward to deal with in apply-style proofs.
``Instead of "apply contradiction", you might prefer to explicitly
``instantiate P using rule_tac, e.g. "apply (rule_tac P="foo" in notE)".
`
Alternatively, the "contradiction" method is more useful in Isar-style proofs:
lemma
fixes x y :: nat
assumes A: "x < y" and B: "y < x"
shows "False"
proof (contradiction)
show "x < x"
using A B by (rule less_trans)
show "¬ x < x"
by (rule less_not_refl)
qed
lemma
fixes x y :: nat
assumes A: "x < y" and B: "y < x"
shows "False"
proof -
have 1: "x < x"
using A B by (rule less_trans)
have 2: "¬ x < x"
by (rule less_not_refl)
from 1 2 show "False"
by contradiction
qed
Hope this helps,
- Brian

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