*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Interpreting feedback from Isabelle/HOL*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Wed, 24 Jul 2019 19:22:29 -0400*Cc*: "John F. Hughes" <jfh at cs.brown.edu>*In-reply-to*: <CAJ=ZMJJYK8nLRkgtUnHOKp-fjrpJM3FUaC7Vgvt3GV2ApRjFGw@mail.gmail.com>*References*: <CAJ=ZMJJYK8nLRkgtUnHOKp-fjrpJM3FUaC7Vgvt3GV2ApRjFGw@mail.gmail.com>*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0

You need to use "thus" (or "then show") if you want the subgoal to be discharged. "Hence" asserts a fact, but does not discharge any subgoal. Lines 152-155 of your Question6.thy should be: > thus ?thesis by simp > (* It feels as if the theorem should be proved by now *) > qed > end On 7/24/19 5:18 PM, John F. Hughes wrote: > theory Question6 > imports Main > begin > > locale affine_plane_data = > fixes meets :: "'point ⇒ 'line ⇒ bool" > begin > > definition parallel:: "'line ⇒ 'line ⇒ bool" (infix "||" 50) > where "l || m ⟷ (l = m ∨ ¬ (∃ P. meets P l ∧ meets P m))" > > definition collinear :: "'point ⇒ 'point ⇒ 'point ⇒ bool" > where "collinear A B C ⟷ (∃ l. meets A l ∧ meets B l ∧ meets C l)" > > end > > locale affine_plane = > affine_plane_data meets > for meets :: "'point ⇒ 'line ⇒ bool" + > assumes > a1: "P ≠ Q ⟹ ∃!l. meets P l ∧ meets Q l" and > a2: "¬ meets P l ⟹ ∃!m. l || m ∧ meets P m" and > a3: "∃P Q R. P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ collinear P Q R" > > begin > > (* Every point lies on some line *) > lemma containing_line: " ∀S. ∃l. meets S l" > using a2 by blast > > (* Every line contains at least one point *) > lemma contained_point: "∀l. ∃S. meets S l" > using a1 a2 a3 parallel_def collinear_def by metis > > lemma symmetric_parallel: "l || m ⟹ m || l" > using parallel_def by auto > > lemma reflexive_parallel: "l || l" > by (simp add: parallel_def) > > lemma transitive_parallel: "⟦l || m ; m || n⟧ ⟹ l || n" > by (metis a2 parallel_def) > > (* Two lines meet in at most one point *) > lemma (in affine_plane) prop1H2: "⟦l ≠ m; meets P l; meets P m; meets Q > l; meets Q m⟧ ⟹ P = Q" > using a1 by auto > > (* We now try to prove that every affine plane contains at least four > points. Sledgehammer > doesn't get anywhere with this one. Here's a proof, though: > > i. by A3 there are three distinct non-collinear points; call them P,Q,R. > ii. By A1, there's a line, which I'll call QR, through Q and R. > iii. By A2, there's a line l through P, parallel to QR. > iv. Similarly, there's a line PQ containing P and Q. > v. There's a line m through R, parallel to the line PQ. > > CASES: l is parallel to m, or it is not. > > vi. l is not parallel to m, for if it were, then PQ || m || l || QR, hence > PQ || QR (by > the lemmas about |⦈ and since both contain Q, they are identical, but then > P,Q,R are collinear, > which is a contradiction. > > vii. So l and m are nonparallel, and they share some point S. > > viii. S lies on m, which is parallel to PQ but not equal to it, > hence disjoint from it (see definition of parallel), so S is not on PQ. > > ix. Hence S != P, S != Q. > > x. Similar (arguing about l), we get S != R. > > xi. Hence the four points P,Q,R,S are all distinct, and we are done. > The proof below attempts to mimic this structure. > *) > > proposition four_points: "∃(P :: 'point) (Q :: 'point) (R :: 'point) (S > :: 'point). P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S" > proof - > obtain P Q R where PQR: "P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ collinear P Q R" > using a3 by auto > > (* ii. By A1, there's a line, which I'll call QR, through Q and R. *) > obtain QR where QR: "meets Q QR ∧ meets R QR" > using PQR a1 by blast > > (* iii. By A2, there's a line l through P, parallel to QR. *) > obtain l where l: "meets P l ∧ l || QR" > using a2 parallel_def by metis > > (* iv. Similarly to ii, there's a line PQ containing P and Q. *) > obtain PQ where PQ: "meets P PQ ∧ meets Q PQ" > using PQR a1 by blast > > (* v. and similar to iii, here's a line m through R, parallel to the > line PQ. *) > > obtain m where m: "meets R m ∧ m || PQ" > using a2 parallel_def by metis > > (* CASES: l is parallel to m, or it is not. *) > (* > vi. l is not parallel to m, for if it were, then PQ || m || l || > QR, hence PQ || QR (by > the lemmas about |⦈ and since both contain Q, they are identical, > but then P,Q,R are collinear, > which is a contradiction. > *) > have "¬ (l || m)" > proof > assume 1: "l || m" > hence "m || l" > using 1 symmetric_parallel by simp > moreover have "PQ || m ∧ l || QR" > using m l symmetric_parallel by blast > ultimately have "PQ || QR" > using transitive_parallel by blast > hence "PQ = QR ∨ ¬ (∃ H. meets H PQ ∧ meets H QR)" > by (simp add: parallel_def) > have "meets Q PQ ∧ meets Q QR" > by (simp add: PQ QR) > hence "PQ = QR" > using ‹PQ = QR ∨ (∄H. meets H PQ ∧ meets H QR)› by blast > hence c1: "collinear P Q R" > using PQ QR collinear_def by blast > moreover have c2: "¬ (collinear P Q R)" > using PQR by blast > thus False > using PQR calculation by blast > qed > > obtain S where S: "meets S l ∧ meets S m" > using ‹¬ l || m› parallel_def by blast > > have "¬ meets S PQ" > using PQ PQR S affine_plane_data.collinear_def m parallel_def by > fastforce > hence "S ≠ P ∧ S ≠ Q" > using PQ by blast > have "¬ meets S QR" > by (metis PQR QR S collinear_def parallel_def l) > hence "S ≠ R" > using QR by auto > hence "P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S" > using PQR ‹S ≠ P ∧ S ≠ Q› by blast > hence "∃(P :: 'point) (Q :: 'point) (R :: 'point) (S :: 'point). P ≠ > Q ∧ P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S" > by auto > hence ?thesis by simp > (* It feels as if the theorem should be proved by now *) > qed > qed

**Follow-Ups**:**Re: [isabelle] Interpreting feedback from Isabelle/HOL***From:*Eugene W. Stark

**References**:**[isabelle] Interpreting feedback from Isabelle/HOL***From:*John F. Hughes

- Previous by Date: [isabelle] Interpreting feedback from Isabelle/HOL
- Next by Date: Re: [isabelle] Interpreting feedback from Isabelle/HOL
- Previous by Thread: [isabelle] Interpreting feedback from Isabelle/HOL
- Next by Thread: Re: [isabelle] Interpreting feedback from Isabelle/HOL
- Cl-isabelle-users July 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