theory Tarski
imports Main
begin

text {*
(* Paste in these 2 commands:
   hol_light> ocaml
   #use "hol.ml";;  
    then paste in the following file*)

(* ================================================================= *)
(* HOL Light Tarski geometry axiomatic proofs up to Gupta's theorem. *)
(* ================================================================= *)

(* Proof assistants like HOL Light can be used to help teach rigorous
   axiomatic geometry in high school using Hilbert's axioms, and
   introduce students to the world of formal proofs, which should
   become a hot area in debugging computer software.

   This is a port, mostly due to John Harrison, of Mizar code, which
   was heavily influenced by Julien Narboux's Coq pseudo-code
   http://dpt-info.u-strasbg.fr/~narboux/tarski.html and Wojciech
   A. Trybulec's incsp_1.miz in the MML library on axioms of incidence
   geometry.  We partially prove the theorem of the 1983 book
   Metamathematische Methoden in der Geometrie by Schwabhäuser,
   Szmielew, and Tarski, that Tarski's (extremely weak!) plane
   geometry axioms imply Hilbert's axioms.  We get about as far as
   Narboux, with Gupta's amazing proof which implies Hilbert's axiom
   I1 that two points determine a line.  

   Thanks to Mizar folks who wrote an influential language I was able
   to learn, Freek Wiedijk, who wrote the miz3 port of Mizar to HOL
   Light, and especially John Harrison, who came up with the entire
   framework of porting my axiomatic proofs to HOL Light.  *)


new_type("point",0);;

new_constant("===",`:point#point->point#point->bool`);;
new_constant("Between",`:point#point#point->bool`);;

parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("on_line",(12, "right"));;
parse_as_infix("equal_line",(12, "right"));;

let cong_DEF = new_definition
 `a,b,c cong x,y,z <=>
   a,b === x,y /\ a,c === x,z /\ b,c === y,z`;;

let is_ordered_DEF = new_definition
 `is_ordered (a,b,c,d) <=>
  Between (a,b,c) /\ Between (a,b,d) /\ Between (a,c,d) /\ Between (b,c,d)`;;

let Line_DEF = new_definition
  `x on_line a,b <=> 
  ~(a = b) /\ (Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b))`;;

let  LineEq_DEF = new_definition
  `a,b equal_line x,y <=>
~(a = b) /\ ~(x = y) /\ ! c .  c on_line a,b  <=>  c on_line x,y`;;



(* ------------------------------------------------------------------------- *)
(* The axioms.                                                               *)
(* ------------------------------------------------------------------------- *)

let A1 = new_axiom
  `!a b. a,b === b,a`;;

let A2 = new_axiom
  `!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`;;

let A3 = new_axiom
  `!a b c. a,b === c,c ==> a = b`;;

let A4 = new_axiom
  `!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;;

let A5 = new_axiom
  `!a b c x a' b' c' x'.
        ~(a = b) /\ a,b,c cong a',b',c' /\
        Between(a,b,x) /\ Between(a',b',x') /\ b,x === b',x'
        ==> c,x === c',x'`;;

let A6 = new_axiom
  `!a b. Between(a,b,a) ==> a = b`;;

let A7 = new_axiom
  `!a b p q z.
        Between(a,p,z) /\ Between(b,q,z) ==>
        ?x. Between(p,x,b) /\ Between(q,x,a)`;;


(* A4 is the Segment Construction axiom, A5 is the SAS axiom and A7 is
   the Inner Pasch axiom.  There are 4 more axioms we're not using yet:
   there exist 3 non-collinear points;
   3 points equidistant from 2 distinct points are collinear;
   Euclid's parallel postulate;
   a first order version of Hilbert's Dedekind Cuts axiom.

   We shall say we apply SAS to a+cbx and a'+c'b'x'.  Normally one
   applies SAS by showing cb = c'b' bx = b'x' (which we assume) and
   angle cbx cong angle c'b'x'.  One might prove the angle congruence
   by showing that the triangles abc /\ a'b'c' were congruent by SSS
   (which we also assume) and then apply the theorem that complements
   of congruent angles are congruent.  Hence Tarski's axiom. *)


(* ------------------------------------------------------------------------- *)
(* Now Mizarlight versions of the actual proofs.                             *)
(* ------------------------------------------------------------------------- *)

#load "unix.cma";;
loadt "miz3/miz3.ml";;

horizon := 0;; 

let EquivReflexive = thm `;
  !a b. a,b === a,b

  proof
   let a b be point;
   b,a === a,b by A1;
  qed by -, A2`;;


let EquivSymmetric = thm `;
  !a b c d. a,b === c,d ==> c,d === a,b

  proof
    let a b c d be point;
    assume a,b === c,d [1];
    a,b === a,b by EquivReflexive;
  qed by -, 1, A2`;;


let EquivTransitive = thm `;
  !a b p q r s .  a,b === p,q /\ p,q === r,s ==> a,b === r,s

  proof
    let a b p q r s be point;
    assume a,b === p,q [H1];
    assume p,q === r,s [H2];
    p,q === a,b by H1, EquivSymmetric;
    qed by -, H2, A2`;;


let Baaa_THM = thm `;
  !a b. Between (a,a,a) /\ a,a === b,b

  proof
    let a b be point;
    consider x such that Between (a,a,x) /\ a,x === b,b [X1] by A4;
    a = x by -, A3;
  qed by -, X1`;;


let Bqaa_THM = thm `;
  !a q. Between(q,a,a)

  proof
    let a q be point;
    consider x such that Between(q,a,x) /\ a,x === a,a [X1] by A4;
    a = x by -, A3;
  qed by -, X1`;;


let C1_THM = thm `;
  let a b x y be point;
  assume             ~(a = b)						[H1];
  assume             Between (a,b,x)                                 	[H2];
  assume             Between (a,b,y)                                 	[H3];
  assume             b,x === b,y                                     	[H4];
  thus    y = x
 
  proof
    a,b === a,b /\ a,y === a,y /\ b,y === b,y by EquivReflexive;  
    a,b,y cong a,b,y by -, cong_DEF;  
    y,x === y,y by -, H1, H2, H3, H4, A5;  
    qed by -, A3`;;


let Bsymmetry_THM = thm `;
  let a p z be point;
  thus Between (a,p,z) ==> Between (z,p,a)

  proof
    assume Between (a,p,z) [H1];
    Between (p,z,z) by Bqaa_THM;  
    consider x such that
    Between (p,x,p) /\ Between (z,x,a) [X1] by -, H1, A7;
    x = p by -, A6;  
  qed by -, X1`;;


let Baaq_THM = thm `;
  let a q be point;
  thus Between (a,a,q)

  proof
    Between (q,a,a) by Bqaa_THM;  
  qed by -, Bsymmetry_THM`;;


let BEquality_THM = thm `;
  let a b c be point;
  thus Between (a,b,c) /\ Between (b,a,c) ==> a = b

  proof
    assume  Between (a,b,c) [H1];
    assume Between (b,a,c);  
    ? x . Between (b,x,b) /\ Between (a,x,a) by -, H1, A7;
    consider x such that
    Between (b,x,b) /\ Between (a,x,a) [X1] by -;
    b = x by X1, A6;  
    Between (a,b,a) by -, X1;  
  qed by -, A6`;;


let B124and234then123_THM = thm `;
  let a b c d be point;
  assume                       Between (a,b,d)				[H1];
  assume                       Between (b,c,d)                         	[H2];  
  thus    Between (a,b,c)

  proof
    ? x . Between (b,x,b) /\ Between (c,x,a) by H1, H2, A7;
    consider x such that
    Between (b,x,b) /\ Between (c,x,a) [X1] by -;
    b = x by X1, A6;  
    Between (c,b,a) by -, X1;   
  qed by -, Bsymmetry_THM`;;


let BTransitivity_THM = thm `;
  let a b c d be point;
  assume                       ~(b = c)					[H1];
  assume                       Between (a,b,c)                         	[H2];
  assume                       Between (b,c,d)                         	[H3];
  thus Between (a,c,d)

  proof
    consider x such that 
    Between (a,c,x) /\ c,x === c,d [X1] by A4;
    Between (x,c,a)  [X2] by -, Bsymmetry_THM;
    Between (c,b,a) by H2, Bsymmetry_THM;
    Between (x,c,b) by -, X2, B124and234then123_THM;
    Between (b,c,x) by -, Bsymmetry_THM;
    x = d by -, H1, H3, X1, C1_THM;   
  qed by -, X1`;;


let BTransitivityOrdered_THM = thm `;
  let a b c d be point;
  assume                       ~(b = c)                                 [H1];
  assume                       Between (a,b,c)                          [H2];
  assume                       Between (b,c,d)                          [H3];
  thus    is_ordered (a,b,c,d)					        
								        
  proof								        
    Between (a,c,d) [X1] by H1, H2, H3, BTransitivity_THM;	        
    Between (d,c,b) [X2] by H3, Bsymmetry_THM;			        
    Between (c,b,a) by -, H2, Bsymmetry_THM;			        
    Between (d,b,a) by -, H1, X2, BTransitivity_THM;		        
    Between (a,b,d) by -, Bsymmetry_THM;   			        
    qed by H2, -, X1, H3, is_ordered_DEF`;;			        
								       

let B124and234Ordered_THM = thm `;
  let a b c d be point;
  assume                       Between (a,b,d)                          [H1];
  assume                       Between (b,c,d)                          [H2];
  thus   is_ordered (a,b,c,d)					        
								        
  proof								        
    cases;							        
    suppose b = c [P1];						        
      Between (a,b,c) [P2] by -, Bqaa_THM;			        
      Between (a,c,d) by P1, H1;   				        
      qed by P2, H1, -, H2, is_ordered_DEF;			        
    suppose ~(b = c) [Q1];					        
      Between (a,b,c) by H1, H2, B124and234then123_THM;   	        
      qed by -, Q1, H2, BTransitivityOrdered_THM;		        
   end`;;							        
								        

let SegmentAddition_THM = thm `;
  let a b c a' b' c' be point;
  assume                Between (a,b,c)                                 [H1];
  assume                Between (a',b',c')                              [H2];
  assume                a,b === a',b'                                   [H3];
  assume                b,c === b',c'                                   [H4];
  thus   a,c === a',c'						        
								        
  proof								        
    cases;							        
    suppose a = b [Y1];						        
      a,a === a',b' by H3, Y1;					        
      a',b' === a,a by -, EquivSymmetric;			        
      a' = b' by -, A3;						        
    qed by -, H4, Y1;						        
    suppose ~(a = b) [Z1];					        
      b,a === a,b by A1;					        
      b,a === a',b' [Z2] by -, H3, EquivTransitive;		        
      a',b' === b',a' by A1;					        
      b,a === b',a' [Z3] by -, Z2, EquivTransitive;		        
      a,a === a',a' by Baaa_THM;				        
      a,b,a cong a',b',a' by -, H3, Z3, cong_DEF;  		        
    qed by -, Z1, H1, H2, H4, A5;				        
  end`;;							        
								        

let CongruenceDoubleSymmetry_THM = thm `;
  let a b c d be point;
  assume               a,b === c,d					[H1];
  thus   b,a === d,c

  proof
    b,a === a,b /\ c,d === d,c [X1] by H1, A1;
    a,b === d,c by H1, X1, EquivTransitive;   
    qed by -, X1, EquivTransitive`;;


let C1prime_THM = thm `;
  let a b x y be point;
  assume                       ~(a = b)                                 [H1];
  assume                       Between (a,b,x)                          [H2];
  assume                       Between (a,b,y)                          [H3];
  assume                       a,x === a,y                              [H4];
  thus         x = y						        
								        
  proof								        
    consider m such that					        
    Between (b,a,m) /\ a,m === a,b [X1] by A4;			        
    Between (m,a,b) [X2] by X1, Bsymmetry_THM;			        
    ~(m = a) [X3] by X1, EquivSymmetric, A3, H1;		        
    is_ordered (m,a,b,x) by H1, X2, H2, BTransitivityOrdered_THM;       
    Between (m,a,x) [X4] by -, is_ordered_DEF;			        
    is_ordered (m,a,b,y) by H1, X2, H3, BTransitivityOrdered_THM;       
    Between (m,a,y) by -, is_ordered_DEF;   			        
    qed by -, X3, X4, H4, C1_THM`;;				        
								        

let SegmentSubtraction_THM = thm `;
  let a b c a' b' c' be point;
  assume                  Between (a,b,c)                             [H1];
  assume                  Between (a',b',c')                          [H2];
  assume                  a,b === a',b'                               [H3];
  assume                  a,c === a',c'                               [H4];
  thus    b,c === b',c'						      
								      
  proof								      
    cases;							      
    suppose a = b [Y1];						      
      a,a === a',b' by -, H3;					      
      a',b' === a,a by -, EquivSymmetric;			      
      a' = b' by -, A3;   					      
      qed by -, H4, Y1;						      
    suppose ~(a = b) [Z1];					      
      consider x such that					      
      Between (a,b,x) /\ b,x === b',c' [Z2] by A4;		      
      a,x === a',c' [Z3] by Z2, H2, H3, SegmentAddition_THM;	      
      a',c' === a,c by H4, EquivSymmetric;			      
      a,x === a,c by -, Z3, EquivTransitive;			      
      x = c by -, Z1, Z2, H1, C1prime_THM;   			      
    qed by -, Z2;						      
  end`;;							      
								      

let EasyAngleTransport_THM = thm `;
    let a O b be point;
    assume             ~(O = a)						[H1];
    thus ? x y . 
           Between (b,O,x) /\ Between (a,O,y) /\ x,y,O cong a,b,O

  proof
    consider x such that
    Between (b,O,x) /\ O,x === O,a [X2] by A4;
    x,O === a,O [X3] by -, CongruenceDoubleSymmetry_THM;
    a,O === x,O [X4] by -, EquivSymmetric;
    a,x === x,a by A1;
    a,O,x cong x,O,a [X5] by X4, -, X2, cong_DEF;
    consider y such that
    Between (a,O,y) /\ O,y === O,b [X6] by A4;
    Between (x,O,b) by X2 ,Bsymmetry_THM;
    x,y === a,b [X7] by H1, X5, X6, -, A5;
    y,O === b,O by X6, CongruenceDoubleSymmetry_THM;
    x,y,O cong a,b,O by X7, X3, -, cong_DEF;
  qed by X2, X6, -`;;


let B123and134Ordered_THM = thm `;
  let a b c d be point;
  assume                       Between (a,b,c)                          [H1];
  assume                       Between (a,c,d)                          [H2];
  thus   is_ordered (a,b,c,d)					        
								        
  proof								        
    Between (d,c,a) /\ Between (c,b,a) by H2, H1, Bsymmetry_THM;        
    is_ordered (d,c,b,a) by -, B124and234Ordered_THM;		        
    Between (d,b,a) /\ Between (d,c,b) by -, is_ordered_DEF;	        
    Between (a,b,d) /\ Between (b,c,d) by -, Bsymmetry_THM;   	        
  qed by -, H1, H2, is_ordered_DEF`;;				        
								        

let BextendToLine_THM = thm `;
  let a b c d be point;
  assume                       ~(a = b)                                 [H1];
  assume                       Between (a,b,c)                          [H2];
  assume                       Between (a,b,d)                          [H3];
  thus ? x . 							        
         is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x)		        
								        
  proof								        
    consider u such that					        
    Between (a,c,u) /\ c,u === b,d [X1] by A4;			        
    is_ordered (a,b,c,u) [X2] by H2, X1, B123and134Ordered_THM;	        
    Between (b,c,u) by X2, is_ordered_DEF;			        
    Between (u,c,b) [X3] by -, Bsymmetry_THM;			        
    u,c === c,u by A1;						        
    u,c === b,d [X4] by -, X1, EquivTransitive;			        
    Between (a,b,u) [X5] by X2, is_ordered_DEF;			        
    consider x such that					        
    Between (a,d,x) /\ d,x === b,c [Y1] by A4;			        
    is_ordered (a,b,d,x) [Y2] by H3, Y1, B123and134Ordered_THM;	        
    Between (b,d,x) [Y3] by -, is_ordered_DEF;			        
    b,c === d,x [Y4] by Y1, EquivSymmetric;			        
    c,b === b,c by A1;						        
    c,b === d,x [Y5] by -, Y4, EquivTransitive;			        
    Between (a,b,x) [Y6] by Y2, is_ordered_DEF;			        
    u,b === b,x [X6] by X3, Y3, X4, Y5, SegmentAddition_THM;	        
    b,u === u,b by A1;						        
    b,u === b,x by -, X6, EquivTransitive;			        
    u = x by -, H1, X5, Y6, C1_THM;				        
  qed by -, X2, Y2`;;						        
								        

let GuptaEasy_THM = thm `;
  let a b c d be point;
  assume                     ~(a = b)                                   [H1];
  assume                     Between (a,b,c)                            [H2];
  assume                     Between (a,b,d)                            [H3];
  assume                     ~(b = c)                                   [H4];
  assume                     ~(b = d)                                   [H5];
  thus ~ Between (c,b,d)					        
								        
  proof
    cases; 
    suppose ~ Between (c,b,d);
    qed by -;
    suppose Between (c,b,d) [H6];
      ? x . is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x) 
      by H1, H2, H3, BextendToLine_THM;
      consider x such that
      is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x) [X1] by -;
      Between (b,d,x) by X1, is_ordered_DEF;
      is_ordered (c,b,d,x) by -, H5, H6, BTransitivityOrdered_THM;
      Between (b,c,x) /\ Between (c,b,x) by -, X1, is_ordered_DEF;
      b = c [X2] by -, BEquality_THM;
      F by -, H4, X2;
    qed by -;
  end`;;


(* The next result is like SAS: there are 5 pairs of segments 4
   equivalent.  We say we apply Inner5Segments to abc-x and a'b'c'-x' *)

let Inner5Segments_THM = thm `;
  let a b c x a' b' c' x' be point;
  assume               a,b,c cong a',b',c'				[H1];
  assume               Between (a,x,c)         				[H2];
  assume               Between (a',x',c')      				[H3];
  assume               c,x === c',x'           				[H4];
  thus   b,x === b',x'

  proof
    a,b === a',b' /\ a,c === a',c' /\ b,c === b',c' [X1] by H1, cong_DEF;
    cases;
    suppose x = c [Case1];
      c',x' === c,c by H4, Case1, EquivSymmetric;
      x' = c' by -, A3;
    qed by -, Case1, X1;
    suppose ~(x = c) [Case2];
      ~(a = c) [X2] by H2, A6, Case2;
      consider y such that
      Between (a,c,y) /\ c,y === a,c [X3] by A4;
      consider y' such that
      Between (a',c',y') /\ c',y' === a,c [X4] by A4;
      a,c === c',y' by X4, EquivSymmetric;
      c,y === c',y' [X5] by -, X3, EquivTransitive;
      c,b === c',b' [X6] by X1, CongruenceDoubleSymmetry_THM;
      a,c,b cong a',c',b' by cong_DEF, X1, X6;
      b,y === b',y' [X7] by -, X2, X3, X4, X5, A5;
      ~(y = c) [X8] by X3, EquivSymmetric, A3, X2;
      Between (y,c,a) /\ Between (c,x,a) by X3, H2, Bsymmetry_THM;
      Between (y,c,x) [X9] by -, B124and234then123_THM;
      Between (y',c',a') /\ Between (c',x',a') by -, X4, H3, Bsymmetry_THM;
      Between (y',c',x') [X10] by -, B124and234then123_THM;
      y,c === y',c' /\ y,b === y',b' by X5, X7, CongruenceDoubleSymmetry_THM;
      y,c,b cong y',c',b' by -, cong_DEF, X6;   
    qed by -, X8, X9, X10, H4, A5;
  end`;;


let RhombusDiagBisect_THM = thm `;
  let b c d c' d' be point;
  assume                       Between (b,c,d')                         [H1];
  assume                       Between (b,d,c')                         [H2];
  assume                       c,d' === c,d                             [H3];
  assume                       d,c' === c,d                             [H4];
  assume                       d',c' === c,d                            [H5];
  thus ? e . 							        
         Between (c,e,c') /\ Between (d,e,d') /\ c,e === c',e /\ d,e === d',e

  proof
    Between (d',c,b) /\ Between (c',d,b) [X1] by H1, H2, Bsymmetry_THM;
    consider e such that
    Between (c,e,c') /\ Between (d,e,d') [X2] by X1, A7;
    c,d === c,d' [X3] by H3, EquivSymmetric;
    c,c' === c,c' [X4] by EquivReflexive;
    c,d === d',c' by H5, EquivSymmetric;
    d,c' === d',c' by -, H4, EquivTransitive;
    c,d,c' cong c,d',c' by -, X3, X4, cong_DEF;
    d,e === d',e [X5] by -, X2, EquivReflexive, Inner5Segments_THM;
    d,c === c,d [X6] by A1;
    c,d === d,c' by H4, EquivSymmetric;
    d,c === d,c' [X7] by -, X6, EquivTransitive;
    d,d' === d,d'  [X8] by EquivReflexive;
    c,d === d',c' [X9] by H5, EquivSymmetric;
    d',c' === c',d' by A1;
    c,d === c',d' by -, X9, EquivTransitive;
    c,d' === c',d' [X10] by -, H3, EquivTransitive;
    d,d' === d,d' by EquivReflexive;
    d,c,d' cong d,c',d' by -, X7, X8, X10, cong_DEF;
    c,e === c',e by -, X2, EquivReflexive, Inner5Segments_THM;
  qed by -, X2, X5`;;


let FlatNormal_THM = thm `;
  let a b c d d' e be point;
  assume                       Between (b,c,d')                         [H1];
  assume                       Between (d,e,d')                         [H2];
  assume                       c,d' === c,d                             [H3];
  assume                       d,e === d',e                             [H4];
  assume                       ~(c = d)                                 [H5];
  assume                       ~(e = d)                                 [H6];
  thus ? p r q . 						        
         Between (p,r,q) /\ Between (r,c,d') /\ Between (e,c,p) /\      
         r,c,p cong r,c,q /\ r,c === e,c /\ p,r === d,e		        
								        
  proof
    ~(c = d') by H5, H3, EquivSymmetric, A3;
    consider p r such that
    Between (e,c,p) /\ Between (d',c,r) /\ p,r,c cong d',e,c [X1] by
    -, EasyAngleTransport_THM;
    p,r === d',e /\ p,c === d',c /\ r,c === e,c [X2] by -, X1, cong_DEF;
    d',e === d,e by H4, EquivSymmetric;
    p,r === d,e [X3] by -, X2, EquivTransitive;
    ~(p = r) [X4] by -, EquivSymmetric, H6, A3;
    consider q such that
    Between (p,r,q) /\ r,q === e,d [X5] by A4;
    Between (d',e,d) [X6] by H2, Bsymmetry_THM;
    c,p === c,d' by -, X2, CongruenceDoubleSymmetry_THM;
    c,p === c,d [X7] by -, H3, EquivTransitive;
::  Apply SAS to p+crq /\ d'+ced
    c,q=== c,d by X4, X1, X5, X6, A5;
    c,d=== c,q by -, EquivSymmetric;
    c,p=== c,q [X8] by -, X7, EquivTransitive;
    r,c=== r,c [X9] by EquivReflexive;
    r,p=== e,d [X10] by X3, CongruenceDoubleSymmetry_THM;
    e,d=== r,q by X5, EquivSymmetric;
    r,p=== r,q by -, X10, EquivTransitive;
    r,c,p cong r,c,q [X11] by -, X9, X8, cong_DEF;
    Between (r,c,d') [X12] by X1, Bsymmetry_THM;
  qed by -, X5, X11, X12, X2, X1, X3`;;


let EqDist2PointsBetween_THM = thm `;
  let a b c p q be point;
  assume               ~(a = b)						[H1];
  assume               Between (a,b,c)                 			[H2];
  assume               a,p === a,q /\ b,p === b,q      			[H3];
  thus    c,p === c,q

::a & b are equidistant from p & q.  Apply SAS to a+pbc /\ a+qbc.

  proof
    a,b  === a,b /\ b,c === b,c [X1] by EquivReflexive;
    a,b,p cong a,b,q by -, H3, cong_DEF;
    p,c === q,c by H1, -, H2, X1, A5;   
  qed by -, CongruenceDoubleSymmetry_THM`;;


let EqDist2PointsInnerBetween_THM = thm `;
  let a x c p q be point;
  assume      	   Between (a,x,c)					[H1];
  assume 	   a,p === a,q /\ c,p === c,q 				[H2]; 
  thus x,p === x,q

::a and c are equidistant from p and q.  Apply Inner5Segments to
::apb-x /\ aqb-x.

  proof
    a,c === a,c /\ c,x === c,x [X1] by EquivReflexive;
    p,c === q,c by H2, CongruenceDoubleSymmetry_THM;
    a,p,c cong a,q,c by -, H2, X1, cong_DEF;
    p,x === q,x by -, H1, X1, Inner5Segments_THM;   
  qed by -, CongruenceDoubleSymmetry_THM`;;



let Gupta_THM = thm `;
  let a b c d be point;
  assume                                       ~(a = b)                 [H1];
  assume                                       Between (a,b,c)          [H2];
  assume                                       Between (a,b,d)          [H3];
  thus Between (b,d,c) \/ Between (b,c,d)			        
								        
  proof
    cases;
    suppose b = c \/ b = d \/ c = d;
      Between (b,d,c) \/ Between (b,c,d) by -, Baaq_THM, Bqaa_THM;
    qed by -;
    suppose ~(b = c) /\ ~(b = d) /\ ~(c = d) [H4];
      assume ~ (Between (b,d,c)) [H5];
      consider d' such that
      Between (a,c,d') /\ c,d' === c,d [X1] by A4;
      consider c' such that
      Between (a,d,c') /\ d,c' === c,d [X2] by A4;
      is_ordered (a,b,c,d') by H2, X1, B123and134Ordered_THM;
      Between (a,b,d') /\ Between (b,c,d') [X3] by -, is_ordered_DEF;
      is_ordered (a,b,d,c') by H3, X2, B123and134Ordered_THM;
      Between (a,b,c') /\ Between (b,d,c') [X4] by -, is_ordered_DEF;
      ~(c = d') [X5] by X1, H4, A3, EquivSymmetric;
      ~(d = c') [X6] by X2, H4, A3, EquivSymmetric;
      ~(b = d') [X7] by X3, H4, A6;
      ~(b = c') [X8] by X4, H4, A6;

::    In the proof below, we prove a stronger result than
::    BextendToLine_THM with much the same proof.  We find u /\ b'
::    with essentially a,b,c,d',u and a b,d,c',b' ordered 5-tuples
::    with d'u === db /\ cb' === bc. *)
      consider u such that
      Between (c,d',u) /\ d',u === b,d [Y1] by A4;
      is_ordered (b,c,d',u) by X5, X3, Y1, BTransitivityOrdered_THM;
      Between (b,c,u) /\  Between (b,d',u) [Y2] by -, is_ordered_DEF;
      consider b' such that
      Between (d,c',b') /\ c',b' === b,c [Y3] by A4;
      is_ordered (b,d,c',b') by X6, X4, Y3, BTransitivityOrdered_THM;

      Between (b,d,b') /\ Between (b,c',b') [Y4] by -, is_ordered_DEF;
      Between (c',d,b) [Y5] by X4, Bsymmetry_THM;
      d,c' === c',d /\ b,d === d,b [Y6] by A1;
      c,d === d,c' by X2, EquivSymmetric; 
      c,d' === d,c' by -, X1, EquivTransitive;
      c,d' === c',d [Y7] by -, Y6, EquivTransitive;
      d',u === d,b by Y1, Y6, EquivTransitive;
      c,u === c',b [Y8] by -, Y1, Y5, Y7, SegmentAddition_THM;
      c',b' === b',c' /\ b',b === b,b' [Y9] by A1;
      b,c  === c',b' by Y3, EquivSymmetric;
      b,c === b',c' [Y10] by -, Y9, EquivTransitive;
      Between (b',c',b) by Y4, Bsymmetry_THM;
      b,u === b',b by -, Y2, Y10, Y8, SegmentAddition_THM;
      b,u === b,b' [Y11] by -, Y9, EquivTransitive;
      is_ordered (a,b,d',u) [Y12] by X7, X3, Y2, BTransitivityOrdered_THM;
      is_ordered (a,b,c',b') by X8, X4, Y4, BTransitivityOrdered_THM;
      Between (a,b,u) /\ Between (a,b,b') by -, Y12, is_ordered_DEF;
      u = b' [Y13]  by -, H1, Y11, C1_THM;

::    Show c'd' === cd by applying SAS to b+c'cd /\ b'+cc'd.
      c',b === c,b' by Y13, Y8, EquivSymmetric;
      b,c' === b',c [Z1] by -, CongruenceDoubleSymmetry_THM;
      c,c' === c',c by A1;
      b,c,c' cong b',c',c [Z2] by -, Y10, Z1, cong_DEF;
      Between (b',c',d) by Y3, Bsymmetry_THM;
      c',d' === c,d [Z3] by -, H4, Z2, X3, Y7, A5;
      d',c' === c',d' by A1;
      d',c' === c,d by -, Z3, EquivTransitive;   

::    c,d',c',d is a "flat" rhombus.  The diagonals bisect each other.
      consider e such that
      Between (c,e,c') /\ Between (d,e,d') /\ c,e === c',e /\ d,e === d',e
      [Z4] by -, X3, X4, X1, X2, RhombusDiagBisect_THM;

      ~(e = c) [U1]
      proof
        cases;
        suppose ~(e = c);
        qed by -;
        suppose e = c [U2];
          c' = e by U2, Z4, EquivSymmetric, A3;
          c' = c by -, U2;
          Between (b,d,c) [U3] by -, X4;
          F by -, U3, H5;
        qed by -;
      end;

      e = d [V1]
      proof
        cases;
        suppose e = d;
        qed by -;
        suppose ~(e = d) [V2];
          consider p r q such that
          Between (p,r,q) /\ Between (r,c,d') /\ Between (e,c,p) /\
          r,c,p cong r,c,q /\ r,c === e,c /\ p,r === d,e [W1] 
          by X3, Z4, X1, H4, V2, FlatNormal_THM;
          r,p === r,q /\ c,p === c,q [W2] by W1, cong_DEF;
::        r and c are equidistant from p and q, r <> c, Between r,c,d', thus also d'
          ~(c = r) by W1, U1, EquivSymmetric, A3;
          d',p === d',q [W3] by -, W1, W2, EqDist2PointsBetween_THM;

::        c and d' are equidistant from p and q, c <> d', 
::        Between c,d',b', thus also b'.
          Between (c,d',b') by Y1, Y13;
          b',p === b',q [W4] by -, X5, W2, W3, EqDist2PointsBetween_THM; 

::        d' and c are equidistant from p and q, d' <> c, Between d',c,b, thus also b. 
          Between (d',c,b) by X3, Bsymmetry_THM;
          b,p === b,q [W5] by -, X5, W3, W2, EqDist2PointsBetween_THM;  

::        b and b' are equidistant from p and q, Between b,c',b, thus also c'.
          c',p === c',q [W7]by Y4, W4, W5, EqDist2PointsInnerBetween_THM;  

::        c' and c are equidistant from p and q, c' <> c, Between c',c,p, thus also p. 
          Between (c',e,c) by Z4, Bsymmetry_THM;
          is_ordered (c',e,c,p) by -, U1, W1, BTransitivityOrdered_THM;
          Between (c',c,p) [W8] by -, is_ordered_DEF;
          ~(c' = c) by Z4, U1, A6;
          p,p === p,q by -, W8, W7, W2, EqDist2PointsBetween_THM;   

::        Now we deduce a contradiction from p = q.
          q = p by -, EquivSymmetric, A3;
          p = r by -, W1, A6;
          e = d [W9] by -, W1, EquivSymmetric, A3;
          F by -, W9, V2;
        qed by -;
      end;

      d' = e by V1, Z4, EquivSymmetric, A3;
      d' = d by -, V1;
      Between (b,c,d) by -, X3;
    qed by -;
  end`;;


(* Using Gupta's theorem, we prove Hilbert's axiom I3; a line is
   determined by two points. *)

let I1part1_THM = thm `;
  let a b x be point;
  assume                                       ~(a = b)                 [H1];
  assume                                       ~(a = x)                 [H2];
  assume                                       x on_line a,b            [H3];
  thus   ! c . 							        
           c on_line a,b   ==>  c on_line a,x			        

  proof
    let c be point;
    assume c on_line a,b						[H4];
    Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b)		[X1] 
            by H3, Line_DEF;
    Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b)		[X2] 
    	    by H4, Line_DEF;
    x = b \/ b = c \/ (~(x = b) /\ ~(b = c));
    cases by -;
    suppose x = b [Case1];
    qed by -, H4;
    suppose b = c [Case3];
      Between (a,c,x) \/ Between (a,x,c) \/ Between (x,a,c) by -, X1;
      Between (a,c,x) \/ Between (a,x,c) \/ Between (c,a,x) by -, Bsymmetry_THM;
   qed by -, H2, Line_DEF;
    suppose ~(x = b) /\ ~(b = c) [Case2];
      Between (a,x,c) \/ Between (a,c,x) \/ Between (x,a,c)		[P]
      proof
        cases by X1;
        suppose Between (a,b,x)						[Y1];
          cases by X2;
          suppose Between (a,b,c)					[Y11];
            Between (b,x,c) \/ Between (b,c,x) by -, Y1, H1, Gupta_THM;
            is_ordered (a,b,x,c) \/ is_ordered (a,b,c,x) by 
                       Case2, Y1, Y11, -, BTransitivityOrdered_THM;
            Between (a,x,c) \/ Between (a,c,x) by -, is_ordered_DEF;
          qed by -;
          suppose Between (a,c,b);
            is_ordered (a,c,b,x) by -, Y1, B123and134Ordered_THM;
          qed by -, is_ordered_DEF;
          suppose Between (c,a,b);
            is_ordered (c,a,b,x) by H1, -, Y1, BTransitivityOrdered_THM;
            Between (c,a,x) by -, is_ordered_DEF;
          qed by -, Bsymmetry_THM;
        end;
        suppose Between (a,x,b)						[Y2]; 
          cases by X2;
          suppose Between (a,b,c);
            is_ordered (a,x,b,c) by -, Y2, B123and134Ordered_THM;
          qed by -, is_ordered_DEF;
          suppose Between (a,c,b)					[Y22];
            consider m such that
            Between (b,a,m) /\ a,m === a,b [X5] by -, A4;
            ~(a = m) [X6] by H1, X5, EquivSymmetric, A3;
            Between (m,a,b) by X5, Bsymmetry_THM;   :: m,a,c,b  & m,a,x,b
            Between (m,a,c) /\ Between (m,a,x) by -, Y22, Y2, B124and234then123_THM;
            Between (a,c,x) \/ Between (a,x,c) by -, X6, Gupta_THM;
          qed by -;
          suppose Between (c,a,b); 
            Between (c,a,x) by -, Y2, B124and234then123_THM;   :: c,a,x,b 
          qed by -, Bsymmetry_THM;
        end;
        suppose Between (x,a,b)						[Y3];
          cases by X2;
          suppose Between (a,b,c);
            is_ordered (x,a,b,c) by H1, -, Y3, BTransitivityOrdered_THM;
            qed by -, is_ordered_DEF;
          suppose Between (a,c,b);
          qed by Y3, -, B124and234then123_THM;  :: x,a,c,b
          suppose Between (c,a,b);
            Between (b,a,x) /\ Between (b,a,c) by Y3, -, Bsymmetry_THM;
            Between (a,x,c) \/ Between (a,c,x) by -, H1, Gupta_THM;
          qed by -; 
        end;
      end;
      Between (a,x,c) \/ Between (a,c,x) \/ Between (c,a,x) by P, Bsymmetry_THM;
      c on_line a,x by -, H2, Line_DEF;
    qed by -;
  end`;;


let I1part2_THM = thm `;
  let a b x be point;
  assume                       ~(a = b)                                 [H1];
  assume                       ~(a = x)                                 [H2];
  assume                       x on_line a,b                            [H3];
  thus    a,b equal_line a,x					        
								        
  proof
    ! c . c on_line a,b <=> c on_line a,x				[P]
    proof
      let c be point;
      c on_line a,b ==> c on_line a,x					[Imp1]
      proof
        assume c on_line a,b;
        c on_line a,x by -, H1, H2, H3, I1part1_THM;
      qed by -;
      c on_line a,x ==> c on_line a,b					[Imp2]
      proof
        assume c on_line a,x						[H4];
        Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) by H3, Line_DEF;
	Between (a,b,x) \/ Between (a,x,b) \/ Between (b,a,x) by -, Bsymmetry_THM;
        b on_line a,x by -, H2, Line_DEF;
        c on_line a,b by -, H1, H2, H4, I1part1_THM;
      qed by -;
    qed by Imp1, Imp2;
  qed by H1, H2, P, LineEq_DEF`;;


let I1part2_THM = thm `;
  let a b x be point;
  assume                       ~(a = b)                                 [H1];
  assume                       ~(a = x)                                 [H2];
  assume                       x on_line a,b                            [H3];
  thus    a,b equal_line a,x					        

  proof
    Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) by H3, Line_DEF;
    Between (a,b,x) \/ Between (a,x,b) \/ Between (b,a,x) by -, Bsymmetry_THM;
    b on_line a,x [Z1] by -, H2, Line_DEF;
    ! c . c on_line a,b ==> c on_line a,x [Z2] by H1, H2, H3, I1part1_THM;
    ! c . c on_line a,x ==> c on_line a,b [Z3] by H1, H2, Z1, I1part1_THM;
    ! c . c on_line a,x <=> c on_line a,b by Z2, Z3;
  qed by H1, H2, -, LineEq_DEF`;;


let LineEqRefl_THM = thm `;
  let a b be point;
  assume                       ~(a = b)					[H1];
  thus     a,b equal_line a,b

  proof
    ! c . c on_line a,b  <=>  c on_line a,b;
    a,b equal_line a,b by -, H1, LineEq_DEF;
  qed by -`;;


let LineEqA1_THM = thm `;
  let a b be point;
  assume                       ~(a = b)					[H1];
  thus    a,b equal_line b,a

  proof
    ! c . c on_line a,b  <=>  c on_line b,a				[P]
    proof
    let c be point;
      c on_line a,b ==> c on_line b,a					[Imp1]
      proof
        assume c on_line a,b;
        Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b) by -, Line_DEF;
        Between (c,b,a) \/ Between (b,c,a) \/ Between (b,a,c) by -, Bsymmetry_THM;
      qed by -, H1, Line_DEF;
      c on_line b,a ==> c on_line a,b					[Imp2]
      proof
        assume c on_line b,a [H3];
        Between (b,a,c) \/  Between (b,c,a) \/ Between (c,b,a) by -, Line_DEF;
        Between (c,a,b) \/  Between (a,c,b) \/ Between (a,b,c) by -, Bsymmetry_THM;
      qed by -, H1, Line_DEF;
    qed by Imp1, Imp2;
  qed by H1, P, LineEq_DEF`;;


let LineEqSymmetric_THM = thm `;
  let a b c d be point;
  assume                       ~(a = b) /\ ~(c = d)			[H1];
  assume                       a,b equal_line c,d                      	[H2];
  thus   c,d equal_line a,b

  proof
    ! x . x on_line a,b  <=>  x on_line c,d by H2, LineEq_DEF;
    ! x . x on_line c,d <=>  x on_line a,b by -;
    c,d equal_line a,b by -, H1, LineEq_DEF;
  qed by -`;;


let LineEqTrans_THM = thm `;
  let a b c d e f be point;
  assume                       ~(a = b) /\ ~(c = d) /\ ~(e = f)         [H1];
  assume                       a,b equal_line c,d                       [H2];
  assume                       c,d equal_line e,f                       [H3];
  thus   a,b equal_line e,f					        
								        
  proof
    (! y . y on_line a,b  <=>  y on_line c,d)  /\ 
    (! y . y on_line c,d  <=>  y on_line e,f)     [X2] by H2, H3, LineEq_DEF;
    (! y . y on_line a,b  <=>  y on_line e,f) by -;
  qed by -, H1, LineEq_DEF`;;


let onlineEq_THM = thm `;
  let a b c d x be point;
  assume               ~(a = b) /\ ~(c = d)                             [H1];
  assume               x on_line a,b                                    [H2];
  assume               a,b equal_line c,d                               [H3];
  thus   x on_line c,d						        
								        
  proof
    ! y . y on_line a,b <=> y on_line c,d by -, LineEq_DEF;
  qed by -, H2`;;


let I1part2Reverse_THM = thm `;
  let a b y be point;
  assume                       ~(a = b) /\ ~(b = y)			[H1];
  assume                       y on_line a,b                           	[H3];
  thus    a,b equal_line y,b

  proof
    a,b equal_line b,a /\ b,y equal_line y,b [Y1] by H1, LineEqA1_THM;
    y on_line b,a by H3, Y1, onlineEq_THM;
    b,a equal_line b,y by -, H1, Y1, I1part2_THM;
    a,b equal_line b,y by -, H1, Y1, LineEqTrans_THM;
    a,b equal_line y,b by -, H1, Y1, LineEqTrans_THM;
  qed by -`;;


let I1_THM = thm `;
  let a b x y be point;
  assume			~(a = b)				[H1];
  assume			~(x = y)				[H2];
  assume   			a on_line x,y 				[H3];
  assume   			b on_line x,y				[H4];
  thus   x,y equal_line a,b

  proof
    cases;
    suppose (x = b)							[H5];
      ~(b = y) [P1] by -, H2;
      b,a equal_line a,b [P2] by H1, LineEqA1_THM;
      x,y equal_line b,y [P3] by H2, H5, LineEqRefl_THM;
      a on_line b,y by H3, H5;
      b,y equal_line b,a by -, P1, H1, I1part2_THM;
      x,y equal_line b,a by -, H1, H2, P1, P3, LineEqTrans_THM;
    qed by -, H1, H2, P2, LineEqTrans_THM;
    suppose
      ~(x = b)								[H6];
      x,y equal_line x,b [P4] by -, H2, H6, H4, I1part2_THM;
      a on_line x,b by -, H2, H6, H3, onlineEq_THM;
      x,b equal_line a,b by -, H6, H1, I1part2Reverse_THM;   
    qed by H1, H2, H6, P4, -, LineEqTrans_THM;
  end`;;
*}

locale tarski_first7 =
  fixes Cong :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool"  ("_ _ \<doteq> _ _" [1000, 1000, 1000, 1000] 50)
  fixes Cong3  ("_ _ _ \<doteq>\<doteq> _ _ _" [1000, 1000, 1000, 1000, 1000, 1000] 50)
  defines "a b c \<doteq>\<doteq> x y z \<equiv> a b \<doteq> x y \<and> a c \<doteq> x z \<and> b c \<doteq> y z"
  fixes Bet :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool"
  assumes A1: "a b \<doteq> b a"
    and A2: "a b \<doteq> p q \<Longrightarrow> a b \<doteq> r s \<Longrightarrow> p q \<doteq> r s"
    and A3: "a b \<doteq> c c \<Longrightarrow> a = b"
    and A4: "\<exists>x. Bet q a x \<and> a x \<doteq> b c"
    and A5: "a \<noteq> b \<Longrightarrow> Bet a b c \<Longrightarrow> Bet a' b' c' \<Longrightarrow> a b c \<doteq>\<doteq> a' b' c' \<Longrightarrow>
      b d \<doteq> b' d' \<Longrightarrow> c d \<doteq> c' d'"
    and A6: "Bet a b a \<Longrightarrow> a = b"
    and A7: "Bet a p c \<Longrightarrow> Bet b q c \<Longrightarrow> \<exists>x. Bet p x b \<and> Bet q x a"
begin


definition "is_ordered a b c d \<longleftrightarrow>
  Bet a b c \<and> Bet a b d \<and> Bet a c d \<and> Bet b c d"

definition on_line  ("_ on'_line _ _" [1000, 1000, 1000] 50)
  where "x on_line a b \<longleftrightarrow>
    a \<noteq> b \<and> (Bet a b x \<or> Bet a x b \<or> Bet x a b)"

definition equal_line  (" _ _ equal'_line _ _" [1000, 1000, 1000, 1000] 50)
  where "a b equal_line x y \<longleftrightarrow>
    a \<noteq> b \<and> x \<noteq> y \<and> (\<forall>c. c on_line a b \<longleftrightarrow> c on_line x y)"


lemma A4_rule: obtains x where "Bet q a x" and "a x \<doteq> b c"
  using A4 by blast

lemma A7_rule:
  assumes "Bet a p c" and "Bet b q c"
  obtains x where "Bet p x b" and "Bet q x a"
  using assms and A7 by blast


lemma Cong_refl [intro, simp]:
  "a b \<doteq> a b"
proof -
  have "b a \<doteq> a b" by (rule A1)
  from this this show ?thesis by (rule A2)
qed

lemma Cong_sym [sym]:
  assumes "a b \<doteq> c d"
  shows "c d \<doteq> a b"
proof -
  have "a b \<doteq> a b" ..
  with assms show ?thesis by (rule A2)
qed

lemma Cong_trans [trans]:
  assumes "p q \<doteq> a b"
    and "a b \<doteq> r s"
  shows "p q \<doteq> r s"
proof -
  from `p q \<doteq> a b` [symmetric] and `a b \<doteq> r s`
  show ?thesis by (rule A2)
qed


lemma Cong3I:
  assumes "a b \<doteq> x y" and "a c \<doteq> x z" and "b c \<doteq> y z"
  shows "a b c \<doteq>\<doteq> x y z"
  using assms unfolding Cong3_def by blast

lemma Cong3E:
  assumes "a b c \<doteq>\<doteq> x y z"
  obtains "a b \<doteq> x y" and "a c \<doteq> x z" "b c \<doteq> y z"
  using assms unfolding Cong3_def by blast

lemma Cong3_refl [intro, simp]:
  "a b c \<doteq>\<doteq> a b c"
  by (blast intro: Cong3I)


lemma Bet_aaa:
  "Bet a a a" and "a a \<doteq> b b"
proof -
  obtain x where x: "Bet a a x" "a x \<doteq> b b" by (rule A4_rule)
  from x(2) have "a = x" by (rule A3)
  from this [symmetric] and x show "Bet a a a" and "a a \<doteq> b b" by simp_all
qed

lemma Bqaa: "Bet q a a"
proof -
  obtain x where x: "Bet q a x" "a x \<doteq> a a" by (rule A4_rule)
  note `Bet q a x`
  also have [symmetric]: "a = x" using `a x \<doteq> a a` by (rule A3)
  finally show ?thesis .
qed


lemma C1:
  assumes neq: "a \<noteq> b"
    and Bet: "Bet a b y"
(*  and "Bet a b x"    -- "FIXME unused"  *)
    and "b x \<doteq> b y"
  shows "y = x"
proof -
  have 1: "a b \<doteq> a b" ..
  have 2: "b y \<doteq> b y" ..
  have "a b y \<doteq>\<doteq> a b y" ..
  with neq Bet Bet have "y x \<doteq> y y" using `b x \<doteq> b y` by (rule A5)
  then show ?thesis by (rule A3)
qed

end

