1 (* ========================================================================== *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
3 (* Section: Appendix *)
\r
4 (* Chapter: Local Fan *)
\r
5 (* Author: John Harrison *)
\r
6 (* Date: 2013-06-11 *)
\r
7 (* ========================================================================== *)
\r
9 module Xivphks = struct
\r
13 (* ------------------------------------------------------------------------- *)
\r
15 (* ------------------------------------------------------------------------- *)
\r
19 azim v0 v1 v2 v3 <= pi ==> azim v0 v2 v3 v1 <= pi`,
\r
20 GEOM_ORIGIN_TAC `v0:real^3` THEN
\r
21 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT] THEN
\r
22 REWRITE_TAC[GSYM REAL_NOT_LT; Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN
\r
23 MESON_TAC[CROSS_TRIPLE]);;
\r
25 (* ------------------------------------------------------------------------- *)
\r
27 (* ------------------------------------------------------------------------- *)
\r
31 1 <= n /\ n - 1 = r /\
\r
32 pairwise (\i j. ~collinear{vec 0,w i,w j}) (0..n) /\
\r
33 (\(i,j,k). dihV (vec 0) (w i) (w j) (w k)) = d /\
\r
34 (\(i,j,k). azim (vec 0) (w i) (w j) (w k)) = a /\
\r
35 (\i. wedge_ge (vec 0) (w i) (w(i + 1)) (w(i - 1))) = W /\
\r
37 (!i. i IN 1..r ==> &2 * e < a(i,i + 1,i - 1)) /\
\r
38 (!i. i IN 1..r ==> a(i,i + 1,i - 1) <= pi) /\
\r
39 (!p q. {p,q,q+1} SUBSET 0..r /\ ~(p = q) /\ ~(p = q + 1)
\r
40 ==> d(p,q,q + 1) < e) /\
\r
41 (!p q. {p,p+1,q} SUBSET 0..r /\ q > p + 1
\r
42 ==> d(p,p + 1,q) < e) /\
\r
43 (!p q. {p+1,p,q} SUBSET 0..r /\ q < p
\r
44 ==> d(p + 1,p,q) < e)
\r
45 ==> (!k j. j + k <= r ==> w j IN W(j + k)) /\
\r
46 (!k j. 1 <= j /\ j + k <= r ==> w(j + k) IN W(j))`,
\r
47 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_ARITH `&0 < &2 * e <=> &0 < e`] THEN
\r
48 REWRITE_TAC[IN_NUMSEG; GT; pairwise; LE_0] THEN STRIP_TAC THEN
\r
49 REWRITE_TAC[AND_FORALL_THM; TAUT
\r
50 `(p ==> r) /\ (q /\ p ==> s) <=> p ==> r /\ (q ==> s)`] THEN
\r
52 [REWRITE_TAC[ADD_CLAUSES; SUB_0] THEN
\r
53 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN
\r
54 REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim; REAL_LE_REFL];
\r
56 ASM_CASES_TAC `k = 0` THENL
\r
57 [ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1] THEN
\r
58 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN
\r
59 REWRITE_TAC[ADD_SUB; azim; REAL_LE_REFL; AZIM_REFL];
\r
61 DISJ_CASES_TAC(ARITH_RULE `r <= 1 \/ 2 <= r`) THENL
\r
62 [ASM_ARITH_TAC; ALL_TAC] THEN
\r
63 SUBGOAL_THEN `&2 * e < &2 * pi` ASSUME_TAC THENL
\r
64 [MATCH_MP_TAC REAL_LT_TRANS THEN
\r
65 EXISTS_TAC `a(1,1 + 1,1 - 1):real` THEN CONJ_TAC THENL
\r
66 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
67 EXPAND_TAC "a" THEN REWRITE_TAC[azim]];
\r
69 REWRITE_TAC[ADD1] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN
\r
70 MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC THENL
\r
71 [DISCH_TAC THEN UNDISCH_THEN
\r
73 ==> (w:num->real^3) j IN W (j + k) /\ (1 <= j ==> w (j + k) IN W j)`
\r
74 (MP_TAC o SPEC `j:num`) THEN
\r
75 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_ARITH_TAC; STRIP_TAC] THEN
\r
77 `a(j + k,j + k + 1,j) <= a(j + k,j + k + 1,j + k - 1)`
\r
79 [UNDISCH_TAC `(w:num->real^3) j IN W (j + k)` THEN
\r
80 MAP_EVERY EXPAND_TAC ["W"; "a"] THEN
\r
81 REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN
\r
82 DISCH_THEN(MP_TAC o CONJUNCT2) THEN MATCH_MP_TAC EQ_IMP THEN
\r
83 REPEAT(BINOP_TAC THEN REWRITE_TAC[]) THEN AP_TERM_TAC THEN ASM_ARITH_TAC;
\r
85 SUBGOAL_THEN `a(j + k,j + k + 1,j + k - 1) <= pi` ASSUME_TAC THENL
\r
86 [ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> j + k - 1 = (j + k) - 1`] THEN
\r
87 REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
89 SUBGOAL_THEN `a(j,j + k,j + k + 1) <= pi` ASSUME_TAC THENL
\r
90 [SUBGOAL_THEN `a (j + k,j + k + 1,j) <= pi` MP_TAC THENL
\r
91 [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]] THEN
\r
94 SUBGOAL_THEN `a(j,j + k,j + k + 1) < e` ASSUME_TAC THENL
\r
95 [SUBGOAL_THEN `a(j,j + k,j + k + 1):real = d(j,j + k,j + k + 1)`
\r
97 [UNDISCH_TAC `a (j,j + k,j + k + 1) <= pi` THEN
\r
98 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN
\r
99 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN
\r
100 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
101 REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
102 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC];
\r
104 SUBGOAL_THEN `a(j,j + 1,j + k) <= a(j,j + 1,j - 1)` ASSUME_TAC THENL
\r
105 [UNDISCH_TAC `(w:num->real^3) (j + k) IN W j` THEN
\r
106 MAP_EVERY EXPAND_TAC ["W"; "a"] THEN
\r
107 SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM];
\r
109 SUBGOAL_THEN `a(j,j + 1,j - 1) <= pi` ASSUME_TAC THENL
\r
110 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
\r
111 SUBGOAL_THEN `a(j,j + 1,j + k) <= pi` ASSUME_TAC THENL
\r
112 [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
\r
113 SUBGOAL_THEN `a(j,j + 1,j + k) < e` ASSUME_TAC THENL
\r
114 [ASM_CASES_TAC `k = 1` THENL
\r
115 [EXPAND_TAC "a" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[AZIM_REFL];
\r
117 SUBGOAL_THEN `a(j,j + 1,j + k):real = d(j,j + 1,j + k)`
\r
119 [UNDISCH_TAC `a (j,j + 1,j + k) <= pi` THEN
\r
120 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN
\r
121 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN
\r
122 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
123 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
124 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN
\r
127 SUBGOAL_THEN `a(j,j + 1,j + k + 1):real <= a(j,j + 1,j - 1)`
\r
129 [MATCH_MP_TAC REAL_LE_TRANS THEN
\r
130 EXISTS_TAC `a(j,j + 1,j + k) + a(j,j + k,j + k + 1)` THEN CONJ_TAC THENL
\r
131 [MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC
\r
132 [`a (j,j + k,j + k + 1):real < e`; `a (j,j + 1,j + k):real < e`] THEN
\r
133 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
\r
134 MATCH_MP_TAC Fan.sum3_azim_fan THEN
\r
135 CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
\r
136 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
138 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC THENL
\r
139 [ASM_REAL_ARITH_TAC; MATCH_MP_TAC REAL_LT_IMP_LE] THEN
\r
140 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
141 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN
\r
142 EXPAND_TAC "a" THEN REWRITE_TAC[azim]];
\r
147 ==> (w:num->real^3) j IN W (j + k) /\ (1 <= j ==> w (j + k) IN W j)`
\r
148 (MP_TAC o SPEC `j + 1`) THEN
\r
149 ASM_REWRITE_TAC[ARITH_RULE `(j + 1) + k = j + k + 1`;
\r
150 ARITH_RULE `1 <= j + 1`] THEN
\r
152 SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` ASSUME_TAC THENL
\r
153 [UNDISCH_TAC `(w:num->real^3) (j + k + 1) IN W (j + 1)` THEN
\r
154 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN
\r
155 EXPAND_TAC "a" THEN SIMP_TAC[ARITH_RULE `(a + 1) + 1 = a + 2`; ADD_SUB];
\r
157 SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) + a(j + 1,j + k + 1,j) =
\r
160 [CONV_TAC SYM_CONV THEN
\r
161 UNDISCH_TAC `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` THEN
\r
162 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC THEN
\r
163 MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[] THEN
\r
164 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
166 SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= a(j + 1,j + 2,j)` ASSUME_TAC THENL
\r
167 [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
\r
168 `a + b = c ==> &0 <= a ==> b <= c`)) THEN
\r
169 EXPAND_TAC "a" THEN REWRITE_TAC[azim];
\r
171 SUBGOAL_THEN `a(j + 1,(j + 1) + 1,(j + 1) - 1) <= pi` MP_TAC THENL
\r
172 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
173 REWRITE_TAC[ADD_SUB; ARITH_RULE `(n + 1) + 1 = n + 2`] THEN
\r
175 SUBGOAL_THEN `a(j + k + 1,j,j + 1) <= pi` ASSUME_TAC THENL
\r
176 [SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= pi` MP_TAC THENL
\r
177 [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]] THEN
\r
178 MESON_TAC[FSQKWKK];
\r
180 SUBGOAL_THEN `a(j + k + 1,j,j + 1) < e` ASSUME_TAC THENL
\r
181 [SUBGOAL_THEN `a(j + k + 1,j,j + 1):real = d(j + k + 1,j,j + 1) `
\r
183 [UNDISCH_TAC `a(j + k + 1,j,j + 1) <= pi` THEN
\r
184 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN
\r
185 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN
\r
186 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
187 REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
188 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC];
\r
190 SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)`
\r
192 [UNDISCH_TAC `(w:num->real^3)(j + 1) IN W (j + k + 1)` THEN
\r
193 MAP_EVERY EXPAND_TAC ["W"; "a"] THEN
\r
194 SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM;
\r
195 ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;
\r
196 ARITH_RULE `(j + k + 1) - 1 = j + k`];
\r
198 SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) + a(j + k + 1,j + 1,j + k) =
\r
199 a(j + k + 1,j + k + 2,j + k)`
\r
201 [CONV_TAC SYM_CONV THEN UNDISCH_TAC
\r
202 `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)` THEN
\r
203 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC THEN
\r
204 MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[] THEN
\r
205 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
207 SUBGOAL_THEN `a(j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1) <= pi`
\r
209 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
210 REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;
\r
211 ARITH_RULE `(j + k + 1) - 1 = j + k`] THEN
\r
213 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= a(j + k + 1,j + k + 2,j + k)`
\r
215 [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
\r
216 `a + b = c ==> &0 <= a ==> b <= c`)) THEN
\r
217 EXPAND_TAC "a" THEN REWRITE_TAC[azim];
\r
219 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= pi` ASSUME_TAC THENL
\r
220 [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
\r
221 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) < e` ASSUME_TAC THENL
\r
222 [ASM_CASES_TAC `k = 1` THENL
\r
223 [ASM_REWRITE_TAC[] THEN EXPAND_TAC "a" THEN REWRITE_TAC[AZIM_REFL] THEN
\r
226 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k):real = d(j + k + 1,j + 1,j + k)`
\r
228 [UNDISCH_TAC `a(j + k + 1,j + 1,j + k) <= pi` THEN
\r
229 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN
\r
230 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN
\r
231 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
233 SUBGOAL_THEN `d((j + k) + 1,j + k,j + 1) < e` MP_TAC THENL
\r
234 [FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
235 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC;
\r
236 EXPAND_TAC "d" THEN REWRITE_TAC[ADD_ASSOC; Counting_spheres.DIHV_SYM]];
\r
238 SUBGOAL_THEN `a(j + k + 1,j + k + 2,j) <= a(j + k + 1,j + k + 2,j + k)`
\r
241 MAP_EVERY EXPAND_TAC ["W"; "a"] THEN
\r
242 SIMP_TAC[Localization.wedge_ge; azim; IN_ELIM_THM;
\r
243 ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;
\r
244 ARITH_RULE `(j + k + 1) - 1 = j + k`]] THEN
\r
245 MATCH_MP_TAC REAL_LE_TRANS THEN
\r
246 EXISTS_TAC `a(j + k + 1,j + k + 2,j) + a(j + k + 1,j,j + k)` THEN
\r
248 [REWRITE_TAC[REAL_LE_ADDR] THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim];
\r
250 MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
\r
251 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
\r
252 MATCH_MP_TAC Fan.sum5_azim_fan THEN CONJ_TAC THENL
\r
254 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC] THEN
\r
255 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC THENL
\r
256 [MATCH_MP_TAC REAL_LE_TRANS THEN
\r
257 EXISTS_TAC `a(j + k + 1,j,j + 1) + a(j + k + 1,j + 1,j + k)` THEN
\r
259 [MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC
\r
260 [`a(j + k + 1,j,j + 1):real < e`;
\r
261 `a(j + k + 1,j + 1,j + k):real < e`] THEN
\r
262 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
\r
263 MATCH_MP_TAC Fan.sum3_azim_fan THEN
\r
264 CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
\r
265 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
266 ASM_REAL_ARITH_TAC];
\r
268 `&2 * e < a (j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1)`
\r
270 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
\r
271 EXPAND_TAC "a" THEN
\r
272 REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`;
\r
273 ARITH_RULE `(j + k + 1) - 1 = j + k`] THEN
\r
274 REAL_ARITH_TAC]]);;
\r
276 (* 1..r are the straight angles. Modified from Xivphks.XIVPHKS by shifting indices. *)
\r
278 let XIVPHKS_SHIFT = prove_by_refinement(
\r
280 pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\
\r
281 pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\
\r
282 (\(i,j,k). dihV (vec 0) (w i) (w j) (w k)) = d /\
\r
283 (\(i,j,k). azim (vec 0) (w i) (w j) (w k)) = a /\
\r
284 (\i. wedge_ge (vec 0) (w i) (w (i + 1)) (w (i - 1))) = W /\
\r
286 (!i. i IN 1..(r+1) ==> &2 * e < a (i,i + 1,i - 1)) /\
\r
287 (!i. i IN 1..(r+1) ==> a (i,i + 1,i - 1) <= pi) /\
\r
289 {p, q, q + 1} SUBSET 1..(r+1) /\ ~(p = q) /\ ~(p = q + 1)
\r
290 ==> d (p,q,q + 1) < e) /\
\r
292 {p, p + 1, q} SUBSET 1..(r+1) /\ q > p + 1 ==> d (p,p + 1,q) < e) /\
\r
293 (!p q. {p + 1, p, q} SUBSET 1..(r+1) /\ q < p ==> d (p + 1,p,q) < e)
\r
294 ==> (!k j. 1 <= j /\ j + k <= r+1 ==> w j IN W (j + k)) /\
\r
295 (!k j. 1 <= j /\ j + k <= r+1 ==> w (j + k) IN W j)`,
\r
298 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_ARITH `&0 < &2 * e <=> &0 < e`];
\r
299 REWRITE_TAC[IN_NUMSEG; GT; pairwise; LE_0] THEN STRIP_TAC;
\r
300 REWRITE_TAC[AND_FORALL_THM; TAUT `(p ==> r) /\ (q /\ p ==> s) <=> p ==> r /\ (q ==> s)`];
\r
302 REWRITE_TAC[ADD_CLAUSES; SUB_0];
\r
303 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];
\r
304 BY(REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim; REAL_LE_REFL]);
\r
305 ASM_CASES_TAC `k = 0`;
\r
306 ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1];
\r
307 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];
\r
308 BY(REWRITE_TAC[ADD_SUB; azim; REAL_LE_REFL; AZIM_REFL]);
\r
309 SUBGOAL_THEN `&2 * e < &2 * pi` ASSUME_TAC;
\r
310 MATCH_MP_TAC REAL_LT_TRANS;
\r
311 EXISTS_TAC `a(1,1 + 1,1 - 1):real` THEN CONJ_TAC;
\r
312 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
313 BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);
\r
314 REWRITE_TAC[ADD1] THEN X_GEN_TAC `j:num`;
\r
315 MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC;
\r
317 FIRST_X_ASSUM (C INTRO_TAC [`j`]);
\r
318 REPEAT WEAKER_STRIP_TAC;
\r
319 FIRST_X_ASSUM MP_TAC THEN ANTS_TAC;
\r
322 FIRST_X_ASSUM_ST `==>` MP_TAC THEN ANTS_TAC;
\r
325 SUBGOAL_THEN `a(j + k,j + k + 1,j) <= a(j + k,j + k + 1,j + k - 1)` ASSUME_TAC;
\r
326 FIRST_X_ASSUM MP_TAC THEN MAP_EVERY EXPAND_TAC ["W"; "a"];
\r
327 REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];
\r
328 DISCH_THEN(MP_TAC o CONJUNCT2) THEN MATCH_MP_TAC EQ_IMP;
\r
329 BY(REPEAT(BINOP_TAC THEN REWRITE_TAC[]) THEN AP_TERM_TAC THEN ASM_ARITH_TAC);
\r
330 SUBGOAL_THEN `a(j + k,j + k + 1,j + k - 1) <= pi` ASSUME_TAC;
\r
331 ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> j + k - 1 = (j + k) - 1`];
\r
332 BY(REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
333 SUBGOAL_THEN `a(j,j + k,j + k + 1) <= pi` ASSUME_TAC;
\r
334 SUBGOAL_THEN `a (j + k,j + k + 1,j) <= pi` MP_TAC THENL [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]];
\r
335 BY(MESON_TAC[FSQKWKK]);
\r
336 SUBGOAL_THEN `a(j,j + k,j + k + 1) < e` ASSUME_TAC;
\r
337 SUBGOAL_THEN `a(j,j + k,j + k + 1):real = d(j,j + k,j + k + 1)` SUBST1_TAC;
\r
338 UNDISCH_TAC `a (j,j + k,j + k + 1) <= pi`;
\r
339 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;
\r
340 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];
\r
341 BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
342 REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC;
\r
343 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG];
\r
345 SUBGOAL_THEN `a(j,j + 1,j + k) <= a(j,j + 1,j - 1)` ASSUME_TAC;
\r
346 UNDISCH_TAC `(w:num->real^3) (j + k) IN W j`;
\r
347 MAP_EVERY EXPAND_TAC ["W"; "a"];
\r
348 BY(SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM]);
\r
349 SUBGOAL_THEN `a(j,j + 1,j - 1) <= pi` ASSUME_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC];
\r
350 SUBGOAL_THEN `a(j,j + 1,j + k) <= pi` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC];
\r
351 SUBGOAL_THEN `a(j,j + 1,j + k) < e` ASSUME_TAC;
\r
352 ASM_CASES_TAC `k=1`;
\r
353 BY(EXPAND_TAC "a" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[AZIM_REFL]);
\r
354 SUBGOAL_THEN `a(j,j + 1,j + k):real = d(j,j + 1,j + k)` SUBST1_TAC;
\r
355 UNDISCH_TAC `a (j,j + 1,j + k) <= pi`;
\r
356 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;
\r
357 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];
\r
358 BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
359 FIRST_X_ASSUM MATCH_MP_TAC;
\r
360 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG];
\r
362 SUBGOAL_THEN `a(j,j + 1,j + k + 1):real <= a(j,j + 1,j - 1)` MP_TAC;
\r
363 MATCH_MP_TAC REAL_LE_TRANS;
\r
364 EXISTS_TAC `a(j,j + 1,j + k) + a(j,j + k,j + k + 1)` THEN CONJ_TAC;
\r
365 MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a (j,j + k,j + k + 1):real < e`; `a (j,j + 1,j + k):real < e`];
\r
366 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
\r
367 MATCH_MP_TAC Fan.sum3_azim_fan;
\r
368 CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC];
\r
369 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
370 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC;
\r
371 BY(ASM_REAL_ARITH_TAC);
\r
372 MATCH_MP_TAC REAL_LT_IMP_LE;
\r
373 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
374 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];
\r
375 BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);
\r
377 COMMENT "midpoint -- down to 1 goal";
\r
379 FIRST_X_ASSUM (C INTRO_TAC [`j+1`]);
\r
380 ASM_REWRITE_TAC[arith `1 <= j+1`;arith `(j + 1) + k = j + k + 1`;];
\r
381 REPEAT WEAKER_STRIP_TAC;
\r
382 SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` ASSUME_TAC;
\r
383 UNDISCH_TAC `(w:num->real^3) (j + k + 1) IN W (j + 1)`;
\r
384 EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM];
\r
385 BY(EXPAND_TAC "a" THEN SIMP_TAC[ARITH_RULE `(a + 1) + 1 = a + 2`; ADD_SUB]);
\r
386 SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) + a(j + 1,j + k + 1,j) = a(j + 1,j + 2,j)` ASSUME_TAC;
\r
388 UNDISCH_TAC `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)`;
\r
389 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC;
\r
390 MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[];
\r
391 TYPIFY_GOAL_THEN `~collinear {vec 0, w (j + 1), w j}` (unlist REWRITE_TAC);
\r
392 FIRST_X_ASSUM_ST `collinear` kill;
\r
393 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
394 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN TRY ASM_ARITH_TAC);
\r
395 SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= a(j + 1,j + 2,j)` ASSUME_TAC;
\r
396 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`));
\r
397 BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);
\r
398 SUBGOAL_THEN `a(j + 1,(j + 1) + 1,(j + 1) - 1) <= pi` MP_TAC;
\r
399 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
400 REWRITE_TAC[ADD_SUB; ARITH_RULE `(n + 1) + 1 = n + 2`];
\r
402 SUBGOAL_THEN `a(j + k + 1,j,j + 1) <= pi` ASSUME_TAC;
\r
403 SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= pi` MP_TAC;
\r
404 BY(ASM_REAL_ARITH_TAC);
\r
405 EXPAND_TAC "a" THEN REWRITE_TAC[];
\r
406 BY(MESON_TAC[FSQKWKK]);
\r
407 SUBGOAL_THEN `a(j + k + 1,j,j + 1) < e` ASSUME_TAC;
\r
408 ASM_CASES_TAC `k = 0`;
\r
409 BY(EXPAND_TAC "a" THEN ASM_REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE;arith `j + 0 + 1 = j+1`]);
\r
410 SUBGOAL_THEN `a(j + k + 1,j,j + 1):real = d(j + k + 1,j,j + 1) ` SUBST1_TAC;
\r
411 UNDISCH_TAC `a(j + k + 1,j,j + 1) <= pi`;
\r
412 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;
\r
413 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];
\r
414 BY(CONJ_TAC THENL [FIRST_X_ASSUM_ST `collinear` kill;ALL_TAC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
415 REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC;
\r
416 BY(REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC);
\r
417 SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC;
\r
418 UNDISCH_TAC `(w:num->real^3)(j + 1) IN W (j + k + 1)`;
\r
419 MAP_EVERY EXPAND_TAC ["W"; "a"];
\r
420 BY(SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]);
\r
421 SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) + a(j + k + 1,j + 1,j + k) = a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC;
\r
423 UNDISCH_TAC `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)`;
\r
424 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC;
\r
425 MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[];
\r
426 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
428 ASM_CASES_TAC `k = 0`;
\r
429 ASM_REWRITE_TAC[arith `j+0+1 = j+1`];
\r
430 EXPAND_TAC "W" THEN REWRITE_TAC[];
\r
431 ASM_SIMP_TAC[arith `1 <= j ==> (j+1)+1 = j+2 /\ (j+1)-1 = j`];
\r
432 BY(REWRITE_TAC[Local_lemmas1.FST_LST_IN_WEDGE_GE]);
\r
433 SUBGOAL_THEN `a(j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1) <= pi` MP_TAC;
\r
434 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
435 REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`];
\r
437 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC;
\r
438 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`));
\r
439 BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]);
\r
440 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= pi` ASSUME_TAC;
\r
441 BY(ASM_REAL_ARITH_TAC);
\r
442 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) < e` ASSUME_TAC;
\r
443 ASM_CASES_TAC `k = 1`;
\r
444 ASM_REWRITE_TAC[] THEN EXPAND_TAC "a" THEN REWRITE_TAC[AZIM_REFL];
\r
445 BY(ASM_REWRITE_TAC[]);
\r
446 SUBGOAL_THEN `a(j + k + 1,j + 1,j + k):real = d(j + k + 1,j + 1,j + k)` SUBST1_TAC;
\r
447 UNDISCH_TAC `a(j + k + 1,j + 1,j + k) <= pi`;
\r
448 MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC;
\r
449 MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[];
\r
450 BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
451 SUBGOAL_THEN `d((j + k) + 1,j + k,j + 1) < e` MP_TAC;
\r
452 FIRST_X_ASSUM MATCH_MP_TAC;
\r
453 BY(REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC);
\r
454 BY(EXPAND_TAC "d" THEN REWRITE_TAC[ADD_ASSOC; Counting_spheres.DIHV_SYM]);
\r
456 ENOUGH_TO_SHOW_TAC `a(j + k + 1,j + k + 2,j) <= a(j + k + 1,j + k + 2,j + k)`;
\r
457 MAP_EVERY EXPAND_TAC ["W"; "a"];
\r
458 BY(SIMP_TAC[Localization.wedge_ge; azim; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]);
\r
459 MATCH_MP_TAC REAL_LE_TRANS;
\r
460 EXISTS_TAC `a(j + k + 1,j + k + 2,j) + a(j + k + 1,j,j + k)`;
\r
462 BY(REWRITE_TAC[REAL_LE_ADDR] THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim]);
\r
463 MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV;
\r
464 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
\r
465 MATCH_MP_TAC Fan.sum5_azim_fan;
\r
467 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
468 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC;
\r
469 MATCH_MP_TAC REAL_LE_TRANS;
\r
470 EXISTS_TAC `a(j + k + 1,j,j + 1) + a(j + k + 1,j + 1,j + k)`;
\r
472 MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a(j + k + 1,j,j + 1):real < e`; `a(j + k + 1,j + 1,j + k):real < e`];
\r
473 EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
\r
474 MATCH_MP_TAC Fan.sum3_azim_fan;
\r
475 CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC];
\r
476 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
477 BY(ASM_REAL_ARITH_TAC);
\r
478 SUBGOAL_THEN `&2 * e < a (j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1)` MP_TAC;
\r
479 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);
\r
481 REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`];
\r