Re: [isabelle] Interpreting feedback from Isabelle/HOL



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.