(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Author    : VU KHAC KY                                               *)
(*      Book lemma: TSKAJXY                                                  *)
(*      Chapter   : Packing (Clusters)                                       *)
(*      Date: November 2013                                                  *)
(*                                                                           *)
(* ========================================================================= *)


(*

This does the special cases of Lemma TSKAJXY for 0, 3, and 4-cells

*)

module Tskajxy_034 = struct

open Sphere;;
open Euler_main_theorem;;
open Pack_defs;;
open Pack_concl;;
open Pack1;;
open Pack2;;
open Packing3;;
open Rogers;;
open Vukhacky_tactics;;
open Marchal_cells;;
open Emnwuus;;
(* open Marchal_cells_2;; *)
open Marchal_cells_2_new;;
open Urrphbz1;;
open Lepjbdj;;
open Hdtfnfz;;
open Rvfxzbu;;
open Sltstlo;;
open Urrphbz2;;
open Urrphbz3;;
open Ynhyjit;;
open Njiutiu;;
open Tezffsk;;
open Qzksykg;;
open Ddzuphj;;
open Ajripqn;;
open Qzyzmjc;;
open Upfzbzm_support_lemmas;;
open Marchal_cells_3;;
open Grutoti;;
open Kizhltl;;
open Sum_gammax_lmfun_estimate;;
open Upfzbzm;;
open Rdwkarc;;
open Ineq;;
open Merge_ineq;;
open Hales_tactic;;
open Tskajxy_lemmas;;

(* ======================================================================== *)

let cell3_from_ineq = 
 `!y4 y5 y6.
         &2 <= y4 /\
         &2 <= y5 /\
         &2 <= y6 /\
         y4 <= &2 * sqrt (&2) /\
         y5 <= &2 * sqrt (&2) /\
         y6 <= &2 * sqrt (&2) /\
         eta_y y4 y5 y6 < sqrt (&2)
         ==> &0 <= gamma3f y4 y5 y6 sqrt2 lmfun`;;


let GRKIBMP_concl = 
  `!y. &2 <= y /\ y <= sqrt8 ==>
     &0 <= gamma2_x_div_azim_v2 (h0cut y) (y*y)`;;

let tsk_hyp_new = mk_conj(GRKIBMP_concl, 
                              mk_conj(cell3_from_ineq,tsk_hyp));;

let TSKAJXY_statement_special_case = new_definition
   `TSKAJXY_statement_special_case <=>
      (!V X.
          saturated V /\
          packing V /\
          mcell_set V X /\
	  ~(?i ul. ul IN barV V 3 /\ (i = 1 \/ i = 2) /\ X = mcell i V ul) /\
          critical_edgeX V X = {}
          ==> gammaX V X lmfun >= &0)`;;
g (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`));; let TSKAJXY_034 = Prove_by_refinement.prove_by_refinement( (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`)), (* {{{ proof *) [ (STRIP_TAC); (REWRITE_TAC[TSKAJXY_statement_special_case; mcell_set; IN_ELIM_THM]); (REWRITE_TAC[IN]); (REPEAT STRIP_TAC); (ASM_CASES_TAC `NULLSET X`); (REWRITE_TAC[gammaX]); (MATCH_MP_TAC (REAL_ARITH `x = &0 /\ y = &0 /\ z = &0 ==> x - y + z >= &0`)); (REWRITE_TAC[total_solid; REAL_ENTIRE]); (REPEAT STRIP_TAC); (MATCH_MP_TAC MEASURE_EQ_0); BY((ASM_REWRITE_TAC[])); (DISJ2_TAC); (REWRITE_WITH `VX V X = {}`); (REWRITE_TAC[VX]); BY((ASM_REWRITE_TAC[])); BY((REWRITE_TAC[SUM_CLAUSES])); (DISJ2_TAC); (REWRITE_WITH `edgeX V X = {}`); (REWRITE_TAC[edgeX]); (REWRITE_WITH `VX V X = {}`); (REWRITE_TAC[VX]); BY((ASM_REWRITE_TAC[])); (ONCE_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]); BY((SET_TAC[])); BY((REWRITE_TAC[SUM_CLAUSES])); (NEW_GOAL `~(X:real^3->bool = {})`); BY((STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[ASSUME `X:real^3->bool = {}`; NEGLIGIBLE_EMPTY])); (ASM_CASES_TAC `i >= 4`); (NEW_GOAL `X = mcell4 V ul`); (ASM_REWRITE_TAC[]); BY((ASM_SIMP_TAC[MCELL_EXPLICIT])); (UP_ASM_TAC THEN REWRITE_TAC[mcell4]); (COND_CASES_TAC); (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[])); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; set_of_list]); (STRIP_TAC); (ABBREV_TAC `y1 = dist (u0:real^3, u1)`); (ABBREV_TAC `y2 = dist (u0:real^3, u2)`); (ABBREV_TAC `y3 = dist (u0:real^3, u3)`); (ABBREV_TAC `y4 = dist (u2:real^3, u3)`); (ABBREV_TAC `y5 = dist (u1:real^3, u3)`); (ABBREV_TAC `y6 = dist (u1:real^3, u2)`); (NEW_GOAL `VX V X = {u0,u1,u2,u3}`); (REWRITE_WITH `VX V X = V INTER X`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); BY((ASM_REWRITE_TAC[])); (REWRITE_WITH `X = mcell 4 V ul`); (ASM_REWRITE_TAC[]); BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT])); (REWRITE_WITH `V INTER mcell 4 V ul = set_of_list (truncate_simplex (4 - 1) ul)`); (MATCH_MP_TAC Lepjbdj.LEPJBDJ); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]); (REWRITE_WITH ` mcell 4 V [u0; u1; u2; u3] = X`); (ASM_REWRITE_TAC[]); BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT])); BY((ASM_REWRITE_TAC[])); BY((ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list])); (REWRITE_WITH `vol X = vol_y y1 y2 y3 y4 y5 y6 /\ gammaX V X lmfun = gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun`); (MATCH_MP_TAC gammaX_gamm4fgcy); (EXISTS_TAC `ul:(real^3)list`); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`); (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); (EXISTS_TAC `i:num`); BY((ASM_REWRITE_TAC[])); (NEW_GOAL `!y1 y2 y3 y4 y5 y6. ineq [#2.0,y1,sqrt8; #2.0,y2,sqrt8; #2.0,y3,sqrt8; #2.0,y4,sqrt8; #2.0, y5, sqrt8; #2.0,y6,sqrt8] (~critical_edge_y y1 /\ ~critical_edge_y y2 /\ ~critical_edge_y y3 /\ ~critical_edge_y y4 /\ ~critical_edge_y y5 /\ ~critical_edge_y y6 /\ &0 < delta_y y1 y2 y3 y4 y5 y6 /\ rad2_y y1 y2 y3 y4 y5 y6 < &2 ==> gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`); (MATCH_MP_TAC TSKAJXY_DERIVED4); BY((ASM_REWRITE_TAC[])); (UP_ASM_TAC THEN REWRITE_TAC[ineq; MESON[] `a ==> b ==> c <=> (a /\ b) ==> c`] THEN STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `~(critical_edge_y y1) /\ ~(critical_edge_y y2) /\ ~(critical_edge_y y3) /\ ~(critical_edge_y y4) /\ ~(critical_edge_y y5) /\ ~(critical_edge_y y6) /\ &0 < delta_y y1 y2 y3 y4 y5 y6`); (REWRITE_TAC[critical_edge_y]); (REPEAT STRIP_TAC); (NEW_GOAL `{u0:real^3, u1} IN critical_edgeX V X`); (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`); (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`); (ASM_REWRITE_TAC[]); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y1`); (EXPAND_TAC "y1" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u1`; NORM_ARITH `norm (u1 - u1) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]); BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_SET_TAC[])); (NEW_GOAL `{u0:real^3, u2} IN critical_edgeX V X`); (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`); (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`); (ASM_REWRITE_TAC[]); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y2`); (EXPAND_TAC "y2" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]); BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_SET_TAC[])); (NEW_GOAL `{u0:real^3, u3} IN critical_edgeX V X`); (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`); (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`); (ASM_REWRITE_TAC[]); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y3`); (EXPAND_TAC "y3" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]); BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_SET_TAC[])); (NEW_GOAL `{u2:real^3, u3} IN critical_edgeX V X`); (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]); (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); (ASM_REWRITE_TAC[]); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y4`); (EXPAND_TAC "y4" THEN REWRITE_TAC[dist; ASSUME `u2:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]); BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_SET_TAC[])); (NEW_GOAL `{u1:real^3, u3} IN critical_edgeX V X`); (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`); (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`); (ASM_REWRITE_TAC[]); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y5`); (EXPAND_TAC "y5" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]); BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_SET_TAC[])); (NEW_GOAL `{u1:real^3, u2} IN critical_edgeX V X`); (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`); (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`); (ASM_REWRITE_TAC[]); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC); BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[])); (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y6`); (EXPAND_TAC "y6" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]); BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_REAL_ARITH_TAC)); BY((ASM_SET_TAC[])); (REWRITE_WITH `&0 < delta_y y1 y2 y3 y4 y5 y6 <=> &0 < sqrt (delta_y y1 y2 y3 y4 y5 y6)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC SQRT_LT_0); (REWRITE_TAC[delta_y]); (ABBREV_TAC `x1 = y1 * y1` THEN ABBREV_TAC `x2 = y2 * y2`); (ABBREV_TAC `x3 = y3 * y3` THEN ABBREV_TAC `x4 = y4 * y4`); (ABBREV_TAC `x5 = y5 * y5` THEN ABBREV_TAC `x6 = y6 * y6`); (REWRITE_WITH `delta_x x1 x2 x3 x4 x5 x6 = (let a = u1:real^3 - u0 in let b = u2 - u0 in let c = u3 - u0 in &4 * (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 - a$2 * b$1 * c$3 + a$2 * b$3 * c$1 + a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2)`); (MATCH_MP_TAC Delta_x.COMPUTE_DELTA_X); (REWRITE_TAC[xlist; ylist]); (REPEAT LET_TAC); (EXPAND_TAC "x1" THEN EXPAND_TAC "x2" THEN EXPAND_TAC "x3"); (EXPAND_TAC "x4" THEN EXPAND_TAC "x5" THEN EXPAND_TAC "x6"); (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; GSYM REAL_POW_2]); (ASM_REWRITE_TAC[]); (STRIP_TAC); BY((ASM_REWRITE_TAC[])); (REPEAT LET_TAC); (REWRITE_TAC[REAL_ARITH `&0 <= &4 * a <=> &0 <= a`]); BY((REWRITE_TAC[Real_ext.REAL_LE_POW_2])); (ONCE_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 < a / &12`]); (REWRITE_WITH `sqrt (delta_y y1 y2 y3 y4 y5 y6) / &12 = vol (convex hull {u0,u1,u2,u3})`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_TAC[delta_y; GSYM REAL_POW_2]); (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3"); (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6"); BY((REWRITE_TAC[VOLUME_OF_CLOSED_TETRAHEDRON])); (REWRITE_TAC[GSYM (ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`)]); (REWRITE_WITH `&0 < vol X <=> ~NULLSET X`); (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT); (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`]); (MATCH_MP_TAC MEASURABLE_CONVEX_HULL); (MATCH_MP_TAC FINITE_IMP_BOUNDED); BY((REWRITE_TAC[Geomdetail.FINITE6])); BY((ASM_REWRITE_TAC[])); (ASM_REWRITE_TAC[]); (NEW_GOAL `!u v. {u,v} IN edgeX V X ==> (#2.0 <= dist (u,v) /\ dist(u,v) <= sqrt8)`); (REPEAT GEN_TAC); (REWRITE_TAC[edgeX; IN]); (REWRITE_TAC[MESON[IN] `VX V X x <=> x IN VX V X`]); (ASM_REWRITE_TAC[IN_ELIM_THM]); (STRIP_TAC); (MP_TAC (ASSUME `packing V`)); (REWRITE_TAC[packing; REAL_ARITH `#2.0 = &2`] THEN STRIP_TAC); (STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (NEW_GOAL `u:real^3 IN {u0,u1,u2,u3} /\ v IN {u0,u1,u2,u3}`); (DEL_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC); BY((SET_TAC[])); (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`); (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (MATCH_MP_TAC BARV_SUBSET); BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[])); (STRIP_TAC); (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]); BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[])); (STRIP_TAC); (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]); BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[])); (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC); BY((SET_TAC[])); (ABBREV_TAC `s = circumcenter {u0,u1,u2,u3:real^3}`); (NEW_GOAL `dist (u,v:real^3) <= dist (s,u) + dist (s, v)`); BY((NORM_ARITH_TAC)); (NEW_GOAL `!w. w IN {u0,u1,u2,u3:real^3} ==> radV {u0,u1,u2,u3:real^3} = dist (circumcenter {u0,u1,u2,u3:real^3},w)`); (MATCH_MP_TAC Rogers.OAPVION2); (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT); BY((EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[])); (NEW_GOAL `dist (s,u) + dist (s,v:real^3) <= sqrt8`); (REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2; sqrt2]); (MATCH_MP_TAC (REAL_ARITH `a < x /\ b < x ==> a + b <= &2 * x`)); (STRIP_TAC); (REWRITE_WITH `dist (s,u:real^3) = radV {u0,u1,u2,u3:real^3}`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (EXPAND_TAC "s"); (FIRST_ASSUM MATCH_MP_TAC); (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC); (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC); BY((SET_TAC[])); (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (REWRITE_TAC[GSYM HL]); BY((ASM_REWRITE_TAC[])); (REWRITE_WITH `dist (s,v:real^3) = radV {u0,u1,u2,u3:real^3}`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (EXPAND_TAC "s"); (FIRST_ASSUM MATCH_MP_TAC); (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC); (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC); BY((SET_TAC[])); (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (REWRITE_TAC[GSYM HL]); BY((ASM_REWRITE_TAC[])); BY((ASM_REAL_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`); (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA); BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[])); (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`); (REPEAT STRIP_TAC); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `edgeX V X = {{u0,u1:real^3}, {u0,u2}, {u0,u3}, {u1,u2}, {u1,u3}, {u2,u3}}`); (REWRITE_TAC[edgeX]); (ONCE_REWRITE_TAC[SET_EQ_LEMMA]); (REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (UNDISCH_TAC `VX V X u` THEN UNDISCH_TAC `VX V X v`); (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]); (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]); (REPEAT STRIP_TAC); (NEW_GOAL `F`); BY((ASM_MESON_TAC[])); BY((ASM_MESON_TAC[])); (REWRITE_WITH `{u,v} = {v,u:real^3}`); BY((SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (REWRITE_WITH `{u,v} = {v,u:real^3}`); BY((SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (REWRITE_WITH `{u,v} = {v,u:real^3}`); BY((SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (NEW_GOAL `F`); BY((ASM_MESON_TAC[])); BY((ASM_MESON_TAC[])); (REWRITE_WITH `{u,v} = {v,u:real^3}`); BY((SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (REWRITE_WITH `{u,v} = {v,u:real^3}`); BY((SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (NEW_GOAL `F`); BY((ASM_MESON_TAC[])); BY((ASM_MESON_TAC[])); (REWRITE_WITH `{u,v} = {v,u:real^3}`); BY((SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (NEW_GOAL `F`); BY((ASM_MESON_TAC[])); BY((ASM_MESON_TAC[])); (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b,c,d,e,f} <=> x = a \/ x = b \/ x = c \/ x = d \/ x = e \/ x = f`]); (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]); (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]); (REPEAT STRIP_TAC); BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[])); BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[])); BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[])); BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[])); BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[])); BY((EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[])); (STRIP_TAC); (EXPAND_TAC "y1"); (FIRST_ASSUM MATCH_MP_TAC); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (STRIP_TAC); (EXPAND_TAC "y2"); (FIRST_ASSUM MATCH_MP_TAC); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (STRIP_TAC); (EXPAND_TAC "y3"); (FIRST_ASSUM MATCH_MP_TAC); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (STRIP_TAC); (EXPAND_TAC "y4"); (FIRST_ASSUM MATCH_MP_TAC); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (STRIP_TAC); (EXPAND_TAC "y5"); (FIRST_ASSUM MATCH_MP_TAC); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (STRIP_TAC); (EXPAND_TAC "y6"); (FIRST_ASSUM MATCH_MP_TAC); BY((ASM_REWRITE_TAC[] THEN SET_TAC[])); (REWRITE_WITH `rad2_y y1 y2 y3 y4 y5 y6 = radV {u0,u1,u2,u3:real^3} pow 2`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_TAC[rad2_y; y_of_x]); (GMATCH_SIMP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Merge_ineq.GDRQXLGv2)); (STRIP_TAC); (STRIP_TAC); (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA); BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[])); (REWRITE_TAC[Collect_geom.coplanar_alt]); (REWRITE_TAC[GSYM Trigonometry2.coplanar1]); (REWRITE_TAC[coplanar] THEN STRIP_TAC); (NEW_GOAL `affine hull {u0, u1, u2, u3:real^3} SUBSET affine hull (affine hull {u, v, w})`); BY((ASM_SIMP_TAC[Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA])); (UP_ASM_TAC THEN REWRITE_WITH `affine hull (affine hull {u, v, w}) = affine hull {u:real^3, v, w}`); BY((REWRITE_TAC[AFFINE_HULL_EQ; AFFINE_AFFINE_HULL])); (STRIP_TAC); (NEW_GOAL `NULLSET X`); (MATCH_MP_TAC NEGLIGIBLE_SUBSET); (EXISTS_TAC `affine hull {u0, u1, u2, u3:real^3}`); (STRIP_TAC); (MATCH_MP_TAC NEGLIGIBLE_SUBSET); (EXISTS_TAC `affine hull {u,v,w:real^3}`); (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]); BY((ASM_REWRITE_TAC[])); (REWRITE_TAC[ASSUME `X = mcell i V ul`]); (REWRITE_WITH `mcell i V ul = mcell4 V ul`); BY((MESON_TAC[ARITH_RULE `4 >= 4`; MCELL_EXPLICIT; ASSUME `i >= 4`])); (REWRITE_TAC[mcell4]); (COND_CASES_TAC); BY((ASM_REWRITE_TAC[set_of_list; CONVEX_HULL_SUBSET_AFFINE_HULL])); BY((SET_TAC[])); BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[])); (REWRITE_TAC[GSYM REAL_POW_2]); (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3"); (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6"); BY((REWRITE_TAC[])); (REWRITE_WITH `radV {u0, u1, u2, u3:real^3} = hl (ul:(real^3)list)`); BY((ASM_REWRITE_TAC[HL;set_of_list])); (REWRITE_WITH `hl (ul:(real^3)list) pow 2 < &2 <=> sqrt (hl ul pow 2) < sqrt (&2)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Real_ext.REAL_PROP_LT_SQRT); BY((REWRITE_TAC[REAL_LE_POW_2] THEN REAL_ARITH_TAC)); (REWRITE_WITH `sqrt (hl (ul:(real^3)list) pow 2) = hl ul`); (MATCH_MP_TAC POW_2_SQRT); (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`)); (NEW_GOAL `hl (truncate_simplex 1 ul) <= hl (ul:(real^3)list)`); (MATCH_MP_TAC Rogers.HL_DECREASE); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3`); BY((ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 3`])); (NEW_GOAL `&0 < hl (truncate_simplex 1 (ul:(real^3)list))`); (MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT); BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[])); BY((ASM_REAL_ARITH_TAC)); BY((ASM_REWRITE_TAC[])); (STRIP_TAC); (NEW_GOAL `F`); BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[])); BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[])); (COMMENT "END OF 4-CELL CASE"); (ASM_CASES_TAC `i = 0`); (NEW_GOAL `VX V X = {}`); (REWRITE_WITH `VX V X = V INTER X`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); BY((ASM_REWRITE_TAC[])); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Lepjbdj.LEPJBDJ_0); BY((ASM_REWRITE_TAC[])); (NEW_GOAL `edgeX V X = {}`); (REWRITE_TAC[edgeX]); (ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`; SET_RULE `x IN {} <=> F`]); BY((SET_TAC[])); (REWRITE_TAC[gammaX]); (MATCH_MP_TAC (REAL_ARITH `b = &0 /\ c = &0 /\ &0 <= a ==> a - b + c >= &0`)); (REPEAT STRIP_TAC); BY((ASM_REWRITE_TAC[total_solid; SUM_CLAUSES] THEN REAL_ARITH_TAC)); BY((ASM_REWRITE_TAC[SUM_CLAUSES] THEN REAL_ARITH_TAC)); (MATCH_MP_TAC MEASURE_POS_LE); (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Urrphbz1.MEASURABLE_MCELL); BY((ASM_REWRITE_TAC[])); COMMENT "insert. thales. Jan 2013"; FIRST_X_ASSUM_ST `gamma3f` MP_TAC; REPEAT (FIRST_X_ASSUM_ST `ineq` kill); DISCH_TAC; TYPIFY `i = 3` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC (arith `~(i >= 4) /\ ~(i=0) /\ ~((i=1) \/ (i=2)) ==> (i = 3)`); REPLICATE_TAC 9 (FIRST_X_ASSUM MP_TAC); REPEAT (FIRST_X_ASSUM kill); BY(MESON_TAC[]); REPEAT (FIRST_X_ASSUM_ST `gamma4fgcy` kill); COMMENT "end of insert"; (NEW_GOAL `X = mcell3 V ul`); (ASM_REWRITE_TAC[]); BY((ASM_SIMP_TAC[MCELL_EXPLICIT])); (UP_ASM_TAC THEN REWRITE_TAC[mcell3]); (COND_CASES_TAC); (STRIP_TAC); (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[])); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s)`); (MATCH_MP_TAC MXI_EXPLICIT); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); BY((ASM_REWRITE_TAC[])); (UP_ASM_TAC THEN STRIP_TAC); (ABBREV_TAC `s2 = omega_list_n V ul 2`); (ABBREV_TAC `s3 = omega_list_n V ul 3`); (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`); (NEW_GOAL `s2 IN voronoi_list V vl`); (EXPAND_TAC "s2" THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); BY((ARITH_TAC)); (NEW_GOAL `s3 IN voronoi_list V vl`); (EXPAND_TAC "s3" THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); BY((ARITH_TAC)); (NEW_GOAL `s IN voronoi_list V vl`); (MATCH_MP_TAC (SET_RULE `(?x. s IN x /\ x SUBSET t)==> s IN t`)); (EXISTS_TAC `convex hull {s2,s3:real^3}`); (STRIP_TAC); BY((ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL])); (NEW_GOAL `voronoi_list V vl = convex hull (voronoi_list V vl)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); BY((REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST])); (ONCE_REWRITE_TAC[ASSUME `voronoi_list V vl = convex hull voronoi_list V vl`]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); BY((ASM_SET_TAC[])); (MP_TAC (ASSUME `s IN voronoi_list V vl`)); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; VORONOI_LIST; VORONOI_SET; set_of_list; SET_RULE `x IN {a,b,c} <=> x=a\/x=b\/x=c`; IN_INTERS]); (STRIP_TAC); (NEW_GOAL `s IN voronoi_closed V u0 /\ s IN voronoi_closed V u1 /\ s IN voronoi_closed V (u2:real^3)`); BY((UP_ASM_TAC THEN SET_TAC[])); (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM] THEN STRIP_TAC); (NEW_GOAL `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V`); (REWRITE_TAC[SET_RULE `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V <=> {u0,u1,u2,u3} SUBSET V`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (MATCH_MP_TAC BARV_SUBSET); BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[])); (FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC); (NEW_GOAL `dist (s,u1:real^3) = sqrt(&2)`); (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]); (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`); BY((NORM_ARITH_TAC)); (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]); BY((ASM_SIMP_TAC[])); (NEW_GOAL `dist (s,u2:real^3) = sqrt(&2)`); (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]); (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`); BY((NORM_ARITH_TAC)); (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]); BY((ASM_SIMP_TAC[])); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`); (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA); BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[])); (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`); (REPEAT STRIP_TAC); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `VX V X = {u0,u1,u2}`); (REWRITE_WITH `VX V X = V INTER X`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `3`); BY((ASM_REWRITE_TAC[])); (REWRITE_WITH `X = mcell 3 V ul`); BY((ASM_REWRITE_TAC[])); (REWRITE_WITH `V INTER mcell 3 V ul = set_of_list (truncate_simplex (3 - 1) ul)`); (MATCH_MP_TAC Lepjbdj.LEPJBDJ); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 4`]); (REWRITE_WITH ` mcell 3 V [u0; u1; u2; u3] = X`); BY((ASM_REWRITE_TAC[])); BY((ASM_REWRITE_TAC[])); BY((ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list])); (UNDISCH_TAC `X = convex hull (set_of_list vl UNION {mxi V ul})`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`; SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]); (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`); BY((EXPAND_TAC "s" THEN AP_TERM_TAC THEN ASM_REWRITE_TAC[])); (STRIP_TAC); (NEW_GOAL `~coplanar {u0,u1,u2,s:real^3}`); (ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR]); (STRIP_TAC); (NEW_GOAL `NULLSET X`); (MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE); (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, s:real^3}`]); (MATCH_MP_TAC COPLANAR_SUBSET); (EXISTS_TAC `affine hull {u0, u1, u2, s:real^3}`); BY((ASM_REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL])); BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[])); (NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`); (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 4`); BY((REWRITE_TAC[Geomdetail.CARD4])); (ASM_CASES_TAC `CARD {u0, u1, u2, s:real^3} <= 3`); (NEW_GOAL `F`); (UNDISCH_TAC `~coplanar {u0, u1, u2, s:real^3}`); (REWRITE_TAC[] THEN MATCH_MP_TAC COPLANAR_SMALL); BY((ASM_REWRITE_TAC[Geomdetail.FINITE6])); BY((UP_ASM_TAC THEN MESON_TAC[])); BY((ASM_ARITH_TAC)); (NEW_GOAL `~(u0 = s:real^3) /\ ~(u1 = s) /\ ~(u2 = s)`); (REPEAT STRIP_TAC); (NEW_GOAL `CARD {u0, u1, u2,s:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u0 = s:real^3`; SET_RULE `{s, u1, u2, s} = {s,u1,u2}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u1 = s:real^3`; SET_RULE `{u0, s, u2, s} = {u0,u2,s}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`); BY((REWRITE_TAC[ASSUME `u2 = s:real^3`; SET_RULE `{u0, u1, s, s} = {u0,u1,s}`;Geomdetail.CARD3 ])); BY((ASM_ARITH_TAC)); (ABBREV_TAC `y4 = dist (u1:real^3, u2)`); (ABBREV_TAC `y5 = dist (u0:real^3, u2)`); (ABBREV_TAC `y6 = dist (u0:real^3, u1)`); COMMENT "insert by thales, Jan 2013"; INTRO_TAC Tskajxy_lemmas.gammaX_gamma3f [`V`;`X`;`ul`;`u0`;`u1`;`u2`;`u3`;`y4`;`y5`;`y6`]; ASM_REWRITE_TAC[]; REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[arith `x >= &0 <=> &0 <= x`]; REPLICATE_TAC 8 (FIRST_X_ASSUM kill); FIRST_X_ASSUM MATCH_MP_TAC; TYPIFY `&2 <= y4 /\ &2 <= y5 /\ &2 <= y6` (C SUBGOAL_THEN ASSUME_TAC); REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM)); BY(ASM_MESON_TAC[packing]); ASM_REWRITE_TAC[]; TYPIFY `y4 <= &2 * sqrt (&2) /\ y5 <= &2 * sqrt (&2) /\ y6 <= &2 * sqrt (&2)` (C SUBGOAL_THEN (unlist REWRITE_TAC)); REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM)); TYPIFY `!(u:real^3) v. (dist(u,s) = sqrt(&2) /\ dist(v,s) = sqrt(&2)) ==> (dist(u,v) <= &2 * sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC o (ONCE_REWRITE_RULE[DIST_SYM])); INTRO_TAC DIST_TRIANGLE [`u`;`s`;`v`]; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); REPEAT (FIRST_X_ASSUM_ST `x = sqrt(&2)` MP_TAC); TYPIFY `!u. dist (s,u) = dist(u,s)` (C SUBGOAL_THEN (unlist REWRITE_TAC)); BY(MESON_TAC[DIST_SYM]); BY(MESON_TAC[]); INTRO_TAC Collect_geom.RADV_FORMULAR [`u0`;`u1`;`u2`]; REWRITE_TAC[Collect_geom.dist3]; ANTS_TAC; BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `hl vl` MP_TAC; EXPAND_TAC "vl"; TYPIFY `hl (truncate_simplex 2 ul) = radV {u0,u1,u2}` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); REWRITE_TAC[Pack_defs.HL]; AP_TERM_TAC; GMATCH_SIMP_TAC Bump.SET_OF_LIST_TRUNCATE_2; ASM_REWRITE_TAC[Bump.EL_EXPLICIT]; REWRITE_TAC[LENGTH]; BY(ARITH_TAC); BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY]) ]);; (* }}} *) (* ======================================================================== *) (* OLD SCRIPT FOLLOWS *) end;;