(* ========================================================================== *) (* FLYSPECK - BOOK FORMALISATION *) (* *) (* Lemma: FATUGPD *) (* Chapter: Tame *) (* Author: Vuong Anh Quyen *) (* Date: 2010-02-09 *) (* ========================================================================== *) flyspeck_needs "hypermap/hypermap.hl";; flyspeck_needs "fan/fan_defs.hl";; flyspeck_needs "fan/planarity.hl";; flyspeck_needs "leg/geomdetail.hl";; flyspeck_needs "packing/pack2.hl";; (* for KIUMVTC *) flyspeck_needs "packing/pack_defs.hl";; (* for h0 def and others *) flyspeck_needs "trigonometry/trig1.hl";; flyspeck_needs "general/prove_by_refinement.hl";; flyspeck_needs "tame/tame_concl.hl";; flyspeck_needs "tame/tame_defs.hl";; (* was commented out *) module Fatugpd = struct open Hypermap;; open Fan_defs;; open Fan;; open Planarity;; open Pack_defs;; open Pack1;; open Pack2;; open Tame_defs;; open Trigonometry1;; open Tame_defs;; open Prove_by_refinement;; let JBDNJJB = Planarity.JBDNJJB;; (* my assumptions *) let UBHDEUU2_concl = Tame_concl.UBHDEUU2_concl;; let UBHDEUU2_hypothesis = new_definition (mk_eq(`UBHDEUU2_hypothesis:bool`,UBHDEUU2_concl));; let UBHDEUU2_quasi = UNDISCH(MATCH_MP (TAUT `(x = y) ==> (x ==> y)`) UBHDEUU2_hypothesis);; (* my tatics *) let Q_LABEL_TAC term phr = UNDISCH_THEN term (LABEL_TAC phr);; let Q_ABBREV_TAC term str = (ABBREV_TAC term) THEN FIRST_X_ASSUM (LABEL_TAC str);; let Q_EXPAND_TAC str = (USE_THEN str (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));; (* some of my lemmas that may help others *) let NOT_EMPTY_IMAGE = prove ( ` !(S:A -> bool) (f:A->B). ~( S = {}) ==> ~( IMAGE f S = {})`, SET_TAC[]);; (* lemma about sup of function on finite set *) let finite_num_func_attain_max = prove_by_refinement( `! (S:A->bool) (f:A->num). FINITE S /\ ~ (S = {}) ==> (? x. x IN S /\ (! y. y IN S ==> f y <= f x))`, [ (REPEAT STRIP_TAC); (* subgoal 1 *) (SUBGOAL_THEN ` FINITE (IMAGE (& o(f:A->num)) (S:A->bool)) /\ ~ (IMAGE (& o f) S = {})` ASSUME_TAC); CONJ_TAC; (* subgoal 1.1 *) (ASM_SIMP_TAC[FINITE_IMAGE]); (* subgoal 2.1 *) (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]); (FIRST_ASSUM(MP_TAC o (MATCH_MP SUP_FINITE))); (CONV_TAC(PAT_CONV `\k. _ IN k /\ _ ==> _` (REWRITE_CONV[IMAGE]))); (PURE_REWRITE_TAC[IN_ELIM_THM]); STRIP_TAC; (EXISTS_TAC `x:A`); (ASM_SIMP_TAC[]); (REPEAT STRIP_TAC); (FIRST_X_ASSUM(MP_TAC o SPEC ` (& o (f:A->num)) y`)); (* subgoal 2 *) (SUBGOAL_THEN ` (& o (f:A->num)) y IN IMAGE (& o f) S` ASSUME_TAC); (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]); (EXISTS_TAC `y:A` THEN ASM_SIMP_TAC[]); (ASM_SIMP_TAC[o_THM; REAL_OF_NUM_LE]); ]);; (* lemma about property of sup *) let sup_property1 = prove_by_refinement( `! (S:real->bool). ~(S = {}) /\(?b. !x. x IN S ==> x <= b) ==> (! epsilon. epsilon > &0 ==> ?x. x IN S /\ x > sup S - epsilon)`, [ (GEN_TAC THEN DISCH_THEN (MP_TAC o (MATCH_MP SUP))); (STRIP_TAC THEN GEN_TAC); (DISCH_THEN (ASSUME_TAC o (MATCH_MP (ARITH_RULE ` epsilon > &0 ==> ~ ( sup (S:real->bool) <= sup S - epsilon)`)))); (MATCH_MP_TAC (MESON[] `! (P:A->bool) (Q:A->bool). ~(!(x:A). P x ==> ~ (Q x)) ==> (?(x:A). P x /\ Q x)`)); (PURE_REWRITE_TAC[ARITH_RULE `~(x > sup S - epsilon) <=> x <= sup S - epsilon`]); (ASM_MESON_TAC[]);]);; (* lemma about maximal of num bounded function *) let bdd_num_func_attain_max = prove_by_refinement( `! (S:A ->bool) (f:A-> num). ~(S = {})/\(?m. !x. x IN S ==> f x <= m) ==> (?x. x IN S /\ (!y. y IN S ==> f y <= f x))`, [ (REPEAT STRIP_TAC); (* subgoal 1 *) (SUBGOAL_THEN `~( IMAGE (& o (f:A->num)) (S:A->bool) = {}) /\ (? b. ! y. y IN (IMAGE (& o f) S) ==> y <= b)` ASSUME_TAC); (CONJ_TAC); (* subgoal 1.1 *) (ASM_SET_TAC[]); (* subgoal 1.2 *) (EXISTS_TAC `& (m:num)`); (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM]); (REPEAT STRIP_TAC); (ONCE_ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[REAL_OF_NUM_LE]); (FIRST_ASSUM (MP_TAC o MATCH_MP SUP)); (ABBREV_TAC `p = sup (IMAGE (& o (f:A->num)) (S:A->bool))` THEN STRIP_TAC); (* subgoal 2 *) (SUBGOAL_THEN `?z. z IN (IMAGE (& o (f:A->num)) (S:A->bool)) /\ z > p - &1` MP_TAC); (EXPAND_TAC "p"); (FIRST_ASSUM (MP_TAC o (SPEC `&1`) o (MATCH_MP sup_property1))); (SIMP_TAC[ARITH_RULE `&1 > &0`]); (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM] THEN STRIP_TAC ); (EXISTS_TAC `x:A`); (ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC); (MATCH_MP_TAC (ARITH_RULE ` n < (m:num) + 1 ==> n <= m`)); (* subgoal 3 *) (SUBGOAL_THEN `&((f:A->num) y) IN (IMAGE (& o f) (S:A->bool))` ASSUME_TAC); (ASM_SIMP_TAC[IN_ELIM_THM;o_THM;IMAGE]); (EXISTS_TAC `y:A`); (ASM_SIMP_TAC[]); (* subgoal 4 *) (SUBGOAL_THEN `&((f:A->num) y) <= p` ASSUME_TAC); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (fst(EQ_IMP_RULE (SPECL [`(f:A->num) y`;`f x + 1`] REAL_OF_NUM_LT)))); (PURE_REWRITE_TAC[GSYM REAL_OF_NUM_ADD]); (ASM_ARITH_TAC); ]);; let BIJ_CARD_EQ = prove ( `! (V:A->bool) (U:B->bool) (f:A->B). FINITE V /\ BIJ f V U ==> CARD U = CARD V`, REPEAT GEN_TAC THEN REWRITE_TAC[BIJ;INJ;SURJ] THEN STRIP_TAC THEN MATCH_MP_TAC CARD_EQ_CARD_IMP THEN ASM_SIMP_TAC[] THEN ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[eq_c] THEN EXISTS_TAC `f:A->B` THEN ASM_MESON_TAC[]);; (* another property of sup *) let SUP_lt = prove_by_refinement( `! (S:real -> bool) (b:real). ~(S = {}) /\ FINITE S /\ (!x. x IN S ==> x < b) ==> sup S < b`, [ (REPEAT STRIP_TAC); (FIRST_ASSUM (fun thm -> (MATCH_MP_TAC thm))); (ASM_SIMP_TAC[SUP_FINITE]); ]);; (* epsilon lemma *) let epsilon_lemma = prove_by_refinement( `! (a:real) b. a < b ==> ? epsilon. epsilon > &0 /\ b > a + epsilon`, [ (REPEAT STRIP_TAC); (EXISTS_TAC `(b - a) / &2`); ASM_ARITH_TAC; ]);; let normalize = new_definition `!(v:real^N). normalize v = inv (norm v) % v`;; let norm_normalize = prove_by_refinement( `! (v:real^3). ~(v = vec 0) ==> norm (normalize v) = &1 `, [ (GEN_TAC THEN STRIP_TAC); (PURE_REWRITE_TAC[normalize;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM]); (MATCH_MP_TAC REAL_MUL_LINV); (ASM_MESON_TAC[NORM_EQ_0]); ]);; let normalize_vec_0 = prove_by_refinement( `normalize (vec 0:real^N) = (vec 0:real^N)`, [(PURE_REWRITE_TAC[normalize;REAL_INV_0;NORM_0;VECTOR_MUL_LZERO]); VECTOR_ARITH_TAC;]);; let norm_mul_normalize = prove_by_refinement( `! (v:real^3).(norm v) % (normalize v) = v`, [ (GEN_TAC); (ASM_CASES_TAC `v:real^3 = vec 0`); (* subgoal 1 *) (ASM_SIMP_TAC[normalize_vec_0; VECTOR_MUL_RZERO]); (* subgoal 2 *) (PURE_REWRITE_TAC[normalize;VECTOR_MUL_ASSOC]); (SUBGOAL_THEN `~(norm (v:real^3) = &0)` (ASSUME_TAC o MATCH_MP REAL_MUL_RINV)); (ASM_MESON_TAC[NORM_EQ_0]); (ASM_SIMP_TAC[VECTOR_MUL_LID]);]);; let dot_normalize = prove_by_refinement( `! v:real^3. v dot (normalize v) = norm v`, [ (GEN_TAC); (ASM_CASES_TAC `v:real^3 = vec 0`); (* subgoal 1 *) (ASM_SIMP_TAC[NORM_0;DOT_LZERO]); (* subgoal 2 *) (SUBGOAL_THEN ` norm (v:real^3) * (v dot normalize v) = norm v pow 2` MP_TAC); (ONCE_REWRITE_TAC[GSYM DOT_RMUL]); (ASM_SIMP_TAC[norm_mul_normalize;DOT_SQUARE_NORM]); (ONCE_REWRITE_TAC[REAL_POW_2]); (MATCH_MP_TAC (REWRITE_RULE [TAUT `A /\ B ==> C <=> A ==> (B ==> C)`] REAL_EQ_LCANCEL_IMP)); (ASM_SIMP_TAC[NORM_EQ_0]);]);; let fourier = prove_by_refinement( ` ! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3 ==> v = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`, [ (REPEAT STRIP_TAC); (FIRST_ASSUM (ASSUME_TAC o (MATCH_MP ORTHONORMAL_IMP_SPANNING))); (UNDISCH_TAC `orthonormal (e1:real^3) e2 e3`); (ONCE_REWRITE_TAC[orthonormal]); (REPEAT STRIP_TAC); (ABBREV_TAC `(u:real^3) = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`); (* subgoal 1 *) (SUBGOAL_THEN ` (v:real^3) dot e1 = u dot e1 ` ASSUME_TAC); (EXPAND_TAC "u"); (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO; REAL_ADD_RID;REAL_MUL_RID]); (* subgoal 2 *) (SUBGOAL_THEN ` (v:real^3) dot e2 = u dot e2 ` ASSUME_TAC); (EXPAND_TAC "u"); (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO; REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]); (* subgoal 3 *) (SUBGOAL_THEN ` (v:real^3) dot e3 = u dot e3 ` ASSUME_TAC); (EXPAND_TAC "u"); (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO; REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]); (* subgoal 4 *) (SUBGOAL_THEN `(v:real^3) - u IN span {e1:real^3, e2, e3}` MP_TAC); (ASM_SET_TAC[]); (SIMP_TAC[SPAN_3;IN_ELIM_THM;IN_UNIV]); (STRIP_TAC); (* subgoal 5 *) (SUBGOAL_THEN `((v:real^3) - u) dot (v - u) = &0` MP_TAC); (PURE_REWRITE_TAC[DOT_LSUB]); (ASM_SIMP_TAC[DOT_RMUL;DOT_RADD;REAL_SUB_REFL]); (ASM_SIMP_TAC[DOT_EQ_0;VECTOR_SUB_EQ]);]);; let norm_lemma1 = prove_by_refinement( `! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3 ==> norm v = sqrt ((v dot e1) pow 2 + (v dot e2) pow 2 + (v dot e3) pow 2)`, [ (REPEAT STRIP_TAC); (PURE_REWRITE_TAC[vector_norm]); (FIRST_ASSUM (ASSUME_TAC o MATCH_MP fourier)); (FIRST_ASSUM (fun thm -> CONV_TAC (PAT_CONV `\x. sqrt (x dot x) = _` (ONCE_REWRITE_CONV[thm])))); (PURE_REWRITE_TAC[DOT_RADD;DOT_LADD;DOT_RMUL;DOT_LMUL; REAL_ADD_RDISTRIB;REAL_ADD_LDISTRIB]); (ONCE_REWRITE_TAC[REAL_MUL_ASSOC]); (ONCE_REWRITE_TAC[GSYM REAL_POW_2]); (FIRST_ASSUM (MP_TAC o MATCH_MP (fst (EQ_IMP_RULE (SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`] orthonormal))))); STRIP_TAC; (ASM_SIMP_TAC[DOT_SYM;REAL_MUL_RZERO;REAL_ADD_RID; REAL_ADD_LID;REAL_MUL_RID]);]);; let coordinates_lemma = prove_by_refinement( `! (v:real^3) (e1:real^3) e2 e3 (x:real) y z. orthonormal e1 e2 e3 /\ v = x % e1 + y % e2 + z % e3 ==> x = v dot e1 /\ y = v dot e2 /\ z = v dot e3`, [ (REPEAT GEN_TAC); (STRIP_TAC); (FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` (MATCH_MP fourier thm)))); (ASM_MESON_TAC[ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT]);]);; let dot_coordinates = prove_by_refinement( `! v:real^3 u e1 e2 e3. orthonormal e1 e2 e3 ==> v dot u = (v dot e1) * (u dot e1) + (v dot e2) * (u dot e2) + (v dot e3) * (u dot e3)`, [ (REPEAT STRIP_TAC); (FIRST_ASSUM((LABEL_TAC "a") o (MATCH_MP (SPEC `u:real^3` fourier)))); (USE_THEN "a" (fun thm -> (CONV_TAC (PAT_CONV `\x. A dot x = B` (ONCE_REWRITE_CONV[thm]))))); (ONCE_REWRITE_TAC[VECTOR_ARITH `(v:real^3) dot (a % e1 + b % e2 + c % e3) = (v dot e1) * a + (v dot e2 ) * b + (v dot e3) * c`]); (SIMP_TAC[]);]);; let dot_coordinates_2 = prove_by_refinement( `! (v:real^3) u e1 e2 e3 x y z a b c. orthonormal e1 e2 e3 /\ v = x % e1 + y % e2 + z % e3 /\ u = a % e1 + b % e2 + c % e3 ==> v dot u = x * a + y * b + z * c`, [(ONCE_REWRITE_TAC[orthonormal]); (REPEAT STRIP_TAC); (ONCE_ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[DOT_SYM;DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL]); ARITH_TAC;]);; let norm_lemma2 = prove_by_refinement( `! (v:real^3) e1 e2 e3 x y z. orthonormal e1 e2 e3 /\ v = x % e1 + y % e2 + z % e3 ==> norm v = sqrt (x pow 2 + y pow 2 + z pow 2)`, [ (REPEAT GEN_TAC); (DISCH_TAC); (FIRST_ASSUM (fun thm -> ONCE_REWRITE_TAC [ MATCH_MP norm_lemma1 (CONJUNCT1 thm)])); (FIRST_ASSUM (fun thm -> SIMP_TAC[ MATCH_MP coordinates_lemma thm]));]);; let dot_gt_0 = prove_by_refinement( `! v:real^3 u. &0 < v dot u <=> &0 < v dot normalize u `, [ (REPEAT GEN_TAC); (ASM_CASES_TAC `u:real^3 = vec 0`); (* subgoal 1 *) (ASM_SIMP_TAC[normalize_vec_0]); (* subgoal 2 *) ( CONV_TAC(PAT_CONV `\x. &0 < A dot x <=> B`(ONCE_REWRITE_CONV[GSYM norm_mul_normalize]))); (PURE_REWRITE_TAC[DOT_RMUL]); (MATCH_MP_TAC (CONJUNCT1 REAL_LT_MUL_EQ)); (MATCH_MP_TAC (REAL_ARITH `&0 <= x /\ ~(x = &0) ==> &0 < x`)); (ASM_SIMP_TAC[NORM_POS_LE;NORM_EQ_0]);]);; let dot_eq_0 = prove_by_refinement( `! v:real^3 u. v dot u = &0 <=> (normalize v) dot u = &0`, [ (REPEAT GEN_TAC); (ASM_CASES_TAC `v:real^3 = vec 0`); (* subgoal 1 *) (ASM_SIMP_TAC[normalize_vec_0]); (* subgoal 2 *) (CONV_TAC(PAT_CONV `\x. x dot y = &0 <=> A` (ONCE_REWRITE_CONV[GSYM norm_mul_normalize]))); (ONCE_REWRITE_TAC[DOT_LMUL]); (CONV_TAC(PAT_CONV `\x. x <=> A` (ONCE_REWRITE_CONV [ARITH_RULE `&0 = norm (v:real^3) * &0`]))); (ONCE_REWRITE_TAC[REAL_EQ_MUL_LCANCEL]); (ASM_SIMP_TAC[NORM_EQ_0]);]);; let azim_ge_azim_dart = prove_by_refinement( `! (V:real^3->bool) E w u v. FAN (vec 0, V, E) /\ w IN V /\ u IN set_of_edge w V E /\ v IN set_of_edge w V E /\ ~(w = u) /\ ~(v = u) ==> azim (vec 0) w u v >= azim_dart (V,E) (w,u)`, [ (REPEAT STRIP_TAC); (ASM_SIMP_TAC[azim_dart]); (PURE_REWRITE_TAC[azim_fan]); (* subgoal 1 *) (SUBGOAL_THEN `CARD (set_of_edge (w:real^3) V E) > 1` ASSUME_TAC); (MP_TAC (SPECL [`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`; `u:real^3`;`w:real^3`] Fan.remark1_fan)); (ASM_SIMP_TAC[]); (STRIP_TAC); (MP_TAC(ISPECL [`v:real^3`;`u:real^3`] Hypermap.CARD_TWO_ELEMENTS)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (ARITH_RULE `(a:num) <= b ==> a = 2 ==> b > 1`)); (MATCH_MP_TAC CARD_SUBSET); (ASM_SET_TAC[]); (ASM_SIMP_TAC[]); (* subgoal 2 *) (SUBGOAL_THEN `~(set_of_edge (w:real^3) V E = {u})` ASSUME_TAC); (ONCE_REWRITE_TAC[TAUT ` ~A <=> A ==> F`]); (DISCH_THEN (MP_TAC o (AP_TERM `(\(S:real^3->bool). CARD S)`))); (SIMP_TAC[BETA_THM;Geomdetail.CARD_SING]); (ASM_ARITH_TAC); (MP_TAC (SPECL [`vec 0 :real^3`;`V:real^3 -> bool`; `E:(real^3->bool)->bool`;`w:real^3`;`u:real^3`] Fan.SIGMA_FAN)); (ASM_SIMP_TAC[]); STRIP_TAC; (ASM_SIMP_TAC[ARITH_RULE `a >= b <=> b <= a`]);]);; (* FATUGPD *) (* definitions in the proof *) let set_of_iso = new_definition ` set_of_iso W = {w| w IN W /\ set_of_edge w W (ECTC W) = {}}`;; (* lemmas prepared for the proof *) let lemma1 = prove_by_refinement( `! (S:real^3->bool). packing S /\ S SUBSET ball_annulus ==> FINITE S`, [ (REPEAT STRIP_TAC); (* subgoal 1 *) (SUBGOAL_THEN ` (S:real^3->bool) = S INTER ball (vec 0,&3 * h0)` ASSUME_TAC); (MATCH_MP_TAC (SET_RULE `! U V. U SUBSET ball_annulus /\ ball_annulus SUBSET V ==> (U = U INTER V)`)); (ASM_SIMP_TAC[ball_annulus;ball;cball;IN_DIFF;SUBSET;IN_ELIM_THM;h0]); (REPEAT STRIP_TAC ); (MATCH_MP_TAC (ARITH_RULE ` u <= &2 * #1.26 ==> u < &3 * #1.26`)); (ASM_SIMP_TAC[]); (ONCE_ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[KIUMVTC]);]);; let lemma2 = prove_by_refinement( `! (V:real^3 -> bool) v. packing V /\ FINITE V /\ v IN V ==> ? epsilon. epsilon > &0 /\ (! w. w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V)) ==> dist (v,w) > &2 + epsilon )`, [ (REPEAT STRIP_TAC); (ABBREV_TAC `(S:real^3->bool) = {w|w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V))}`); (ASM_CASES_TAC `(S:real^3 ->bool) = {}`); (* subgoal 1 *) (EXISTS_TAC `&1`); (SIMP_TAC[ARITH_RULE `&1 > &0`]); (REPEAT STRIP_TAC); (* subgoal 1.1 *) (SUBGOAL_THEN `~((S:real^3->bool) = {})` ASSUME_TAC); (ASM_SET_TAC[]); (ASM_MESON_TAC[]); (* subgoal 2 *) (* subgoal 2.1 *) (SUBGOAL_THEN `FINITE (S:real^3 -> bool)` ASSUME_TAC); (MATCH_MP_TAC (ISPECL [`(S:real^3-> bool)`;`(V:real^3 ->bool)`] FINITE_SUBSET)); (ASM_SET_TAC[]); (ABBREV_TAC `(f:real^3 -> real) = (\w. dist (v,w))`); (* subgoal 2.2 *) (SUBGOAL_THEN `&2 < inf (IMAGE (f:real^3 -> real) (S:real^3 ->bool))` ASSUME_TAC); (* subgoal 2.2.1 *) (SUBGOAL_THEN `FINITE (IMAGE (f:real^3 ->real) S) /\ ~ (IMAGE f S = {})` ASSUME_TAC); (ASM_SIMP_TAC[FINITE_IMAGE;NOT_EMPTY_IMAGE]); (ASM_SIMP_TAC[REAL_LT_INF_FINITE]); (EXPAND_TAC "S"); (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]); (REPEAT STRIP_TAC); (ONCE_ASM_REWRITE_TAC[]); (EXPAND_TAC "f"); (MATCH_MP_TAC (ARITH_RULE `! (a:real). &2 <= a /\ ~(&2 = a) ==> &2 < a`)); CONJ_TAC; (* subgoal 2.2.3 *) (UNDISCH_TAC `packing (V:real^3 -> bool)`); (PURE_REWRITE_TAC[packing]); (DISCH_THEN (fun thm -> MATCH_MP_TAC (ISPECL [`x':real^3`;`v:real^3`] thm))); (ASM_MESON_TAC[IN]); (* subgoal 2.2.4 *) (SUBGOAL_THEN `&2 = dist (v,x') ==> (x' IN set_of_edge v V (ECTC V))` ASSUME_TAC); (STRIP_TAC); (PURE_REWRITE_TAC[set_of_edge]); (ASM_SIMP_TAC[ECTC;IN_ELIM_THM]); (EXISTS_TAC `v:real^3`); (EXISTS_TAC `x':real^3`); (ASM_SIMP_TAC[]); (ASM_MESON_TAC[]); (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP epsilon_lemma))); (FIRST_X_ASSUM CHOOSE_TAC); (EXISTS_TAC `epsilon:real`); (ASM_SIMP_TAC[]); (REPEAT STRIP_TAC); (MATCH_MP_TAC (ARITH_RULE `! u:real v w. u >= v /\ v > w ==> u > w`)); (EXISTS_TAC `inf (IMAGE (f:real^3 -> real) (S:real^3 -> bool))`); (ASM_SIMP_TAC[]); (* subgoal 2.3 *) (SUBGOAL_THEN `dist (v,w:real^3) IN (IMAGE (f:real^3 -> real) S)` ASSUME_TAC); (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]); (EXISTS_TAC `w:real^3`); (CONJ_TAC); (* subgoal 2.3.1 *) (EXPAND_TAC "S"); (ASM_SIMP_TAC[IN_ELIM_THM]); (* subgoal 2.3.2 *) (EXPAND_TAC "f"); (SIMP_TAC[]); (* subgoal 2.3.3 *) (SUBGOAL_THEN `~(IMAGE (f:real^3 -> real) S = {}) /\ (? b:real. !x. x IN (IMAGE f S) ==> b <= x )` ASSUME_TAC); (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]); (EXISTS_TAC `&2`); STRIP_TAC; (EXPAND_TAC "f"); (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]); (REPEAT STRIP_TAC); (ONCE_ASM_REWRITE_TAC[]); (SIMP_TAC[]); (UNDISCH_TAC `packing (V:real^3 -> bool)`); (PURE_REWRITE_TAC[packing]); (DISCH_THEN (fun thm -> MP_TAC (ISPECL [`v:real^3`;`x':real^3`] thm))); (MATCH_MP_TAC (TAUT `U ==> ((U ==> V)==> V) `)); (CONV_TAC (PAT_CONV `\x y. x /\ y /\ _ ` (ONCE_REWRITE_CONV[GSYM IN]))); (ASM_SIMP_TAC[]); (UNDISCH_TAC `(x':real^3) IN S`); (EXPAND_TAC "S"); (PURE_REWRITE_TAC[IN_ELIM_THM]); (SIMP_TAC[]); (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP INF))); (ONCE_REWRITE_TAC[ARITH_RULE `a >= b <=> b <= a`]); (FIRST_X_ASSUM (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm))); (ASM_SIMP_TAC[]); ]);; let lemma3 = prove_by_refinement( `! (w:real^3) (W:real^3 -> bool). packing W /\ w IN W /\ ~(set_of_edge w W (ECTC W) = {}) /\ ~(surrounded_node (W,(ECTC W)) w) ==> ?u. (u IN set_of_edge w W (ECTC W)) /\ (azim_dart (W, (ECTC W)) (w,u) >= pi)`, [ (PURE_REWRITE_TAC[surrounded_node]); (PURE_REWRITE_TAC[GSYM EXISTS_NOT_THM]); (PURE_REWRITE_TAC[TAUT `~(A ==> B) <=> A /\ ~B`]); (PURE_REWRITE_TAC[ARITH_RULE `~ (a < pi) <=> a >= pi`]); (PURE_REWRITE_TAC[dart_of_fan]); (PURE_REWRITE_TAC[SET_RULE `x IN A UNION B <=> x IN A \/ x IN B`]); (SIMP_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (* subgoal 1 *) (SUBGOAL_THEN `set_of_edge (w:real^3) (W:real^3 ->bool) (ECTC W) = {}` ASSUME_TAC); (FIRST_X_ASSUM (fun thm -> ALL_TAC)); (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm])); (ASM_SIMP_TAC[]); (ASM_MESON_TAC[]); (* subgoal 2 *) (EXISTS_TAC `SND (x:real^3 # real^3)`); (Q_LABEL_TAC `FST (x:real^3 # real^3) = w` "a"); (USE_THEN "a" (fun thm -> SIMP_TAC[PAIR; GSYM thm])); (ASM_SIMP_TAC[]); (PURE_REWRITE_TAC[IN_ELIM_THM;set_of_edge]); (* subgoal 2.1 *) (SUBGOAL_THEN `w:real^3 = v` (LABEL_TAC "b")); (REMOVE_THEN "a" (fun thm -> PURE_REWRITE_TAC[GSYM thm])); (ASM_SIMP_TAC[]); (ASM_SIMP_TAC[]); (UNDISCH_TAC `{v:real^3,w':real^3} IN ECTC (W:real^3 -> bool)`); (REWRITE_TAC[ECTC;IN_ELIM_THM;Geomdetail.PAIR_EQ_EXPAND]); (STRIP_TAC); (* subgoal 2.2 *) (ASM_SIMP_TAC[]); (* subgoal 2.3 *) (ASM_SIMP_TAC[]);]);; let lemma4 = prove_by_refinement( `! w:real^3 u v. ~collinear {vec 0, w, u} /\ ~collinear {vec 0, w, v} /\ azim (vec 0) w u v >= pi ==> (w cross u) dot v <= &0`, [ (REPEAT STRIP_TAC); (MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] JBDNJJB)); (ASM_SIMP_TAC[]); STRIP_TAC; (ABBREV_TAC `(a:real) = ((w:real^3) cross u) dot v`); (MATCH_MP_TAC (SPECL [`t:real`;`a:real`;`&0`] REAL_LE_LCANCEL_IMP)); (ASM_SIMP_TAC[]); (Q_LABEL_TAC `sin (azim (vec 0) w u v ) = t * a` "b"); (USE_THEN "b" (fun thm -> (ONCE_REWRITE_TAC[GSYM thm; REAL_MUL_RZERO]))); (* subgoal 1 *) (SUBGOAL_THEN `azim (vec 0 :real^3) w u v < &2 * pi` ASSUME_TAC); (SIMP_TAC[SPECL [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`] azim]); (ABBREV_TAC `b:real = azim (vec 0:real^3) w u v`); (ONCE_REWRITE_TAC[ARITH_RULE `m <= &0 <=> &0 <= -- m `]); (ONCE_REWRITE_TAC[GSYM SIN_NEG]); (ONCE_REWRITE_TAC[GSYM SIN_PERIODIC]); (* subgoal 2 *) (SUBGOAL_THEN `-- pi < --b + &2 * pi /\ --b + &2 * pi <= pi` ASSUME_TAC); ASM_ARITH_TAC; (ABBREV_TAC `c:real = --b + &2 * pi`); (FIRST_ASSUM (ASSUME_TAC o (MATCH_MP SIN_NEGPOS_PI))); (ONCE_REWRITE_TAC[ARITH_RULE `&0 <= x <=> x = &0 \/ &0 < x`]); (ONCE_ASM_REWRITE_TAC[]); (MATCH_MP_TAC (ARITH_RULE ` (&0 <= c /\ c <= pi) ==> ((c = &0 \/ c = pi) \/ &0 < c /\ c < pi)`)); (ASM_SIMP_TAC[]); (EXPAND_TAC "c"); (MATCH_MP_TAC (ARITH_RULE `b < a ==> &0 <= --b + a`)); (ASM_SIMP_TAC[]);]);; let lemma5 = prove_by_refinement( `! (V:real^3 -> bool) v. packing V /\ V SUBSET ball_annulus /\ v IN V ==> ! u. (u IN set_of_edge v V (ECTC V)) ==> v dot u > &0`, [ (REPEAT STRIP_TAC); (* subgoal 1 *) (SUBGOAL_THEN `!(w:real^3). w IN V ==> w dot w >= &4` (LABEL_TAC "a")); (REPEAT STRIP_TAC); (MP_TAC (SET_RULE `(w:real^3) IN V /\ V SUBSET ball_annulus ==> w IN ball_annulus`)); (ASM_SIMP_TAC[]); (PURE_REWRITE_TAC[ball_annulus]); (PURE_REWRITE_TAC[DIFF;ball;IN_ELIM_THM]); (PURE_REWRITE_TAC[REAL_ARITH `~(a < &2) <=> a >= &2`]); (PURE_REWRITE_TAC[dist; DIST_SYM;VECTOR_SUB_RZERO]); (PURE_REWRITE_TAC[NORM_GE_SQUARE]); (SIMP_TAC[ARITH_RULE `~(&2 <= &0) /\ &2 pow 2 = &4`]); (MATCH_MP_TAC (ARITH_RULE `&2 * a > &0 ==> a > &0`)); (ONCE_REWRITE_TAC[VECTOR_ARITH `&2 * (v dot u) = v dot v + u dot u - (v - u) dot (v - u)`]); (* subgoal 2 *) (SUBGOAL_THEN `(v:real^3 - u) dot (v - u) = &4 /\ u IN V` MP_TAC); (UNDISCH_TAC `u:real^3 IN set_of_edge v V (ECTC V)`); (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]); STRIP_TAC; (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]); (ONCE_REWRITE_TAC[GSYM dist]); (FIRST_ASSUM (MP_TAC o (MATCH_MP (fst (EQ_IMP_RULE Geomdetail.PAIR_EQ_EXPAND))))); (REPEAT STRIP_TAC); (* subgoal 2.1 *) (ASM_SIMP_TAC[]); ARITH_TAC; (* subgoal 2.2 *) (ONCE_REWRITE_TAC[DIST_SYM]); (ASM_SIMP_TAC[]); ARITH_TAC; (STRIP_TAC); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (ARITH_RULE `a >= &4 /\ b >= &4 ==> a + b - &4 > &0`)); (USE_THEN "a" (fun thm -> MP_TAC( SPEC `v:real^3` thm))); (USE_THEN "a" (fun thm -> MP_TAC( SPEC `u:real^3` thm))); (ASM_SIMP_TAC[]);]);; let lemma6 = prove_by_refinement( `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\ orthonormal e1 e2 e3 /\ u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2 ==> norm u = norm v`, [ (REPEAT STRIP_TAC); (* subgoal 1 *) (SUBGOAL_THEN `orthonormal e1 e2 e3 /\ u:real^3 = (cos (phi:real) * norm (v:real^3)) % e1 + (sin phi * norm v) % e2 + &0 % e3` ASSUME_TAC); (ASM_SIMP_TAC[]); VECTOR_ARITH_TAC; (FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP (SPECL [`u:real^3`;`e1:real^3`;`e2:real^3`;`e3:real^3`; ` cos (phi:real) * norm (v:real^3)`;`sin (phi:real) * norm (v:real^3)`;`&0`] norm_lemma2))); (ONCE_ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[ARITH_RULE `( a * m) pow 2 + (b * m) pow 2 + &0 pow 2 = (b pow 2 + a pow 2) * m pow 2`]); (SIMP_TAC[SIN_CIRCLE;REAL_MUL_LID]); (MATCH_MP_TAC POW_2_SQRT); (SIMP_TAC[NORM_POS_LE]);]);; let lemma7 = prove_by_refinement( `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\ orthonormal e1 e2 e3 /\ &0 < phi /\ phi < pi /\ &0 < norm v /\ u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2 ==> (! w:real^3. &0 < w dot e1 /\ w dot e2 <= &0 ==> dist (v,w) < dist (u,w))`, [ (REPEAT STRIP_TAC); (PURE_REWRITE_TAC[dist;NORM_LT]); (ONCE_REWRITE_TAC[ARITH_RULE `a < b <=> &0 < b - a `]); (ONCE_REWRITE_TAC[VECTOR_ARITH `(u - w) dot (u - w) - (v - w) dot (v - w) = u dot u - v dot v - &2 * ((u - v) dot w )`]); (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]); (* subgoal 1 *) (SUBGOAL_THEN `norm (u:real^3) = norm (v:real^3)` ASSUME_TAC); (MATCH_MP_TAC (SPECL [`v:real^3`;`u:real^3`;`phi:real`; `e1:real^3`; `e2:real^3`;`e3:real^3`] lemma6)); (ASM_SIMP_TAC[]); (FIRST_ASSUM (fun thm -> SIMP_TAC[thm; ARITH_RULE `a - a - b = --b`])); (ONCE_REWRITE_TAC[ARITH_RULE `&0 < --(&2 * a) <=> a < &0`]); (* subgoal 2 *) (SUBGOAL_THEN `v:real^3 = (norm v) % e1` (LABEL_TAC "v_coordinate")); (ASM_SIMP_TAC[norm_mul_normalize]); (Q_LABEL_TAC `orthonormal e1 e2 e3` "base"); (USE_THEN "base" (ASSUME_TAC o MATCH_MP (SPECL [`(u - v):real^3`;`w:real^3`; `e1:real^3`;`e2:real^3`;`e3:real^3`] dot_coordinates))); (ONCE_ASM_REWRITE_TAC[]); (* subgoal 3 *) (SUBGOAL_THEN `(u:real^3 - v) dot e1 = (cos phi - &1) * norm v /\ (u - v) dot e2 = sin phi * norm v /\ (u - v) dot e3 = &0` MP_TAC); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC (SPECL [`u:real^3 - v`;`e1:real^3`;`e2:real^3`;`e3:real^3`; `(cos phi - &1) * norm v`;`sin phi * norm v`;`&0`] coordinates_lemma)); (USE_THEN "base" (fun thm -> SIMP_TAC[thm])); (USE_THEN "v_coordinate" (fun thm -> CONV_TAC( PAT_CONV `\x. U - x = _` (ONCE_REWRITE_CONV[thm])))); (Q_LABEL_TAC `u:real^3 = (cos phi * norm (v:real^3)) % e1 + (sin phi * norm v) % e2` "u"); (USE_THEN "u" (fun thm -> ONCE_REWRITE_TAC[thm])); (VECTOR_ARITH_TAC); (DISCH_THEN (LABEL_TAC "c")); (USE_THEN "c" (fun thm -> ONCE_REWRITE_TAC[thm])); (PURE_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_RID]); (MATCH_MP_TAC (REAL_ARITH `a < &0 /\ b <= &0 ==> a + b < &0`)); CONJ_TAC; (* subgoal 4 *) (ONCE_REWRITE_TAC[REAL_ARITH `((a - &1) * b) * c < &0 <=> &0 < ((&1 - a) * b) * c`]); (MATCH_MP_TAC REAL_LT_MUL); (ASM_SIMP_TAC[]); (MATCH_MP_TAC REAL_LT_MUL); (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC[REAL_ARITH `&0 < &1 - a <=> (a <= &1 /\ ~(a = &1))`]); (SIMP_TAC[COS_BOUNDS;COS_ONE_2PI]); (ONCE_REWRITE_TAC[ TAUT `~(A \/ B) <=> ~A /\ ~B`]); (STRIP_TAC); (* subgoal 4.1 *) (ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]); (STRIP_TAC); (FIRST_X_ASSUM(LABEL_TAC "phi")); (* subgoal 4.1.1 *) (SUBGOAL_THEN `0 < n:num` ASSUME_TAC); (ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]); (MATCH_MP_TAC (SPECL [`&0`;`&(n:num)`;`&2 * pi`] REAL_LT_RCANCEL_IMP)); (SIMP_TAC[ARITH_RULE `&0 * &2 * pi = &0`; ARITH_RULE `&0 < &2 * a <=> &0 < a`]); (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm])); (ASM_SIMP_TAC[PI_POS]); (* subgoal 4.1.2 *) (SUBGOAL_THEN `n:num < 1` ASSUME_TAC); (ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]); (MATCH_MP_TAC (SPECL [`&(n:num)`;`&1`;`&2 * pi`] REAL_LT_RCANCEL_IMP)); (SIMP_TAC[ARITH_RULE `&1 * &2 * pi = &2 * pi`; ARITH_RULE `&0 < &2 * a <=> &0 < a`]); (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm])); (SIMP_TAC[PI_POS]); (MATCH_MP_TAC(ARITH_RULE `a < pi /\ pi < b ==> a < b`)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC(ARITH_RULE `&0 < a ==> a < &2 * a`)); (SIMP_TAC[PI_POS]); (ASM_MESON_TAC[ARITH_RULE `~(0 < n:num /\ n < 1)`]); (* subgoal 4.2 *) (ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]); (STRIP_TAC); (FIRST_X_ASSUM(LABEL_TAC "phi")); (* subgoal 4.2.1 *) (SUBGOAL_THEN `~(&0 < phi:real)` ASSUME_TAC); (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[thm])); (ONCE_REWRITE_TAC[ARITH_RULE `~(&0 < -- a) <=> &0 <= a`]); (MATCH_MP_TAC REAL_LE_MUL); (SIMP_TAC[REAL_POS]); (MATCH_MP_TAC (ARITH_RULE `&0 < a ==> &0 <= a`)); (MATCH_MP_TAC REAL_LT_MUL); (SIMP_TAC[PI_POS]); ARITH_TAC; (ASM_MESON_TAC[]); (* subgoal 5 *) (ONCE_REWRITE_TAC[ARITH_RULE `a * b <= &0 <=> &0 <= a * (--b)`]); (MATCH_MP_TAC REAL_LE_MUL); (ONCE_REWRITE_TAC[ARITH_RULE `&0 <= -- a <=> a <= &0`]); (ASM_SIMP_TAC[]); (MATCH_MP_TAC REAL_LE_MUL); (SIMP_TAC[NORM_POS_LE]); (MATCH_MP_TAC SIN_POS_PI_LE); (ASM_ARITH_TAC);]);; let lemma8 = prove_by_refinement( `! w:real^3 W:real^3->bool. w IN W ==> set_of_edge w W (ECTC W) = {v| v IN W /\ dist (w,v) = &2}`, [ (REPEAT STRIP_TAC); (MATCH_MP_TAC SUBSET_ANTISYM); CONJ_TAC; (* subgoal 1 *) (PURE_REWRITE_TAC[SUBSET]); (GEN_TAC); (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]); (STRIP_TAC); (SUBGOAL_THEN `dist (w:real^3,x) = dist (v:real^3,w'')` ASSUME_TAC); (MATCH_MP_TAC Geomdetail.DIST_PAIR_LEMMA); (ASM_SIMP_TAC[]); (ASM_ARITH_TAC); (* subgoal 2 *) (PURE_REWRITE_TAC[SUBSET]); (GEN_TAC); (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]); (STRIP_TAC); (EXISTS_TAC `w:real^3`); (EXISTS_TAC `x:real^3`); (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC[DIST_NZ]); (ASM_ARITH_TAC);]);; (* main proof *) let FATUGPD_quasi = prove_by_refinement( ` UBHDEUU2_hypothesis ==> (!V. packing V /\ V SUBSET ball_annulus ==> (?W phi. BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\ (!w. w IN W ==> (set_of_edge w W (ECTC W) = {}) \/ (surrounded_node (W,(ECTC W)) w))))`, [ DISCH_TAC; GEN_TAC; STRIP_TAC; (ABBREV_TAC `S = {(U:real^3->bool)| FINITE U /\ packing U /\ (?phi. BIJ phi (V:real^3->bool) U /\ (! v. v IN V ==> norm v = norm (phi v)))}`); (ABBREV_TAC `(f:(real^3 ->bool)->num) = (\U. CARD (set_of_iso U))`); (* subgoal 1 *) (SUBGOAL_THEN `FINITE (V:real^3->bool)` (LABEL_TAC "finite_v")); (ASM_SIMP_TAC[lemma1]); (* subgoal 2 *) (SUBGOAL_THEN `! (U:real^3 ->bool). U IN S ==> FINITE U` (LABEL_TAC "finite_u")); (EXPAND_TAC "S"); (SIMP_TAC[IN_ELIM_THM]); (* subgoal 3 *) (SUBGOAL_THEN `~ ((S:(real^3->bool)->bool) = {}) /\ (?m. !U. U IN S ==> (f:(real^3->bool)->num) U <= m)` (LABEL_TAC "asm1")); CONJ_TAC; (* subgoal 3.1 *) (PURE_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY]); (EXISTS_TAC `V:real^3->bool`); (EXPAND_TAC "S"); (ASM_SIMP_TAC[IN_ELIM_THM]); (EXISTS_TAC `(I:real^3->real^3)`); CONJ_TAC; (* subgoal 3.1.1 *) (SIMP_TAC[BIJ;INJ;SURJ;I_THM]); (SET_TAC[]); (* subgoal 3.1.2 *) (SIMP_TAC[I_THM]); (* subgoal 3.2 *) (EXISTS_TAC `CARD (V:real^3->bool)`); (GEN_TAC); (* subgoal 3.2.1 *) (SUBGOAL_THEN `! (U:real^3->bool). U IN S ==> CARD U = CARD (V:real^3->bool)` MP_TAC); (GEN_TAC); (EXPAND_TAC "S"); (PURE_REWRITE_TAC[IN_ELIM_THM]); STRIP_TAC; (MATCH_MP_TAC BIJ_CARD_EQ); (EXISTS_TAC `phi:real^3->real^3`); (ASM_SIMP_TAC[]); (DISCH_THEN (MP_TAC o (fun thm -> (SPEC `U:real^3 ->bool` thm)))); (MATCH_MP_TAC (TAUT ` (p ==> (q ==> r)) ==> ((p ==> q) ==> (p ==> r))`)); (REPEAT STRIP_TAC); (* subgoal 3.2.2 *) (SUBGOAL_THEN `(f:(real^3->bool) -> num) U <= CARD U` ASSUME_TAC); (EXPAND_TAC "f"); (MATCH_MP_TAC CARD_SUBSET); CONJ_TAC; (* subgoal 3.2.2.1 *) (SET_TAC[set_of_iso]); (* subgoal 3.2.2.2 *) (UNDISCH_TAC `(U:real^3->bool) IN (S:(real^3->bool)->bool)`); (ASM_SIMP_TAC[]); ASM_ARITH_TAC; (REMOVE_THEN "asm1" (ASSUME_TAC o (MATCH_MP bdd_num_func_attain_max))); (FIRST_X_ASSUM CHOOSE_TAC); (EXISTS_TAC `U:real^3->bool`); (FIRST_X_ASSUM MP_TAC); (STRIP_TAC); (UNDISCH_TAC `U:real^3 -> bool IN S`); (EXPAND_TAC "S"); (SIMP_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `phi:real^3 ->real^3`); (ASM_SIMP_TAC[]); (REPEAT STRIP_TAC); (* subgoal 4 *) (SUBGOAL_THEN `! v:real^3. v IN U ==> norm v <= &2 * h0 /\ ~(norm v < &2)` (LABEL_TAC "norm_bdd")); GEN_TAC; (UNDISCH_TAC `BIJ phi (V:real^3->bool) (U:real^3->bool)`); (PURE_REWRITE_TAC[BIJ;SURJ]); ( STRIP_TAC); (STRIP_TAC); (FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` thm))); (FIRST_ASSUM (fun thm -> SIMP_TAC[thm])); STRIP_TAC; (UNDISCH_TAC `! v:real^3. v IN V ==> norm v = norm ((phi:real^3 -> real^3) v)`); (DISCH_THEN (fun thm -> MP_TAC (SPEC `y:real^3` thm))); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (ARITH_RULE `a <= &2 * h0 /\ ~(a < &2) ==> a = b ==> b <= &2 * h0 /\ ~(b < &2)`)); (* subgoal 4.1 *) (SUBGOAL_THEN `y:real^3 IN ball_annulus` MP_TAC); (MATCH_MP_TAC (SET_RULE `y:real^3 IN V /\ V SUBSET ball_annulus ==> y IN ball_annulus`)); (ASM_SIMP_TAC[]); (PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]); (SIMP_TAC[DIST_0]); (* subgoal 5 *) (SUBGOAL_THEN `(U:real^3 -> bool) SUBSET ball_annulus` (LABEL_TAC "u_annu")); (PURE_REWRITE_TAC[SUBSET]); GEN_TAC; STRIP_TAC; (PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]); (SIMP_TAC[DIST_0]); (ASM_SIMP_TAC[]); (* subgoal 6 *) (SUBGOAL_THEN `! v:real^3. v IN U ==> ~(v = vec 0)` (LABEL_TAC "not_0")); (GEN_TAC); STRIP_TAC; (ONCE_REWRITE_TAC[GSYM NORM_POS_LT]); (MATCH_MP_TAC (ARITH_RULE `~(norm (v:real^3) < &2) ==> &0 < norm v`)); (ASM_SIMP_TAC[]); (* subgoal 7 *) (SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U) ==> ~(collinear {vec 0, w, v})` (LABEL_TAC "not_li")); (GEN_TAC); (MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8)); (ASM_SIMP_TAC[]); (SIMP_TAC[IN_ELIM_THM;ECTC]); (MATCH_MP_TAC (TAUT `(B ==> C) ==> (A ==> B ==> C)`)); STRIP_TAC; (ONCE_REWRITE_TAC[COLLINEAR_BETWEEN_CASES]); (ONCE_REWRITE_TAC[TAUT `~(A \/ B \/ C) <=> ~A /\ ~B /\ ~C`]); (ONCE_REWRITE_TAC[between]); (ONCE_REWRITE_TAC[DIST_0]); (CONV_TAC (PAT_CONV `\x. A /\ ~( _ = x + _ ) /\ ~( _ = _ + x)` (ONCE_REWRITE_CONV[DIST_SYM]))); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (ARITH_RULE `(a <= &2 * #1.26) /\ ~(a < &2) /\ (b <= &2 * #1.26) /\ ~(b < &2) ==> ~(&2 = a + b) /\ ~(b = &2 + a) /\ ~(a = b + &2)`)); (ONCE_REWRITE_TAC[GSYM h0]); (ASM_SIMP_TAC[]); (ASM_CASES_TAC `~(set_of_edge (w:real^3) (U:real^3->bool) (ECTC U) = {}) /\ ~(surrounded_node (U,ECTC U) w)`); (ABBREV_TAC `result:bool = (set_of_edge w U (ECTC U) = {} \/ surrounded_node (U,ECTC U) w)`); (MP_TAC (SPECL [`U:real^3 -> bool`;`w:real^3`] lemma2)); (ASM_SIMP_TAC[]); (STRIP_TAC); (MP_TAC (SPECL[`w:real^3`;`U:real^3->bool`] lemma3)); (ASM_SIMP_TAC[]); (STRIP_TAC); (Q_ABBREV_TAC `e1:real^3 = normalize w` "e1"); (Q_ABBREV_TAC `y:real^3 = w cross u` "y_axis"); (Q_ABBREV_TAC `e2:real^3 = normalize y` "e2"); (Q_ABBREV_TAC `e3:real^3 = e1 cross e2` "e3"); (* subgoal 8 *) (SUBGOAL_THEN `orthonormal (e1:real^3) e2 e3` ASSUME_TAC); (PURE_REWRITE_TAC[orthonormal]); (ONCE_REWRITE_TAC[GSYM NORM_EQ_1]); (* subgoal 8.1 *) (SUBGOAL_THEN `norm (e1:real^3) = &1` ASSUME_TAC); (Q_EXPAND_TAC "e1"); (MATCH_MP_TAC norm_normalize); (ASM_SIMP_TAC[]); (* subgoal 8.2 *) (SUBGOAL_THEN `norm (e2:real^3) = &1` ASSUME_TAC); (Q_EXPAND_TAC "e2"); (MATCH_MP_TAC norm_normalize); (Q_EXPAND_TAC "y_axis"); (ONCE_REWRITE_TAC[CROSS_EQ_0]); (ASM_SIMP_TAC[]); (* subgoal 8.3 *) (SUBGOAL_THEN `(e1:real^3) dot e2 = &0` ASSUME_TAC); (Q_EXPAND_TAC "e1"); (ONCE_REWRITE_TAC[GSYM dot_eq_0]); (Q_EXPAND_TAC "e2"); (ONCE_REWRITE_TAC[DOT_SYM]); (ONCE_REWRITE_TAC[GSYM dot_eq_0]); (Q_EXPAND_TAC "y_axis"); (SIMP_TAC[DOT_CROSS_SELF]); (* subgoal 8.4 *) (SUBGOAL_THEN `(e1:real^3) dot e3 = &0 /\ e2 dot e3 = &0` ASSUME_TAC); (Q_EXPAND_TAC "e3"); (SIMP_TAC[DOT_CROSS_SELF]); (* subgoal 8.5 *) (SUBGOAL_THEN `norm (e3:real^3) = &1` ASSUME_TAC); (Q_EXPAND_TAC "e3"); (MP_TAC(ISPECL [`e1:real^3`;`e2:real^3`] NORM_CROSS_DOT)); (ASM_SIMP_TAC[REAL_POW_2;REAL_MUL_RZERO;REAL_ADD_RID;REAL_MUL_RID]); (ONCE_REWRITE_TAC[GSYM REAL_POW_2]); (STRIP_TAC); (MP_TAC(SPECL [`norm (e3:real^3)`;`2`] REAL_POW_EQ_1_IMP)); (ASM_SIMP_TAC[ARITH_RULE `~(2 = 0)`]); (STRIP_TAC); (MATCH_MP_TAC (ARITH_RULE `abs x = &1 /\ &0 <= x ==> x = &1`)); (ASM_SIMP_TAC[NORM_POS_LE]); (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]); (ASM_SIMP_TAC[REAL_POW_2]); ARITH_TAC; (* subgoal 9 *) (SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U) ==> v dot e2 <= &0` ASSUME_TAC); (GEN_TAC); (STRIP_TAC); (ONCE_REWRITE_TAC[DOT_SYM]); (ONCE_REWRITE_TAC[ARITH_RULE `a <= &0 <=> &0 < --a \/ a = &0`]); (ONCE_REWRITE_TAC[VECTOR_ARITH `--((e2:real^3) dot v) = (--v) dot e2`]); (Q_EXPAND_TAC "e2"); (ONCE_REWRITE_TAC[GSYM dot_gt_0]); (ONCE_REWRITE_TAC[GSYM dot_eq_0]); (ONCE_REWRITE_TAC[VECTOR_ARITH ` --(v:real^3) dot y = -- (y dot v)`]); (ONCE_REWRITE_TAC[ARITH_RULE ` (&0 < --a \/ a = &0 )<=> a <= &0`]); (Q_EXPAND_TAC "y_axis"); (ASM_CASES_TAC `v:real^3 = u`); (* subgoal 9.1 *) (FIRST_ASSUM(fun thm -> SIMP_TAC[thm;DOT_CROSS_SELF])); ARITH_TAC; (* subgoal 9.2 *) (MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] lemma4)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT `A ==> (A ==>B) ==> B`)); (MP_TAC (SPEC `U:real^3 -> bool` UBHDEUU2_quasi)); (ASM_SIMP_TAC[]); (DISCH_TAC); (MP_TAC (SPECL [`U:real^3->bool`;`(ECTC U):(real^3->bool)->bool`;`w:real^3`; `u:real^3`;`v:real^3`] azim_ge_azim_dart)); (ASM_SIMP_TAC[]); (* subgoal 9.2.1 *) (SUBGOAL_THEN `~(w:real^3 = u)` ASSUME_TAC); (UNDISCH_TAC `u:real^3 IN set_of_edge w U (ECTC U)`); (MP_TAC(SPECL [`w:real^3`;`U:real^3->bool`] lemma8)); (ASM_SIMP_TAC[IN_ELIM_THM]); (STRIP_TAC); (STRIP_TAC); (ONCE_REWRITE_TAC[GSYM DIST_EQ_0]); (ASM_ARITH_TAC); (ASM_SIMP_TAC[]); (ASM_ARITH_TAC); (* subgoal 10 *) (SUBGOAL_THEN `?(a:real). &0 < a /\ a < pi /\ (&2 - &2 * cos a ) * ( norm (w:real^3) pow 2) < epsilon pow 2` ASSUME_TAC); (MP_TAC (SPEC `&0` REAL_CONTINUOUS_AT_COS)); (ONCE_REWRITE_TAC[real_continuous_atreal]); (DISCH_THEN (MP_TAC o (SPEC `epsilon pow 2 / (&2 * norm(w:real^3) pow 2)`))); (* subgoal 10.1 *) (SUBGOAL_THEN `&0 < epsilon pow 2/ (&2 * norm (w:real^3) pow 2)` ASSUME_TAC); (MATCH_MP_TAC REAL_LT_DIV); (CONJ_TAC); (* subgoal 10.1.1 *) (MATCH_MP_TAC REAL_POW_LT); (ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]); (* subgoal 10.1.2 *) (MATCH_MP_TAC (ARITH_RULE ` &0 < a ==> &0 < &2 * a`)); (MATCH_MP_TAC REAL_POW_LT); (ASM_SIMP_TAC[NORM_POS_LT]); (ASM_SIMP_TAC[COS_0;REAL_MUL_RID;REAL_SUB_RZERO]); (DISCH_THEN CHOOSE_TAC); (FIRST_X_ASSUM MP_TAC); STRIP_TAC; (Q_ABBREV_TAC `m:real = min (d / &2) (pi / &2)` "phi"); (EXISTS_TAC `m:real`); (* subgoal 10.2 *) (SUBGOAL_THEN `&0 < m:real` ASSUME_TAC); (Q_EXPAND_TAC "phi"); (SIMP_TAC[REAL_LT_MIN;PI2_BOUNDS]); (MATCH_MP_TAC REAL_LT_DIV); (ASM_ARITH_TAC); (* subgoal 10.3 *) (SUBGOAL_THEN `m < pi` ASSUME_TAC); (Q_EXPAND_TAC "phi"); (ONCE_REWRITE_TAC[REAL_MIN_LT]); (DISJ2_TAC); (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> a / &2 < a`)); (SIMP_TAC[PI_POS]); (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC [REAL_ARITH `(&2 - &2 * a) * b = (&1 - a) * (&2 * b)`]); (MP_TAC (SPECL [`&1 - cos (m:real)`;`epsilon:real pow 2`; `&2 * norm (w:real^3) pow 2`] REAL_LT_RDIV_EQ)); (* subgoal 10.4 *) (SUBGOAL_THEN `&0 < &2 * norm (w:real^3) pow 2` ASSUME_TAC); (ONCE_REWRITE_TAC[ARITH_RULE `&0 < &2 * a <=> &0 < a`]); (MATCH_MP_TAC REAL_POW_LT); (ASM_SIMP_TAC[NORM_POS_LT]); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT `A ==> (A <=> B ) ==> B`)); (MATCH_MP_TAC (REAL_ARITH `abs a < b ==> a < b`)); (ONCE_REWRITE_TAC[REAL_ARITH `abs (a - b) = abs (b - a)`]); (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm)); (* subgoal 10.5 *) (SUBGOAL_THEN `abs (m:real) = m` ASSUME_TAC); (ONCE_REWRITE_TAC[REAL_ABS_REFL]); (ASM_ARITH_TAC); (ASM_SIMP_TAC[]); (Q_EXPAND_TAC "phi"); (ONCE_REWRITE_TAC[REAL_MIN_LT]); (DISJ1_TAC); ASM_ARITH_TAC; (FIRST_X_ASSUM CHOOSE_TAC); (Q_ABBREV_TAC `s:real^3 = (cos a * norm (w:real^3)) % e1 + (sin a * norm w) % e2` "subs_point"); (Q_ABBREV_TAC `U':real^3 -> bool = s INSERT (U DELETE w)` "new_set"); (* subgoal 11 *) (SUBGOAL_THEN `!(v:real^3). v IN U /\ ~(v = w) ==> &2 < dist (s,v)` (LABEL_TAC "dist_gt_2")); (GEN_TAC); (STRIP_TAC); (ASM_CASES_TAC `(v:real^3) IN set_of_edge w U (ECTC U)`); (* subgoal 11.1 *) (SUBGOAL_THEN `dist ((w:real^3),v) = &2` ASSUME_TAC); (FIRST_X_ASSUM MP_TAC); (MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`)); (SIMP_TAC[IN_ELIM_THM]); (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm])); (MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`; `e1:real^3`;`e2:real^3`;`e3:real^3`] lemma7)); (ASM_SIMP_TAC[NORM_POS_LT]); (DISCH_THEN (fun thm -> MATCH_MP_TAC (SPEC `v:real^3` thm))); (ASM_SIMP_TAC[]); (Q_EXPAND_TAC "e1"); (ONCE_REWRITE_TAC[GSYM dot_gt_0]); (ONCE_REWRITE_TAC[ARITH_RULE `&0 < a <=> a > &0`]); (ONCE_REWRITE_TAC[DOT_SYM]); (MP_TAC (SPECL [`U:real^3->bool`;`w:real^3`] lemma5)); (ASM_SIMP_TAC[]); (* subgoal 11.2 *) (ONCE_REWRITE_TAC[DIST_SYM]); (MATCH_MP_TAC (REAL_ARITH `&2 < dist (v:real^3,w) - dist (s,w) /\ dist (v,w) - dist (s,w) <= a ==> &2 < a`)); (SIMP_TAC[Pack1.real_sub_norm]); (MATCH_MP_TAC (REAL_ARITH `a > &2 + (epsilon:real) /\ b < epsilon ==> &2 < a - b`)); (ONCE_REWRITE_TAC[DIST_SYM]); (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC[DIST_SYM]); (PURE_REWRITE_TAC[dist]); (ONCE_REWRITE_TAC[NORM_LT_SQUARE]); (ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]); (* subgoal 11.2.1 *) (SUBGOAL_THEN `s:real^3 - w = ((cos (a:real) - &1) * norm (w:real^3)) % e1 + (sin a * norm w) % e2 + &0 % e3` ASSUME_TAC); (* subgoal 11.2.1.1 *) (SUBGOAL_THEN `w:real^3 = norm w % e1` ASSUME_TAC); (Q_EXPAND_TAC "e1"); (SIMP_TAC[norm_mul_normalize]); (FIRST_X_ASSUM(fun thm -> CONV_TAC(PAT_CONV `\x. s - x = A` (ONCE_REWRITE_CONV[thm])))); (Q_EXPAND_TAC "subs_point"); (SIMP_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_RID]); (ONCE_REWRITE_TAC[VECTOR_ARITH `(a % (e1:real^3) + b % e2) - c % e1 = (a - c) % e1 + b % e2`]); (SIMP_TAC[ARITH_RULE `a * b - b = (a - &1) * b`]); (MP_TAC (SPECL [`s:real^3 - w`;`s:real^3 - w`;`e1:real^3`;`e2:real^3`;`e3:real^3`; `(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`; `(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`] dot_coordinates_2)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT `B ==> A ==> B`)); (ONCE_REWRITE_TAC [REAL_ARITH `(a * b) * a * b + (c * b) * c * b + &0 * &0 = (a * a + c * c) * b pow 2`]); (ONCE_REWRITE_TAC [REAL_ARITH `(a - &1) * (a - &1) + b * b = &1 - &2 * a + b pow 2 + a pow 2`]); (SIMP_TAC[SIN_CIRCLE]); (ASM_SIMP_TAC[REAL_ARITH `&1 - b + &1 = &2 - b`]); (* subgoal 12 *) (SUBGOAL_THEN `!(v:real^3). v IN U' /\ ~(v = s) ==> &2 < dist (s,v)` (LABEL_TAC "iso")); (GEN_TAC); (Q_EXPAND_TAC "new_set"); (SIMP_TAC[IN_INSERT; TAUT ` ((A \/ B) /\ ~A) <=> (~A /\ B)`]); (SIMP_TAC[IN_DELETE]); (ASM_SIMP_TAC[]); (* subgoal 13 *) (SUBGOAL_THEN `~(s:real^3 IN U)` ASSUME_TAC); (ONCE_REWRITE_TAC[SET_RULE `~(x IN S) <=> (!y. y IN S ==> ~(x = y))`]); GEN_TAC; STRIP_TAC; (ASM_CASES_TAC `y':real^3 = w`); (* subgoal 13.1 *) (ASM_SIMP_TAC[]); (* subgoal 13.1.1 *) (SUBGOAL_THEN `w:real^3 = norm w % e1 + &0 % e2 + &0 % e3` ASSUME_TAC); (SIMP_TAC[ VECTOR_ARITH `a % e1 + &0 % e2 + &0 % e3 = a % e1`]); (Q_EXPAND_TAC "e1"); (SIMP_TAC[norm_mul_normalize]); (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[thm])); (USE_THEN "subs_point" (fun thm -> ONCE_REWRITE_TAC[GSYM thm])); (CONV_TAC(PAT_CONV `\x. ~(x = A)` (ONCE_REWRITE_CONV[ VECTOR_ARITH `a % e1 + b % e2 = a % e1 + b % e2 + &0 % e3`]))); (MP_TAC ( SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`; `cos a * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`; `norm (w:real^3)`;`&0`;`&0`] ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT )); (MATCH_MP_TAC(TAUT `(A /\ ~C) ==> ((A ==> ( B <=> C)) ==> ~B) `)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT `~B ==> ~ (A /\ B)`)); (SIMP_TAC[REAL_ENTIRE]); (SIMP_TAC[TAUT `~(A \/ B) <=> ~A /\ ~B`]); CONJ_TAC; (* subgoal 13.1.2 *) (ASM_SIMP_TAC[PI_WORKS]); (* subgoal 13.1.3 *) (MATCH_MP_TAC(ARITH_RULE `&0 < x ==> ~(x = &0)`)); (ASM_SIMP_TAC[NORM_POS_LT]); (* subgoal 13.2 *) (ONCE_REWRITE_TAC[DIST_NZ]); (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &0 < a`)); (USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm)); (ASM_SIMP_TAC[]); (* subgoal 14 *) (SUBGOAL_THEN `U':real^3 -> bool IN S` ASSUME_TAC); (EXPAND_TAC "S"); (SIMP_TAC[IN_ELIM_THM]); (* subgoal 14.1 *) (SUBGOAL_THEN `norm (s:real^3) = norm (w:real^3)` ASSUME_TAC); (MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`; `e1:real^3`;`e2:real^3`;`e3:real^3`] lemma6)); (ASM_SIMP_TAC[]); (* subgoal 14.2 *) (SUBGOAL_THEN `FINITE (U':real^3->bool)` ASSUME_TAC); (Q_EXPAND_TAC "new_set"); (ONCE_REWRITE_TAC[FINITE_INSERT]); (ASM_SIMP_TAC[FINITE_DELETE]); (* subgoal 14.3 *) (SUBGOAL_THEN `packing (U':real^3 -> bool)` ASSUME_TAC); (PURE_REWRITE_TAC[packing]); (REPEAT GEN_TAC); (CONV_TAC(PAT_CONV `\x. x /\ x /\ A ==> B` (ONCE_REWRITE_CONV[GSYM IN]))); (STRIP_TAC); (ASM_CASES_TAC `u':real^3 = s`); (* subgoal 14.3.1 *) (ASM_SIMP_TAC[]); (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`)); (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm)); (ASM_SIMP_TAC[]); (FIRST_X_ASSUM(fun thm-> ONCE_REWRITE_TAC[GSYM thm])); (ASM_SIMP_TAC[EQ_SYM_EQ]); (ASM_CASES_TAC `v:real^3 = s`); (* subgoal 14.3.2.1 *) (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC[DIST_SYM]); (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`)); (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm)); (ASM_SIMP_TAC[]); (* subgoal 14.3.2.2 *) (UNDISCH_TAC `u':real^3 IN U'`); (Q_EXPAND_TAC "new_set"); (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]); (STRIP_TAC); (UNDISCH_TAC `v:real^3 IN U'`); (Q_EXPAND_TAC "new_set"); (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]); (STRIP_TAC); (UNDISCH_TAC `packing (U:real^3->bool)`); (PURE_REWRITE_TAC[packing]); (DISCH_THEN (fun thm -> MATCH_MP_TAC (SPECL [`u':real^3`;`v:real^3`] thm))); (CONV_TAC(PAT_CONV `\x. x /\ x /\ A` (ONCE_REWRITE_CONV[GSYM IN]))); (ASM_SIMP_TAC[]); (ASM_SIMP_TAC[]); (Q_ABBREV_TAC `(h:real^3->real^3) = (\v. if v = w then s else v)` "h"); (EXISTS_TAC `(h:real^3->real^3) o (phi:real^3->real^3)`); (CONJ_TAC); (* subgoal 14.4 *) (MATCH_MP_TAC Hypermap.COMPOSE_BIJ); (EXISTS_TAC `U:real^3->bool`); (ASM_SIMP_TAC[]); (* subgoal 14.4.1 *) (SUBGOAL_THEN `!v:real^3. v IN U ==> (h:real^3->real^3) v IN U'` ASSUME_TAC); (REPEAT STRIP_TAC); (Q_EXPAND_TAC "h"); (SIMP_TAC[BETA_THM]); (COND_CASES_TAC); (* subgoal 14.4.1.1 *) (Q_EXPAND_TAC "new_set"); (SET_TAC[]); (* subgoal 14.5.1.2 *) (Q_EXPAND_TAC "new_set"); (SIMP_TAC[IN_INSERT]); (DISJ2_TAC); (ASM_SIMP_TAC[IN_DELETE]); (ASM_SIMP_TAC[BIJ;INJ;SURJ]); (CONJ_TAC); (* subgoal 14.5.2 *) (REPEAT STRIP_TAC); (UNDISCH_TAC `(h:real^3->real^3) x = h y'`); (Q_EXPAND_TAC "h"); (SIMP_TAC[BETA_THM]); (COND_CASES_TAC); (* subgoal 14.5.2.1 *) (COND_CASES_TAC); (* subgoal 14.5.2.1.1 *) (ASM_SIMP_TAC[]); (* subgoal 14.5.2.1.2 *) (ASM_MESON_TAC[]); (* subgoal 14.5.2.2 *) (COND_CASES_TAC); (* subgoal 14.5.2.2.1 *) (ASM_MESON_TAC[]); (* subgoal 14.5.2.2.2 *) (SIMP_TAC []); (* subgoal 14.5.3 *) (REPEAT STRIP_TAC); (ASM_CASES_TAC `x:real^3 = s`); (* subgoal 14.5.3.1 *) (EXISTS_TAC `w:real^3`); (ASM_SIMP_TAC[]); (Q_EXPAND_TAC "h"); (SIMP_TAC[BETA_THM]); (* subgoal 14.5.3.2 *) (EXISTS_TAC `x:real^3`); (UNDISCH_TAC `x:real^3 IN U'`); (Q_EXPAND_TAC "new_set"); (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]); (STRIP_TAC); (Q_EXPAND_TAC "h"); (ASM_SIMP_TAC[BETA_THM]); (REPEAT STRIP_TAC); (SIMP_TAC[o_THM]); (* subgoal 14.6 *) (SUBGOAL_THEN `! x:real^3. x IN U ==> norm x = norm ((h:real^3->real^3) x)` MATCH_MP_TAC); (REPEAT STRIP_TAC); (Q_EXPAND_TAC "h"); (SIMP_TAC[BETA_THM]); (COND_CASES_TAC); (* subgoal 14.6.1 *) (ASM_SIMP_TAC[]); (* subgoal 14.6.2 *) (SIMP_TAC[]); (UNDISCH_TAC `BIJ (phi:real^3->real^3) V U`); (SIMP_TAC[BIJ]); (DISCH_THEN (fun thm -> MP_TAC (CONJUNCT1 thm))); (SIMP_TAC[INJ]); (DISCH_THEN (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm))); (ASM_SIMP_TAC[]); (* subgoal 15 *) (SUBGOAL_THEN `~((f:(real^3->bool)->num) U' <= f U)` ASSUME_TAC); (ONCE_REWRITE_TAC[ ARITH_RULE `~((a:num) <= b) <=> (b < a)`]); (EXPAND_TAC "f"); (MATCH_MP_TAC CARD_PSUBSET); (CONJ_TAC); (* subgoal 15.1 *) (ONCE_REWRITE_TAC[PSUBSET_ALT]); (CONJ_TAC); (* subgoal 15.1.1 *) (ONCE_REWRITE_TAC[SUBSET]); GEN_TAC; (ONCE_REWRITE_TAC[set_of_iso]); (SIMP_TAC[IN_ELIM_THM]); (STRIP_TAC); (* subgoal 15.1.1.1 *) (SUBGOAL_THEN `x:real^3 IN U'` ASSUME_TAC); (Q_EXPAND_TAC "new_set"); (SIMP_TAC[IN_INSERT]); DISJ2_TAC; (SIMP_TAC[IN_DELETE]); (ASM_SIMP_TAC[]); (ASM_MESON_TAC[]); (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC[GSYM SUBSET_EMPTY]); (UNDISCH_TAC `set_of_edge x U (ECTC U) = {}`); (DISCH_THEN(fun thm -> ONCE_REWRITE_TAC[GSYM thm])); (MP_TAC (SPECL [`x:real^3`;`U:real^3->bool`] lemma8)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`)); (MP_TAC (SPECL [`x:real^3`;`U':real^3->bool`] lemma8)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`)); (SIMP_TAC[SUBSET;IN_ELIM_THM]); GEN_TAC; (Q_EXPAND_TAC "new_set"); (SIMP_TAC[IN_INSERT;IN_DELETE]); (MATCH_MP_TAC (TAUT `(D ==> ~A) ==> (A \/ B /\ C) /\ D ==> B`)); (MATCH_MP_TAC (TAUT `(B ==> ~A) ==> (A ==> ~B)`)); STRIP_TAC; (ASM_SIMP_TAC[]); (ONCE_REWRITE_TAC[DIST_SYM]); (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~(a = &2)`)); (USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm)); (ASM_SIMP_TAC[]); (ASM_SET_TAC[]); (* subgoal 15.2 *) (EXISTS_TAC `s:real^3`); (CONJ_TAC); (* subgoal 15.2.1 *) (SIMP_TAC[set_of_iso;IN_ELIM_THM]); (* subgoal 15.2.1.1 *) (SUBGOAL_THEN `s:real^3 IN U'` ASSUME_TAC); (Q_EXPAND_TAC "new_set"); (SET_TAC[]); (ASM_SIMP_TAC[]); (MP_TAC (SPECL [`s:real^3`;`U':real^3->bool`] lemma8)); (ASM_SIMP_TAC[]); (MATCH_MP_TAC (TAUT ` B ==> A ==> B`)); (ONCE_REWRITE_TAC[SET_RULE `{x| P x} = {} <=> !x. ~(P x)`]); (GEN_TAC); (MATCH_MP_TAC (TAUT ` (A ==> ~B) ==> ~(A /\ B)`)); (STRIP_TAC); (ASM_CASES_TAC `v:real^3 = s`); (* subgoal 15.2.1.2 *) (ASM_SIMP_TAC[DIST_REFL]); ARITH_TAC; (* subgoal 15.2.1.3 *) (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~ (a = &2)`)); (USE_THEN "iso" (fun thm -> MATCH_MP_TAC thm)); (ASM_SIMP_TAC[]); (* subgoal 15.2.2 *) (ASM_SIMP_TAC[set_of_iso;IN_ELIM_THM]); (MATCH_MP_TAC ( ISPECL [`set_of_iso (U':real^3->bool)`; `U':real^3->bool`] FINITE_SUBSET)); (ASM_SIMP_TAC[set_of_iso]); (SET_TAC[]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); ]);; end;;