(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                                   *)
(* Author: Nguyen Quang Truong                                          *)
(* Date: 2013 - 5 - 31                                                        *)
(* ========================================================================== *)


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




module Lunar_deform = struct


open Hales_tactic;;
open Localization;;
open Wrgcvdr_cizmrrh;;
open Fan;;
open Fan_defs;;
open Localization;;
open Hypermap;;
open Hypermap_iso;;
open Conforming;;
open Sphere;;


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




(*
let asms_search0 sths =
  let rec immediatesublist l1 l2 =
    match (l1,l2) with
      [],_ -> true
    | _,[] -> false
    | (h1::t1,h2::t2) -> h1 = h2 & immediatesublist t1 t2 in
  let rec sublist l1 l2 =
    match (l1,l2) with
      [],_ -> true
    | _,[] -> false
    | (h1::t1,h2::t2) -> immediatesublist l1 l2 or sublist l1 t2 in
  let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th)
  and name_contains s (n,th) = sublist (explode s) (explode n) in
  let rec filterpred tm =
    match tm with
      Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
    | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
    | Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
    | pat -> exists_subterm_satisfying (can (term_match [] pat)) in
  fun pats ->
    let triv,nontriv = partition is_var pats in
    (if triv <> [] then
      warn true
         ("Ignoring plain variables in search: "^
          end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
     else ());
    (if nontriv = [] & triv <> [] then []
     else itlist (filter o filterpred) pats sths);;

let asms_search tms =
  let gstk = !current_goalstack in
  match gstk with
    [] -> []
  | (meta,gl::_,just)::_
       -> let (sths,_) = gl in
          map snd (asms_search0 sths tms)
  | _  -> failwith "asm_searchs: Invalid goal state";;

let ASMS_SEARCH_TCL (tms:(term)list) (thstac:(thm)list->tactic) : tactic =
  fun (gl:goal) ->
  let (sths,tm) = gl in
  let ths1 = map snd (asms_search0 sths tms) in
  thstac ths1 gl;;

let ASM_SEARCH_TCL (tms:(term)list) (thstac:thm->tactic) : tactic =
  let foo ths = match ths with
                  [] -> failwith "ASM_SEARCH_TCL: No matching asms found"
                | _  -> thstac (hd ths) in
  ASMS_SEARCH_TCL tms foo;;

let ASM_SEARCH_TC = asms_search;;
*)

let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;

let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (SPEC_ALL ( tm ))];;

let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `; MESON[]`
a ==> b ==> c <=> a /\ b ==> c `];;

let DOWN_TAC = REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IMP_IMP] THEN PHA;;


let DOWN = FIRST_X_ASSUM MP_TAC;;

let DOWNS n = REPLICATE_TAC n DOWN THEN PHA;;

let REMOVE_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (TAUT` a ==> b ==> a`);;


(*
let types_thm th = let cl = concl th in
List.map dest_var (frees cl );;

let seans_fn () =
let (tms,tm) = top_goal () in
let vss = map frees (tm::tms) in
let vs = setify (flat vss) in
map dest_var vs;;
*)




let PAT_REWRITE_TAC tm thms =
(CONV_TAC (PAT_CONV tm (REWRITE_CONV thms )));;

let FOR_ASM th =
let th1 = REWRITE_RULE[MESON[]` a /\ b ==> c <=>
a ==> b ==> c `] th in
let th2 = SPEC_ALL th1 in UNDISCH_ALL th2;;

(* change a th having form |- A ==> t to the form A |- t
to get ready to some other commands


|- A ==> t
----------- FOR_ASM
A |- t
*)

let ASSUME_TAC2 = ASSUME_TAC o FOR_ASM;;


let PAT_ONCE_REWRITE_TAC tm thms =
(CONV_TAC (PAT_CONV tm (ONCE_REWRITE_CONV thms )));;

let ASM_PAT_RW_TAC tm thms = EVERY_ASSUM (fun th ->
(CONV_TAC (PAT_CONV tm (ONCE_REWRITE_CONV
( th ::[ thms ] )))));;

let PAT_TH_TAC tm th =
(CONV_TAC (PAT_CONV tm (REWRITE_CONV[th] )));;


let IMP_TO_EQ_RULE th = MATCH_MP (TAUT` (a ==> b ) ==>
( a <=> a /\ b )`) (SPEC_ALL th);;

let NHANH_PAT tm th = PAT_ONCE_REWRITE_TAC tm
[ IMP_TO_EQ_RULE th ];;


let MAKE_FIRST_TAC tm = UNDISCH_TAC tm THEN DISCH_TAC;;


(* ---------- BG TEST ------------- *)


(*
let rec els L = match L with
[] -> p ()
| (x::l) -> e x; els l;;

let rec bls L = match L with
[] -> p ()
| (x::l) -> b (); bls l;;
*)

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



let CONS_IMP_CONTINUOUS_ATREAL = 
prove_by_refinement(` (! t. t IN real_interval (a,b) ==> f t = (u:real^N) ) ==> (! t. t IN real_interval (a,b) ==> f continuous atreal t ) `,
[REWRITE_TAC[continuous_atreal; real_interval; IN_ELIM_THM]; REPEAT STRIP_TAC; EXISTS_TAC` min (b - t ) ( t - a ) ` ; CONJ_TAC; REWRITE_TAC[REAL_LT_MIN]; ASM_REAL_ARITH_TAC; GEN_TAC; REWRITE_TAC[REAL_LT_MIN]; STRIP_TAC; ASSUME_TAC2 (REAL_ARITH` a < t /\ t < b /\ abs (x' - t) < b - t /\ abs (x' - t) < t - a ==> x' < b /\ a < x' `); SUBGOAL_THEN ` f (x':real) = (u:real^N) ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[DIST_REFL]]);;
let AFF_GT_SUBSET_AFFINE_HULL21 = ISPECL [` {u, v:real^N} `;` {w:real^N } `] AFF_GT_SUBSET_AFFINE_HULL;;
let DISJTINCT_PROPERTY = 
prove_by_refinement ( ` FINITE V /\ (f : real^N -> real -> real^N) u continuous atreal (&0) /\ f u (&0) = u /\ a < &0 /\ &0 < b /\ (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') ==> (?e. &0 < e /\ (!t u'. --e < t /\ t < e /\ u' IN V /\ ~(u' = u) ==> ~(f u t = f u' t)))`,
[ STRIP_TAC; SUBGOAL_THEN`!u'. u' IN V /\ ~(u = u') ==> (!t. t IN real_interval (a,b) ==> (f: real^N -> real -> real^N) u' continuous atreal t )` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; MATCH_MP_TAC (GEN`u: real^N ` CONS_IMP_CONTINUOUS_ATREAL); EXISTS_TAC` u': real^N `; REPEAT STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; MP_TAC (ISPECL [` &0 `;` u:real^N `;` f: real^N -> real -> real^N `; ` V:real^N -> bool `] (GEN_ALL Local_lemmas1.CONTINUOUS_FUN_DISTINCT_FINITE_SET)); ANTS_TAC; ASM_REWRITE_TAC[]; ANTS_TAC; CONJ_TAC; REPEAT STRIP_TAC; SUBGOAL_THEN` &0 IN real_interval (a,b) ` MP_TAC; ASM_REWRITE_TAC[real_interval; IN_ELIM_THM]; ASM_MESON_TAC[]; GEN_TAC; REWRITE_TAC[IN_INSERT]; STRIP_TAC; ASM_REWRITE_TAC[]; SUBGOAL_THEN` &0 IN real_interval (a,b) ` MP_TAC; ASM_REWRITE_TAC[real_interval; IN_ELIM_THM]; ASM_MESON_TAC[]; REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT]; MESON_TAC[]]);;
let EDGE_FORM_IN_LOCAL_FAN = 
prove_by_refinement( ` local_fan (V,E,FF) /\ x IN E ==> ? u v. ~( u = v ) /\ {u, v} = x `,
[REWRITE_TAC[local_fan; FAN; graph; IN]; LET_TAC; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x:real^3 -> bool `)); DOWN; REWRITE_TAC[Local_lemmas1.HAS_SIZE_2_EXISTS2]; MESON_TAC[]]);;
let EDGE_IN_LOCAL_FAN_DET_RHO_NODE = 
prove_by_refinement (` local_fan (V,E,FF) /\ x IN E ==> (?v. v IN V /\ {v, rho_node1 FF v} = x) `,
[NHANH EDGE_FORM_IN_LOCAL_FAN; STRIP_TAC; UNDISCH_TAC` (x:real^3 -> bool) IN E `; UNDISCH_TAC` local_fan (V,E,FF) `; PHA; EXPAND_TAC "x";
NHANH Local_lemmas.LOFA_IN_E_IMP_IN_FF; STRIP_TAC; DOWN; UNDISCH_TAC` local_fan (V,E,FF) `; PHA; NHANH Local_lemmas.DETER_RHO_NODE; STRIP_TAC; EXISTS_TAC `u: real^3 `; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V; Local_lemmas.DETER_RHO_NODE; INSERT_COMM]; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V; Local_lemmas.DETER_RHO_NODE; INSERT_COMM]]);;
let TOW_POINTS_IN_IMP_AFF_GT_SUBSET = 
prove_by_refinement (` DISJOINT {x, u} {v:real^N } /\ a IN aff_gt {x,u} {v} /\ b IN aff_gt {x, u} {v} /\ DISJOINT {x} {a,b} ==> aff_gt {x} {a,b} SUBSET aff_gt {x,u} {v} `,
[NHANH AFF_GT_2_1; NHANH AFF_GT_1_2; STRIP_TAC; UNDISCH_TAC` a IN aff_gt {x, u} {v:real^N }`; UNDISCH_TAC` b IN aff_gt {x, u} {v:real^N }`; ASM_REWRITE_TAC[IN_ELIM_THM; SUBSET]; STRIP_TAC; STRIP_TAC; GEN_TAC; STRIP_TAC; DOWN; ASM_REWRITE_TAC[]; REWRITE_TAC[VECTOR_ARITH` t1'' % x + t2'' % (t1' % x + t2' % u + t3' % v) + t3'' % (t1 % x + t2 % u + t3 % v) = (t1'' + t2'' * t1' + t3'' * t1 ) % x + (t2'' * t2' + t3'' * t2) % u + (t2'' * t3' + t3'' * t3 ) % v `]; STRIP_TAC; EXISTS_TAC` (t1'' + t2'' * t1' + t3'' * t1:real) `; EXISTS_TAC` t2'' * t2' + t3'' * t2:real `; EXISTS_TAC` t2'' * t3' + t3'' * t3 `; CONJ_TAC; MATCH_MP_TAC Real_ext.REAL_PROP_POS_ADD2; ASM_MESON_TAC[REAL_LT_MUL]; ASM_REWRITE_TAC[]; UNDISCH_TAC` t1' + t2' + t3' = &1 `; UNDISCH_TAC` t1 + t2 + t3 = &1 `; UNDISCH_TAC` t1'' + t2'' + t3'' = &1 `; PHA; CONV_TAC REAL_RING]);;
let REAL_LT_MUL12 = 
prove(` &0 < b /\ a < &0 ==> a * b < &0 `,
REWRITE_TAC[REAL_ARITH` a * b < &0 <=> &0 < (-- a) * (b ) `] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN DOWN_TAC THEN REAL_ARITH_TAC);;
let COLL_IN_AFF_GT_INTER_EMPTY = 
prove_by_refinement (` ~ collinear {a,b,x: real^N} /\ u IN aff_gt {a,b} {x} ==> aff_gt {a, b} {x} INTER aff_lt {a} {u} = {} `,
[NHANH Local_lemmas.COLL_IN_AFF_GT_TOO; NHANH Fan.th3a; STRIP_TAC; DOWN; NHANH (SET_RULE` DISJOINT {a, b} {u} ==> DISJOINT {a} {u} `); NHANH AFF_LT_1_1; STRIP_TAC; UNDISCH_TAC` DISJOINT {a, b} {x: real^N} `; NHANH AFF_GT_2_1; STRIP_TAC; UNDISCH_TAC` u IN aff_gt {a, b} {x: real^N} `; ASM_REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; REWRITE_TAC[SET_RULE` A INTER B = {} <=> (! x. x IN B ==> ~( x IN A)) `]; REWRITE_TAC[IN_ELIM_THM]; GEN_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[Local_lemmas.VECTOR_ADD_LDISTRIB1]; STRIP_TAC; SUBGOAL_THEN` (t1' + t2' * t1 ) + (t2' * t2 ) + (t2' * t3) = &1 ` ASSUME_TAC; ASM_REWRITE_TAC[REAL_RING` (t1' + t2' * t1) + t2' * t2 + t2' * t3 = t1' + t2' * (t1 + t2 + t3 ) `; REAL_ARITH` a * &1 = a `]; ABBREV_TAC` vv: real^N = t1'' % a + t2'' % b + t3' % x ` ; SUBGOAL_THEN` (vv: real^N) IN affine hull {a, b, x} ` ASSUME_TAC; ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM]; ASM_MESON_TAC[]; UNDISCH_TAC` ~collinear {a, b, x:real^N} `; DOWN THEN PHA; NHANH Collect_geom.lemma11; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [` t1'': real `;` t2'': real `;` t3': real `])); ANTS_TAC; ASM_REWRITE_TAC[]; FIRST_ASSUM (MP_TAC o (SPECL [` (t1': real) + t2' * t1`;`( t2': real ) * t2 `;` (t2': real) * t3 `])); ANTS_TAC; ASM_REWRITE_TAC[]; UNDISCH_TAC` t1' % a + (t2' * t1) % a + (t2' * t2) % b + (t2' * t3) % x = (vv: real^N) `; ASM_REWRITE_TAC[]; DISCH_THEN (SUBST1_TAC o SYM); CONV_TAC VECTOR_ARITH; STRIP_TAC; STRIP_TAC; DOWN; EXPAND_TAC "t3''";
ASSUME_TAC2 (SPECL [` t2': real `;` t3: real `] (GEN_ALL REAL_LT_MUL12)); DOWN; UNDISCH_TAC` &0 < t3' `; REAL_ARITH_TAC]);;
let HKIRPEP_ALT = 
prove(` convex_local_fan (V,E,FF) /\ lunar (v,w) V E ==> (!u. u IN V DIFF {v, w} ==> interior_angle1 (vec 0) FF u = pi) /\ &0 < interior_angle1 (vec 0) FF v /\ interior_angle1 (vec 0) FF v <= pi /\ interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w /\ (?i j. i + j = CARD V /\ i < CARD V /\ ~(i = 0) /\ ~(i = 1) /\ w = ITER i (rho_node1 FF) v /\ {ITER l (rho_node1 FF) v | 0 < l /\ l < i} = aff_gt {vec 0, v} {rho_node1 FF v} INTER V /\ j < CARD V /\ ~(j = 0) /\ ~(j = 1) /\ v = ITER j (rho_node1 FF) w /\ {ITER l (rho_node1 FF) w | 0 < l /\ l < j} = aff_gt {vec 0, v} {ivs_rho_node1 FF v} INTER V) `,
NHANH Local_lemmas.HKIRPEP THEN STRIP_TAC THEN UNDISCH_TAC` v = ITER j (rho_node1 FF) w ` THEN UNDISCH_TAC` w = ITER i (rho_node1 FF) v ` THEN DISCH_THEN (ASSUME_TAC o SYM) THEN DISCH_THEN (ASSUME_TAC o SYM) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC` i: num ` THEN EXISTS_TAC` j:num ` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (GEN_ALL Local_lemmas1.CARD_V_TWO_HAFL_CIRCLE) THEN EXISTS_TAC` E: (real^3 -> bool) -> bool ` THEN EXISTS_TAC` FF: real^3 # real^3 -> bool ` THEN EXISTS_TAC` w:real^3 ` THEN EXISTS_TAC` v: real^3 ` THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC` convex_local_fan (V,E,FF)` THEN UNDISCH_TAC ` lunar (v,w:real^3) V E ` THEN SIMP_TAC[convex_local_fan; lunar; INSERT_SUBSET]);;
let LUNAR_IMP_IN_TWO_HAFLS_PLANE = 
prove_by_refinement (` convex_local_fan (V,E,FF) /\ lunar (v,w) V E ==> (! u. u IN V /\ ~( u = v ) /\ ~( u = w) ==> u IN aff_gt {vec 0, v} {rho_node1 FF v} \/ u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} ) `,
[NHANH HKIRPEP_ALT; STRIP_TAC; ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO; SUBGOAL_THEN` lunar (v,w:real^3) V E ` MP_TAC; FIRST_X_ASSUM ACCEPT_TAC; REWRITE_TAC[lunar; circular; INSERT_SUBSET]; STRIP_TAC; ASSUME_TAC2 (SPEC_ALL Localization.LOFA_IMP_LT_CARD_SET_V_ALT); GEN_TAC THEN STRIP_TAC; UNDISCH_TAC` (u:real^3) IN V `; EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; ASM_CASES_TAC` n = 0 `; FIRST_X_ASSUM (SUBST_ALL_TAC); DOWN; UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[ITER]; ASM_CASES_TAC` n < (i:num) `; DISJ1_TAC; UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n: num `; ASM_REWRITE_TAC[]; UNDISCH_TAC` ~( n = 0) `; ARITH_TAC; ASM_SIMP_TAC[IN_INTER]; ASM_CASES_TAC` n = (i:num) `; UNDISCH_TAC` u = ITER n (rho_node1 FF) v `; UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; DISJ2_TAC; SUBGOAL_THEN`u IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n - (i:num ) `; UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; EXPAND_TAC "w"; REWRITE_TAC[ITER_ADD]; ASSUME_TAC2 (ARITH_RULE` ~( n < i) ==> n - i + i = (n:num ) `); ASM_REWRITE_TAC[]; ASSUME_TAC2 (ARITH_RULE` ~(n < i) ==> (n - i < j <=> (n:num) < i + j ) `); ASM_REWRITE_TAC[ARITH_RULE` 0 < n - i <=> ~( n < i ) /\ ~( n = (i:num)) `]; UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); ASM_SIMP_TAC[IN_INTER]]);;
let IN_CONV0_IMP_AFF_EQ1 = 
prove(` a IN conv0 {x, y} ==> aff {a, x} = aff {a, y} `,
NHANH Local_lemmas.IN_CONV0_IMP_AFF_EQ THEN ONCE_REWRITE_TAC[INSERT_COMM] THEN NHANH Local_lemmas.IN_CONV0_IMP_AFF_EQ THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[INSERT_COMM]);;
let AFF_LT_SUBSET_AFF11 = 
prove_by_refinement ( ` DISJOINT {a} {b} ==> aff_lt {a} {b} SUBSET aff {a,b:real^N} `,
[NHANH AFF_LT_1_1; SIMP_TAC[Collect_geom.AFF_2POINTS_INTERPRET; SUBSET; IN_ELIM_THM]; STRIP_TAC; GEN_TAC; STRIP_TAC; EXISTS_TAC` t1: real `; EXISTS_TAC` t2: real `; ASM_REWRITE_TAC[]]);;
let IN_AFF_LT_STILL_NOT_COLLINEAR = 
prove_by_refinement (` ~ collinear {x: real^N,y,a} /\ b IN aff_lt {x, y} {a} ==> ~ collinear {x,y,b} `,
[REPEAT STRIP_TAC; UNDISCH_TAC` b IN aff_lt {x, y} {a: real^N} `; PHA; UNDISCH_TAC ` ~collinear {x, y, a: real^N} `; NHANH Fan.th3a; NHANH AFF_LT_2_1; SIMP_TAC[IN_ELIM_THM]; REPEAT STRIP_TAC; UNDISCH_TAC` ~collinear {x, y, a:real^N} `; PHA; UNDISCH_TAC` collinear {x,y,b:real^N} `; REWRITE_TAC[Local_lemmas.collinear_fan22; Collect_geom.AFF_2POINTS_INTERPRET; IN_ELIM_THM]; STRIP_TAC; DISJ1_TAC; DOWN; ASM_REWRITE_TAC[]; REWRITE_TAC[ VECTOR_ARITH` t1 % x + t2 % y + t3 % a = ta % x + tb % y <=> t3 % a = (ta - t1) % x + (tb - t2) % y `]; NHANH_PAT`\x. x ==> y ` (MESON[]` a = b ==> ( &1 / t3) % a = (&1 / t3) % b `); REWRITE_TAC[Local_lemmas.VECTOR_ADD_LDISTRIB1]; ASSUME_TAC2 (REAL_FIELD` t3 < &0 ==> &1 / t3 * t3 = &1 `); ASM_REWRITE_TAC[VECTOR_MUL_LID]; SIMP_TAC[]; STRIP_TAC; EXISTS_TAC` (&1 / t3 * (ta - t1)) `; EXISTS_TAC` (&1 / t3 * (tb - t2)) `; ASM_REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_ARITH` a - x + b - y = (a + b ) - ( x + y )`]; UNDISCH_TAC`t1 + t2 + t3 = &1 `; ASM_SIMP_TAC[REAL_ARITH` a + b + c = &1 <=> &1 - ( a + b ) = c `]; ASM_REWRITE_TAC[]]);;
let AZIM_PI_LEMMA = 
prove_by_refinement (` ~(aff_gt {u} s INTER aff_lt {u} {a} = {} ) /\ aff_gt {u} s SUBSET aff_gt {u, v} {y} /\ a IN aff_gt {u, v} {x} /\ ~ collinear {u, v, x} /\ ~ collinear {u, v, y} ==> azim u v x y = pi `,
[MP_TAC ( ISPECL [`{u: real^3} `;` {u, v:real^3} `; `{a: real^3 }`] AFF_LT_MONO_LEFT); ANTS_TAC; CONV_TAC SET_RULE; REPEAT STRIP_TAC; SUBGOAL_THEN` aff_gt {u,v} {x} = aff_gt {u,v} {a:real^3} ` MP_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; DISCH_THEN (ASSUME_TAC o SYM); ASSUME_TAC2 ( SET_RULE` ~(aff_gt {u: real^3} s INTER aff_lt {u} {a} = {}) /\ aff_lt {u} {a} SUBSET aff_lt {u, v} {a} /\ aff_gt {u} s SUBSET aff_gt {u, v} {y} ==> ~ ( aff_gt {u, v} {y} INTER aff_lt {u, v} {a} = {} ) `); DOWN; REWRITE_TAC[SET_RULE` ~( A INTER B = {} ) <=> ? x. x IN A /\ x IN B `]; STRIP_TAC; UNDISCH_TAC` x' IN aff_gt {u, v} {y:real^3} `; UNDISCH_TAC` ~ collinear {u, v, y:real^3} `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_TOO; STRIP_TAC; SUBGOAL_THEN` ~ collinear {u, v, a: real^3} ` ASSUME_TAC; MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO); EXISTS_TAC` x: real ^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` ~collinear {u, v, x' : real^3} `; UNDISCH_TAC` ~collinear {u, v, a: real^3} `; PHA; NHANH AZIM_EQ_PI_ALT; STRIP_TAC; SUBGOAL_THEN` azim u v a x' = azim u v a y ` MP_TAC; MATCH_MP_TAC AZIM_EQ_IMP; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (ASSUME_TAC o SYM); STRIP_TAC; UNDISCH_TAC` x' IN aff_lt {u, v} {a:real^3} `; ASM_REWRITE_TAC[]; SUBGOAL_THEN` azim u v a y = azim u v x y ` MP_TAC; ONCE_REWRITE_TAC[ Rogers.AZIM_EQ_SYM]; MATCH_MP_TAC (* Polar_fan. *) AZIM_EQ_IMP; ASM_REWRITE_TAC[]; SIMP_TAC[]]);;
(* ================================================== *)
let SUB_LUNAR_DEFORM_LEMMA = 
prove_by_refinement(` FINITE V /\ convex_local_fan (V,E,FF) /\ lunar (v,w) V E /\ (! x. x IN E ==> x SUBSET V) /\ f (u:real^3) (&0 ) = u /\ f u continuous atreal (&0) /\ interior_angle1 (vec 0) FF v < pi /\ a < &0 /\ &0 < b /\ u IN V /\ ~(u = v) /\ ~(u = w) /\ (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\ (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u}) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> lunar (v,w) (IMAGE (\v. f v t) V) (IMAGE (IMAGE (\v. f v t)) E)))`,
[ STRIP_TAC; ASSUME_TAC2 Local_lemmas.HKIRPEP; DOWN_TAC; REWRITE_TAC[lunar; circular]; STRIP_TAC; SUBGOAL_THEN` ! t. t IN real_interval (a,b) ==> {v, w} SUBSET IMAGE (\v. (f:real^3->real->real^3) v t) V ` ASSUME_TAC; REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_IMAGE]; REPEAT STRIP_TAC; EXISTS_TAC` v:real^3` ; SUBGOAL_THEN` (v:real^3) IN V ` MP_TAC; MATCH_MP_TAC (SET_RULE` {v, w:real^3} SUBSET V ==> v IN V`); FIRST_X_ASSUM ACCEPT_TAC; SIMP_TAC[]; FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` &0 `)); FIRST_X_ASSUM (ASSUME_TAC o (ISPECL[ ` v:real^3`; ` t:real `])); STRIP_TAC; ONCE_REWRITE_TAC[EQ_SYM_EQ]; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; EXISTS_TAC` w:real^3 `; SUBGOAL_THEN` (w:real^3) IN V ` ASSUME_TAC; MATCH_MP_TAC (SET_RULE` {v, w} SUBSET V ==> w IN V ` ); FIRST_X_ASSUM ACCEPT_TAC; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o GSYM); ASM_REWRITE_TAC[]; FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` &0 `)) THEN FIRST_X_ASSUM (ASSUME_TAC o (SPECL[ ` w:real^3 `; ` t:real `])); ONCE_REWRITE_TAC[EQ_SYM_EQ]; FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; ABBREV_TAC` CONCL = ?e. &0 < e /\ (!t. --e < t /\ t < e ==> ~(?v w u. {v, w} IN IMAGE (IMAGE (\v. (f:real^3 -> real -> real^3) v t)) E /\ u IN IMAGE (\v. f v t) V /\ ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\ {v, w} SUBSET IMAGE (\v. f v t) V /\ ~(v = w) /\ collinear {vec 0, v, w}) `; MP_TAC (ISPEC`V: real^3 -> bool ` (GEN`V: real^N -> bool ` DISJTINCT_PROPERTY)); ANTS_TAC; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` t IN real_interval (a,b) /\ --e < t /\ t < e ==> (!v w u'. {v, w} IN IMAGE (IMAGE (\v. (f:real^3 -> real -> real^3) v t)) E /\ u' IN IMAGE (\v. f v t) V /\ ~( f u t IN {u' ,v, w} ) ==> (aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u'} = {})) ` ASSUME_TAC; REWRITE_TAC[IN_IMAGE]; REPEAT STRIP_TAC; SUBGOAL_THEN` x SUBSET (V:real^3 -> bool ) ` ASSUME_TAC; FIRST_ASSUM MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; ASM_CASES_TAC` (u:real^3) IN x `; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN {v', w'} ` ASSUME_TAC; UNDISCH_TAC` {v': real^3, w'} = IMAGE (\v. (f:real^3 -> real -> real^3) v t) x `; SIMP_TAC[IN_IMAGE]; STRIP_TAC; EXISTS_TAC` u:real^3 `; ASM_REWRITE_TAC[]; DOWN; REPLICATE_TAC 3 DOWN; SIMP_TAC[IN_INSERT]; MESON_TAC[]; SUBGOAL_THEN` t IN real_interval (a, b) ==> IMAGE (\v. (f:real^3 -> real -> real^3) v t ) x = x ` MP_TAC; STRIP_TAC; MATCH_MP_TAC Counting_spheres.pad2d3d_dropout_lemma; EXISTS_TAC` \x. (x:real^3) IN V /\ ~( x = u ) ` ; CONJ_TAC; GEN_TAC; REWRITE_TAC[BETA_THM]; DOWN THEN DOWN THEN DOWN; REWRITE_TAC[SUBSET]; MESON_TAC[]; GEN_TAC; REWRITE_TAC[BETA_THM]; STRIP_TAC; UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> (f: real^3 -> real -> real^3) u' t = u' `; DISCH_THEN MATCH_MP_TAC; ASM_REWRITE_TAC[]; DISCH_THEN ASSUME_TAC2; FIRST_X_ASSUM SUBST_ALL_TAC; ASM_CASES_TAC` x' = (u:real^3) `; FIRST_X_ASSUM SUBST_ALL_TAC; UNDISCH_TAC` ~((f:real^3 -> real -> real^3 ) u t IN {u', v', w'}) ` ; ASM_REWRITE_TAC[IN_INSERT]; SUBGOAL_THEN` (f: real^3 -> real -> real^3) x' t = x' ` MP_TAC; UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> (f: real^3 -> real -> real^3 ) u' t = u' ` ; DISCH_THEN MATCH_MP_TAC; ASM_REWRITE_TAC[]; DISCH_THEN SUBST_ALL_TAC; UNDISCH_TAC` ~(?v w u. {v, w} IN E /\ u IN V /\ ~(aff_gt {vec 0} {v, w: real^3} INTER aff_lt {vec 0} {u} = {})) `; UNDISCH_TAC` x': real^3 IN V `; UNDISCH_TAC` (x: real^3 -> bool) IN E `; EXPAND_TAC "x'";
EXPAND_TAC "x"; MESON_TAC[]; ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO; MP_TAC (SPECL [` i:num `;` j:num `] (GENL[` n:num `;` n': num `] Local_lemmas1.CARD_V_TWO_HAFL_CIRCLE)); ANTS_TAC; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[SET_RULE` x IN A /\ y IN A <=> {x,y} SUBSET A `]; STRIP_TAC; ASSUME_TAC2 (SET_RULE` {v, w:real^3} SUBSET V ==> v IN V `); ASSUME_TAC2 Localization.LOFA_IMP_LT_CARD_SET_V_ALT; UNDISCH_TAC` (u:real^3) IN V `; EXPAND_TAC "V"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; UNDISCH_TAC` v = ITER j (rho_node1 FF) w ` ; DOWN; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); MP_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ; ANTS_TAC; ASM_REWRITE_TAC[lunar; circular]; DISCH_THEN (ASSUME_TAC o SYM); FIRST_X_ASSUM SUBST_ALL_TAC; SUBGOAL_THEN` u IN aff_gt {vec 0, v} {rho_node1 FF v} \/ u IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC; ASM_CASES_TAC` (n:num) < i ` ; DISJ1_TAC; ASM_CASES_TAC` n = 0 `; FIRST_X_ASSUM SUBST_ALL_TAC; REPLICATE_TAC 4 DOWN THEN PHA; ASM_REWRITE_TAC[ITER]; SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n: num `; ASM_REWRITE_TAC[]; DOWN THEN DOWN; ARITH_TAC; DOWN; ASM_SIMP_TAC[IN_INTER]; ASM_CASES_TAC` (n:num) = i ` ; FIRST_X_ASSUM SUBST_ALL_TAC; REPLICATE_TAC 2 DOWN THEN PHA; ASM_REWRITE_TAC[]; DISJ2_TAC; ASSUME_TAC2 (ARITH_RULE` ~( n:num < i) ==> i + ( n - i ) = n`); SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j}` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` (n: num) - i `; EXPAND_TAC "w"; ASM_REWRITE_TAC[ITER_ADD; ADD_SYM]; REPLICATE_TAC 3 DOWN THEN PHA; SIMP_TAC[ (ARITH_RULE` ~((n:num) < i) ==> ( n - i < j <=> n < i + j ) `)]; ASM_REWRITE_TAC[]; ARITH_TAC; ASM_SIMP_TAC[IN_INTER]; ASSUME_TAC2 (SET_RULE` {v, w:real^3} SUBSET V ==> w IN V `); MP_TAC (SPEC` w:real^3 ` Local_lemmas.LOFA_IMP_LT_CARD_SET_V); ANTS_TAC; ASM_SIMP_TAC[SET_RULE` {a,b} SUBSET V ==> b IN V `]; STRIP_TAC; SUBGOAL_THEN` u IN {ITER n (rho_node1 FF) v | n < CARD (V:real^3 -> bool)} ` ASSUME_TAC; EXPAND_TAC "u"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n:num `; ASM_REWRITE_TAC[]; DOWN; ASM_REWRITE_TAC[]; EXPAND_TAC "V"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; DOWN; DISCH_THEN (ASSUME_TAC o SYM); DOWN_TAC; REWRITE_TAC[TAUT` a /\ b /\ c <=> (a /\ b) /\ c `]; SPEC_TAC (`n':num `,` n': num ` ); SPEC_TAC (`n:num `,` n: num ` ); SPEC_TAC (`v:real^3 `, ` v:real^3 `); SPEC_TAC (`i: num `,` i:num ` ); SPEC_TAC (`w:real^3 `, ` w:real^3 `); SPEC_TAC (`j: num `,` j:num ` ); MATCH_MP_TAC ( MESON[]` (! j w i v n n'. P j w i v n n' ==> P i v j w n' n) /\ (! j w i v n n'. P j w i v n n' /\ u IN Q v ==> concl ) ==> (! j w i v n n'. P j w i v n n'/\ (u IN Q v \/ u IN Q w ) ==> concl )`); CONJ_TAC; SIMP_TAC[]; SIMP_TAC[INSERT_COMM; ADD_SYM]; REPEAT GEN_TAC; STRIP_TAC; CONJ_TAC; UNDISCH_TAC` interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w ` ; DISCH_THEN (SUBST1_TAC o SYM); ASM_REWRITE_TAC[]; UNDISCH_TAC`(?e. &0 < e /\ (!t. --e < t /\ t < e ==> ((~(?v w u. ({v, w} IN IMAGE (IMAGE (\v. f v t)) E /\ u IN IMAGE (\v. f v t) V) /\ ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\ {v, w} SUBSET IMAGE (\v. (f:real^3 -> real -> real^3) v t) V) /\ ~(v = w)) /\ collinear {v, w, vec 0})) <=> CONCL`; ASM_REWRITE_TAC[]; PHA; REPEAT STRIP_TAC; (* ==================================== prove_by_refinement (`FINITE V /\ convex_local_fan (V,E,FF) /\ ~(?v w u. {v, w} IN E /\ u IN V /\ ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\ {v, w} SUBSET V /\ ~(v = w) /\ collinear {vec 0, v, w} /\ (!x. x IN E ==> x SUBSET V) /\ f u (&0) = u /\ f u continuous atreal (&0) /\ interior_angle1 (vec 0) FF v < pi /\ a < &0 /\ &0 < b /\ ~(u = v) /\ ~(u = w) /\ (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\ (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u}) /\ (!u. u IN V DIFF {v, w} ==> interior_angle1 (vec 0) FF u = pi) /\ &0 < interior_angle1 (vec 0) FF v /\ interior_angle1 (vec 0) FF v <= pi /\ interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w /\ i < CARD V /\ ~(i = 0) /\ ~(i = 1) /\ {ITER l (rho_node1 FF) v | 0 < l /\ l < i} = aff_gt {vec 0, v} {rho_node1 FF v} INTER V /\ j < CARD V /\ ~(j = 0) /\ ~(j = 1) /\ {ITER l (rho_node1 FF) w | 0 < l /\ l < j} = aff_gt {vec 0, w} {rho_node1 FF w} INTER V /\ (!t. t IN real_interval (a,b) ==> {v, w} SUBSET IMAGE (\v. f v t) V) /\ ((?e. &0 < e /\ (!t. --e < t /\ t < e ==> ~(?v w u. {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\ u IN IMAGE (\v. f v t) V /\ ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\ {v, w} SUBSET IMAGE (\v. f v t) V /\ ~(v = w) /\ collinear {vec 0, v, w})) <=> CONCL) /\ &0 < e /\ (!t u'. --e < t /\ t < e /\ u' IN V /\ ~(u' = u) ==> ~(f u t = f u' t)) /\ (t IN real_interval (a,b) /\ --e < t /\ t < e ==> (!v w u'. {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\ u' IN IMAGE (\v. f v t) V /\ ~(f u t IN {u', v, w}) ==> aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u'} = {})) /\ local_fan (V,E,FF) /\ i + j = CARD V /\ v IN V /\ {ITER n (rho_node1 FF) v | n < CARD V} = V /\ n < CARD V /\ ITER n (rho_node1 FF) v = u /\ ITER j (rho_node1 FF) w = v /\ ITER i (rho_node1 FF) v = w /\ w IN V /\ {ITER n (rho_node1 FF) w | n < CARD V} = V /\ n' < CARD V /\ ITER n' (rho_node1 FF) w = u /\ u IN aff_gt {vec 0, v} {rho_node1 FF v} ==> CONCL`, [STRIP_TAC ; ================================= *) SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} ` MP_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2 ; ASM_REWRITE_TAC[]; STRIP_TAC; ABBREV_TAC` u1 = ( (u dot v ) / ( v dot v )) % (v:real^3)`; ABBREV_TAC` uh = u - (u1:real^3) `; SUBGOAL_THEN` uh dot (v:real^3) = &0 ` ASSUME_TAC; EXPAND_TAC "uh"; EXPAND_TAC "u1"; REWRITE_TAC[DOT_LSUB; DOT_LMUL]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 ` )); DOWN; REWRITE_TAC[GSYM DOT_EQ_0]; CONV_TAC REAL_FIELD; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u continuous atreal (&0) ` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[continuous_atreal]; DISCH_THEN (MP_TAC o (SPEC` norm (uh: real ^3)`)); ANTS_TAC; REWRITE_TAC[NORM_POS_LT]; STRIP_TAC; FIRST_X_ASSUM SUBST_ALL_TAC; UNDISCH_TAC` (u:real^3) - u1 = vec 0 ` ; REWRITE_TAC[VECTOR_SUB_EQ]; EXPAND_TAC "u1"; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `)); ASSUME_TAC2 (ISPEC` v:real^3 ` (GEN_ALL Local_lemmas.COLLINEAR_ONCE_VEC_0)); FIRST_X_ASSUM (MP_TAC o (SPEC` u: real^3 `)); STRIP_TAC; STRIP_TAC; SUBGOAL_THEN` collinear {vec 0, v, u:real^3 } ` MP_TAC; ASM_REWRITE_TAC[]; DOWN THEN MESON_TAC[]; REWRITE_TAC[]; MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO); EXISTS_TAC` rho_node1 FF v `; ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; ASM_REWRITE_TAC[]; STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; SUBGOAL_THEN` ~ collinear {vec 0, v, u:real^3} ` MP_TAC; MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO); EXISTS_TAC` rho_node1 FF v `; ASM_REWRITE_TAC[]; NHANH Fan.th3a; NHANH AFF_GT_2_1; STRIP_TAC; SUBGOAL_THEN` (uh: real^3) IN aff_gt {vec 0, v} {u} ` MP_TAC; ASM_REWRITE_TAC[IN_ELIM_THM]; EXPAND_TAC "uh"; EXPAND_TAC "u1"; EXISTS_TAC` (u dot v) / (v dot (v:real^3))`; EXISTS_TAC` -- ((u dot v) / (v dot (v:real^3)))`; EXISTS_TAC` &1 `; CONJ_TAC; REAL_ARITH_TAC; CONJ_TAC; REAL_ARITH_TAC; CONV_TAC VECTOR_ARITH; UNDISCH_TAC` ~collinear {vec 0, v, (u:real^3)}`; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; STRIP_TAC; MP_TAC (ISPEC` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL); ASSUME_TAC (ISPECL [` vec 0: real^3`;`u:real^3`] (GENL [` u:real^N `;` w:real^N `] AFF_GT_SUBSET_AFFINE_HULL21)); SUBGOAL_THEN` {vec 0, v , uh:real^3} SUBSET affine hull {vec 0, v, u}` MP_TAC; MP_TAC (ISPEC` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL); SIMP_TAC[INSERT_SUBSET]; STRIP_TAC; UNDISCH_TAC` aff_gt {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) ` ; REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET]; DISCH_THEN MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; REPEAT STRIP_TAC; UNDISCH_TAC` uh IN aff_gt {vec 0, v} {u:real^3} `; UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_TOO; STRIP_TAC; DOWN; UNDISCH_TAC` {vec 0, v, uh} SUBSET affine hull {vec 0, v, u:real^3} `; PHA; NHANH Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ; STRIP_TAC; SUBGOAL_THEN` affine hull {vec 0, v, w, u:real^3} = affine hull {vec 0, v, u } ` ASSUME_TAC; MP_TAC (SPECL [` w:real^3 `;` {vec 0, v, u:real^3} `] Marchal_cells_3.AFFINE_HULL_3_INSERT); ANTS_TAC; MP_TAC (ISPECL [` vec 0: real^3 `;` v:real^3 `; ` w:real^3 `] COLLINEAR_3_AFFINE_HULL); ANTS_TAC; ONCE_REWRITE_TAC[EQ_SYM_EQ]; ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_ASSUM MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; STRIP_TAC; SUBGOAL_THEN` collinear {vec 0, v, w:real^3} ` MP_TAC; ASM_REWRITE_TAC[]; FIRST_ASSUM SUBST1_TAC; SPEC_TAC (`w:real^3 `,` w:real^3 `); REWRITE_TAC[GSYM SUBSET]; MATCH_MP_TAC Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA ; REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET]; REWRITE_TAC[INSERT_COMM]; SUBGOAL_THEN` ! t. -- d < t /\ t < d /\ t IN real_interval (a,b) ==> f u t IN aff_gt {vec 0, v} {u:real^3} ` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; UNDISCH_TAC` !t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u:real^3} ` ; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` t':real `)); DOWN; ASM_REWRITE_TAC[]; REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM]; STRIP_TAC; ASM_CASES_TAC` w' = &0 `; FIRST_X_ASSUM SUBST_ALL_TAC; UNDISCH_TAC` !x'. abs (x' - &0) < d ==> dist ((f: real^3 -> real -> real^3) u x',f u (&0)) < norm (uh: real^3) ` ; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPEC` t': real `)); REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT]; DISCH_THEN ASSUME_TAC2; DOWN; SUBST_ALL_TAC (VECTOR_ARITH` u - u1 = (uh: real^3) <=> u = uh + u1 `); ASM_REWRITE_TAC[VECTOR_ARITH` u' % vec 0 + v' % v + &0 % uh = v' % v `]; EXPAND_TAC "u1"; REWRITE_TAC[dist; Pack1.norm_ineq_lt; VECTOR_ARITH` a % v - ( u + b % v ) = ( a - b ) % v - u `]; REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_LMUL; DOT_RMUL]; ABBREV_TAC` con1 = v' - (u dot v) / ((v:real^3) dot v) `; ASM_REWRITE_TAC[DOT_SYM; Collect_geom.ZERO_NEUTRAL; REAL_ARITH` a - ( &0 - x ) = a + x `]; MP_TAC (ISPEC` v:real^3 ` DOT_POS_LE); REWRITE_TAC[REAL_ARITH` a + x < x <=> a < &0 `]; MP_TAC (SPEC` con1: real` REAL_LE_SQUARE ); STRIP_TAC; STRIP_TAC; ASSUME_TAC2 (SPECL [` con1 * (con1:real)`;` v dot (v:real^3) `] REAL_LE_MUL); DOWN; REAL_ARITH_TAC; ASM_CASES_TAC` w' < &0 `; UNDISCH_TAC` !x'. abs (x' - &0) < d ==> dist ((f:real^3 -> real -> real^3) u x',f u (&0)) < norm (uh: real^3) `; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPEC` t': real `)); REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT]; DISCH_THEN ASSUME_TAC2; DOWN; SUBST_ALL_TAC (VECTOR_ARITH` u - u1 = uh <=> u = uh + (u1: real^3) `); ASM_REWRITE_TAC[dist]; REWRITE_TAC[Pack1.norm_ineq_lt] ; EXPAND_TAC "u1" ; REWRITE_TAC[VECTOR_ARITH` (u' % vec 0 + v' % v + w' % uh) - (uh + uv % v) = (v' - uv ) % v + (w' - &1) % uh `] ; ABBREV_TAC` con1 = (u dot v) / (v dot (v:real^3)) ` ; ASM_REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; DOT_SYM; Collect_geom.ZERO_NEUTRAL] ; ASSUME_TAC (ISPEC` v:real^ 3 ` DOT_POS_LE) ; ASSUME_TAC (SPEC` v' - con1:real ` REAL_LE_SQUARE) ; ASSUME_TAC (ISPEC` uh:real^ 3 ` DOT_POS_LE) ; STRIP_TAC ; MP_TAC (ISPECL [` &1 `;` -- w' + &1 `] Collect_geom.POW2_COND) ; ANTS_TAC ; UNDISCH_TAC` w' < &0 ` ; REAL_ARITH_TAC ; STRIP_TAC ; SUBGOAL_THEN` &1 <= -- w' + &1 ` MP_TAC ; UNDISCH_TAC` w' < &0 ` ; REAL_ARITH_TAC ; ASM_REWRITE_TAC[] ; REWRITE_TAC[REAL_ARITH` &1 pow 2 <= (--w' + &1) pow 2 <=> &0 <= (w' - &1 ) * (w' - &1 ) - &1 `] ; STRIP_TAC ; ASSUME_TAC2 (ISPECL[`(w' - &1) * (w' - &1) - &1 `;` (uh:real^3 ) dot uh `] REAL_LE_MUL) ; ASSUME_TAC2 (ISPECL[`(v' - con1) * (v' - con1)`;` (v:real^3 ) dot v `] REAL_LE_MUL) ; UNDISCH_TAC` (v' - con1) * (v' - con1) * ((v:real^3) dot v) + (w' - &1) * (w' - &1) * (uh dot uh) < uh dot (uh: real^3) ` ; DOWN THEN DOWN ; REAL_ARITH_TAC ; SUBGOAL_THEN` f u (t': real) IN aff_gt {vec 0, v} {u:real^3} ` MP_TAC ; UNDISCH_TAC` aff_gt {vec 0, v} {u} = aff_gt {vec 0, v} {uh:real^3} ` ; DISCH_THEN SUBST1_TAC ; UNDISCH_TAC` ~collinear {vec 0, v, uh:real^3} ` ; NHANH Fan.th3a ; NHANH AFF_GT_2_1 ; SIMP_TAC[IN_ELIM_THM] ; STRIP_TAC ; EXISTS_TAC` u': real ` ; EXISTS_TAC` v':real ` ; EXISTS_TAC` w': real ` ; ASM_REWRITE_TAC[]; UNDISCH_TAC` ~( w' = &0 ) `; UNDISCH_TAC` ~( w' < &0 ) `; REAL_ARITH_TAC; ASM_REWRITE_TAC[IN_ELIM_THM]; SUBGOAL_THEN` ! t u. abs t < d /\ t IN real_interval (a,b) /\ (u:real^3) IN V ==> f u t IN aff_gt {vec 0, v} {u} ` MP_TAC; REPEAT STRIP_TAC; ASM_CASES_TAC` ~(u = u':real^3 )`; UNDISCH_TAC` !u' t. u' IN V /\ ~(u: real^3 = u') /\ t IN real_interval (a,b) ==> f u' t = u' `; DISCH_THEN (MP_TAC o (SPECL [` u':real^3 `;` t': real`])); ANTS_TAC; ASM_REWRITE_TAC[]; SIMP_TAC[]; MP_TAC (ISPECL [` {vec 0, v:real^3} `;` {u':real^3} `] (GEN_ALL Local_lemmas.CONV0_SUBSET_AFF_GT)); SIMP_TAC[Geomdetail.CONV0_SING; INSERT_SUBSET]; DOWN; REWRITE_TAC[]; DISCH_THEN SUBST_ALL_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[REAL_BOUNDS_LT]; STRIP_TAC; SUBGOAL_THEN` ! t. abs t < d /\ t IN real_interval (a,b) ==> (! s. s IN IMAGE (IMAGE (\v. f (v:real^3) t)) E ==> aff_gt {vec 0} s SUBSET aff_gt { vec 0, v} {rho_node1 FF v } \/ aff_gt {vec 0} s SUBSET aff_gt { vec 0, w} {rho_node1 FF w })` MP_TAC; REWRITE_TAC[GSYM REAL_BOUNDS_LT]; PHA; DOWN; FIRST_ASSUM NHANH; STRIP_TAC; GEN_TAC THEN STRIP_TAC; GEN_TAC; REWRITE_TAC[IN_IMAGE]; STRIP_TAC; DOWN; UNDISCH_TAC` local_fan (V,E, FF) `; PHA; NHANH EDGE_IN_LOCAL_FAN_DET_RHO_NODE; STRIP_TAC; UNDISCH_TAC` (v': real^3) IN V `; EXPAND_TAC "V"; REWRITE_TAC[IN_ELIM_THM]; ONCE_REWRITE_TAC[EQ_SYM_EQ]; STRIP_TAC; ASM_CASES_TAC` n'' < (j:num ) `; ASM_CASES_TAC` n'' = 0 `; FIRST_X_ASSUM SUBST_ALL_TAC; DOWN THEN DOWN; REWRITE_TAC[ITER]; DISCH_THEN (SUBST_ALL_TAC o SYM); STRIP_TAC; DISJ2_TAC; UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = (u': real^3) `; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [` w:real^3 `;` t': real `])); ANTS_TAC; ASM_REWRITE_TAC[]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` rho_node1 FF w `])); ANTS_TAC; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[]; MP_TAC Local_lemmas.AFF_GT_SAME_WITH_ENDS; ANTS_TAC; ASM_REWRITE_TAC[lunar; circular]; SIMP_TAC[]; STRIP_TAC THEN STRIP_TAC; ASSUME_TAC2 (SPEC`w: real^3 ` (GEN`v: real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)); SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w} = aff_gt {vec 0, w} { f (rho_node1 FF w) (t':real)} ` MP_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; DISCH_THEN (ASSUME_TAC o SYM); MP_TAC (ISPECL [` {w:real^3} `;` {vec 0, w:real^3} `;` {(f (rho_node1 FF w) (t': real)): real^3 } `] (GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS)); ANTS_TAC; REWRITE_TAC[IN_INSERT; INSERT_SUBSET; EMPTY_SUBSET]; REWRITE_TAC[SET_RULE` A UNION {a} = a INSERT A `]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `)); ASSUME_TAC2 (SET_RULE` ~((w:real^3) = vec 0) ==> {vec 0, w} DIFF {w} = {vec 0} `); UNDISCH_TAC` s = IMAGE (\v. (f:real^3 -> real -> real^3) v t') x `; DISCH_THEN (ASSUME_TAC o SYM); ASM_SIMP_TAC[]; SUBGOAL_THEN` {w, f (rho_node1 FF w) (t':real)} = s ` MP_TAC; EXPAND_TAC "s"; EXPAND_TAC "x"; REWRITE_TAC[EXTENSION; IN_IMAGE]; GEN_TAC; EQ_TAC; REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]; STRIP_TAC; EXISTS_TAC `w:real^3 `; ASM_REWRITE_TAC[]; EXISTS_TAC` rho_node1 FF w `; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]; STRIP_TAC; DISJ1_TAC; ASM_REWRITE_TAC[]; DISJ2_TAC; ASM_REWRITE_TAC[]; SIMP_TAC[]; ASM_CASES_TAC` n'' = j - 1 `; ASSUME_TAC2 (ARITH_RULE` ~( j = 0 ) ==> j - 1 + 1 = j`); SUBGOAL_THEN` rho_node1 FF v' = v ` MP_TAC; EXPAND_TAC "v'"; UNDISCH_TAC` n'' = j - 1 `; SIMP_TAC[GSYM ITER; ADD1]; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n'':num `; ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `]; ASM_REWRITE_TAC[]; STRIP_TAC; DISJ2_TAC; DOWN; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_INTER]; STRIP_TAC; SUBGOAL_THEN` IMAGE (\v. f v t') x = { f (v':real^3) (t':real), v:real^3} ` MP_TAC; REWRITE_TAC[EXTENSION]; GEN_TAC; EQ_TAC; EXPAND_TAC "x"; REWRITE_TAC[IN_IMAGE; IN_INSERT; NOT_IN_EMPTY]; STRIP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; DISJ2_TAC; UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = (u': real^3) `; DISCH_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "x"; REWRITE_TAC[IN_IMAGE; IN_INSERT; NOT_IN_EMPTY]; STRIP_TAC; EXISTS_TAC `v': real^3 `; ASM_REWRITE_TAC[]; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[EQ_SYM_EQ]; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; SIMP_TAC[]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [` t': real`;` v': real^3 `])); ANTS_TAC; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; STRIP_TAC; MP_TAC (ISPECL [` {v:real^3 } `; `{ vec 0, v:real^3 } `; ` { (f: real^3 -> real -> real^3) v' t' } `] (GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS)); ANTS_TAC; REWRITE_TAC[IN_INSERT; INSERT_SUBSET; EMPTY_SUBSET]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `)); ASSUME_TAC2 ( SET_RULE` ~((v:real^3) = vec 0 ) ==> {vec 0, v} DIFF {v} = {vec 0 } `); ASM_REWRITE_TAC[SET_RULE` {a} UNION {b} = {a,b} `]; MP_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI; ANTS_TAC; ASM_REWRITE_TAC[lunar; circular]; STRIP_TAC; ASSUME_TAC2 ( SPEC` w:real^3 ` (GEN` v:real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)); MP_TAC (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS); ANTS_TAC; ASM_REWRITE_TAC[lunar; circular]; STRIP_TAC; SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC; ASM_REWRITE_TAC[lunar; circular]; ASSUME_TAC2 Local_lemmas.NOT_COLL_RHONODE_SND_POINT; UNDISCH_TAC` v' IN aff_gt {vec 0, w} {rho_node1 FF w} `; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` ~ collinear {vec 0, v, v':real^3 } ` MP_TAC; MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO); EXISTS_TAC` rho_node1 FF w `; ASM_REWRITE_TAC[]; STRIP_TAC; STRIP_TAC; UNDISCH_TAC` v' IN aff_gt {vec 0, v} {rho_node1 FF w} `; UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; STRIP_TAC; SUBGOAL_THEN` aff_gt {vec 0, v} {f v' (t':real)} = aff_gt {vec 0, v} {v': real^3}` ASSUME_TAC; MATCH_MP_TAC (GSYM Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ); ASM_REWRITE_TAC[]; UNDISCH_TAC` aff_gt {vec 0} {f v' t', v} SUBSET aff_gt {vec 0, v} {(f: real^3 -> real -> real^3) v' t'} `; ASM_REWRITE_TAC[]; SUBGOAL_THEN` lunar (v, (w:real^3)) V E` ASSUME_TAC; ASM_REWRITE_TAC[lunar; circular]; SUBGOAL_THEN` v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} /\ rho_node1 FF v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC; EXPAND_TAC "v'"; REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; EXISTS_TAC`n'': num `; ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `]; EXISTS_TAC` n'' + 1 `; REWRITE_TAC[GSYM ITER; ADD1; ARITH_RULE` 0 < a + 1 `]; MATCH_MP_TAC (ARITH_RULE` n'' < j /\ ~(n'' = j - 1) ==> n'' + 1 < j `); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; UNDISCH_TAC` aff_gt {vec 0, v} {u: real^3} = {y | ?t1 t2 t3. &0 < t3 /\ t1 + t2 + t3 = &1 /\ y = t1 % vec 0 + t2 % v + t3 % u} `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[IN_INTER]; STRIP_TAC; DISJ2_TAC; EXPAND_TAC "x"; REWRITE_TAC[IMAGE_CLAUSES]; ASSUME_TAC2 ( SPEC` w:real^3 ` (GEN` v: real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)); SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w } = aff_gt { vec 0, w} {v'} ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w } = aff_gt { vec 0, w} {rho_node1 FF v'} ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; DOWN; DOWN; ASSUME_TAC2 (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS); ASSUME_TAC2 Local_lemmas.NOT_COLL_RHONODE_SND_POINT; UNDISCH_TAC` v' IN aff_gt {vec 0, w} {rho_node1 FF w} `; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF w} = aff_gt {vec 0, v} {v'} ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; SUBGOAL_THEN` f (v':real^3) (t': real) IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; SUBGOAL_THEN` f (rho_node1 FF v') (t': real) IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC; ASM_REWRITE_TAC[]; UNDISCH_TAC` rho_node1 FF v' IN aff_gt {vec 0, w} {rho_node1 FF w} `; DOWN; ASM_REWRITE_TAC[]; STRIP_TAC; UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_SIMP_TAC[]; STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; REPEAT STRIP_TAC; ASSUME_TAC2 ( let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO in ISPECL [` rho_node1 FF w` ;` vec 0: real^3 `;` w:real^3 `; ` (f:real^3 -> real -> real^3) v' t' `] tt); ASSUME_TAC2 ( let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO in ISPECL [` rho_node1 FF w` ;` vec 0: real^3 `;` w:real^3 `; ` (f:real^3 -> real -> real^3) (rho_node1 FF v') t' `] tt); DOWN THEN DOWN; NHANH Fan.th3b1; PHA; NHANH (SET_RULE` ~( a = x ) /\ t /\ ~( a = y ) ==> DISJOINT {a} {x,y} `); STRIP_TAC; UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `; NHANH Fan.th3a; STRIP_TAC; MATCH_MP_TAC TOW_POINTS_IN_IMP_AFF_GT_SUBSET; ASM_REWRITE_TAC[]; UNDISCH_TAC` (f: real^3 -> real -> real^3) v' t' IN aff_gt {vec 0, w} {rho_node1 FF w} `; UNDISCH_TAC` (f: real^3 -> real -> real^3) (rho_node1 FF v') t' IN aff_gt {vec 0, w} {rho_node1 FF w} `; ASM_REWRITE_TAC[]; SIMP_TAC[]; ASM_CASES_TAC` n'' = (j:num) ` ; FIRST_X_ASSUM SUBST_ALL_TAC; DOWN THEN DOWN; ASM_REWRITE_TAC[]; EXPAND_TAC "x"; REWRITE_TAC[IMAGE_CLAUSES]; DISCH_THEN (SUBST_ALL_TAC o SYM); STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) v t' = v ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; MP_TAC ( let tt = GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS in ISPECL [` {v:real^3 } `; `{vec 0, v:real^3} ` ;` { (f: real^3 -> real -> real^3) (rho_node1 FF v) t' }` ] tt); ANTS_TAC; REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v: real^3 `)); ASSUME_TAC2 (SET_RULE` ~( v = vec 0) ==> {vec 0, v} DIFF {v} = {vec 0: real^3 }`); ASM_REWRITE_TAC[SET_RULE` {a} UNION {b} = {b,a} `]; FIRST_ASSUM (MP_TAC o (ISPECL [` t': real `;` rho_node1 FF v `])); ANTS_TAC; ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; STRIP_TAC; ASSUME_TAC2 ( let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` (f:real^3 -> real -> real^3) (rho_node1 FF v) t' `] tt); FIRST_X_ASSUM (SUBST1_TAC o SYM); ASM_REWRITE_TAC[]; SIMP_TAC[]; ASM_CASES_TAC` n'' = CARD (V: real^3 -> bool) - 1 `; SUBGOAL_THEN` rho_node1 FF v' = w ` ASSUME_TAC; EXPAND_TAC "v'"; DOWN THEN SIMP_TAC[]; STRIP_TAC; REWRITE_TAC[GSYM ITER; ADD1]; ASSUME_TAC2 (ARITH_RULE` n'' < CARD (V:real^3 -> bool) ==> CARD V - 1 + 1 = CARD V `); ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `)); ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `)); UNDISCH_TAC` ITER n'' (rho_node1 FF) w = v' `; ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (GSYM ( SPECL [` w:real^3 `;` v:real^3 `] (GENL [` v: real^3 `;` w:real^3 `] Local_lemmas.AFF_IVS_RHO_NODE_EQQ))); ANTS_TAC; ASM_REWRITE_TAC[Local_lemmas.LUNAR_COMM; lunar; circular; INSERT_SUBSET; EMPTY_SUBSET]; UNDISCH_TAC` collinear {vec 0, v, w:real^3} `; SIMP_TAC[INSERT_COMM]; STRIP_TAC; EXPAND_TAC "x"; ASM_REWRITE_TAC[IMAGE_CLAUSES]; SUBGOAL_THEN` (f:real^3 -> real -> real^3 ) w t' = w ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` v': real^3 `])); ANTS_TAC; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; EXPAND_TAC "v'"; ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `)); ASM_REWRITE_TAC[]; SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC; ASM_REWRITE_TAC[lunar; circular]; MP_TAC Local_lemmas.IVS_RNODE_IN_AFF_V; ANTS_TAC; ASM_REWRITE_TAC[]; STRIP_TAC THEN STRIP_TAC; MP_TAC ( let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v: real^3 `;` v': real^3 `] tt); ANTS_TAC; UNDISCH_TAC ` ivs_rho_node1 FF w IN aff_gt {vec 0, v} {rho_node1 FF v} ` ; ASM_REWRITE_TAC[]; DISCH_THEN (SUBST_ALL_TAC o SYM); DOWN; ASM_REWRITE_TAC[]; UNDISCH_TAC ` aff_gt {vec 0, v} {u: real^3} = {y | ?t1 t2 t3. &0 < t3 /\ t1 + t2 + t3 = &1 /\ y = t1 % vec 0 + t2 % v + t3 % u}`; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; SUBGOAL_THEN` aff_gt {vec 0, v} {uh: real^3} = aff_gt {vec 0, w} {ivs_rho_node1 FF w} ` MP_TAC; ASM_REWRITE_TAC[]; SIMP_TAC[]; ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas.LOFA_IMP_NOT_COLL_IVS); REPEAT STRIP_TAC; SUBGOAL_THEN` aff_gt {vec 0, w} {ivs_rho_node1 FF w} = aff_gt {vec 0, w} {(f: real^3 -> real -> real^3) v' t' } ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; REPLICATE_TAC 3 DOWN THEN PHA; SIMP_TAC[]; FIRST_X_ASSUM SUBST1_TAC; DISJ1_TAC; MP_TAC ( let tt = GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS in ISPECL [` {w:real^3 } `;` {vec 0, w:real^3} `; `{(f: real^3 -> real -> real^3) v' t' } `] tt); ANTS_TAC; REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `)); DOWN; SIMP_TAC[SET_RULE` ~(w = vec 0) ==> {vec 0, w} DIFF {w} = {vec 0 } `; SET_RULE` {a} UNION {b} = {a,b} `]; SUBGOAL_THEN` x SUBSET {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC; EXPAND_TAC "x"; REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM]; ABBREV_TAC `i' = n'' - (j:num ) `; ASSUME_TAC2 (ARITH_RULE` ~( n'' < j) ==> (n'' - j) + j = (n'': num) `); SUBGOAL_THEN` ITER i' (rho_node1 FF) v = v' ` ASSUME_TAC; EXPAND_TAC "v"; REWRITE_TAC[ITER_ADD]; EXPAND_TAC "i'"; FIRST_ASSUM SUBST1_TAC; ASM_REWRITE_TAC[]; CONJ_TAC; EXISTS_TAC` i': num `; ASM_REWRITE_TAC[]; CONJ_TAC; EXPAND_TAC "i'"; UNDISCH_TAC` ~(n'' < j:num) `; UNDISCH_TAC` ~(n'' = j:num) `; ARITH_TAC; EXPAND_TAC "i'"; UNDISCH_TAC` ~( n'' < j: num) `; SIMP_TAC[ARITH_RULE`~( n'' < j) ==> (n'' - j < i <=> n'' < i + (j:num))`]; ASM_REWRITE_TAC[]; EXISTS_TAC` i' + 1 `; ASM_REWRITE_TAC[GSYM ADD1; ITER; ARITH_RULE` 0 < SUC a `]; EXPAND_TAC "i'"; UNDISCH_TAC` ~( n'' < j: num) `; SIMP_TAC[ARITH_RULE`~( n'' < j) ==> (SUC (n'' - j) < i <=> n'' < (i + (j:num)) - 1 )`]; ASM_REWRITE_TAC[]; STRIP_TAC; MATCH_MP_TAC (ARITH_RULE` n < x /\ ~( n = x - 1) ==> n < x - 1 `); ASM_REWRITE_TAC[]; UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; EXPAND_TAC "x"; REWRITE_TAC[IMAGE_CLAUSES; INSERT_SUBSET; EMPTY_SUBSET; IN_INTER]; STRIP_TAC; ASSUME_TAC2 ( let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` v': real^3 `] tt); ASSUME_TAC2 ( let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` rho_node1 FF v'`] tt); DOWN THEN DOWN; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); FIRST_ASSUM (MP_TAC o (SPECL [` t':real `;` v': real^3 `])); ANTS_TAC; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [` t':real `;` rho_node1 FF v' `])); ANTS_TAC; ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT]; STRIP_TAC; DOWN THEN DOWN; ASM_REWRITE_TAC[]; STRIP_TAC; UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_TOO; NHANH Fan.th3a; NHANH Fan.th3b1; STRIP_TAC; UNDISCH_TAC` (f: real^3 -> real -> real^3) v' t' IN aff_gt {vec 0, v} {rho_node1 FF v} `; UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_TOO; NHANH Fan.th3b1; STRIP_TAC; DISJ1_TAC; MATCH_MP_TAC TOW_POINTS_IN_IMP_AFF_GT_SUBSET; ASM_REWRITE_TAC[SET_RULE` DISJOINT {a} {x,y} <=> ~( a = x ) /\ ~( a = y) `]; STRIP_TAC; SUBGOAL_THEN` !t. abs t < d /\ t IN real_interval (a,b) ==> (!s u. s IN IMAGE (IMAGE (\v. f v t)) E /\ u IN IMAGE (\v. (f:real^3 -> real -> real^3) v t) V ==> (aff_gt {vec 0} s INTER aff_lt {vec 0} {u} = {})) ` ASSUME_TAC; FIRST_ASSUM NHANH; GEN_TAC THEN STRIP_TAC; FIRST_ASSUM NHANH; GEN_TAC THEN GEN_TAC; ABBREV_TAC` vw = (aff_gt {vec 0} s SUBSET aff_gt {vec 0, v} {rho_node1 FF v} \/ aff_gt {vec 0} s SUBSET aff_gt {vec 0, w} {rho_node1 FF w})`; STRIP_TAC; DOWN; REWRITE_TAC[IN_IMAGE]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` x: real^3 `])); ANTS_TAC; ASM_REWRITE_TAC[]; STRIP_TAC; ASSUME_TAC2 Local_lemmas1.LOCAL_RHO_NODE_PAIR_E; DOWN; SUBGOAL_THEN` FAN (vec 0: real^3,V,E)` MP_TAC; UNDISCH_TAC` local_fan (V: real^3 -> bool,E,FF) `; SIMP_TAC[local_fan]; LET_TAC; SIMP_TAC[]; PHA; NHANH Topology.disjoint_fan3; STRIP_TAC; ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas1.LOCAL_RHO_NODE_PAIR_E); DOWN; SUBGOAL_THEN` FAN (vec 0: real^3,V,E)` MP_TAC; UNDISCH_TAC` local_fan (V: real^3 -> bool,E,FF) `; SIMP_TAC[local_fan]; LET_TAC; SIMP_TAC[]; PHA; NHANH Topology.disjoint_fan3; STRIP_TAC; SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC; ASM_REWRITE_TAC[lunar; circular]; ASSUME_TAC2 Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI; DOWN THEN STRIP_TAC; UNDISCH_TAC` vec 0 IN conv0 {v, w:real^3} `; NHANH IN_CONV0_IMP_AFF_EQ1; STRIP_TAC; ASM_CASES_TAC ` x = v:real^3 `; FIRST_X_ASSUM SUBST_ALL_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) v t' = v ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; SIMP_TAC[]; STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; FIRST_ASSUM (ASSUME_TAC2 o SPEC_ALL); DOWN; REWRITE_TAC[SET_RULE` ~( a = b) <=> DISJOINT {b} {a} `]; NHANH AFF_LT_SUBSET_AFF11; UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `; UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `; UNDISCH_TAC` aff {vec 0, v} INTER aff_gt {vec 0, v} {rho_node1 FF v} = {} `; UNDISCH_TAC` vw: bool `; EXPAND_TAC "vw"; DISCH_TAC; PHA THEN STRIP_TAC; MATCH_MP_TAC (SET_RULE`!A. a SUBSET A /\ x INTER A = {} ==> x INTER a = {} `); EXISTS_TAC` aff {vec 0, v:real^3} `; ASM_REWRITE_TAC[]; UNDISCH_TAC` aff_gt {vec 0} s SUBSET aff_gt {vec 0, v} {rho_node1 FF v} \/ aff_gt {vec 0} s SUBSET aff_gt {vec 0, w} {rho_node1 FF w} `; STRIP_TAC; MATCH_MP_TAC (SET_RULE`!A. a SUBSET A /\ x INTER A = {} ==> a INTER x = {} `); EXISTS_TAC` aff_gt {vec 0, v} {rho_node1 FF v} `; UNDISCH_TAC` aff_gt {vec 0, v} {u:real^3} = {y | ?t1 t2 t3. &0 < t3 /\ t1 + t2 + t3 = &1 /\ y = t1 % vec 0 + t2 % v + t3 % u} `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` aff_gt {vec 0, v} {u} = aff_gt {vec 0, v} {uh: real^3} `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; DOWN; UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `; CONV_TAC SET_RULE; ASM_CASES_TAC` x = (w:real^3) `; FIRST_X_ASSUM SUBST_ALL_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) w t' = w ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; SIMP_TAC[]; STRIP_TAC; UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w: real^3} `; UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `; UNDISCH_TAC` aff {vec 0, v} INTER aff_gt {vec 0, v} {rho_node1 FF v} = {} `; ASSUME_TAC2 (Local_lemmas.LOFA_IMP_V_DIFF); FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC ` w:real^3 `)); DOWN; NHANH (SET_RULE` ~( a = b) ==> DISJOINT {b} {a} `); NHANH AFF_LT_SUBSET_AFF11; STRIP_TAC; DOWN; UNDISCH_TAC` vw: bool `; EXPAND_TAC "vw"; CONV_TAC SET_RULE; ASSUME_TAC2 LUNAR_IMP_IN_TWO_HAFLS_PLANE; FIRST_X_ASSUM (MP_TAC o (SPEC` x: real^3 `)); PHA; ANTS_TAC; ASM_REWRITE_TAC[]; ASSUME_TAC2 (GSYM Local_lemmas.AFF_IVS_RHO_NODE_EQQ); FIRST_ASSUM SUBST1_TAC; DISCH_TAC; UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `; DISCH_THEN (ASSUME_TAC o SYM); ASSUME_TAC2 (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS); UNDISCH_TAC` x IN aff_gt {vec 0, v} {rho_node1 FF v} \/ x IN aff_gt {vec 0, w} {rho_node1 FF w} `; STRIP_TAC; UNDISCH_TAC` vw: bool `; EXPAND_TAC "vw"; STRIP_TAC; UNDISCH_TAC` x IN aff_gt {vec 0, v} {rho_node1 FF v} ` ; UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC o SYM); FIRST_ASSUM (MP_TAC o (SPECL [` t': real`;` x: real^3 `])); ANTS_TAC; ASM_REWRITE_TAC[]; FIRST_ASSUM SUBST1_TAC; STRIP_TAC; MATCH_MP_TAC (SET_RULE` ! s. a SUBSET s /\ s INTER b = {} ==> a INTER b = {} `); EXISTS_TAC` aff_gt {vec 0, v} {rho_node1 FF v} `; ASM_REWRITE_TAC[]; MATCH_MP_TAC COLL_IN_AFF_GT_INTER_EMPTY; ASM_REWRITE_TAC[]; ASM_CASES_TAC` aff_gt {vec 0} s INTER aff_lt {vec 0} {u': real^3} = {} `; FIRST_X_ASSUM ACCEPT_TAC; MP_TAC (ISPECL [` s: real^3 -> bool `; `u': real^3 `; `vec 0: real^3 `; `v:real^3 `; `rho_node1 FF v `; ` ivs_rho_node1 FF v `] (GEN_ALL AZIM_PI_LEMMA)); ANTS_TAC; ASM_REWRITE_TAC[]; DOWN THEN DOWN; ASM_SIMP_TAC[]; STRIP_TAC THEN STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS; ASM_REWRITE_TAC[]; SUBGOAL_THEN ` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {x} ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; UNDISCH_TAC` interior_angle1 (vec 0) FF v < pi `; ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS; UNDISCH_TAC` interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w `; ASM_SIMP_TAC[]; STRIP_TAC; REAL_ARITH_TAC; UNDISCH_TAC` vw: bool `; EXPAND_TAC "vw"; STRIP_TAC; ASM_CASES_TAC` aff_gt {vec 0} s INTER aff_lt {vec 0} {u': real^3} = {} `; FIRST_X_ASSUM ACCEPT_TAC; MP_TAC ( let tt = GEN_ALL AZIM_PI_LEMMA in ISPECL [` s: real^3 -> bool `; `u': real^3 `;` vec 0: real^3 `;` w: real^3 `; ` rho_node1 FF w `;` ivs_rho_node1 FF w `] tt); ANTS_TAC; ASM_REWRITE_TAC[]; SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, w} {ivs_rho_node1 FF w} ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ; ASM_REWRITE_TAC[Local_lemmas.LUNAR_COMM]; FIRST_X_ASSUM (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas.AFF_GT_SAME_WITH_ENDS; UNDISCH_TAC` x IN aff_gt {vec 0, w} {rho_node1 FF w} `; FIRST_X_ASSUM SUBST1_TAC; UNDISCH_TAC` aff_gt {vec 0, v} {ivs_rho_node1 FF v} = aff_gt {vec 0, w} {rho_node1 FF w} `; DISCH_THEN (SUBST1_TAC o SYM ); ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS; ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas.LOFA_IMP_NOT_COLL_IVS); ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` aff_gt {vec 0, v} {ivs_rho_node1 FF v} = aff_gt {vec 0, v} {x} ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; ASM_REWRITE_TAC[]; UNDISCH_TAC` interior_angle1 (vec 0) FF v < pi `; ASM_REWRITE_TAC[]; ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w: real^ 3 `)); ASM_REWRITE_TAC[]; REAL_ARITH_TAC; MATCH_MP_TAC (SET_RULE` ! A. a SUBSET A /\ A INTER b = {} ==> a INTER b = {} `); EXISTS_TAC` aff_gt {vec 0, w} {rho_node1 FF w} `; CONJ_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC COLL_IN_AFF_GT_INTER_EMPTY; CONJ_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; ASM_REWRITE_TAC[]; UNDISCH_TAC` aff_gt {vec 0, w} {rho_node1 FF w} = aff_gt {vec 0, v} {rho_node1 FF w}`; ASSUME_TAC2 Local_lemmas.AFF_IVS_RHO_NODE_EQQ; FIRST_X_ASSUM SUBST1_TAC; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; UNDISCH_TAC ` x IN aff_gt {vec 0, w} {rho_node1 FF w} `; UNDISCH_TAC` aff_gt {vec 0, v} {ivs_rho_node1 FF v} = aff_gt {vec 0, w} {rho_node1 FF w} `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS; DOWN; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; SIMP_TAC[]; ASM_REWRITE_TAC[]; EXPAND_TAC "CONCL"; ABBREV_TAC` e1 = min ( -- a) b `; EXISTS_TAC` min e1 d `; CONJ_TAC; EXPAND_TAC "e1"; REWRITE_TAC[REAL_LT_MIN]; ASM_REWRITE_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `]; GEN_TAC; REWRITE_TAC[REAL_BOUNDS_LT]; EXPAND_TAC "e1"; REWRITE_TAC[REAL_LT_MIN]; STRIP_TAC; CONJ_TAC; REWRITE_TAC[MESON[] ` ~(?v w u. P v w u /\ Q v w u /\ ~ R v w u ) <=> (! v w u. P v w u /\ Q v w u ==> R v w u ) `]; REPEAT GEN_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC` t': real `)); ANTS_TAC; ASM_REWRITE_TAC[real_interval; IN_ELIM_THM]; DOWN THEN DOWN THEN DOWN; REAL_ARITH_TAC; SIMP_TAC[]; CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; DOWN THEN DOWN THEN DOWN; REWRITE_TAC[real_interval; IN_ELIM_THM]; REAL_ARITH_TAC; ASM_REWRITE_TAC[]]);;
let LOCAL_FAN_SET_E = 
prove_by_refinement(` local_fan (V,E,FF) ==> {{v, rho_node1 FF v} | v IN V } = E `,
[REWRITE_TAC[EXTENSION; IN_ELIM_THM]; STRIP_TAC; GEN_TAC; EQ_TAC; STRIP_TAC; DOWN; SIMP_TAC[GSYM EXTENSION]; STRIP_TAC; MATCH_MP_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E; ASM_REWRITE_TAC[]; REWRITE_TAC[GSYM EXTENSION]; DOWN THEN PHA; NHANH EDGE_IN_LOCAL_FAN_DET_RHO_NODE; SIMP_TAC[EQ_SYM_EQ]]);;
let LOCAL_FAN_FACE_FF = 
prove_by_refinement(` local_fan (V,E,FF) ==> { v, rho_node1 FF v | v IN V } = FF `,
[REWRITE_TAC[EXTENSION; IN_ELIM_THM]; STRIP_TAC; GEN_TAC; EQ_TAC; STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS; DOWN THEN STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM ACCEPT_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2; DOWN THEN PHA THEN STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x: real^3 # real^3 `)); EXISTS_TAC` FST (x: real^3 # real^3 ) `; CONJ_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_IN_V2; ASM_REWRITE_TAC[]; FIRST_X_ASSUM ACCEPT_TAC]);;
let ORD_PAIRS_INJ_IMAGE = 
prove_by_refinement(` (! s. s IN E ==> INJ f s (IMAGE f s )) ==> ord_pairs (IMAGE (\s. IMAGE f s) E) = IMAGE (\ (x:real^N,y). (f: real^N -> real^M) x, f y) (ord_pairs E ) `,
[REWRITE_TAC[EXTENSION]; STRIP_TAC; GEN_TAC THEN EQ_TAC; REWRITE_TAC[ord_pairs; IN_ELIM_THM; IN_IMAGE]; NHANH_PAT `\x. x ==> y ` (SET_RULE` {a,b} = S ==> a IN S /\ b IN S `); REWRITE_TAC[IN_IMAGE]; STRIP_TAC; EXISTS_TAC` (x'': real^N, x''': real^N) `; ASM_REWRITE_TAC[]; SUBGOAL_THEN` {x'', x''': real^N} = x' ` MP_TAC; ASM_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; INSERT_SUBSET; EMPTY_SUBSET]; DOWN THEN DOWN; FIRST_X_ASSUM NHANH; REWRITE_TAC[SUBSET; INJ]; STRIP_TAC; REPEAT STRIP_TAC; UNDISCH_TAC` !x. (x:real^N) IN x' ==> (f x):real^M IN IMAGE f x' `; DISCH_THEN (ASSUME_TAC2 o (SPEC` x'''': real^N `)); DOWN_TAC; CONV_TAC SET_RULE; DOWN THEN DOWN; MESON_TAC[]; REWRITE_TAC[IN_IMAGE; ord_pairs; IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC` (f: real^N -> real^M ) a `; EXISTS_TAC` (f: real^N -> real^M ) b `; ASM_REWRITE_TAC[]; EXISTS_TAC` {a, b: real^N } `; ASM_REWRITE_TAC[IMAGE_CLAUSES]]);;
let SET2_DETER =
prove(` s = {x,y} /\ a IN s /\ b IN s /\ ~( a = b) ==> s = {a, b} `,
STRIP_TAC THEN REPLICATE_TAC 3 DOWN THEN PHA THEN ASM_REWRITE_TAC[] THEN CONV_TAC SET_RULE);;
let INSERT_UNION_CLAUSES =
prove(` x INSERT S UNION U = S UNION x INSERT U /\ {} UNION U = U `,
REWRITE_TAC[Local_lemmas.INSERT_UNION2; UNION_EMPTY]);;
let INJ_IMP_BIJ_IMAGE = 
prove(` INJ f S S' ==> BIJ f S (IMAGE f S) `,
SIMP_TAC[BIJ; INJ; SURJ; FUN_IN_IMAGE] THEN STRIP_TAC THEN REWRITE_TAC[IN_IMAGE] THEN ASM_MESON_TAC[]);;
let BIJ_AND_MAP_COMM = 
prove_by_refinement(` local_fan (V,E,FF) /\ BIJ (f: real^3 -> real^3) V V' /\ IMAGE (\s. IMAGE f s) E = E' /\ FAN (vec 0, V', E') /\ (\(x,y). f x, f y ) = ff ==> BIJ ff ( darts_of_hyp E V) (darts_of_hyp E' V') /\ (!x. x IN darts_of_hyp E V ==> ff_of_hyp (vec 0,V',E') (ff x) = ff (ff_of_hyp (vec 0,V,E) x)) `,
[REWRITE_TAC[hyp_iso; local_fan]; LET_TAC; NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC; REWRITE_TAC[local_fan]; LET_TAC; ASM_REWRITE_TAC[]; DOWN; ASM_SIMP_TAC[]; STRIP_TAC; CONJ_TAC; EXISTS_TAC` (x: real^3 # real^3) `; ASM_REWRITE_TAC[]; UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `; DISCH_THEN SUBST_ALL_TAC; ASM_SIMP_TAC[]; UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ; ASM_SIMP_TAC[]; ASSUME_TAC2 LOCAL_FAN_SET_E; ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF; ASSUME_TAC2 LOCAL_FAN_FACE_FF; SUBST_ALL_TAC ( MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `); ASM_REWRITE_TAC[]; SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC; EXPAND_TAC "E'";
REWRITE_TAC[EXTENSION]; GEN_TAC; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM; IN_IMAGE]; EQ_TAC; STRIP_TAC; EXISTS_TAC` {v, rho_node1 FF v} `; REWRITE_TAC[IMAGE_CLAUSES]; ASM_REWRITE_TAC[]; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; STRIP_TAC; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[IMAGE_CLAUSES]; UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `; PAT_REWRITE_TAC `\x. x ==> y ` [BIJ]; NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1; STRIP_TAC; SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC; REWRITE_TAC[self_pairs]; EXPAND_TAC "V'"; EXPAND_TAC "E'"; REWRITE_TAC[IN_IMAGE]; MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `); GEN_TAC; STRIP_TAC; DOWN; PHA; REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM]; EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `; EXISTS_TAC` x': real^3 `; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs]; SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC; REWRITE_TAC[INJ]; REPEAT STRIP_TAC; REWRITE_TAC[IN_IMAGE]; EXISTS_TAC` x': real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` (s: real^3 -> bool) IN E `; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; ASM_CASES_TAC` x' = (y:real^3) `; DOWN THEN SIMP_TAC[]; REPLICATE_TAC 6 DOWN THEN PHA; NHANH ( MESON[SET2_DETER]` x' IN s /\ y IN s /\ f x' = f y /\ v IN V /\ s = {v, rho_node1 FF v} /\ ~(x' = y) ==> s = {x', y} `); STRIP_TAC; SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC; DOWN; ASM_REWRITE_TAC[IMAGE_CLAUSES]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC `v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `; REWRITE_TAC[FAN; fan6]; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `)); DOWN; UNDISCH_TAC` s = {x', y:real^3} `; SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY]; ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2]; NHANH ORD_PAIRS_INJ_IMAGE; REWRITE_TAC[GSYM ord_pairs]; SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC; REWRITE_TAC[EXTENSION; IN_IMAGE]; GEN_TAC; EQ_TAC; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `)); EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; DOWN THEN DOWN; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; REPEAT STRIP_TAC; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; REPLICATE_TAC 4 DOWN THEN PHA; CONV_TAC SET_RULE; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC` {v, rho_node1 FF v }`; ASM_REWRITE_TAC[]; EXPAND_TAC "E"; DOWN THEN DOWN; CONV_TAC SET_RULE; SIMP_TAC[]; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC; REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM]; GEN_TAC; STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `)); PHA; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `; DISCH_THEN (SUBST1_TAC o SYM); SIMP_TAC[darts_of_hyp; UNION_EMPTY]; (* ============ *) ASM_SIMP_TAC[]; STRIP_TAC; CONJ_TAC; MATCH_MP_TAC (GEN_ALL INJ_IMP_BIJ_IMAGE); EXISTS_TAC` IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (FF UNION {(v:real^3,w: real^3) | w,v IN FF} )`; REWRITE_TAC[INJ; FUN_IN_IMAGE]; EXPAND_TAC "ff"; SUBGOAL_THEN` !x. x IN FF UNION {v,w | w,v IN FF} ==> (? a b. x = (a,b) /\ a IN V /\ b IN (V: real^3 -> bool)) ` MP_TAC; REWRITE_TAC[IN_UNION]; REPEAT STRIP_TAC; DOWN; EXPAND_TAC "FF"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC` v: real^3 `; EXISTS_TAC` rho_node1 FF v `; ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[]; DOWN; EXPAND_TAC "FF"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC` rho_node1 FF v' `; EXISTS_TAC` v': real^ 3 `; DOWN THEN DOWN; ASM_SIMP_TAC[PAIR_EQ]; REPEAT STRIP_TAC; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[]; DISCH_THEN NHANH; REPEAT STRIP_TAC; DOWN; ASM_REWRITE_TAC[]; EXPAND_TAC "ff"; REWRITE_TAC[PAIR_EQ]; UNDISCH_TAC` INJ (f:real^3 -> real^3) V V' `; DOWN THEN DOWN; UNDISCH_TAC` (a:real^3) IN V `; UNDISCH_TAC` (b: real^3) IN V `; REWRITE_TAC[INJ]; MESON_TAC[]; UNDISCH_TAC` darts_of_hyp E V = FF UNION {v:real^3,w | w,v IN FF} `; DISCH_THEN (ASSUME_TAC2 o SYM); ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; SUBGOAL_THEN` (ff: real^3 # real^3 -> real^3 # real^3) x' IN darts_of_hyp E' V' ` MP_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC FUN_IN_IMAGE; FIRST_ASSUM ACCEPT_TAC; DOWN; SIMP_TAC[Wrgcvdr_cizmrrh.ff_of_hyp2]; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (SUBST1_TAC o SYM); REWRITE_TAC[]; REWRITE_TAC[IN_UNION]; STRIP_TAC THEN STRIP_TAC; UNDISCH_TAC` (x': real^3 # real^3 ) IN FF `; EXPAND_TAC "FF"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "ff"; REWRITE_TAC[PAIR_EQ]; SUBGOAL_THEN` rho_node1 FF v IN V ` MP_TAC; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[]; UNDISCH_TAC` local_fan (V,E,FF) `; PHA; NHANH Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND; ASSUME_TAC2 Local_lemmas.IVS_RHO_IDD; ASM_SIMP_TAC[]; ONCE_REWRITE_TAC[INSERT_COMM]; REWRITE_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET]; STRIP_TAC; SUBGOAL_THEN` EE ((f:real^3 -> real^3) (rho_node1 FF v)) E' = { f v, f (rho_node1 FF (rho_node1 FF v )) } ` MP_TAC; REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET]; CONJ_TAC; GEN_TAC; REWRITE_TAC[IN_ELIM_THM]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; DOWN; REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND]; STRIP_TAC; UNDISCH_TAC` INJ (f: real^3 -> real ^3) V V' `; REWRITE_TAC[INJ]; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`rho_node1 FF v `;` v': real^3 `])); ASM_REWRITE_TAC[]; CONV_TAC SET_RULE; UNDISCH_TAC` INJ (f: real^3 -> real ^3) V V' `; REWRITE_TAC[INJ]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [`rho_node1 FF v `;` rho_node1 FF v'`])); ANTS_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[]; ASSUME_TAC2 Polar_fan.RHO_NODE1_INJECTIVE; FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL[` v: real^3 `;` v': real^3 `])); ASM_SIMP_TAC[]; REWRITE_TAC[IN_INSERT]; GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM]; REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]; STRIP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC `v: real^3 `; ASM_REWRITE_TAC[INSERT_COMM]; ASM_REWRITE_TAC[]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` rho_node1 FF v `; ASM_REWRITE_TAC[]; SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET]; UNDISCH_TAC` (x': real^3 # real^3) IN {v,w | w,v IN FF} `; EXPAND_TAC "FF"; REWRITE_TAC[IN_ELIM_THM; PAIR_EQ]; STRIP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "ff"; REWRITE_TAC[PAIR_EQ]; ASSUME_TAC2 ( SPEC` v': real^3 ` ( GEN`v: real^3 ` Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)); ASM_REWRITE_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET]; SUBGOAL_THEN` EE ((f:real^3 -> real^3) v') E'= { f (rho_node1 FF v'), f (ivs_rho_node1 FF v' )} ` MP_TAC; REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET]; UNDISCH_TAC` INJ (f: real^3 -> real^3) V V' `; REWRITE_TAC[INJ]; STRIP_TAC; CONJ_TAC; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM; Collect_geom.PAIR_EQ_EXPAND]; REPEAT STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL [` v': real^3 `;` v'': real^3 `])); ASM_REWRITE_TAC[IN_INSERT]; FIRST_X_ASSUM (MP_TAC o (SPECL [` v': real^3 `;` rho_node1 FF v'' `])); ANTS_TAC; ASM_REWRITE_TAC[IN_INSERT]; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[]; STRIP_TAC; ASM_REWRITE_TAC[]; ASSUME_TAC2 ( SPEC ` v'': real^3 ` ( GEN`v: real^3 ` Local_lemmas.IVS_RHO_IDD)); ASM_REWRITE_TAC[IN_INSERT]; REWRITE_TAC[IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY]; REPEAT STRIP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` v': real^3 `; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` ivs_rho_node1 FF v' `; ASM_REWRITE_TAC[]; ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V; CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; ASSUME_TAC2 ( SPEC` v': real ^3 ` ( GEN`v: real^3 ` Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS )); ASM_REWRITE_TAC[INSERT_COMM]; SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET]]);;
let NODE_EDGE_COMM_LEMMA = 
prove_by_refinement (` local_fan (V,E,FF) /\ BIJ f V V' /\ IMAGE (\s. IMAGE f s) E = E' /\ FAN (vec 0,V',E') /\ (\(x,y). f x,f y) = ff ==> (!x. x IN darts_of_hyp E V ==> nn_of_hyp (vec 0,V',E') (ff x) = ff (nn_of_hyp (vec 0,V,E) x) /\ ee_of_hyp (vec 0,V',E') (ff x) = ff (ee_of_hyp (vec 0,V,E) x) ) `,
[REWRITE_TAC[hyp_iso; local_fan]; LET_TAC; NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC; REWRITE_TAC[local_fan]; LET_TAC; ASM_REWRITE_TAC[]; DOWN; ASM_SIMP_TAC[]; STRIP_TAC; CONJ_TAC; EXISTS_TAC` (x: real^3 # real^3) `; ASM_REWRITE_TAC[]; UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `; DISCH_THEN SUBST_ALL_TAC; ASM_SIMP_TAC[]; UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ; ASM_SIMP_TAC[]; ASSUME_TAC2 LOCAL_FAN_SET_E; ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF; ASSUME_TAC2 LOCAL_FAN_FACE_FF; SUBST_ALL_TAC ( MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `); ASM_REWRITE_TAC[]; SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC; EXPAND_TAC "E'";
REWRITE_TAC[EXTENSION]; GEN_TAC; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM; IN_IMAGE]; EQ_TAC; STRIP_TAC; EXISTS_TAC` {v, rho_node1 FF v} `; REWRITE_TAC[IMAGE_CLAUSES]; ASM_REWRITE_TAC[]; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; STRIP_TAC; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[IMAGE_CLAUSES]; UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `; PAT_REWRITE_TAC `\x. x ==> y ` [BIJ]; NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1; STRIP_TAC; SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC; REWRITE_TAC[self_pairs]; EXPAND_TAC "V'"; EXPAND_TAC "E'"; REWRITE_TAC[IN_IMAGE]; MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `); GEN_TAC; STRIP_TAC; DOWN; PHA; REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM]; EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `; EXISTS_TAC` x': real^3 `; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs]; SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC; REWRITE_TAC[INJ]; REPEAT STRIP_TAC; REWRITE_TAC[IN_IMAGE]; EXISTS_TAC` x': real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` (s: real^3 -> bool) IN E `; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; ASM_CASES_TAC` x' = (y:real^3) `; DOWN THEN SIMP_TAC[]; REPLICATE_TAC 6 DOWN THEN PHA; NHANH ( MESON[SET2_DETER]` x' IN s /\ y IN s /\ f x' = f y /\ v IN V /\ s = {v, rho_node1 FF v} /\ ~(x' = y) ==> s = {x', y} `); STRIP_TAC; SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC; DOWN; ASM_REWRITE_TAC[IMAGE_CLAUSES]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC `v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `; REWRITE_TAC[FAN; fan6]; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `)); DOWN; UNDISCH_TAC` s = {x', y:real^3} `; SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY]; ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2]; NHANH ORD_PAIRS_INJ_IMAGE; REWRITE_TAC[GSYM ord_pairs]; SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC; REWRITE_TAC[EXTENSION; IN_IMAGE]; GEN_TAC; EQ_TAC; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `)); EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; DOWN THEN DOWN; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; REPEAT STRIP_TAC; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; REPLICATE_TAC 4 DOWN THEN PHA; CONV_TAC SET_RULE; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC` {v, rho_node1 FF v }`; ASM_REWRITE_TAC[]; EXPAND_TAC "E"; DOWN THEN DOWN; CONV_TAC SET_RULE; SIMP_TAC[]; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC; REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM]; GEN_TAC; STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `)); PHA; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `; DISCH_THEN (SUBST1_TAC o SYM); SIMP_TAC[darts_of_hyp; UNION_EMPTY]; STRIP_TAC; REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2]; UNDISCH_TAC` darts_of_hyp E V = FF UNION {v:real^3,w | w,v IN FF} `; DISCH_THEN (ASSUME_TAC o SYM); ASM_SIMP_TAC[]; SUBGOAL_THEN`(! x. x IN darts_of_hyp E (V:real^3 -> bool) ==> ((ff x): real^3 # real^3) IN darts_of_hyp E' V' )` MP_TAC; ASM_REWRITE_TAC[FUN_IN_IMAGE]; STRIP_TAC; FIRST_ASSUM NHANH; ASM_SIMP_TAC[]; SUBGOAL_THEN` ! v. v IN V ==> ivs_rho_node1 FF (rho_node1 FF v) = v ` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD; ASM_REWRITE_TAC[]; SUBGOAL_THEN` ! v. v IN V ==> rho_node1 FF (ivs_rho_node1 FF v) = v ` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS; ASM_REWRITE_TAC[]; SUBGOAL_THEN` !v . v IN V ==> rho_node1 FF v IN V ` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_SIMP_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; SUBGOAL_THEN` !v . v IN V ==> ivs_rho_node1 FF v IN V ` ASSUME_TAC; MATCH_MP_TAC Polar_fan.IVS_RHO_NODE1_IN_V; EXISTS_TAC` E: (real^3 -> bool) -> bool `; ASM_REWRITE_TAC[]; UNDISCH_TAC` INJ (f: real^3 -> real^3) V V' `; REWRITE_TAC[INJ]; STRIP_TAC; SUBGOAL_THEN` !v. v IN V ==> EE v E = {rho_node1 FF v, (ivs_rho_node1 FF v)} ` ASSUME_TAC; REPEAT STRIP_TAC; MATCH_MP_TAC Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND; ASM_REWRITE_TAC[]; SUBGOAL_THEN`!v. v IN V ==> EE ((f:real^3 -> real^3) v ) E' = {f (rho_node1 FF v), f (ivs_rho_node1 FF v ) } ` ASSUME_TAC; REPEAT STRIP_TAC; REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; GEN_TAC THEN STRIP_TAC; DOWN; REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND]; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL [` v: real^3 `;` v': real^3 `])); ASM_REWRITE_TAC[IN_INSERT]; FIRST_X_ASSUM (MP_TAC o (SPECL [` v: real^3 `;` rho_node1 FF v' `])); ANTS_TAC; ASM_REWRITE_TAC[IN_INSERT]; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_REWRITE_TAC[]; STRIP_TAC; ASM_SIMP_TAC[IN_INSERT]; REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]; GEN_TAC THEN STRIP_TAC; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; EXISTS_TAC` ivs_rho_node1 FF v `; ASM_SIMP_TAC[INSERT_COMM]; GEN_TAC THEN STRIP_TAC; SUBGOAL_THEN` x' IN FF UNION {v:real^3,w | w,v IN FF} ` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_UNION]; STRIP_TAC; DOWN; EXPAND_TAC "FF"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "ff"; REWRITE_TAC[]; CONJ_TAC; ASM_SIMP_TAC[PAIR_EQ]; REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]; REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2]; UNDISCH_TAC` x' IN darts_of_hyp E (V: real^3 -> bool) `; UNDISCH_TAC` (ff: real^3 # real^3 -> real^3 # real^3 ) x' IN IMAGE ff (darts_of_hyp E V) `; ASM_REWRITE_TAC[]; EXPAND_TAC "ff"; SIMP_TAC[]; DOWN; EXPAND_TAC "FF"; REWRITE_TAC[IN_ELIM_THM; PAIR_EQ]; STRIP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "ff"; REWRITE_TAC[PAIR_EQ]; ASM_SIMP_TAC[]; ONCE_REWRITE_TAC[INSERT_COMM]; REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]; REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2]; UNDISCH_TAC` x' IN darts_of_hyp E (V: real^3 -> bool) `; UNDISCH_TAC` (ff: real^3 # real^3 -> real^3 # real^3 ) x' IN IMAGE ff (darts_of_hyp E V) `; ASM_REWRITE_TAC[]; EXPAND_TAC "ff"; SIMP_TAC[]]);;
let HYP_ISO_LEMMAA = 
prove_by_refinement (` local_fan (V,E,FF) /\ BIJ f V V' /\ IMAGE (\s. IMAGE f s) E = E' /\ FAN (vec 0,V',E') /\ (\(x,y). f x,f y) = ff ==> hyp_iso ff (hypermap (HYP (vec 0, V, E)), hypermap (HYP (vec 0, V', E')))`,
[REWRITE_TAC[hyp_iso; local_fan]; LET_TAC; NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC; REWRITE_TAC[local_fan]; LET_TAC; ASM_REWRITE_TAC[]; DOWN; ASM_SIMP_TAC[]; STRIP_TAC; CONJ_TAC; EXISTS_TAC` (x: real^3 # real^3) `; ASM_REWRITE_TAC[]; UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `; DISCH_THEN SUBST_ALL_TAC; ASM_SIMP_TAC[]; UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ; ASM_SIMP_TAC[]; ASSUME_TAC2 LOCAL_FAN_SET_E; ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF; ASSUME_TAC2 LOCAL_FAN_FACE_FF; SUBST_ALL_TAC ( MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `); ASM_REWRITE_TAC[]; SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC; EXPAND_TAC "E'";
REWRITE_TAC[EXTENSION]; GEN_TAC; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM; IN_IMAGE]; EQ_TAC; STRIP_TAC; EXISTS_TAC` {v, rho_node1 FF v} `; REWRITE_TAC[IMAGE_CLAUSES]; ASM_REWRITE_TAC[]; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; STRIP_TAC; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[IMAGE_CLAUSES]; UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `; PAT_REWRITE_TAC `\x. x ==> y ` [BIJ]; NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1; STRIP_TAC; SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC; REWRITE_TAC[self_pairs]; EXPAND_TAC "V'"; EXPAND_TAC "E'"; REWRITE_TAC[IN_IMAGE]; MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `); GEN_TAC; STRIP_TAC; DOWN; PHA; REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM]; EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `; EXISTS_TAC` x': real^3 `; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs]; SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC; REWRITE_TAC[INJ]; REPEAT STRIP_TAC; REWRITE_TAC[IN_IMAGE]; EXISTS_TAC` x': real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` (s: real^3 -> bool) IN E `; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; ASM_CASES_TAC` x' = (y:real^3) `; DOWN THEN SIMP_TAC[]; REPLICATE_TAC 6 DOWN THEN PHA; NHANH ( MESON[SET2_DETER]` x' IN s /\ y IN s /\ f x' = f y /\ v IN V /\ s = {v, rho_node1 FF v} /\ ~(x' = y) ==> s = {x', y} `); STRIP_TAC; SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC; DOWN; ASM_REWRITE_TAC[IMAGE_CLAUSES]; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC `v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `; REWRITE_TAC[FAN; fan6]; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `)); DOWN; UNDISCH_TAC` s = {x', y:real^3} `; SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY]; ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2]; NHANH ORD_PAIRS_INJ_IMAGE; REWRITE_TAC[GSYM ord_pairs]; SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC; REWRITE_TAC[EXTENSION; IN_IMAGE]; GEN_TAC; EQ_TAC; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `)); EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; DOWN THEN DOWN; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; REPEAT STRIP_TAC; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; REPLICATE_TAC 4 DOWN THEN PHA; CONV_TAC SET_RULE; EXPAND_TAC "E'"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; EXISTS_TAC` {v, rho_node1 FF v }`; ASM_REWRITE_TAC[]; EXPAND_TAC "E"; DOWN THEN DOWN; CONV_TAC SET_RULE; SIMP_TAC[]; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC; REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM]; GEN_TAC; STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `)); PHA; EXPAND_TAC "E"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `; DISCH_THEN (SUBST1_TAC o SYM); SIMP_TAC[darts_of_hyp; UNION_EMPTY]; MP_TAC BIJ_AND_MAP_COMM; ANTS_TAC; ASM_REWRITE_TAC[BIJ]; MP_TAC NODE_EDGE_COMM_LEMMA; ANTS_TAC; ASM_REWRITE_TAC[BIJ]; ASM_REWRITE_TAC[]; SIMP_TAC[]; REPEAT STRIP_TAC; DOWN; NHANH (ISPEC `ff: real^3 # real^3 -> real^3 # real^3 ` FUN_IN_IMAGE); STRIP_TAC; ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2]; UNDISCH_TAC` x' IN FF UNION {v,w | w:real^3,v IN FF} `; REWRITE_TAC[IN_ELIM_THM]; SUBGOAL_THEN` x' IN FF UNION {v:real^3,w | w,v IN FF} ==> ? a b. x' = (a,b) ` MP_TAC; EXPAND_TAC "FF"; REWRITE_TAC[IN_UNION; IN_ELIM_THM]; MESON_TAC[]; DISCH_THEN NHANH; STRIP_TAC; DOWN; SIMP_TAC[]; EXPAND_TAC "ff"; SIMP_TAC[]]);; let POWER_COMM = REWRITE_RULE[IN_UNIV] (SPEC` (:A) ` Hypermap_iso.power_comm);; let ITER_COMM = REWRITE_RULE[Wrgcvdr_cizmrrh.POWER_TO_ITER] POWER_COMM;;
let IMAGE_FACE_F = 
prove_by_refinement( ` hyp_iso (f: A -> B) (H,HH) ==> ! x . x IN dart H ==> IMAGE f (face H x ) = face HH ( f x ) `,
[REWRITE_TAC[hyp_iso]; STRIP_TAC THEN GEN_TAC THEN STRIP_TAC; REWRITE_TAC[EXTENSION; face; orbit_map; IN_ELIM_THM]; SUBGOAL_THEN`! x n. x IN dart H ==> (face_map HH POWER n) ((f:A -> B) x) = f ((face_map H POWER n) (x)) ` ASSUME_TAC; ONCE_REWRITE_TAC[EQ_SYM_EQ]; MATCH_MP_TAC ( REWRITE_RULE[TAUT` a ==> b ==> c <=> a /\ b ==> c `] Hypermap_iso.power_comm); ASM_SIMP_TAC[Hypermap.lemma_dart_invariant]; ASM_SIMP_TAC[IN_IMAGE; IN_ELIM_THM]; MESON_TAC[]]);;
let COMM_BIJ_HAS_SAME_ORDS = 
prove_by_refinement(`BIJ f (:A) (:B) /\ (! x. (f o h) x = (g o (f: A -> B)) x ) /\ has_orders h k ==> has_orders g k`,
[REWRITE_TAC[has_orders]; REPEAT STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` i: num `)); DOWN; PHA; REWRITE_TAC[FUN_EQ_THM]; GEN_TAC; UNDISCH_TAC` BIJ f (:A) (:B) `; REWRITE_TAC[BIJ; INJ]; STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; REWRITE_TAC[IN_UNIV]; UNDISCH_TAC` !x. (f o h) x = (g o (f:A -> B)) x `; REWRITE_TAC[o_THM]; NHANH ITER_COMM; SIMP_TAC[]; STRIP_TAC; ASM_REWRITE_TAC[I_THM]; DOWN_TAC; REWRITE_TAC[o_THM]; NHANH ITER_COMM; STRIP_TAC; SIMP_TAC[FUN_EQ_THM]; UNDISCH_TAC` BIJ f (:A) (:B) `; REWRITE_TAC[BIJ; INJ; SURJ]; STRIP_TAC; GEN_TAC; SUBGOAL_THEN` x IN (:B) ` MP_TAC; REWRITE_TAC[IN_UNIV]; FIRST_X_ASSUM NHANH; STRIP_TAC; EXPAND_TAC "x";
UNDISCH_TAC` !x n. f (ITER n h x) = ITER n g ((f: A -> B) x) `; ONCE_REWRITE_TAC[EQ_SYM_EQ]; SIMP_TAC[]; STRIP_TAC; ASM_REWRITE_TAC[I_THM]]);;
let DIH2K_HYP_ISO_LEMMA = 
prove_by_refinement (` BIJ f (:A) (:B) /\ FINITE (dart (H: (A) hypermap) ) /\ dih2k H k /\ hyp_iso (f: A -> B) (H, HH) ==> dih2k HH k `,
[NHANH IMAGE_FACE_F; REWRITE_TAC[dih2k; hyp_iso]; STRIP_TAC; CONJ_TAC; SUBGOAL_THEN` CARD (dart (H: (A) hypermap )) = CARD (dart (HH:(B) hypermap)) ` MP_TAC; MATCH_MP_TAC (Local_lemmas.BIJ_IMP_CARD_EQ); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; SIMP_TAC[]; CONJ_TAC; GEN_TAC; LET_TAC; STRIP_TAC; UNDISCH_TAC` BIJ (f: A -> B) (dart H) (dart HH) `; NHANH Add_triangle.BIJ_IMAGE; REWRITE_TAC[BIJ; SURJ]; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` x: B `)); DOWN THEN STRIP_TAC; SUBGOAL_THEN` (let S = face (H: (A) hypermap) y in dart H = S UNION IMAGE (node_map H) S) ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; LET_TAC; SUBGOAL_THEN` IMAGE f (face H (y:A)) = face HH ((f: A -> B) (y:A)) ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM ACCEPT_TAC; ASM_REWRITE_TAC[]; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[GSYM IMAGE_o]; UNDISCH_TAC` (y:A) IN dart H ` ; NHANH Hypermap.lemma_face_subset; STRIP_TAC; SUBGOAL_THEN` IMAGE (node_map HH o (f: A -> B)) S' = IMAGE (f o (node_map H )) S' ` ASSUME_TAC; MATCH_MP_TAC Lvducxu.IDE_ON_S_IMP_SAME_IMAGE; GEN_TAC THEN DOWN; ASM_SIMP_TAC[SUBSET]; DISCH_THEN NHANH; ASM_SIMP_TAC[o_THM]; ASM_REWRITE_TAC[]; REWRITE_TAC[IMAGE_o; GSYM IMAGE_UNION]; SIMP_TAC[]; SUBGOAL_THEN`!x. (x:A) IN dart H <=> ((f x): B) IN dart HH ` ASSUME_TAC; UNDISCH_TAC` BIJ (f: A -> B) (dart H ) (dart HH ) ` ; UNDISCH_TAC ` BIJ f (:A) (:B) ` ; REWRITE_TAC[BIJ; INJ; SURJ]; STRIP_TAC THEN STRIP_TAC; GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM NHANH; STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPECL [` y: A `;` x: A `])); FIRST_X_ASSUM (MP_TAC o (SPECL [` y: A `;` x: A `])); ANTS_TAC; ASM_REWRITE_TAC[IN_UNIV]; ASM_SIMP_TAC[]; DISCH_THEN SUBST_ALL_TAC; FIRST_ASSUM ACCEPT_TAC; CONJ_TAC; MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS); EXISTS_TAC` f: A -> B `; EXISTS_TAC` face_map (H: (A) hypermap)`; ASM_REWRITE_TAC[]; GEN_TAC; ASM_CASES_TAC` (x:A) IN dart H `; ASM_SIMP_TAC[o_THM]; DOWN; NHANH Lvducxu.NOT_IN_DART_IMP_IDE; ASM_REWRITE_TAC[]; NHANH Lvducxu.NOT_IN_DART_IMP_IDE; SIMP_TAC[o_THM]; CONJ_TAC; MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS); EXISTS_TAC` f: A -> B `; EXISTS_TAC` edge_map (H: (A) hypermap)`; ASM_REWRITE_TAC[]; GEN_TAC; ASM_CASES_TAC` (x:A) IN dart H `; ASM_SIMP_TAC[o_THM]; DOWN; NHANH Lvducxu.NOT_IN_DART_IMP_IDE; ASM_REWRITE_TAC[]; NHANH Lvducxu.NOT_IN_DART_IMP_IDE; SIMP_TAC[o_THM]; MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS); EXISTS_TAC` f: A -> B `; EXISTS_TAC` node_map (H: (A) hypermap)`; ASM_REWRITE_TAC[]; GEN_TAC; ASM_CASES_TAC` (x:A) IN dart H `; ASM_SIMP_TAC[o_THM]; DOWN; NHANH Lvducxu.NOT_IN_DART_IMP_IDE; ASM_REWRITE_TAC[]; NHANH Lvducxu.NOT_IN_DART_IMP_IDE; SIMP_TAC[o_THM]]);;
let AUTOMAP_IMP_ALL_ITER_IN2 = MESON[IN; Trigonometry2.AUTOMAP_IMP_ALL_ITER_IN] ` p IN W /\ (!x. x IN W ==> f x IN W) ==> ITER N f p IN W `;;
let ITER_COMM_RESTRICTED = 
prove_by_refinement(` (!(x:A). x IN V ==> f x IN V') /\ (!x. h x IN V <=> x IN V) /\ (!(y:B). g y IN V' <=> y IN V') /\ (!x. x IN V ==> f (h x) = g (f x)) ==> ! x. x IN V ==> f (ITER n h x) = ITER n g ( f x ) `,
[ STRIP_TAC; SPEC_TAC (`n:num `,`n:num `); INDUCT_TAC; REWRITE_TAC[ITER]; GEN_TAC THEN STRIP_TAC; REWRITE_TAC[ITER]; SUBGOAL_THEN` ITER n h (x:A) IN V ` ASSUME_TAC; MATCH_MP_TAC AUTOMAP_IMP_ALL_ITER_IN2; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x:A `)); FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` ITER n h (x:A) `)); ASM_REWRITE_TAC[]]);;
let HAS_THE_SAME_ORD_LEM = 
prove_by_refinement(` (! x. ~( x IN V ) ==> h x = x ) /\ (! y. ~( y IN V') ==> g y = y ) /\ BIJ (f: A -> B) V V' /\ (! x. (h x IN V) <=> x IN V ) /\ (! y. (g y IN V') <=> y IN V' ) /\ (!x. x IN V ==> (f (h x )) = (g (f x ))) /\ has_orders h k ==> has_orders g k `,
[REWRITE_TAC[BIJ; INJ; SURJ; has_orders]; REPEAT STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` i:num `)); DOWN; PHA; REWRITE_TAC[FUN_EQ_THM]; GEN_TAC; ASM_CASES_TAC` (x:A) IN V `; UNDISCH_TAC` !x y. x IN V /\ y IN V /\ (f: A -> B) x = f y ==> x = y ` ; DISCH_THEN MATCH_MP_TAC; ASM_REWRITE_TAC[I_THM]; CONJ_TAC; MATCH_MP_TAC AUTOMAP_IMP_ALL_ITER_IN2; ASM_REWRITE_TAC[]; MP_TAC (SPEC `i:num ` (GEN `n:num ` ITER_COMM_RESTRICTED)); ANTS_TAC; ASM_REWRITE_TAC[]; DISCH_THEN (ASSUME_TAC2 o (SPEC` x: A `)); ASM_REWRITE_TAC[I_THM]; REWRITE_TAC[I_THM]; MATCH_MP_TAC ITER_FIXPOINT; DOWN; ASM_REWRITE_TAC[]; REWRITE_TAC[FUN_EQ_THM; I_THM]; GEN_TAC; ASM_CASES_TAC` x IN (V': B -> bool) `; DOWN; UNDISCH_TAC` !x. x IN V' ==> (?y. y IN V /\ (f: A -> B) y = x) `; DISCH_THEN NHANH; STRIP_TAC; MP_TAC (let tt = GEN` n: num ` ITER_COMM_RESTRICTED in SPEC` k: num ` tt); ANTS_TAC; ASM_REWRITE_TAC[]; DISCH_THEN (ASSUME_TAC2 o (SPEC` y: A `)); DOWN; ASM_REWRITE_TAC[I_THM]; MESON_TAC[]; MATCH_MP_TAC ITER_FIXPOINT; ASM_SIMP_TAC[]]);;
let COMM_THEN_IMAGE_IMAGE_EQ = SET_RULE ` (! x. x IN S ==> f ( g x ) = h ( f x )) /\ A SUBSET S ==> IMAGE f ( IMAGE g A ) = IMAGE h ( IMAGE f A ) `;;
let IN_DART_PRESERVED = 
prove(` (!x: A. face_map H x IN dart H <=> x IN dart H) /\ (!x: A. node_map H x IN dart H <=> x IN dart H) /\ (!x: A. edge_map H x IN dart H <=> x IN dart H)`,
MESON_TAC [Hypermap_iso.h_map_outside; Hypermap.lemma_dart_invariant]);;
let HYP_ISO_DIH2K_PRESERVED = 
prove_by_refinement (`FINITE (dart H) /\ dih2k H k /\ hyp_iso (f: A -> B) (H,HH) ==> dih2k HH k `,
[NHANH Hypermap_iso.iso_components; REWRITE_TAC[dih2k; hyp_iso]; STRIP_TAC; CONJ_TAC; ASSUME_TAC2 ( let tt = GEN_ALL Local_lemmas.BIJ_IMP_CARD_EQ in ISPECL [` f: A -> B `;` dart (H: (A) hypermap) `;` dart (HH: (B) hypermap) `] tt); DOWN; ASM_SIMP_TAC[]; CONJ_TAC; GEN_TAC THEN STRIP_TAC; DOWN; UNDISCH_TAC ` BIJ (f: A -> B) ( dart H ) ( dart HH ) `; REWRITE_TAC[BIJ; SURJ]; STRIP_TAC; FIRST_ASSUM NHANH; STRIP_TAC; LET_TAC; SUBGOAL_THEN` (let S = face H (y:A) in dart H = S UNION IMAGE (node_map H) S) ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; LET_TAC; SUBGOAL_THEN` node HH (f y) = IMAGE f (node H y) /\ face HH (f y) = IMAGE f (face H y) /\ edge HH ((f: A -> B) y) = IMAGE f (edge H y) ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; ASM_REWRITE_TAC[]; SIMP_TAC[]; PHA THEN STRIP_TAC; SUBGOAL_THEN` IMAGE (f: A -> B) (IMAGE (node_map H) S') = IMAGE (node_map HH) (IMAGE f S') ` ASSUME_TAC; MATCH_MP_TAC (GEN_ALL COMM_THEN_IMAGE_IMAGE_EQ); EXISTS_TAC` dart (H: (A) hypermap ) `; UNDISCH_TAC` !x. x IN dart H ==> edge_map HH ((f: A -> B) x) = f (edge_map H x) /\ node_map HH (f x) = f (node_map H x) /\ face_map HH (f x) = f (face_map H x) `; SIMP_TAC[]; STRIP_TAC; EXPAND_TAC "S'";
MATCH_MP_TAC Hypermap.lemma_face_subset; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (SUBST1_TAC o SYM); REWRITE_TAC[GSYM IMAGE_UNION]; SUBGOAL_THEN` BIJ (f: A -> B) (dart H ) (dart HH ) ` MP_TAC; ASM_REWRITE_TAC[BIJ; SURJ]; NHANH Add_triangle.BIJ_IMAGE; SIMP_TAC[]; ASM_REWRITE_TAC[]; ASSUME_TAC Hypermap_iso.h_map_outside; CONJ_TAC; MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM); EXISTS_TAC` dart (HH: (B) hypermap) `; EXISTS_TAC` dart (H: (A) hypermap) `; EXISTS_TAC` f: A -> B `; EXISTS_TAC` face_map (H: (A) hypermap ) `; ASM_REWRITE_TAC[]; DOWN THEN SIMP_TAC[]; DISCH_THEN NHANH; NHANH ( ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside); SIMP_TAC[IN_DART_PRESERVED]; ASM_SIMP_TAC[]; CONJ_TAC; MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM); EXISTS_TAC` dart (HH: (B) hypermap) `; EXISTS_TAC` dart (H: (A) hypermap) `; EXISTS_TAC` f: A -> B `; EXISTS_TAC` edge_map (H: (A) hypermap ) `; ASM_REWRITE_TAC[]; DOWN THEN SIMP_TAC[]; DISCH_THEN NHANH; NHANH ( ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside); SIMP_TAC[IN_DART_PRESERVED]; ASM_SIMP_TAC[]; MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM); EXISTS_TAC` dart (HH: (B) hypermap) `; EXISTS_TAC` dart (H: (A) hypermap) `; EXISTS_TAC` f: A -> B `; EXISTS_TAC` node_map (H: (A) hypermap ) `; ASM_REWRITE_TAC[]; DOWN THEN SIMP_TAC[]; DISCH_THEN NHANH; NHANH ( ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside); SIMP_TAC[IN_DART_PRESERVED]; ASM_SIMP_TAC[]]);;
let CONT_ATREAL_INJ_PRESERVED = 
prove_by_refinement( ` FINITE V /\ (!v. v IN V ==> (ff: real^N -> real -> real^M) v continuous atreal r) /\ INJ (\v. ff v r ) V (IMAGE (\v. ff v r ) V ) ==> ? e. &0 < e /\ (! t. abs ( t - r) < e ==> INJ (\v. ff v t ) V (IMAGE (\v. ff v t ) V )) `,
[REWRITE_TAC[INJ]; STRIP_TAC; MP_TAC (SPEC_ALL Local_lemmas1.CONTINUOUS_ATREAL_INJ_PRESERVED); ANTS_TAC; ASM_REWRITE_TAC[]; ANTS_TAC; ASM_REWRITE_TAC[]; DOWN; MESON_TAC[]; STRIP_TAC; EXISTS_TAC` d : real `; ASM_REWRITE_TAC[]; GEN_TAC; FIRST_X_ASSUM NHANH; REWRITE_TAC[IN_IMAGE]; MESON_TAC[]]);;
let INJ_BIJ_IMAGE = 
prove(` INJ f S S' /\ A SUBSET S ==> BIJ f A (IMAGE f A) `,
REWRITE_TAC[BIJ; INJ; SURJ] THEN CONV_TAC SET_RULE);;
let XRECQNS_UPDATE = 
prove_by_refinement(` deformation f V (a,b) /\ local_fan (V,E,FF) ==> (?e. &0 < e /\ (!t. abs t < e ==> local_fan (IMAGE (\v. f v t) V, IMAGE (\s. IMAGE (\v. f v t) s ) E , IMAGE (\(u,v). (f u t, f v t )) FF) )) `,
[NHANH_PAT `\x. x ==> y ` Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN; STRIP_TAC; ASSUME_TAC2 Deformation.XRECQNS; DOWN THEN PHA; REWRITE_TAC[REAL_BOUNDS_LT]; STRIP_TAC; DOWN_TAC; REWRITE_TAC[deformation]; STRIP_TAC; UNDISCH_TAC` FAN (vec 0, V:real^3 -> bool, E ) `; REWRITE_TAC[FAN; fan1; fan2]; STRIP_TAC; SUBGOAL_THEN` FINITE V /\ (!v. v IN V ==> (f: real^3 -> real -> real^3) v continuous atreal (&0)) /\ INJ (\v. f v (&0)) V (IMAGE (\v. f v (&0)) V) ` MP_TAC; ASM_REWRITE_TAC[]; CONJ_TAC; GEN_TAC THEN STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPECL [` v:real^3 `;` &0 `])); DOWN THEN SIMP_TAC[]; UNDISCH_TAC` !v. v IN V ==> f v (&0) = v:real^3 `; REWRITE_TAC[INJ; IN_IMAGE]; MESON_TAC[]; NHANH ( ISPECL [` f: real^3 -> real -> real^3 `;` &0 `] ( GENL [` ff: real^N -> real -> real^M `;` r: real `] CONT_ATREAL_INJ_PRESERVED)); STRIP_TAC; DOWN THEN REWRITE_TAC[REAL_ARITH` a - &0 = a `]; STRIP_TAC; EXISTS_TAC ` min e e' `; ASM_REWRITE_TAC[REAL_LT_MIN]; FIRST_ASSUM NHANH; SUBGOAL_THEN` ! f s. INJ (f:real^3 -> real^3) s (IMAGE f s) <=> BIJ f s (IMAGE f s ) ` ASSUME_TAC; REWRITE_TAC[BIJ; SURJ; IN_IMAGE]; MESON_TAC[]; ASM_REWRITE_TAC[]; GEN_TAC THEN STRIP_TAC; ABBREV_TAC` V' = IMAGE (\v. (f:real^3 -> real -> real^3) v t) V `; ABBREV_TAC` E' = IMAGE (\s. IMAGE (\v. (f: real^3 -> real -> real^3) v t) s) E `; ABBREV_TAC` ff = (\(x,y). (f:real^3 -> real -> real^3) x t, f y t) `; MP_TAC (SPEC` (\v. (f:real^3 -> real -> real^3) v t ) ` ( GEN ` f: real^3 -> real^3 ` HYP_ISO_LEMMAA)); ANTS_TAC; ASM_REWRITE_TAC[]; SUBGOAL_THEN` FAN (vec 0,IMAGE (\v. (f: real^3 -> real -> real^3) v t) V,IMAGE (IMAGE (\v. f v t)) E) ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "V'";
EXPAND_TAC "E'"; SIMP_TAC[ETA_AX]; SUBGOAL_THEN` FAN (vec 0,IMAGE (\v. (f: real^3 -> real -> real^3) v t) V,IMAGE (IMAGE (\v. f v t)) E) ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; DOWN THEN DOWN THEN DOWN; SIMP_TAC[ETA_AX; local_fan]; REPEAT STRIP_TAC; LET_TAC; UNDISCH_TAC` local_fan (V,E,FF) `; REWRITE_TAC[local_fan]; LET_TAC; STRIP_TAC; UNDISCH_TAC` hyp_iso (ff: real^3 # real^3 -> real^3 # real^3) (H',H) `; NHANH IMAGE_FACE_F; STRIP_TAC; CONJ_TAC; EXISTS_TAC ` (ff: real^3 # real^3 -> real^3 # real^3) x `; DOWN THEN DOWN; REWRITE_TAC[hyp_iso; BIJ; INJ]; ASM_SIMP_TAC[]; MATCH_MP_TAC ( let tt = GEN_ALL HYP_ISO_DIH2K_PRESERVED in ISPECL [` (ff: real^3 # real^3 -> real^3 # real^3 ) `;` H': (real^3 #real^3) hypermap `; ` H: (real^3 #real^3) hypermap `; ` k: num `] tt); ASM_REWRITE_TAC[]; ASSUME_TAC2 (ISPEC` vec 0: real^3 ` ( GEN` x: real^N ` Wrgcvdr_cizmrrh.FAN_IMP_FIMITE_DARTS)); UNDISCH_TAC` FAN (vec 0, V:real^3 -> bool , E ) `; NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP; ASM_SIMP_TAC[]; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x: real^3 # real^3 `)); FIRST_X_ASSUM (SUBST1_TAC o SYM); UNDISCH_TAC` (x: real^3 # real^3) IN dart H' `; NHANH Hypermap.lemma_face_subset; STRIP_TAC; SUBGOAL_THEN` FINITE (face H' (x:real^3 # real^3 )) ` MP_TAC; REWRITE_TAC[Hypermap.FACE_FINITE]; UNDISCH_TAC` hyp_iso (ff: real^3 # real^3 -> real^3 # real^3 ) (H', H) `; REWRITE_TAC[hyp_iso; BIJ]; NHANH INJ_IMP_BIJ_IMAGE; STRIP_TAC; STRIP_TAC; UNDISCH_TAC` face H' (x: real^3 # real^3) SUBSET dart H' `; UNDISCH_TAC` INJ (ff: real^3 # real^3 -> real^3 # real^3 ) (dart H') (dart H) `; PHA; NHANH INJ_BIJ_IMAGE; STRIP_TAC; DOWN; UNDISCH_TAC` FINITE (face H' (x: real^3 # real^3)) `; PHA; NHANH Misc_defs_and_lemmas.BIJ_CARD; STRIP_TAC; FIRST_X_ASSUM (SUBST1_TAC o SYM); UNDISCH_TAC` dih2k (H': (real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) `; ASM_REWRITE_TAC[]]);;
let NORM_CROSS_LE = 
prove_by_refinement(` norm ( u cross v) <= norm u * norm v `,
[MP_TAC (SPEC_ALL Trigonometry1.cross_mag); SIMP_TAC[]; MP_TAC SIN_BOUNDS; ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `]; REWRITE_TAC[REAL_ARITH` a * b - a * b * c = a * b * ( &1 - c ) `]; MP_TAC NORM_POS_LE; REPEAT STRIP_TAC; ASM_MESON_TAC[REAL_LE_MUL; NORM_POS_LE]]);;
let CONT_ATREAL_REAL_CONTS = 
prove_by_refinement (` f continuous atreal r ==> (\r. ((f r) cross y ) dot ( x cross y)) real_continuous atreal r `,
[REWRITE_TAC[real_continuous_atreal; continuous_atreal]; REPEAT STRIP_TAC; REWRITE_TAC[GSYM DOT_LSUB]; REWRITE_TAC[VEC3_RULE` x cross y - z cross y = ( x - z) cross y `]; ASM_CASES_TAC` (y:real^3) = vec 0 `; ASM_REWRITE_TAC[CROSS_RZERO; DOT_RZERO; REAL_ABS_0]; EXISTS_TAC` e: real `; ASM_REWRITE_TAC[]; ASM_CASES_TAC` (x:real^3) = vec 0 `; ASM_REWRITE_TAC[CROSS_LZERO; DOT_RZERO; REAL_ABS_0]; EXISTS_TAC` e:real `; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (MP_TAC o (SPEC` e / (norm (x:real^3) * norm (y:real^3) * norm (y:real^3) ) `)); ANTS_TAC; MATCH_MP_TAC REAL_LT_DIV; ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LT_MUL; ASM_REWRITE_TAC[NORM_POS_LT]; MATCH_MP_TAC REAL_LT_MUL; ASM_REWRITE_TAC[NORM_POS_LT]; STRIP_TAC; EXISTS_TAC` d:real `; FIRST_X_ASSUM NHANH; ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; MP_TAC (ISPECL [` ( f (x': real) - f r ) cross y `;` x cross y `] NORM_CAUCHY_SCHWARZ_ABS); ASSUME_TAC (SPECL [` (f:real -> real^3) x' - f r `;` y: real^3 `] (GEN_ALL NORM_CROSS_LE)); MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `); SUBGOAL_THEN` norm ((f (x':real) - f r) cross y) * norm (x cross y) <= (norm ( f x' - f r) * norm y ) * norm (x cross y ) ` ASSUME_TAC; MATCH_MP_TAC REAL_LE_RMUL; ASM_REWRITE_TAC[NORM_POS_LE]; DOWN; MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `); MP_TAC ( SPECL [` x:real^3 `;` y: real^3 `] (GEN_ALL NORM_CROSS_LE)); STRIP_TAC; SUBGOAL_THEN` &0 <= norm ((f: real -> real^3) x' - f r) * norm (y:real^3) ` ASSUME_TAC; MATCH_MP_TAC REAL_LE_MUL; REWRITE_TAC[NORM_POS_LE]; UNDISCH_TAC` norm (x cross y) <= norm x * norm y `; DOWN THEN PHA; NHANH Real_ext.REAL_LE_RMUL_IMP; DOWN THEN DOWN; REWRITE_TAC[dist]; REPEAT STRIP_TAC; ONCE_REWRITE_TAC[REAL_MUL_SYM]; DOWN; MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `); SUBGOAL_THEN ` &0 < norm (x:real^3) /\ &0 < norm (y:real^3) ` MP_TAC; ASM_REWRITE_TAC[NORM_POS_LT]; STRIP_TAC; ONCE_REWRITE_TAC[REAL_ARITH` (x * y ) * a * y = a * x * y * y `]; SUBGOAL_THEN` &0 < norm (x:real^3) * norm y * norm (y:real^3) ` MP_TAC; DOWN THEN DOWN; MESON_TAC[REAL_LT_MUL]; UNDISCH_TAC` norm ((f:real -> real^3) x' - f r) < e / (norm (x:real^3) * norm y * norm (y:real^3)) `; PHA; NHANH REAL_LT_RMUL; STRIP_TAC THEN DOWN; ASM_SIMP_TAC[REAL_FIELD` &0 < a ==> e / a * a = e `]]);;
let CONTINUOUS_POS_PRES = 
prove_by_refinement ( ` ~ collinear {(x:real^3),y, vec 0} /\ f r = a % x + b % y /\ &0 < a /\ f continuous atreal r ==> ? e. &0 < e /\ ! t. abs t < e ==> ! t1 t2. f ( r + t ) = t1 % x + t2 % y ==> &0 < t1 `,
[NHANH CONT_ATREAL_REAL_CONTS; REWRITE_TAC[real_continuous_atreal]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPEC` a * norm ( x cross y ) * norm ( x cross y ) `)); ANTS_TAC; MATCH_MP_TAC REAL_LT_MUL; ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LT_MUL; REWRITE_TAC[TAUT` a /\ a <=> a `]; REWRITE_TAC[NORM_POS_LT; CROSS_EQ_0]; UNDISCH_TAC` ~collinear {x, y:real^3, vec 0} `; SIMP_TAC[INSERT_COMM]; STRIP_TAC; EXISTS_TAC` d: real `; ASM_REWRITE_TAC[] ; GEN_TAC; REPEAT STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPEC` r + (t:real) `)); ANTS_TAC; ASM_REWRITE_TAC[REAL_ARITH` (a + b) - a = b `]; ASM_REWRITE_TAC[GSYM DOT_LSUB; VEC3_RULE` x cross z - y cross z = ( x - y) cross z `]; REWRITE_TAC[VECTOR_ARITH` (t1 % x + t2 % y) - (a % x + b % y) = ( t1 - a ) % x + ( t2 - b ) % y `; CROSS_LADD; CROSS_LMUL; CROSS_REFL]; REWRITE_TAC[VECTOR_ARITH` x + a % vec 0 = x `; DOT_LMUL; REAL_ABS_MUL; DOT_SQUARE_NORM]; SUBGOAL_THEN` &0 <= norm (x cross y) pow 2 ` MP_TAC; REWRITE_TAC[REAL_LE_POW_2]; REWRITE_TAC[GSYM REAL_ABS_REFL]; SIMP_TAC[REAL_POW_2]; REWRITE_TAC[REAL_ABS_REFL]; REWRITE_TAC[REAL_ARITH` &0 <= a <=> a = &0 \/ &0 < a `]; STRIP_TAC; ASM_SIMP_TAC[]; REAL_ARITH_TAC; ASM_SIMP_TAC[REAL_LT_RMUL_EQ]; UNDISCH_TAC` &0 < a `; REAL_ARITH_TAC]);;
let IVS_RHO_NODE_V_IN_FF = 
prove_by_refinement(` local_fan (V,E,FF) /\ v IN V ==> ivs_rho_node1 FF v, v IN FF `,
[NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2; STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC`ivs_rho_node1 FF v `)); ANTS_TAC; MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V; ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS; ASM_REWRITE_TAC[]]);;
let IN_AFF_GT_IMP_AZIMEQ = 
prove_by_refinement( ` x IN aff_gt {u,v} {y} ==> azim u v w x = azim u v w y `,
[ ASM_CASES_TAC` collinear {u,v,w:real^3} `; ASM_SIMP_TAC[AZIM_DEGENERATE]; ASM_CASES_TAC` collinear {u,v,y:real^3} `; ASM_SIMP_TAC[AZIM_DEGENERATE]; DOWN_TAC; NHANH Fan.th3b; STRIP_TAC; DOWN THEN DOWN; ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL]; MP_TAC (ISPECL [` {u, v:real^3} `;` {y:real^3} `] AFF_GT_SUBSET_AFFINE_HULL); REWRITE_TAC[SUBSET]; DISCH_THEN NHANH; REPEAT STRIP_TAC; SUBGOAL_THEN` affine hull ({u, v:real^3} UNION {y}) = affine hull {u,v} ` ASSUME_TAC; MATCH_MP_TAC AFFINE_HULLS_EQ; REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {c,a,b} `]; CONJ_TAC; ONCE_REWRITE_TAC[INSERT_SUBSET]; ASM_REWRITE_TAC[]; REWRITE_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL]; MP_TAC (SPEC` {u,v:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL); MATCH_MP_TAC (SET_RULE` a SUBSET b ==> c SUBSET a ==> c SUBSET b `); MATCH_MP_TAC HULL_MONO; CONV_TAC SET_RULE; FIRST_X_ASSUM SUBST_ALL_TAC; DOWN; ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL; AZIM_DEGENERATE]; DOWN_TAC; REWRITE_TAC[AZIM_EQ_IMP]]);;
let IN_AFF_GT_IMP_AZIMEQ2 = MESON[IN_AFF_GT_IMP_AZIMEQ]` x IN aff_gt {u, v} {y} ==> ! w. azim u v w x = azim u v w y `;;
let NOT_COLL_IMP_ZERO_DETER = 
prove_by_refinement(` ~ collinear {vec 0, u, v } ==> (! a b. a % u + b % v = vec 0 <=> a = &0 /\ b = &0) `,
[REWRITE_TAC[Local_lemmas1.COLL_EQ_DEPENDENT]; STRIP_TAC; GEN_TAC THEN GEN_TAC; EQ_TAC; DOWN; MESON_TAC[]; SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]]);;
let CROSS_IN_SAME_DIRECTION = 
prove_by_refinement (` local_fan (V,E,FF) /\ v IN V /\ {ITER n (rho_node1 FF) v | n <= l} = U /\ plane P /\ vec 0 IN P /\ U SUBSET P /\ v cross rho_node1 FF v = e ==> (!i. i < l ==> ? k. &0 < k /\ ITER i (rho_node1 FF) v cross ITER ( i + 1) (rho_node1 FF ) v = k % e ) `,
[NHANH Local_lemmas.RHO_NODE_SET_IN_A_PLANE_IMP_POS_DIRECT; ASM_CASES_TAC` l = 0 `; ASM_REWRITE_TAC[ARITH_RULE` ~( n < 0) `]; STRIP_TAC; SUBGOAL_THEN` {vec 0, v, rho_node1 FF v } SUBSET P ` ASSUME_TAC; ONCE_REWRITE_TAC[INSERT_SUBSET]; ASM_REWRITE_TAC[]; MATCH_MP_TAC SUBSET_TRANS; EXISTS_TAC` U: real^3 -> bool `; ASM_REWRITE_TAC[]; REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET]; EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; EXISTS_TAC` 0 `; REWRITE_TAC[ITER; ARITH_RULE` 0 <= l `]; EXISTS_TAC` 1 `; REWRITE_TAC[ITER1]; MATCH_MP_TAC (ARITH_RULE` ~( l = 0) ==> 1 <= l `); ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; DOWN THEN DOWN; PHA; UNDISCH_TAC` plane (P: real^3 -> bool) `; PHA; NHANH Local_lemmas.THREE_NOT_COLL_DETER_PLANE; STRIP_TAC; NHANH (ARITH_RULE` i < (l:num) ==> i <= l /\ i + 1 <= l `); GEN_TAC THEN STRIP_TAC; SUBGOAL_THEN` ITER i (rho_node1 FF) v IN U /\ ITER (i + 1) (rho_node1 FF) v IN U` ASSUME_TAC; EXPAND_TAC "U"; REWRITE_TAC[IN_ELIM_THM]; DOWN THEN DOWN; MESON_TAC[]; DOWN; UNDISCH_TAC` U SUBSET (P: real^3 -> bool) `; REWRITE_TAC[SUBSET]; DISCH_THEN NHANH ; EXPAND_TAC "P"; REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3]; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC ` i:num `)); DOWN; ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; CROSS_LADD; CROSS_RADD]; REWRITE_TAC[CROSS_LMUL; CROSS_RMUL; CROSS_REFL; VECTOR_MUL_LZERO; VECTOR_MUL_RZERO]; REWRITE_TAC[VECTOR_ADD_LID; VECTOR_ADD_RID]; ASM_REWRITE_TAC[VECTOR_MUL_ASSOC]; ONCE_REWRITE_TAC[CROSS_SKEW]; ASM_REWRITE_TAC[VECTOR_ARITH` (v' * w') % e + (w * v'') % --e = ((v' * w') - (w * v'')) % e `]; REWRITE_TAC[DOT_LMUL]; UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `; ASM_REWRITE_TAC[GSYM CROSS_EQ_0]; REWRITE_TAC[GSYM DOT_POS_LT]; SIMP_TAC[REAL_LT_MUL_EQ]; STRIP_TAC; MESON_TAC[]]);;
let ITER_CROSS_SAME_DIRECTION = 
prove_by_refinement (`local_fan (V,E,FF) /\ v IN V /\ {ITER n (rho_node1 FF) v | n <= l} = U /\ plane P /\ vec 0 IN P /\ U SUBSET P ==> (!i j. i < l /\ j < l ==> ? k. &0 < k /\ ITER i (rho_node1 FF) v cross ITER ( i + 1) (rho_node1 FF ) v = k % (ITER j (rho_node1 FF) v cross ITER ( j + 1) (rho_node1 FF ) v) ) `,
[STRIP_TAC; ABBREV_TAC ` e = v cross rho_node1 FF v `; ASSUME_TAC2 CROSS_IN_SAME_DIRECTION; FIRST_X_ASSUM NHANH; REPEAT STRIP_TAC; ASM_REWRITE_TAC[]; EXISTS_TAC` k / (k': real) `; CONJ_TAC; MATCH_MP_TAC REAL_LT_DIV; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[REAL_FIELD` &0 < a ==> x / a * a = x `; VECTOR_MUL_ASSOC]]);;
let ITER_IN_AFF_GT_2_1 = 
prove_by_refinement(` local_fan (V,E,FF) /\ v IN V /\ {ITER n (rho_node1 FF) v | n <= l} = U /\ plane P /\ vec 0 IN P /\ U SUBSET P ==> (! i. i < l - 1 ==> ITER ( i + 2) (rho_node1 FF) v IN aff_lt {vec 0, ITER (i + 1) (rho_node1 FF) v } {ITER i (rho_node1 FF ) v } ) `,
[STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE3; GEN_TAC; FIRST_X_ASSUM (ASSUME_TAC o (SPEC` i:num `)); STRIP_TAC; SUBGOAL_THEN` {vec 0, ITER i (rho_node1 FF) v, ITER ( i + 1) (rho_node1 FF) v} SUBSET P` ASSUME_TAC; ONCE_REWRITE_TAC[INSERT_SUBSET]; ASM_REWRITE_TAC[]; MATCH_MP_TAC SUBSET_TRANS; EXISTS_TAC` U: real^3 -> bool`; ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET]; EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; EXISTS_TAC` i:num `; ASM_REWRITE_TAC[]; DOWN; ARITH_TAC; EXISTS_TAC` i + 1 `; ASM_REWRITE_TAC[]; DOWN; ARITH_TAC; UNDISCH_TAC` ~collinear {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} `; UNDISCH_TAC` {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} SUBSET P `; UNDISCH_TAC` plane (P:real^3 -> bool) `; PHA; NHANH Local_lemmas.THREE_NOT_COLL_DETER_PLANE; STRIP_TAC; SUBGOAL_THEN` ITER (i + 2) (rho_node1 FF) v IN U ` MP_TAC; EXPAND_TAC "U"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` i + 2 `; REWRITE_TAC[]; UNDISCH_TAC` i < l - 1 `; ARITH_TAC; UNDISCH_TAC` (U:real^3 -> bool) SUBSET P `; REWRITE_TAC[SUBSET]; STRIP_TAC; FIRST_ASSUM NHANH; EXPAND_TAC "P"; REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3]; STRIP_TAC; MP_TAC ITER_CROSS_SAME_DIRECTION; ANTS_TAC; ASM_REWRITE_TAC[SUBSET]; DISCH_THEN (MP_TAC o (SPECL [` i + 1`;` i:num `])); ASSUME_TAC2 (ARITH_RULE` i < l - 1 ==> i + 1 < l `); ASSUME_TAC2 (ARITH_RULE` i < l - 1 ==> i < l `); ANTS_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[ARITH_RULE` (a + 1) + 1 = a + 2 `; VECTOR_MUL_RZERO; VECTOR_ADD_LID]; REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID]; STRIP_TAC; DOWN; ABBREV_TAC` e1 = ITER i (rho_node1 FF) v cross ITER (i + 1) (rho_node1 FF) v `; ONCE_REWRITE_TAC[CROSS_SKEW; VECTOR_ARITH` a % -- x = ( -- a ) % x `]; ASM_REWRITE_TAC[]; SUBGOAL_THEN` ~( e1:real^3 = vec 0) ` MP_TAC; EXPAND_TAC "e1"; REWRITE_TAC[CROSS_EQ_0]; ASM_REWRITE_TAC[]; SIMP_TAC[VECTOR_MUL_RCANCEL; VECTOR_ARITH` a % -- x = ( -- a ) % x `]; STRIP_TAC THEN STRIP_TAC; UNDISCH_TAC` ~collinear {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} `; ONCE_REWRITE_TAC[Collect_geom.PER_SET2]; NHANH Fan.th3a; NHANH AFF_LT_2_1; SIMP_TAC[Collect_geom.PER_SET2]; STRIP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC `u: real `; EXISTS_TAC` w: real `; EXISTS_TAC` v':real`; ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID]; CONJ_TAC; UNDISCH_TAC` --v' = (k: real) `; UNDISCH_TAC ` &0 < k `; REAL_ARITH_TAC; CONJ_TAC; UNDISCH_TAC` u + v' + w = &1 `; REAL_ARITH_TAC; CONV_TAC VECTOR_ARITH]);; (* search[` v cross rho_node1 FF v `];; *)
let AZIM_PI_ITER_LOCAL_FAN = 
prove_by_refinement (`local_fan (V,E,FF) /\ v IN V /\ {ITER n (rho_node1 FF) v | n <= l} = U /\ plane P /\ vec 0 IN P /\ U SUBSET P ==> (!i. i < l - 1 ==> azim (vec 0) (ITER (i + 1) (rho_node1 FF ) v ) (ITER (i) (rho_node1 FF ) v ) (ITER (i + 2) (rho_node1 FF ) v ) = pi ) `,
[NHANH ITER_IN_AFF_GT_2_1; STRIP_TAC; GEN_TAC; FIRST_X_ASSUM NHANH; STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE3; FIRST_ASSUM (MP_TAC o (SPEC` i: num `)); FIRST_ASSUM (MP_TAC o (SPEC` i + 1`)); STRIP_TAC; ONCE_REWRITE_TAC[Collect_geom.PER_SET2]; DOWN THEN DOWN; DOWN; REWRITE_TAC[ARITH_RULE` (a + 1) + 1 = a + 2 `]; MESON_TAC[AZIM_EQ_PI_ALT]]);;
let LOCAL_CONVEX_NOT_COLLINEAR = 
prove_by_refinement (`convex_local_fan (V,E,FF) /\ lunar (v,w) V E ==> (!u. u IN V /\ ~(u = v) /\ ~(u = w) ==> ~ collinear {vec 0, v, u}) `,
[NHANH LUNAR_IMP_IN_TWO_HAFLS_PLANE; REWRITE_TAC[lunar; INSERT_SUBSET]; NHANH Local_lemmas.CVX_LO_IMP_LO; STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS; FIRST_X_ASSUM NHANH; GEN_TAC; DOWN THEN DOWN; MESON_TAC[Planarity.aff_gt_imp_not_collinear]]);;
let LOCAL_CONVEX_NOT_COLLINEAR2 = 
prove(` convex_local_fan (V,E,FF) /\ lunar (v,w) V E ==> (!u. u IN V /\ ~(u = v) /\ ~(u = w) ==> ~collinear {vec 0, w, u})`,
ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM] THEN NHANH LOCAL_CONVEX_NOT_COLLINEAR THEN MESON_TAC[]);;
let LOCAL_FAN_RHO_NODE_PROS2 = 
prove(` local_fan (V,E,FF) ==> (!x. x IN V ==> x,rho_node1 FF x IN FF) `,
NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS THEN SIMP_TAC[]);;
(* ============================= -====================================== ================================ *)
let MHAEYJN_CONVEX_LOCAL_FAN = 
prove_by_refinement ( `!a b V E FF f v w u. convex_local_fan (V,E,FF) /\ lunar (v,w) V E /\ deformation f V (a,b) /\ interior_angle1 (vec 0) FF v < pi /\ u IN V /\ ~(u = v) /\ ~(u = w) /\ (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\ (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u}) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> convex_local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) ))`,
[REPEAT GEN_TAC; NHANH_PAT`\x. x ==> y ` Local_lemmas.CVX_LO_IMP_LO; NHANH_PAT`\x. x ==> y ` Local_lemmas.LOCAL_FAN_FINITE_V; NHANH Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN; REWRITE_TAC[FAN; UNIONS_SUBSET]; STRIP_TAC; MP_TAC SUB_LUNAR_DEFORM_LEMMA; ANTS_TAC; ASM_REWRITE_TAC[]; UNDISCH_TAC` deformation f (V:real^3 -> bool) (a,b) `; REWRITE_TAC[deformation; real_interval; IN_ELIM_THM]; ASM_SIMP_TAC[]; REWRITE_TAC[REAL_BOUNDS_LT]; STRIP_TAC; ASSUME_TAC2 XRECQNS_UPDATE; ASSUME_TAC2 HKIRPEP_ALT; DOWN THEN DOWN THEN STRIP_TAC; STRIP_TAC; SUBGOAL_THEN` ! x y. x IN V /\ y IN V /\ ~ collinear {vec 0, x, y} /\ (? a b . (f:real^3 -> real -> real^3) u (&0) = a % x + b % y /\ &0 < a ) ==> (?e. &0 < e /\ (!t. abs t < e ==> (!t1 t2. f u (t) = t1 % x + t2 % y ==> &0 < t1))) ` ASSUME_TAC; SUBGOAL_THEN` deformation (f:real^3 -> real -> real^3) V (a,b) ` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[deformation]; STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`u: real^3 `;` &0 `])); REPEAT GEN_TAC; ONCE_REWRITE_TAC[MESON[REAL_ARITH` t = &0 + t `]` f u t = A <=> f u ( &0 + t ) = A `]; MATCH_MP_TAC (GEN_ALL CONTINUOUS_POS_PRES); EXISTS_TAC` b': real `; EXISTS_TAC` a': real `; UNDISCH_TAC` ~ collinear {vec 0, x, y:real^3} `; ASM_REWRITE_TAC[INSERT_COMM]; ABBREV_TAC` ss = { (x,y) | x IN V /\ y IN V /\ ~collinear {vec 0, x, y} /\ (?a b. (f:real^3 -> real -> real^3) u (&0) = a % x + b % y /\ &0 < a) } ` ; SUBGOAL_THEN` ss SUBSET { (x,y) | x IN (V:real^3 -> bool) /\ y IN V} ` MP_TAC; EXPAND_TAC "ss";
CONV_TAC SET_RULE; STRIP_TAC; SUBGOAL_THEN` FINITE {x,y | x IN (V:real^3 -> bool) /\ y IN V} ` ASSUME_TAC; MATCH_MP_TAC FINITE_PRODUCT; ASM_REWRITE_TAC[]; UNDISCH_TAC` ss SUBSET {x,y | x IN V /\ (y:real^3) IN V} `; UNDISCH_TAC` FINITE {x,y | x IN V /\ y:real^3 IN V} `; PHA; NHANH FINITE_SUBSET; STRIP_TAC; SUBGOAL_THEN` (!x. (x:real^3 # real^3) IN ss ==> (?e. &0 < e /\ (!t. abs t < e ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % (FST x) + t2 % (SND x) ==> &0 < t1))))` MP_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; GEN_TAC; STRIP_TAC; ASM_SIMP_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; EXISTS_TAC` a': real `; EXISTS_TAC` b': real `; ASM_REWRITE_TAC[]; DOWN; PHA; NHANH Deformation.MINIMIZE_OVER_MEMBERS; STRIP_TAC; EXISTS_TAC` min b ( min (-- a) ( min e (min e' e''))) `; SUBGOAL_THEN` deformation f (V: real^3 -> bool) (a,b) ` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[deformation; real_interval; IN_ELIM_THM]; STRIP_TAC; REWRITE_TAC[REAL_LT_MIN]; CONJ_TAC; ASM_REWRITE_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `]; REWRITE_TAC[convex_local_fan]; GEN_TAC THEN STRIP_TAC; ABBREV_TAC` IV = IMAGE (\v. (f:real^3 -> real -> real^3) v t) V `; ABBREV_TAC` IE = IMAGE (IMAGE (\v. (f: real^3 -> real -> real^3) v t)) E`; ABBREV_TAC` IF = IMAGE (\uv. (f: real^3 -> real -> real^3) (FST uv) t,f (SND uv) t) FF `; SUBGOAL_THEN` local_fan (IV, IE , IF) ` MP_TAC; UNDISCH_TAC` !t. abs t < e' ==> local_fan (IMAGE (\v. f v t) V, IMAGE (\s. IMAGE (\v. f v t) s) E, IMAGE (\(u,v). (f: real^3 -> real -> real^3) u t,f v t) FF) `; DISCH_THEN (ASSUME_TAC2 o SPEC_ALL); DOWN; UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[ETA_AX]; SUBGOAL_THEN`! (fg: real^3 -> real^3). (\(u:real^3,v:real^3). fg u,fg v) = (\uv. fg (FST uv),fg (SND uv)) ` ASSUME_TAC; REWRITE_TAC[FUN_EQ_THM; BETA_THM]; GEN_TAC THEN GEN_TAC; PAT_ONCE_REWRITE_TAC`\x. f x = y ` [GSYM PAIR]; PURE_ONCE_REWRITE_TAC[BETA_THM]; ABBREV_TAC` x1 = FST (x:real^3 # real^3) `; ABBREV_TAC` x2 = SND (x:real^3 # real^3) `; REWRITE_TAC[BETA_THM]; ASM_REWRITE_TAC[]; SIMP_TAC[] THEN STRIP_TAC; GEN_TAC; UNDISCH_TAC` local_fan (IV, IE, IF) `; PHA; PAT_ONCE_REWRITE_TAC`\x. y /\ x ==> z ` [GSYM PAIR]; ABBREV_TAC` xx = FST (x:real^3 # real^3) `; NHANH Local_lemmas.LOCAL_FAN_IMP_IN_V; NHANH Local_lemmas.DETER_RHO_NODE; STRIP_TAC; ONCE_REWRITE_TAC[GSYM PAIR]; ABBREV_TAC` xy = SND (x:real^3 # real^3) `; UNDISCH_TAC` xx:real^3 IN IV `; UNDISCH_TAC` local_fan (IV,IE,IF) `; PHA; UNDISCH_TAC` rho_node1 IF xx = xy `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; NHANH Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND; NHANH Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND; SIMP_TAC[]; STRIP_TAC; ASSUME_TAC2 LOCAL_FAN_FACE_FF; SUBGOAL_THEN` lunar (v:real^3,w) V E ` MP_TAC; FIRST_ASSUM ACCEPT_TAC; REWRITE_TAC[lunar; INSERT_SUBSET]; STRIP_TAC; ASSUME_TAC2 Localization.LOFA_IMP_LT_CARD_SET_V_ALT; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `)); DOWN THEN STRIP_TAC; ASSUME_TAC2 (SPEC`u: real^3 ` Local_lemmas1.IVS_RHO_NODE_DIFF_ID); ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `)); SUBGOAL_THEN`! v:real^3. v IN V ==> ivs_rho_node1 FF (rho_node1 FF v) = v ` ASSUME_TAC; GEN_TAC; STRIP_TAC; MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD; ASM_REWRITE_TAC[]; SUBGOAL_THEN`!v. v IN V ==> rho_node1 FF (ivs_rho_node1 FF v) = v ` MP_TAC; GEN_TAC; STRIP_TAC; MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` ! v. v: real^3 IN V ==> rho_node1 FF v IN V ` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; ASM_SIMP_TAC[]; SUBGOAL_THEN` deformation f (V: real^3 -> bool) (a,b) ` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[deformation]; STRIP_TAC; SUBGOAL_THEN` t IN real_interval (a,b) ` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM; real_interval]; ASM_REWRITE_TAC[]; UNDISCH_TAC` abs t < b `; UNDISCH_TAC` abs t < -- a `; REAL_ARITH_TAC; ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V; SUBGOAL_THEN` (f:real^3 -> real -> real^3) (rho_node1 FF u) t = rho_node1 FF u ` ASSUME_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_SIMP_TAC[]; SUBGOAL_THEN` (f:real^3 -> real -> real^3) (rho_node1 FF (rho_node1 FF u)) t = rho_node1 FF (rho_node1 FF u )` ASSUME_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_SIMP_TAC[]; SUBGOAL_THEN` (f:real^3 -> real -> real^3) (ivs_rho_node1 FF u) t = ivs_rho_node1 FF u ` ASSUME_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_SIMP_TAC[]; ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS; DOWN THEN DISCH_THEN (ASSUME_TAC o GSYM); UNDISCH_TAC` xx: real^3 IN IV `; EXPAND_TAC "IV"; REWRITE_TAC[IN_IMAGE]; STRIP_TAC; SUBGOAL_THEN` ! (v:real^3). v IN V ==> (f:real^3 -> real -> real^3) v t, f (rho_node1 FF v) t IN IF ` ASSUME_TAC; EXPAND_TAC "IF"; REWRITE_TAC[IN_IMAGE]; EXPAND_TAC "FF"; REWRITE_TAC[IN_ELIM_THM]; GEN_TAC THEN STRIP_TAC; EXISTS_TAC` v', rho_node1 FF v' `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; EXISTS_TAC` v': real^3 `; ASM_REWRITE_TAC[]; SUBGOAL_THEN` ! (v:real^3). v IN V ==> rho_node1 IF ((f:real^3 -> real -> real^3) v t ) = f ( rho_node1 FF v ) t ` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v': real^3 `)); DOWN; UNDISCH_TAC` local_fan (IV, IE, IF) `; PHA; NHANH Local_lemmas.DETER_RHO_NODE; SIMP_TAC[]; SUBGOAL_THEN` ! (v:real^3). v IN V ==> ivs_rho_node1 IF ((f:real^3 -> real -> real^3) v t ) = f ( ivs_rho_node1 FF v ) t ` ASSUME_TAC; GEN_TAC THEN STRIP_TAC; SUBGOAL_THEN` f (ivs_rho_node1 FF v') t, (f:real^3 -> real -> real^3) v' t IN IF ` ASSUME_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v' `)); FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v' `)); ANTS_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; DOWN; UNDISCH_TAC` local_fan (IV, IE, IF) `; PHA; NHANH Local_lemmas.IVS_RHO_NODE1_DETE; SIMP_TAC[]; SUBGOAL_THEN` IV SUBSET (f:real^3 -> real -> real^3) u t INSERT V ` ASSUME_TAC; REWRITE_TAC[SUBSET]; EXPAND_TAC "IV"; REWRITE_TAC[IN_IMAGE]; GEN_TAC THEN STRIP_TAC; ASM_CASES_TAC` x''' = (u: real^3) `; ASM_REWRITE_TAC[IN_INSERT]; ASM_SIMP_TAC[IN_INSERT]; UNDISCH_TAC` x': real^3 IN V `; ASM_REWRITE_TAC[]; SUBGOAL_THEN` (f:real^3 -> real -> real^3) (ivs_rho_node1 FF (ivs_rho_node1 FF u)) t = ivs_rho_node1 FF (ivs_rho_node1 FF u) ` ASSUME_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; CONJ_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; UNDISCH_TAC` !v. v IN V ==> ~(rho_node1 FF (rho_node1 FF v) = v) `; DISCH_THEN (MP_TAC o (SPEC` ivs_rho_node1 FF (ivs_rho_node1 FF u) `)); ANTS_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; SUBGOAL_THEN` convex_local_fan (V,E,FF) ` MP_TAC; FIRST_X_ASSUM ACCEPT_TAC; REWRITE_TAC[convex_local_fan]; STRIP_TAC; ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2; SUBGOAL_THEN` ! v. v IN V ==> wedge_in_fan_ge (v ,rho_node1 FF v) E = wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) ` ASSUME_TAC; GEN_TAC; STRIP_TAC; MATCH_MP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND; ASM_REWRITE_TAC[]; SUBGOAL_THEN` ! v. v IN V ==> azim_in_fan (v,rho_node1 FF v) E = azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) ` ASSUME_TAC; GEN_TAC; STRIP_TAC; MATCH_MP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND; ASM_REWRITE_TAC[]; (* ----- *) ASSUME_TAC2 Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI; DOWN; NHANH IN_CONV0_IMP_AFF_EQ1; STRIP_TAC; SUBGOAL_THEN` w IN aff {vec 0, v:real^3 } ` ASSUME_TAC; UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; MP_TAC (SPEC` {vec 0, w:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL); REWRITE_TAC[SUBSET; Sphere.aff]; DISCH_THEN MATCH_MP_TAC; REWRITE_TAC[IN_INSERT]; SUBGOAL_THEN` ! v:real^3. v IN V ==> ~collinear {vec 0, v, ivs_rho_node1 FF v} ` ASSUME_TAC; UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); GEN_TAC THEN STRIP_TAC; MATCH_MP_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS; ASM_REWRITE_TAC[]; ASSUME_TAC2 LUNAR_IMP_IN_TWO_HAFLS_PLANE; SUBGOAL_THEN` ! x. x IN V /\ ~( x = v ) /\ ~( x = w:real^3) ==> ~ collinear {vec 0, v, x} ` ASSUME_TAC; DOWN THEN PHA; STRIP_TAC; FIRST_ASSUM NHANH; GEN_TAC; SUBGOAL_THEN` ~collinear {vec 0, v, ivs_rho_node1 FF v} /\ ~collinear {vec 0, v, rho_node1 FF v} ` MP_TAC; ASM_SIMP_TAC[]; MESON_TAC[Planarity.aff_gt_imp_not_collinear]; ASM_SIMP_TAC[]; SUBGOAL_THEN` ! x. x IN V /\ ~( x = v ) /\ ~( x = w:real^3) ==> rho_node1 FF x IN aff_ge {vec 0, v} {x} /\ ivs_rho_node1 FF x IN aff_ge {vec 0, v} {x} ` ASSUME_TAC; DOWN THEN DOWN THEN PHA THEN STRIP_TAC; GEN_TAC; FIRST_ASSUM NHANH; STRIP_TAC; SUBGOAL_THEN` x'': real^3 IN V ` MP_TAC; FIRST_ASSUM ACCEPT_TAC; EXPAND_TAC "V"; REWRITE_TAC[IN_ELIM_THM]; STRIP_TAC; UNDISCH_TAC` ~collinear {vec 0, v, x'':real^3} `; NHANH Fan.th3a; STRIP_TAC; DOWN; MP_TAC (SET_RULE` {} SUBSET {x'':real^3}`); PHA; NHANH AFF_GE_MONO_RIGHT; REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; GSYM aff]; STRIP_TAC; ASM_CASES_TAC` n = 0 `; UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `; UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[ITER]; UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `; DISCH_THEN (ASSUME_TAC o SYM); ASM_CASES_TAC` n = (i:num) `; UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `; ASM_REWRITE_TAC[]; ASSUME_TAC AFF_GT_SUBSET_AFF_GE; ASM_CASES_TAC` n < (i:num) `; SUBGOAL_THEN` x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n: num` ; ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `]; ASM_REWRITE_TAC[IN_INTER]; UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; SUBGOAL_THEN` ~ collinear {vec 0, v, rho_node1 FF v} ` MP_TAC; ASM_SIMP_TAC[]; NHANH Fan.th3a; NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION; STRIP_TAC; UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ONCE_REWRITE_TAC[EQ_SYM_EQ]; STRIP_TAC; ASM_REWRITE_TAC[]; SUBGOAL_THEN` ~ collinear {vec 0, v, x'': real^3} ` MP_TAC; ASM_SIMP_TAC[]; NHANH Fan.th3a; NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION; ASM_SIMP_TAC[]; STRIP_TAC; UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w: real^3} `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; CONJ_TAC; ASM_CASES_TAC` n = (i - 1) `; EXPAND_TAC "x''"; REWRITE_TAC[GSYM ITER]; ASM_SIMP_TAC[ARITH_RULE` ~( i = 0) ==> SUC ( i - 1) = i `; IN_UNION]; SUBGOAL_THEN` rho_node1 FF x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` SUC n `; EXPAND_TAC "x''"; REWRITE_TAC[GSYM ITER]; REWRITE_TAC[ARITH_RULE` 0 < SUC n `]; MATCH_MP_TAC (ARITH_RULE` n < i /\ ~( n = i - 1) ==> SUC n < i `); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[IN_UNION; IN_INTER]; SIMP_TAC[]; ASM_CASES_TAC` n = 1`; DOWN; EXPAND_TAC "x''"; SIMP_TAC[ITER1]; ASM_SIMP_TAC[]; SIMP_TAC[IN_UNION]; REWRITE_TAC[aff]; STRIP_TAC; DISJ1_TAC; MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET]; SUBGOAL_THEN` ivs_rho_node1 FF x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n - 1 `; EXPAND_TAC "x''"; ASSUME_TAC2 (ARITH_RULE`~( n = 0) ==> SUC ( n - 1) = n `); EXPAND_TAC "n"; REWRITE_TAC[ITER]; SUBGOAL_THEN` ITER (n - 1) (rho_node1 FF) v IN V ` ASSUME_TAC; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; UNDISCH_TAC` ~( n = 0) `; UNDISCH_TAC` ~( n = 1) `; UNDISCH_TAC` n < (i:num) `; ARITH_TAC; ASM_REWRITE_TAC[IN_INTER; IN_UNION]; SIMP_TAC[]; ASSUME_TAC2 (ARITH_RULE` ~( n < (i:num) ) ==> (n - i) + i = n `); SUBGOAL_THEN` x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` n - (i:num) `; ASM_REWRITE_TAC[]; EXPAND_TAC "n"; REWRITE_TAC[GSYM ITER_ADD]; ASM_REWRITE_TAC[]; CONJ_TAC; UNDISCH_TAC` ~( n = (i:num)) `; UNDISCH_TAC` ~( n < (i:num)) `; ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE` ~( n < (i:num)) ==> ( n - i < j <=> n < i + j )`]; UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[IN_INTER]; SUBGOAL_THEN` ~ collinear {vec 0, v, ivs_rho_node1 FF v}` MP_TAC; ASM_SIMP_TAC[]; PHA; NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ; ONCE_REWRITE_TAC[EQ_SYM_EQ]; STRIP_TAC; SUBGOAL_THEN` ~ collinear {vec 0, v, x'':real^3} ` MP_TAC; ASM_SIMP_TAC[]; NHANH Fan.th3a; NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION; SIMP_TAC[]; STRIP_TAC; CONJ_TAC; ASM_REWRITE_TAC[]; ASM_CASES_TAC` n = (i + j) - 1 `; EXPAND_TAC "x''"; REWRITE_TAC[GSYM ITER]; ASM_SIMP_TAC[]; ASSUME_TAC2 (ARITH_RULE` n < CARD (V:real^3 -> bool) ==> SUC (CARD V - 1) = CARD V `); ASM_REWRITE_TAC[]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID; FIRST_ASSUM (ASSUME_TAC2 o SPEC_ALL); ASM_REWRITE_TAC[IN_UNION]; UNDISCH_TAC` aff {vec 0, v:real^3} = aff {vec 0, w} `; DISCH_THEN (SUBST1_TAC o SYM); REWRITE_TAC[aff]; MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET]; SUBGOAL_THEN` rho_node1 FF x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC; REWRITE_TAC[IN_ELIM_THM]; EXPAND_TAC "x''"; REWRITE_TAC[GSYM ITER]; ASM_SIMP_TAC[ARITH_RULE` ~( n < i ) ==> SUC n = SUC ( n - i ) + i `]; REWRITE_TAC[GSYM ITER_ADD]; ASM_REWRITE_TAC[]; EXISTS_TAC ` SUC ( n - i ) `; REWRITE_TAC[]; UNDISCH_TAC` n < CARD (V:real^3 -> bool) `; UNDISCH_TAC` i + j = CARD (V: real^3 -> bool) `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; UNDISCH_TAC` ~( n < (i:num)) `; UNDISCH_TAC` ~ ( n = ( i + j ) - 1) `; ARITH_TAC; ASM_REWRITE_TAC[IN_INTER; IN_UNION]; SIMP_TAC[]; ASM_CASES_TAC` n = i + 1 `; REWRITE_TAC[IN_UNION]; EXPAND_TAC "x''"; FIRST_ASSUM SUBST1_TAC; REWRITE_TAC[GSYM ADD1; ITER]; ASM_SIMP_TAC[aff]; MESON_TAC[HULL_SUBSET; SUBSET; IN_INSERT]; SUBGOAL_THEN` ivs_rho_node1 FF x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM]; EXPAND_TAC "x''"; ASSUME_TAC2 (ARITH_RULE` ~( n < (i:num) ) /\ ~(n = i + 1) /\ ~( n = i ) ==> SUC ( n - 1 - i ) + i = n `); EXPAND_TAC "n"; REWRITE_TAC[GSYM ITER_ADD; ITER]; ASM_REWRITE_TAC[]; SUBGOAL_THEN` ITER (n - 1 - i) (rho_node1 FF) w IN V ` ASSUME_TAC; ASM_SIMP_TAC[]; ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[]; EXISTS_TAC` n - 1 - i `; ASM_REWRITE_TAC[]; CONJ_TAC; UNDISCH_TAC` ~(n = i + 1) `; UNDISCH_TAC` ~( n < (i:num) ) `; UNDISCH_TAC` ~( n = (i:num)) `; ARITH_TAC; UNDISCH_TAC` n < CARD (V:real^3 -> bool) `; UNDISCH_TAC` i + j = CARD (V:real^3 -> bool) `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; UNDISCH_TAC` ~( n < i:num ) `; UNDISCH_TAC` ~( n = i:num ) `; ARITH_TAC; DOWN; ASM_REWRITE_TAC[IN_INTER; IN_UNION]; SIMP_TAC[]; SUBGOAL_THEN` ! u:real^3. affine hull {vec 0, v, w, u} = affine hull {vec 0, v, u} ` ASSUME_TAC; GEN_TAC; REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ]; CONJ_TAC; MATCH_MP_TAC HULL_MINIMAL; REWRITE_TAC[AFFINE_AFFINE_HULL]; MP_TAC (SPEC` {vec 0, v, u': real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL); SIMP_TAC[INSERT_SUBSET]; STRIP_TAC; SUBGOAL_THEN` affine hull {vec 0, v:real^3} SUBSET affine hull {vec 0, v, u'}` MP_TAC; MATCH_MP_TAC HULL_MONO; CONV_TAC SET_RULE; REWRITE_TAC[SUBSET]; DISCH_THEN MATCH_MP_TAC; UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `; ASM_REWRITE_TAC[GSYM aff]; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; UNDISCH_TAC` aff {vec 0, v} = aff { vec 0, w:real^3} `; DISCH_THEN (SUBST1_TAC o SYM); ASM_REWRITE_TAC[]; MATCH_MP_TAC HULL_MONO; CONV_TAC SET_RULE; SUBGOAL_THEN`! x'. x' IN V ==> (f:real^3 -> real -> real^3) u t IN wedge_ge (vec 0) (x') (rho_node1 FF x') (ivs_rho_node1 FF x') ` ASSUME_TAC; GEN_TAC; STRIP_TAC; ASM_CASES_TAC` x'' = (v:real^3) `; UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM]; FIRST_ASSUM (MP_TAC o (SPEC` v, rho_node1 FF v ` )); ANTS_TAC; ASM_SIMP_TAC[]; REWRITE_TAC[SUBSET]; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `)); DOWN; UNDISCH_TAC` !v. v IN V ==> wedge_in_fan_ge (v,rho_node1 FF v) E = wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `; DISCH_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `)); ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM]; SUBGOAL_THEN` ~ collinear {vec 0, v , u:real^3 } ` MP_TAC; ASM_SIMP_TAC[]; STRIP_TAC; SUBGOAL_THEN` (!x. x IN (ss:real^3 # real^3 -> bool) ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; FIRST_ASSUM (MP_TAC o (SPEC` (u:real^3, v:real^3) `)); ANTS_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u:real^3 `; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `; SIMP_TAC[INSERT_COMM]; STRIP_TAC; ASM_SIMP_TAC[]; EXISTS_TAC` &1 `; EXISTS_TAC` &0 `; CONJ_TAC; CONV_TAC VECTOR_ARITH; REAL_ARITH_TAC; REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3]; STRIP_TAC; DOWN; REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID]; ONCE_REWRITE_TAC[VECTOR_ADD_SYM]; FIRST_ASSUM NHANH; STRIP_TAC; UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `; NHANH Fan.th3a; NHANH AFF_GT_2_1; STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, v} {u} ` ASSUME_TAC; ASM_REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u': real `; EXISTS_TAC` v': real `; EXISTS_TAC` w': real`; ASM_REWRITE_TAC[]; CONV_TAC VECTOR_ARITH; DOWN; NHANH IN_AFF_GT_IMP_AZIMEQ2; SIMP_TAC[]; ASM_CASES_TAC` x'' = w:real^3 `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM]; FIRST_ASSUM (MP_TAC o (SPEC` w, rho_node1 FF w `)); ANTS_TAC; ASM_SIMP_TAC[]; UNDISCH_TAC` !v. v IN V ==> wedge_in_fan_ge (v,rho_node1 FF v) E = wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w: real^3 `)); DOWN; SIMP_TAC[]; STRIP_TAC; REWRITE_TAC[SUBSET]; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u:real^3 `)); DOWN; REWRITE_TAC[wedge_ge; IN_ELIM_THM]; SUBGOAL_THEN` ~collinear {vec 0, v, u:real^3} ` MP_TAC; ASM_SIMP_TAC[]; ASM_REWRITE_TAC[Fan.collinear_fan]; PHA THEN STRIP_TAC; SUBGOAL_THEN` ~( w = vec 0: real^3) ` MP_TAC; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; ASM_SIMP_TAC[]; ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF; ONCE_REWRITE_TAC[EQ_SYM_EQ]; UNDISCH_TAC` ~(u IN aff {vec 0, w: real^3}) `; PHA; REWRITE_TAC[GSYM Fan.collinear_fan]; NHANH Fan.th3a; NHANH AFF_GT_2_1; STRIP_TAC; SUBGOAL_THEN` (!x. x IN ss ==> (!t1 t2. (f: real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPEC` (u:real^3, w:real^3) `)); ANTS_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u:real^3 `; EXISTS_TAC` w:real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` ~collinear {vec 0, w, u: real^3} `; SIMP_TAC[INSERT_COMM]; ASM_SIMP_TAC[]; STRIP_TAC; EXISTS_TAC` &1 `; EXISTS_TAC` &0 `; CONJ_TAC; CONV_TAC VECTOR_ARITH; REAL_ARITH_TAC; REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u }` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; SUBGOAL_THEN` affine hull {vec 0, v, w, u} SUBSET affine hull {vec 0, w, u:real^3} ` MP_TAC; MATCH_MP_TAC HULL_MINIMAL; REWRITE_TAC[AFFINE_AFFINE_HULL]; MP_TAC (ISPEC` {vec 0, w, u: real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL); SIMP_TAC[INSERT_SUBSET]; STRIP_TAC; MP_TAC (SET_RULE` {vec 0, w:real^3} SUBSET {vec 0, w, u} `); NHANH (ISPEC` affine ` HULL_MONO); REWRITE_TAC[SUBSET]; STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `; REWRITE_TAC[aff]; DISCH_THEN (SUBST1_TAC o SYM); MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET]; REWRITE_TAC[SUBSET]; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` (f:real^3 -> real -> real^3) u t `)); DOWN; REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3; VECTOR_MUL_RZERO; VECTOR_ADD_LID]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPECL [` w': real `;` v': real `])); ANTS_TAC; ASM_REWRITE_TAC[]; CONV_TAC VECTOR_ARITH; STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, w} {u} ` MP_TAC; ASM_REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u': real `; EXISTS_TAC` v': real `; EXISTS_TAC` w': real `; ASM_REWRITE_TAC[]; CONV_TAC VECTOR_ARITH; STRIP_TAC; UNDISCH_TAC` &0 <= azim (vec 0) w (rho_node1 FF w) u `; UNDISCH_TAC` azim (vec 0) w (rho_node1 FF w) u <= azim (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w) `; PHA; DOWN; NHANH IN_AFF_GT_IMP_AZIMEQ2; SIMP_TAC[]; SUBGOAL_THEN` interior_angle1 (vec 0) FF x'' = pi /\ rho_node1 FF x'' IN aff {x'', v, w} /\ ivs_rho_node1 FF x'' IN aff {x'', v, w} ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY]; ASM_REWRITE_TAC[]; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; SUBGOAL_THEN` azim (vec 0) x'' (rho_node1 FF x'') (ivs_rho_node1 FF x'') = interior_angle1 (vec 0) FF x'' ` MP_TAC; ASM_SIMP_TAC[]; DISCH_THEN (SUBST1_TAC o SYM); NHANH Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT; SIMP_TAC[]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPEC` x'', rho_node1 FF x'' `)); ANTS_TAC; ASM_SIMP_TAC[]; ASM_REWRITE_TAC[]; UNDISCH_TAC` !v. v IN V ==> wedge_in_fan_ge (v,rho_node1 FF v) E = wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `; STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` x'': real^3 `)); ASM_REWRITE_TAC[VECTOR_ARITH` x - vec 0 = x `; SUBSET; IN_ELIM_THM]; STRIP_TAC; ABBREV_TAC` e1 = x'' cross rho_node1 FF x'' `; SUBGOAL_THEN` e1 dot v = &0 /\ e1 dot (w:real^3) = &0 ` MP_TAC; UNDISCH_TAC` vec 0 IN conv0 {v, w:real^3} `; REWRITE_TAC[Collect_geom.CONV0_SET2; IN_ELIM_THM]; STRIP_TAC; MP_TAC (ISPEC` e1: real^3 ` DOT_RZERO); ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL]; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `)); FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `)); DOWN THEN DOWN; UNDISCH_TAC` &0 < a' `; UNDISCH_TAC` &0 < b' `; REWRITE_TAC[REAL_ARITH` &0 <= a <=> a = &0 \/ &0 < a `]; MESON_TAC[REAL_LT_ADD; REAL_LT_MUL; REAL_ARITH` &0 < a ==> ~(a = &0) `; REAL_ARITH` &0 < a ==> ~( a + x * &0 = &0 \/ x * &0 + a = &0) `]; STRIP_TAC; UNDISCH_TAC` !u. u IN V ==> ~(u = v) ==> ~(u = w) ==> u IN aff_gt {vec 0, v} {rho_node1 FF v} \/ u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} `; PHA THEN STRIP_TAC; FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u:real^3 `)); SUBGOAL_THEN` rho_node1 FF v IN V /\ ivs_rho_node1 FF v IN V ` MP_TAC; ASM_SIMP_TAC[]; SUBGOAL_THEN` ~ collinear { vec 0, v, rho_node1 FF v } /\ ~ collinear {vec 0, v, ivs_rho_node1 FF v } ` MP_TAC; ASM_SIMP_TAC[]; NHANH Fan.th3a; NHANH AFF_GT_2_1; DOWN THEN STRIP_TAC; STRIP_TAC; STRIP_TAC; UNDISCH_TAC` u IN aff_gt {vec 0, v} {rho_node1 FF v} `; ASM_REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID]; STRIP_TAC; SUBGOAL_THEN` (!x. x IN ss ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v, v `)); ANTS_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` rho_node1 FF v `; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `; SIMP_TAC[INSERT_COMM]; STRIP_TAC; UNDISCH_TAC` u = t2 % v + t3 % rho_node1 FF v `; DISCH_THEN (ASSUME_TAC o SYM); ASM_SIMP_TAC[]; EXISTS_TAC` t3: real `; EXISTS_TAC` t2:real `; ASM_REWRITE_TAC[]; EXPAND_TAC "u"; CONV_TAC VECTOR_ARITH; REWRITE_TAC[]; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u } ` MP_TAC; ASM_SIMP_TAC[]; FIRST_X_ASSUM (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3]; EXPAND_TAC "u"; REWRITE_TAC[VECTOR_ARITH` u % vec 0 + v % v' + w % (t2 % v' + t3 % ax) = ( v + w * t2 ) % v' + ( w * t3) % ax`]; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[VECTOR_ARITH` a + b = b + (a:real^N) `]; PHA THEN STRIP_TAC; UNDISCH_TAC` (f:real^3 -> real -> real^3) u t = (w' * t3) % rho_node1 FF v + (v' + w' * t2) % v `; ONCE_REWRITE_TAC[VECTOR_ARITH` a + b = b + (a:real^N) `]; FIRST_ASSUM NHANH; SIMP_TAC[DOT_RADD; DOT_RMUL]; ASM_REWRITE_TAC[REAL_ARITH` a * &0 + x = x `]; STRIP_TAC; SUBGOAL_THEN` &0 <= e1 dot rho_node1 FF v ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LE_MUL; ASM_REWRITE_TAC[]; UNDISCH_TAC` &0 < w' * t3 `; REAL_ARITH_TAC; STRIP_TAC; STRIP_TAC; UNDISCH_TAC` u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} `; ASM_REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID]; STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM]; REWRITE_TAC[VECTOR_ARITH` u % vec 0 + v % vv + w % (t2 % vv + t3 % vc) = ( v + w * t2 ) % vv + (w * t3 ) % vc `]; FIRST_X_ASSUM (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` (!x. x IN ss ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v, v `)); ANTS_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` ivs_rho_node1 FF v `; EXISTS_TAC` v: real^3 `; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[]; UNDISCH_TAC` ~collinear {vec 0, v, ivs_rho_node1 FF v} `; SIMP_TAC[INSERT_COMM]; STRIP_TAC; EXISTS_TAC` t3: real`; EXISTS_TAC` t2: real `; ASM_REWRITE_TAC[]; EXPAND_TAC "u"; CONV_TAC VECTOR_ARITH; REWRITE_TAC[]; ONCE_REWRITE_TAC[VECTOR_ADD_SYM]; DISCH_THEN (ASSUME_TAC2 o (SPECL [` w' * t3: real `; ` v' + w' * t2: real`])); ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_MUL_RZERO; REAL_ADD_LID]; UNDISCH_TAC` !x. x IN V ==> &0 <= e1 dot (x: real^3) `; DISCH_THEN (ASSUME_TAC2 o (SPEC` ivs_rho_node1 FF v `)); MATCH_MP_TAC REAL_LE_MUL; ASM_REWRITE_TAC[]; UNDISCH_TAC` &0 < w' * t3 `; CONV_TAC REAL_ARITH; ASM_CASES_TAC` ~( x' = (u:real^3)) /\ ~( rho_node1 FF x' = u ) /\ ~( ivs_rho_node1 FF x' = u ) ` ; DOWN THEN STRIP_TAC; UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_SIMP_TAC[]; STRIP_TAC; UNDISCH_TAC` !x. (x:real^3 # real^3) IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `; DISCH_THEN (MP_TAC o (SPEC` x', rho_node1 FF x' `)); ANTS_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; STRIP_TAC; MATCH_MP_TAC SUBSET_TRANS; EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `; ASM_REWRITE_TAC[INSERT_SUBSET]; ASM_SIMP_TAC[]; STRIP_TAC; ASM_CASES_TAC` x' = u:real^3 `; ASM_SIMP_TAC[]; SUBGOAL_THEN` rho_node1 FF u IN aff_ge {vec 0, v} {u} /\ ivs_rho_node1 FF u IN aff_ge {vec 0, v} {u} ` ASSUME_TAC; ASM_SIMP_TAC[]; SUBGOAL_THEN` ~collinear {vec 0, v, u:real^3} ` ASSUME_TAC; ASM_SIMP_TAC[]; SUBGOAL_THEN` (f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t IN IV ` ASSUME_TAC; EXPAND_TAC "IV"; REWRITE_TAC[IN_IMAGE]; EXISTS_TAC` ivs_rho_node1 FF u `; ASM_SIMP_TAC[]; ABBREV_TAC` UU = {ITER n (rho_node1 IF) ( (f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t ) | n <= 2} `; ABBREV_TAC` P = affine hull {vec 0, v, u:real^3} `; ASSUME_TAC (ISPECL [` {vec 0, v:real^3 }`;` {u:real^3} `] AFF_GE_SUBSET_AFFINE_HULL); SUBGOAL_THEN` plane (P:real^3 -> bool) ` ASSUME_TAC; REWRITE_TAC[plane]; EXISTS_TAC` vec 0: real^3 `; EXISTS_TAC` v: real^3 `; EXISTS_TAC` u: real^3 `; ASM_REWRITE_TAC[]; SUBGOAL_THEN` vec 0 IN (P:real^3 -> bool) ` ASSUME_TAC; MP_TAC ( prove(` {vec 0, v, u:real^3} SUBSET affine hull {vec 0, v, u} `, REWRITE_TAC[HULL_SUBSET])); UNDISCH_TAC` w = ITER i (rho_node1 FF ) v ` ; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF ) w ` ; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[SUBSET]; DISCH_THEN MATCH_MP_TAC; REWRITE_TAC[IN_INSERT]; SUBGOAL_THEN` UU SUBSET (P: real^3 -> bool) ` ASSUME_TAC; EXPAND_TAC "UU"; REWRITE_TAC[SUBSET; IN_ELIM_THM]; GEN_TAC; REWRITE_TAC[ARITH_RULE` n <= 2 <=> n = 0 \/ n = 1 \/ n = 2 `]; STRIP_TAC; DOWN; ASM_REWRITE_TAC[ITER]; STRIP_TAC; UNDISCH_TAC` aff_ge {vec 0, v:real^3} {u} SUBSET affine hull ({vec 0, v} UNION {u}) `; UNDISCH_TAC` w = ITER i (rho_node1 FF) v `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET]; DISCH_THEN MATCH_MP_TAC; ASM_REWRITE_TAC[]; DOWN; DOWN; SIMP_TAC[ITER1]; SUBGOAL_THEN` rho_node1 IF ((f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t) = f (rho_node1 FF (ivs_rho_node1 FF u)) t` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_SIMP_TAC[]; SIMP_TAC[]; ASM_SIMP_TAC[]; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; SIMP_TAC[]; UNDISCH_TAC` x'' = ITER n (rho_node1 IF) ((f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t) ` ; DOWN THEN SIMP_TAC[]; REWRITE_TAC[Lvducxu.ITER12]; SUBGOAL_THEN` rho_node1 IF (f (ivs_rho_node1 FF u) (t:real)) = f (rho_node1 FF (ivs_rho_node1 FF u)) t ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_SIMP_TAC[]; SIMP_TAC[]; PHA THEN STRIP_TAC; ASM_SIMP_TAC[]; UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) `; UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `; DISCH_THEN (ASSUME_TAC o SYM); UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET]; DISCH_THEN MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASSUME_TAC2 ( SPECL [` IE: (real^3 -> bool) -> bool `;` IV: real^3 -> bool `;` UU: real^3 -> bool `;` P: real^3 -> bool `;` 2 `;` IF: real^3 # real^3 -> bool `; `((f:real ^3 -> real -> real^3) (ivs_rho_node1 FF u) t) `] (GEN_ALL AZIM_PI_ITER_LOCAL_FAN)); FIRST_X_ASSUM (MP_TAC o (SPEC` 0 `)); ANTS_TAC; ARITH_TAC; UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `; UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); REWRITE_TAC[ADD; ITER; ITER1; Lvducxu.ITER12]; SUBGOAL_THEN` rho_node1 IF (f (ivs_rho_node1 FF u) (t:real)) = f (rho_node1 FF (ivs_rho_node1 FF u)) t ` MP_TAC; ASM_SIMP_TAC[]; SIMP_TAC[]; ASM_SIMP_TAC[]; NHANH (MESON[PI_POS]` x = pi ==> &0 < x `); NHANH Local_lemmas1.AZIM_POS_IMP_SUM_2PI; STRIP_TAC; DOWN; ASM_REWRITE_TAC[REAL_ARITH` a + x = &2 * a <=> x = a `]; SIMP_TAC[REAL_LE_REFL]; STRIP_TAC; SUBGOAL_THEN` wedge_ge (vec 0) (f u (t:real)) (rho_node1 FF u) (ivs_rho_node1 FF u) = wedge_ge (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) ` ASSUME_TAC; DOWN; SUBGOAL_THEN` interior_angle1 (vec 0) FF u = pi ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY]; SUBGOAL_THEN` azim (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) = pi ` MP_TAC; DOWN; ASM_SIMP_TAC[]; NHANH Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT; SIMP_TAC[VECTOR_SUB_RZERO]; PHA THEN STRIP_TAC; SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, rho_node1 FF u } ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ ; ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET]; CONJ_TAC; EXPAND_TAC "P"; MP_TAC (ISPECL [` affine: (real^3 -> bool) -> bool `; ` { vec 0, v, u:real^3} `] HULL_SUBSET); REWRITE_TAC[SUBSET]; DISCH_THEN MATCH_MP_TAC; REWRITE_TAC[IN_INSERT]; UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) `; REWRITE_TAC[SUBSET;SET_RULE` {a,b} UNION {c} = {a,b,c} `]; ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; ASM_REWRITE_TAC[]; SUBGOAL_THEN` f u (t:real) IN affine hull {vec 0, v, w, u:real^3} ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; DOWN; ASM_REWRITE_TAC[]; SIMP_TAC[IN_ELIM_THM; AFFINE_HULL_3]; PHA THEN STRIP_TAC; SUBGOAL_THEN` (!x. x IN ss ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; FIRST_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `)); ANTS_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u: real^3 `; EXISTS_TAC` rho_node1 FF u `; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[]; EXISTS_TAC` &1 `; EXISTS_TAC` &0 `; CONJ_TAC; CONV_TAC VECTOR_ARITH; REAL_ARITH_TAC; REWRITE_TAC[]; DISCH_THEN (MP_TAC o (SPECL [` v': real `;` w': real `])); ANTS_TAC; ASM_REWRITE_TAC[]; CONV_TAC VECTOR_ARITH; ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; CROSS_LADD; CROSS_LMUL; CROSS_REFL; VECTOR_ADD_RID; DOT_LMUL]; SIMP_TAC[REAL_LE_MUL_EQ]; ASM_REWRITE_TAC[]; FIRST_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `)); ANTS_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; UNDISCH_TAC` !v. v IN V ==> wedge_in_fan_ge (v,rho_node1 FF v) E = wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `; DISCH_THEN (ASSUME_TAC2 o (SPEC` u:real^3 `)); DOWN; SIMP_TAC[]; STRIP_TAC; MATCH_MP_TAC SUBSET_TRANS; EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[INSERT_SUBSET]; SUBGOAL_THEN` azim_in_fan (u, rho_node1 FF u) E <= pi /\ V SUBSET wedge_in_fan_ge (u, rho_node1 FF u) E ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_SIMP_TAC[]; DOWN THEN STRIP_TAC; DOWN; UNDISCH_TAC` wedge_in_fan_ge (u,rho_node1 FF u) E = wedge_ge (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) `; SIMP_TAC[]; SUBGOAL_THEN` (!x. (x :real^3 # real^3) IN ss ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; UNDISCH_TAC` w = ITER i (rho_node1 FF ) v ` ; UNDISCH_TAC` v = ITER j (rho_node1 FF ) w ` ; DISCH_THEN (ASSUME_TAC o SYM); DISCH_THEN (ASSUME_TAC o SYM); ASM_CASES_TAC` rho_node1 FF x' = u `; ASM_SIMP_TAC[]; SUBGOAL_THEN` ~(rho_node1 FF (rho_node1 FF ( ivs_rho_node1 FF x')) = (ivs_rho_node1 FF x')) ` MP_TAC; FIRST_ASSUM MATCH_MP_TAC; ASM_SIMP_TAC[]; SUBGOAL_THEN` rho_node1 FF (ivs_rho_node1 FF x') = x' ` SUBST1_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; STRIP_TAC; SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, ivs_rho_node1 FF u }` MP_TAC; MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ; ASM_SIMP_TAC[]; ASSUME_TAC2 (ISPECL [` {vec 0, v:real^3} `;` {u:real^3} `] AFF_GE_SUBSET_AFFINE_HULL); MP_TAC (ISPECL [` affine: (real^3 -> bool) -> bool `;` {vec 0, v, u:real^3} `] HULL_SUBSET); SIMP_TAC[INSERT_SUBSET]; STRIP_TAC; UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u: real^3}) `; REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET]; DISCH_THEN MATCH_MP_TAC; ASM_SIMP_TAC[]; STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3; VECTOR_MUL_RZERO; VECTOR_ADD_LID]; STRIP_TAC; SUBGOAL_THEN` ~ collinear {vec 0, u, ivs_rho_node1 FF u } ` ASSUME_TAC; ASM_SIMP_TAC[]; FIRST_ASSUM (MP_TAC o (SPEC` u, ivs_rho_node1 FF u ` )); ANTS_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u:real^3 `; EXISTS_TAC` ivs_rho_node1 FF u `; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[]; EXISTS_TAC` &1 `; EXISTS_TAC` &0 `; CONJ_TAC; CONV_TAC VECTOR_ARITH; REAL_ARITH_TAC; REWRITE_TAC[]; DISCH_THEN (ASSUME_TAC2 o (SPECL [` v': real `;` w': real `])); DOWN THEN DOWN; ONCE_REWRITE_TAC[SET_RULE` {a,b} = {b,a} `]; DOWN; SUBGOAL_THEN` ivs_rho_node1 FF u = x' ` ASSUME_TAC; EXPAND_TAC "u"; ASM_SIMP_TAC[]; ASM_REWRITE_TAC[]; PHA THEN STRIP_TAC; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, x'} {u:real^3} ` MP_TAC; DOWN THEN DOWN; NHANH Fan.th3a; NHANH AFF_GT_2_1; SIMP_TAC[IN_ELIM_THM]; STRIP_TAC; STRIP_TAC; EXISTS_TAC` u': real `; EXISTS_TAC` w': real `; EXISTS_TAC` v': real` ; ASM_REWRITE_TAC[]; CONJ_TAC; UNDISCH_TAC` u' + v' + w' = &1 `; REAL_ARITH_TAC; CONV_TAC VECTOR_ARITH; NHANH IN_AFF_GT_IMP_AZIMEQ2; REWRITE_TAC[GSYM Rogers.AZIM_EQ_SYM]; SIMP_TAC[wedge_ge]; STRIP_TAC; UNDISCH_TAC` !x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `; STRIP_TAC; FIRST_ASSUM (MP_TAC o (SPEC` x', rho_node1 FF x' `)); ANTS_TAC; ASM_SIMP_TAC[]; DOWN THEN PHA; ASM_SIMP_TAC[GSYM wedge_ge]; UNDISCH_TAC` !v. v IN V ==> azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) = interior_angle1 (vec 0) FF v `; DISCH_THEN (ASSUME_TAC o GSYM); ASM_SIMP_TAC[]; STRIP_TAC; MATCH_MP_TAC SUBSET_TRANS; EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `; UNDISCH_TAC` (f: real^3 -> real -> real^3) u t = v' % u + w' % x' `; DISCH_THEN (ASSUME_TAC o SYM); ASM_SIMP_TAC[]; UNDISCH_TAC` rho_node1 FF x' = u `; DISCH_THEN (ASSUME_TAC o SYM); ASM_SIMP_TAC[INSERT_SUBSET]; SUBGOAL_THEN` (f: real^3 -> real -> real^3) u t IN wedge_ge (vec 0) x' (rho_node1 FF x') (ivs_rho_node1 FF x') ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; DOWN; SIMP_TAC[]; ASM_CASES_TAC` ivs_rho_node1 FF x' = u `; ASM_REWRITE_TAC[]; SUBGOAL_THEN` x' = rho_node1 FF u ` ASSUME_TAC; FIRST_X_ASSUM (SUBST1_TAC o SYM); ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; UNDISCH_TAC`!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `; DISCH_THEN (MP_TAC o (SPEC` x', rho_node1 FF x' `)); ANTS_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; UNDISCH_TAC` !v. v IN V ==> azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) = interior_angle1 (vec 0) FF v `; DISCH_THEN (ASSUME_TAC2 o (SPEC` x': real^3 `)); FIRST_X_ASSUM (MP_TAC o SYM); ASM_REWRITE_TAC[]; SIMP_TAC[]; STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `)); ANTS_TAC; EXPAND_TAC "ss"; REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u: real^3 `; EXISTS_TAC` rho_node1 FF u `; ASM_SIMP_TAC[]; EXISTS_TAC` &1 `; EXISTS_TAC` &0 `; CONJ_TAC; CONV_TAC VECTOR_ARITH; REAL_ARITH_TAC; ASM_REWRITE_TAC[]; STRIP_TAC; SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, rho_node1 FF u } ` ASSUME_TAC; MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ; ASM_SIMP_TAC[]; MP_TAC (ISPEC ` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL); SIMP_TAC[INSERT_SUBSET]; ASM_SIMP_TAC[]; STRIP_TAC; MP_TAC (ISPECL [` {vec 0, v:real^3} `;` {u: real^3} `] AFF_GE_SUBSET_AFFINE_HULL); REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET]; DISCH_THEN MATCH_MP_TAC; ASM_SIMP_TAC[]; SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_ASSUM ACCEPT_TAC; ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID]; STRIP_TAC; SUBGOAL_THEN` &0 < v' ` ASSUME_TAC; FIRST_X_ASSUM MATCH_MP_TAC; EXISTS_TAC` w': real`; ASM_REWRITE_TAC[]; SUBGOAL_THEN` ~ collinear {vec 0, u, rho_node1 FF u } ` MP_TAC; ASM_SIMP_TAC[]; ONCE_REWRITE_TAC[Collect_geom.PER_SET2]; NHANH Fan.th3a; NHANH AFF_GT_2_1; STRIP_TAC; SUBGOAL_THEN` (f:real ^3 -> real -> real^3) u t IN aff_gt {vec 0, rho_node1 FF u } {u} ` MP_TAC; ASM_REWRITE_TAC[IN_ELIM_THM]; EXISTS_TAC` u': real `; EXISTS_TAC` w': real `; EXISTS_TAC` v': real `; ASM_REWRITE_TAC[]; CONJ_TAC; UNDISCH_TAC` u' + v' + w' = &1 `; REAL_ARITH_TAC; CONV_TAC VECTOR_ARITH; NHANH IN_AFF_GT_IMP_AZIMEQ2; SIMP_TAC[]; STRIP_TAC THEN STRIP_TAC; MATCH_MP_TAC SUBSET_TRANS; EXISTS_TAC` (f: real^3 -> real -> real^3) u t INSERT V `; UNDISCH_TAC` (f: real^3 -> real -> real^3) u t = v' % u + w' % rho_node1 FF u `; DISCH_THEN (ASSUME_TAC o SYM); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[INSERT_SUBSET; wedge_ge]; ASM_SIMP_TAC[GSYM wedge_ge]; UNDISCH_TAC` !x'. x' IN V ==> (f: real^3 -> real -> real^3) u t IN wedge_ge (vec 0) x' (rho_node1 FF x') (ivs_rho_node1 FF x') `; DISCH_THEN (MP_TAC o (SPEC` rho_node1 FF u `)); ANTS_TAC; ASM_SIMP_TAC[]; ASM_SIMP_TAC[]; UNDISCH_TAC` ~(~(x' = u) /\ ~(rho_node1 FF x' = u) /\ ~(ivs_rho_node1 FF x' = u)) `; ASM_REWRITE_TAC[]]);;
let MHAEYJN = 
prove_by_refinement( `!a b V E FF f v w u. convex_local_fan (V,E,FF) /\ lunar (v,w) V E /\ deformation f V (a,b) /\ interior_angle1 (vec 0) FF v < pi /\ u IN V /\ ~(u = v) /\ ~(u = w) /\ (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\ (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u}) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> convex_local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\ lunar (v,w) (IMAGE (\v. f v t) V) (IMAGE (IMAGE (\v. f v t)) E)))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL SUB_LUNAR_DEFORM_LEMMA) [`FF`;`a`;`b`;`u`;`v`;`w`;`V`;`f`;`E`]; ANTS_TAC; ASM_REWRITE_TAC[]; RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_REAL_INTERVAL]); ASM_SIMP_TAC[]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_SIMP_TAC[Local_lemmas.CVX_LO_IMP_LO]); CONJ_TAC; MATCH_MP_TAC Local_lemmas.LOCAL_FAN_FINITE_V; BY(ASM_REWRITE_TAC[]); RULE_ASSUM_TAC(REWRITE_RULE[Localization.local_fan;Fan.FAN;LET_DEF;LET_END_DEF]); FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC; BY(FIRST_X_ASSUM MP_TAC THEN FIRST_X_ASSUM_ST `UNIONS` MP_TAC THEN SET_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC MHAEYJN_CONVEX_LOCAL_FAN [`a`;`b`;`V`;`E`;`FF`;`f`;`v`;`w`;`u`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `if e < e' then e else e'` EXISTS_TAC; REPEAT WEAKER_STRIP_TAC; CONJ_TAC; BY(COND_CASES_TAC THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *) end;;