(* ========================================================================== *)
(* 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;;