legacy/oldpacking/packing/development/sum_beta_bump.hl

   1 (* ========================================================================= *)\r
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
   3 (*                                                                           *)\r
   4 (*      Authour   : VU KHAC KY                                               *)\r
   5 (*      Book lemma:                                                          *)\r
   6 (*      Chaper    : Packing (Cells cluster)                                  *)\r
   7 (*                                                                           *)\r
   8 (* ------------------ The lemma about sum of beta_bump --------------------- *)\r
   9 (* ========================================================================= *)\r
  10 \r
  11 (* ========================================================================= *)\r
  12 (*    Checkpointed files                                                     *)\r
  13 (* ========================================================================= *)\r
  14 (*\r
  15 \r
  16 loads "/home/vu/flyspeck/working/marchal_cells_3.hl";;\r
  17 flyspeck_needs "packing/UPFZBZM_support_lemmas.hl";;\r
  18 open Upfzbzm_support_lemmas;;\r
  19 flyspeck_needs "packing/LEPJBDJ.hl";;\r
  20 open Lepjbdj;;\r
  21 \r
  22 *)\r
  23 \r
  24 (* ========================================================================== *)\r
  25 (*   Begin the proof                                                          *)\r
  26 (* ========================================================================== *)\r
  27 \r
  28 module Sum_beta_bump = struct\r
  29 \r
  30 open Rogers;;\r
  31 open Vukhacky_tactics;;\r
  32 open Pack_defs;;\r
  33 open Pack_concl;; \r
  34 open Pack1;;\r
  35 open Sphere;; \r
  36 open Marchal_cells;;\r
  37 open Emnwuus;;\r
  38 open Marchal_cells_2_new;;\r
  39 open Lepjbdj;;\r
  40 open Upfzbzm_support_lemmas;;\r
  41 \r
  42 let SUM_BETA_BUMP_LEMMA = prove_by_refinement (\r
  43  `!V X. saturated V /\ packing V /\ mcell_set V X ==> \r
  44          sum {e | e IN critical_edgeX V X } (\e. beta_bump V e X) = &0`,\r
  45 \r
  46 [(REPEAT STRIP_TAC THEN UP_ASM_TAC);\r
  47  (ASM_CASES_TAC `~(X:real^3->bool = {})`);\r
  48  (REWRITE_TAC[mcell_set; IN_ELIM_THM]);\r
  49  (STRIP_TAC);\r
  50  (NEW_GOAL `barV V 3 ul`);\r
  51  (ASM_SET_TAC[IN]);\r
  52 \r
  53  (ASM_CASES_TAC `i < 4`);  (* consider case i < 4 va i >= 4 *)\r
  54  (NEW_GOAL `~(i = 4)`);\r
  55  (ASM_ARITH_TAC);\r
  56  (NEW_GOAL `i <= 4`);\r
  57  (ASM_ARITH_TAC);\r
  58  (ASM_REWRITE_TAC[beta_bump]);\r
  59  (REPEAT LET_TAC);\r
  60  (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);\r
  61  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
  62  (STRIP_TAC);\r
  63  (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\ \r
  64                               mcell i V ul = mcell k V ul')`);\r
  65  (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);\r
  66  (ASM_REWRITE_TAC[]);\r
  67  (MATCH_MP_TAC SELECT_AX);\r
  68  (EXISTS_TAC `(i:num,ul:(real^3)list)`);\r
  69  (EXPAND_TAC "P");\r
  70  (REWRITE_TAC[BETA_THM]);\r
  71  (ASM_REWRITE_TAC[IN]);\r
  72  (UP_ASM_TAC THEN EXPAND_TAC "P");\r
  73  (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);\r
  74  (NEW_GOAL `barV V 3 ul'`);\r
  75  (ASM_SET_TAC[]);\r
  76 \r
  77  (NEW_GOAL `i = k:num`);\r
  78  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);\r
  79  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
  80  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
  81  (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`);\r
  82  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
  83  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
  84  (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
  85 \r
  86  (ASM_CASES_TAC `i = 0`);\r
  87  (NEW_GOAL `V INTER mcell i V ul  = {} `);\r
  88  (REWRITE_TAC[ASSUME `i = 0`]);\r
  89  (MATCH_MP_TAC LEPJBDJ_0);\r
  90  (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);\r
  91  (ASM_CASES_TAC `k = 0`);\r
  92  (ASM_REWRITE_TAC[]);\r
  93  (NEW_GOAL `V INTER mcell k V ul' \r
  94            = set_of_list (truncate_simplex (k - 1) ul')`);\r
  95  (MATCH_MP_TAC LEPJBDJ);\r
  96  (ASM_REWRITE_TAC[]);\r
  97  (STRIP_TAC);\r
  98  (ASM_ARITH_TAC);\r
  99  (ASM_MESON_TAC[]);\r
 100  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
 101 \r
 102  (ASM_CASES_TAC `k = 1`);\r
 103  (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);\r
 104  (ASM_SET_TAC[]);\r
 105  (ASM_CASES_TAC `k = 2`);\r
 106  (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);\r
 107  (ASM_SET_TAC[]);\r
 108  (ASM_CASES_TAC `k = 3`);\r
 109  (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);\r
 110  (ASM_SET_TAC[]);\r
 111  (ASM_CASES_TAC `k = 4`);\r
 112  (ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]);\r
 113  (ASM_SET_TAC[]);\r
 114  (NEW_GOAL `F`);\r
 115  (ASM_ARITH_TAC);\r
 116  (ASM_MESON_TAC[]);  (* Finish the case i = 0 *)\r
 117 \r
 118  (NEW_GOAL `V INTER mcell i V ul\r
 119            = set_of_list (truncate_simplex (i - 1) ul)`);\r
 120  (MATCH_MP_TAC LEPJBDJ);\r
 121  (ASM_REWRITE_TAC[]);\r
 122  (STRIP_TAC);\r
 123  (ASM_ARITH_TAC);\r
 124  (ASM_MESON_TAC[]);\r
 125 \r
 126  (ASM_CASES_TAC `k = 0`);\r
 127  (NEW_GOAL `V INTER mcell k V ul' = {}`);\r
 128  (ASM_REWRITE_TAC[]);\r
 129  (MATCH_MP_TAC LEPJBDJ_0);\r
 130  (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);\r
 131  (NEW_GOAL `F`);\r
 132  (NEW_GOAL \r
 133   `~(set_of_list (truncate_simplex (i - 1) (ul:(real^3)list)) = {})`);\r
 134  (ASM_CASES_TAC `i = 1`);\r
 135  (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);\r
 136  (SET_TAC[]);\r
 137  (ASM_CASES_TAC `i = 2`);\r
 138  (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);\r
 139  (SET_TAC[]);\r
 140  (ASM_CASES_TAC `i = 3`);\r
 141  (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);\r
 142  (SET_TAC[]);\r
 143  (NEW_GOAL `F`);\r
 144  (ASM_ARITH_TAC);\r
 145  (ASM_MESON_TAC[]);\r
 146  (ASM_MESON_TAC[]);\r
 147  (ASM_MESON_TAC[]);\r
 148 \r
 149  (NEW_GOAL `V INTER mcell k V ul'\r
 150            = set_of_list (truncate_simplex (k - 1) ul')`);\r
 151  (MATCH_MP_TAC LEPJBDJ);\r
 152  (ASM_REWRITE_TAC[]);\r
 153  (STRIP_TAC);\r
 154  (ASM_ARITH_TAC);\r
 155  (ASM_MESON_TAC[]);\r
 156 \r
 157  (NEW_GOAL `CARD (set_of_list (truncate_simplex (i - 1) (ul:(real^3)list))) \r
 158             = i:num`);\r
 159  (REWRITE_WITH \r
 160   `LENGTH (truncate_simplex (i - 1) (ul:(real^3)list)) = (i - 1) + 1 /\ \r
 161    CARD (set_of_list (truncate_simplex (i - 1) ul)) = (i - 1) + 1`);\r
 162  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);\r
 163  (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);\r
 164  (ASM_REWRITE_TAC[]);\r
 165  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
 166  (EXISTS_TAC `3`);\r
 167  (STRIP_TAC);\r
 168  (ASM_REWRITE_TAC[]);\r
 169  (ASM_ARITH_TAC);\r
 170  (ASM_ARITH_TAC);\r
 171 \r
 172  (NEW_GOAL `CARD (set_of_list (truncate_simplex (k - 1) (ul':(real^3)list))) \r
 173             = k:num`);\r
 174  (REWRITE_WITH \r
 175   `LENGTH (truncate_simplex (k - 1) (ul':(real^3)list)) = (k - 1) + 1 /\ \r
 176    CARD (set_of_list (truncate_simplex (k - 1) ul')) = (k - 1) + 1`);\r
 177  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);\r
 178  (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);\r
 179  (ASM_REWRITE_TAC[]);\r
 180  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
 181  (EXISTS_TAC `3`);\r
 182  (STRIP_TAC);\r
 183  (ASM_REWRITE_TAC[]);\r
 184  (ASM_ARITH_TAC);\r
 185  (ASM_ARITH_TAC);\r
 186  (ASM_MESON_TAC[]);\r
 187  (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]);\r
 188  (ASM_REWRITE_TAC[]);\r
 189 \r
 190  (NEW_GOAL `!e. sum\r
 191       {e',e'',p,vl | k = 4 /\  critical_edgeX V (mcell k V ul') = {e', e''} /\\r
 192                      e = e' /\ p permutes 0..3 /\ vl = left_action_list p ul' /\\r
 193                      e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}}\r
 194       (\(e',e'',p,vl). \r
 195            (bump (hl [EL 0 vl; EL 1 vl]) - bump (hl [EL 2 vl; EL 3 vl])) / &4) \r
 196             = &0`);\r
 197  GEN_TAC;\r
 198  (ABBREV_TAC `SET1 = {e',e'',p,vl | k = 4 /\\r
 199                     critical_edgeX V (mcell k V ul') = {e', e''} /\\r
 200                     e = e' /\ p permutes 0..3 /\\r
 201                     vl = left_action_list p ul' /\\r
 202                     e' = {EL 0 vl, EL 1 vl} /\\r
 203                     e'' = {EL 2 vl, EL 3 vl}}`);\r
 204  (NEW_GOAL \r
 205   `SET1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool = {}`);\r
 206  (EXPAND_TAC "SET1");\r
 207  (NEW_GOAL `~(k = 4)`);\r
 208  (ASM_MESON_TAC[]);\r
 209  (UP_ASM_TAC);\r
 210  (SET_TAC[]);\r
 211  (ASM_REWRITE_TAC[]);\r
 212  (ASM_REWRITE_TAC[SUM_CLAUSES]);\r
 213 \r
 214  (ASM_REWRITE_TAC[]);\r
 215  (REWRITE_TAC[SUM_0]);\r
 216 \r
 217 (* Finish the case where i < 4 *)\r
 218 (* ========================================================================= *)\r
 219 (* begin with the case i >= 4  *)\r
 220 \r
 221  (ASM_REWRITE_TAC[beta_bump]);\r
 222  (REPEAT LET_TAC);\r
 223  (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);\r
 224  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 225  (STRIP_TAC);\r
 226  (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\ \r
 227                               mcell i V ul = mcell k V ul')`);\r
 228  (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);\r
 229  (ASM_REWRITE_TAC[]);\r
 230  (MATCH_MP_TAC SELECT_AX);\r
 231  (EXISTS_TAC `(4,ul:(real^3)list)`);\r
 232  (EXPAND_TAC "P");\r
 233  (REWRITE_TAC[BETA_THM]);\r
 234  (ASM_REWRITE_TAC[IN; ARITH_RULE `4 <= 4`]);\r
 235  (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`; \r
 236    ARITH_RULE `4 >= 4`; mcell4]);\r
 237  (UP_ASM_TAC THEN EXPAND_TAC "P");\r
 238  (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);\r
 239  (NEW_GOAL `barV V 3 ul'`);\r
 240  (ASM_SET_TAC[]);\r
 241  (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]);\r
 242 \r
 243  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);\r
 244  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
 245  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
 246  (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`);\r
 247  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
 248  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
 249  (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
 250  (NEW_GOAL `mcell i V ul = mcell 4 V ul`);\r
 251  (UNDISCH_TAC `mcell i V ul = mcell k V ul'` THEN DISCH_TAC THEN DEL_TAC);\r
 252  (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`; \r
 253    ARITH_RULE `4 >= 4`; mcell4]);\r
 254 \r
 255  (NEW_GOAL `k = 4:num`);\r
 256 \r
 257  (NEW_GOAL `V INTER mcell 4 V ul  = \r
 258              set_of_list (truncate_simplex 3 ul)`);\r
 259  (REWRITE_TAC[ARITH_RULE `3 = 4 - 1`]);\r
 260  (MATCH_MP_TAC LEPJBDJ);\r
 261  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]);\r
 262  (ASM_MESON_TAC[]);\r
 263 \r
 264  (ASM_CASES_TAC `k = 0`);\r
 265  (NEW_GOAL `V INTER mcell k V ul'  = {}`);\r
 266  (REWRITE_TAC[ASSUME `k = 0`]);\r
 267  (MATCH_MP_TAC LEPJBDJ_0);\r
 268  (ASM_REWRITE_TAC[]);\r
 269  (NEW_GOAL `F`);\r
 270  (UNDISCH_TAC `V INTER mcell 4 V ul = set_of_list (truncate_simplex 3 ul)`);\r
 271  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]);\r
 272  (ASM_SET_TAC[]);\r
 273  (ASM_MESON_TAC[]);\r
 274 \r
 275 (* ============================= *)\r
 276 \r
 277  (NEW_GOAL `V INTER mcell k V ul'  = \r
 278              set_of_list (truncate_simplex (k - 1) ul')`);\r
 279  (MATCH_MP_TAC LEPJBDJ);\r
 280  (ASM_REWRITE_TAC[]);\r
 281  (STRIP_TAC);\r
 282  (ASM_ARITH_TAC);\r
 283  (ASM_SET_TAC[]);\r
 284 \r
 285  (NEW_GOAL `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = \r
 286              set_of_list (truncate_simplex (k - 1) ul')`);\r
 287  (ASM_SET_TAC[]);\r
 288  (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} = 4`);\r
 289  (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);\r
 290  (ASM_REWRITE_TAC[set_of_list]);\r
 291  (REWRITE_WITH `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`);\r
 292  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);\r
 293  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
 294  (ARITH_TAC);\r
 295 \r
 296  (ASM_CASES_TAC `k = 1`);\r
 297  (NEW_GOAL `F`);\r
 298  (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = \r
 299                 set_of_list (truncate_simplex (k - 1) ul')`);\r
 300  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `1 - 1 = 0`;   \r
 301                    TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);\r
 302  (STRIP_TAC);\r
 303  (NEW_GOAL `CARD {v0:real^3} = 4`);\r
 304  (ASM_MESON_TAC[]);\r
 305  (UP_ASM_TAC THEN REWRITE_TAC[Geomdetail.CARD_SING]);\r
 306  (ARITH_TAC);\r
 307  (ASM_MESON_TAC[]);\r
 308 \r
 309  (ASM_CASES_TAC `k = 2`);\r
 310  (NEW_GOAL `F`);\r
 311  (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = \r
 312                 set_of_list (truncate_simplex (k - 1) ul')`);\r
 313  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `2 - 1 = 1`;   \r
 314                    TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);\r
 315  (STRIP_TAC);\r
 316  (NEW_GOAL `CARD {v0, v1:real^3} = 4`);\r
 317  (ASM_MESON_TAC[]);\r
 318  (NEW_GOAL `CARD {v0, v1:real^3} <= 2`);\r
 319  (MESON_TAC[Geomdetail.CARD2]);\r
 320  (ASM_ARITH_TAC);\r
 321  (ASM_MESON_TAC[]);\r
 322 \r
 323  (ASM_CASES_TAC `k = 3`);\r
 324  (NEW_GOAL `F`);\r
 325  (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = \r
 326                 set_of_list (truncate_simplex (k - 1) ul')`);\r
 327  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `3 - 1 = 2`;   \r
 328                    TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);\r
 329  (STRIP_TAC);\r
 330  (NEW_GOAL `CARD {v0, v1, v2:real^3} = 4`);\r
 331  (ASM_MESON_TAC[]);\r
 332  (NEW_GOAL `CARD {v0, v1, v2:real^3} <= 3`);\r
 333  (MESON_TAC[Geomdetail.CARD3]);\r
 334  (ASM_ARITH_TAC);\r
 335  (ASM_MESON_TAC[]);\r
 336 \r
 337  (ASM_ARITH_TAC);  (* concluded that k = 4 now *)\r
 338 \r
 339 (* ======================================================================== *)\r
 340 \r
 341 \r
 342  (REWRITE_TAC[ASSUME `mcell i V ul = mcell k V ul'`; ASSUME `k = 4`]);\r
 343  (ASM_CASES_TAC `~(CARD (critical_edgeX V (mcell 4 V ul'))  = 2)`);\r
 344  (MATCH_MP_TAC SUM_EQ_0);\r
 345  (REPEAT STRIP_TAC);\r
 346  (ABBREV_TAC `y = {v0,v1,v2,v3:real^3} DIFF x`);\r
 347  (ASM_CASES_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`);\r
 348  (REWRITE_WITH \r
 349  `{e',e'',p,vl | critical_edgeX V (mcell 4 V ul') = {e', e''} /\\r
 350                 x = e' /\\r
 351                 p permutes 0..3 /\\r
 352                 vl = left_action_list p ul' /\\r
 353                 e' = {EL 0 vl, EL 1 vl} /\\r
 354                 e'' = {EL 2 vl, EL 3 vl}} = {}`);\r
 355  (REWRITE_TAC[SET_RULE `a = {} <=> (!t. t IN a ==> F)`]);\r
 356  (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
 357  (NEW_GOAL `y = e'':real^3->bool`);\r
 358  (ONCE_ASM_REWRITE_TAC[] THEN EXPAND_TAC "y");\r
 359  (REWRITE_TAC[ASSUME `x = e':real^3->bool`; \r
 360                ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);\r
 361  (REWRITE_WITH `{v0, v1, v2, v3:real^3} = set_of_list (ul')`);\r
 362  (ASM_REWRITE_TAC[set_of_list]);\r
 363  (REWRITE_WITH `set_of_list (ul':(real^3)list) = set_of_list vl`);\r
 364  (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REWRITE_TAC[ASSUME \r
 365   `vl:(real^3)list = left_action_list p ul'`]);\r
 366  (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);\r
 367  (ASM_REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);\r
 368 \r
 369  (NEW_GOAL `vl:(real^3)list = [EL 0 vl; EL 1 vl; EL 2 vl; EL 3 vl]`);\r
 370  (ASM_REWRITE_TAC[TABLE_4; left_action_list; LENGTH; EL; HD; TL;\r
 371    ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4 /\ 1 = SUC 0 /\ 2 = SUC 1/\ 3 = SUC 2`]);\r
 372  (ABBREV_TAC `w0:real^3 = EL 0 vl`);\r
 373  (ABBREV_TAC `w1:real^3 = EL 1 vl`);\r
 374  (ABBREV_TAC `w2:real^3 = EL 2 vl`);\r
 375  (ABBREV_TAC `w3:real^3 = EL 3 vl`);\r
 376  (REWRITE_TAC[ASSUME `vl = [w0;w1;w2;w3:real^3]`; set_of_list]);\r
 377  (REWRITE_WITH `{w0,w1,w2,w3} = {w0,w1} UNION {w2,w3:real^3}`);\r
 378  (SET_TAC[]);\r
 379  (MATCH_MP_TAC (SET_RULE `DISJOINT a b ==> ((a UNION b) DIFF a = b)`));\r
 380 \r
 381  (REWRITE_TAC[DISJOINT; INTER]);\r
 382  (NEW_GOAL `CARD {w0, w1, w2 , w3:real^3} = 4`);\r
 383  (REWRITE_WITH `{w0, w1, w2 , w3:real^3} = set_of_list vl`);\r
 384  (REWRITE_TAC[ASSUME `vl = [w0; w1; w2; w3:real^3]`; set_of_list]);\r
 385  (ONCE_ASM_REWRITE_TAC[]);\r
 386  (REWRITE_WITH `set_of_list (left_action_list p ul') \r
 387                = set_of_list (ul':(real^3)list)`);\r
 388  (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);\r
 389  (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);\r
 390  (REWRITE_WITH `LENGTH (ul':(real^3)list) = 3 + 1 /\ \r
 391                  CARD (set_of_list ul') = 3 + 1`);\r
 392  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);\r
 393  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
 394  (ARITH_TAC);\r
 395  (REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]);\r
 396  (REWRITE_TAC[SET_RULE `x = {} <=> (!z. z IN x ==> F)`]);\r
 397  (REWRITE_TAC[IN;IN_ELIM_THM] THEN STRIP_TAC);\r
 398  (REPEAT STRIP_TAC);\r
 399 \r
 400  (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);\r
 401  (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`);\r
 402  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);\r
 403  (REWRITE_TAC[Geomdetail.CARD3]);\r
 404  (ASM_ARITH_TAC);\r
 405  (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);\r
 406  (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`);\r
 407  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);\r
 408  (REWRITE_TAC[Geomdetail.CARD3]);\r
 409  (ASM_ARITH_TAC);\r
 410  (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);\r
 411  (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`);\r
 412  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);\r
 413  (REWRITE_TAC[Geomdetail.CARD3]);\r
 414  (ASM_ARITH_TAC);\r
 415  (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);\r
 416  (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`);\r
 417  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);\r
 418  (REWRITE_TAC[Geomdetail.CARD3]);\r
 419  (ASM_ARITH_TAC);\r
 420 \r
 421  (UNDISCH_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`);\r
 422  (REWRITE_TAC[ASSUME `x = e':real^3->bool`; ASSUME `y = e'':real^3->bool`]);\r
 423  (ASM_REWRITE_TAC[]);\r
 424  (REWRITE_TAC[SUM_CLAUSES]);\r
 425  (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC);\r
 426  (NEW_GOAL `F`);\r
 427  (UNDISCH_TAC `~(CARD (critical_edgeX V (mcell 4 V ul')) = 2)`);\r
 428  (REWRITE_TAC[ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]);\r
 429  (REWRITE_TAC[Geomdetail.CARD_SET2]);\r
 430  (EXPAND_TAC "y");\r
 431  (STRIP_TAC);\r
 432  (NEW_GOAL `{v0, v1,v2,v3:real^3} = {}`);\r
 433  (MATCH_MP_TAC (SET_RULE `!s:real^3->bool. x = s DIFF x ==> s = {}`));\r
 434  (ASM_MESON_TAC[]);\r
 435  (UP_ASM_TAC THEN SET_TAC[]);\r
 436  (ASM_MESON_TAC[]);\r
 437 \r
 438  (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC);\r
 439  (NEW_GOAL `?x y. critical_edgeX V (mcell 4 V ul') = {x, y} /\ ~(x = y)`);\r
 440  (MATCH_MP_TAC Rogers.CARD_2_IMP_DOUBLE);\r
 441  (ASM_REWRITE_TAC[FINITE_critical_edgeX]);\r
 442  (UP_ASM_TAC THEN STRIP_TAC);\r
 443  (REWRITE_TAC[SET_RULE `{x | x IN s} = s`; \r
 444                ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]);\r
 445  (ASM_SIMP_TAC[Collect_geom.SUM_DIS2]);\r
 446 \r
 447 \r
 448  (REWRITE_WITH \r
 449  `{e',e'',p,vl | {x, y} = {e', e''} /\\r
 450                 x = e' /\\r
 451                 p permutes 0..3 /\\r
 452                 vl = left_action_list p [v0; v1; v2; v3:real^3] /\\r
 453                 e' = {EL 0 vl, EL 1 vl} /\\r
 454                 e'' = {EL 2 vl, EL 3 vl}} =\r
 455  {e',e'',p,vl | e' = x /\ e'' = y /\\r
 456                 p permutes 0..3 /\\r
 457                 vl = left_action_list p [v0; v1; v2; v3] /\\r
 458                 x = {EL 0 vl, EL 1 vl} /\\r
 459                 y = {EL 2 vl, EL 3 vl}}`);\r
 460  (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);\r
 461  (STRIP_TAC);\r
 462 \r
 463  (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);\r
 464  (REPEAT STRIP_TAC);\r
 465  (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);\r
 466  (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);\r
 467  (REPEAT STRIP_TAC);\r
 468  (ASM_REWRITE_TAC[]);\r
 469  (ASM_REWRITE_TAC[]);\r
 470  (ASM_REWRITE_TAC[]);\r
 471  (ASM_REWRITE_TAC[]);\r
 472  (REWRITE_TAC[ASSUME `e':real^3->bool = x`; \r
 473    ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`]);\r
 474  (REWRITE_TAC[ASSUME `e'':real^3->bool = y`; \r
 475    ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`]);\r
 476  (ASM_REWRITE_TAC[]);\r
 477 \r
 478  (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);\r
 479  (REPEAT STRIP_TAC);\r
 480  (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);\r
 481  (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);\r
 482  (NEW_GOAL `y = e'':(real^3->bool)`);\r
 483  (ASM_SET_TAC[]);\r
 484  (REPEAT STRIP_TAC);\r
 485  (ASM_REWRITE_TAC[]);\r
 486  (ASM_REWRITE_TAC[]);\r
 487  (ASM_REWRITE_TAC[]);\r
 488  (ASM_REWRITE_TAC[]);\r
 489  (REWRITE_TAC[ASSUME `x:real^3->bool = e'`; \r
 490    ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);\r
 491  (REWRITE_TAC[ASSUME `y:real^3->bool = e''`; \r
 492    ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]);\r
 493  (ASM_REWRITE_TAC[]);\r
 494 \r
 495 \r
 496  (REWRITE_WITH \r
 497  `{e',e'',p,vl | {x, y} = {e', e''} /\\r
 498                 y = e' /\\r
 499                 p permutes 0..3 /\\r
 500                 vl = left_action_list p [v0; v1; v2; v3:real^3] /\\r
 501                 e' = {EL 0 vl, EL 1 vl} /\\r
 502                 e'' = {EL 2 vl, EL 3 vl}} =\r
 503  {e',e'',p,vl | e' = y /\ e'' = x /\\r
 504                 p permutes 0..3 /\\r
 505                 vl = left_action_list p [v0; v1; v2; v3] /\\r
 506                 y = {EL 0 vl, EL 1 vl} /\\r
 507                 x = {EL 2 vl, EL 3 vl}}`);\r
 508  (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);\r
 509  (STRIP_TAC);\r
 510 \r
 511  (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);\r
 512  (REPEAT STRIP_TAC);\r
 513  (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);\r
 514  (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);\r
 515  (REPEAT STRIP_TAC);\r
 516 \r
 517  (REWRITE_TAC[ASSUME `e' = y:real^3->bool`; ASSUME `e'' = x:real^3->bool`]);\r
 518  (SET_TAC[]);\r
 519  (ASM_REWRITE_TAC[]);\r
 520  (ASM_REWRITE_TAC[]);\r
 521  (ASM_REWRITE_TAC[]);\r
 522  (REWRITE_TAC[ASSUME `e':real^3->bool = y`; \r
 523    ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`]);\r
 524  (REWRITE_TAC[ASSUME `e'':real^3->bool = x`; \r
 525    ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`]);\r
 526  (ASM_REWRITE_TAC[]);\r
 527 \r
 528  (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);\r
 529  (REPEAT STRIP_TAC);\r
 530  (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);\r
 531  (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);\r
 532  (NEW_GOAL `x = e'':(real^3->bool)`);\r
 533  (ASM_SET_TAC[]);\r
 534  (REPEAT STRIP_TAC);\r
 535  (ASM_REWRITE_TAC[]);\r
 536  (ASM_REWRITE_TAC[]);\r
 537  (ASM_REWRITE_TAC[]);\r
 538  (ASM_REWRITE_TAC[]);\r
 539  (REWRITE_TAC[ASSUME `y:real^3->bool = e'`; \r
 540    ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);\r
 541  (REWRITE_TAC[ASSUME `x:real^3->bool = e''`; \r
 542    ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]);\r
 543  (ASM_REWRITE_TAC[]);\r
 544 \r
 545  (ABBREV_TAC `S1 = {e',e'',p,vl | e' = x /\\r
 546                 e'' = y /\\r
 547                 p permutes 0..3 /\\r
 548                 vl = left_action_list p [v0; v1; v2; v3:real^3] /\\r
 549                 x = {EL 0 vl, EL 1 vl} /\\r
 550                 y = {EL 2 vl, EL 3 vl}}`);\r
 551  (ABBREV_TAC `S2 =  {e',e'',p,vl | e' = y /\\r
 552                 e'' = x /\\r
 553                 p permutes 0..3 /\\r
 554                 vl = left_action_list p [v0; v1; v2; v3:real^3] /\\r
 555                 y = {EL 0 vl, EL 1 vl} /\\r
 556                 x = {EL 2 vl, EL 3 vl}}`);\r
 557  (REWRITE_WITH\r
 558   `sum (S2:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool)   \r
 559           (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -\r
 560                    bump (hl [EL 2 vl; EL 3 vl])) / &4) =  \r
 561    sum S2 (\(e',e'',p,vl). -- ((bump (hl [EL 2 vl; EL 3 vl]) -\r
 562                    bump (hl [EL 0 vl; EL 1 vl])) / &4))`);\r
 563  (ONCE_REWRITE_TAC[REAL_ARITH `(bump (hl [EL 0 vl; EL 1 vl]) -\r
 564                    bump (hl [EL 2 vl; EL 3 vl])) /\r
 565                   &4 = -- ((bump (hl [EL 2 vl; EL 3 vl]) -\r
 566                       bump (hl [EL 0 vl; EL 1 vl])) /\r
 567                      &4)`]);\r
 568  (ASM_REWRITE_TAC[]);\r
 569  (ONCE_REWRITE_TAC[SUM_NEG]);\r
 570  (ABBREV_TAC `f =  (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). \r
 571  ((bump (hl [EL 2 vl; EL 3 vl]) - bump (hl [EL 0 vl; EL 1 vl])) / &4))`);\r
 572  (REWRITE_WITH \r
 573 `(\(e',e'',p,vl). \r
 574    --((bump (hl [EL 2 vl; EL 3 vl]) -bump (hl [EL 0 vl; EL 1 vl])) / &4)) \r
 575   = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). \r
 576    -- f (e',e'',p,vl))`);\r
 577  (EXPAND_TAC "f");\r
 578  (REWRITE_TAC[BETA_THM]);\r
 579 \r
 580  (REWRITE_WITH \r
 581 `sum (S2:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool) (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list).\r
 582  -- f (e',e'',p,vl)) =\r
 583 sum S2 (\x. -- f x)`);\r
 584  (AP_TERM_TAC);\r
 585  (REWRITE_TAC[FUN_EQ_THM]);\r
 586  (EXPAND_TAC "f");\r
 587  (REWRITE_TAC[BETA_THM]);\r
 588  (REPEAT STRIP_TAC);\r
 589 \r
 590  (ABBREV_TAC `e' = FST (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`);\r
 591  (ABBREV_TAC `e'' = FST (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`);\r
 592  (ABBREV_TAC `p = FST (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);\r
 593  (ABBREV_TAC `vl = SND (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);\r
 594 \r
 595  (REWRITE_WITH `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = \r
 596   (e',e'',p, vl)`);\r
 597  (EXPAND_TAC "e'" THEN EXPAND_TAC "e''" THEN EXPAND_TAC "p" THEN EXPAND_TAC "vl");\r
 598  (REWRITE_TAC[PAIR]);\r
 599  (REWRITE_TAC[SUM_NEG]);\r
 600  (REWRITE_TAC[REAL_ARITH `a + -- b = &0 <=> a = b`]);\r
 601 \r
 602 (* --------------------------------------------------------------------------- *)\r
 603 (* Begin new part *)\r
 604 \r
 605  (EXPAND_TAC "f");\r
 606  (ABBREV_TAC \r
 607 `g = (\x. let (e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list) = x \r
 608           in \r
 609            (e'', e', (\i. \r
 610                           if p i = 0 then 2 else\r
 611                           if p i = 1 then 3 else\r
 612                           if p i = 2 then 0 else\r
 613                           if p i = 3 then 1 else i), \r
 614            [EL 2 vl;EL 3 vl;EL 0 vl;EL 1 vl]))`);\r
 615  (REWRITE_WITH \r
 616 `S1 = IMAGE    \r
 617  (g:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->(real^3->bool)#\r
 618    (real^3->bool)#(num->num)#(real^3)list) S2 /\  \r
 619  (\(e',e'',p,vl). (bump (hl [EL 2 vl; EL 3 vl]) -\r
 620                    bump (hl [EL 0 vl; EL 1 vl])) / &4) =  \r
 621  (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -\r
 622                    bump (hl [EL 2 vl; EL 3 vl])) / &4) o g `);\r
 623 \r
 624 (* ======================================================================= *)\r
 625 \r
 626  (REPEAT STRIP_TAC);\r
 627   (* New goal 1: to prove S1 = IMAGE g S2 *)\r
 628  \r
 629  (EXPAND_TAC "S1" THEN EXPAND_TAC "S2");\r
 630  (REWRITE_TAC[IMAGE]);\r
 631  (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN ONCE_REWRITE_TAC[IN] THEN  \r
 632    REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
 633  (EXISTS_TAC \r
 634    `(e'':real^3->bool,\r
 635      e':real^3->bool,\r
 636      (\i. if p i = 0\r
 637              then 2\r
 638              else if p i = 1\r
 639                   then 3\r
 640                   else if p i = 2 then 0 else if p i = 3 then 1 else i),\r
 641      [EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl])`);\r
 642  (REPEAT STRIP_TAC);\r
 643  (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`);\r
 644  (ABBREV_TAC `p' =  (\i. if p i = 0\r
 645              then 2\r
 646              else if p i = 1\r
 647                   then 3\r
 648                   else if p i = 2 then 0 else if p i = 3 then 1 else i)`);\r
 649  (EXISTS_TAC `p':num->num`);\r
 650  (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`);\r
 651  (REWRITE_WITH \r
 652 `EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 2 (vl:(real^3)list) /\ \r
 653  EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 3 vl /\\r
 654  EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 0 vl /\\r
 655  EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 1 vl`);\r
 656  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
 657  (REWRITE_TAC[ASSUME `e'' = y:real^3->bool`; ASSUME `e' = x:real^3->bool`;\r
 658    ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`; \r
 659    ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`;left_action_list; \r
 660    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
 661 \r
 662  (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);\r
 663  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
 664  (COND_CASES_TAC);\r
 665  (REFL_TAC);\r
 666  (NEW_GOAL `F`);\r
 667  (ASM_ARITH_TAC);\r
 668  (ASM_MESON_TAC[]);\r
 669 \r
 670  (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);\r
 671  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
 672  (COND_CASES_TAC);\r
 673  (NEW_GOAL `F`);\r
 674  (ASM_ARITH_TAC);\r
 675  (ASM_MESON_TAC[]);\r
 676  (COND_CASES_TAC);\r
 677  (REFL_TAC);\r
 678  (NEW_GOAL `F`);\r
 679  (ASM_ARITH_TAC);\r
 680  (ASM_MESON_TAC[]);\r
 681 \r
 682  (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);\r
 683  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
 684  (COND_CASES_TAC);\r
 685  (NEW_GOAL `F`);\r
 686  (ASM_ARITH_TAC);\r
 687  (ASM_MESON_TAC[]);\r
 688  (COND_CASES_TAC);\r
 689  (NEW_GOAL `F`);\r
 690  (ASM_ARITH_TAC);\r
 691  (ASM_MESON_TAC[]);\r
 692  (COND_CASES_TAC);\r
 693  (REFL_TAC);\r
 694  (NEW_GOAL `F`);\r
 695  (ASM_ARITH_TAC);\r
 696  (ASM_MESON_TAC[]);\r
 697 \r
 698  (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);\r
 699  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
 700  (COND_CASES_TAC);\r
 701  (NEW_GOAL `F`);\r
 702  (ASM_ARITH_TAC);\r
 703  (ASM_MESON_TAC[]);\r
 704  (COND_CASES_TAC);\r
 705  (NEW_GOAL `F`);\r
 706  (ASM_ARITH_TAC);\r
 707  (ASM_MESON_TAC[]);\r
 708  (COND_CASES_TAC);\r
 709  (NEW_GOAL `F`);\r
 710  (ASM_ARITH_TAC);\r
 711  (ASM_MESON_TAC[]);\r
 712  (COND_CASES_TAC);\r
 713  (REFL_TAC);\r
 714  (NEW_GOAL `F`);\r
 715  (ASM_ARITH_TAC);\r
 716  (ASM_MESON_TAC[]);\r
 717 \r
 718  (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);\r
 719  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
 720  (COND_CASES_TAC);\r
 721  (NEW_GOAL `F`);\r
 722  (ASM_ARITH_TAC);\r
 723  (ASM_MESON_TAC[]);\r
 724  (COND_CASES_TAC);\r
 725  (NEW_GOAL `F`);\r
 726  (ASM_ARITH_TAC);\r
 727  (ASM_MESON_TAC[]);\r
 728  (COND_CASES_TAC);\r
 729  (NEW_GOAL `F`);\r
 730  (ASM_ARITH_TAC);\r
 731  (ASM_MESON_TAC[]);\r
 732  (COND_CASES_TAC);\r
 733  (NEW_GOAL `F`);\r
 734  (ASM_ARITH_TAC);\r
 735  (ASM_MESON_TAC[]);\r
 736  (REFL_TAC);\r
 737 \r
 738  (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);\r
 739  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
 740  (REPEAT STRIP_TAC);\r
 741  (ABBREV_TAC `s = (p:num->num) u`);\r
 742  (NEW_GOAL `(p:num->num) s = s`);\r
 743  (FIRST_ASSUM MATCH_MP_TAC);\r
 744  (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);\r
 745  (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);\r
 746  (ASM_REWRITE_TAC[]);\r
 747  (UP_ASM_TAC THEN STRIP_TAC);\r
 748  (NEW_GOAL `s = x'':num`);\r
 749  (FIRST_ASSUM MATCH_MP_TAC);\r
 750  (ASM_REWRITE_TAC[]);\r
 751  (NEW_GOAL `u = x'':num`);\r
 752  (FIRST_ASSUM MATCH_MP_TAC);\r
 753  (ASM_REWRITE_TAC[]);\r
 754  (ASM_REWRITE_TAC[]);\r
 755 \r
 756 \r
 757 \r
 758  (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);\r
 759  (REPEAT STRIP_TAC);\r
 760  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
 761  (NEW_GOAL `(p':num->num) u = 2`);\r
 762  (FIRST_ASSUM MATCH_MP_TAC);\r
 763  (ASM_REWRITE_TAC[]);\r
 764  (NEW_GOAL `F`);\r
 765  (ASM_ARITH_TAC);\r
 766  (ASM_MESON_TAC[]);\r
 767  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
 768  (NEW_GOAL `(p':num->num) u = 3`);\r
 769  (FIRST_ASSUM MATCH_MP_TAC);\r
 770  (ASM_REWRITE_TAC[]);\r
 771  (NEW_GOAL `F`);\r
 772  (ASM_ARITH_TAC);\r
 773  (ASM_MESON_TAC[]);\r
 774  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
 775  (NEW_GOAL `(p':num->num) u = 1`);\r
 776  (FIRST_ASSUM MATCH_MP_TAC);\r
 777  (ASM_REWRITE_TAC[]);\r
 778  (NEW_GOAL `F`);\r
 779  (ASM_ARITH_TAC);\r
 780  (ASM_MESON_TAC[]);\r
 781  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
 782  (NEW_GOAL `(p':num->num) u = u`);\r
 783  (FIRST_ASSUM MATCH_MP_TAC);\r
 784  (ASM_REWRITE_TAC[]);\r
 785  (NEW_GOAL `(p:num->num) u = u`);\r
 786  (FIRST_ASSUM MATCH_MP_TAC);\r
 787  (ASM_REWRITE_TAC[]);\r
 788  (NEW_GOAL `F`);\r
 789  (ASM_ARITH_TAC);\r
 790  (ASM_MESON_TAC[]);\r
 791  (ASM_ARITH_TAC);\r
 792 \r
 793  (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);\r
 794  (REPEAT STRIP_TAC);\r
 795  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
 796  (NEW_GOAL `(p':num->num) u = 2`);\r
 797  (FIRST_ASSUM MATCH_MP_TAC);\r
 798  (ASM_REWRITE_TAC[]);\r
 799  (NEW_GOAL `F`);\r
 800  (ASM_ARITH_TAC);\r
 801  (ASM_MESON_TAC[]);\r
 802  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
 803  (NEW_GOAL `(p':num->num) u = 3`);\r
 804  (FIRST_ASSUM MATCH_MP_TAC);\r
 805  (ASM_REWRITE_TAC[]);\r
 806  (NEW_GOAL `F`);\r
 807  (ASM_ARITH_TAC);\r
 808  (ASM_MESON_TAC[]);\r
 809  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
 810  (NEW_GOAL `(p':num->num) u = 0`);\r
 811  (FIRST_ASSUM MATCH_MP_TAC);\r
 812  (ASM_REWRITE_TAC[]);\r
 813  (NEW_GOAL `F`);\r
 814  (ASM_ARITH_TAC);\r
 815  (ASM_MESON_TAC[]);\r
 816  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
 817  (NEW_GOAL `(p':num->num) u = u`);\r
 818  (FIRST_ASSUM MATCH_MP_TAC);\r
 819  (ASM_REWRITE_TAC[]);\r
 820  (NEW_GOAL `(p:num->num) u = u`);\r
 821  (FIRST_ASSUM MATCH_MP_TAC);\r
 822  (ASM_REWRITE_TAC[]);\r
 823  (NEW_GOAL `F`);\r
 824  (ASM_ARITH_TAC);\r
 825  (ASM_MESON_TAC[]);\r
 826  (ASM_ARITH_TAC);\r
 827 \r
 828  (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);\r
 829  (REPEAT STRIP_TAC);\r
 830  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
 831  (NEW_GOAL `(p':num->num) u = 3`);\r
 832  (FIRST_ASSUM MATCH_MP_TAC);\r
 833  (ASM_REWRITE_TAC[]);\r
 834  (NEW_GOAL `F`);\r
 835  (ASM_ARITH_TAC);\r
 836  (ASM_MESON_TAC[]);\r
 837  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
 838  (NEW_GOAL `(p':num->num) u = 0`);\r
 839  (FIRST_ASSUM MATCH_MP_TAC);\r
 840  (ASM_REWRITE_TAC[]);\r
 841  (NEW_GOAL `F`);\r
 842  (ASM_ARITH_TAC);\r
 843  (ASM_MESON_TAC[]);\r
 844  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
 845  (NEW_GOAL `(p':num->num) u = 1`);\r
 846  (FIRST_ASSUM MATCH_MP_TAC);\r
 847  (ASM_REWRITE_TAC[]);\r
 848  (NEW_GOAL `F`);\r
 849  (ASM_ARITH_TAC);\r
 850  (ASM_MESON_TAC[]);\r
 851  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
 852  (NEW_GOAL `(p':num->num) u = u`);\r
 853  (FIRST_ASSUM MATCH_MP_TAC);\r
 854  (ASM_REWRITE_TAC[]);\r
 855  (NEW_GOAL `(p:num->num) u = u`);\r
 856  (FIRST_ASSUM MATCH_MP_TAC);\r
 857  (ASM_REWRITE_TAC[]);\r
 858  (NEW_GOAL `F`);\r
 859  (ASM_ARITH_TAC);\r
 860  (ASM_MESON_TAC[]);\r
 861  (ASM_ARITH_TAC);\r
 862 \r
 863  (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);\r
 864  (REPEAT STRIP_TAC);\r
 865  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
 866  (NEW_GOAL `(p':num->num) u = 2`);\r
 867  (FIRST_ASSUM MATCH_MP_TAC);\r
 868  (ASM_REWRITE_TAC[]);\r
 869  (NEW_GOAL `F`);\r
 870  (ASM_ARITH_TAC);\r
 871  (ASM_MESON_TAC[]);\r
 872  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
 873  (NEW_GOAL `(p':num->num) u = 0`);\r
 874  (FIRST_ASSUM MATCH_MP_TAC);\r
 875  (ASM_REWRITE_TAC[]);\r
 876  (NEW_GOAL `F`);\r
 877  (ASM_ARITH_TAC);\r
 878  (ASM_MESON_TAC[]);\r
 879  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
 880  (NEW_GOAL `(p':num->num) u = 1`);\r
 881  (FIRST_ASSUM MATCH_MP_TAC);\r
 882  (ASM_REWRITE_TAC[]);\r
 883  (NEW_GOAL `F`);\r
 884  (ASM_ARITH_TAC);\r
 885  (ASM_MESON_TAC[]);\r
 886  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
 887  (NEW_GOAL `(p':num->num) u = u`);\r
 888  (FIRST_ASSUM MATCH_MP_TAC);\r
 889  (ASM_REWRITE_TAC[]);\r
 890  (NEW_GOAL `(p:num->num) u = u`);\r
 891  (FIRST_ASSUM MATCH_MP_TAC);\r
 892  (ASM_REWRITE_TAC[]);\r
 893  (NEW_GOAL `F`);\r
 894  (ASM_ARITH_TAC);\r
 895  (ASM_MESON_TAC[]);\r
 896  (ASM_ARITH_TAC);\r
 897 \r
 898  (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);\r
 899  (REPEAT STRIP_TAC);\r
 900  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
 901  (NEW_GOAL `(p':num->num) u = 2`);\r
 902  (FIRST_ASSUM MATCH_MP_TAC);\r
 903  (ASM_REWRITE_TAC[]);\r
 904  (NEW_GOAL `F`);\r
 905  (ASM_ARITH_TAC);\r
 906  (ASM_MESON_TAC[]);\r
 907  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
 908  (NEW_GOAL `(p':num->num) u = 3`);\r
 909  (FIRST_ASSUM MATCH_MP_TAC);\r
 910  (ASM_REWRITE_TAC[]);\r
 911  (NEW_GOAL `F`);\r
 912  (ASM_ARITH_TAC);\r
 913  (ASM_MESON_TAC[]);\r
 914  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
 915  (NEW_GOAL `(p':num->num) u = 0`);\r
 916  (FIRST_ASSUM MATCH_MP_TAC);\r
 917  (ASM_REWRITE_TAC[]);\r
 918  (NEW_GOAL `F`);\r
 919  (ASM_ARITH_TAC);\r
 920  (ASM_MESON_TAC[]);\r
 921  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
 922  (NEW_GOAL `(p':num->num) u = 1`);\r
 923  (FIRST_ASSUM MATCH_MP_TAC);\r
 924  (ASM_REWRITE_TAC[]);\r
 925  (NEW_GOAL `F`);\r
 926  (ASM_ARITH_TAC);\r
 927  (ASM_MESON_TAC[]);\r
 928  (ASM_ARITH_TAC);\r
 929 \r
 930 (* ------------------------------------------------------------------------- *)\r
 931 (* begin to prove that p' permutes 0..3 *)\r
 932 \r
 933 \r
 934  (NEW_GOAL `p' permutes 0..3`);\r
 935  (REWRITE_TAC[permutes]);\r
 936  (REPEAT STRIP_TAC);\r
 937  (NEW_GOAL `x'' > 3`);\r
 938  (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);\r
 939  (EXPAND_TAC "p'");\r
 940  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC);\r
 941  (NEW_GOAL `(p:num->num) x'' = x''`);\r
 942  (ASM_SIMP_TAC[]);\r
 943  (COND_CASES_TAC);\r
 944  (ASM_ARITH_TAC);\r
 945  (COND_CASES_TAC);\r
 946  (ASM_ARITH_TAC);\r
 947  (COND_CASES_TAC);\r
 948  (ASM_ARITH_TAC);\r
 949  (COND_CASES_TAC);\r
 950  (ASM_ARITH_TAC);\r
 951  (REFL_TAC);\r
 952 \r
 953  (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC);\r
 954 \r
 955  (ASM_CASES_TAC `y' = 0`);\r
 956  (NEW_GOAL `?z. (p:num->num) z = 2`);\r
 957  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
 958  (UP_ASM_TAC THEN STRIP_TAC);\r
 959  (EXISTS_TAC `z:num`);\r
 960  (ASM_REWRITE_TAC[]);\r
 961  (REPEAT STRIP_TAC);\r
 962  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
 963  (NEW_GOAL `(p:num->num) y'' = 2`);\r
 964  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
 965  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
 966  (REPEAT STRIP_TAC);\r
 967  (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`);\r
 968  (ASM_REWRITE_TAC[]);\r
 969  (UP_ASM_TAC THEN STRIP_TAC);\r
 970  (REWRITE_WITH `y'' = s:num`);\r
 971  (FIRST_ASSUM MATCH_MP_TAC);\r
 972  (ASM_REWRITE_TAC[]);\r
 973  (REWRITE_WITH `z = s:num`);\r
 974  (FIRST_ASSUM MATCH_MP_TAC);\r
 975  (ASM_REWRITE_TAC[]);\r
 976 \r
 977  (ASM_CASES_TAC `y' = 1`);\r
 978  (NEW_GOAL `?z. (p:num->num) z = 3`);\r
 979  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
 980  (UP_ASM_TAC THEN STRIP_TAC);\r
 981  (EXISTS_TAC `z:num`);\r
 982  (ASM_REWRITE_TAC[]);\r
 983  (REPEAT STRIP_TAC);\r
 984  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
 985  (NEW_GOAL `(p:num->num) y'' = 3`);\r
 986  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
 987  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
 988  (REPEAT STRIP_TAC);\r
 989  (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`);\r
 990  (ASM_REWRITE_TAC[]);\r
 991  (UP_ASM_TAC THEN STRIP_TAC);\r
 992  (REWRITE_WITH `y'' = s:num`);\r
 993  (FIRST_ASSUM MATCH_MP_TAC);\r
 994  (ASM_REWRITE_TAC[]);\r
 995  (REWRITE_WITH `z = s:num`);\r
 996  (FIRST_ASSUM MATCH_MP_TAC);\r
 997  (ASM_REWRITE_TAC[]);\r
 998 \r
 999  (ASM_CASES_TAC `y' = 2`);\r
1000  (NEW_GOAL `?z. (p:num->num) z = 0`);\r
1001  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1002  (UP_ASM_TAC THEN STRIP_TAC);\r
1003  (EXISTS_TAC `z:num`);\r
1004  (ASM_REWRITE_TAC[]);\r
1005  (REPEAT STRIP_TAC);\r
1006  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1007  (NEW_GOAL `(p:num->num) y'' = 0`);\r
1008  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1009  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1010  (REPEAT STRIP_TAC);\r
1011  (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`);\r
1012  (ASM_REWRITE_TAC[]);\r
1013  (UP_ASM_TAC THEN STRIP_TAC);\r
1014  (REWRITE_WITH `y'' = s:num`);\r
1015  (FIRST_ASSUM MATCH_MP_TAC);\r
1016  (ASM_REWRITE_TAC[]);\r
1017  (REWRITE_WITH `z = s:num`);\r
1018  (FIRST_ASSUM MATCH_MP_TAC);\r
1019  (ASM_REWRITE_TAC[]);\r
1020 \r
1021  (ASM_CASES_TAC `y' = 3`);\r
1022  (NEW_GOAL `?z. (p:num->num) z = 1`);\r
1023  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1024  (UP_ASM_TAC THEN STRIP_TAC);\r
1025  (EXISTS_TAC `z:num`);\r
1026  (ASM_REWRITE_TAC[]);\r
1027  (REPEAT STRIP_TAC);\r
1028  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1029  (NEW_GOAL `(p:num->num) y'' = 1`);\r
1030  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1031  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1032  (REPEAT STRIP_TAC);\r
1033  (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`);\r
1034  (ASM_REWRITE_TAC[]);\r
1035  (UP_ASM_TAC THEN STRIP_TAC);\r
1036  (REWRITE_WITH `y'' = s:num`);\r
1037  (FIRST_ASSUM MATCH_MP_TAC);\r
1038  (ASM_REWRITE_TAC[]);\r
1039  (REWRITE_WITH `z = s:num`);\r
1040  (FIRST_ASSUM MATCH_MP_TAC);\r
1041  (ASM_REWRITE_TAC[]);\r
1042 \r
1043 \r
1044 \r
1045  (NEW_GOAL `y' > 3`);\r
1046  (ASM_ARITH_TAC);\r
1047  (NEW_GOAL `?z. (p:num->num) z = y'`);\r
1048  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1049  (UP_ASM_TAC THEN STRIP_TAC);\r
1050  (EXISTS_TAC `z:num`);\r
1051  (ASM_REWRITE_TAC[]);\r
1052  (REPEAT STRIP_TAC);\r
1053  (NEW_GOAL `(p:num->num) z = z`);\r
1054  (FIRST_ASSUM MATCH_MP_TAC);\r
1055  (ASM_ARITH_TAC);\r
1056  (NEW_GOAL `(p':num->num) z = z`);\r
1057  (FIRST_ASSUM MATCH_MP_TAC);\r
1058  (ASM_ARITH_TAC);\r
1059  (ASM_ARITH_TAC);\r
1060 \r
1061  (NEW_GOAL `(p:num->num) z = z`);\r
1062  (FIRST_ASSUM MATCH_MP_TAC);\r
1063  (ASM_ARITH_TAC);\r
1064  (NEW_GOAL `(p':num->num) z = z`);\r
1065  (FIRST_ASSUM MATCH_MP_TAC);\r
1066  (ASM_ARITH_TAC);\r
1067  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1068  (REPEAT STRIP_TAC);\r
1069  (NEW_GOAL `(p:num->num) y'' > 3`);\r
1070  (FIRST_ASSUM MATCH_MP_TAC);\r
1071  (ASM_REWRITE_TAC[]);\r
1072 \r
1073  (NEW_GOAL `(p:num->num) y'' = y''`);\r
1074  (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`));\r
1075  (ASM_REWRITE_TAC[]);\r
1076  (NEW_GOAL `(p':num->num) y'' = y''`);\r
1077  (FIRST_ASSUM MATCH_MP_TAC);\r
1078  (ASM_REWRITE_TAC[]);\r
1079 \r
1080  (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`);\r
1081  (ASM_REWRITE_TAC[]);\r
1082  (UP_ASM_TAC THEN STRIP_TAC);\r
1083  (REWRITE_WITH `y'' = s:num`);\r
1084  (FIRST_ASSUM MATCH_MP_TAC);\r
1085  (ASM_MESON_TAC[]);\r
1086  (REWRITE_WITH `z = s:num`);\r
1087  (FIRST_ASSUM MATCH_MP_TAC);\r
1088  (ASM_MESON_TAC[]);\r
1089 \r
1090 \r
1091 (* finish proving that p' permutes 0..3 *)\r
1092 \r
1093  (REWRITE_TAC[ASSUME `p' permutes 0..3`]);\r
1094 \r
1095 (* --------------------------------------------------------------------- *)\r
1096 \r
1097  (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`);\r
1098  (ASM_REWRITE_TAC[left_action_list; \r
1099    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
1100  (REWRITE_WITH  `EL 2\r
1101  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
1102   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
1103  = EL (inverse p 2) [v0; v1; v2; v3:real^3]`);\r
1104  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
1105  (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`);\r
1106  (ABBREV_TAC `j = inverse (p:num->num) 2`);\r
1107  (NEW_GOAL `(p:num->num) j = 2`);\r
1108  (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`);\r
1109  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1110  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1111  (ASM_REWRITE_TAC[]);\r
1112  (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`);\r
1113  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1114  (EXPAND_TAC "p'");\r
1115  (COND_CASES_TAC);\r
1116  (NEW_GOAL `F`);\r
1117  (ASM_ARITH_TAC);\r
1118  (ASM_MESON_TAC[]);\r
1119  (COND_CASES_TAC);\r
1120  (NEW_GOAL `F`);\r
1121  (ASM_ARITH_TAC);\r
1122  (ASM_MESON_TAC[]);\r
1123  (COND_CASES_TAC);\r
1124  (REFL_TAC);\r
1125  (NEW_GOAL `F`);\r
1126  (ASM_MESON_TAC[]);\r
1127  (ASM_MESON_TAC[]);\r
1128 \r
1129 \r
1130 \r
1131  (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`);\r
1132  (ASM_REWRITE_TAC[left_action_list; \r
1133    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
1134  (REWRITE_WITH  `EL 3\r
1135  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
1136   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
1137  = EL (inverse p 3) [v0; v1; v2; v3:real^3]`);\r
1138  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
1139  (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`);\r
1140  (ABBREV_TAC `j = inverse (p:num->num) 3`);\r
1141  (NEW_GOAL `(p:num->num) j = 3`);\r
1142  (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`);\r
1143  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1144  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1145  (ASM_REWRITE_TAC[]);\r
1146  (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`);\r
1147  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1148  (EXPAND_TAC "p'");\r
1149 \r
1150 \r
1151  (COND_CASES_TAC);\r
1152  (NEW_GOAL `F`);\r
1153  (ASM_ARITH_TAC);\r
1154  (ASM_MESON_TAC[]);\r
1155  (COND_CASES_TAC);\r
1156  (NEW_GOAL `F`);\r
1157  (ASM_ARITH_TAC);\r
1158  (ASM_MESON_TAC[]);\r
1159  (COND_CASES_TAC);\r
1160  (NEW_GOAL `F`);\r
1161  (ASM_ARITH_TAC);\r
1162  (ASM_MESON_TAC[]);\r
1163  (COND_CASES_TAC);\r
1164  (REFL_TAC);\r
1165  (NEW_GOAL `F`);\r
1166  (ASM_MESON_TAC[]);\r
1167  (ASM_MESON_TAC[]);\r
1168 \r
1169  (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`);\r
1170  (ASM_REWRITE_TAC[left_action_list; \r
1171    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
1172  (REWRITE_WITH  `EL 0\r
1173  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
1174   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
1175  = EL (inverse p 0) [v0; v1; v2; v3:real^3]`);\r
1176  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
1177  (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`);\r
1178  (ABBREV_TAC `j = inverse (p:num->num) 0`);\r
1179  (NEW_GOAL `(p:num->num) j = 0`);\r
1180  (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`);\r
1181  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1182  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1183  (ASM_REWRITE_TAC[]);\r
1184  (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`);\r
1185  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1186  (EXPAND_TAC "p'");\r
1187  (COND_CASES_TAC);\r
1188  (REFL_TAC);\r
1189  (NEW_GOAL `F`);\r
1190  (ASM_ARITH_TAC);\r
1191  (ASM_MESON_TAC[]);\r
1192 \r
1193  (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`);\r
1194  (ASM_REWRITE_TAC[left_action_list; \r
1195    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
1196  (REWRITE_WITH  `EL 1\r
1197  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
1198   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
1199  = EL (inverse p 1) [v0; v1; v2; v3:real^3]`);\r
1200  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
1201  (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`);\r
1202  (ABBREV_TAC `j = inverse (p:num->num) 1`);\r
1203  (NEW_GOAL `(p:num->num) j = 1`);\r
1204  (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`);\r
1205  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1206  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1207  (ASM_REWRITE_TAC[]);\r
1208  (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`);\r
1209  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1210  (EXPAND_TAC "p'");\r
1211  (COND_CASES_TAC);\r
1212  (NEW_GOAL `F`);\r
1213  (ASM_ARITH_TAC);\r
1214  (ASM_MESON_TAC[]);\r
1215  (COND_CASES_TAC);\r
1216  (REFL_TAC);\r
1217  (NEW_GOAL `F`);\r
1218  (ASM_ARITH_TAC);\r
1219  (ASM_MESON_TAC[]);\r
1220 \r
1221 \r
1222 (* ======================================================================= *)\r
1223 \r
1224  (EXPAND_TAC "g");\r
1225  (LET_TAC);\r
1226  (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; \r
1227    ASSUME `x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list =\r
1228    e',e'',p,vl`]);\r
1229  (REPEAT STRIP_TAC);\r
1230  (REWRITE_TAC[ASSUME `e':real^3->bool = e''''`]);\r
1231  (REWRITE_TAC[ASSUME `e'':real^3->bool = e'''`]);\r
1232  (REWRITE_TAC[FUN_EQ_THM]);\r
1233 \r
1234  (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);\r
1235  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1236  (COND_CASES_TAC);\r
1237  (REFL_TAC);\r
1238  (NEW_GOAL `F`);\r
1239  (ASM_ARITH_TAC);\r
1240  (ASM_MESON_TAC[]);\r
1241 \r
1242  (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);\r
1243  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1244  (COND_CASES_TAC);\r
1245  (NEW_GOAL `F`);\r
1246  (ASM_ARITH_TAC);\r
1247  (ASM_MESON_TAC[]);\r
1248  (COND_CASES_TAC);\r
1249  (REFL_TAC);\r
1250  (NEW_GOAL `F`);\r
1251  (ASM_ARITH_TAC);\r
1252  (ASM_MESON_TAC[]);\r
1253 \r
1254  (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);\r
1255  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1256  (COND_CASES_TAC);\r
1257  (NEW_GOAL `F`);\r
1258  (ASM_ARITH_TAC);\r
1259  (ASM_MESON_TAC[]);\r
1260  (COND_CASES_TAC);\r
1261  (NEW_GOAL `F`);\r
1262  (ASM_ARITH_TAC);\r
1263  (ASM_MESON_TAC[]);\r
1264  (COND_CASES_TAC);\r
1265  (REFL_TAC);\r
1266  (NEW_GOAL `F`);\r
1267  (ASM_ARITH_TAC);\r
1268  (ASM_MESON_TAC[]);\r
1269 \r
1270  (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);\r
1271  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1272  (COND_CASES_TAC);\r
1273  (NEW_GOAL `F`);\r
1274  (ASM_ARITH_TAC);\r
1275  (ASM_MESON_TAC[]);\r
1276  (COND_CASES_TAC);\r
1277  (NEW_GOAL `F`);\r
1278  (ASM_ARITH_TAC);\r
1279  (ASM_MESON_TAC[]);\r
1280  (COND_CASES_TAC);\r
1281  (NEW_GOAL `F`);\r
1282  (ASM_ARITH_TAC);\r
1283  (ASM_MESON_TAC[]);\r
1284  (COND_CASES_TAC);\r
1285  (REFL_TAC);\r
1286  (NEW_GOAL `F`);\r
1287  (ASM_ARITH_TAC);\r
1288  (ASM_MESON_TAC[]);\r
1289 \r
1290  (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);\r
1291  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1292  (COND_CASES_TAC);\r
1293  (NEW_GOAL `F`);\r
1294  (ASM_ARITH_TAC);\r
1295  (ASM_MESON_TAC[]);\r
1296  (COND_CASES_TAC);\r
1297  (NEW_GOAL `F`);\r
1298  (ASM_ARITH_TAC);\r
1299  (ASM_MESON_TAC[]);\r
1300  (COND_CASES_TAC);\r
1301  (NEW_GOAL `F`);\r
1302  (ASM_ARITH_TAC);\r
1303  (ASM_MESON_TAC[]);\r
1304  (COND_CASES_TAC);\r
1305  (NEW_GOAL `F`);\r
1306  (ASM_ARITH_TAC);\r
1307  (ASM_MESON_TAC[]);\r
1308  (REFL_TAC);\r
1309 \r
1310  (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);\r
1311  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1312  (REPEAT STRIP_TAC);\r
1313  (ABBREV_TAC `s = (p:num->num) u`);\r
1314  (NEW_GOAL `(p:num->num) s = s`);\r
1315  (FIRST_ASSUM MATCH_MP_TAC);\r
1316  (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);\r
1317  (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);\r
1318  (ASM_REWRITE_TAC[]);\r
1319  (UP_ASM_TAC THEN STRIP_TAC);\r
1320  (NEW_GOAL `s = x'':num`);\r
1321  (FIRST_ASSUM MATCH_MP_TAC);\r
1322  (ASM_REWRITE_TAC[]);\r
1323  (NEW_GOAL `u = x'':num`);\r
1324  (FIRST_ASSUM MATCH_MP_TAC);\r
1325  (ASM_REWRITE_TAC[]);\r
1326  (ASM_REWRITE_TAC[]);\r
1327 \r
1328  (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);\r
1329  (REPEAT STRIP_TAC);\r
1330  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1331  (NEW_GOAL `(p':num->num) u = 2`);\r
1332  (FIRST_ASSUM MATCH_MP_TAC);\r
1333  (ASM_REWRITE_TAC[]);\r
1334  (NEW_GOAL `F`);\r
1335  (ASM_ARITH_TAC);\r
1336  (ASM_MESON_TAC[]);\r
1337  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1338  (NEW_GOAL `(p':num->num) u = 3`);\r
1339  (FIRST_ASSUM MATCH_MP_TAC);\r
1340  (ASM_REWRITE_TAC[]);\r
1341  (NEW_GOAL `F`);\r
1342  (ASM_ARITH_TAC);\r
1343  (ASM_MESON_TAC[]);\r
1344  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1345  (NEW_GOAL `(p':num->num) u = 1`);\r
1346  (FIRST_ASSUM MATCH_MP_TAC);\r
1347  (ASM_REWRITE_TAC[]);\r
1348  (NEW_GOAL `F`);\r
1349  (ASM_ARITH_TAC);\r
1350  (ASM_MESON_TAC[]);\r
1351  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1352  (NEW_GOAL `(p':num->num) u = u`);\r
1353  (FIRST_ASSUM MATCH_MP_TAC);\r
1354  (ASM_REWRITE_TAC[]);\r
1355  (NEW_GOAL `(p:num->num) u = u`);\r
1356  (FIRST_ASSUM MATCH_MP_TAC);\r
1357  (ASM_REWRITE_TAC[]);\r
1358  (NEW_GOAL `F`);\r
1359  (ASM_ARITH_TAC);\r
1360  (ASM_MESON_TAC[]);\r
1361  (ASM_ARITH_TAC);\r
1362 \r
1363  (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);\r
1364  (REPEAT STRIP_TAC);\r
1365  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1366  (NEW_GOAL `(p':num->num) u = 2`);\r
1367  (FIRST_ASSUM MATCH_MP_TAC);\r
1368  (ASM_REWRITE_TAC[]);\r
1369  (NEW_GOAL `F`);\r
1370  (ASM_ARITH_TAC);\r
1371  (ASM_MESON_TAC[]);\r
1372  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1373  (NEW_GOAL `(p':num->num) u = 3`);\r
1374  (FIRST_ASSUM MATCH_MP_TAC);\r
1375  (ASM_REWRITE_TAC[]);\r
1376  (NEW_GOAL `F`);\r
1377  (ASM_ARITH_TAC);\r
1378  (ASM_MESON_TAC[]);\r
1379  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1380  (NEW_GOAL `(p':num->num) u = 0`);\r
1381  (FIRST_ASSUM MATCH_MP_TAC);\r
1382  (ASM_REWRITE_TAC[]);\r
1383  (NEW_GOAL `F`);\r
1384  (ASM_ARITH_TAC);\r
1385  (ASM_MESON_TAC[]);\r
1386  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1387  (NEW_GOAL `(p':num->num) u = u`);\r
1388  (FIRST_ASSUM MATCH_MP_TAC);\r
1389  (ASM_REWRITE_TAC[]);\r
1390  (NEW_GOAL `(p:num->num) u = u`);\r
1391  (FIRST_ASSUM MATCH_MP_TAC);\r
1392  (ASM_REWRITE_TAC[]);\r
1393  (NEW_GOAL `F`);\r
1394  (ASM_ARITH_TAC);\r
1395  (ASM_MESON_TAC[]);\r
1396  (ASM_ARITH_TAC);\r
1397 \r
1398  (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);\r
1399  (REPEAT STRIP_TAC);\r
1400  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1401  (NEW_GOAL `(p':num->num) u = 3`);\r
1402  (FIRST_ASSUM MATCH_MP_TAC);\r
1403  (ASM_REWRITE_TAC[]);\r
1404  (NEW_GOAL `F`);\r
1405  (ASM_ARITH_TAC);\r
1406  (ASM_MESON_TAC[]);\r
1407  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1408  (NEW_GOAL `(p':num->num) u = 0`);\r
1409  (FIRST_ASSUM MATCH_MP_TAC);\r
1410  (ASM_REWRITE_TAC[]);\r
1411  (NEW_GOAL `F`);\r
1412  (ASM_ARITH_TAC);\r
1413  (ASM_MESON_TAC[]);\r
1414  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1415  (NEW_GOAL `(p':num->num) u = 1`);\r
1416  (FIRST_ASSUM MATCH_MP_TAC);\r
1417  (ASM_REWRITE_TAC[]);\r
1418  (NEW_GOAL `F`);\r
1419  (ASM_ARITH_TAC);\r
1420  (ASM_MESON_TAC[]);\r
1421  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1422  (NEW_GOAL `(p':num->num) u = u`);\r
1423  (FIRST_ASSUM MATCH_MP_TAC);\r
1424  (ASM_REWRITE_TAC[]);\r
1425  (NEW_GOAL `(p:num->num) u = u`);\r
1426  (FIRST_ASSUM MATCH_MP_TAC);\r
1427  (ASM_REWRITE_TAC[]);\r
1428  (NEW_GOAL `F`);\r
1429  (ASM_ARITH_TAC);\r
1430  (ASM_MESON_TAC[]);\r
1431  (ASM_ARITH_TAC);\r
1432 \r
1433  (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);\r
1434  (REPEAT STRIP_TAC);\r
1435  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1436  (NEW_GOAL `(p':num->num) u = 2`);\r
1437  (FIRST_ASSUM MATCH_MP_TAC);\r
1438  (ASM_REWRITE_TAC[]);\r
1439  (NEW_GOAL `F`);\r
1440  (ASM_ARITH_TAC);\r
1441  (ASM_MESON_TAC[]);\r
1442  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1443  (NEW_GOAL `(p':num->num) u = 0`);\r
1444  (FIRST_ASSUM MATCH_MP_TAC);\r
1445  (ASM_REWRITE_TAC[]);\r
1446  (NEW_GOAL `F`);\r
1447  (ASM_ARITH_TAC);\r
1448  (ASM_MESON_TAC[]);\r
1449  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1450  (NEW_GOAL `(p':num->num) u = 1`);\r
1451  (FIRST_ASSUM MATCH_MP_TAC);\r
1452  (ASM_REWRITE_TAC[]);\r
1453  (NEW_GOAL `F`);\r
1454  (ASM_ARITH_TAC);\r
1455  (ASM_MESON_TAC[]);\r
1456  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1457  (NEW_GOAL `(p':num->num) u = u`);\r
1458  (FIRST_ASSUM MATCH_MP_TAC);\r
1459  (ASM_REWRITE_TAC[]);\r
1460  (NEW_GOAL `(p:num->num) u = u`);\r
1461  (FIRST_ASSUM MATCH_MP_TAC);\r
1462  (ASM_REWRITE_TAC[]);\r
1463  (NEW_GOAL `F`);\r
1464  (ASM_ARITH_TAC);\r
1465  (ASM_MESON_TAC[]);\r
1466  (ASM_ARITH_TAC);\r
1467 \r
1468  (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);\r
1469  (REPEAT STRIP_TAC);\r
1470  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1471  (NEW_GOAL `(p':num->num) u = 2`);\r
1472  (FIRST_ASSUM MATCH_MP_TAC);\r
1473  (ASM_REWRITE_TAC[]);\r
1474  (NEW_GOAL `F`);\r
1475  (ASM_ARITH_TAC);\r
1476  (ASM_MESON_TAC[]);\r
1477  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1478  (NEW_GOAL `(p':num->num) u = 3`);\r
1479  (FIRST_ASSUM MATCH_MP_TAC);\r
1480  (ASM_REWRITE_TAC[]);\r
1481  (NEW_GOAL `F`);\r
1482  (ASM_ARITH_TAC);\r
1483  (ASM_MESON_TAC[]);\r
1484  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1485  (NEW_GOAL `(p':num->num) u = 0`);\r
1486  (FIRST_ASSUM MATCH_MP_TAC);\r
1487  (ASM_REWRITE_TAC[]);\r
1488  (NEW_GOAL `F`);\r
1489  (ASM_ARITH_TAC);\r
1490  (ASM_MESON_TAC[]);\r
1491  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1492  (NEW_GOAL `(p':num->num) u = 1`);\r
1493  (FIRST_ASSUM MATCH_MP_TAC);\r
1494  (ASM_REWRITE_TAC[]);\r
1495  (NEW_GOAL `F`);\r
1496  (ASM_ARITH_TAC);\r
1497  (ASM_MESON_TAC[]);\r
1498  (ASM_ARITH_TAC);\r
1499 \r
1500  (GEN_TAC);\r
1501  (COND_CASES_TAC);\r
1502  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1503  (COND_CASES_TAC);\r
1504  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1505  (COND_CASES_TAC);\r
1506  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1507  (COND_CASES_TAC);\r
1508  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1509  (NEW_GOAL `(p:num->num) x'' > 3`);\r
1510  (FIRST_ASSUM MATCH_MP_TAC);\r
1511  (ASM_ARITH_TAC);\r
1512  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1513 \r
1514 (* ------------------------------------------------------------------------- *)\r
1515 \r
1516  (EXPAND_TAC "vl'");\r
1517  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);  \r
1518  (REWRITE_TAC[ASSUME `vl = left_action_list p [v0; v1; v2; v3:real^3]`;                        left_action_list; TABLE_4; LENGTH;EL; HD;TL;\r
1519                ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);\r
1520 (* ======================================================================= *)\r
1521 \r
1522  (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`);\r
1523  (ABBREV_TAC `p' =  (\i. if p i = 0\r
1524              then 2\r
1525              else if p i = 1\r
1526                   then 3\r
1527                   else if p i = 2 then 0 else if p i = 3 then 1 else i)`);\r
1528  (EXISTS_TAC `p':num->num`);\r
1529  (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`);\r
1530  (REWRITE_WITH \r
1531   `{EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl], \r
1532     EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]} \r
1533    = {EL 0 vl, EL 1 (vl:(real^3)list)}`);\r
1534  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);  \r
1535  (REWRITE_WITH \r
1536   `{EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl], \r
1537     EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]} \r
1538    = {EL 2 vl, EL 3 (vl:(real^3)list)}`);\r
1539  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);  \r
1540  (REWRITE_TAC[ASSUME `e'' = x:real^3->bool`; ASSUME `e' = y:real^3->bool`;\r
1541    ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`; \r
1542    ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`;left_action_list; \r
1543    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
1544 \r
1545  (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);\r
1546  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1547  (COND_CASES_TAC);\r
1548  (REFL_TAC);\r
1549  (NEW_GOAL `F`);\r
1550  (ASM_ARITH_TAC);\r
1551  (ASM_MESON_TAC[]);\r
1552 \r
1553  (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);\r
1554  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1555  (COND_CASES_TAC);\r
1556  (NEW_GOAL `F`);\r
1557  (ASM_ARITH_TAC);\r
1558  (ASM_MESON_TAC[]);\r
1559  (COND_CASES_TAC);\r
1560  (REFL_TAC);\r
1561  (NEW_GOAL `F`);\r
1562  (ASM_ARITH_TAC);\r
1563  (ASM_MESON_TAC[]);\r
1564 \r
1565  (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);\r
1566  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1567  (COND_CASES_TAC);\r
1568  (NEW_GOAL `F`);\r
1569  (ASM_ARITH_TAC);\r
1570  (ASM_MESON_TAC[]);\r
1571  (COND_CASES_TAC);\r
1572  (NEW_GOAL `F`);\r
1573  (ASM_ARITH_TAC);\r
1574  (ASM_MESON_TAC[]);\r
1575  (COND_CASES_TAC);\r
1576  (REFL_TAC);\r
1577  (NEW_GOAL `F`);\r
1578  (ASM_ARITH_TAC);\r
1579  (ASM_MESON_TAC[]);\r
1580 \r
1581  (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);\r
1582  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1583  (COND_CASES_TAC);\r
1584  (NEW_GOAL `F`);\r
1585  (ASM_ARITH_TAC);\r
1586  (ASM_MESON_TAC[]);\r
1587  (COND_CASES_TAC);\r
1588  (NEW_GOAL `F`);\r
1589  (ASM_ARITH_TAC);\r
1590  (ASM_MESON_TAC[]);\r
1591  (COND_CASES_TAC);\r
1592  (NEW_GOAL `F`);\r
1593  (ASM_ARITH_TAC);\r
1594  (ASM_MESON_TAC[]);\r
1595  (COND_CASES_TAC);\r
1596  (REFL_TAC);\r
1597  (NEW_GOAL `F`);\r
1598  (ASM_ARITH_TAC);\r
1599  (ASM_MESON_TAC[]);\r
1600 \r
1601  (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);\r
1602  (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");\r
1603  (COND_CASES_TAC);\r
1604  (NEW_GOAL `F`);\r
1605  (ASM_ARITH_TAC);\r
1606  (ASM_MESON_TAC[]);\r
1607  (COND_CASES_TAC);\r
1608  (NEW_GOAL `F`);\r
1609  (ASM_ARITH_TAC);\r
1610  (ASM_MESON_TAC[]);\r
1611  (COND_CASES_TAC);\r
1612  (NEW_GOAL `F`);\r
1613  (ASM_ARITH_TAC);\r
1614  (ASM_MESON_TAC[]);\r
1615  (COND_CASES_TAC);\r
1616  (NEW_GOAL `F`);\r
1617  (ASM_ARITH_TAC);\r
1618  (ASM_MESON_TAC[]);\r
1619  (REFL_TAC);\r
1620 \r
1621  (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);\r
1622  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1623  (REPEAT STRIP_TAC);\r
1624  (ABBREV_TAC `s = (p:num->num) u`);\r
1625  (NEW_GOAL `(p:num->num) s = s`);\r
1626  (FIRST_ASSUM MATCH_MP_TAC);\r
1627  (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);\r
1628  (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);\r
1629  (ASM_REWRITE_TAC[]);\r
1630  (UP_ASM_TAC THEN STRIP_TAC);\r
1631  (NEW_GOAL `s = x''':num`);\r
1632  (FIRST_ASSUM MATCH_MP_TAC);\r
1633  (ASM_REWRITE_TAC[]);\r
1634  (NEW_GOAL `u = x''':num`);\r
1635  (FIRST_ASSUM MATCH_MP_TAC);\r
1636  (ASM_REWRITE_TAC[]);\r
1637  (ASM_REWRITE_TAC[]);\r
1638 \r
1639  (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);\r
1640  (REPEAT STRIP_TAC);\r
1641  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1642  (NEW_GOAL `(p':num->num) u = 2`);\r
1643  (FIRST_ASSUM MATCH_MP_TAC);\r
1644  (ASM_REWRITE_TAC[]);\r
1645  (NEW_GOAL `F`);\r
1646  (ASM_ARITH_TAC);\r
1647  (ASM_MESON_TAC[]);\r
1648  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1649  (NEW_GOAL `(p':num->num) u = 3`);\r
1650  (FIRST_ASSUM MATCH_MP_TAC);\r
1651  (ASM_REWRITE_TAC[]);\r
1652  (NEW_GOAL `F`);\r
1653  (ASM_ARITH_TAC);\r
1654  (ASM_MESON_TAC[]);\r
1655  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1656  (NEW_GOAL `(p':num->num) u = 1`);\r
1657  (FIRST_ASSUM MATCH_MP_TAC);\r
1658  (ASM_REWRITE_TAC[]);\r
1659  (NEW_GOAL `F`);\r
1660  (ASM_ARITH_TAC);\r
1661  (ASM_MESON_TAC[]);\r
1662  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1663  (NEW_GOAL `(p':num->num) u = u`);\r
1664  (FIRST_ASSUM MATCH_MP_TAC);\r
1665  (ASM_REWRITE_TAC[]);\r
1666  (NEW_GOAL `(p:num->num) u = u`);\r
1667  (FIRST_ASSUM MATCH_MP_TAC);\r
1668  (ASM_REWRITE_TAC[]);\r
1669  (NEW_GOAL `F`);\r
1670  (ASM_ARITH_TAC);\r
1671  (ASM_MESON_TAC[]);\r
1672  (ASM_ARITH_TAC);\r
1673 \r
1674  (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);\r
1675  (REPEAT STRIP_TAC);\r
1676  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1677  (NEW_GOAL `(p':num->num) u = 2`);\r
1678  (FIRST_ASSUM MATCH_MP_TAC);\r
1679  (ASM_REWRITE_TAC[]);\r
1680  (NEW_GOAL `F`);\r
1681  (ASM_ARITH_TAC);\r
1682  (ASM_MESON_TAC[]);\r
1683  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1684  (NEW_GOAL `(p':num->num) u = 3`);\r
1685  (FIRST_ASSUM MATCH_MP_TAC);\r
1686  (ASM_REWRITE_TAC[]);\r
1687  (NEW_GOAL `F`);\r
1688  (ASM_ARITH_TAC);\r
1689  (ASM_MESON_TAC[]);\r
1690  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1691  (NEW_GOAL `(p':num->num) u = 0`);\r
1692  (FIRST_ASSUM MATCH_MP_TAC);\r
1693  (ASM_REWRITE_TAC[]);\r
1694  (NEW_GOAL `F`);\r
1695  (ASM_ARITH_TAC);\r
1696  (ASM_MESON_TAC[]);\r
1697  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1698  (NEW_GOAL `(p':num->num) u = u`);\r
1699  (FIRST_ASSUM MATCH_MP_TAC);\r
1700  (ASM_REWRITE_TAC[]);\r
1701  (NEW_GOAL `(p:num->num) u = u`);\r
1702  (FIRST_ASSUM MATCH_MP_TAC);\r
1703  (ASM_REWRITE_TAC[]);\r
1704  (NEW_GOAL `F`);\r
1705  (ASM_ARITH_TAC);\r
1706  (ASM_MESON_TAC[]);\r
1707  (ASM_ARITH_TAC);\r
1708 \r
1709  (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);\r
1710  (REPEAT STRIP_TAC);\r
1711  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1712  (NEW_GOAL `(p':num->num) u = 3`);\r
1713  (FIRST_ASSUM MATCH_MP_TAC);\r
1714  (ASM_REWRITE_TAC[]);\r
1715  (NEW_GOAL `F`);\r
1716  (ASM_ARITH_TAC);\r
1717  (ASM_MESON_TAC[]);\r
1718  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1719  (NEW_GOAL `(p':num->num) u = 0`);\r
1720  (FIRST_ASSUM MATCH_MP_TAC);\r
1721  (ASM_REWRITE_TAC[]);\r
1722  (NEW_GOAL `F`);\r
1723  (ASM_ARITH_TAC);\r
1724  (ASM_MESON_TAC[]);\r
1725  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1726  (NEW_GOAL `(p':num->num) u = 1`);\r
1727  (FIRST_ASSUM MATCH_MP_TAC);\r
1728  (ASM_REWRITE_TAC[]);\r
1729  (NEW_GOAL `F`);\r
1730  (ASM_ARITH_TAC);\r
1731  (ASM_MESON_TAC[]);\r
1732  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1733  (NEW_GOAL `(p':num->num) u = u`);\r
1734  (FIRST_ASSUM MATCH_MP_TAC);\r
1735  (ASM_REWRITE_TAC[]);\r
1736  (NEW_GOAL `(p:num->num) u = u`);\r
1737  (FIRST_ASSUM MATCH_MP_TAC);\r
1738  (ASM_REWRITE_TAC[]);\r
1739  (NEW_GOAL `F`);\r
1740  (ASM_ARITH_TAC);\r
1741  (ASM_MESON_TAC[]);\r
1742  (ASM_ARITH_TAC);\r
1743 \r
1744  (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);\r
1745  (REPEAT STRIP_TAC);\r
1746  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1747  (NEW_GOAL `(p':num->num) u = 2`);\r
1748  (FIRST_ASSUM MATCH_MP_TAC);\r
1749  (ASM_REWRITE_TAC[]);\r
1750  (NEW_GOAL `F`);\r
1751  (ASM_ARITH_TAC);\r
1752  (ASM_MESON_TAC[]);\r
1753  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1754  (NEW_GOAL `(p':num->num) u = 0`);\r
1755  (FIRST_ASSUM MATCH_MP_TAC);\r
1756  (ASM_REWRITE_TAC[]);\r
1757  (NEW_GOAL `F`);\r
1758  (ASM_ARITH_TAC);\r
1759  (ASM_MESON_TAC[]);\r
1760  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1761  (NEW_GOAL `(p':num->num) u = 1`);\r
1762  (FIRST_ASSUM MATCH_MP_TAC);\r
1763  (ASM_REWRITE_TAC[]);\r
1764  (NEW_GOAL `F`);\r
1765  (ASM_ARITH_TAC);\r
1766  (ASM_MESON_TAC[]);\r
1767  (ASM_CASES_TAC `(p:num->num) u > 3`);\r
1768  (NEW_GOAL `(p':num->num) u = u`);\r
1769  (FIRST_ASSUM MATCH_MP_TAC);\r
1770  (ASM_REWRITE_TAC[]);\r
1771  (NEW_GOAL `(p:num->num) u = u`);\r
1772  (FIRST_ASSUM MATCH_MP_TAC);\r
1773  (ASM_REWRITE_TAC[]);\r
1774  (NEW_GOAL `F`);\r
1775  (ASM_ARITH_TAC);\r
1776  (ASM_MESON_TAC[]);\r
1777  (ASM_ARITH_TAC);\r
1778 \r
1779  (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);\r
1780  (REPEAT STRIP_TAC);\r
1781  (ASM_CASES_TAC `(p:num->num) u = 0`);\r
1782  (NEW_GOAL `(p':num->num) u = 2`);\r
1783  (FIRST_ASSUM MATCH_MP_TAC);\r
1784  (ASM_REWRITE_TAC[]);\r
1785  (NEW_GOAL `F`);\r
1786  (ASM_ARITH_TAC);\r
1787  (ASM_MESON_TAC[]);\r
1788  (ASM_CASES_TAC `(p:num->num) u = 1`);\r
1789  (NEW_GOAL `(p':num->num) u = 3`);\r
1790  (FIRST_ASSUM MATCH_MP_TAC);\r
1791  (ASM_REWRITE_TAC[]);\r
1792  (NEW_GOAL `F`);\r
1793  (ASM_ARITH_TAC);\r
1794  (ASM_MESON_TAC[]);\r
1795  (ASM_CASES_TAC `(p:num->num) u = 2`);\r
1796  (NEW_GOAL `(p':num->num) u = 0`);\r
1797  (FIRST_ASSUM MATCH_MP_TAC);\r
1798  (ASM_REWRITE_TAC[]);\r
1799  (NEW_GOAL `F`);\r
1800  (ASM_ARITH_TAC);\r
1801  (ASM_MESON_TAC[]);\r
1802  (ASM_CASES_TAC `(p:num->num) u = 3`);\r
1803  (NEW_GOAL `(p':num->num) u = 1`);\r
1804  (FIRST_ASSUM MATCH_MP_TAC);\r
1805  (ASM_REWRITE_TAC[]);\r
1806  (NEW_GOAL `F`);\r
1807  (ASM_ARITH_TAC);\r
1808  (ASM_MESON_TAC[]);\r
1809  (ASM_ARITH_TAC);\r
1810 \r
1811 (* ------------------------------------------------------------------------- *)\r
1812 (* begin to prove that p' permutes 0..3 *)\r
1813 \r
1814  (NEW_GOAL `p' permutes 0..3`);\r
1815  (REWRITE_TAC[permutes]);\r
1816  (REPEAT STRIP_TAC);\r
1817  (NEW_GOAL `x''' > 3`);\r
1818  (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);\r
1819  (EXPAND_TAC "p'");\r
1820  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC);\r
1821 \r
1822  (NEW_GOAL `(p:num->num) x''' = x'''`);\r
1823  (ASM_SIMP_TAC[]);\r
1824  (COND_CASES_TAC);\r
1825  (NEW_GOAL `F`);\r
1826  (ASM_ARITH_TAC);\r
1827  (ASM_MESON_TAC[]);\r
1828  (COND_CASES_TAC);\r
1829  (NEW_GOAL `F`);\r
1830  (ASM_ARITH_TAC);\r
1831  (ASM_MESON_TAC[]);\r
1832  (COND_CASES_TAC);\r
1833  (NEW_GOAL `F`);\r
1834  (ASM_ARITH_TAC);\r
1835  (ASM_MESON_TAC[]);\r
1836  (COND_CASES_TAC);\r
1837  (NEW_GOAL `F`);\r
1838  (ASM_ARITH_TAC);\r
1839  (ASM_MESON_TAC[]);\r
1840  (REFL_TAC);\r
1841 \r
1842  (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC);\r
1843 \r
1844  (ASM_CASES_TAC `y' = 0`);\r
1845  (NEW_GOAL `?z. (p:num->num) z = 2`);\r
1846  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1847  (UP_ASM_TAC THEN STRIP_TAC);\r
1848  (EXISTS_TAC `z:num`);\r
1849  (ASM_REWRITE_TAC[]);\r
1850  (REPEAT STRIP_TAC);\r
1851  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1852  (NEW_GOAL `(p:num->num) y'' = 2`);\r
1853  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1854  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1855  (REPEAT STRIP_TAC);\r
1856  (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`);\r
1857  (ASM_REWRITE_TAC[]);\r
1858  (UP_ASM_TAC THEN STRIP_TAC);\r
1859  (REWRITE_WITH `y'' = s:num`);\r
1860  (FIRST_ASSUM MATCH_MP_TAC);\r
1861  (ASM_REWRITE_TAC[]);\r
1862  (REWRITE_WITH `z = s:num`);\r
1863  (FIRST_ASSUM MATCH_MP_TAC);\r
1864  (ASM_REWRITE_TAC[]);\r
1865 \r
1866  (ASM_CASES_TAC `y' = 1`);\r
1867  (NEW_GOAL `?z. (p:num->num) z = 3`);\r
1868  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1869  (UP_ASM_TAC THEN STRIP_TAC);\r
1870  (EXISTS_TAC `z:num`);\r
1871  (ASM_REWRITE_TAC[]);\r
1872  (REPEAT STRIP_TAC);\r
1873  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1874  (NEW_GOAL `(p:num->num) y'' = 3`);\r
1875  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1876  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1877  (REPEAT STRIP_TAC);\r
1878  (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`);\r
1879  (ASM_REWRITE_TAC[]);\r
1880  (UP_ASM_TAC THEN STRIP_TAC);\r
1881  (REWRITE_WITH `y'' = s:num`);\r
1882  (FIRST_ASSUM MATCH_MP_TAC);\r
1883  (ASM_REWRITE_TAC[]);\r
1884  (REWRITE_WITH `z = s:num`);\r
1885  (FIRST_ASSUM MATCH_MP_TAC);\r
1886  (ASM_REWRITE_TAC[]);\r
1887 \r
1888  (ASM_CASES_TAC `y' = 2`);\r
1889  (NEW_GOAL `?z. (p:num->num) z = 0`);\r
1890  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1891  (UP_ASM_TAC THEN STRIP_TAC);\r
1892  (EXISTS_TAC `z:num`);\r
1893  (ASM_REWRITE_TAC[]);\r
1894  (REPEAT STRIP_TAC);\r
1895  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1896  (NEW_GOAL `(p:num->num) y'' = 0`);\r
1897  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1898  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1899  (REPEAT STRIP_TAC);\r
1900  (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`);\r
1901  (ASM_REWRITE_TAC[]);\r
1902  (UP_ASM_TAC THEN STRIP_TAC);\r
1903  (REWRITE_WITH `y'' = s:num`);\r
1904  (FIRST_ASSUM MATCH_MP_TAC);\r
1905  (ASM_REWRITE_TAC[]);\r
1906  (REWRITE_WITH `z = s:num`);\r
1907  (FIRST_ASSUM MATCH_MP_TAC);\r
1908  (ASM_REWRITE_TAC[]);\r
1909 \r
1910  (ASM_CASES_TAC `y' = 3`);\r
1911  (NEW_GOAL `?z. (p:num->num) z = 1`);\r
1912  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1913  (UP_ASM_TAC THEN STRIP_TAC);\r
1914  (EXISTS_TAC `z:num`);\r
1915  (ASM_REWRITE_TAC[]);\r
1916  (REPEAT STRIP_TAC);\r
1917  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1918  (NEW_GOAL `(p:num->num) y'' = 1`);\r
1919  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
1920  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1921  (REPEAT STRIP_TAC);\r
1922  (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`);\r
1923  (ASM_REWRITE_TAC[]);\r
1924  (UP_ASM_TAC THEN STRIP_TAC);\r
1925  (REWRITE_WITH `y'' = s:num`);\r
1926  (FIRST_ASSUM MATCH_MP_TAC);\r
1927  (ASM_REWRITE_TAC[]);\r
1928  (REWRITE_WITH `z = s:num`);\r
1929  (FIRST_ASSUM MATCH_MP_TAC);\r
1930  (ASM_REWRITE_TAC[]);\r
1931 \r
1932  (NEW_GOAL `y' > 3`);\r
1933  (ASM_ARITH_TAC);\r
1934  (NEW_GOAL `?z. (p:num->num) z = y'`);\r
1935  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);\r
1936  (UP_ASM_TAC THEN STRIP_TAC);\r
1937  (EXISTS_TAC `z:num`);\r
1938  (ASM_REWRITE_TAC[]);\r
1939  (REPEAT STRIP_TAC);\r
1940  (NEW_GOAL `(p:num->num) z = z`);\r
1941  (FIRST_ASSUM MATCH_MP_TAC);\r
1942  (ASM_ARITH_TAC);\r
1943  (NEW_GOAL `(p':num->num) z = z`);\r
1944  (FIRST_ASSUM MATCH_MP_TAC);\r
1945  (ASM_ARITH_TAC);\r
1946  (ASM_ARITH_TAC);\r
1947 \r
1948  (NEW_GOAL `(p:num->num) z = z`);\r
1949  (FIRST_ASSUM MATCH_MP_TAC);\r
1950  (ASM_ARITH_TAC);\r
1951  (NEW_GOAL `(p':num->num) z = z`);\r
1952  (FIRST_ASSUM MATCH_MP_TAC);\r
1953  (ASM_ARITH_TAC);\r
1954  (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
1955  (REPEAT STRIP_TAC);\r
1956  (NEW_GOAL `(p:num->num) y'' > 3`);\r
1957  (FIRST_ASSUM MATCH_MP_TAC);\r
1958  (ASM_REWRITE_TAC[]);\r
1959 \r
1960  (NEW_GOAL `(p:num->num) y'' = y''`);\r
1961  (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`));\r
1962  (ASM_REWRITE_TAC[]);\r
1963  (NEW_GOAL `(p':num->num) y'' = y''`);\r
1964  (FIRST_ASSUM MATCH_MP_TAC);\r
1965  (ASM_REWRITE_TAC[]);\r
1966 \r
1967  (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`);\r
1968  (ASM_REWRITE_TAC[]);\r
1969  (UP_ASM_TAC THEN STRIP_TAC);\r
1970  (REWRITE_WITH `y'' = s:num`);\r
1971  (FIRST_ASSUM MATCH_MP_TAC);\r
1972  (ASM_MESON_TAC[]);\r
1973  (REWRITE_WITH `z = s:num`);\r
1974  (FIRST_ASSUM MATCH_MP_TAC);\r
1975  (ASM_MESON_TAC[]);\r
1976 \r
1977 \r
1978 (* finish proving that p' permutes 0..3 *)\r
1979 \r
1980  (REWRITE_TAC[ASSUME `p' permutes 0..3`]);\r
1981 \r
1982 (* --------------------------------------------------------------------- *)\r
1983 \r
1984  (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`);\r
1985  (ASM_REWRITE_TAC[left_action_list; \r
1986    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
1987  (REWRITE_WITH  `EL 2\r
1988  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
1989   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
1990  = EL (inverse p 2) [v0; v1; v2; v3:real^3]`);\r
1991  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
1992  (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`);\r
1993  (ABBREV_TAC `j = inverse (p:num->num) 2`);\r
1994  (NEW_GOAL `(p:num->num) j = 2`);\r
1995  (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`);\r
1996  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1997  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
1998  (ASM_REWRITE_TAC[]);\r
1999  (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`);\r
2000  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
2001  (EXPAND_TAC "p'");\r
2002  (COND_CASES_TAC);\r
2003  (NEW_GOAL `F`);\r
2004  (ASM_ARITH_TAC);\r
2005  (ASM_MESON_TAC[]);\r
2006  (COND_CASES_TAC);\r
2007  (NEW_GOAL `F`);\r
2008  (ASM_ARITH_TAC);\r
2009  (ASM_MESON_TAC[]);\r
2010  (COND_CASES_TAC);\r
2011  (REFL_TAC);\r
2012  (NEW_GOAL `F`);\r
2013  (ASM_MESON_TAC[]);\r
2014  (ASM_MESON_TAC[]);\r
2015 \r
2016 \r
2017  (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`);\r
2018  (ASM_REWRITE_TAC[left_action_list; \r
2019    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
2020  (REWRITE_WITH  `EL 3\r
2021  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
2022   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
2023  = EL (inverse p 3) [v0; v1; v2; v3:real^3]`);\r
2024  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2025  (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`);\r
2026  (ABBREV_TAC `j = inverse (p:num->num) 3`);\r
2027  (NEW_GOAL `(p:num->num) j = 3`);\r
2028  (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`);\r
2029  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
2030  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
2031  (ASM_REWRITE_TAC[]);\r
2032  (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`);\r
2033  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
2034  (EXPAND_TAC "p'");\r
2035  (COND_CASES_TAC);\r
2036  (NEW_GOAL `F`);\r
2037  (ASM_ARITH_TAC);\r
2038  (ASM_MESON_TAC[]);\r
2039  (COND_CASES_TAC);\r
2040  (NEW_GOAL `F`);\r
2041  (ASM_ARITH_TAC);\r
2042  (ASM_MESON_TAC[]);\r
2043  (COND_CASES_TAC);\r
2044  (NEW_GOAL `F`);\r
2045  (ASM_ARITH_TAC);\r
2046  (ASM_MESON_TAC[]);\r
2047  (COND_CASES_TAC);\r
2048  (REFL_TAC);\r
2049  (NEW_GOAL `F`);\r
2050  (ASM_MESON_TAC[]);\r
2051  (ASM_MESON_TAC[]);\r
2052 \r
2053  (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`);\r
2054  (ASM_REWRITE_TAC[left_action_list; \r
2055    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
2056  (REWRITE_WITH  `EL 0\r
2057  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
2058   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
2059  = EL (inverse p 0) [v0; v1; v2; v3:real^3]`);\r
2060  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2061  (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`);\r
2062  (ABBREV_TAC `j = inverse (p:num->num) 0`);\r
2063  (NEW_GOAL `(p:num->num) j = 0`);\r
2064  (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`);\r
2065  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
2066  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
2067  (ASM_REWRITE_TAC[]);\r
2068  (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`);\r
2069  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
2070  (EXPAND_TAC "p'");\r
2071  (COND_CASES_TAC);\r
2072  (REFL_TAC);\r
2073  (NEW_GOAL `F`);\r
2074  (ASM_ARITH_TAC);\r
2075  (ASM_MESON_TAC[]);\r
2076 \r
2077 \r
2078  (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`);\r
2079  (ASM_REWRITE_TAC[left_action_list; \r
2080    LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);\r
2081  (REWRITE_WITH  `EL 1\r
2082  [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; \r
2083   EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] \r
2084  = EL (inverse p 1) [v0; v1; v2; v3:real^3]`);\r
2085  (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2086  (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`);\r
2087  (ABBREV_TAC `j = inverse (p:num->num) 1`);\r
2088  (NEW_GOAL `(p:num->num) j = 1`);\r
2089  (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`);\r
2090  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
2091  (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
2092  (ASM_REWRITE_TAC[]);\r
2093  (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`);\r
2094  (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);\r
2095  (EXPAND_TAC "p'");\r
2096  (COND_CASES_TAC);\r
2097  (NEW_GOAL `F`);\r
2098  (ASM_ARITH_TAC);\r
2099  (ASM_MESON_TAC[]);\r
2100  (COND_CASES_TAC);\r
2101  (REFL_TAC);\r
2102  (NEW_GOAL `F`);\r
2103  (ASM_ARITH_TAC);\r
2104  (ASM_MESON_TAC[]);\r
2105 \r
2106 \r
2107 (* ======================================================================= *)\r
2108 \r
2109  (ONCE_REWRITE_TAC[ASSUME  \r
2110    `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list \r
2111  = g (x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`]);\r
2112  (REWRITE_TAC[ASSUME\r
2113   `x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = e',e'',p,vl`]  \r
2114    THEN EXPAND_TAC "g");\r
2115  (LET_TAC);\r
2116  (REWRITE_TAC[PAIR_EQ]);\r
2117  (EXPAND_TAC "p'" THEN REWRITE_TAC[]);\r
2118  (ASM_REWRITE_TAC[]);\r
2119 \r
2120 (*  --------------------------------------------------- *)\r
2121 (* It is left to prove only 3 subgoals *)\r
2122 \r
2123  (EXPAND_TAC "g");\r
2124  (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);\r
2125  (REWRITE_TAC[FUN_EQ_THM]);\r
2126  (GEN_TAC);\r
2127  (NEW_GOAL `?e1 e2 p1 vl1. \r
2128    x' = (e1:real^3->bool,e2:real^3->bool,p1:num->num, vl1:(real^3)list)`);\r
2129  (EXISTS_TAC `FST  \r
2130   (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`);\r
2131  (EXISTS_TAC `FST (SND\r
2132   (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`);\r
2133  (EXISTS_TAC `FST (SND (SND  \r
2134   (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);\r
2135  (EXISTS_TAC `SND (SND (SND  \r
2136   (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);\r
2137  (REWRITE_TAC[PAIR]);\r
2138  (UP_ASM_TAC THEN STRIP_TAC);\r
2139  (ASM_REWRITE_TAC[]);\r
2140  (REWRITE_WITH \r
2141  `(\x. let e',e'',p,vl = x in\r
2142        e'', e', (\i. if p i = 0 then 2\r
2143                 else if p i = 1 then 3\r
2144                 else if p i = 2 then 0 \r
2145                 else if p i = 3 then 1 else i),\r
2146        [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl])\r
2147   = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). \r
2148       e'', e', (\i. if p i = 0 then 2\r
2149                 else if p i = 1 then 3\r
2150                 else if p i = 2 then 0 \r
2151                 else if p i = 3 then 1 else i),\r
2152        [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl])`);\r
2153  (REWRITE_TAC[FUN_EQ_THM]);\r
2154  (GEN_TAC);\r
2155  (LET_TAC);\r
2156  (REWRITE_TAC[BETA_THM]);\r
2157  (REWRITE_TAC[o_THM]);\r
2158  (REWRITE_WITH \r
2159  `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 2 (vl1:(real^3)list) /\\r
2160   EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 3 (vl1:(real^3)list) /\\r
2161   EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 0 (vl1:(real^3)list) /\\r
2162   EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 1 (vl1:(real^3)list)`);\r
2163  (REWRITE_TAC[EL;HD;TL; LENGTH; ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2164 \r
2165  (MATCH_MP_TAC SUM_IMAGE);\r
2166  (EXPAND_TAC "S1" THEN EXPAND_TAC "S2");\r
2167  (ONCE_REWRITE_TAC[IN]);\r
2168  (REWRITE_TAC[IN_ELIM_THM]);\r
2169  (EXPAND_TAC "g");\r
2170  (REPEAT STRIP_TAC);\r
2171 \r
2172  (NEW_GOAL `(let e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1 = x' in\r
2173        e2,\r
2174        e1,\r
2175        (\i. if p1 i = 0\r
2176             then 2\r
2177             else if p1 i = 1\r
2178                  then 3\r
2179                  else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i),\r
2180        [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1]) =\r
2181       (let f1,f2,p2,vl2 = y' in\r
2182        f2,\r
2183        f1,\r
2184        (\i. if p2 i = 0\r
2185             then 2\r
2186             else if p2 i = 1\r
2187                  then 3\r
2188                  else if p2 i = 2 then 0 else if p2 i = 3 then 1 else i),\r
2189        [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)])`);\r
2190  (ASM_REWRITE_TAC[ETA_AX]);\r
2191  (UP_ASM_TAC THEN DEL_TAC THEN REPEAT LET_TAC THEN REWRITE_TAC[PAIR_EQ] THEN \r
2192    REPEAT STRIP_TAC);\r
2193  (ASM_REWRITE_TAC[]);\r
2194  (ASM_REWRITE_TAC[]);\r
2195  (REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC);\r
2196  (ABBREV_TAC \r
2197   `q = (\i. if p1 i = 0\r
2198            then 2\r
2199            else if p1 i = 1\r
2200                 then 3\r
2201                 else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i)`);\r
2202 \r
2203  (NEW_GOAL `!u:num. p1 u = 0 ==> q u = 2`);\r
2204  (REPEAT STRIP_TAC THEN EXPAND_TAC "q");\r
2205  (COND_CASES_TAC);\r
2206  (REFL_TAC);\r
2207  (NEW_GOAL `F`);\r
2208  (ASM_ARITH_TAC);\r
2209  (ASM_MESON_TAC[]);\r
2210 \r
2211  (NEW_GOAL `!u:num. p1 u = 1 ==> q u = 3`);\r
2212  (REPEAT STRIP_TAC THEN EXPAND_TAC "q");\r
2213  (COND_CASES_TAC);\r
2214  (NEW_GOAL `F`);\r
2215  (ASM_ARITH_TAC);\r
2216  (ASM_MESON_TAC[]);\r
2217  (COND_CASES_TAC);\r
2218  (REFL_TAC);\r
2219  (NEW_GOAL `F`);\r
2220  (ASM_ARITH_TAC);\r
2221  (ASM_MESON_TAC[]);\r
2222 \r
2223  (NEW_GOAL `!u:num. p1 u = 2 ==> q u = 0`);\r
2224  (REPEAT STRIP_TAC THEN EXPAND_TAC "q");\r
2225  (COND_CASES_TAC);\r
2226  (NEW_GOAL `F`);\r
2227  (ASM_ARITH_TAC);\r
2228  (ASM_MESON_TAC[]);\r
2229  (COND_CASES_TAC);\r
2230  (NEW_GOAL `F`);\r
2231  (ASM_ARITH_TAC);\r
2232  (ASM_MESON_TAC[]);\r
2233  (COND_CASES_TAC);\r
2234  (REFL_TAC);\r
2235  (NEW_GOAL `F`);\r
2236  (ASM_ARITH_TAC);\r
2237  (ASM_MESON_TAC[]);\r
2238 \r
2239  (NEW_GOAL `!u:num. p1 u = 3 ==> q u = 1`);\r
2240  (REPEAT STRIP_TAC THEN EXPAND_TAC "q");\r
2241  (COND_CASES_TAC);\r
2242  (NEW_GOAL `F`);\r
2243  (ASM_ARITH_TAC);\r
2244  (ASM_MESON_TAC[]);\r
2245  (COND_CASES_TAC);\r
2246  (NEW_GOAL `F`);\r
2247  (ASM_ARITH_TAC);\r
2248  (ASM_MESON_TAC[]);\r
2249  (COND_CASES_TAC);\r
2250  (NEW_GOAL `F`);\r
2251  (ASM_ARITH_TAC);\r
2252  (ASM_MESON_TAC[]);\r
2253  (COND_CASES_TAC);\r
2254  (REFL_TAC);\r
2255  (NEW_GOAL `F`);\r
2256  (ASM_ARITH_TAC);\r
2257  (ASM_MESON_TAC[]);\r
2258 \r
2259  (NEW_GOAL `!u:num. p1 u > 3 ==> q u = u`);\r
2260  (REPEAT STRIP_TAC THEN EXPAND_TAC "q");\r
2261  (COND_CASES_TAC);\r
2262  (NEW_GOAL `F`);\r
2263  (ASM_ARITH_TAC);\r
2264  (ASM_MESON_TAC[]);\r
2265  (COND_CASES_TAC);\r
2266  (NEW_GOAL `F`);\r
2267  (ASM_ARITH_TAC);\r
2268  (ASM_MESON_TAC[]);\r
2269  (COND_CASES_TAC);\r
2270  (NEW_GOAL `F`);\r
2271  (ASM_ARITH_TAC);\r
2272  (ASM_MESON_TAC[]);\r
2273  (COND_CASES_TAC);\r
2274  (NEW_GOAL `F`);\r
2275  (ASM_ARITH_TAC);\r
2276  (ASM_MESON_TAC[]);\r
2277  (REFL_TAC);\r
2278 \r
2279  (NEW_GOAL `!u:num. p1 u > 3 ==> p1 u = u`);\r
2280  (NEW_GOAL `p1 permutes 0..3`);\r
2281  (REWRITE_WITH `p1:num->num = p`);\r
2282  (UNDISCH_TAC `e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1:(real^3)list = e',e'',p,vl` THEN REWRITE_TAC[PAIR_EQ]);\r
2283  (MESON_TAC[]);\r
2284  (ASM_REWRITE_TAC[]);\r
2285  (UNDISCH_TAC `p1 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
2286  (REPEAT STRIP_TAC);\r
2287  (ABBREV_TAC `s = (p1:num->num) u`);\r
2288  (NEW_GOAL `(p1:num->num) s = s`);\r
2289  (FIRST_ASSUM MATCH_MP_TAC);\r
2290  (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);\r
2291  (NEW_GOAL `?z. (p1:num->num) z = s /\ (!y'. p1 y' = s ==> y' = z)`);\r
2292  (ASM_REWRITE_TAC[]);\r
2293  (UP_ASM_TAC THEN STRIP_TAC);\r
2294  (NEW_GOAL `s = z:num`);\r
2295  (FIRST_ASSUM MATCH_MP_TAC);\r
2296  (ASM_REWRITE_TAC[]);\r
2297  (NEW_GOAL `u = z:num`);\r
2298  (FIRST_ASSUM MATCH_MP_TAC);\r
2299  (ASM_REWRITE_TAC[]);\r
2300  (ASM_REWRITE_TAC[]);\r
2301 \r
2302  (NEW_GOAL `!u:num. q u = 0 ==> p1 u = 2`);\r
2303  (REPEAT STRIP_TAC);\r
2304  (ASM_CASES_TAC `(p1:num->num) u = 0`);\r
2305  (NEW_GOAL `(q:num->num) u = 2`);\r
2306  (FIRST_ASSUM MATCH_MP_TAC);\r
2307  (ASM_REWRITE_TAC[]);\r
2308  (NEW_GOAL `F`);\r
2309  (ASM_ARITH_TAC);\r
2310  (ASM_MESON_TAC[]);\r
2311  (ASM_CASES_TAC `(p1:num->num) u = 1`);\r
2312  (NEW_GOAL `(q:num->num) u = 3`);\r
2313  (FIRST_ASSUM MATCH_MP_TAC);\r
2314  (ASM_REWRITE_TAC[]);\r
2315  (NEW_GOAL `F`);\r
2316  (ASM_ARITH_TAC);\r
2317  (ASM_MESON_TAC[]);\r
2318  (ASM_CASES_TAC `(p1:num->num) u = 3`);\r
2319  (NEW_GOAL `(q:num->num) u = 1`);\r
2320  (FIRST_ASSUM MATCH_MP_TAC);\r
2321  (ASM_REWRITE_TAC[]);\r
2322  (NEW_GOAL `F`);\r
2323  (ASM_ARITH_TAC);\r
2324  (ASM_MESON_TAC[]);\r
2325  (ASM_CASES_TAC `(p1:num->num) u > 3`);\r
2326  (NEW_GOAL `(q:num->num) u = u`);\r
2327  (FIRST_ASSUM MATCH_MP_TAC);\r
2328  (ASM_REWRITE_TAC[]);\r
2329  (NEW_GOAL `(p1:num->num) u = u`);\r
2330  (FIRST_ASSUM MATCH_MP_TAC);\r
2331  (ASM_REWRITE_TAC[]);\r
2332  (NEW_GOAL `F`);\r
2333  (ASM_ARITH_TAC);\r
2334  (ASM_MESON_TAC[]);\r
2335  (ASM_ARITH_TAC);\r
2336 \r
2337  (NEW_GOAL `!u:num. q u = 1 ==> p1 u = 3`);\r
2338  (REPEAT STRIP_TAC);\r
2339  (ASM_CASES_TAC `(p1:num->num) u = 0`);\r
2340  (NEW_GOAL `(q:num->num) u = 2`);\r
2341  (FIRST_ASSUM MATCH_MP_TAC);\r
2342  (ASM_REWRITE_TAC[]);\r
2343  (NEW_GOAL `F`);\r
2344  (ASM_ARITH_TAC);\r
2345  (ASM_MESON_TAC[]);\r
2346  (ASM_CASES_TAC `(p1:num->num) u = 1`);\r
2347  (NEW_GOAL `(q:num->num) u = 3`);\r
2348  (FIRST_ASSUM MATCH_MP_TAC);\r
2349  (ASM_REWRITE_TAC[]);\r
2350  (NEW_GOAL `F`);\r
2351  (ASM_ARITH_TAC);\r
2352  (ASM_MESON_TAC[]);\r
2353  (ASM_CASES_TAC `(p1:num->num) u = 2`);\r
2354  (NEW_GOAL `(q:num->num) u = 0`);\r
2355  (FIRST_ASSUM MATCH_MP_TAC);\r
2356  (ASM_REWRITE_TAC[]);\r
2357  (NEW_GOAL `F`);\r
2358  (ASM_ARITH_TAC);\r
2359  (ASM_MESON_TAC[]);\r
2360  (ASM_CASES_TAC `(p1:num->num) u > 3`);\r
2361  (NEW_GOAL `(q:num->num) u = u`);\r
2362  (FIRST_ASSUM MATCH_MP_TAC);\r
2363  (ASM_REWRITE_TAC[]);\r
2364  (NEW_GOAL `(p1:num->num) u = u`);\r
2365  (FIRST_ASSUM MATCH_MP_TAC);\r
2366  (ASM_REWRITE_TAC[]);\r
2367  (NEW_GOAL `F`);\r
2368  (ASM_ARITH_TAC);\r
2369  (ASM_MESON_TAC[]);\r
2370  (ASM_ARITH_TAC);\r
2371 \r
2372  (NEW_GOAL `!u:num. q u = 2 ==> p1 u = 0`);\r
2373  (REPEAT STRIP_TAC);\r
2374  (ASM_CASES_TAC `(p1:num->num) u = 1`);\r
2375  (NEW_GOAL `(q:num->num) u = 3`);\r
2376  (FIRST_ASSUM MATCH_MP_TAC);\r
2377  (ASM_REWRITE_TAC[]);\r
2378  (NEW_GOAL `F`);\r
2379  (ASM_ARITH_TAC);\r
2380  (ASM_MESON_TAC[]);\r
2381  (ASM_CASES_TAC `(p1:num->num) u = 2`);\r
2382  (NEW_GOAL `(q:num->num) u = 0`);\r
2383  (FIRST_ASSUM MATCH_MP_TAC);\r
2384  (ASM_REWRITE_TAC[]);\r
2385  (NEW_GOAL `F`);\r
2386  (ASM_ARITH_TAC);\r
2387  (ASM_MESON_TAC[]);\r
2388  (ASM_CASES_TAC `(p1:num->num) u = 3`);\r
2389  (NEW_GOAL `(q:num->num) u = 1`);\r
2390  (FIRST_ASSUM MATCH_MP_TAC);\r
2391  (ASM_REWRITE_TAC[]);\r
2392  (NEW_GOAL `F`);\r
2393  (ASM_ARITH_TAC);\r
2394  (ASM_MESON_TAC[]);\r
2395  (ASM_CASES_TAC `(p1:num->num) u > 3`);\r
2396  (NEW_GOAL `(q:num->num) u = u`);\r
2397  (FIRST_ASSUM MATCH_MP_TAC);\r
2398  (ASM_REWRITE_TAC[]);\r
2399  (NEW_GOAL `(p1:num->num) u = u`);\r
2400  (FIRST_ASSUM MATCH_MP_TAC);\r
2401  (ASM_REWRITE_TAC[]);\r
2402  (NEW_GOAL `F`);\r
2403  (ASM_ARITH_TAC);\r
2404  (ASM_MESON_TAC[]);\r
2405  (ASM_ARITH_TAC);\r
2406 \r
2407  (NEW_GOAL `!u:num. q u = 3 ==> p1 u = 1`);\r
2408  (REPEAT STRIP_TAC);\r
2409  (ASM_CASES_TAC `(p1:num->num) u = 0`);\r
2410  (NEW_GOAL `(q:num->num) u = 2`);\r
2411  (FIRST_ASSUM MATCH_MP_TAC);\r
2412  (ASM_REWRITE_TAC[]);\r
2413  (NEW_GOAL `F`);\r
2414  (ASM_ARITH_TAC);\r
2415  (ASM_MESON_TAC[]);\r
2416  (ASM_CASES_TAC `(p1:num->num) u = 2`);\r
2417  (NEW_GOAL `(q:num->num) u = 0`);\r
2418  (FIRST_ASSUM MATCH_MP_TAC);\r
2419  (ASM_REWRITE_TAC[]);\r
2420  (NEW_GOAL `F`);\r
2421  (ASM_ARITH_TAC);\r
2422  (ASM_MESON_TAC[]);\r
2423  (ASM_CASES_TAC `(p1:num->num) u = 3`);\r
2424  (NEW_GOAL `(q:num->num) u = 1`);\r
2425  (FIRST_ASSUM MATCH_MP_TAC);\r
2426  (ASM_REWRITE_TAC[]);\r
2427  (NEW_GOAL `F`);\r
2428  (ASM_ARITH_TAC);\r
2429  (ASM_MESON_TAC[]);\r
2430  (ASM_CASES_TAC `(p1:num->num) u > 3`);\r
2431  (NEW_GOAL `(q:num->num) u = u`);\r
2432  (FIRST_ASSUM MATCH_MP_TAC);\r
2433  (ASM_REWRITE_TAC[]);\r
2434  (NEW_GOAL `(p1:num->num) u = u`);\r
2435  (FIRST_ASSUM MATCH_MP_TAC);\r
2436  (ASM_REWRITE_TAC[]);\r
2437  (NEW_GOAL `F`);\r
2438  (ASM_ARITH_TAC);\r
2439  (ASM_MESON_TAC[]);\r
2440  (ASM_ARITH_TAC);\r
2441 \r
2442  (NEW_GOAL `!u:num. q u > 3 ==> p1 u > 3`);\r
2443  (REPEAT STRIP_TAC);\r
2444  (ASM_CASES_TAC `(p1:num->num) u = 0`);\r
2445  (NEW_GOAL `(q:num->num) u = 2`);\r
2446  (FIRST_ASSUM MATCH_MP_TAC);\r
2447  (ASM_REWRITE_TAC[]);\r
2448  (NEW_GOAL `F`);\r
2449  (ASM_ARITH_TAC);\r
2450  (ASM_MESON_TAC[]);\r
2451  (ASM_CASES_TAC `(p1:num->num) u = 1`);\r
2452  (NEW_GOAL `(q:num->num) u = 3`);\r
2453  (FIRST_ASSUM MATCH_MP_TAC);\r
2454  (ASM_REWRITE_TAC[]);\r
2455  (NEW_GOAL `F`);\r
2456  (ASM_ARITH_TAC);\r
2457  (ASM_MESON_TAC[]);\r
2458  (ASM_CASES_TAC `(p1:num->num) u = 2`);\r
2459  (NEW_GOAL `(q:num->num) u = 0`);\r
2460  (FIRST_ASSUM MATCH_MP_TAC);\r
2461  (ASM_REWRITE_TAC[]);\r
2462  (NEW_GOAL `F`);\r
2463  (ASM_ARITH_TAC);\r
2464  (ASM_MESON_TAC[]);\r
2465  (ASM_CASES_TAC `(p1:num->num) u = 3`);\r
2466  (NEW_GOAL `(q:num->num) u = 1`);\r
2467  (FIRST_ASSUM MATCH_MP_TAC);\r
2468  (ASM_REWRITE_TAC[]);\r
2469  (NEW_GOAL `F`);\r
2470  (ASM_ARITH_TAC);\r
2471  (ASM_MESON_TAC[]);\r
2472  (ASM_ARITH_TAC);\r
2473 \r
2474 \r
2475  (NEW_GOAL `!u:num. p2 u = 0 ==> q u = 2`);\r
2476  (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);\r
2477  (NEW_GOAL `!u:num. p2 u = 1 ==> q u = 3`);\r
2478  (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);\r
2479  (COND_CASES_TAC);\r
2480  (NEW_GOAL `F`);\r
2481  (ASM_ARITH_TAC);\r
2482  (ASM_MESON_TAC[]);\r
2483  (REFL_TAC);\r
2484 \r
2485  (NEW_GOAL `!u:num. p2 u = 2 ==> q u = 0`);\r
2486  (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);\r
2487  (COND_CASES_TAC);\r
2488  (COND_CASES_TAC);\r
2489  (NEW_GOAL `F`);\r
2490  (ASM_ARITH_TAC);\r
2491  (ASM_MESON_TAC[]);\r
2492  (REFL_TAC);\r
2493 \r
2494  (NEW_GOAL `!u:num. p2 u = 3 ==> q u = 1`);\r
2495  (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);\r
2496  (COND_CASES_TAC);\r
2497  (NEW_GOAL `F`);\r
2498  (ASM_ARITH_TAC);\r
2499  (ASM_MESON_TAC[]);\r
2500  (COND_CASES_TAC);\r
2501  (COND_CASES_TAC);\r
2502  (NEW_GOAL `F`);\r
2503  (ASM_ARITH_TAC);\r
2504  (ASM_MESON_TAC[]);\r
2505  (REFL_TAC);\r
2506 \r
2507  (NEW_GOAL `!u:num. p2 u > 3 ==> q u = u`);\r
2508  (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);\r
2509  (COND_CASES_TAC);\r
2510  (NEW_GOAL `F`);\r
2511  (ASM_ARITH_TAC);\r
2512  (ASM_MESON_TAC[]);\r
2513  (COND_CASES_TAC);\r
2514  (NEW_GOAL `F`);\r
2515  (ASM_ARITH_TAC);\r
2516  (ASM_MESON_TAC[]);\r
2517  (COND_CASES_TAC);\r
2518  (NEW_GOAL `F`);\r
2519  (ASM_ARITH_TAC);\r
2520  (ASM_MESON_TAC[]);\r
2521  (COND_CASES_TAC);\r
2522  (NEW_GOAL `F`);\r
2523  (ASM_ARITH_TAC);\r
2524  (ASM_MESON_TAC[]);\r
2525  (REFL_TAC);\r
2526 \r
2527  (NEW_GOAL `!u:num. p2 u > 3 ==> p2 u = u`);\r
2528  (NEW_GOAL `p2 permutes 0..3`);\r
2529  (REWRITE_WITH `p2:num->num = p'`);\r
2530  (UNDISCH_TAC `f1:real^3->bool,f2:real^3->bool,p2:num->num,vl2:(real^3)list = e''',e'''',p',vl'` THEN REWRITE_TAC[PAIR_EQ]);\r
2531  (MESON_TAC[]);\r
2532  (ASM_REWRITE_TAC[]);\r
2533  (UNDISCH_TAC `p2 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);\r
2534  (REPEAT STRIP_TAC);\r
2535  (ABBREV_TAC `s = (p2:num->num) u`);\r
2536  (NEW_GOAL `(p2:num->num) s = s`);\r
2537  (FIRST_ASSUM MATCH_MP_TAC);\r
2538  (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);\r
2539  (NEW_GOAL `?z. (p2:num->num) z = s /\ (!y'. p2 y' = s ==> y' = z)`);\r
2540  (ASM_REWRITE_TAC[]);\r
2541  (UP_ASM_TAC THEN STRIP_TAC);\r
2542  (NEW_GOAL `s = z:num`);\r
2543  (FIRST_ASSUM MATCH_MP_TAC);\r
2544  (ASM_REWRITE_TAC[]);\r
2545  (NEW_GOAL `u = z:num`);\r
2546  (FIRST_ASSUM MATCH_MP_TAC);\r
2547  (ASM_REWRITE_TAC[]);\r
2548  (ASM_REWRITE_TAC[]);\r
2549 \r
2550  (NEW_GOAL `!u:num. q u = 0 ==> p2 u = 2`);\r
2551  (REPEAT STRIP_TAC);\r
2552  (ASM_CASES_TAC `(p2:num->num) u = 0`);\r
2553  (NEW_GOAL `(q:num->num) u = 2`);\r
2554  (FIRST_ASSUM MATCH_MP_TAC);\r
2555  (ASM_REWRITE_TAC[]);\r
2556  (NEW_GOAL `F`);\r
2557  (ASM_ARITH_TAC);\r
2558  (ASM_MESON_TAC[]);\r
2559  (ASM_CASES_TAC `(p2:num->num) u = 1`);\r
2560  (NEW_GOAL `(q:num->num) u = 3`);\r
2561  (FIRST_ASSUM MATCH_MP_TAC);\r
2562  (ASM_REWRITE_TAC[]);\r
2563  (NEW_GOAL `F`);\r
2564  (ASM_ARITH_TAC);\r
2565  (ASM_MESON_TAC[]);\r
2566  (ASM_CASES_TAC `(p2:num->num) u = 3`);\r
2567  (NEW_GOAL `(q:num->num) u = 1`);\r
2568  (FIRST_ASSUM MATCH_MP_TAC);\r
2569  (ASM_REWRITE_TAC[]);\r
2570  (NEW_GOAL `F`);\r
2571  (ASM_ARITH_TAC);\r
2572  (ASM_MESON_TAC[]);\r
2573  (ASM_CASES_TAC `(p2:num->num) u > 3`);\r
2574  (NEW_GOAL `(q:num->num) u = u`);\r
2575  (FIRST_ASSUM MATCH_MP_TAC);\r
2576  (ASM_REWRITE_TAC[]);\r
2577  (NEW_GOAL `(p2:num->num) u = u`);\r
2578  (FIRST_ASSUM MATCH_MP_TAC);\r
2579  (ASM_REWRITE_TAC[]);\r
2580  (NEW_GOAL `F`);\r
2581  (ASM_ARITH_TAC);\r
2582  (ASM_MESON_TAC[]);\r
2583  (ASM_ARITH_TAC);\r
2584 \r
2585  (NEW_GOAL `!u:num. q u = 1 ==> p2 u = 3`);\r
2586  (REPEAT STRIP_TAC);\r
2587  (ASM_CASES_TAC `(p2:num->num) u = 0`);\r
2588  (NEW_GOAL `(q:num->num) u = 2`);\r
2589  (FIRST_ASSUM MATCH_MP_TAC);\r
2590  (ASM_REWRITE_TAC[]);\r
2591  (NEW_GOAL `F`);\r
2592  (ASM_ARITH_TAC);\r
2593  (ASM_MESON_TAC[]);\r
2594  (ASM_CASES_TAC `(p2:num->num) u = 1`);\r
2595  (NEW_GOAL `(q:num->num) u = 3`);\r
2596  (FIRST_ASSUM MATCH_MP_TAC);\r
2597  (ASM_REWRITE_TAC[]);\r
2598  (NEW_GOAL `F`);\r
2599  (ASM_ARITH_TAC);\r
2600  (ASM_MESON_TAC[]);\r
2601  (ASM_CASES_TAC `(p2:num->num) u = 2`);\r
2602  (NEW_GOAL `(q:num->num) u = 0`);\r
2603  (FIRST_ASSUM MATCH_MP_TAC);\r
2604  (ASM_REWRITE_TAC[]);\r
2605  (NEW_GOAL `F`);\r
2606  (ASM_ARITH_TAC);\r
2607  (ASM_MESON_TAC[]);\r
2608  (ASM_CASES_TAC `(p2:num->num) u > 3`);\r
2609  (NEW_GOAL `(q:num->num) u = u`);\r
2610  (FIRST_ASSUM MATCH_MP_TAC);\r
2611  (ASM_REWRITE_TAC[]);\r
2612  (NEW_GOAL `(p2:num->num) u = u`);\r
2613  (FIRST_ASSUM MATCH_MP_TAC);\r
2614  (ASM_REWRITE_TAC[]);\r
2615  (NEW_GOAL `F`);\r
2616  (ASM_ARITH_TAC);\r
2617  (ASM_MESON_TAC[]);\r
2618  (ASM_ARITH_TAC);\r
2619 \r
2620  (NEW_GOAL `!u:num. q u = 2 ==> p2 u = 0`);\r
2621  (REPEAT STRIP_TAC);\r
2622  (ASM_CASES_TAC `(p2:num->num) u = 1`);\r
2623  (NEW_GOAL `(q:num->num) u = 3`);\r
2624  (FIRST_ASSUM MATCH_MP_TAC);\r
2625  (ASM_REWRITE_TAC[]);\r
2626  (NEW_GOAL `F`);\r
2627  (ASM_ARITH_TAC);\r
2628  (ASM_MESON_TAC[]);\r
2629  (ASM_CASES_TAC `(p2:num->num) u = 2`);\r
2630  (NEW_GOAL `(q:num->num) u = 0`);\r
2631  (FIRST_ASSUM MATCH_MP_TAC);\r
2632  (ASM_REWRITE_TAC[]);\r
2633  (NEW_GOAL `F`);\r
2634  (ASM_ARITH_TAC);\r
2635  (ASM_MESON_TAC[]);\r
2636  (ASM_CASES_TAC `(p2:num->num) u = 3`);\r
2637  (NEW_GOAL `(q:num->num) u = 1`);\r
2638  (FIRST_ASSUM MATCH_MP_TAC);\r
2639  (ASM_REWRITE_TAC[]);\r
2640  (NEW_GOAL `F`);\r
2641  (ASM_ARITH_TAC);\r
2642  (ASM_MESON_TAC[]);\r
2643  (ASM_CASES_TAC `(p2:num->num) u > 3`);\r
2644  (NEW_GOAL `(q:num->num) u = u`);\r
2645  (FIRST_ASSUM MATCH_MP_TAC);\r
2646  (ASM_REWRITE_TAC[]);\r
2647  (NEW_GOAL `(p2:num->num) u = u`);\r
2648  (FIRST_ASSUM MATCH_MP_TAC);\r
2649  (ASM_REWRITE_TAC[]);\r
2650  (NEW_GOAL `F`);\r
2651  (ASM_ARITH_TAC);\r
2652  (ASM_MESON_TAC[]);\r
2653  (ASM_ARITH_TAC);\r
2654 \r
2655  (NEW_GOAL `!u:num. q u = 3 ==> p2 u = 1`);\r
2656  (REPEAT STRIP_TAC);\r
2657  (ASM_CASES_TAC `(p2:num->num) u = 0`);\r
2658  (NEW_GOAL `(q:num->num) u = 2`);\r
2659  (FIRST_ASSUM MATCH_MP_TAC);\r
2660  (ASM_REWRITE_TAC[]);\r
2661  (NEW_GOAL `F`);\r
2662  (ASM_ARITH_TAC);\r
2663  (ASM_MESON_TAC[]);\r
2664  (ASM_CASES_TAC `(p2:num->num) u = 2`);\r
2665  (NEW_GOAL `(q:num->num) u = 0`);\r
2666  (FIRST_ASSUM MATCH_MP_TAC);\r
2667  (ASM_REWRITE_TAC[]);\r
2668  (NEW_GOAL `F`);\r
2669  (ASM_ARITH_TAC);\r
2670  (ASM_MESON_TAC[]);\r
2671  (ASM_CASES_TAC `(p2:num->num) u = 3`);\r
2672  (NEW_GOAL `(q:num->num) u = 1`);\r
2673  (FIRST_ASSUM MATCH_MP_TAC);\r
2674  (ASM_REWRITE_TAC[]);\r
2675  (NEW_GOAL `F`);\r
2676  (ASM_ARITH_TAC);\r
2677  (ASM_MESON_TAC[]);\r
2678  (ASM_CASES_TAC `(p2:num->num) u > 3`);\r
2679  (NEW_GOAL `(q:num->num) u = u`);\r
2680  (FIRST_ASSUM MATCH_MP_TAC);\r
2681  (ASM_REWRITE_TAC[]);\r
2682  (NEW_GOAL `(p2:num->num) u = u`);\r
2683  (FIRST_ASSUM MATCH_MP_TAC);\r
2684  (ASM_REWRITE_TAC[]);\r
2685  (NEW_GOAL `F`);\r
2686  (ASM_ARITH_TAC);\r
2687  (ASM_MESON_TAC[]);\r
2688  (ASM_ARITH_TAC);\r
2689 \r
2690  (NEW_GOAL `!u:num. q u > 3 ==> p2 u > 3`);\r
2691  (REPEAT STRIP_TAC);\r
2692  (ASM_CASES_TAC `(p2:num->num) u = 0`);\r
2693  (NEW_GOAL `(q:num->num) u = 2`);\r
2694  (FIRST_ASSUM MATCH_MP_TAC);\r
2695  (ASM_REWRITE_TAC[]);\r
2696  (NEW_GOAL `F`);\r
2697  (ASM_ARITH_TAC);\r
2698  (ASM_MESON_TAC[]);\r
2699  (ASM_CASES_TAC `(p2:num->num) u = 1`);\r
2700  (NEW_GOAL `(q:num->num) u = 3`);\r
2701  (FIRST_ASSUM MATCH_MP_TAC);\r
2702  (ASM_REWRITE_TAC[]);\r
2703  (NEW_GOAL `F`);\r
2704  (ASM_ARITH_TAC);\r
2705  (ASM_MESON_TAC[]);\r
2706  (ASM_CASES_TAC `(p2:num->num) u = 2`);\r
2707  (NEW_GOAL `(q:num->num) u = 0`);\r
2708  (FIRST_ASSUM MATCH_MP_TAC);\r
2709  (ASM_REWRITE_TAC[]);\r
2710  (NEW_GOAL `F`);\r
2711  (ASM_ARITH_TAC);\r
2712  (ASM_MESON_TAC[]);\r
2713  (ASM_CASES_TAC `(p2:num->num) u = 3`);\r
2714  (NEW_GOAL `(q:num->num) u = 1`);\r
2715  (FIRST_ASSUM MATCH_MP_TAC);\r
2716  (ASM_REWRITE_TAC[]);\r
2717  (NEW_GOAL `F`);\r
2718  (ASM_ARITH_TAC);\r
2719  (ASM_MESON_TAC[]);\r
2720  (ASM_ARITH_TAC);\r
2721 \r
2722  (ASM_CASES_TAC `(q:num->num) x'' = 0`);\r
2723  (NEW_GOAL `(p1:num->num) x'' = 2`);\r
2724  (ASM_SIMP_TAC[]);\r
2725  (NEW_GOAL `(p2:num->num) x'' = 2`);\r
2726  (ASM_SIMP_TAC[]);\r
2727  (ASM_REWRITE_TAC[]);\r
2728 \r
2729  (ASM_CASES_TAC `(q:num->num) x'' = 1`);\r
2730  (NEW_GOAL `(p1:num->num) x'' = 3`);\r
2731  (ASM_SIMP_TAC[]);\r
2732  (NEW_GOAL `(p2:num->num) x'' = 3`);\r
2733  (ASM_SIMP_TAC[]);\r
2734  (ASM_REWRITE_TAC[]);\r
2735 \r
2736  (ASM_CASES_TAC `(q:num->num) x'' = 2`);\r
2737  (NEW_GOAL `(p1:num->num) x'' = 0`);\r
2738  (ASM_SIMP_TAC[]);\r
2739  (NEW_GOAL `(p2:num->num) x'' = 0`);\r
2740  (ASM_SIMP_TAC[]);\r
2741  (ASM_REWRITE_TAC[]);\r
2742 \r
2743  (ASM_CASES_TAC `(q:num->num) x'' = 3`);\r
2744  (NEW_GOAL `(p1:num->num) x'' = 1`);\r
2745  (ASM_SIMP_TAC[]);\r
2746  (NEW_GOAL `(p2:num->num) x'' = 1`);\r
2747  (ASM_SIMP_TAC[]);\r
2748  (ASM_REWRITE_TAC[]);\r
2749 \r
2750  (NEW_GOAL `(q:num->num) x'' > 3`);\r
2751  (ASM_ARITH_TAC);\r
2752  (NEW_GOAL `(p1:num->num) x'' > 3`);\r
2753  (ASM_SIMP_TAC[]);\r
2754  (ASM_SIMP_TAC[]);\r
2755 \r
2756  (REWRITE_TAC[Packing3.LIST_EL_EQ]);\r
2757 \r
2758 (* ------------------------------------------------------------------------- *)\r
2759 \r
2760  (REWRITE_WITH `LENGTH (vl1:(real^3)list) = 4`);\r
2761  (REWRITE_WITH `(vl1:(real^3)list) = vl`);\r
2762  (UNDISCH_TAC `e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1:(real^3)list \r
2763    =  e',e'',p,vl` THEN REWRITE_TAC[PAIR_EQ]);\r
2764  (MESON_TAC[]);\r
2765  (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);\r
2766  (REWRITE_WITH `LENGTH (vl2:(real^3)list) = 4`);\r
2767  (REWRITE_WITH `(vl2:(real^3)list) = vl'`);\r
2768  (UNDISCH_TAC `f1:real^3->bool,f2:real^3->bool,p2:num->num,vl2:(real^3)list \r
2769    =  e''',e'''',p',vl'` THEN REWRITE_TAC[PAIR_EQ]);\r
2770  (MESON_TAC[]);\r
2771  (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);\r
2772  (REPEAT STRIP_TAC);\r
2773 \r
2774  (ASM_CASES_TAC `j = 0`);\r
2775  (NEW_GOAL `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =\r
2776              EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);\r
2777  (AP_TERM_TAC);\r
2778  (ASM_REWRITE_TAC[]);\r
2779  (UP_ASM_TAC THEN REWRITE_WITH \r
2780   `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 0 vl1 /\\r
2781    EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 0 vl2`);\r
2782  (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2783  (ASM_REWRITE_TAC[]);\r
2784 \r
2785  (ASM_CASES_TAC `j = 1`);\r
2786  (NEW_GOAL `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =\r
2787              EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);\r
2788  (AP_TERM_TAC);\r
2789  (ASM_REWRITE_TAC[]);\r
2790  (UP_ASM_TAC THEN REWRITE_WITH \r
2791   `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 1 vl1 /\\r
2792    EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 1 vl2`);\r
2793  (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2794  (ASM_REWRITE_TAC[]);\r
2795 \r
2796  (ASM_CASES_TAC `j = 2`);\r
2797  (NEW_GOAL `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =\r
2798              EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);\r
2799  (AP_TERM_TAC);\r
2800  (ASM_REWRITE_TAC[]);\r
2801  (UP_ASM_TAC THEN REWRITE_WITH \r
2802   `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 2 vl1 /\\r
2803    EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 2 vl2`);\r
2804  (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2805  (ASM_REWRITE_TAC[]);\r
2806 \r
2807  (ASM_CASES_TAC `j = 3`);\r
2808  (NEW_GOAL `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =\r
2809              EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);\r
2810  (AP_TERM_TAC);\r
2811  (ASM_REWRITE_TAC[]);\r
2812  (UP_ASM_TAC THEN REWRITE_WITH \r
2813   `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 3 vl1 /\\r
2814    EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 3 vl2`);\r
2815  (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);\r
2816  (ASM_REWRITE_TAC[]);\r
2817 \r
2818  (NEW_GOAL `F`);\r
2819  (ASM_ARITH_TAC);\r
2820  (ASM_MESON_TAC[]);\r
2821 \r
2822  (NEW_GOAL `X:real^3->bool = {}`);\r
2823  (ASM_MESON_TAC[]);\r
2824  (REPEAT STRIP_TAC);\r
2825  (REWRITE_WITH `{e | e IN critical_edgeX V X} = {}`);\r
2826  (REWRITE_TAC[SET_RULE `{x| x IN s} = s`]);\r
2827  (ASM_REWRITE_TAC[critical_edgeX; edgeX]);\r
2828  (REWRITE_WITH `VX V {} = {}`);\r
2829  (REWRITE_TAC [VX]);\r
2830  (COND_CASES_TAC);\r
2831  (REFL_TAC);\r
2832  (NEW_GOAL `F`);\r
2833  (UP_ASM_TAC THEN REWRITE_TAC[NEGLIGIBLE_EMPTY]);\r
2834  (ASM_MESON_TAC[]);\r
2835  (REWRITE_WITH `{{u:real^3, v:real^3} | {} u /\ {} v /\ ~(u = v)} = \r
2836                  {{u, v} | u IN {} /\ v IN {} /\ ~(u = v)}`);\r
2837  (REWRITE_TAC[IN]);\r
2838  (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]);\r
2839  (REWRITE_WITH `{{u:real^3, v:real^3} | F} = {}`);\r
2840  (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]);\r
2841  (GEN_TAC);\r
2842  (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`);\r
2843  (REWRITE_TAC[IN]);\r
2844  (SET_TAC[]);\r
2845  (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]);\r
2846  (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]);\r
2847  (GEN_TAC);\r
2848  (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`);\r
2849  (REWRITE_TAC[IN]);\r
2850  (SET_TAC[]);\r
2851  (REWRITE_TAC[SUM_CLAUSES])]);;\r
2852 \r
2853 \r
2854 \r
2855 \r
2856 end;;\r
2857 \r