text_formalization/tame/JGTDEBU.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Tame Hypermap                                                     *)\r
   5 (* Author: Alexey Solovyev                                                    *)\r
   6 (* Date: 2013-01-22                                                           *)\r
   7 (* JGTDEBU: general properties of a contravening packing                      *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 needs "fan/hypermap_iso-compiled.hl";;\r
  11 needs "tame/TameGeneral.hl";;\r
  12 \r
  13 \r
  14 module Jgtdebu = struct\r
  15 \r
  16 parse_as_infix("iso",(24,"right"));;\r
  17 open Tame_defs;;\r
  18 open Fan_defs;;\r
  19 open Hypermap_iso;;\r
  20 open Hypermap_and_fan;;\r
  21 open Tame_general;;\r
  22 \r
  23 let contravening_imp_conforming = prove(`!V. contravening V ==>\r
  24                                           conforming_fan (vec 0,V,ESTD V)`,\r
  25    REPEAT STRIP_TAC THEN\r
  26      MATCH_MP_TAC Conforming.PIIJBJK THEN\r
  27      MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN \r
  28      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
  29      ASM_REWRITE_TAC[Planarity.fan80] THEN\r
  30      CONJ_TAC THEN REPEAT GEN_TAC THEN REPEAT DISCH_TAC THENL\r
  31      [\r
  32        MATCH_MP_TAC (ARITH_RULE `a >= 3 ==> a > 1`) THEN\r
  33          MATCH_MP_TAC SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3 THEN\r
  34          ASM_SIMP_TAC[CONTRAVENING_IMP_SURROUNDED];\r
  35        ALL_TAC\r
  36      ] THEN\r
  37      SUBGOAL_THEN `v,u IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL\r
  38      [\r
  39        REWRITE_TAC[dart_of_fan; IN_UNION; IN_ELIM_THM] THEN DISJ2_TAC THEN\r
  40          EXISTS_TAC `v:real^3` THEN EXISTS_TAC `u:real^3` THEN ASM_REWRITE_TAC[];\r
  41        ALL_TAC\r
  42      ] THEN\r
  43      ASM_SIMP_TAC[GSYM CONTRAVENING_IMP_AZIM_DART_EQ_AZIM; AZIM_DART_POS] THEN\r
  44      MP_TAC (SPEC `V:real^3->bool` CONTRAVENING_IMP_FULLY_SURROUNDED) THEN\r
  45      ASM_SIMP_TAC[fully_surrounded]);;\r
  46 \r
  47 \r
  48 (* 1 *)\r
  49 let JGTDEBU1 = prove(`!V. contravening V \r
  50                      ==> planar_hypermap (hypermap_of_fan (V, ESTD V))`,\r
  51    REPEAT STRIP_TAC THEN\r
  52      MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN \r
  53      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
  54      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] fan_hypermaps_iso) THEN\r
  55      ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o MATCH_MP iso_planar) THEN \r
  56      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN\r
  57      ASM_SIMP_TAC[Conforming.GGRLKHP; contravening_imp_conforming]);;\r
  58 \r
  59 \r
  60 (* 2 *)\r
  61 let JGTDEBU2 = prove(`!V. contravening V ==>\r
  62                        plain_hypermap (hypermap_of_fan (V,ESTD V))`,\r
  63    REPEAT STRIP_TAC THEN\r
  64      MATCH_MP_TAC PLAIN_HYPERMAP_OF_FAN THEN\r
  65      ASM_SIMP_TAC[CONTRAVENING_FAN]);;\r
  66 \r
  67          \r
  68 (* 3 *)\r
  69 let JGTDEBU3 = prove(`!V. contravening V \r
  70                      ==> connected_hypermap (hypermap_of_fan (V, ESTD V))`,\r
  71    REPEAT STRIP_TAC THEN\r
  72      MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN \r
  73      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
  74      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] fan_hypermaps_iso) THEN\r
  75      ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o MATCH_MP iso_connected) THEN \r
  76      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN\r
  77      ASM_SIMP_TAC[Conforming.WGVWSKE; contravening_imp_conforming]);;\r
  78 \r
  79 \r
  80 (* 4 *)\r
  81 let JGTDEBU4 = prove(`!V. contravening V ==> \r
  82        simple_hypermap (hypermap_of_fan (V, ESTD V))`,\r
  83    REPEAT STRIP_TAC THEN\r
  84      MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN \r
  85      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
  86      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] fan_hypermaps_iso) THEN\r
  87      ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o MATCH_MP iso_simple) THEN \r
  88      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN\r
  89      ASM_SIMP_TAC[Conforming.SRPRNPL; contravening_imp_conforming]);;\r
  90 \r
  91 \r
  92 (* 5 *)\r
  93 let JGTDEBU5 = prove(`!V. contravening V ==>\r
  94                        is_edge_nondegenerate (hypermap_of_fan (V,ESTD V))`,\r
  95    REPEAT STRIP_TAC THEN\r
  96      MATCH_MP_TAC HYPERMAP_OF_FAN_EDGE_NONDEGENERATE THEN\r
  97      ASM_SIMP_TAC[CONTRAVENING_FAN; CONTRAVENING_IMP_FULLY_SURROUNDED]);;\r
  98 \r
  99 \r
 100 (* 6 *)\r
 101 let JGTDEBU6 = prove(`!V. contravening V ==>\r
 102                        no_loops (hypermap_of_fan (V,ESTD V))`,\r
 103    REPEAT STRIP_TAC THEN\r
 104      MATCH_MP_TAC HYPERMAP_OF_FAN_NO_LOOPS THEN\r
 105      ASM_SIMP_TAC[CONTRAVENING_FAN]);;\r
 106 \r
 107 \r
 108 (* 7 *)\r
 109 let JGTDEBU7 = prove(`!V.  contravening V ==>\r
 110                        is_no_double_joints (hypermap_of_fan (V,ESTD V))`,\r
 111    REPEAT STRIP_TAC THEN\r
 112      MATCH_MP_TAC HYPERMAP_OF_FAN_NO_DOUBLE_JOINTS THEN\r
 113      ASM_SIMP_TAC[CONTRAVENING_FAN]);;\r
 114 \r
 115 \r
 116 (* number_of_faces  (hypermap_of_fan (V, ESTD V)) >= 3 *)\r
 117 let CONTRAVENING_HAS_SIZE_lemma = prove(`!V. contravening V ==> ?n. n > 0 /\ V HAS_SIZE n`,\r
 118    GEN_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN\r
 119      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 120      REMOVE_THEN "A" MP_TAC THEN\r
 121      REWRITE_TAC[contravening] THEN\r
 122      REPLICATE_TAC 4 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN\r
 123      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN\r
 124      EXISTS_TAC `CARD (V:real^3->bool)` THEN\r
 125      ASM_SIMP_TAC[ARITH_RULE `a = 13 \/ a = 14 \/ a = 15 ==> a > 0`] THEN\r
 126      REWRITE_TAC[HAS_SIZE] THEN\r
 127      REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN\r
 128      REWRITE_TAC[Fan_defs.FAN; Fan_defs.fan1] THEN\r
 129      SIMP_TAC[]);;\r
 130      \r
 131 \r
 132 (* 8 *)\r
 133 let JGTDEBU8 = prove(`!V. contravening V ==>\r
 134                        number_of_faces (hypermap_of_fan (V,ESTD V)) >= 3`,\r
 135    GEN_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN\r
 136      MP_TAC (SPEC `V:real^3->bool` JGTDEBU4) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 137      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 138      USE_THEN "A" MP_TAC THEN\r
 139      REWRITE_TAC[contravening] THEN\r
 140      REPLICATE_TAC 5 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN\r
 141      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN\r
 142      REWRITE_TAC[Hypermap.number_of_faces] THEN\r
 143      SUBGOAL_THEN `?v:real^3. v IN V` MP_TAC THENL\r
 144      [\r
 145        MP_TAC (SPEC `V:real^3->bool` CONTRAVENING_HAS_SIZE_lemma) THEN\r
 146          ASM_REWRITE_TAC[ARITH_RULE `n > 0 <=> ~(n = 0)`] THEN\r
 147          STRIP_TAC THEN\r
 148          MP_TAC (SPEC `n:num` num_CASES) THEN\r
 149          ASM_REWRITE_TAC[] THEN\r
 150          STRIP_TAC THEN\r
 151          FIRST_X_ASSUM (MP_TAC o check (is_binary "HAS_SIZE" o concl)) THEN\r
 152          ASM_REWRITE_TAC[HAS_SIZE_CLAUSES] THEN\r
 153          STRIP_TAC THEN\r
 154          EXISTS_TAC `a:real^3` THEN\r
 155          POP_ASSUM MP_TAC THEN\r
 156          SIMP_TAC[INSERT; EXTENSION; IN_ELIM_THM];\r
 157        ALL_TAC\r
 158      ] THEN\r
 159      STRIP_TAC THEN\r
 160      MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `v:real^3`] DART_EXISTS) THEN\r
 161      ASM_REWRITE_TAC[] THEN\r
 162      STRIP_TAC THEN\r
 163      ABBREV_TAC `H = hypermap_of_fan (V,ESTD V)` THEN \r
 164      SUBGOAL_THEN `v,w IN dart1_of_fan (V:real^3->bool,ESTD V)` ASSUME_TAC THENL\r
 165      [\r
 166        MATCH_MP_TAC SURROUNDED_IMP_IN_DART1_OF_FAN THEN\r
 167          ASM_SIMP_TAC[];\r
 168        ALL_TAC\r
 169      ] THEN\r
 170      ABBREV_TAC `A = {face H y | y | y IN dart H /\ T /\ y IN node H (v:real^3,w:real^3)}` THEN\r
 171      SUBGOAL_THEN `A SUBSET face_set (H:(real^3#real^3)hypermap)` ASSUME_TAC THENL\r
 172      [\r
 173        EXPAND_TAC "A" THEN\r
 174          REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN\r
 175          GEN_TAC THEN STRIP_TAC THEN\r
 176          ASM_REWRITE_TAC[GSYM Hypermap.lemma_in_face_set] THEN\r
 177          EXPAND_TAC "H" THEN\r
 178          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN];\r
 179        ALL_TAC\r
 180      ] THEN\r
 181      ONCE_REWRITE_TAC[GE] THEN\r
 182      MATCH_MP_TAC LE_TRANS THEN\r
 183      EXISTS_TAC `CARD (A:(real^3#real^3->bool)->bool)` THEN\r
 184      CONJ_TAC THENL\r
 185      [\r
 186        EXPAND_TAC "A" THEN\r
 187          MP_TAC (ISPECL [`H:(real^3#real^3)hypermap`; `v:real^3,w:real^3`; `(\x:real^3#real^3. T)`] SIMPLE_HYPERMAP_lemma) THEN\r
 188          REMOVE_ASSUM THEN REMOVE_ASSUM THEN\r
 189          ASM_REWRITE_TAC[ETA_AX] THEN\r
 190          EXPAND_TAC "H" THEN\r
 191          ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 192          SIMP_TAC[SIMPLE_HYPERMAP_lemma] THEN\r
 193          DISCH_THEN (fun th -> ALL_TAC) THEN\r
 194          SUBGOAL_THEN `{y:real^3#real^3 | y IN node H (v,w)} = node H (v,w)` MP_TAC THENL\r
 195          [\r
 196            REWRITE_TAC[EXTENSION; IN_ELIM_THM];\r
 197            ALL_TAC\r
 198          ] THEN\r
 199          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 200          REWRITE_TAC[GSYM GE] THEN\r
 201          EXPAND_TAC "H" THEN\r
 202          MATCH_MP_TAC SURROUNDED_IMP_CARD_NODE_GE_3 THEN\r
 203          ASM_SIMP_TAC[];\r
 204        ALL_TAC\r
 205      ] THEN\r
 206 \r
 207 \r
 208      MATCH_MP_TAC CARD_SUBSET THEN\r
 209      ASM_REWRITE_TAC[Hypermap.FINITE_HYPERMAP_ORBITS]\r
 210                     );;\r
 211  \r
 212 \r
 213 (* 10 *)\r
 214 (* tame_10  (hypermap_of_fan (V, ESTD V)) *)\r
 215 let JGTDEBU10 = prove(`!V. contravening V ==> tame_10 (hypermap_of_fan (V,ESTD V))`,\r
 216    GEN_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN\r
 217      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 218      REMOVE_THEN "A" MP_TAC THEN\r
 219      REWRITE_TAC[contravening; tame_10; Hypermap.number_of_nodes] THEN\r
 220      REPLICATE_TAC 4 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN\r
 221      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN\r
 222      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] NODE_SET_AS_IMAGE) THEN\r
 223      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
 224      SUBGOAL_THEN `CARD(IMAGE (f:real^3 -> ((real^3#real^3) -> bool)) V) = CARD V` (fun th -> REWRITE_TAC[th]) THENL\r
 225      [\r
 226        MATCH_MP_TAC CARD_IMAGE_INJ THEN\r
 227          FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (concl th) = `(vec 0:real^3,V:real^3->bool,ESTD V)`)) THEN\r
 228          REWRITE_TAC[Fan_defs.FAN; Fan_defs.fan1] THEN\r
 229          ASM_SIMP_TAC[] THEN\r
 230          DISCH_THEN (fun th -> ALL_TAC) THEN\r
 231          REPEAT STRIP_TAC THEN\r
 232          FIRST_X_ASSUM (MP_TAC o SPECL [`x:real^3`; `y:real^3`]) THEN\r
 233          ASM_SIMP_TAC[];\r
 234        ALL_TAC\r
 235      ] THEN\r
 236      ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]);;\r
 237      \r
 238 \r
 239 (* 11 *)\r
 240 (* tame_11a  (hypermap_of_fan (V, ESTD V)) *)\r
 241 let JGTDEBU11 = prove(`!V. contravening V ==> tame_11a (hypermap_of_fan (V,ESTD V))`,\r
 242    REPEAT STRIP_TAC THEN\r
 243      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN\r
 244      REWRITE_TAC[tame_11a] THEN\r
 245      ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN\r
 246      REPEAT STRIP_TAC THEN\r
 247      MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN\r
 248      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN\r
 249      MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `v:real^3`; `w:real^3`] SURROUNDED_IMP_IN_DART1_OF_FAN) THEN\r
 250      MP_TAC (SPEC_ALL CONTRAVENING_IMP_SURROUNDED) THEN\r
 251      ASM_SIMP_TAC[] THEN REPEAT DISCH_TAC THEN\r
 252      MATCH_MP_TAC SURROUNDED_IMP_CARD_NODE_GE_3 THEN\r
 253      ASM_REWRITE_TAC[]);;\r
 254          \r
 255 \r
 256 end;;\r