1 module Nkezbfc_local = struct
19 open Prove_by_refinement;;
20 open Wrgcvdr_cizmrrh;;
32 (* deprecated 2013-02-22
33 let sol_local_fan = new_definition ` sol_local_fan V E f= &2 * pi+ sum f (\e. azim_in_fan e E- pi)`;;
36 let sol_local = new_definition ` sol_local E f= &2 * pi+ sum f (\e. azim_in_fan e E- pi)`;;
39 let CONVEX_LOFA_IMP_INANGLE_EQ_AZIM = prove_by_refinement
40 (`convex_local_fan (V,E,FF) ==>(!v. v IN V ==> interior_angle1 (vec 0) FF v = azim_in_fan (v, rho_node1 FF v) E) `,
41 [REWRITE_TAC[convex_local_fan; azim_in_fan2];
43 ASSUME_TAC2 EXISTS_INVERSE_OF_V;
45 ASSUME_TAC2 LOFA_IMP_EE_TWO_ELMS;
46 ASSUME_TAC2 LOFA_CARD_EE_V_1;
47 ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2;
49 UNDISCH_TAC` v:real^3 IN V `;
51 UNDISCH_TAC` !x. x IN FF
52 ==> (let d = azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x) in
53 if CARD (EE (FST x) E) > 1
54 then azim (vec 0) (FST x) (SND x) d
57 V SUBSET wedge_in_fan_ge x E`;
60 SWITCH_TAC` EE v E = {rho_node1 FF v, vv} `;
61 ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `];
63 DOWN THEN DOWN THEN PHA;
64 ASSUME_TAC2 (SPEC `vv:real^3 ` (GEN` v:real^3 ` IVS_RHO_IDD));
67 UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `;
68 DISCH_THEN (SUBST1_TAC o SYM);
71 SIMP_TAC[interior_angle1; GSYM ivs_rho_node1; AZIM_CYCLE_TWO_POINT_SET]]);;
75 let SOL_LOFA_EQ_SUM_INANGLE=prove_by_refinement(` convex_local_fan(V,E,FF)
76 ==> sol_local E FF= &2 * pi + sum V (\v. interior_angle1 (vec 0) FF v -pi)`,
77 [REWRITE_TAC[sol_local;]
79 THEN POP_ASSUM(fun th-> MP_TAC th THEN
80 REWRITE_TAC[convex_local_fan] THEN STRIP_TAC
82 THEN MRESAL_TAC (GEN_ALL WRGCVDR)[`E:(real^3->bool)->bool`;`(\x:real^3#real^3. FST x)`;`FF:(real^3#real^3)->bool`;`V:real^3->bool`;`hro:real^3->real^3`][REAL_ARITH`&2 * pi + A= &2 * pi + B<=> A=B`;BIJ;INJ;SURJ]
83 THEN MATCH_MP_TAC SUM_EQ_GENERAL
84 THEN EXISTS_TAC`(\x:real^3#real^3. FST x)`
85 THEN ASM_REWRITE_TAC[]
92 ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS
95 THEN POP_ASSUM(fun th-> MRESA1_TAC th `x:real^3#real^3`)
96 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th;])
97 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_IN_V2
98 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
99 THEN POP_ASSUM(fun th-> MRESA1_TAC th `FST (x:real^3#real^3)`)]);;
103 let CARD_VERTEX_GE_3_LOCAL_FAN=prove_by_refinement(`!V E FF. convex_local_fan(V,E,FF)
107 THEN POP_ASSUM(fun th-> MP_TAC th THEN
108 REWRITE_TAC[convex_local_fan] THEN STRIP_TAC
110 THEN SUBGOAL_THEN`?v:real^3. v IN V`ASSUME_TAC;
112 THEN SIMP_TAC[convex_local_fan;local_fan;FAN;fan1;SET_RULE`~(V SUBSET {}) <=> ~(V= {})`;SET_RULE`~(V={}) <=> ?v. v IN V`]
118 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
119 THEN REMOVE_ASSUM_TAC
120 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
121 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
122 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`rho_node1 FF v` ;`V:real^3->bool`]
123 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
124 THEN REMOVE_ASSUM_TAC
125 THEN POP_ASSUM(fun th-> MRESA1_TAC th `rho_node1 FF v:real^3`)
126 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
127 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v)` ;`V:real^3->bool`]
128 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
129 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v:real^3`;]
130 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
131 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF v:real^3`;]
132 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v:real^3`]
133 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, v:real^3} {rho_node1 FF v}==> ~(v=rho_node1 FF v)`)
135 THEN MRESA_TAC th3[`vec 0:real^3`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v):real^3`]
136 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, rho_node1 FF v:real^3} {rho_node1 FF (rho_node1 FF v)}==> ~(rho_node1 FF v=rho_node1 FF(rho_node1 FF v))`)
138 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE
139 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
140 THEN SUBGOAL_THEN(`CARD {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}=3`)ASSUME_TAC;
142 SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
143 IN_INSERT; NOT_IN_EMPTY]
144 THEN ASM_REWRITE_TAC[]
146 MP_TAC(SET_RULE`rho_node1 FF v IN V /\ v IN V /\ rho_node1 FF (rho_node1 FF v) IN V==> {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3} SUBSET V`)
149 THEN REWRITE_TAC[local_fan;FAN;fan1]
151 THEN REPEAT STRIP_TAC
152 THEN MRESA_TAC CARD_SUBSET[`{v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}`;`V:real^3->bool`]]);;
157 let REP_VERTEX_3_LOCAL_FAN=prove_by_refinement(` CARD V=3 /\ convex_local_fan(V,E,FF)
158 ==> ?v. V= {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v)}
159 /\ ~(v=rho_node1 FF v) /\ ~(rho_node1 FF v=rho_node1 FF (rho_node1 FF v))/\
160 ~(rho_node1 FF (rho_node1 FF v)=v)`,
163 THEN POP_ASSUM(fun th-> MP_TAC th THEN
164 REWRITE_TAC[convex_local_fan] THEN STRIP_TAC
166 THEN SUBGOAL_THEN`?v:real^3. v IN V`ASSUME_TAC;
168 THEN SIMP_TAC[convex_local_fan;local_fan;FAN;fan1;SET_RULE`~(V SUBSET {}) <=> ~(V= {})`;SET_RULE`~(V={}) <=> ?v. v IN V`]
173 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
174 THEN REMOVE_ASSUM_TAC
175 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
176 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
177 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`rho_node1 FF v` ;`V:real^3->bool`]
178 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
179 THEN REMOVE_ASSUM_TAC
180 THEN POP_ASSUM(fun th-> MRESA1_TAC th `rho_node1 FF v:real^3`)
181 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
182 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v)` ;`V:real^3->bool`]
183 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
184 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v:real^3`;]
185 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
186 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF v:real^3`;]
187 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v:real^3`]
188 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, v:real^3} {rho_node1 FF v}==> ~(v=rho_node1 FF v)`)
190 THEN MRESA_TAC th3[`vec 0:real^3`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v):real^3`]
191 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, rho_node1 FF v:real^3} {rho_node1 FF (rho_node1 FF v)}==> ~(rho_node1 FF v=rho_node1 FF(rho_node1 FF v))`)
193 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE
194 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
195 THEN SUBGOAL_THEN(`CARD {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}=3`)ASSUME_TAC;
196 SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
197 IN_INSERT; NOT_IN_EMPTY]
198 THEN ASM_REWRITE_TAC[]
201 MP_TAC(SET_RULE`rho_node1 FF v IN V /\ v IN V /\ rho_node1 FF (rho_node1 FF v) IN V==> {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3} SUBSET V`)
204 THEN REWRITE_TAC[local_fan;FAN;fan1]
206 THEN REPEAT STRIP_TAC
207 THEN MRESA_TAC CARD_SUBSET_EQ[`{v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}`;`V:real^3->bool`]
208 THEN EXISTS_TAC`v:real^3`
209 THEN ASM_REWRITE_TAC[]
211 THEN REPEAT RESA_TAC]);;
214 let CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS = prove(`convex_local_fan (V,E,FF) ==>(!v. v IN V ==> interior_angle1 (vec 0) FF v = azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v)) `,
216 REWRITE_TAC[convex_local_fan; azim_in_fan2]
217 THEN REPEAT STRIP_TAC
218 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
219 THEN DOWN THEN STRIP_TAC
220 THEN ASSUME_TAC2 LOFA_IMP_EE_TWO_ELMS
221 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
222 THEN ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2
223 THEN DOWN THEN STRIP_TAC
224 THEN UNDISCH_TAC` v:real^3 IN V `
225 THEN FIRST_ASSUM NHANH
226 THEN UNDISCH_TAC` !x. x IN FF
227 ==> (let d = azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x) in
228 if CARD (EE (FST x) E) > 1
229 then azim (vec 0) (FST x) (SND x) d
232 V SUBSET wedge_in_fan_ge x E`
233 THEN DISCH_THEN NHANH
235 THEN SWITCH_TAC` EE v E = {rho_node1 FF v, vv} `
236 THEN ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `]
238 THEN DOWN THEN DOWN THEN PHA
239 THEN ASSUME_TAC2 (SPEC `vv:real^3 ` (GEN` v:real^3 ` IVS_RHO_IDD))
242 THEN UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `
243 THEN DISCH_THEN (SUBST1_TAC o SYM)
246 THEN SIMP_TAC[interior_angle1; GSYM ivs_rho_node1; AZIM_CYCLE_TWO_POINT_SET]);;
248 let SOL_LOCAL_FAN_POS_CASE3=prove(`!V E FF. convex_local_fan(V,E,FF)
250 ==> &0 <= sol_local E FF`,
252 THEN ASSUME_TAC2 SOL_LOFA_EQ_SUM_INANGLE
253 THEN ASM_REWRITE_TAC[]
254 THEN ASSUME_TAC2 REP_VERTEX_3_LOCAL_FAN
255 THEN POP_ASSUM MP_TAC
257 THEN SIMP_TAC[HAS_SIZE; SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
258 IN_INSERT; NOT_IN_EMPTY]
259 THEN ASM_REWRITE_TAC[]
260 THEN UNDISCH_TAC`convex_local_fan (V:real^3->bool,E,FF)`
262 THEN POP_ASSUM( fun th-> MP_TAC th
263 THEN REWRITE_TAC[convex_local_fan ] THEN ASSUME_TAC th)
265 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;][SET_RULE`A IN {A,B,C}`]
266 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF v:real^3`;][SET_RULE`B IN {A,B,C}`]
267 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF (rho_node1 FF v):real^3`;][SET_RULE`C IN {A,B,C}`]
268 THEN DISJ_CASES_TAC(SET_RULE`(?v. v IN V /\ pi <= interior_angle1 (vec 0) FF v)\/ ~(?v. v IN V /\ pi <= interior_angle1 (vec 0) FF v)`)
272 THEN ASM_REWRITE_TAC[SET_RULE`A IN {B,C,D}<=> A=B \/ A=C\/ A=D`]
274 THEN POP_ASSUM MP_TAC
275 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
276 THEN POP_ASSUM MP_TAC
277 THEN POP_ASSUM MP_TAC
278 THEN POP_ASSUM MP_TAC
281 THEN POP_ASSUM MP_TAC
282 THEN POP_ASSUM MP_TAC
283 THEN POP_ASSUM MP_TAC
284 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM; REAL_ARITH`~(a<= b) <=> b<a`]
285 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
286 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`A IN {A,B,C}`]
287 THEN MRESAL1_TAC th`rho_node1 FF v:real^3`[SET_RULE`B IN {A,B,C}`]
288 THEN MRESAL1_TAC th`rho_node1 FF (rho_node1 FF v:real^3)`[SET_RULE`C IN {A,B,C}`])
289 THEN MRESAL_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;][SET_RULE`A IN {A,B,C}`]
290 THEN MRESAL_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF v:real^3`;][SET_RULE`B IN {A,B,C}`]
291 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
292 THEN REMOVE_ASSUM_TAC
293 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `rho_node1 FF (rho_node1 FF v):real^3`[SET_RULE`C IN {A,B,C}`])
294 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
295 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF (rho_node1 FF v):real^3`;][SET_RULE`C IN {A,B,C}`]
296 THEN MRESA_TAC th3[`vec 0:real^3`;`rho_node1 FF (rho_node1 FF v):real^3`;`rho_node1 FF (rho_node1 FF (rho_node1 FF v)):real^3`]
297 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, rho_node1 FF (rho_node1 FF v):real^3} {rho_node1 FF (rho_node1 FF (rho_node1 FF v))}==> ~(rho_node1 FF (rho_node1 FF v)=rho_node1 FF (rho_node1 FF (rho_node1 FF v)))`)
299 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
300 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (rho_node1 FF v):real^3`;`rho_node1 FF (rho_node1 FF (rho_node1 FF v))` ;`V:real^3->bool`][SET_RULE`C IN {A,B,C}`]
301 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
302 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `rho_node1 FF v:real^3`[SET_RULE`B IN {A,B,C}`])
303 THEN MP_TAC(SET_RULE`~(rho_node1 FF (rho_node1 FF v) =
304 rho_node1 FF (rho_node1 FF (rho_node1 FF v:real^3)))
305 /\ rho_node1 FF (rho_node1 FF (rho_node1 FF v)) IN
306 {v, rho_node1 FF v, rho_node1 FF (rho_node1 FF v)}
307 /\ ~(rho_node1 FF (rho_node1 FF (rho_node1 FF v)) = rho_node1 FF v)
308 ==> rho_node1 FF (rho_node1 FF (rho_node1 FF v))=v
311 THEN MRESAL_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (rho_node1 FF v):real^3`;][SET_RULE`C IN {A,B,C}`]
312 THEN ABBREV_TAC`u=rho_node1 FF v`
313 THEN ABBREV_TAC`w=rho_node1 FF u`
314 THEN REPEAT STRIP_TAC
315 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`A IN {A,B,C}`]
316 THEN MRESAL1_TAC th`u:real^3`[SET_RULE`B IN {A,B,C}`]
317 THEN MRESAL1_TAC th`w:real^3`[SET_RULE`C IN {A,B,C}`;])
318 THEN REWRITE_TAC[REAL_ARITH`&0 <=
319 &2 * pi + A - pi + B - pi + C - pi + &0 <=> &0 <= A+B+C - pi `]
320 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
321 THEN REMOVE_ASSUM_TAC
322 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `v:real^3`[SET_RULE`A IN {A,B,C}`]
323 THEN MRESAL1_TAC th `u:real^3`[SET_RULE`B IN {A,B,C}`])
324 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
325 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v:real^3`;][SET_RULE`A IN {A,B,C}`]
326 THEN UNDISCH_TAC`~collinear {vec 0, w:real^3, rho_node1 FF w}`
327 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
329 THEN MP_TAC(REAL_ARITH`&0< azim (vec 0) v u w /\ azim (vec 0) v u w < pi ==> ~(azim (vec 0) v u w = &0 \/ azim (vec 0) v u (w:real^3) = pi)`)
331 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
332 THEN POP_ASSUM (fun th->
333 MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
335 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
337 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
339 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
342 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
343 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
344 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
345 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`]
346 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
347 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
348 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
349 THEN MRESAL_TAC VOLUME_SOLID_TRIANGLE[`&1:real`;`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`][REAL_ARITH`&0< &1`]
350 THEN POP_ASSUM MP_TAC
352 THEN MRESA_TAC MEASURABLE_BALL_AFF_GT[`vec 0:real^3`;`&1`;`{vec 0:real^3}`;`{v,u,w:real^3}`]
354 THEN MP_TAC(MESON[volume_props]`measurable (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w})==> vol (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w}) >= &0`)
356 THEN POP_ASSUM MP_TAC
357 THEN REAL_ARITH_TAC]);;
360 let AFF_LT_1_1 = prove
367 y = t1 % x + t2 % w}`,
368 REWRITE_TAC[SET_RULE`~(x=w) <=> DISJOINT {x} {w}`] THEN AFF_TAC);;
370 let PROPERTIES_GENERIC_LOCAL_FAN=prove_by_refinement(`!V E FF v0. local_fan(V,E,FF) /\ v0 IN V /\ generic V E
371 ==> (!v. v IN V /\ ~(v = v0) ==> ~collinear {vec 0, v0, v})`,
373 THEN REWRITE_TAC[generic;]
375 THEN POP_ASSUM MP_TAC
376 THEN DISCH_THEN(LABEL_TAC"LINH")
377 THEN REPEAT STRIP_TAC
378 THEN MRESA_TAC(GEN_ALL LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;]
379 THEN REMOVE_ASSUM_TAC
380 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v0:real^3`)
381 THEN MRESAL_TAC(GEN_ALL LOCAL_FAN_IN_FF_IN_ORD_PAIRS)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`v0,rho_node1 FF v0`;`E:(real^3->bool)->bool`;][GSYM IN_E_IFF_IN_ORD_E]
382 THEN REMOVE_THEN "LINH"(fun th-> MRESA_TAC th[`v0:real^3`;`rho_node1 FF v0`;`v:real^3`])
383 THEN POP_ASSUM MP_TAC
384 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?w. w IN A`]
385 THEN POP_ASSUM MP_TAC
386 THEN POP_ASSUM MP_TAC
387 THEN POP_ASSUM MP_TAC
388 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
389 THEN REWRITE_TAC[COLLINEAR_3_EXPAND;VECTOR_ARITH`u % vec 0+ a=a`]
390 THEN REPEAT STRIP_TAC;
392 THEN REWRITE_TAC[local_fan;FAN;fan2]
396 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= &1-u \/ &1 -u< &0`);
397 SUBGOAL_THEN`~(vec 0= v0:real^3)`ASSUME_TAC;
399 THEN REWRITE_TAC[local_fan;FAN;fan2]
402 SUBGOAL_THEN`~(vec 0= v:real^3)`ASSUME_TAC;
404 THEN REWRITE_TAC[local_fan;FAN;fan2]
407 SUBGOAL_THEN`v IN aff_ge {vec 0} {v0:real^3}` ASSUME_TAC;
408 MRESAL_TAC AFF_GE_1_1[`vec 0:real^3`;`v0:real^3`][IN_ELIM_THM]
409 THEN EXISTS_TAC `u:real`
410 THEN EXISTS_TAC `&1-u:real`
411 THEN ASM_REWRITE_TAC[REAL_ARITH`u+ &1- u= &1`]
412 THEN VECTOR_ARITH_TAC;
413 SUBGOAL_THEN`v IN aff_ge {vec 0} {v:real^3}` ASSUME_TAC;
414 MRESAL_TAC AFF_GE_1_1[`vec 0:real^3`;`v:real^3`][IN_ELIM_THM]
415 THEN EXISTS_TAC `&0:real`
416 THEN EXISTS_TAC `&1:real`
417 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 + &1= &1 /\ &0<= &1`]
418 THEN VECTOR_ARITH_TAC;
419 UNDISCH_TAC`local_fan (V:real^3->bool,E,FF)`
420 THEN REWRITE_TAC[local_fan;FAN;fan7]
423 THEN REMOVE_ASSUM_TAC
424 THEN REMOVE_ASSUM_TAC
425 THEN REMOVE_ASSUM_TAC
426 THEN UNDISCH_TAC `v=(&1 - u) % v0:real^3`
427 THEN MP_TAC(SET_RULE`~(v = (v0:real^3))==> {v} INTER {v0}= {}`)
428 THEN ASM_REWRITE_TAC[]
429 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{v:real^3}`;`{v0:real^3}`][UNION;IN_ELIM_THM;SET_RULE`(?v. v IN V /\ {v0} = {v})<=> v0 IN V`])
431 THEN UNDISCH_TAC`aff_ge {vec 0} {v} INTER aff_ge {vec 0} {v0} =
432 aff_ge {vec 0} ({v} INTER {v0:real^3})`
433 THEN ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]
435 THEN MP_TAC(SET_RULE`v IN aff_ge {vec 0} {v0}/\ v IN aff_ge {vec 0} {v:real^3}
436 /\ aff_ge {vec 0} {v} INTER aff_ge {vec 0} {v0} = {vec 0} ==> vec 0= v`)
437 THEN ASM_REWRITE_TAC[];
438 MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v0:real^3`;]
439 THEN MRESA_TAC Planarity.point_in_aff_ge[`vec 0:real^3`;`v0:real^3`;`rho_node1 FF v0`]
440 THEN EXISTS_TAC`v0:real^3`
441 THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM]
442 THEN SUBGOAL_THEN`~(vec 0= v:real^3)`ASSUME_TAC;
444 THEN REWRITE_TAC[local_fan;FAN;fan2]
449 THEN MRESAL_TAC AFF_LT_1_1[`vec 0:real^3`;`(&1 - u) % v0:real^3`][IN_ELIM_THM]
450 THEN EXISTS_TAC `&1- inv(&1-u):real`
451 THEN EXISTS_TAC `inv(&1-u):real`
452 THEN ASM_REWRITE_TAC[REAL_ARITH`&1-a+a= &1`; VECTOR_ARITH`a %b%v=(a*b)%v`]
453 THEN MP_TAC(REAL_ARITH`&1- u< &0 ==> ~(&1- u = &0)`)
455 THEN MRESA1_TAC REAL_MUL_LINV`&1- u:real`
456 THEN REWRITE_TAC[VECTOR_ARITH`v0 = (&1 - inv (&1 - u)) % vec 0 + &1 % v0`;REAL_ARITH`a< &0<=> &0< -- a`;GSYM REAL_INV_NEG;REAL_LT_INV_EQ]
458 THEN REAL_ARITH_TAC]);;
460 let PROPERTIES_GENERIC= prove(` local_fan(V,E,FF) /\ generic V E /\ v IN V /\ w IN V
461 ==> (!u u1. u IN {v,w} /\ u1 IN V /\ ~(u=u1) ==> ~(collinear {vec 0, u, u1}))`,
462 REWRITE_TAC[SET_RULE`u IN {v,w} <=> u=v \/ u=w`]
463 THEN REPEAT STRIP_TAC
464 THEN ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN]);;
466 let PROPERTIES_GENERIC1= prove(` convex_local_fan(V,E,FF) /\ generic V E /\ v IN V /\ w IN V
467 ==> (!u u1. u IN {v,w} /\ u1 IN V /\ ~(u=u1) ==> ~(collinear {vec 0, u, u1}))`,
468 REWRITE_TAC[SET_RULE`u IN {v,w} <=> u=v \/ u=w`;convex_local_fan]
469 THEN REPEAT STRIP_TAC
470 THEN ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN;]);;
473 let AZIM_PI_WEDGE_SIN = prove_by_refinement(` azim u v w ww = pi ==>
474 wedge u v w ww = {x| &0 < sin (azim u v w x ) } `,
475 [REWRITE_TAC[wedge; EXTENSION; IN_ELIM_THM]
476 THEN ONCE_REWRITE_TAC[GSYM (SPEC ` -- (u:real^3) ` AZIM_TRANSLATION)]
477 THEN REWRITE_TAC[VECTOR_ARITH` -- a + (a:real^N) = vec 0`;VECTOR_ARITH` -- a + b = b - a:real^N `; re_eqvl]
478 THEN REPEAT STRIP_TAC
479 THEN ASM_REWRITE_TAC[]
481 SIMP_TAC[SIN_POS_PI];
482 MP_TAC (SPECL [`u - u:real^3 `;` v - u:real^3 `;` w - u:real^3 `;
483 ` x - u:real^3 `] AZIM_RANGE)
485 THEN ABBREV_TAC ` goc = azim (u - u) (v - u) (w - u) (x - u) `
486 THEN MP_TAC(REAL_ARITH`&0 <= goc==> goc= &0 \/ &0< goc `)
488 ASM_REWRITE_TAC[SIN_0]
491 THEN ASM_CASES_TAC `collinear {u, v, x:real^3}`;
492 MRESA_TAC azim_def[`w:real^3`;`x:real^3`;`v:real^3`;`u:real^3`]
493 THEN POP_ASSUM MP_TAC
494 THEN ONCE_REWRITE_TAC[GSYM (SPEC ` -- (u:real^3) ` AZIM_TRANSLATION)]
495 THEN REWRITE_TAC[VECTOR_ARITH` -- a + (a:real^N) = vec 0`;VECTOR_ARITH` -- a + b = b - a:real^N `; re_eqvl]
497 THEN ASM_REWRITE_TAC[SIN_0]
501 THEN ASM_CASES_TAC ` goc < pi `
502 THEN ASM_REWRITE_TAC[]
503 THEN SUBGOAL_THEN` sin goc < &0 ` MP_TAC;
504 ONCE_REWRITE_TAC[SIN_SUB_PERIODIC]
505 THEN REWRITE_TAC[REAL_ARITH` -- a < &0 <=> &0 < a `]
506 THEN MATCH_MP_TAC SIN_POS_PI
508 ASM_REWRITE_TAC[REAL_ARITH` a - b < b <=> a < &2 * b `;REAL_ARITH` &0 < a - pi <=> ~( a < pi ) /\ ~(a= pi) `]
510 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th; SIN_PI])
512 ASM_TAC THEN REAL_ARITH_TAC]);;
517 let AZIM_PI_WEDGE_CROSS_DOT = prove_by_refinement(` azim u v w ww = pi ==>
518 wedge u v w ww = {x | &0 < ((v - u) cross ( w - u )) dot ( x - u )}`,
519 [SIMP_TAC[AZIM_PI_WEDGE_SIN; EXTENSION; IN_ELIM_THM];
521 ONCE_REWRITE_TAC[GSYM (SPEC ` -- (u:real^3) ` AZIM_TRANSLATION)];
522 REWRITE_TAC[VECTOR_ARITH` -- a + a:real^N = vec 0 `; VECTOR_ARITH` -- a + x = x - a:real^N `];
523 MP_TAC (SPECL [` v - u:real^3 `;` w - u:real^3 `;` x - u:real^3 `] Trigonometry2.JBDNJJB);
524 REWRITE_TAC[re_eqvl];
526 ASM_REWRITE_TAC[VECTOR_SUB_REFL];
527 ASM_SIMP_TAC[REAL_LT_MUL_EQ]]);;
530 let AFF_GT_SUBSET_WEDGE_IMP_VERTEX=prove(`!x v w y z. ~collinear{x,v,w}
533 /\ aff_gt {x} {v,w} SUBSET wedge x v y z
534 ==> w IN wedge x v y z`,
536 THEN MRESA_TAC Planarity.exists_in_aff_gt[`x:real^3`;`v:real^3`;`w:real^3`]
537 THEN MP_TAC(SET_RULE`y' IN aff_gt {x} {v, w} /\ aff_gt {x:real^3} {v, w} SUBSET wedge x v y z ==> y' IN wedge x v y z`)
538 THEN MRESA_TAC th3[`x:real^3`;`v:real^3`;`w:real^3`]
539 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
540 THEN MRESA_TAC Planarity.aff_gt_inter_aff_gt[`x:real^3`;`v:real^3`;`w:real^3`]
541 THEN UNDISCH_TAC`y' IN aff_gt {x} {v, w:real^3}`
542 THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM]
544 THEN MRESA_TAC Planarity.aff_gt_imp_not_collinear[`x:real^3`;`w:real^3`;`v:real^3`;`y':real^3`]
545 THEN MRESA_TAC AZIM_EQ[`x:real^3`;`v:real^3`;`y:real^3`;`w:real^3`;`y':real^3`]
548 let CONDITION_INANGLE_CROSS_DOT=prove(` aff_gt {x} {v,w} SUBSET wedge x v y z
552 /\ u= (v-x) cross (w-x)
554 ==> &0 < ((v - x) cross (y - x)) dot (w - x)/\
555 &0 < ((v - x) cross (w - x)) dot (z - x)`,
557 THEN MRESA_TAC (AFF_GT_SUBSET_WEDGE_IMP_VERTEX)[`x:real^3`;`v:real^3`;`w:real^3`;`y:real^3`;`z:real^3`]
558 THEN POP_ASSUM MP_TAC
559 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
561 THEN MP_TAC(REAL_ARITH`azim x v y w < azim x v y z /\ azim x v y z < pi
562 ==> azim x v y w < pi /\ azim x v y w <= azim x v y z`)
564 THEN MRESA1_TAC SIN_POS_PI`azim x v y w`
565 THEN POP_ASSUM MP_TAC
566 THEN MRESA_TAC Fan.sum4_azim_fan[`x:real^3`;`v:real^3`;`y:real^3`;`w:real^3`;`z:real^3`]
567 THEN MP_TAC(REAL_ARITH`azim x v y w < azim x v y z /\ &0< azim x v y w
568 /\ azim x v y z < pi /\ azim x v y z = azim x v y w + azim x v w z
569 ==> &0< azim x v w z /\ azim x v w z< pi`)
571 THEN MRESA1_TAC SIN_POS_PI`azim x v w z`
572 THEN POP_ASSUM MP_TAC
573 THEN ONCE_REWRITE_TAC[GSYM (SPEC ` -- (x:real^3) ` AZIM_TRANSLATION)]
574 THEN REWRITE_TAC[VECTOR_ARITH` -- a + (a:real^N) = vec 0`;VECTOR_ARITH` -- a + b = b - a:real^N `; re_eqvl]
575 THEN MP_TAC (SPECL [` v - x:real^3 `;` w - x:real^3 `;` z - x:real^3 `] Trigonometry2.JBDNJJB)
576 THEN REWRITE_TAC[re_eqvl;VECTOR_ARITH`a-a= vec 0`]
577 THEN MP_TAC (SPECL [` v - x:real^3 `;` y - x:real^3 `;` w - x:real^3 `] Trigonometry2.JBDNJJB)
578 THEN REWRITE_TAC[re_eqvl;]
581 THEN REPEAT STRIP_TAC
582 THEN MP_TAC REAL_LT_MUL_EQ
584 THEN REMOVE_ASSUM_TAC
585 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t:real`;`((v - x) cross (y - x)) dot (w - x:real^3)`] THEN MRESA_TAC th[`t':real`;`(((v - x) cross (w - x)) dot (z - x:real^3))`]));;
587 let AFF_GE_3_1 = prove
590 ==> aff_ge {x,v,u} {w} =
593 t1 + t2 +t3 +t4 = &1 /\
594 y = t1 % x + t2 % v + t3 % u +t4 % w }`,
598 let AFF_GE_2_2=prove(`!x u v w.
599 DISJOINT {x, u} {v, w}
600 ==> aff_ge {x, u} {v, w} =
604 t1 + t2 + t3 +t4= &1 /\
605 y = t1 % x + t2 %u + t3 % v + t4 % w}`,
610 let inter_aff_ge_3_1_is_aff_ge_2_2=prove(`!x v u w:real^3.
613 aff_ge {x,v,u} {w} INTER aff_ge {x,u,w} {v} =aff_ge {x,u} {v,w}`,
614 GEOM_ORIGIN_TAC `x:real^3`
615 THEN REPEAT STRIP_TAC
616 THEN MRESA_TAC notcoplanar_disjoints[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
617 THEN MRESA_TAC notcoplanar_disjoint[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
618 THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
619 THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
620 THEN MRESA_TAC AFF_GE_2_2[`(vec 0):real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
621 THEN MRESA_TAC NOT_COPLANAR_0_4_IMP_INDEPENDENT[`v:real^3`;`u:real^3`;`w:real^3`]
622 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;INTER]
623 THEN REDUCE_VECTOR_TAC
628 THEN POP_ASSUM MP_TAC
629 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % v + t3 % u + t4 % w = t2' % u + t3' % w + t4' % v <=> (t2-t4') % v + (t3-t2') % u + (t4-t3') % w= vec 0`]
631 THEN MRESAL_TAC INDEPENDENT_3[`v:real^3`;`u:real^3`;`w:real^3`;`t2-t4':real`; `t3-t2':real`; `t4 -t3':real`][REAL_ARITH`A-B= &0<=> A=B`]
632 THEN REPEAT STRIP_TAC
633 THEN EXISTS_TAC`t1':real`
634 THEN EXISTS_TAC`t2':real`
635 THEN EXISTS_TAC`t4':real`
636 THEN EXISTS_TAC`t3':real`
637 THEN ASM_REWRITE_TAC[REAL_ARITH`t1+t2+t3+t4=t1+t2+t4+t3:real`;VECTOR_ARITH`t4' % v + t2' % u + t3' % w = t2' % u + t4' % v + t3' % w:real^3`]
644 THEN EXISTS_TAC`t3:real`
645 THEN EXISTS_TAC`t2:real`
646 THEN EXISTS_TAC`t4:real`
647 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % u + t3 % v + t4 % w = t3 % v + t2 % u + t4 % w:real^3`;REAL_ARITH`t1 + t3 + t2 + t4=t1 + t2 + t3 + t4`];
649 THEN EXISTS_TAC`t2:real`
650 THEN EXISTS_TAC`t4:real`
651 THEN EXISTS_TAC`t3:real`
652 THEN ASM_REWRITE_TAC[REAL_ARITH`t1 + t2 + t4+ t3:real=t1 + t2 + t3 + t4`]
653 THEN VECTOR_ARITH_TAC]]);;
656 let aff_ge_3_1_rep_cross_dot=prove(
657 `!x:real^3 v:real^3 u:real^3 w:real^3.
659 /\ &0< ((v-x) cross (u-x)) dot (w-x)
660 ==> aff_ge {x,v,u} {w} ={y:real^3| &0<= (((v-x) cross (u-x)) dot (y-x)) }`,
663 THEN POP_ASSUM MP_TAC
664 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
665 THEN MRESA_TAC notcoplanar_disjoints[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
666 THEN DISCH_THEN(LABEL_TAC"YEU")
667 THEN MRESA_TAC AFF_GE_3_1[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
668 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]
672 THEN ASM_REWRITE_TAC[VECTOR_ARITH`((t1 % x + t2 % v + t3 % u + t4 % w) - x)=((t1+t2+t3+t4) - &1) % x + t2 % (v-x) + t3 % (u-x) + t4 % (w - x)`; REAL_ARITH`&1- &1= &0`]
673 THEN REDUCE_VECTOR_TAC
674 THEN REWRITE_TAC[CROSS_LNEG;CROSS_LMUL;CROSS_LADD;CROSS_REFL;DOT_RMUL;DOT_RADD;DOT_CROSS_SELF;]
675 THEN REDUCE_ARITH_TAC
676 THEN MATCH_MP_TAC REAL_LE_MUL
677 THEN ASM_REWRITE_TAC[]
678 THEN ASM_TAC THEN REAL_ARITH_TAC;
679 DISCH_THEN(LABEL_TAC"ME")
680 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate) THEN RESA_TAC
681 THEN MRESA_TAC ORTHONORMAL_IMP_SPANNING[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3)( v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;]
682 THEN POP_ASSUM MP_TAC
683 THEN ASM_REWRITE_TAC[SPAN_3;EXTENSION]
684 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(x':real^3)-(x:real^3)`th) THEN ASSUME_TAC(th))
685 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)-(x:real^3)`th)THEN ASSUME_TAC(th))
686 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)-(x:real^3)`th)THEN ASSUME_TAC(th))
687 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(v:real^3)-(x:real^3)`th))
688 THEN REWRITE_TAC[SET_RULE`(a:real^3) IN (:real^3)`;IN_ELIM_THM;VECTOR_ARITH`A-B=C<=>A=C+B:real^3`]
689 THEN REPEAT STRIP_TAC
690 THEN ABBREV_TAC`e1=e1_fan x v u:real^3`
691 THEN ABBREV_TAC`e2=e2_fan x v u:real^3`
692 THEN ABBREV_TAC`e3=e3_fan x v u:real^3`
693 THEN REMOVE_THEN"YEU" MP_TAC
694 THEN MRESA_TAC ORTHONORMAL_CROSS[`e1:real^3`;`e2:real^3`;`e3:real^3`;]
695 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1 % x +
696 t2 % ((u' % e1 + v' % e2 + w' % e3) + x) +
697 t3 % ((u'' % e1 + v'' % e2 + w'' % e3) + x) +
698 t4 % ((u''' % e1 + v''' % e2 + w''' % e3) + x)
699 = (t2 * u' + t3 * u'' +t4 * u''') % e1 + (t2 * v'+t3*v''+ t4 * v''') % e2 + (t2 * w'+ t3 * w''+ t4 * w''') % e3 +(t1+t2+t3+t4) % x :real^3`;VECTOR_ARITH`((u' % e1 + v' % e2 + w' % e3) + x) - x=u' % e1 + v' % e2 + w' % e3`;CROSS_LMUL;CROSS_RMUL;CROSS_LADD;CROSS_RADD;CROSS_REFL;]
700 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
701 THEN ASM_REWRITE_TAC[]
702 THEN REDUCE_VECTOR_TAC
703 THEN FIND_ASSUM MP_TAC`orthonormal e1 e2 (e3:real^3)`
704 THEN REWRITE_TAC[orthonormal]
706 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LNEG]
707 THEN ONCE_REWRITE_TAC[DOT_SYM]
708 THEN ASM_REWRITE_TAC[]
709 THEN REDUCE_ARITH_TAC
710 THEN ABBREV_TAC`a1=vector[u':real;u'':real;u''':real]:real^3`
711 THEN ABBREV_TAC`a2=vector[v':real;v'':real;v''':real]:real^3`
712 THEN ABBREV_TAC`a3=vector[w':real;w'':real;w''':real]:real^3`
713 THEN ABBREV_TAC`A=vector[a1;a2;a3:real^3]:real^3^3`
714 THEN ABBREV_TAC`b=vector[u'''':real;v'''':real;w'''':real]:real^3`
716 THEN SUBGOAL_THEN`&0< det(A:real^3^3)`ASSUME_TAC
722 THEN REWRITE_TAC[DET_3;VECTOR_3]
723 THEN POP_ASSUM MP_TAC
725 MP_TAC(REAL_ARITH`&0< det (A:real^3^3)==> ~(det A= &0) /\ &0<= det (A:real^3^3)`) THEN RESA_TAC
726 THEN MRESA_TAC CRAMER[`A:real^3^3`;]
727 THEN POP_ASSUM MP_TAC
728 THEN REWRITE_TAC[SWAP_FORALL_THM]
730 THEN POP_ASSUM(fun th-> MRESA_TAC th[`b:real^3`])
731 THEN POP_ASSUM MP_TAC
732 THEN REWRITE_TAC[MESON[]
733 ` (!x. p(x) <=> x = a) <=> (?x. p(x)) /\ (!x. p(x) ==> x = a)`]
735 THEN POP_ASSUM MP_TAC
736 THEN POP_ASSUM MP_TAC
737 THEN DISCH_THEN(LABEL_TAC "LINH1")
738 THEN DISCH_THEN(LABEL_TAC "LINH2")
739 THEN REMOVE_THEN "LINH1" MP_TAC
740 THEN MRESAL_TAC MATRIX_VECTOR_MUL_COMPONENT[`A:real^3^3`;`x'':real^3`][DIMINDEX_3]
741 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1:num`[ARITH_RULE`1<=1/\ 1<=3`;LAMBDA_BETA;VECTOR_3] THEN ASSUME_TAC th)
742 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`2:num`[ARITH_RULE`1<=2/\ 2<=3`;VECTOR_3] THEN ASSUME_TAC th)
743 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`1<=3/\ 3<=3`;VECTOR_3;])
745 THEN POP_ASSUM(fun th -> MP_TAC th THEN ASSUME_TAC th)
746 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[VECTOR_3;CART_EQ;]
747 THEN REWRITE_TAC[DIMINDEX_3]
749 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1:num`[ARITH_RULE`1<=1/\ 1<=3`;DOT_SYM;] THEN ASSUME_TAC th)
750 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`2:num`[ARITH_RULE`1<=2/\ 2<=3`;DOT_SYM;] THEN ASSUME_TAC th)
751 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`1<=3/\ 3<=3`;DOT_SYM;])
752 THEN POP_ASSUM MP_TAC
753 THEN POP_ASSUM MP_TAC
754 THEN POP_ASSUM MP_TAC
755 THEN POP_ASSUM MP_TAC
761 THEN REWRITE_TAC[VECTOR_3;DOT_3]
762 THEN DISCH_THEN(LABEL_TAC"MA")
763 THEN REPEAT STRIP_TAC
764 THEN EXISTS_TAC`&1- (x'':real^3)$1 - x''$2 -x''$3`
765 THEN EXISTS_TAC`(x'':real^3)$1`
766 THEN EXISTS_TAC`(x'':real^3)$2`
767 THEN EXISTS_TAC`(x'':real^3)$3`
768 THEN ASM_REWRITE_TAC[REAL_ARITH` &1 - x''$1 - x''$2 - x''$3 + x''$1 + x''$2 + x''$3= &1`;VECTOR_ARITH`(u'''' % e1 + v'''' % e2 + w'''' % e3) + x =
769 u'''' % e1 + v'''' % e2 + w'''' % e3 + &1 % x`]
770 THEN REMOVE_THEN "MA" MP_TAC
772 THEN MRESAL_TAC CRAMER_LEMMA1[`A:real^3^3`;`x'':real^3`;`3`][ARITH_RULE`1<=3/\ 3<=3`;DIMINDEX_3;]
773 THEN POP_ASSUM MP_TAC
774 THEN REMOVE_ASSUM_TAC
775 THEN DISCH_THEN(LABEL_TAC"LINH3")
776 THEN ABBREV_TAC`b1=vector[u':real;u'':real;u'''':real]:real^3`
777 THEN ABBREV_TAC`b2=vector[v':real;v'':real;v'''':real]:real^3`
778 THEN ABBREV_TAC`b3=vector[w':real;w'':real;w'''':real]:real^3`
779 THEN ABBREV_TAC`B=vector[b1;b2;b3:real^3]:real^3^3`
780 THEN SUBGOAL_THEN`(lambda i j. if j = 3 then (b:real^3)$i else (A:real^3^3)$i$j):real^3^3=B` ASSUME_TAC
783 ONCE_ASM_SIMP_TAC[CART_EQ;]
784 THEN ONCE_ASM_SIMP_TAC[CART_EQ;]
785 THEN ASM_SIMP_TAC[LAMBDA_BETA;DIMINDEX_3]
786 THEN REPEAT STRIP_TAC
788 THEN ASM_REWRITE_TAC[]
789 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> i=1 \/ i=2 \/ i=3`)
796 THEN MP_TAC(ARITH_RULE`1<=i' /\ i'<= 3/\ ~(i'=3)==> i'=1 \/ i'=2`)
798 THEN REWRITE_TAC[VECTOR_3]
806 THEN REWRITE_TAC[VECTOR_3];
807 REMOVE_THEN"LINH3" MP_TAC
808 THEN ASM_REWRITE_TAC[]
809 THEN REMOVE_ASSUM_TAC
811 THEN SUBGOAL_THEN`&0<= det(B:real^3^3)`ASSUME_TAC
812 THENL[REMOVE_ASSUM_TAC
817 THEN REWRITE_TAC[DET_3;VECTOR_3]
818 THEN REMOVE_THEN "ME" MP_TAC
819 THEN ASM_REWRITE_TAC[VECTOR_ARITH`((u' % e1 + v' % e2 + w' % e3) + x) - x=u' % e1 + v' % e2 + w' % e3`;CROSS_LMUL;CROSS_RMUL;CROSS_LADD;CROSS_RADD;CROSS_REFL;]
820 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
821 THEN ASM_REWRITE_TAC[]
822 THEN REDUCE_VECTOR_TAC
823 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LNEG]
824 THEN ONCE_REWRITE_TAC[DOT_SYM]
825 THEN ASM_REWRITE_TAC[]
826 THEN REDUCE_ARITH_TAC
830 THEN MRESA1_TAC REAL_LE_INV`det (A:real^3^3)`
831 THEN MRESA1_TAC REAL_MUL_LINV`det (A:real^3^3)`
832 THEN MRESAL_TAC REAL_LE_MUL[`inv(det(A:real^3^3))`;`(x'':real^3)$3 * det(A:real^3^3)`][REAL_ARITH`A*(B*C)=(A*C)*B`;REAL_ARITH`&1*A=A`]]]]]);;
836 let PROPERTIES_AFF_GT_SUBSET_WEDGE=prove_by_refinement(`convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ ~(v=w)/\ generic V E
837 /\ azim_in_fan (v, rho_node1 FF v) E < pi
838 /\ aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt (v, rho_node1 FF v) E
841 aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt x E)`,
842 let lemma=prove(`!A. A \/ ~A`, SET_TAC[])
845 REWRITE_TAC[convex_local_fan;wedge_in_fan_gt]
847 THEN POP_ASSUM MP_TAC
848 THEN NHANH (ARITH_RULE` a = 2 ==> a > 1 `)
849 THEN MRESAL_TAC (GEN_ALL LOFA_CARD_EE_V_1)[`FF:real^3#real^3->bool`;`V:real^3->bool`;`v:real^3`;`E:(real^3->bool)->bool`;][ARITH_RULE`2>1`]
850 THEN REPEAT STRIP_TAC
851 THEN SUBGOAL_THEN ` FST (x:real^3 # real^3) IN V /\ SND x IN V ` MP_TAC;
852 MATCH_MP_TAC LOCAL_FAN_IMP_IN_V
853 THEN ASM_REWRITE_TAC[];
855 THEN ONCE_REWRITE_TAC[GSYM PAIR]
856 THEN REWRITE_TAC[wedge_in_fan_gt;]
857 THEN MRESAL_TAC (GEN_ALL LOFA_CARD_EE_V_1)[`FF:real^3#real^3->bool`;`V:real^3->bool`;`FST (x:real^3#real^3)`;`E:(real^3->bool)->bool`;][ARITH_RULE`2>1`]
858 THEN MRESAL_TAC (GEN_ALL PGSQVBL)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`;`x:real^3#real^3`;`E:(real^3->bool)->bool`][convex_local_fan;SET_RULE`{a,b} SUBSET V<=> a IN V /\ b IN V`]
859 THEN POP_ASSUM MP_TAC
860 THEN UNDISCH_TAC`!x:real^3#real^3. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E`
862 THEN POP_ASSUM(fun th-> MRESA1_TAC th `x:real^3#real^3` THEN POP_ASSUM MP_TAC
863 THEN POP_ASSUM MP_TAC THEN ASSUME_TAC th)
864 THEN ONCE_REWRITE_TAC[GSYM PAIR]
865 THEN REWRITE_TAC[wedge_in_fan_ge;azim_in_fan]
866 THEN ASM_REWRITE_TAC[ARITH_RULE`2>1`]
869 THEN MRESA_TAC PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`]
870 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`)
871 THEN MP_TAC(REAL_ARITH`azim (vec 0) (FST x) (SND x) d <= pi==> azim (vec 0) (FST x) (SND x) d = pi \/ azim (vec 0) (FST x) (SND x) d < pi`)
873 MRESA_TAC (GEN_ALL AZIM_PI_WEDGE_GE_CROSS_DOT)[`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`vec 0:real^3`]
874 THEN MRESA_TAC (GEN_ALL AZIM_PI_WEDGE_CROSS_DOT)[`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`vec 0:real^3`]
875 THEN REWRITE_TAC[VECTOR_ARITH`a- vec 0=a`]
876 THEN REPEAT STRIP_TAC
877 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`]
878 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;SUBSET]
879 THEN REPEAT STRIP_TAC
880 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0 +a=a`;DOT_RADD;DOT_RMUL]
881 THEN MATCH_MP_TAC(REAL_ARITH`!A B. (&0< A /\ &0<= B)\/(&0<= A/\ &0< B)==> &0< A+B`)
882 THEN MP_TAC REAL_LT_MUL_EQ
884 THEN REMOVE_ASSUM_TAC
885 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
886 THEN MP_TAC REAL_LE_MUL_EQ
888 THEN REMOVE_ASSUM_TAC
889 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
890 THEN MP_TAC(SET_RULE`V SUBSET {x' | &0 <= (FST x cross SND x) dot (x':real^3)} /\ v IN V
892 ==> &0<= (FST x cross SND x) dot w /\ &0<= (FST x cross SND x) dot v`)
894 THEN ONCE_REWRITE_TAC[SET_RULE`A\/ B<=> ~(~A /\ ~ B)`]
896 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot w /\ &0 <= (FST x cross SND x) dot v /\ ~(&0 < (FST x cross SND x) dot v) /\ ~(&0 < (FST x cross SND x) dot w)
897 ==> (FST x cross SND x) dot v= &0 /\
898 (FST x cross SND x) dot w = &0`)
900 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
901 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
902 THEN DOWN THEN STRIP_TAC
903 THEN ASSUME_TAC2 LOFA_IMP_EE_TWO_ELMS
904 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
905 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
906 THEN UNDISCH_TAC`aff_gt {vec 0} {v, w:real^3} SUBSET
907 wedge (vec 0) v (rho_node1 FF v)
908 (azim_cycle (EE v E) (vec 0) v (rho_node1 FF v))`
909 THEN ASM_REWRITE_TAC[azim_in_fan;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
912 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`d':real^3`]
913 THEN POP_ASSUM MP_TAC
914 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
915 THEN STRIP_TAC THEN STRIP_TAC
916 THEN MRESAL_TAC (GEN_ALL CONDITION_INANGLE_CROSS_DOT)[`v cross w:real^3`;`(rho_node1 FF v:real^3)`;`v:real^3`;`w:real^3`;`d':real^3`;`vec 0:real^3`][VECTOR_ARITH`a- vec 0=a`]
917 THEN UNDISCH_TAC`&0 < (v cross rho_node1 FF v) dot w`
919 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
920 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
921 THEN REPEAT STRIP_TAC
922 THEN ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V
923 THEN MP_TAC(SET_RULE`V SUBSET {x':real^3 | &0 <= (FST x cross SND x) dot x'}
924 /\ d' IN V /\ rho_node1 FF v IN V==> &0 <= (FST x cross SND x) dot d'
925 /\ &0 <= (FST x cross SND x) dot (rho_node1 FF v)`)
927 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross w:real^3`;`(rho_node1 FF v)`;`d':real^3`][CROSS_LAGRANGE;
928 VECTOR_ARITH`&0 % v - &0 % w= vec 0`;DOT_LZERO; REAL_ARITH`&0=A-B<=> A=B`]
929 THEN MP_TAC(REAL_ARITH`&0 < (v cross w) dot (d':real^3)==> &0 <= (v cross w) dot d'`)
931 THEN MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`w:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
932 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot rho_node1 FF v
933 ==> (FST x cross SND x) dot rho_node1 FF v= &0 \/ &0 < (FST x cross SND x) dot rho_node1 FF v`)
935 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`rho_node1 FF v:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
936 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (rho_node1 FF v)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
938 THEN REWRITE_TAC[CROSS_EQ_0]
939 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
942 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
943 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
946 MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot (d':real^3)
947 ==> (FST x cross SND x) dot (d':real^3)= &0 \/ &0 < (FST x cross SND x) dot (d':real^3)`)
949 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`d':real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
950 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (d':real^3)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
952 THEN REWRITE_TAC[CROSS_EQ_0]
953 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
956 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
957 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
958 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
959 THEN REWRITE_TAC[ DOT_LNEG]
962 MRESA_TAC REAL_LT_MUL[`(FST x cross SND x) dot rho_node1 FF v`;`((v cross w) dot (d':real^3))`]
963 THEN MP_TAC REAL_LT_MUL_EQ
965 THEN REMOVE_ASSUM_TAC
966 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(FST x cross SND x) dot (d':real^3)`;`(v cross w) dot (rho_node1 FF v:real^3)`] )
967 THEN POP_ASSUM MP_TAC
969 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
970 THEN REWRITE_TAC[ DOT_LNEG]
973 MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`]
974 THEN MRESA_TAC(GEN_ALL EXISTS_INVERSE_OF_V)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`]
975 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` FST(x:real^3#real^3)`;`vv:real^3`]
976 THEN UNDISCH_TAC`azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x) = d:real^3`
977 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
978 THEN POP_ASSUM MP_TAC THEN RESA_TAC
979 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:real^3#real^3`)
980 THEN SUBGOAL_THEN`rho_node1 FF (FST x)= SND x` ASSUME_TAC;
981 POP_ASSUM (fun th-> ONCE_REWRITE_TAC[th])
983 ASM_REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
985 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`vv:real^3`]
986 THEN POP_ASSUM MP_TAC
987 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
989 THEN MRESA_TAC (GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`]
990 THEN MRESA_TAC (GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`]
991 THEN POP_ASSUM MP_TAC
992 THEN MRESAL_TAC( GEN_ALL CONVEX_LOFA_IMP_INANGLE_EQ_AZIM) [`V:real^3->bool`;`FF:real^3#real^3->bool`;`E:(real^3->bool)->bool`][convex_local_fan]
993 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `FST (x:real^3#real^3)`[azim_in_fan;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET; ARITH_RULE`2>1`])
996 THEN MP_TAC(REAL_ARITH`&0 < azim (vec 0) (FST x) (SND x) d /\ azim (vec 0) (FST x) (SND x) d< pi ==> ~( azim (vec 0) (FST x) (SND x) d= &0 \/ azim (vec 0) (FST x) (SND x) d= pi)`)
998 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`]
999 THEN MRESA_TAC WEDGE_LUNE[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`]
1000 THEN MRESA_TAC inter_aff_gt_3_1_is_aff_gt_2_2[`vec 0:real^3`;`SND (x:real^3#real^3)`; `FST (x:real^3#real^3)`;`d:real^3`]
1001 THEN POP_ASSUM MP_TAC
1002 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1004 THEN MRESA_TAC inter_aff_ge_3_1_is_aff_ge_2_2[`vec 0:real^3`;`SND (x:real^3#real^3)`; `FST (x:real^3#real^3)`;`d:real^3`]
1005 THEN POP_ASSUM MP_TAC
1006 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1008 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1009 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;SET_RULE`A SUBSET B INTER C<=> A SUBSET B /\ A SUBSET C`])
1010 THEN MRESA1_TAC SIN_POS_PI`azim (vec 0) (FST x) (SND x) d`
1011 THEN POP_ASSUM MP_TAC
1012 THEN MP_TAC (SPECL [` FST(x:real^3#real^3) `;` SND (x:real^3#real^3) `;` d:real^3 `] Trigonometry2.JBDNJJB)
1013 THEN REWRITE_TAC[re_eqvl;]
1015 THEN MP_TAC REAL_LT_MUL_EQ
1017 THEN REMOVE_ASSUM_TAC
1018 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t:real`;`((FST x cross SND (x:real^3#real^3)) dot d)`] )
1019 THEN REMOVE_ASSUM_TAC
1020 THEN REMOVE_ASSUM_TAC
1021 THEN REMOVE_ASSUM_TAC
1023 THEN MRESAL_TAC aff_ge_3_1_rep_cross_dot[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`][VECTOR_ARITH`a- vec 0=a`]
1024 THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`][VECTOR_ARITH`a- vec 0=a`]
1025 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1026 THEN ASM_REWRITE_TAC[]
1027 THEN MRESAL_TAC aff_ge_3_1_rep_cross_dot[`vec 0:real^3`;`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`][VECTOR_ARITH`a- vec 0=a`]
1028 THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot[`vec 0:real^3`;`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`][VECTOR_ARITH`a- vec 0=a`]
1029 THEN POP_ASSUM MP_TAC
1030 THEN POP_ASSUM MP_TAC
1031 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
1032 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1035 THEN ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE]
1036 THEN REPEAT STRIP_TAC;
1037 MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`]
1038 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;SUBSET]
1039 THEN REPEAT STRIP_TAC
1040 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0 +a=a`;DOT_RADD;DOT_RMUL]
1041 THEN MATCH_MP_TAC(REAL_ARITH`!A B. (&0< A /\ &0<= B)\/(&0<= A/\ &0< B)==> &0< A+B`)
1042 THEN MP_TAC REAL_LT_MUL_EQ
1044 THEN REMOVE_ASSUM_TAC
1045 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
1046 THEN MP_TAC REAL_LE_MUL_EQ
1048 THEN REMOVE_ASSUM_TAC
1049 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
1050 THEN MP_TAC(SET_RULE`V SUBSET {x' | &0 <= (FST x cross SND x) dot (x':real^3)} /\ v IN V
1052 ==> &0<= (FST x cross SND x) dot w /\ &0<= (FST x cross SND x) dot v`)
1054 THEN ONCE_REWRITE_TAC[SET_RULE`A\/ B<=> ~(~A /\ ~ B)`]
1056 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot w /\ &0 <= (FST x cross SND x) dot v /\ ~(&0 < (FST x cross SND x) dot v) /\ ~(&0 < (FST x cross SND x) dot w)
1057 ==> (FST x cross SND x) dot v= &0 /\
1058 (FST x cross SND x) dot w = &0`)
1060 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
1061 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
1062 THEN DOWN THEN STRIP_TAC
1063 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`vv':real^3`]
1064 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
1065 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
1066 THEN UNDISCH_TAC`aff_gt {vec 0} {v, w:real^3} SUBSET
1067 wedge (vec 0) v (rho_node1 FF v)
1068 (azim_cycle (EE v E) (vec 0) v (rho_node1 FF v))`
1069 THEN ASM_REWRITE_TAC[azim_in_fan;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
1072 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`d':real^3`]
1073 THEN POP_ASSUM MP_TAC
1074 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1075 THEN STRIP_TAC THEN STRIP_TAC
1076 THEN MRESAL_TAC (GEN_ALL CONDITION_INANGLE_CROSS_DOT)[`v cross w:real^3`;`(rho_node1 FF v:real^3)`;`v:real^3`;`w:real^3`;`d':real^3`;`vec 0:real^3`][VECTOR_ARITH`a- vec 0=a`]
1077 THEN UNDISCH_TAC`&0 < (v cross rho_node1 FF v) dot w`
1079 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1080 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1081 THEN REPEAT STRIP_TAC
1082 THEN ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V
1083 THEN MP_TAC(SET_RULE`V SUBSET {x':real^3 | &0 <= (FST x cross SND x) dot x'}
1084 /\ d' IN V /\ rho_node1 FF v IN V==> &0 <= (FST x cross SND x) dot d'
1085 /\ &0 <= (FST x cross SND x) dot (rho_node1 FF v)`)
1087 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross w:real^3`;`(rho_node1 FF v)`;`d':real^3`][CROSS_LAGRANGE;
1088 VECTOR_ARITH`&0 % v - &0 % w= vec 0`;DOT_LZERO; REAL_ARITH`&0=A-B<=> A=B`]
1089 THEN MP_TAC(REAL_ARITH`&0 < (v cross w) dot (d':real^3)==> &0 <= (v cross w) dot d'`)
1091 THEN MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`w:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1092 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot rho_node1 FF v
1093 ==> (FST x cross SND x) dot rho_node1 FF v= &0 \/ &0 < (FST x cross SND x) dot rho_node1 FF v`)
1095 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`rho_node1 FF v:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1096 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (rho_node1 FF v)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1098 THEN REWRITE_TAC[CROSS_EQ_0]
1099 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
1102 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1103 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1105 THEN REAL_ARITH_TAC;
1106 MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot (d':real^3)
1107 ==> (FST x cross SND x) dot (d':real^3)= &0 \/ &0 < (FST x cross SND x) dot (d':real^3)`)
1109 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`d':real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1110 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (d':real^3)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1112 THEN REWRITE_TAC[CROSS_EQ_0]
1113 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
1116 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1117 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1118 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1119 THEN REWRITE_TAC[ DOT_LNEG]
1121 THEN REAL_ARITH_TAC;
1122 MRESA_TAC REAL_LT_MUL[`(FST x cross SND x) dot rho_node1 FF v`;`((v cross w) dot (d':real^3))`]
1123 THEN MP_TAC REAL_LT_MUL_EQ
1125 THEN REMOVE_ASSUM_TAC
1126 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(FST x cross SND x) dot (d':real^3)`;`(v cross w) dot (rho_node1 FF v:real^3)`] )
1127 THEN POP_ASSUM MP_TAC
1129 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1130 THEN REWRITE_TAC[ DOT_LNEG]
1132 THEN REAL_ARITH_TAC;
1133 MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`]
1134 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;SUBSET]
1135 THEN REPEAT STRIP_TAC
1136 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0 +a=a`;DOT_RADD;DOT_RMUL]
1137 THEN MATCH_MP_TAC(REAL_ARITH`!A B. (&0< A /\ &0<= B)\/(&0<= A/\ &0< B)==> &0< A+B`)
1138 THEN MP_TAC REAL_LT_MUL_EQ
1140 THEN REMOVE_ASSUM_TAC
1141 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((d cross FST (x:real^3#real^3)) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((d cross FST (x:real^3#real^3)) dot w:real^3)`])
1142 THEN MP_TAC REAL_LE_MUL_EQ
1144 THEN REMOVE_ASSUM_TAC
1145 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((d cross FST (x:real^3#real^3)) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((d cross FST (x:real^3#real^3)) dot w:real^3)`])
1146 THEN MP_TAC(SET_RULE`V SUBSET {y | &0 <= (d cross FST (x:real^3#real^3)) dot (y:real^3)} /\ v IN V
1148 ==> &0<= (d cross FST x) dot w /\ &0<= (d cross FST x) dot v`)
1150 THEN ONCE_REWRITE_TAC[SET_RULE`A\/ B<=> ~(~A /\ ~ B)`]
1152 THEN MP_TAC(REAL_ARITH`&0 <= (d cross FST x) dot w /\ &0 <= (d cross FST x) dot v /\ ~(&0 < (d cross FST x) dot v) /\ ~(&0 < (d cross FST x) dot w)
1153 ==> (d cross FST (x:real^3#real^3)) dot v= &0 /\
1154 (d cross FST x) dot w = &0`)
1156 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
1157 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
1158 THEN DOWN THEN STRIP_TAC
1159 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`vv':real^3`]
1160 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
1161 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
1162 THEN UNDISCH_TAC`aff_gt {vec 0} {v, w:real^3} SUBSET
1163 wedge (vec 0) v (rho_node1 FF v)
1164 (azim_cycle (EE v E) (vec 0) v (rho_node1 FF v))`
1165 THEN ASM_REWRITE_TAC[azim_in_fan;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
1168 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`d':real^3`]
1169 THEN POP_ASSUM MP_TAC
1170 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1171 THEN STRIP_TAC THEN STRIP_TAC
1172 THEN MRESAL_TAC (GEN_ALL CONDITION_INANGLE_CROSS_DOT)[`v cross w:real^3`;`(rho_node1 FF v:real^3)`;`v:real^3`;`w:real^3`;`d':real^3`;`vec 0:real^3`][VECTOR_ARITH`a- vec 0=a`]
1173 THEN UNDISCH_TAC`&0 < (v cross rho_node1 FF v) dot w`
1175 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1176 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1177 THEN REPEAT STRIP_TAC
1178 THEN ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V
1179 THEN MP_TAC(SET_RULE`V SUBSET {x':real^3 | &0 <= (d cross FST (x:real^3#real^3)) dot x'}
1180 /\ d' IN V /\ rho_node1 FF v IN V==> &0 <= (d cross FST (x:real^3#real^3)) dot d'
1181 /\ &0 <= (d cross FST (x:real^3#real^3)) dot (rho_node1 FF v)`)
1183 THEN MRESAL_TAC DOT_CROSS[`(d cross FST (x:real^3#real^3):real^3)`;`v cross w:real^3`;`(rho_node1 FF v)`;`d':real^3`][CROSS_LAGRANGE;
1184 VECTOR_ARITH`&0 % v - &0 % w= vec 0`;DOT_LZERO; REAL_ARITH`&0=A-B<=> A=B`]
1185 THEN MP_TAC(REAL_ARITH`&0 < (v cross w) dot (d':real^3)==> &0 <= (v cross w) dot d'`)
1187 THEN MRESAL_TAC CROSS_CROSS_DET[`d:real^3`;`FST (x:real^3#real^3)`;`v:real^3`;`w:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1188 THEN MP_TAC(REAL_ARITH`&0 <= (d cross FST (x:real^3#real^3)) dot rho_node1 FF v
1189 ==> (d cross FST (x:real^3#real^3)) dot rho_node1 FF v= &0 \/ &0 < (d cross FST (x:real^3#real^3)) dot rho_node1 FF v`)
1191 MRESAL_TAC CROSS_CROSS_DET[`d:real^3`;`FST (x:real^3#real^3)`;`v:real^3`;`rho_node1 FF v:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1192 THEN MRESAL_TAC DOT_CROSS[`(d cross FST (x:real^3#real^3))`;`v cross (rho_node1 FF v)`;`d cross FST (x:real^3#real^3):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1194 THEN REWRITE_TAC[CROSS_EQ_0]
1195 THEN UNDISCH_TAC `!x:real^3. x IN V ==> x,rho_node1 FF x IN FF`
1197 THEN POP_ASSUM(fun th-> MRESA1_TAC th`vv:real^3`)
1198 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (d:real^3,FST (x:real^3#real^3))`];
1201 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1202 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1204 THEN REAL_ARITH_TAC;
1205 MP_TAC(REAL_ARITH`&0 <= ((d cross FST (x:real^3#real^3))) dot (d':real^3)
1206 ==> ((d cross FST (x:real^3#real^3))) dot (d':real^3)= &0 \/ &0 < ((d cross FST (x:real^3#real^3))) dot (d':real^3)`)
1208 MRESAL_TAC CROSS_CROSS_DET[`d:real^3`;`FST (x:real^3#real^3)`;`v:real^3`;`d':real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1209 THEN MRESAL_TAC DOT_CROSS[`(d cross FST (x:real^3#real^3))`;`v cross (d':real^3)`;`(d cross FST (x:real^3#real^3)):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1211 THEN REWRITE_TAC[CROSS_EQ_0]
1212 THEN UNDISCH_TAC `!x:real^3. x IN V ==> x,rho_node1 FF x IN FF`
1214 THEN POP_ASSUM(fun th-> MRESA1_TAC th`vv:real^3`)
1215 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (d:real^3,FST (x:real^3#real^3))`];
1218 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1219 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1220 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1221 THEN REWRITE_TAC[ DOT_LNEG]
1223 THEN REAL_ARITH_TAC;
1224 MRESA_TAC REAL_LT_MUL[`(d cross FST (x:real^3#real^3)) dot rho_node1 FF v`;`((v cross w) dot (d':real^3))`]
1225 THEN MP_TAC REAL_LT_MUL_EQ
1227 THEN REMOVE_ASSUM_TAC
1228 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(d cross FST (x:real^3#real^3)) dot (d':real^3)`;`(v cross w) dot (rho_node1 FF v:real^3)`] )
1229 THEN POP_ASSUM MP_TAC
1231 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1232 THEN REWRITE_TAC[ DOT_LNEG]
1234 THEN REAL_ARITH_TAC]);;
1236 let AFF_GE_SUBSET_AFF_GE_UNION=prove(`!x v u v1:real^3.
1237 DISJOINT {x} {v, u} /\
1238 DISJOINT {x} {v, v1} /\
1239 DISJOINT {x} {v1, u} /\
1240 v1 IN aff_gt {x} {v, u}
1241 ==> aff_ge {x} {v, u} SUBSET aff_ge {x} {v, v1} UNION aff_ge {x} {v1,u}`,
1243 THEN POP_ASSUM MP_TAC
1244 THEN MRESA_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`]
1245 THEN MRESA_TAC AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`]
1246 THEN MRESA_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`v1:real^3`]
1247 THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v1:real^3`;`u:real^3`][SUBSET;IN_ELIM_THM;UNION]
1248 THEN REPEAT STRIP_TAC
1249 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1'' % x + t2'' % v + t3'' % (t1 % x + t2 % v + t3 % u)= (t1''+t3'' *t1) % x + (t2''+ t3''* t2) % v + (t3''*t3) % u`
1250 ;VECTOR_ARITH`t1'' % x + t2'' % (t1 % x + t2 % v + t3 % u) + t3'' % u=
1251 (t1''+ t2''* t1) % x + (t2'' * t2) % v + (t3'' + t2''*t3) % u`]
1252 THEN DISJ_CASES_TAC(REAL_ARITH`inv t3 * t3' <= inv t2 * t2' \/ inv t2 * t2' <= inv t3 * t3'`)
1254 MATCH_MP_TAC(SET_RULE`A==> A\/B`)
1255 THEN MP_TAC(REAL_ARITH`&0< t3==> ~(t3= &0) /\ &0<= t3`)
1257 THEN MRESA1_TAC REAL_MUL_LINV`t3:real`
1258 THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)/\ &0<= t2`)
1260 THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
1261 THEN EXISTS_TAC`&1-(t2'- inv t3 * t3' * t2)- inv t3 * t3'`
1262 THEN EXISTS_TAC`(t2'- inv t3 * t3' * t2)`
1263 THEN EXISTS_TAC`inv t3 * t3'`
1264 THEN ASM_REWRITE_TAC[REAL_ARITH`&1- A-B+A+B= &1`;REAL_ARITH`&0<= a-b<=>b<=a`; REAL_ARITH`t2' - inv t3 * t3' * t2 + (inv t3 * t3') * t2= t2'`; REAL_ARITH`(A*B)*C=B*(A*C)`; REAL_ARITH`&1 - (t2' - inv t3 * t3' * t2) - inv t3 * t3' + t3' * inv t3 * t1=
1265 &1 - t2' -inv t3 * t3' *(t3-(t1+t2+t3)+ &1)`; REAL_ARITH`a- &1+ &1=a`; REAL_ARITH`a* &1=a`]
1266 THEN ASM_REWRITE_TAC[REAL_ARITH`a*b*c= (a*c) *b`; REAL_ARITH`(&1 - t2' - &1 * t3')= t1' + &1- (t1'+t2'+t3')`; REAL_ARITH`a+ &1- &1=a`;]
1267 THEN MRESA_TAC REAL_LE_LMUL[`t2:real`;`inv t3 * t3'`;`inv t2 * t2'`]
1268 THEN POP_ASSUM MP_TAC
1269 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C=(B*A)*C/\ &1* a=a`]
1271 THEN MATCH_MP_TAC REAL_LE_MUL
1272 THEN ASM_REWRITE_TAC[]
1273 THEN MATCH_MP_TAC REAL_LE_INV
1274 THEN ASM_REWRITE_TAC[];
1275 MATCH_MP_TAC(SET_RULE`B==> A\/B`)
1276 THEN MP_TAC(REAL_ARITH`&0< t3==> ~(t3= &0) /\ &0<= t3`)
1278 THEN MRESA1_TAC REAL_MUL_LINV`t3:real`
1279 THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)/\ &0<= t2`)
1281 THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
1282 THEN EXISTS_TAC`&1- inv t2 * t2' -( t3'- inv t2 * t2'* t3)`
1283 THEN EXISTS_TAC`inv t2 * t2'`
1284 THEN EXISTS_TAC`( t3'- inv t2 * t2'* t3)`
1285 THEN ASM_REWRITE_TAC[REAL_ARITH`&1- A-B+A+B= &1`;REAL_ARITH`&0<= a-b<=>b<=a`; REAL_ARITH`t2' - inv t3 * t3' * t2 + (inv t3 * t3') * t2= t2'`; REAL_ARITH`(A*B)*C=B*(A*C)`;]
1286 THEN ASM_REWRITE_TAC[ REAL_ARITH`(&1 - inv t2 * t2' - (t3' - (inv t2 * t3) * t2') + (t2' * t1) * inv t2)
1287 = &1 - t3' - inv t2 * t2'* ( t2 -(t1+t2+t3)+ &1)`; REAL_ARITH`a- &1+ &1=a`; REAL_ARITH`a* &1=a`;REAL_ARITH`a*b*c= (a*c) *b`; REAL_ARITH`(&1 - t2' - &1 * t3')= t1' + &1- (t1'+t3'+t2')`; REAL_ARITH`a+ &1- &1=a`;]
1288 THEN MRESA_TAC REAL_LE_LMUL[`t3:real`;`inv t2 * t2'`;`inv t3 * t3'`]
1289 THEN POP_ASSUM MP_TAC
1290 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C=(B*A)*C/\ &1* a=a`]
1292 THEN MATCH_MP_TAC REAL_LE_MUL
1293 THEN ASM_REWRITE_TAC[]
1294 THEN MATCH_MP_TAC REAL_LE_INV
1295 THEN ASM_REWRITE_TAC[]]);;
1298 let aff_ge_subset3_aff_ge=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
1299 DISJOINT {x} {v,u} /\ DISJOINT {x} {v,v1}
1300 /\ v1 IN aff_gt {x} {v,u}
1302 aff_ge {x} {v,v1} SUBSET aff_ge {x} {v,u}`,
1304 THEN POP_ASSUM MP_TAC
1305 THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM]
1306 THEN MRESAL_TAC AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM]
1307 THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`v1:real^3`][IN_ELIM_THM;SUBSET]
1308 THEN REPEAT STRIP_TAC
1309 THEN POP_ASSUM MP_TAC
1310 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % v + t3' % (t1 % x + t2 % v + t3 % u)
1311 =(t1'+ t3'*t1) % x + (t2'+ t3' * t2) % v + (t3' * t3) % u:real^3`]
1313 THEN EXISTS_TAC`t1' + t3' * t1:real`
1314 THEN EXISTS_TAC`t2' + t3' * t2:real`
1315 THEN EXISTS_TAC`t3' * t3:real`
1316 THEN MP_TAC(REAL_ARITH`&0< t2 /\ &0< t3==> &0<= t2 /\ &0<= t3`)
1318 THEN MRESA_TAC REAL_LE_MUL[`t3':real`;`t2:real`]
1319 THEN MRESA_TAC REAL_LE_MUL[`t3':real`;`t3:real`]
1320 THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t3' * t1) + (t2' + t3' * t2) + t3' * t3=
1321 t1'+ t2' + t3'*(t1+t2+t3)`; REAL_ARITH`A* &1=A`]
1323 THEN REAL_ARITH_TAC);;
1326 let AFF_GE_EQ_AFF_GE_UNION=prove(`!x v u v1:real^3.
1327 DISJOINT {x} {v, u} /\
1328 DISJOINT {x} {v, v1} /\
1329 DISJOINT {x} {v1, u} /\
1330 v1 IN aff_gt {x} {v, u}
1331 ==> aff_ge {x} {v, u} = aff_ge {x} {v, v1} UNION aff_ge {x} {v1,u}`,
1333 THEN ASSUME_TAC2 AFF_GE_SUBSET_AFF_GE_UNION
1334 THEN MRESA_TAC aff_ge_subset3_aff_ge[`x:real^3`;`v:real^3`;`u:real^3`;`v1:real^3`]
1335 THEN MRESA_TAC aff_ge_subset3_aff_ge[`x:real^3`;`u:real^3`;`v:real^3`;`v1:real^3`]
1336 THEN POP_ASSUM MP_TAC
1337 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1338 THEN ASM_REWRITE_TAC[]
1340 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1341 THEN POP_ASSUM MP_TAC
1342 THEN POP_ASSUM MP_TAC
1343 THEN POP_ASSUM MP_TAC
1348 let order = new_definition ` order f x y = (@n. ITER n f x =y /\ (!i. 0< i /\ i< n ==> ~(ITER i f x= y)))`;;
1349 let slicev = new_definition ` slicev E FF v w = {u| ?n. 0<= n /\ n<= order (rho_node1 FF) v w /\ u= ITER n (rho_node1 FF) v}`;;
1351 let slicee = new_definition ` slicee E FF v w = {e| ?u. u IN (slicev E FF v w) DELETE w /\ e={u,rho_node1 FF u} } UNION {{w,v}}`;;
1353 let slicef = new_definition ` slicef E FF v w = {f| ?u. u IN (slicev E FF v w) DELETE w /\ f=(u,rho_node1 FF u) } UNION {(w,v)}`;;
1356 let rho_fun = new_definition `rho_fun y = &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
1359 let tau_fun = new_definition `tau_fun V E f = sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;
1363 let ORDER=prove(`(ITER n f x = y /\ (!i. 0 < i /\ i < n ==> ~(ITER i f x = y)))
1365 ITER (order f x y) f x= y /\ (!i. 0 < i /\ i < order f x y ==> ~(ITER i f x = y))`,
1367 THEN ONCE_REWRITE_TAC[order]
1368 THEN SELECT_ELIM_TAC
1369 THEN ASM_REWRITE_TAC[]
1370 THEN POP_ASSUM MP_TAC
1371 THEN POP_ASSUM MP_TAC
1374 let UNIQUE_ORDER=prove_by_refinement(`!f:A->A. ITER n f x = y /\ (!i. 0 < i /\ i < n ==> ~(ITER i f x = y)) /\ ~(x=y)
1378 THEN MRESA_TAC (GEN_ALL ORDER)[`n:num`;`f:A->A`;`x:A`;`y:A`]
1379 THEN MP_TAC(ARITH_RULE`order (f:A->A) x y =0 \/ 0< order (f:A->A) x y `)
1381 POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th;ITER])
1383 MP_TAC(ARITH_RULE`order (f:A->A) x y <n \/ n<= order (f:A->A) x y `)
1388 THEN POP_ASSUM(fun th-> MRESA1_TAC th `order (f:A->A) x y`)
1389 THEN POP_ASSUM MP_TAC
1390 THEN DISCH_THEN(LABEL_TAC "THY")
1391 THEN REPEAT STRIP_TAC
1392 THEN REMOVE_THEN "THY" MP_TAC
1394 MP_TAC(ARITH_RULE`n<= order (f:A->A) x y ==> n< order (f:A->A) x y \/ order (f:A->A) x y =n`)
1396 MP_TAC(ARITH_RULE`n =0 \/ 0< n`)
1398 POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th;ITER])
1401 THEN POP_ASSUM MP_TAC
1402 THEN POP_ASSUM MP_TAC
1403 THEN POP_ASSUM MP_TAC
1404 THEN POP_ASSUM MP_TAC
1405 THEN DISCH_THEN(LABEL_TAC "THY")
1406 THEN REPEAT STRIP_TAC
1407 THEN REMOVE_THEN "THY" (fun th-> MRESA1_TAC th`n:num`)]);;
1413 let COMPATIBLE_BW_TWO_LEMMAS = prove_by_refinement
1414 (`convex_local_fan (V,E,FF) /\
1418 (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
1419 HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
1420 fv = face HS (v,rho_node1 FF v)
1421 ==> (v_prime V fv = slicev E FF v w ) /\
1422 e_prime (E UNION {{v, w}}) fv = slicee E FF v w /\
1423 fv = slicef E FF v w `,
1425 ASSUME_TAC2 PROVE_THE_SLICE_ASSUMPTION;
1426 MP_TAC POINTS_IN_HAFL_CIRCLE;
1429 SIMP_TAC[convex_local_fan];
1431 ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO;
1432 ASSUME_TAC2 POINT_PRESENTED_IN_RHOND1;
1433 DOWN THEN STRIP_TAC;
1435 MP_TAC DETERMINE_FV2;
1438 ASM_REWRITE_TAC[TAUT` a /\ b ==> c <=> a ==> b ==> c `];
1442 SUBGOAL_THEN` v_prime (V:real^3 -> bool) (fv:real^3#real^3 -> bool) =
1443 slicev (E:(real^3 -> bool) -> bool) FF v w ` MP_TAC;
1444 ASM_REWRITE_TAC[slicev; EXTENSION; IN_ELIM_THM];
1448 EXISTS_TAC` n':num`;
1449 ASM_REWRITE_TAC[LE_0];
1450 MP_TAC (ISPECL [` v:real^3 `;` w:real^3 `;` n:num `; ` rho_node1 FF `] (GEN_ALL UNIQUE_ORDER));
1454 ASM_CASES_TAC` i = 0`;
1455 ASM_REWRITE_TAC[ITER];
1456 ASSUME_TAC2 (ARITH_RULE` ~( i =0) ==> 0 < i `);
1462 ASM_CASES_TAC` n < (n': num) `;
1464 FIRST_X_ASSUM NHANH;
1472 EXISTS_TAC `n':num `;
1474 MP_TAC (ISPECL [` v:real^3 `;` w:real^3 `;` n:num `; ` rho_node1 FF `] (GEN_ALL UNIQUE_ORDER));
1478 ASM_CASES_TAC` i = 0 `;
1479 ASM_REWRITE_TAC[ITER];
1480 ASSUME_TAC2 (ARITH_RULE` ~( i = 0) ==> 0 < i `);
1482 DISCH_THEN SUBST_ALL_TAC;
1483 GEN_TAC THEN DISCH_TAC;
1484 ASSUME_TAC2 (ARITH_RULE` m < n' /\ n' <= n ==> m < n:num `);
1490 REWRITE_TAC[slicee; slicef];
1491 DISCH_THEN (SUBST_ALL_TAC o SYM);
1492 REWRITE_TAC[e_prime];
1496 REWRITE_TAC[EXTENSION; IN_UNION];
1499 ONCE_REWRITE_TAC[IN_ELIM_THM];
1501 FIRST_ASSUM SUBST1_TAC;
1502 REWRITE_TAC[IN_INSERT];
1503 FIRST_ASSUM (SUBST1_TAC o SYM);
1512 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ];
1515 EXISTS_TAC` ITER m (rho_node1 FF) v `;
1516 REWRITE_TAC[GSYM IN_INSERT; GSYM EXTENSION];
1519 SIMP_TAC[GSYM ITER; ADD1];
1521 REWRITE_TAC[IN_DELETE; IN_ELIM_THM];
1523 EXISTS_TAC `m:num `;
1526 GEN_TAC THEN STRIP_TAC;
1527 ASSUME_TAC2 (ARITH_RULE` m' < m /\ m < (n:num) ==> m' < n`);
1531 UNDISCH_TAC` m < (n:num) `;
1534 DISJ2_TAC THEN DISJ1_TAC;
1542 REWRITE_TAC[INSERT_COMM];
1543 REPLICATE_TAC 3 DOWN;
1544 REWRITE_TAC[NOT_IN_EMPTY];
1546 REPLICATE_TAC 3 DOWN;
1547 REWRITE_TAC[NOT_IN_EMPTY];
1549 (* ==================== *)
1551 REWRITE_TAC[GSYM EXTENSION; GSYM IN_INSERT];
1553 FIRST_ASSUM SUBST1_TAC;
1556 REWRITE_TAC[IN_ELIM_THM; IN_DELETE];
1558 EXISTS_TAC` u: real^3`;
1559 EXISTS_TAC` rho_node1 FF u `;
1560 REWRITE_TAC[IN_INSERT; IN_ELIM_THM];
1566 MATCH_MP_TAC LOCAL_RHO_NODE_PAIR_E;
1568 UNDISCH_TAC` (v:real^3) IN V `;
1569 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;
1570 DOWN THEN SIMP_TAC[];
1572 EXISTS_TAC` n': num `;
1573 REWRITE_TAC[GSYM ITER; ADD1];
1574 ASM_CASES_TAC` (n:num) < n' `;
1576 FIRST_X_ASSUM NHANH;
1580 ASM_CASES_TAC` n = (n': num) `;
1581 UNDISCH_TAC` ~(u = (w:real^3)) `;
1582 FIRST_X_ASSUM SUBST_ALL_TAC;
1584 DOWN THEN ARITH_TAC;
1591 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM];
1593 EXISTS_TAC` w:real^3 `;
1594 EXISTS_TAC` v:real^3 `;
1595 DOWN THEN SIMP_TAC[];
1598 SIMP_TAC[INSERT_COMM];
1600 FIRST_ASSUM SUBST1_TAC;
1606 FIRST_X_ASSUM (SUBST1_TAC o SYM);
1607 ASSUME_TAC2 DETERMINE_FV;
1608 FIRST_X_ASSUM SUBST1_TAC;
1609 REWRITE_TAC[EXTENSION; IN_INSERT; IN_UNION; IN_ELIM_THM];
1613 FIRST_X_ASSUM (fun x -> REWRITE_TAC[x]);
1615 EXISTS_TAC` ITER n' (rho_node1 FF) v `;
1616 ASM_REWRITE_TAC[IN_DELETE; IN_ELIM_THM;GSYM ITER; ADD1];
1618 EXISTS_TAC `n': num `;
1621 NHANH (ARITH_RULE` a < (b:num) ==> a < b + 1 `);
1622 FIRST_X_ASSUM NHANH;
1624 MP_TAC (ARITH_RULE` n' < n' + 1 `);
1628 REWRITE_TAC[NOT_IN_EMPTY];
1632 REWRITE_TAC[IN_ELIM_THM; IN_DELETE];
1635 EXISTS_TAC` n':num `;
1636 ASM_REWRITE_TAC[ADD1;GSYM ITER];
1638 ASM_CASES_TAC` m = (n': num) `;
1640 UNDISCH_TAC` ~( u = (w:real^3)) `;
1643 REWRITE_TAC[ARITH_RULE` ~(m = n') /\ m < n' + 1 <=> m < (n':num) `];
1645 DOWN THEN SIMP_TAC[]]);;
1651 let COMPATIBLE_BW_TWO_LEMMAS2 = prove_by_refinement
1652 (`(convex_local_fan (V,E,FF) /\
1656 (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
1657 HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
1658 fv = face HS (v,rho_node1 FF v))/\
1659 fw = face HS (w, rho_node1 FF w)
1660 ==> ( (v_prime V fv = slicev E FF v w ) /\
1661 e_prime (E UNION {{v, w}}) fv = slicee E FF v w /\
1662 fv = slicef E FF v w ) /\
1663 ( (v_prime V fw = slicev E FF w v ) /\
1664 e_prime (E UNION {{w, v}}) fw = slicee E FF w v /\
1665 fw = slicef E FF w v )`,
1666 [NHANH COMPATIBLE_BW_TWO_LEMMAS;
1670 FIRST_X_ASSUM ACCEPT_TAC;
1672 FIRST_X_ASSUM ACCEPT_TAC;
1673 FIRST_X_ASSUM ACCEPT_TAC;
1676 MATCH_MP_TAC COMPATIBLE_BW_TWO_LEMMAS;
1678 REWRITE_TAC[INSERT_COMM];
1679 ASM_REWRITE_TAC[]]);;
1685 let EJRCFJD_concl=`!V E FF v w. convex_local_fan(V,E,FF)
1688 /\ (!u u1. u IN {v,w} /\ u1 IN V /\ ~(u=u1) ==> ~(collinear {vec 0, u, u1}))
1689 /\ (!e. e IN FF ==> aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt e E)
1690 ==> convex_local_fan(slicev E FF v w, slicee E FF v w, slicef E FF v w)
1691 /\ convex_local_fan(slicev E FF w v, slicee E FF w v, slicef E FF w v)
1692 /\ tau_fun V E FF >= tau_fun (slicev E FF v w) (slicee E FF v w) (slicef E FF v w) + tau_fun (slicev E FF w v) (slicee E FF w v) (slicef E FF w v)
1693 /\ sol_local E FF= sol_local (slicee E FF v w) (slicef E FF v w) + sol_local (slicee E FF w v) (slicef E FF w v)
1694 /\ CARD (slicev E FF v w) < CARD V
1695 /\ CARD (slicev E FF w v) < CARD V
1696 /\(generic V E ==> generic (slicev E FF v w) (slicee E FF v w)
1697 /\ generic (slicev E FF w v) (slicee E FF w v))`
1700 let NKEZBFC_concl=`!V E FF. convex_local_fan(V,E,FF) /\ generic V E
1701 ==> &0 <= sol_local E FF`
1704 let NKEZBFC_concl2 = mk_imp (EJRCFJD_concl, NKEZBFC_concl);;
1707 let lemma=prove(`!A. A \/ ~A`, SET_TAC[]);;
1708 let lemma1=prove(`!A. ~A \/ A`, SET_TAC[]);;
1718 let NKEZBFC_PREP =prove_by_refinement(NKEZBFC_concl2,
1720 THEN ABBREV_TAC`n= CARD (V:real^3->bool)-3`
1722 THEN DISCH_THEN(LABEL_TAC"LINH")
1723 THEN SPEC_TAC(`V:real^3->bool`,`V:real^3->bool`)
1724 THEN SPEC_TAC(`E:(real^3->bool)->bool`,`E:(real^3->bool)->bool`)
1725 THEN SPEC_TAC(`FF:real^3#real^3->bool`,`FF:real^3#real^3->bool`)
1726 THEN SPEC_TAC(`n:num`,`n:num`)
1727 THEN MATCH_MP_TAC num_WF
1730 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`]
1731 THEN MP_TAC(ARITH_RULE`3<= CARD (V:real^3->bool) /\ CARD V -3 =0 <=> CARD V=3`)
1733 THEN ASM_MESON_TAC[SOL_LOCAL_FAN_POS_CASE3];
1735 THEN DISCH_THEN(LABEL_TAC"LINH1")
1736 THEN DISCH_THEN(LABEL_TAC"LIN21")
1737 THEN REPEAT STRIP_TAC
1738 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`]
1739 THEN MRESA1_TAC lemma `(?v w:real^3. v IN V /\ w IN V
1740 /\ (!e. e IN FF ==> aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt e E)
1742 MRESA_TAC (GEN_ALL PROPERTIES_GENERIC1)[`FF:real^3#real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`;`V:real^3->bool`;]
1743 THEN REMOVE_THEN "LINH"(fun th-> MRESA_TAC th[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`])
1744 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`(slicev (E:(real^3->bool)->bool) FF v w):real^3->bool`;`(slicee (E:(real^3->bool)->bool) FF v w):(real^3->bool)->bool`;`(slicef (E:(real^3->bool)->bool) FF v w):real^3#real^3->bool`]
1745 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`(slicev (E:(real^3->bool)->bool) FF w v):real^3->bool`;`(slicee (E:(real^3->bool)->bool) FF w v ):(real^3->bool)->bool`;`(slicef (E:(real^3->bool)->bool) FF w v ):real^3#real^3->bool`]
1746 THEN MP_TAC(ARITH_RULE`CARD (slicev E FF v w)< CARD V
1747 /\ CARD (slicev E FF w v)< CARD V
1748 /\ 3<= CARD V /\ 3<= CARD (slicev E FF v w)
1749 /\ 3<= CARD (slicev E FF w v)==> CARD (slicev (E:(real^3->bool)->bool) FF v w) -3 < CARD V -3
1750 /\ CARD (slicev E FF w v) -3 < CARD (V:real^3->bool) -3`)
1752 THEN REMOVE_THEN "LIN21"(fun th-> MRESA1_TAC th`CARD (slicev (E:(real^3->bool)->bool) FF v w) -3`
1753 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(slicef (E:(real^3->bool)->bool) FF v w)`;`(slicee (E:(real^3->bool)->bool) FF v w)`;`(slicev (E:(real^3->bool)->bool) FF v w):real^3->bool`])
1754 THEN MRESA1_TAC th`CARD (slicev (E:(real^3->bool)->bool) FF w v) -3`
1755 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(slicef (E:(real^3->bool)->bool) FF w v)`;`(slicee (E:(real^3->bool)->bool) FF w v)`;`(slicev (E:(real^3->bool)->bool) FF w v)`]))
1756 THEN POP_ASSUM MP_TAC
1757 THEN POP_ASSUM MP_TAC
1758 THEN REAL_ARITH_TAC;
1760 THEN REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM]
1761 THEN DISCH_THEN(LABEL_TAC"LINH2")
1762 THEN ASSUME_TAC2 SOL_LOFA_EQ_SUM_INANGLE
1763 THEN MRESA1_TAC lemma`(!v. v IN V==> pi <= interior_angle1 (vec 0) FF v )`;
1764 MATCH_MP_TAC(REAL_ARITH`&0< pi /\ &0<= A==> &0<= &2 * pi+A`)
1765 THEN REWRITE_TAC[PI_WORKS]
1766 THEN MATCH_MP_TAC SUM_POS_LE
1767 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<= A`]
1769 THEN REWRITE_TAC[convex_local_fan;local_fan;FAN;fan1]
1771 THEN REPEAT STRIP_TAC
1772 THEN ASM_REWRITE_TAC[];
1774 THEN REWRITE_TAC[NOT_IMP;NOT_FORALL_THM;REAL_ARITH`~(a<=b) <=> b<a`]
1776 THEN UNDISCH_TAC`convex_local_fan (V:real^3->bool,E,FF)`
1778 THEN POP_ASSUM(fun th -> MP_TAC th THEN REWRITE_TAC[convex_local_fan] THEN ASSUME_TAC th THEN STRIP_TAC)
1779 THEN MRESA_TAC PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;]
1780 THEN ABBREV_TAC`vv=(\i. ITER i (rho_node1 FF) v)`
1781 THEN ABBREV_TAC`bta=(\i. azim (vec 0) v (vv 1) (vv i))`
1782 THEN ABBREV_TAC`k=CARD (V:real^3->bool)`
1783 THEN MRESA1_TAC lemma1`(!i. i<k ==> bta i= &0 \/ bta i= bta (k-1)):bool`;
1785 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;DE_MORGAN_THM]
1787 THEN DISJ_CASES_TAC(ARITH_RULE` k-1<= i \/ (i< k-1)`);
1788 MP_TAC(ARITH_RULE`k-1<= i /\ i< k /\ 3<= k==> i= k-1`)
1790 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1792 MP_TAC(ARITH_RULE` 3<= k==> k-1<k`)
1794 THEN MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
1795 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
1796 THEN POP_ASSUM MP_TAC
1797 THEN EXPAND_TAC "bta"
1799 THEN EXPAND_TAC "vv"
1802 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`k-1:num`])
1803 THEN MP_TAC(REAL_ARITH`~(bta i = &0) /\ ~(bta i = bta (k - 1))
1804 /\ &0<= bta i /\ bta i<= bta(k-1)==> &0< bta i /\ bta i< bta(k-1)`)
1805 THEN ASM_REWRITE_TAC[]
1806 THEN EXPAND_TAC "bta"
1808 THEN EXPAND_TAC "vv"
1810 THEN ASM_REWRITE_TAC[azim;ITER1]
1811 THEN ABBREV_TAC`w=(ITER i (rho_node1 FF) v)`
1812 THEN ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
1813 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
1815 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
1816 THEN POP_ASSUM (fun th-> MRESA1_TAC th `i:num`)
1817 THEN REMOVE_THEN "LINH2"(fun th-> MRESA_TAC th [`v:real^3`;`w:real^3`] )
1818 THEN SUBGOAL_THEN`0< i` ASSUME_TAC;
1819 ONCE_REWRITE_TAC[ARITH_RULE`0<i<=> ~(i=0)`]
1821 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1822 THEN UNDISCH_TAC`~(bta 0 = &0)`
1823 THEN EXPAND_TAC"bta"
1825 THEN REWRITE_TAC[ITER;Local_lemmas.AZIM_SPEC_DEGENERATE];
1826 ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
1827 THEN POP_ASSUM(fun th->MRESAL_TAC th[`0:num`;`i:num`][ITER])
1828 THEN SUBGOAL_THEN`azim_in_fan (v,rho_node1 FF v) E < pi`ASSUME_TAC;
1829 ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
1830 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
1831 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
1832 SUBGOAL_THEN`aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt (v,rho_node1 FF v) E`
1834 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
1835 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
1836 THEN DOWN THEN STRIP_TAC
1837 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`vv':real^3`]
1838 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
1839 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
1840 THEN ASM_REWRITE_TAC[azim_in_fan;wedge_in_fan_gt;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;]
1843 THEN UNDISCH_TAC `!v'. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v':real^3}`
1845 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`)
1846 THEN MRESA_TAC Planarity.aff_gt_inter_aff_gt[`vec 0:real^3`;`v:real^3`;`w:real^3`]
1847 THEN MATCH_MP_TAC(SET_RULE`A SUBSET B==> A INTER C SUBSET B`)
1848 THEN REWRITE_TAC[SUBSET]
1849 THEN REPEAT STRIP_TAC
1850 THEN MRESA_TAC Planarity.aff_gt_imp_not_collinear[`vec 0:real^3`;`w:real^3`;`v:real^3`;`x:real^3`]
1851 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`(rho_node1 FF v)`;`w:real^3`;`x:real^3`]
1852 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
1853 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1854 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
1855 THEN POP_ASSUM MP_TAC
1857 THEN REMOVE_ASSUM_TAC
1858 THEN POP_ASSUM (fun th-> MRESA1_TAC th`vv':real^3`)
1859 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`d:real^3`]
1860 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
1861 MRESA_TAC (GEN_ALL PROPERTIES_AFF_GT_SUBSET_WEDGE)
1862 [`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`;`E:(real^3->bool)->bool`;];
1864 THEN SUBGOAL_THEN`interior_angle1 (vec 0) FF v= bta (k-1)` ASSUME_TAC;
1865 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
1866 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
1867 THEN EXPAND_TAC"bta"
1869 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1870 THEN ASM_REWRITE_TAC[ITER1]
1871 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
1872 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`);
1873 ASSUME_TAC2 Local_lemmas.INTERIOR_ANGLE1_POS
1874 THEN POP_ASSUM MP_TAC
1877 THEN SUBGOAL_THEN`?i. i< k-1/\ bta i= &0 /\ bta (i+1)= bta (k-1)` ASSUME_TAC;
1878 ONCE_REWRITE_TAC[SET_RULE`A= ~(~A)`]
1880 THEN UNDISCH_TAC`CARD (V:real^3->bool) = k`
1881 THEN POP_ASSUM MP_TAC
1882 THEN REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM]
1884 THEN SUBGOAL_THEN`!i:num. i< k ==> bta i = &0` ASSUME_TAC;
1887 THEN EXPAND_TAC "bta"
1888 THEN EXPAND_TAC "vv"
1889 THEN REWRITE_TAC[ITER;Local_lemmas.AZIM_SPEC_DEGENERATE];
1890 REWRITE_TAC[ARITH_RULE`SUC i= i+1`]
1891 THEN POP_ASSUM MP_TAC
1892 THEN POP_ASSUM MP_TAC
1893 THEN POP_ASSUM MP_TAC
1894 THEN DISCH_THEN(LABEL_TAC"LINH1")
1895 THEN DISCH_THEN(LABEL_TAC"LINH2")
1896 THEN DISCH_THEN(LABEL_TAC"LINH3")
1898 THEN MP_TAC(ARITH_RULE`i+1< k /\ 3<= k ==> i< k /\ (i< k-1)`)
1900 THEN REMOVE_THEN "LINH3" MP_TAC
1902 THEN REMOVE_THEN "LINH2"(fun th-> MRESA1_TAC th `i:num`)
1903 THEN REMOVE_THEN "LINH1"(fun th-> MRESA1_TAC th `i+1:num`);
1905 THEN DISCH_THEN(LABEL_TAC"LINH1")
1907 THEN MP_TAC(ARITH_RULE`3<= k==> k-1< k/\ 0< k`)
1909 THEN REMOVE_THEN "LINH1"(fun th-> MRESA1_TAC th`k-1:num`)
1910 THEN MP_TAC(REAL_ARITH`&0< bta(k-1)==> ~(bta(k-1)= &0)`)
1911 THEN ASM_REWRITE_TAC[];
1914 THEN MP_TAC(ARITH_RULE`i< k-1 ==> i< k`)
1916 THEN SUBGOAL_THEN`!j. 0 < j /\ j < k /\ ~(j=i) /\ ~(j=i+1)
1917 ==> interior_angle1 (vec 0) FF (ITER j (rho_node1 FF) v) = pi` ASSUME_TAC;
1919 THEN POP_ASSUM MP_TAC
1920 THEN ONCE_REWRITE_TAC[ARITH_RULE`~(j=i+1)<=> (j< i+1\/ i+1< j)`]
1921 THEN MP_TAC(ARITH_RULE`~(j=i:num)<=> (j< i\/ i< j)`)
1922 THEN ASM_REWRITE_TAC[ARITH_RULE`((j < i \/ i < j)
1923 /\(j < i + 1 \/ i + 1 < j)) <=> (j < i \/ i + 1 < j:num)`; SET_RULE`A==>B==>C <=> A/\B ==>C`]
1924 THEN REMOVE_ASSUM_TAC
1926 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
1927 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
1928 THEN POP_ASSUM MP_TAC
1929 THEN EXPAND_TAC "bta"
1931 THEN EXPAND_TAC "vv"
1934 THEN REMOVE_ASSUM_TAC
1935 THEN REMOVE_ASSUM_TAC
1936 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`);
1937 MP_TAC(ARITH_RULE` i<k-1==> i+1=k-1\/ (i+1< k-1 /\ 0< i+1)`)
1939 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1940 THEN POP_ASSUM MP_TAC
1941 THEN POP_ASSUM MP_TAC
1942 THEN UNDISCH_TAC`3<= (k:num)`
1944 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
1945 `FF:real^3#real^3->bool`; `i+1:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
1946 THEN POP_ASSUM MP_TAC
1947 THEN EXPAND_TAC "bta"
1949 THEN EXPAND_TAC "vv"
1952 THEN REMOVE_ASSUM_TAC
1953 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`);
1954 ASSUME_TAC2 Local_lemmas.LOFA_IMP_LT_CARD_SET_V
1955 THEN ABBREV_TAC`u=(ITER i (rho_node1 FF) v)`
1956 THEN ABBREV_TAC`w=(ITER (i+1) (rho_node1 FF) v)`
1957 THEN ABBREV_TAC`s={v,u,w:real^3}`
1958 THEN SUBGOAL_THEN`s SUBSET V:real^3->bool` ASSUME_TAC;
1961 THEN REWRITE_TAC[SET_RULE`{A,B,C} SUBSET V<=> A IN V /\ B IN V /\ C IN V`;IN_ELIM_THM]
1964 THEN REWRITE_TAC[ITER;]
1965 THEN ASM_REWRITE_TAC[]
1966 THEN UNDISCH_TAC`3<=k`
1970 THEN ASM_REWRITE_TAC[];
1971 EXISTS_TAC `i+1:num`
1972 THEN ASM_REWRITE_TAC[]
1973 THEN UNDISCH_TAC`i < k - 1:num`
1975 SUBGOAL_THEN`(!x. x IN V /\ ~(x IN s) ==> (\v. interior_angle1 (vec 0) FF v - pi) x = &0)` ASSUME_TAC;
1977 THEN REWRITE_TAC[IN_ELIM_THM]
1978 THEN ASM_REWRITE_TAC[]
1979 THEN REPEAT STRIP_TAC
1980 THEN POP_ASSUM MP_TAC
1981 THEN POP_ASSUM MP_TAC
1982 THEN DISJ_CASES_TAC(ARITH_RULE`n' = 0 \/ 0< (n':num)`);
1983 ASM_REWRITE_TAC[ITER]
1987 DISJ_CASES_TAC(ARITH_RULE`n' = i \/ ~(n':num=i)`);
1988 ASM_REWRITE_TAC[ITER]
1992 DISJ_CASES_TAC(ARITH_RULE`n' = i+1 \/ ~(n':num=i+1)`);
1993 ASM_REWRITE_TAC[ITER]
1998 THEN UNDISCH_TAC`!j. 0 < j /\ j < k /\ ~(j = i) /\ ~(j = i + 1)
1999 ==> interior_angle1 (vec 0) FF (ITER j (rho_node1 FF) v) = pi`
2001 THEN POP_ASSUM(fun th-> MRESA1_TAC th`n':num`)
2002 THEN REAL_ARITH_TAC;
2003 MRESA_TAC SUM_SUPERSET[`(\v:real^3. interior_angle1 (vec 0) FF v - pi)`;`s:real^3->bool`;`V:real^3->bool`]
2004 THEN REMOVE_ASSUM_TAC
2005 THEN REMOVE_ASSUM_TAC
2006 THEN POP_ASSUM MP_TAC
2007 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; ])
2008 THEN REWRITE_TAC[SET_RULE`{A,B,C} SUBSET V <=> A IN V /\ B IN V /\ C IN V`]
2010 THEN DISJ_CASES_TAC(ARITH_RULE`i = 0 \/ 0< (i:num)`);
2011 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; ARITH_RULE`0+1=1`]
2012 THEN REPEAT STRIP_TAC)
2013 THEN UNDISCH_TAC`bta 1 = bta (k - 1):real`
2014 THEN UNDISCH_TAC `&0 < bta (k - 1):real`
2015 THEN MRESA_TAC( GEN_ALL Local_lemmas.FIRST_EQ0_LAST_LT_PI)
2016 [`E:(real^3->bool)->bool`;`V:real^3->bool`;
2017 `FF:real^3#real^3->bool`;`v:real^3`;`vv:num->real^3`; `bta:num->real`;`CARD (V:real^3->bool)`]
2018 THEN POP_ASSUM MP_TAC
2019 THEN EXPAND_TAC "bta"
2021 THEN EXPAND_TAC "vv"
2024 THEN ASM_REWRITE_TAC[]
2025 THEN REAL_ARITH_TAC;
2026 MP_TAC(ARITH_RULE`i< k-1==> i+1< k`)
2028 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
2029 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`0`;`i:num`][ITER] THEN MRESAL_TAC th[`0`;`i+1:num`][ITER;ARITH_RULE`0< i+1`] THEN MRESAL_TAC th[`i:num`;`i+1:num`][ARITH_RULE`i<i+1`])
2030 THEN UNDISCH_TAC`interior_angle1 (vec 0) FF v = bta (k - 1):real`
2032 THEN REMOVE_ASSUM_TAC
2033 THEN SIMP_TAC[HAS_SIZE; SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
2034 IN_INSERT; NOT_IN_EMPTY]
2035 THEN ASM_REWRITE_TAC[]
2036 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;][SET_RULE`A IN {A,B,C}`]
2037 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;][SET_RULE`B IN {A,B,C}`]
2038 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` w:real^3`;][SET_RULE`C IN {A,B,C}`]
2039 THEN DISJ_CASES_TAC(SET_RULE`(?v1. v1 IN {v,u,w} /\ pi <= interior_angle1 (vec 0) FF v1)\/ ~(?v1. v1 IN {v,u,w} /\ pi <= interior_angle1 (vec 0) FF v1)`);
2041 THEN ASM_REWRITE_TAC[SET_RULE`A IN {B,C,D}<=> A=B \/ A=C\/ A=D`]
2043 THEN POP_ASSUM MP_TAC
2044 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2045 THEN POP_ASSUM MP_TAC
2046 THEN POP_ASSUM MP_TAC
2047 THEN POP_ASSUM MP_TAC
2048 THEN REAL_ARITH_TAC;
2050 THEN POP_ASSUM MP_TAC
2051 THEN POP_ASSUM MP_TAC
2052 THEN POP_ASSUM MP_TAC
2053 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM; REAL_ARITH`~(a<= b) <=> b<a`]
2054 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
2055 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`A IN {A,B,C}`]
2056 THEN MRESAL1_TAC th`u:real^3`[SET_RULE`B IN {A,B,C}`]
2057 THEN MRESAL1_TAC th`w:real^3`[SET_RULE`C IN {A,B,C}`])
2058 THEN REPEAT STRIP_TAC
2059 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`u:real^3`[SET_RULE`B IN {A,B,C}`]
2060 THEN MRESAL1_TAC th`w:real^3`[SET_RULE`C IN {A,B,C}`])
2061 THEN UNDISCH_TAC`interior_angle1 (vec 0) FF v < pi`
2063 THEN SUBGOAL_THEN`u IN aff_gt {vec 0, v} {rho_node1 FF v}` ASSUME_TAC;
2064 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2065 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2066 THEN POP_ASSUM MP_TAC
2067 THEN EXPAND_TAC "bta"
2069 THEN EXPAND_TAC "vv"
2072 THEN REMOVE_ASSUM_TAC
2073 THEN SUBGOAL_THEN`u IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}` ASSUME_TAC;
2074 REWRITE_TAC[IN_ELIM_THM]
2075 THEN EXISTS_TAC`i:num`
2076 THEN ASM_REWRITE_TAC[]
2078 MP_TAC(SET_RULE`{ITER k (rho_node1 FF) v | 0 < k /\ k <= i} SUBSET
2079 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v} /\ u IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i} ==> u IN aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}`)
2080 THEN ASM_REWRITE_TAC[ITER1];
2081 SUBGOAL_THEN`w IN aff_gt {vec 0, v} {ivs_rho_node1 FF v}` ASSUME_TAC;
2082 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2083 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2084 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2085 THEN MP_TAC(ARITH_RULE` i<k-1==> i+1=k-1\/ (i+1< k-1 /\ 0< i+1)`)
2087 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2088 THEN ASM_REWRITE_TAC[]
2089 THEN MATCH_MP_TAC Local_lemmas.DISJOINT_IMP_Z_IN_AFF_GT
2090 THEN ASM_REWRITE_TAC[SET_RULE`DISJOINT {A,B}{C}<=> ~(A=C) /\ ~(B=C)`]
2091 THEN UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2093 THEN POP_ASSUM(fun th-> MRESA1_TAC th`w:real^3`)
2094 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`];
2095 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2096 `FF:real^3#real^3->bool`; `i+1:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2097 THEN POP_ASSUM MP_TAC
2098 THEN EXPAND_TAC "bta"
2100 THEN EXPAND_TAC "vv"
2103 THEN SUBGOAL_THEN`w IN {ITER n (rho_node1 FF) v | i + 1 <= n /\ n < k}` ASSUME_TAC;
2104 REWRITE_TAC[IN_ELIM_THM]
2105 THEN EXISTS_TAC`i+1:num`
2106 THEN ASM_REWRITE_TAC[]
2109 THEN POP_ASSUM MP_TAC
2111 UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2113 THEN POP_ASSUM(fun th-> MRESA1_TAC th`w:real^3` THEN MRESA1_TAC th`u:real^3` THEN ASSUME_TAC th)
2114 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
2115 THEN ASSUME_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS
2116 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2117 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`ivs_rho_node1 FF v`;`w:real^3`]
2118 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2119 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`w:real^3`;`rho_node1 FF v`;`u:real^3`;]
2120 THEN MP_TAC(REAL_ARITH`&0 < azim (vec 0) v (rho_node1 FF v) w ==> ~(azim (vec 0) v (rho_node1 FF v) w= &0)`)
2122 THEN MRESA_TAC AZIM_COMPL[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`w:real^3`]
2123 THEN MP_TAC(REAL_ARITH` azim (vec 0) v (rho_node1 FF v) w < &2 * pi==> ~(&2 * pi - azim (vec 0) v (rho_node1 FF v) w = &0)`)
2124 THEN ASM_REWRITE_TAC[azim]
2126 THEN MRESAL_TAC AZIM_COMPL[`vec 0:real^3`;`v:real^3`;`w:real^3`;`u:real^3`][REAL_ARITH`a-(a- B)=B`]
2127 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC)
2128 THEN REMOVE_ASSUM_TAC
2129 THEN REMOVE_ASSUM_TAC
2130 THEN REMOVE_ASSUM_TAC
2131 THEN REMOVE_ASSUM_TAC
2132 THEN SUBGOAL_THEN`rho_node1 FF u= w` ASSUME_TAC;
2134 THEN REWRITE_TAC[ARITH_RULE`i+1= SUC i`;ITER]
2135 THEN ASM_REWRITE_TAC[];
2136 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2137 THEN SUBGOAL_THEN`ivs_rho_node1 FF w=u` ASSUME_TAC;
2139 THEN REWRITE_TAC[ARITH_RULE`i+1= SUC i`;ITER]
2140 THEN ASM_REWRITE_TAC[]
2141 THEN MRESA_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;];
2142 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2143 THEN SUBGOAL_THEN`!j. j< i==> aff_ge {vec 0:real^3} {v, vv (j+1)}= UNIONS {aff_ge {vec 0} {vv j1, vv (j1+1)}| j1 <= j}`ASSUME_TAC;
2147 THEN REWRITE_TAC[ARITH_RULE`j1<= 0<=> j1= 0`;ARITH_RULE`0+1=1`;ITER1;ITER;
2149 {aff_ge {vec 0} {ITER j1 (rho_node1 FF) v, ITER (j1 + 1) (rho_node1 FF) v} |
2151 0}= aff_ge {vec 0} {ITER 0 (rho_node1 FF) v, ITER (0 + 1) (rho_node1 FF) v}`];
2153 THEN DISCH_THEN(LABEL_TAC"LINH")
2154 THEN REPEAT STRIP_TAC
2155 THEN MP_TAC(ARITH_RULE`SUC j<i /\ i<k-1==> SUC j+1< k/\ j< i /\ j+1<k/\ SUC j <= i/\ SUC(SUC j)<= i /\ SUC j < k/\ SUC (SUC j)<k`)
2157 THEN REMOVE_THEN"LINH" MP_TAC
2159 THEN REWRITE_TAC[ARITH_RULE`j1<= SUC j <=> j1<= j \/ j1= SUC j`
2160 ;SET_RULE`UNIONS {aff_ge {vec 0} {vv j1, vv (j1 + 1)} | j1 <= j \/ j1 = SUC j}
2161 = UNIONS {aff_ge {vec 0} {vv j1, vv (j1 + 1)} | j1 <= j } UNION aff_ge {vec 0} {vv (SUC j), vv (SUC j + 1)}`]
2162 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ARITH_RULE`SUC i= i+1`] THEN ASSUME_TAC (SYM th))
2163 THEN MATCH_MP_TAC AFF_GE_EQ_AFF_GE_UNION
2164 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_CARD_FF_V_EQ
2165 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`SUC j+1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2166 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0< SUC j+1`;ITER])
2167 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`j+1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2168 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0< j+1`;ITER])
2169 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
2171 THEN UNDISCH_TAC`!v'. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v':real^3}`
2173 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (SUC j + 1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2174 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (j + 1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2175 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (j + 1) (rho_node1 FF) v`]
2176 THEN MRESAL_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (SUC j + 1) (rho_node1 FF) v`][ARITH_RULE`SUC i=i+1`]
2177 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2) [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` ITER (j + 1) (rho_node1 FF) v:real^3`;]
2178 THEN MRESA_TAC th3[`vec 0:real^3`;`ITER (j + 1) (rho_node1 FF) v:real^3`;`rho_node1 FF
2179 (ITER (j + 1) (rho_node1 FF) v)`]
2180 THEN REMOVE_ASSUM_TAC
2181 THEN POP_ASSUM MP_TAC
2182 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2184 THEN MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2185 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2186 THEN POP_ASSUM MP_TAC
2187 THEN EXPAND_TAC "bta"
2189 THEN EXPAND_TAC "vv"
2192 THEN REMOVE_ASSUM_TAC
2193 THEN ABBREV_TAC`g=rho_node1 FF (ITER j (rho_node1 FF) v)`
2194 THEN SUBGOAL_THEN`g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}` ASSUME_TAC;
2195 REWRITE_TAC[IN_ELIM_THM]
2196 THEN EXISTS_TAC`SUC j`
2197 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER];
2198 MP_TAC(SET_RULE` g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}
2199 /\ {ITER k (rho_node1 FF) v | 0 < k /\ k <= i} SUBSET
2200 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}
2202 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}`)
2204 THEN UNDISCH_TAC `~collinear {vec 0, v, ITER (j + 1) (rho_node1 FF) v}`
2205 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2207 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`ivs_rho_node1 FF v`;`ITER 1 (rho_node1 FF) v`;`g:real^3`][ITER1]
2208 THEN SUBGOAL_THEN`rho_node1 FF g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}` ASSUME_TAC;
2209 REWRITE_TAC[IN_ELIM_THM]
2210 THEN EXISTS_TAC`SUC (SUC j)`
2211 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER];
2212 MP_TAC(SET_RULE` rho_node1 FF g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}
2213 /\ {ITER k (rho_node1 FF) v | 0 < k /\ k <= i} SUBSET
2214 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}
2215 ==> rho_node1 FF g IN
2216 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}`)
2218 THEN UNDISCH_TAC `~collinear {vec 0, v, ITER (SUC j + 1) (rho_node1 FF) v}`
2219 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2221 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`ivs_rho_node1 FF v`;`ITER 1 (rho_node1 FF) v`;`rho_node1 FF g:real^3`][ITER1]
2222 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`ivs_rho_node1 FF v`;`g:real^3`;`rho_node1 FF g:real^3`][ITER1]
2223 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0, v:real^3}`;`{g:real^3}`]
2224 THEN MP_TAC(SET_RULE`rho_node1 FF g IN aff_gt {vec 0, v} { g}
2225 /\ aff_gt {vec 0, v} {g} SUBSET
2226 aff_ge {vec 0, v} {g}
2227 ==> rho_node1 FF g IN
2228 aff_ge {vec 0, v} {g}`)
2230 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v:real^3`;`g:real^3`;` rho_node1 FF g:real^3`]
2231 THEN POP_ASSUM MP_TAC
2232 THEN UNDISCH_TAC`UNIONS {aff_ge {vec 0} {vv j1, vv (j1 + 1)} | j1 <= j} =
2233 aff_ge {vec 0:real^3} {v, vv (j + 1)}`
2234 THEN EXPAND_TAC "vv"
2235 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2236 THEN ASM_REWRITE_TAC[]
2238 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;UNIONS;IN_ELIM_THM])
2240 THEN POP_ASSUM MP_TAC
2242 THEN UNDISCH_TAC`local_fan (V:real^3->bool,E,FF)`
2244 THEN POP_ASSUM(fun th-> MP_TAC th
2245 THEN REWRITE_TAC[local_fan;]
2248 THEN REMOVE_ASSUM_TAC
2249 THEN REMOVE_ASSUM_TAC
2250 THEN REMOVE_ASSUM_TAC
2252 THEN UNDISCH_TAC`!i. ITER i (rho_node1 FF) v IN V`
2254 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC(SUC j)`[ITER] THEN MRESA1_TAC th`j1:num` )
2255 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_EE_TWO_ELMS
2256 )[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (ITER j1 (rho_node1 FF) v)`;`ITER j1 (rho_node1 FF) v`]
2257 THEN MP_TAC(SET_RULE`EE (rho_node1 FF (ITER j1 (rho_node1 FF) v)) E =
2258 {rho_node1 FF (rho_node1 FF (ITER j1 (rho_node1 FF) v)), ITER j1
2263 v IN EE (rho_node1 FF (ITER j1 (rho_node1 FF) v)) E `)
2264 THEN REWRITE_TAC[EE;IN_ELIM_THM]
2265 THEN REWRITE_TAC[GSYM EE]
2267 THEN POP_ASSUM MP_TAC
2268 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2270 THEN MP_TAC(ARITH_RULE`j1<= j==> j1< SUC(SUC j) /\ SUC j1< SUC(SUC j)`)
2272 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
2273 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j1:num`;`SUC(SUC j)`;][ITER]
2274 THEN MRESAL_TAC th[`SUC j1:num`;`SUC(SUC j)`;][ITER])
2275 THEN MRESA_TAC (GEN_ALL Local_lemmas.FAN_IN_AFF_GE_IMP_EQ)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`vec 0:real^3`;`ITER j1 (rho_node1 FF) v`;`rho_node1 FF g`;`rho_node1 FF (ITER j1 (rho_node1 FF) v)`];
2277 THEN MP_TAC(ARITH_RULE`0< i==> i-1< i/\ i-1+1=i`)
2280 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i-1`)
2281 THEN SUBGOAL_THEN`ivs_rho_node1 FF u IN aff_ge {vec 0} {v,u}` ASSUME_TAC;
2284 THEN ASM_REWRITE_TAC[]
2286 THEN REWRITE_TAC[IN_ELIM_THM;UNIONS]
2287 THEN EXISTS_TAC`aff_ge {vec 0}
2288 {ITER (i-1) (rho_node1 FF) v, ITER (i-1 + 1) (rho_node1 FF) v}`
2291 THEN ASM_REWRITE_TAC[ARITH_RULE`A-1<=A-1`];
2293 THEN MRESA_TAC( GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`u:real^3`]
2294 THEN POP_ASSUM MP_TAC
2295 THEN ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2296 THEN POP_ASSUM(fun th-> MRESA1_TAC th`u:real^3`)
2297 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2299 THEN REWRITE_TAC[ITER_ADD; ]
2300 THEN MP_TAC(ARITH_RULE`0<i /\ 3<= k ==>k -1 + i = k + (i-1)`)
2302 THEN ONCE_REWRITE_TAC[GSYM ITER_ADD; ]
2303 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
2304 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i-1:num`)
2305 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID
2306 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (i - 1) (rho_node1 FF) v`)
2307 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2309 THEN MRESA_TAC Planarity.point_in_aff_ge[`vec 0:real^3`;`ITER (i - 1) (rho_node1 FF) v`;`u:real^3`];
2310 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2311 THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
2312 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`u:real^3`;`V:real^3->bool`]
2313 THEN POP_ASSUM(fun th-> MRESA1_TAC th`k-1:num`)
2314 THEN SUBGOAL_THEN`azim (vec 0) u w (ivs_rho_node1 FF u)= azim (vec 0) u w v` ASSUME_TAC;
2315 DISJ_CASES_TAC(SET_RULE`v= ivs_rho_node1 FF u \/ ~(ivs_rho_node1 FF u= v)`);
2317 UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2319 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ivs_rho_node1 FF u`)
2320 THEN MRESA_TAC Topology.aff_ge_inter_aff_ge[`vec 0:real^3`;`v:real^3`;`u:real^3`]
2321 THEN MP_TAC(SET_RULE`ivs_rho_node1 FF u IN aff_ge {vec 0} {v, u}
2322 /\ aff_ge {vec 0} {v, u} =
2323 aff_ge {vec 0, v} {u} INTER aff_ge {vec 0, u} {v}
2324 ==> ivs_rho_node1 FF u IN aff_ge {vec 0,u} { v}`)
2326 THEN MRESA_TAC( GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`u:real^3`]
2327 THEN MRESA_TAC AZIM_EQ_0_GE[`vec 0:real^3`;`u:real^3`;`ivs_rho_node1 FF u`;`v:real^3`]
2328 THEN POP_ASSUM MP_TAC
2329 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2331 THEN MRESAL_TAC Fan.sum5_azim_fan[`vec 0:real^3`;`u:real^3`;`w:real^3`;`(ivs_rho_node1 FF u)`;`v:real^3`][azim]
2332 THEN POP_ASSUM MP_TAC
2333 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2334 THEN ASM_REWRITE_TAC[]
2335 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2) [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;]
2336 THEN POP_ASSUM MP_TAC
2337 THEN UNDISCH_TAC`ITER (i + 1) (rho_node1 FF) v = w`
2338 THEN REWRITE_TAC[ARITH_RULE`i+1=SUC i`;ITER]
2341 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2343 THEN REAL_ARITH_TAC;
2345 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2346 THEN SUBGOAL_THEN`!j. j< k-i-1==> aff_ge {vec 0:real^3} {v, vv (k-j-1)}= UNIONS {aff_ge {vec 0} {vv (k-j1-1), vv (k-j1)}| j1 <= j}`ASSUME_TAC;
2350 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID
2351 THEN REWRITE_TAC[ARITH_RULE`j1<= 0<=> j1= 0`;ARITH_RULE`k-0=k`;ITER1;ITER;
2354 {ITER (k - j1 - 1) (rho_node1 FF) v, ITER (k - j1) (rho_node1 FF) v} |
2357 {ITER (k - 0 - 1) (rho_node1 FF) v, ITER (k - 0) (rho_node1 FF) v}`]
2358 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2359 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
2362 THEN DISCH_THEN(LABEL_TAC"LINH")
2363 THEN REPEAT STRIP_TAC
2364 THEN MP_TAC(ARITH_RULE`SUC j<k-i-1 /\ 0<i /\i<k-1==> i+1< k-SUC j/\ j< k-i-1/\ k-j-1-1<k /\ 0< k-j-1-1 /\ k-j-1< k /\ 0< k-j-1`)
2366 THEN REMOVE_THEN"LINH" MP_TAC
2368 THEN REWRITE_TAC[ARITH_RULE`j1<= SUC j <=> j1<= j \/ j1= SUC j`
2370 {aff_ge {vec 0} {vv (k - j1 - 1), vv (k - j1)} | j1 <= j \/ j1 = SUC j }
2372 {aff_ge {vec 0} {vv (k - j1 - 1), vv (k - j1)} | j1 <= j} UNION aff_ge {vec 0} {vv (k-SUC j-1), vv (k-SUC j)}`]
2373 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ARITH_RULE`SUC i= i+1`] THEN ASSUME_TAC (SYM th))
2374 THEN GEN_REWRITE_TAC(RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
2375 THEN REWRITE_TAC[ARITH_RULE`k-(j+1)=k-j-1`]
2376 THEN MATCH_MP_TAC AFF_GE_EQ_AFF_GE_UNION
2377 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_CARD_FF_V_EQ
2378 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`k-j-1-1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2379 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ITER])
2380 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`k-j-1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2381 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0< j+1`;ITER])
2382 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
2384 THEN UNDISCH_TAC`!v'. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v':real^3}`
2386 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (k-j - 1-1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2387 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (k-j-1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2388 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (k-j-1 - 1) (rho_node1 FF) v`]
2389 THEN MRESAL_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (k-j-1) (rho_node1 FF) v`][ARITH_RULE`SUC i=i+1`]
2390 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2) [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` ITER (k-j-1- 1) (rho_node1 FF) v:real^3`;]
2391 THEN MRESA_TAC th3[`vec 0:real^3`;`ITER (k-j -1- 1) (rho_node1 FF) v:real^3`;`rho_node1 FF
2392 (ITER (k-j - 1-1) (rho_node1 FF) v)`]
2393 THEN REMOVE_ASSUM_TAC
2394 THEN POP_ASSUM MP_TAC
2395 THEN MP_TAC(ARITH_RULE`0< k - j - 1 - 1 ==> SUC (k - j - 1 - 1)= k-j-1`)
2397 THEN REWRITE_TAC[GSYM ITER]
2399 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2400 THEN ASM_REWRITE_TAC[]
2401 THEN MP_TAC(ARITH_RULE` i<k-1==> i+1=k-1\/ (i+1< k-1 /\ 0< i+1)`)
2403 UNDISCH_TAC`SUC j < k - i -1`
2404 THEN POP_ASSUM MP_TAC
2406 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2407 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2408 THEN MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2409 `FF:real^3#real^3->bool`; `i+1:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2410 THEN POP_ASSUM MP_TAC
2411 THEN EXPAND_TAC "bta"
2413 THEN EXPAND_TAC "vv"
2416 THEN ABBREV_TAC`g=ITER (k-j-1-1) (rho_node1 FF) v`
2417 THEN SUBGOAL_THEN`ITER (k - j - 1) (rho_node1 FF) v= rho_node1 FF g` ASSUME_TAC;
2419 THEN REWRITE_TAC[GSYM ITER]
2420 THEN ASM_REWRITE_TAC[];
2421 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN ASSUME_TAC th)
2422 THEN SUBGOAL_THEN`g IN {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k}` ASSUME_TAC;
2423 REWRITE_TAC[IN_ELIM_THM]
2424 THEN EXISTS_TAC`k-j-1-1`
2425 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER]
2426 THEN MP_TAC(ARITH_RULE`SUC j < k - i - 1 /\ 0<i==> i+1<= k-j-1-1`)
2428 MP_TAC(SET_RULE` g IN {ITER n (rho_node1 FF) v | i+1<=n /\ n < k}
2429 /\ {ITER n (rho_node1 FF) v | i+1<=n /\ n < k} SUBSET
2430 aff_gt {vec 0, v} {ITER (k-1) (rho_node1 FF) v}
2432 aff_gt {vec 0, v} {ITER (k-1) (rho_node1 FF) v}`)
2434 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`ITER (k-1) (rho_node1 FF) v`;`g:real^3`][ITER1]
2435 THEN SUBGOAL_THEN`rho_node1 FF g IN {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k}` ASSUME_TAC;
2436 REWRITE_TAC[IN_ELIM_THM]
2437 THEN EXISTS_TAC`k-j-1`
2438 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER]
2439 THEN MP_TAC(ARITH_RULE`SUC j < k - i - 1 /\ 0<i==> i+1<= k-j-1`)
2441 MP_TAC(SET_RULE` rho_node1 FF g IN {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k}
2442 /\ {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k} SUBSET
2443 aff_gt {vec 0, v} {ITER (k-1) (rho_node1 FF) v}
2444 ==> rho_node1 FF g IN
2445 aff_gt {vec 0, v} {ITER(k-1) (rho_node1 FF) v}`)
2447 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`ITER (k-1) (rho_node1 FF) v`;`rho_node1 FF g:real^3`][ITER1]
2448 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`rho_node1 FF g:real^3`;`g:real^3`][ITER1]
2449 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0, v:real^3}`;`{rho_node1 FF g:real^3}`]
2450 THEN MP_TAC(SET_RULE`g IN aff_gt {vec 0, v} {rho_node1 FF g}
2451 /\ aff_gt {vec 0, v} {rho_node1 FF g} SUBSET
2452 aff_ge {vec 0, v} {rho_node1 FF g}
2454 aff_ge {vec 0, v} {rho_node1 FF g}`)
2456 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2457 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v:real^3`;` rho_node1 FF g:real^3`;` g:real^3`]
2458 THEN POP_ASSUM MP_TAC
2459 THEN UNDISCH_TAC`UNIONS {aff_ge {vec 0} {vv (k - j1 - 1), vv (k - j1)} | j1 <= j} =
2460 aff_ge {vec 0:real^3} {v, vv (k - j - 1)}`
2461 THEN EXPAND_TAC "vv"
2462 THEN ASM_REWRITE_TAC[]
2464 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;UNIONS;IN_ELIM_THM])
2466 THEN POP_ASSUM MP_TAC
2468 THEN UNDISCH_TAC`local_fan (V:real^3->bool,E,FF)`
2470 THEN POP_ASSUM(fun th-> MP_TAC th
2471 THEN REWRITE_TAC[local_fan;]
2474 THEN REMOVE_ASSUM_TAC
2475 THEN REMOVE_ASSUM_TAC
2476 THEN REMOVE_ASSUM_TAC
2478 THEN UNDISCH_TAC`!i. ITER i (rho_node1 FF) v IN V`
2480 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`k-j-1-1`[ITER] THEN MRESA1_TAC th`k-j1-1:num` )
2481 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_EE_TWO_ELMS
2482 )[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)`;`ITER (k-j1-1) (rho_node1 FF) v`]
2483 THEN MP_TAC(SET_RULE`EE (rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)) E =
2484 {rho_node1 FF (rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)), ITER (k-j1-1)
2489 v IN EE (rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)) E `)
2490 THEN REWRITE_TAC[EE;IN_ELIM_THM]
2491 THEN REWRITE_TAC[GSYM EE]
2493 THEN POP_ASSUM MP_TAC
2494 THEN ASM_REWRITE_TAC[GSYM ITER]
2495 THEN MP_TAC(ARITH_RULE`j1<=j /\ SUC j< k-i-1 /\ 0<i ==> SUC (k-j1-1)= k-j1 /\ k-j-1-1< k-j1 /\ k-j-1-1< k-j1-1 /\ k-j1-1<k`)
2497 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2499 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
2500 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k-j-1-1:num`;`k-j1-1`;][ITER] THEN ASSUME_TAC th)
2501 THEN SUBGOAL_THEN`~(ITER (k - j1) (rho_node1 FF) v = g)` ASSUME_TAC;
2502 MP_TAC(ARITH_RULE`j < k - i - 1 /\ j1<=j /\ 0< i==> k-j1=k \/ k- j1< k`)
2504 ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID
2505 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`);
2507 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k-j-1-1:num`;`k-j1:num`;][ITER] THEN ASSUME_TAC th)
2508 THEN POP_ASSUM MP_TAC
2509 THEN DISCH_THEN(LABEL_TAC"linh")
2511 THEN REMOVE_THEN"linh" MP_TAC
2513 MRESA_TAC (GEN_ALL Local_lemmas.FAN_IN_AFF_GE_IMP_EQ)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`vec 0:real^3`;`ITER (k-j1-1) (rho_node1 FF) v`;`g:real^3`;`ITER (k-j1) (rho_node1 FF) v`];
2515 THEN MP_TAC(ARITH_RULE`i< k-1/\ 0< i ==> k-i-1-1< k-i-1 /\ k - (k - i - 1 - 1) - 1= SUC(i) /\ k - (k - i - 1 - 1) = SUC(SUC i)`)
2518 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k-i-1-1`[ARITH_RULE`SUC i=i+1`])
2519 THEN SUBGOAL_THEN`rho_node1 FF w IN aff_ge {vec 0} {v,w}` ASSUME_TAC ;
2522 THEN ASM_REWRITE_TAC[]
2524 THEN REWRITE_TAC[IN_ELIM_THM;UNIONS]
2525 THEN EXISTS_TAC`aff_ge {vec 0}
2526 {ITER (k-(k - i - 1 - 1)-1) (rho_node1 FF) v, ITER (k-(k - i - 1 - 1)) (rho_node1 FF) v}`
2528 EXISTS_TAC`k - i - 1 - 1:num`
2529 THEN ASM_REWRITE_TAC[ARITH_RULE`A-1<=A-1`];
2530 ASM_REWRITE_TAC[ARITH_RULE`SUC i=i+1`]
2531 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+1= SUC i`]
2532 THEN ASM_REWRITE_TAC[ITER]
2533 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`w:real^3`]
2534 THEN MRESA_TAC Planarity.point_in_aff_ge[`vec 0:real^3`;`w:real^3`;`rho_node1 FF w:real^3`];
2535 SUBGOAL_THEN`azim (vec 0) w (rho_node1 FF w) u= azim (vec 0) w v u` ASSUME_TAC;
2536 DISJ_CASES_TAC(SET_RULE`v= rho_node1 FF w \/ ~(rho_node1 FF w= v)`);
2538 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
2539 THEN POP_ASSUM(fun th-> MRESA1_TAC th`w:real^3`)
2540 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ITER1])
2541 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`w:real^3`]
2542 THEN UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2544 THEN POP_ASSUM(fun th-> MRESA1_TAC th`rho_node1 FF w`)
2545 THEN MRESA_TAC Topology.aff_ge_inter_aff_ge[`vec 0:real^3`;`v:real^3`;`w:real^3`]
2546 THEN MP_TAC(SET_RULE`rho_node1 FF w IN aff_ge {vec 0} {v, w}
2547 /\ aff_ge {vec 0} {v, w} =
2548 aff_ge {vec 0, v} {w} INTER aff_ge {vec 0, w} {v}
2549 ==> rho_node1 FF w IN aff_ge {vec 0,w} { v}`)
2551 THEN MRESA_TAC AZIM_EQ_0_GE[`vec 0:real^3`;`w:real^3`;`rho_node1 FF w`;`v:real^3`]
2552 THEN POP_ASSUM MP_TAC
2553 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2555 THEN MRESAL_TAC Fan.sum5_azim_fan[`vec 0:real^3`;`w:real^3`;`u:real^3`;`(rho_node1 FF w)`;`v:real^3`][azim]
2556 THEN POP_ASSUM MP_TAC
2557 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2558 THEN ASM_REWRITE_TAC[]
2559 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
2560 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;]
2561 THEN POP_ASSUM MP_TAC
2562 THEN UNDISCH_TAC`ITER (i + 1) (rho_node1 FF) v = w`
2563 THEN REWRITE_TAC[ARITH_RULE`i+1=SUC i`;ITER]
2566 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2568 THEN POP_ASSUM MP_TAC
2569 THEN REWRITE_TAC[REAL_ARITH`a+ &0=a`]
2571 THEN MP_TAC(REAL_ARITH`&0< azim (vec 0) w (rho_node1 FF w) u ==> ~(azim (vec 0) w (rho_node1 FF w) u = &0)`)
2573 THEN MRESAL_TAC AZIM_COMPL[`vec 0:real^3`;`w:real^3`;`rho_node1 FF w:real^3`;`u:real^3`][REAL_ARITH`a-(a- B)=B`]
2574 THEN POP_ASSUM MP_TAC
2575 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2577 THEN MP_TAC(REAL_ARITH` azim (vec 0) w (rho_node1 FF w) u < &2 * pi ==> ~(&2 * pi - azim (vec 0) w (rho_node1 FF w) u = &0)`)
2578 THEN ASM_REWRITE_TAC[azim]
2580 THEN MRESAL_TAC AZIM_COMPL[`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`][REAL_ARITH`a-(a- B)=B`]
2581 THEN POP_ASSUM MP_TAC
2582 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2585 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2586 THEN MP_TAC(REAL_ARITH`&0< azim (vec 0) v u w /\ azim (vec 0) v u w < pi ==> ~(azim (vec 0) v u w = &0 \/ azim (vec 0) v u (w:real^3) = pi)`)
2588 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
2589 THEN POP_ASSUM (fun th->
2590 MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
2592 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2594 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
2596 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
2599 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
2600 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
2601 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
2602 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`]
2603 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
2604 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
2605 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
2606 THEN MRESAL_TAC VOLUME_SOLID_TRIANGLE[`&1:real`;`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`][REAL_ARITH`&0< &1`]
2607 THEN POP_ASSUM MP_TAC
2609 THEN MRESA_TAC MEASURABLE_BALL_AFF_GT[`vec 0:real^3`;`&1`;`{vec 0:real^3}`;`{v,u,w:real^3}`]
2611 THEN MP_TAC(MESON[volume_props]`measurable (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w})==> vol (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w}) >= &0`)
2613 THEN POP_ASSUM MP_TAC
2614 THEN REAL_ARITH_TAC]);;