1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas Hales *)
8 (* ========================================================================== *)
14 `!V X. saturated V /\ packing V /\ mcell_set V X /\ critical_edge V X = {} ==>
15 gammaX V X lmfun >= &0`,
17 I proved a few lemmas, but I realized that I need RVFXZBU, before going
18 very far, and this still hasn't been formalized.
19 The theorem is needed for the proof that `cell_param (mcell k V ul) = (k,ul)`.
27 let exists_eq = prove_by_refinement(
28 `!P Q. (!(x:A). (P x = Q x)) ==> ((?x. P x) <=> (?x. Q x))`,
35 let mcell_set_alt = prove_by_refinement(
36 `!V X. mcell_set V X = (?ul. (barV V 3 ul) /\ (X = mcell0 V ul \/ X = mcell1 V ul \/ X = mcell2 V ul \/ X = mcell3 V ul \/ X = mcell4 V ul))`,
39 REWRITE_TAC [Pack_defs.mcell_set;IN_ELIM_THM;IN] ;
41 ONCE_REWRITE_TAC[SWAP_EXISTS_THM];
42 MATCH_MP_TAC exists_eq;
45 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
46 MP_TAC (ARITH_RULE `i=0 \/ i=1 \/ i=2 \/ i=3 \/ i>=4`);
47 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC [Marchal_cells_2.MCELL_EXPLICIT];
48 ASM_MESON_TAC [Marchal_cells_2.MCELL_EXPLICIT];
49 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
50 EXISTS_TAC `0` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
51 EXISTS_TAC `1` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
52 EXISTS_TAC `2` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
53 EXISTS_TAC `3` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
54 EXISTS_TAC `4` THEN (MESON_TAC[Marchal_cells_2.MCELL_EXPLICIT;ARITH_RULE `4 >= 4`])
58 let mcell4_convex_hull = prove_by_refinement(
59 `!V X ul. barV V 3 vl /\ hl vl < sqrt(&2) ==> ?u0 u1 u2 u3. (vl = [u0;u1;u2;u3] /\ (mcell4 V vl = convex hull {u0,u1,u2,u3}))`,
63 ASM_REWRITE_TAC [Pack_defs.mcell4];
64 SUBGOAL_THEN `?u0 u1 u2 u3. vl = [(u0:real^3);u1;u2;u3]` (fun t -> MP_TAC t THEN MESON_TAC[set_of_list]);
65 MATCH_MP_TAC Marchal_cells.BARV_3_EXPLICIT;