1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================== *)
12 module Disjoint_fan = struct
18 open Hypermap_of_fan;;
22 open Hypermap_of_fan;;
30 (* ========================================================================== *)
32 (* ========================================================================== *)
34 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).
35 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
37 w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
38 (aff{x,v} UNION aff_gt {x,v} {w1})={}`,
40 REPEAT STRIP_TAC THEN REWRITE_TAC[UNION_OVER_INTER]
41 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[]
42 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[]
47 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).
48 FAN(x,V,E)/\ {v,w} IN E
50 aff_ge {x} {v , w} SUBSET (aff_gt {x , v} {w}) UNION (aff {x, v})`,
52 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)
53 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
54 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GE_1_2)
55 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
56 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GT_2_1)
57 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
58 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]affine_hull_2_fan)
59 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[SUBSET; UNION;IN_ELIM_THM]
61 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
62 MATCH_MP_TAC MONO_OR THEN
63 SUBGOAL_THEN `((?t1:real t2:real t3:real.
64 (&0 < t2 \/ t2 = &0) /\
67 (x':real^3) = t1 % x + t2 % v + t3 % w)
69 &0< t3 /\ t1 + t2 + t3 = &1 /\ x' = t1 % x + t2 % v + t3 % w))` ASSUME_TAC
72 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
73 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN GEN_TAC THEN
74 REWRITE_TAC[REAL_ARITH `(&0< (t2:real) \/ (t2 = &0)) <=> ( &0<= t2)`] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN
75 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
76 REWRITE_TAC [REAL_ARITH `(a:real)+ &0 = a`; VECTOR_ARITH `&0 % (w:real^3) = vec 0`;
77 VECTOR_ARITH ` ((x':real^3) = (t1:real) % (x:real^3) + (t2:real) % (v:real^3) + vec 0)<=> ( x' = t1 % x + t2 % v )` ]
81 let IBZWFFH=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (w1:real^3).
82 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
84 w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
85 aff_ge {x} {v , w1}={}`,
86 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)
87 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
88 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)
89 THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);;