*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Proof by contradiction*From*: "John F. Hughes" <jfh at cs.brown.edu>*Date*: Thu, 28 Mar 2019 09:39:53 -0400

I'm struggling with trying to encode a proof by contradiction in Isar. In the euclidean plane, I'm trying to prove that if two vertical lines l and k lie at different x-coordinates, then they have no points in common. In a math book, I'd write: Suppose (u,v) is on both x = a and x = b, and a \ne b; then u = a and u = b, so a = b. Contradiction. With Isabelle in the back of my mind, perhaps I'd write this: Proof: Because l is vertical, it's defined by an equation x = a ; similarly k is defined by x = b, and we're given that a \ne b. Suppose T = (u,v) lies on both. Then u = a because T is on l, and u = b because T is on k, and thus a = b. That's a contradiction with the given fact a \ne b. Hence T cannot lie on both lines. QED. I've attempted to mimic this proof in Isar below, and it's fairly readable, I hope. "a2meets P m" is my way of saying "the point P is on the line m", and it's written this way to make it consistent with other stuff I'm writing about general affine geometries. Although the resulting proof is wordy, I feel as if I'm headed in the right direction. But I cannot figure out the syntax for saying "OK, I've proved False. Surely we can conclude the theorem by contradiction!": theory Brief6 imports Complex_Main begin datatype a2pt = A2Point "real" "real" datatype a2ln = A2Ordinary "real" "real" | A2Vertical "real" text "Ordinary m b represents the line y = mx+b; Vertical xo is the line x = xo " fun a2meets :: "a2pt ⇒ a2ln ⇒ bool" where "a2meets (A2Point x y) (A2Ordinary m b) = (y = m*x + b)" | "a2meets (A2Point x y) (A2Vertical xi) = (x = xi)" (* Lemma: vertical lines with different x-coords are disjoint *) lemma A2_vert: "x0 ≠ x1 ∧ l = A2Vertical x0 ∧ k = A2Vertical x1 ⟹ ¬ (∃ T. a2meets T l ∧ a2meets T k)" proof - assume diff_x: "x0 ≠ x1" assume l_form: "l = A2Vertical x0" assume k_form: "k = A2Vertical x1" have "¬ (∃ T. a2meets T l ∧ a2meets T k)" proof (rule ccontr) assume "∃ T. a2meets T l ∧ a2meets T k" fix u v assume T_form: "T = A2Point u v" have T_on_l: "a2meets T l" by (metis ‹∃T. a2meets T l ∧ a2meets T k› a2meets.elims(2) a2meets.simps(2) diff_x k_form l_form) have T_on_k: "a2meets T k" by (metis ‹∃T. a2meets T l ∧ a2meets T k› a2meets.elims(2) a2meets.simps(2) diff_x k_form l_form) have "u = x0" using T_form T_on_l l_form by auto have "u = x1" using T_form T_on_k k_form by auto have False using ‹u = x0› ‹u = x1› diff_x by blast qed ======= I'd appreciate it if (a) someone could add whatever last line or two is needed to finish this proof, and (b) someone could show how to make the proof more idiomatic and perhaps briefer (which might entail rewriting the lemma itself, and if that's necessary, it's fine with me). --John

**Follow-Ups**:**Re: [isabelle] Proof by contradiction***From:*Lawrence Paulson

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

- Previous by Date: [isabelle] 1st CFP for Certified Programs and Proofs (CPP 2020)
- Next by Date: Re: [isabelle] Proof by contradiction
- Previous by Thread: [isabelle] 1st CFP for Certified Programs and Proofs (CPP 2020)
- 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