100/independence.ml

   1 (* ========================================================================= *)
   2 (* Independence of the parallel postulate. The statement and some ideas are  *)
   3 (* taken from Tim Makarios's MSc thesis "A mechanical verification of the    *)
   4 (* independence of Tarski's Euclidean axiom".                                *)
   5 (*                                                                           *)
   6 (* In the file Multivariate/tarski.ml it is shown that all 11 of Tarski's    *)
   7 (* axioms for geometry hold for the Euclidean plane `:real^2`, with          *)
   8 (* betweenness and congruence of segments as:                                *)
   9 (*                                                                           *)
  10 (*      B x y z  <=> between y (x,z)                                         *)
  11 (*      ab == pq <=> dist(a,b) = dist(p,q)                                   *)
  12 (*                                                                           *)
  13 (* The present file shows that the Klein model of the hyperbolic plane (type *)
  14 (* `:plane`) satisfies all Tarski's axioms except that it satisfies the      *)
  15 (* negation of the Euclidean axiom (10), with betweenness and congruence of  *)
  16 (* segments as:                                                              *)
  17 (*                                                                           *)
  18 (*      B x y z  <=> pbetween y (x,z)                                        *)
  19 (*      ab == pq <=> pdist(a,b) = pdist(p,q)                                 *)
  20 (*                                                                           *)
  21 (* Collectively, these two results show that the Euclidean axiom is          *)
  22 (* independent of the others. For more references regarding Tarski's axioms  *)
  23 (* for geometry see "http://en.wikipedia.org/wiki/Tarski's_axioms".          *)
  24 (* ========================================================================= *)
  25
  26 needs "Multivariate/tarski.ml";;
  27 needs "Multivariate/cauchy.ml";;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* The semimetric we will use, directly on real^N first. Choose a sensible   *)
  31 (* default outside unit ball so some handy theorems become unconditional.    *)
  32 (* ------------------------------------------------------------------------- *)
  33
  34 let mdist = new_definition
  35  `mdist(x:real^N,y:real^N) =
  36     if norm(x) < &1 /\ norm(y) < &1 then
  37      (&1 - x dot y) pow 2 / ((&1 - norm(x) pow 2) * (&1 - norm(y) pow 2)) - &1
  38     else dist(x,y)`;;
  39
  40 let MDIST_INCREASES_ONLINE = prove
  41  (`!a b x:real^N.
  42       norm a < &1 /\ norm b < &1 /\ norm x < &1 /\ between x (a,b) /\ ~(x = b)
  43       ==> mdist(a,x) < mdist(a,b)`,
  44   REPEAT STRIP_TAC THEN ASM_CASES_TAC `b:real^N = a` THENL
  45    [ASM_MESON_TAC[BETWEEN_REFL_EQ]; ALL_TAC] THEN
  46   ASM_SIMP_TAC[mdist; real_div; REAL_INV_MUL] THEN
  47   SUBGOAL_THEN
  48    `norm(a:real^N) pow 2 < &1 /\ norm(b:real^N) pow 2 < &1 /\
  49     norm(x:real^N) pow 2 < &1`
  50   MP_TAC THENL [ASM_SIMP_TAC[ABS_SQUARE_LT_1; REAL_ABS_NORM]; ALL_TAC] THEN
  51   REWRITE_TAC[REAL_ARITH `a * inv x * inv b - &1 < c * inv x * d - &1 <=>
  52                           (a / b) / x < (c * d) / x`] THEN
  53   SIMP_TAC[REAL_LT_DIV2_EQ; REAL_LT_LDIV_EQ; REAL_SUB_LT] THEN
  54   ONCE_REWRITE_TAC[REAL_ARITH `(a * inv b) * c:real = (a * c) / b`] THEN
  55   SIMP_TAC[REAL_LT_RDIV_EQ; REAL_SUB_LT] THEN
  56   SUBGOAL_THEN `(a:real^N) dot b < &1 /\ (a:real^N) dot x < &1` MP_TAC THENL
  57    [CONJ_TAC THEN MATCH_MP_TAC(MESON[REAL_LET_TRANS; NORM_CAUCHY_SCHWARZ]
  58      `norm(x) * norm(y) < &1 ==> (x:real^N) dot y < &1`) THEN
  59     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
  60     MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[NORM_POS_LE];
  61     ALL_TAC] THEN
  62   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BETWEEN_IN_SEGMENT]) THEN
  63   REWRITE_TAC[IN_SEGMENT; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `u:real` THEN
  64   ASM_CASES_TAC `u = &1` THEN
  65   ASM_SIMP_TAC[VECTOR_ARITH `(&1 - &1) % a + &1 % b:real^N = b`] THEN
  66   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  67   SIMP_TAC[VECTOR_ARITH `(&1 - u) % a + u % b:real^N = a + u % (b - a)`] THEN
  68   ABBREV_TAC `c:real^N = b - a` THEN
  69   SUBGOAL_THEN `b:real^N = a + c` SUBST_ALL_TAC THENL
  70    [EXPAND_TAC "c" THEN VECTOR_ARITH_TAC; ALL_TAC] THEN
  71   RULE_ASSUM_TAC(SIMP_RULE[VECTOR_ARITH `a + c:real^N = a <=> c = vec 0`]) THEN
  72   REWRITE_TAC[NORM_POW_2; VECTOR_ARITH
  73     `(a + b:real^N) dot (a + b) = a dot a + &2 * a dot b + b dot b`] THEN
  74   REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN REWRITE_TAC[DOT_LMUL] THEN
  75   REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH
  76    `(&1 - (a + x * b)) pow 2 * (&1 - (a + &2 * b + c)) <
  77     (&1 - (a + b)) pow 2 * (&1 - (a + &2 * x * b + x * x * c)) <=>
  78     &0 < (&1 - a - b * x) * ((&1 - a) * c + b pow 2) * (&1 - x) +
  79          (&1 - a - b) * ((&1 - a) * c + b pow 2) * (&1 - x) * x`] THEN
  80   MATCH_MP_TAC REAL_LTE_ADD THEN CONJ_TAC THENL
  81    [REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC);
  82     REPEAT(MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC)] THEN
  83   TRY ASM_REAL_ARITH_TAC THEN TRY(MATCH_MP_TAC REAL_LT_IMP_LE) THEN
  84   MATCH_MP_TAC REAL_LTE_ADD THEN REWRITE_TAC[REAL_LE_POW_2] THEN
  85   MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[DOT_POS_LT; REAL_SUB_LT]);;
  86
  87 let MDIST_REFL = prove
  88  (`!x:real^N. mdist(x,x) = &0`,
  89   GEN_TAC THEN REWRITE_TAC[mdist; DIST_REFL; NORM_POW_2; NORM_LT_SQUARE] THEN
  90   CONV_TAC REAL_FIELD);;
  91
  92 let MDIST_SYM = prove
  93  (`!x y:real^N. mdist(x,y) = mdist(y,x)`,
  94   REWRITE_TAC[mdist; CONJ_ACI; REAL_MUL_AC; DIST_SYM; DOT_SYM]);;
  95
  96 let MDIST_POS_LT = prove
  97  (`!x y:real^N. ~(x = y) ==> &0 < mdist(x,y)`,
  98   REPEAT STRIP_TAC THEN
  99   ASM_CASES_TAC `norm(x:real^N) < &1 /\ norm(y:real^N) < &1` THENL
 100    [ASM_MESON_TAC[MDIST_INCREASES_ONLINE; MDIST_REFL; BETWEEN_REFL];
 101     ASM_SIMP_TAC[mdist; DIST_POS_LT]]);;
 102
 103 let MDIST_POS_LE = prove
 104  (`!x y:real^N. &0 <= mdist(x,y)`,
 105   REPEAT GEN_TAC THEN ASM_CASES_TAC `x:real^N = y` THEN
 106   ASM_SIMP_TAC[MDIST_REFL; MDIST_POS_LT; REAL_LE_LT]);;
 107
 108 let MDIST_EQ_0 = prove
 109  (`!x y:real^N. mdist(x,y) = &0 <=> x = y`,
 110   MESON_TAC[MDIST_REFL; MDIST_POS_LT; REAL_LT_REFL]);;
 111
 112 let BETWEEN_COLLINEAR_MDIST_EQ = prove
 113  (`!a b x:real^N.
 114         norm(a) < &1 /\ norm(b) < &1 /\ norm(x) < &1
 115         ==> (between x (a,b) <=>
 116              collinear {a, x, b} /\
 117              mdist(x,a) <= mdist (a,b) /\ mdist(x,b) <= mdist(a,b))`,
 118   REPEAT GEN_TAC THEN STRIP_TAC THEN EQ_TAC THENL
 119    [SIMP_TAC[BETWEEN_IMP_COLLINEAR];
 120     REWRITE_TAC[COLLINEAR_BETWEEN_CASES]] THEN
 121   ASM_MESON_TAC[MDIST_INCREASES_ONLINE; MDIST_SYM; REAL_LT_IMP_LE;
 122                 REAL_LE_REFL; BETWEEN_SYM; REAL_NOT_LE; BETWEEN_REFL]);;
 123
 124 let CONTINUOUS_AT_LIFT_MDIST = prove
 125  (`!a x:real^N.
 126       norm(a) < &1 /\ norm(x) < &1 ==> (\x. lift(mdist(a,x))) continuous at x`,
 127   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_TRANSFORM_AT THEN EXISTS_TAC
 128    `\x:real^N. lift((&1 - a dot x) pow 2 /
 129                     ((&1 - norm a pow 2) * (&1 - norm x pow 2)) - &1)` THEN
 130   EXISTS_TAC `&1 - norm(x:real^N)` THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
 131   CONJ_TAC THENL
 132    [X_GEN_TAC `y:real^N` THEN DISCH_THEN(MP_TAC o MATCH_MP (NORM_ARITH
 133     `dist(y,x) < &1 - norm x ==> norm y < &1`)) THEN ASM_SIMP_TAC[mdist];
 134     REWRITE_TAC[LIFT_SUB; real_div; LIFT_CMUL; REAL_INV_MUL] THEN
 135     MATCH_MP_TAC CONTINUOUS_SUB THEN SIMP_TAC[CONTINUOUS_CONST] THEN
 136     REPEAT(MATCH_MP_TAC CONTINUOUS_MUL THEN CONJ_TAC) THEN
 137     SIMP_TAC[CONTINUOUS_CONST; o_DEF; REAL_POW_2; LIFT_CMUL] THENL
 138      [MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_MUL);
 139       MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_AT_INV)] THEN
 140     ASM_SIMP_TAC[REAL_ARITH `x < &1 * &1 ==> ~(&1 - x = &0)`; REAL_LT_MUL2;
 141                  NORM_POS_LE; LIFT_SUB] THEN
 142     SIMP_TAC[GSYM REAL_POW_2; NORM_POW_2; CONTINUOUS_CONST; CONTINUOUS_AT_ID;
 143              CONTINUOUS_SUB; CONTINUOUS_LIFT_DOT2]]);;
 144
 145 let HYPERBOLIC_MIDPOINT = prove
 146  (`!a b:real^N.
 147         norm a < &1 /\ norm b < &1
 148         ==> ?x. between x (a,b) /\ mdist(x,a) = mdist(x,b)`,
 149   REPEAT STRIP_TAC THEN MP_TAC(ISPECL
 150    [`\x:real^N. lift(mdist(x,a) - mdist(x,b))`; `segment[a:real^N,b]`]
 151      CONNECTED_CONTINUOUS_IMAGE) THEN
 152   ANTS_TAC THENL
 153    [REWRITE_TAC[CONNECTED_SEGMENT; LIFT_SUB] THEN
 154     MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN REPEAT STRIP_TAC THEN
 155     MATCH_MP_TAC CONTINUOUS_SUB THEN ONCE_REWRITE_TAC[MDIST_SYM] THEN
 156     CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_AT_LIFT_MDIST THEN
 157     ASM_MESON_TAC[BETWEEN_NORM_LT; BETWEEN_IN_SEGMENT];
 158     REWRITE_TAC[GSYM IS_INTERVAL_CONNECTED_1; IS_INTERVAL_1] THEN
 159     REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
 160     REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM; LIFT_DROP] THEN
 161     DISCH_THEN(MP_TAC o SPECL [`a:real^N`; `b:real^N`; `lift(&0)`]) THEN
 162     ASM_SIMP_TAC[MDIST_REFL; LIFT_DROP; ENDS_IN_SEGMENT; IN_IMAGE] THEN
 163     REWRITE_TAC[REAL_SUB_RZERO; REAL_ARITH `&0 - x <= &0 <=> &0 <= x`] THEN
 164     ASM_SIMP_TAC[MDIST_POS_LE; LIFT_EQ; BETWEEN_IN_SEGMENT] THEN
 165     ASM_MESON_TAC[REAL_SUB_0; MDIST_SYM]]);;
 166
 167 let MDIST_EQ_ORIGIN = prove
 168  (`!x:real^N y:real^N.
 169         norm x < &1 /\ norm y < &1
 170         ==> (mdist(vec 0,x) = mdist(vec 0,y) <=> norm x = norm y)`,
 171   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[mdist; NORM_0; REAL_LT_01] THEN
 172   REWRITE_TAC[DOT_LZERO] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 173   REWRITE_TAC[real_div; REAL_MUL_LID; REAL_EQ_INV2;
 174               REAL_ARITH `x - &1 = y - &1 <=> x = y`] THEN
 175   REWRITE_TAC[REAL_ARITH `&1 - x = &1 - y <=> x = y`;
 176               GSYM REAL_EQ_SQUARE_ABS; REAL_ABS_NORM]);;
 177
 178 let MDIST_CONGRUENT_TRIPLES_0 = prove
 179  (`!a b:real^N a' b':real^N.
 180         norm a < &1 /\ norm b < &1 /\ norm a' < &1 /\ norm b' < &1
 181         ==> (mdist(vec 0,a) = mdist(vec 0,a') /\ mdist(a,b) = mdist(a',b') /\
 182              mdist(b,vec 0) = mdist(b',vec 0) <=>
 183              dist(vec 0,a) = dist(vec 0,a') /\ dist(a,b) = dist(a',b') /\
 184              dist(b,vec 0) = dist(b',vec 0))`,
 185   REPEAT STRIP_TAC THEN
 186   ASM_SIMP_TAC[MDIST_EQ_ORIGIN; REWRITE_RULE[MDIST_SYM] MDIST_EQ_ORIGIN] THEN
 187   REWRITE_TAC[DIST_0; NORM_0; REAL_LT_01] THEN MATCH_MP_TAC(TAUT
 188    `(a /\ b ==> (x <=> y)) ==> (a /\ x /\ b <=> a /\ y /\ b)`) THEN
 189   STRIP_TAC THEN ASM_SIMP_TAC[mdist; DIST_EQ; real_div; REAL_INV_MUL; REAL_RING
 190    `x * a * b - &1 = y * a * b - &1 <=> x = y \/ a = &0 \/ b = &0`] THEN
 191   REWRITE_TAC[dist; NORM_POW_2; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
 192   REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS; NORM_POW_2] THEN
 193   ASM_SIMP_TAC[REAL_INV_EQ_0; real_abs; REAL_SUB_LE; REAL_SUB_0] THEN
 194   ASM_SIMP_TAC[ABS_SQUARE_LT_1; REAL_ABS_NORM; REAL_LT_IMP_NE; REAL_LT_IMP_LE;
 195                MESON[NORM_CAUCHY_SCHWARZ; REAL_LET_TRANS; NORM_POS_LE;
 196                      REAL_LT_MUL2; REAL_MUL_RID; REAL_LT_IMP_LE]
 197                 `norm x < &1 /\ norm y < &1 ==> x dot y < &1`] THEN
 198   RULE_ASSUM_TAC(REWRITE_RULE[NORM_EQ]) THEN ASM_REAL_ARITH_TAC);;
 199
 200 (* ------------------------------------------------------------------------- *)
 201 (* Deduce existence of hyperbolic translations via the Poincare disc model.  *)
 202 (* Use orthogonal projection onto a hemisphere touching the unit disc,       *)
 203 (* then stereographic projection back from the other pole of the sphere plus *)
 204 (* scaling. See Greenberg's "Euclidean & Non-Euclidean Geometries" fig 7.13. *)
 205 (* ------------------------------------------------------------------------- *)
 206
 207 let kleinify = new_definition
 208  `kleinify z = Cx(&2 / (&1 + norm(z) pow 2)) * z`;;
 209
 210 let poincarify = new_definition
 211  `poincarify x = Cx((&1 - sqrt(&1 - norm(x) pow 2)) / norm(x) pow 2) * x`;;
 212
 213 let KLEINIFY_0,POINCARIFY_0 = (CONJ_PAIR o prove)
 214  (`kleinify (Cx(&0)) = Cx(&0) /\ poincarify (Cx(&0)) = Cx(&0)`,
 215   REWRITE_TAC[kleinify; poincarify; COMPLEX_MUL_RZERO]);;
 216
 217 let NORM_KLEINIFY = prove
 218  (`!z. norm(kleinify z) = (&2 * norm(z)) / (&1 + norm(z) pow 2)`,
 219   REWRITE_TAC[kleinify; COMPLEX_NORM_MUL; COMPLEX_NORM_CX; REAL_ABS_DIV] THEN
 220   SIMP_TAC[REAL_LE_POW_2; REAL_ARITH `&0 <= x ==> abs(&1 + x) = &1 + x`] THEN
 221   REAL_ARITH_TAC);;
 222
 223 let NORM_KLEINIFY_LT = prove
 224  (`!z. norm(kleinify z) < &1 <=> ~(norm z = &1)`,
 225   ASM_SIMP_TAC[NORM_KLEINIFY; REAL_LE_POW_2; REAL_LT_LDIV_EQ; REAL_MUL_LID;
 226                 REAL_ARITH `&0 <= x ==> &0 < &1 + x`] THEN
 227   SIMP_TAC[REAL_ARITH `&2 * z < (&1 + z pow 2) <=> &0 < (z - &1) pow 2`] THEN
 228   REWRITE_TAC[REAL_POW_2; REAL_LT_SQUARE] THEN REAL_ARITH_TAC);;
 229
 230 let NORM_POINCARIFY_LT = prove
 231  (`!x. norm(x) < &1 ==> norm(poincarify x) < &1`,
 232   REPEAT STRIP_TAC THEN REWRITE_TAC[poincarify; COMPLEX_NORM_MUL] THEN
 233   MATCH_MP_TAC(REAL_ARITH `x * y <= &1 * y /\ y < &1 ==> x * y < &1`) THEN
 234   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
 235   REWRITE_TAC[NORM_POS_LE; COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
 236   REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_POW] THEN
 237   ASM_CASES_TAC `x:real^2 = vec 0` THEN
 238   ASM_SIMP_TAC[REAL_LE_LDIV_EQ; NORM_POS_LT; REAL_POW_LT; NORM_0] THENL
 239    [REAL_ARITH_TAC; REWRITE_TAC[REAL_MUL_LID]] THEN
 240   MATCH_MP_TAC(REAL_ARITH `s <= &1 /\ &1 - x <= s ==> abs(&1 - s) <= x`) THEN
 241   CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LSQRT; MATCH_MP_TAC REAL_LE_RSQRT] THEN
 242   REWRITE_TAC[REAL_SUB_LE; REAL_POS; REAL_MUL_LID; REAL_POW_ONE] THEN
 243   ASM_SIMP_TAC[REAL_ARITH `(&1 - x) pow 2 <= &1 - x <=> &0 <= x * (&1 - x)`;
 244    REAL_ARITH `&1 - x <= &1 <=> &0 <= x`; REAL_LE_MUL; REAL_POW_LE;
 245    REAL_SUB_LE; ABS_SQUARE_LE_1; REAL_LT_IMP_LE; REAL_ABS_NORM; NORM_POS_LE]);;
 246
 247 let KLEINIFY_POINCARIFY = prove
 248  (`!x. norm(x) < &1 ==> kleinify(poincarify x) = x`,
 249   REPEAT STRIP_TAC THEN REWRITE_TAC[kleinify; poincarify] THEN MATCH_MP_TAC
 250     (COMPLEX_RING `(~(x = Cx(&0)) ==> w * z = Cx(&1)) ==> w * z * x = x`) THEN
 251   DISCH_TAC THEN REWRITE_TAC[GSYM CX_MUL; CX_INJ; COMPLEX_NORM_MUL] THEN
 252   REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_POW] THEN
 253   ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
 254    `~(y = &0)
 255     ==> (&1 + (a / y pow 2 * y) pow 2) = (y pow 2 + a pow 2) / y pow 2`] THEN
 256   REWRITE_TAC[REAL_POW2_ABS; real_div; REAL_INV_MUL; REAL_INV_INV] THEN
 257   ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
 258    `~(y = &0) ==> (&2 * x * y pow 2) * z * inv(y pow 2) = &2 * x * z`] THEN
 259   MATCH_MP_TAC(REAL_FIELD `&0 < y /\ &2 * y = x ==> &2 * inv(x) * y = &1`) THEN
 260   CONJ_TAC THENL
 261    [REWRITE_TAC[REAL_SUB_LT] THEN MATCH_MP_TAC REAL_LT_LSQRT THEN
 262     REWRITE_TAC[REAL_POS; REAL_ARITH `&1 - x < &1 pow 2 <=> &0 < x`] THEN
 263     ASM_SIMP_TAC[REAL_POW_LT; COMPLEX_NORM_NZ];
 264     SUBGOAL_THEN `sqrt(&1 - norm(x:real^2) pow 2) pow 2 = &1 - norm x pow 2`
 265     MP_TAC THENL [MATCH_MP_TAC SQRT_POW_2; CONV_TAC REAL_FIELD]] THEN
 266   ASM_SIMP_TAC[REAL_SUB_LE; ABS_SQUARE_LE_1; REAL_ABS_NORM; REAL_LT_IMP_LE]);;
 267
 268 let POINCARIFY_KLEINIFY = prove
 269  (`!x. norm(x) < &1 ==> poincarify(kleinify x) = x`,
 270   REPEAT STRIP_TAC THEN REWRITE_TAC[kleinify; poincarify] THEN
 271   MATCH_MP_TAC(COMPLEX_RING
 272    `(~(x = Cx(&0)) ==> w * z = Cx(&1)) ==> w * z * x = x`) THEN
 273   DISCH_TAC THEN REWRITE_TAC[GSYM CX_MUL; CX_INJ] THEN
 274   REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
 275   REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_POW; REAL_ABS_NUM] THEN
 276   REWRITE_TAC[real_div; REAL_INV_MUL; REAL_INV_INV; GSYM REAL_MUL_ASSOC;
 277               REAL_INV_POW; REAL_POW_MUL] THEN
 278   MATCH_MP_TAC(REAL_FIELD
 279    `~(c = &0) /\ abs d < &1 /\ a * b = &2 * c pow 2 * (&1 + d)
 280     ==> a * inv(&2) pow 2 * b * inv(c) pow 2 * &2 * inv(&1 + d) = &1`) THEN
 281   ASM_REWRITE_TAC[REAL_ABS_POW; COMPLEX_NORM_ZERO; ABS_SQUARE_LT_1] THEN
 282   ASM_SIMP_TAC[REAL_ABS_NORM; REAL_POW_LE; NORM_POS_LE; REAL_ARITH
 283    `&0 <= x ==> abs(&1 + x) = &1 + x`] THEN
 284   MATCH_MP_TAC(REAL_FIELD
 285    `~(x = &0) /\ abs x < &1 /\ a = &2 * x / (&1 + x)
 286     ==> a * (&1 + x) pow 2 = &2 * x * (&1 + x)`) THEN
 287   ASM_REWRITE_TAC[REAL_ABS_NORM; COMPLEX_NORM_ZERO; REAL_ABS_POW;
 288                   ABS_SQUARE_LT_1; REAL_POW_EQ_0] THEN
 289   MATCH_MP_TAC(REAL_ARITH `x = &1 - y ==> &1 - x = y`) THEN
 290   MATCH_MP_TAC SQRT_UNIQUE THEN
 291   REWRITE_TAC[REAL_ARITH `&0 <= &1 - &2 * x / y <=> (&2 * x) / y <= &1`] THEN
 292   SIMP_TAC[REAL_LE_LDIV_EQ; REAL_POW_LE; NORM_POS_LE; REAL_ARITH
 293    `&0 <= x ==> &0 < &1 + x`] THEN
 294   REWRITE_TAC[REAL_ARITH `&2 * x <= &1 * (&1 + x) <=> x <= &1`] THEN
 295   ASM_SIMP_TAC[ABS_SQUARE_LE_1; REAL_ABS_NORM; REAL_LT_IMP_LE] THEN
 296   SUBGOAL_THEN `~(&1 + norm(x:complex) pow 2 = &0)` MP_TAC THENL
 297    [ALL_TAC; CONV_TAC REAL_FIELD] THEN
 298   MATCH_MP_TAC(REAL_ARITH `abs(x) < &1 ==> ~(&1 + x = &0)`) THEN
 299   ASM_REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NORM; ABS_SQUARE_LT_1]);;
 300
 301 let MDIST_KLEINIFY = prove
 302  (`!w z. ~(norm w = &1) /\ ~(norm z = &1)
 303          ==> mdist(kleinify w,kleinify z) =
 304              &4 * (&1 / &2 + norm(w - z) pow 2 /
 305                              ((&1 - norm w pow 2) * (&1 - norm z pow 2))) pow 2
 306              - &1`,
 307   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 308    `(&4 * norm(w - z:real^2) pow 2 *
 309      ((&1 - norm w pow 2) * (&1 - norm z pow 2) + norm(w - z) pow 2)) /
 310     ((&1 - norm w pow 2) pow 2 * (&1 - norm z pow 2) pow 2)` THEN
 311   CONJ_TAC THENL
 312    [ASM_SIMP_TAC[mdist; NORM_KLEINIFY_LT] THEN MATCH_MP_TAC(REAL_FIELD
 313      `~(y = &0) /\ z = (w + &1) * y ==> z / y - &1 = w`) THEN
 314     CONJ_TAC THENL
 315      [REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN CONJ_TAC THEN
 316       MATCH_MP_TAC (REAL_ARITH `x < &1 ==> ~(&1 - x = &0)`) THEN
 317       ASM_SIMP_TAC[REAL_POW_1_LT; NORM_KLEINIFY_LT; NORM_POS_LE; ARITH];
 318       REWRITE_TAC[kleinify; COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
 319       REWRITE_TAC[GSYM COMPLEX_CMUL; DOT_LMUL] THEN REWRITE_TAC[DOT_RMUL] THEN
 320       SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NUM; REAL_POW_LE; NORM_POS_LE;
 321                REAL_ARITH `&0 <= x ==> abs(&1 + x) = &1 + x`] THEN
 322       MATCH_MP_TAC(REAL_FIELD
 323        `(~(y' = &0) /\ ~(y = &0)) /\
 324         (y * y' - &4 * d) pow 2 =
 325         b * (y pow 2 - &4 * x pow 2) * (y' pow 2 - &4 * x' pow 2)
 326         ==> (&1 - &2 / y * &2 / y' * d) pow 2 =
 327             b * (&1 - (&2 / y * x) pow 2) * (&1 - (&2 / y' * x') pow 2)`) THEN
 328       CONJ_TAC THENL
 329        [CONJ_TAC THEN
 330         MATCH_MP_TAC(REAL_ARITH `~(abs x = &1) ==> ~(&1 + x = &0)`) THEN
 331         ASM_SIMP_TAC[REAL_ABS_POW; REAL_POW_EQ_1; REAL_ABS_NORM] THEN ARITH_TAC;
 332         REWRITE_TAC[REAL_RING `(&1 + x) pow 2 - &4 * x = (&1 - x) pow 2`] THEN
 333         MATCH_MP_TAC(REAL_FIELD
 334          `(~(y = &0) /\ ~(y' = &0)) /\ a - y * y' = b
 335           ==> a = (b / (y * y') + &1) * y * y'`) THEN
 336         CONJ_TAC THENL
 337          [ASM_REWRITE_TAC[REAL_POW_EQ_0; REAL_POW_EQ_1; REAL_ABS_NORM; ARITH;
 338                           REAL_ARITH `&1 - x = &0 <=> x = &1`];
 339           REWRITE_TAC[NORM_POW_2; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
 340           REAL_ARITH_TAC]]];
 341     REPEAT(POP_ASSUM MP_TAC) THEN
 342     REWRITE_TAC[NORM_EQ_SQUARE; GSYM NORM_POW_2] THEN CONV_TAC REAL_FIELD]);;
 343
 344 let MDIST_KLEINIFY_EQ = prove
 345  (`!w z w' z'.
 346       ~(norm w = &1) /\ ~(norm z = &1) /\ ~(norm w' = &1) /\ ~(norm z' = &1) /\
 347       norm(w - z) pow 2 * (&1 - norm w' pow 2) * (&1 - norm z' pow 2) =
 348       norm(w' - z') pow 2 * (&1 - norm w pow 2) * (&1 - norm z pow 2)
 349       ==> mdist(kleinify w,kleinify z) = mdist(kleinify w',kleinify z')`,
 350   SIMP_TAC[MDIST_KLEINIFY; NORM_EQ_SQUARE; GSYM NORM_POW_2; REAL_POS] THEN
 351   CONV_TAC REAL_FIELD);;
 352
 353 let NORM_KLEINIFY_MOEBIUS_LT = prove
 354  (`!w x. norm w < &1 /\ norm x < &1
 355          ==> norm(kleinify(moebius_function (&0) w x)) < &1`,
 356   SIMP_TAC[MOEBIUS_FUNCTION_NORM_LT_1; NORM_KLEINIFY_LT; REAL_LT_IMP_NE]);;
 357
 358 let MDIST_KLEINIFY_MOEBIUS = prove
 359  (`!w x y. norm w < &1 /\ norm x < &1 /\ norm y < &1
 360            ==> mdist(kleinify(moebius_function (&0) w x),
 361                      kleinify(moebius_function (&0) w y)) =
 362                mdist(kleinify x,kleinify y)`,
 363   REPEAT STRIP_TAC THEN MATCH_MP_TAC MDIST_KLEINIFY_EQ THEN
 364   ASM_SIMP_TAC[MOEBIUS_FUNCTION_NORM_LT_1; REAL_LT_IMP_NE] THEN
 365   REWRITE_TAC[MOEBIUS_FUNCTION_SIMPLE] THEN
 366   SUBGOAL_THEN
 367    `~(Cx(&1) - cnj w * x = Cx(&0)) /\ ~(Cx(&1) - cnj w * y = Cx(&0))`
 368   STRIP_ASSUME_TAC THENL
 369    [REWRITE_TAC[COMPLEX_SUB_0] THEN CONJ_TAC THEN
 370     MATCH_MP_TAC(MESON[REAL_LT_REFL] `norm(x) < norm(y) ==> ~(y = x)`) THEN
 371     REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM; COMPLEX_NORM_MUL] THEN
 372     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 373     MATCH_MP_TAC REAL_LT_MUL2 THEN REWRITE_TAC[NORM_POS_LE] THEN
 374     ASM_REWRITE_TAC[COMPLEX_NORM_CNJ];
 375     ASM_SIMP_TAC[COMPLEX_FIELD
 376      `~(Cx(&1) - cnj w * x = Cx(&0)) /\ ~(Cx(&1) - cnj w * y = Cx(&0))
 377       ==> (x - w) / (Cx (&1) - cnj w * x) - (y - w) / (Cx (&1) - cnj w * y) =
 378           ((Cx(&1) - w * cnj w) * (x - y)) /
 379           ((Cx (&1) - cnj w * x) * (Cx (&1) - cnj w * y))`] THEN
 380     REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_POW] THEN
 381     ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
 382      `~(y = &0) /\ ~(y' = &0)
 383       ==> (&1 - (x / y) pow 2) * (&1 - (x' / y') pow 2) =
 384           ((y pow 2 - x pow 2) * (y' pow 2 - x' pow 2)) / (y * y') pow 2`] THEN
 385     REWRITE_TAC[REAL_POW_DIV; COMPLEX_NORM_MUL] THEN REWRITE_TAC[real_div] THEN
 386     MATCH_MP_TAC(REAL_RING
 387      `x * y:real = w * z ==> (x * i) * y = w * z * i`) THEN
 388     REWRITE_TAC[GSYM COMPLEX_NORM_MUL] THEN REWRITE_TAC[NORM_POW_2; DOT_2] THEN
 389     REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; complex_sub; complex_mul; CX_DEF;
 390                 complex_add; RE; IM; cnj; complex_neg] THEN REAL_ARITH_TAC]);;
 391
 392 let COLLINEAR_KLEINIFY_MOEBIUS = prove
 393  (`!w x y z. norm w < &1 /\ norm x < &1 /\ norm y < &1 /\ norm z < &1
 394              ==> (collinear {kleinify(moebius_function (&0) w x),
 395                              kleinify(moebius_function (&0) w y),
 396                              kleinify(moebius_function (&0) w z)} <=>
 397                   collinear {kleinify x,kleinify y,kleinify z})`,
 398   REPEAT STRIP_TAC THEN
 399   REWRITE_TAC[COLLINEAR_3_2D; kleinify; GSYM RE_DEF; GSYM IM_DEF] THEN
 400   REWRITE_TAC[RE_MUL_CX; IM_MUL_CX] THEN
 401   SIMP_TAC[NORM_POS_LE; REAL_POW_LE; REAL_ARITH `&0 <= x ==> ~(&1 + x = &0)`;
 402      REAL_FIELD
 403      `~(nx = &0) /\ ~(ny = &0) /\ ~(nz = &0)
 404       ==> ((&2 / nz * rz - &2 / nx * rx) * (&2 / ny * iy - &2 / nx * ix) =
 405            (&2 / ny * ry - &2 / nx * rx) * (&2 / nz * iz - &2 / nx * ix) <=>
 406            (nx * rz - nz * rx) * (nx * iy - ny * ix) =
 407            (nx * ry - ny * rx) * (nx * iz - nz * ix))`] THEN
 408   REWRITE_TAC[COMPLEX_NORM_DIV; MOEBIUS_FUNCTION_SIMPLE] THEN
 409   ONCE_REWRITE_TAC[COMPLEX_DIV_CNJ] THEN
 410   REWRITE_TAC[RE_DIV_CX; GSYM CX_POW; IM_DIV_CX] THEN
 411   SUBGOAL_THEN
 412    `~(Cx (&1) - cnj w * x = Cx(&0)) /\ ~(Cx (&1) - cnj w * y = Cx(&0)) /\
 413     ~(Cx (&1) - cnj w * z = Cx(&0))`
 414   STRIP_ASSUME_TAC THENL
 415    [REWRITE_TAC[COMPLEX_SUB_0] THEN REPEAT CONJ_TAC THEN
 416     MATCH_MP_TAC(MESON[REAL_LT_REFL] `norm x < norm y ==> ~(y = x)`) THEN
 417     REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CNJ; COMPLEX_NORM_CX] THEN
 418     ONCE_REWRITE_TAC[REAL_ARITH `abs(&1) = &1 * &1`] THEN
 419     MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[NORM_POS_LE];
 420     ALL_TAC] THEN
 421   ASM_SIMP_TAC[COMPLEX_NORM_ZERO; REAL_FIELD
 422    `~(nx = &0) /\ ~(ny = &0) /\ ~(nz = &0)
 423     ==>(((&1 + (nxw / nx) pow 2) * rz / nz pow 2 -
 424          (&1 + (nzw / nz) pow 2) * rx / nx pow 2) *
 425         ((&1 + (nxw / nx) pow 2) * iy / ny pow 2 -
 426          (&1 + (nyw / ny) pow 2) * ix / nx pow 2) =
 427         ((&1 + (nxw / nx) pow 2) * ry / ny pow 2 -
 428          (&1 + (nyw / ny) pow 2) * rx / nx pow 2) *
 429         ((&1 + (nxw / nx) pow 2) * iz / nz pow 2 -
 430          (&1 + (nzw / nz) pow 2) * ix / nx pow 2) <=>
 431         ((nx pow 2 + nxw pow 2) * rz - (nz pow 2 + nzw pow 2) * rx) *
 432         ((nx pow 2 + nxw pow 2) * iy - (ny pow 2 + nyw pow 2) * ix) =
 433         ((nx pow 2 + nxw pow 2) * ry - (ny pow 2 + nyw pow 2) * rx) *
 434         ((nx pow 2 + nxw pow 2) * iz - (nz pow 2 + nzw pow 2) * ix))`] THEN
 435   REWRITE_TAC[COMPLEX_SQNORM; complex_sub; complex_mul; complex_add;
 436               complex_neg; cnj; CX_DEF; RE; IM] THEN
 437   ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN MATCH_MP_TAC(REAL_RING
 438    `!a b. a * lhs = b * rhs /\ ~(a = &0) /\ ~(b = &0)
 439           ==> (lhs = &0 <=> rhs = &0)`) THEN
 440   EXISTS_TAC `Re x pow 2 + Im x pow 2 + &1` THEN
 441   EXISTS_TAC `--(Re w pow 2 + Im w pow 2 - &1) pow 3 *
 442               ((&1 - Re(x) pow 2 - Im(x) pow 2) *
 443                (&1 - Re(w) pow 2 - Im(w) pow 2) +
 444                &2 * (Re w - Re x) pow 2 + &2 * (Im w - Im x) pow 2)` THEN
 445   REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM; REAL_POW_EQ_0; ARITH_EQ] THEN
 446   REPEAT CONJ_TAC THENL
 447    [REAL_ARITH_TAC;
 448     MATCH_MP_TAC(REAL_ARITH `&0 <= x + y ==> ~(x + y + &1 = &0)`) THEN
 449     ASM_SIMP_TAC[GSYM COMPLEX_SQNORM; REAL_LE_POW_2];
 450     MATCH_MP_TAC(REAL_ARITH `x + y < &1 ==> ~(--(x + y - &1) = &0)`) THEN
 451     ASM_SIMP_TAC[GSYM COMPLEX_SQNORM; REAL_POW_1_LT; NORM_POS_LE; ARITH];
 452     MATCH_MP_TAC(REAL_ARITH `&0 < x /\ &0 <= y ==> ~(x + y = &0)`) THEN
 453     SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL; REAL_POS; REAL_LE_POW_2] THEN
 454     MATCH_MP_TAC REAL_LT_MUL THEN
 455     ASM_REWRITE_TAC[REAL_ARITH `&0 < &1 - x - y <=> x + y < &1`] THEN
 456     ASM_SIMP_TAC[GSYM COMPLEX_SQNORM; REAL_POW_1_LT; NORM_POS_LE; ARITH]]);;
 457
 458 let BETWEEN_KLEINIFY_MOEBIUS = prove
 459  (`!w x y z. norm w < &1 /\ norm x < &1 /\ norm y < &1 /\ norm z < &1
 460              ==> (between (kleinify(moebius_function (&0) w x))
 461                           (kleinify(moebius_function (&0) w y),
 462                            kleinify(moebius_function (&0) w z)) <=>
 463                   between (kleinify x) (kleinify y,kleinify z))`,
 464   SIMP_TAC[BETWEEN_COLLINEAR_MDIST_EQ; NORM_KLEINIFY_MOEBIUS_LT;
 465            NORM_KLEINIFY_LT; REAL_LT_IMP_NE;
 466            COLLINEAR_KLEINIFY_MOEBIUS; MDIST_KLEINIFY_MOEBIUS]);;
 467
 468 let hyperbolic_isometry = new_definition
 469  `hyperbolic_isometry (f:real^2->real^2) <=>
 470     (!x. norm x < &1 ==> norm(f x) < &1) /\
 471     (!x y. norm x < &1 /\ norm y < &1 ==> mdist(f x,f y) = mdist(x,y)) /\
 472     (!x y z. norm x < &1 /\ norm y < &1 /\ norm z < &1
 473              ==> (between (f x) (f y,f z) <=> between x (y,z)))`;;
 474
 475 let HYPERBOLIC_TRANSLATION = prove
 476  (`!w. norm w < &1
 477        ==> ?f:real^2->real^2 g:real^2->real^2.
 478                 hyperbolic_isometry f /\ hyperbolic_isometry g /\
 479                 f(w) = vec 0 /\ g(vec 0) = w /\
 480                 (!x. norm x < &1 ==> f(g x) = x) /\
 481                 (!x. norm x < &1 ==> g(f x) = x)`,
 482   REPEAT STRIP_TAC THEN SIMP_TAC[hyperbolic_isometry] THEN MAP_EVERY EXISTS_TAC
 483    [`\x. kleinify(moebius_function(&0) (poincarify w) (poincarify x))`;
 484    `\x. kleinify(moebius_function(&0) (--(poincarify w)) (poincarify x))`] THEN
 485   ASM_SIMP_TAC[NORM_KLEINIFY_MOEBIUS_LT; NORM_POINCARIFY_LT;
 486                MDIST_KLEINIFY_MOEBIUS; KLEINIFY_POINCARIFY; VECTOR_NEG_NEG;
 487                BETWEEN_KLEINIFY_MOEBIUS; NORM_NEG; MOEBIUS_FUNCTION_COMPOSE;
 488                POINCARIFY_KLEINIFY; MOEBIUS_FUNCTION_NORM_LT_1] THEN
 489   ASM_SIMP_TAC[MOEBIUS_FUNCTION_SIMPLE; COMPLEX_SUB_REFL; complex_div;
 490                COMPLEX_VEC_0; KLEINIFY_0; POINCARIFY_0; COMPLEX_MUL_LZERO;
 491                COMPLEX_MUL_RZERO; COMPLEX_SUB_LZERO; COMPLEX_NEG_NEG;
 492                COMPLEX_SUB_RZERO; COMPLEX_INV_1; COMPLEX_MUL_RID;
 493                KLEINIFY_POINCARIFY]);;
 494
 495 (* ------------------------------------------------------------------------- *)
 496 (* Our model.                                                                *)
 497 (* ------------------------------------------------------------------------- *)
 498
 499 let plane_tybij =
 500   let th = prove
 501    (`?x:real^2. norm x < &1`,
 502     EXISTS_TAC `vec 0:real^2` THEN NORM_ARITH_TAC) in
 503   new_type_definition "plane" ("mk_plane","dest_plane") th;;
 504
 505 let pbetween = new_definition
 506  `pbetween y (x,z) <=> between (dest_plane y) (dest_plane x,dest_plane z)`;;
 507
 508 let pdist = new_definition
 509  `pdist(x,y) = mdist(dest_plane x,dest_plane y)`;;
 510
 511 let DEST_PLANE_NORM_LT = prove
 512  (`!x. norm(dest_plane x) < &1`,
 513   MESON_TAC[plane_tybij]);;
 514
 515 let DEST_PLANE_EQ = prove
 516  (`!x y. dest_plane x = dest_plane y <=> x = y`,
 517   MESON_TAC[plane_tybij]);;
 518
 519 let FORALL_DEST_PLANE = prove
 520  (`!P. (!x. P(dest_plane x)) <=> (!x. norm x < &1 ==> P x)`,
 521   MESON_TAC[plane_tybij]);;
 522
 523 let EXISTS_DEST_PLANE = prove
 524  (`!P. (?x. P(dest_plane x)) <=> (?x. norm x < &1 /\ P x)`,
 525   MESON_TAC[plane_tybij]);;
 526
 527 (* ------------------------------------------------------------------------- *)
 528 (* Axiom 1 (reflexivity for equidistance).                                   *)
 529 (* ------------------------------------------------------------------------- *)
 530
 531 let TARSKI_AXIOM_1_NONEUCLIDEAN = prove
 532  (`!a b. pdist(a,b) = pdist(b,a)`,
 533   REWRITE_TAC[pdist; MDIST_SYM]);;
 534
 535 (* ------------------------------------------------------------------------- *)
 536 (* Axiom 2 (transitivity for equidistance).                                  *)
 537 (* ------------------------------------------------------------------------- *)
 538
 539 let TARSKI_AXIOM_2_NONEUCLIDEAN = prove
 540  (`!a b p q r s.
 541         pdist(a,b) = pdist(p,q) /\ pdist(a,b) = pdist(r,s)
 542         ==> pdist(p,q) = pdist(r,s)`,
 543   REAL_ARITH_TAC);;
 544
 545 (* ------------------------------------------------------------------------- *)
 546 (* Axiom 3 (identity for equidistance).                                      *)
 547 (* ------------------------------------------------------------------------- *)
 548
 549 let TARSKI_AXIOM_3_NONEUCLIDEAN = prove
 550  (`!a b c. pdist(a,b) = pdist(c,c) ==> a = b`,
 551   SIMP_TAC[FORALL_DEST_PLANE; pdist; MDIST_REFL; MDIST_EQ_0; DEST_PLANE_EQ]);;
 552
 553 (* ------------------------------------------------------------------------- *)
 554 (* Axiom 4 (segment construction).                                           *)
 555 (* ------------------------------------------------------------------------- *)
 556
 557 let TARSKI_AXIOM_4_NONEUCLIDEAN = prove
 558  (`!a q b c. ?x. pbetween a (q,x) /\ pdist(a,x) = pdist(b,c)`,
 559   REWRITE_TAC[pbetween; pdist; FORALL_DEST_PLANE; EXISTS_DEST_PLANE] THEN
 560   REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
 561   REPEAT GEN_TAC THEN DISCH_TAC THEN
 562   SUBGOAL_THEN `?d:real^2. norm d < &1 /\ mdist(b:real^2,c) = mdist(vec 0,d)`
 563   STRIP_ASSUME_TAC THENL
 564    [MP_TAC(SPEC `b:real^2` HYPERBOLIC_TRANSLATION) THEN
 565     ASM_REWRITE_TAC[hyperbolic_isometry] THEN ASM_MESON_TAC[];
 566     ASM_REWRITE_TAC[]] THEN
 567   SUBGOAL_THEN
 568    `norm(a:real^2) < &1 /\ norm(q:real^2) < &1 /\ norm(d:real^2) < &1`
 569    MP_TAC THENL [ASM_REWRITE_TAC[]; REPEAT(POP_ASSUM(K ALL_TAC))] THEN
 570   MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`d:real^2`; `q:real^2`; `a:real^2`] THEN
 571   MATCH_MP_TAC(MESON[] `P(vec 0) /\ (P(vec 0) ==> !x. P x) ==> !x. P x`) THEN
 572   REWRITE_TAC[NORM_0; REAL_LT_01] THEN CONJ_TAC THENL
 573    [MP_TAC(ISPEC `vec 0:real^2` TARSKI_AXIOM_4_EUCLIDEAN) THEN
 574     MESON_TAC[DIST_0; MDIST_EQ_ORIGIN];
 575     DISCH_THEN(LABEL_TAC "*") THEN REPEAT STRIP_TAC THEN
 576     MP_TAC(ISPEC `a:real^2` HYPERBOLIC_TRANSLATION) THEN
 577     ASM_REWRITE_TAC[hyperbolic_isometry; LEFT_IMP_EXISTS_THM] THEN
 578     MAP_EVERY X_GEN_TAC [`f:real^2->real^2`; `g:real^2->real^2`] THEN
 579     STRIP_TAC THEN
 580     REMOVE_THEN "*" (MP_TAC o SPECL [`(f:real^2->real^2) q`; `d:real^2`]) THEN
 581     ASM_SIMP_TAC[] THEN
 582     DISCH_THEN(X_CHOOSE_THEN `x:real^2` STRIP_ASSUME_TAC) THEN
 583     EXISTS_TAC `(g:real^2->real^2) x` THEN ASM_MESON_TAC[]]);;
 584
 585 (* ------------------------------------------------------------------------- *)
 586 (* Axiom 5 (five-segments axiom).                                            *)
 587 (* ------------------------------------------------------------------------- *)
 588
 589 let TARSKI_AXIOM_5_NONEUCLIDEAN = prove
 590  (`!a b c x a' b' c' x'.
 591         ~(a = b) /\
 592         pdist(a,b) = pdist(a',b') /\
 593         pdist(a,c) = pdist(a',c') /\
 594         pdist(b,c) = pdist(b',c') /\
 595         pbetween b (a,x) /\ pbetween b' (a',x') /\ pdist(b,x) = pdist(b',x')
 596         ==> pdist(c,x) = pdist(c',x')`,
 597   REWRITE_TAC[FORALL_DEST_PLANE; pdist; pbetween; GSYM DEST_PLANE_EQ] THEN
 598   REPEAT STRIP_TAC THEN MP_TAC(ISPEC `b':real^2` HYPERBOLIC_TRANSLATION) THEN
 599   MP_TAC(ISPEC `b:real^2` HYPERBOLIC_TRANSLATION) THEN
 600   ASM_REWRITE_TAC[RIGHT_IMP_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN
 601   REWRITE_TAC[hyperbolic_isometry] THEN MAP_EVERY X_GEN_TAC
 602    [`f:real^2->real^2`; `f':real^2->real^2`; `g:real^2->real^2`;
 603     `g':real^2->real^2`] THEN REPEAT STRIP_TAC THEN
 604   MP_TAC(ISPECL [`(f:real^2->real^2) x`; `(f:real^2->real^2) c`;
 605                 `(g:real^2->real^2) x'`; `(g:real^2->real^2) c'`]
 606         MDIST_CONGRUENT_TRIPLES_0) THEN
 607   ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 608   MATCH_MP_TAC(TAUT `(p ==> r) /\ q ==> (p <=> q) ==> r`) THEN
 609   CONJ_TAC THENL [ASM_MESON_TAC[MDIST_SYM]; ALL_TAC] THEN
 610   MP_TAC(ISPECL [`(f:real^2->real^2) a`; `(f:real^2->real^2) c`;
 611                 `(g:real^2->real^2) a'`; `(g:real^2->real^2) c'`]
 612         MDIST_CONGRUENT_TRIPLES_0) THEN
 613   ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 614   MATCH_MP_TAC(TAUT `p /\ (q ==> r) ==> (p <=> q) ==> r`) THEN CONJ_TAC THENL
 615    [ASM_SIMP_TAC[GSYM MDIST_CONGRUENT_TRIPLES_0] THEN  CONJ_TAC THEN
 616     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
 617      [SYM(ASSUME `(f:complex->complex) b = vec 0`)] THEN
 618     GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
 619      [SYM(ASSUME `(g:complex->complex) b' = vec 0`)] THEN
 620     ASM_SIMP_TAC[] THEN ASM_MESON_TAC[MDIST_SYM];
 621     STRIP_TAC THEN MP_TAC(ISPECL
 622      [`(f:real^2->real^2) a`; `(f:real^2->real^2) b`; `(f:real^2->real^2) c`;
 623       `(f:real^2->real^2) x`;`(g:real^2->real^2) a'`; `(g:real^2->real^2) b'`;
 624       `(g:real^2->real^2) c'`; `(g:real^2->real^2) x'`]
 625      TARSKI_AXIOM_5_EUCLIDEAN) THEN
 626     SUBGOAL_THEN
 627      `mdist((f:real^2->real^2) b,f x) = mdist((g:real^2->real^2) b',g x')`
 628     MP_TAC THENL
 629      [ASM_SIMP_TAC[];
 630       ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[MDIST_EQ_ORIGIN] THEN DISCH_TAC] THEN
 631     ASM_MESON_TAC[DIST_SYM; DIST_0]]);;
 632
 633 (* ------------------------------------------------------------------------- *)
 634 (* Axiom 6 (identity for between-ness).                                      *)
 635 (* ------------------------------------------------------------------------- *)
 636
 637 let TARSKI_AXIOM_6_NONEUCLIDEAN = prove
 638  (`!a b. pbetween b (a,a) ==> a = b`,
 639   REWRITE_TAC[pbetween; FORALL_DEST_PLANE; GSYM DEST_PLANE_EQ] THEN
 640   MESON_TAC[TARSKI_AXIOM_6_EUCLIDEAN]);;
 641
 642 (* ------------------------------------------------------------------------- *)
 643 (* Axiom 7 (Pasch's axiom).                                                  *)
 644 (* ------------------------------------------------------------------------- *)
 645
 646 let TARSKI_AXIOM_7_NONEUCLIDEAN = prove
 647  (`!a b c p q.
 648     pbetween p (a,c) /\ pbetween q (b,c)
 649     ==> ?x. pbetween x (p,b) /\ pbetween x (q,a)`,
 650   REWRITE_TAC[pbetween; FORALL_DEST_PLANE; EXISTS_DEST_PLANE] THEN
 651   MESON_TAC[BETWEEN_NORM_LT; TARSKI_AXIOM_7_EUCLIDEAN]);;
 652
 653 (* ------------------------------------------------------------------------- *)
 654 (* Axiom 8 (lower 2-dimensional axiom).                                      *)
 655 (* ------------------------------------------------------------------------- *)
 656
 657 let TARSKI_AXIOM_8_NONEUCLIDEAN = prove
 658  (`?a b c. ~pbetween b (a,c) /\ ~pbetween c (b,a) /\ ~pbetween a (c,b)`,
 659   REWRITE_TAC[pbetween; EXISTS_DEST_PLANE; NORM_LT_SQUARE; NORM_POW_2] THEN
 660   MAP_EVERY (fun t -> EXISTS_TAC t THEN
 661     SIMP_TAC[DOT_LMUL; DOT_RMUL; DOT_BASIS_BASIS; DIMINDEX_2; ARITH] THEN
 662     REWRITE_TAC[DOT_LZERO] THEN CONV_TAC REAL_RAT_REDUCE_CONV)
 663    [`vec 0:real^2`; `(&1 / &2) % basis 1:real^2`;
 664     `(&1 / &2) % basis 2:real^2`] THEN
 665   REPEAT CONJ_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR) THEN
 666   SIMP_TAC[COLLINEAR_3_2D; VECTOR_MUL_COMPONENT; VEC_COMPONENT; ARITH;
 667            BASIS_COMPONENT; DIMINDEX_2] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
 668
 669 (* ------------------------------------------------------------------------- *)
 670 (* Axiom 9 (upper 2-dimensional axiom).                                      *)
 671 (* ------------------------------------------------------------------------- *)
 672
 673 let TARSKI_AXIOM_9_NONEUCLIDEAN = prove
 674  (`!p q a b c.
 675         ~(p = q) /\
 676         pdist(a,p) = pdist(a,q) /\ pdist(b,p) = pdist(b,q) /\
 677         pdist(c,p) = pdist(c,q)
 678         ==> pbetween b (a,c) \/ pbetween c (b,a) \/ pbetween a (c,b)`,
 679   REWRITE_TAC[pdist; pbetween; FORALL_DEST_PLANE; GSYM DEST_PLANE_EQ] THEN
 680   REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
 681   REPEAT STRIP_TAC THEN
 682   MP_TAC(ISPECL [`p:real^2`; `q:real^2`] HYPERBOLIC_MIDPOINT) THEN
 683   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `x:real^2` THEN
 684   STRIP_TAC THEN MP_TAC(ISPEC `x:real^2` HYPERBOLIC_TRANSLATION) THEN
 685   SUBGOAL_THEN `norm(x:real^2) < &1` ASSUME_TAC THENL
 686    [ASM_MESON_TAC[BETWEEN_NORM_LT]; ONCE_REWRITE_TAC[BETWEEN_SYM]] THEN
 687   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; hyperbolic_isometry] THEN
 688   REWRITE_TAC[GSYM COLLINEAR_BETWEEN_CASES] THEN REPEAT STRIP_TAC THEN
 689   SUBGOAL_THEN `collinear{(f:real^2->real^2) b,f c,f a}` MP_TAC THENL
 690    [ALL_TAC; ASM_SIMP_TAC[COLLINEAR_BETWEEN_CASES]] THEN
 691   SUBGOAL_THEN `mdist(f a,f p) = mdist(f a,f q) /\
 692                 mdist(f b,f p) = mdist(f b,f q) /\
 693                 mdist(f c,f p) = mdist(f c,f q) /\
 694                 ~((f:real^2->real^2) q = f p)`
 695   MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 696   SUBGOAL_THEN `(f:real^2->real^2) q = --(f p)` SUBST1_TAC THENL
 697    [SUBGOAL_THEN `between ((f:real^2->real^2) x) (f p,f q) /\
 698                   mdist(f x,f p) = mdist(f x,f q)`
 699     MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 700     ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[MDIST_EQ_ORIGIN] THEN
 701     REWRITE_TAC[GSYM MIDPOINT_BETWEEN; midpoint; NORM_ARITH
 702      `norm(a:real^N) = norm b <=> dist(a,vec 0) = dist(vec 0,b)`] THEN
 703     VECTOR_ARITH_TAC;
 704     REWRITE_TAC[mdist] THEN ASM_SIMP_TAC[NORM_NEG; real_div; REAL_INV_MUL] THEN
 705     ASM_SIMP_TAC[REAL_SUB_LT; ABS_SQUARE_LT_1; REAL_ABS_NORM; REAL_FIELD
 706      `&0 < x /\ &0 < y
 707       ==> (a * inv x * inv y - &1 = b * inv x * inv y - &1 <=> a = b)`] THEN
 708     ONCE_REWRITE_TAC[VECTOR_ARITH `--x:real^N = x <=> x = vec 0`] THEN
 709     REWRITE_TAC[COLLINEAR_3_2D; VECTOR_SUB_COMPONENT; DOT_2; GSYM DOT_EQ_0;
 710                   VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RING]);;
 711
 712 (* ------------------------------------------------------------------------- *)
 713 (* Axiom 10 (Euclidean axiom).                                               *)
 714 (* ------------------------------------------------------------------------- *)
 715
 716 let NOT_TARSKI_AXIOM_10_NONEUCLIDEAN = prove
 717  (`~(!a b c d t.
 718       pbetween d (a,t) /\ pbetween d (b,c) /\ ~(a = d)
 719       ==> ?x y. pbetween b (a,x) /\ pbetween c (a,y) /\ pbetween t (x,y))`,
 720   REWRITE_TAC[pbetween; FORALL_DEST_PLANE; EXISTS_DEST_PLANE;
 721               GSYM DEST_PLANE_EQ; RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
 722   DISCH_THEN(MP_TAC o SPECL
 723    [`vec 0:real^2`; `&1 / &2 % basis 1:real^2`; `&1 / &2 % basis 2:real^2`;
 724     `&1 / &4 % basis 1 + &1 / &4 % basis 2:real^2`;
 725     `&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2`]) THEN
 726   REWRITE_TAC[NOT_IMP; CONJ_ASSOC] THEN CONJ_TAC THENL
 727    [ALL_TAC;
 728     REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`] THEN
 729     REWRITE_TAC[IMP_CONJ] THEN REPEAT(GEN_TAC THEN DISCH_TAC) THEN
 730     REWRITE_TAC[IMP_IMP] THEN
 731     DISCH_THEN(CONJUNCTS_THEN (MP_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
 732     SIMP_TAC[COLLINEAR_3_2D; BASIS_COMPONENT; DIMINDEX_2; ARITH; VEC_COMPONENT;
 733              VECTOR_MUL_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 734     REWRITE_TAC[REAL_SUB_LZERO; REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_SUB_RZERO;
 735                 REAL_ARITH `&0 = &1 / &2 * x <=> x = &0`] THEN
 736     REWRITE_TAC[REAL_ENTIRE] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 737     MP_TAC(ISPECL [`x:real^2`; `1`] COMPONENT_LE_NORM) THEN
 738     MP_TAC(ISPECL [`y:real^2`; `2`] COMPONENT_LE_NORM) THEN
 739     SIMP_TAC[DIMINDEX_2; ARITH; BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
 740     REPEAT STRIP_TAC THEN SUBGOAL_THEN
 741      `norm(&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2) pow 2 <= &1 / &2`
 742     MP_TAC THENL
 743      [SUBGOAL_THEN `(&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2)$2 =
 744                     (&3 / &5 % basis 1 + &3 / &5 % basis 2:real^2)$1`
 745       MP_TAC THENL
 746        [SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; ARITH; BASIS_COMPONENT;
 747                 VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT] THEN
 748         REAL_ARITH_TAC;
 749         ASM_REWRITE_TAC[]] THEN
 750       REWRITE_TAC[NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL] THEN
 751       ASM_SIMP_TAC[DIMINDEX_2; FORALL_2; DOT_2; VECTOR_ADD_COMPONENT; ARITH;
 752                    VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2] THEN
 753       DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
 754         `a * &0 + y = x + b * &0 ==> abs x + abs y <= (&1 - u) * &1 + u * &1
 755          ==> abs x <= abs(&1 / &2) /\ abs y <= abs(&1 / &2)`)) THEN
 756       ANTS_TAC THENL
 757        [REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN
 758         CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REAL_ARITH_TAC;
 759         REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN REAL_ARITH_TAC];
 760       ALL_TAC]] THEN
 761   SIMP_TAC[NORM_LT_SQUARE; NORM_POW_2; DOT_LADD; DOT_RADD; DOT_LZERO;
 762            DOT_LMUL; DOT_RMUL; DOT_BASIS_BASIS; DIMINDEX_2; ARITH] THEN
 763   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 764   REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN REPEAT CONJ_TAC THENL
 765    [EXISTS_TAC `&5 / &12`; EXISTS_TAC `&1 / &2`; ALL_TAC] THEN
 766   SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; ARITH; BASIS_COMPONENT;
 767            VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT] THEN
 768   CONV_TAC REAL_RAT_REDUCE_CONV);;
 769
 770 (* ------------------------------------------------------------------------- *)
 771 (* Axiom 11 (Continuity).                                                    *)
 772 (* ------------------------------------------------------------------------- *)
 773
 774 let TARSKI_AXIOM_11_NONEUCLIDEAN = prove
 775  (`!X Y. (?a. !x y. x IN X /\ y IN Y ==> pbetween x (a,y))
 776          ==> (?b. !x y. x IN X /\ y IN Y ==> pbetween b (x,y))`,
 777   REPEAT GEN_TAC THEN
 778   ASM_CASES_TAC `X:plane->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
 779   ASM_CASES_TAC `Y:plane->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
 780   REWRITE_TAC[pbetween; EXISTS_DEST_PLANE] THEN
 781   DISCH_THEN(X_CHOOSE_THEN `a:real^2` STRIP_ASSUME_TAC) THEN
 782   MP_TAC(ISPECL [`IMAGE dest_plane X`; `IMAGE dest_plane Y`]
 783         TARSKI_AXIOM_11_EUCLIDEAN) THEN REWRITE_TAC[IN_IMAGE] THEN
 784   ANTS_TAC THENL [ASM SET_TAC[]; MATCH_MP_TAC MONO_EXISTS] THEN
 785   ASM_MESON_TAC[MEMBER_NOT_EMPTY; DEST_PLANE_NORM_LT; BETWEEN_NORM_LT]);;