100/platonic.ml

   1 (* ========================================================================= *)
   2 (* The five Platonic solids exist and there are no others.                   *)
   3 (* ========================================================================= *)
   4
   5 needs "100/polyhedron.ml";;
   6 needs "Multivariate/cross.ml";;
   7
   8 prioritize_real();;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Some standard regular polyhedra (vertex coordinates from Wikipedia).      *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let std_tetrahedron = new_definition
  15  `std_tetrahedron =
  16      convex hull
  17        {vector[&1;&1;&1],vector[-- &1;-- &1;&1],
  18         vector[-- &1;&1;-- &1],vector[&1;-- &1;-- &1]}:real^3->bool`;;
  19
  20 let std_cube = new_definition
  21  `std_cube =
  22      convex hull
  23        {vector[&1;&1;&1],vector[&1;&1;-- &1],
  24         vector[&1;-- &1;&1],vector[&1;-- &1;-- &1],
  25         vector[-- &1;&1;&1],vector[-- &1;&1;-- &1],
  26         vector[-- &1;-- &1;&1],vector[-- &1;-- &1;-- &1]}:real^3->bool`;;
  27
  28 let std_octahedron = new_definition
  29  `std_octahedron =
  30       convex hull
  31        {vector[&1;&0;&0],vector[-- &1;&0;&0],
  32         vector[&0;&0;&1],vector[&0;&0;-- &1],
  33         vector[&0;&1;&0],vector[&0;-- &1;&0]}:real^3->bool`;;
  34
  35 let std_dodecahedron = new_definition
  36  `std_dodecahedron =
  37       let p = (&1 + sqrt(&5)) / &2 in
  38       convex hull
  39        {vector[&1;&1;&1],vector[&1;&1;-- &1],
  40         vector[&1;-- &1;&1],vector[&1;-- &1;-- &1],
  41         vector[-- &1;&1;&1],vector[-- &1;&1;-- &1],
  42         vector[-- &1;-- &1;&1],vector[-- &1;-- &1;-- &1],
  43         vector[&0;inv p;p],vector[&0;inv p;--p],
  44         vector[&0;--inv p;p],vector[&0;--inv p;--p],
  45         vector[inv p;p;&0],vector[inv p;--p;&0],
  46         vector[--inv p;p;&0],vector[--inv p;--p;&0],
  47         vector[p;&0;inv p],vector[--p;&0;inv p],
  48         vector[p;&0;--inv p],vector[--p;&0;--inv p]}:real^3->bool`;;
  49
  50 let std_icosahedron = new_definition
  51  `std_icosahedron =
  52       let p = (&1 + sqrt(&5)) / &2 in
  53       convex hull
  54        {vector[&0; &1; p],vector[&0; &1; --p],
  55         vector[&0; -- &1; p],vector[&0; -- &1; --p],
  56         vector[&1; p; &0],vector[&1; --p; &0],
  57         vector[-- &1; p; &0],vector[-- &1; --p; &0],
  58         vector[p; &0; &1],vector[--p; &0; &1],
  59         vector[p; &0; -- &1],vector[--p; &0; -- &1]}:real^3->bool`;;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* Slightly ad hoc conversions for computation in Q[sqrt(5)].                *)
  63 (* Numbers are canonically represented as either a rational constant r or an *)
  64 (* expression r1 + r2 * sqrt(5) where r2 is nonzero but r1 may be zero and   *)
  65 (* must be present.                                                          *)
  66 (* ------------------------------------------------------------------------- *)
  67
  68 let REAL_RAT5_OF_RAT_CONV =
  69   let pth = prove
  70    (`p = p + &0 * sqrt(&5)`,
  71     REAL_ARITH_TAC) in
  72   let conv = REWR_CONV pth in
  73   fun tm -> if is_ratconst tm then conv tm else REFL tm;;
  74
  75 let REAL_RAT_OF_RAT5_CONV =
  76   let pth = prove
  77    (`p + &0 * sqrt(&5) = p`,
  78     REAL_ARITH_TAC) in
  79   GEN_REWRITE_CONV TRY_CONV [pth];;
  80
  81 let REAL_RAT5_ADD_CONV =
  82   let pth = prove
  83     (`(a1 + b1 * sqrt(&5)) + (a2 + b2 * sqrt(&5)) =
  84       (a1 + a2) + (b1 + b2) * sqrt(&5)`,
  85      REAL_ARITH_TAC) in
  86   REAL_RAT_ADD_CONV ORELSEC
  87   (BINOP_CONV REAL_RAT5_OF_RAT_CONV THENC
  88    GEN_REWRITE_CONV I [pth] THENC
  89    LAND_CONV REAL_RAT_ADD_CONV THENC
  90    RAND_CONV(LAND_CONV REAL_RAT_ADD_CONV) THENC
  91    REAL_RAT_OF_RAT5_CONV);;
  92
  93 let REAL_RAT5_SUB_CONV =
  94   let pth = prove
  95     (`(a1 + b1 * sqrt(&5)) - (a2 + b2 * sqrt(&5)) =
  96       (a1 - a2) + (b1 - b2) * sqrt(&5)`,
  97      REAL_ARITH_TAC) in
  98   REAL_RAT_SUB_CONV ORELSEC
  99   (BINOP_CONV REAL_RAT5_OF_RAT_CONV THENC
 100    GEN_REWRITE_CONV I [pth] THENC
 101    LAND_CONV REAL_RAT_SUB_CONV THENC
 102    RAND_CONV(LAND_CONV REAL_RAT_SUB_CONV) THENC
 103    REAL_RAT_OF_RAT5_CONV);;
 104
 105 let REAL_RAT5_MUL_CONV =
 106   let pth = prove
 107     (`(a1 + b1 * sqrt(&5)) * (a2 + b2 * sqrt(&5)) =
 108       (a1 * a2 + &5 * b1 * b2) + (a1 * b2 + a2 * b1) * sqrt(&5)`,
 109      MP_TAC(ISPEC `&5` SQRT_POW_2) THEN CONV_TAC REAL_FIELD) in
 110   REAL_RAT_MUL_CONV ORELSEC
 111   (BINOP_CONV REAL_RAT5_OF_RAT_CONV THENC
 112    GEN_REWRITE_CONV I [pth] THENC
 113    LAND_CONV(COMB_CONV (RAND_CONV REAL_RAT_MUL_CONV) THENC
 114              RAND_CONV REAL_RAT_MUL_CONV THENC
 115              REAL_RAT_ADD_CONV) THENC
 116    RAND_CONV(LAND_CONV
 117     (BINOP_CONV REAL_RAT_MUL_CONV THENC REAL_RAT_ADD_CONV)) THENC
 118    REAL_RAT_OF_RAT5_CONV);;
 119
 120 let REAL_RAT5_INV_CONV =
 121   let pth = prove
 122    (`~(a pow 2 = &5 * b pow 2)
 123      ==> inv(a + b * sqrt(&5)) =
 124          a / (a pow 2 - &5 * b pow 2) +
 125          --b / (a pow 2 - &5 * b pow 2) * sqrt(&5)`,
 126     REPEAT GEN_TAC THEN
 127     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM REAL_SUB_0] THEN
 128     SUBGOAL_THEN
 129      `a pow 2 - &5 * b pow 2 = (a + b * sqrt(&5)) * (a - b * sqrt(&5))`
 130     SUBST1_TAC THENL
 131      [MP_TAC(SPEC `&5` SQRT_POW_2) THEN CONV_TAC REAL_FIELD;
 132       REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN CONV_TAC REAL_FIELD]) in
 133   fun tm ->
 134     try REAL_RAT_INV_CONV tm with Failure _ ->
 135     let th1 = PART_MATCH (lhs o rand) pth tm in
 136     let th2 = MP th1 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th1)))) in
 137     let th3 = CONV_RULE(funpow 2 RAND_CONV (funpow 2 LAND_CONV
 138                 REAL_RAT_NEG_CONV)) th2 in
 139     let th4 = CONV_RULE(RAND_CONV(RAND_CONV(LAND_CONV
 140                (RAND_CONV(LAND_CONV REAL_RAT_POW_CONV THENC
 141                           RAND_CONV(RAND_CONV REAL_RAT_POW_CONV THENC
 142                                     REAL_RAT_MUL_CONV) THENC
 143                           REAL_RAT_SUB_CONV) THENC
 144                 REAL_RAT_DIV_CONV)))) th3 in
 145     let th5 = CONV_RULE(RAND_CONV(LAND_CONV
 146                (RAND_CONV(LAND_CONV REAL_RAT_POW_CONV THENC
 147                           RAND_CONV(RAND_CONV REAL_RAT_POW_CONV THENC
 148                                     REAL_RAT_MUL_CONV) THENC
 149                           REAL_RAT_SUB_CONV) THENC
 150                 REAL_RAT_DIV_CONV))) th4 in
 151     th5;;
 152
 153 let REAL_RAT5_DIV_CONV =
 154   GEN_REWRITE_CONV I [real_div] THENC
 155   RAND_CONV REAL_RAT5_INV_CONV THENC
 156   REAL_RAT5_MUL_CONV;;
 157
 158 let REAL_RAT5_LE_CONV =
 159   let lemma = prove
 160    (`!x y. x <= y * sqrt(&5) <=>
 161            x <= &0 /\ &0 <= y \/
 162            &0 <= x /\ &0 <= y /\ x pow 2 <= &5 * y pow 2 \/
 163            x <= &0 /\ y <= &0 /\ &5 * y pow 2 <= x pow 2`,
 164     REPEAT GEN_TAC THEN MP_TAC(ISPEC `&5` SQRT_POW_2) THEN
 165     REWRITE_TAC[REAL_POS] THEN DISCH_THEN(fun th ->
 166       GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM th]) THEN
 167     REWRITE_TAC[GSYM REAL_POW_MUL; GSYM REAL_LE_SQUARE_ABS] THEN
 168     MP_TAC(ISPECL [`sqrt(&5)`; `y:real`] (CONJUNCT1 REAL_LE_MUL_EQ)) THEN
 169     SIMP_TAC[SQRT_POS_LT; REAL_OF_NUM_LT; ARITH] THEN REAL_ARITH_TAC) in
 170   let pth = prove
 171    (`(a1 + b1 * sqrt(&5)) <= (a2 + b2 * sqrt(&5)) <=>
 172         a1 <= a2 /\ b1 <= b2 \/
 173         a2 <= a1 /\ b1 <= b2 /\ (a1 - a2) pow 2 <= &5 * (b2 - b1) pow 2 \/
 174         a1 <= a2 /\ b2 <= b1 /\ &5 * (b2 - b1) pow 2 <= (a1 - a2) pow 2`,
 175     REWRITE_TAC[REAL_ARITH
 176      `a + b * x <= a' + b' * x <=> a - a' <= (b' - b) * x`] THEN
 177     REWRITE_TAC[lemma] THEN REAL_ARITH_TAC) in
 178   REAL_RAT_LE_CONV ORELSEC
 179   (BINOP_CONV REAL_RAT5_OF_RAT_CONV THENC
 180    GEN_REWRITE_CONV I [pth] THENC
 181    REAL_RAT_REDUCE_CONV);;
 182
 183 let REAL_RAT5_EQ_CONV =
 184   GEN_REWRITE_CONV I [GSYM REAL_LE_ANTISYM] THENC
 185   BINOP_CONV REAL_RAT5_LE_CONV THENC
 186   GEN_REWRITE_CONV I [AND_CLAUSES];;
 187
 188 (* ------------------------------------------------------------------------- *)
 189 (* Conversions for operations on 3D vectors with coordinates in Q[sqrt(5)]   *)
 190 (* ------------------------------------------------------------------------- *)
 191
 192 let VECTOR3_SUB_CONV =
 193   let pth = prove
 194    (`vector[x1;x2;x3] - vector[y1;y2;y3]:real^3 =
 195      vector[x1-y1; x2-y2; x3-y3]`,
 196     SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3] THEN
 197     REWRITE_TAC[VECTOR_3; VECTOR_SUB_COMPONENT]) in
 198   GEN_REWRITE_CONV I [pth] THENC RAND_CONV(LIST_CONV REAL_RAT5_SUB_CONV);;
 199
 200 let VECTOR3_CROSS_CONV =
 201   let pth = prove
 202    (`(vector[x1;x2;x3]) cross (vector[y1;y2;y3]) =
 203      vector[x2 * y3 - x3 * y2; x3 * y1 - x1 * y3; x1 * y2 - x2 * y1]`,
 204     REWRITE_TAC[cross; VECTOR_3]) in
 205   GEN_REWRITE_CONV I [pth] THENC
 206   RAND_CONV(LIST_CONV(BINOP_CONV REAL_RAT5_MUL_CONV THENC REAL_RAT5_SUB_CONV));;
 207
 208 let VECTOR3_EQ_0_CONV =
 209   let pth = prove
 210    (`vector[x1;x2;x3]:real^3 = vec 0 <=>
 211         x1 = &0 /\ x2 = &0 /\ x3 = &0`,
 212     SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3] THEN
 213     REWRITE_TAC[VECTOR_3; VEC_COMPONENT]) in
 214   GEN_REWRITE_CONV I [pth] THENC
 215   DEPTH_BINOP_CONV `(/\)` REAL_RAT5_EQ_CONV THENC
 216   REWRITE_CONV[];;
 217
 218 let VECTOR3_DOT_CONV =
 219   let pth = prove
 220    (`(vector[x1;x2;x3]:real^3) dot (vector[y1;y2;y3]) =
 221         x1*y1 + x2*y2 + x3*y3`,
 222     REWRITE_TAC[DOT_3; VECTOR_3]) in
 223   GEN_REWRITE_CONV I [pth] THENC
 224   DEPTH_BINOP_CONV `(+):real->real->real` REAL_RAT5_MUL_CONV THENC
 225   RAND_CONV REAL_RAT5_ADD_CONV THENC
 226   REAL_RAT5_ADD_CONV;;
 227
 228 (* ------------------------------------------------------------------------- *)
 229 (* Put any irrational coordinates in our standard form.                      *)
 230 (* ------------------------------------------------------------------------- *)
 231
 232 let STD_DODECAHEDRON = prove
 233  (`std_dodecahedron =
 234    convex hull
 235     { vector[&1; &1; &1],
 236       vector[&1; &1; -- &1],
 237       vector[&1; -- &1; &1],
 238       vector[&1; -- &1; -- &1],
 239       vector[-- &1; &1; &1],
 240       vector[-- &1; &1; -- &1],
 241       vector[-- &1; -- &1; &1],
 242       vector[-- &1; -- &1; -- &1],
 243       vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)],
 244       vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)],
 245       vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)],
 246       vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)],
 247       vector[-- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0],
 248       vector[-- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0],
 249       vector[&1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0],
 250       vector[&1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0],
 251       vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)],
 252       vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)],
 253       vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)],
 254       vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)]}`,
 255   let golden_inverse = prove
 256    (`inv((&1 + sqrt(&5)) / &2) = -- &1 / &2 + &1 / &2 * sqrt(&5)`,
 257     MP_TAC(ISPEC `&5` SQRT_POW_2) THEN CONV_TAC REAL_FIELD) in
 258   REWRITE_TAC[std_dodecahedron] THEN
 259   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 260   REWRITE_TAC[golden_inverse] THEN
 261   REWRITE_TAC[REAL_ARITH `(&1 + s) / &2 = &1 / &2 + &1 / &2 * s`] THEN
 262   REWRITE_TAC[REAL_ARITH `--(a + b * sqrt(&5)) = --a + --b * sqrt(&5)`] THEN
 263   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[]);;
 264
 265 let STD_ICOSAHEDRON = prove
 266  (`std_icosahedron =
 267    convex hull
 268     { vector[&0; &1; &1 / &2 + &1 / &2 * sqrt(&5)],
 269       vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)],
 270       vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt(&5)],
 271       vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)],
 272       vector[&1; &1 / &2 + &1 / &2 * sqrt(&5); &0],
 273       vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0],
 274       vector[-- &1; &1 / &2 + &1 / &2 * sqrt(&5); &0],
 275       vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0],
 276       vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1],
 277       vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1],
 278       vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1],
 279       vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1]}`,
 280   REWRITE_TAC[std_icosahedron] THEN
 281   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 282   REWRITE_TAC[REAL_ARITH `(&1 + s) / &2 = &1 / &2 + &1 / &2 * s`] THEN
 283   REWRITE_TAC[REAL_ARITH `--(a + b * sqrt(&5)) = --a + --b * sqrt(&5)`] THEN
 284   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[]);;
 285
 286 (* ------------------------------------------------------------------------- *)
 287 (* Explicit computation of facets.                                           *)
 288 (* ------------------------------------------------------------------------- *)
 289
 290 let COMPUTE_FACES_2 = prove
 291  (`!f s:real^3->bool.
 292         FINITE s
 293         ==> (f face_of (convex hull s) /\ aff_dim f = &2 <=>
 294              ?x y z. x IN s /\ y IN s /\ z IN s /\
 295                      let a = (z - x) cross (y - x) in
 296                      ~(a = vec 0) /\
 297                      let b = a dot x in
 298                      ((!w. w IN s ==> a dot w <= b) \/
 299                       (!w. w IN s ==> a dot w >= b)) /\
 300                      f = convex hull (s INTER {x | a dot x = b}))`,
 301   REPEAT GEN_TAC THEN STRIP_TAC THEN EQ_TAC THENL
 302    [STRIP_TAC THEN
 303     SUBGOAL_THEN `?t:real^3->bool. t SUBSET s /\ f = convex hull t`
 304     MP_TAC THENL
 305      [MATCH_MP_TAC FACE_OF_CONVEX_HULL_SUBSET THEN
 306       ASM_SIMP_TAC[FINITE_IMP_COMPACT];
 307       DISCH_THEN(X_CHOOSE_THEN `t:real^3->bool` MP_TAC)] THEN
 308     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
 309     RULE_ASSUM_TAC(REWRITE_RULE[AFF_DIM_CONVEX_HULL]) THEN
 310     MP_TAC(ISPEC `t:real^3->bool` AFFINE_BASIS_EXISTS) THEN
 311     DISCH_THEN(X_CHOOSE_THEN `u:real^3->bool` STRIP_ASSUME_TAC) THEN
 312     SUBGOAL_THEN `(u:real^3->bool) HAS_SIZE 3` MP_TAC THENL
 313      [ASM_SIMP_TAC[HAS_SIZE; AFFINE_INDEPENDENT_IMP_FINITE] THEN
 314       REWRITE_TAC[GSYM INT_OF_NUM_EQ] THEN MATCH_MP_TAC(INT_ARITH
 315        `aff_dim(u:real^3->bool) = &2 /\ aff_dim u = &(CARD u) - &1
 316         ==> &(CARD u):int = &3`) THEN CONJ_TAC
 317       THENL [ASM_MESON_TAC[AFF_DIM_AFFINE_HULL]; ASM_MESON_TAC[AFF_DIM_UNIQUE]];
 318       ALL_TAC] THEN
 319     CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
 320     MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`; `z:real^3`] THEN
 321     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 322     DISCH_THEN SUBST_ALL_TAC THEN
 323     MAP_EVERY EXISTS_TAC  [`x:real^3`; `y:real^3`; `z:real^3`] THEN
 324     REPLICATE_TAC 3 (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
 325     REPEAT LET_TAC THEN
 326     SUBGOAL_THEN `~collinear{x:real^3,y,z}` MP_TAC THENL
 327      [ASM_REWRITE_TAC[COLLINEAR_3_EQ_AFFINE_DEPENDENT]; ALL_TAC] THEN
 328     ONCE_REWRITE_TAC[SET_RULE `{x,y,z} = {z,x,y}`] THEN
 329     ONCE_REWRITE_TAC[COLLINEAR_3] THEN ASM_REWRITE_TAC[GSYM CROSS_EQ_0] THEN
 330     DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 331     SUBGOAL_THEN `(a:real^3) dot y = b /\ (a:real^3) dot z = b`
 332     STRIP_ASSUME_TAC THENL
 333      [MAP_EVERY UNDISCH_TAC
 334        [`(z - x) cross (y - x) = a`; `(a:real^3) dot x = b`] THEN VEC3_TAC;
 335       ALL_TAC] THEN
 336     MP_TAC(ISPECL [`convex hull s:real^3->bool`; `convex hull t:real^3->bool`]
 337         EXPOSED_FACE_OF_POLYHEDRON) THEN
 338     ASM_SIMP_TAC[POLYHEDRON_CONVEX_HULL; exposed_face_of] THEN
 339     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 340     MAP_EVERY X_GEN_TAC [`a':real^3`; `b':real`] THEN
 341     DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 342     SUBGOAL_THEN
 343      `aff_dim(t:real^3->bool)
 344       <= aff_dim({x:real^3 | a dot x = b} INTER {x | a' dot x = b'})`
 345     MP_TAC THENL
 346      [GEN_REWRITE_TAC LAND_CONV [GSYM AFF_DIM_AFFINE_HULL] THEN
 347       FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
 348        [SYM th]) THEN
 349       REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN MATCH_MP_TAC AFF_DIM_SUBSET THEN
 350       REWRITE_TAC[SUBSET_INTER] THEN CONJ_TAC THENL
 351        [ASM SET_TAC[];
 352         MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `t:real^3->bool` THEN
 353         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
 354         EXISTS_TAC `convex hull t:real^3->bool` THEN
 355         REWRITE_TAC[HULL_SUBSET] THEN ASM SET_TAC[]];
 356       ALL_TAC] THEN
 357     ASM_SIMP_TAC[AFF_DIM_AFFINE_INTER_HYPERPLANE; AFF_DIM_HYPERPLANE;
 358                  AFFINE_HYPERPLANE; DIMINDEX_3] THEN
 359     REPEAT(COND_CASES_TAC THEN CONV_TAC INT_REDUCE_CONV) THEN
 360     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
 361      [SUBSET_HYPERPLANES]) THEN
 362     ASM_REWRITE_TAC[HYPERPLANE_EQ_EMPTY] THEN
 363     DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC (MP_TAC o SYM)) THENL
 364      [RULE_ASSUM_TAC(REWRITE_RULE[INTER_UNIV]) THEN
 365       SUBGOAL_THEN `s SUBSET {x:real^3 | a dot x = b}` ASSUME_TAC THENL
 366        [MATCH_MP_TAC SUBSET_TRANS THEN
 367         EXISTS_TAC `convex hull s:real^3->bool` THEN
 368         REWRITE_TAC[HULL_SUBSET] THEN ASM_REWRITE_TAC[] THEN
 369         MATCH_MP_TAC SUBSET_TRANS THEN
 370         EXISTS_TAC `affine hull t:real^3->bool` THEN
 371         REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL] THEN
 372         FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
 373         MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[AFFINE_HYPERPLANE] THEN
 374         ASM SET_TAC[];
 375         ALL_TAC] THEN
 376       CONJ_TAC THENL
 377        [RULE_ASSUM_TAC(REWRITE_RULE[SUBSET; IN_ELIM_THM]) THEN
 378         ASM_SIMP_TAC[real_ge; REAL_LE_REFL];
 379         ASM_SIMP_TAC[SET_RULE `s SUBSET t ==> s INTER t = s`]];
 380       ALL_TAC] THEN
 381     DISCH_THEN(fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th) THEN
 382     CONJ_TAC THENL
 383      [MATCH_MP_TAC(TAUT `(~p /\ ~q ==> F) ==> p \/ q`) THEN
 384       REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; real_ge; REAL_NOT_LE] THEN
 385       DISCH_THEN(CONJUNCTS_THEN2
 386        (X_CHOOSE_TAC `u:real^3`) (X_CHOOSE_TAC `v:real^3`)) THEN
 387       SUBGOAL_THEN `(a':real^3) dot u < b' /\ a' dot v < b'` ASSUME_TAC THENL
 388        [REWRITE_TAC[REAL_LT_LE] THEN REWRITE_TAC
 389          [SET_RULE `f x <= b /\ ~(f x = b) <=>
 390                     x IN {x | f x <= b} /\ ~(x IN {x | f x = b})`] THEN
 391         ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[IN_ELIM_THM; REAL_LT_IMP_NE] THEN
 392         SUBGOAL_THEN `(u:real^3) IN convex hull s /\ v IN convex hull s`
 393         MP_TAC THENL [ASM_SIMP_TAC[HULL_INC]; ASM SET_TAC[]];
 394         ALL_TAC] THEN
 395       SUBGOAL_THEN `?w:real^3. w IN segment[u,v] /\ w IN {w | a' dot w = b'}`
 396       MP_TAC THENL
 397        [ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_ELIM_THM] THEN
 398         MATCH_MP_TAC CONNECTED_IVT_HYPERPLANE THEN
 399         MAP_EVERY EXISTS_TAC [`v:real^3`; `u:real^3`] THEN
 400         ASM_SIMP_TAC[ENDS_IN_SEGMENT; CONNECTED_SEGMENT; REAL_LT_IMP_LE];
 401         REWRITE_TAC[IN_SEGMENT; IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN
 402         ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 403         REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
 404         REWRITE_TAC[UNWIND_THM2; DOT_RADD; DOT_RMUL; CONJ_ASSOC] THEN
 405         DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
 406         MATCH_MP_TAC(REAL_ARITH `a < b ==> a = b ==> F`) THEN
 407         MATCH_MP_TAC REAL_CONVEX_BOUND_LT THEN ASM_REAL_ARITH_TAC];
 408       MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 409        [MATCH_MP_TAC HULL_MONO THEN REWRITE_TAC[SUBSET_INTER] THEN
 410         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
 411         EXISTS_TAC `convex hull t:real^3->bool` THEN
 412         REWRITE_TAC[HULL_SUBSET] THEN ASM SET_TAC[];
 413         FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
 414         REWRITE_TAC[SUBSET_INTER] THEN
 415         SIMP_TAC[HULL_MONO; INTER_SUBSET] THEN
 416         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
 417         EXISTS_TAC `convex hull {x:real^3 | a dot x = b}` THEN
 418         SIMP_TAC[HULL_MONO; INTER_SUBSET] THEN
 419         MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
 420         REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_HYPERPLANE]]];
 421     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 422     MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`; `z:real^3`] THEN
 423     REPEAT LET_TAC THEN
 424     DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN CONJ_TAC THENL
 425      [ASM_REWRITE_TAC[] THEN
 426       SUBGOAL_THEN
 427        `convex hull (s INTER {x:real^3 | a dot x = b}) =
 428         (convex hull s) INTER {x | a dot x = b}`
 429       SUBST1_TAC THENL
 430        [MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 431          [SIMP_TAC[SUBSET_INTER; HULL_MONO; INTER_SUBSET] THEN
 432           MATCH_MP_TAC SUBSET_TRANS THEN
 433           EXISTS_TAC `convex hull {x:real^3 | a dot x = b}` THEN
 434           SIMP_TAC[HULL_MONO; INTER_SUBSET] THEN
 435           MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
 436           REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_HYPERPLANE];
 437         ALL_TAC] THEN
 438       ASM_CASES_TAC `s SUBSET {x:real^3 | a dot x = b}` THENL
 439        [ASM_SIMP_TAC[SET_RULE `s SUBSET t ==> s INTER t = s`] THEN SET_TAC[];
 440         ALL_TAC] THEN
 441       MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
 442        `convex hull (convex hull (s INTER {x:real^3 | a dot x = b}) UNION
 443                      convex hull (s DIFF {x | a dot x = b})) INTER
 444         {x | a dot x = b}` THEN
 445       CONJ_TAC THENL
 446        [MATCH_MP_TAC(SET_RULE
 447          `s SUBSET t ==> (s INTER u) SUBSET (t INTER u)`) THEN
 448         MATCH_MP_TAC HULL_MONO THEN MATCH_MP_TAC(SET_RULE
 449          `s INTER t SUBSET (P hull (s INTER t)) /\
 450           s DIFF t SUBSET (P hull (s DIFF t))
 451           ==> s SUBSET (P hull (s INTER t)) UNION (P hull (s DIFF t))`) THEN
 452         REWRITE_TAC[HULL_SUBSET];
 453         ALL_TAC] THEN
 454       W(MP_TAC o PART_MATCH (lhs o rand) CONVEX_HULL_UNION_NONEMPTY_EXPLICIT o
 455         lhand o lhand o snd) THEN
 456       ANTS_TAC THENL
 457        [SIMP_TAC[CONVEX_CONVEX_HULL; CONVEX_HULL_EQ_EMPTY] THEN ASM SET_TAC[];
 458         DISCH_THEN SUBST1_TAC] THEN
 459       REWRITE_TAC[SUBSET; IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN
 460       MAP_EVERY X_GEN_TAC [`p:real^3`; `u:real`; `q:real^3`] THEN
 461       REPLICATE_TAC 4 DISCH_TAC THEN ASM_CASES_TAC `u = &0` THEN
 462       ASM_REWRITE_TAC[VECTOR_ARITH `(&1 - &0) % p + &0 % q:real^N = p`] THEN
 463       MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
 464       REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN FIRST_X_ASSUM DISJ_CASES_TAC THENL
 465        [MATCH_MP_TAC(REAL_ARITH `x < y ==> ~(x = y)`) THEN
 466         MATCH_MP_TAC(REAL_ARITH
 467          `(&1 - u) * p = (&1 - u) * b /\ u * q < u * b
 468           ==> (&1 - u) * p + u * q < b`) THEN
 469         CONJ_TAC THENL
 470          [SUBGOAL_THEN `p IN {x:real^3 | a dot x = b}` MP_TAC THENL
 471            [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
 472              `x IN s ==> s SUBSET t ==> x IN t`)) THEN
 473             MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HYPERPLANE] THEN
 474             SET_TAC[];
 475             SIMP_TAC[IN_ELIM_THM]];
 476           MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
 477            [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 478           ONCE_REWRITE_TAC[SET_RULE
 479            `(a:real^3) dot q < b <=> q IN {x | a dot x < b}`] THEN
 480           FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
 481            `x IN s ==> s SUBSET t ==> x IN t`)) THEN
 482           MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_LT] THEN
 483           ASM_SIMP_TAC[SUBSET; IN_DIFF; IN_ELIM_THM; REAL_LT_LE]];
 484         MATCH_MP_TAC(REAL_ARITH `x > y ==> ~(x = y)`) THEN
 485         MATCH_MP_TAC(REAL_ARITH
 486          `(&1 - u) * p = (&1 - u) * b /\ u * b < u * q
 487           ==> (&1 - u) * p + u * q > b`) THEN
 488         CONJ_TAC THENL
 489          [SUBGOAL_THEN `p IN {x:real^3 | a dot x = b}` MP_TAC THENL
 490            [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
 491              `x IN s ==> s SUBSET t ==> x IN t`)) THEN
 492             MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HYPERPLANE] THEN
 493             SET_TAC[];
 494             SIMP_TAC[IN_ELIM_THM]];
 495           MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
 496            [ASM_REAL_ARITH_TAC; REWRITE_TAC[GSYM real_gt]] THEN
 497           ONCE_REWRITE_TAC[SET_RULE
 498            `(a:real^3) dot q > b <=> q IN {x | a dot x > b}`] THEN
 499           FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
 500            `x IN s ==> s SUBSET t ==> x IN t`)) THEN
 501           MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_GT] THEN
 502           RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN
 503           ASM_SIMP_TAC[SUBSET; IN_DIFF; IN_ELIM_THM; real_gt; REAL_LT_LE]]];
 504         ALL_TAC] THEN
 505       FIRST_X_ASSUM DISJ_CASES_TAC THENL
 506        [MATCH_MP_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE THEN
 507         REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
 508         SIMP_TAC[SET_RULE `(!x. x IN s ==> P x) <=> s SUBSET {x | P x}`] THEN
 509         MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_LE] THEN
 510         ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
 511         MATCH_MP_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_GE THEN
 512         REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
 513         SIMP_TAC[SET_RULE `(!x. x IN s ==> P x) <=> s SUBSET {x | P x}`] THEN
 514         MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_GE] THEN
 515         ASM_SIMP_TAC[SUBSET; IN_ELIM_THM]];
 516       REWRITE_TAC[GSYM INT_LE_ANTISYM] THEN CONJ_TAC THENL
 517        [MATCH_MP_TAC INT_LE_TRANS THEN
 518         EXISTS_TAC `aff_dim {x:real^3 | a dot x = b}` THEN CONJ_TAC THENL
 519          [MATCH_MP_TAC AFF_DIM_SUBSET THEN ASM_REWRITE_TAC[] THEN
 520           MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HYPERPLANE] THEN
 521           SET_TAC[];
 522           ASM_SIMP_TAC[AFF_DIM_HYPERPLANE; DIMINDEX_3] THEN INT_ARITH_TAC];
 523         MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `aff_dim {x:real^3,y,z}` THEN
 524         CONJ_TAC THENL
 525          [SUBGOAL_THEN `~collinear{x:real^3,y,z}` MP_TAC THENL
 526            [ONCE_REWRITE_TAC[SET_RULE `{x,y,z} = {z,x,y}`] THEN
 527             ONCE_REWRITE_TAC[COLLINEAR_3] THEN
 528             ASM_REWRITE_TAC[GSYM CROSS_EQ_0];
 529             REWRITE_TAC[COLLINEAR_3_EQ_AFFINE_DEPENDENT; DE_MORGAN_THM] THEN
 530             STRIP_TAC] THEN
 531           ASM_SIMP_TAC[AFF_DIM_AFFINE_INDEPENDENT] THEN
 532           SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
 533           ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
 534           CONV_TAC INT_REDUCE_CONV;
 535           MATCH_MP_TAC AFF_DIM_SUBSET THEN ASM_REWRITE_TAC[INSERT_SUBSET] THEN
 536           REWRITE_TAC[EMPTY_SUBSET] THEN REPEAT CONJ_TAC THEN
 537           MATCH_MP_TAC HULL_INC THEN
 538           ASM_REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN
 539           MAP_EVERY UNDISCH_TAC
 540            [`(z - x) cross (y - x) = a`; `(a:real^3) dot x = b`] THEN
 541           VEC3_TAC]]]]);;
 542
 543 let COMPUTE_FACES_2_STEP_1 = prove
 544  (`!f v s t:real^3->bool.
 545        (?x y z. x IN (v INSERT s) /\ y IN (v INSERT s) /\ z IN (v INSERT s) /\
 546                 let a = (z - x) cross (y - x) in
 547                 ~(a = vec 0) /\
 548                 let b = a dot x in
 549                 ((!w. w IN t ==> a dot w <= b) \/
 550                  (!w. w IN t ==> a dot w >= b)) /\
 551                 f = convex hull (t INTER {x | a dot x = b})) <=>
 552        (?y z. y IN s /\ z IN s /\
 553                 let a = (z - v) cross (y - v) in
 554                 ~(a = vec 0) /\
 555                 let b = a dot v in
 556                 ((!w. w IN t ==> a dot w <= b) \/
 557                  (!w. w IN t ==> a dot w >= b)) /\
 558                 f = convex hull (t INTER {x | a dot x = b})) \/
 559        (?x y z. x IN s /\ y IN s /\ z IN s /\
 560                 let a = (z - x) cross (y - x) in
 561                 ~(a = vec 0) /\
 562                 let b = a dot x in
 563                 ((!w. w IN t ==> a dot w <= b) \/
 564                  (!w. w IN t ==> a dot w >= b)) /\
 565                 f = convex hull (t INTER {x | a dot x = b}))`,
 566   REPEAT GEN_TAC THEN REWRITE_TAC[IN_INSERT] THEN MATCH_MP_TAC(MESON[]
 567        `(!x y z. Q x y z ==> Q x z y) /\
 568         (!x y z. Q x y z ==> Q y x z) /\
 569         (!x z. ~(Q x x z))
 570         ==> ((?x y z. (x = v \/ P x) /\ (y = v \/ P y) /\ (z = v \/ P z) /\
 571              Q x y z) <=>
 572             (?y z. P y /\ P z /\ Q v y z) \/
 573             (?x y z. P x /\ P y /\ P z /\ Q x y z))`) THEN
 574   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 575   REWRITE_TAC[VECTOR_SUB_REFL; CROSS_0] THEN
 576   CONJ_TAC THEN REPEAT GEN_TAC THEN
 577   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 578   MAP_EVERY (SUBST1_TAC o VEC3_RULE)
 579    [`(z - y) cross (x - y) = --((z - x) cross (y - x))`;
 580     `(y - x) cross (z - x) =  --((z - x) cross (y - x))`] THEN
 581   REWRITE_TAC[VECTOR_NEG_EQ_0; DOT_LNEG; REAL_EQ_NEG2; REAL_LE_NEG2;
 582               real_ge] THEN
 583   REWRITE_TAC[DISJ_ACI] THEN
 584   REWRITE_TAC[VEC3_RULE
 585    `((z - x) cross (y - x)) dot y = ((z - x) cross (y - x)) dot x`]);;
 586
 587 let COMPUTE_FACES_2_STEP_2 = prove
 588  (`!f u v s:real^3->bool.
 589          (?y z. y IN (u INSERT s) /\ z IN (u INSERT s) /\
 590                 let a = (z - v) cross (y - v) in
 591                 ~(a = vec 0) /\
 592                 let b = a dot v in
 593                 ((!w. w IN t ==> a dot w <= b) \/
 594                  (!w. w IN t ==> a dot w >= b)) /\
 595                 f = convex hull (t INTER {x | a dot x = b})) <=>
 596          (?z. z IN s /\
 597               let a = (z - v) cross (u - v) in
 598               ~(a = vec 0) /\
 599               let b = a dot v in
 600               ((!w. w IN t ==> a dot w <= b) \/
 601                (!w. w IN t ==> a dot w >= b)) /\
 602               f = convex hull (t INTER {x | a dot x = b})) \/
 603          (?y z. y IN s /\ z IN s /\
 604                 let a = (z - v) cross (y - v) in
 605                 ~(a = vec 0) /\
 606                 let b = a dot v in
 607                 ((!w. w IN t ==> a dot w <= b) \/
 608                  (!w. w IN t ==> a dot w >= b)) /\
 609                 f = convex hull (t INTER {x | a dot x = b}))`,
 610   REPEAT GEN_TAC THEN REWRITE_TAC[IN_INSERT] THEN MATCH_MP_TAC(MESON[]
 611        `(!x y. Q x y ==> Q y x) /\
 612         (!x. ~(Q x x))
 613         ==> ((?y z. (y = u \/ P y) /\ (z = u \/ P z) /\
 614              Q y z) <=>
 615             (?z. P z /\ Q u z) \/
 616             (?y z. P y /\ P z /\ Q y z))`) THEN
 617   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 618   REWRITE_TAC[CROSS_REFL] THEN REPEAT GEN_TAC THEN
 619   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN SUBST1_TAC
 620    (VEC3_RULE `(x - v) cross (y - v) = --((y - v) cross (x - v))`) THEN
 621   REWRITE_TAC[VECTOR_NEG_EQ_0; DOT_LNEG; REAL_EQ_NEG2; REAL_LE_NEG2;
 622               real_ge] THEN REWRITE_TAC[DISJ_ACI]);;
 623
 624 let COMPUTE_FACES_TAC =
 625   let lemma = prove
 626    (`(x INSERT s) INTER {x | P x} =
 627                         if P x then x INSERT (s INTER {x | P x})
 628                         else s INTER {x | P x}`,
 629     COND_CASES_TAC THEN ASM SET_TAC[]) in
 630   SIMP_TAC[COMPUTE_FACES_2; FINITE_INSERT; FINITE_EMPTY] THEN
 631   REWRITE_TAC[COMPUTE_FACES_2_STEP_1] THEN
 632   REWRITE_TAC[COMPUTE_FACES_2_STEP_2] THEN
 633   REWRITE_TAC[NOT_IN_EMPTY] THEN
 634   REWRITE_TAC[EXISTS_IN_INSERT; NOT_IN_EMPTY] THEN
 635   REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
 636   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_SUB_CONV) THEN
 637   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_CROSS_CONV) THEN
 638   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 639   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_EQ_0_CONV) THEN
 640   REWRITE_TAC[real_ge] THEN
 641   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_DOT_CONV) THEN
 642   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 643   CONV_TAC(ONCE_DEPTH_CONV REAL_RAT5_LE_CONV) THEN
 644   REWRITE_TAC[INSERT_AC] THEN REWRITE_TAC[DISJ_ACI] THEN
 645   REPEAT(CHANGED_TAC
 646    (ONCE_REWRITE_TAC[lemma] THEN
 647     CONV_TAC(ONCE_DEPTH_CONV
 648      (LAND_CONV VECTOR3_DOT_CONV THENC REAL_RAT5_EQ_CONV))) THEN
 649     REWRITE_TAC[]) THEN
 650   REWRITE_TAC[INTER_EMPTY] THEN
 651   REWRITE_TAC[INSERT_AC] THEN REWRITE_TAC[DISJ_ACI];;
 652
 653 (* ------------------------------------------------------------------------- *)
 654 (* Apply this to our standard Platonic solids to derive facets.              *)
 655 (* Note: this is quite slow and can take a couple of hours.                  *)
 656 (* ------------------------------------------------------------------------- *)
 657
 658 let TETRAHEDRON_FACETS = time prove
 659  (`!f:real^3->bool.
 660         f face_of std_tetrahedron /\ aff_dim f = &2 <=>
 661         f = convex hull {vector[-- &1; -- &1; &1], vector[-- &1; &1; -- &1], vector[&1; -- &1; -- &1]} \/
 662         f = convex hull {vector[-- &1; -- &1; &1], vector[-- &1; &1; -- &1], vector[&1; &1; &1]} \/
 663         f = convex hull {vector[-- &1; -- &1; &1], vector[&1; -- &1; -- &1], vector[&1; &1; &1]} \/
 664         f = convex hull {vector[-- &1; &1; -- &1], vector[&1; -- &1; -- &1], vector[&1; &1; &1]}`,
 665   GEN_TAC THEN REWRITE_TAC[std_tetrahedron] THEN COMPUTE_FACES_TAC);;
 666
 667 let CUBE_FACETS = time prove
 668  (`!f:real^3->bool.
 669         f face_of std_cube /\ aff_dim f = &2 <=>
 670         f = convex hull {vector[-- &1; -- &1; -- &1], vector[-- &1; -- &1; &1], vector[-- &1; &1; -- &1], vector[-- &1; &1; &1]} \/
 671         f = convex hull {vector[-- &1; -- &1; -- &1], vector[-- &1; -- &1; &1], vector[&1; -- &1; -- &1], vector[&1; -- &1; &1]} \/
 672         f = convex hull {vector[-- &1; -- &1; -- &1], vector[-- &1; &1; -- &1], vector[&1; -- &1; -- &1], vector[&1; &1; -- &1]} \/
 673         f = convex hull {vector[-- &1; -- &1; &1], vector[-- &1; &1; &1], vector[&1; -- &1; &1], vector[&1; &1; &1]} \/
 674         f = convex hull {vector[-- &1; &1; -- &1], vector[-- &1; &1; &1], vector[&1; &1; -- &1], vector[&1; &1; &1]} \/
 675         f = convex hull {vector[&1; -- &1; -- &1], vector[&1; -- &1; &1], vector[&1; &1; -- &1], vector[&1; &1; &1]}`,
 676   GEN_TAC THEN REWRITE_TAC[std_cube] THEN COMPUTE_FACES_TAC);;
 677
 678 let OCTAHEDRON_FACETS = time prove
 679  (`!f:real^3->bool.
 680         f face_of std_octahedron /\ aff_dim f = &2 <=>
 681         f = convex hull {vector[-- &1; &0; &0], vector[&0; -- &1; &0], vector[&0; &0; -- &1]} \/
 682         f = convex hull {vector[-- &1; &0; &0], vector[&0; -- &1; &0], vector[&0; &0; &1]} \/
 683         f = convex hull {vector[-- &1; &0; &0], vector[&0; &1; &0], vector[&0; &0; -- &1]} \/
 684         f = convex hull {vector[-- &1; &0; &0], vector[&0; &1; &0], vector[&0; &0; &1]} \/
 685         f = convex hull {vector[&1; &0; &0], vector[&0; -- &1; &0], vector[&0; &0; -- &1]} \/
 686         f = convex hull {vector[&1; &0; &0], vector[&0; -- &1; &0], vector[&0; &0; &1]} \/
 687         f = convex hull {vector[&1; &0; &0], vector[&0; &1; &0], vector[&0; &0; -- &1]} \/
 688         f = convex hull {vector[&1; &0; &0], vector[&0; &1; &0], vector[&0; &0; &1]}`,
 689   GEN_TAC THEN REWRITE_TAC[std_octahedron] THEN COMPUTE_FACES_TAC);;
 690
 691 let ICOSAHEDRON_FACETS = time prove
 692  (`!f:real^3->bool.
 693         f face_of std_icosahedron /\ aff_dim f = &2 <=>
 694         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1], vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1], vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0]} \/
 695         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1], vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1], vector[-- &1; &1 / &2 + &1 / &2 * sqrt(&5); &0]} \/
 696         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1], vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 697         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1], vector[-- &1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 698         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 699         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1], vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 700         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1], vector[-- &1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 701         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt(&5)], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 702         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1], vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0]} \/
 703         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1], vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1], vector[&1; &1 / &2 + &1 / &2 * sqrt(&5); &0]} \/
 704         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 705         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1], vector[&1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 706         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 707         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 708         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1], vector[&1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 709         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt(&5)], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 710         f = convex hull {vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 711         f = convex hull {vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 712         f = convex hull {vector[-- &1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 713         f = convex hull {vector[-- &1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&1; &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt(&5)]}`,
 714   GEN_TAC THEN REWRITE_TAC[STD_ICOSAHEDRON] THEN COMPUTE_FACES_TAC);;
 715
 716 let DODECAHEDRON_FACETS = time prove
 717  (`!f:real^3->bool.
 718         f face_of std_dodecahedron /\ aff_dim f = &2 <=>
 719         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)], vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[-- &1; -- &1; -- &1], vector[-- &1; -- &1; &1]} \/
 720         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)], vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[-- &1; &1; -- &1], vector[-- &1; &1; &1]} \/
 721         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)], vector[-- &1; -- &1; &1], vector[-- &1; &1; &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)], vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 722         f = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[-- &1; -- &1; -- &1], vector[-- &1; &1; -- &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 723         f = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[-- &1; -- &1; -- &1], vector[&1; -- &1; -- &1], vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 724         f = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[-- &1; -- &1; &1], vector[&1; -- &1; &1], vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 725         f = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5); &0], vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)], vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&1; -- &1; -- &1], vector[&1; -- &1; &1]} \/
 726         f = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[-- &1; &1; -- &1], vector[&1; &1; -- &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)]} \/
 727         f = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[-- &1; &1; &1], vector[&1; &1; &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 728         f = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5); &0], vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)], vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&1; &1; -- &1], vector[&1; &1; &1]} \/
 729         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; -- &1 / &2 + &1 / &2 * sqrt(&5)], vector[&1; -- &1; &1], vector[&1; &1; &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)], vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); &1 / &2 + &1 / &2 * sqrt(&5)]} \/
 730         f = convex hull {vector[&1 / &2 + &1 / &2 * sqrt(&5); &0; &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&1; -- &1; -- &1], vector[&1; &1; -- &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)], vector[&0; &1 / &2 + -- &1 / &2 * sqrt(&5); -- &1 / &2 + -- &1 / &2 * sqrt(&5)]}`,
 731   GEN_TAC THEN REWRITE_TAC[STD_DODECAHEDRON] THEN COMPUTE_FACES_TAC);;
 732
 733 (* ------------------------------------------------------------------------- *)
 734 (* Given a coplanar set, return a hyperplane containing it.                  *)
 735 (* Maps term s to theorem |- !x. x IN s ==> n dot x = d                      *)
 736 (* Currently assumes |s| >= 3 but it would be trivial to do other cases.     *)
 737 (* ------------------------------------------------------------------------- *)
 738
 739 let COPLANAR_HYPERPLANE_RULE =
 740   let rec allsets m l =
 741     if m = 0 then [[]] else
 742     match l with
 743       [] -> []
 744     | h::t -> map (fun g -> h::g) (allsets (m - 1) t) @ allsets m t in
 745   let mk_sub = mk_binop `(-):real^3->real^3->real^3`
 746   and mk_cross = mk_binop `cross`
 747   and mk_dot = mk_binop `(dot):real^3->real^3->real`
 748   and zerovec_tm = `vector[&0;&0;&0]:real^3`
 749   and template = `(!x:real^3. x IN s ==> n dot x = d)`
 750   and s_tm = `s:real^3->bool`
 751   and n_tm = `n:real^3`
 752   and d_tm = `d:real` in
 753   let mk_normal [x;y;z] = mk_cross (mk_sub y x) (mk_sub z x) in
 754   let eval_normal t =
 755     (BINOP_CONV VECTOR3_SUB_CONV THENC VECTOR3_CROSS_CONV) (mk_normal t) in
 756   let check_normal t =
 757     let th = eval_normal t in
 758     let n = rand(concl th) in
 759     if n = zerovec_tm then failwith "check_normal" else n in
 760   fun tm ->
 761     let s = dest_setenum tm in
 762     if length s < 3 then failwith "COPLANAR_HYPERPLANE_RULE: trivial" else
 763     let n = tryfind check_normal (allsets 3 s) in
 764     let d = rand(concl(VECTOR3_DOT_CONV(mk_dot n (hd s)))) in
 765     let ptm = vsubst [tm,s_tm; n,n_tm; d,d_tm] template in
 766     EQT_ELIM
 767     ((REWRITE_CONV[FORALL_IN_INSERT; NOT_IN_EMPTY] THENC
 768       DEPTH_BINOP_CONV `/\`
 769        (LAND_CONV VECTOR3_DOT_CONV THENC REAL_RAT5_EQ_CONV) THENC
 770       GEN_REWRITE_CONV DEPTH_CONV [AND_CLAUSES]) ptm);;
 771
 772 (* ------------------------------------------------------------------------- *)
 773 (* Explicit computation of edges, assuming hyperplane containing the set.    *)
 774 (* ------------------------------------------------------------------------- *)
 775
 776 let COMPUTE_FACES_1 = prove
 777  (`!s:real^3->bool n d.
 778         (!x. x IN s ==> n dot x = d)
 779         ==> FINITE s /\ ~(n = vec 0)
 780             ==> !f. f face_of (convex hull s) /\ aff_dim f = &1 <=>
 781                     ?x y. x IN s /\ y IN s /\
 782                           let a = n cross (y - x) in
 783                           ~(a = vec 0) /\
 784                           let b = a dot x in
 785                           ((!w. w IN s ==> a dot w <= b) \/
 786                            (!w. w IN s ==> a dot w >= b)) /\
 787                           f = convex hull (s INTER {x | a dot x = b})`,
 788   REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN GEN_TAC THEN EQ_TAC THENL
 789    [STRIP_TAC THEN
 790     SUBGOAL_THEN `?t:real^3->bool. t SUBSET s /\ f = convex hull t`
 791     MP_TAC THENL
 792      [MATCH_MP_TAC FACE_OF_CONVEX_HULL_SUBSET THEN
 793       ASM_SIMP_TAC[FINITE_IMP_COMPACT];
 794       DISCH_THEN(X_CHOOSE_THEN `t:real^3->bool` MP_TAC)] THEN
 795     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
 796     RULE_ASSUM_TAC(REWRITE_RULE[AFF_DIM_CONVEX_HULL]) THEN
 797     MP_TAC(ISPEC `t:real^3->bool` AFFINE_BASIS_EXISTS) THEN
 798     DISCH_THEN(X_CHOOSE_THEN `u:real^3->bool` STRIP_ASSUME_TAC) THEN
 799     SUBGOAL_THEN `(u:real^3->bool) HAS_SIZE 2` MP_TAC THENL
 800      [ASM_SIMP_TAC[HAS_SIZE; AFFINE_INDEPENDENT_IMP_FINITE] THEN
 801       REWRITE_TAC[GSYM INT_OF_NUM_EQ] THEN MATCH_MP_TAC(INT_ARITH
 802        `aff_dim(u:real^3->bool) = &1 /\ aff_dim u = &(CARD u) - &1
 803         ==> &(CARD u):int = &2`) THEN CONJ_TAC
 804       THENL [ASM_MESON_TAC[AFF_DIM_AFFINE_HULL]; ASM_MESON_TAC[AFF_DIM_UNIQUE]];
 805       ALL_TAC] THEN
 806     CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
 807     MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN
 808     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
 809     MAP_EVERY EXISTS_TAC  [`x:real^3`; `y:real^3`] THEN
 810     REPLICATE_TAC 2 (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
 811     SUBGOAL_THEN `(x:real^3) IN s /\ y IN s` STRIP_ASSUME_TAC THENL
 812      [ASM SET_TAC[]; ALL_TAC] THEN
 813     REPEAT LET_TAC THEN
 814     MP_TAC(ISPECL [`n:real^3`; `y - x:real^3`] NORM_AND_CROSS_EQ_0) THEN
 815     ASM_SIMP_TAC[DOT_RSUB; VECTOR_SUB_EQ; REAL_SUB_0] THEN DISCH_TAC THEN
 816     SUBGOAL_THEN `(a:real^3) dot y = b` ASSUME_TAC THENL
 817      [MAP_EVERY UNDISCH_TAC
 818        [`n cross (y - x) = a`; `(a:real^3) dot x = b`] THEN VEC3_TAC;
 819       ALL_TAC] THEN
 820     MP_TAC(ISPECL [`convex hull s:real^3->bool`; `convex hull t:real^3->bool`]
 821         EXPOSED_FACE_OF_POLYHEDRON) THEN
 822     ASM_SIMP_TAC[POLYHEDRON_CONVEX_HULL; EXPOSED_FACE_OF_PARALLEL] THEN
 823     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 824     MAP_EVERY X_GEN_TAC [`a':real^3`; `b':real`] THEN
 825     SUBGOAL_THEN `~(convex hull t:real^3->bool = {})` ASSUME_TAC THENL
 826      [REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN EXISTS_TAC `x:real^3` THEN
 827       MATCH_MP_TAC HULL_INC THEN ASM SET_TAC[];
 828       ASM_REWRITE_TAC[]] THEN
 829     ASM_CASES_TAC `convex hull t:real^3->bool = convex hull s` THEN
 830     ASM_REWRITE_TAC[] THENL
 831      [FIRST_X_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE RAND_CONV
 832         [GSYM AFFINE_HULL_CONVEX_HULL]) THEN
 833       UNDISCH_THEN `convex hull t:real^3->bool = convex hull s`
 834        (fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th) THEN
 835       RULE_ASSUM_TAC(REWRITE_RULE[AFFINE_HULL_CONVEX_HULL]) THEN
 836       REWRITE_TAC[SET_RULE `s = s INTER t <=> s SUBSET t`] THEN STRIP_TAC THEN
 837       SUBGOAL_THEN `s SUBSET {x:real^3 | a dot x = b}` ASSUME_TAC THENL
 838        [MATCH_MP_TAC SUBSET_TRANS THEN
 839         EXISTS_TAC `affine hull s:real^3->bool` THEN
 840         REWRITE_TAC[HULL_SUBSET] THEN
 841         FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
 842         MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[AFFINE_HYPERPLANE] THEN
 843         ASM SET_TAC[];
 844         CONJ_TAC THENL
 845          [RULE_ASSUM_TAC(REWRITE_RULE[SUBSET; IN_ELIM_THM]) THEN
 846           ASM_SIMP_TAC[real_ge; REAL_LE_REFL];
 847           AP_TERM_TAC THEN ASM SET_TAC[]]];
 848       STRIP_TAC] THEN
 849     RULE_ASSUM_TAC(REWRITE_RULE[AFFINE_HULL_CONVEX_HULL]) THEN
 850     SUBGOAL_THEN
 851      `aff_dim(t:real^3->bool)
 852       <= aff_dim(({x:real^3 | a dot x = b} INTER {x:real^3 | a' dot x = b'})
 853                  INTER {x | n dot x = d})`
 854     MP_TAC THENL
 855      [GEN_REWRITE_TAC LAND_CONV [GSYM AFF_DIM_AFFINE_HULL] THEN
 856       FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
 857        [SYM th]) THEN
 858       REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN MATCH_MP_TAC AFF_DIM_SUBSET THEN
 859       REWRITE_TAC[SUBSET_INTER; INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN
 860       ASM_SIMP_TAC[] THEN
 861       SUBGOAL_THEN `(x:real^3) IN convex hull t /\ y IN convex hull t`
 862       MP_TAC THENL
 863        [CONJ_TAC THEN MATCH_MP_TAC HULL_INC THEN ASM SET_TAC[];
 864         ASM SET_TAC[]];
 865       ALL_TAC] THEN
 866     ASM_SIMP_TAC[AFF_DIM_AFFINE_INTER_HYPERPLANE; AFF_DIM_HYPERPLANE;
 867                  AFFINE_HYPERPLANE; DIMINDEX_3; AFFINE_INTER] THEN
 868     ASM_CASES_TAC `{x:real^3 | a dot x = b} SUBSET {v | a' dot v = b'}` THEN
 869     ASM_REWRITE_TAC[] THENL
 870      [ALL_TAC;
 871       REPEAT(COND_CASES_TAC THEN CONV_TAC INT_REDUCE_CONV) THEN
 872       FIRST_X_ASSUM(MP_TAC o MATCH_MP (SET_RULE
 873        `s INTER t SUBSET u ==> !x. x IN s /\ x IN t ==> x IN u`)) THEN
 874       DISCH_THEN(MP_TAC o SPEC `x + n:real^3`) THEN
 875       MATCH_MP_TAC(TAUT `p /\ q /\ ~r ==> (p /\ q ==> r) ==> s`) THEN
 876       ASM_SIMP_TAC[IN_ELIM_THM; DOT_RADD] THEN REPEAT CONJ_TAC THENL
 877        [EXPAND_TAC "a" THEN VEC3_TAC;
 878         ALL_TAC;
 879         ASM_REWRITE_TAC[REAL_EQ_ADD_LCANCEL_0; DOT_EQ_0]] THEN
 880       SUBGOAL_THEN `a' dot (x:real^3) = b'` SUBST1_TAC THENL
 881        [SUBGOAL_THEN `(x:real^3) IN convex hull t` MP_TAC THENL
 882          [MATCH_MP_TAC HULL_INC THEN ASM SET_TAC[]; ASM SET_TAC[]];
 883         ALL_TAC] THEN
 884       SUBGOAL_THEN `(n:real^3) dot (x + a') = n dot x` MP_TAC THENL
 885        [ALL_TAC;
 886         SIMP_TAC[DOT_RADD] THEN REWRITE_TAC[DOT_SYM] THEN REAL_ARITH_TAC] THEN
 887       MATCH_MP_TAC(REAL_ARITH `x:real = d /\ y = d ==> x = y`) THEN
 888       SUBGOAL_THEN
 889        `affine hull s SUBSET {x:real^3 | n dot x = d}`
 890       MP_TAC THENL
 891        [MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[AFFINE_HYPERPLANE] THEN
 892         ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
 893         REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_SIMP_TAC[HULL_INC]]] THEN
 894     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SUBSET_HYPERPLANES]) THEN
 895     ASM_REWRITE_TAC[HYPERPLANE_EQ_EMPTY; HYPERPLANE_EQ_UNIV] THEN
 896     DISCH_THEN(fun th -> DISCH_THEN(K ALL_TAC) THEN MP_TAC(SYM th)) THEN
 897     DISCH_THEN(fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th) THEN
 898     CONJ_TAC THENL
 899      [MATCH_MP_TAC(TAUT `(~p /\ ~q ==> F) ==> p \/ q`) THEN
 900       REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; real_ge; REAL_NOT_LE] THEN
 901       DISCH_THEN(CONJUNCTS_THEN2
 902        (X_CHOOSE_TAC `u:real^3`) (X_CHOOSE_TAC `v:real^3`)) THEN
 903       SUBGOAL_THEN `(a':real^3) dot u < b' /\ a' dot v < b'` ASSUME_TAC THENL
 904        [REWRITE_TAC[REAL_LT_LE] THEN REWRITE_TAC
 905          [SET_RULE `f x <= b /\ ~(f x = b) <=>
 906                     x IN {x | f x <= b} /\ ~(x IN {x | f x = b})`] THEN
 907         ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[IN_ELIM_THM; REAL_LT_IMP_NE] THEN
 908         SUBGOAL_THEN `(u:real^3) IN convex hull s /\ v IN convex hull s`
 909         MP_TAC THENL [ASM_SIMP_TAC[HULL_INC]; ASM SET_TAC[]];
 910         ALL_TAC] THEN
 911       SUBGOAL_THEN `?w:real^3. w IN segment[u,v] /\ w IN {w | a' dot w = b'}`
 912       MP_TAC THENL
 913        [ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_ELIM_THM] THEN
 914         MATCH_MP_TAC CONNECTED_IVT_HYPERPLANE THEN
 915         MAP_EVERY EXISTS_TAC [`v:real^3`; `u:real^3`] THEN
 916         ASM_SIMP_TAC[ENDS_IN_SEGMENT; CONNECTED_SEGMENT; REAL_LT_IMP_LE];
 917         REWRITE_TAC[IN_SEGMENT; IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN
 918         ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 919         REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
 920         REWRITE_TAC[UNWIND_THM2; DOT_RADD; DOT_RMUL; CONJ_ASSOC] THEN
 921         DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
 922         MATCH_MP_TAC(REAL_ARITH `a < b ==> a = b ==> F`) THEN
 923         MATCH_MP_TAC REAL_CONVEX_BOUND_LT THEN ASM_REAL_ARITH_TAC];
 924       FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
 925       MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 926        [MATCH_MP_TAC HULL_MONO THEN REWRITE_TAC[SUBSET_INTER] THEN
 927         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
 928         EXISTS_TAC `convex hull t:real^3->bool` THEN
 929         REWRITE_TAC[HULL_SUBSET] THEN ASM SET_TAC[];
 930         ASM_REWRITE_TAC[SUBSET_INTER] THEN
 931         SIMP_TAC[HULL_MONO; INTER_SUBSET] THEN
 932         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
 933         EXISTS_TAC `convex hull {x:real^3 | a dot x = b}` THEN
 934         SIMP_TAC[HULL_MONO; INTER_SUBSET] THEN
 935         MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
 936         REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_HYPERPLANE]]];
 937     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 938     MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN
 939     REPEAT LET_TAC THEN
 940     DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN CONJ_TAC THENL
 941      [ASM_REWRITE_TAC[] THEN
 942       SUBGOAL_THEN
 943        `convex hull (s INTER {x:real^3 | a dot x = b}) =
 944         (convex hull s) INTER {x | a dot x = b}`
 945       SUBST1_TAC THENL
 946        [MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 947          [SIMP_TAC[SUBSET_INTER; HULL_MONO; INTER_SUBSET] THEN
 948           MATCH_MP_TAC SUBSET_TRANS THEN
 949           EXISTS_TAC `convex hull {x:real^3 | a dot x = b}` THEN
 950           SIMP_TAC[HULL_MONO; INTER_SUBSET] THEN
 951           MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
 952           REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_HYPERPLANE];
 953           ALL_TAC] THEN
 954       ASM_CASES_TAC `s SUBSET {x:real^3 | a dot x = b}` THENL
 955        [ASM_SIMP_TAC[SET_RULE `s SUBSET t ==> s INTER t = s`] THEN SET_TAC[];
 956         ALL_TAC] THEN
 957       MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
 958        `convex hull (convex hull (s INTER {x:real^3 | a dot x = b}) UNION
 959                      convex hull (s DIFF {x | a dot x = b})) INTER
 960         {x | a dot x = b}` THEN
 961       CONJ_TAC THENL
 962        [MATCH_MP_TAC(SET_RULE
 963          `s SUBSET t ==> (s INTER u) SUBSET (t INTER u)`) THEN
 964         MATCH_MP_TAC HULL_MONO THEN MATCH_MP_TAC(SET_RULE
 965          `s INTER t SUBSET (P hull (s INTER t)) /\
 966           s DIFF t SUBSET (P hull (s DIFF t))
 967           ==> s SUBSET (P hull (s INTER t)) UNION (P hull (s DIFF t))`) THEN
 968         REWRITE_TAC[HULL_SUBSET];
 969         ALL_TAC] THEN
 970       W(MP_TAC o PART_MATCH (lhs o rand) CONVEX_HULL_UNION_NONEMPTY_EXPLICIT o
 971         lhand o lhand o snd) THEN
 972       ANTS_TAC THENL
 973        [SIMP_TAC[CONVEX_CONVEX_HULL; CONVEX_HULL_EQ_EMPTY] THEN ASM SET_TAC[];
 974         DISCH_THEN SUBST1_TAC] THEN
 975       REWRITE_TAC[SUBSET; IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN
 976       MAP_EVERY X_GEN_TAC [`p:real^3`; `u:real`; `q:real^3`] THEN
 977       REPLICATE_TAC 4 DISCH_TAC THEN ASM_CASES_TAC `u = &0` THEN
 978       ASM_REWRITE_TAC[VECTOR_ARITH `(&1 - &0) % p + &0 % q:real^N = p`] THEN
 979       MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
 980       REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN FIRST_X_ASSUM DISJ_CASES_TAC THENL
 981        [MATCH_MP_TAC(REAL_ARITH `x < y ==> ~(x = y)`) THEN
 982         MATCH_MP_TAC(REAL_ARITH
 983          `(&1 - u) * p = (&1 - u) * b /\ u * q < u * b
 984           ==> (&1 - u) * p + u * q < b`) THEN
 985         CONJ_TAC THENL
 986          [SUBGOAL_THEN `p IN {x:real^3 | a dot x = b}` MP_TAC THENL
 987            [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
 988              `x IN s ==> s SUBSET t ==> x IN t`)) THEN
 989             MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HYPERPLANE] THEN
 990             SET_TAC[];
 991             SIMP_TAC[IN_ELIM_THM]];
 992           MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
 993            [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 994           ONCE_REWRITE_TAC[SET_RULE
 995            `(a:real^3) dot q < b <=> q IN {x | a dot x < b}`] THEN
 996           FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
 997            `x IN s ==> s SUBSET t ==> x IN t`)) THEN
 998           MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_LT] THEN
 999           ASM_SIMP_TAC[SUBSET; IN_DIFF; IN_ELIM_THM; REAL_LT_LE]];
1000         MATCH_MP_TAC(REAL_ARITH `x > y ==> ~(x = y)`) THEN
1001         MATCH_MP_TAC(REAL_ARITH
1002          `(&1 - u) * p = (&1 - u) * b /\ u * b < u * q
1003           ==> (&1 - u) * p + u * q > b`) THEN
1004         CONJ_TAC THENL
1005          [SUBGOAL_THEN `p IN {x:real^3 | a dot x = b}` MP_TAC THENL
1006            [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
1007              `x IN s ==> s SUBSET t ==> x IN t`)) THEN
1008             MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HYPERPLANE] THEN
1009             SET_TAC[];
1010             SIMP_TAC[IN_ELIM_THM]];
1011           MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
1012            [ASM_REAL_ARITH_TAC; REWRITE_TAC[GSYM real_gt]] THEN
1013           ONCE_REWRITE_TAC[SET_RULE
1014            `(a:real^3) dot q > b <=> q IN {x | a dot x > b}`] THEN
1015           FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
1016            `x IN s ==> s SUBSET t ==> x IN t`)) THEN
1017           MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_GT] THEN
1018           RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN
1019           ASM_SIMP_TAC[SUBSET; IN_DIFF; IN_ELIM_THM; real_gt; REAL_LT_LE]]];
1020         ALL_TAC] THEN
1021       FIRST_X_ASSUM DISJ_CASES_TAC THENL
1022        [MATCH_MP_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE THEN
1023         REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
1024         SIMP_TAC[SET_RULE `(!x. x IN s ==> P x) <=> s SUBSET {x | P x}`] THEN
1025         MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_LE] THEN
1026         ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
1027         MATCH_MP_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_GE THEN
1028         REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
1029         SIMP_TAC[SET_RULE `(!x. x IN s ==> P x) <=> s SUBSET {x | P x}`] THEN
1030         MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_HALFSPACE_GE] THEN
1031         ASM_SIMP_TAC[SUBSET; IN_ELIM_THM]];
1032       ASM_REWRITE_TAC[GSYM INT_LE_ANTISYM] THEN CONJ_TAC THENL
1033        [ALL_TAC;
1034         MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `aff_dim{x:real^3,y}` THEN
1035         CONJ_TAC THENL
1036          [ASM_REWRITE_TAC[AFF_DIM_2] THEN
1037           ASM_MESON_TAC[CROSS_0; VECTOR_SUB_REFL; INT_LE_REFL];
1038           MATCH_MP_TAC AFF_DIM_SUBSET THEN
1039           REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
1040           CONJ_TAC THEN MATCH_MP_TAC HULL_INC THEN
1041           ASM_REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN
1042           MAP_EVERY UNDISCH_TAC
1043            [`n cross (y - x) = a`; `(a:real^3) dot x = b`] THEN
1044           VEC3_TAC]] THEN
1045       REWRITE_TAC[AFF_DIM_CONVEX_HULL] THEN MATCH_MP_TAC INT_LE_TRANS THEN
1046       EXISTS_TAC
1047        `aff_dim({x:real^3 | a dot x = b} INTER {x | n dot x = d})` THEN
1048       CONJ_TAC THENL
1049        [MATCH_MP_TAC AFF_DIM_SUBSET THEN ASM SET_TAC[]; ALL_TAC] THEN
1050       ASM_SIMP_TAC[AFF_DIM_AFFINE_INTER_HYPERPLANE; AFFINE_HYPERPLANE;
1051                    AFF_DIM_HYPERPLANE; DIMINDEX_3] THEN
1052       REPEAT(COND_CASES_TAC THEN CONV_TAC INT_REDUCE_CONV) THEN
1053       FIRST_X_ASSUM(MP_TAC o SPEC `x + n:real^3` o
1054         GEN_REWRITE_RULE I [SUBSET]) THEN
1055       ASM_SIMP_TAC[IN_ELIM_THM; DOT_RADD; REAL_EQ_ADD_LCANCEL_0; DOT_EQ_0] THEN
1056       EXPAND_TAC "a" THEN VEC3_TAC]]);;
1057
1058 (* ------------------------------------------------------------------------- *)
1059 (* Given a coplanar set, return exhaustive edge case theorem.                *)
1060 (* ------------------------------------------------------------------------- *)
1061
1062 let COMPUTE_EDGES_CONV =
1063   let lemma = prove
1064    (`(x INSERT s) INTER {x | P x} =
1065                         if P x then x INSERT (s INTER {x | P x})
1066                         else s INTER {x | P x}`,
1067     COND_CASES_TAC THEN ASM SET_TAC[]) in
1068   fun tm ->
1069     let th1 = MATCH_MP COMPUTE_FACES_1 (COPLANAR_HYPERPLANE_RULE tm) in
1070     let th2 = MP (CONV_RULE(LAND_CONV
1071      (COMB2_CONV (RAND_CONV(PURE_REWRITE_CONV[FINITE_INSERT; FINITE_EMPTY]))
1072                  (RAND_CONV VECTOR3_EQ_0_CONV THENC
1073                   GEN_REWRITE_CONV I [NOT_CLAUSES]) THENC
1074       GEN_REWRITE_CONV I [AND_CLAUSES])) th1) TRUTH in
1075     CONV_RULE
1076      (BINDER_CONV(RAND_CONV
1077         (REWRITE_CONV[RIGHT_EXISTS_AND_THM] THENC
1078          REWRITE_CONV[EXISTS_IN_INSERT; NOT_IN_EMPTY] THENC
1079          REWRITE_CONV[FORALL_IN_INSERT; NOT_IN_EMPTY] THENC
1080          ONCE_DEPTH_CONV VECTOR3_SUB_CONV THENC
1081          ONCE_DEPTH_CONV VECTOR3_CROSS_CONV THENC
1082          ONCE_DEPTH_CONV let_CONV THENC
1083          ONCE_DEPTH_CONV VECTOR3_EQ_0_CONV THENC
1084          REWRITE_CONV[real_ge] THENC
1085          ONCE_DEPTH_CONV VECTOR3_DOT_CONV THENC
1086          ONCE_DEPTH_CONV let_CONV THENC
1087          ONCE_DEPTH_CONV REAL_RAT5_LE_CONV THENC
1088          REWRITE_CONV[INSERT_AC] THENC REWRITE_CONV[DISJ_ACI] THENC
1089          REPEATC(CHANGED_CONV
1090           (ONCE_REWRITE_CONV[lemma] THENC
1091            ONCE_DEPTH_CONV(LAND_CONV VECTOR3_DOT_CONV THENC
1092                            REAL_RAT5_EQ_CONV) THENC
1093            REWRITE_CONV[])) THENC
1094          REWRITE_CONV[INTER_EMPTY] THENC
1095          REWRITE_CONV[INSERT_AC] THENC REWRITE_CONV[DISJ_ACI]
1096         ))) th2;;
1097
1098 (* ------------------------------------------------------------------------- *)
1099 (* Use this to prove the number of edges per face for each Platonic solid.   *)
1100 (* ------------------------------------------------------------------------- *)
1101
1102 let CARD_EQ_LEMMA = prove
1103  (`!x s n. 0 < n /\ ~(x IN s) /\ s HAS_SIZE (n - 1)
1104            ==> (x INSERT s) HAS_SIZE n`,
1105   REWRITE_TAC[HAS_SIZE] THEN REPEAT STRIP_TAC THEN
1106   ASM_SIMP_TAC[CARD_CLAUSES; FINITE_INSERT] THEN ASM_ARITH_TAC);;
1107
1108 let EDGES_PER_FACE_TAC th =
1109   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1110   EXISTS_TAC `CARD  {e:real^3->bool | e face_of f /\ aff_dim(e) = &1}` THEN
1111   CONJ_TAC THENL
1112    [AP_TERM_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
1113     REWRITE_TAC[IN_ELIM_THM] THEN
1114     ASM_MESON_TAC[FACE_OF_FACE; FACE_OF_TRANS; FACE_OF_IMP_SUBSET];
1115     ALL_TAC] THEN
1116   MP_TAC(ISPEC `f:real^3->bool` th) THEN ASM_REWRITE_TAC[] THEN
1117   DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
1118   W(fun (_,w) -> REWRITE_TAC[COMPUTE_EDGES_CONV(find_term is_setenum w)]) THEN
1119   REWRITE_TAC[SET_RULE `x = a \/ x = b <=> x IN {a,b}`] THEN
1120   REWRITE_TAC[GSYM IN_INSERT; SET_RULE `{x | x IN s} = s`] THEN
1121   REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC
1122    (MESON[HAS_SIZE] `s HAS_SIZE n ==> CARD s = n`) THEN
1123   REPEAT
1124   (MATCH_MP_TAC CARD_EQ_LEMMA THEN REPEAT CONJ_TAC THENL
1125     [CONV_TAC NUM_REDUCE_CONV THEN NO_TAC;
1126      REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; SEGMENT_EQ; DE_MORGAN_THM] THEN
1127      REPEAT CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
1128       `~(a = c /\ b = d) /\ ~(a = d /\ b = c) /\ ~(a = b /\ c = d)
1129        ==> ~({a,b} = {c,d})`) THEN
1130      PURE_ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
1131      CONV_TAC(ONCE_DEPTH_CONV VECTOR3_SUB_CONV) THEN
1132      CONV_TAC(ONCE_DEPTH_CONV VECTOR3_EQ_0_CONV) THEN
1133      REWRITE_TAC[] THEN NO_TAC;
1134      ALL_TAC]) THEN
1135   CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[CONJUNCT1 HAS_SIZE_CLAUSES];;
1136
1137 let TETRAHEDRON_EDGES_PER_FACE = prove
1138  (`!f. f face_of std_tetrahedron /\ aff_dim(f) = &2
1139        ==> CARD {e | e face_of std_tetrahedron /\ aff_dim(e) = &1 /\
1140                      e SUBSET f} = 3`,
1141   EDGES_PER_FACE_TAC TETRAHEDRON_FACETS);;
1142
1143 let CUBE_EDGES_PER_FACE = prove
1144  (`!f. f face_of std_cube /\ aff_dim(f) = &2
1145        ==> CARD {e | e face_of std_cube /\ aff_dim(e) = &1 /\
1146                      e SUBSET f} = 4`,
1147   EDGES_PER_FACE_TAC CUBE_FACETS);;
1148
1149 let OCTAHEDRON_EDGES_PER_FACE = prove
1150  (`!f. f face_of std_octahedron /\ aff_dim(f) = &2
1151        ==> CARD {e | e face_of std_octahedron /\ aff_dim(e) = &1 /\
1152                      e SUBSET f} = 3`,
1153   EDGES_PER_FACE_TAC OCTAHEDRON_FACETS);;
1154
1155 let DODECAHEDRON_EDGES_PER_FACE = prove
1156  (`!f. f face_of std_dodecahedron /\ aff_dim(f) = &2
1157        ==> CARD {e | e face_of std_dodecahedron /\ aff_dim(e) = &1 /\
1158                      e SUBSET f} = 5`,
1159   EDGES_PER_FACE_TAC DODECAHEDRON_FACETS);;
1160
1161 let ICOSAHEDRON_EDGES_PER_FACE = prove
1162  (`!f. f face_of std_icosahedron /\ aff_dim(f) = &2
1163        ==> CARD {e | e face_of std_icosahedron /\ aff_dim(e) = &1 /\
1164                      e SUBSET f} = 3`,
1165   EDGES_PER_FACE_TAC ICOSAHEDRON_FACETS);;
1166
1167 (* ------------------------------------------------------------------------- *)
1168 (* Show that the Platonic solids are all full-dimensional.                   *)
1169 (* ------------------------------------------------------------------------- *)
1170
1171 let POLYTOPE_3D_LEMMA = prove
1172  (`(let a = (z - x) cross (y - x) in
1173     ~(a = vec 0) /\ ?w. w IN s /\ ~(a dot w = a dot x))
1174    ==> aff_dim(convex hull (x INSERT y INSERT z INSERT s:real^3->bool)) = &3`,
1175   REPEAT GEN_TAC THEN LET_TAC THEN STRIP_TAC THEN
1176   REWRITE_TAC[GSYM INT_LE_ANTISYM] THEN CONJ_TAC THENL
1177    [REWRITE_TAC[GSYM DIMINDEX_3; AFF_DIM_LE_UNIV]; ALL_TAC] THEN
1178   REWRITE_TAC[AFF_DIM_CONVEX_HULL] THEN MATCH_MP_TAC INT_LE_TRANS THEN
1179   EXISTS_TAC `aff_dim {w:real^3,x,y,z}` THEN CONJ_TAC THENL
1180    [ALL_TAC; MATCH_MP_TAC AFF_DIM_SUBSET THEN ASM SET_TAC[]] THEN
1181   ONCE_REWRITE_TAC[AFF_DIM_INSERT] THEN COND_CASES_TAC THENL
1182    [SUBGOAL_THEN `w IN {w:real^3 | a dot w = a dot x}` MP_TAC THENL
1183      [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
1184        `x IN s ==> s SUBSET t ==> x IN t`)) THEN
1185       MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[AFFINE_HYPERPLANE] THEN
1186       REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN
1187       UNDISCH_TAC `~(a:real^3 = vec 0)` THEN EXPAND_TAC "a" THEN VEC3_TAC;
1188       ASM_REWRITE_TAC[IN_ELIM_THM]];
1189     UNDISCH_TAC `~(a:real^3 = vec 0)` THEN EXPAND_TAC "a" THEN
1190     REWRITE_TAC[CROSS_EQ_0; GSYM COLLINEAR_3] THEN
1191     REWRITE_TAC[COLLINEAR_3_EQ_AFFINE_DEPENDENT; INSERT_AC; DE_MORGAN_THM] THEN
1192     STRIP_TAC THEN ASM_SIMP_TAC[AFF_DIM_AFFINE_INDEPENDENT] THEN
1193     SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
1194     ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN INT_ARITH_TAC]);;
1195
1196 let POLYTOPE_FULLDIM_TAC =
1197   MATCH_MP_TAC POLYTOPE_3D_LEMMA THEN
1198   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_SUB_CONV) THEN
1199   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_CROSS_CONV) THEN
1200   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN CONJ_TAC THENL
1201    [CONV_TAC(RAND_CONV VECTOR3_EQ_0_CONV) THEN REWRITE_TAC[];
1202     CONV_TAC(ONCE_DEPTH_CONV VECTOR3_DOT_CONV) THEN
1203     REWRITE_TAC[EXISTS_IN_INSERT; NOT_IN_EMPTY] THEN
1204     CONV_TAC(ONCE_DEPTH_CONV VECTOR3_DOT_CONV) THEN
1205     CONV_TAC(ONCE_DEPTH_CONV REAL_RAT5_EQ_CONV) THEN
1206     REWRITE_TAC[]];;
1207
1208 let STD_TETRAHEDRON_FULLDIM = prove
1209  (`aff_dim std_tetrahedron = &3`,
1210   REWRITE_TAC[std_tetrahedron] THEN POLYTOPE_FULLDIM_TAC);;
1211
1212 let STD_CUBE_FULLDIM = prove
1213  (`aff_dim std_cube = &3`,
1214   REWRITE_TAC[std_cube] THEN POLYTOPE_FULLDIM_TAC);;
1215
1216 let STD_OCTAHEDRON_FULLDIM = prove
1217  (`aff_dim std_octahedron = &3`,
1218   REWRITE_TAC[std_octahedron] THEN POLYTOPE_FULLDIM_TAC);;
1219
1220 let STD_DODECAHEDRON_FULLDIM = prove
1221  (`aff_dim std_dodecahedron = &3`,
1222   REWRITE_TAC[STD_DODECAHEDRON] THEN POLYTOPE_FULLDIM_TAC);;
1223
1224 let STD_ICOSAHEDRON_FULLDIM = prove
1225  (`aff_dim std_icosahedron = &3`,
1226   REWRITE_TAC[STD_ICOSAHEDRON] THEN POLYTOPE_FULLDIM_TAC);;
1227
1228 (* ------------------------------------------------------------------------- *)
1229 (* Complete list of edges for each Platonic solid.                           *)
1230 (* ------------------------------------------------------------------------- *)
1231
1232 let COMPUTE_EDGES_TAC defn fulldim facets =
1233   GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1234   EXISTS_TAC
1235    (vsubst[lhs(concl defn),`p:real^3->bool`]
1236       `?f:real^3->bool. (f face_of p /\ aff_dim f = &2) /\
1237                         (e face_of f /\ aff_dim e = &1)`) THEN
1238   CONJ_TAC THENL
1239    [EQ_TAC THENL [STRIP_TAC; MESON_TAC[FACE_OF_TRANS]] THEN
1240     MP_TAC(ISPECL [lhs(concl defn); `e:real^3->bool`]
1241         FACE_OF_POLYHEDRON_SUBSET_FACET) THEN
1242     ANTS_TAC THENL
1243      [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
1244        [REWRITE_TAC[defn] THEN
1245         MATCH_MP_TAC POLYHEDRON_CONVEX_HULL THEN
1246         REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1247         CONJ_TAC THEN
1248         DISCH_THEN(MP_TAC o AP_TERM `aff_dim:(real^3->bool)->int`) THEN
1249         ASM_REWRITE_TAC[fulldim; AFF_DIM_EMPTY] THEN
1250         CONV_TAC INT_REDUCE_CONV];
1251       MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[facet_of] THEN
1252       REWRITE_TAC[fulldim] THEN CONV_TAC INT_REDUCE_CONV THEN
1253       ASM_MESON_TAC[FACE_OF_FACE]];
1254     REWRITE_TAC[facets] THEN
1255     REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
1256     REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2] THEN
1257     CONV_TAC(LAND_CONV(DEPTH_BINOP_CONV `\/`
1258      (fun tm -> REWR_CONV (COMPUTE_EDGES_CONV(rand(rand(lhand tm)))) tm))) THEN
1259     REWRITE_TAC[INSERT_AC] THEN REWRITE_TAC[DISJ_ACI]];;
1260
1261 let TETRAHEDRON_EDGES = prove
1262  (`!e. e face_of std_tetrahedron /\ aff_dim e = &1 <=>
1263        e = convex hull {vector[-- &1; -- &1; &1], vector[-- &1; &1; -- &1]} \/
1264        e = convex hull {vector[-- &1; -- &1; &1], vector[&1; -- &1; -- &1]} \/
1265        e = convex hull {vector[-- &1; -- &1; &1], vector[&1; &1; &1]} \/
1266        e = convex hull {vector[-- &1; &1; -- &1], vector[&1; -- &1; -- &1]} \/
1267        e = convex hull {vector[-- &1; &1; -- &1], vector[&1; &1; &1]} \/
1268        e = convex hull {vector[&1; -- &1; -- &1], vector[&1; &1; &1]}`,
1269   COMPUTE_EDGES_TAC
1270     std_tetrahedron STD_TETRAHEDRON_FULLDIM TETRAHEDRON_FACETS);;
1271
1272 let CUBE_EDGES = prove
1273  (`!e. e face_of std_cube /\ aff_dim e = &1 <=>
1274        e = convex hull {vector[-- &1; -- &1; -- &1], vector[-- &1; -- &1; &1]} \/
1275        e = convex hull {vector[-- &1; -- &1; -- &1], vector[-- &1; &1; -- &1]} \/
1276        e = convex hull {vector[-- &1; -- &1; -- &1], vector[&1; -- &1; -- &1]} \/
1277        e = convex hull {vector[-- &1; -- &1; &1], vector[-- &1; &1; &1]} \/
1278        e = convex hull {vector[-- &1; -- &1; &1], vector[&1; -- &1; &1]} \/
1279        e = convex hull {vector[-- &1; &1; -- &1], vector[-- &1; &1; &1]} \/
1280        e = convex hull {vector[-- &1; &1; -- &1], vector[&1; &1; -- &1]} \/
1281        e = convex hull {vector[-- &1; &1; &1], vector[&1; &1; &1]} \/
1282        e = convex hull {vector[&1; -- &1; -- &1], vector[&1; -- &1; &1]} \/
1283        e = convex hull {vector[&1; -- &1; -- &1], vector[&1; &1; -- &1]} \/
1284        e = convex hull {vector[&1; -- &1; &1], vector[&1; &1; &1]} \/
1285        e = convex hull {vector[&1; &1; -- &1], vector[&1; &1; &1]}`,
1286   COMPUTE_EDGES_TAC
1287     std_cube STD_CUBE_FULLDIM CUBE_FACETS);;
1288
1289 let OCTAHEDRON_EDGES = prove
1290  (`!e. e face_of std_octahedron /\ aff_dim e = &1 <=>
1291        e = convex hull {vector[-- &1; &0; &0], vector[&0; -- &1; &0]} \/
1292        e = convex hull {vector[-- &1; &0; &0], vector[&0; &1; &0]} \/
1293        e = convex hull {vector[-- &1; &0; &0], vector[&0; &0; -- &1]} \/
1294        e = convex hull {vector[-- &1; &0; &0], vector[&0; &0; &1]} \/
1295        e = convex hull {vector[&1; &0; &0], vector[&0; -- &1; &0]} \/
1296        e = convex hull {vector[&1; &0; &0], vector[&0; &1; &0]} \/
1297        e = convex hull {vector[&1; &0; &0], vector[&0; &0; -- &1]} \/
1298        e = convex hull {vector[&1; &0; &0], vector[&0; &0; &1]} \/
1299        e = convex hull {vector[&0; -- &1; &0], vector[&0; &0; -- &1]} \/
1300        e = convex hull {vector[&0; -- &1; &0], vector[&0; &0; &1]} \/
1301        e = convex hull {vector[&0; &1; &0], vector[&0; &0; -- &1]} \/
1302        e = convex hull {vector[&0; &1; &0], vector[&0; &0; &1]}`,
1303    COMPUTE_EDGES_TAC
1304      std_octahedron STD_OCTAHEDRON_FULLDIM OCTAHEDRON_FACETS);;
1305
1306 let DODECAHEDRON_EDGES = prove
1307  (`!e. e face_of std_dodecahedron /\ aff_dim e = &1 <=>
1308        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)], vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1309        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)], vector[-- &1; -- &1; &1]} \/
1310        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)], vector[-- &1; &1; &1]} \/
1311        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)], vector[-- &1; -- &1; -- &1]} \/
1312        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)], vector[-- &1; &1; -- &1]} \/
1313        e = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1314        e = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&1; -- &1; -- &1]} \/
1315        e = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&1; -- &1; &1]} \/
1316        e = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1317        e = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&1; &1; -- &1]} \/
1318        e = convex hull {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&1; &1; &1]} \/
1319        e = convex hull {vector[&1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[-- &1; -- &1; -- &1]} \/
1320        e = convex hull {vector[&1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[-- &1; -- &1; &1]} \/
1321        e = convex hull {vector[&1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[-- &1; &1; -- &1]} \/
1322        e = convex hull {vector[&1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[-- &1; &1; &1]} \/
1323        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)], vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1324        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)], vector[&1; -- &1; &1]} \/
1325        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)], vector[&1; &1; &1]} \/
1326        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)], vector[&1; -- &1; -- &1]} \/
1327        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)], vector[&1; &1; -- &1]} \/
1328        e = convex hull {vector[-- &1; -- &1; -- &1], vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1329        e = convex hull {vector[-- &1; -- &1; &1], vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1330        e = convex hull {vector[-- &1; &1; -- &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1331        e = convex hull {vector[-- &1; &1; &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1332        e = convex hull {vector[&1; -- &1; -- &1], vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1333        e = convex hull {vector[&1; -- &1; &1], vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1334        e = convex hull {vector[&1; &1; -- &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1335        e = convex hull {vector[&1; &1; &1], vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1336        e = convex hull {vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)], vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1337        e = convex hull {vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)], vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)]}`,
1338   COMPUTE_EDGES_TAC
1339     STD_DODECAHEDRON STD_DODECAHEDRON_FULLDIM DODECAHEDRON_FACETS);;
1340
1341 let ICOSAHEDRON_EDGES = prove
1342  (`!e. e face_of std_icosahedron /\ aff_dim e = &1 <=>
1343        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1], vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1]} \/
1344        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1], vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1345        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1], vector[-- &1; &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1346        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1347        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1348        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1], vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1349        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1], vector[-- &1; &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1350        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1351        e = convex hull {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1352        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1], vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1]} \/
1353        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1354        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1], vector[&1; &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1355        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1356        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1357        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1358        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1], vector[&1; &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1359        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1360        e = convex hull {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1361        e = convex hull {vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1362        e = convex hull {vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1363        e = convex hull {vector[-- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1364        e = convex hull {vector[-- &1; &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&1; &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1365        e = convex hull {vector[-- &1; &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1366        e = convex hull {vector[-- &1; &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1367        e = convex hull {vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1368        e = convex hull {vector[&1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0], vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1369        e = convex hull {vector[&1; &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1370        e = convex hull {vector[&1; &1 / &2 + &1 / &2 * sqrt (&5); &0], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1371        e = convex hull {vector[&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)], vector[&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1372        e = convex hull {vector[&0; -- &1; &1 / &2 + &1 / &2 * sqrt (&5)], vector[&0; &1; &1 / &2 + &1 / &2 * sqrt (&5)]}`,
1373   COMPUTE_EDGES_TAC
1374     STD_ICOSAHEDRON STD_ICOSAHEDRON_FULLDIM ICOSAHEDRON_FACETS);;
1375
1376 (* ------------------------------------------------------------------------- *)
1377 (* Enumerate all the vertices.                                               *)
1378 (* ------------------------------------------------------------------------- *)
1379
1380 let COMPUTE_VERTICES_TAC defn fulldim edges =
1381   GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1382   EXISTS_TAC
1383    (vsubst[lhs(concl defn),`p:real^3->bool`]
1384       `?e:real^3->bool. (e face_of p /\ aff_dim e = &1) /\
1385                         (v face_of e /\ aff_dim v = &0)`) THEN
1386   CONJ_TAC THENL
1387    [EQ_TAC THENL [STRIP_TAC; MESON_TAC[FACE_OF_TRANS]] THEN
1388     MP_TAC(ISPECL [lhs(concl defn); `v:real^3->bool`]
1389         FACE_OF_POLYHEDRON_SUBSET_FACET) THEN
1390     ANTS_TAC THENL
1391      [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
1392        [REWRITE_TAC[defn] THEN
1393         MATCH_MP_TAC POLYHEDRON_CONVEX_HULL THEN
1394         REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1395         CONJ_TAC THEN
1396         DISCH_THEN(MP_TAC o AP_TERM `aff_dim:(real^3->bool)->int`) THEN
1397         ASM_REWRITE_TAC[fulldim; AFF_DIM_EMPTY] THEN
1398         CONV_TAC INT_REDUCE_CONV];
1399       REWRITE_TAC[facet_of] THEN
1400       DISCH_THEN(X_CHOOSE_THEN `f:real^3->bool` STRIP_ASSUME_TAC)] THEN
1401     MP_TAC(ISPECL [`f:real^3->bool`; `v:real^3->bool`]
1402         FACE_OF_POLYHEDRON_SUBSET_FACET) THEN
1403     ANTS_TAC THENL
1404      [REPEAT CONJ_TAC THENL
1405        [MATCH_MP_TAC FACE_OF_POLYHEDRON_POLYHEDRON THEN
1406         FIRST_ASSUM(fun th ->
1407           EXISTS_TAC (rand(concl th)) THEN
1408           CONJ_TAC THENL [ALL_TAC; ACCEPT_TAC th]) THEN
1409         REWRITE_TAC[defn] THEN
1410         MATCH_MP_TAC POLYHEDRON_CONVEX_HULL THEN
1411         REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1412         ASM_MESON_TAC[FACE_OF_FACE];
1413         DISCH_THEN(MP_TAC o AP_TERM `aff_dim:(real^3->bool)->int`) THEN
1414         ASM_REWRITE_TAC[fulldim; AFF_DIM_EMPTY] THEN
1415         CONV_TAC INT_REDUCE_CONV;
1416         DISCH_THEN(MP_TAC o AP_TERM `aff_dim:(real^3->bool)->int`) THEN
1417         ASM_REWRITE_TAC[fulldim; AFF_DIM_EMPTY] THEN
1418         CONV_TAC INT_REDUCE_CONV];
1419       MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[facet_of] THEN
1420       ASM_REWRITE_TAC[fulldim] THEN CONV_TAC INT_REDUCE_CONV THEN
1421       ASM_MESON_TAC[FACE_OF_FACE; FACE_OF_TRANS]];
1422     REWRITE_TAC[edges] THEN
1423     REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
1424     REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2] THEN
1425     REWRITE_TAC[AFF_DIM_EQ_0; RIGHT_AND_EXISTS_THM] THEN
1426     ONCE_REWRITE_TAC[MESON[]
1427      `v face_of s /\ v = {a} <=> {a} face_of s /\ v = {a}`] THEN
1428     REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; FACE_OF_SING] THEN
1429     REWRITE_TAC[EXTREME_POINT_OF_SEGMENT] THEN
1430     REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
1431     REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2] THEN
1432     REWRITE_TAC[DISJ_ACI]];;
1433
1434 let TETRAHEDRON_VERTICES = prove
1435  (`!v. v face_of std_tetrahedron /\ aff_dim v = &0 <=>
1436        v = {vector [-- &1; -- &1; &1]} \/
1437        v = {vector [-- &1; &1; -- &1]} \/
1438        v = {vector [&1; -- &1; -- &1]} \/
1439        v = {vector [&1; &1; &1]}`,
1440   COMPUTE_VERTICES_TAC
1441     std_tetrahedron STD_TETRAHEDRON_FULLDIM TETRAHEDRON_EDGES);;
1442
1443 let CUBE_VERTICES = prove
1444  (`!v. v face_of std_cube /\ aff_dim v = &0 <=>
1445        v = {vector [-- &1; -- &1; -- &1]} \/
1446        v = {vector [-- &1; -- &1; &1]} \/
1447        v = {vector [-- &1; &1; -- &1]} \/
1448        v = {vector [-- &1; &1; &1]} \/
1449        v = {vector [&1; -- &1; -- &1]} \/
1450        v = {vector [&1; -- &1; &1]} \/
1451        v = {vector [&1; &1; -- &1]} \/
1452        v = {vector [&1; &1; &1]}`,
1453   COMPUTE_VERTICES_TAC
1454     std_cube STD_CUBE_FULLDIM CUBE_EDGES);;
1455
1456 let OCTAHEDRON_VERTICES = prove
1457  (`!v. v face_of std_octahedron /\ aff_dim v = &0 <=>
1458        v = {vector [-- &1; &0; &0]} \/
1459        v = {vector [&1; &0; &0]} \/
1460        v = {vector [&0; -- &1; &0]} \/
1461        v = {vector [&0; &1; &0]} \/
1462        v = {vector [&0; &0; -- &1]} \/
1463        v = {vector [&0; &0; &1]}`,
1464    COMPUTE_VERTICES_TAC
1465      std_octahedron STD_OCTAHEDRON_FULLDIM OCTAHEDRON_EDGES);;
1466
1467 let DODECAHEDRON_VERTICES = prove
1468  (`!v. v face_of std_dodecahedron /\ aff_dim v = &0 <=>
1469        v = {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1470        v = {vector[-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1471        v = {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1472        v = {vector[-- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1473        v = {vector[&1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1474        v = {vector[&1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1475        v = {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1476        v = {vector[&1 / &2 + &1 / &2 * sqrt (&5); &0; &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1477        v = {vector[-- &1; -- &1; -- &1]} \/
1478        v = {vector[-- &1; -- &1; &1]} \/
1479        v = {vector[-- &1; &1; -- &1]} \/
1480        v = {vector[-- &1; &1; &1]} \/
1481        v = {vector[&1; -- &1; -- &1]} \/
1482        v = {vector[&1; -- &1; &1]} \/
1483        v = {vector[&1; &1; -- &1]} \/
1484        v = {vector[&1; &1; &1]} \/
1485        v = {vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1486        v = {vector[&0; -- &1 / &2 + &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1487        v = {vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1488        v = {vector[&0; &1 / &2 + -- &1 / &2 * sqrt (&5); &1 / &2 + &1 / &2 * sqrt (&5)]}`,
1489   COMPUTE_VERTICES_TAC
1490     STD_DODECAHEDRON STD_DODECAHEDRON_FULLDIM DODECAHEDRON_EDGES);;
1491
1492 let ICOSAHEDRON_VERTICES = prove
1493  (`!v. v face_of std_icosahedron /\ aff_dim v = &0 <=>
1494        v = {vector [-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; -- &1]} \/
1495        v = {vector [-- &1 / &2 + -- &1 / &2 * sqrt (&5); &0; &1]} \/
1496        v = {vector [&1 / &2 + &1 / &2 * sqrt (&5); &0; -- &1]} \/
1497        v = {vector [&1 / &2 + &1 / &2 * sqrt (&5); &0; &1]} \/
1498        v = {vector [-- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1499        v = {vector [-- &1; &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1500        v = {vector [&1; -- &1 / &2 + -- &1 / &2 * sqrt (&5); &0]} \/
1501        v = {vector [&1; &1 / &2 + &1 / &2 * sqrt (&5); &0]} \/
1502        v = {vector [&0; -- &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1503        v = {vector [&0; -- &1; &1 / &2 + &1 / &2 * sqrt (&5)]} \/
1504        v = {vector [&0; &1; -- &1 / &2 + -- &1 / &2 * sqrt (&5)]} \/
1505        v = {vector [&0; &1; &1 / &2 + &1 / &2 * sqrt (&5)]}`,
1506   COMPUTE_VERTICES_TAC
1507     STD_ICOSAHEDRON STD_ICOSAHEDRON_FULLDIM ICOSAHEDRON_EDGES);;
1508
1509 (* ------------------------------------------------------------------------- *)
1510 (* Number of edges meeting at each vertex.                                   *)
1511 (* ------------------------------------------------------------------------- *)
1512
1513 let EDGES_PER_VERTEX_TAC defn edges verts =
1514   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1515   EXISTS_TAC
1516    (vsubst[lhs(concl defn),`p:real^3->bool`]
1517      `CARD {e | (e face_of p /\ aff_dim(e) = &1) /\
1518                 (v:real^3->bool) face_of e}`) THEN
1519   CONJ_TAC THENL
1520    [AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
1521     ASM_MESON_TAC[FACE_OF_FACE];
1522     ALL_TAC] THEN
1523   MP_TAC(ISPEC `v:real^3->bool` verts) THEN
1524   ASM_REWRITE_TAC[] THEN
1525   DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
1526   REWRITE_TAC[edges] THEN
1527   REWRITE_TAC[SET_RULE
1528    `{e | (P e \/ Q e) /\ R e} =
1529     {e | P e /\ R e} UNION {e | Q e /\ R e}`] THEN
1530   REWRITE_TAC[MESON[FACE_OF_SING]
1531    `e = a /\ {x} face_of e <=> e = a /\ x extreme_point_of a`] THEN
1532   REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; EXTREME_POINT_OF_SEGMENT] THEN
1533   ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
1534   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_SUB_CONV) THEN
1535   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_EQ_0_CONV) THEN
1536   REWRITE_TAC[EMPTY_GSPEC; UNION_EMPTY] THEN
1537   REWRITE_TAC[SET_RULE `{x | x = a} = {a}`] THEN
1538   REWRITE_TAC[SET_RULE `{x} UNION s = x INSERT s`] THEN MATCH_MP_TAC
1539    (MESON[HAS_SIZE] `s HAS_SIZE n ==> CARD s = n`) THEN
1540   REPEAT
1541   (MATCH_MP_TAC CARD_EQ_LEMMA THEN REPEAT CONJ_TAC THENL
1542     [CONV_TAC NUM_REDUCE_CONV THEN NO_TAC;
1543      REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM; SEGMENT_EQ] THEN
1544      REPEAT CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
1545       `~(a = c /\ b = d) /\ ~(a = d /\ b = c) /\ ~(a = b /\ c = d)
1546        ==> ~({a,b} = {c,d})`) THEN
1547      PURE_ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
1548      CONV_TAC(ONCE_DEPTH_CONV VECTOR3_SUB_CONV) THEN
1549      CONV_TAC(ONCE_DEPTH_CONV VECTOR3_EQ_0_CONV) THEN
1550      REWRITE_TAC[] THEN NO_TAC;
1551      ALL_TAC]) THEN
1552   CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[CONJUNCT1 HAS_SIZE_CLAUSES];;
1553
1554 let TETRAHEDRON_EDGES_PER_VERTEX = prove
1555  (`!v. v face_of std_tetrahedron /\ aff_dim(v) = &0
1556        ==> CARD {e | e face_of std_tetrahedron /\ aff_dim(e) = &1 /\
1557                      v SUBSET e} = 3`,
1558   EDGES_PER_VERTEX_TAC
1559     std_tetrahedron TETRAHEDRON_EDGES TETRAHEDRON_VERTICES);;
1560
1561 let CUBE_EDGES_PER_VERTEX = prove
1562  (`!v. v face_of std_cube /\ aff_dim(v) = &0
1563        ==> CARD {e | e face_of std_cube /\ aff_dim(e) = &1 /\
1564                      v SUBSET e} = 3`,
1565   EDGES_PER_VERTEX_TAC
1566     std_cube CUBE_EDGES CUBE_VERTICES);;
1567
1568 let OCTAHEDRON_EDGES_PER_VERTEX = prove
1569  (`!v. v face_of std_octahedron /\ aff_dim(v) = &0
1570        ==> CARD {e | e face_of std_octahedron /\ aff_dim(e) = &1 /\
1571                      v SUBSET e} = 4`,
1572   EDGES_PER_VERTEX_TAC
1573     std_octahedron OCTAHEDRON_EDGES OCTAHEDRON_VERTICES);;
1574
1575 let DODECAHEDRON_EDGES_PER_VERTEX = prove
1576  (`!v. v face_of std_dodecahedron /\ aff_dim(v) = &0
1577        ==> CARD {e | e face_of std_dodecahedron /\ aff_dim(e) = &1 /\
1578                      v SUBSET e} = 3`,
1579   EDGES_PER_VERTEX_TAC
1580     STD_DODECAHEDRON DODECAHEDRON_EDGES DODECAHEDRON_VERTICES);;
1581
1582 let ICOSAHEDRON_EDGES_PER_VERTEX = prove
1583  (`!v. v face_of std_icosahedron /\ aff_dim(v) = &0
1584        ==> CARD {e | e face_of std_icosahedron /\ aff_dim(e) = &1 /\
1585                      v SUBSET e} = 5`,
1586   EDGES_PER_VERTEX_TAC
1587     STD_ICOSAHEDRON ICOSAHEDRON_EDGES ICOSAHEDRON_VERTICES);;
1588
1589 (* ------------------------------------------------------------------------- *)
1590 (* Number of Platonic solids.                                                *)
1591 (* ------------------------------------------------------------------------- *)
1592
1593 let MULTIPLE_COUNTING_LEMMA = prove
1594  (`!R:A->B->bool s t.
1595         FINITE s /\ FINITE t /\
1596         (!x. x IN s ==> CARD {y | y IN t /\ R x y} = m) /\
1597         (!y. y IN t ==> CARD {x | x IN s /\ R x y} = n)
1598         ==> m * CARD s = n * CARD t`,
1599   REPEAT STRIP_TAC THEN
1600   MP_TAC(ISPECL [`R:A->B->bool`; `\x:A y:B. 1`; `s:A->bool`; `t:B->bool`]
1601         NSUM_NSUM_RESTRICT) THEN
1602   ASM_SIMP_TAC[NSUM_CONST; FINITE_RESTRICT] THEN ARITH_TAC);;
1603
1604 let SIZE_ZERO_DIMENSIONAL_FACES = prove
1605  (`!s:real^N->bool.
1606         polyhedron s
1607         ==> CARD {f | f face_of s /\ aff_dim f = &0} =
1608             CARD {v | v extreme_point_of s} /\
1609             (FINITE {f | f face_of s /\ aff_dim f = &0} <=>
1610              FINITE {v | v extreme_point_of s}) /\
1611             (!n. {f | f face_of s /\ aff_dim f = &0} HAS_SIZE n <=>
1612                  {v | v extreme_point_of s} HAS_SIZE n)`,
1613   REWRITE_TAC[RIGHT_AND_FORALL_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
1614   SUBGOAL_THEN `{f | f face_of s /\ aff_dim f = &0} =
1615                 IMAGE (\v:real^N. {v}) {v | v extreme_point_of s}`
1616   SUBST1_TAC THENL
1617    [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN
1618     REWRITE_TAC[AFF_DIM_SING; FACE_OF_SING; IN_ELIM_THM] THEN
1619     REWRITE_TAC[AFF_DIM_EQ_0] THEN MESON_TAC[];
1620     REPEAT STRIP_TAC THENL
1621      [MATCH_MP_TAC CARD_IMAGE_INJ;
1622       MATCH_MP_TAC FINITE_IMAGE_INJ_EQ;
1623       MATCH_MP_TAC HAS_SIZE_IMAGE_INJ_EQ] THEN
1624     ASM_SIMP_TAC[FINITE_POLYHEDRON_EXTREME_POINTS] THEN SET_TAC[]]);;
1625
1626 let PLATONIC_SOLIDS_LIMITS = prove
1627  (`!p:real^3->bool m n.
1628     polytope p /\ aff_dim p = &3 /\
1629     (!f. f face_of p /\ aff_dim(f) = &2
1630          ==> CARD {e | e face_of p /\ aff_dim(e) = &1 /\ e SUBSET f} = m) /\
1631     (!v. v face_of p /\ aff_dim(v) = &0
1632          ==> CARD {e | e face_of p /\ aff_dim(e) = &1 /\ v SUBSET e} = n)
1633     ==> m = 3 /\ n = 3 \/       // Tetrahedron
1634         m = 4 /\ n = 3 \/       // Cube
1635         m = 3 /\ n = 4 \/       // Octahedron
1636         m = 5 /\ n = 3 \/       // Dodecahedron
1637         m = 3 /\ n = 5          // Icosahedron`,
1638   REPEAT STRIP_TAC THEN
1639   MP_TAC(ISPEC `p:real^3->bool` EULER_RELATION) THEN
1640   ASM_REWRITE_TAC[] THEN
1641   SUBGOAL_THEN
1642    `m * CARD {f:real^3->bool | f face_of p /\ aff_dim f = &2} =
1643     2 * CARD {e | e face_of p /\ aff_dim e = &1} /\
1644     n * CARD {v | v face_of p /\ aff_dim v = &0} =
1645     2 * CARD {e | e face_of p /\ aff_dim e = &1}`
1646   MP_TAC THENL
1647    [CONJ_TAC THEN MATCH_MP_TAC MULTIPLE_COUNTING_LEMMA THENL
1648      [EXISTS_TAC `\(f:real^3->bool) (e:real^3->bool). e SUBSET f`;
1649       EXISTS_TAC `\(v:real^3->bool) (e:real^3->bool). v SUBSET e`] THEN
1650     ONCE_REWRITE_TAC[SET_RULE `f face_of s <=> f IN {f | f face_of s}`] THEN
1651     ASM_SIMP_TAC[FINITE_POLYTOPE_FACES; FINITE_RESTRICT] THEN
1652     ASM_REWRITE_TAC[IN_ELIM_THM; GSYM CONJ_ASSOC] THEN
1653     X_GEN_TAC `e:real^3->bool` THEN STRIP_TAC THENL
1654      [MP_TAC(ISPECL [`p:real^3->bool`; `e:real^3->bool`]
1655           POLYHEDRON_RIDGE_TWO_FACETS) THEN
1656       ASM_SIMP_TAC[POLYTOPE_IMP_POLYHEDRON] THEN ANTS_TAC THENL
1657        [CONV_TAC INT_REDUCE_CONV THEN DISCH_THEN SUBST_ALL_TAC THEN
1658         RULE_ASSUM_TAC(REWRITE_RULE[AFF_DIM_EMPTY]) THEN ASM_INT_ARITH_TAC;
1659         CONV_TAC INT_REDUCE_CONV THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
1660         MAP_EVERY X_GEN_TAC [`f1:real^3->bool`; `f2:real^3->bool`] THEN
1661         STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1662         EXISTS_TAC `CARD {f1:real^3->bool,f2}` THEN CONJ_TAC THENL
1663          [AP_TERM_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
1664           REWRITE_TAC[IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
1665           ASM_MESON_TAC[];
1666           ASM_SIMP_TAC[CARD_CLAUSES; IN_INSERT; FINITE_RULES;
1667                        NOT_IN_EMPTY; ARITH]]];
1668       SUBGOAL_THEN `?a b:real^3. e = segment[a,b]` STRIP_ASSUME_TAC THENL
1669        [MATCH_MP_TAC COMPACT_CONVEX_COLLINEAR_SEGMENT THEN
1670         REPEAT CONJ_TAC THENL
1671          [DISCH_THEN SUBST_ALL_TAC THEN
1672           RULE_ASSUM_TAC(REWRITE_RULE[AFF_DIM_EMPTY]) THEN ASM_INT_ARITH_TAC;
1673           MATCH_MP_TAC FACE_OF_IMP_COMPACT THEN
1674           EXISTS_TAC `p:real^3->bool` THEN
1675           ASM_SIMP_TAC[POLYTOPE_IMP_CONVEX; POLYTOPE_IMP_COMPACT];
1676           ASM_MESON_TAC[FACE_OF_IMP_CONVEX];
1677           MP_TAC(ISPEC `e:real^3->bool` AFF_DIM) THEN
1678           DISCH_THEN(X_CHOOSE_THEN `b:real^3->bool` MP_TAC) THEN
1679           ASM_REWRITE_TAC[INT_ARITH `&1:int = b - &1 <=> b = &2`] THEN
1680           DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) MP_TAC) THEN
1681           ASM_CASES_TAC `FINITE(b:real^3->bool)` THENL
1682            [ALL_TAC; ASM_MESON_TAC[AFFINE_INDEPENDENT_IMP_FINITE]] THEN
1683           REWRITE_TAC[INT_OF_NUM_EQ] THEN STRIP_TAC THEN
1684           SUBGOAL_THEN `(b:real^3->bool) HAS_SIZE 2` MP_TAC THENL
1685            [ASM_REWRITE_TAC[HAS_SIZE]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
1686           REWRITE_TAC[COLLINEAR_AFFINE_HULL] THEN
1687           REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
1688           ASM_MESON_TAC[HULL_SUBSET]];
1689         ASM_CASES_TAC `a:real^3 = b` THENL
1690          [UNDISCH_TAC `aff_dim(e:real^3->bool) = &1` THEN
1691           ASM_REWRITE_TAC[SEGMENT_REFL; AFF_DIM_SING; INT_OF_NUM_EQ; ARITH_EQ];
1692           ALL_TAC] THEN
1693         MATCH_MP_TAC EQ_TRANS THEN
1694         EXISTS_TAC `CARD {v:real^3 | v extreme_point_of segment[a,b]}` THEN
1695         CONJ_TAC THENL
1696          [MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN
1697           EXISTS_TAC `\v:real^3. {v}` THEN
1698           REWRITE_TAC[IN_ELIM_THM; FACE_OF_SING; AFF_DIM_SING] THEN
1699           REPEAT CONJ_TAC THENL
1700            [ASM_REWRITE_TAC[EXTREME_POINT_OF_SEGMENT] THEN
1701             REWRITE_TAC[SET_RULE `{x | x = a \/ x = b} = {a,b}`] THEN
1702             REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1703             X_GEN_TAC `v:real^3` THEN REWRITE_TAC[GSYM FACE_OF_SING] THEN
1704             ASM_MESON_TAC[FACE_OF_TRANS; FACE_OF_IMP_SUBSET];
1705             X_GEN_TAC `s:real^3->bool` THEN REWRITE_TAC[AFF_DIM_EQ_0] THEN
1706             DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1707             DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1708             DISCH_THEN(X_CHOOSE_THEN `v:real^3` SUBST_ALL_TAC) THEN
1709             REWRITE_TAC[EXISTS_UNIQUE] THEN EXISTS_TAC `v:real^3` THEN
1710             ASM_REWRITE_TAC[GSYM FACE_OF_SING] THEN CONJ_TAC THENL
1711              [ASM_MESON_TAC[FACE_OF_FACE]; SET_TAC[]]];
1712           ASM_REWRITE_TAC[EXTREME_POINT_OF_SEGMENT] THEN
1713           REWRITE_TAC[SET_RULE `{x | x = a \/ x = b} = {a,b}`] THEN
1714           ASM_SIMP_TAC[FINITE_INSERT; CARD_CLAUSES; FINITE_EMPTY] THEN
1715           ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; ARITH]]]];
1716     ALL_TAC] THEN
1717   STRIP_TAC THEN
1718   DISCH_THEN(ASSUME_TAC o MATCH_MP (ARITH_RULE
1719    `(a + b) - c = 2 ==> a + b = c + 2`)) THEN
1720   SUBGOAL_THEN `4 <= CARD {v:real^3->bool | v face_of p /\ aff_dim v = &0}`
1721   ASSUME_TAC THENL
1722    [ASM_SIMP_TAC[SIZE_ZERO_DIMENSIONAL_FACES; POLYTOPE_IMP_POLYHEDRON] THEN
1723     MP_TAC(ISPEC `p:real^3->bool` POLYTOPE_VERTEX_LOWER_BOUND) THEN
1724     ASM_REWRITE_TAC[] THEN CONV_TAC INT_REDUCE_CONV THEN
1725     REWRITE_TAC[INT_OF_NUM_LE];
1726     ALL_TAC] THEN
1727   SUBGOAL_THEN `4 <= CARD {f:real^3->bool | f face_of p /\ aff_dim f = &2}`
1728   ASSUME_TAC THENL
1729    [MP_TAC(ISPEC `p:real^3->bool` POLYTOPE_FACET_LOWER_BOUND) THEN
1730     ASM_REWRITE_TAC[] THEN CONV_TAC INT_REDUCE_CONV THEN
1731     ASM_REWRITE_TAC[INT_OF_NUM_LE; facet_of] THEN
1732     MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
1733     GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN
1734     CONV_TAC INT_REDUCE_CONV THEN GEN_TAC THEN EQ_TAC THEN
1735     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1736     ASM_MESON_TAC[INT_ARITH `~(&2:int = -- &1)`; AFF_DIM_EMPTY];
1737     ALL_TAC] THEN
1738   FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
1739    `v + f = e + 2 ==> 4 <= v /\ 4 <= f ==> 6 <= e`)) THEN
1740   ASM_REWRITE_TAC[] THEN
1741   ASM_CASES_TAC
1742    `CARD {e:real^3->bool | e face_of p /\ aff_dim e = &1} = 0` THEN
1743   ASM_REWRITE_TAC[ARITH] THEN DISCH_TAC THEN
1744   SUBGOAL_THEN `3 <= m` ASSUME_TAC THENL
1745    [ASM_CASES_TAC `{f:real^3->bool | f face_of p /\ aff_dim f = &2} = {}` THENL
1746      [UNDISCH_TAC
1747        `4 <= CARD {f:real^3->bool | f face_of p /\ aff_dim f = &2}` THEN
1748       ASM_REWRITE_TAC[CARD_CLAUSES] THEN ARITH_TAC;
1749       FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY])] THEN
1750     REWRITE_TAC[IN_ELIM_THM] THEN
1751     DISCH_THEN(X_CHOOSE_THEN `f:real^3->bool` MP_TAC) THEN
1752     DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN
1753      FIRST_X_ASSUM(SUBST1_TAC o SYM o C MATCH_MP th)) THEN
1754     MP_TAC(ISPEC `f:real^3->bool` POLYTOPE_FACET_LOWER_BOUND) THEN
1755     ASM_REWRITE_TAC[facet_of] THEN CONV_TAC INT_REDUCE_CONV THEN
1756     ANTS_TAC THENL [ASM_MESON_TAC[FACE_OF_POLYTOPE_POLYTOPE]; ALL_TAC] THEN
1757     REWRITE_TAC[INT_OF_NUM_LE] THEN MATCH_MP_TAC EQ_IMP THEN
1758     AP_TERM_TAC THEN AP_TERM_TAC THEN
1759     GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN
1760     CONV_TAC INT_REDUCE_CONV THEN X_GEN_TAC `e:real^3->bool` THEN
1761     EQ_TAC THEN ASM_CASES_TAC `e:real^3->bool = {}` THEN
1762     ASM_SIMP_TAC[AFF_DIM_EMPTY] THEN CONV_TAC INT_REDUCE_CONV THENL
1763      [ASM_MESON_TAC[FACE_OF_TRANS; FACE_OF_IMP_SUBSET];
1764       ASM_MESON_TAC[FACE_OF_FACE]];
1765     ALL_TAC] THEN
1766   FIRST_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `3 <= m ==> ~(m = 0)`)) THEN
1767   ASM_CASES_TAC `n = 0` THENL
1768    [UNDISCH_THEN `n = 0` SUBST_ALL_TAC THEN
1769     FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
1770      `0 * x = 2 * e ==> e = 0`)) THEN ASM_REWRITE_TAC[];
1771     ALL_TAC] THEN
1772   FIRST_ASSUM(MP_TAC o MATCH_MP (NUM_RING
1773     `v + f = e + 2 ==> !m n. m * n * v + n * m * f = m * n * (e + 2)`)) THEN
1774   DISCH_THEN(MP_TAC o SPECL [`m:num`; `n:num`]) THEN ASM_REWRITE_TAC[] THEN
1775   REWRITE_TAC[ARITH_RULE `m * 2 * e + n * 2 * e = m * n * (e + 2) <=>
1776                           e * 2 * (m + n) = m * n * (e + 2)`] THEN
1777   ABBREV_TAC `E = CARD {e:real^3->bool | e face_of p /\ aff_dim e = &1}` THEN
1778   ASM_CASES_TAC `n = 1` THENL
1779    [ASM_REWRITE_TAC[MULT_CLAUSES; ARITH_RULE
1780      `E * 2 * (n + 1) = n * (E + 2) <=> E * (n + 2) = 2 * n`] THEN
1781     MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
1782     MATCH_MP_TAC(ARITH_RULE `n:num < m ==> ~(m = n)`) THEN
1783     MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `2 * (m + 2)` THEN
1784     CONJ_TAC THENL [ARITH_TAC; MATCH_MP_TAC LE_MULT2 THEN ASM_ARITH_TAC];
1785     ALL_TAC] THEN
1786   ASM_CASES_TAC `n = 2` THENL
1787    [ASM_REWRITE_TAC[ARITH_RULE `E * 2 * (n + 2) = n * 2 * (E + 2) <=>
1788                                 E = n`] THEN
1789     DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
1790     FIRST_X_ASSUM(MP_TAC o MATCH_MP (NUM_RING
1791      `E * c = 2 * E ==> E = 0 \/ c = 2`)) THEN
1792     ASM_ARITH_TAC;
1793     ALL_TAC] THEN
1794   SUBGOAL_THEN `3 <= n` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1795   ASM_CASES_TAC `m * n < 2 * (m + n)` THENL
1796    [DISCH_TAC;
1797     DISCH_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
1798     SUBGOAL_THEN `E * 2 * (m + n) <= E * m * n` MP_TAC THENL
1799      [REWRITE_TAC[LE_MULT_LCANCEL] THEN ASM_ARITH_TAC;
1800       ASM_REWRITE_TAC[ARITH_RULE `m * n * (E + 2) <= E * m * n <=>
1801                                   2 * m * n = 0`] THEN
1802       MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
1803       REWRITE_TAC[MULT_EQ_0] THEN ASM_ARITH_TAC]] THEN
1804   SUBGOAL_THEN `&m - &2:real < &4 /\ &n - &2 < &4` MP_TAC THENL
1805    [CONJ_TAC THENL
1806      [MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN EXISTS_TAC `&n - &2`;
1807       MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&m - &2`] THEN
1808     ASM_SIMP_TAC[REAL_SUB_LT; REAL_OF_NUM_LT;
1809                  ARITH_RULE `2 < n <=> 3 <= n`] THEN
1810     MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&4` THEN
1811     REWRITE_TAC[REAL_ARITH `(m - &2) * (n - &2) < &4 <=>
1812                             m * n < &2 * (m + n)`] THEN
1813     ASM_REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; REAL_OF_NUM_LT] THEN
1814     REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_SUB_RDISTRIB; REAL_LE_SUB_LADD] THEN
1815     REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; REAL_OF_NUM_LE] THEN
1816     ASM_ARITH_TAC;
1817     ALL_TAC] THEN
1818   REWRITE_TAC[REAL_LT_SUB_RADD; REAL_OF_NUM_ADD; REAL_OF_NUM_LT] THEN
1819   REWRITE_TAC[ARITH_RULE `m < 4 + 2 <=> m <= 5`] THEN
1820   ASM_SIMP_TAC[ARITH_RULE
1821    `3 <= m ==> (m <= 5 <=> m = 3 \/ m = 4 \/ m = 5)`] THEN
1822   STRIP_TAC THEN UNDISCH_TAC `E * 2 * (m + n) = m * n * (E + 2)` THEN
1823   ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN ASM_ARITH_TAC);;
1824
1825 (* ------------------------------------------------------------------------- *)
1826 (* If-and-only-if version.                                                   *)
1827 (* ------------------------------------------------------------------------- *)
1828
1829 let PLATONIC_SOLIDS = prove
1830  (`!m n.
1831    (?p:real^3->bool.
1832      polytope p /\ aff_dim p = &3 /\
1833      (!f. f face_of p /\ aff_dim(f) = &2
1834           ==> CARD {e | e face_of p /\ aff_dim(e) = &1 /\ e SUBSET f} = m) /\
1835      (!v. v face_of p /\ aff_dim(v) = &0
1836           ==> CARD {e | e face_of p /\ aff_dim(e) = &1 /\ v SUBSET e} = n)) <=>
1837      m = 3 /\ n = 3 \/       // Tetrahedron
1838      m = 4 /\ n = 3 \/       // Cube
1839      m = 3 /\ n = 4 \/       // Octahedron
1840      m = 5 /\ n = 3 \/       // Dodecahedron
1841      m = 3 /\ n = 5          // Icosahedron`,
1842   REPEAT GEN_TAC THEN EQ_TAC THEN
1843   REWRITE_TAC[LEFT_IMP_EXISTS_THM; PLATONIC_SOLIDS_LIMITS] THEN
1844   STRIP_TAC THENL
1845    [EXISTS_TAC `std_tetrahedron` THEN
1846     ASM_REWRITE_TAC[TETRAHEDRON_EDGES_PER_VERTEX; TETRAHEDRON_EDGES_PER_FACE;
1847                     STD_TETRAHEDRON_FULLDIM] THEN
1848     REWRITE_TAC[std_tetrahedron] THEN MATCH_MP_TAC POLYTOPE_CONVEX_HULL THEN
1849     REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1850     EXISTS_TAC `std_cube` THEN
1851     ASM_REWRITE_TAC[CUBE_EDGES_PER_VERTEX; CUBE_EDGES_PER_FACE;
1852                     STD_CUBE_FULLDIM] THEN
1853     REWRITE_TAC[std_cube] THEN MATCH_MP_TAC POLYTOPE_CONVEX_HULL THEN
1854     REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1855     EXISTS_TAC `std_octahedron` THEN
1856     ASM_REWRITE_TAC[OCTAHEDRON_EDGES_PER_VERTEX; OCTAHEDRON_EDGES_PER_FACE;
1857                     STD_OCTAHEDRON_FULLDIM] THEN
1858     REWRITE_TAC[std_octahedron] THEN MATCH_MP_TAC POLYTOPE_CONVEX_HULL THEN
1859     REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1860     EXISTS_TAC `std_dodecahedron` THEN
1861     ASM_REWRITE_TAC[DODECAHEDRON_EDGES_PER_VERTEX; DODECAHEDRON_EDGES_PER_FACE;
1862                     STD_DODECAHEDRON_FULLDIM] THEN
1863     REWRITE_TAC[STD_DODECAHEDRON] THEN MATCH_MP_TAC POLYTOPE_CONVEX_HULL THEN
1864     REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1865     EXISTS_TAC `std_icosahedron` THEN
1866     ASM_REWRITE_TAC[ICOSAHEDRON_EDGES_PER_VERTEX; ICOSAHEDRON_EDGES_PER_FACE;
1867                     STD_ICOSAHEDRON_FULLDIM] THEN
1868     REWRITE_TAC[STD_ICOSAHEDRON] THEN MATCH_MP_TAC POLYTOPE_CONVEX_HULL THEN
1869     REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY]]);;
1870
1871 (* ------------------------------------------------------------------------- *)
1872 (* Show that the regular polyhedra do have all edges and faces congruent.    *)
1873 (* ------------------------------------------------------------------------- *)
1874
1875 parse_as_infix("congruent",(12,"right"));;
1876
1877 let congruent = new_definition
1878  `(s:real^N->bool) congruent (t:real^N->bool) <=>
1879         ?c f. orthogonal_transformation f /\ t = IMAGE (\x. c + f x) s`;;
1880
1881 let CONGRUENT_SIMPLE = prove
1882  (`(?A:real^3^3. orthogonal_matrix A /\ IMAGE (\x:real^3. A ** x) s = t)
1883    ==> (convex hull s) congruent (convex hull t)`,
1884   REPEAT GEN_TAC THEN
1885   DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM))) THEN
1886   SIMP_TAC[CONVEX_HULL_LINEAR_IMAGE; MATRIX_VECTOR_MUL_LINEAR] THEN
1887   REWRITE_TAC[congruent] THEN EXISTS_TAC `vec 0:real^3` THEN
1888   EXISTS_TAC `\x:real^3. (A:real^3^3) ** x` THEN
1889   REWRITE_TAC[VECTOR_ADD_LID; ORTHOGONAL_TRANSFORMATION_MATRIX] THEN
1890   ASM_SIMP_TAC[MATRIX_OF_MATRIX_VECTOR_MUL; MATRIX_VECTOR_MUL_LINEAR]);;
1891
1892 let CONGRUENT_SEGMENTS = prove
1893  (`!a b c d:real^N.
1894         dist(a,b) = dist(c,d)
1895         ==> segment[a,b] congruent segment[c,d]`,
1896   REPEAT STRIP_TAC THEN
1897   MP_TAC(ISPECL [`b - a:real^N`; `d - c:real^N`]
1898     ORTHOGONAL_TRANSFORMATION_EXISTS) THEN
1899   ANTS_TAC THENL [POP_ASSUM MP_TAC THEN NORM_ARITH_TAC; ALL_TAC] THEN
1900   DISCH_THEN(X_CHOOSE_THEN `f:real^N->real^N` STRIP_ASSUME_TAC) THEN
1901   REWRITE_TAC[congruent] THEN
1902   EXISTS_TAC `c - (f:real^N->real^N) a` THEN
1903   EXISTS_TAC `f:real^N->real^N` THEN
1904   FIRST_ASSUM(ASSUME_TAC o MATCH_MP ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
1905   SUBGOAL_THEN
1906    `(\x. (c - f a) + (f:real^N->real^N) x) = (\x. (c - f a) + x) o f`
1907   SUBST1_TAC THENL [REWRITE_TAC[FUN_EQ_THM; o_THM]; ALL_TAC] THEN
1908   ASM_SIMP_TAC[GSYM CONVEX_HULL_LINEAR_IMAGE; SEGMENT_CONVEX_HULL; IMAGE_o;
1909                GSYM CONVEX_HULL_TRANSLATION] THEN
1910   REWRITE_TAC[IMAGE_CLAUSES] THEN
1911   AP_TERM_TAC THEN BINOP_TAC THENL
1912    [VECTOR_ARITH_TAC; AP_THM_TAC THEN AP_TERM_TAC] THEN
1913   REWRITE_TAC[VECTOR_ARITH `d:real^N = c - a + b <=> b - a = d - c`] THEN
1914   ASM_MESON_TAC[LINEAR_SUB]);;
1915
1916 let compute_dist =
1917   let mk_sub = mk_binop `(-):real^3->real^3->real^3`
1918   and dot_tm = `(dot):real^3->real^3->real` in
1919   fun v1 v2 -> let vth = VECTOR3_SUB_CONV(mk_sub v1 v2) in
1920                let dth = CONV_RULE(RAND_CONV VECTOR3_DOT_CONV)
1921                           (MK_COMB(AP_TERM dot_tm vth,vth)) in
1922                rand(concl dth);;
1923
1924 let le_rat5 =
1925   let mk_le = mk_binop `(<=):real->real->bool` and t_tm = `T` in
1926   fun r1 r2 -> rand(concl(REAL_RAT5_LE_CONV(mk_le r1 r2))) = t_tm;;
1927
1928 let three_adjacent_points s =
1929   match s with
1930   | x::t -> let (y,_)::(z,_)::_ =
1931               sort (fun (_,r1) (_,r2) -> le_rat5 r1 r2)
1932                    (map (fun y -> y,compute_dist x y) t) in
1933             x,y,z
1934   | _ -> failwith "three_adjacent_points: no points";;
1935
1936 let mk_33matrix =
1937   let a11_tm = `a11:real`
1938   and a12_tm = `a12:real`
1939   and a13_tm = `a13:real`
1940   and a21_tm = `a21:real`
1941   and a22_tm = `a22:real`
1942   and a23_tm = `a23:real`
1943   and a31_tm = `a31:real`
1944   and a32_tm = `a32:real`
1945   and a33_tm = `a33:real`
1946   and pat_tm =
1947    `vector[vector[a11; a12; a13];
1948            vector[a21; a22; a23];
1949            vector[a31; a32; a33]]:real^3^3` in
1950   fun [a11;a12;a13;a21;a22;a23;a31;a32;a33] ->
1951     vsubst[a11,a11_tm;
1952            a12,a12_tm;
1953            a13,a13_tm;
1954            a21,a21_tm;
1955            a22,a22_tm;
1956            a23,a23_tm;
1957            a31,a31_tm;
1958            a32,a32_tm;
1959            a33,a33_tm] pat_tm;;
1960
1961 let MATRIX_VECTOR_MUL_3 = prove
1962  (`(vector[vector[a11;a12;a13];
1963            vector[a21; a22; a23];
1964            vector[a31; a32; a33]]:real^3^3) **
1965    (vector[x1;x2;x3]:real^3) =
1966    vector[a11 * x1 + a12 * x2 + a13 * x3;
1967           a21 * x1 + a22 * x2 + a23 * x3;
1968           a31 * x1 + a32 * x2 + a33 * x3]`,
1969   SIMP_TAC[CART_EQ; matrix_vector_mul; LAMBDA_BETA] THEN
1970   REWRITE_TAC[DIMINDEX_3; FORALL_3; SUM_3; VECTOR_3]);;
1971
1972 let MATRIX_LEMMA = prove
1973  (`!A:real^3^3.
1974    A ** x1 = x2 /\
1975    A ** y1 = y2 /\
1976    A ** z1 = z2 <=>
1977    (vector [x1; y1; z1]:real^3^3) ** (row 1 A:real^3) =
1978    vector [x2$1; y2$1; z2$1] /\
1979    (vector [x1; y1; z1]:real^3^3) ** (row 2 A:real^3) =
1980    vector [x2$2; y2$2; z2$2] /\
1981    (vector [x1; y1; z1]:real^3^3) ** (row 3 A:real^3) =
1982    vector [x2$3; y2$3; z2$3]`,
1983   SIMP_TAC[CART_EQ; transp; matrix_vector_mul; row; VECTOR_3; LAMBDA_BETA] THEN
1984   REWRITE_TAC[FORALL_3; DIMINDEX_3; VECTOR_3; SUM_3] THEN REAL_ARITH_TAC);;
1985
1986 let MATRIX_BY_CRAMER_LEMMA = prove
1987  (`!A:real^3^3.
1988         ~(det(vector[x1; y1; z1]:real^3^3) = &0)
1989         ==> (A ** x1 = x2 /\
1990              A ** y1 = y2 /\
1991              A ** z1 = z2 <=>
1992              A = lambda m k. det((lambda i j.
1993                                   if j = k
1994                                   then (vector[x2$m; y2$m; z2$m]:real^3)$i
1995                                   else (vector[x1; y1; z1]:real^3^3)$i$j)
1996                                  :real^3^3) /
1997                              det(vector[x1;y1;z1]:real^3^3))`,
1998   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [MATRIX_LEMMA] THEN
1999   ASM_SIMP_TAC[CRAMER] THEN REWRITE_TAC[CART_EQ; row] THEN
2000   SIMP_TAC[LAMBDA_BETA] THEN REWRITE_TAC[DIMINDEX_3; FORALL_3]);;
2001
2002 let MATRIX_BY_CRAMER = prove
2003  (`!A:real^3^3 x1 y1 z1 x2 y2 z2.
2004         let d = det(vector[x1; y1; z1]:real^3^3) in
2005         ~(d = &0)
2006         ==> (A ** x1 = x2 /\
2007              A ** y1 = y2 /\
2008              A ** z1 = z2 <=>
2009                A$1$1 =
2010                (x2$1 * y1$2 * z1$3 +
2011                 x1$2 * y1$3 * z2$1 +
2012                 x1$3 * y2$1 * z1$2 -
2013                 x2$1 * y1$3 * z1$2 -
2014                 x1$2 * y2$1 * z1$3 -
2015                 x1$3 * y1$2 * z2$1) / d /\
2016                A$1$2 =
2017                (x1$1 * y2$1 * z1$3 +
2018                 x2$1 * y1$3 * z1$1 +
2019                 x1$3 * y1$1 * z2$1 -
2020                 x1$1 * y1$3 * z2$1 -
2021                 x2$1 * y1$1 * z1$3 -
2022                 x1$3 * y2$1 * z1$1) / d /\
2023                A$1$3 =
2024                (x1$1 * y1$2 * z2$1 +
2025                 x1$2 * y2$1 * z1$1 +
2026                 x2$1 * y1$1 * z1$2 -
2027                 x1$1 * y2$1 * z1$2 -
2028                 x1$2 * y1$1 * z2$1 -
2029                 x2$1 * y1$2 * z1$1) / d /\
2030                A$2$1 =
2031                (x2$2 * y1$2 * z1$3 +
2032                 x1$2 * y1$3 * z2$2 +
2033                 x1$3 * y2$2 * z1$2 -
2034                 x2$2 * y1$3 * z1$2 -
2035                 x1$2 * y2$2 * z1$3 -
2036                 x1$3 * y1$2 * z2$2) / d /\
2037                A$2$2 =
2038                (x1$1 * y2$2 * z1$3 +
2039                 x2$2 * y1$3 * z1$1 +
2040                 x1$3 * y1$1 * z2$2 -
2041                 x1$1 * y1$3 * z2$2 -
2042                 x2$2 * y1$1 * z1$3 -
2043                 x1$3 * y2$2 * z1$1) / d /\
2044                A$2$3 =
2045                (x1$1 * y1$2 * z2$2 +
2046                 x1$2 * y2$2 * z1$1 +
2047                 x2$2 * y1$1 * z1$2 -
2048                 x1$1 * y2$2 * z1$2 -
2049                 x1$2 * y1$1 * z2$2 -
2050                 x2$2 * y1$2 * z1$1) / d /\
2051                A$3$1 =
2052                (x2$3 * y1$2 * z1$3 +
2053                 x1$2 * y1$3 * z2$3 +
2054                 x1$3 * y2$3 * z1$2 -
2055                 x2$3 * y1$3 * z1$2 -
2056                 x1$2 * y2$3 * z1$3 -
2057                 x1$3 * y1$2 * z2$3) / d /\
2058                A$3$2 =
2059                (x1$1 * y2$3 * z1$3 +
2060                 x2$3 * y1$3 * z1$1 +
2061                 x1$3 * y1$1 * z2$3 -
2062                 x1$1 * y1$3 * z2$3 -
2063                 x2$3 * y1$1 * z1$3 -
2064                 x1$3 * y2$3 * z1$1) / d /\
2065                A$3$3 =
2066                (x1$1 * y1$2 * z2$3 +
2067                 x1$2 * y2$3 * z1$1 +
2068                 x2$3 * y1$1 * z1$2 -
2069                 x1$1 * y2$3 * z1$2 -
2070                 x1$2 * y1$1 * z2$3 -
2071                 x2$3 * y1$2 * z1$1) / d)`,
2072   REPEAT GEN_TAC THEN CONV_TAC let_CONV THEN DISCH_TAC THEN
2073   ASM_SIMP_TAC[MATRIX_BY_CRAMER_LEMMA] THEN
2074   REWRITE_TAC[DET_3; CART_EQ] THEN
2075   SIMP_TAC[LAMBDA_BETA; DIMINDEX_3; ARITH; VECTOR_3] THEN
2076   REWRITE_TAC[FORALL_3; ARITH; VECTOR_3] THEN REWRITE_TAC[CONJ_ACI]);;
2077
2078 let CONGRUENT_EDGES_TAC edges =
2079   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[IMP_IMP] THEN
2080   REWRITE_TAC[edges] THEN
2081   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL] THEN
2082   MATCH_MP_TAC CONGRUENT_SEGMENTS THEN REWRITE_TAC[DIST_EQ] THEN
2083   REWRITE_TAC[dist; NORM_POW_2] THEN
2084   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_SUB_CONV) THEN
2085   CONV_TAC(ONCE_DEPTH_CONV VECTOR3_DOT_CONV) THEN
2086   CONV_TAC(ONCE_DEPTH_CONV REAL_RAT5_EQ_CONV) THEN
2087   REWRITE_TAC[];;
2088
2089 let CONGRUENT_FACES_TAC facets =
2090   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[IMP_IMP] THEN
2091   REWRITE_TAC[facets] THEN
2092   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
2093   W(fun (asl,w) ->
2094         let t1 = rand(lhand w) and t2 = rand(rand w) in
2095         let (x1,y1,z1) = three_adjacent_points (dest_setenum t1)
2096         and (x2,y2,z2) = three_adjacent_points (dest_setenum t2) in
2097         let th1 = SPECL [`A:real^3^3`;x1;y1;z1;x2;y2;z2] MATRIX_BY_CRAMER in
2098         let th2 = REWRITE_RULE[VECTOR_3; DET_3] th1 in
2099         let th3 = CONV_RULE (DEPTH_CONV REAL_RAT5_MUL_CONV) th2 in
2100         let th4 = CONV_RULE (DEPTH_CONV
2101          (REAL_RAT5_ADD_CONV ORELSEC REAL_RAT5_SUB_CONV)) th3 in
2102         let th5 = CONV_RULE let_CONV th4 in
2103         let th6 = CONV_RULE(ONCE_DEPTH_CONV REAL_RAT5_DIV_CONV) th5 in
2104         let th7 = CONV_RULE(ONCE_DEPTH_CONV REAL_RAT5_EQ_CONV) th6 in
2105         let th8 = MP th7 (EQT_ELIM(REWRITE_CONV[] (lhand(concl th7)))) in
2106         let tms = map rhs (conjuncts(rand(concl th8))) in
2107         let matt = mk_33matrix tms in
2108         MATCH_MP_TAC CONGRUENT_SIMPLE THEN EXISTS_TAC matt THEN CONJ_TAC THENL
2109          [REWRITE_TAC[ORTHOGONAL_MATRIX; CART_EQ] THEN
2110           SIMP_TAC[transp; LAMBDA_BETA; matrix_mul; mat] THEN
2111           REWRITE_TAC[DIMINDEX_3; SUM_3; FORALL_3; VECTOR_3; ARITH] THEN
2112           CONV_TAC(ONCE_DEPTH_CONV REAL_RAT5_MUL_CONV) THEN
2113           CONV_TAC(DEPTH_CONV REAL_RAT5_ADD_CONV) THEN
2114           CONV_TAC(ONCE_DEPTH_CONV REAL_RAT5_EQ_CONV) THEN
2115           REWRITE_TAC[] THEN NO_TAC;
2116           REWRITE_TAC[IMAGE_CLAUSES; MATRIX_VECTOR_MUL_3] THEN
2117           CONV_TAC(ONCE_DEPTH_CONV REAL_RAT5_MUL_CONV) THEN
2118           CONV_TAC(DEPTH_CONV REAL_RAT5_ADD_CONV) THEN
2119           REWRITE_TAC[INSERT_AC]]);;
2120
2121 let TETRAHEDRON_CONGRUENT_EDGES = prove
2122  (`!e1 e2. e1 face_of std_tetrahedron /\ aff_dim e1 = &1 /\
2123            e2 face_of std_tetrahedron /\ aff_dim e2 = &1
2124            ==> e1 congruent e2`,
2125   CONGRUENT_EDGES_TAC TETRAHEDRON_EDGES);;
2126
2127 let TETRAHEDRON_CONGRUENT_FACETS = prove
2128  (`!f1 f2. f1 face_of std_tetrahedron /\ aff_dim f1 = &2 /\
2129            f2 face_of std_tetrahedron /\ aff_dim f2 = &2
2130            ==> f1 congruent f2`,
2131   CONGRUENT_FACES_TAC TETRAHEDRON_FACETS);;
2132
2133 let CUBE_CONGRUENT_EDGES = prove
2134  (`!e1 e2. e1 face_of std_cube /\ aff_dim e1 = &1 /\
2135            e2 face_of std_cube /\ aff_dim e2 = &1
2136            ==> e1 congruent e2`,
2137   CONGRUENT_EDGES_TAC CUBE_EDGES);;
2138
2139 let CUBE_CONGRUENT_FACETS = prove
2140  (`!f1 f2. f1 face_of std_cube /\ aff_dim f1 = &2 /\
2141            f2 face_of std_cube /\ aff_dim f2 = &2
2142            ==> f1 congruent f2`,
2143   CONGRUENT_FACES_TAC CUBE_FACETS);;
2144
2145 let OCTAHEDRON_CONGRUENT_EDGES = prove
2146  (`!e1 e2. e1 face_of std_octahedron /\ aff_dim e1 = &1 /\
2147            e2 face_of std_octahedron /\ aff_dim e2 = &1
2148            ==> e1 congruent e2`,
2149   CONGRUENT_EDGES_TAC OCTAHEDRON_EDGES);;
2150
2151 let OCTAHEDRON_CONGRUENT_FACETS = prove
2152  (`!f1 f2. f1 face_of std_octahedron /\ aff_dim f1 = &2 /\
2153            f2 face_of std_octahedron /\ aff_dim f2 = &2
2154            ==> f1 congruent f2`,
2155   CONGRUENT_FACES_TAC OCTAHEDRON_FACETS);;
2156
2157 let DODECAHEDRON_CONGRUENT_EDGES = prove
2158  (`!e1 e2. e1 face_of std_dodecahedron /\ aff_dim e1 = &1 /\
2159            e2 face_of std_dodecahedron /\ aff_dim e2 = &1
2160            ==> e1 congruent e2`,
2161   CONGRUENT_EDGES_TAC DODECAHEDRON_EDGES);;
2162
2163 let DODECAHEDRON_CONGRUENT_FACETS = prove
2164  (`!f1 f2. f1 face_of std_dodecahedron /\ aff_dim f1 = &2 /\
2165            f2 face_of std_dodecahedron /\ aff_dim f2 = &2
2166            ==> f1 congruent f2`,
2167   CONGRUENT_FACES_TAC DODECAHEDRON_FACETS);;
2168
2169 let ICOSAHEDRON_CONGRUENT_EDGES = prove
2170  (`!e1 e2. e1 face_of std_icosahedron /\ aff_dim e1 = &1 /\
2171            e2 face_of std_icosahedron /\ aff_dim e2 = &1
2172            ==> e1 congruent e2`,
2173   CONGRUENT_EDGES_TAC ICOSAHEDRON_EDGES);;
2174
2175 let ICOSAHEDRON_CONGRUENT_FACETS = prove
2176  (`!f1 f2. f1 face_of std_icosahedron /\ aff_dim f1 = &2 /\
2177            f2 face_of std_icosahedron /\ aff_dim f2 = &2
2178            ==> f1 congruent f2`,
2179   CONGRUENT_FACES_TAC ICOSAHEDRON_FACETS);;