(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Fan *) (* Author: Hoang Le Truong *) (* Date: 2010-02-09 *) (* ========================================================================== *) module Disjoint_fan = struct open Sphere;; open Fan_defs;; open Hypermap_of_fan;; open Tactic_fan;; open Lemma_fan;; open Fan;; open Hypermap_of_fan;; open Node_fan;; open Azim_node;; open Sum_azim_node;; (* ========================================================================== *) (* DISJOINT IN FAN *) (* ========================================================================== *) let disjiont_union_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (w1:real^3). FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E) ==> w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER (aff{x,v} UNION aff_gt {x,v} {w1})={}`, REPEAT STRIP_TAC THEN REWRITE_TAC[UNION_OVER_INTER] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (w1:real^3)`] disjoint_set_fan) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;] disjoint_fan1) THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);; let aff_ge_subset_aff_gt_union_aff=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3). FAN(x,V,E)/\ {v,w} IN E ==> aff_ge {x} {v , w} SUBSET (aff_gt {x , v} {w}) UNION (aff {x, v})`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;` (v:real^3)`] remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]affine_hull_2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[SUBSET; UNION;IN_ELIM_THM] THEN GEN_TAC THEN REWRITE_TAC[REAL_ARITH `(&0 <= (t3:real)) <=> (&0 < t3) \/ ( t3 = &0)`; TAUT `(a \/ b) /\ (c \/ d) /\ e /\ f <=> ((a \/ b)/\ c /\ e /\ f) \/ ((a \/ b) /\ d /\ e /\ f)`; EXISTS_OR_THM] THEN MATCH_MP_TAC MONO_OR THEN SUBGOAL_THEN `((?t1:real t2:real t3:real. (&0 < t2 \/ t2 = &0) /\ &0< t3 /\ t1 + t2 + t3 = &1 /\ (x':real^3) = t1 % x + t2 % v + t3 % w) ==> (?t1 t2 t3. &0< t3 /\ t1 + t2 + t3 = &1 /\ x' = t1 % x + t2 % v + t3 % w))` ASSUME_TAC THENL [MESON_TAC[]; ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN GEN_TAC THEN REWRITE_TAC[REAL_ARITH `(&0< (t2:real) \/ (t2 = &0)) <=> ( &0<= t2)`] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC [REAL_ARITH `(a:real)+ &0 = a`; VECTOR_ARITH `&0 % (w:real^3) = vec 0`; VECTOR_ARITH ` ((x':real^3) = (t1:real) % (x:real^3) + (t2:real) % (v:real^3) + vec 0)<=> ( x' = t1 % x + t2 % v )` ] THEN MESON_TAC[]]);; let IBZWFFH=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (w1:real^3). FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E) ==> w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER aff_ge {x} {v , w1}={}`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w1:real^3)`] aff_ge_subset_aff_gt_union_aff) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;`w:real^3`;` (w1:real^3)`] disjiont_union_fan) THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);; end;;