(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma:                                                          *)
(*      Chaper    : Packing (Cells cluster)                                  *)
(*                                                                           *)
(* ------------------ The lemma about sum of beta_bump --------------------- *)
(* ========================================================================= *)

(* ========================================================================= *)
(*    Checkpointed files                                                     *)
(* ========================================================================= *)
(*

loads "/home/vu/flyspeck/working/marchal_cells_3.hl";;
flyspeck_needs "packing/UPFZBZM_support_lemmas.hl";;
open Upfzbzm_support_lemmas;;
flyspeck_needs "packing/LEPJBDJ.hl";;
open Lepjbdj;;

*)

(* ========================================================================== *)
(*   Begin the proof                                                          *)
(* ========================================================================== *)

module Sum_beta_bump = struct

open Rogers;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Sphere;; 
open Marchal_cells;;
open Emnwuus;;
open Marchal_cells_2_new;;
open Lepjbdj;;
open Upfzbzm_support_lemmas;;

let SUM_BETA_BUMP_LEMMA = 
prove_by_refinement ( `!V X. saturated V /\ packing V /\ mcell_set V X ==> sum {e | e IN critical_edgeX V X } (\e. beta_bump V e X) = &0`,
[(REPEAT STRIP_TAC THEN UP_ASM_TAC); (ASM_CASES_TAC `~(X:real^3->bool = {})`); (REWRITE_TAC[mcell_set; IN_ELIM_THM]); (STRIP_TAC); (NEW_GOAL `barV V 3 ul`); (ASM_SET_TAC[IN]); (ASM_CASES_TAC `i < 4`); (* consider case i < 4 va i >= 4 *) (NEW_GOAL `~(i = 4)`); (ASM_ARITH_TAC); (NEW_GOAL `i <= 4`); (ASM_ARITH_TAC); (ASM_REWRITE_TAC[beta_bump]); (REPEAT LET_TAC); (UP_ASM_TAC THEN REWRITE_TAC[cell_params]); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (STRIP_TAC); (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\ mcell i V ul = mcell k V ul')`); (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SELECT_AX); (EXISTS_TAC `(i:num,ul:(real^3)list)`); (EXPAND_TAC "P"); (REWRITE_TAC[BETA_THM]); (ASM_REWRITE_TAC[IN]); (UP_ASM_TAC THEN EXPAND_TAC "P"); (REWRITE_TAC[BETA_THM] THEN STRIP_TAC); (NEW_GOAL `barV V 3 ul'`); (ASM_SET_TAC[]); (NEW_GOAL `i = k:num`); (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC); (ASM_CASES_TAC `i = 0`); (NEW_GOAL `V INTER mcell i V ul = {} `); (REWRITE_TAC[ASSUME `i = 0`]); (MATCH_MP_TAC LEPJBDJ_0); (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]); (ASM_CASES_TAC `k = 0`); (ASM_REWRITE_TAC[]); (NEW_GOAL `V INTER mcell k V ul' = set_of_list (truncate_simplex (k - 1) ul')`); (MATCH_MP_TAC LEPJBDJ); (ASM_REWRITE_TAC[]); (STRIP_TAC); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (ASM_CASES_TAC `k = 1`); (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]); (ASM_SET_TAC[]); (ASM_CASES_TAC `k = 2`); (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_SET_TAC[]); (ASM_CASES_TAC `k = 3`); (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]); (ASM_SET_TAC[]); (ASM_CASES_TAC `k = 4`); (ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]); (ASM_SET_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (* Finish the case i = 0 *) (NEW_GOAL `V INTER mcell i V ul = set_of_list (truncate_simplex (i - 1) ul)`); (MATCH_MP_TAC LEPJBDJ); (ASM_REWRITE_TAC[]); (STRIP_TAC); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `k = 0`); (NEW_GOAL `V INTER mcell k V ul' = {}`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC LEPJBDJ_0); (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]); (NEW_GOAL `F`); (NEW_GOAL `~(set_of_list (truncate_simplex (i - 1) (ul:(real^3)list)) = {})`); (ASM_CASES_TAC `i = 1`); (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]); (SET_TAC[]); (ASM_CASES_TAC `i = 2`); (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (SET_TAC[]); (ASM_CASES_TAC `i = 3`); (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]); (SET_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `V INTER mcell k V ul' = set_of_list (truncate_simplex (k - 1) ul')`); (MATCH_MP_TAC LEPJBDJ); (ASM_REWRITE_TAC[]); (STRIP_TAC); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `CARD (set_of_list (truncate_simplex (i - 1) (ul:(real^3)list))) = i:num`); (REWRITE_WITH `LENGTH (truncate_simplex (i - 1) (ul:(real^3)list)) = (i - 1) + 1 /\ CARD (set_of_list (truncate_simplex (i - 1) ul)) = (i - 1) + 1`); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_ARITH_TAC); (ASM_ARITH_TAC); (NEW_GOAL `CARD (set_of_list (truncate_simplex (k - 1) (ul':(real^3)list))) = k:num`); (REWRITE_WITH `LENGTH (truncate_simplex (k - 1) (ul':(real^3)list)) = (k - 1) + 1 /\ CARD (set_of_list (truncate_simplex (k - 1) ul')) = (k - 1) + 1`); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_ARITH_TAC); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!e. sum {e',e'',p,vl | k = 4 /\ critical_edgeX V (mcell k V ul') = {e', e''} /\ e = e' /\ p permutes 0..3 /\ vl = left_action_list p ul' /\ e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}} (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) - bump (hl [EL 2 vl; EL 3 vl])) / &4) = &0`); GEN_TAC; (ABBREV_TAC `SET1 = {e',e'',p,vl | k = 4 /\ critical_edgeX V (mcell k V ul') = {e', e''} /\ e = e' /\ p permutes 0..3 /\ vl = left_action_list p ul' /\ e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}}`); (NEW_GOAL `SET1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool = {}`); (EXPAND_TAC "SET1"); (NEW_GOAL `~(k = 4)`); (ASM_MESON_TAC[]); (UP_ASM_TAC); (SET_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[SUM_CLAUSES]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[SUM_0]); (* Finish the case where i < 4 *) (* ========================================================================= *) (* begin with the case i >= 4 *) (ASM_REWRITE_TAC[beta_bump]); (REPEAT LET_TAC); (UP_ASM_TAC THEN REWRITE_TAC[cell_params]); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (STRIP_TAC); (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\ mcell i V ul = mcell k V ul')`); (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SELECT_AX); (EXISTS_TAC `(4,ul:(real^3)list)`); (EXPAND_TAC "P"); (REWRITE_TAC[BETA_THM]); (ASM_REWRITE_TAC[IN; ARITH_RULE `4 <= 4`]); (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`; ARITH_RULE `4 >= 4`; mcell4]); (UP_ASM_TAC THEN EXPAND_TAC "P"); (REWRITE_TAC[BETA_THM] THEN STRIP_TAC); (NEW_GOAL `barV V 3 ul'`); (ASM_SET_TAC[]); (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]); (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC); (NEW_GOAL `mcell i V ul = mcell 4 V ul`); (UNDISCH_TAC `mcell i V ul = mcell k V ul'` THEN DISCH_TAC THEN DEL_TAC); (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`; ARITH_RULE `4 >= 4`; mcell4]); (NEW_GOAL `k = 4:num`); (NEW_GOAL `V INTER mcell 4 V ul = set_of_list (truncate_simplex 3 ul)`); (REWRITE_TAC[ARITH_RULE `3 = 4 - 1`]); (MATCH_MP_TAC LEPJBDJ); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]); (ASM_MESON_TAC[]); (ASM_CASES_TAC `k = 0`); (NEW_GOAL `V INTER mcell k V ul' = {}`); (REWRITE_TAC[ASSUME `k = 0`]); (MATCH_MP_TAC LEPJBDJ_0); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (UNDISCH_TAC `V INTER mcell 4 V ul = set_of_list (truncate_simplex 3 ul)`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]); (ASM_SET_TAC[]); (ASM_MESON_TAC[]); (* ============================= *) (NEW_GOAL `V INTER mcell k V ul' = set_of_list (truncate_simplex (k - 1) ul')`); (MATCH_MP_TAC LEPJBDJ); (ASM_REWRITE_TAC[]); (STRIP_TAC); (ASM_ARITH_TAC); (ASM_SET_TAC[]); (NEW_GOAL `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = set_of_list (truncate_simplex (k - 1) ul')`); (ASM_SET_TAC[]); (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} = 4`); (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`); (ASM_REWRITE_TAC[set_of_list]); (REWRITE_WITH `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (ARITH_TAC); (ASM_CASES_TAC `k = 1`); (NEW_GOAL `F`); (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = set_of_list (truncate_simplex (k - 1) ul')`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]); (STRIP_TAC); (NEW_GOAL `CARD {v0:real^3} = 4`); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[Geomdetail.CARD_SING]); (ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `k = 2`); (NEW_GOAL `F`); (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = set_of_list (truncate_simplex (k - 1) ul')`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (STRIP_TAC); (NEW_GOAL `CARD {v0, v1:real^3} = 4`); (ASM_MESON_TAC[]); (NEW_GOAL `CARD {v0, v1:real^3} <= 2`); (MESON_TAC[Geomdetail.CARD2]); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `k = 3`); (NEW_GOAL `F`); (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = set_of_list (truncate_simplex (k - 1) ul')`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]); (STRIP_TAC); (NEW_GOAL `CARD {v0, v1, v2:real^3} = 4`); (ASM_MESON_TAC[]); (NEW_GOAL `CARD {v0, v1, v2:real^3} <= 3`); (MESON_TAC[Geomdetail.CARD3]); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (* concluded that k = 4 now *) (* ======================================================================== *) (REWRITE_TAC[ASSUME `mcell i V ul = mcell k V ul'`; ASSUME `k = 4`]); (ASM_CASES_TAC `~(CARD (critical_edgeX V (mcell 4 V ul')) = 2)`); (MATCH_MP_TAC SUM_EQ_0); (REPEAT STRIP_TAC); (ABBREV_TAC `y = {v0,v1,v2,v3:real^3} DIFF x`); (ASM_CASES_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`); (REWRITE_WITH `{e',e'',p,vl | critical_edgeX V (mcell 4 V ul') = {e', e''} /\ x = e' /\ p permutes 0..3 /\ vl = left_action_list p ul' /\ e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}} = {}`); (REWRITE_TAC[SET_RULE `a = {} <=> (!t. t IN a ==> F)`]); (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (NEW_GOAL `y = e'':real^3->bool`); (ONCE_ASM_REWRITE_TAC[] THEN EXPAND_TAC "y"); (REWRITE_TAC[ASSUME `x = e':real^3->bool`; ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]); (REWRITE_WITH `{v0, v1, v2, v3:real^3} = set_of_list (ul')`); (ASM_REWRITE_TAC[set_of_list]); (REWRITE_WITH `set_of_list (ul':(real^3)list) = set_of_list vl`); (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REWRITE_TAC[ASSUME `vl:(real^3)list = left_action_list p ul'`]); (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST); (ASM_REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]); (NEW_GOAL `vl:(real^3)list = [EL 0 vl; EL 1 vl; EL 2 vl; EL 3 vl]`); (ASM_REWRITE_TAC[TABLE_4; left_action_list; LENGTH; EL; HD; TL; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4 /\ 1 = SUC 0 /\ 2 = SUC 1/\ 3 = SUC 2`]); (ABBREV_TAC `w0:real^3 = EL 0 vl`); (ABBREV_TAC `w1:real^3 = EL 1 vl`); (ABBREV_TAC `w2:real^3 = EL 2 vl`); (ABBREV_TAC `w3:real^3 = EL 3 vl`); (REWRITE_TAC[ASSUME `vl = [w0;w1;w2;w3:real^3]`; set_of_list]); (REWRITE_WITH `{w0,w1,w2,w3} = {w0,w1} UNION {w2,w3:real^3}`); (SET_TAC[]); (MATCH_MP_TAC (SET_RULE `DISJOINT a b ==> ((a UNION b) DIFF a = b)`)); (REWRITE_TAC[DISJOINT; INTER]); (NEW_GOAL `CARD {w0, w1, w2 , w3:real^3} = 4`); (REWRITE_WITH `{w0, w1, w2 , w3:real^3} = set_of_list vl`); (REWRITE_TAC[ASSUME `vl = [w0; w1; w2; w3:real^3]`; set_of_list]); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_WITH `set_of_list (left_action_list p ul') = set_of_list (ul':(real^3)list)`); (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST); (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]); (REWRITE_WITH `LENGTH (ul':(real^3)list) = 3 + 1 /\ CARD (set_of_list ul') = 3 + 1`); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (ARITH_TAC); (REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]); (REWRITE_TAC[SET_RULE `x = {} <=> (!z. z IN x ==> F)`]); (REWRITE_TAC[IN;IN_ELIM_THM] THEN STRIP_TAC); (REPEAT STRIP_TAC); (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`); (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (REWRITE_TAC[Geomdetail.CARD3]); (ASM_ARITH_TAC); (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`); (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (REWRITE_TAC[Geomdetail.CARD3]); (ASM_ARITH_TAC); (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`); (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (REWRITE_TAC[Geomdetail.CARD3]); (ASM_ARITH_TAC); (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`); (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (REWRITE_TAC[Geomdetail.CARD3]); (ASM_ARITH_TAC); (UNDISCH_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`); (REWRITE_TAC[ASSUME `x = e':real^3->bool`; ASSUME `y = e'':real^3->bool`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[SUM_CLAUSES]); (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC); (NEW_GOAL `F`); (UNDISCH_TAC `~(CARD (critical_edgeX V (mcell 4 V ul')) = 2)`); (REWRITE_TAC[ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]); (REWRITE_TAC[Geomdetail.CARD_SET2]); (EXPAND_TAC "y"); (STRIP_TAC); (NEW_GOAL `{v0, v1,v2,v3:real^3} = {}`); (MATCH_MP_TAC (SET_RULE `!s:real^3->bool. x = s DIFF x ==> s = {}`)); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN SET_TAC[]); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC); (NEW_GOAL `?x y. critical_edgeX V (mcell 4 V ul') = {x, y} /\ ~(x = y)`); (MATCH_MP_TAC Rogers.CARD_2_IMP_DOUBLE); (ASM_REWRITE_TAC[FINITE_critical_edgeX]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_TAC[SET_RULE `{x | x IN s} = s`; ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]); (ASM_SIMP_TAC[Collect_geom.SUM_DIS2]); (REWRITE_WITH `{e',e'',p,vl | {x, y} = {e', e''} /\ x = e' /\ p permutes 0..3 /\ vl = left_action_list p [v0; v1; v2; v3:real^3] /\ e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}} = {e',e'',p,vl | e' = x /\ e'' = y /\ p permutes 0..3 /\ vl = left_action_list p [v0; v1; v2; v3] /\ x = {EL 0 vl, EL 1 vl} /\ y = {EL 2 vl, EL 3 vl}}`); (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]); (STRIP_TAC); (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`); (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `e':real^3->bool = x`; ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`]); (REWRITE_TAC[ASSUME `e'':real^3->bool = y`; ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`); (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`); (NEW_GOAL `y = e'':(real^3->bool)`); (ASM_SET_TAC[]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `x:real^3->bool = e'`; ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]); (REWRITE_TAC[ASSUME `y:real^3->bool = e''`; ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{e',e'',p,vl | {x, y} = {e', e''} /\ y = e' /\ p permutes 0..3 /\ vl = left_action_list p [v0; v1; v2; v3:real^3] /\ e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}} = {e',e'',p,vl | e' = y /\ e'' = x /\ p permutes 0..3 /\ vl = left_action_list p [v0; v1; v2; v3] /\ y = {EL 0 vl, EL 1 vl} /\ x = {EL 2 vl, EL 3 vl}}`); (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]); (STRIP_TAC); (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`); (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`); (REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `e' = y:real^3->bool`; ASSUME `e'' = x:real^3->bool`]); (SET_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `e':real^3->bool = y`; ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`]); (REWRITE_TAC[ASSUME `e'':real^3->bool = x`; ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`); (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`); (NEW_GOAL `x = e'':(real^3->bool)`); (ASM_SET_TAC[]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `y:real^3->bool = e'`; ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]); (REWRITE_TAC[ASSUME `x:real^3->bool = e''`; ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]); (ASM_REWRITE_TAC[]); (ABBREV_TAC `S1 = {e',e'',p,vl | e' = x /\ e'' = y /\ p permutes 0..3 /\ vl = left_action_list p [v0; v1; v2; v3:real^3] /\ x = {EL 0 vl, EL 1 vl} /\ y = {EL 2 vl, EL 3 vl}}`); (ABBREV_TAC `S2 = {e',e'',p,vl | e' = y /\ e'' = x /\ p permutes 0..3 /\ vl = left_action_list p [v0; v1; v2; v3:real^3] /\ y = {EL 0 vl, EL 1 vl} /\ x = {EL 2 vl, EL 3 vl}}`); (REWRITE_WITH `sum (S2:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool) (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) - bump (hl [EL 2 vl; EL 3 vl])) / &4) = sum S2 (\(e',e'',p,vl). -- ((bump (hl [EL 2 vl; EL 3 vl]) - bump (hl [EL 0 vl; EL 1 vl])) / &4))`); (ONCE_REWRITE_TAC[REAL_ARITH `(bump (hl [EL 0 vl; EL 1 vl]) - bump (hl [EL 2 vl; EL 3 vl])) / &4 = -- ((bump (hl [EL 2 vl; EL 3 vl]) - bump (hl [EL 0 vl; EL 1 vl])) / &4)`]); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[SUM_NEG]); (ABBREV_TAC `f = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). ((bump (hl [EL 2 vl; EL 3 vl]) - bump (hl [EL 0 vl; EL 1 vl])) / &4))`); (REWRITE_WITH `(\(e',e'',p,vl). --((bump (hl [EL 2 vl; EL 3 vl]) -bump (hl [EL 0 vl; EL 1 vl])) / &4)) = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). -- f (e',e'',p,vl))`); (EXPAND_TAC "f"); (REWRITE_TAC[BETA_THM]); (REWRITE_WITH `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). -- f (e',e'',p,vl)) = sum S2 (\x. -- f x)`); (AP_TERM_TAC); (REWRITE_TAC[FUN_EQ_THM]); (EXPAND_TAC "f"); (REWRITE_TAC[BETA_THM]); (REPEAT STRIP_TAC); (ABBREV_TAC `e' = FST (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`); (ABBREV_TAC `e'' = FST (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`); (ABBREV_TAC `p = FST (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`); (ABBREV_TAC `vl = SND (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`); (REWRITE_WITH `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = (e',e'',p, vl)`); (EXPAND_TAC "e'" THEN EXPAND_TAC "e''" THEN EXPAND_TAC "p" THEN EXPAND_TAC "vl"); (REWRITE_TAC[PAIR]); (REWRITE_TAC[SUM_NEG]); (REWRITE_TAC[REAL_ARITH `a + -- b = &0 <=> a = b`]); (* --------------------------------------------------------------------------- *) (* Begin new part *) (EXPAND_TAC "f"); (ABBREV_TAC `g = (\x. let (e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list) = x in (e'', e', (\i. if p i = 0 then 2 else if p i = 1 then 3 else if p i = 2 then 0 else if p i = 3 then 1 else i), [EL 2 vl;EL 3 vl;EL 0 vl;EL 1 vl]))`); (REWRITE_WITH `S1 = IMAGE (g:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->(real^3->bool)# (real^3->bool)#(num->num)#(real^3)list) S2 /\ (\(e',e'',p,vl). (bump (hl [EL 2 vl; EL 3 vl]) - bump (hl [EL 0 vl; EL 1 vl])) / &4) = (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) - bump (hl [EL 2 vl; EL 3 vl])) / &4) o g `); (* ======================================================================= *) (REPEAT STRIP_TAC); (* New goal 1: to prove S1 = IMAGE g S2 *) (EXPAND_TAC "S1" THEN EXPAND_TAC "S2"); (REWRITE_TAC[IMAGE]); (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXISTS_TAC `(e'':real^3->bool, e':real^3->bool, (\i. if p i = 0 then 2 else if p i = 1 then 3 else if p i = 2 then 0 else if p i = 3 then 1 else i), [EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl])`); (REPEAT STRIP_TAC); (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`); (ABBREV_TAC `p' = (\i. if p i = 0 then 2 else if p i = 1 then 3 else if p i = 2 then 0 else if p i = 3 then 1 else i)`); (EXISTS_TAC `p':num->num`); (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`); (REWRITE_WITH `EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 2 (vl:(real^3)list) /\ EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 3 vl /\ EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 0 vl /\ EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 1 vl`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_TAC[ASSUME `e'' = y:real^3->bool`; ASSUME `e' = x:real^3->bool`; ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`; ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`;left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p u > 3 ==> p u = u`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (ABBREV_TAC `s = (p:num->num) u`); (NEW_GOAL `(p:num->num) s = s`); (FIRST_ASSUM MATCH_MP_TAC); (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `s = x'':num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `u = x'':num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (* ------------------------------------------------------------------------- *) (* begin to prove that p' permutes 0..3 *) (NEW_GOAL `p' permutes 0..3`); (REWRITE_TAC[permutes]); (REPEAT STRIP_TAC); (NEW_GOAL `x'' > 3`); (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (EXPAND_TAC "p'"); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC); (NEW_GOAL `(p:num->num) x'' = x''`); (ASM_SIMP_TAC[]); (COND_CASES_TAC); (ASM_ARITH_TAC); (COND_CASES_TAC); (ASM_ARITH_TAC); (COND_CASES_TAC); (ASM_ARITH_TAC); (COND_CASES_TAC); (ASM_ARITH_TAC); (REFL_TAC); (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC); (ASM_CASES_TAC `y' = 0`); (NEW_GOAL `?z. (p:num->num) z = 2`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 2`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `y' = 1`); (NEW_GOAL `?z. (p:num->num) z = 3`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 3`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `y' = 2`); (NEW_GOAL `?z. (p:num->num) z = 0`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 0`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `y' = 3`); (NEW_GOAL `?z. (p:num->num) z = 1`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 1`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `y' > 3`); (ASM_ARITH_TAC); (NEW_GOAL `?z. (p:num->num) z = y'`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (NEW_GOAL `(p:num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (NEW_GOAL `(p':num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (ASM_ARITH_TAC); (NEW_GOAL `(p:num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (NEW_GOAL `(p':num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `(p:num->num) y'' > 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = y''`); (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`)); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p':num->num) y'' = y''`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_MESON_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_MESON_TAC[]); (* finish proving that p' permutes 0..3 *) (REWRITE_TAC[ASSUME `p' permutes 0..3`]); (* --------------------------------------------------------------------- *) (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 2 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 2) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`); (ABBREV_TAC `j = inverse (p:num->num) 2`); (NEW_GOAL `(p:num->num) j = 2`); (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 3 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 3) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`); (ABBREV_TAC `j = inverse (p:num->num) 3`); (NEW_GOAL `(p:num->num) j = 3`); (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 0 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 0) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`); (ABBREV_TAC `j = inverse (p:num->num) 0`); (NEW_GOAL `(p:num->num) j = 0`); (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 1 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 1) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`); (ABBREV_TAC `j = inverse (p:num->num) 1`); (NEW_GOAL `(p:num->num) j = 1`); (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (* ======================================================================= *) (EXPAND_TAC "g"); (LET_TAC); (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; ASSUME `x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = e',e'',p,vl`]); (REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `e':real^3->bool = e''''`]); (REWRITE_TAC[ASSUME `e'':real^3->bool = e'''`]); (REWRITE_TAC[FUN_EQ_THM]); (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p u > 3 ==> p u = u`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (ABBREV_TAC `s = (p:num->num) u`); (NEW_GOAL `(p:num->num) s = s`); (FIRST_ASSUM MATCH_MP_TAC); (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `s = x'':num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `u = x'':num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (GEN_TAC); (COND_CASES_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (COND_CASES_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (COND_CASES_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (COND_CASES_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) x'' > 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (* ------------------------------------------------------------------------- *) (EXPAND_TAC "vl'"); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_TAC[ASSUME `vl = left_action_list p [v0; v1; v2; v3:real^3]`; left_action_list; TABLE_4; LENGTH;EL; HD;TL; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]); (* ======================================================================= *) (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`); (ABBREV_TAC `p' = (\i. if p i = 0 then 2 else if p i = 1 then 3 else if p i = 2 then 0 else if p i = 3 then 1 else i)`); (EXISTS_TAC `p':num->num`); (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`); (REWRITE_WITH `{EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl], EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]} = {EL 0 vl, EL 1 (vl:(real^3)list)}`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `{EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl], EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]} = {EL 2 vl, EL 3 (vl:(real^3)list)}`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_TAC[ASSUME `e'' = x:real^3->bool`; ASSUME `e' = y:real^3->bool`; ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`; ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`;left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`); (REPEAT STRIP_TAC THEN EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p u > 3 ==> p u = u`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (ABBREV_TAC `s = (p:num->num) u`); (NEW_GOAL `(p:num->num) s = s`); (FIRST_ASSUM MATCH_MP_TAC); (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `s = x''':num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `u = x''':num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u > 3`); (NEW_GOAL `(p':num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p:num->num) u = 0`); (NEW_GOAL `(p':num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 1`); (NEW_GOAL `(p':num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 2`); (NEW_GOAL `(p':num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p:num->num) u = 3`); (NEW_GOAL `(p':num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (* ------------------------------------------------------------------------- *) (* begin to prove that p' permutes 0..3 *) (NEW_GOAL `p' permutes 0..3`); (REWRITE_TAC[permutes]); (REPEAT STRIP_TAC); (NEW_GOAL `x''' > 3`); (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (EXPAND_TAC "p'"); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC); (NEW_GOAL `(p:num->num) x''' = x'''`); (ASM_SIMP_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC); (ASM_CASES_TAC `y' = 0`); (NEW_GOAL `?z. (p:num->num) z = 2`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 2`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `y' = 1`); (NEW_GOAL `?z. (p:num->num) z = 3`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 3`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `y' = 2`); (NEW_GOAL `?z. (p:num->num) z = 0`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 0`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `y' = 3`); (NEW_GOAL `?z. (p:num->num) z = 1`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = 1`); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `y' > 3`); (ASM_ARITH_TAC); (NEW_GOAL `?z. (p:num->num) z = y'`); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `z:num`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (NEW_GOAL `(p:num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (NEW_GOAL `(p':num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (ASM_ARITH_TAC); (NEW_GOAL `(p:num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (NEW_GOAL `(p':num->num) z = z`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_ARITH_TAC); (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (NEW_GOAL `(p:num->num) y'' > 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p:num->num) y'' = y''`); (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`)); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p':num->num) y'' = y''`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `y'' = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_MESON_TAC[]); (REWRITE_WITH `z = s:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_MESON_TAC[]); (* finish proving that p' permutes 0..3 *) (REWRITE_TAC[ASSUME `p' permutes 0..3`]); (* --------------------------------------------------------------------- *) (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 2 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 2) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`); (ABBREV_TAC `j = inverse (p:num->num) 2`); (NEW_GOAL `(p:num->num) j = 2`); (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 3 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 3) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`); (ABBREV_TAC `j = inverse (p:num->num) 3`); (NEW_GOAL `(p:num->num) j = 3`); (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 0 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 0) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`); (ABBREV_TAC `j = inverse (p:num->num) 0`); (NEW_GOAL `(p:num->num) j = 0`); (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`); (ASM_REWRITE_TAC[left_action_list; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]); (REWRITE_WITH `EL 1 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] = EL (inverse p 1) [v0; v1; v2; v3:real^3]`); (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`); (ABBREV_TAC `j = inverse (p:num->num) 1`); (NEW_GOAL `(p:num->num) j = 1`); (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`); (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]); (EXPAND_TAC "p'"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (* ======================================================================= *) (ONCE_REWRITE_TAC[ASSUME `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = g (x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`]); (REWRITE_TAC[ASSUME `x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = e',e'',p,vl`] THEN EXPAND_TAC "g"); (LET_TAC); (REWRITE_TAC[PAIR_EQ]); (EXPAND_TAC "p'" THEN REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (* --------------------------------------------------- *) (* It is left to prove only 3 subgoals *) (EXPAND_TAC "g"); (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC); (REWRITE_TAC[FUN_EQ_THM]); (GEN_TAC); (NEW_GOAL `?e1 e2 p1 vl1. x' = (e1:real^3->bool,e2:real^3->bool,p1:num->num, vl1:(real^3)list)`); (EXISTS_TAC `FST (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`); (EXISTS_TAC `FST (SND (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`); (EXISTS_TAC `FST (SND (SND (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`); (EXISTS_TAC `SND (SND (SND (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`); (REWRITE_TAC[PAIR]); (UP_ASM_TAC THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `(\x. let e',e'',p,vl = x in e'', e', (\i. if p i = 0 then 2 else if p i = 1 then 3 else if p i = 2 then 0 else if p i = 3 then 1 else i), [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]) = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). e'', e', (\i. if p i = 0 then 2 else if p i = 1 then 3 else if p i = 2 then 0 else if p i = 3 then 1 else i), [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl])`); (REWRITE_TAC[FUN_EQ_THM]); (GEN_TAC); (LET_TAC); (REWRITE_TAC[BETA_THM]); (REWRITE_TAC[o_THM]); (REWRITE_WITH `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 2 (vl1:(real^3)list) /\ EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 3 (vl1:(real^3)list) /\ EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 0 (vl1:(real^3)list) /\ EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 1 (vl1:(real^3)list)`); (REWRITE_TAC[EL;HD;TL; LENGTH; ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]); (MATCH_MP_TAC SUM_IMAGE); (EXPAND_TAC "S1" THEN EXPAND_TAC "S2"); (ONCE_REWRITE_TAC[IN]); (REWRITE_TAC[IN_ELIM_THM]); (EXPAND_TAC "g"); (REPEAT STRIP_TAC); (NEW_GOAL `(let e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1 = x' in e2, e1, (\i. if p1 i = 0 then 2 else if p1 i = 1 then 3 else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i), [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1]) = (let f1,f2,p2,vl2 = y' in f2, f1, (\i. if p2 i = 0 then 2 else if p2 i = 1 then 3 else if p2 i = 2 then 0 else if p2 i = 3 then 1 else i), [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)])`); (ASM_REWRITE_TAC[ETA_AX]); (UP_ASM_TAC THEN DEL_TAC THEN REPEAT LET_TAC THEN REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC); (ABBREV_TAC `q = (\i. if p1 i = 0 then 2 else if p1 i = 1 then 3 else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i)`); (NEW_GOAL `!u:num. p1 u = 0 ==> q u = 2`); (REPEAT STRIP_TAC THEN EXPAND_TAC "q"); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p1 u = 1 ==> q u = 3`); (REPEAT STRIP_TAC THEN EXPAND_TAC "q"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p1 u = 2 ==> q u = 0`); (REPEAT STRIP_TAC THEN EXPAND_TAC "q"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p1 u = 3 ==> q u = 1`); (REPEAT STRIP_TAC THEN EXPAND_TAC "q"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!u:num. p1 u > 3 ==> q u = u`); (REPEAT STRIP_TAC THEN EXPAND_TAC "q"); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p1 u > 3 ==> p1 u = u`); (NEW_GOAL `p1 permutes 0..3`); (REWRITE_WITH `p1:num->num = p`); (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]); (MESON_TAC[]); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `p1 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (ABBREV_TAC `s = (p1:num->num) u`); (NEW_GOAL `(p1:num->num) s = s`); (FIRST_ASSUM MATCH_MP_TAC); (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (NEW_GOAL `?z. (p1:num->num) z = s /\ (!y'. p1 y' = s ==> y' = z)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `s = z:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `u = z:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!u:num. q u = 0 ==> p1 u = 2`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p1:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p1:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u = 1 ==> p1 u = 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p1:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p1:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u = 2 ==> p1 u = 0`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p1:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p1:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u = 3 ==> p1 u = 1`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p1:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p1:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u > 3 ==> p1 u > 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p1:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p1:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. p2 u = 0 ==> q u = 2`); (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `!u:num. p2 u = 1 ==> q u = 3`); (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p2 u = 2 ==> q u = 0`); (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]); (COND_CASES_TAC); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p2 u = 3 ==> q u = 1`); (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p2 u > 3 ==> q u = u`); (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `!u:num. p2 u > 3 ==> p2 u = u`); (NEW_GOAL `p2 permutes 0..3`); (REWRITE_WITH `p2:num->num = p'`); (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]); (MESON_TAC[]); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `p2 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (REPEAT STRIP_TAC); (ABBREV_TAC `s = (p2:num->num) u`); (NEW_GOAL `(p2:num->num) s = s`); (FIRST_ASSUM MATCH_MP_TAC); (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (NEW_GOAL `?z. (p2:num->num) z = s /\ (!y'. p2 y' = s ==> y' = z)`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `s = z:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `u = z:num`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!u:num. q u = 0 ==> p2 u = 2`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p2:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p2:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u = 1 ==> p2 u = 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p2:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p2:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u = 2 ==> p2 u = 0`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p2:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p2:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u = 3 ==> p2 u = 1`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p2:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u > 3`); (NEW_GOAL `(q:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `(p2:num->num) u = u`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `!u:num. q u > 3 ==> p2 u > 3`); (REPEAT STRIP_TAC); (ASM_CASES_TAC `(p2:num->num) u = 0`); (NEW_GOAL `(q:num->num) u = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 1`); (NEW_GOAL `(q:num->num) u = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 2`); (NEW_GOAL `(q:num->num) u = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `(p2:num->num) u = 3`); (NEW_GOAL `(q:num->num) u = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (ASM_CASES_TAC `(q:num->num) x'' = 0`); (NEW_GOAL `(p1:num->num) x'' = 2`); (ASM_SIMP_TAC[]); (NEW_GOAL `(p2:num->num) x'' = 2`); (ASM_SIMP_TAC[]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `(q:num->num) x'' = 1`); (NEW_GOAL `(p1:num->num) x'' = 3`); (ASM_SIMP_TAC[]); (NEW_GOAL `(p2:num->num) x'' = 3`); (ASM_SIMP_TAC[]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `(q:num->num) x'' = 2`); (NEW_GOAL `(p1:num->num) x'' = 0`); (ASM_SIMP_TAC[]); (NEW_GOAL `(p2:num->num) x'' = 0`); (ASM_SIMP_TAC[]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `(q:num->num) x'' = 3`); (NEW_GOAL `(p1:num->num) x'' = 1`); (ASM_SIMP_TAC[]); (NEW_GOAL `(p2:num->num) x'' = 1`); (ASM_SIMP_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `(q:num->num) x'' > 3`); (ASM_ARITH_TAC); (NEW_GOAL `(p1:num->num) x'' > 3`); (ASM_SIMP_TAC[]); (ASM_SIMP_TAC[]); (REWRITE_TAC[Packing3.LIST_EL_EQ]); (* ------------------------------------------------------------------------- *) (REWRITE_WITH `LENGTH (vl1:(real^3)list) = 4`); (REWRITE_WITH `(vl1:(real^3)list) = vl`); (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]); (MESON_TAC[]); (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]); (REWRITE_WITH `LENGTH (vl2:(real^3)list) = 4`); (REWRITE_WITH `(vl2:(real^3)list) = vl'`); (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]); (MESON_TAC[]); (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]); (REPEAT STRIP_TAC); (ASM_CASES_TAC `j = 0`); (NEW_GOAL `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`); (AP_TERM_TAC); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 0 vl1 /\ EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 0 vl2`); (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `j = 1`); (NEW_GOAL `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`); (AP_TERM_TAC); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 1 vl1 /\ EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 1 vl2`); (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `j = 2`); (NEW_GOAL `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`); (AP_TERM_TAC); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 2 vl1 /\ EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 2 vl2`); (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `j = 3`); (NEW_GOAL `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`); (AP_TERM_TAC); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 3 vl1 /\ EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 3 vl2`); (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `X:real^3->bool = {}`); (ASM_MESON_TAC[]); (REPEAT STRIP_TAC); (REWRITE_WITH `{e | e IN critical_edgeX V X} = {}`); (REWRITE_TAC[SET_RULE `{x| x IN s} = s`]); (ASM_REWRITE_TAC[critical_edgeX; edgeX]); (REWRITE_WITH `VX V {} = {}`); (REWRITE_TAC [VX]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (UP_ASM_TAC THEN REWRITE_TAC[NEGLIGIBLE_EMPTY]); (ASM_MESON_TAC[]); (REWRITE_WITH `{{u:real^3, v:real^3} | {} u /\ {} v /\ ~(u = v)} = {{u, v} | u IN {} /\ v IN {} /\ ~(u = v)}`); (REWRITE_TAC[IN]); (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]); (REWRITE_WITH `{{u:real^3, v:real^3} | F} = {}`); (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]); (GEN_TAC); (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`); (REWRITE_TAC[IN]); (SET_TAC[]); (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]); (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]); (GEN_TAC); (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`); (REWRITE_TAC[IN]); (SET_TAC[]); (REWRITE_TAC[SUM_CLAUSES])]);;
end;;