*To*: "Brian Huffman" <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] About contradiction method*From*: "Glauber Cabral" <glauber.sp at gmail.com>*Date*: Thu, 19 Jun 2008 20:03:21 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20080619072023.0uymhd4u34c8g0oo@webmail.pdx.edu>*References*: <deb09ce60806171123s59bc8a69sedab7247a1873512@mail.gmail.com> <deb09ce60806171330q3ee9bc1cse578036c201c1e0@mail.gmail.com> <B545CFE5-9350-4A08-97BC-0527BBCE057A@cam.ac.uk> <deb09ce60806180605p4931baa6xc28c52f4a99cd183@mail.gmail.com> <20080619072023.0uymhd4u34c8g0oo@webmail.pdx.edu>

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

**References**:**[isabelle] About contradiction method***From:*Glauber Cabral

**Re: [isabelle] About contradiction method***From:*Lawrence Paulson

**Re: [isabelle] About contradiction method***From:*Glauber Cabral

**Re: [isabelle] About contradiction method***From:*Brian Huffman

- Previous by Date: [isabelle] need help with quantified ints
- Next by Date: [isabelle] Herlihy, Milner, Hoare, O'Hearn etc.: LASER summer school
- Previous by Thread: Re: [isabelle] About contradiction method
- Next by Thread: [isabelle] Isar Proof
- Cl-isabelle-users June 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list