2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Hoang Le Truong *)
8 (* ========================================================================== *)
13 module Dwwutkw = struct
19 open Hypermap_of_fan;;
23 open Hypermap_of_fan;;
31 open Fully_surrounded;;
32 open Sin_azim_cross_dot;;
35 open Dartset_leads_into;;
42 let condition_not_edge_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds.
43 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
44 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
46 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
47 /\ e1 IN E /\ e2 = {v, u}
48 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
54 THEN ASM_REWRITE_TAC[]
56 THEN DISCH_THEN(LABEL_TAC"YEU")
58 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
59 THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
60 THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
63 THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
65 THEN SUBGOAL_THEN`aff_ge {x} e1 SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
66 THENL[REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
68 THEN EXISTS_TAC `e1:real^3->bool`
69 THEN ASM_REWRITE_TAC[]
70 THEN FIND_ASSUM MP_TAC(`(e1:real^3->bool) IN E`)
72 THEN ASM_REWRITE_TAC[];
73 ASSUME_TAC(SET_RULE`aff_gt {x} {v, u} INTER
74 (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u})
76 THEN MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} e1 SUBSET xfan (x,V,E)
77 ==> aff_gt {x} {v, u} INTER aff_ge {x} e1={}`)
80 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
81 THEN MATCH_MP_TAC exists_in_aff_gt
82 THEN ASM_REWRITE_TAC[]]);;
86 let condition_not_intersection_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds e1:real^3->bool e2:real^3->bool.
87 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
88 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
90 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
91 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
92 /\ e1 IN E /\ e2 = {v, u}
93 ==>aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} (e1 INTER e2)`,
95 THEN ASM_REWRITE_TAC[]
96 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
97 THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
98 THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
100 THEN POP_ASSUM MP_TAC
101 THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
103 THEN SUBGOAL_THEN`aff_ge {x} e1 SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
105 REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
106 THEN REPEAT STRIP_TAC
107 THEN EXISTS_TAC `e1:real^3->bool`
108 THEN ASM_REWRITE_TAC[]
109 THEN ASM_TAC THEN SET_TAC[IN];
110 MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} e1 SUBSET xfan (x,V,E)
111 ==> aff_gt {x} {v, u} INTER aff_ge {x} e1={}`)
113 THEN MP_TAC(SET_RULE`
114 aff_gt {x:real^3} {v, u} INTER aff_ge {x} e1={}==>
115 aff_ge {x} e1 INTER (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u})
116 = (aff_ge {x} e1 INTER aff_ge {x} {v}) UNION (aff_ge {x} e1 INTER aff_ge {x} {u})`)
118 THEN MP_TAC(SET_RULE`e1 IN E==> e1 IN E UNION {{v:real^3} | v IN V}`)
120 THEN MP_TAC(SET_RULE`v:real^3 IN V==> {v} IN E UNION {{v} | v IN V}`)
122 THEN MP_TAC(SET_RULE`u:real^3 IN V==> {u} IN E UNION {{v} | v IN V}`)
124 THEN FIND_ASSUM MP_TAC(`FAN(x:real^3,V,E)`)
125 THEN REWRITE_TAC[FAN;fan7]
127 THEN POP_ASSUM(fun th-> MRESA_TAC th [`e1:real^3->bool`;`{v:real^3}`]THEN ASSUME_TAC th)
128 THEN POP_ASSUM(fun th-> MRESA_TAC th [`e1:real^3->bool`;`{u:real^3}`])
129 THEN MRESA_TAC condition_not_edge_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`;`ds:real^3#real^3#real^3#real^3->bool`]
130 THEN FIND_ASSUM MP_TAC (`graph (E:(real^3->bool)->bool)`)
131 THEN REWRITE_TAC[GRAPH]
133 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `e1:real^3->bool`[HAS_SIZE])
134 THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
135 THEN POP_ASSUM MP_TAC
136 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
138 THEN MRESA_TAC properties_edges_eq_fan[`e1:real^3->bool`; `v:real^3`;`u:real^3`]
139 THENL[MP_TAC(SET_RULE`~(v IN e1)==> e1 INTER {v:real^3}={} /\ e1 INTER {v, u}=e1 INTER {u}`)
141 THEN ASSUME_TAC(SET_RULE`{} SUBSET e1 INTER {u}:real^3->bool`)
142 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} (e1 INTER {u})`)
144 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`e1 INTER {u}:real^3->bool`]
145 THEN POP_ASSUM MP_TAC THEN SET_TAC[];
146 MP_TAC(SET_RULE`~(u IN e1)==> e1 INTER {u:real^3}={} /\ e1 INTER {v, u}=e1 INTER {v}`)
148 THEN ASSUME_TAC(SET_RULE`{} SUBSET e1 INTER {v}:real^3->bool`)
149 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} (e1 INTER {v})`)
151 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`e1 INTER {v}:real^3->bool`]
152 THEN POP_ASSUM MP_TAC THEN SET_TAC[]]]);;
158 let condition_not_intersection_point_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds:real^3#real^3#real^3#real^3->bool e1:real^3->bool w:real^3.
159 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
160 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
162 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
163 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
164 /\ w IN V /\ e1 = {v, u}
165 ==>aff_ge {x} e1 INTER aff_ge {x} {w} = aff_ge {x} (e1 INTER {w})`,
167 THEN ASM_REWRITE_TAC[]
168 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
169 THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
170 THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
172 THEN POP_ASSUM MP_TAC
173 THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
175 THEN SUBGOAL_THEN`aff_ge {x} {w} SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
177 REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
178 THEN REPEAT STRIP_TAC
179 THEN MRESA_TAC exists_edge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` w:real^3`]
180 THEN EXISTS_TAC `{w,v'}:real^3->bool`
181 THEN ASM_REWRITE_TAC[]
182 THEN REMOVE_ASSUM_TAC
183 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v':real^3)`;
185 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(w:real^3)`;` (v':real^3)`]
186 THEN ASM_TAC THEN SET_TAC[IN];
187 MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} {w} SUBSET xfan (x,V,E)
188 ==> aff_gt {x} {v, u} INTER aff_ge {x} {w}={}`)
190 THEN MP_TAC(SET_RULE`
191 aff_gt {x:real^3} {v, u} INTER aff_ge {x} {w}={}==>
192 (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u}) INTER aff_ge {x} {w}
193 = (aff_ge {x} {w} INTER aff_ge {x} {v}) UNION (aff_ge {x} {w} INTER aff_ge {x} {u})`)
195 THEN MP_TAC(SET_RULE`w IN V==> {w} IN E UNION {{v:real^3} | v IN V}`)
197 THEN MP_TAC(SET_RULE`v:real^3 IN V==> {v} IN E UNION {{v} | v IN V}`)
199 THEN MP_TAC(SET_RULE`u:real^3 IN V==> {u} IN E UNION {{v} | v IN V}`)
201 THEN FIND_ASSUM MP_TAC(`FAN(x:real^3,V,E)`)
202 THEN REWRITE_TAC[FAN;fan7]
204 THEN POP_ASSUM(fun th-> MRESA_TAC th [`{w}:real^3->bool`;`{v:real^3}`]THEN ASSUME_TAC th)
205 THEN POP_ASSUM(fun th-> MRESA_TAC th [`{w}:real^3->bool`;`{u:real^3}`])
206 THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
207 THEN POP_ASSUM MP_TAC
208 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
210 THEN MP_TAC(SET_RULE`~(v=u:real^3)==> ({v, u} INTER {w}= {w} INTER {v} /\ {w} INTER {u}={}) \/ ({v, u} INTER {w}= {w} INTER {u} /\ {w} INTER {v}={})`)
212 THENL[ ASSUME_TAC(SET_RULE`{} SUBSET {w} INTER {v}:real^3->bool`)
213 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} ({w} INTER {v})`)
215 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`{w} INTER {v}:real^3->bool`]
216 THEN POP_ASSUM MP_TAC THEN SET_TAC[];
217 ASSUME_TAC(SET_RULE`{} SUBSET {w} INTER {u}:real^3->bool`)
218 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} ({w} INTER {u})`)
220 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`{w} INTER {u}:real^3->bool`]
221 THEN POP_ASSUM MP_TAC THEN SET_TAC[]]]);;
225 let DWWUTKW=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds.
226 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
227 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
229 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
230 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
231 /\ E1=E UNION {{v,u}}
234 THEN FIND_ASSUM MP_TAC`FAN(x:real^3,V,E)`
235 THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7]
237 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
238 THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
239 THEN POP_ASSUM MP_TAC
240 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
242 THEN MRESA_TAC add_edge_graph_fan[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
243 THEN MRESA_TAC garph_add_edge_is_garph[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
244 THEN MRESA_TAC add_edge_into_collinear_fan[`x:real^3`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
245 THEN REWRITE_TAC[UNION;IN_ELIM_THM;IN_SING]
248 THENL[ REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
249 THEN POP_ASSUM MATCH_MP_TAC
250 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];
252 MRESA_TAC condition_not_intersection_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e1:real^3->bool`;`e2:real^3->bool`];
254 REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
255 THEN POP_ASSUM MATCH_MP_TAC
256 THEN POP_ASSUM MP_TAC
257 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];
259 MRESA_TAC condition_not_intersection_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e2:real^3->bool`;`e1:real^3->bool`]
260 THEN ASM_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`];
262 ASM_REWRITE_TAC[SET_RULE`A INTER A=A`];
264 MRESA_TAC condition_not_intersection_point_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e1:real^3->bool`;`v':real^3`];
266 REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e2:real^3->bool`;`e1:real^3->bool`])
267 THEN ASM_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`]
268 THEN POP_ASSUM MATCH_MP_TAC
269 THEN POP_ASSUM MP_TAC
270 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];
272 MRESA_TAC condition_not_intersection_point_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e2:real^3->bool`;`v':real^3`]
273 THEN ASM_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`];
275 REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
276 THEN POP_ASSUM MATCH_MP_TAC
277 THEN POP_ASSUM MP_TAC
278 THEN POP_ASSUM MP_TAC
279 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);;