*To*: Mathias Fleury <mathias.fleury12 at gmail.com>*Subject*: Re: [isabelle] Proof by contradiction*From*: "John F. Hughes" <jfh at cs.brown.edu>*Date*: Thu, 28 Mar 2019 12:14:37 -0400*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <AFF3A3EA-DFC5-4649-A85E-A644D0F7CF49@gmail.com>*References*: <CAJ=ZMJK-Liu5JGNE0YqK+vwXEo9Bq7=ryczAP8H5mHcJ-164vw@mail.gmail.com> <AFF3A3EA-DFC5-4649-A85E-A644D0F7CF49@gmail.com>

Thanks...this is *exactly* what I was looking for. It leads me to a few more questions, though, * First, T (from "T = A2Point u v") is not bound. Isabelle/jEdit is showing > that with the different background. You want something along: > obtain T where > ‹…› > * Similarly, you have to use obtain for u and v, not fix. Can you suggest somewhere that I can learn the distinction between "obtain" and "fix"? The reference manual has a paragraph that's too cryptic for my current understanding of logic (which is quite basic); Ballarin's tutorial slides basically say "they're different". I think I need something in the middle. :) * Then the last step has to be "show False" instead of "have False". Then > you will get an error ("Failed to refine any pending goal"), because "rule > ccontr is only negating once more ‹¬ (∃ T. a2meets T l ∧ a2meets T k)›. > You can fix that by removing "rule ccontr" and rely on the default rule > to do the right thing. If I actually *wanted* to do a proof by contradiction, even though it's not necessary here, would I have to start with proof (rule ccontr) assume "¬¬ (∃ T. a2meets T l ∧ a2meets T k)" Perhaps choosing a theorem with a negation in the conclusion was a bad place to start trying to use proof-by-contradiction. But I'd really like to see how to do such a proof. Later you suggest restating the theorem as its contrapositive (which may or may not be a good idea...I don't know whether Isabelle can use the contrapositive as effectively for what I need to do next), and propose three things (which I've reordered): * use cartouche * use "defines" instead of "assumes" * remove the "exist" quantifier My questions: -- Typing double-quotes is easy; typing cartouches is tough (for me) --- is there some simple way to do this, and are they the preferred form now? -- the reference manual, page 102) says that 'defines" defines a previously declared parameter, but in your use > lemma A2_vert2: > fixes x0 x1 :: real > defines l_form: ‹l ≡ A2Vertical x0› > defines k_form: ‹k ≡ A2Vertical x1› > assumes ‹a2meets T l› and ‹a2meets T k› > shows ‹l = k› > by (cases T) (use assms in auto) > the parameters l and k haven't been previously declared (as far as I can tell). Of course, that description of "defines" is in the section about locales in the reference manual, so it's probably the wrong one. But it's the only mention of that keyword in the whole manual, so I'm at a loss for what this actually means here. -- does this form of the statement really remove the "exists" quantifier? Or is there an implicit "exists" in the "assumes" line? And does removing it (assuming it's really gone) make things easier for the prover? --John

**Follow-Ups**:**Re: [isabelle] Proof by contradiction***From:*Wolfgang Jeltsch

**References**:**[isabelle] Proof by contradiction***From:*John F. Hughes

**Re: [isabelle] Proof by contradiction***From:*Mathias Fleury

- Previous by Date: Re: [isabelle] Proof by contradiction
- Next by Date: [isabelle] New in the AFP: The Transcendence of Certain Infinite Series
- Previous by Thread: Re: [isabelle] Proof by contradiction
- Next by Thread: Re: [isabelle] Proof by contradiction
- Cl-isabelle-users March 2019 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