Re: [isabelle] About contradiction method



Hi Brian.

Thank you for this explanation. It helped me me to understand how
contradiction works. I've already tried to instantiate P with *rule_tac
methods, but I guess I did some mistake and that didn't work.
The ccontr worked for me, as it was told in the list.

Best regards,
Glauber

On Thu, Jun 19, 2008 at 11:20 AM, Brian Huffman <brianh at cs.pdx.edu> wrote:

> 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.