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.