1 (* ========================================================================= *)
\r
2 (* Flyspeck "polar fan" formalization. *)
\r
3 (* ========================================================================= *)
\r
5 (* ------------------------------------------------------------------------- *)
\r
6 (* Some natural lemmas that I should perhaps put in Multivariate/flyspeck.ml *)
\r
7 (* ------------------------------------------------------------------------- *)
\r
9 module Polar_fan = struct
\r
11 let DIHV_ARCV = prove
\r
13 orthogonal (e - u) (v - u) /\ orthogonal (e - u) (w - u) /\ ~(e = u)
\r
14 ==> dihV u e v w = arcV u v w`,
\r
15 GEOM_ORIGIN_TAC `u:real^N` THEN
\r
16 REWRITE_TAC[dihV; orthogonal; VECTOR_SUB_RZERO] THEN
\r
17 CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
\r
18 SIMP_TAC[DOT_SYM; VECTOR_MUL_LZERO; VECTOR_SUB_RZERO] THEN
\r
19 REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO] THEN
\r
20 REWRITE_TAC[VECTOR_ANGLE_LMUL; VECTOR_ANGLE_RMUL] THEN
\r
21 SIMP_TAC[DOT_POS_LE; DOT_EQ_0]);;
\r
23 let AZIM_DIHV_SAME_STRONG = prove
\r
24 (`!v w v1 v2:real^3.
\r
25 ~collinear {v,w,v1} /\ ~collinear {v,w,v2} /\
\r
26 azim v w v1 v2 <= pi
\r
27 ==> azim v w v1 v2 = dihV v w v1 v2`,
\r
28 REWRITE_TAC[REAL_LE_LT] THEN
\r
29 MESON_TAC[AZIM_DIHV_SAME; AZIM_DIHV_EQ_PI]);;
\r
31 let AZIM_ARCV = prove
\r
33 orthogonal (e - u) (v - u) /\ orthogonal (e - u) (w - u) /\
\r
34 ~collinear{u,e,v} /\ ~collinear{u,e,w} /\
\r
36 ==> azim u e v w = arcV u v w`,
\r
37 REPEAT GEN_TAC THEN ASM_CASES_TAC `u:real^3 = e` THENL
\r
38 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
\r
39 STRIP_TAC THEN ASM_SIMP_TAC[GSYM DIHV_ARCV] THEN
\r
40 MATCH_MP_TAC AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[]);;
\r
42 let PLANE_AFFINE_HULL_3 = prove
\r
43 (`!a b c:real^N. plane(affine hull {a,b,c}) <=> ~collinear{a,b,c}`,
\r
44 REWRITE_TAC[plane] THEN MESON_TAC[COLLINEAR_AFFINE_HULL_COLLINEAR]);;
\r
46 let AFFINE_HULL_3_GENERATED = prove
\r
48 s SUBSET affine hull {u,v,w} /\ ~collinear s
\r
49 ==> affine hull {u,v,w} = affine hull s`,
\r
50 REWRITE_TAC[COLLINEAR_AFF_DIM; INT_NOT_LE] THEN REPEAT STRIP_TAC THEN
\r
51 CONV_TAC SYM_CONV THEN
\r
52 GEN_REWRITE_TAC RAND_CONV [GSYM HULL_HULL] THEN
\r
53 MATCH_MP_TAC AFF_DIM_EQ_AFFINE_HULL THEN ASM_REWRITE_TAC[] THEN
\r
54 MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&2:int` THEN
\r
55 CONJ_TAC THENL [ALL_TAC; ASM_INT_ARITH_TAC] THEN
\r
56 REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN
\r
57 W(MP_TAC o PART_MATCH (lhand o rand) AFF_DIM_LE_CARD o lhand o goal_concl) THEN
\r
58 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN
\r
59 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] INT_LE_TRANS) THEN
\r
60 REWRITE_TAC[INT_LE_SUB_RADD; INT_OF_NUM_ADD; INT_OF_NUM_LE] THEN
\r
61 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN ARITH_TAC);;
\r
63 let COLLINEAR_AZIM_0_OR_PI = prove
\r
64 (`!u e v w. collinear {u,v,w} ==> azim u e v w = &0 \/ azim u e v w = pi`,
\r
65 REPEAT STRIP_TAC THEN
\r
66 ASM_CASES_TAC `collinear{u:real^3,e,v}` THEN
\r
67 ASM_SIMP_TAC[AZIM_DEGENERATE] THEN
\r
68 ASM_CASES_TAC `collinear{u:real^3,e,w}` THEN
\r
69 ASM_SIMP_TAC[AZIM_DEGENERATE] THEN
\r
70 ASM_SIMP_TAC[AZIM_EQ_0_PI_EQ_COPLANAR] THEN
\r
71 ONCE_REWRITE_TAC[SET_RULE `{u,e,v,w} = {u,v,w,e}`] THEN
\r
72 ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);;
\r
74 let ANGLES_ADD_AFF_GE = prove
\r
76 ~(v = u) /\ ~(w = u) /\ ~(x = u) /\ x IN aff_ge {u} {v,w}
\r
77 ==> angle(v,u,x) + angle(x,u,w) = angle(v,u,w)`,
\r
78 GEOM_ORIGIN_TAC `u:real^N` THEN REPEAT GEN_TAC THEN
\r
79 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
80 ASM_SIMP_TAC[AFF_GE_1_2_0] THEN
\r
81 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
82 MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
\r
83 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
\r
84 SUBGOAL_THEN `a = &0 /\ b = &0 \/ &0 < a + b` STRIP_ASSUME_TAC THENL
\r
85 [ASM_REAL_ARITH_TAC;
\r
86 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID];
\r
88 DISCH_TAC THEN MP_TAC(ISPECL
\r
89 [`v:real^N`; `w:real^N`; `inv(a + b) % x:real^N`; `vec 0:real^N`]
\r
90 ANGLES_ADD_BETWEEN) THEN
\r
91 ASM_REWRITE_TAC[angle; VECTOR_SUB_RZERO] THEN
\r
92 ASM_SIMP_TAC[VECTOR_ANGLE_RMUL; VECTOR_ANGLE_LMUL;
\r
93 REAL_INV_EQ_0; REAL_LE_INV_EQ; REAL_LT_IMP_NZ; REAL_LT_IMP_LE] THEN
\r
94 DISCH_THEN MATCH_MP_TAC THEN
\r
95 REWRITE_TAC[BETWEEN_IN_SEGMENT; CONVEX_HULL_2; SEGMENT_CONVEX_HULL] THEN
\r
96 REWRITE_TAC[IN_ELIM_THM] THEN
\r
97 MAP_EVERY EXISTS_TAC [`a / (a + b):real`; `b / (a + b):real`] THEN
\r
98 ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE; VECTOR_ADD_LDISTRIB] THEN
\r
99 REWRITE_TAC[VECTOR_MUL_ASSOC; real_div; REAL_MUL_AC] THEN
\r
100 UNDISCH_TAC `&0 < a + b` THEN CONV_TAC REAL_FIELD);;
\r
102 let AFF_GE_SCALE_LEMMA = prove
\r
104 &0 < a /\ ~(v = vec 0)
\r
105 ==> aff_ge {vec 0} {a % u,v} = aff_ge {vec 0} {u,v}`,
\r
106 REPEAT STRIP_TAC THEN ASM_CASES_TAC `u:real^N = vec 0` THEN
\r
107 ASM_REWRITE_TAC[VECTOR_MUL_RZERO] THEN
\r
108 ASM_SIMP_TAC[AFF_GE_1_2_0; VECTOR_MUL_EQ_0; REAL_LT_IMP_NZ;
\r
109 SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
\r
110 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; SUBSET; FORALL_IN_GSPEC] THEN
\r
111 CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`b:real`; `c:real`] THEN
\r
112 REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THENL
\r
113 [EXISTS_TAC `a * b:real`; EXISTS_TAC `b / a:real`] THEN
\r
114 EXISTS_TAC `c:real` THEN
\r
115 ASM_SIMP_TAC[REAL_LE_DIV; REAL_LE_MUL; REAL_LT_IMP_LE] THEN
\r
116 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
\r
117 REPLICATE_TAC 2 (AP_THM_TAC THEN AP_TERM_TAC) THEN
\r
118 UNDISCH_TAC `&0 < a` THEN CONV_TAC REAL_FIELD);;
\r
120 let AZIM_SAME_WITHIN_AFF_GE = prove
\r
122 v IN aff_ge {a} {u,w} /\ ~collinear{a,u,v} /\ ~collinear{a,u,w}
\r
123 ==> azim a u v z = azim a u w z`,
\r
124 GEOM_ORIGIN_TAC `a:real^3` THEN
\r
125 GEOM_BASIS_MULTIPLE_TAC 3 `u:real^3` THEN
\r
126 X_GEN_TAC `u:real` THEN ASM_CASES_TAC `u = &0` THEN
\r
127 ASM_SIMP_TAC[AZIM_DEGENERATE; VECTOR_MUL_LZERO; REAL_LE_LT] THEN
\r
128 ASM_SIMP_TAC[AZIM_SPECIAL_SCALE; COLLINEAR_SPECIAL_SCALE] THEN
\r
129 DISCH_TAC THEN REPEAT GEN_TAC THEN
\r
130 ASM_CASES_TAC `w:real^3 = vec 0` THENL
\r
131 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
\r
132 ASM_SIMP_TAC[AFF_GE_SCALE_LEMMA] THEN
\r
133 REWRITE_TAC[COLLINEAR_BASIS_3; AZIM_ARG] THEN
\r
134 ASM_SIMP_TAC[AFF_GE_1_2_0; BASIS_NONZERO; ARITH; DIMINDEX_3;
\r
135 SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
\r
136 REWRITE_TAC[IMP_CONJ; LEFT_IMP_EXISTS_THM; IN_ELIM_THM] THEN
\r
137 MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN DISCH_TAC THEN DISCH_TAC THEN
\r
138 DISCH_THEN(MP_TAC o AP_TERM `dropout 3:real^3->real^2`) THEN
\r
139 REWRITE_TAC[DROPOUT_ADD; DROPOUT_MUL; DROPOUT_BASIS_3] THEN
\r
140 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
\r
141 DISCH_THEN SUBST1_TAC THEN REPEAT DISCH_TAC THEN
\r
142 REWRITE_TAC[COMPLEX_CMUL] THEN
\r
143 REWRITE_TAC[complex_div; COMPLEX_INV_MUL; GSYM CX_INV] THEN
\r
144 ONCE_REWRITE_TAC[COMPLEX_RING `a * b * c:complex = b * a * c`] THEN
\r
145 MATCH_MP_TAC ARG_MUL_CX THEN REWRITE_TAC[REAL_LT_INV_EQ] THEN
\r
146 ASM_REWRITE_TAC[REAL_LT_LE] THEN ASM_MESON_TAC[VECTOR_MUL_LZERO]);;
\r
148 let AZIM_SAME_WITHIN_AFF_GE_ALT = prove
\r
150 v IN aff_ge {a} {u,w} /\ ~collinear{a,u,v} /\ ~collinear{a,u,w}
\r
151 ==> azim a u z v = azim a u z w`,
\r
152 REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
153 FIRST_ASSUM(ASSUME_TAC o MATCH_MP AZIM_SAME_WITHIN_AFF_GE) THEN
\r
154 ASM_CASES_TAC `collinear {a:real^3,u,z}` THEN
\r
155 ASM_SIMP_TAC[AZIM_DEGENERATE] THEN
\r
156 W(MP_TAC o PART_MATCH (lhs o rand) AZIM_COMPL o lhand o goal_concl) THEN
\r
157 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
\r
158 W(MP_TAC o PART_MATCH (lhs o rand) AZIM_COMPL o rand o goal_concl) THEN
\r
161 let COLLINEAR_WITHIN_AFF_GE_COLLINEAR = prove
\r
163 v IN aff_ge {a} {u,w} /\ collinear{a,u,w} ==> collinear{a,v,w}`,
\r
164 GEOM_ORIGIN_TAC `a:real^N` THEN REPEAT GEN_TAC THEN
\r
165 ASM_CASES_TAC `w:real^N = vec 0` THENL
\r
166 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
\r
167 ASM_CASES_TAC `u:real^N = vec 0` THENL
\r
168 [ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF] THEN
\r
169 ASM_REWRITE_TAC[SET_RULE `{a} DIFF {a,b} = {}`] THEN
\r
170 REWRITE_TAC[GSYM CONVEX_HULL_AFF_GE] THEN
\r
171 ONCE_REWRITE_TAC[SET_RULE `{z,v,w} = {z,w,v}`] THEN
\r
172 ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN
\r
173 MESON_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET];
\r
174 ONCE_REWRITE_TAC[SET_RULE `{z,v,w} = {z,w,v}`] THEN
\r
175 ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
\r
176 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_TAC `a:real`)) THEN
\r
177 ASM_SIMP_TAC[AFF_GE_1_2_0; SET_RULE
\r
178 `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
\r
179 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
180 MAP_EVERY X_GEN_TAC [`b:real`; `c:real`] THEN STRIP_TAC THEN
\r
181 ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; VECTOR_MUL_ASSOC] THEN
\r
184 (* ------------------------------------------------------------------------- *)
\r
185 (* Borderline case. *)
\r
186 (* ------------------------------------------------------------------------- *)
\r
188 let GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE = prove
\r
190 ~collinear{vec 0,v,u} /\ ~collinear{vec 0,v,w} /\
\r
191 azim (vec 0) v w u = pi /\
\r
192 aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {}
\r
193 ==> v IN aff_ge {vec 0} {u,w}`,
\r
194 REPEAT GEN_TAC THEN
\r
195 MAP_EVERY (fun t ->
\r
196 ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
\r
197 [`v:real^3 = vec 0`; `u:real^3 = vec 0`; `w:real^3 = vec 0`;
\r
198 `u:real^3 = v`; `v:real^3 = w`] THEN
\r
199 REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
200 ASM_SIMP_TAC[AZIM_EQ_PI] THEN
\r
201 ASM_SIMP_TAC[AFF_LT_2_1; AFF_LT_1_1; AFF_GE_1_2; DISJOINT_INSERT;
\r
202 DISJOINT_EMPTY; IN_INSERT; NOT_IN_EMPTY] THEN
\r
203 REWRITE_TAC[TAUT `p /\ x = &1 /\ q <=> x = &1 /\ p /\ q`] THEN
\r
204 REWRITE_TAC[VECTOR_MUL_RZERO; REAL_ARITH
\r
205 `t1 + x = &1 <=> t1 = &1 - x`] THEN
\r
206 REWRITE_TAC[RIGHT_EXISTS_AND_THM; VECTOR_ADD_LID] THEN
\r
207 ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
\r
208 REWRITE_TAC[UNWIND_THM2] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
\r
209 REWRITE_TAC[UNWIND_THM2; IN_ELIM_THM] THEN
\r
210 REWRITE_TAC[IMP_CONJ; LEFT_IMP_EXISTS_THM] THEN
\r
211 MAP_EVERY X_GEN_TAC [`s:real`; `t:real`] THEN REPEAT STRIP_TAC THEN
\r
212 DISJ_CASES_TAC(REAL_ARITH `&0 < s \/ s <= &0`) THENL
\r
213 [MAP_EVERY EXISTS_TAC [`--t / s:real`; `&1 / s`] THEN
\r
214 ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; REAL_LT_IMP_LE;
\r
215 REAL_ARITH `t < &0 ==> &0 <= --t`] THEN
\r
216 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
\r
217 ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN VECTOR_ARITH_TAC;
\r
218 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
\r
219 `s INTER t = {} ==> !x. x IN s /\ x IN t ==> P`)) THEN
\r
220 EXISTS_TAC `t % u:real^3` THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
221 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
\r
222 MAP_EVERY EXISTS_TAC [`--s:real`; `&1`] THEN
\r
223 REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
\r
224 ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]);;
\r
226 let UNION_AFF_GE_1_2 = prove
\r
228 v IN aff_ge {a} {u,w} /\ ~(u = a) /\ ~(v = a) /\ ~(w = a)
\r
229 ==> aff_ge {a} {u,v} UNION aff_ge {a} {v,w} = aff_ge {a} {u,w}`,
\r
230 GEOM_ORIGIN_TAC `a:real^N` THEN REPEAT STRIP_TAC THEN
\r
231 UNDISCH_TAC `(v:real^N) IN aff_ge {vec 0} {u,w}` THEN
\r
232 ASM_SIMP_TAC[AFF_GE_1_2_0; SET_RULE
\r
233 `a UNION b = c <=> a SUBSET c /\ b SUBSET c /\ c SUBSET a UNION b`] THEN
\r
234 REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN
\r
235 REWRITE_TAC[IN_ELIM_THM; IN_UNION; LEFT_IMP_EXISTS_THM] THEN
\r
236 MAP_EVERY X_GEN_TAC [`m:real`; `n:real`] THEN STRIP_TAC THEN
\r
237 REPEAT CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
\r
239 [MAP_EVERY EXISTS_TAC [`a + b * m:real`; `b * n:real`] THEN
\r
240 ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL] THEN VECTOR_ARITH_TAC;
\r
241 MAP_EVERY EXISTS_TAC [`a * m:real`; `a * n + b:real`] THEN
\r
242 ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL] THEN VECTOR_ARITH_TAC;
\r
244 DISJ_CASES_TAC(REAL_ARITH `b * m <= a * n \/ a * n <= b * m`) THENL
\r
245 [DISJ1_TAC; DISJ2_TAC] THEN
\r
246 ASM_REWRITE_TAC[] THENL
\r
247 [MAP_EVERY EXISTS_TAC [`a - b / n * m:real`; `b / n:real`] THEN
\r
248 ASM_SIMP_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; VECTOR_ADD_ASSOC] THEN
\r
249 ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; REAL_SUB_ADD; VECTOR_MUL_RCANCEL;
\r
250 VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN
\r
251 ASM_SIMP_TAC[REAL_SUB_LE; REAL_LE_DIV] THEN ASM_CASES_TAC `n = &0` THENL
\r
252 [MAP_EVERY UNDISCH_TAC [`v:real^N = m % u + n % w`; `b * m <= a * n`] THEN
\r
253 ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LE_MUL; REAL_ENTIRE;
\r
254 REAL_ARITH `&0 <= x ==> (x <= &0 <=> x = &0)`] THEN
\r
255 STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
\r
256 ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO];
\r
257 ASM_SIMP_TAC[REAL_DIV_RMUL] THEN
\r
258 REWRITE_TAC[REAL_ARITH `b / n * m:real = (b * m) / n`] THEN
\r
259 ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LT_LE]];
\r
260 MAP_EVERY EXISTS_TAC [`a / m:real`; `b - a / m * n:real`] THEN
\r
261 REWRITE_TAC[VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN
\r
262 REWRITE_TAC[VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_RDISTRIB] THEN
\r
263 ASM_REWRITE_TAC[REAL_SUB_ADD2; VECTOR_MUL_RCANCEL;
\r
264 VECTOR_ARITH `x + a:real^N = y + a <=> x = y`] THEN
\r
265 ASM_SIMP_TAC[REAL_SUB_LE; REAL_LE_DIV] THEN ASM_CASES_TAC `m = &0` THENL
\r
266 [MAP_EVERY UNDISCH_TAC [`v:real^N = m % u + n % w`; `a * n <= b * m`] THEN
\r
267 ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LE_MUL; REAL_ENTIRE;
\r
268 REAL_ARITH `&0 <= x ==> (x <= &0 <=> x = &0)`] THEN
\r
269 STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
\r
270 ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO];
\r
271 ASM_SIMP_TAC[REAL_DIV_RMUL] THEN
\r
272 REWRITE_TAC[REAL_ARITH `b / n * m:real = (b * m) / n`] THEN
\r
273 ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LT_LE]]]);;
\r
275 (* ------------------------------------------------------------------------- *)
\r
276 (* More specialist lemmas. *)
\r
277 (* ------------------------------------------------------------------------- *)
\r
279 let AZIM_CYCLE_BASIC_PROPERTIES = prove
\r
282 ==> (azim_cycle W v w p) IN W /\
\r
283 !q. q IN W /\ ~(q = p)
\r
284 ==> azim v w p (azim_cycle W v w p) <= azim v w p q`,
\r
285 REPEAT GEN_TAC THEN ASM_CASES_TAC `W SUBSET {p:real^3}` THENL
\r
286 [ASM_SIMP_TAC[Sphere.azim_cycle; AZIM_REFL; azim]; ALL_TAC] THEN
\r
287 UNDISCH_TAC `~(W SUBSET {p:real^3})` THEN
\r
288 ONCE_REWRITE_TAC[TAUT `p ==> q /\ r ==> s <=> p /\ q ==> r ==> s`] THEN
\r
289 DISCH_THEN(MP_TAC o MATCH_MP Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) THEN
\r
290 SIMP_TAC[IN] THEN MESON_TAC[REAL_LE_LT]);;
\r
292 let AZIM_CYCLE_TWO_POINT_SET_ALT = prove
\r
293 (`!W x u v w. W = {v,w} ==> azim_cycle W x u v = w`,
\r
294 MESON_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]);;
\r
296 let IVS_AZIM_CYCLE_TWO_POINT_SET = prove
\r
297 (`!a b. ivs_azim_cycle {a, b} v w a = b`,
\r
298 REWRITE_TAC[Wrgcvdr_cizmrrh.ivs_azim_cycle; NOT_INSERT_EMPTY] THEN
\r
299 SIMP_TAC[SET_RULE `x IN {a,b} /\ P x <=> x = a /\ P a \/ x = b /\ P b`] THEN
\r
300 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN
\r
301 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
\r
302 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN
\r
305 let IVS_AZIM_CYCLE_TWO_POINT_SET_ALT = prove
\r
306 (`!W x u v w. W = {v,w} ==> ivs_azim_cycle W x u v = w`,
\r
307 MESON_TAC[IVS_AZIM_CYCLE_TWO_POINT_SET]);;
\r
309 let AZIM_CYCLE_SING = prove
\r
310 (`!x u v. azim_cycle {v} x u v = v`,
\r
311 REWRITE_TAC[Sphere.azim_cycle; SUBSET_REFL]);;
\r
313 let IVS_AZIM_CYCLE_SING = prove
\r
314 (`!x u v. ivs_azim_cycle {v} x u v = v`,
\r
315 ONCE_REWRITE_TAC[SET_RULE `{v} = {v,v}`] THEN
\r
316 REWRITE_TAC[IVS_AZIM_CYCLE_TWO_POINT_SET]);;
\r
318 let RHO_NODE1_INJECTIVE = prove
\r
321 ==> !v w. v IN V /\ w IN V
\r
322 ==> (rho_node1 FF v = rho_node1 FF w <=> v = w)`,
\r
323 MESON_TAC[Local_lemmas.IVS_RHO_IDD]);;
\r
325 let IVS_RHO_NODE1_IN_V = prove
\r
326 (`!V E FF. local_fan (V,E,FF) ==> !v. v IN V ==> ivs_rho_node1 FF v IN V`,
\r
327 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V;
\r
328 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);;
\r
330 let LOCAL_FAN_ITER_IVS_RHO_NODE_IN_V = prove
\r
331 (`!V E FF. local_fan (V,E,FF) /\ v IN V
\r
332 ==> !i. ITER i (ivs_rho_node1 FF) v IN V`,
\r
333 REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN
\r
334 ASM_SIMP_TAC[ITER] THEN ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]);;
\r
336 let LOCAL_FAN_ORBIT_MAP_EXPLICIT = prove
\r
338 local_fan(V,E,FF) /\ v IN V /\ w IN V
\r
339 ==> ?i. i < CARD V /\ w = ITER i (rho_node1 FF) v`,
\r
340 REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o
\r
341 MATCH_MP Local_lemmas.LOCAL_FAN_ORBIT_MAP_V) THEN
\r
342 REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER; Hypermap.orbit_map] THEN
\r
343 ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
\r
344 DISCH_THEN(MP_TAC o SPEC `w:real^3`) THEN ASM_REWRITE_TAC[GE; LE_0] THEN
\r
345 DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
\r
346 EXISTS_TAC `n MOD (CARD(V:real^3->bool))` THEN
\r
347 FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOCAL_FAN_FINITE_V) THEN
\r
348 FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN
\r
349 MP_TAC(ISPECL [`n:num`; `CARD(V:real^3->bool)`] DIVISION) THEN
\r
350 ABBREV_TAC `i = n MOD (CARD(V:real^3->bool))` THEN
\r
351 ABBREV_TAC `m = n DIV (CARD(V:real^3->bool))` THEN
\r
352 ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_THEN(K ALL_TAC) THEN
\r
353 SPEC_TAC(`m:num`,`p:num`) THEN
\r
354 INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
\r
355 ONCE_REWRITE_TAC[ARITH_RULE `(a + b) + c:num = (a + c) + b`] THEN
\r
356 ONCE_REWRITE_TAC[GSYM ITER_ADD] THEN
\r
357 FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID) THEN
\r
360 let LOCAL_FAN_ORBIT_MAP_EXPLICIT_IVS = prove
\r
362 local_fan(V,E,FF) /\ v IN V /\ w IN V
\r
363 ==> ?i. i < CARD V /\ w = ITER i (ivs_rho_node1 FF) v`,
\r
364 REPEAT STRIP_TAC THEN
\r
365 FIRST_ASSUM(MP_TAC o SPECL [`w:real^3`; `v:real^3`] o
\r
366 MATCH_MP (REWRITE_RULE[IMP_CONJ] LOCAL_FAN_ORBIT_MAP_EXPLICIT)) THEN
\r
367 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
\r
368 X_GEN_TAC `i:num` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
369 CONV_TAC SYM_CONV THEN
\r
370 UNDISCH_TAC `(w:real^3) IN V` THEN SPEC_TAC(`w:real^3`,`w:real^3`) THEN
\r
371 SPEC_TAC(`i:num`,`n:num`) THEN INDUCT_TAC THENL
\r
372 [REWRITE_TAC[ITER]; ALL_TAC] THEN
\r
373 X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN
\r
374 ONCE_REWRITE_TAC[ITER_ALT] THEN REWRITE_TAC[ITER] THEN
\r
375 MATCH_MP_TAC EQ_TRANS THEN
\r
376 EXISTS_TAC `ITER n (ivs_rho_node1 FF) (ITER n (rho_node1 FF) x)` THEN
\r
377 CONJ_TAC THENL [AP_TERM_TAC; ASM_SIMP_TAC[]] THEN
\r
378 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD;
\r
379 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);;
\r
381 let ITER_IVS_RHO_IDD = prove
\r
383 local_fan (V,E,FF) /\ v IN V
\r
384 ==> ITER n (ivs_rho_node1 FF) (ITER n (rho_node1 FF) v) = v`,
\r
385 REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN
\r
386 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
\r
387 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THENL
\r
388 [REWRITE_TAC[ITER]; ONCE_REWRITE_TAC[ITER_ALT] THEN REWRITE_TAC[ITER]] THEN
\r
389 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD;
\r
390 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);;
\r
392 let ITER_RHO_IVS_IDD = prove
\r
394 local_fan (V,E,FF) /\ v IN V
\r
395 ==> ITER n (rho_node1 FF) (ITER n (ivs_rho_node1 FF) v) = v`,
\r
396 REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN
\r
397 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
\r
398 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THENL
\r
399 [REWRITE_TAC[ITER]; ONCE_REWRITE_TAC[ITER_ALT] THEN REWRITE_TAC[ITER]] THEN
\r
400 ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD; LOCAL_FAN_ITER_IVS_RHO_NODE_IN_V]);;
\r
402 let LOFA_IMP_ITER_IVS_RHO_NODE_ID = prove
\r
405 ==> (!v. v IN V ==> ITER (CARD V) (ivs_rho_node1 FF) v = v)`,
\r
406 MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID; ITER_IVS_RHO_IDD]);;
\r
408 let GENERIC_LOCAL_FAN_AZIM_POS = prove
\r
410 convex_local_fan(V,E,FF) /\ generic V E /\
\r
411 (!v. v IN V ==> interior_angle1 (vec 0) FF v < pi) /\
\r
412 v IN V /\ w IN V /\ ~(w = v) /\ ~(w = rho_node1 FF v)
\r
413 ==> &0 < sin(azim (vec 0) v (rho_node1 FF v) w)`,
\r
414 REPEAT STRIP_TAC THEN
\r
415 FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I
\r
416 [Wrgcvdr_cizmrrh.convex_local_fan]) THEN
\r
417 MATCH_MP_TAC SIN_POS_PI THEN REWRITE_TAC[REAL_LT_LE] THEN
\r
418 REWRITE_TAC[Local_lemmas.AZIM_RANGE] THEN
\r
419 ONCE_REWRITE_TAC[MESON[] `~(z = a) /\ p /\ q <=> p /\ ~(a = z) /\ q`] THEN
\r
421 [ASM_MESON_TAC[Local_lemmas.IN_V_IMP_AZIM_LESS_PI]; ALL_TAC] THEN
\r
422 FIRST_ASSUM(MP_TAC o SPECL [`v:real^3`; `w:real^3`] o
\r
423 MATCH_MP (REWRITE_RULE[IMP_CONJ] LOCAL_FAN_ORBIT_MAP_EXPLICIT)) THEN
\r
424 ASM_REWRITE_TAC[] THEN
\r
425 DISCH_THEN(X_CHOOSE_THEN `m:num` (STRIP_ASSUME_TAC o GSYM)) THEN
\r
426 ASM_CASES_TAC `m = 0` THENL [ASM_MESON_TAC[ITER]; ALL_TAC] THEN
\r
427 ASM_CASES_TAC `m = 1` THENL [ASM_MESON_TAC[Lvducxu.ITER12]; ALL_TAC] THEN
\r
428 FIRST_ASSUM(MP_TAC o GEN_ALL o MATCH_MP
\r
429 (REWRITE_RULE[IMP_CONJ] Local_lemmas.EGHNAVX)) THEN
\r
430 DISCH_THEN(MP_TAC o SPECL
\r
431 [`\i. azim (vec 0) v (rho_node1 FF v) (ITER i (rho_node1 FF) v)`;
\r
432 `m:num`; `v:real^3`; `\i. ITER i (rho_node1 FF) (v:real^3)`;
\r
433 `CARD(V:real^3->bool)`]) THEN
\r
434 ASM_REWRITE_TAC[IMP_IMP; Lvducxu.ITER12] THEN
\r
436 [ASM_MESON_TAC[IN_INSERT; Nkezbfc_local.PROPERTIES_GENERIC1]; ALL_TAC] THEN
\r
437 REWRITE_TAC[TAUT `p ==> ~q /\ ~r <=> q \/ r ==> ~p`] THEN
\r
438 STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
\r
439 [DISCH_THEN(MP_TAC o SPEC `1` o el 3 o CONJUNCTS) THEN
\r
440 ASM_REWRITE_TAC[Lvducxu.ITER12; NOT_IMP] THEN CONJ_TAC THENL
\r
442 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; REAL_LT_REFL]];
\r
443 REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
444 DISCH_THEN(MP_TAC o CONJUNCT2) THEN REWRITE_TAC[NOT_IMP] THEN
\r
445 FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
\r
446 `m < CARD V ==> m < CARD V - 1 \/ m = CARD V - 1`)) THEN
\r
447 DISCH_THEN DISJ_CASES_TAC THENL
\r
448 [REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
\r
449 [ASM_SIMP_TAC[LE_1] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
\r
450 (REAL_ARITH `x = pi ==> x <= y /\ y <= pi ==> pi = y`)) THEN
\r
451 ASM_REWRITE_TAC[] THEN EXPAND_TAC "w" THEN
\r
452 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
453 DISCH_THEN(MP_TAC o SPEC `CARD(V:real^3->bool) - 1` o CONJUNCT1) THEN
\r
454 REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
\r
455 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V;
\r
457 MATCH_MP_TAC(TAUT `F ==> p`) THEN
\r
458 FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP
\r
459 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) THEN
\r
460 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
\r
461 `x < pi /\ y = pi ==> ~(x = y)`) THEN
\r
462 ASM_SIMP_TAC[] THEN
\r
463 SUBGOAL_THEN `ivs_rho_node1 FF v = w` (fun t -> ASM_REWRITE_TAC[t]) THEN
\r
464 SUBGOAL_THEN `v = rho_node1 FF w` MP_TAC THENL
\r
465 [ALL_TAC; ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]] THEN
\r
466 EXPAND_TAC "w" THEN REWRITE_TAC[GSYM(CONJUNCT2 ITER)] THEN
\r
467 SUBGOAL_THEN `SUC m = CARD(V:real^3->bool)` SUBST1_TAC THENL
\r
469 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]]]]);;
\r
471 let nn_of_hyp3 = prove
\r
472 (`!x V E. nn_of_hyp (x,V,E) =
\r
473 \(v,w). if (v,w) IN darts_of_hyp E V
\r
474 then (v,azim_cycle (EE v E) x v w) else (v,w)`,
\r
475 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; Wrgcvdr_cizmrrh.nn_of_hyp]);;
\r
477 let ff_of_hyp3 = prove
\r
478 (`!x V E. ff_of_hyp (x,V,E) =
\r
479 \(v,w). if (v,w) IN darts_of_hyp E V
\r
480 then (w,ivs_azim_cycle (EE w E) x w v) else (v,w)`,
\r
481 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; Wrgcvdr_cizmrrh.ff_of_hyp]);;
\r
483 let ee_of_hyp3 = prove
\r
484 (`!x V E. ee_of_hyp (x,V,E) =
\r
485 \(v,w). if (v,w) IN darts_of_hyp E V then (w,v) else (v,w)`,
\r
486 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; Wrgcvdr_cizmrrh.ee_of_hyp]);;
\r
488 let ORDER_AZIM_SUM2Pi_0 = prove
\r
490 ~collinear {x, y, z} /\
\r
491 (!i. i IN 0..n ==> ~collinear {x, y, g i}) /\
\r
495 j IN 0..n /\ k IN 0..n /\ j < k
\r
496 ==> azim x y z (g j) < azim x y z (g k))
\r
497 ==> sum (0..n) (\i. azim x y (g i) (g (i + 1))) = &2 * pi`,
\r
498 REPEAT STRIP_TAC THEN
\r
500 [`x:real^3`; `y:real^3`; `z:real^3`; `n + 1`; `\i. (g:num->real^3) (i - 1)`]
\r
501 Counting_spheres.ORDER_AZIM_SUM2Pi) THEN
\r
502 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
\r
503 [ASM_REWRITE_TAC[ADD_SUB; SUB_REFL; ARITH_RULE `1 < n + 1 <=> 0 < n`] THEN
\r
504 REWRITE_TAC[IN_NUMSEG] THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
\r
505 STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN
\r
507 GEN_REWRITE_TAC (funpow 4 LAND_CONV)
\r
508 [ARITH_RULE `1 = 0 + 1`] THEN
\r
509 REWRITE_TAC[SUM_OFFSET; ADD_SUB]]);;
\r
511 let LOCAL_FAN_NOT_EMPTY_FF = prove
\r
512 (`!V E FF. local_fan (V,E,FF) ==> ~(FF = {})`,
\r
513 REPEAT STRIP_TAC THEN
\r
514 FIRST_ASSUM(MP_TAC o GEN_ALL o MATCH_MP
\r
515 (REWRITE_RULE[IMP_CONJ] Wrgcvdr_cizmrrh.BIJ_BETWEEN_FF_AND_V)) THEN
\r
516 DISCH_THEN(MP_TAC o SPEC `FST:real^3#real^3->real^3`) THEN
\r
517 ASM_REWRITE_TAC[BIJ; INJ; SURJ; NOT_IN_EMPTY; ETA_AX] THEN
\r
518 FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN
\r
521 let LOCAL_FAN_NOT_CARD_FF_GE_2 = prove
\r
522 (`!V E FF. local_fan (V,E,FF) ==> 2 <= CARD FF`,
\r
523 REPEAT STRIP_TAC THEN
\r
524 REWRITE_TAC[ARITH_RULE `2 <= n <=> ~(n = 0) /\ ~(n = 1)`] THEN
\r
525 FIRST_ASSUM(ASSUME_TAC o MATCH_MP Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF) THEN
\r
526 ASM_SIMP_TAC[MESON[HAS_SIZE]
\r
527 `FINITE s ==> (CARD s = n <=> s HAS_SIZE n)`] THEN
\r
528 CONJ_TAC THEN CONV_TAC(RAND_CONV HAS_SIZE_CONV) THEN
\r
529 ASM_MESON_TAC[LOCAL_FAN_NOT_EMPTY_FF;
\r
530 Local_lemmas.LOCAL_FAN_NOT_SING_FF]);;
\r
532 let SIN_AZIM_MUTUAL_CROSS = prove
\r
533 (`(sin (azim (vec 0) u v w) < &0 <=> (u cross v) dot w < &0) /\
\r
534 (&0 < sin (azim (vec 0) u v w) <=> &0 < (u cross v) dot w) /\
\r
535 (sin (azim (vec 0) u v w) <= &0 <=> (u cross v) dot w <= &0) /\
\r
536 (&0 <= sin (azim (vec 0) u v w) <=> &0 <= (u cross v) dot w) /\
\r
537 (sin (azim (vec 0) u v w) = &0 <=> (u cross v) dot w = &0)`,
\r
538 REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS;
\r
539 GSYM REAL_LE_ANTISYM; GSYM REAL_NOT_LT]);;
\r
541 let CROSS_POSITIVE_MULTIPLE_AZIM_AXIS = prove
\r
542 (`!x y z. ~(x = vec 0) /\ orthogonal x y /\ orthogonal x z /\
\r
543 &0 < azim (vec 0) x y z /\ azim (vec 0) x y z < pi
\r
544 ==> ?a. &0 < a /\ y cross z = a % x`,
\r
545 REPEAT STRIP_TAC THEN
\r
546 SUBGOAL_THEN `collinear{vec 0,x,y cross z}` MP_TAC THENL
\r
547 [REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM CROSS_EQ_0] THEN VEC3_TAC;
\r
549 ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN
\r
550 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real` THEN
\r
551 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
552 SUBGOAL_THEN `&0 < sin(azim (vec 0) x y z)` MP_TAC THENL
\r
553 [ASM_SIMP_TAC[SIN_POS_PI]; REWRITE_TAC[SIN_AZIM_MUTUAL_CROSS]] THEN
\r
554 ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN
\r
555 ASM_SIMP_TAC[REAL_LT_MUL_EQ; DOT_LMUL; DOT_POS_LT]);;
\r
557 let CROSS_POSITIVE_MULTIPLE_AZIM_AXIS_ALT = prove
\r
558 (`!x y z. ~(x = vec 0) /\ orthogonal x y /\ orthogonal x z /\
\r
559 &0 < azim (vec 0) x y z /\ azim (vec 0) x y z < pi
\r
560 ==> ?a. &0 < a /\ x = a % (y cross z)`,
\r
561 REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
562 FIRST_ASSUM(MP_TAC o MATCH_MP CROSS_POSITIVE_MULTIPLE_AZIM_AXIS) THEN
\r
563 DISCH_THEN(X_CHOOSE_THEN `a:real` STRIP_ASSUME_TAC) THEN
\r
564 EXISTS_TAC `inv(a):real` THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN
\r
565 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ;
\r
568 (* ------------------------------------------------------------------------- *)
\r
569 (* Equivalences for fan7 and so for FAN. *)
\r
570 (* ------------------------------------------------------------------------- *)
\r
572 let GMLWKPK = prove
\r
575 ==> (fan7(x,V,E) <=>
\r
576 !e1 e2. e1 IN E UNION {{v} | v IN V} /\
\r
577 e2 IN E UNION {{v} | v IN V}
\r
578 ==> (e1 INTER e2 = {}
\r
579 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\
\r
580 (!v. e1 INTER e2 = {v}
\r
581 ==> aff_ge {x} e1 INTER aff_ge {x} e2 =
\r
583 REPEAT STRIP_TAC THEN REWRITE_TAC[Fan.fan7] THEN EQ_TAC THENL
\r
584 [SIMP_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]; ALL_TAC] THEN
\r
585 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e1:real^N->bool` THEN
\r
586 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e2:real^N->bool` THEN
\r
587 MATCH_MP_TAC(TAUT `(p ==> q ==> r) ==> (q ==> p) ==> q ==> r`) THEN
\r
588 STRIP_TAC THEN DISCH_TAC THEN
\r
589 SUBGOAL_THEN `e1 = e2 \/ e1 INTER e2 = {} \/ (?v:real^N. e1 INTER e2 = {v})`
\r
592 STRIP_TAC THEN ASM_REWRITE_TAC[INTER_IDEMPOT] THEN
\r
593 ASM_MESON_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]] THEN
\r
594 SUBGOAL_THEN `?a b:real^N c d:real^N. e1 = {a,b} /\ e2 = {c,d}` MP_TAC THENL
\r
596 DISCH_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN SUBST_ALL_TAC)) THEN
\r
598 FIRST_ASSUM(CONJUNCTS_THEN MP_TAC) THEN
\r
599 REWRITE_TAC[IN_UNION; IN_ELIM_THM] THEN
\r
600 SUBGOAL_THEN `!e:real^N->bool. e IN E ==> ?v w. ~(v = w) /\ e = {v,w}`
\r
601 (LABEL_TAC "*") THENL
\r
602 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.graph]) THEN
\r
603 MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
\r
604 MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[IN] THEN
\r
605 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[];
\r
606 ASM_MESON_TAC[SET_RULE `{v,v} = {v}`]]);;
\r
608 let GMLWKPK_ALT = prove
\r
610 graph E /\ (!e. e IN E ==> ~(x IN e))
\r
611 ==> (fan7(x,V,E) <=>
\r
612 (!e1 e2. e1 IN E UNION {{v} | v IN V} /\
\r
613 e2 IN E UNION {{v} | v IN V} /\
\r
615 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\
\r
616 (!e1 e2 v. e1 IN E /\ e2 IN E /\ e1 INTER e2 = {v}
\r
617 ==> aff_ge {x} e1 INTER aff_ge {x} e2 =
\r
619 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN
\r
620 EQ_TAC THEN SIMP_TAC[IN_UNION] THEN STRIP_TAC THEN
\r
621 MATCH_MP_TAC(MESON[]
\r
622 `(!x y. R x y ==> R y x) /\
\r
623 (!x y. P x /\ P y ==> R x y) /\
\r
624 (!x y. Q x /\ Q y ==> R x y) /\
\r
625 (!x y. P x /\ Q y ==> R x y)
\r
626 ==> !x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y`) THEN
\r
627 CONJ_TAC THENL [REWRITE_TAC[INTER_ACI]; ASM_SIMP_TAC[]] THEN CONJ_TAC THEN
\r
628 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THENL
\r
629 [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> a = c /\ b = c`] THEN SET_TAC[];
\r
630 X_GEN_TAC `e1:real^N->bool` THEN DISCH_TAC THEN X_GEN_TAC `v:real^N`] THEN
\r
631 SUBGOAL_THEN `(e1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
632 [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
633 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
634 MAP_EVERY X_GEN_TAC [`u:real^N`; `w:real^N`] THEN
\r
635 STRIP_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
636 SIMP_TAC[SET_RULE `{a,b} INTER {c} = {d} <=> d = c /\ (a = c \/ b = c)`] THEN
\r
637 REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
\r
638 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
639 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]);;
\r
641 let FAN_ECONOMIZED = prove
\r
644 UNIONS E SUBSET V /\
\r
649 (!e1 e2. e1 IN E UNION {{v} | v IN V} /\
\r
650 e2 IN E UNION {{v} | v IN V}
\r
651 ==> (e1 INTER e2 = {}
\r
652 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\
\r
653 (!v. e1 INTER e2 = {v}
\r
654 ==> aff_ge {x} e1 INTER aff_ge {x} e2 =
\r
656 REPEAT GEN_TAC THEN REWRITE_TAC[Fan.FAN] THEN
\r
658 MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
\r
659 DISCH_TAC THEN REPEAT AP_TERM_TAC THEN ASM_SIMP_TAC[GMLWKPK]);;
\r
661 let FAN7_AFF_GT_CONDITION = prove
\r
663 graph E /\ ~(x IN V) /\ (!e. e IN E ==> e SUBSET V /\ ~(x IN e)) /\
\r
664 (!v w. v IN V /\ w IN V
\r
665 ==> aff_ge {x} {v} INTER aff_ge {x} {w} =
\r
666 aff_ge {x} ({v} INTER {w})) /\
\r
667 (!v e. v IN V /\ e IN E
\r
668 ==> aff_gt {x} {v} INTER aff_gt {x} e = {}) /\
\r
669 (!e1 e2. e1 IN E /\ e2 IN E /\ ~(e1 = e2)
\r
670 ==> aff_gt {x} e1 INTER aff_gt {x} e2 = {})
\r
673 (`!x v:real^N. ~(v = x) ==> aff_ge {x} {v} = aff_gt {x} {v} UNION {x}`,
\r
674 REPEAT STRIP_TAC THEN
\r
675 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_AFF_GT_DECOMP o lhand o goal_concl) THEN
\r
676 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN
\r
677 ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
\r
678 REWRITE_TAC[SET_RULE `{f x | x IN {a}} = {f a}`; UNIONS_1] THEN
\r
679 REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; SET_RULE `{v} DELETE v = {}`] THEN
\r
680 REWRITE_TAC[AFFINE_HULL_SING])
\r
683 ~(v = x) /\ ~(w = x)
\r
684 ==> aff_ge {x} {v,w} =
\r
685 aff_gt {x} {v,w} UNION aff_ge {x} {v} UNION aff_ge {x} {w}`,
\r
686 REPEAT STRIP_TAC THEN ASM_CASES_TAC `w:real^N = v` THENL
\r
687 [ASM_REWRITE_TAC[INSERT_AC; AFF_GT_SUBSET_AFF_GE; SET_RULE
\r
688 `s = t UNION s UNION s <=> t SUBSET s`];
\r
689 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_AFF_GT_DECOMP o
\r
690 lhand o goal_concl) THEN
\r
691 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN
\r
692 ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
\r
693 REWRITE_TAC[SET_RULE `{f x | x IN {a,b}} = {f a,f b}`; UNIONS_2] THEN
\r
694 ASM_SIMP_TAC[SET_RULE `~(v = w) ==> {v,w} DELETE v = {w}`;
\r
695 SET_RULE `~(v = w) ==> {v,w} DELETE w = {v}`] THEN
\r
696 REWRITE_TAC[UNION_ACI]])
\r
698 (`!P:(A->bool)->(A->bool)->bool.
\r
699 (!v w. ~(v = w) ==> P {v,w} {v,w}) /\
\r
700 (!v w y z. ~(v = w) /\ ~(y = z) /\ {v,w} INTER {y,z} = {}
\r
701 ==> P {v,w} {y,z}) /\
\r
702 (!v w y. ~(v = w) /\ ~(w = y) /\ ~(v = y) ==> P {v,w} {w,y})
\r
703 ==> !v w y z. ~(v = w) /\ ~(y = z) ==> P {v,w} {y,z}`,
\r
704 REPEAT STRIP_TAC THEN
\r
705 ASM_CASES_TAC `{v:A,w} = {y,z}` THEN ASM_SIMP_TAC[] THEN
\r
706 ASM_CASES_TAC `{v:A,w} INTER {y,z} = {}` THEN ASM_SIMP_TAC[] THEN
\r
707 SUBGOAL_THEN `v:A = y \/ v = z \/ w = y \/ w = z` MP_TAC THENL
\r
708 [ASM SET_TAC[]; ALL_TAC] THEN
\r
709 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST_ALL_TAC) THEN
\r
710 ASM_MESON_TAC[SET_RULE `{a,b} = {b,a}`]) in
\r
711 REPEAT STRIP_TAC THEN REWRITE_TAC[Fan.fan7] THEN
\r
713 `!v:real^N e. v IN V /\ e IN E ==> aff_gt {x} e INTER aff_gt {x} {v} = {}`
\r
714 ASSUME_TAC THENL [ASM_MESON_TAC[INTER_COMM]; ALL_TAC] THEN
\r
715 REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(MESON[]
\r
716 `(!e1 e2. R e1 e2 <=> R e2 e1) /\
\r
717 (!e1. Q e1 ==> !e2. Q e2 ==> R e1 e2) /\
\r
718 (!e1. P e1 ==> (!e2. P e2 ==> R e1 e2) /\ (!e2. Q e2 ==> R e1 e2))
\r
719 ==> !e1 e2. (P e1 \/ Q e1) /\ (P e2 \/ Q e2) ==> R e1 e2`) THEN
\r
720 CONJ_TAC THENL [REWRITE_TAC[INTER_ACI]; ALL_TAC] THEN
\r
721 ASM_SIMP_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `e1:real^N->bool` THEN
\r
723 SUBGOAL_THEN `(e1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
724 [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
725 DISCH_THEN(X_CHOOSE_THEN `v:real^N` (X_CHOOSE_THEN `w:real^N`
\r
726 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))) THEN
\r
727 SUBGOAL_THEN `{v:real^N,w} SUBSET V /\ ~(x IN {v,w})` STRIP_ASSUME_TAC THENL
\r
728 [ASM MESON_TAC[]; ALL_TAC] THEN
\r
730 [X_GEN_TAC `e2:real^N->bool` THEN DISCH_TAC THEN
\r
731 SUBGOAL_THEN `(e2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
732 [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
733 DISCH_THEN(X_CHOOSE_THEN `y:real^N` (X_CHOOSE_THEN `z:real^N`
\r
734 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))) THEN
\r
735 SUBGOAL_THEN `{y:real^N,z} SUBSET V /\ ~(x IN {y,z})` STRIP_ASSUME_TAC THENL
\r
736 [ASM MESON_TAC[]; ALL_TAC] THEN
\r
737 MAP_EVERY UNDISCH_TAC
\r
738 [`{v:real^N, w} IN E`; `{y:real^N, z} IN E`;
\r
739 `{v:real^N, w} SUBSET V`; `{y:real^N, z} SUBSET V`;
\r
740 `~((x:real^N) IN {v,w})`; `~((x:real^N) IN {y,z})`;
\r
741 `~(y:real^N = z)`; `~(v:real^N = w)`] THEN
\r
742 GEN_REWRITE_TAC I [IMP_IMP] THEN MAP_EVERY (fun t -> SPEC_TAC(t,t))
\r
743 [`z:real^N`; `y:real^N`; `w:real^N`; `v:real^N`] THEN
\r
744 MATCH_MP_TAC slemma THEN
\r
745 CONJ_TAC THENL [REWRITE_TAC[INTER_IDEMPOT]; ALL_TAC] THEN
\r
746 REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
\r
747 SIMP_TAC[SET_RULE `~(y = v) ==> {v,w} INTER {w,y} = {w}`] THEN
\r
748 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
\r
749 REWRITE_TAC[SET_RULE
\r
750 `{a,b} INTER {c,d} = {} <=>
\r
751 ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d)`] THEN
\r
752 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT STRIP_TAC THEN
\r
753 ASM_SIMP_TAC[lemma2; UNION_OVER_INTER] THEN
\r
754 REWRITE_TAC[ONCE_REWRITE_RULE[INTER_COMM] UNION_OVER_INTER] THEN
\r
755 ASM_SIMP_TAC[SET_RULE `~(a = b) ==> {a} INTER {b} = {}`] THEN
\r
756 ASM_SIMP_TAC[lemma1; UNION_OVER_INTER] THEN
\r
757 REWRITE_TAC[ONCE_REWRITE_RULE[INTER_COMM] UNION_OVER_INTER] THEN
\r
758 ASM_SIMP_TAC[SET_RULE `~(v = y) ==> ~({v,w} = {w,y})`;
\r
759 SET_RULE `~(v = y) /\ ~(v = z) ==> ~({v,w} = {y,z})`] THEN
\r
760 REWRITE_TAC[UNION_EMPTY; UNION_ASSOC; INTER_IDEMPOT] THEN
\r
761 ASM_SIMP_TAC[GSYM lemma1] THEN
\r
762 MATCH_MP_TAC SUBSET_ANTISYM THEN
\r
763 (CONJ_TAC THENL [REWRITE_TAC[UNION_SUBSET]; SET_TAC[]]) THEN
\r
764 REWRITE_TAC[SUBSET_REFL] THENL
\r
765 [REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING] THEN SET_TAC[];
\r
767 REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC AFF_GE_MONO_RIGHT) THEN
\r
768 ASM_REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
\r
769 REWRITE_TAC[EMPTY_SUBSET] THEN
\r
770 MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `{x:real^N}` THEN
\r
771 (CONJ_TAC THENL [SET_TAC[]; ALL_TAC]) THEN
\r
772 GEN_REWRITE_TAC LAND_CONV [GSYM AFFINE_HULL_SING] THEN
\r
773 REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN
\r
774 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
\r
775 RULE_ASSUM_TAC(REWRITE_RULE[INSERT_SUBSET; EMPTY_SUBSET]) THEN
\r
776 RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM]) THEN
\r
777 X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
\r
778 SUBGOAL_THEN `~(y:real^N = x)` ASSUME_TAC THENL
\r
779 [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
780 ASM_SIMP_TAC[lemma2] THEN ASM_SIMP_TAC[SET_RULE
\r
781 `(s UNION t) INTER u = s INTER u UNION t INTER u`] THEN
\r
782 ASM_SIMP_TAC[lemma1; UNION_OVER_INTER; UNION_EMPTY] THEN
\r
783 ASM_CASES_TAC `y:real^N = v` THENL
\r
784 [ASM_REWRITE_TAC[INTER_IDEMPOT] THEN
\r
785 SUBGOAL_THEN `{w:real^N} INTER {v} = {} /\ {v,w} INTER {v} = {v}`
\r
786 (CONJUNCTS_THEN SUBST1_TAC) THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
787 MATCH_MP_TAC(SET_RULE
\r
788 `{x} SUBSET t /\ u SUBSET t ==> (s INTER {x}) UNION t UNION u = t`) THEN
\r
789 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM AFFINE_HULL_SING] THEN
\r
790 REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN
\r
791 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
\r
793 ASM_CASES_TAC `y:real^N = w` THENL
\r
794 [ASM_REWRITE_TAC[INTER_IDEMPOT] THEN
\r
795 SUBGOAL_THEN `{v:real^N} INTER {w} = {} /\ {v,w} INTER {w} = {w}`
\r
796 (CONJUNCTS_THEN SUBST1_TAC) THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
797 MATCH_MP_TAC(SET_RULE
\r
798 `{x} SUBSET t /\ t SUBSET u ==> (s INTER {x}) UNION t UNION u = u`) THEN
\r
799 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM AFFINE_HULL_SING] THEN
\r
800 REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN CONJ_TAC THEN
\r
801 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
\r
803 SUBGOAL_THEN `{v:real^N} INTER {y} = {} /\ {w} INTER {y} = {} /\
\r
804 {v, w} INTER {y} = {}`
\r
805 (REPEAT_TCL CONJUNCTS_THEN SUBST1_TAC) THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
806 MATCH_MP_TAC(SET_RULE
\r
807 `{x} SUBSET s ==> a INTER {x} UNION s UNION s = s`) THEN
\r
808 GEN_REWRITE_TAC LAND_CONV [GSYM AFFINE_HULL_SING] THEN
\r
809 REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL] THEN
\r
810 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]]);;
\r
812 let FAN_AFF_GT_CONDITION = prove
\r
814 UNIONS E SUBSET V /\
\r
819 (!v w. v IN V /\ w IN V
\r
820 ==> aff_ge {x} {v} INTER aff_ge {x} {w} =
\r
821 aff_ge {x} ({v} INTER {w})) /\
\r
822 (!v e. v IN V /\ e IN E
\r
823 ==> aff_gt {x} {v} INTER aff_gt {x} e = {}) /\
\r
824 (!e1 e2. e1 IN E /\ e2 IN E /\ ~(e1 = e2)
\r
825 ==> aff_gt {x} e1 INTER aff_gt {x} e2 = {})
\r
827 REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[Fan.FAN] THEN
\r
828 MATCH_MP_TAC FAN7_AFF_GT_CONDITION THEN ASM_REWRITE_TAC[] THEN
\r
829 RULE_ASSUM_TAC(REWRITE_RULE[Fan.fan2; UNIONS_SUBSET]) THEN
\r
830 ASM_SIMP_TAC[] THEN ASM SET_TAC[]);;
\r
832 let GMLWKPK_SIMPLE = prove
\r
834 UNIONS E SUBSET V /\ graph E /\ fan6(x,V,E) /\
\r
835 (!e. e IN E ==> ~(x IN e))
\r
836 ==> (fan7 (x,V,E) <=>
\r
838 e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\
\r
840 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x})`,
\r
843 ~collinear{x,u,v} /\ ~collinear{x,v,w}
\r
844 ==> (~(aff_ge {x} {u,v} INTER aff_ge {x} {v,w} =
\r
845 aff_ge {x} {v}) <=>
\r
846 u IN aff_ge {x} {v,w} \/ w IN aff_ge {x} {u,v})`,
\r
847 REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `x:real^N` THEN
\r
848 REPEAT GEN_TAC THEN
\r
849 MAP_EVERY (fun t ->
\r
850 ASM_CASES_TAC t THENL
\r
851 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC])
\r
852 [`u:real^N = v`; `w:real^N = v`;
\r
853 `u:real^N = vec 0`; `v:real^N = vec 0`; `w:real^N = vec 0`] THEN
\r
854 STRIP_TAC THEN EQ_TAC THENL
\r
855 [DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE
\r
857 ==> t SUBSET s /\ t SUBSET s' ==> t PSUBSET s INTER s'`)) THEN
\r
859 [CONJ_TAC THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
\r
860 REWRITE_TAC[PSUBSET_ALT]] THEN
\r
861 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
\r
862 ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; LEFT_IMP_EXISTS_THM] THEN
\r
863 REWRITE_TAC[IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN
\r
864 MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
\r
865 DISCH_TAC THEN DISCH_TAC THEN
\r
866 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
867 MAP_EVERY X_GEN_TAC [`c:real`; `d:real`] THEN STRIP_TAC THEN
\r
868 ASM_CASES_TAC `a = &0` THENL
\r
869 [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]; ALL_TAC] THEN
\r
870 ASM_CASES_TAC `d = &0` THENL
\r
871 [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID]; ALL_TAC] THEN
\r
872 DISCH_THEN(K ALL_TAC) THEN DISJ_CASES_TAC
\r
873 (REAL_ARITH `b <= c \/ c <= b`)
\r
875 [FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH
\r
876 `a % u + b % v:real^N = c % v + d % w
\r
877 ==> a % u = (c - b) % v + d % w`)) THEN
\r
878 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a):real^N->real^N`) THEN
\r
879 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
\r
880 DISCH_THEN(K ALL_TAC) THEN DISJ1_TAC THEN
\r
881 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
\r
882 MAP_EVERY EXISTS_TAC [`inv a * (c - b):real`; `inv a * d:real`] THEN
\r
883 ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE];
\r
884 FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH
\r
885 `a % u + b % v:real^N = c % v + d % w
\r
886 ==> d % w = (b - c) % v + a % u`)) THEN
\r
887 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv d):real^N->real^N`) THEN
\r
888 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
\r
889 DISCH_THEN(K ALL_TAC) THEN DISJ2_TAC THEN
\r
890 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
\r
891 MAP_EVERY EXISTS_TAC [`inv d * a:real`; `inv d * (b - c):real`] THEN
\r
892 ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE] THEN
\r
893 REWRITE_TAC[VECTOR_ADD_SYM]];
\r
894 STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
\r
895 `(?x. x IN s /\ x IN t /\ ~(x IN u)) ==> ~(s INTER t = u)`)
\r
897 [EXISTS_TAC `u:real^N` THEN ASM_REWRITE_TAC[] THEN
\r
898 ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN
\r
900 [MAP_EVERY EXISTS_TAC [`&1`; `&0`] THEN
\r
901 REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;
\r
902 DISCH_THEN(X_CHOOSE_THEN `a:real`
\r
903 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
\r
904 UNDISCH_TAC `~collinear{vec 0:real^N,a % v,v}` THEN
\r
906 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
\r
907 REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]];
\r
908 EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[] THEN
\r
909 ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN
\r
911 [MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
\r
912 REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;
\r
913 DISCH_THEN(X_CHOOSE_THEN `a:real`
\r
914 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
\r
915 UNDISCH_TAC `~collinear{vec 0:real^N,v,a % v}` THEN
\r
916 REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]]]]) in
\r
917 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN
\r
918 EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN
\r
919 REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(MESON[]
\r
920 `(!x y. R x y ==> R y x) /\
\r
921 (!x. Q x ==> !y. Q y ==> R x y) /\
\r
922 (!x. P x ==> (!y. Q y ==> R x y) /\ (!y. P y ==> R x y))
\r
923 ==> (!x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y)`) THEN
\r
924 CONJ_TAC THENL [SIMP_TAC[INTER_ACI]; ALL_TAC] THEN
\r
925 REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL
\r
926 [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> c = a /\ b = a`] THEN
\r
927 REWRITE_TAC[INTER_IDEMPOT];
\r
929 X_GEN_TAC `ee1:real^N->bool` THEN DISCH_TAC THEN CONJ_TAC THENL
\r
930 [X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN
\r
931 REWRITE_TAC[SET_RULE `s INTER {a} = {b} <=> b = a /\ a IN s`] THEN
\r
932 SIMP_TAC[IMP_CONJ; FORALL_UNWIND_THM2] THEN DISCH_TAC THEN
\r
933 REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
\r
934 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
\r
936 X_GEN_TAC `ee2:real^N->bool` THEN DISCH_TAC THEN
\r
937 SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
938 [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
939 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
940 MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN
\r
941 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
942 SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
943 [ASM_MESON_TAC[Fan.graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
944 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
945 MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN
\r
946 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
947 ONCE_REWRITE_TAC[SET_RULE
\r
948 `{a,b} INTER {c,d} = {v} <=>
\r
949 v = a /\ {a,b} INTER {c,d} = {v} \/
\r
950 v = b /\ {a,b} INTER {c,d} = {v}`] THEN
\r
952 `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN
\r
953 REWRITE_TAC[FORALL_AND_THM; FORALL_UNWIND_THM2] THEN
\r
954 MAP_EVERY UNDISCH_TAC [`{v1:real^N,w1} IN E`; `~(v1:real^N = w1)`] THEN
\r
955 MAP_EVERY (fun s -> SPEC_TAC(s,s))
\r
956 [`w1:real^N`; `v1:real^N`] THEN
\r
957 REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]
\r
958 `(!v w. P v w ==> P w v) /\
\r
959 (!v w. R v w ==> Q w v) /\
\r
960 (!v w. P v w ==> R v w)
\r
961 ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN
\r
962 REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN
\r
963 MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
\r
964 ONCE_REWRITE_TAC[SET_RULE
\r
965 `{a,b} INTER {c,d} = {v} <=>
\r
966 v = c /\ {a,b} INTER {c,d} = {v} \/
\r
967 v = d /\ {a,b} INTER {c,d} = {v}`] THEN
\r
969 `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN
\r
970 MAP_EVERY UNDISCH_TAC [`{v2:real^N,w2} IN E`; `~(v2:real^N = w2)`] THEN
\r
971 MAP_EVERY (fun s -> SPEC_TAC(s,s)) [`w2:real^N`; `v2:real^N`] THEN
\r
972 REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]
\r
973 `(!v w. P v w ==> P w v) /\
\r
974 (!v w. Q v w ==> R w v) /\
\r
975 (!v w. P v w ==> Q v w)
\r
976 ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN
\r
977 REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN
\r
978 MAP_EVERY X_GEN_TAC [`v':real^N`; `w:real^N`] THEN STRIP_TAC THEN
\r
979 ONCE_REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
\r
980 ASM_CASES_TAC `u:real^N = w` THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
981 DISCH_TAC THEN W(MP_TAC o PART_MATCH (rand o lhand o rand) lemma o goal_concl) THEN
\r
983 [REWRITE_TAC[SET_RULE `{x,v,w} = {x} UNION {v,w}`] THEN
\r
984 ASM_MESON_TAC[Fan.fan6; INSERT_AC];
\r
986 MATCH_MP_TAC(TAUT `~q ==> (~p <=> q) ==> p`) THEN
\r
987 REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
\r
988 `aff_ge {x} {v} INTER aff_ge {x} s = {x} /\
\r
989 v IN aff_ge {x} {v} /\ ~(v = x)
\r
990 ==> ~(v IN aff_ge {x} s)`) THEN
\r
991 REPEAT CONJ_TAC THENL
\r
992 [FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
993 ASM_REWRITE_TAC[IN_UNION] THEN
\r
994 CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN
\r
995 REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `u:real^N` THEN
\r
996 REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN
\r
997 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
998 REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{u:real^N,v}` THEN
\r
1000 SUBGOAL_THEN `DISJOINT {x:real^N} {u:real^N}` ASSUME_TAC THENL
\r
1001 [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
\r
1002 ASM_MESON_TAC[IN_INSERT];
\r
1003 ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN
\r
1004 MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
\r
1005 REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];
\r
1006 ASM_MESON_TAC[IN_INSERT];
\r
1007 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1008 ASM_REWRITE_TAC[IN_UNION] THEN
\r
1009 CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN
\r
1010 REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `w:real^N` THEN
\r
1011 REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN
\r
1012 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1013 REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{v:real^N,w}` THEN
\r
1015 SUBGOAL_THEN `DISJOINT {x:real^N} {w:real^N}` ASSUME_TAC THENL
\r
1016 [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
\r
1017 ASM_MESON_TAC[IN_INSERT];
\r
1018 ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN
\r
1019 MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
\r
1020 REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];
\r
1021 ASM_MESON_TAC[IN_INSERT]]);;
\r
1023 let FAN_ECONOMIZED_SIMPLE = prove
\r
1026 UNIONS E SUBSET V /\
\r
1031 (!e1 e2. e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\
\r
1033 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x})`,
\r
1034 REPEAT GEN_TAC THEN REWRITE_TAC[Fan.FAN] THEN
\r
1035 REWRITE_TAC[CONJ_ASSOC] THEN
\r
1036 MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
\r
1037 REWRITE_TAC[GSYM CONJ_ASSOC] THEN
\r
1038 STRIP_TAC THEN MATCH_MP_TAC GMLWKPK_SIMPLE THEN
\r
1039 ASM_REWRITE_TAC[] THEN X_GEN_TAC `e:real^N->bool` THEN DISCH_TAC THEN
\r
1040 FIRST_X_ASSUM(MP_TAC o SPEC `e:real^N->bool` o
\r
1041 GEN_REWRITE_RULE I [Fan.fan6]) THEN
\r
1042 ASM_REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_TAC THEN
\r
1043 ASM_SIMP_TAC[SET_RULE `x IN u ==> {x} UNION u = u`] THEN
\r
1044 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.GRAPH]) THEN
\r
1045 DISCH_THEN(MP_TAC o SPEC `e:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
\r
1046 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
\r
1047 STRIP_TAC THEN ASM_REWRITE_TAC[COLLINEAR_2]);;
\r
1049 (* ------------------------------------------------------------------------- *)
\r
1050 (* Definition of the polar fan. *)
\r
1051 (* ------------------------------------------------------------------------- *)
\r
1053 let JNVXCRC = new_definition
\r
1054 `polar_fan(V,(E:(real^3->bool)->bool),FF) =
\r
1055 let r = rho_node1 FF in
\r
1056 let prime = \v. v cross (r v) in
\r
1057 ({ prime v | v IN V},
\r
1058 { {prime v,prime(r v)} | v IN V},
\r
1059 { (prime v,prime(r v)) | v IN V})`;;
\r
1061 (* ------------------------------------------------------------------------- *)
\r
1062 (* Properties of the polar fan. *)
\r
1063 (* ------------------------------------------------------------------------- *)
\r
1065 let BGMIFTE = prove
\r
1066 (`!V E FF V' E' FF'.
\r
1067 convex_local_fan(V,E,FF) /\ generic V E /\
\r
1068 (!v. v IN V ==> interior_angle1 (vec 0) FF v < pi) /\
\r
1069 (V',E',FF') = polar_fan (V,E,FF)
\r
1070 ==> convex_local_fan(V',E',FF') /\
\r
1072 CARD V' = CARD V /\
\r
1073 let r = rho_node1 FF in
\r
1074 let prime = \v. v cross (r v) in
\r
1076 ==> arcV (vec 0) (prime v) (prime(r v)) =
\r
1077 pi - interior_angle1 (vec 0) FF (r v) /\
\r
1078 &0 < arcV (vec 0) (prime v) (prime(r v)) /\
\r
1079 arcV (vec 0) (prime v) (prime(r v)) < pi) /\
\r
1081 ==> arcV (vec 0) v (r v) =
\r
1082 pi - interior_angle1 (vec 0) FF' (prime v) /\
\r
1083 &0 < arcV (vec 0) v (r v) /\
\r
1084 arcV (vec 0) v (r v) < pi)`,
\r
1085 let lemma1 = prove
\r
1086 (`((v0 cross v1) cross (v1 cross v2)) dot (w0 cross w1) =
\r
1087 ((v1 cross v2) dot v0) * ((w0 cross w1) dot v1)`,
\r
1089 and lemma2 = prove
\r
1090 (`(v cross v') cross (w cross w') =
\r
1091 ((w cross w') dot v) % v' - ((w cross w') dot v') % v`,
\r
1093 and lemma3 = prove
\r
1094 (`a % v:real^N = b % w ==> a = &0 /\ b = &0 \/ collinear{vec 0,w,v}`,
\r
1095 ASM_CASES_TAC `a = &0` THEN ASM_CASES_TAC `b = &0` THEN
\r
1096 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0; VECTOR_ARITH
\r
1097 `vec 0:real^N = a % b <=> a % b = vec 0`] THEN
\r
1098 TRY(SIMP_TAC[INSERT_AC; COLLINEAR_2] THEN NO_TAC) THEN
\r
1099 REWRITE_TAC[COLLINEAR_LEMMA] THEN
\r
1100 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a) :real^N->real^N`) THEN
\r
1101 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
\r
1103 and lemma4 = prove
\r
1104 (`(v1 cross v2) cross (v0 cross v1) = --(((v0 cross v1) dot v2) % v1)`,
\r
1106 and lemma5 = prove
\r
1107 (`(v0 cross v1) cross (v1 cross v2) = ((v0 cross v1) dot v2) % v1`,
\r
1109 and lemma6 = prove
\r
1110 (`(x cross y) dot z = (z cross x) dot y`,
\r
1112 and lemma7 = prove
\r
1113 (`!a b c d:real^N.
\r
1114 ~(aff_gt {a,b,c} {d} INTER affine hull {a,b,c} = {})
\r
1115 ==> d IN affine hull {a,b,c}`,
\r
1116 REPEAT GEN_TAC THEN DISJ_CASES_TAC
\r
1117 (SET_RULE `(d:real^N) IN {a,b,c} \/ DISJOINT {a,b,c} {d}`) THEN
\r
1118 ASM_SIMP_TAC[HULL_INC] THEN ASM_SIMP_TAC[AFF_GT_3_1; AFFINE_HULL_3] THEN
\r
1119 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
\r
1120 ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[EXISTS_IN_GSPEC] THEN
\r
1121 REWRITE_TAC[IN_ELIM_THM; RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
\r
1122 MAP_EVERY X_GEN_TAC [`xa:real`; `xb:real`; `xc:real`;
\r
1123 `ya:real`; `yb:real`; `yc:real`; `u:real`] THEN
\r
1124 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
1125 REWRITE_TAC[VECTOR_ARITH
\r
1126 `xa % a + xb % b + xc % c :real^N = ya % a + yb % b + yc % c + d <=>
\r
1127 d = (xa - ya) % a + (xb - yb) % b + (xc - yc) % c`] THEN
\r
1129 MAP_EVERY EXISTS_TAC
\r
1130 [`(xa - ya) / u:real`; `(xb - yb) / u:real`; `(xc - yc) / u:real`] THEN
\r
1131 ASM_SIMP_TAC[REAL_FIELD
\r
1132 `&0 < u ==> (a / u + b / u + c / u = &1 <=> a + b + c = u)`] THEN
\r
1133 CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
\r
1134 FIRST_X_ASSUM(MP_TAC o AP_TERM `(%) (inv u) :real^N->real^N`) THEN
\r
1135 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_LT_IMP_NZ; REAL_MUL_LINV] THEN
\r
1136 REWRITE_TAC[VECTOR_MUL_LID] THEN DISCH_THEN SUBST1_TAC THEN
\r
1137 VECTOR_ARITH_TAC) in
\r
1138 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT LET_TAC THEN
\r
1139 FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I
\r
1140 [Wrgcvdr_cizmrrh.convex_local_fan]) THEN
\r
1141 SUBGOAL_THEN `!v. v IN V ==> ~((prime:real^3->real^3) v = vec 0)`
\r
1143 [GEN_TAC THEN STRIP_TAC THEN
\r
1144 EXPAND_TAC "prime" THEN REWRITE_TAC[CROSS_EQ_0] THEN
\r
1145 EXPAND_TAC "r" THEN
\r
1146 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
1149 `!v w. v IN V /\ w IN V /\ ~(v = w)
\r
1150 ==> ~collinear{vec 0,(prime:real^3->real^3) v,prime w}`
\r
1152 [REPEAT GEN_TAC THEN STRIP_TAC THEN
\r
1153 REWRITE_TAC[GSYM CROSS_EQ_0] THEN EXPAND_TAC "prime" THEN
\r
1154 REWRITE_TAC[lemma2; VECTOR_SUB_EQ] THEN
\r
1155 DISCH_THEN(MP_TAC o MATCH_MP lemma3) THEN
\r
1156 REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THENL
\r
1158 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]] THEN
\r
1159 SUBGOAL_THEN `~(v:real^3 = r w /\ w = r v)` MP_TAC THENL
\r
1160 [EXPAND_TAC "r" THEN
\r
1161 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE];
\r
1162 REWRITE_TAC[DE_MORGAN_THM] THEN MATCH_MP_TAC MONO_OR THEN
\r
1163 CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_IMP_NZ THEN
\r
1164 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
1165 EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN
\r
1166 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN
\r
1167 ASM_REWRITE_TAC[] THEN EXPAND_TAC "r" THEN
\r
1168 ASM_MESON_TAC[RHO_NODE1_INJECTIVE;
\r
1169 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]];
\r
1171 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [JNVXCRC]) THEN
\r
1172 ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
\r
1173 ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
\r
1174 REWRITE_TAC[PAIR_EQ] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
\r
1176 `!v w. v IN V /\ w IN V
\r
1177 ==> ((prime:real^3->real^3) v = prime w <=> v = w)`
\r
1178 ASSUME_TAC THENL [ASM_MESON_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
\r
1179 FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOCAL_FAN_FINITE_V) THEN
\r
1180 SUBGOAL_THEN `CARD(V':real^3->bool) = CARD(V:real^3->bool)` ASSUME_TAC THENL
\r
1181 [EXPAND_TAC "V'" THEN REWRITE_TAC[SIMPLE_IMAGE] THEN
\r
1182 MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_MESON_TAC[];
\r
1183 ASM_REWRITE_TAC[]] THEN
\r
1185 `!v w:real^3. v IN V /\ w IN V /\ ~(w = v) /\ ~(w = r v)
\r
1186 ==> &0 < sin(azim (vec 0) (prime v) (prime(r v)) (prime w))`
\r
1188 [REPEAT STRIP_TAC THEN REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
1189 EXPAND_TAC "prime" THEN REWRITE_TAC[lemma1] THEN
\r
1190 MATCH_MP_TAC REAL_LT_MUL THEN
\r
1191 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN CONJ_TAC THENL
\r
1192 [FIRST_ASSUM(MP_TAC o SPEC `(r:real^3->real^3) v` o
\r
1193 MATCH_MP Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) THEN
\r
1194 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
\r
1195 [EXPAND_TAC "r" THEN
\r
1196 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1198 MATCH_MP_TAC(MESON[] `(c' = c /\ d = d') /\ &0 < sin i
\r
1199 ==> i = azim a b c d ==> &0 < sin(azim a b c' d')`) THEN
\r
1200 REWRITE_TAC[] THEN CONJ_TAC THENL
\r
1201 [EXPAND_TAC "r" THEN MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD THEN
\r
1203 MATCH_MP_TAC SIN_POS_PI THEN EXPAND_TAC "r" THEN
\r
1204 ASM_MESON_TAC[Local_lemmas.INTERIOR_ANGLE1_POS;
\r
1205 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]];
\r
1206 EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN
\r
1207 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN
\r
1208 ASM_REWRITE_TAC[] THEN
\r
1209 ASM_MESON_TAC[RHO_NODE1_INJECTIVE;
\r
1210 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]];
\r
1213 `!v w:real^3. v IN V /\ w IN V /\ ~(w = v) /\ ~(w = r v)
\r
1214 ==> &0 < azim (vec 0) (prime v) (prime(r v)) (prime w) /\
\r
1215 azim (vec 0) (prime v) (prime(r v)) (prime w) < pi`
\r
1217 [REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC SIN_POS_PI_REV THEN
\r
1218 ASM_SIMP_TAC[azim; REAL_LT_IMP_LE];
\r
1220 ONCE_REWRITE_TAC[TAUT `p /\ q /\ r /\ s <=> r /\ s /\ p /\ q`] THEN
\r
1222 [X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
\r
1224 [`vec 0:real^3`; `(r:real^3->real^3) v`; `v:real^3`;
\r
1225 `(r:real^3->real^3) (r v)`]
\r
1226 Hvihvec.HVIHVEC) THEN
\r
1227 CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
\r
1228 REWRITE_TAC[VECTOR_SUB_RZERO] THEN ANTS_TAC THENL
\r
1229 [EXPAND_TAC "r" THEN
\r
1230 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_V_DIFF;
\r
1231 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1233 EXPAND_TAC "prime" THEN
\r
1234 SUBST1_TAC(ISPECL [`v:real^3`; `(r:real^3->real^3) v`] CROSS_SKEW) THEN
\r
1235 REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO; VECTOR_ANGLE_LNEG] THEN
\r
1236 DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC(REAL_ARITH
\r
1237 `x = y /\ &0 < x /\ x < pi
\r
1238 ==> pi - x = pi - y /\ &0 < pi - x /\ pi - x < pi`) THEN
\r
1239 FIRST_ASSUM(MP_TAC o SPEC `(r:real^3->real^3) v` o
\r
1240 MATCH_MP Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) THEN
\r
1242 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN
\r
1243 MATCH_MP_TAC(REAL_ARITH
\r
1244 `&0 < i /\ i < pi /\
\r
1245 (&0 < a /\ a < pi ==> d = a)
\r
1246 ==> i = a ==> d = i /\ &0 < d /\ d < pi`) THEN
\r
1247 REPEAT(CONJ_TAC THENL
\r
1248 [ASM_MESON_TAC[Local_lemmas.INTERIOR_ANGLE1_POS;
\r
1249 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1251 SUBGOAL_THEN `ivs_rho_node1 FF (r v) = v` SUBST1_TAC THENL
\r
1252 [ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]; ALL_TAC] THEN
\r
1253 ONCE_REWRITE_TAC[DIHV_SYM] THEN ASM_REWRITE_TAC[] THEN
\r
1254 STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC AZIM_DIHV_SAME THEN
\r
1255 ASM_REWRITE_TAC[] THEN
\r
1256 GEN_REWRITE_TAC (funpow 3 RAND_CONV) [SET_RULE `{a,c,b} = {a,b,c}`] THEN
\r
1257 EXPAND_TAC "r" THEN
\r
1258 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
\r
1259 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1261 FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN
\r
1263 `!v w. v IN V /\ w IN V /\
\r
1264 ~(w = v) /\ ~(w = r v) /\ ~(w = ivs_rho_node1 FF v)
\r
1265 ==> &0 < azim (vec 0) (prime v) (prime (r v)) (prime w) /\
\r
1266 azim (vec 0) (prime v) (prime (r v)) (prime w) <
\r
1267 azim (vec 0) (prime v) (prime (r v))
\r
1268 (prime (ivs_rho_node1 FF v))`
\r
1270 [REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN
\r
1272 `~(prime w = prime v) /\
\r
1273 ~(prime w = prime(r v)) /\
\r
1274 ~(prime w:real^3 = prime(ivs_rho_node1 FF v))`
\r
1275 STRIP_ASSUME_TAC THENL
\r
1276 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1277 IVS_RHO_NODE1_IN_V];
\r
1279 MP_TAC(ISPECL [`vec 0:real^3`; `(prime:real^3->real^3) v`;
\r
1280 `prime(r(v:real^3):real^3):real^3`;
\r
1281 `(prime:real^3->real^3) w`;
\r
1282 `(prime:real^3->real^3) (ivs_rho_node1 FF v)`]
\r
1283 Fan.sum3_azim_fan) THEN
\r
1286 [MATCH_MP_TAC(REAL_ARITH
\r
1287 `(&0 < x /\ x < pi) /\ (&0 < y /\ y < pi) ==> x + y < &2 * pi`) THEN
\r
1289 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1290 ASM_REWRITE_TAC[] THEN
\r
1291 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1292 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD;
\r
1293 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]];
\r
1294 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LT_ADDR] THEN
\r
1295 MATCH_MP_TAC(REAL_ARITH `&0 < x /\ x < pi ==> &0 < x`)] THEN
\r
1296 MATCH_MP_TAC SIN_POS_PI_REV THEN
\r
1297 SIMP_TAC[azim; REAL_LT_IMP_LE] THEN
\r
1298 REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
1299 ONCE_REWRITE_TAC[lemma6] THEN
\r
1300 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
1301 ABBREV_TAC `u = ivs_rho_node1 FF v` THEN
\r
1302 (SUBGOAL_THEN `v = (r:real^3->real^3) u` ASSUME_TAC THENL
\r
1303 [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD; IVS_RHO_NODE1_IN_V]; ALL_TAC]) THEN
\r
1304 ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1305 ASM_MESON_TAC[IVS_RHO_NODE1_IN_V];
\r
1309 ==> arcV (vec 0) v (r v) =
\r
1310 pi - azim (vec 0) (prime v)
\r
1311 (prime(r v)) (prime(ivs_rho_node1 FF v)) /\
\r
1312 &0 < arcV (vec 0) v (r v) /\
\r
1313 arcV (vec 0) v (r v) < pi`
\r
1315 [X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
\r
1316 MATCH_MP_TAC(REAL_ARITH
\r
1317 `!d. (&0 < a /\ a < pi) /\
\r
1318 (&0 < a /\ a < pi ==> d = a) /\
\r
1320 ==> v = pi - a /\ &0 < v /\ v < pi`) THEN
\r
1321 EXISTS_TAC `dihV (vec 0:real^3) (prime v) (prime (r v))
\r
1322 (prime (ivs_rho_node1 FF v))` THEN
\r
1324 [FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1325 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1326 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
\r
1327 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD];
\r
1330 [STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC AZIM_DIHV_SAME THEN
\r
1331 ASM_REWRITE_TAC[] THEN
\r
1332 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1333 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1334 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1335 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
\r
1336 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD];
\r
1338 W(MP_TAC o PART_MATCH (lhs o rand) Hvihvec.HVIHVEC o lhand o goal_concl) THEN
\r
1339 ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST1_TAC] THEN
\r
1340 REWRITE_TAC[VECTOR_SUB_RZERO] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
\r
1341 EXPAND_TAC "prime" THEN
\r
1342 SUBGOAL_THEN `r (ivs_rho_node1 FF v) = v` SUBST1_TAC THENL
\r
1343 [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN
\r
1344 ONCE_REWRITE_TAC[VECTOR_ANGLE_SYM] THEN
\r
1345 REWRITE_TAC[lemma4; lemma5; VECTOR_ANGLE_LNEG] THEN AP_TERM_TAC THEN
\r
1347 `&0 < (ivs_rho_node1 FF v cross v) dot r v /\
\r
1348 &0 < ((v cross r v) dot r (r v))`
\r
1349 STRIP_ASSUME_TAC THENL
\r
1350 [REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN CONJ_TAC THENL
\r
1351 [ABBREV_TAC `w = ivs_rho_node1 FF v` THEN
\r
1352 SUBGOAL_THEN `(w:real^3) IN V` ASSUME_TAC THENL
\r
1353 [ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN
\r
1354 SUBGOAL_THEN `v = (r:real^3->real^3) w` SUBST1_TAC THENL
\r
1355 [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD]; ALL_TAC];
\r
1357 EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN
\r
1358 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN
\r
1359 ASM_REWRITE_TAC[] THEN EXPAND_TAC "r" THEN
\r
1360 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1361 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
\r
1362 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
1363 REWRITE_TAC[ARCV_ANGLE; angle; VECTOR_SUB_RZERO] THEN
\r
1364 REWRITE_TAC[VECTOR_ANGLE_LMUL; VECTOR_ANGLE_RMUL] THEN
\r
1365 REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN ASM_REAL_ARITH_TAC];
\r
1367 SUBGOAL_THEN `FAN(vec 0:real^3,V',E')` ASSUME_TAC THENL
\r
1368 [MATCH_MP_TAC FAN_AFF_GT_CONDITION THEN
\r
1369 REPLICATE_TAC 4 (GEN_REWRITE_TAC I [CONJ_ASSOC]) THEN CONJ_TAC THENL
\r
1370 [REWRITE_TAC[Fan.fan1; Fan.fan2; Fan.fan6; Polyhedron.GRAPH;
\r
1371 UNIONS_SUBSET] THEN
\r
1372 MAP_EVERY EXPAND_TAC ["V'"; "E'"] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1373 REPEAT CONJ_TAC THENL
\r
1374 [REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN
\r
1375 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1376 X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
\r
1377 REWRITE_TAC[HAS_SIZE_2_EXISTS] THEN MAP_EVERY EXISTS_TAC
\r
1378 [`(prime:real^3->real^3) (v:real^3)`;
\r
1379 `(prime:real^3->real^3) ((r:real^3->real^3) v)`] THEN
\r
1380 CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
\r
1381 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1382 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1383 ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC FINITE_IMAGE THEN
\r
1384 ASM_REWRITE_TAC[];
\r
1385 UNDISCH_TAC `~(V:real^3->bool = {})` THEN SET_TAC[];
\r
1387 X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
\r
1388 REWRITE_TAC[SET_RULE `{a} UNION {b,c} = {a,b,c}`] THEN
\r
1389 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1390 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1391 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]];
\r
1393 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
\r
1394 MAP_EVERY EXPAND_TAC ["V'"; "E'"] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1395 REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM] THEN CONJ_TAC THENL
\r
1396 [MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN STRIP_TAC THEN
\r
1397 ASM_CASES_TAC `w:real^3 = v` THEN ASM_REWRITE_TAC[INTER_IDEMPOT] THEN
\r
1398 ASM_SIMP_TAC[SET_RULE `~(x = y) ==> {x} INTER {y} = {}`] THEN
\r
1399 MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
\r
1400 [REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING] THEN
\r
1401 MATCH_MP_TAC SUBSET_TRANS THEN
\r
1402 EXISTS_TAC `(affine hull ({vec 0:real^3} UNION {prime v})) INTER
\r
1403 (affine hull ({vec 0} UNION {prime(w:real^3)}))` THEN
\r
1404 SIMP_TAC[AFF_GE_SUBSET_AFFINE_HULL; SET_RULE
\r
1405 `s SUBSET s' /\ t SUBSET t' ==> s INTER t SUBSET s' INTER t'`] THEN
\r
1406 W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INTER o
\r
1407 lhand o goal_concl) THEN
\r
1408 REWRITE_TAC[SET_RULE
\r
1409 `({z} UNION {a}) UNION ({z} UNION {b}) = {z,a,b}`] THEN
\r
1411 [DISCH_THEN(MP_TAC o MATCH_MP AFFINE_DEPENDENT_IMP_COLLINEAR_3) THEN
\r
1413 DISCH_THEN SUBST1_TAC] THEN
\r
1415 `({vec 0} UNION {(prime:real^3->real^3) v}) INTER
\r
1416 ({vec 0} UNION {prime w}) = {vec 0}`
\r
1417 (fun th -> SIMP_TAC[th; AFFINE_HULL_SING; SUBSET_REFL]) THEN
\r
1419 REWRITE_TAC[SUBSET_INTER] THEN CONJ_TAC THEN
\r
1420 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]];
\r
1422 MATCH_MP_TAC(SET_RULE
\r
1423 `(!a b. P a /\ P b /\ f a = f b ==> a = b) /\
\r
1424 (!a b. R a b ==> R b a) /\
\r
1425 Q /\ (!a b. P a /\ P b /\ ~({f a,g a} = {f b,g b}) /\
\r
1426 ~(b = a) /\ ~(f b = f a) /\ ~(f b = g a)
\r
1428 ==> Q /\ !a b. (P a /\ P b) /\ ~({f a,g a} = {f b,g b}) ==> R a b`) THEN
\r
1429 CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
1430 CONJ_TAC THENL [SIMP_TAC[INTER_COMM]; ALL_TAC] THEN
\r
1431 GEN_REWRITE_TAC LAND_CONV [SWAP_FORALL_THM] THEN
\r
1432 GEN_REWRITE_TAC I [CONJ_SYM] THEN
\r
1433 GEN_REWRITE_TAC I [AND_FORALL_THM] THEN X_GEN_TAC `v:real^3` THEN
\r
1434 ASM_CASES_TAC `(v:real^3) IN V` THEN ASM_REWRITE_TAC[] THEN
\r
1435 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [INTER_COMM] THEN
\r
1437 `aff_gt {vec 0} {(prime:real^3->real^3) v, prime (r v)} SUBSET
\r
1438 affine hull {vec 0, prime v,prime(r v)}`
\r
1440 [MATCH_MP_TAC SUBSET_TRANS THEN
\r
1441 EXISTS_TAC `aff_ge {vec 0} {(prime:real^3->real^3) v, prime (r v)}` THEN
\r
1442 REWRITE_TAC[AFF_GT_SUBSET_AFF_GE] THEN
\r
1443 REWRITE_TAC[GSYM AFF_GE_EQ_AFFINE_HULL; aff_ge_def] THEN
\r
1444 MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[];
\r
1447 `aff_gt {vec 0,prime v, prime (r v)} {prime(ivs_rho_node1 FF v)} INTER
\r
1448 affine hull {vec 0, (prime:real^3->real^3) v,prime(r v)} = {}`
\r
1450 [GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN
\r
1451 DISCH_THEN(ASSUME_TAC o MATCH_MP lemma7) THEN
\r
1453 `coplanar {vec 0,(prime:real^3->real^3) v, prime (r v),
\r
1454 prime(ivs_rho_node1 FF v)}`
\r
1456 [MATCH_MP_TAC(MESON[coplanar]
\r
1457 `{a,b,c,d} SUBSET affine hull {a,b,c} ==> coplanar {a,b,c,d}`) THEN
\r
1458 ASM_SIMP_TAC[INSERT_SUBSET; HULL_INC; IN_INSERT; EMPTY_SUBSET];
\r
1460 W(MP_TAC o PART_MATCH (rhs o rand) AZIM_EQ_0_PI_EQ_COPLANAR o
\r
1461 lhand o goal_concl) THEN
\r
1463 [CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC;
\r
1464 DISCH_THEN(SUBST1_TAC o SYM) THEN
\r
1465 MATCH_MP_TAC(REAL_ARITH
\r
1466 `&0 < x /\ x < pi ==> x = &0 \/ x = pi ==> F`) THEN
\r
1467 FIRST_X_ASSUM MATCH_MP_TAC] THEN
\r
1468 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1469 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD;
\r
1470 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1471 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE];
\r
1474 `!w z. {w,z} SUBSET
\r
1475 aff_gt {vec 0,prime v, prime (r v)} {prime(ivs_rho_node1 FF v)}
\r
1476 ==> aff_gt {vec 0} {(prime:real^3->real^3) v, prime (r v)} INTER
\r
1477 aff_gt {vec 0} {w,z} = {}`
\r
1479 [REPEAT GEN_TAC THEN
\r
1480 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP(SET_RULE
\r
1482 ==> ap INTER a = {} /\
\r
1483 (s SUBSET ap ==> aff_gt {vec 0} s SUBSET ap)
\r
1484 ==> s SUBSET ap ==> t INTER aff_gt {vec 0} s = {}`)) THEN
\r
1485 MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN
\r
1486 CONJ_TAC THENL [FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
\r
1487 MATCH_MP_TAC(SET_RULE
\r
1488 `!z. z IN a /\ (DISJOINT {z} p /\ p SUBSET g ==> q SUBSET g)
\r
1489 ==> g INTER a = {} ==> p SUBSET g ==> q SUBSET g`) THEN
\r
1490 EXISTS_TAC `vec 0:real^3` THEN
\r
1491 SIMP_TAC[HULL_INC; IN_INSERT; AFF_GT_1_2] THEN
\r
1492 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
\r
1493 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_3_1 o rand o lhand o goal_concl) THEN
\r
1495 [REWRITE_TAC[SET_RULE
\r
1496 `DISJOINT {a,b,c} {d} <=> ~(d = a) /\ ~(d = b) /\ ~(d = c)`] THEN
\r
1497 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1498 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD;
\r
1499 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1500 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE];
\r
1501 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
\r
1502 REWRITE_TAC[TAUT `p /\ t = &1 /\ q <=> t = &1 /\ p /\ q`] THEN
\r
1503 REWRITE_TAC[REAL_ARITH `t + s = &1 <=> t = &1 - s`] THEN
\r
1504 ONCE_REWRITE_TAC[MESON[]
\r
1505 `(?a b c d. P a b c d) <=> (?d b c a. P a b c d)`] THEN
\r
1506 REWRITE_TAC[UNWIND_THM2] THEN
\r
1507 ONCE_REWRITE_TAC[MESON[]
\r
1508 `(?a b c. P a b c) <=> (?b c a. P a b c)`] THEN
\r
1509 REWRITE_TAC[UNWIND_THM2] THEN DISCH_THEN SUBST1_TAC THEN
\r
1510 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
\r
1511 REWRITE_TAC[SUBSET; IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN
\r
1512 REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
\r
1513 MAP_EVERY X_GEN_TAC [`x1:real`; `x2:real`; `x3:real`] THEN
\r
1514 MAP_EVERY X_GEN_TAC [`y1:real`; `y2:real`; `y3:real`] THEN
\r
1515 STRIP_TAC THEN MAP_EVERY X_GEN_TAC
\r
1516 [`p:real^3`; `z1:real`; `z2:real`] THEN
\r
1517 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
1518 EXISTS_TAC `z1 * x1 + z2 * y1:real` THEN
\r
1519 EXISTS_TAC `z1 * x2 + z2 * y2:real` THEN
\r
1520 EXISTS_TAC `z1 * x3 + z2 * y3:real` THEN
\r
1521 ASM_SIMP_TAC[REAL_LT_MUL; REAL_LT_ADD] THEN VECTOR_ARITH_TAC];
\r
1524 `!w. w IN V /\ ~(w = v) /\ ~(w = r v)
\r
1525 ==> prime w IN aff_gt {vec 0, prime v, prime(r v)}
\r
1526 {(prime:real^3->real^3)(ivs_rho_node1 FF v)}`
\r
1528 [REPEAT STRIP_TAC THEN ASM_CASES_TAC `w = ivs_rho_node1 FF v` THENL
\r
1529 [W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_3_1 o rand o goal_concl) THEN
\r
1531 [REWRITE_TAC[SET_RULE
\r
1532 `DISJOINT {a,b,c} {d} <=> ~(d = a) /\ ~(d = b) /\ ~(d = c)`] THEN
\r
1533 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1534 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD;
\r
1535 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1536 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE];
\r
1537 DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
\r
1538 MAP_EVERY EXISTS_TAC [`&0`; `&0`; `&0`; `&1`] THEN
\r
1539 CONV_TAC REAL_RAT_REDUCE_CONV THEN VECTOR_ARITH_TAC];
\r
1542 `~(prime w = prime v) /\
\r
1543 ~(prime w = prime(r v)) /\
\r
1544 ~(prime w:real^3 = prime(ivs_rho_node1 FF v))`
\r
1545 STRIP_ASSUME_TAC THENL
\r
1546 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1547 IVS_RHO_NODE1_IN_V];
\r
1551 `(prime:real^3->real^3) v`;
\r
1552 `(prime:real^3->real^3) (r(v:real^3))`;
\r
1553 `(prime:real^3->real^3) (ivs_rho_node1 FF v)`]
\r
1554 WEDGE_LUNE_GT) THEN
\r
1555 REWRITE_TAC[wedge] THEN ANTS_TAC THENL
\r
1556 [REPEAT(FIRST_ASSUM MATCH_MP_TAC ORELSE CONJ_TAC) THEN
\r
1557 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1558 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD;
\r
1559 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
1560 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE];
\r
1562 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
\r
1563 DISCH_THEN(MP_TAC o SPEC `(prime:real^3->real^3) w`) THEN
\r
1564 MATCH_MP_TAC(TAUT `(q ==> r) /\ p ==> (p <=> q) ==> r`) THEN
\r
1565 REPEAT CONJ_TAC THENL
\r
1566 [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> x IN s ==> x IN t`) THEN
\r
1567 REWRITE_TAC[aff_gt_def] THEN MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN
\r
1569 FIRST_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[];
\r
1573 ONCE_REWRITE_TAC[CONJ_SYM] THEN CONJ_TAC THEN X_GEN_TAC `w:real^3` THENL
\r
1574 [DISCH_TAC THEN ASM_CASES_TAC `w:real^3 = v` THENL
\r
1575 [ASM_REWRITE_TAC[] THEN
\r
1576 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_1 o
\r
1577 rand o lhand o goal_concl) THEN
\r
1578 ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
\r
1579 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_2 o
\r
1580 lhand o lhand o goal_concl) THEN
\r
1581 REWRITE_TAC[SET_RULE
\r
1582 `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
\r
1584 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1585 DISCH_THEN SUBST1_TAC] THEN
\r
1586 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
\r
1587 REWRITE_TAC[TAUT `p /\ t = &1 /\ q <=> t = &1 /\ p /\ q`] THEN
\r
1588 REWRITE_TAC[REAL_ARITH `t + s = &1 <=> t = &1 - s`] THEN
\r
1589 ONCE_REWRITE_TAC[MESON[]
\r
1590 `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
\r
1591 REWRITE_TAC[UNWIND_THM2] THEN
\r
1592 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
\r
1593 REWRITE_TAC[UNWIND_THM2] THEN
\r
1594 SIMP_TAC[SET_RULE `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
\r
1595 X_GEN_TAC `p:real^3` THEN
\r
1596 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
1597 MAP_EVERY X_GEN_TAC [`t1:real`; `t2:real`] THEN STRIP_TAC THEN
\r
1598 DISCH_THEN(X_CHOOSE_THEN `t3:real` MP_TAC) THEN ASM_REWRITE_TAC[] THEN
\r
1599 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
\r
1600 REWRITE_TAC[VECTOR_ARITH
\r
1601 `a % v + b % w:real^N = c % v <=> b % w = (c - a) % v`] THEN
\r
1602 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv t2) :real^3->real^3`) THEN
\r
1603 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN
\r
1604 SUBGOAL_THEN `~collinear{vec 0,(prime:real^3->real^3) v,prime(r v)}`
\r
1606 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1607 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
1608 REWRITE_TAC[COLLINEAR_LEMMA_ALT; VECTOR_MUL_LID] THEN
\r
1611 ASM_CASES_TAC `w:real^3 = (r:real^3->real^3) v` THENL
\r
1612 [ASM_REWRITE_TAC[] THEN
\r
1613 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_1 o
\r
1614 rand o lhand o goal_concl) THEN
\r
1615 ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
\r
1616 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GT_1_2 o
\r
1617 lhand o lhand o goal_concl) THEN
\r
1618 REWRITE_TAC[SET_RULE
\r
1619 `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
\r
1621 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1622 DISCH_THEN SUBST1_TAC] THEN
\r
1623 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
\r
1624 REWRITE_TAC[TAUT `p /\ t = &1 /\ q <=> t = &1 /\ p /\ q`] THEN
\r
1625 REWRITE_TAC[REAL_ARITH `t + s = &1 <=> t = &1 - s`] THEN
\r
1626 ONCE_REWRITE_TAC[MESON[]
\r
1627 `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
\r
1628 REWRITE_TAC[UNWIND_THM2] THEN
\r
1629 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
\r
1630 REWRITE_TAC[UNWIND_THM2] THEN
\r
1631 SIMP_TAC[SET_RULE `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
\r
1632 X_GEN_TAC `p:real^3` THEN
\r
1633 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
1634 MAP_EVERY X_GEN_TAC [`t1:real`; `t2:real`] THEN STRIP_TAC THEN
\r
1635 DISCH_THEN(X_CHOOSE_THEN `t3:real` MP_TAC) THEN ASM_REWRITE_TAC[] THEN
\r
1636 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
\r
1637 REWRITE_TAC[VECTOR_ARITH
\r
1638 `a % v + b % w:real^N = c % w <=> a % v = (c - b) % w`] THEN
\r
1639 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv t1) :real^3->real^3`) THEN
\r
1640 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN
\r
1641 SUBGOAL_THEN `~collinear{vec 0,prime(r v),(prime:real^3->real^3) v}`
\r
1644 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1645 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
1646 REWRITE_TAC[COLLINEAR_LEMMA_ALT; VECTOR_MUL_LID] THEN
\r
1649 SUBST1_TAC(SET_RULE
\r
1650 `{(prime:real^3->real^3) w} = {prime w,prime w}`) THEN
\r
1651 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1652 REWRITE_TAC[SET_RULE `{w,w} SUBSET s <=> w IN s`] THEN
\r
1656 ASM_CASES_TAC `(r:real^3->real^3) w = v` THENL
\r
1658 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1659 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
\r
1660 CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
\r
1661 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1662 Local_lemmas.IVS_RHO_IDD]] THEN
\r
1663 MATCH_MP_TAC(SET_RULE
\r
1664 `!f. (!x. x IN s ==> f x = &0) /\ (!x. x IN t ==> ~(f x = &0))
\r
1665 ==> s INTER t = {}`) THEN
\r
1666 EXISTS_TAC `\p. azim (vec 0) (prime(v:real^3)) (prime (r v)) p` THEN
\r
1667 REWRITE_TAC[] THEN CONJ_TAC THENL
\r
1668 [REPEAT STRIP_TAC THEN MATCH_MP_TAC AZIM_EQ_0_GE_IMP THEN
\r
1669 MATCH_MP_TAC(SET_RULE `!s. x IN s /\ s SUBSET t ==> x IN t`) THEN
\r
1670 EXISTS_TAC `aff_gt {vec 0} {(prime:real^3->real^3) v,prime(r v)}` THEN
\r
1671 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
\r
1672 EXISTS_TAC `aff_ge {vec 0} {(prime:real^3->real^3) v,prime(r v)}` THEN
\r
1673 REWRITE_TAC[AFF_GT_SUBSET_AFF_GE] THEN REWRITE_TAC[aff_ge_def] THEN
\r
1674 MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[];
\r
1676 X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN
\r
1678 `azim (vec 0) (prime(v:real^3)) (prime (r v)) x =
\r
1679 azim (vec 0) (prime v) (prime (r v)) (prime w)`
\r
1681 [MATCH_MP_TAC AZIM_EQ_IMP THEN
\r
1682 REPEAT(CONJ_TAC THENL
\r
1683 [FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
1684 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1685 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
1687 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
\r
1688 `x IN s ==> s SUBSET t ==> x IN t`)) THEN
\r
1689 ASM_REWRITE_TAC[aff_gt_def] THEN MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN
\r
1692 SUBGOAL_THEN `w = ivs_rho_node1 FF v` SUBST1_TAC THENL
\r
1693 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1694 Local_lemmas.IVS_RHO_IDD];
\r
1695 ASM_MESON_TAC[REAL_ARITH
\r
1696 `a = pi - z /\ &0 < a /\ a < pi ==> ~(z = &0)`]];
\r
1698 SUBGOAL_THEN `local_fan(V':real^3->bool,E',FF')` ASSUME_TAC THENL
\r
1699 [ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.local_fan] THEN
\r
1700 LET_TAC THEN EXPAND_TAC "H" THEN REWRITE_TAC[Wrgcvdr_cizmrrh.dih2k] THEN
\r
1701 REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN FIRST_ASSUM
\r
1702 (fun th -> REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.HYP_LEMMA th] THEN
\r
1703 REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP th]) THEN
\r
1704 REWRITE_TAC[Wrgcvdr_cizmrrh.HYP] THEN
\r
1705 ABBREV_TAC `FF'' = { ((prime:real^3->real^3)(r v),prime v) | v IN V}` THEN
\r
1706 SUBGOAL_THEN `darts_of_hyp E' (V':real^3->bool) = FF' UNION FF''`
\r
1707 (fun th -> SUBST1_TAC th THEN ASSUME_TAC th)
\r
1709 [REWRITE_TAC[Wrgcvdr_cizmrrh.darts_of_hyp; Wrgcvdr_cizmrrh.ord_pairs;
\r
1710 Wrgcvdr_cizmrrh.self_pairs; Wrgcvdr_cizmrrh.EE] THEN
\r
1711 MATCH_MP_TAC(SET_RULE `t = {} /\ s = u ==> s UNION t = u`) THEN
\r
1713 [PURE_REWRITE_TAC[SET_RULE `s = {} <=> !x. x IN s ==> F`] THEN
\r
1714 PURE_REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1715 REWRITE_TAC[TAUT `~(p /\ q) <=> p ==> ~q`] THEN
\r
1716 EXPAND_TAC "V'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1717 EXPAND_TAC "E'" THEN ASM SET_TAC[];
\r
1718 MAP_EVERY EXPAND_TAC ["E'"; "FF'"; "FF''"] THEN
\r
1719 GEN_REWRITE_TAC I [EXTENSION] THEN
\r
1720 REWRITE_TAC[FORALL_PAIR_THM; IN_UNION; IN_ELIM_PAIR_THM] THEN
\r
1721 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
\r
1722 REWRITE_TAC[SET_RULE
\r
1723 `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
\r
1729 ==> EE (prime v) E' = {prime(r v):real^3,prime(ivs_rho_node1 FF v)}`
\r
1731 [X_GEN_TAC `v:real^3 ` THEN DISCH_TAC THEN
\r
1732 REWRITE_TAC[PAIR_EQ; Wrgcvdr_cizmrrh.EE] THEN EXPAND_TAC "E'" THEN
\r
1733 REWRITE_TAC[IN_ELIM_THM; SET_RULE
\r
1734 `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
\r
1735 REWRITE_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM] THEN
\r
1736 GEN_TAC THEN REWRITE_TAC[EXISTS_OR_THM; LEFT_OR_DISTRIB] THEN
\r
1738 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1739 Tecoxbm.RHO_IVS_IDD;
\r
1740 Local_lemmas.IVS_RHO_IDD; IVS_RHO_NODE1_IN_V];
\r
1742 SUBGOAL_THEN `!n v. v IN V ==> ITER n (r:real^3->real^3) v IN V`
\r
1744 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V];
\r
1746 SUBGOAL_THEN `!n v. v IN V ==> ITER n (ivs_rho_node1 FF) v IN V`
\r
1748 [ASM_MESON_TAC[LOCAL_FAN_ITER_IVS_RHO_NODE_IN_V];
\r
1752 ==> ITER n (ff_of_hyp (vec 0,V',E')) (prime v,prime (r v)) =
\r
1753 ((prime:real^3->real^3)(ITER n r v),prime(r(ITER n r v)))`
\r
1755 [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
\r
1756 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
\r
1757 INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN
\r
1758 ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN
\r
1759 COND_CASES_TAC THENL
\r
1760 [SUBGOAL_THEN `r(ITER n (r:real^3->real^3) v) IN V` ASSUME_TAC THENL
\r
1761 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1762 ASM_SIMP_TAC[PAIR_EQ]] THEN
\r
1763 MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN
\r
1764 MATCH_MP_TAC(SET_RULE `a = a' /\ b = b' ==> {a,b} = {b',a'}`) THEN
\r
1765 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD];
\r
1766 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT
\r
1767 `~(a \/ b) ==> a ==> c`)) THEN
\r
1768 EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
1773 ==> ITER n (ff_of_hyp (vec 0,V',E')) (prime(r v),prime v) =
\r
1774 ((prime:real^3->real^3) (r(ITER n (ivs_rho_node1 FF) v)),
\r
1775 prime(ITER n (ivs_rho_node1 FF) v))`
\r
1777 [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
\r
1778 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
\r
1779 INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN
\r
1780 ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN
\r
1781 COND_CASES_TAC THENL
\r
1782 [ASM_SIMP_TAC[PAIR_EQ] THEN
\r
1783 CONJ_TAC THENL [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD]; ALL_TAC] THEN
\r
1784 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
\r
1785 MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN
\r
1786 ASM_SIMP_TAC[PAIR_EQ] THEN REWRITE_TAC[INSERT_AC];
\r
1787 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT
\r
1788 `~(a \/ b) ==> b ==> c`)) THEN
\r
1789 EXPAND_TAC "FF''" THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
1793 `!x. x IN FF' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF'`
\r
1795 [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1796 X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
\r
1797 REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN
\r
1798 ASM_SIMP_TAC[] THEN
\r
1800 `(!n. ITER n (r:real^3->real^3) v IN V) /\
\r
1801 (!w. w IN V ==> ?n. w = ITER n r v)`
\r
1803 [ASM_MESON_TAC[LOCAL_FAN_ORBIT_MAP_EXPLICIT];
\r
1804 REWRITE_TAC[GE; LE_0] THEN EXPAND_TAC "FF'" THEN SET_TAC[]];
\r
1807 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
1808 DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN REWRITE_TAC[IN_UNION] THEN
\r
1809 MATCH_MP_TAC(SET_RULE
\r
1810 `(?x. P x) /\ (!x. P x ==> R x) ==> ?x. (P x \/ Q x) /\ R x`) THEN
\r
1811 ASM_SIMP_TAC[] THEN EXPAND_TAC "FF'" THEN ASM SET_TAC[];
\r
1814 `CARD(FF':real^3#real^3->bool) = CARD(V:real^3->bool) /\
\r
1815 CARD(FF'':real^3#real^3->bool) = CARD V`
\r
1816 STRIP_ASSUME_TAC THENL
\r
1817 [MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
1818 REWRITE_TAC[SIMPLE_IMAGE] THEN
\r
1819 CONJ_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN
\r
1820 ASM_REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[];
\r
1823 [REWRITE_TAC[MULT_2] THEN MATCH_MP_TAC(MESON[CARD_UNION]
\r
1824 `CARD t = CARD s /\ FINITE s /\ FINITE t /\ s INTER t = {}
\r
1825 ==> CARD(s UNION t) = CARD s + CARD s`) THEN
\r
1826 ASM_REWRITE_TAC[] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
1827 REWRITE_TAC[SIMPLE_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE] THEN
\r
1828 REWRITE_TAC[SET_RULE `IMAGE f s INTER IMAGE g s = {} <=>
\r
1829 !x y. x IN s /\ y IN s ==> ~(f x = g y)`] THEN
\r
1830 REWRITE_TAC[PAIR_EQ] THEN
\r
1831 MAP_EVERY(fun th -> FIRST_ASSUM(MP_TAC o GEN_ALL o MATCH_MP
\r
1832 (REWRITE_RULE[IMP_CONJ] th)))
\r
1833 [Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1834 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE] THEN
\r
1838 `!x. x IN FF'' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF''`
\r
1840 [EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1841 X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
\r
1842 REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN
\r
1843 ASM_SIMP_TAC[] THEN
\r
1845 `(!n. ITER n (ivs_rho_node1 FF) v IN V) /\
\r
1846 (!w. w IN V ==> ?n. w = ITER n (ivs_rho_node1 FF) v)`
\r
1848 [ASM_MESON_TAC[LOCAL_FAN_ORBIT_MAP_EXPLICIT_IVS];
\r
1849 REWRITE_TAC[GE; LE_0] THEN EXPAND_TAC "FF''" THEN SET_TAC[]];
\r
1851 REWRITE_TAC[Lvducxu.HAS_ORD2_INTERPRET] THEN
\r
1853 `(!x. x IN FF' ==> nn_of_hyp (vec 0,V',E') x IN FF'') /\
\r
1854 (!x. x IN FF'' ==> nn_of_hyp (vec 0,V',E') x IN FF')`
\r
1855 STRIP_ASSUME_TAC THENL
\r
1856 [ASM_SIMP_TAC[nn_of_hyp3; FORALL_PAIR_THM; IN_UNION] THEN
\r
1857 MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
1858 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN CONJ_TAC THEN
\r
1859 REPEAT GEN_TAC THEN
\r
1860 DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THENL
\r
1861 [EXISTS_TAC `ivs_rho_node1 FF v` THEN ASM_SIMP_TAC[] THEN
\r
1862 REPEAT CONJ_TAC THENL
\r
1863 [ASM_MESON_TAC[IVS_RHO_NODE1_IN_V];
\r
1864 ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD];
\r
1865 ASM_MESON_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]];
\r
1866 EXISTS_TAC `rho_node1 FF v` THEN ASM_SIMP_TAC[] THEN
\r
1867 MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN
\r
1869 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN
\r
1870 ASM_SIMP_TAC[] THEN DISCH_TAC THEN
\r
1871 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
\r
1872 ASM_MESON_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;
\r
1873 Local_lemmas.IVS_RHO_IDD]];
\r
1875 SUBGOAL_THEN `nn_of_hyp (vec 0,V',E') o nn_of_hyp (vec 0,V',E') = I`
\r
1877 [ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN
\r
1878 MAP_EVERY X_GEN_TAC [`w:real^3`; `z:real^3`] THEN
\r
1879 ASM_CASES_TAC `(w:real^3,z:real^3) IN FF' UNION FF''` THENL
\r
1880 [ALL_TAC; ASM_REWRITE_TAC[nn_of_hyp3]] THEN
\r
1881 FIRST_X_ASSUM(DISJ_CASES_TAC o GEN_REWRITE_RULE I [IN_UNION]) THEN
\r
1882 ONCE_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2] THEN
\r
1883 ASM_SIMP_TAC[IN_UNION] THEN
\r
1884 ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2; IN_UNION; PAIR_EQ] THENL
\r
1885 [UNDISCH_TAC `(w:real^3,z:real^3) IN FF'` THEN EXPAND_TAC "FF'";
\r
1886 UNDISCH_TAC `(w:real^3,z:real^3) IN FF''` THEN EXPAND_TAC "FF''"] THEN
\r
1887 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
\r
1888 DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THEN
\r
1889 ASM_SIMP_TAC[] THEN MATCH_MP_TAC AZIM_CYCLE_TWO_POINT_SET_ALT THEN
\r
1890 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THENL
\r
1891 [SET_TAC[]; ALL_TAC] THEN
\r
1892 SUBGOAL_THEN `(r:real^3->real^3) v IN V` ASSUME_TAC THENL
\r
1893 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]; ALL_TAC] THEN
\r
1894 ASM_SIMP_TAC[] THEN
\r
1895 SUBGOAL_THEN `ivs_rho_node1 FF (r v) = v` SUBST1_TAC THENL
\r
1896 [ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD]; ALL_TAC] THEN
\r
1897 MATCH_MP_TAC(SET_RULE `a' = a ==> {a,b} = {a',b}`) THEN
\r
1898 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
\r
1899 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];
\r
1901 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
\r
1902 [REWRITE_TAC[IN_UNION; MESON[]
\r
1903 `(!x. P x \/ Q x ==> R x) <=>
\r
1904 (!x. P x ==> R x) /\ (!x. Q x ==> R x)`] THEN
\r
1905 CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN ASM_SIMP_TAC[] THEN
\r
1907 `IMAGE (nn_of_hyp (vec 0,V',E')) FF' = FF'' /\
\r
1908 IMAGE (nn_of_hyp (vec 0,V',E')) FF'' = FF'`
\r
1909 MP_TAC THENL [ALL_TAC; SET_TAC[]] THEN
\r
1910 MATCH_MP_TAC(SET_RULE
\r
1911 `(!x. f(f x) = x) /\
\r
1912 (!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> f x IN s)
\r
1913 ==> IMAGE f s = t /\ IMAGE f t = s`) THEN
\r
1914 RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM; o_THM; I_THM]) THEN
\r
1915 ASM_REWRITE_TAC[];
\r
1917 REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders] THEN CONJ_TAC THENL
\r
1919 [X_GEN_TAC `i:num` THEN STRIP_TAC THEN
\r
1920 REWRITE_TAC[FUN_EQ_THM; I_THM; NOT_FORALL_THM] THEN
\r
1921 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
1922 DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THEN
\r
1923 EXISTS_TAC `((prime:real^3->real^3) v,prime(r v))` THEN
\r
1924 ASM_SIMP_TAC[PAIR_EQ] THEN
\r
1925 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_DIS_ELMS23; ITER];
\r
1926 REWRITE_TAC[FUN_EQ_THM; I_THM] THEN
\r
1927 MATCH_MP_TAC(MESON[IN_UNION]
\r
1929 (!x. x IN FF' ==> P x) /\ (!x. x IN FF'' ==> P x) /\
\r
1930 (!x. ~(x IN FF' UNION FF'') ==> P x)
\r
1931 ==> !x. P x`) THEN
\r
1932 MAP_EVERY EXISTS_TAC
\r
1933 [`FF':real^3#real^3->bool`; `FF'':real^3#real^3->bool`] THEN
\r
1934 REPEAT CONJ_TAC THENL
\r
1935 [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1936 ASM_SIMP_TAC[PAIR_EQ] THEN
\r
1937 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID];
\r
1938 EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1939 ASM_SIMP_TAC[PAIR_EQ] THEN
\r
1940 ASM_MESON_TAC[LOFA_IMP_ITER_IVS_RHO_NODE_ID];
\r
1941 ASM_REWRITE_TAC[FORALL_PAIR_THM; ff_of_hyp3] THEN
\r
1942 REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
1943 SPEC_TAC(`CARD(V:real^3->bool)`,`k:num`) THEN
\r
1944 INDUCT_TAC THEN ASM_REWRITE_TAC[ITER]]];
\r
1946 REPEAT CONJ_TAC THENL
\r
1947 [REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN
\r
1948 MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN
\r
1949 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
\r
1950 UNDISCH_TAC `(v:real^3,w) IN darts_of_hyp E' V'` THEN
\r
1951 ASM_REWRITE_TAC[] THEN
\r
1953 `(!v w:real^3. (v,w) IN FF' ==> (w,v) IN FF'') /\
\r
1954 (!v w:real^3. (v,w) IN FF'' ==> (w,v) IN FF')`
\r
1955 MP_TAC THENL [ALL_TAC; REWRITE_TAC[IN_UNION] THEN MESON_TAC[]] THEN
\r
1956 MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
1957 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[];
\r
1958 REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; I_THM] THEN
\r
1959 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
1960 DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN
\r
1961 DISCH_THEN(MP_TAC o SPEC `(prime:real^3->real^3) v,prime(r v)`) THEN
\r
1962 ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN
\r
1963 REWRITE_TAC[IN_ELIM_THM] THEN
\r
1964 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE; PAIR_EQ;
\r
1965 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
1966 REWRITE_TAC[nn_of_hyp3; FUN_EQ_THM; I_THM] THEN
\r
1967 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
1968 DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN
\r
1969 DISCH_THEN(MP_TAC o SPEC `(prime:real^3->real^3) v,prime(r v)`) THEN
\r
1970 ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN
\r
1971 REWRITE_TAC[IN_ELIM_THM] THEN
\r
1972 COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
\r
1973 ASM_SIMP_TAC[PAIR_EQ; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN
\r
1974 ASM_MESON_TAC[IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD;
\r
1975 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
1976 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]];
\r
1978 SUBGOAL_THEN `convex_local_fan(V':real^3->bool,E',FF')` ASSUME_TAC THENL
\r
1979 [ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.convex_local_fan] THEN
\r
1980 EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
1981 SIMP_TAC[Wrgcvdr_cizmrrh.azim_in_fan; Wrgcvdr_cizmrrh.wedge_in_fan_ge] THEN
\r
1982 X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN ABBREV_TAC
\r
1983 `d = azim_cycle (EE (prime(v:real^3)) E')
\r
1984 (vec 0) (prime v) (prime (r v))` THEN
\r
1985 CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
\r
1986 SUBGOAL_THEN `CARD (EE (prime(v:real^3):real^3) E') = 2` SUBST1_TAC THENL
\r
1987 [MATCH_MP_TAC(GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1) THEN
\r
1988 MAP_EVERY EXISTS_TAC [`FF':real^3#real^3->bool`; `V':real^3->bool`] THEN
\r
1989 ASM_REWRITE_TAC[] THEN EXPAND_TAC "V'" THEN ASM SET_TAC[];
\r
1990 CONV_TAC NUM_REDUCE_CONV] THEN
\r
1991 SUBGOAL_THEN `d:real^3 = prime(ivs_rho_node1 FF v)` SUBST1_TAC THENL
\r
1992 [EXPAND_TAC "d" THEN
\r
1993 SUBGOAL_THEN `EE (prime v:real^3) E' =
\r
1994 {prime(r v),prime(ivs_rho_node1 FF v)}`
\r
1995 (fun th -> REWRITE_TAC[th; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]) THEN
\r
1996 FIRST_ASSUM(fun th -> REWRITE_TAC
\r
1997 [MATCH_MP Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE th]) THEN
\r
1998 REWRITE_TAC[Fan.set_of_edge] THEN MAP_EVERY EXPAND_TAC ["V'"; "E'"] THEN
\r
1999 REWRITE_TAC[IN_ELIM_THM; SET_RULE
\r
2000 `{w | P w /\ (?v. v IN V /\ w = prime v)} =
\r
2001 IMAGE prime {v | v IN V /\ P(prime v)}`] THEN
\r
2002 REWRITE_TAC[SET_RULE `{f a,f b} = IMAGE f {a,b}`] THEN AP_TERM_TAC THEN
\r
2003 REWRITE_TAC[RIGHT_AND_EXISTS_THM; IMAGE_CLAUSES] THEN
\r
2005 `!w z. w IN V /\ z IN V /\
\r
2006 {prime v:real^3,prime w} = {prime z,prime(r z)} <=>
\r
2007 (w:real^3) IN V /\ z IN V /\ {v,w} = {z,r z}`
\r
2008 (fun th -> REWRITE_TAC[th])
\r
2010 [REWRITE_TAC[SET_RULE
\r
2011 `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
\r
2012 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
2014 REWRITE_TAC[SET_RULE
\r
2015 `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
\r
2016 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
\r
2017 X_GEN_TAC `w:real^3` THEN ASM_CASES_TAC `(w:real^3) IN V` THENL
\r
2018 [ASM_REWRITE_TAC[];
\r
2019 ASM_MESON_TAC[IVS_RHO_NODE1_IN_V;
\r
2020 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]] THEN
\r
2021 REWRITE_TAC[MESON[] `(?v. P v /\ (x = v /\ Q v \/ R v /\ y = v)) <=>
\r
2022 P x /\ Q x \/ P y /\ R y`] THEN
\r
2023 ASM_CASES_TAC `w = (r:real^3->real^3) v` THEN ASM_REWRITE_TAC[] THEN
\r
2024 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; Tecoxbm.RHO_IVS_IDD];
\r
2027 [MATCH_MP_TAC(REAL_ARITH `&0 < x /\ x < pi ==> x <= pi`) THEN
\r
2028 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
2029 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
2030 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
\r
2031 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD];
\r
2033 EXPAND_TAC "V'" THEN REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN
\r
2034 X_GEN_TAC `w:real^3` THEN DISCH_TAC THEN
\r
2035 REWRITE_TAC[Wrgcvdr_cizmrrh.wedge_ge; IN_ELIM_THM; azim] THEN
\r
2036 ASM_CASES_TAC `(prime:real^3->real^3) w = prime v` THEN
\r
2037 ASM_REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim] THEN
\r
2038 ASM_CASES_TAC `w:real^3 = v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2039 ASM_CASES_TAC `(prime:real^3->real^3) w = prime(ivs_rho_node1 FF v)` THEN
\r
2040 ASM_REWRITE_TAC[REAL_LE_REFL] THEN
\r
2041 ASM_CASES_TAC `w = ivs_rho_node1 FF v` THENL
\r
2042 [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2043 ASM_CASES_TAC `(prime:real^3->real^3) w = prime(r(v:real^3))` THEN
\r
2044 ASM_REWRITE_TAC[AZIM_REFL; azim] THEN
\r
2045 ASM_CASES_TAC `w = (r:real^3->real^3) v` THENL
\r
2046 [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2047 MP_TAC(ISPECL [`vec 0:real^3`; `(prime:real^3->real^3) v`;
\r
2048 `prime(r(v:real^3):real^3):real^3`;
\r
2049 `(prime:real^3->real^3) w`;
\r
2050 `(prime:real^3->real^3) (ivs_rho_node1 FF v)`]
\r
2051 Fan.sum3_azim_fan) THEN
\r
2052 ANTS_TAC THENL [ALL_TAC; SIMP_TAC[REAL_LE_ADDR; azim]] THEN
\r
2055 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
2056 ASM_REWRITE_TAC[] THEN
\r
2057 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
2058 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD;
\r
2059 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]] THEN
\r
2060 MATCH_MP_TAC(REAL_ARITH
\r
2061 `(&0 < x /\ x < pi) /\ (&0 < y /\ y < pi) ==> x + y < &2 * pi`) THEN
\r
2062 ASM_SIMP_TAC[] THEN MATCH_MP_TAC SIN_POS_PI_REV THEN
\r
2063 SIMP_TAC[azim; REAL_LT_IMP_LE] THEN
\r
2064 REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
2065 ONCE_REWRITE_TAC[lemma6] THEN
\r
2066 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
2067 ABBREV_TAC `u = ivs_rho_node1 FF v` THEN
\r
2068 SUBGOAL_THEN `v = (r:real^3->real^3) u` ASSUME_TAC THENL
\r
2069 [ASM_MESON_TAC[Tecoxbm.RHO_IVS_IDD; IVS_RHO_NODE1_IN_V]; ALL_TAC] THEN
\r
2070 ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
2071 ASM_MESON_TAC[IVS_RHO_NODE1_IN_V];
\r
2073 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN
\r
2077 ==> interior_angle1 (vec 0) FF' (prime v) =
\r
2078 azim (vec 0) (prime v)
\r
2079 (prime(rho_node1 FF v)) (prime(ivs_rho_node1 FF v))`
\r
2080 (fun th -> ASM_SIMP_TAC[th]) THEN
\r
2081 REWRITE_TAC[Local_lemmas.interior_angle1; Local_lemmas.rho_node1] THEN
\r
2082 X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN EXPAND_TAC "FF'" THEN
\r
2083 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
\r
2084 MATCH_MP_TAC(MESON[]
\r
2085 `c = c' /\ d = d' ==> azim a b c d = azim a b c' d'`) THEN
\r
2086 CONJ_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN
\r
2087 ASM_REWRITE_TAC[GSYM Local_lemmas.rho_node1] THEN
\r
2088 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD;
\r
2089 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
2090 IVS_RHO_NODE1_IN_V; Tecoxbm.RHO_IVS_IDD];
\r
2092 FIRST_ASSUM(MP_TAC o MATCH_MP Wrgcvdr_cizmrrh.CIZMRRH) THEN
\r
2093 REWRITE_TAC[DE_MORGAN_THM] THEN
\r
2094 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN MP_TAC) THENL
\r
2096 DISCH_THEN(MP_TAC o GEN_ALL o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
\r
2097 Local_lemmas.KCHMAMG) o CONJUNCT1) THEN
\r
2098 DISCH_THEN(MP_TAC o SPEC `FF':(real^3#real^3)->bool`) THEN
\r
2099 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `~p ==> p /\ q ==> r`) THEN
\r
2100 EXPAND_TAC "V'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
2101 RULE_ASSUM_TAC(REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]) THEN
\r
2102 ASM_MESON_TAC[REAL_ARITH `a = pi - i /\ &0 < a /\ a < pi ==> ~(i = pi)`];
\r
2104 REWRITE_TAC[Wrgcvdr_cizmrrh.lunar; RIGHT_EXISTS_AND_THM] THEN
\r
2105 MATCH_MP_TAC(TAUT `~q ==> (p /\ q) /\ r ==> s`) THEN
\r
2106 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; RIGHT_EXISTS_AND_THM;
\r
2107 GSYM CONJ_ASSOC] THEN
\r
2108 EXPAND_TAC "V'" THEN REWRITE_TAC[EXISTS_IN_GSPEC] THEN
\r
2109 ASM_MESON_TAC[]]);;
\r
2111 (* ------------------------------------------------------------------------- *)
\r
2112 (* Perimeter and its bound of 2 pi *)
\r
2113 (* ------------------------------------------------------------------------- *)
\r
2115 let IQCPCGW = new_definition
\r
2116 `fan_perimeter(V,(E:(real^3->bool)->bool),FF) =
\r
2117 let v = @v. v IN V in
\r
2118 sum(0..CARD(FF)-1)
\r
2119 (\i. arcV (vec 0) (ITER i (rho_node1 FF) v)
\r
2120 (ITER (i+1) (rho_node1 FF) v))`;;
\r
2122 let FAN_PERIMETER_INVARIANT = prove
\r
2124 local_fan(V,E,FF) /\ v IN V
\r
2125 ==> fan_perimeter(V,E,FF) =
\r
2126 sum (0..CARD(FF)-1)
\r
2127 (\i. arcV (vec 0) (ITER i (rho_node1 FF) v)
\r
2128 (ITER (i+1) (rho_node1 FF) v))`,
\r
2130 (`!i j k. i < k /\ j < k
\r
2131 ==> (i + j) MOD k = if i + j < k then i + j else (i + j) - k`,
\r
2132 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN MATCH_MP_TAC MOD_UNIQ THENL
\r
2133 [EXISTS_TAC `0`; EXISTS_TAC `1`] THEN ASM_ARITH_TAC) in
\r
2134 REPEAT STRIP_TAC THEN REWRITE_TAC[IQCPCGW] THEN
\r
2135 FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN
\r
2136 ABBREV_TAC `w:real^3 = @v. v IN V` THEN
\r
2137 CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
\r
2138 SUBGOAL_THEN `(w:real^3) IN V` ASSUME_TAC THENL
\r
2139 [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2140 FIRST_ASSUM(MP_TAC o SPECL [`v:real^3`; `w:real^3`] o
\r
2141 MATCH_MP (REWRITE_RULE[IMP_CONJ] LOCAL_FAN_ORBIT_MAP_EXPLICIT)) THEN
\r
2142 ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `m:num`
\r
2143 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
\r
2144 MATCH_MP_TAC SUM_EQ_GENERAL THEN
\r
2145 EXISTS_TAC `\i. (i + m) MOD (CARD(V:real^3->bool))` THEN
\r
2146 REWRITE_TAC[ITER_ADD] THEN
\r
2147 FIRST_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `m < n ==> 0 < n`)) THEN
\r
2148 ABBREV_TAC `k = CARD(V:real^3->bool)` THEN
\r
2149 ASM_SIMP_TAC[IN_NUMSEG; LE_0;
\r
2150 ARITH_RULE `0 < k ==> (n <= k - 1 <=> n < k)`] THEN
\r
2151 CONJ_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THENL
\r
2152 [REWRITE_TAC[EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL
\r
2153 [EXISTS_TAC `((k - m) + i) MOD k` THEN ASM_SIMP_TAC[DIVISION; LE_1] THEN
\r
2154 MATCH_MP_TAC EQ_TRANS THEN
\r
2155 EXISTS_TAC `((k - m + i) + m) MOD k` THEN CONJ_TAC THENL
\r
2156 [FIRST_ASSUM(fun th ->
\r
2157 ONCE_REWRITE_TAC[GSYM(MATCH_MP MOD_ADD_MOD
\r
2158 (MATCH_MP (ARITH_RULE `0 < k ==> ~(k = 0)`) th))]) THEN
\r
2159 ASM_MESON_TAC[MOD_MOD_REFL; LE_1];
\r
2160 MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC];
\r
2161 MAP_EVERY X_GEN_TAC [`p:num`; `q:num`] THEN
\r
2162 DISCH_THEN(CONJUNCTS_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
2163 ASM_SIMP_TAC[lemma] THEN ASM_ARITH_TAC];
\r
2164 ASM_SIMP_TAC[DIVISION; LE_1; lemma] THEN COND_CASES_TAC THEN
\r
2165 ASM_REWRITE_TAC[ARITH_RULE `(x + 1) + y = (x + y) + 1`] THEN
\r
2166 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
\r
2167 [MATCH_MP(ARITH_RULE
\r
2168 `~(i + m:num < k) ==> i + m = ((i + m) - k) + k`) th]) THEN
\r
2169 REWRITE_TAC[ARITH_RULE `(x + k) + 1 = (x + 1) + k`] THEN
\r
2170 REWRITE_TAC[GSYM ADD1] THEN REWRITE_TAC[GSYM ITER_ADD] THEN
\r
2171 BINOP_TAC THEN AP_TERM_TAC THEN
\r
2172 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]]);;
\r
2174 let FAN_PERIMETER_INVARIANT_CARD_V = prove
\r
2176 local_fan(V,E,FF) /\ v IN V
\r
2177 ==> fan_perimeter(V,E,FF) =
\r
2178 sum (0..CARD V - 1)
\r
2179 (\i. arcV (vec 0) (ITER i (rho_node1 FF) v)
\r
2180 (ITER (i+1) (rho_node1 FF) v))`,
\r
2181 REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
2182 FIRST_ASSUM(SUBST1_TAC o MATCH_MP FAN_PERIMETER_INVARIANT) THEN
\r
2183 FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ o
\r
2187 let FAN_PERIMETER = prove
\r
2190 ==> fan_perimeter(V,E,FF) = sum V (\v. arcV (vec 0) v (rho_node1 FF v))`,
\r
2191 REPEAT STRIP_TAC THEN
\r
2192 SUBGOAL_THEN `FINITE V /\ ~(V:real^3->bool = {})`
\r
2193 (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THENL
\r
2194 [RULE_ASSUM_TAC(REWRITE_RULE
\r
2195 [Localization.local_fan2; Fan.FAN; Fan.fan1; LET_DEF; LET_END_DEF]) THEN
\r
2197 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN
\r
2198 X_GEN_TAC `v:real^3` THEN DISCH_TAC] THEN
\r
2199 FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP (REWRITE_RULE[IMP_CONJ]
\r
2200 FAN_PERIMETER_INVARIANT_CARD_V)) THEN
\r
2201 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
\r
2202 MATCH_MP_TAC SUM_EQ_GENERAL THEN
\r
2203 EXISTS_TAC `\i. ITER i (rho_node1 FF) v` THEN
\r
2204 REWRITE_TAC[GSYM ADD1; ITER] THEN CONJ_TAC THENL
\r
2205 [ALL_TAC; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]] THEN
\r
2206 X_GEN_TAC `w:real^3` THEN
\r
2207 ASM_CASES_TAC `V:real^3->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
\r
2209 SUBGOAL_THEN `~(CARD(V:real^3->bool) = 0)` ASSUME_TAC THENL
\r
2210 [ASM_SIMP_TAC[CARD_EQ_0]; ALL_TAC] THEN
\r
2211 ASM_SIMP_TAC[IN_NUMSEG; EXISTS_UNIQUE_DEF; LE_0; ARITH_RULE
\r
2212 `~(n = 0) ==> (i <= n - 1 <=> i < n)`] THEN
\r
2213 ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;
\r
2214 Local_lemmas1.POINT_PRESENTED_IN_RHOND1]);;
\r
2216 let WSEWPCH = prove
\r
2217 (`!V E FF. convex_local_fan(V,E,FF) ==> fan_perimeter(V,E,FF) <= &2 * pi`,
\r
2218 let lemma1 = prove
\r
2219 (`!u v x. x IN affine hull {vec 0,u,v} ==> orthogonal (u cross v) x`,
\r
2220 REWRITE_TAC[AFFINE_HULL_3; FORALL_IN_GSPEC; orthogonal] THEN
\r
2221 REWRITE_TAC[DOT_RADD; DOT_RMUL; DOT_RZERO; DOT_CROSS_SELF] THEN
\r
2222 REAL_ARITH_TAC) in
\r
2223 let lemma2 = prove
\r
2225 x IN affine hull {vec 0,u,v} /\ ~collinear{vec 0,u,v} /\ ~(x = vec 0)
\r
2226 ==> ~collinear{vec 0,u cross v,x}`,
\r
2227 REPEAT GEN_TAC THEN
\r
2228 MATCH_MP_TAC(TAUT `(s /\ p ==> q \/ r) ==> p /\ ~q /\ ~r ==> ~s`) THEN
\r
2229 STRIP_TAC THEN REWRITE_TAC[GSYM CROSS_EQ_0] THEN
\r
2230 REWRITE_TAC[GSYM NORM_AND_CROSS_EQ_0] THEN
\r
2231 ASM_SIMP_TAC[CROSS_EQ_0; GSYM orthogonal; lemma1])
\r
2232 and lemma3 = prove
\r
2233 (`(v cross v') cross (w cross w') =
\r
2234 ((w cross w') dot v) % v' - ((w cross w') dot v') % v`,
\r
2236 and lemma4 = prove
\r
2237 (`a % v:real^N = b % w ==> a = &0 /\ b = &0 \/ collinear{vec 0,w,v}`,
\r
2238 ASM_CASES_TAC `a = &0` THEN ASM_CASES_TAC `b = &0` THEN
\r
2239 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0; VECTOR_ARITH
\r
2240 `vec 0:real^N = a % b <=> a % b = vec 0`] THEN
\r
2241 TRY(SIMP_TAC[INSERT_AC; COLLINEAR_2] THEN NO_TAC) THEN
\r
2242 REWRITE_TAC[COLLINEAR_LEMMA] THEN
\r
2243 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a) :real^N->real^N`) THEN
\r
2244 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
\r
2246 and lemma5 = prove
\r
2247 (`(a INTER a = {} ==> f a INTER f a = z) /\
\r
2248 (!e1 e2. (e1 IN E \/ e1 IN V) /\ (e2 IN E \/ e2 IN V) /\ e1 INTER e2 = {}
\r
2249 ==> f e1 INTER f e2 = z) /\
\r
2250 (!e. (e IN E /\ e IN E' \/ e IN V) /\
\r
2251 e INTER a = {} ==> f e INTER f a = z)
\r
2252 ==> (!e. e IN E' ==> e = a \/ e IN E)
\r
2253 ==> (!e1 e2. (e1 IN E' \/ e1 IN V) /\ (e2 IN E' \/ e2 IN V) /\
\r
2255 ==> f e1 INTER f e2 = z)`,
\r
2256 STRIP_TAC THEN DISCH_THEN(fun th ->
\r
2257 MP_TAC th THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
\r
2258 DISCH_THEN(fun th' -> MP_TAC th THEN
\r
2259 MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MP_TAC th')) THEN
\r
2260 ONCE_REWRITE_TAC[IMP_IMP] THEN
\r
2261 DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN
\r
2262 ASM_MESON_TAC[INTER_COMM]) in
\r
2263 GEN_TAC THEN WF_INDUCT_TAC `CARD(V:real^3->bool)` THEN
\r
2264 RULE_ASSUM_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP]) THEN
\r
2265 REPEAT STRIP_TAC THEN FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I
\r
2266 [Wrgcvdr_cizmrrh.convex_local_fan]) THEN
\r
2267 FIRST_ASSUM(ASSUME_TAC o MATCH_MP Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN) THEN
\r
2268 FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN
\r
2269 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN
\r
2270 X_GEN_TAC `v:real^3` THEN DISCH_TAC THEN
\r
2271 FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP (REWRITE_RULE[IMP_CONJ]
\r
2272 FAN_PERIMETER_INVARIANT)) THEN
\r
2273 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
2274 FIRST_ASSUM(MP_TAC o MATCH_MP Wrgcvdr_cizmrrh.CIZMRRH) THEN
\r
2275 ASM_CASES_TAC `circular (V:real^3->bool) E` THEN ASM_REWRITE_TAC[] THENL
\r
2276 [REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM] THEN STRIP_TAC THEN
\r
2277 FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
\r
2278 Local_lemmas.KCHMAMG)) THEN
\r
2279 ASM_REWRITE_TAC[] THEN
\r
2280 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
\r
2281 DISCH_THEN(X_CHOOSE_THEN `A:real^3->bool` MP_TAC) THEN
\r
2282 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
2283 DISCH_THEN(X_CHOOSE_THEN `pl:real^3` STRIP_ASSUME_TAC) THEN
\r
2284 MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC EQ_TRANS THEN
\r
2286 `sum (0..CARD FF - 1)
\r
2287 (\i. azim (vec 0) pl (ITER i (rho_node1 FF) v)
\r
2288 (ITER (i + 1) (rho_node1 FF) v))` THEN
\r
2290 [MATCH_MP_TAC SUM_EQ_NUMSEG THEN REWRITE_TAC[GSYM ADD1; ITER] THEN
\r
2291 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V];
\r
2293 MATCH_MP_TAC ORDER_AZIM_SUM2Pi_0 THEN
\r
2294 FIRST_ASSUM(MP_TAC o MATCH_MP
\r
2295 Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR) THEN
\r
2296 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
\r
2297 [SET_RULE `{a,b,c} = {b,c,a}`] THEN
\r
2299 FIRST_ASSUM(ASSUME_TAC o MATCH_MP LOCAL_FAN_NOT_CARD_FF_GE_2) THEN
\r
2300 EXISTS_TAC `v:real^3` THEN ASM_SIMP_TAC[] THEN
\r
2301 ASM_SIMP_TAC[ARITH_RULE `2 <= f ==> 0 < f - 1 /\ (f - 1 + 1 = f)`] THEN
\r
2302 REWRITE_TAC[IN_NUMSEG; LE_0] THEN REPEAT CONJ_TAC THENL
\r
2303 [X_GEN_TAC `i:num` THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
2304 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V];
\r
2305 FIRST_ASSUM(SUBST1_TAC o
\r
2306 MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN
\r
2307 REWRITE_TAC[ITER] THEN
\r
2308 ASM_MESON_TAC[Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2];
\r
2310 `?a. &0 < a /\ pl:real^3 = a % (v cross rho_node1 FF v)`
\r
2311 STRIP_ASSUME_TAC THENL
\r
2312 [MATCH_MP_TAC CROSS_POSITIVE_MULTIPLE_AZIM_AXIS_ALT THEN
\r
2313 ASM_SIMP_TAC[orthogonal] THEN
\r
2314 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.CYCLIC_SET]) THEN
\r
2315 ASM_CASES_TAC `pl:real^3 = vec 0` THEN ASM_REWRITE_TAC[] THEN
\r
2316 DISCH_THEN(K ALL_TAC) THEN
\r
2317 REPEAT(CONJ_TAC THENL
\r
2318 [ASM_MESON_TAC[SUBSET; Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
2320 REWRITE_TAC[REAL_LT_LE; Local_lemmas1.ARCV_BOUNDS] THEN
\r
2321 DISCH_THEN(MP_TAC o AP_TERM `sin` o SYM) THEN
\r
2322 REWRITE_TAC[SIN_0] THEN
\r
2323 MATCH_MP_TAC Trigonometry2.NOT_COLLINEAR_IMP_NOT_SIN0 THEN
\r
2324 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2];
\r
2325 ASM_SIMP_TAC[AZIM_SPECIAL_SCALE]] THEN
\r
2326 ASM_SIMP_TAC[ARITH_RULE
\r
2327 `2 <= f ==> (j <= f - 1 /\ k <= f - 1 /\ j < k <=>
\r
2328 j < k /\ k < f /\ k <= f - 1)`] THEN
\r
2329 FIRST_ASSUM(SUBST1_TAC o
\r
2330 MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN
\r
2331 MATCH_MP_TAC(GEN_ALL Local_lemmas.RHO_NODE1_MONO_WITH_AZIM) THEN
\r
2332 MAP_EVERY EXISTS_TAC
\r
2333 [`E:(real^3->bool)->bool`;
\r
2334 `{ITER j (rho_node1 FF) v | j <= CARD(V:real^3->bool) - 1}`;
\r
2335 `A:real^3->bool`] THEN
\r
2336 ASM_SIMP_TAC[SUBSET; FORALL_IN_GSPEC] THEN
\r
2337 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V; SUBSET]];
\r
2339 ASM_CASES_TAC `?v w:real^3. lunar (v,w) V E` THEN ASM_REWRITE_TAC[] THENL
\r
2340 [DISCH_TAC THEN FIRST_X_ASSUM(X_CHOOSE_THEN `w:real^3` MP_TAC) THEN
\r
2341 DISCH_THEN(X_CHOOSE_TAC `z:real^3`) THEN
\r
2342 FIRST_ASSUM(MP_TAC o MATCH_MP (GEN_ALL (ONCE_REWRITE_RULE[IMP_CONJ_ALT]
\r
2343 Local_lemmas.HKIRPEP))) THEN
\r
2344 DISCH_THEN(MP_TAC o SPEC `FF:real^3#real^3->bool`) THEN
\r
2345 ASM_REWRITE_TAC[] THEN
\r
2346 REPLICATE_TAC 4 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
2347 DISCH_THEN(CONJUNCTS_THEN2
\r
2348 (X_CHOOSE_THEN `n:num` MP_TAC) (X_CHOOSE_THEN `m:num` MP_TAC)) THEN
\r
2350 (REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
2351 DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) ASSUME_TAC)) THEN
\r
2352 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
\r
2353 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Localization.lunar]) THEN
\r
2354 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN STRIP_TAC THEN
\r
2355 FIRST_ASSUM(MP_TAC o SPEC `w:real^3` o MATCH_MP
\r
2356 (ONCE_REWRITE_RULE[IMP_CONJ] FAN_PERIMETER_INVARIANT)) THEN
\r
2357 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
\r
2358 FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN
\r
2359 SUBGOAL_THEN `CARD(V:real^3->bool) = m + n` SUBST1_TAC THENL
\r
2360 [REWRITE_TAC[GSYM LE_ANTISYM] THEN CONJ_TAC THENL
\r
2361 [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ]
\r
2362 (GEN_ALL Local_lemmas1.CARD_IS_LEAST_CYCLE))) THEN
\r
2363 EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[GSYM ITER_ADD; ADD_EQ_0];
\r
2365 ONCE_REWRITE_TAC[GSYM NOT_LT] THEN DISCH_TAC THEN
\r
2366 SUBGOAL_THEN `CARD(V:real^3->bool) <= (m + n) - CARD V` MP_TAC THENL
\r
2367 [ALL_TAC; ASM_ARITH_TAC] THEN
\r
2368 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ]
\r
2369 (GEN_ALL Local_lemmas1.CARD_IS_LEAST_CYCLE))) THEN
\r
2370 EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[SUB_EQ_0; NOT_LE] THEN
\r
2371 SUBGOAL_THEN `ITER (CARD(V:real^3->bool)) (rho_node1 FF) w = w`
\r
2372 (fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SYM th])
\r
2374 [ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID]; ALL_TAC] THEN
\r
2375 ASM_SIMP_TAC[ITER_ADD; ARITH_RULE `p:num < n ==> n - p + p = n`] THEN
\r
2376 ASM_REWRITE_TAC[GSYM ITER_ADD];
\r
2378 ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> (m + n) - 1 = (n - 1) + m`] THEN
\r
2379 SIMP_TAC[SUM_ADD_SPLIT; LE_0] THEN
\r
2380 ASM_SIMP_TAC[SUB_REFL; ARITH_EQ; ARITH_RULE
\r
2381 `~(m = 0) /\ ~(n = 0) ==> m - 1 + n = m + (n - 1)`] THEN
\r
2382 REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] SUM_OFFSET] THEN
\r
2383 REWRITE_TAC[GSYM ADD_ASSOC] THEN
\r
2384 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)
\r
2385 [ONCE_REWRITE_RULE[ADD_SYM] (GSYM ITER_ADD)] THEN
\r
2386 ASM_REWRITE_TAC[] THEN
\r
2387 SUBGOAL_THEN `~(w:real^3 = vec 0) /\ ~(z:real^3 = vec 0)`
\r
2388 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[Fan.FAN; Fan.fan2]; ALL_TAC] THEN
\r
2391 ==> ITER i (rho_node1 FF) w IN
\r
2392 affine hull {vec 0,w,rho_node1 FF w}) /\
\r
2394 ==> ITER i (rho_node1 FF) z IN
\r
2395 affine hull {vec 0,w,ivs_rho_node1 FF w})`
\r
2396 STRIP_ASSUME_TAC THENL
\r
2397 [SIMP_TAC[ARITH_RULE `i <= n <=> i = 0 \/ i = n \/ 0 < i /\ i < n`] THEN
\r
2398 CONJ_TAC THEN UNDISCH_TAC `collinear {vec 0:real^3, w, z}` THEN
\r
2399 ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN DISCH_TAC THEN
\r
2400 (X_GEN_TAC `i:num` THEN STRIP_TAC THEN
\r
2401 ASM_SIMP_TAC[ITER; HULL_INC; IN_INSERT] THENL
\r
2402 [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
\r
2403 `z IN P hull s ==> P hull s SUBSET P hull t ==> z IN P hull t`)) THEN
\r
2404 MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
\r
2405 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
\r
2406 `{f i | P i} = s INTER t
\r
2407 ==> P k /\ s SUBSET s' ==> f k IN s'`)) THEN
\r
2408 ASM_REWRITE_TAC[] THEN
\r
2409 MP_TAC(GEN_ALL(ISPECL [`sgn_gt`; `u:real^3->bool`]
\r
2410 AFFSIGN_EQ_AFFINE_HULL)) THEN REWRITE_TAC[aff_gt_def] THEN
\r
2411 DISCH_THEN(fun th -> REWRITE_TAC[GSYM th]) THEN
\r
2412 MATCH_MP_TAC AFFSIGN_MONO_SHUFFLE THEN SET_TAC[]]);
\r
2414 FIRST_ASSUM(MP_TAC o MATCH_MP (GEN_ALL (ONCE_REWRITE_RULE[IMP_CONJ]
\r
2415 Local_lemmas.RHO_NODE1_MONO_WITH_AZIM))) THEN
\r
2416 DISCH_THEN(fun th ->
\r
2417 MP_TAC(SPECL [`{ITER i (rho_node1 FF) z | i <= m}`;
\r
2418 `affine hull {vec 0, w, ivs_rho_node1 FF w}`;
\r
2419 `m:num`; `z cross rho_node1 FF z`; `z:real^3`] th) THEN
\r
2420 MP_TAC(SPECL [`{ITER i (rho_node1 FF) w | i <= n}`;
\r
2421 `affine hull {vec 0, w, rho_node1 FF w}`;
\r
2422 `n:num`; `w cross rho_node1 FF w`; `w:real^3`] th)) THEN
\r
2423 ASM_REWRITE_TAC[PLANE_AFFINE_HULL_3; SUBSET; FORALL_IN_GSPEC] THEN
\r
2424 SIMP_TAC[HULL_INC; IN_INSERT] THEN ANTS_TAC THENL
\r
2425 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2];
\r
2426 DISCH_THEN(LABEL_TAC "W")] THEN
\r
2428 [ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS];
\r
2429 DISCH_THEN(LABEL_TAC "Z")] THEN
\r
2432 ==> ITER i (rho_node1 FF) z IN affine hull {vec 0,z,rho_node1 FF z}`
\r
2434 [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
\r
2435 `(!x. P x ==> f x IN s)
\r
2436 ==> P 0 /\ P(SUC 0) /\ (f 0 IN s /\ f(SUC 0) IN s ==> s = t)
\r
2437 ==> (!x. P x ==> f x IN t)`)) THEN
\r
2438 REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
\r
2439 REWRITE_TAC[ITER] THEN STRIP_TAC THEN
\r
2440 MATCH_MP_TAC AFFINE_HULL_3_GENERATED THEN
\r
2441 ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET; HULL_INC; IN_INSERT] THEN
\r
2442 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2];
\r
2446 ==> azim (vec 0) (w cross rho_node1 FF w)
\r
2447 (ITER i (rho_node1 FF) w)
\r
2448 (ITER (i + 1) (rho_node1 FF) w) =
\r
2449 azim (vec 0) (w cross rho_node1 FF w)
\r
2450 w (ITER (i + 1) (rho_node1 FF) w) -
\r
2451 azim (vec 0) (w cross rho_node1 FF w)
\r
2452 w (ITER i (rho_node1 FF) w)) /\
\r
2454 ==> azim (vec 0) (z cross rho_node1 FF z)
\r
2455 (ITER i (rho_node1 FF) z)
\r
2456 (ITER (i + 1) (rho_node1 FF) z) =
\r
2457 azim (vec 0) (z cross rho_node1 FF z)
\r
2458 z (ITER (i + 1) (rho_node1 FF) z) -
\r
2459 azim (vec 0) (z cross rho_node1 FF z)
\r
2460 z (ITER i (rho_node1 FF) z))`
\r
2461 STRIP_ASSUME_TAC THENL
\r
2463 (REWRITE_TAC[REAL_ARITH `a:real = b - c <=> b = c + a`] THEN
\r
2464 REPEAT STRIP_TAC THEN MATCH_MP_TAC Fan.sum4_azim_fan THEN
\r
2466 [MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
2468 REPEAT CONJ_TAC THEN MATCH_MP_TAC lemma2 THEN
\r
2469 ASM_SIMP_TAC[HULL_INC; IN_INSERT] THEN
\r
2472 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
\r
2474 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2];
\r
2476 MATCH_MP_TAC(MESON[]
\r
2477 `!V. ~(z IN V) /\ w IN V ==> ~(w = z)`) THEN
\r
2478 EXISTS_TAC `V:real^3->bool` THEN CONJ_TAC THENL
\r
2479 [ASM_MESON_TAC[Fan.fan2; Fan.FAN];
\r
2480 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]]) THEN
\r
2481 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]]);
\r
2483 MATCH_MP_TAC REAL_LE_TRANS THEN
\r
2486 (\i. azim (vec 0) (w cross rho_node1 FF w)
\r
2487 (ITER i (rho_node1 FF) w)
\r
2488 (ITER (i + 1) (rho_node1 FF) w)) +
\r
2490 (\i. azim (vec 0) (z cross rho_node1 FF z)
\r
2491 (ITER i (rho_node1 FF) z)
\r
2492 (ITER (i + 1) (rho_node1 FF) z))` THEN
\r
2494 [MATCH_MP_TAC REAL_EQ_IMP_LE THEN BINOP_TAC THEN
\r
2495 MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `i:num` THEN
\r
2496 STRIP_TAC THEN REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN
\r
2497 MATCH_MP_TAC AZIM_ARCV THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN
\r
2498 (REPEAT CONJ_TAC THENL
\r
2499 [MATCH_MP_TAC lemma1 THEN
\r
2500 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
2501 MATCH_MP_TAC lemma1 THEN
\r
2502 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
2503 MATCH_MP_TAC lemma2 THEN CONJ_TAC THENL
\r
2504 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
\r
2506 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2];
\r
2508 MATCH_MP_TAC(MESON[]
\r
2509 `!V. ~(z IN V) /\ w IN V ==> ~(w = z)`) THEN
\r
2510 EXISTS_TAC `V:real^3->bool` THEN CONJ_TAC THENL
\r
2511 [ASM_MESON_TAC[Fan.fan2; Fan.FAN];
\r
2512 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]];
\r
2513 MATCH_MP_TAC lemma2 THEN CONJ_TAC THENL
\r
2514 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
\r
2516 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2];
\r
2518 MATCH_MP_TAC(MESON[]
\r
2519 `!V. ~(z IN V) /\ w IN V ==> ~(w = z)`) THEN
\r
2520 EXISTS_TAC `V:real^3->bool` THEN CONJ_TAC THENL
\r
2521 [ASM_MESON_TAC[Fan.fan2; Fan.FAN];
\r
2522 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]];
\r
2524 ASM_SIMP_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
\r
2525 `&0 <= y /\ x <= pi ==> x - y <= pi`) THEN
\r
2526 REWRITE_TAC[azim] THEN MATCH_MP_TAC REAL_LE_TRANS THENL
\r
2528 `azim (vec 0) (w cross rho_node1 FF w)
\r
2529 w (ITER n (rho_node1 FF) w)`;
\r
2531 `azim (vec 0) (z cross rho_node1 FF z)
\r
2532 z (ITER m (rho_node1 FF) z)`] THEN
\r
2534 [FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
\r
2535 `i <= n - 1 ==> ~(n = 0) ==> i + 1 = n \/ i + 1 < n`)) THEN
\r
2536 ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
\r
2537 STRIP_TAC THENL [ASM_REWRITE_TAC[REAL_LE_REFL]; ALL_TAC] THEN
\r
2538 MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
2540 ASM_REWRITE_TAC[]]) THEN
\r
2541 MATCH_MP_TAC(REAL_ARITH
\r
2542 `&0 < pi /\ (x = &0 \/ x = pi) ==> x <= pi`);
\r
2543 ASM_SIMP_TAC[] THEN REWRITE_TAC[SUM_DIFFS_ALT; LE_0] THEN
\r
2544 REWRITE_TAC[ITER; AZIM_REFL] THEN
\r
2545 ASM_SIMP_TAC[SUB_ADD; LE_1; REAL_SUB_RZERO] THEN
\r
2546 MATCH_MP_TAC(REAL_ARITH
\r
2547 `&0 < pi /\ (x = &0 \/ x = pi) /\ (y = &0 \/ y = pi)
\r
2548 ==> x + y <= &2 * pi`)] THEN
\r
2549 REWRITE_TAC[PI_POS] THEN REPEAT CONJ_TAC THEN
\r
2550 MATCH_MP_TAC COLLINEAR_AZIM_0_OR_PI THEN
\r
2551 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
\r
2552 ASM_REWRITE_TAC[];
\r
2555 ASM_CASES_TAC `!v. v IN V ==> interior_angle1 (vec 0) FF v < pi` THENL
\r
2556 [SUBGOAL_THEN `?vef. vef = polar_fan(V,E,FF)` MP_TAC THENL
\r
2557 [REWRITE_TAC[EXISTS_REFL]; REWRITE_TAC[EXISTS_PAIR_THM]] THEN
\r
2558 FIRST_ASSUM(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ] BGMIFTE)) THEN
\r
2559 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
2560 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `V':real^3->bool` THEN
\r
2561 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `E':(real^3->bool)->bool` THEN
\r
2562 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `FF':real^3#real^3->bool` THEN
\r
2563 DISCH_THEN(fun th -> DISCH_THEN(ASSUME_TAC o SYM) THEN MP_TAC th) THEN
\r
2564 ASM_REWRITE_TAC[] THEN
\r
2565 REPEAT LET_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL
\r
2566 [`V':real^3->bool`; `E':(real^3->bool)->bool`; `FF':real^3#real^3->bool`]
\r
2567 Localization.NKEZBFC) THEN
\r
2568 ASM_REWRITE_TAC[] THEN
\r
2569 FIRST_ASSUM(SUBST1_TAC o
\r
2570 MATCH_MP Nkezbfc_local.SOL_LOFA_EQ_SUM_INANGLE) THEN
\r
2571 MATCH_MP_TAC(REAL_ARITH
\r
2572 `--s = t ==> &0 <= &2 * pi + s ==> t <= &2 * pi`) THEN
\r
2573 REWRITE_TAC[GSYM SUM_NEG; REAL_NEG_SUB] THEN
\r
2574 SUBGOAL_THEN `V' = IMAGE (prime:real^3->real^3) V` SUBST1_TAC THENL
\r
2575 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE LAND_CONV [JNVXCRC]) THEN
\r
2576 CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
\r
2577 ASM_REWRITE_TAC[PAIR_EQ] THEN ASM SET_TAC[];
\r
2579 W(MP_TAC o PART_MATCH (lhand o rand) SUM_IMAGE o lhand o goal_concl) THEN
\r
2582 `!x y. x IN V /\ y IN V /\ ~(x = y)
\r
2583 ==> ~collinear{vec 0,(prime:real^3->real^3) x,prime y}`
\r
2585 [ALL_TAC; ASM_MESON_TAC[INSERT_AC; COLLINEAR_2]] THEN
\r
2586 REPEAT GEN_TAC THEN STRIP_TAC THEN
\r
2587 REWRITE_TAC[GSYM CROSS_EQ_0] THEN EXPAND_TAC "prime" THEN
\r
2588 REWRITE_TAC[lemma3; VECTOR_SUB_EQ] THEN
\r
2589 DISCH_THEN(MP_TAC o MATCH_MP lemma4) THEN
\r
2590 REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THENL
\r
2592 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]] THEN
\r
2593 SUBGOAL_THEN `~(x:real^3 = r y /\ y = r x)` MP_TAC THENL
\r
2594 [EXPAND_TAC "r" THEN
\r
2595 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE];
\r
2596 REWRITE_TAC[DE_MORGAN_THM] THEN MATCH_MP_TAC MONO_OR THEN
\r
2597 CONJ_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_IMP_NZ THEN
\r
2598 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
2599 EXPAND_TAC "r" THEN MATCH_MP_TAC GENERIC_LOCAL_FAN_AZIM_POS THEN
\r
2600 MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`] THEN
\r
2601 ASM_REWRITE_TAC[] THEN EXPAND_TAC "r" THEN
\r
2602 ASM_MESON_TAC[RHO_NODE1_INJECTIVE;
\r
2603 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]];
\r
2605 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
\r
2606 MATCH_MP_TAC EQ_TRANS THEN
\r
2607 EXISTS_TAC `sum V (\v:real^3. arcV (vec 0) v (r v))` THEN CONJ_TAC THENL
\r
2608 [MATCH_MP_TAC SUM_EQ THEN ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2609 FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN
\r
2610 CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN
\r
2611 EXISTS_TAC `\i. ITER i r (v:real^3)` THEN
\r
2612 REWRITE_TAC[GSYM ADD1; ITER] THEN
\r
2613 UNDISCH_THEN `rho_node1 FF = r` (SUBST_ALL_TAC o SYM) THEN CONJ_TAC THENL
\r
2614 [ALL_TAC; ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]] THEN
\r
2615 X_GEN_TAC `w:real^3` THEN
\r
2616 ASM_CASES_TAC `V:real^3->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
\r
2618 SUBGOAL_THEN `~(CARD(V:real^3->bool) = 0)` ASSUME_TAC THENL
\r
2619 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.FAN]) THEN
\r
2620 ASM_SIMP_TAC[Fan.fan1; CARD_EQ_0];
\r
2622 ASM_SIMP_TAC[IN_NUMSEG; EXISTS_UNIQUE_DEF; LE_0; ARITH_RULE
\r
2623 `~(n = 0) ==> (i <= n - 1 <=> i < n)`] THEN
\r
2624 ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;
\r
2625 Local_lemmas1.POINT_PRESENTED_IN_RHOND1];
\r
2627 UNDISCH_THEN `(v:real^3) IN V` (K ALL_TAC) THEN
\r
2628 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
\r
2629 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN STRIP_TAC THEN
\r
2630 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
\r
2631 REWRITE_TAC[NOT_IMP] THEN
\r
2632 DISCH_THEN(X_CHOOSE_THEN `v:real^3` STRIP_ASSUME_TAC) THEN
\r
2633 FIRST_X_ASSUM(MP_TAC o MATCH_MP (REAL_ARITH
\r
2634 `~(a < pi) ==> a <= pi ==> a = pi`)) THEN
\r
2636 [ASM_MESON_TAC[Local_lemmas.CONVEX_LOFA_IMP_INANGLE_LE_PI]; DISCH_TAC] THEN
\r
2637 SUBGOAL_THEN `FINITE(V:real^3->bool)` ASSUME_TAC THENL
\r
2638 [ASM_MESON_TAC[Fan.FAN; Fan.fan1]; ALL_TAC] THEN
\r
2639 DISJ_CASES_TAC(ARITH_RULE `CARD(V:real^3->bool) <= 2 \/ 3 <= CARD V`) THENL
\r
2640 [FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP
\r
2641 (ONCE_REWRITE_RULE[IMP_CONJ] FAN_PERIMETER_INVARIANT)) THEN
\r
2642 FIRST_ASSUM(SUBST1_TAC o MATCH_MP Local_lemmas.LOFA_IMP_CARD_FF_V_EQ) THEN
\r
2643 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
\r
2644 MATCH_MP_TAC REAL_LE_TRANS THEN
\r
2645 EXISTS_TAC `sum (0..CARD(V:real^3->bool) - 1) (\i. pi)` THEN
\r
2647 [MATCH_MP_TAC SUM_LE_NUMSEG THEN
\r
2648 REWRITE_TAC[Local_lemmas1.ARCV_BOUNDS];
\r
2649 SIMP_TAC[SUM_CONST_NUMSEG; REAL_LE_RMUL_EQ; PI_POS] THEN
\r
2650 REWRITE_TAC[REAL_OF_NUM_LE] THEN ASM_ARITH_TAC];
\r
2652 ABBREV_TAC `V' = V DIFF {v:real^3}` THEN
\r
2653 ABBREV_TAC `r = \u. if rho_node1 FF u = v then rho_node1 FF v
\r
2654 else rho_node1 FF u` THEN
\r
2655 ABBREV_TAC `E' = {{v,r v} | (v:real^3) IN V'}` THEN
\r
2656 ABBREV_TAC `FF' = {(v,(r:real^3->real^3) v) | v IN V'}` THEN
\r
2657 SUBGOAL_THEN `!w:real^3. w IN V' ==> r w IN V'` ASSUME_TAC THENL
\r
2658 [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
2659 GEN_TAC THEN STRIP_TAC THEN EXPAND_TAC "r" THEN
\r
2660 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
\r
2661 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
\r
2662 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
2665 `!x y. x IN V' /\ y IN V' ==> ((r:real^3->real^3) x = r y <=> x = y)`
\r
2667 [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
2668 REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
\r
2669 EXPAND_TAC "r" THEN
\r
2670 REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
\r
2671 ASM_MESON_TAC[RHO_NODE1_INJECTIVE];
\r
2673 SUBGOAL_THEN `!w:real^3. w IN V' ==> ~(r w = w)` ASSUME_TAC THENL
\r
2674 [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
2675 GEN_TAC THEN STRIP_TAC THEN EXPAND_TAC "r" THEN
\r
2676 COND_CASES_TAC THEN
\r
2677 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
\r
2678 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
2680 SUBGOAL_THEN `!w. w IN V' ==> rho_node1 FF' w = r w` ASSUME_TAC THENL
\r
2681 [EXPAND_TAC "FF'" THEN REWRITE_TAC[Localization.rho_node1] THEN
\r
2682 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN ASM_MESON_TAC[];
\r
2684 SUBGOAL_THEN `FINITE V' /\ CARD(V':real^3->bool) + 1 = CARD(V:real^3->bool)`
\r
2685 STRIP_ASSUME_TAC THENL
\r
2686 [EXPAND_TAC "V'" THEN REWRITE_TAC[SET_RULE `s DIFF {a} = s DELETE a`] THEN
\r
2687 ASM_SIMP_TAC[FINITE_DELETE; CARD_DELETE] THEN
\r
2688 ASM_SIMP_TAC[ARITH_RULE `v - 1 + 1 = v <=> ~(v = 0)`; CARD_EQ_0] THEN
\r
2691 SUBGOAL_THEN `CARD(V':real^3->bool) < CARD(V:real^3->bool)` ASSUME_TAC THENL
\r
2692 [ASM_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
\r
2693 UNDISCH_TAC `interior_angle1 (vec 0) FF v = pi` THEN
\r
2694 FIRST_ASSUM(fun th ->
\r
2695 W(MP_TAC o PART_MATCH (lhand o rand)
\r
2696 (MATCH_MP Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS th) o
\r
2697 lhand o lhand o goal_concl)) THEN
\r
2698 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN DISCH_TAC THEN
\r
2699 SUBGOAL_THEN `v IN aff_ge {vec 0} {ivs_rho_node1 FF v, rho_node1 FF v}`
\r
2701 [MATCH_MP_TAC GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE THEN
\r
2703 [ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]; ALL_TAC] THEN
\r
2705 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2];
\r
2706 ASM_REWRITE_TAC[]] THEN
\r
2707 FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I
\r
2708 [Localization.generic]) THEN
\r
2710 [ASM_MESON_TAC[Local_lemmas1.LOCAL_RHO_NODE_PAIR_E; IN_DIFF];
\r
2711 ASM_MESON_TAC[IVS_RHO_NODE1_IN_V]];
\r
2714 `fan_perimeter (V,E,FF) =
\r
2715 sum V' (\v. arcV (vec 0) v (rho_node1 FF' v))`
\r
2718 [`V:real^3->bool`; `E:(real^3->bool)->bool`; `FF:real^3#real^3->bool`]
\r
2719 FAN_PERIMETER) THEN
\r
2720 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
\r
2721 SUBGOAL_THEN `V = (v:real^3) INSERT V'` SUBST1_TAC THENL
\r
2722 [ASM SET_TAC[]; ALL_TAC] THEN
\r
2723 ASM_SIMP_TAC[SUM_CLAUSES] THEN
\r
2724 COND_CASES_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
2725 ABBREV_TAC `u = ivs_rho_node1 FF v` THEN
\r
2726 SUBGOAL_THEN `(u:real^3) IN V'` ASSUME_TAC THENL
\r
2727 [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
2728 EXPAND_TAC "u" THEN
\r
2729 ASM_MESON_TAC[Local_lemmas1.IVS_RHO_NODE_DIFF_ID;
\r
2730 IVS_RHO_NODE1_IN_V];
\r
2732 SUBGOAL_THEN `V' = (u:real^3) INSERT (V' DELETE u)` SUBST1_TAC THENL
\r
2733 [ASM SET_TAC[]; ASM_SIMP_TAC[SUM_CLAUSES; FINITE_DELETE]] THEN
\r
2734 REWRITE_TAC[IN_DELETE] THEN MATCH_MP_TAC(REAL_ARITH
\r
2735 `s' = s /\ a + b = c
\r
2736 ==> b + a + s' = c + s`) THEN
\r
2738 [MATCH_MP_TAC SUM_EQ THEN ASM_SIMP_TAC[IN_DELETE] THEN
\r
2739 X_GEN_TAC `w:real^3` THEN STRIP_TAC THEN EXPAND_TAC "r" THEN
\r
2740 COND_CASES_TAC THEN REWRITE_TAC[] THEN
\r
2741 MAP_EVERY UNDISCH_TAC [`(u:real^3) IN V'`; `(w:real^3) IN V'`] THEN
\r
2742 EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
2743 REPEAT STRIP_TAC THEN
\r
2744 ASM_MESON_TAC[RHO_NODE1_INJECTIVE;
\r
2745 Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS];
\r
2747 EXPAND_TAC "r" THEN REWRITE_TAC[] THEN COND_CASES_TAC THENL
\r
2748 [ALL_TAC; ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]] THEN
\r
2749 ASM_REWRITE_TAC[] THEN
\r
2750 REWRITE_TAC[ARCV_ANGLE] THEN MATCH_MP_TAC ANGLES_ADD_AFF_GE THEN
\r
2751 REPEAT(CONJ_TAC THENL
\r
2752 [RULE_ASSUM_TAC(REWRITE_RULE[Fan.fan2; Fan.FAN]) THEN
\r
2753 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; IN_DIFF];
\r
2757 DISJ_CASES_TAC(ARITH_RULE `CARD(V':real^3->bool) <= 2 \/ 3 <= CARD V'`) THENL
\r
2758 [MATCH_MP_TAC REAL_LE_TRANS THEN
\r
2759 EXISTS_TAC `sum (V':real^3->bool) (\i. pi)` THEN CONJ_TAC THENL
\r
2760 [MATCH_MP_TAC SUM_LE THEN ASM_SIMP_TAC[Local_lemmas1.ARCV_BOUNDS];
\r
2761 ASM_SIMP_TAC[SUM_CONST; REAL_LE_RMUL_EQ; PI_POS] THEN
\r
2762 REWRITE_TAC[REAL_OF_NUM_LE] THEN ASM_ARITH_TAC];
\r
2764 SUBGOAL_THEN `convex_local_fan (V',E',FF')` ASSUME_TAC THENL
\r
2767 [`V':real^3->bool`; `E':(real^3->bool)->bool`; `FF':real^3#real^3->bool`]
\r
2768 FAN_PERIMETER) THEN
\r
2769 ASM_SIMP_TAC[Local_lemmas.CVX_LO_IMP_LO] THEN
\r
2770 DISCH_THEN(SUBST1_TAC o SYM) THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
2771 ASM_REWRITE_TAC[]] THEN
\r
2772 FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `3 <= n ==> ~(n = 0)`)) THEN
\r
2773 ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_TAC THEN
\r
2774 SUBGOAL_THEN `~((vec 0:real^3) IN V')` ASSUME_TAC THENL
\r
2775 [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF] THEN
\r
2776 ASM_MESON_TAC[Fan.FAN; Fan.fan2];
\r
2778 SUBGOAL_THEN `FAN(vec 0:real^3,V',E')` ASSUME_TAC THENL
\r
2779 [REWRITE_TAC[FAN_ECONOMIZED_SIMPLE] THEN REPEAT CONJ_TAC THENL
\r
2780 [EXPAND_TAC "E'" THEN REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN
\r
2781 ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET];
\r
2782 EXPAND_TAC "E'" THEN REWRITE_TAC[Fan.GRAPH; FORALL_IN_GSPEC] THEN
\r
2783 ASM_SIMP_TAC[Local_lemmas1.SET2_HAS_SIZE2];
\r
2784 REWRITE_TAC[Fan.fan1] THEN ASM SET_TAC[];
\r
2785 ASM_REWRITE_TAC[Fan.fan2];
\r
2786 EXPAND_TAC "E'" THEN REWRITE_TAC[Fan.fan6; FORALL_IN_GSPEC] THEN
\r
2787 X_GEN_TAC `u:real^3` THEN REWRITE_TAC[INSERT_UNION_EQ; UNION_EMPTY] THEN
\r
2788 EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN STRIP_TAC THEN
\r
2789 EXPAND_TAC "r" THEN COND_CASES_TAC THENL
\r
2791 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]] THEN
\r
2793 FIRST_ASSUM(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ]
\r
2794 (GEN_ALL Local_lemmas.FAN_SUB_NOT_EQ_COLL_IN_CONV0))) THEN
\r
2795 DISCH_THEN(MP_TAC o SPECL [`u:real^3`; `rho_node1 FF v`]) THEN
\r
2796 ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; NOT_IMP] THEN
\r
2798 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
\r
2799 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
2801 REWRITE_TAC[Collect_geom.CONV0_SET2; IN_ELIM_THM] THEN
\r
2802 FIRST_X_ASSUM(MP_TAC o
\r
2803 SPECL [`v:real^3`; `rho_node1 FF v`; `u:real^3`] o
\r
2804 GEN_REWRITE_RULE I [Localization.generic]) THEN
\r
2806 [ASM_MESON_TAC[Local_lemmas1.LOCAL_RHO_NODE_PAIR_E]; ALL_TAC] THEN
\r
2807 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
\r
2808 REWRITE_TAC[LEFT_IMP_EXISTS_THM; GSYM MEMBER_NOT_EMPTY] THEN
\r
2809 MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
\r
2810 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
\r
2811 DISCH_THEN(ASSUME_TAC o SYM) THEN
\r
2813 `~(u:real^3 = vec 0) /\ ~(v = vec 0) /\ ~(rho_node1 FF v = vec 0)`
\r
2814 STRIP_ASSUME_TAC THENL
\r
2815 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [Fan.FAN]) THEN
\r
2816 REWRITE_TAC[Fan.fan2] THEN
\r
2817 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
2818 ASM_SIMP_TAC[AFF_GE_1_2_0; IN_INTER; EXISTS_IN_GSPEC] THEN
\r
2819 MAP_EVERY EXISTS_TAC [`&0`; `b:real`] THEN
\r
2820 ASM_SIMP_TAC[REAL_LE_REFL; REAL_LT_IMP_LE] THEN
\r
2821 ASM_SIMP_TAC[AFF_LT_1_1; SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
\r
2822 REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_RZERO; IN_ELIM_THM] THEN
\r
2823 MAP_EVERY EXISTS_TAC [`&1 + a`; `--a`] THEN
\r
2824 REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
\r
2825 ASM_REWRITE_TAC[VECTOR_ARITH
\r
2826 `vec 0 + a:real^N = vec 0 + --x % b <=> x % b + a = vec 0`]];
\r
2828 `E' SUBSET {ivs_rho_node1 FF v,rho_node1 FF v} INSERT E`
\r
2830 [EXPAND_TAC "E'" THEN REWRITE_TAC[FORALL_IN_GSPEC; SUBSET] THEN
\r
2831 X_GEN_TAC `w:real^3` THEN EXPAND_TAC "V'" THEN
\r
2832 REWRITE_TAC[IN_DIFF; IN_SING] THEN STRIP_TAC THEN
\r
2833 REWRITE_TAC[IN_INSERT] THEN
\r
2834 EXPAND_TAC "r" THEN COND_CASES_TAC THENL
\r
2835 [DISJ1_TAC THEN BINOP_TAC THEN REWRITE_TAC[] THEN
\r
2836 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD];
\r
2837 DISJ2_TAC THEN ASM_MESON_TAC[Local_lemmas1.LOCAL_RHO_NODE_PAIR_E]];
\r
2838 REWRITE_TAC[SUBSET; IN_INSERT; IN_UNION]] THEN
\r
2839 MATCH_MP_TAC lemma5 THEN CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
\r
2841 [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FAN_ECONOMIZED_SIMPLE]) THEN
\r
2842 DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN EXPAND_TAC "V'" THEN
\r
2845 X_GEN_TAC `e:real^3->bool` THEN
\r
2846 SIMP_TAC[SET_RULE `s INTER {a,b} = {} <=> ~(a IN s) /\ ~(b IN s)`] THEN
\r
2848 `aff_ge {vec 0} {ivs_rho_node1 FF v, rho_node1 FF v} =
\r
2849 aff_ge {vec 0} {ivs_rho_node1 FF v, v} UNION
\r
2850 aff_ge {vec 0} {v, rho_node1 FF v}`
\r
2852 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC UNION_AFF_GE_1_2 THEN
\r
2853 ASM_REWRITE_TAC[] THEN
\r
2854 RULE_ASSUM_TAC(REWRITE_RULE[Fan.fan2; Fan.FAN]) THEN
\r
2855 ASM_MESON_TAC[IVS_RHO_NODE1_IN_V;
\r
2856 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
\r
2858 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
\r
2859 MATCH_MP_TAC(SET_RULE
\r
2860 `s INTER t = u /\ s INTER t' = u ==> s INTER (t UNION t') = u`) THEN
\r
2861 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FAN_ECONOMIZED_SIMPLE]) THEN
\r
2862 DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN
\r
2863 DISCH_THEN(fun th -> CONJ_TAC THEN MATCH_MP_TAC th) THEN
\r
2864 (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
\r
2865 ASM_REWRITE_TAC[SET_RULE
\r
2866 `s INTER {a,b} = {} <=> ~(a IN s) /\ ~(b IN s)`] THEN
\r
2868 [REWRITE_TAC[IN_UNION] THEN DISJ1_TAC THEN
\r
2869 ASM_MESON_TAC[Tecoxbm.IVS_RHO_NODE_IN_EDGE;
\r
2870 Local_lemmas1.LOCAL_RHO_NODE_PAIR_E;
\r
2871 SET_RULE `{a,b} = {b,a}`];
\r
2873 FIRST_X_ASSUM(DISJ_CASES_THEN MP_TAC) THEN
\r
2874 SIMP_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
2875 EXPAND_TAC "V'" THEN SIMP_TAC[IN_SING; IN_DIFF] THEN
\r
2876 EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
2877 EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
2878 STRIP_TAC THEN ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
\r
2879 EXPAND_TAC "r" THEN COND_CASES_TAC THEN
\r
2880 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE]];
\r
2882 MP_TAC(ISPECL [`V':real^3->bool`; `r:real^3->real^3`]
\r
2883 SURJECTIVE_IFF_INJECTIVE) THEN
\r
2884 ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
2885 DISCH_THEN(MP_TAC o snd o EQ_IMP_RULE) THEN
\r
2886 ANTS_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[RIGHT_IMP_EXISTS_THM]] THEN
\r
2887 REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
2888 X_GEN_TAC `r':real^3->real^3` THEN
\r
2889 REWRITE_TAC[TAUT `p ==> q /\ r <=> (p ==> q) /\ (p ==> r)`] THEN
\r
2890 REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN
\r
2892 `!x y. x IN V' /\ y IN V' ==> ((r':real^3->real^3) x = r' y <=> x = y)`
\r
2893 ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2895 `!x. x IN V' ==> (r':real^3->real^3)(r x) = x`
\r
2896 ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2897 SUBGOAL_THEN `local_fan(V':real^3->bool,E',FF')` ASSUME_TAC THENL
\r
2898 [ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.local_fan] THEN
\r
2899 LET_TAC THEN EXPAND_TAC "H" THEN REWRITE_TAC[Wrgcvdr_cizmrrh.dih2k] THEN
\r
2900 REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN FIRST_ASSUM
\r
2901 (fun th -> REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.HYP_LEMMA th] THEN
\r
2902 REWRITE_TAC[MATCH_MP Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP th]) THEN
\r
2903 REWRITE_TAC[Wrgcvdr_cizmrrh.HYP] THEN
\r
2904 ABBREV_TAC `FF'' = { ((r:real^3->real^3) v,v) | v IN V'}` THEN
\r
2905 SUBGOAL_THEN `darts_of_hyp E' (V':real^3->bool) = FF' UNION FF''`
\r
2906 (fun th -> SUBST1_TAC th THEN ASSUME_TAC th)
\r
2908 [REWRITE_TAC[Wrgcvdr_cizmrrh.darts_of_hyp; Wrgcvdr_cizmrrh.ord_pairs;
\r
2909 Wrgcvdr_cizmrrh.self_pairs; Wrgcvdr_cizmrrh.EE] THEN
\r
2910 MATCH_MP_TAC(SET_RULE `t = {} /\ s = u ==> s UNION t = u`) THEN
\r
2912 [PURE_REWRITE_TAC[SET_RULE `s = {} <=> !x. x IN s ==> F`] THEN
\r
2913 PURE_REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
2914 X_GEN_TAC `w:real^3` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
\r
2915 (MP_TAC o SPEC `(r:real^3->real^3) w`)) THEN
\r
2916 EXPAND_TAC "E'" THEN ASM SET_TAC[];
\r
2917 EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
2918 REWRITE_TAC[SET_RULE
\r
2919 `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
\r
2920 MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN SET_TAC[]];
\r
2921 ASM_REWRITE_TAC[]] THEN
\r
2923 `!w:real^3. w IN V' ==> EE w E' = {r w,(r':real^3->real^3) w}`
\r
2925 [X_GEN_TAC `w:real^3 ` THEN DISCH_TAC THEN
\r
2926 REWRITE_TAC[PAIR_EQ; Wrgcvdr_cizmrrh.EE] THEN EXPAND_TAC "E'" THEN
\r
2927 REWRITE_TAC[IN_ELIM_THM; SET_RULE
\r
2928 `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
\r
2931 SUBGOAL_THEN `!n w. w IN V' ==> ITER n (r:real^3->real^3) w IN V'`
\r
2933 [INDUCT_TAC THEN REWRITE_TAC[ITER] THEN ASM SET_TAC[]; ALL_TAC] THEN
\r
2934 SUBGOAL_THEN `!n w. w IN V' ==> ITER n (r':real^3->real^3) w IN V'`
\r
2936 [INDUCT_TAC THEN REWRITE_TAC[ITER] THEN ASM SET_TAC[]; ALL_TAC] THEN
\r
2939 ==> ITER n (ff_of_hyp (vec 0,V',E')) (w,r w) =
\r
2940 (ITER n r w,r(ITER n r w))`
\r
2942 [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
\r
2943 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
\r
2944 INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN
\r
2945 ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN
\r
2946 COND_CASES_TAC THENL
\r
2947 [SUBGOAL_THEN `r(ITER n (r:real^3->real^3) w) IN V'` ASSUME_TAC THENL
\r
2948 [ASM_MESON_TAC[]; ALL_TAC] THEN
\r
2949 AP_TERM_TAC THEN MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN
\r
2950 ASM_SIMP_TAC[] THEN
\r
2951 MATCH_MP_TAC(SET_RULE `a = a' /\ b = b' ==> {a,b} = {b',a'}`) THEN
\r
2953 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT
\r
2954 `~(a \/ b) ==> a ==> c`)) THEN
\r
2955 EXPAND_TAC "FF'" THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
2960 ==> ITER n (ff_of_hyp (vec 0,V',E')) (r w,w) =
\r
2961 r(ITER n r' w),ITER n r' w`
\r
2963 [ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
\r
2964 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
\r
2965 INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN
\r
2966 ASM_REWRITE_TAC[ff_of_hyp3; IN_UNION] THEN
\r
2967 COND_CASES_TAC THENL
\r
2968 [SUBGOAL_THEN `(r:real^3->real^3)
\r
2969 (ITER n (r':real^3->real^3) w) IN V'` ASSUME_TAC THENL
\r
2970 [ASM_MESON_TAC[]; ASM_SIMP_TAC[]] THEN
\r
2971 AP_TERM_TAC THEN MATCH_MP_TAC IVS_AZIM_CYCLE_TWO_POINT_SET_ALT THEN
\r
2972 ASM_SIMP_TAC[] THEN
\r
2973 MATCH_MP_TAC(SET_RULE `a = a' /\ b = b' ==> {a,b} = {b',a'}`) THEN
\r
2975 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT
\r
2976 `~(a \/ b) ==> b ==> c`)) THEN
\r
2977 EXPAND_TAC "FF''" THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
2981 `(!x:real^3 k. x IN V' /\ 0 < k /\ k < CARD V' ==> ~(ITER k r x = x)) /\
\r
2983 x IN V' /\ y IN V' ==> ?i. i < CARD V' /\ y = ITER i r x) /\
\r
2984 (!x. x IN V' ==> ITER (CARD V') r x = x) /\
\r
2985 (!x. x IN V' ==> ITER (CARD V') r' x = x)`
\r
2988 `!k. k < CARD(V':real^3->bool)
\r
2989 ==> ITER k r (rho_node1 FF v) = ITER (k + 1) (rho_node1 FF) v`
\r
2991 [REWRITE_TAC[GSYM ITER_ADD; num_CONV `1`; ITER] THEN
\r
2992 MATCH_MP_TAC num_INDUCTION THEN
\r
2993 SIMP_TAC[ITER; ARITH_RULE `SUC k < n ==> k < n`] THEN
\r
2994 X_GEN_TAC `i:num` THEN DISCH_THEN(K ALL_TAC) THEN DISCH_TAC THEN
\r
2995 EXPAND_TAC "r" THEN
\r
2996 REWRITE_TAC[GSYM(CONJUNCT2 ITER); GSYM(CONJUNCT2 ITER_ALT)] THEN
\r
2997 COND_CASES_TAC THEN REWRITE_TAC[] THEN
\r
2998 FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
\r
2999 `SUC i < V ==> ~(V + 1 <= SUC(SUC i))`)) THEN
\r
3000 MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN ASM_REWRITE_TAC[] THEN
\r
3001 ASM_MESON_TAC[Local_lemmas1.CARD_IS_LEAST_CYCLE; NOT_SUC];
\r
3004 `ITER (CARD(V':real^3->bool)) r (rho_node1 FF v) = rho_node1 FF v`
\r
3006 [FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
\r
3007 `3 <= n ==> n = SUC(n - 1)`)) THEN
\r
3008 ASM_SIMP_TAC[ITER;
\r
3009 ARITH_RULE `3 <= n ==> n - 1 < n /\ n - 1 + 1 = n`] THEN
\r
3010 EXPAND_TAC "r" THEN REWRITE_TAC[GSYM(CONJUNCT2 ITER)] THEN
\r
3011 ASM_REWRITE_TAC[ADD1] THEN
\r
3012 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID];
\r
3015 `!x. x IN V' ==> ?k. k < CARD V' /\ ITER k r (rho_node1 FF v) = x`
\r
3016 (LABEL_TAC "Reach") THENL
\r
3017 [EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
3018 X_GEN_TAC `x:real^3` THEN STRIP_TAC THEN
\r
3019 MP_TAC(ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`;
\r
3020 `FF:real^3#real^3->bool`; `rho_node1 FF v`; `x:real^3`]
\r
3021 LOCAL_FAN_ORBIT_MAP_EXPLICIT) THEN
\r
3022 EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
3023 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
\r
3024 [ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
3025 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
3026 MATCH_MP_TAC MONO_EXISTS] THEN
\r
3027 X_GEN_TAC `i:num` THEN FIRST_ASSUM(fun th ->
\r
3028 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [SYM th]) THEN
\r
3029 REWRITE_TAC[ARITH_RULE `i < v + 1 <=> i < v \/ i = v`] THEN
\r
3030 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
\r
3031 ASM_SIMP_TAC[GSYM ITER_ADD; num_CONV `1`; ITER] THEN
\r
3032 ASM_REWRITE_TAC[GSYM(CONJUNCT2 ITER_ALT); ADD1] THEN
\r
3033 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID];
\r
3035 MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
\r
3036 [MAP_EVERY X_GEN_TAC [`x:real^3`; `i:num`] THEN STRIP_TAC THEN
\r
3037 REMOVE_THEN "Reach" (MP_TAC o SPEC `x:real^3`) THEN
\r
3038 ASM_REWRITE_TAC[] THEN
\r
3039 DISCH_THEN(X_CHOOSE_THEN `j:num` (STRIP_ASSUME_TAC o GSYM)) THEN
\r
3040 ASM_REWRITE_TAC[ITER_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
\r
3041 REWRITE_TAC[GSYM ITER_ADD] THEN
\r
3044 x IN V' /\ y IN V' /\ ~(x = y)
\r
3045 ==> ~(ITER j r x = ITER j r y)`
\r
3046 MATCH_MP_TAC THENL
\r
3047 [INDUCT_TAC THEN REWRITE_TAC[ITER] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
\r
3048 REPEAT CONJ_TAC THENL
\r
3049 [FIRST_X_ASSUM MATCH_MP_TAC;
\r
3051 ASM_SIMP_TAC[GSYM ITER_ADD; num_CONV `1`; ITER] THEN
\r
3052 DISCH_TAC THEN UNDISCH_TAC `i < CARD(V':real^3->bool)` THEN
\r
3053 MATCH_MP_TAC(ARITH_RULE `V + 1 <= i ==> i < V ==> F`) THEN
\r
3054 ASM_REWRITE_TAC[] THEN
\r
3055 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ]
\r
3056 (GEN_ALL Local_lemmas1.CARD_IS_LEAST_CYCLE))) THEN
\r
3057 EXISTS_TAC `rho_node1 FF v` THEN ASM_SIMP_TAC[LE_1]] THEN
\r
3058 EXPAND_TAC "V'" THEN REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
3059 ASM_MESON_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
\r
3060 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE];
\r
3061 DISCH_THEN(LABEL_TAC "Rdistinct")] THEN
\r
3063 [REPEAT STRIP_TAC THEN MP_TAC(ISPECL
\r
3064 [`IMAGE (\i. ITER i r (x:real^3)) {i | i < CARD(V':real^3->bool)}`;
\r
3065 `V':real^3->bool`] SUBSET_CARD_EQ) THEN
\r
3066 ASM_SIMP_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
\r
3067 MATCH_MP_TAC(TAUT `(q ==> r) /\ p ==> (p <=> q) ==> r`) THEN
\r
3068 CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
3069 GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_LT] THEN
\r
3070 MATCH_MP_TAC CARD_IMAGE_INJ THEN REWRITE_TAC[FINITE_NUMSEG_LT] THEN
\r
3071 MATCH_MP_TAC WLOG_LT THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
3072 CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
\r
3073 MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN REPEAT STRIP_TAC THEN
\r
3074 REMOVE_THEN "Rdistinct"
\r
3075 (MP_TAC o SPECL [`ITER i (r:real^3->real^3) x`; `j - i:num`]) THEN
\r
3076 ASM_SIMP_TAC[ITER_ADD; LT_IMP_LE; SUB_ADD] THEN ASM_ARITH_TAC;
\r
3078 MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
\r
3079 [X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN
\r
3080 REMOVE_THEN "Reach" (MP_TAC o SPEC `x:real^3`) THEN
\r
3081 ASM_REWRITE_TAC[] THEN
\r
3082 DISCH_THEN(X_CHOOSE_THEN `j:num` (STRIP_ASSUME_TAC o GSYM)) THEN
\r
3083 ASM_REWRITE_TAC[ITER_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
\r
3084 REWRITE_TAC[GSYM ITER_ADD] THEN ASM_MESON_TAC[];
\r
3086 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:real^3` THEN
\r
3087 DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
\r
3088 ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM o AP_TERM
\r
3089 `ITER (CARD(V':real^3->bool)) (r':real^3->real^3)`) THEN
\r
3090 SPEC_TAC(`CARD(V':real^3->bool)`,`j:num`) THEN
\r
3091 INDUCT_TAC THEN ONCE_REWRITE_TAC[ITER_ALT] THEN ASM_SIMP_TAC[ITER];
\r
3092 DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "Rdistinct") MP_TAC) THEN
\r
3093 DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "Rorbit") STRIP_ASSUME_TAC)] THEN
\r
3095 `!x. x IN FF' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF'`
\r
3097 [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
3098 X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN
\r
3099 REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN
\r
3100 ASM_SIMP_TAC[GE; LE_0] THEN EXPAND_TAC "FF'" THEN ASM SET_TAC[];
\r
3103 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
3104 DISCH_THEN(X_CHOOSE_TAC `w:real^3`) THEN REWRITE_TAC[IN_UNION] THEN
\r
3105 MATCH_MP_TAC(SET_RULE
\r
3106 `(?x. P x) /\ (!x. P x ==> R x) ==> ?x. (P x \/ Q x) /\ R x`) THEN
\r
3107 ASM_SIMP_TAC[] THEN EXPAND_TAC "FF'" THEN ASM SET_TAC[];
\r
3110 `CARD(FF':real^3#real^3->bool) = CARD(V':real^3->bool) /\
\r
3111 CARD(FF'':real^3#real^3->bool) = CARD V'`
\r
3112 STRIP_ASSUME_TAC THENL
\r
3113 [MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
3114 REWRITE_TAC[SIMPLE_IMAGE] THEN
\r
3115 CONJ_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN
\r
3116 ASM_REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[];
\r
3119 [REWRITE_TAC[MULT_2] THEN MATCH_MP_TAC(MESON[CARD_UNION]
\r
3120 `CARD t = CARD s /\ FINITE s /\ FINITE t /\ s INTER t = {}
\r
3121 ==> CARD(s UNION t) = CARD s + CARD s`) THEN
\r
3122 ASM_REWRITE_TAC[] THEN MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
3123 REWRITE_TAC[SIMPLE_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE] THEN
\r
3124 REWRITE_TAC[SET_RULE `IMAGE f s INTER IMAGE g s = {} <=>
\r
3125 !x y. x IN s /\ y IN s ==> ~(f x = g y)`] THEN
\r
3126 REWRITE_TAC[PAIR_EQ] THEN
\r
3127 MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN STRIP_TAC THEN
\r
3128 REMOVE_THEN "Rdistinct" (MP_TAC o SPECL [`x:real^3`; `SUC(SUC 0)`]) THEN
\r
3129 ASM_SIMP_TAC[ITER; ARITH; ARITH_RULE `3 <= V ==> SUC(SUC 0) < V`] THEN
\r
3133 `!x. x IN FF'' ==> orbit_map (ff_of_hyp (vec 0,V',E')) x = FF''`
\r
3135 [EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
3136 X_GEN_TAC `x:real^3` THEN DISCH_TAC THEN
\r
3137 REWRITE_TAC[Hypermap.orbit_map; Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN
\r
3138 ASM_SIMP_TAC[GE; LE_0] THEN EXPAND_TAC "FF''" THEN
\r
3139 SUBGOAL_THEN `!y:real^3. y IN V' ==> ?i. ITER i r' x = y` MP_TAC THENL
\r
3140 [ALL_TAC; ASM SET_TAC[]] THEN
\r
3141 X_GEN_TAC `y:real^3` THEN DISCH_TAC THEN
\r
3142 REMOVE_THEN "Rorbit" (MP_TAC o SPECL [`y:real^3`; `x:real^3`]) THEN
\r
3143 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
\r
3144 X_GEN_TAC `i:num` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
3145 SPEC_TAC(`i:num`,`j:num`) THEN
\r
3146 INDUCT_TAC THEN ONCE_REWRITE_TAC[ITER_ALT] THEN ASM_SIMP_TAC[ITER];
\r
3148 REWRITE_TAC[Lvducxu.HAS_ORD2_INTERPRET] THEN
\r
3150 `(!x. x IN FF' ==> nn_of_hyp (vec 0,V',E') x IN FF'') /\
\r
3151 (!x. x IN FF'' ==> nn_of_hyp (vec 0,V',E') x IN FF')`
\r
3152 STRIP_ASSUME_TAC THENL
\r
3153 [ASM_SIMP_TAC[nn_of_hyp3; FORALL_PAIR_THM; IN_UNION] THEN
\r
3154 MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
3155 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN CONJ_TAC THEN
\r
3156 REPEAT GEN_TAC THEN
\r
3157 DISCH_THEN(X_CHOOSE_THEN `w:real^3` STRIP_ASSUME_TAC) THENL
\r
3158 [EXISTS_TAC `(r':real^3->real^3) w` THEN ASM_SIMP_TAC[] THEN
\r
3159 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];
\r
3160 EXISTS_TAC `(r:real^3->real^3) w` THEN ASM_SIMP_TAC[] THEN
\r
3161 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
\r
3162 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]];
\r
3164 SUBGOAL_THEN `nn_of_hyp (vec 0,V',E') o nn_of_hyp (vec 0,V',E') = I`
\r
3166 [ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN
\r
3167 MAP_EVERY X_GEN_TAC [`w:real^3`; `z:real^3`] THEN
\r
3168 ASM_CASES_TAC `(w:real^3,z:real^3) IN FF' UNION FF''` THENL
\r
3169 [ALL_TAC; ASM_REWRITE_TAC[nn_of_hyp3]] THEN
\r
3170 FIRST_X_ASSUM(DISJ_CASES_TAC o GEN_REWRITE_RULE I [IN_UNION]) THEN
\r
3171 ONCE_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2] THEN
\r
3172 ASM_SIMP_TAC[IN_UNION] THEN
\r
3173 ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2; IN_UNION; PAIR_EQ] THENL
\r
3174 [UNDISCH_TAC `(w:real^3,z:real^3) IN FF'` THEN EXPAND_TAC "FF'";
\r
3175 UNDISCH_TAC `(w:real^3,z:real^3) IN FF''` THEN EXPAND_TAC "FF''"] THEN
\r
3176 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
\r
3177 DISCH_THEN(X_CHOOSE_THEN `y:real^3` STRIP_ASSUME_TAC) THEN
\r
3178 ASM_SIMP_TAC[] THEN MATCH_MP_TAC AZIM_CYCLE_TWO_POINT_SET_ALT THEN
\r
3179 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THENL
\r
3180 [SET_TAC[]; ALL_TAC] THEN
\r
3182 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
\r
3183 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];
\r
3185 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
\r
3186 [REWRITE_TAC[IN_UNION; MESON[]
\r
3187 `(!x. P x \/ Q x ==> R x) <=>
\r
3188 (!x. P x ==> R x) /\ (!x. Q x ==> R x)`] THEN
\r
3189 CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN ASM_SIMP_TAC[] THEN
\r
3191 `IMAGE (nn_of_hyp (vec 0,V',E')) FF' = FF'' /\
\r
3192 IMAGE (nn_of_hyp (vec 0,V',E')) FF'' = FF'`
\r
3193 MP_TAC THENL [ALL_TAC; SET_TAC[]] THEN
\r
3194 MATCH_MP_TAC(SET_RULE
\r
3195 `(!x. f(f x) = x) /\
\r
3196 (!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> f x IN s)
\r
3197 ==> IMAGE f s = t /\ IMAGE f t = s`) THEN
\r
3198 RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM; o_THM; I_THM]) THEN
\r
3199 ASM_REWRITE_TAC[];
\r
3201 REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders] THEN CONJ_TAC THENL
\r
3203 [X_GEN_TAC `i:num` THEN STRIP_TAC THEN
\r
3204 REWRITE_TAC[FUN_EQ_THM; I_THM; NOT_FORALL_THM] THEN
\r
3205 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
3206 DISCH_THEN(X_CHOOSE_THEN `w:real^3` STRIP_ASSUME_TAC) THEN
\r
3207 EXISTS_TAC `(w,(r:real^3->real^3) w)` THEN
\r
3208 ASM_SIMP_TAC[PAIR_EQ];
\r
3209 REWRITE_TAC[FUN_EQ_THM; I_THM] THEN
\r
3210 MATCH_MP_TAC(MESON[IN_UNION]
\r
3212 (!x. x IN FF' ==> P x) /\ (!x. x IN FF'' ==> P x) /\
\r
3213 (!x. ~(x IN FF' UNION FF'') ==> P x)
\r
3214 ==> !x. P x`) THEN
\r
3215 MAP_EVERY EXISTS_TAC
\r
3216 [`FF':real^3#real^3->bool`; `FF'':real^3#real^3->bool`] THEN
\r
3217 REPEAT CONJ_TAC THENL
\r
3218 [EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
3219 ASM_SIMP_TAC[PAIR_EQ];
\r
3220 EXPAND_TAC "FF''" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
3221 ASM_SIMP_TAC[PAIR_EQ];
\r
3222 ASM_REWRITE_TAC[FORALL_PAIR_THM; ff_of_hyp3] THEN
\r
3223 REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
3224 SPEC_TAC(`CARD(V':real^3->bool)`,`k:num`) THEN
\r
3225 INDUCT_TAC THEN ASM_REWRITE_TAC[ITER]]];
\r
3227 REPEAT CONJ_TAC THENL
\r
3228 [REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; o_THM; I_THM; FORALL_PAIR_THM] THEN
\r
3229 MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN
\r
3230 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
\r
3231 UNDISCH_TAC `(x:real^3,y) IN darts_of_hyp E' V'` THEN
\r
3232 ASM_REWRITE_TAC[] THEN
\r
3234 `(!x y:real^3. (x,y) IN FF' ==> (y,x) IN FF'') /\
\r
3235 (!x y:real^3. (x,y) IN FF'' ==> (y,x) IN FF')`
\r
3236 MP_TAC THENL [ALL_TAC; REWRITE_TAC[IN_UNION] THEN MESON_TAC[]] THEN
\r
3237 MAP_EVERY EXPAND_TAC ["FF'"; "FF''"] THEN
\r
3238 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[];
\r
3239 REWRITE_TAC[ee_of_hyp3; FUN_EQ_THM; I_THM] THEN
\r
3240 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
3241 DISCH_THEN(X_CHOOSE_TAC `x:real^3`) THEN
\r
3242 DISCH_THEN(MP_TAC o SPEC `x,(r:real^3->real^3) x`) THEN
\r
3243 ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN
\r
3244 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[PAIR_EQ] THEN
\r
3245 REMOVE_THEN "Rdistinct" (MP_TAC o SPECL [`x:real^3`; `SUC 0`]) THEN
\r
3246 ASM_SIMP_TAC[ITER; ARITH; ARITH_RULE `3 <= V ==> 1 < V`] THEN
\r
3247 ASM_MESON_TAC[PAIR_EQ];
\r
3248 REWRITE_TAC[nn_of_hyp3; FUN_EQ_THM; I_THM] THEN
\r
3249 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
\r
3250 DISCH_THEN(X_CHOOSE_TAC `x:real^3`) THEN
\r
3251 DISCH_THEN(MP_TAC o SPEC `x,(r:real^3->real^3) x`) THEN
\r
3252 ASM_REWRITE_TAC[IN_UNION] THEN EXPAND_TAC "FF'" THEN
\r
3253 REWRITE_TAC[IN_ELIM_THM] THEN
\r
3254 COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
\r
3255 ASM_SIMP_TAC[PAIR_EQ; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN
\r
3256 REMOVE_THEN "Rdistinct" (MP_TAC o SPECL [`x:real^3`; `SUC(SUC 0)`]) THEN
\r
3257 ASM_SIMP_TAC[ITER; ARITH; ARITH_RULE `3 <= V ==> 2 < V`] THEN
\r
3260 ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.convex_local_fan] THEN
\r
3261 EXPAND_TAC "FF'" THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
\r
3262 SIMP_TAC[Wrgcvdr_cizmrrh.azim_in_fan; Wrgcvdr_cizmrrh.wedge_in_fan_ge] THEN
\r
3263 X_GEN_TAC `u:real^3` THEN DISCH_TAC THEN ABBREV_TAC
\r
3264 `d = azim_cycle (EE u E') (vec 0) u (r u)` THEN
\r
3265 CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
\r
3266 SUBGOAL_THEN `CARD (EE (u:real^3) E') = 2` SUBST1_TAC THENL
\r
3267 [MATCH_MP_TAC(GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1) THEN
\r
3268 MAP_EVERY EXISTS_TAC [`FF':real^3#real^3->bool`; `V':real^3->bool`] THEN
\r
3269 ASM_REWRITE_TAC[] THEN EXPAND_TAC "V'" THEN ASM SET_TAC[];
\r
3270 CONV_TAC NUM_REDUCE_CONV] THEN
\r
3271 SUBGOAL_THEN `d = (r':real^3->real^3) u` SUBST1_TAC THENL
\r
3272 [EXPAND_TAC "d" THEN
\r
3273 SUBGOAL_THEN `EE (u:real^3) E' = {r u,r' u}`
\r
3274 (fun th -> REWRITE_TAC[th; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]) THEN
\r
3275 FIRST_ASSUM(fun th -> REWRITE_TAC
\r
3276 [MATCH_MP Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE th]) THEN
\r
3277 REWRITE_TAC[Fan.set_of_edge] THEN
\r
3278 EXPAND_TAC "E'" THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
3279 REWRITE_TAC[SET_RULE
\r
3280 `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
\r
3284 `!z. azim (vec 0) u (r u) z = azim (vec 0) u (rho_node1 FF u) z`
\r
3286 [X_GEN_TAC `z:real^3` THEN EXPAND_TAC "r" THEN
\r
3287 COND_CASES_TAC THEN REWRITE_TAC[] THEN
\r
3288 CONV_TAC SYM_CONV THEN MATCH_MP_TAC AZIM_SAME_WITHIN_AFF_GE THEN
\r
3289 ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
\r
3290 [SUBGOAL_THEN `u = ivs_rho_node1 FF v`
\r
3291 (fun th -> ASM_REWRITE_TAC[th]) THEN
\r
3292 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; IN_DIFF];
\r
3293 EXPAND_TAC "v" THEN
\r
3294 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; IN_DIFF];
\r
3295 DISCH_THEN(MP_TAC o SPEC `v:real^3` o MATCH_MP
\r
3296 (ONCE_REWRITE_RULE[IMP_CONJ_ALT] COLLINEAR_WITHIN_AFF_GE_COLLINEAR)) THEN
\r
3297 REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
\r
3298 [SUBGOAL_THEN `u = ivs_rho_node1 FF v`
\r
3299 (fun th -> ASM_REWRITE_TAC[th]) THEN
\r
3300 ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; IN_DIFF];
\r
3301 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]]];
\r
3304 [FIRST_ASSUM(MP_TAC o SPEC `u:real^3` o GEN_ALL o MATCH_MP
\r
3305 (ONCE_REWRITE_RULE[IMP_CONJ] Local_lemmas.IN_V_IMP_AZIM_LESS_PI)) THEN
\r
3306 ANTS_TAC THENL [ASM SET_TAC[]; ASM_REWRITE_TAC[]] THEN
\r
3307 DISCH_THEN MATCH_MP_TAC THEN ASM SET_TAC[];
\r
3309 FIRST_ASSUM(MP_TAC o CONJUNCT2 o GEN_REWRITE_RULE I
\r
3310 [Wrgcvdr_cizmrrh.convex_local_fan]) THEN
\r
3311 DISCH_THEN(MP_TAC o SPEC `u,rho_node1 FF u`) THEN ANTS_TAC THENL
\r
3312 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS; IN_DIFF];
\r
3313 DISCH_THEN(MP_TAC o CONJUNCT2)] THEN
\r
3314 MP_TAC(GEN_ALL(MATCH_MP(ONCE_REWRITE_RULE[IMP_CONJ]
\r
3315 Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND)
\r
3316 (ASSUME `local_fan (V:real^3->bool,E,FF)`))) THEN
\r
3317 DISCH_THEN(MP_TAC o SPEC `u:real^3`) THEN
\r
3318 ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
\r
3319 ASM_CASES_TAC `rho_node1 FF v = u` THENL
\r
3320 [ABBREV_TAC `w = ivs_rho_node1 FF v` THEN
\r
3321 EXPAND_TAC "r" THEN COND_CASES_TAC THENL
\r
3322 [ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE]; ALL_TAC] THEN
\r
3323 SUBGOAL_THEN `(r':real^3->real^3) u = w` SUBST1_TAC THENL
\r
3324 [SUBGOAL_THEN `(r:real^3->real^3) (r'(u:real^3)) = r w` MP_TAC THENL
\r
3325 [ASM_SIMP_TAC[] THEN EXPAND_TAC "r" THEN
\r
3326 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
\r
3327 ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS; IN_DIFF];
\r
3328 MATCH_MP_TAC EQ_IMP THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
3329 ASM_SIMP_TAC[] THEN EXPAND_TAC "V'" THEN
\r
3330 REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
3331 ASM_MESON_TAC[IN_DIFF; IN_SING; Local_lemmas1.LOCAL_FAN_IVS_IN_V;
\r
3332 Local_lemmas1.IVS_RHO_NODE_DIFF_ID]];
\r
3334 SUBGOAL_THEN `ivs_rho_node1 FF u = v` SUBST1_TAC THENL
\r
3335 [ASM_MESON_TAC[Local_lemmas.IVS_RHO_IDD; IN_DIFF];
\r
3336 REWRITE_TAC[Localization.wedge_ge; azim]] THEN
\r
3337 MATCH_MP_TAC(SET_RULE
\r
3338 `v' SUBSET v /\ s = t ==> v SUBSET s ==> v' SUBSET t`) THEN
\r
3339 CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
3340 MATCH_MP_TAC(SET_RULE
\r
3341 `a = b ==> {x | f x <= a} = {x | f x <= b}`) THEN
\r
3342 MATCH_MP_TAC AZIM_SAME_WITHIN_AFF_GE_ALT THEN REPEAT CONJ_TAC THENL
\r
3343 [ASM_MESON_TAC[INSERT_AC];
\r
3344 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; INSERT_AC];
\r
3345 DISCH_THEN(MP_TAC o SPEC `v:real^3` o MATCH_MP
\r
3346 (ONCE_REWRITE_RULE[IMP_CONJ_ALT] COLLINEAR_WITHIN_AFF_GE_COLLINEAR)) THEN
\r
3347 REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
\r
3348 [ASM_MESON_TAC[INSERT_AC];
\r
3349 ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]]];
\r
3350 ASM_REWRITE_TAC[Localization.wedge_ge; azim] THEN
\r
3351 SUBGOAL_THEN `(r':real^3->real^3) u = ivs_rho_node1 FF u`
\r
3352 (fun th -> REWRITE_TAC[th] THEN ASM SET_TAC[]) THEN
\r
3354 `(r:real^3->real^3)((r':real^3->real^3) u) = r(ivs_rho_node1 FF u)`
\r
3356 [ASM_SIMP_TAC[] THEN EXPAND_TAC "r" THEN
\r
3357 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
\r
3358 ASM_MESON_TAC[IN_DIFF; IN_SING; Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS];
\r
3359 MATCH_MP_TAC EQ_IMP THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
3360 ASM_SIMP_TAC[] THEN EXPAND_TAC "V'" THEN
\r
3361 REWRITE_TAC[IN_DIFF; IN_SING] THEN
\r
3362 ASM_MESON_TAC[IN_DIFF; IN_SING; Local_lemmas1.LOCAL_FAN_IVS_IN_V;
\r
3363 Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]]]);;
\r
git://colo12-c703.uibk.ac.at / Flyspeck/.git / blob