(* ========================================================================= *)
(* Independence of the parallel postulate. The statement and some ideas are  *)
(* taken from Tim Makarios's MSc thesis "A mechanical verification of the    *)
(* independence of Tarski's Euclidean axiom".                                *)
(*                                                                           *)
(* In the file Multivariate/tarski.ml it is shown that all 11 of Tarski's    *)
(* axioms for geometry hold for the Euclidean plane `:real^2`, with          *)
(* betweenness and congruence of segments as:                                *)
(*                                                                           *)
(*      B x y z  <=> between y (x,z)                                         *)
(*      ab == pq <=> dist(a,b) = dist(p,q)                                   *)
(*                                                                           *)
(* The present file shows that the Klein model of the hyperbolic plane (type *)
(* `:plane`) satisfies all Tarski's axioms except that it satisfies the      *)
(* negation of the Euclidean axiom (10), with betweenness and congruence of  *)
(* segments as:                                                              *)
(*                                                                           *)
(*      B x y z  <=> pbetween y (x,z)                                        *)
(*      ab == pq <=> pdist(a,b) = pdist(p,q)                                 *)
(*                                                                           *)
(* Collectively, these two results show that the Euclidean axiom is          *)
(* independent of the others. For more references regarding Tarski's axioms  *)
(* for geometry see "http://en.wikipedia.org/wiki/Tarski's_axioms".          *)
(* ========================================================================= *)

needs "Multivariate/tarski.ml";;
needs "Multivariate/cauchy.ml";;

(* ------------------------------------------------------------------------- *)
(* The semimetric we will use, directly on real^N first. Choose a sensible   *)
(* default outside unit ball so some handy theorems become unconditional.    *)
(* ------------------------------------------------------------------------- *)


let mdist = new_definition
 `mdist(x:real^N,y:real^N) =
    if norm(x) < &1 /\ norm(y) < &1 then
     (&1 - x dot y) pow 2 / ((&1 - norm(x) pow 2) * (&1 - norm(y) pow 2)) - &1
    else dist(x,y)`;;


let MDIST_INCREASES_ONLINE = 
prove
 (`!a b x:real^N.
      norm a < &1 /\ norm b < &1 /\ norm x < &1 /\ between x (a,b) /\ ~(x = b)
      ==> mdist(a,x) < mdist(a,b)`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `b:real^N = a` THENL
   [ASM_MESON_TAC[BETWEEN_REFL_EQ]; ALL_TAC] THEN
  ASM_SIMP_TAC[mdist; real_div; REAL_INV_MUL] THEN
  SUBGOAL_THEN
   `norm(a:real^N) pow 2 < &1 /\ norm(b:real^N) pow 2 < &1 /\
    norm(x:real^N) pow 2 < &1`
  MP_TAC THENL [ASM_SIMP_TAC[ABS_SQUARE_LT_1; REAL_ABS_NORM]; ALL_TAC] THEN
  REWRITE_TAC[REAL_ARITH `a * inv x * inv b - &1 < c * inv x * d - &1 <=>
                          (a / b) / x < (c * d) / x`] THEN
  SIMP_TAC[REAL_LT_DIV2_EQ; REAL_LT_LDIV_EQ; REAL_SUB_LT] THEN
  ONCE_REWRITE_TAC[REAL_ARITH `(a * inv b) * c:real = (a * c) / b`] THEN
  SIMP_TAC[REAL_LT_RDIV_EQ; REAL_SUB_LT] THEN
  SUBGOAL_THEN `(a:real^N) dot b < &1 /\ (a:real^N) dot x < &1` MP_TAC THENL
   [CONJ_TAC THEN MATCH_MP_TAC(MESON[REAL_LET_TRANS; NORM_CAUCHY_SCHWARZ]
     `norm(x) * norm(y) < &1 ==> (x:real^N) dot y < &1`) THEN
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
    MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[NORM_POS_LE];
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BETWEEN_IN_SEGMENT]) THEN
  REWRITE_TAC[IN_SEGMENT; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `u:real` THEN
  ASM_CASES_TAC `u = &1` THEN
  ASM_SIMP_TAC[VECTOR_ARITH `(&1 - &1) % a + &1 % b:real^N = b`] THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  SIMP_TAC[VECTOR_ARITH `(&1 - u) % a + u % b:real^N = a + u % (b - a)`] THEN
  ABBREV_TAC `c:real^N = b - a` THEN
  SUBGOAL_THEN `b:real^N = a + c` SUBST_ALL_TAC THENL
   [EXPAND_TAC "c" THEN VECTOR_ARITH_TAC; ALL_TAC] THEN
  RULE_ASSUM_TAC(SIMP_RULE[VECTOR_ARITH `a + c:real^N = a <=> c = vec 0`]) THEN
  REWRITE_TAC[NORM_POW_2; VECTOR_ARITH
    `(a + b:real^N) dot (a + b) = a dot a + &2 * a dot b + b dot b`] THEN
  REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN REWRITE_TAC[DOT_LMUL] THEN
  REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH
   `(&1 - (a + x * b)) pow 2 * (&1 - (a + &2 * b + c)) <
    (&1 - (a + b)) pow 2 * (&1 - (a + &2 * x * b + x * x * c)) <=>
    &0 < (&1 - a - b * x) * ((&1 - a) * c + b pow 2) * (&1 - x) +
         (&1 - a - b) * ((&1 - a) * c + b pow 2) * (&1 - x) * x`] THEN
  MATCH_MP_TAC REAL_LTE_ADD THEN CONJ_TAC THENL
   [REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC);
    REPEAT(MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC)] THEN
  TRY ASM_REAL_ARITH_TAC THEN TRY(MATCH_MP_TAC REAL_LT_IMP_LE) THEN
  MATCH_MP_TAC REAL_LTE_ADD THEN REWRITE_TAC[REAL_LE_POW_2] THEN
  MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[DOT_POS_LT; REAL_SUB_LT]);;


let MDIST_REFL = 
prove
 (`!x:real^N. mdist(x,x) = &0`,

  GEN_TAC THEN REWRITE_TAC[mdist; DIST_REFL; NORM_POW_2; NORM_LT_SQUARE] THEN
  CONV_TAC REAL_FIELD);;


let MDIST_SYM = 
prove
 (`!x y:real^N. mdist(x,y) = mdist(y,x)`,

  REWRITE_TAC[mdist; CONJ_ACI; REAL_MUL_AC; DIST_SYM; DOT_SYM]);;


let MDIST_POS_LT = 
prove
 (`!x y:real^N. ~(x = y) ==> &0 < mdist(x,y)`,

  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `norm(x:real^N) < &1 /\ norm(y:real^N) < &1` THENL
   [ASM_MESON_TAC[MDIST_INCREASES_ONLINE; MDIST_REFL; BETWEEN_REFL];
    ASM_SIMP_TAC[mdist; DIST_POS_LT]]);;


let MDIST_POS_LE = 
prove
 (`!x y:real^N. &0 <= mdist(x,y)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `x:real^N = y` THEN
  ASM_SIMP_TAC[MDIST_REFL; MDIST_POS_LT; REAL_LE_LT]);;


let MDIST_EQ_0 = 
prove
 (`!x y:real^N. mdist(x,y) = &0 <=> x = y`,


let BETWEEN_COLLINEAR_MDIST_EQ = 
prove
 (`!a b x:real^N.
        norm(a) < &1 /\ norm(b) < &1 /\ norm(x) < &1
        ==> (between x (a,b) <=>
             collinear {a, x, b} /\
             mdist(x,a) <= mdist (a,b) /\ mdist(x,b) <= mdist(a,b))`,

  REPEAT GEN_TAC THEN STRIP_TAC THEN EQ_TAC THENL
   [SIMP_TAC[BETWEEN_IMP_COLLINEAR];
    REWRITE_TAC[COLLINEAR_BETWEEN_CASES]] THEN
  ASM_MESON_TAC[MDIST_INCREASES_ONLINE; MDIST_SYM; REAL_LT_IMP_LE;
                REAL_LE_REFL; BETWEEN_SYM; REAL_NOT_LE; BETWEEN_REFL]);;


let CONTINUOUS_AT_LIFT_MDIST = 
prove
 (`!a x:real^N.
      norm(a) < &1 /\ norm(x) < &1 ==> (\x. lift(mdist(a,x))) continuous at x`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_TRANSFORM_AT THEN EXISTS_TAC
   `\x:real^N. lift((&1 - a dot x) pow 2 /
                    ((&1 - norm a pow 2) * (&1 - norm x pow 2)) - &1)` THEN
  EXISTS_TAC `&1 - norm(x:real^N)` THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
  CONJ_TAC THENL
   [X_GEN_TAC `y:real^N` THEN DISCH_THEN(MP_TAC o MATCH_MP (NORM_ARITH
    `dist(y,x) < &1 - norm x ==> norm y < &1`)) THEN ASM_SIMP_TAC[mdist];
    REWRITE_TAC[LIFT_SUB; real_div; LIFT_CMUL; REAL_INV_MUL] THEN
    MATCH_MP_TAC CONTINUOUS_SUB THEN SIMP_TAC[CONTINUOUS_CONST] THEN
    REPEAT(MATCH_MP_TAC CONTINUOUS_MUL THEN CONJ_TAC) THEN
    SIMP_TAC[CONTINUOUS_CONST; o_DEF; REAL_POW_2; LIFT_CMUL] THENL
     [MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_MUL);
      MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_AT_INV)] THEN
    ASM_SIMP_TAC[REAL_ARITH `x < &1 * &1 ==> ~(&1 - x = &0)`; REAL_LT_MUL2;
                 NORM_POS_LE; LIFT_SUB] THEN
    SIMP_TAC[GSYM REAL_POW_2; NORM_POW_2; CONTINUOUS_CONST; CONTINUOUS_AT_ID;
             CONTINUOUS_SUB; CONTINUOUS_LIFT_DOT2]]);;


let HYPERBOLIC_MIDPOINT = 
prove
 (`!a b:real^N.
        norm a < &1 /\ norm b < &1
        ==> ?x. between x (a,b) /\ mdist(x,a) = mdist(x,b)`,

  REPEAT STRIP_TAC THEN MP_TAC(ISPECL
   [`\x:real^N. lift(mdist(x,a) - mdist(x,b))`; `segment[a:real^N,b]`]
     CONNECTED_CONTINUOUS_IMAGE) THEN
  ANTS_TAC THENL
   [REWRITE_TAC[CONNECTED_SEGMENT; LIFT_SUB] THEN
    MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC CONTINUOUS_SUB THEN ONCE_REWRITE_TAC[MDIST_SYM] THEN
    CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_AT_LIFT_MDIST THEN
    ASM_MESON_TAC[BETWEEN_NORM_LT; BETWEEN_IN_SEGMENT];
    REWRITE_TAC[GSYM IS_INTERVAL_CONNECTED_1; IS_INTERVAL_1] THEN
    REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
    REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM; LIFT_DROP] THEN
    DISCH_THEN(MP_TAC o SPECL [`a:real^N`; `b:real^N`; `lift(&0)`]) THEN
    ASM_SIMP_TAC[MDIST_REFL; LIFT_DROP; ENDS_IN_SEGMENT; IN_IMAGE] THEN
    REWRITE_TAC[REAL_SUB_RZERO; REAL_ARITH `&0 - x <= &0 <=> &0 <= x`] THEN
    ASM_SIMP_TAC[MDIST_POS_LE; LIFT_EQ; BETWEEN_IN_SEGMENT] THEN
    ASM_MESON_TAC[REAL_SUB_0; MDIST_SYM]]);;


let MDIST_EQ_ORIGIN = 
prove
 (`!x:real^N y:real^N.
        norm x < &1 /\ norm y < &1
        ==> (mdist(vec 0,x) = mdist(vec 0,y) <=> norm x = norm y)`,

  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[mdist; NORM_0; REAL_LT_01] THEN
  REWRITE_TAC[DOT_LZERO] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  REWRITE_TAC[real_div; REAL_MUL_LID; REAL_EQ_INV2;
              REAL_ARITH `x - &1 = y - &1 <=> x = y`] THEN
  REWRITE_TAC[REAL_ARITH `&1 - x = &1 - y <=> x = y`;
              GSYM REAL_EQ_SQUARE_ABS; REAL_ABS_NORM]);;


let MDIST_CONGRUENT_TRIPLES_0 = 
prove
 (`!a b:real^N a' b':real^N.
        norm a < &1 /\ norm b < &1 /\ norm a' < &1 /\ norm b' < &1
        ==> (mdist(vec 0,a) = mdist(vec 0,a') /\ mdist(a,b) = mdist(a',b') /\
             mdist(b,vec 0) = mdist(b',vec 0) <=>
             dist(vec 0,a) = dist(vec 0,a') /\ dist(a,b) = dist(a',b') /\
             dist(b,vec 0) = dist(b',vec 0))`,

  REPEAT STRIP_TAC THEN
  ASM_SIMP_TAC[MDIST_EQ_ORIGIN; REWRITE_RULE[MDIST_SYM] MDIST_EQ_ORIGIN] THEN
  REWRITE_TAC[DIST_0; NORM_0; REAL_LT_01] THEN MATCH_MP_TAC(TAUT
   `(a /\ b ==> (x <=> y)) ==> (a /\ x /\ b <=> a /\ y /\ b)`) THEN
  STRIP_TAC THEN ASM_SIMP_TAC[mdist; DIST_EQ; real_div; REAL_INV_MUL; REAL_RING
   `x * a * b - &1 = y * a * b - &1 <=> x = y \/ a = &0 \/ b = &0`] THEN
  REWRITE_TAC[dist; NORM_POW_2; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
  REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS; NORM_POW_2] THEN
  ASM_SIMP_TAC[REAL_INV_EQ_0; real_abs; REAL_SUB_LE; REAL_SUB_0] THEN
  ASM_SIMP_TAC[ABS_SQUARE_LT_1; REAL_ABS_NORM; REAL_LT_IMP_NE; REAL_LT_IMP_LE;
               MESON[NORM_CAUCHY_SCHWARZ; REAL_LET_TRANS; NORM_POS_LE;
                     REAL_LT_MUL2; REAL_MUL_RID; REAL_LT_IMP_LE]
                `norm x < &1 /\ norm y < &1 ==> x dot y < &1`] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[NORM_EQ]) THEN ASM_REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Deduce existence of hyperbolic translations via the Poincare disc model.  *)
(* Use orthogonal projection onto a hemisphere touching the unit disc,       *)
(* then stereographic projection back from the other pole of the sphere plus *)
(* scaling. See Greenberg's "Euclidean & Non-Euclidean Geometries" fig 7.13. *)
(* ------------------------------------------------------------------------- *)


let kleinify = new_definition
 `kleinify z = Cx(&2 / (&1 + norm(z) pow 2)) * z`;;


let poincarify = new_definition
 `poincarify x = Cx((&1 - sqrt(&1 - norm(x) pow 2)) / norm(x) pow 2) * x`;;

let KLEINIFY_0,POINCARIFY_0 = (CONJ_PAIR o prove)
 (`kleinify (Cx(&0)) = Cx(&0) /\ poincarify (Cx(&0)) = Cx(&0)`,
  REWRITE_TAC[kleinify; poincarify; COMPLEX_MUL_RZERO]);;


let NORM_KLEINIFY = 
prove
 (`!z. norm(kleinify z) = (&2 * norm(z)) / (&1 + norm(z) pow 2)`,

  REWRITE_TAC[kleinify; COMPLEX_NORM_MUL; COMPLEX_NORM_CX; REAL_ABS_DIV] THEN
  SIMP_TAC[REAL_LE_POW_2; REAL_ARITH `&0 <= x ==> abs(&1 + x) = &1 + x`] THEN
  REAL_ARITH_TAC);;


let NORM_KLEINIFY_LT = 
prove
 (`!z. norm(kleinify z) < &1 <=> ~(norm z = &1)`,

  ASM_SIMP_TAC[NORM_KLEINIFY; REAL_LE_POW_2; REAL_LT_LDIV_EQ; REAL_MUL_LID;
                REAL_ARITH `&0 <= x ==> &0 < &1 + x`] THEN
  SIMP_TAC[REAL_ARITH `&2 * z < (&1 + z pow 2) <=> &0 < (z - &1) pow 2`] THEN
  REWRITE_TAC[REAL_POW_2; REAL_LT_SQUARE] THEN REAL_ARITH_TAC);;


let NORM_POINCARIFY_LT = 
prove
 (`!x. norm(x) < &1 ==> norm(poincarify x) < &1`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[poincarify; COMPLEX_NORM_MUL] THEN
  MATCH_MP_TAC(REAL_ARITH `x * y <= &1 * y /\ y < &1 ==> x * y < &1`) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
  REWRITE_TAC[NORM_POS_LE; COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
  REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_POW] THEN
  ASM_CASES_TAC `x:real^2 = vec 0` THEN
  ASM_SIMP_TAC[REAL_LE_LDIV_EQ; NORM_POS_LT; REAL_POW_LT; NORM_0] THENL
   [REAL_ARITH_TAC; REWRITE_TAC[REAL_MUL_LID]] THEN
  MATCH_MP_TAC(REAL_ARITH `s <= &1 /\ &1 - x <= s ==> abs(&1 - s) <= x`) THEN
  CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LSQRT; MATCH_MP_TAC REAL_LE_RSQRT] THEN
  REWRITE_TAC[REAL_SUB_LE; REAL_POS; REAL_MUL_LID; REAL_POW_ONE] THEN
  ASM_SIMP_TAC[REAL_ARITH `(&1 - x) pow 2 <= &1 - x <=> &0 <= x * (&1 - x)`;
   REAL_ARITH `&1 - x <= &1 <=> &0 <= x`; REAL_LE_MUL; REAL_POW_LE;
   REAL_SUB_LE; ABS_SQUARE_LE_1; REAL_LT_IMP_LE; REAL_ABS_NORM; NORM_POS_LE]);;


let KLEINIFY_POINCARIFY = 
prove
 (`!x. norm(x) < &1 ==> kleinify(poincarify x) = x`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[kleinify; poincarify] THEN MATCH_MP_TAC
    (COMPLEX_RING `(~(x = Cx(&0)) ==> w * z = Cx(&1)) ==> w * z * x = x`) THEN
  DISCH_TAC THEN REWRITE_TAC[GSYM CX_MUL; CX_INJ; COMPLEX_NORM_MUL] THEN
  REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_POW] THEN
  ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
   `~(y = &0)
    ==> (&1 + (a / y pow 2 * y) pow 2) = (y pow 2 + a pow 2) / y pow 2`] THEN
  REWRITE_TAC[REAL_POW2_ABS; real_div; REAL_INV_MUL; REAL_INV_INV] THEN
  ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
   `~(y = &0) ==> (&2 * x * y pow 2) * z * inv(y pow 2) = &2 * x * z`] THEN
  MATCH_MP_TAC(REAL_FIELD `&0 < y /\ &2 * y = x ==> &2 * inv(x) * y = &1`) THEN
  CONJ_TAC THENL
   [REWRITE_TAC[REAL_SUB_LT] THEN MATCH_MP_TAC REAL_LT_LSQRT THEN
    REWRITE_TAC[REAL_POS; REAL_ARITH `&1 - x < &1 pow 2 <=> &0 < x`] THEN
    ASM_SIMP_TAC[REAL_POW_LT; COMPLEX_NORM_NZ];
    SUBGOAL_THEN `sqrt(&1 - norm(x:real^2) pow 2) pow 2 = &1 - norm x pow 2`
    MP_TAC THENL [MATCH_MP_TAC SQRT_POW_2; CONV_TAC REAL_FIELD]] THEN
  ASM_SIMP_TAC[REAL_SUB_LE; ABS_SQUARE_LE_1; REAL_ABS_NORM; REAL_LT_IMP_LE]);;


let POINCARIFY_KLEINIFY = 
prove
 (`!x. norm(x) < &1 ==> poincarify(kleinify x) = x`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[kleinify; poincarify] THEN
  MATCH_MP_TAC(COMPLEX_RING
   `(~(x = Cx(&0)) ==> w * z = Cx(&1)) ==> w * z * x = x`) THEN
  DISCH_TAC THEN REWRITE_TAC[GSYM CX_MUL; CX_INJ] THEN
  REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
  REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_POW; REAL_ABS_NUM] THEN
  REWRITE_TAC[real_div; REAL_INV_MUL; REAL_INV_INV; GSYM REAL_MUL_ASSOC;
              REAL_INV_POW; REAL_POW_MUL] THEN
  MATCH_MP_TAC(REAL_FIELD
   `~(c = &0) /\ abs d < &1 /\ a * b = &2 * c pow 2 * (&1 + d)
    ==> a * inv(&2) pow 2 * b * inv(c) pow 2 * &2 * inv(&1 + d) = &1`) THEN
  ASM_REWRITE_TAC[REAL_ABS_POW; COMPLEX_NORM_ZERO; ABS_SQUARE_LT_1] THEN
  ASM_SIMP_TAC[REAL_ABS_NORM; REAL_POW_LE; NORM_POS_LE; REAL_ARITH
   `&0 <= x ==> abs(&1 + x) = &1 + x`] THEN
  MATCH_MP_TAC(REAL_FIELD
   `~(x = &0) /\ abs x < &1 /\ a = &2 * x / (&1 + x)
    ==> a * (&1 + x) pow 2 = &2 * x * (&1 + x)`) THEN
  ASM_REWRITE_TAC[REAL_ABS_NORM; COMPLEX_NORM_ZERO; REAL_ABS_POW;
                  ABS_SQUARE_LT_1; REAL_POW_EQ_0] THEN
  MATCH_MP_TAC(REAL_ARITH `x = &1 - y ==> &1 - x = y`) THEN
  MATCH_MP_TAC SQRT_UNIQUE THEN
  REWRITE_TAC[REAL_ARITH `&0 <= &1 - &2 * x / y <=> (&2 * x) / y <= &1`] THEN
  SIMP_TAC[REAL_LE_LDIV_EQ; REAL_POW_LE; NORM_POS_LE; REAL_ARITH
   `&0 <= x ==> &0 < &1 + x`] THEN
  REWRITE_TAC[REAL_ARITH `&2 * x <= &1 * (&1 + x) <=> x <= &1`] THEN
  ASM_SIMP_TAC[ABS_SQUARE_LE_1; REAL_ABS_NORM; REAL_LT_IMP_LE] THEN
  SUBGOAL_THEN `~(&1 + norm(x:complex) pow 2 = &0)` MP_TAC THENL
   [ALL_TAC; CONV_TAC REAL_FIELD] THEN
  MATCH_MP_TAC(REAL_ARITH `abs(x) < &1 ==> ~(&1 + x = &0)`) THEN
  ASM_REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NORM; ABS_SQUARE_LT_1]);;


let MDIST_KLEINIFY = 
prove
 (`!w z. ~(norm w = &1) /\ ~(norm z = &1)
         ==> mdist(kleinify w,kleinify z) =
             &4 * (&1 / &2 + norm(w - z) pow 2 /
                             ((&1 - norm w pow 2) * (&1 - norm z pow 2))) pow 2
             - &1`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
   `(&4 * norm(w - z:real^2) pow 2 *
     ((&1 - norm w pow 2) * (&1 - norm z pow 2) + norm(w - z) pow 2)) /
    ((&1 - norm w pow 2) pow 2 * (&1 - norm z pow 2) pow 2)` THEN
  CONJ_TAC THENL
   [ASM_SIMP_TAC[mdist; NORM_KLEINIFY_LT] THEN MATCH_MP_TAC(REAL_FIELD
     `~(y = &0) /\ z = (w + &1) * y ==> z / y - &1 = w`) THEN
    CONJ_TAC THENL
     [REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN CONJ_TAC THEN
      MATCH_MP_TAC (REAL_ARITH `x < &1 ==> ~(&1 - x = &0)`) THEN
      ASM_SIMP_TAC[REAL_POW_1_LT; NORM_KLEINIFY_LT; NORM_POS_LE; ARITH];
      REWRITE_TAC[kleinify; COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
      REWRITE_TAC[GSYM COMPLEX_CMUL; DOT_LMUL] THEN REWRITE_TAC[DOT_RMUL] THEN
      SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NUM; REAL_POW_LE; NORM_POS_LE;
               REAL_ARITH `&0 <= x ==> abs(&1 + x) = &1 + x`] THEN
      MATCH_MP_TAC(REAL_FIELD
       `(~(y' = &0) /\ ~(y = &0)) /\
        (y * y' - &4 * d) pow 2 =
        b * (y pow 2 - &4 * x pow 2) * (y' pow 2 - &4 * x' pow 2)
        ==> (&1 - &2 / y * &2 / y' * d) pow 2 =
            b * (&1 - (&2 / y * x) pow 2) * (&1 - (&2 / y' * x') pow 2)`) THEN
      CONJ_TAC THENL
       [CONJ_TAC THEN
        MATCH_MP_TAC(REAL_ARITH `~(abs x = &1) ==> ~(&1 + x = &0)`) THEN
        ASM_SIMP_TAC[REAL_ABS_POW; REAL_POW_EQ_1; REAL_ABS_NORM] THEN ARITH_TAC;
        REWRITE_TAC[REAL_RING `(&1 + x) pow 2 - &4 * x = (&1 - x) pow 2`] THEN
        MATCH_MP_TAC(REAL_FIELD
         `(~(y = &0) /\ ~(y' = &0)) /\ a - y * y' = b
          ==> a = (b / (y * y') + &1) * y * y'`) THEN
        CONJ_TAC THENL
         [ASM_REWRITE_TAC[REAL_POW_EQ_0; REAL_POW_EQ_1; REAL_ABS_NORM; ARITH;
                          REAL_ARITH `&1 - x = &0 <=> x = &1`];
          REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
          REAL_ARITH_TAC]]];
    REPEAT(POP_ASSUM MP_TAC) THEN
    REWRITE_TAC[NORM_EQ_SQUARE; GSYM NORM_POW_2] THEN CONV_TAC REAL_FIELD]);;


let MDIST_KLEINIFY_EQ = 
prove
 (`!w z w' z'.
      ~(norm w = &1) /\ ~(norm z = &1) /\ ~(norm w' = &1) /\ ~(norm z' = &1) /\
      norm(w - z) pow 2 * (&1 - norm w' pow 2) * (&1 - norm z' pow 2) =
      norm(w' - z') pow 2 * (&1 - norm w pow 2) * (&1 - norm z pow 2)
      ==> mdist(kleinify w,kleinify z) = mdist(kleinify w',kleinify z')`,

  SIMP_TAC[MDIST_KLEINIFY; NORM_EQ_SQUARE; GSYM NORM_POW_2; REAL_POS] THEN
  CONV_TAC REAL_FIELD);;


let NORM_KLEINIFY_MOEBIUS_LT = 
prove
 (`!w x. norm w < &1 /\ norm x < &1
         ==> norm(kleinify(moebius_function (&0) w x)) < &1`,


let MDIST_KLEINIFY_MOEBIUS = 
prove
 (`!w x y. norm w < &1 /\ norm x < &1 /\ norm y < &1
           ==> mdist(kleinify(moebius_function (&0) w x),
                     kleinify(moebius_function (&0) w y)) =
               mdist(kleinify x,kleinify y)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC MDIST_KLEINIFY_EQ THEN
  ASM_SIMP_TAC[MOEBIUS_FUNCTION_NORM_LT_1; REAL_LT_IMP_NE] THEN
  REWRITE_TAC[MOEBIUS_FUNCTION_SIMPLE] THEN
  SUBGOAL_THEN
   `~(Cx(&1) - cnj w * x = Cx(&0)) /\ ~(Cx(&1) - cnj w * y = Cx(&0))`
  STRIP_ASSUME_TAC THENL
   [REWRITE_TAC[COMPLEX_SUB_0] THEN CONJ_TAC THEN
    MATCH_MP_TAC(MESON[REAL_LT_REFL] `norm(x) < norm(y) ==> ~(y = x)`) THEN
    REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM; COMPLEX_NORM_MUL] THEN
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
    MATCH_MP_TAC REAL_LT_MUL2 THEN REWRITE_TAC[NORM_POS_LE] THEN
    ASM_REWRITE_TAC[COMPLEX_NORM_CNJ];
    ASM_SIMP_TAC[COMPLEX_FIELD
     `~(Cx(&1) - cnj w * x = Cx(&0)) /\ ~(Cx(&1) - cnj w * y = Cx(&0))
      ==> (x - w) / (Cx (&1) - cnj w * x) - (y - w) / (Cx (&1) - cnj w * y) =
          ((Cx(&1) - w * cnj w) * (x - y)) /
          ((Cx (&1) - cnj w * x) * (Cx (&1) - cnj w * y))`] THEN
    REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_POW] THEN
    ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
     `~(y = &0) /\ ~(y' = &0)
      ==> (&1 - (x / y) pow 2) * (&1 - (x' / y') pow 2) =
          ((y pow 2 - x pow 2) * (y' pow 2 - x' pow 2)) / (y * y') pow 2`] THEN
    REWRITE_TAC[REAL_POW_DIV; COMPLEX_NORM_MUL] THEN REWRITE_TAC[real_div] THEN
    MATCH_MP_TAC(REAL_RING
     `x * y:real = w * z ==> (x * i) * y = w * z * i`) THEN
    REWRITE_TAC[GSYM COMPLEX_NORM_MUL] THEN REWRITE_TAC[NORM_POW_2; DOT_2] THEN
    REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; complex_sub; complex_mul; CX_DEF;
                complex_add; RE; IM; cnj; complex_neg] THEN REAL_ARITH_TAC]);;


let COLLINEAR_KLEINIFY_MOEBIUS = 
prove
 (`!w x y z. norm w < &1 /\ norm x < &1 /\ norm y < &1 /\ norm z < &1
             ==> (collinear {kleinify(moebius_function (&0) w x),
                             kleinify(moebius_function (&0) w y),
                             kleinify(moebius_function (&0) w z)} <=>
                  collinear {kleinify x,kleinify y,kleinify z})`,

  REPEAT STRIP_TAC THEN
  REWRITE_TAC[COLLINEAR_3_2D; kleinify; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[RE_MUL_CX; IM_MUL_CX] THEN
  SIMP_TAC[NORM_POS_LE; REAL_POW_LE; REAL_ARITH `&0 <= x ==> ~(&1 + x = &0)`;
     REAL_FIELD
     `~(nx = &0) /\ ~(ny = &0) /\ ~(nz = &0)
      ==> ((&2 / nz * rz - &2 / nx * rx) * (&2 / ny * iy - &2 / nx * ix) =
           (&2 / ny * ry - &2 / nx * rx) * (&2 / nz * iz - &2 / nx * ix) <=>
           (nx * rz - nz * rx) * (nx * iy - ny * ix) =
           (nx * ry - ny * rx) * (nx * iz - nz * ix))`] THEN
  REWRITE_TAC[COMPLEX_NORM_DIV; MOEBIUS_FUNCTION_SIMPLE] THEN
  ONCE_REWRITE_TAC[COMPLEX_DIV_CNJ] THEN
  REWRITE_TAC[RE_DIV_CX; GSYM CX_POW; IM_DIV_CX] THEN
  SUBGOAL_THEN
   `~(Cx (&1) - cnj w * x = Cx(&0)) /\ ~(Cx (&1) - cnj w * y = Cx(&0)) /\
    ~(Cx (&1) - cnj w * z = Cx(&0))`
  STRIP_ASSUME_TAC THENL
   [REWRITE_TAC[COMPLEX_SUB_0] THEN REPEAT CONJ_TAC THEN
    MATCH_MP_TAC(MESON[REAL_LT_REFL] `norm x < norm y ==> ~(y = x)`) THEN
    REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CNJ; COMPLEX_NORM_CX] THEN
    ONCE_REWRITE_TAC[REAL_ARITH `abs(&1) = &1 * &1`] THEN
    MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[NORM_POS_LE];
    ALL_TAC] THEN
  ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
   `~(nx = &0) /\ ~(ny = &0) /\ ~(nz = &0)
    ==>(((&1 + (nxw / nx) pow 2) * rz / nz pow 2 -
         (&1 + (nzw / nz) pow 2) * rx / nx pow 2) *
        ((&1 + (nxw / nx) pow 2) * iy / ny pow 2 -
         (&1 + (nyw / ny) pow 2) * ix / nx pow 2) =
        ((&1 + (nxw / nx) pow 2) * ry / ny pow 2 -
         (&1 + (nyw / ny) pow 2) * rx / nx pow 2) *
        ((&1 + (nxw / nx) pow 2) * iz / nz pow 2 -
         (&1 + (nzw / nz) pow 2) * ix / nx pow 2) <=>
        ((nx pow 2 + nxw pow 2) * rz - (nz pow 2 + nzw pow 2) * rx) *
        ((nx pow 2 + nxw pow 2) * iy - (ny pow 2 + nyw pow 2) * ix) =
        ((nx pow 2 + nxw pow 2) * ry - (ny pow 2 + nyw pow 2) * rx) *
        ((nx pow 2 + nxw pow 2) * iz - (nz pow 2 + nzw pow 2) * ix))`] THEN
  REWRITE_TAC[COMPLEX_SQNORM; complex_sub; complex_mul; complex_add;
              complex_neg; cnj; CX_DEF; RE; IM] THEN
  ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN MATCH_MP_TAC(REAL_RING
   `!a b. a * lhs = b * rhs /\ ~(a = &0) /\ ~(b = &0)
          ==> (lhs = &0 <=> rhs = &0)`) THEN
  EXISTS_TAC `Re x pow 2 + Im x pow 2 + &1` THEN
  EXISTS_TAC `--(Re w pow 2 + Im w pow 2 - &1) pow 3 *
              ((&1 - Re(x) pow 2 - Im(x) pow 2) *
               (&1 - Re(w) pow 2 - Im(w) pow 2) +
               &2 * (Re w - Re x) pow 2 + &2 * (Im w - Im x) pow 2)` THEN
  REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM; REAL_POW_EQ_0; ARITH_EQ] THEN
  REPEAT CONJ_TAC THENL
   [REAL_ARITH_TAC;
    MATCH_MP_TAC(REAL_ARITH `&0 <= x + y ==> ~(x + y + &1 = &0)`) THEN
    ASM_SIMP_TAC[GSYM COMPLEX_SQNORM; REAL_LE_POW_2];
    MATCH_MP_TAC(REAL_ARITH `x + y < &1 ==> ~(--(x + y - &1) = &0)`) THEN
    ASM_SIMP_TAC[GSYM COMPLEX_SQNORM; REAL_POW_1_LT; NORM_POS_LE; ARITH];
    MATCH_MP_TAC(REAL_ARITH `&0 < x /\ &0 <= y ==> ~(x + y = &0)`) THEN
    SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL; REAL_POS; REAL_LE_POW_2] THEN
    MATCH_MP_TAC REAL_LT_MUL THEN
    ASM_REWRITE_TAC[REAL_ARITH `&0 < &1 - x - y <=> x + y < &1`] THEN
    ASM_SIMP_TAC[GSYM COMPLEX_SQNORM; REAL_POW_1_LT; NORM_POS_LE; ARITH]]);;


let BETWEEN_KLEINIFY_MOEBIUS = 
prove
 (`!w x y z. norm w < &1 /\ norm x < &1 /\ norm y < &1 /\ norm z < &1
             ==> (between (kleinify(moebius_function (&0) w x))
                          (kleinify(moebius_function (&0) w y),
                           kleinify(moebius_function (&0) w z)) <=>
                  between (kleinify x) (kleinify y,kleinify z))`,


let hyperbolic_isometry = new_definition
 `hyperbolic_isometry (f:real^2->real^2) <=>
    (!x. norm x < &1 ==> norm(f x) < &1) /\
    (!x y. norm x < &1 /\ norm y < &1 ==> mdist(f x,f y) = mdist(x,y)) /\
    (!x y z. norm x < &1 /\ norm y < &1 /\ norm z < &1
             ==> (between (f x) (f y,f z) <=> between x (y,z)))`;;


let HYPERBOLIC_TRANSLATION = 
prove
 (`!w. norm w < &1
       ==> ?f:real^2->real^2 g:real^2->real^2.
                hyperbolic_isometry f /\ hyperbolic_isometry g /\
                f(w) = vec 0 /\ g(vec 0) = w /\
                (!x. norm x < &1 ==> f(g x) = x) /\
                (!x. norm x < &1 ==> g(f x) = x)`,

(* ------------------------------------------------------------------------- *)
(* Our model.                                                                *)
(* ------------------------------------------------------------------------- *)

let plane_tybij =
  
let th = 
prove
   (`?x:real^2. norm x < &1`,

    EXISTS_TAC `vec 0:real^2` THEN NORM_ARITH_TAC) in
  new_type_definition "plane" ("mk_plane","dest_plane") th;;


let pbetween = new_definition
 `pbetween y (x,z) <=> between (dest_plane y) (dest_plane x,dest_plane z)`;;


let pdist = new_definition
 `pdist(x,y) = mdist(dest_plane x,dest_plane y)`;;


let DEST_PLANE_NORM_LT = 
prove
 (`!x. norm(dest_plane x) < &1`,

  MESON_TAC[plane_tybij]);;


let DEST_PLANE_EQ = 
prove
 (`!x y. dest_plane x = dest_plane y <=> x = y`,

  MESON_TAC[plane_tybij]);;


let FORALL_DEST_PLANE = 
prove
 (`!P. (!x. P(dest_plane x)) <=> (!x. norm x < &1 ==> P x)`,

  MESON_TAC[plane_tybij]);;


let EXISTS_DEST_PLANE = 
prove
 (`!P. (?x. P(dest_plane x)) <=> (?x. norm x < &1 /\ P x)`,

  MESON_TAC[plane_tybij]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 1 (reflexivity for equidistance).                                   *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_1_NONEUCLIDEAN = 
prove
 (`!a b. pdist(a,b) = pdist(b,a)`,

  REWRITE_TAC[pdist; MDIST_SYM]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 2 (transitivity for equidistance).                                  *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_2_NONEUCLIDEAN = 
prove
 (`!a b p q r s.
        pdist(a,b) = pdist(p,q) /\ pdist(a,b) = pdist(r,s)
        ==> pdist(p,q) = pdist(r,s)`,

  REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Axiom 3 (identity for equidistance).                                      *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_3_NONEUCLIDEAN = 
prove
 (`!a b c. pdist(a,b) = pdist(c,c) ==> a = b`,

(* ------------------------------------------------------------------------- *)
(* Axiom 4 (segment construction).                                           *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_4_NONEUCLIDEAN = 
prove
 (`!a q b c. ?x. pbetween a (q,x) /\ pdist(a,x) = pdist(b,c)`,

  REWRITE_TAC[pbetween; pdist; FORALL_DEST_PLANE; EXISTS_DEST_PLANE] THEN
  REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  SUBGOAL_THEN `?d:real^2. norm d < &1 /\ mdist(b:real^2,c) = mdist(vec 0,d)`
  STRIP_ASSUME_TAC THENL
   [MP_TAC(SPEC `b:real^2` HYPERBOLIC_TRANSLATION) THEN
    ASM_REWRITE_TAC[hyperbolic_isometry] THEN ASM_MESON_TAC[];
    ASM_REWRITE_TAC[]] THEN
  SUBGOAL_THEN
   `norm(a:real^2) < &1 /\ norm(q:real^2) < &1 /\ norm(d:real^2) < &1`
   MP_TAC THENL [ASM_REWRITE_TAC[]; REPEAT(POP_ASSUM(K ALL_TAC))] THEN
  MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`d:real^2`; `q:real^2`; `a:real^2`] THEN
  MATCH_MP_TAC(MESON[] `P(vec 0) /\ (P(vec 0) ==> !x. P x) ==> !x. P x`) THEN
  REWRITE_TAC[NORM_0; REAL_LT_01] THEN CONJ_TAC THENL
   [MP_TAC(ISPEC `vec 0:real^2` TARSKI_AXIOM_4_EUCLIDEAN) THEN
    MESON_TAC[DIST_0; MDIST_EQ_ORIGIN];
    DISCH_THEN(LABEL_TAC "*") THEN REPEAT STRIP_TAC THEN
    MP_TAC(ISPEC `a:real^2` HYPERBOLIC_TRANSLATION) THEN
    ASM_REWRITE_TAC[hyperbolic_isometry; LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`f:real^2->real^2`; `g:real^2->real^2`] THEN
    STRIP_TAC THEN
    REMOVE_THEN "*" (MP_TAC o SPECL [`(f:real^2->real^2) q`; `d:real^2`]) THEN
    ASM_SIMP_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `x:real^2` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `(g:real^2->real^2) x` THEN ASM_MESON_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 5 (five-segments axiom).                                            *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_5_NONEUCLIDEAN = 
prove
 (`!a b c x a' b' c' x'.
        ~(a = b) /\
        pdist(a,b) = pdist(a',b') /\
        pdist(a,c) = pdist(a',c') /\
        pdist(b,c) = pdist(b',c') /\
        pbetween b (a,x) /\ pbetween b' (a',x') /\ pdist(b,x) = pdist(b',x')
        ==> pdist(c,x) = pdist(c',x')`,

  REWRITE_TAC[FORALL_DEST_PLANE; pdist; pbetween; GSYM DEST_PLANE_EQ] THEN
  REPEAT STRIP_TAC THEN MP_TAC(ISPEC `b':real^2` HYPERBOLIC_TRANSLATION) THEN
  MP_TAC(ISPEC `b:real^2` HYPERBOLIC_TRANSLATION) THEN
  ASM_REWRITE_TAC[RIGHT_IMP_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN
  REWRITE_TAC[hyperbolic_isometry] THEN MAP_EVERY X_GEN_TAC
   [`f:real^2->real^2`; `f':real^2->real^2`; `g:real^2->real^2`;
    `g':real^2->real^2`] THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`(f:real^2->real^2) x`; `(f:real^2->real^2) c`;
                `(g:real^2->real^2) x'`; `(g:real^2->real^2) c'`]
        MDIST_CONGRUENT_TRIPLES_0) THEN
  ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  MATCH_MP_TAC(TAUT `(p ==> r) /\ q ==> (p <=> q) ==> r`) THEN
  CONJ_TAC THENL [ASM_MESON_TAC[MDIST_SYM]; ALL_TAC] THEN
  MP_TAC(ISPECL [`(f:real^2->real^2) a`; `(f:real^2->real^2) c`;
                `(g:real^2->real^2) a'`; `(g:real^2->real^2) c'`]
        MDIST_CONGRUENT_TRIPLES_0) THEN
  ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  MATCH_MP_TAC(TAUT `p /\ (q ==> r) ==> (p <=> q) ==> r`) THEN CONJ_TAC THENL
   [ASM_SIMP_TAC[GSYM MDIST_CONGRUENT_TRIPLES_0] THEN  CONJ_TAC THEN
    GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
     [SYM(ASSUME `(f:complex->complex) b = vec 0`)] THEN
    GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
     [SYM(ASSUME `(g:complex->complex) b' = vec 0`)] THEN
    ASM_SIMP_TAC[] THEN ASM_MESON_TAC[MDIST_SYM];
    STRIP_TAC THEN MP_TAC(ISPECL
     [`(f:real^2->real^2) a`; `(f:real^2->real^2) b`; `(f:real^2->real^2) c`;
      `(f:real^2->real^2) x`;`(g:real^2->real^2) a'`; `(g:real^2->real^2) b'`;
      `(g:real^2->real^2) c'`; `(g:real^2->real^2) x'`]
     TARSKI_AXIOM_5_EUCLIDEAN) THEN
    SUBGOAL_THEN
     `mdist((f:real^2->real^2) b,f x) = mdist((g:real^2->real^2) b',g x')`
    MP_TAC THENL
     [ASM_SIMP_TAC[];
      ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[MDIST_EQ_ORIGIN] THEN DISCH_TAC] THEN
    ASM_MESON_TAC[DIST_SYM; DIST_0]]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 6 (identity for between-ness).                                      *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_6_NONEUCLIDEAN = 
prove
 (`!a b. pbetween b (a,a) ==> a = b`,

  REWRITE_TAC[pbetween; FORALL_DEST_PLANE; GSYM DEST_PLANE_EQ] THEN
  MESON_TAC[TARSKI_AXIOM_6_EUCLIDEAN]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 7 (Pasch's axiom).                                                  *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_7_NONEUCLIDEAN = 
prove
 (`!a b c p q.
    pbetween p (a,c) /\ pbetween q (b,c)
    ==> ?x. pbetween x (p,b) /\ pbetween x (q,a)`,

(* ------------------------------------------------------------------------- *)
(* Axiom 8 (lower 2-dimensional axiom).                                      *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_8_NONEUCLIDEAN = 
prove
 (`?a b c. ~pbetween b (a,c) /\ ~pbetween c (b,a) /\ ~pbetween a (c,b)`,

  REWRITE_TAC[pbetween; EXISTS_DEST_PLANE; NORM_LT_SQUARE; NORM_POW_2] THEN
  MAP_EVERY (fun t -> EXISTS_TAC t THEN
    SIMP_TAC[DOT_LMUL; DOT_RMUL; DOT_BASIS_BASIS; DIMINDEX_2; ARITH] THEN
    REWRITE_TAC[DOT_LZERO] THEN CONV_TAC REAL_RAT_REDUCE_CONV)
   [`vec 0:real^2`; `(&1 / &2) % basis 1:real^2`;
    `(&1 / &2) % basis 2:real^2`] THEN
  REPEAT CONJ_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR) THEN
  SIMP_TAC[COLLINEAR_3_2D; VECTOR_MUL_COMPONENT; VEC_COMPONENT; ARITH;
           BASIS_COMPONENT; DIMINDEX_2] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;

(* ------------------------------------------------------------------------- *)
(* Axiom 9 (upper 2-dimensional axiom).                                      *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_9_NONEUCLIDEAN = 
prove
 (`!p q a b c.
        ~(p = q) /\
        pdist(a,p) = pdist(a,q) /\ pdist(b,p) = pdist(b,q) /\
        pdist(c,p) = pdist(c,q)
        ==> pbetween b (a,c) \/ pbetween c (b,a) \/ pbetween a (c,b)`,

  REWRITE_TAC[pdist; pbetween; FORALL_DEST_PLANE; GSYM DEST_PLANE_EQ] THEN
  REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`p:real^2`; `q:real^2`] HYPERBOLIC_MIDPOINT) THEN
  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `x:real^2` THEN
  STRIP_TAC THEN MP_TAC(ISPEC `x:real^2` HYPERBOLIC_TRANSLATION) THEN
  SUBGOAL_THEN `norm(x:real^2) < &1` ASSUME_TAC THENL
   [ASM_MESON_TAC[BETWEEN_NORM_LT]; ONCE_REWRITE_TAC[BETWEEN_SYM]] THEN
  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; hyperbolic_isometry] THEN
  REWRITE_TAC[GSYM COLLINEAR_BETWEEN_CASES] THEN REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `collinear{(f:real^2->real^2) b,f c,f a}` MP_TAC THENL
   [ALL_TAC; ASM_SIMP_TAC[COLLINEAR_BETWEEN_CASES]] THEN
  SUBGOAL_THEN `mdist(f a,f p) = mdist(f a,f q) /\
                mdist(f b,f p) = mdist(f b,f q) /\
                mdist(f c,f p) = mdist(f c,f q) /\
                ~((f:real^2->real^2) q = f p)`
  MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  SUBGOAL_THEN `(f:real^2->real^2) q = --(f p)` SUBST1_TAC THENL
   [SUBGOAL_THEN `between ((f:real^2->real^2) x) (f p,f q) /\
                  mdist(f x,f p) = mdist(f x,f q)`
    MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
    ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[MDIST_EQ_ORIGIN] THEN
    REWRITE_TAC[GSYM MIDPOINT_BETWEEN; midpoint; NORM_ARITH
     `norm(a:real^N) = norm b <=> dist(a,vec 0) = dist(vec 0,b)`] THEN
    VECTOR_ARITH_TAC;
    REWRITE_TAC[mdist] THEN ASM_SIMP_TAC[NORM_NEG; real_div; REAL_INV_MUL] THEN
    ASM_SIMP_TAC[REAL_SUB_LT; ABS_SQUARE_LT_1; REAL_ABS_NORM; REAL_FIELD
     `&0 < x /\ &0 < y
      ==> (a * inv x * inv y - &1 = b * inv x * inv y - &1 <=> a = b)`] THEN
    ONCE_REWRITE_TAC[VECTOR_ARITH `--x:real^N = x <=> x = vec 0`] THEN
    REWRITE_TAC[COLLINEAR_3_2D; VECTOR_SUB_COMPONENT; DOT_2; GSYM DOT_EQ_0;
                  VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RING]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 10 (Euclidean axiom).                                               *)
(* ------------------------------------------------------------------------- *)


let NOT_TARSKI_AXIOM_10_NONEUCLIDEAN = 
prove
 (`~(!a b c d t.
      pbetween d (a,t) /\ pbetween d (b,c) /\ ~(a = d)
      ==> ?x y. pbetween b (a,x) /\ pbetween c (a,y) /\ pbetween t (x,y))`,

  REWRITE_TAC[pbetween; FORALL_DEST_PLANE; EXISTS_DEST_PLANE;
              GSYM DEST_PLANE_EQ; RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
  DISCH_THEN(MP_TAC o SPECL
   [`vec 0:real^2`; `&1 / &2 % basis 1:real^2`; `&1 / &2 % basis 2:real^2`;
    `&1 / &4 % basis 1 + &1 / &4 % basis 2:real^2`;
    `&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2`]) THEN
  REWRITE_TAC[NOT_IMP; CONJ_ASSOC] THEN CONJ_TAC THENL
   [ALL_TAC;
    REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`] THEN
    REWRITE_TAC[IMP_CONJ] THEN REPEAT(GEN_TAC THEN DISCH_TAC) THEN
    REWRITE_TAC[IMP_IMP] THEN
    DISCH_THEN(CONJUNCTS_THEN (MP_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
    SIMP_TAC[COLLINEAR_3_2D; BASIS_COMPONENT; DIMINDEX_2; ARITH; VEC_COMPONENT;
             VECTOR_MUL_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
    REWRITE_TAC[REAL_SUB_LZERO; REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO;
                REAL_ARITH `&0 = &1 / &2 * x <=> x = &0`] THEN
    REWRITE_TAC[REAL_ENTIRE] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
    MP_TAC(ISPECL [`x:real^2`; `1`] COMPONENT_LE_NORM) THEN
    MP_TAC(ISPECL [`y:real^2`; `2`] COMPONENT_LE_NORM) THEN
    SIMP_TAC[DIMINDEX_2; ARITH; BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
    REPEAT STRIP_TAC THEN SUBGOAL_THEN
     `norm(&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2) pow 2 <= &1 / &2`
    MP_TAC THENL
     [SUBGOAL_THEN `(&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2)$2 =
                    (&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2)$1`
      MP_TAC THENL
       [SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; ARITH; BASIS_COMPONENT;
                VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT] THEN
        REAL_ARITH_TAC;
        ASM_REWRITE_TAC[]] THEN
      REWRITE_TAC[NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL] THEN
      ASM_SIMP_TAC[DIMINDEX_2; FORALL_2; DOT_2; VECTOR_ADD_COMPONENT; ARITH;
                   VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2] THEN
      DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
        `a * &0 + y = x + b * &0 ==> abs x + abs y <= (&1 - u) * &1 + u * &1
         ==> abs x <= abs(&1 / &2) /\ abs y <= abs(&1 / &2)`)) THEN
      ANTS_TAC THENL
       [REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN
        CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REAL_ARITH_TAC;
        REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN REAL_ARITH_TAC];
      ALL_TAC]] THEN
  SIMP_TAC[NORM_LT_SQUARE; NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LZERO;
           DOT_LMUL; DOT_RMUL; DOT_BASIS_BASIS; DIMINDEX_2; ARITH] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN
  REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN REPEAT CONJ_TAC THENL
   [EXISTS_TAC `&5 / &12`; EXISTS_TAC `&1 / &2`; ALL_TAC] THEN
  SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; ARITH; BASIS_COMPONENT;
           VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV);;

(* ------------------------------------------------------------------------- *)
(* Axiom 11 (Continuity).                                                    *)
(* ------------------------------------------------------------------------- *)


let TARSKI_AXIOM_11_NONEUCLIDEAN = 
prove
 (`!X Y. (?a. !x y. x IN X /\ y IN Y ==> pbetween x (a,y))
         ==> (?b. !x y. x IN X /\ y IN Y ==> pbetween b (x,y))`,

  REPEAT GEN_TAC THEN
  ASM_CASES_TAC `X:plane->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
  ASM_CASES_TAC `Y:plane->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
  REWRITE_TAC[pbetween; EXISTS_DEST_PLANE] THEN
  DISCH_THEN(X_CHOOSE_THEN `a:real^2` STRIP_ASSUME_TAC) THEN
  MP_TAC(ISPECL [`IMAGE dest_plane X`; `IMAGE dest_plane Y`]
        TARSKI_AXIOM_11_EUCLIDEAN) THEN REWRITE_TAC[IN_IMAGE] THEN
  ANTS_TAC THENL [ASM SET_TAC[]; MATCH_MP_TAC MONO_EXISTS] THEN
  ASM_MESON_TAC[MEMBER_NOT_EMPTY; DEST_PLANE_NORM_LT; BETWEEN_NORM_LT]);;