(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                           *)
(* Lemma: OXLZLEZ                                                             *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-12-31                                                           *)
(* ========================================================================== *)

(* REDO THE beta_bump  *)



module Bump = struct

  open Hales_tactic;;

let WEAK_SELECT_TAC  =
  
let unbeta = 
prove( `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,
MESON_TAC[]) in let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in unbeta_tac THEN (MATCH_MP_TAC Tactics.SELECT_THM) THEN BETA_TAC THEN REPEAT WEAK_STRIP_TAC;;
let BETA_ORDERED_PAIR_THM = 
prove_by_refinement( `!(g:A->B->C) x. ((\ ( u, v). g u v) x = g (FST x) (SND x))`,
(* {{{ proof *) [ REPEAT GEN_TAC; INTRO_TAC (GSYM PAIR) [`x`]; DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[GABS_DEF;GEQ_DEF]) ]);;
(* }}} *)
let BIJ_SUM = 
prove_by_refinement( `!(A:A->bool) (B:B->bool) f ab. BIJ ab A B ==> (sum A (f o ab) = sum B f)`,
(* {{{ proof *) [ REWRITE_TAC[BIJ;INJ]; BY(ASM_MESON_TAC[ SUM_IMAGE ; Misc_defs_and_lemmas.SURJ_IMAGE ]) ]);;
(* }}} *)
let EL_EXPLICIT = 
prove_by_refinement( `!h t. EL 0 (CONS (h:a) t) = h /\ EL 1 (CONS h t) = EL 0 t /\ EL 2 (CONS h t) = EL 1 t /\ EL 3 (CONS h t) = EL 2 t /\ EL 4 (CONS h t) = EL 3 t /\ EL 5 (CONS h t) = EL 4 t /\ EL 6 (CONS h t) = EL 5 t`,
(* {{{ proof *) [ BY(REWRITE_TAC[EL;HD;TL;arith `6 = SUC 5 /\ 5 = SUC 4 /\ 4 = SUC 3 /\ 3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`]) ]);;
(* }}} *)
let LENGTH1 = 
prove_by_refinement( `!ul:(A) list. LENGTH ul = 1 ==> ul = [EL 0 ul]`,
(* {{{ proof *) [ REWRITE_TAC[LENGTH_EQ_CONS;arith `1 = SUC 0`;LENGTH_EQ_NIL]; REPEAT WEAK_STRIP_TAC; BY(ASM_REWRITE_TAC[EL;HD]) ]);;
(* }}} *)
let LENGTH2 = 
prove_by_refinement( `!ul:(A) list. LENGTH ul = 2 ==> ul = [EL 0 ul;EL 1 ul]`,
(* {{{ proof *) [ REWRITE_TAC[LENGTH_EQ_CONS;arith `2 = SUC 1`]; REPEAT WEAK_STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH1)); BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;TL]) ]);;
(* }}} *)
let LENGTH3 = 
prove_by_refinement( `!(ul:(A)list). LENGTH ul = 3 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul]`,
(* {{{ proof *) [ REWRITE_TAC[LENGTH_EQ_CONS;arith `3 = SUC 2`]; REPEAT WEAK_STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH2)); BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;TL]) ]);;
(* }}} *)
let LENGTH4 = 
prove_by_refinement( `!(ul:(A)list). LENGTH ul = 4 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul; EL 3 ul]`,
(* {{{ proof *) [ REWRITE_TAC[LENGTH_EQ_CONS;arith `4 = SUC 3`]; REPEAT WEAK_STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH3)); BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;arith `3 = SUC 2`;TL]) ]);;
(* }}} *)
let set_of_list2 = 
prove_by_refinement( `!(ul:(A) list). LENGTH ul = 2 ==> set_of_list ul = {EL 0 ul, EL 1 ul}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH2)); ABBREV_TAC `a:A = EL 0 ul`; ABBREV_TAC `b:A = EL 1 ul`; DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[set_of_list]) ]);;
(* }}} *)
let set_of_list2_explicit = 
prove_by_refinement( `!(a:A) b. set_of_list [a;b] = {a,b}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; GMATCH_SIMP_TAC set_of_list2; BY(REWRITE_TAC[LENGTH;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`]) ]);;
(* }}} *)
let set_of_list3 = 
prove_by_refinement( `!(ul:(A) list). LENGTH ul = 3 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3)); ABBREV_TAC `a:A = EL 0 ul`; ABBREV_TAC `b:A = EL 1 ul`; ABBREV_TAC `c:A = EL 2 ul`; DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[set_of_list]) ]);;
(* }}} *)
let set_of_list3_explicit = 
prove_by_refinement( `!(a:A) b c. set_of_list [a;b;c] = {a,b,c}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; GMATCH_SIMP_TAC set_of_list3; BY(REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0 /\ 3 = SUC 2 /\ 4 = SUC 3`;LENGTH]) ]);;
(* }}} *)
let set_of_list4 = 
prove_by_refinement( `!(ul:(A) list). LENGTH ul = 4 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH4)); ABBREV_TAC `a:A = EL 0 ul`; ABBREV_TAC `b:A = EL 1 ul`; ABBREV_TAC `c:A = EL 2 ul`; ABBREV_TAC `d:A = EL 3 ul`; DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[set_of_list]) ]);;
(* }}} *)
let set_of_list4_explicit = 
prove_by_refinement( `!(a:A) b c d. set_of_list [a;b;c;d] = {a,b,c,d}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; GMATCH_SIMP_TAC set_of_list4; BY(REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0 /\ 3 = SUC 2 /\ 4 = SUC 3`;LENGTH]) ]);;
(* }}} *)
let SET_OF_LIST_TRUNCATE_1 = 
prove_by_refinement( `!(ul:(A)list). 2 <= LENGTH ul ==> set_of_list (truncate_simplex 1 ul) = {EL 0 ul,EL 1 ul}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; GMATCH_SIMP_TAC set_of_list2; CONJ_TAC; REWRITE_TAC[arith `2 = 1 + 1`]; MATCH_MP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX; BY(ASM_REWRITE_TAC[arith `1 + 1 =2`]); REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX); BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC) ]);;
(* }}} *)
let SET_OF_LIST_TRUNCATE_2 = 
prove_by_refinement( `!(ul:(A)list). 3 <= LENGTH ul ==> set_of_list (truncate_simplex 2 ul) = {EL 0 ul,EL 1 ul,EL 2 ul}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; GMATCH_SIMP_TAC set_of_list3; CONJ_TAC; REWRITE_TAC[arith `3 = 2 + 1`]; MATCH_MP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX; BY(ASM_REWRITE_TAC[arith `2 + 1 =3`]); REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX); ASM_REWRITE_TAC[]; BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC) ]);;
(* }}} *)
let VX_EMPTY = 
prove_by_refinement( `!V vl k. (NULLSET (mcell k V vl)) ==> (VX V (mcell k V vl) = {})`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; BY(ASM_REWRITE_TAC[Pack_defs.VX]) ]);;
(* }}} *)
let RIJRIED = 
prove_by_refinement( `!V vl k. (NULLSET (mcell k V vl)) ==> (edgeX V (mcell k V vl) = {})`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[Pack_defs.edgeX]; INTRO_TAC VX_EMPTY[`V`;`vl`;`k`]; ASM_SIMP_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY]; BY(MESON_TAC[IN]) ]);;
(* }}} *)
let  HDTFNFZ_SUBSET = 
prove_by_refinement( `!V ul k X. saturated V /\ packing V /\ barV V 3 ul /\ X = mcell k V ul ==> VX V X SUBSET V INTER X`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; TYPIFY `NULLSET X` ASM_CASES_TAC; BY(ASM_MESON_TAC[EMPTY_SUBSET;VX_EMPTY]); BY(ASM_MESON_TAC[Hdtfnfz.HDTFNFZ;SUBSET_REFL]) ]);;
(* }}} *)
let HDTFNFZ_ALT = 
prove_by_refinement( `!V ul k X. saturated V /\ packing V /\ barV V 3 ul /\ X = mcell k V ul /\ ~NULLSET X ==> VX V X = V INTER X`,
(* {{{ proof *) [ ASM_MESON_TAC[Hdtfnfz.HDTFNFZ] ]);;
(* }}} *)
let VORONOI_V = 
prove_by_refinement( `!V (w:real^A). w IN V ==> (V INTER voronoi_closed V w = {w})`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.voronoi_closed;EXTENSION;IN_SING;IN_INTER;IN_ELIM_THM]; REWRITE_TAC[IN]; REPEAT WEAK_STRIP_TAC; BY(ASM_MESON_TAC[DIST_EQ_0;arith `x <= &0 /\ &0 <= x ==> x = &0`;DIST_POS_LE]) ]);;
(* }}} *)
let V_CELL0_EMPTY = 
prove_by_refinement( `!V vl. saturated V /\ packing V /\ barV V 3 vl ==> V INTER (mcell0 V vl) = {}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;Pack_defs.mcell0;IN_DIFF]; REPEAT WEAK_STRIP_TAC; INTRO_TAC Marchal_cells_3.ROGERS_SUBSET_VORONOI_CLOSED [`V`;`vl`]; ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC VORONOI_V [`V`;`HD vl`]; REWRITE_TAC[EXTENSION;IN_SING;IN_INTER]; TYPIFY `x = HD vl` ASM_CASES_TAC; FIRST_X_ASSUM_ST `ball` MP_TAC; REWRITE_TAC[ball]; ASM_REWRITE_TAC[ball;IN_ELIM_THM;DIST_REFL]; MATCH_MP_TAC (TAUT `a ==> (~a ==> b)`); GMATCH_SIMP_TAC REAL_LT_RSQRT; BY(REAL_ARITH_TAC); DISCH_THEN ( MP_TAC); ANTS_TAC; BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;SUBSET;IN;Packing3.BARV_IMP_HD_IN_SET_OF_LIST]); DISCH_THEN (C INTRO_TAC [`x`]); BY(ASM_MESON_TAC[SUBSET]) ]);;
(* }}} *)
let V_CELL1_SINGLE = 
prove_by_refinement( `!V vl. saturated V /\ packing V /\ barV V 3 vl ==> V INTER (mcell1 V vl) SUBSET {HD vl}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;Pack_defs.mcell1;IN_DIFF;SUBSET;IN_SING]; REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM MP_TAC; COND_CASES_TAC; DISCH_TAC; TYPIFY `x IN cball(HD vl,sqrt(&2))` (C SUBGOAL_THEN MP_TAC); FIRST_X_ASSUM MP_TAC; BY(SET_TAC[]); REWRITE_TAC[cball;IN_ELIM_THM]; TYPIFY `sqrt(&2) < sqrt(&4)` (C SUBGOAL_THEN MP_TAC); GMATCH_SIMP_TAC SQRT_MONO_LT_EQ; BY(REAL_ARITH_TAC); REWRITE_TAC[Collect_geom2.SQRT4_EQ2]; FIRST_X_ASSUM_ST `packing` MP_TAC; REWRITE_TAC[Sphere.packing]; TYPIFY `HD vl IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;SUBSET;IN;Packing3.BARV_IMP_HD_IN_SET_OF_LIST]); BY(ASM_MESON_TAC[IN;arith `&2 <= d /\ d <= s /\ s < &2 ==> F`]); BY(REWRITE_TAC[NOT_IN_EMPTY]) ]);;
(* }}} *)
let EDGE_IMP_K2 = 
prove_by_refinement( `!V vl k. saturated V /\ packing V /\ barV V 3 vl /\ (k <= 1) ==> (edgeX V (mcell k V vl) = {})`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; ASM_REWRITE_TAC[EXTENSION;Pack_defs.mcell;NOT_IN_EMPTY;Pack_defs.edgeX;IN_ELIM_THM;IN_INSERT]; REPEAT WEAK_STRIP_TAC; REPEAT (FIRST_X_ASSUM_ST `mcell0` MP_TAC); COND_CASES_TAC; INTRO_TAC V_CELL0_EMPTY [`V`;`vl`]; INTRO_TAC HDTFNFZ_SUBSET [`V`;`vl`;`0`;`mcell 0 V vl`]; ASM_REWRITE_TAC[Pack_defs.mcell]; BY(SET_TAC[IN]); TYPIFY `k=1` (C SUBGOAL_THEN ASSUME_TAC); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); ASM_REWRITE_TAC[]; INTRO_TAC HDTFNFZ_SUBSET [`V`;`vl`;`1`;`mcell 1 V vl`]; ASM_REWRITE_TAC[Pack_defs.mcell;arith `~(1=0)`]; INTRO_TAC V_CELL1_SINGLE [`V`;`vl`]; ASM_REWRITE_TAC[]; REWRITE_TAC[SUBSET;IN_SING;IN_INTER]; REPEAT WEAK_STRIP_TAC; BY(ASM_MESON_TAC[IN]) ]);;
(* }}} *) (* DEC 31, 2012 *) (* 2 CELL EXPLICIT *)
let MCELL2_VERTEX = 
prove_by_refinement( `!V ul. saturated V /\ packing V /\ barV V 3 ul ==> VX V (mcell2 V ul) SUBSET {EL 0 ul,EL 1 ul}`,
(* {{{ proof *) [ REWRITE_TAC[SUBSET]; REPEAT WEAK_STRIP_TAC; TYPIFY `set_of_list (truncate_simplex 1 ul) = {EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN ASSUME_TAC); TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN MP_TAC); BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1 = 4`]); DISCH_THEN (MP_TAC o (MATCH_MP LENGTH4)); BY(MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list2_explicit]); INTRO_TAC Rogers.XYOFCGX [`V`;`{EL 0 ul,EL 1 ul}`;`circumcenter {EL 0 ul,EL 1 ul}`]; INTRO_TAC Urrphbz1.MCELL_2_PROPERTIES_lemma1 [`V`;`ul`;`0`;`x`]; INTRO_TAC HDTFNFZ_SUBSET [`V`;`ul`;`2`;`mcell2 V ul`]; ASM_REWRITE_TAC[]; ANTS_TAC; BY(REWRITE_TAC[Pack_defs.mcell;arith `~(2 = 0) /\ ~(2 = 1)`]); DISCH_TAC; TYPIFY `x IN V /\ x IN mcell2 V ul` (C SUBGOAL_THEN MP_TAC); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); WEAK_STRIP_TAC; ASM_REWRITE_TAC[]; DISCH_TAC; REWRITE_TAC[Rogers.CIRCUMCENTER_2]; ANTS_TAC; CONJ_TAC; MATCH_MP_TAC SUBSET_TRANS; TYPIFY `set_of_list ul` EXISTS_TAC; CONJ_TAC; GMATCH_SIMP_TAC set_of_list4; CONJ2_TAC; BY(SET_TAC[]); BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]); BY(ASM_MESON_TAC[Packing3.BARV_SUBSET]); CONJ_TAC; BY(REWRITE_TAC[AFFINE_INDEPENDENT_2]); FIRST_X_ASSUM_ST `mcell2` MP_TAC; REWRITE_TAC[Pack_defs.mcell2]; REWRITE_TAC[Pack_defs.HL]; COND_CASES_TAC THEN REWRITE_TAC[NOT_IN_EMPTY]; DISCH_THEN kill; FIRST_X_ASSUM MP_TAC; MATCH_MP_TAC (arith `x = x' ==> (x < y /\ z ==> x' < y)`); BY(ASM_REWRITE_TAC[]); REWRITE_TAC[IN_DIFF]; DISCH_THEN (C INTRO_TAC [`EL 0 ul`;`x`]); REPEAT WEAK_STRIP_TAC; PROOF_BY_CONTR_TAC; FIRST_X_ASSUM_ST `dist` MP_TAC; ANTS_TAC; ASM_REWRITE_TAC[]; BY(SET_TAC[]); FIRST_X_ASSUM_ST `dist` (MP_TAC o (ONCE_REWRITE_RULE[DIST_SYM])); TYPIFY ` hl(truncate_simplex 1 ul) = dist(HD ul,midpoint (HD ul,HD (TL ul)))` ENOUGH_TO_SHOW_TAC; DISCH_THEN SUBST1_TAC; REWRITE_TAC[EL;arith `1 = SUC 0`]; BY(REAL_ARITH_TAC); TYPIFY ` (truncate_simplex 1 ul) = [EL 0 ul; EL 1 ul]` (C SUBGOAL_THEN SUBST1_TAC); TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN MP_TAC); BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1 = 4`]); DISCH_THEN (MP_TAC o (MATCH_MP LENGTH4)); BY(MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1]); ASM_REWRITE_TAC[Marchal_cells_3.HL_2]; REWRITE_TAC[DIST_MIDPOINT]; REWRITE_TAC[EL;arith `1 = SUC 0`]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let MCELL2_EDGE = 
prove_by_refinement( `!V ul e. saturated V /\ packing V /\ barV V 3 ul /\ edgeX V (mcell2 V ul) e ==> e = {EL 0 ul, EL 1 ul}`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM]; REPEAT WEAK_STRIP_TAC; INTRO_TAC MCELL2_VERTEX [`V`;`ul`]; ASM_REWRITE_TAC[]; REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND]; REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY]; DISCH_TAC; FIRST_ASSUM (C INTRO_TAC [`u`]); FIRST_X_ASSUM (C INTRO_TAC [`v`]); BY(ASM_MESON_TAC[IN]) ]);;
(* }}} *) (* 3 AND 4 CELL EXPLICIT *)
let MCELL4 = 
prove_by_refinement( `!V ul. mcell4 V ul = mcell 4 V ul`,
(* {{{ proof *) [ BY(REWRITE_TAC[Pack_defs.mcell;arith `~(4 =0) /\ ~(4 = 1) /\ ~(4=2) /\ ~(4=3)`]) ]);;
(* }}} *)
let MCELL3 = 
prove_by_refinement( `!V ul. mcell3 V ul = mcell 3 V ul`,
(* {{{ proof *) [ BY(REWRITE_TAC[Pack_defs.mcell;arith `~(3 =0) /\ ~(3 = 1) /\ ~(3=2)`]) ]);;
(* }}} *)
let MCELL2 = 
prove_by_refinement( `!V ul. mcell2 V ul = mcell 2 V ul`,
(* {{{ proof *) [ BY(REWRITE_TAC[Pack_defs.mcell;arith `~(2 =0) /\ ~(2 = 1)`]) ]);;
(* }}} *)
let MCELL1 = 
prove_by_refinement( `!V ul. mcell1 V ul = mcell 1 V ul`,
(* {{{ proof *) [ BY(REWRITE_TAC[Pack_defs.mcell;arith `~(1 =0)`]) ]);;
(* }}} *)
let MCELL0 = 
prove_by_refinement( `!V ul. mcell0 V ul = mcell 0 V ul`,
(* {{{ proof *) [ BY(REWRITE_TAC[Pack_defs.mcell;arith `~(1 =0)`]) ]);;
(* }}} *)
let MCELL_CELL_PARAMETERS_EXIST = 
prove_by_refinement( `!V ul k X. (k <= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==> FST (cell_params V X) = k`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.cell_params]; REPEAT WEAK_STRIP_TAC; SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[BETA_ORDERED_PAIR_THM]); INTRO_TAC Ajripqn.AJRIPQN [`V`;`ul`;`SND t`;`k`;`FST t`]; REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY;arith `x = 0 \/ x = 1 \/ x = 2 \/ x = 3 \/ x = 4 <=> x <= 4`]; REWRITE_TAC[IN]; REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM_ST `==>` MP_TAC; ANTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[INTER_IDEMPOT]); BY(DISCH_THEN (unlist REWRITE_TAC)); REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[NOT_EXISTS_THM]; DISCH_THEN (C INTRO_TAC [`k,ul`]); BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let MCELL4_CELL_PARAMETERS_EXIST = 
prove_by_refinement( `!V ul X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==> FST (cell_params V X) = 4`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL4;arith `4 <= 4`]; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let MCELL3_CELL_PARAMETERS_EXIST = 
prove_by_refinement( `!V ul X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==> FST (cell_params V X) = 3`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL3;arith `3 <= 4`]; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let MCELL2_CELL_PARAMETERS_EXIST = 
prove_by_refinement( `!V ul X. packing V /\ saturated V /\ (X = mcell2 V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==> FST (cell_params V X) = 2`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL2;arith `2 <= 4`]; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let MCELL_PARAM_UL = 
prove_by_refinement( `!V ul vl X k. (k<= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\ vl = SND (cell_params V X) ==> (X = mcell k V vl /\ vl IN barV V 3)`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.cell_params]; REPEAT WEAK_STRIP_TAC; INTRO_TAC MCELL_CELL_PARAMETERS_EXIST [`V`;`ul`;`k`;`X`]; ASM_REWRITE_TAC[]; REWRITE_TAC[Pack_defs.cell_params]; WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[BETA_ORDERED_PAIR_THM]); WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[BETA_ORDERED_PAIR_THM]); REPEAT WEAK_STRIP_TAC; CONJ_TAC; BY(MESON_TAC[]); REPEAT WEAK_STRIP_TAC; CONJ_TAC; BY(ASM_MESON_TAC[]); REWRITE_TAC[NOT_EXISTS_THM]; DISCH_THEN (C INTRO_TAC [`k,ul`]); BY(ASM_MESON_TAC[FST;SND]) ]);;
(* }}} *)
let MCELL4_PARAM_UL = 
prove_by_refinement( `!V ul vl X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\ vl = SND (cell_params V X) ==> (X = mcell4 V (vl) /\ vl IN barV V 3)`,
(* {{{ proof *) [ REWRITE_TAC[MCELL4]; REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL; BY(ASM_MESON_TAC[arith `4 <= 4`]) ]);;
(* }}} *)
let MCELL3_PARAM_UL = 
prove_by_refinement( `!V ul vl X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\ vl = SND (cell_params V X) ==> (X = mcell3 V (vl) /\ vl IN barV V 3)`,
(* {{{ proof *) [ REWRITE_TAC[MCELL3]; REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL; BY(ASM_MESON_TAC[arith `3 <= 4`]) ]);;
(* }}} *)
let MCELL2_PARAM_UL = 
prove_by_refinement( `!V ul vl X. packing V /\ saturated V /\ (X = mcell2 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\ vl = SND (cell_params V X) ==> (X = mcell2 V (vl) /\ vl IN barV V 3)`,
(* {{{ proof *) [ REWRITE_TAC[MCELL2]; REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL; BY(ASM_MESON_TAC[arith `2 <= 4`]) ]);;
(* }}} *)
let MCELL4_VX = 
prove_by_refinement( `!V ul X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ul IN barV V 3 ==> VX V X SUBSET (set_of_list (SND (cell_params V X)))`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.VX]; REPEAT WEAK_STRIP_TAC; COND_CASES_TAC; BY(REWRITE_TAC[EMPTY_SUBSET]); REWRITE_TAC[LET_DEF;LET_END_DEF]; REWRITE_TAC[BETA_ORDERED_PAIR_THM]; INTRO_TAC MCELL4_CELL_PARAMETERS_EXIST [`V`;`ul`;`X`]; ASM_REWRITE_TAC[]; DISCH_TAC; ASM_REWRITE_TAC[arith `~(4 = 0) /\ 4 - 1 = 3`]; MATCH_MP_TAC (MESON[SUBSET_REFL] `a = b ==> a SUBSET b`); AP_TERM_TAC; INTRO_TAC MCELL4_PARAM_UL [`V`;`ul`;`SND (cell_params V X)`;`X`]; ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC; MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_REFL; BY(ASM_MESON_TAC[Sphere.BARV;IN]) ]);;
(* }}} *)
let MCELL3_VX = 
prove_by_refinement( `!V ul X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ul IN barV V 3 ==> VX V X SUBSET (set_of_list (truncate_simplex 2 (SND (cell_params V X))))`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.VX]; REPEAT WEAK_STRIP_TAC; COND_CASES_TAC; BY(REWRITE_TAC[EMPTY_SUBSET]); REWRITE_TAC[LET_DEF;LET_END_DEF]; REWRITE_TAC[BETA_ORDERED_PAIR_THM]; INTRO_TAC MCELL3_CELL_PARAMETERS_EXIST [`V`;`ul`;`X`]; ASM_REWRITE_TAC[]; DISCH_TAC; ASM_REWRITE_TAC[arith `~(3 = 0) /\ 2 = 3 - 1`]; BY(SET_TAC[]) ]);;
(* }}} *)
let MCELL4_SET_OF_LIST_VX = 
prove_by_refinement( `!V ul X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ~(NULLSET X) /\ barV V 3 ul ==> set_of_list ul = V INTER X`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; TYPIFY `set_of_list ul SUBSET V INTER X /\ V INTER X = VX V X /\ VX V X SUBSET set_of_list (SND (cell_params V X)) /\ CARD (set_of_list (SND (cell_params V X))) <= 4 /\ CARD (set_of_list ul) = 4` ENOUGH_TO_SHOW_TAC; REPEAT WEAK_STRIP_TAC; TYPIFY `set_of_list ul = set_of_list (SND (cell_params V X))` ENOUGH_TO_SHOW_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); MATCH_MP_TAC CARD_SUBSET_LE; CONJ_TAC; BY(REWRITE_TAC[FINITE_SET_OF_LIST]); CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); CONJ_TAC; REWRITE_TAC[SUBSET_INTER]; CONJ_TAC; MATCH_MP_TAC Packing3.BARV_SUBSET; BY(ASM_MESON_TAC[]); FIRST_X_ASSUM_ST `NULLSET` MP_TAC; ASM_REWRITE_TAC[Pack_defs.mcell4]; COND_CASES_TAC; BY(REWRITE_TAC[HULL_SUBSET]); BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]); COMMENT "goal 2";
CONJ_TAC; BY(ASM_MESON_TAC[HDTFNFZ_ALT;MCELL4]); CONJ_TAC; MATCH_MP_TAC MCELL4_VX; BY(ASM_MESON_TAC[IN]); CONJ_TAC; TYPIFY `LENGTH (SND (cell_params V X)) = 4` ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[Geomdetail.CARD_SET_OF_LIST_LE]); INTRO_TAC MCELL4_PARAM_UL [`V`;`ul`;`SND(cell_params V X)`;`X`]; ASM_REWRITE_TAC[]; ANTS_TAC; BY(ASM_REWRITE_TAC[IN]); BY(MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]); REWRITE_TAC[arith `4 = 3 + 1`]; MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA; BY(ASM_MESON_TAC[]) ]);; (* }}} *)
let MCELL3_SET_OF_LIST_VX = 
prove_by_refinement( `!V ul X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ~(NULLSET X) /\ barV V 3 ul ==> set_of_list (truncate_simplex 2 ul) = V INTER X`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; TYPIFY `set_of_list (truncate_simplex 2 ul) SUBSET V INTER X /\ V INTER X = VX V X /\ VX V X SUBSET set_of_list (truncate_simplex 2 (SND (cell_params V X))) /\ CARD (set_of_list (truncate_simplex 2 (SND (cell_params V X)))) <= 3 /\ CARD (set_of_list (truncate_simplex 2 ul)) = 3` ENOUGH_TO_SHOW_TAC; REPEAT WEAK_STRIP_TAC; TYPIFY `set_of_list (truncate_simplex 2 ul) = set_of_list (truncate_simplex 2 (SND (cell_params V X)))` ENOUGH_TO_SHOW_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); MATCH_MP_TAC CARD_SUBSET_LE; CONJ_TAC; BY(REWRITE_TAC[FINITE_SET_OF_LIST]); CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); COMMENT "list of conjunts";
CONJ_TAC; REWRITE_TAC[SUBSET_INTER]; CONJ_TAC; MATCH_MP_TAC SUBSET_TRANS; TYPIFY `set_of_list ul` EXISTS_TAC; CONJ_TAC; MATCH_MP_TAC Rogers.SET_OF_LIST_TRUNCATE_SIMPLEX_SUBSET; BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 + 1 <= 3 + 1`]); MATCH_MP_TAC Packing3.BARV_SUBSET; BY(ASM_MESON_TAC[]); FIRST_X_ASSUM_ST `NULLSET` MP_TAC; ASM_REWRITE_TAC[Pack_defs.mcell3]; COND_CASES_TAC; DISCH_TAC; MATCH_MP_TAC SUBSET_TRANS; TYPIFY `set_of_list (truncate_simplex 2 ul) UNION {mxi V ul}` EXISTS_TAC; CONJ_TAC; BY(SET_TAC[]); BY(REWRITE_TAC[HULL_SUBSET]); BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]); COMMENT "goal 2"; CONJ_TAC; BY(ASM_MESON_TAC[HDTFNFZ_ALT;MCELL3]); CONJ_TAC; MATCH_MP_TAC MCELL3_VX; BY(ASM_MESON_TAC[IN]); CONJ_TAC; TYPIFY `2+1 <= LENGTH (SND (cell_params V X))` ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[Geomdetail.CARD_SET_OF_LIST_LE;Packing3.LENGTH_TRUNCATE_SIMPLEX;arith `2+1= 3 /\ 2 + 1 <= 2+1`]); INTRO_TAC MCELL3_PARAM_UL [`V`;`ul`;`SND(cell_params V X)`;`X`]; ASM_REWRITE_TAC[]; ANTS_TAC; BY(ASM_REWRITE_TAC[IN]); BY(MESON_TAC[Sphere.BARV;IN;arith `2 + 1 <= 3+1`]); INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`]; ASM_REWRITE_TAC[]; TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]); FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP LENGTH4)); FIRST_X_ASSUM SUBST1_TAC; REWRITE_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_2]; REWRITE_TAC[set_of_list3_explicit;set_of_list4_explicit]; TYPED_ABBREV_TAC `(s:real^3 -> bool) = {EL 0 ul, EL 1 ul, EL 2 ul}` ; TYPIFY ` {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul} = (EL 3 ul) INSERT s ` (C SUBGOAL_THEN SUBST1_TAC); EXPAND_TAC "s"; BY(SET_TAC[]); GMATCH_SIMP_TAC (CONJUNCT2 CARD_CLAUSES); CONJ_TAC; BY(ASM_MESON_TAC[FINITE_EMPTY;FINITE_INSERT]); COND_CASES_TAC; BY(ASM_MESON_TAC[Geomdetail.CARD3;arith `~( 3 + 1 <= 3)`]); BY(ARITH_TAC) ]);; (* }}} *)
let MCELL4_EDGE = 
prove_by_refinement( `!V ul u v. packing V /\ saturated V /\ ~NULLSET (mcell4 V ul) /\ barV V 3 ul ==> ({u,v} IN edgeX V (mcell4 V ul) <=> (~(u= v) /\ {u,v} SUBSET set_of_list ul))`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM]; INTRO_TAC HDTFNFZ_ALT [`V`;`ul`;`4`;`mcell4 V ul`]; ANTS_TAC; BY(ASM_REWRITE_TAC[MCELL4]); DISCH_THEN SUBST1_TAC; INTRO_TAC (GSYM MCELL4_SET_OF_LIST_VX) [`V`;`ul`;`mcell4 V ul`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_THEN SUBST1_TAC; REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;Geomdetail.PAIR_EQ_EXPAND]; BY(MESON_TAC[IN]) ]);;
(* }}} *)
let MCELL3_EDGE = 
prove_by_refinement( `!V ul u v. packing V /\ saturated V /\ ~NULLSET (mcell3 V ul) /\ barV V 3 ul ==> ({u,v} IN edgeX V (mcell3 V ul) <=> (~(u= v) /\ {u,v} SUBSET (set_of_list(truncate_simplex 2 ul))))`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM]; INTRO_TAC HDTFNFZ_ALT [`V`;`ul`;`3`;`mcell3 V ul`]; ANTS_TAC; BY(ASM_REWRITE_TAC[MCELL3]); DISCH_THEN SUBST1_TAC; INTRO_TAC (GSYM MCELL3_SET_OF_LIST_VX) [`V`;`ul`;`mcell3 V ul`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_THEN SUBST1_TAC; REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;Geomdetail.PAIR_EQ_EXPAND]; BY(MESON_TAC[IN]) ]);;
(* }}} *)
let EDGE_MCELL_EL = 
prove_by_refinement( `!V X e. e IN edgeX V X ==> (?u v. e = {u,v} /\ ~(u=v))`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM]; BY(MESON_TAC[]) ]);;
(* }}} *)
let MCELL_EDGE = 
prove_by_refinement( `!V ul k e. (k < 4) /\ packing V /\ saturated V /\ ~NULLSET (mcell k V ul) /\ barV V 3 ul /\ e IN edgeX V (mcell k V ul) ==> e SUBSET (set_of_list(truncate_simplex 2 ul))`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Sphere.BARV;arith `3 + 1 = 4`]); TYPIFY `k = 3 \/ k = 2 \/ k <= 1` (C SUBGOAL_THEN MP_TAC); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); INTRO_TAC EDGE_MCELL_EL [`V`;`mcell k V ul`;`e`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); WEAK_STRIP_TAC; ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC; INTRO_TAC MCELL3_EDGE [`V`;`ul`;`u`;`v`]; BY(ASM_MESON_TAC[MCELL3]); INTRO_TAC MCELL2_EDGE [`V`;`ul`;`e`]; ANTS_TAC; BY(ASM_MESON_TAC[IN;MCELL2]); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; GMATCH_SIMP_TAC SET_OF_LIST_TRUNCATE_2; ASM_REWRITE_TAC[]; CONJ_TAC; BY(ARITH_TAC); BY(SET_TAC[]); INTRO_TAC EDGE_IMP_K2 [`V`;`ul`;`k`]; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[NOT_IN_EMPTY]) ]);;
(* }}} *) (* let MCELL_BUMP_0 = prove_by_refinement( `!V ul e k. (k < 4 ) /\ packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell k V ul) ==> beta_bumpA V e (mcell k V ul) = &0`, (* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[Pack_defs.beta_bumpA]; REWRITE_TAC[LET_DEF;LET_END_DEF]; REWRITE_TAC[BETA_ORDERED_PAIR_THM]; INTRO_TAC MCELL_CELL_PARAMETERS_EXIST [`V`;`ul`;`k`;`mcell k V ul`]; ANTS_TAC; BY(ASM_SIMP_TAC[arith `k < 4 ==> k <= 4`;IN]); DISCH_THEN SUBST1_TAC; ASM_SIMP_TAC[arith `k < 4 ==> ~(k=4)`]; REWRITE_TAC[GSPEC;SETSPEC]; BY(REWRITE_TAC[SYM EMPTY;SUM_CLAUSES]) ]);; (* }}} *) *)
let CARD2_EDGEX = 
prove_by_refinement( `!V X e. e IN edgeX V X ==> CARD e = 2`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM]; REPEAT WEAK_STRIP_TAC; ASM_REWRITE_TAC[]; BY(ASM_SIMP_TAC[Hypermap.CARD_TWO_ELEMENTS]) ]);;
(* }}} *)
let DIFF_EDGEX = 
prove_by_refinement( `!V X ul k e. (k < 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ~NULLSET X /\ barV V 3 ul /\ e IN edgeX V X ==> ~((VX V X DIFF e) IN edgeX V X)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; ABBREV_TAC `e' = (VX V X DIFF e)`; INTRO_TAC MCELL_EDGE [`V`;`ul`;`k`;`e`]; ANTS_TAC; BY(ASM_MESON_TAC[]); INTRO_TAC MCELL_EDGE [`V`;`ul`;`k`;`e'`]; ANTS_TAC; BY(ASM_MESON_TAC[]); REPEAT WEAK_STRIP_TAC; REPEAT (FIRST_X_ASSUM_ST `set_of_list` MP_TAC); TYPIFY `3 <= LENGTH ul` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 <= 3 + 1`]); ASM_SIMP_TAC[ SET_OF_LIST_TRUNCATE_2]; REPEAT WEAK_STRIP_TAC; INTRO_TAC Geomdetail.CARD3 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`]; REPEAT WEAK_STRIP_TAC; INTRO_TAC CARD_UNION_GEN [`e`;`e'`]; TYPIFY `e INTER e' = {}` ((C SUBGOAL_THEN SUBST1_TAC)); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); REWRITE_TAC[CARD_CLAUSES;arith `x - 0 = x`]; TYPIFY `FINITE {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN MP_TAC); BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]); DISCH_TAC; DISCH_THEN ( MP_TAC) THEN ANTS_TAC; BY(ASM_MESON_TAC[FINITE_SUBSET]); TYPIFY `CARD (e UNION e') <= CARD {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC CARD_SUBSET; BY(ASM_REWRITE_TAC[UNION_SUBSET]); REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP CARD2_EDGEX))); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC) ]);;
(* }}} *)
let CRITICAL_EDGEX_ALT = 
prove_by_refinement( `!V X e. e IN critical_edgeX V X <=> e IN edgeX V X /\ hminus <= radV e /\ radV e <= hplus `,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.critical_edgeX;Pack_defs.HL;Pack_defs.edgeX]; REWRITE_TAC[IN_ELIM_THM;set_of_list2_explicit]; BY(MESON_TAC[]) ]);;
(* }}} *)
let SUBCRITICAL_EDGEX_ALT = 
prove_by_refinement( `!V X e. e IN subcritical_edgeX V X <=> e IN edgeX V X /\ radV e < hminus `,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.subcritical_edgeX;Pack_defs.HL;Pack_defs.edgeX]; REWRITE_TAC[IN_ELIM_THM;set_of_list2_explicit]; BY(MESON_TAC[]) ]);;
(* }}} *)
let MCELL_BUMP_0 = 
prove_by_refinement( `!V ul e k. (k < 4 ) /\ packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell k V ul) ==> beta_bump_v1 V e (mcell k V ul) = &0`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.beta_bump_v1]; REPEAT WEAK_STRIP_TAC; ABBREV_TAC `e' = VX V (mcell k V ul) DIFF e`; REWRITE_TAC[LET_DEF;LET_END_DEF]; REWRITE_TAC[CRITICAL_EDGEX_ALT;IN_ELIM_THM]; COND_CASES_TAC; BY(ASM_MESON_TAC[DIFF_EDGEX]); BY(REWRITE_TAC[]) ]);;
(* }}} *)
let MCELL4_EDGE_OPP = 
prove_by_refinement( `!V ul. packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell4 V ul) ==> VX V (mcell4 V ul) DIFF {EL 0 ul, EL 1 ul} = {EL 2 ul, EL 3 ul}`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; ABBREV_TAC `e' = VX V (mcell4 V ul) DIFF {EL 0 ul, EL 1 ul}`; TYPIFY `VX V (mcell4 V ul) = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC Hdtfnfz.HDTFNFZ; CONJ_TAC; BY(ASM_MESON_TAC[MCELL4]); MATCH_MP_TAC (GSYM MCELL4_SET_OF_LIST_VX); BY(ASM_MESON_TAC[MCELL4]); INTRO_TAC set_of_list4 [`ul`]; ANTS_TAC; BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]); DISCH_TAC; TYPIFY `e' SUBSET {EL 2 ul, EL 3 ul}` (C SUBGOAL_THEN ASSUME_TAC); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); TYPIFY `e' = {EL 2 ul,EL 3 ul}` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC CARD_SUBSET_LE; ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]; INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`]; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[arith `3 + 1 = 4`]; INTRO_TAC Hypermap.CARD_MINUS_DIFF_TWO_SET [`{EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul}`;`EL 0 ul`;`EL 1 ul`]; REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]; ANTS_TAC; BY(SET_TAC[]); ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC; MATCH_MP_TAC (arith `v <= 2 /\ 2 <= x ==> v <= x`); REWRITE_TAC[Geomdetail.CARD2]; MATCH_MP_TAC (arith `(?u. 4 = x + u /\ u <= 2) ==> 2 <= x`); TYPIFY `CARD {EL 0 ul, EL 1 ul}` EXISTS_TAC; CONJ_TAC; BY(ASM_MESON_TAC[]); BY(REWRITE_TAC[Geomdetail.CARD2]); BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let MCELL_BUMP_OPP = 
prove_by_refinement( `!V ul. packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell4 V ul) /\ ~({EL 2 ul,EL 3 ul} IN critical_edgeX V (mcell4 V ul)) ==> beta_bump_v1 V {EL 0 ul,EL 1 ul} (mcell4 V ul) = &0 `,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.beta_bump_v1]; REPEAT WEAK_STRIP_TAC; INTRO_TAC MCELL4_EDGE_OPP [`V`;`ul`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_THEN SUBST1_TAC; REWRITE_TAC[LET_DEF;LET_END_DEF]; BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let BETA_BUMP_NZ = 
prove_by_refinement( `!V ul e e'. packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell4 V ul) /\ (e = {EL 0 ul, EL 1 ul}) /\ (e' = {EL 2 ul, EL 3 ul}) /\ (e IN critical_edgeX V (mcell4 V ul)) /\ (e' IN critical_edgeX V (mcell4 V ul)) /\ (!f. f IN edgeX V (mcell4 V ul) ==> (f = e \/ f = e' \/ f IN subcritical_edgeX V (mcell4 V ul))) ==> beta_bump_v1 V e (mcell4 V ul) = bump (radV e) - bump (radV e')`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; INTRO_TAC MCELL4_EDGE_OPP [`V`;`ul`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; ASM_REWRITE_TAC[Pack_defs.beta_bump_v1]; ASM_REWRITE_TAC[LET_DEF;LET_END_DEF]; COND_CASES_TAC; BY(REWRITE_TAC[]); PROOF_BY_CONTR_TAC; FIRST_X_ASSUM_ST `mcell4` MP_TAC; REWRITE_TAC[]; CONJ_TAC; REWRITE_TAC[MCELL4;Pack_defs.mcell_set;IN_ELIM_THM]; BY(ASM_MESON_TAC[IN]); CONJ_TAC; BY(ASM_MESON_TAC[]); BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let BETA_BUMP_INVOLUTION = 
prove_by_refinement( `!V X r e. saturated V /\ packing V /\ mcell_set V X /\ e IN critical_edgeX V X /\ (\e. VX V X DIFF e) = r ==> r ( r e) = e`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; EXPAND_TAC "r";
TYPIFY `e SUBSET VX V X` ENOUGH_TO_SHOW_TAC; BY(SET_TAC[]); FIRST_X_ASSUM_ST `IN` MP_TAC; REWRITE_TAC[CRITICAL_EDGEX_ALT]; REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM]; BY(SET_TAC[]) ]);; (* }}} *) (* let BETA_BUMP_INVOLUTION = prove_by_refinement( `!V X r e. saturated V /\ packing V /\ mcell_set V X /\ e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) /\ (\e. VX V X DIFF e) = r ==> r ( r e) = e`, (* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; EXPAND_TAC "r"; TYPIFY `e SUBSET VX V X` ENOUGH_TO_SHOW_TAC; BY(SET_TAC[]); FIRST_X_ASSUM_ST `IN` MP_TAC; REWRITE_TAC[CRITICAL_EDGEX_ALT]; REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM]; BY(SET_TAC[]) ]);; (* }}} *) *)
let BETA_BUMP_ALT = 
prove_by_refinement( `!V X r e. saturated V /\ packing V /\ mcell_set V X /\ (\e. VX V X DIFF e) = r ==> beta_bump_v1 V e X = if ~(NULLSET X) /\ e IN critical_edgeX V X /\ r e IN critical_edgeX V X /\ (!f. f IN edgeX V X ==> f = e \/ f = (r e) \/ f IN subcritical_edgeX V X) then bump (radV e) - bump (radV (r e)) else &0`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[Pack_defs.beta_bump_v1]; REWRITE_TAC[Pack_defs.beta_bump_v1;LET_DEF;LET_END_DEF]; EXPAND_TAC "r";
BY(ASM_REWRITE_TAC[IN]) ]);; (* }}} *)
let BETA_BUMP_INVOLUTION_CRITICAL = 
prove_by_refinement( `!V X r e. saturated V /\ packing V /\ mcell_set V X /\ e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) /\ (\e. VX V X DIFF e) = r ==> r e IN critical_edgeX V X`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; PROOF_BY_CONTR_TAC; INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`e`]; BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let BETA_BUMP_INVOLUTION_NEG = 
prove_by_refinement( `!V X r e. saturated V /\ packing V /\ mcell_set V X /\ e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) /\ (\e. VX V X DIFF e) = r ==> beta_bump_v1 V (r e) X = -- beta_bump_v1 V e X`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; INTRO_TAC BETA_BUMP_INVOLUTION_CRITICAL [`V`;`X`;`r`;`e`]; ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`e`]; ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`r e`]; ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; TYPIFY `r (r e) = e` (C SUBGOAL_THEN SUBST1_TAC); INTRO_TAC BETA_BUMP_INVOLUTION [`V`;`X`;`r`;`e`]; DISCH_THEN MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); REPEAT COND_CASES_TAC; BY(REAL_ARITH_TAC); BY(ASM_MESON_TAC[]); BY(ASM_MESON_TAC[]); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let BETA_BUMP_INVOLUTION_BIJ = 
prove_by_refinement( `!V X s r. saturated V /\ packing V /\ mcell_set V X /\ ({e | e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) } = s ) /\ (\e. VX V X DIFF e) = r ==> BIJ r s s`,
(* {{{ proof *) [ REWRITE_TAC[BIJ;INJ]; REPEAT WEAK_STRIP_TAC; SUBCONJ_TAC; CONJ_TAC; GEN_TAC; EXPAND_TAC "s";
REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAK_STRIP_TAC; BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION_NEG;arith `(-- x = &0 <=> x = &0)`; BETA_BUMP_INVOLUTION_CRITICAL]); EXPAND_TAC "s"; REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAK_STRIP_TAC; TYPIFY `r ( r x) = r ( r y)` (C SUBGOAL_THEN ASSUME_TAC); AP_TERM_TAC; BY(ASM_REWRITE_TAC[]); BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION]); DISCH_TAC; REWRITE_TAC[SURJ]; ASM_REWRITE_TAC[]; EXPAND_TAC "s"; REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAK_STRIP_TAC; TYPIFY `r x` EXISTS_TAC; SUBCONJ_TAC; FIRST_X_ASSUM_ST `==>` MP_TAC; EXPAND_TAC "s"; REWRITE_TAC[IN_ELIM_THM]; BY(ASM_MESON_TAC[]); DISCH_TAC; BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION]) ]);; (* }}} *)
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_v1 V e X) = &0`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; ABBREV_TAC `s = {e | e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) } `; INTRO_TAC SUM_SUPERSET [`(\e. beta_bump_v1 V e X)`;`s`;`{e | e IN critical_edgeX V X }`]; ANTS_TAC; EXPAND_TAC "s";
REWRITE_TAC[IN_ELIM_THM;SUBSET]; BY(MESON_TAC[]); DISCH_THEN SUBST1_TAC; ABBREV_TAC `r = (\e. VX V X DIFF e)`; INTRO_TAC BIJ_SUM [`s`;`s`;`(\e. beta_bump_v1 V e X)`;`r`]; ANTS_TAC; BY(ASM_MESON_TAC[ BETA_BUMP_INVOLUTION_BIJ]); INTRO_TAC SUM_EQ [`((\e. beta_bump_v1 V e X) o r)`;`(\e. -- beta_bump_v1 V e X)`;`s`]; ANTS_TAC; EXPAND_TAC "s"; REWRITE_TAC[IN_ELIM_THM]; REWRITE_TAC[o_DEF]; BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION_NEG]); DISCH_THEN SUBST1_TAC; REWRITE_TAC[SUM_NEG]; BY(REAL_ARITH_TAC) ]);; (* }}} *)
let REAL_ABS_TRIANGLE_BOUND = 
prove_by_refinement( `!a b x. a <= x /\ x <= b ==> abs x <= abs a + abs b`,
(* {{{ proof *) [ BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let CRITICAL_EDGEX_BOUND = 
prove_by_refinement( `?c1. !V X e. e IN critical_edgeX V X ==> abs(radV e - h0) <= c1`,
(* {{{ proof *) [ REWRITE_TAC[CRITICAL_EDGEX_ALT]; EXISTS_TAC `abs (hplus) + abs (hminus) + abs (h0)`; REPEAT WEAK_STRIP_TAC; INTRO_TAC REAL_ABS_TRIANGLE_BOUND [`hminus`;`hplus`;`radV e`]; ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let ABS_BUMP = 
prove_by_refinement( `!h c1. abs(h- h0) <= c1 ==> abs(bump h) <= abs (#0.005) * (&1 + (c1 pow 2) / abs((hplus - h0) pow 2))`,
(* {{{ proof *) [ REWRITE_TAC[Pack_defs.bump ]; REPEAT WEAK_STRIP_TAC; REWRITE_TAC[REAL_ABS_MUL]; GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP; CONJ_TAC; BY(REAL_ARITH_TAC); MATCH_MP_TAC (arith ` abs x + abs y <= z ==> abs (x - y) <= z`); REWRITE_TAC[arith `abs(&1) + x <= &1 + y <=> x <= y`]; REWRITE_TAC[REAL_ABS_DIV]; REWRITE_TAC[real_div]; MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL; REWRITE_TAC[REAL_LE_INV_EQ]; CONJ2_TAC; BY(REAL_ARITH_TAC); REWRITE_TAC[REAL_ABS_POW]; MATCH_MP_TAC Collect_geom2.POS_IMP_POW2; ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let BOUND_BETA_BUMP = 
prove_by_refinement( `?c. !V X e. saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X e ==> beta_bump_v1 V e X <= c`,
(* {{{ proof *) [ INTRO_TAC CRITICAL_EDGEX_BOUND []; REPEAT WEAK_STRIP_TAC; EXISTS_TAC `&2 * abs (#0.005) * (&1 + (c1 pow 2) / abs((hplus - h0) pow 2))`; REPEAT WEAK_STRIP_TAC; REWRITE_TAC[Pack_defs.beta_bump_v1;LET_DEF;LET_END_DEF]; COND_CASES_TAC; MATCH_MP_TAC REAL_LE_TRANS; ABBREV_TAC `e' = VX V X DIFF e`; TYPIFY `abs (bump (radV e)) + abs (bump (radV e'))` EXISTS_TAC; CONJ_TAC; BY(REAL_ARITH_TAC); MATCH_MP_TAC (arith `x <= z /\ y <= z ==> x + y <= &2 * z`); BY(ASM_MESON_TAC[ ABS_BUMP]); MATCH_MP_TAC (arith `&0 <= x ==> &0 <= &2 * abs (#0.005) * x`); REWRITE_TAC[real_div]; MATCH_MP_TAC (arith `&0 <= x ==> &0 <= &1 + x`); GMATCH_SIMP_TAC REAL_LE_MUL; REWRITE_TAC[REAL_LE_INV_EQ]; REWRITE_TAC[ REAL_LE_POW_2]; BY(REAL_ARITH_TAC) ]);;
(* }}} *) end;;