2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Local Fan *)
6 (* Author: Hoang Le Truong *)
8 (* ========================================================================= *)
13 module Dih2k_hypermap = struct
34 open Prove_by_refinement;;
36 open Wrgcvdr_cizmrrh;;
40 parse_as_infix("has_orders",(12,"right"));;
42 let cstab=new_definition ` cstab= #3.01`;;
44 let rho_fun = new_definition `rho_fun y = &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
47 let tau_fun = new_definition `tau_fun V E f = sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;
49 (* deprecated 2013-02-26:
50 let standard = new_definition
51 ` standard v w <=> &2 <= norm(v-w) /\ norm (v-w) <= &2 *h0 `;;
53 let protracted = new_definition
54 ` protracted v w <=> &2 * h0 <= norm(v-w) /\ norm (v-w) <= sqrt (&8) `;;
56 let diagonal0 = new_definition
57 ` (diagonal0 (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) <=> ~(v = w) /\ ~({v,w} IN E) `;;
59 let diagonal1 = new_definition
60 ` diagonal1 (V,E) <=> !v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E)
61 ==> &2 * h0 <= norm(v-w) `;;
63 let main_estimate= new_definition
64 ` main_estimate(V,E,f) <=>
65 convex_local_fan(V,E,f) /\
67 V SUBSET ball_annulus /\
75 let torsor = new_definition
76 ` torsor (s:A->bool) k (f:A->A) <=> (!x. x IN s ==> (f x) IN s) /\ (!x1 x2. x1 IN s /\ x2 IN s /\ f x1 = f x2 ==> x1=x2) /\ (!i x. 0 < i /\ i < k /\ x IN s ==> ~((f POWER i) x = x)) /\ (!x. x IN s==> (f POWER k) x = x)
80 let constraint_system=new_definition
81 `constraint_system k d (s:A->bool) (a:A#A->real) (b:A#A->real) J f<=>
84 (!i j. a(i,j)= a(j,i) /\ b(i,j)=b(j,i) /\ a(i,j)<= b(i,j))
85 /\(!i j. a(i,j)= a(i,(f POWER k) j) /\ b(i,j)=b(i,(f POWER k) j))
86 /\ J SUBSET {{i,f i}| i IN s} /\
89 let stable_system=new_definition
90 `stable_system k d s a b J f<=>
91 constraint_system k d s a b J f /\
92 (!i j. i IN s /\ j IN s /\ ~(i=j) ==> &2<= a(i,j)) /\
93 (!i. i IN s==> a(i,i)= &0 /\ b(i,f i)<= cstab)/\
94 (!i j. {i,j} IN J ==> a(i,j)= sqrt(&8) /\ b(i,j) =cstab)`;;
98 let V_SY=new_definition
99 `V_SY (v:real^N^M) = rows v`;;
101 let E_SY=new_definition
102 `E_SY (v:real^N^M) = { {row i v,row (SUC(i MOD dimindex(:M))) v } | 1<=i /\ i <= dimindex(:M)}`;;
104 let F_SY=new_definition
105 `F_SY (v:real^N^M) = { (row i v,row (SUC(i MOD dimindex(:M))) v ) | 1<=i /\ i <= dimindex(:M)}`;;
107 let CONDITION1_SY=new_definition
108 `CONDITION1_SY a b (v:real^N^M)
110 (!i j. 1<=i /\ i <= dimindex(:M) /\ 1<=j /\ j <= dimindex(:M)
112 a(i,j)<= norm(row i v- row j v) /\
113 norm(row i v- row j v)<= b(i,j)) `;;
116 let CONDITION2_SY=new_definition
117 `CONDITION2_SY (v:real^3^M)
118 <=> convex_local_fan(V_SY v,E_SY v,F_SY v)`;;
125 let finite_product_tybij =
127 (`?x. x IN 1..(dimindex(:A) * dimindex(:B))`,
128 EXISTS_TAC `1` THEN SIMP_TAC[IN_NUMSEG; LE_REFL; DIMINDEX_GE_1;]
129 THEN MRESA1_TAC DIMINDEX_GE_1`(:A)`
130 THEN MRESA1_TAC DIMINDEX_GE_1`(:B)`
131 THEN MRESAL_TAC LE_MULT2[`1`;`dimindex(:A)`;`1`;`dimindex(:B)`][ARITH_RULE `1 *1=1`])
133 new_type_definition "finite_product" ("mk_finite_product","dest_finite_product") th;;
135 let matvec = new_definition
136 `(matvec:(A^N)^M->A^(M,N)finite_product) f =
137 lambda i. f$ (if i MOD dimindex(:N)=0 then i DIV dimindex(:N) else SUC(i DIV dimindex(:N)))
138 $(if (i MOD dimindex(:N))=0 then dimindex(:N) else (i MOD dimindex(:N)))`;;
141 let vecmat = new_definition
142 `(vecmat:num->A^(M,N)finite_product ->A^N) j f =
143 lambda i. f$(j * dimindex(:N)+i)`;;
145 let vecmats= new_definition
146 `(vecmats:A^(M,N)finite_product ->(A^N)^M) f =
147 lambda i j. f$((i-1) * dimindex(:N)+j)`;;
150 let B_SY1=new_definition
151 `B_SY1 a b = {matvec(v:real^3^M) |(!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus)
152 /\ CONDITION1_SY a b v /\ CONDITION2_SY v}`;;
155 let FINITE_PRODUCT_IMAGE = prove
156 (`UNIV:(A,B)finite_product->bool =
157 IMAGE mk_finite_product (1..(dimindex(:A)*dimindex(:B)))`,
158 REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN
159 MESON_TAC[finite_product_tybij]);;
162 let DIMINDEX_HAS_SIZE_FINITE_PRODUCT = prove
163 (`(UNIV:(M,N)finite_product->bool) HAS_SIZE (dimindex(:M) * dimindex(:N))`,
164 SIMP_TAC[FINITE_PRODUCT_IMAGE] THEN
165 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
166 ONCE_REWRITE_TAC[DIMINDEX_UNIV] THEN REWRITE_TAC[HAS_SIZE_NUMSEG_1] THEN
167 MESON_TAC[finite_product_tybij]);;
170 let DIMINDEX_FINITE_PRODUCT = prove
171 (`dimindex(:(M,N)finite_product) = dimindex(:M) * dimindex(:N)`,
172 GEN_REWRITE_TAC LAND_CONV [dimindex] THEN
173 REWRITE_TAC[REWRITE_RULE[HAS_SIZE] DIMINDEX_HAS_SIZE_FINITE_PRODUCT]);;
176 let INDEX_VECMAT=prove(` i< dimindex(:M) /\ 1<= i' /\ i'<= dimindex (:N) ==>
177 1<= i * dimindex (:N) + i'/\
178 i * dimindex (:N) + i'<= dimindex(:(M,N)finite_product) `,
180 THEN MP_TAC(ARITH_RULE`1<= i' ==> 1<=i * dimindex (:N) + i'`)
182 THEN REWRITE_TAC[DIMINDEX_FINITE_PRODUCT]
183 THEN MRESAL_TAC LE_MULT2[`SUC i`;`dimindex(:M)`;`dimindex(:N)`;`dimindex(:N)`][ARITH_RULE `dimindex(:N)<=dimindex(:N)`;ADD1]
188 let VECMAT_ROW=prove(` i< dimindex(:M)==> vecmat i (matvec (f:real^N^M))= row (SUC i) f`,
189 SIMP_TAC[vecmat;matvec;row;CART_EQ;LAMBDA_BETA;GSYM LE_SUC_LT]
190 THEN REPEAT STRIP_TAC
191 THEN MRESA1_TAC Hypermap.GE_1`i:num`
192 THEN ASM_SIMP_TAC[LAMBDA_BETA]
193 THEN MP_TAC(ARITH_RULE`1<= i' ==> 1<=i * dimindex (:N) + i'`)
195 THEN SUBGOAL_THEN`i * dimindex (:N) + i'<= dimindex(:(M,N)finite_product)` ASSUME_TAC
197 REWRITE_TAC[DIMINDEX_FINITE_PRODUCT]
198 THEN MRESAL_TAC LE_MULT2[`SUC i`;`dimindex(:M)`;`dimindex(:N)`;`dimindex(:N)`][ARITH_RULE `dimindex(:N)<=dimindex(:N)`;ADD1]
201 ASM_SIMP_TAC[LAMBDA_BETA]
202 THEN MP_TAC(ARITH_RULE`i' <= dimindex (:N)==> i' = dimindex (:N)\/ i' < dimindex (:N)`)
205 REWRITE_TAC[ARITH_RULE`A*B+B=(A+1)*B:num`]
206 THEN MP_TAC(ARITH_RULE`1<=dimindex (:N)==> 0<dimindex (:N)`)
207 THEN SIMP_TAC[DIMINDEX_GE_1]
209 THEN MRESAL_TAC DIVMOD_UNIQ[`(i + 1) * dimindex (:N)`;`dimindex (:N)`;`(i + 1) `;`0`][ARITH_RULE`A+0=A:num`;ADD1];
210 MP_TAC(ARITH_RULE`1<= i'==> ~(i'=0)`)
212 THEN MRESAL_TAC DIVMOD_UNIQ[`i * dimindex (:N) + i'`;`dimindex (:N)`;`i:num`;`i':num`][ARITH_RULE`A+0=A:num`;ADD1]]]);;
215 let VECMATS_MATVEC_ID=prove(`vecmats (matvec A)= A:real^N^M`,
216 ONCE_REWRITE_TAC[FUN_EQ_THM;CART_EQ;]
217 THEN SIMP_TAC[LAMBDA_BETA;vecmats;]
218 THEN REPEAT STRIP_TAC
219 THEN MP_TAC(ARITH_RULE`1<= i/\ i<= dimindex (:M) ==> i-1<dimindex (:M)`)
221 THEN ABBREV_TAC`n= i-1`
222 THEN SUBGOAL_THEN(`i= SUC n`) ASSUME_TAC
228 THEN MRESAL_TAC (GEN_ALL VECMAT_ROW)[`n:num`;`A:real^N^M`][vecmat;row]
229 THEN SIMP_TAC[CART_EQ;LAMBDA_BETA]]);;
232 let MATVEC_VECMATS_ID=prove_by_refinement(`matvec(vecmats (A:real^(M,N)finite_product))= A:real^(M,N)finite_product`,
233 [SIMP_TAC[matvec;vecmats;CART_EQ;LAMBDA_BETA;DIMINDEX_FINITE_PRODUCT]
234 THEN REPEAT STRIP_TAC
235 THEN DISJ_CASES_TAC(SET_RULE`i MOD dimindex (:N) = 0\/ ~(i MOD dimindex (:N) = 0)`)
236 THEN ASM_SIMP_TAC[LAMBDA_BETA;];
237 MP_TAC(ARITH_RULE`dimindex(:N)<=dimindex(:N)`)
238 THEN MRESA1_TAC DIMINDEX_GE_1`(:N)`
239 THEN MRESAL_TAC DIV_MULT[`dimindex (:N)`;` dimindex (:M)`][DIMINDEX_NONZERO]
240 THEN MRESAL_TAC DIV_MONO[`i:num`;`dimindex (:M) * dimindex (:N)`;` dimindex (:N)`][DIMINDEX_NONZERO]
241 THEN POP_ASSUM MP_TAC
242 THEN ONCE_REWRITE_TAC[ ARITH_RULE`dimindex (:M) * dimindex (:N)= dimindex (:N) * dimindex (:M)`;]
243 THEN ASM_REWRITE_TAC[]
244 THEN MRESAL_TAC MOD_EQ_0[`i:num`;`dimindex (:N)`][DIMINDEX_NONZERO]
245 THEN POP_ASSUM MP_TAC
246 THEN DISJ_CASES_TAC(ARITH_RULE`q=0 \/ 1<=q`);
247 ASM_REWRITE_TAC[ARITH_RULE`0*A=0`]
249 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
251 MRESAL_TAC DIV_MULT[`dimindex (:N)`;` q:num`][DIMINDEX_NONZERO]
252 THEN ONCE_REWRITE_TAC[ ARITH_RULE`q * dimindex (:N)= dimindex (:N) * q`;]
253 THEN ASM_REWRITE_TAC[]
254 THEN MP_TAC(ARITH_RULE`1<= q==> q-1+1=q`)
255 THEN ASM_SIMP_TAC[LAMBDA_BETA;ARITH_RULE`a*b+a=a*(b+1)`];
256 MRESAL_TAC DIVISION[`i:num`;`dimindex (:N)`][DIMINDEX_NONZERO]
257 THEN MP_TAC(ARITH_RULE`~(i MOD dimindex (:N) = 0) /\ i MOD dimindex (:N)< dimindex (:N) ==> 1<=i MOD dimindex (:N) /\ i MOD dimindex (:N)<= dimindex (:N)
258 /\ 1<=SUC (i DIV dimindex (:N))`)
260 THEN MRESAL_TAC LE_LDIV[`dimindex (:N)`;`i:num`;`dimindex (:M)`][DIMINDEX_NONZERO]
261 THEN POP_ASSUM MP_TAC
262 THEN ONCE_REWRITE_TAC[ ARITH_RULE`dimindex (:M) * dimindex (:N)= dimindex (:N) * dimindex (:M)`;]
263 THEN ASM_REWRITE_TAC[]
265 THEN MP_TAC(ARITH_RULE`i DIV dimindex (:N) <= dimindex (:M) ==> i DIV dimindex (:N) = dimindex (:M) \/ SUC(i DIV dimindex (:N)) <= dimindex (:M)`)
267 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th])
269 MP_TAC(ARITH_RULE` (SUC (i DIV dimindex (:N)))-1=i DIV dimindex (:N)`)
271 THEN ASM_SIMP_TAC[LAMBDA_BETA;ARITH_RULE`a*b+a=a*(b+1)`]
272 THEN ASM_MESON_TAC[]]);;
281 let LINEAR_VECMAT = prove
282 (`linear (vecmat i)`,
283 SIMP_TAC[linear; vecmat; CART_EQ; LAMBDA_BETA; VECTOR_ADD_COMPONENT;
284 VECTOR_MUL_COMPONENT; DIMINDEX_FINITE_PRODUCT;]);;
286 let VECMAT_VEC = prove
287 (`!i n. i< dimindex(:M)==> ((vecmat i):real^(M,N)finite_product->real^N) (vec n) = vec n`,
288 SIMP_TAC[vec; vecmat; LAMBDA_BETA; CART_EQ;]
289 THEN REPEAT STRIP_TAC
290 THEN MRESA_TAC (GEN_ALL INDEX_VECMAT)[`i:num`;`i':num`]
291 THEN ASM_SIMP_TAC[vec; vecmat; LAMBDA_BETA; CART_EQ;]);;
293 let VECMAT_ADD = prove
294 (`!i x:real^(M,N)finite_product y. (vecmat i) (x + y) = (vecmat i) (x) + (vecmat i) (y)`,
295 REWRITE_TAC[REWRITE_RULE[linear] LINEAR_VECMAT]);;
298 let VECMAT_CMUL = prove
299 (`!i x:real^(M,N)finite_product c. (vecmat i)(c % x) = c % (vecmat i)(x)`,
300 REWRITE_TAC[REWRITE_RULE[linear] LINEAR_VECMAT]);;
302 let VECMAT_NEG = prove
303 (`!i x:real^(M,N)finite_product. --((vecmat i) x) = (vecmat i)(--x)`,
304 ONCE_REWRITE_TAC[VECTOR_ARITH `--x = --(&1) % x`] THEN
305 REWRITE_TAC[VECMAT_CMUL]);;
307 let VECMAT_SUB = prove
308 (`!i x:real^(M,N)finite_product y. (vecmat i)(x - y) = (vecmat i)(x) - (vecmat i)(y)`,
309 REWRITE_TAC[VECTOR_SUB; VECMAT_NEG; VECMAT_ADD]);;
311 let FSTCART_VSUM = prove
312 (`!k x i. FINITE k ==> i< dimindex(:M) ==> ((vecmat i)(vsum k x) = vsum k (\i'. ((vecmat i):real^(M,N)finite_product->real^N)(x i')))`,
313 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
314 MATCH_MP_TAC FINITE_INDUCT_STRONG
316 SIMP_TAC[VSUM_CLAUSES; FINITE_RULES; VECMAT_ADD; VECMAT_VEC]);;
319 let MATVEC_ADD = prove(`matvec (x:real^N^M) + matvec y= matvec (x +y) `,
320 SIMP_TAC[matvec;LAMBDA_BETA;CART_EQ;matrix_add;vector_add;DIMINDEX_FINITE_PRODUCT]
321 THEN REPEAT STRIP_TAC
322 THEN DISJ_CASES_TAC(SET_RULE`i MOD dimindex (:N) =0\/ ~(i MOD dimindex (:N)=0)`)
325 THEN MRESAL_TAC DIV_MULT[`dimindex (:N)`;`dimindex (:M)`][DIMINDEX_NONZERO]
326 THEN POP_ASSUM MP_TAC
327 THEN ONCE_REWRITE_TAC[ARITH_RULE`dimindex (:N) * dimindex (:M)=dimindex (:M) * dimindex (:N)`]
329 THEN MRESAL_TAC MOD_EQ_0[`i:num`;`dimindex (:N)`][DIMINDEX_NONZERO]
330 THEN MRESAL_TAC DIV_MONO[`i:num`;`dimindex (:M)* dimindex (:N)`;`dimindex (:N)`][DIMINDEX_NONZERO]
331 THEN DISJ_CASES_TAC(ARITH_RULE`q= 0\/ 1<=q`)
332 THENL[POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`0*A=0`])
335 THEN POP_ASSUM MP_TAC
336 THEN ONCE_REWRITE_TAC[ARITH_RULE`q * dimindex (:N)=dimindex (:N) * q`]
337 THEN MRESAL_TAC DIV_MULT[`dimindex (:N)`;`q:num`][DIMINDEX_NONZERO]
338 THEN MP_TAC(ARITH_RULE`dimindex (:N)<=dimindex (:N)`)
339 THEN MRESA1_TAC DIMINDEX_GE_1`(:N)`
340 THEN ASM_SIMP_TAC[LAMBDA_BETA;]];
342 THEN SUBGOAL_THEN`1 <= SUC (i DIV dimindex (:N))` ASSUME_TAC
344 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`];
345 MRESAL_TAC DIVISION[`i:num`;`dimindex (:N):num`][DIMINDEX_NONZERO]
346 THEN MP_TAC(ARITH_RULE`~(i MOD dimindex (:N) = 0) /\ i MOD dimindex (:N) < dimindex (:N) ==> 1<= i MOD dimindex (:N) /\ i MOD dimindex (:N) <= dimindex (:N) `)
348 THEN MRESAL_TAC DIV_MULT[`dimindex (:N)`;`dimindex (:M)`][DIMINDEX_NONZERO]
349 THEN POP_ASSUM MP_TAC
350 THEN ONCE_REWRITE_TAC[ARITH_RULE`dimindex (:N) * dimindex (:M)=dimindex (:M) * dimindex (:N)`]
352 THEN MRESAL_TAC MOD_EQ_0[`i:num`;`dimindex (:N)`][DIMINDEX_NONZERO]
353 THEN MRESAL_TAC DIV_MONO[`i:num`;`dimindex (:M)* dimindex (:N)`;`dimindex (:N)`][DIMINDEX_NONZERO]
354 THEN MP_TAC(ARITH_RULE`i DIV dimindex (:N)<= dimindex (:M)==> i DIV dimindex (:N)= dimindex (:M) \/ SUC(i DIV dimindex (:N))<= dimindex (:M)`)
357 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
358 THEN REPEAT STRIP_TAC)
359 THEN MP_TAC(ARITH_RULE`i = dimindex (:M) * dimindex (:N) + i MOD dimindex (:N) /\ ~(i MOD dimindex (:N)= 0)
360 ==> dimindex (:M) * dimindex (:N)< i`)
362 THEN REMOVE_ASSUM_TAC
363 THEN REMOVE_ASSUM_TAC
364 THEN REMOVE_ASSUM_TAC
365 THEN REMOVE_ASSUM_TAC
366 THEN REMOVE_ASSUM_TAC
367 THEN REMOVE_ASSUM_TAC
368 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
372 ASM_SIMP_TAC[LAMBDA_BETA;]]]]);;
375 let MATVEC_SUB = prove(`matvec (x:real^N^M) - matvec y= matvec (x -y) `,
376 SIMP_TAC[matvec;LAMBDA_BETA;CART_EQ;matrix_sub;vector_sub;DIMINDEX_FINITE_PRODUCT]
377 THEN REPEAT STRIP_TAC
378 THEN DISJ_CASES_TAC(SET_RULE`i MOD dimindex (:N) =0\/ ~(i MOD dimindex (:N)=0)`)
381 THEN MRESAL_TAC DIV_MULT[`dimindex (:N)`;`dimindex (:M)`][DIMINDEX_NONZERO]
382 THEN POP_ASSUM MP_TAC
383 THEN ONCE_REWRITE_TAC[ARITH_RULE`dimindex (:N) * dimindex (:M)=dimindex (:M) * dimindex (:N)`]
385 THEN MRESAL_TAC MOD_EQ_0[`i:num`;`dimindex (:N)`][DIMINDEX_NONZERO]
386 THEN MRESAL_TAC DIV_MONO[`i:num`;`dimindex (:M)* dimindex (:N)`;`dimindex (:N)`][DIMINDEX_NONZERO]
387 THEN DISJ_CASES_TAC(ARITH_RULE`q= 0\/ 1<=q`)
388 THENL[POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`0*A=0`])
391 THEN POP_ASSUM MP_TAC
392 THEN ONCE_REWRITE_TAC[ARITH_RULE`q * dimindex (:N)=dimindex (:N) * q`]
393 THEN MRESAL_TAC DIV_MULT[`dimindex (:N)`;`q:num`][DIMINDEX_NONZERO]
394 THEN MP_TAC(ARITH_RULE`dimindex (:N)<=dimindex (:N)`)
395 THEN MRESA1_TAC DIMINDEX_GE_1`(:N)`
396 THEN ASM_SIMP_TAC[LAMBDA_BETA;]];
398 THEN SUBGOAL_THEN`1 <= SUC (i DIV dimindex (:N))` ASSUME_TAC
400 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`];
401 MRESAL_TAC DIVISION[`i:num`;`dimindex (:N):num`][DIMINDEX_NONZERO]
402 THEN MP_TAC(ARITH_RULE`~(i MOD dimindex (:N) = 0) /\ i MOD dimindex (:N) < dimindex (:N) ==> 1<= i MOD dimindex (:N) /\ i MOD dimindex (:N) <= dimindex (:N) `)
404 THEN MRESAL_TAC DIV_MULT[`dimindex (:N)`;`dimindex (:M)`][DIMINDEX_NONZERO]
405 THEN POP_ASSUM MP_TAC
406 THEN ONCE_REWRITE_TAC[ARITH_RULE`dimindex (:N) * dimindex (:M)=dimindex (:M) * dimindex (:N)`]
408 THEN MRESAL_TAC MOD_EQ_0[`i:num`;`dimindex (:N)`][DIMINDEX_NONZERO]
409 THEN MRESAL_TAC DIV_MONO[`i:num`;`dimindex (:M)* dimindex (:N)`;`dimindex (:N)`][DIMINDEX_NONZERO]
410 THEN MP_TAC(ARITH_RULE`i DIV dimindex (:N)<= dimindex (:M)==> i DIV dimindex (:N)= dimindex (:M) \/ SUC(i DIV dimindex (:N))<= dimindex (:M)`)
413 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
414 THEN REPEAT STRIP_TAC)
415 THEN MP_TAC(ARITH_RULE`i = dimindex (:M) * dimindex (:N) + i MOD dimindex (:N) /\ ~(i MOD dimindex (:N)= 0)
416 ==> dimindex (:M) * dimindex (:N)< i`)
418 THEN REMOVE_ASSUM_TAC
419 THEN REMOVE_ASSUM_TAC
420 THEN REMOVE_ASSUM_TAC
421 THEN REMOVE_ASSUM_TAC
422 THEN REMOVE_ASSUM_TAC
423 THEN REMOVE_ASSUM_TAC
424 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
428 ASM_SIMP_TAC[LAMBDA_BETA;]]]]);;
433 let NORM_VECMAT = prove
434 (`!x. i< dimindex(:M) ==> norm(((vecmat i):real^(M,N)finite_product->real^N) x) <= norm x`,
436 SIMP_TAC[SQRT_MONO_LE_EQ; DOT_POS_LE; vector_norm]
438 SIMP_TAC[vecmat; dot; DIMINDEX_FINITE_PRODUCT; LAMBDA_BETA; DIMINDEX_NONZERO;
439 SUM_ADD_SPLIT; REAL_LE_ADDR; SUM_POS_LE; FINITE_NUMSEG;
440 REAL_LE_SQUARE; ARITH_RULE `a+b = b+a:num`;
441 ARITH_RULE `~(d = 0) ==> 1 <= d + 1`;GSYM LE_SUC_LT]
443 THEN MRESA_TAC SUM_OFFSET[`i * dimindex (:N)`;`(\i:num. x$i * (x:real^(M,N)finite_product)$i)`;`1`;`dimindex (:N)`]
444 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ARITH_RULE`A+ B*A=(B+1)*A`])
445 THEN ASSUME_TAC(ARITH_RULE` 1<=1+i * dimindex (:N)/\ 0< 1+i * dimindex (:N)`)
446 THEN MRESAL_TAC LE_MULT2[`SUC i`;`dimindex(:M)`;`dimindex(:N)`;`dimindex(:N)`][ARITH_RULE `dimindex(:N)<=dimindex(:N)`;ADD1]
447 THEN MP_TAC(ARITH_RULE`
448 1<= dimindex (:N)/\ 0< 1+i * dimindex (:N)/\
449 (i + 1) * dimindex (:N) <= dimindex (:M) * dimindex (:N)
450 ==> 1 + i * dimindex (:N)<=dimindex (:M) * dimindex (:N)+1
451 /\ (i + 1) * dimindex (:N) <= dimindex (:M) * dimindex (:N)+1/\
452 1 + i * dimindex (:N)<= (i+1) * dimindex (:N)+1
453 /\ 0< (i+1) * dimindex (:N)`)
454 THEN ASM_SIMP_TAC[DIMINDEX_GE_1]
456 THEN MRESA_TAC SUM_COMBINE_L[`(\i:num. x$i * (x:real^(M,N)finite_product)$i)`;`1`;`1 + i * dimindex (:N)`;`dimindex (:M) * dimindex (:N)`]
457 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
458 THEN MRESA_TAC SUM_COMBINE_R[`(\i:num. x$i * (x:real^(M,N)finite_product)$i)`;`1 + i * dimindex (:N)`;`(i+1) * dimindex (:N)`;`dimindex (:M) * dimindex (:N)`]
459 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
460 THEN MATCH_MP_TAC(REAL_ARITH`&0<= b /\ &0<=c==> a<=b+a+c`)
462 THEN SIMP_TAC[REAL_LE_SQUARE;REAL_LE_ADDR; SUM_POS_LE;FINITE_NUMSEG;]);;
465 let DIST_VECMAT = prove
466 (`!x y. i< dimindex(:M) ==> dist(((vecmat i):real^(M,N)finite_product->real^N) x,(vecmat i) y) <= dist(x,y)`,
467 REWRITE_TAC[dist; GSYM VECMAT_SUB; NORM_VECMAT]);;
470 let DOT_VECMAT = prove_by_refinement( `!x y:real^(M,N)finite_product.
471 sum (0..(dimindex(:M)-1)) (\i. ((vecmat i):real^(M,N)finite_product->real^N) x dot (vecmat i) y) = x dot y`,
472 [ SIMP_TAC[vecmat; dot; LAMBDA_BETA; DIMINDEX_FINITE_PRODUCT;ARITH_RULE `a+b = b+a:num`;]
473 THEN REPEAT STRIP_TAC
474 THEN SUBGOAL_THEN`(\i. sum (1..dimindex (:N))
475 (\i'. (x:real^(M,N)finite_product)$(i' + i * dimindex (:N)) * y$(i' + i * dimindex (:N))))= (\i. sum (1+i * dimindex (:N) ..(i+1)*dimindex (:N))
476 (\i'. x$i' * (y:real^(M,N)finite_product)$i'))`(fun th-> REWRITE_TAC[th]);
477 SIMP_TAC[FUN_EQ_THM;]
479 THEN MRESAL_TAC SUM_OFFSET[`x' * dimindex (:N)`;`(\i'. (x:real^(M,N)finite_product)$(i') * (y:real^(M,N)finite_product)$(i'))`;`1`;`dimindex (:N)`][ARITH_RULE`A+B*A=(B+1)*A`];
480 ABBREV_TAC `n= dimindex (:N)`
481 THEN ABBREV_TAC `m= dimindex (:M)-1`
482 THEN SUBGOAL_THEN`dimindex (:M)= SUC m`(fun th-> REWRITE_TAC[th]);
484 THEN MRESA1_TAC DIMINDEX_GE_1`(:M)`
486 THEN POP_ASSUM MP_TAC
488 SPEC_TAC (`m:num`,`m:num`)
490 ASM_SIMP_TAC[SUM_SING_NUMSEG;ARITH_RULE`1+ 0*n=1 /\ (0+1) *n=n /\ 1 *n=n`;ADD1];
491 MRESA1_TAC Hypermap.GE_1`m':num`
492 THEN MP_TAC(ARITH_RULE`1<= SUC m'==> 0<= SUC m'`)
494 THEN ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;ADD1;ARITH_RULE`a+b = b+a:num`]
495 THEN MRESAL_TAC SUM_COMBINE_R[`(\i:num. (x:real^(M,N)finite_product)$i * (y:real^(M,N)finite_product)$i)`;`1`;`(m'+1) * n`;`(1+ m' +1) *n`][ARITH_RULE`1<= A+1`]
496 THEN POP_ASSUM MATCH_MP_TAC
497 THEN MRESAL_TAC LE_MULT2[`(m' + 1)`;`1+m' + 1`;`dimindex(:N)`;`dimindex(:N)`][ARITH_RULE `dimindex(:N)<=dimindex(:N)/\ a<= 1+a`;ADD1]]);;
500 let NORM_VECMAT_SUM = prove_by_refinement(
501 `!x:real^(M,N)finite_product. norm x <= sum (0..(dimindex(:M)-1)) (\i. norm(((vecmat i):real^(M,N)finite_product->real^N) x)) `,
503 THEN SUBGOAL_THEN`&0<= sum (1..dimindex (:M) * dimindex (:N)) (\i. (x:real^(M,N)finite_product)$i * x$i)` ASSUME_TAC;
504 MATCH_MP_TAC SUM_POS_LE_NUMSEG
505 THEN REPEAT STRIP_TAC
506 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
508 THEN SUBGOAL_THEN`!i. &0<=sum (1..dimindex (:N)) (\i'. vecmat i x$i' * vecmat i (x:real^(M,N)finite_product)$i')` ASSUME_TAC;
510 THEN MATCH_MP_TAC SUM_POS_LE_NUMSEG
511 THEN REPEAT STRIP_TAC
512 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
514 THEN MRESA_TAC DOT_VECMAT[`x:real^(M,N)finite_product`;`x:real^(M,N)finite_product`]
515 THEN POP_ASSUM MP_TAC
516 THEN ASM_SIMP_TAC[vector_norm;dot;DIMINDEX_FINITE_PRODUCT]
518 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
519 THEN ABBREV_TAC `n= dimindex (:N)`
520 THEN ABBREV_TAC `m= dimindex (:M)-1`
521 THEN SUBGOAL_THEN`dimindex (:M)= SUC m`(fun th-> REWRITE_TAC[th] );
523 THEN MRESA1_TAC DIMINDEX_GE_1`(:M)`
525 THEN POP_ASSUM MP_TAC
527 SPEC_TAC (`m:num`,`m:num`)
530 THEN POP_ASSUM(fun th-> MRESA1_TAC th`0`)
531 THEN POP_ASSUM MP_TAC
532 THEN ASM_SIMP_TAC[SUM_SING_NUMSEG;ARITH_RULE`1+ 0*n=1 /\ (0+1) *n=n /\ 1 *n=n /\ 0*n+i=i/\ 0+1=1`;ADD1;vecmat;]
533 THEN REPEAT STRIP_TAC
534 THEN ASM_SIMP_TAC[SQRT_MONO_LE_EQ]
535 THEN MATCH_MP_TAC SUM_LE_NUMSEG
536 THEN REPEAT STRIP_TAC
537 THEN MRESAL_TAC (GEN_ALL INDEX_VECMAT)[`0:num`;`i:num`][ARITH_RULE`0 * n +a=a /\ 0<1 `]
538 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_REFL];
540 THEN DISCH_THEN(LABEL_TAC"THY")
541 THEN REPEAT STRIP_TAC
542 THEN SUBGOAL_THEN`&0 <=
543 sum (0..m') (\i. sum (1..n) (\i'. vecmat i (x:real^(M,N)finite_product)$i' * vecmat i x$i'))` ASSUME_TAC;
544 MATCH_MP_TAC SUM_POS_LE_NUMSEG
545 THEN REPEAT STRIP_TAC
546 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
547 REMOVE_THEN "THY" MP_TAC
548 THEN ASM_REWRITE_TAC[]
550 THEN MRESA1_TAC Hypermap.GE_1`m':num`
551 THEN MP_TAC(ARITH_RULE`1<= SUC m'==> 0<= SUC m'`)
553 THEN ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG]
554 THEN MATCH_MP_TAC REAL_LE_LSQRT
556 MATCH_MP_TAC (REAL_ARITH`&0<=a /\ &0<= b==> &0<= a+b`)
558 THEN MATCH_MP_TAC SUM_POS_LE_NUMSEG
559 THEN REPEAT STRIP_TAC
560 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
562 MATCH_MP_TAC (REAL_ARITH`&0<=a /\ &0<= b==> &0<= a+b`)
564 MATCH_MP_TAC SUM_POS_LE_NUMSEG
565 THEN REPEAT STRIP_TAC
566 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE]
567 THEN MATCH_MP_TAC SQRT_POS_LE
568 THEN MATCH_MP_TAC SUM_POS_LE_NUMSEG
569 THEN REPEAT STRIP_TAC
570 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
571 MATCH_MP_TAC SQRT_POS_LE
572 THEN MATCH_MP_TAC SUM_POS_LE_NUMSEG
573 THEN REPEAT STRIP_TAC
574 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
575 SIMP_TAC[REAL_POW_2; REAL_ARITH
576 ` (x + y) * (x + y) =x*x + y*y + &2 * x * y`;REAL_ARITH
577 `&0 <= y * (y * x * x - x * d) - x * (y * d - x * y * y) <=>
578 x * y * d <= x * y * x * y`]
579 THEN SUBGOAL_THEN`&0<=sum (1..n) (\i'. vecmat (SUC m') x$i' * vecmat (SUC m') (x:real^(M,N)finite_product)
581 MATCH_MP_TAC SUM_POS_LE_NUMSEG
582 THEN REPEAT STRIP_TAC
583 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
584 ASM_SIMP_TAC[GSYM REAL_POW_2;SQRT_POW_2;REAL_ARITH`a+b<=c+b+d<=> a<=c+d`
586 THEN MATCH_MP_TAC(REAL_ARITH`a<=b /\ &0<= c==> a<= b+ &2 * c`)
587 THEN ASM_SIMP_TAC[ REAL_LSQRT_LE;REAL_POW_2]
588 THEN MATCH_MP_TAC REAL_LE_MUL
590 MATCH_MP_TAC SUM_POS_LE_NUMSEG
591 THEN REPEAT STRIP_TAC
592 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE]
593 THEN MATCH_MP_TAC SQRT_POS_LE
594 THEN MATCH_MP_TAC SUM_POS_LE_NUMSEG
595 THEN REPEAT STRIP_TAC
596 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE];
597 MATCH_MP_TAC SQRT_POS_LE
598 THEN MATCH_MP_TAC SUM_POS_LE_NUMSEG
599 THEN REPEAT STRIP_TAC
600 THEN ASM_SIMP_TAC[LAMBDA_BETA;REAL_LE_SQUARE]]);;
603 let BOUNDED_MATVEC = prove
604 (`!s:num->real^N->bool.
605 (!i. 1<=i /\ i <= dimindex(:M) ==> bounded (s i)) ==> bounded {matvec(x:real^N^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i x IN s i)}`,
606 REPEAT GEN_TAC THEN REWRITE_TAC[bounded; IN_ELIM_THM;]
607 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[RIGHT_IMP_EXISTS_THM]
608 THEN REWRITE_TAC[SKOLEM_THM]
610 THEN POP_ASSUM MP_TAC
611 THEN DISCH_THEN(LABEL_TAC"THY")
612 THEN ABBREV_TAC`b=sum (0..(dimindex(:M)-1)) (\i. a (SUC i))`
613 THEN EXISTS_TAC`b:real`
614 THEN REPEAT STRIP_TAC
615 THEN POP_ASSUM MP_TAC
616 THEN POP_ASSUM MP_TAC
617 THEN DISCH_THEN(LABEL_TAC"THY1")
619 THEN ASM_REWRITE_TAC[]
620 THEN MRESA1_TAC NORM_VECMAT_SUM`x:real^(M,N)finite_product`
621 THEN MATCH_MP_TAC(REAL_ARITH`!a B C. a<= B/\ B<= C==> a<= C`)
622 THEN EXISTS_TAC`sum (0..dimindex (:M) - 1) (\i. norm (vecmat i (matvec (x':real^N^M))))`
623 THEN ASM_REWRITE_TAC[]
625 THEN MATCH_MP_TAC SUM_LE_NUMSEG
626 THEN REPEAT STRIP_TAC
627 THEN MP_TAC(ARITH_RULE`i <= dimindex (:M) - 1 /\ 1 <= dimindex (:M) ==> i < dimindex (:M) /\ SUC i <= dimindex (:M) /\ 1<= SUC i`)
628 THEN SIMP_TAC[DIMINDEX_GE_1]
630 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i:num`;`x':real^N^M`]
631 THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`SUC i`)
632 THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th`SUC i`)
633 THEN POP_ASSUM (fun th-> MRESA1_TAC th`row (SUC i) (x':real^N^M)`));;
636 let CLOSED_MATVEC = prove
637 (`!s:num->real^N->bool.
638 (!i. 1<=i /\ i <= dimindex(:M) ==> closed (s i)) ==> closed {matvec(x:real^N^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i x IN s i)}`,
639 REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist]
640 THEN DISCH_THEN(LABEL_TAC"THY")
641 THEN REPEAT STRIP_TAC
642 THEN EXISTS_TAC`vecmats (l:real^(M,N)finite_product)`
643 THEN SIMP_TAC[MATVEC_VECMATS_ID]
644 THEN POP_ASSUM MP_TAC
645 THEN POP_ASSUM MP_TAC
646 THEN REWRITE_TAC[SKOLEM_THM]
648 THEN POP_ASSUM MP_TAC
649 THEN DISCH_THEN(LABEL_TAC"THY1")
650 THEN DISCH_THEN(LABEL_TAC"THY2")
651 THEN REPEAT STRIP_TAC
652 THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th`i:num`)
653 THEN POP_ASSUM MP_TAC
654 THEN DISCH_THEN(LABEL_TAC"THY3")
655 THEN SUBGOAL_THEN`(!n. row i ((x':num->real^N^M) n) IN s i)`ASSUME_TAC
658 THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`n:num`)
660 SUBGOAL_THEN`(!e. &0 < e ==> (?N. !n. N <= n ==> norm (row i ((x':num->real^N^M) n) - row i (vecmats (l:real^(M,N)finite_product))) < e))`ASSUME_TAC
663 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e:real`)
664 THEN POP_ASSUM MP_TAC
665 THEN DISCH_THEN(LABEL_TAC"THY2")
666 THEN EXISTS_TAC`N:num`
667 THEN REPEAT STRIP_TAC
668 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)
669 THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\ SUC(i-1)=i`)
671 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((x':num->real^N^M) n)`]
672 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,N)finite_product)`]
673 THEN POP_ASSUM MP_TAC
674 THEN SIMP_TAC[MATVEC_VECMATS_ID]
676 THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((x':num->real^N^M) n) - (l:real^(M,N)finite_product)`][VECMAT_SUB]
679 REMOVE_THEN "THY3"(fun th-> MRESA_TAC th[`(\n. row i ((x':num->real^N^M) n))`;`row i (vecmats (l:real^(M,N)finite_product))`])]]);;
683 let COMPACT_MATVEC = prove
684 (`!s:num->real^N->bool.
685 (!i. 1<=i /\ i <= dimindex(:M) ==> compact (s i)) ==> compact {matvec(x:real^N^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i x IN s i)}`,
686 SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_MATVEC; CLOSED_MATVEC]);;
690 let CLOSED_BALL_ANNULUS=prove(` closed ball_annulus`,
691 REWRITE_TAC[ball_annulus]
692 THEN MATCH_MP_TAC CLOSED_DIFF
693 THEN SIMP_TAC[CLOSED_CBALL;OPEN_BALL]);;
695 let BOUNDED_BALL_ANNULUS=prove(` bounded ball_annulus`,
696 REWRITE_TAC[ball_annulus]
697 THEN MRESAL_TAC BOUNDED_SUBSET[`(cball (vec 0,&2 * h0) DIFF ball ((vec 0:real^3),&2))`;`cball ((vec 0:real^3),&2 * h0)`][BOUNDED_CBALL]
698 THEN POP_ASSUM MATCH_MP_TAC
702 let COMPACT_BALL_ANNULUS=prove(` compact ball_annulus`,
703 SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_BALL_ANNULUS; CLOSED_BALL_ANNULUS]);;
706 let COMPACT_BALL_ANNULUS_MATVEC=prove(` compact{matvec(v:real^3^M) |(!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus)}`,
707 SIMP_TAC[COMPACT_MATVEC;COMPACT_BALL_ANNULUS]);;
710 let CLOSED_CONDITION1_SY=prove(`closed {matvec(v:real^N^M) |CONDITION1_SY a b v }`,
711 REWRITE_TAC[CONDITION1_SY]
712 THEN REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist]
713 THEN REPEAT STRIP_TAC
714 THEN EXISTS_TAC`vecmats (l:real^(M,N)finite_product)`
715 THEN SIMP_TAC[MATVEC_VECMATS_ID]
716 THEN POP_ASSUM MP_TAC
717 THEN POP_ASSUM MP_TAC
718 THEN REWRITE_TAC[SKOLEM_THM]
720 THEN POP_ASSUM MP_TAC
721 THEN DISCH_THEN(LABEL_TAC"THY1")
722 THEN DISCH_THEN(LABEL_TAC"THY2")
725 THEN SUBGOAL_THEN`((\n. row i (v n) - row j ((v:num->real^N^M) n)) --> row i (vecmats l) - row j (vecmats (l:real^(M,N)finite_product)))
726 sequentially`ASSUME_TAC
728 SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]
729 THEN REPEAT STRIP_TAC
730 THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`]
731 THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`)
733 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e/ &2:real`)
734 THEN POP_ASSUM MP_TAC
735 THEN DISCH_THEN(LABEL_TAC"THY2")
736 THEN EXISTS_TAC`N:num`
737 THEN REPEAT STRIP_TAC
738 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)
739 THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\ SUC(i-1)=i`)
741 THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\ SUC(j-1)=j`)
743 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^N^M) n)`]
744 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,N)finite_product)`]
745 THEN POP_ASSUM MP_TAC
746 THEN SIMP_TAC[MATVEC_VECMATS_ID]
748 THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^N^M) n) - (l:real^(M,N)finite_product)`][VECMAT_SUB]
749 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`((v:num->real^N^M) n)`]
750 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`vecmats (l:real^(M,N)finite_product)`]
751 THEN POP_ASSUM MP_TAC
752 THEN SIMP_TAC[MATVEC_VECMATS_ID]
754 THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`j-1`;`matvec ((v:num->real^N^M) n) - (l:real^(M,N)finite_product)`][VECMAT_SUB]
755 THEN MRESAL_TAC NORM_TRIANGLE[`row i ((v:num->real^N^M) n) - row i (vecmats (l:real^(M,N)finite_product))`;`--(row j ((v:num->real^N^M) n) - row j (vecmats (l:real^(M,N)finite_product)))`][NORM_NEG;VECTOR_ARITH`A+ --B=A-B:real^N` ]
760 MRESA_TAC LIM_NORM_LBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^N^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,N)finite_product))`;`(a:num#num->real)(i,j)`]
761 THEN POP_ASSUM MATCH_MP_TAC
762 THEN SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]
764 THEN REPEAT STRIP_TAC
765 THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`n:num`)
767 MRESA_TAC LIM_NORM_UBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^N^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,N)finite_product))`;`(b:num#num->real)(i,j)`]
768 THEN POP_ASSUM MATCH_MP_TAC
769 THEN SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]
771 THEN REPEAT STRIP_TAC
772 THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`n:num`)
773 THEN ASM_SIMP_TAC[]]]);;
776 let SUC_NOT=prove(`1<k ==> 1 <= SUC (i MOD k) /\
777 SUC (i MOD k) <= k /\
778 ~(i = SUC (i MOD k))` ,
779 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
781 THEN MP_TAC(ARITH_RULE`1 < k==> ~(1=k) /\ ~(k=0)`)
783 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
784 THEN MP_TAC(ARITH_RULE`i MOD k < k==> SUC(i MOD k) <= k`)
786 THEN DISJ_CASES_TAC(ARITH_RULE`i<k \/ k<=i:num`)
788 MRESA_TAC MOD_LT[`i:num`;`k:num`]
791 THEN ABBREV_TAC`m=SUC (i MOD k)`
792 THEN MP_TAC(ARITH_RULE`m <= k /\k <= i /\
795 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th])
796 THEN REPEAT STRIP_TAC
797 THEN POP_ASSUM MP_TAC
798 THEN ASM_REWRITE_TAC[]
799 THEN MRESAL_TAC MOD_MULT[`m:num`;`1:num`][ARITH_RULE`m*1=m/\ SUC 0=1`]]);;
801 let NONPARALLEL_BALL_ANNULUS=prove_by_refinement(`&2<= norm(v-w) /\ norm(v-w)<= cstab /\ v IN ball_annulus /\ w IN ball_annulus
802 ==> ~(collinear ({vec 0} UNION {v,w}))`,
803 [REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`;GSYM NORM_CAUCHY_SCHWARZ_EQUAL;NORM_LE_SQUARE;NORM_LT_SQUARE;]
804 THEN ONCE_REWRITE_TAC[REAL_ARITH`A<=B <=> B >= A`]
805 THEN REWRITE_TAC[NORM_GE_SQUARE;REAL_ARITH`~(&2<= &0) /\ &0 < &2`]
806 THEN ONCE_REWRITE_TAC[REAL_ARITH`A>=B <=> B <= A`]
807 THEN REWRITE_TAC[DOT_RSUB;DOT_LSUB;DOT_SQUARE_NORM]
808 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= v dot w \/ &0<= --(v dot (w:real^3))`);
810 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
812 THEN REPEAT STRIP_TAC
813 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN MP_TAC th)
815 THEN ONCE_REWRITE_TAC[DOT_SYM]
817 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] )
818 THEN REWRITE_TAC[REAL_ARITH`A pow 2 -A*B-(A*B-B pow 2)=(A-B) pow 2`;GSYM REAL_LE_SQUARE_ABS;ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(a<b)<=> b<=a`]
819 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= norm (v:real^3) -norm w \/ &0<= --(norm v -norm (w:real^3))`);
821 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
823 THEN REPEAT STRIP_TAC
824 THEN MP_TAC(REAL_ARITH`norm (v:real^3) <= &2 * h0 /\ &2 <= norm (w:real^3) ==> norm v - norm w <= &2*(h0 - &1)`)
825 THEN ASM_REWRITE_TAC[h0]
829 THEN REWRITE_TAC[GSYM REAL_ABS_REFL;REAL_ABS_NEG]
831 THEN ONCE_REWRITE_TAC[REAL_ARITH`--(A-B)=B-A`]
832 THEN REPEAT STRIP_TAC
833 THEN MP_TAC(REAL_ARITH`norm (w:real^3) <= &2 * h0 /\ &2 <= norm (v:real^3) ==> norm w - norm v <= &2*(h0 - &1)`)
834 THEN ASM_REWRITE_TAC[h0]
838 THEN REWRITE_TAC[GSYM REAL_ABS_REFL;REAL_ABS_NEG]
840 THEN ONCE_REWRITE_TAC[REAL_ARITH`--A=B<=> A= --B`]
841 THEN REPEAT STRIP_TAC
842 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN MP_TAC th)
844 THEN ONCE_REWRITE_TAC[DOT_SYM]
846 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] )
847 THEN REWRITE_TAC[REAL_ARITH`A pow 2 -(--(A*B))-(--(A*B)-B pow 2)=(A+B) pow 2`;GSYM REAL_LE_SQUARE_ABS;ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(a<b)<=> b<=a`]
849 THEN REMOVE_ASSUM_TAC
850 THEN MP_TAC(REAL_ARITH`&0<= norm (v:real^3) /\ &0<= norm (w:real^3)==> &0<= norm v + norm w`)
851 THEN SIMP_TAC[NORM_POS_LE]
852 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
854 THEN REPEAT STRIP_TAC
855 THEN MP_TAC(REAL_ARITH`&2<=norm (w:real^3) /\ &2 <= norm (v:real^3) ==> &4<= norm v + norm w `)
856 THEN ASM_REWRITE_TAC[]
858 THEN REWRITE_TAC[cstab]
859 THEN REAL_ARITH_TAC]);;
861 (* inserted by tch 2013-04-20 *)
863 let NONPARALLEL_BALL_ANNULUS362 =prove_by_refinement(`&2<= norm(v-w) /\ norm(v-w)<= #3.62 /\ v IN ball_annulus /\ w IN ball_annulus
864 ==> ~(collinear ({vec 0} UNION {v,w}))`,
865 [REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`;GSYM NORM_CAUCHY_SCHWARZ_EQUAL;NORM_LE_SQUARE;NORM_LT_SQUARE;]
866 THEN ONCE_REWRITE_TAC[REAL_ARITH`A<=B <=> B >= A`]
867 THEN REWRITE_TAC[NORM_GE_SQUARE;REAL_ARITH`~(&2<= &0) /\ &0 < &2`]
868 THEN ONCE_REWRITE_TAC[REAL_ARITH`A>=B <=> B <= A`]
869 THEN REWRITE_TAC[DOT_RSUB;DOT_LSUB;DOT_SQUARE_NORM]
870 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= v dot w \/ &0<= --(v dot (w:real^3))`);
872 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
874 THEN REPEAT STRIP_TAC
875 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN MP_TAC th)
877 THEN ONCE_REWRITE_TAC[DOT_SYM]
879 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] )
880 THEN REWRITE_TAC[REAL_ARITH`A pow 2 -A*B-(A*B-B pow 2)=(A-B) pow 2`;GSYM REAL_LE_SQUARE_ABS;ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(a<b)<=> b<=a`]
881 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= norm (v:real^3) -norm w \/ &0<= --(norm v -norm (w:real^3))`);
883 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
885 THEN REPEAT STRIP_TAC
886 THEN MP_TAC(REAL_ARITH`norm (v:real^3) <= &2 * h0 /\ &2 <= norm (w:real^3) ==> norm v - norm w <= &2*(h0 - &1)`)
887 THEN ASM_REWRITE_TAC[h0]
891 THEN REWRITE_TAC[GSYM REAL_ABS_REFL;REAL_ABS_NEG]
893 THEN ONCE_REWRITE_TAC[REAL_ARITH`--(A-B)=B-A`]
894 THEN REPEAT STRIP_TAC
895 THEN MP_TAC(REAL_ARITH`norm (w:real^3) <= &2 * h0 /\ &2 <= norm (v:real^3) ==> norm w - norm v <= &2*(h0 - &1)`)
896 THEN ASM_REWRITE_TAC[h0]
900 THEN REWRITE_TAC[GSYM REAL_ABS_REFL;REAL_ABS_NEG]
902 THEN ONCE_REWRITE_TAC[REAL_ARITH`--A=B<=> A= --B`]
903 THEN REPEAT STRIP_TAC
904 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN MP_TAC th)
906 THEN ONCE_REWRITE_TAC[DOT_SYM]
908 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] )
909 THEN REWRITE_TAC[REAL_ARITH`A pow 2 -(--(A*B))-(--(A*B)-B pow 2)=(A+B) pow 2`;GSYM REAL_LE_SQUARE_ABS;ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(a<b)<=> b<=a`]
911 THEN REMOVE_ASSUM_TAC
912 THEN MP_TAC(REAL_ARITH`&0<= norm (v:real^3) /\ &0<= norm (w:real^3)==> &0<= norm v + norm w`)
913 THEN SIMP_TAC[NORM_POS_LE]
914 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
916 THEN REPEAT STRIP_TAC
917 THEN MP_TAC(REAL_ARITH`&2<=norm (w:real^3) /\ &2 <= norm (v:real^3) ==> &4<= norm v + norm w `)
918 THEN ASM_REWRITE_TAC[]
920 THEN REWRITE_TAC[cstab]
921 THEN REAL_ARITH_TAC]);;
924 let VEC0_BALL_ANNULUS=prove_by_refinement(`&2<= norm(v-w) /\ ~(v= vec 0) /\ ~(w= vec 0)
925 /\ v IN ball_annulus /\ w IN ball_annulus
926 /\ z IN aff_ge {vec 0} {v}
927 /\ z IN aff_ge {vec 0} {w}
929 [REWRITE_TAC[ball_annulus;dist;ball;cball;DIFF;IN_ELIM_THM;NORM_NEG;VECTOR_ARITH`vec 0 -A= --A`]
930 THEN REPEAT STRIP_TAC
931 THEN POP_ASSUM MP_TAC
932 THEN POP_ASSUM MP_TAC
933 THEN MRESA_TAC AFF_GE_1_1[`vec 0:real^3`;`v:real^3`]
934 THEN MRESA_TAC AFF_GE_1_1[`vec 0:real^3`;`w:real^3`]
935 THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`t % vec 0 + A=A`]
936 THEN REPEAT STRIP_TAC
937 THEN POP_ASSUM MP_TAC
938 THEN MP_TAC(REAL_ARITH`&0<= t2'==> t2'= &0 \/ &0< t2'`)
941 MP_TAC(REAL_ARITH`&0<= t2 ==> t2= &0 \/ &0< t2`)
945 THEN MP_TAC(SET_RULE`t2 % v = t2' % w:real^3==> inv t2 %(t2 % v)= inv t2 %(t2' %w)`)
946 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
947 THEN MP_TAC(REAL_ARITH`&0< t2 ==> ~(t2= &0)`)
949 THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
950 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C /\ &1 %v=v`]
952 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;VECTOR_ARITH`a%v- v=(a- &1) %v`;NORM_MUL;REAL_ARITH`~(a<b)<=> b<=a`])
953 THEN REPEAT STRIP_TAC
954 THEN MRESA1_TAC REAL_LE_INV_EQ`t2:real`
955 THEN MRESA_TAC REAL_LE_MUL[`inv t2`;`t2':real`]
956 THEN POP_ASSUM MP_TAC
957 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
959 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;VECTOR_ARITH`a%v- v=(a- &1) %v`;NORM_MUL;REAL_ARITH`~(a<b)<=> b<=a`])
960 THEN REPEAT STRIP_TAC
961 THEN MP_TAC(REAL_ARITH`&2 <= norm (w:real^3) /\ (inv t2 * t2') * norm w <= &2 * h0 ==>
962 (inv t2 * t2'- &1) * norm w <= &2 * h0 - &2
965 THEN MP_TAC(REAL_ARITH`&2 <= (inv t2 * t2') * norm w /\ norm w <= &2 * h0
966 ==> (--(inv t2 * t2'- &1)) * norm (w:real^3) <= &2 * h0 - &2`)
968 THEN POP_ASSUM MP_TAC
969 THEN POP_ASSUM MP_TAC
970 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= (inv t2 * t2' - &1)\/ &0<= --(inv t2 * t2' - &1)`)
971 THEN POP_ASSUM MP_TAC
972 THEN REWRITE_TAC[GSYM REAL_ABS_REFL]
974 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;h0])
975 THEN REAL_ARITH_TAC]);;
980 let BALL_ANNULUS_3PONITS_ANGLE= prove_by_refinement(`~(v= vec 0) /\ ~(w= vec 0) /\ ~(v=w)/\
982 /\ v IN ball_annulus /\ w IN ball_annulus
983 ==> &0< cos( angle(v,w,vec 0))`,
984 [REWRITE_TAC[ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(A< &2)<=> &2<= A`]
985 THEN REPEAT STRIP_TAC
986 THEN MRESAL_TAC LAW_OF_COSINES[`w:real^3`;`v:real^3`;`vec 0:real^3`;][dist;VECTOR_ARITH`A- vec 0= A`;
987 NORM_NEG;REAL_ARITH`A=(B+C)-D<=> B+C-A=D`]
988 THEN POP_ASSUM MP_TAC
989 THEN ONCE_REWRITE_TAC[ VECTOR_ARITH`A-B= --(B-A:real^3)`;]
990 THEN REWRITE_TAC[NORM_NEG]
992 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2:real`;`norm(v-w:real^3)`][NORM_POS_LE;REAL_ARITH`&0<= &2`]
993 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2:real`;`norm(w:real^3)`][NORM_POS_LE;REAL_ARITH`&0<= &2`]
994 THEN SUBGOAL_THEN`&0<= &2 * h0` ASSUME_TAC;
997 MRESAL_TAC Trigonometry2.POW2_COND[`norm(v:real^3)`;`&2 * h0:real`;][NORM_POS_LE;REAL_ARITH`&0<= &2`]
998 THEN MP_TAC(REAL_ARITH`&2 pow 2 <= norm (v - w) pow 2 /\
999 &2 pow 2 <= norm (w) pow 2/\ norm v pow 2 <= (&2 * h0) pow 2
1000 ==> &2 pow 2 + &2 pow 2 - (&2 * h0) pow 2 <= norm (v - w:real^3) pow 2 + norm w pow 2 - norm v pow 2`)
1002 THEN SUBGOAL_THEN`&0< &2 pow 2 + &2 pow 2 - (&2 * h0) pow 2`ASSUME_TAC;
1004 THEN REAL_ARITH_TAC;
1005 MP_TAC(REAL_ARITH`&0 < &2 pow 2 + &2 pow 2 - (&2 * h0) pow 2/\ &2 pow 2 + &2 pow 2 - (&2 * h0) pow 2 <=
1006 &2 * norm (v - w) * norm w * cos (angle (v,w,vec 0:real^3))
1007 ==> &0< norm (v - w) * norm w * cos (angle (v,w,vec 0:real^3))`)
1009 THEN MRESA_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`w:real^3`]
1010 THEN MRESAL_TAC REAL_LT_MUL[`inv(norm (v-w:real^3))`;`norm (v - w:real^3) * norm (w:real^3) * cos (angle(v, w, vec 0:real^3))`][REAL_ARITH`A*B*C*D=(A*B)*C*D/\ &1 *A=A`]
1011 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w:real^3`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
1012 THEN MRESAL_TAC REAL_LT_MUL[`inv(norm (w:real^3))`;` norm (w:real^3) * cos (angle(v, w, vec 0:real^3))`][REAL_ARITH`A*B*C=(A*B)*C/\ &1 *A=A`]]);;
1018 let BALL_ANNULUS_3PONITS_NORM_MIN= prove_by_refinement(`~(v= vec 0) /\ ~(w= vec 0) /\ ~(v=w)/\ ~collinear{vec 0,v,w}/\
1020 /\ v IN ball_annulus /\ w IN ball_annulus
1023 /\ a= sqrt(&4 -h0 pow 2)
1024 ==> a <= norm(v-z)`,
1025 [REWRITE_TAC[ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(A< &2)<=> &2<= A`]
1026 THEN REPEAT STRIP_TAC
1027 THEN SUBGOAL_THEN`&0<= &4 -h0 pow 2` ASSUME_TAC;
1029 THEN REAL_ARITH_TAC;
1030 MRESA1_TAC SQRT_WORKS`&4 -h0 pow 2`
1031 THEN MRESAL_TAC Trigonometry2.POW2_COND[`a:real`;`norm(v-z:real^3)`][NORM_POS_LE]
1032 THEN DISJ_CASES_TAC(SET_RULE`z= vec 0 \/ ~((z:real^3)= vec 0)`);
1033 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
1034 THEN REWRITE_TAC[VECTOR_MUL_EQ_0]
1035 THEN REPEAT STRIP_TAC)
1039 SUBGOAL_THEN`angle(v,vec 0,z) =angle(v,vec 0,w:real^3)` ASSUME_TAC;
1040 ASM_SIMP_TAC[ANGLE_EQ;]
1042 THEN SIMP_TAC[VECTOR_ARITH`A- vec 0=A`;DOT_RMUL;NORM_MUL]
1043 THEN MP_TAC(REAL_ARITH`&0< t==> &0<=t`)
1045 THEN MRESA1_TAC REAL_ABS_REFL`t:real`
1046 THEN REAL_ARITH_TAC;
1047 DISJ_CASES_TAC(REAL_ARITH`pi/ &2 < angle(v,vec 0,w:real^3)\/ angle(v,vec 0,w)<= pi/ &2 `);
1048 MRESA_TAC ANGLE_RANGE[`v:real^3`;`vec 0:real^3`;`w:real^3`]
1049 THEN MP_TAC(REAL_ARITH`pi/ &2 < angle(v,vec 0,w) /\ &0< pi
1050 ==> -- pi < angle(v,vec 0,w:real^3)`)
1051 THEN REWRITE_TAC[PI_WORKS]
1053 THEN MRESA1_TAC Trigonometry1.COS_NEGPOS_PI`angle(v, vec 0, w:real^3)`
1054 THEN REMOVE_ASSUM_TAC
1055 THEN REMOVE_ASSUM_TAC
1056 THEN MP_TAC(REAL_ARITH`cos (angle (v,vec 0,w)) < &0 ==> &0<= -- cos (angle (v,vec 0,w:real^3)) `)
1058 THEN MRESAL_TAC LAW_OF_COSINES[`vec 0:real^3`;`v:real^3`;`z:real^3`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG]
1059 THEN MRESAL_TAC REAL_LE_MUL[`norm (z:real^3) `;`-- cos (angle (v,vec 0,w:real^3))`][NORM_POS_LE]
1060 THEN MRESAL_TAC REAL_LE_MUL[`norm (v:real^3) `;`norm (z:real^3) * -- cos (angle (v,vec 0,w:real^3))`][NORM_POS_LE]
1061 THEN MP_TAC(REAL_ARITH`
1062 &0 <= norm v * norm z * --cos (angle (v,vec 0,w))
1063 /\ &0<= norm z pow 2 ==> norm v pow 2 <= (norm v pow 2 + norm z pow 2) -
1064 &2 * norm (v:real^3) * norm (z:real^3) * cos (angle (v,vec 0,w:real^3))`)
1065 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
1067 THEN MATCH_MP_TAC(REAL_ARITH`!A B C. A<=B /\ B<=C==> A<= C`)
1068 THEN EXISTS_TAC`norm (v:real^3) pow 2`
1069 THEN ASM_REWRITE_TAC[]
1070 THEN MATCH_MP_TAC(REAL_ARITH`!A B C. A<=B /\ B<=C==> A<= C`)
1074 THEN REAL_ARITH_TAC;
1075 REWRITE_TAC[REAL_ARITH`&4= &2 pow 2`]
1076 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2:real`;`norm(v:real^3)`][NORM_POS_LE;REAL_ARITH`&0<= &2`];
1078 THEN REWRITE_TAC[REAL_ARITH`A<=B <=> A=B \/ A<B`]
1080 REWRITE_TAC[REAL_ARITH` A=B \/ A<B<=> A<=B `]
1081 THEN MP_TAC(REAL_ARITH`
1082 &0<= norm z pow 2 ==> norm v pow 2 <= (norm (v:real^3) pow 2 + norm (z:real^3) pow 2)`)
1083 THEN ASM_REWRITE_TAC[REAL_LE_POW_2]
1085 THEN MRESAL_TAC LAW_OF_COSINES[`vec 0:real^3`;`v:real^3`;`z:real^3`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG;COS_PI2;REAL_ARITH`a * &0= &0 /\ A- &0=A`]
1086 THEN MATCH_MP_TAC(REAL_ARITH`!A B C. A<=B /\ B<=C==> A<= C`)
1087 THEN EXISTS_TAC`norm (v:real^3) pow 2`
1088 THEN ASM_REWRITE_TAC[]
1089 THEN MATCH_MP_TAC(REAL_ARITH`!A B C. A<=B /\ B<=C==> A<= C`)
1093 THEN REAL_ARITH_TAC;
1094 REWRITE_TAC[REAL_ARITH`&4= &2 pow 2`]
1095 THEN MRESAL_TAC Trigonometry2.POW2_COND[`&2:real`;`norm(v:real^3)`][NORM_POS_LE;REAL_ARITH`&0<= &2`];
1096 REWRITE_TAC[REAL_ARITH` A=B \/ A<B<=> A<=B `]
1097 THEN ABBREV_TAC`t1=norm v * cos(angle(v:real^3,vec 0,w))`
1098 THEN ABBREV_TAC`u= (t1* inv(norm w) ) % w:real^3`
1099 THEN MRESA_TAC ANGLE_RANGE[`v:real^3`;`vec 0:real^3`;`w:real^3`]
1100 THEN MP_TAC(REAL_ARITH`&0 <= angle(v,vec 0,w) /\ &0< pi
1101 ==> -- pi < angle(v,vec 0,w:real^3) /\ -- (pi/ &2) < angle(v,vec 0,w:real^3)`)
1102 THEN REWRITE_TAC[PI_WORKS]
1104 THEN MRESA1_TAC Trigonometry1.COS_NEGPOS_PI`angle(v, vec 0, w:real^3)`
1105 THEN MRESA1_TAC NORM_POS_LT`v:real^3`
1106 THEN MRESA_TAC REAL_LT_MUL[`norm (v:real^3)`;`cos (angle(v, vec 0, w:real^3))`]
1107 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w:real^3`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
1108 THEN MRESA_TAC REAL_LT_MUL[`t1:real`;`inv (norm (w:real^3))`]
1109 THEN ABBREV_TAC`t2=norm (v-w) * cos(angle(v:real^3,w,vec 0))`
1110 THEN MRESAL_TAC (GEN_ALL BALL_ANNULUS_3PONITS_ANGLE)[`v:real^3`;`w:real^3`][ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(A< &2)<=> &2<= A`]
1111 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
1112 THEN MRESA_TAC REAL_LT_MUL[`norm (v-w:real^3)`;`cos (angle(v,w, vec 0:real^3))`]
1113 THEN SUBGOAL_THEN`~(u= vec 0:real^3)` ASSUME_TAC;
1115 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
1116 THEN REWRITE_TAC[VECTOR_MUL_EQ_0]
1117 THEN REPEAT STRIP_TAC)
1121 SUBGOAL_THEN`angle(v,vec 0,u) =angle(v,vec 0,w:real^3)` ASSUME_TAC;
1122 ASM_SIMP_TAC[ANGLE_EQ;]
1124 THEN SIMP_TAC[VECTOR_ARITH`A- vec 0=A`;DOT_RMUL;NORM_MUL]
1125 THEN MP_TAC(REAL_ARITH`&0< t1 * inv(norm (w:real^3))==> &0<= t1 * inv(norm (w:real^3))`)
1127 THEN MRESA1_TAC REAL_ABS_REFL`t1 * inv(norm(w:real^3)):real`
1128 THEN REAL_ARITH_TAC;
1129 SUBGOAL_THEN`norm (v-u:real^3)= norm v * sin(angle(v, vec 0, w:real^3))` ASSUME_TAC;
1130 MRESAL_TAC REAL_LE_MUL[`norm (v:real^3)`;`sin(angle(v, vec 0, w:real^3))`][SIN_ANGLE_POS;NORM_POS_LE]
1131 THEN MRESAL_TAC Trigonometry2.EQ_POW2_COND[`norm (v-u:real^3)`;`norm v * sin(angle(v, vec 0, w:real^3))`][NORM_POS_LE]
1132 THEN MRESAL_TAC LAW_OF_COSINES[`vec 0:real^3`;`v:real^3`;`u:real^3`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG;COS_PI2;REAL_ARITH`a * &0= &0 /\ A- &0=A/\ (A*B) pow 2= A pow 2* B pow 2`]
1134 THEN REWRITE_TAC[NORM_MUL]
1135 THEN MP_TAC(REAL_ARITH`&0 < t1 * inv (norm w) ==> &0 <= t1 * inv (norm (w:real^3))`)
1137 THEN MRESA1_TAC REAL_ABS_REFL`t1 * inv(norm(w:real^3)):real`
1138 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ A * &1=A/\ A*B*C*D*E= A*B*E*(C*D)`]
1140 THEN REWRITE_TAC[REAL_ARITH`(norm v pow 2 + (norm v * cos (angle (v,vec 0,w))) pow 2) -
1141 &2 * norm v * (norm v * cos (angle (v,vec 0,w))) * cos (angle (v,vec 0,w))
1142 = norm v pow 2 *(&1 - cos (angle (v,vec 0,w)) pow 2)`]
1143 THEN SIMP_TAC[Trigonometry2.COS_POW2_INTER]
1144 THEN REAL_ARITH_TAC;
1145 SUBGOAL_THEN`angle(v,u,vec 0:real^3) =pi/ &2` ASSUME_TAC;
1146 MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`vec 0:real^3`;][dist;VECTOR_ARITH`A- vec 0= A`;NORM_NEG;COS_PI2;REAL_ARITH`a * &0= &0 /\ A- &0=A/\ (A*B) pow 2= A pow 2* B pow 2`]
1147 THEN POP_ASSUM MP_TAC
1148 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
1149 THEN ASM_REWRITE_TAC[NORM_NEG]
1151 THEN REWRITE_TAC[NORM_MUL]
1152 THEN MP_TAC(REAL_ARITH`&0 < t1 * inv (norm w) ==> &0 <= t1 * inv (norm (w:real^3))`)
1154 THEN MRESA1_TAC REAL_ABS_REFL`t1 * inv(norm(w:real^3)):real`
1155 THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B)*C=A*(B*C)/\ A * &1=A/\ A*B*C*D*E= A*B*E*(C*D)`]
1156 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v:real^3`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
1158 THEN SIMP_TAC[Trigonometry2.COS_POW2_INTER;REAL_ARITH`(A*B)pow 2=A pow 2 * B pow 2`;REAL_ARITH`norm v pow 2 =
1159 (norm v pow 2 * sin (angle (v,vec 0,w)) pow 2 +
1160 norm v pow 2 * (&1 - sin (angle (v,vec 0,w)) pow 2)) -
1163 (norm v * cos (angle (v,vec 0,w))) *
1164 cos (angle (v,u,vec 0)) *
1165 sin (angle (v,vec 0,w))
1168 (norm v * cos (angle (v,vec 0,w))) *
1169 cos (angle (v,u,vec 0)) *
1170 sin (angle (v,vec 0,w))= &0`;]
1171 THEN ASM_REWRITE_TAC[REAL_ENTIRE]
1172 THEN MP_TAC(REAL_ARITH`angle (v,vec 0,w) < pi / &2 /\ &0<= angle (v,vec 0,w)
1173 ==> ~((angle (v,vec 0,w) = --(pi / &2) \/ angle (v,vec 0,w:real^3) = pi / &2))`)
1175 THEN ASM_SIMP_TAC[SIN_ANGLE_EQ_0]
1176 THEN MRESA_TAC COLLINEAR_ANGLE[`v:real^3`;`vec 0:real^3`;`w:real^3`]
1177 THEN POP_ASSUM MP_TAC
1178 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
1180 THEN MRESA_TAC ANGLE_RANGE[`v:real^3`;`u:real^3`;`vec 0:real^3`;]
1181 THEN MP_TAC(REAL_ARITH`&0 <= angle(v,u,vec 0) /\ &0< pi
1182 ==> -- pi < angle(v,u,vec 0:real^3) /\ ~( angle(v,u,vec 0:real^3)= -- (pi/ &2))`)
1183 THEN REWRITE_TAC[PI_WORKS]
1185 THEN MRESA1_TAC Trigonometry1.COS_NEGPOS_PI`angle(v, u,vec 0:real^3)`;
1186 SUBGOAL_THEN`collinear{vec 0, u, w:real^3}` ASSUME_TAC;
1187 ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1188 THEN ASM_REWRITE_TAC[COLLINEAR_LEMMA]
1189 THEN EXISTS_TAC`t1 * inv(norm (w:real^3))`
1190 THEN ASM_SIMP_TAC[];
1191 SUBGOAL_THEN`~(u=w:real^3)` ASSUME_TAC;
1193 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
1194 THEN REPEAT STRIP_TAC)
1195 THEN REMOVE_ASSUM_TAC
1196 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;COS_PI2])
1197 THEN REAL_ARITH_TAC;
1198 SUBGOAL_THEN `angle(u, vec 0, w:real^3)= &0` ASSUME_TAC;
1199 MRESA_TAC ANGLE_EQ[`u:real^3`;`vec 0:real^3`;`w:real^3`;`w:real^3`;`vec 0:real^3`;`w:real^3`]
1200 THEN POP_ASSUM MP_TAC
1201 THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`]
1203 THEN SIMP_TAC[DOT_LMUL;NORM_MUL]
1204 THEN MP_TAC(REAL_ARITH`&0 < t1 * inv (norm w) ==> &0 <= t1 * inv (norm (w:real^3))`)
1206 THEN MRESA1_TAC REAL_ABS_REFL`t1 * inv(norm(w:real^3)):real`
1207 THEN ASM_REWRITE_TAC[REAL_ARITH`(w dot w) * ((t1 * inv (norm w)) * norm w) * norm w =
1208 ((t1 * inv (norm w)) * (w dot w)) * norm w * norm w`]
1210 THEN ASM_SIMP_TAC[ANGLE_REFL_MID];
1211 MRESA_TAC COLLINEAR_ANGLE[`vec 0:real^3`;`u:real^3`;`w:real^3`];
1212 MRESA_TAC (GEN_ALL ANGLE_EQ_0_LEFT)[`v:real^3`;`vec 0:real^3`;`u:real^3`;`w:real^3`;]
1213 THEN POP_ASSUM(fun th -> ASSUME_TAC(SYM th) )
1214 THEN MRESA_TAC TRIANGLE_ANGLE_SUM[`v:real^3`;`u:real^3`;`w:real^3`;]
1215 THEN MP_TAC(REAL_ARITH`pi / &2 = angle (v,u,w)
1216 /\ &0<= angle (u,v,w) /\ &0<= angle (v,u,w) /\ &0<= angle (u,w,v)/\
1217 angle (u,v,w) + angle (v,u,w) + angle (u,w,v:real^3) = pi
1218 ==> angle (u,w,v) <= pi/ &2`)
1219 THEN ASM_SIMP_TAC[ANGLE_RANGE]
1220 THEN MRESAL_TAC TRIANGLE_ANGLE_SUM[`vec 0:real^3`;`u:real^3`;`w:real^3`;][REAL_ARITH`&0+ A=A`]
1221 THEN MRESAL_TAC (GEN_ALL ANGLE_EQ_PI_LEFT)[`v:real^3`;`u:real^3`;`w:real^3`;`vec 0:real^3`][REAL_ARITH`A- B<= A/ &2 <=> A/ &2 <=B`]
1222 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1223 THEN MRESA_TAC ANGLE_RANGE[`v:real^3`;`w:real^3`;`vec 0:real^3`;]
1224 THEN MP_TAC(REAL_ARITH`&0 <= angle(v,w,vec 0) /\ &0< pi
1225 ==> -- pi < angle(v,w,vec 0:real^3) /\ ~( angle(v,w,vec 0:real^3)= -- (pi/ &2))`)
1226 THEN REWRITE_TAC[PI_WORKS]
1228 THEN MRESA1_TAC Trigonometry1.COS_NEGPOS_PI`angle(v, w:real^3, vec 0)`
1229 THEN POP_ASSUM MP_TAC
1230 THEN REAL_ARITH_TAC;
1231 MRESAL_TAC (GEN_ALL ANGLE_EQ_PI_LEFT)[`v:real^3`;`vec 0:real^3`;`u:real^3`;`w:real^3`][REAL_ARITH`A- B<= A/ &2 <=> A/ &2 <=B`]
1232 THEN POP_ASSUM MP_TAC
1233 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1234 THEN ASM_REWRITE_TAC[REAL_ARITH`A/ &2= A- B<=> B= A/ &2`]
1236 THEN SUBGOAL_THEN`norm(v- u)<= norm(v-z:real^3)`ASSUME_TAC;
1237 DISJ_CASES_TAC(SET_RULE`z=u \/ ~(u=z:real^3)`);
1239 THEN REAL_ARITH_TAC;
1240 SUBGOAL_THEN`collinear{vec 0, u,z:real^3}`ASSUME_TAC;
1241 ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1242 THEN ASM_REWRITE_TAC[COLLINEAR_LEMMA]
1244 THEN EXISTS_TAC`t1 * inv(norm (w:real^3)) * inv t`
1245 THEN SIMP_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`;REAL_ARITH`(A*B*C)*D=A*B*(C*D)`]
1246 THEN MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`)
1248 THEN MRESAL1_TAC REAL_MUL_LINV`t:real`[REAL_ARITH`A* &1=A`];
1249 SUBGOAL_THEN`angle(v,u,z:real^3) = pi/ &2` ASSUME_TAC;
1250 MRESA_TAC COLLINEAR_ANGLE[`vec 0:real^3`;`u:real^3`;`z:real^3`];
1251 MRESA_TAC (GEN_ALL ANGLE_EQ_0_LEFT)[`v:real^3`;`vec 0:real^3`;`u:real^3`;`z:real^3`;];
1252 MRESAL_TAC (GEN_ALL ANGLE_EQ_PI_LEFT)[`v:real^3`;`vec 0:real^3`;`u:real^3`;`z:real^3`][REAL_ARITH`A- B<= A/ &2 <=> A/ &2 <=B`]
1253 THEN POP_ASSUM MP_TAC
1254 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1255 THEN ASM_REWRITE_TAC[REAL_ARITH`A/ &2= A-B<=> B=A/ &2`]
1257 THEN ONCE_REWRITE_TAC[ANGLE_SYM]
1258 THEN ASM_REWRITE_TAC[];
1259 MRESAL_TAC Collect_geom.POW2_COND[`norm(v- u:real^3)`;`norm(v-z:real^3)`][NORM_POS_LE]
1260 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`z:real^3`;][dist;VECTOR_ARITH`A- vec 0= A`;NORM_NEG;COS_PI2;REAL_ARITH`a * &0= &0 /\ A- &0=A/\ (A*B) pow 2= A pow 2* B pow 2`]
1261 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
1262 THEN ASM_REWRITE_TAC[NORM_NEG; REAL_ARITH`(A*B) pow 2= A pow 2 * B pow 2`;REAL_ARITH`A<=A+B<=> &0<=B`]
1263 THEN MRESAL_TAC Collect_geom.POW2_COND[`&0`;`norm(z-u:real^3)`][NORM_POS_LE;REAL_ARITH`&0<= &0/\ &0 pow 2= &0`];
1264 MRESAL_TAC Collect_geom.POW2_COND[`norm(v-u:real^3)`;`norm(v-z:real^3)`][NORM_POS_LE]
1265 THEN MATCH_MP_TAC(REAL_ARITH`!A B C. A<=B /\ B<= C==> A<= C`)
1266 THEN EXISTS_TAC`norm(v- u:real^3) pow 2`
1267 THEN ASM_REWRITE_TAC[]
1268 THEN MRESAL_TAC ANGLE_EQ_PI_DIST[`vec 0:real^3`;`u:real^3`;`w:real^3`][dist;VECTOR_ARITH`vec 0-A= -- A`;NORM_NEG]
1269 THEN MP_TAC(REAL_ARITH`norm w = norm u + norm (u - w:real^3)
1270 /\ &0<= norm u /\ &0<= norm (u - w:real^3) /\ norm w<= &2 * h0
1271 ==> norm u<= h0 \/ norm (u - w:real^3)<= h0`)
1272 THEN ASM_REWRITE_TAC[NORM_POS_LE]
1275 THEN POP_ASSUM MP_TAC
1276 THEN POP_ASSUM MP_TAC
1277 THEN POP_ASSUM MP_TAC
1278 THEN POP_ASSUM MP_TAC
1279 THEN POP_ASSUM MP_TAC
1280 THEN POP_ASSUM MP_TAC
1281 THEN POP_ASSUM MP_TAC
1282 THEN POP_ASSUM MP_TAC
1283 THEN POP_ASSUM MP_TAC
1284 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC)
1285 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`vec 0:real^3`;][dist;VECTOR_ARITH`A- vec 0= A`;NORM_NEG;COS_PI2;REAL_ARITH`a * &0= &0 /\ A- &0=A/\ (A*B) pow 2= A pow 2* B pow 2 `;REAL_ARITH`A=B+C<=>B=A-C`]
1286 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`;]
1287 THEN ASM_REWRITE_TAC[NORM_NEG]
1288 THEN MRESAL_TAC Collect_geom.POW2_COND[`&2`;`norm(v:real^3)`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
1289 THEN MRESAL_TAC Collect_geom.POW2_COND[`norm(u:real^3)`;`h0`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
1290 THEN POP_ASSUM MP_TAC
1291 THEN POP_ASSUM MP_TAC
1292 THEN REWRITE_TAC[h0;]
1293 THEN REAL_ARITH_TAC;
1295 THEN POP_ASSUM MP_TAC
1296 THEN POP_ASSUM MP_TAC
1297 THEN POP_ASSUM MP_TAC
1298 THEN POP_ASSUM MP_TAC
1299 THEN POP_ASSUM MP_TAC
1300 THEN POP_ASSUM MP_TAC
1301 THEN POP_ASSUM MP_TAC
1302 THEN POP_ASSUM MP_TAC
1303 THEN POP_ASSUM MP_TAC
1304 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC)
1305 THEN MRESAL_TAC LAW_OF_COSINES[`u:real^3`;`v:real^3`;`w:real^3`;][dist;VECTOR_ARITH`A- vec 0= A`;NORM_NEG;COS_PI2;REAL_ARITH`a * &0= &0 /\ A- &0=A/\ (A*B) pow 2= A pow 2* B pow 2 `;REAL_ARITH`A=B+C<=>B=A-C`]
1306 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`;]
1307 THEN ASM_REWRITE_TAC[NORM_NEG]
1308 THEN MRESAL_TAC Collect_geom.POW2_COND[`&2`;`norm(v-w:real^3)`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
1309 THEN MRESAL_TAC Collect_geom.POW2_COND[`norm(u-w:real^3)`;`h0`][NORM_POS_LE;REAL_ARITH`&0 <= &2 `]
1310 THEN POP_ASSUM MP_TAC
1311 THEN POP_ASSUM MP_TAC
1312 THEN REWRITE_TAC[h0;]
1313 THEN REAL_ARITH_TAC]);;
1315 let BALL_ANNULUS_4PONITS_AFF_GT=prove(` ~collinear {vec 0, v, z}
1316 /\ ~collinear {vec 0, w, z} /\
1317 &2<= norm(v-w) /\ norm(v-w)<= cstab /\ &2<= norm(z-v) /\ &2<= norm(z-w)
1318 /\ v IN ball_annulus /\ w IN ball_annulus
1319 /\ z IN ball_annulus
1320 ==> ~ (z IN aff_gt {vec 0} {v,w})`,
1321 REWRITE_TAC[ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(A< &2)<=> &2<= A`]
1322 THEN REPEAT STRIP_TAC
1323 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`z:real^3`]
1324 THEN MRESA_TAC th3[`v:real^3`;`vec 0:real^3`;`z:real^3`]
1325 THEN POP_ASSUM MP_TAC
1327 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
1329 THEN MRESA_TAC th3[`vec 0:real^3`;`w:real^3`;`z:real^3`]
1330 THEN MRESA_TAC th3[`w:real^3`;`vec 0:real^3`;`z:real^3`]
1331 THEN POP_ASSUM MP_TAC
1333 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
1335 THEN MRESAL_TAC Planarity.scale_in_edges_fan[`vec 0:real^3`;`v:real^3`;`w:real^3`;`z:real^3`][SET_RULE`DISJOINT {A}{B,C}<=> ~(B=A) /\ ~(C=A)`;VECTOR_ARITH`A-vec 0=A`]
1336 THEN MRESA_TAC (GEN_ALL BALL_ANNULUS_3PONITS_NORM_MIN)[`z:real^3`;`a:real`;`sqrt (&4 - h0 pow 2)`;`v:real^3`;`a % z:real^3`]
1337 THEN POP_ASSUM MP_TAC
1339 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
1340 THEN ASM_REWRITE_TAC[ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(A< &2)<=> &2<= A`;VECTOR_ARITH`((&1 - t) % v + t % w) - v= t%(w-v)`;NORM_MUL]
1341 THEN MRESA1_TAC (GEN_ALL Trigonometry2.LT_IMP_ABS_REFL)`t:real`
1342 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
1343 THEN REWRITE_TAC[NORM_NEG]
1345 THEN MRESA_TAC (GEN_ALL BALL_ANNULUS_3PONITS_NORM_MIN)[`z:real^3`;`a:real`;`sqrt (&4 - h0 pow 2)`;`w:real^3`;`a % z:real^3`]
1346 THEN POP_ASSUM MP_TAC
1348 THEN ONCE_REWRITE_TAC[VECTOR_ARITH`A-B= --(B-A):real^3`]
1349 THEN ASM_REWRITE_TAC[ball_annulus;IN_ELIM_THM;DIFF;ball;cball;dist;VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;REAL_ARITH`~(A< &2)<=> &2<= A`;VECTOR_ARITH`((&1 - t) % v + t % w) - w= (&1-t)%(v-w)`;NORM_MUL]
1350 THEN MP_TAC(REAL_ARITH`t< &1==> &0< &1- t`)
1352 THEN MRESA1_TAC (GEN_ALL Trigonometry2.LT_IMP_ABS_REFL)`&1- t:real`
1354 THEN MP_TAC(REAL_ARITH`sqrt (&4 - h0 pow 2) <= t * norm (v - w)
1355 /\ sqrt (&4 - h0 pow 2) <= (&1 - t) * norm (v - w)
1356 /\ norm (v - w:real^3) <=cstab
1357 ==> &2 * sqrt (&4 - h0 pow 2) <= cstab`)
1359 THEN SUBGOAL_THEN`&0<= cstab` ASSUME_TAC
1360 THENL[REWRITE_TAC[cstab]
1361 THEN REAL_ARITH_TAC;
1362 SUBGOAL_THEN`&0<= &4 -h0 pow 2` ASSUME_TAC
1365 THEN REAL_ARITH_TAC;
1366 MRESA1_TAC SQRT_WORKS`&4 -h0 pow 2`
1367 THEN MP_TAC(REAL_ARITH`&0<= sqrt(&4- h0 pow 2)==> &0<= &2 * sqrt(&4- h0 pow 2) `)
1369 THEN MRESAL_TAC Collect_geom.POW2_COND[`&2 * sqrt (&4 - h0 pow 2)`;`cstab`][REAL_ARITH`(A*B)pow 2= A pow 2 * B pow 2`]
1370 THEN POP_ASSUM MP_TAC
1371 THEN REWRITE_TAC[h0; cstab]
1372 THEN REAL_ARITH_TAC]]);;
1374 let AFF_INTER_AFF_GT_EQ_EMPTY=prove(`~collinear {x,y,z:real^3} ==> aff {x,y} INTER aff_gt{x} {y,z}={}`,
1376 THEN MRESA_TAC th3[`x:real^3`;`y:real^3`;`z:real^3`]
1377 THEN ASM_SIMP_TAC[INTER;EXTENSION;IN_ELIM_THM;affine_hull_2_fan;AFF_GT_1_2]
1382 THEN POP_ASSUM MP_TAC
1383 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1 % x + t2 % v = t1' % x + t2' % v + t3 % w <=> t3 % w = (t1 - t1') % x + (t2 -t2') % v`]
1384 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1385 THEN REMOVE_ASSUM_TAC
1386 THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM(th);REAL_ARITH`a+b+c=d+e <=> c = (d-a)+ (e-b)`])
1387 THEN DISCH_TAC THEN MP_TAC(REAL_ARITH`&0 < (t3:real) ==> ~(t3= &0)`)
1388 THEN ASM_REWRITE_TAC[]THEN DISCH_TAC
1389 THEN MP_TAC(ISPEC`t3:real`REAL_MUL_LINV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1391 THEN MP_TAC(SET_RULE` (t3:real) = (t1- t1') + (t2-t2') ==> (inv t3) *(t3:real) = (inv t3) * ((t1- t1')+ (t2-t2'))`)
1392 THEN ASM_REWRITE_TAC[REAL_ARITH`a*(b+c)= a *b + a*c`] THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
1393 THEN DISCH_TAC THEN DISCH_TAC
1394 THEN MP_TAC(SET_RULE` (t3:real) % z= (t1- t1') % (x:real^3) + (t2-t2') % y ==> (inv t3) % ((t3:real)% z) = (inv t3) % ((t1- t1') %x+ (t2-t2') % y)`)
1395 THEN ASM_REWRITE_TAC[VECTOR_ARITH`m% (n% p)=a%(b % x + c % v)<=> (m*n) %p = (a *b)%x + (a*c)% v`]
1396 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
1397 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(SYM(th))) THEN REWRITE_TAC[VECTOR_ARITH`&1 %w=w`]
1399 THEN SUBGOAL_THEN`z IN aff{(x:real^3),y}` ASSUME_TAC
1401 SIMP_TAC[INTER;EXTENSION;IN_ELIM_THM;affine_hull_2_fan;AFF_GT_1_2]
1402 THEN EXISTS_TAC`inv t3 * (t1-t1')` THEN EXISTS_TAC`inv t3 * (t2-t2')`
1403 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1404 THEN POP_ASSUM(fun th-> REWRITE_TAC[th]);
1410 let AFF_GE_INTER_AFF_GT_EQ_EMPTY=prove_by_refinement(`~collinear {x,y,z:real^3}/\ ~(x=u)/\ ~(u IN aff_gt {x} {y,z}) ==> aff_ge {x} {u} INTER aff_gt{x} {y,z}={}`,
1412 THEN MRESA_TAC th3[`x:real^3`;`y:real^3`;`z:real^3`]
1413 THEN ASM_SIMP_TAC[INTER;EXTENSION;IN_ELIM_THM;AFF_GE_1_1;AFF_GT_1_2]
1417 THEN POP_ASSUM MP_TAC
1418 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1 % x + t2 % u = t1' % x + t2' % v + t3 % w <=> t2 % u = (t1' - t1) % x + t2' % v +t3 %w`]
1419 THEN MP_TAC(REAL_ARITH`&0 < (t3:real) ==> ~(t3= &0)`)
1420 THEN RESA_TAC THEN MP_TAC(ISPEC`t3:real`REAL_MUL_LINV)
1422 THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0< t2`)
1424 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;VECTOR_ARITH`&0 % A= vec 0`;VECTOR_ARITH`vec 0=A+B+C<=> C= -- A -B`] THEN REPEAT STRIP_TAC)
1425 THEN MP_TAC(SET_RULE` (t3:real) % z= --((t1'- t1) % (x:real^3)) - t2' % y ==> (inv t3) % ((t3:real)% z) = (inv t3) % (--((t1'- t1) %x) - t2' % y)`)
1426 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
1427 THEN ASM_REWRITE_TAC[VECTOR_ARITH`(A%B%C=(A*B)%C) /\ &1 %C=C`]
1428 THEN DISCH_TAC THEN SUBGOAL_THEN`z IN aff{(x:real^3),y}` ASSUME_TAC;
1429 SIMP_TAC[INTER;EXTENSION;IN_ELIM_THM;affine_hull_2_fan;AFF_GT_1_2]
1430 THEN EXISTS_TAC`-- inv t3 * (t1'-t1)` THEN EXISTS_TAC`-- inv t3 * t2'`
1431 THEN ASM_REWRITE_TAC[REAL_ARITH`--inv t3 * (t1' - t1) + --inv t3 * t2'
1432 = (inv t3) *(t3 +(t1+ &0)-(t1'+t2'+t3)) /\ A+ &1 - &1=A`]
1433 THEN VECTOR_ARITH_TAC;
1435 THEN ASM_REWRITE_TAC[];
1436 MP_TAC(REAL_ARITH`&0 < (t2:real) ==> ~(t2= &0)`)
1437 THEN RESA_TAC THEN MP_TAC(ISPEC`t2:real`REAL_MUL_LINV)
1440 THEN MP_TAC(SET_RULE` t2 % u = (t1' - t1) % x + t2' % y + t3 % z ==> (inv t2) % ((t2:real)% u) = (inv t2) % ((t1' - t1) % x + t2' % y + t3 % z:real^3)`)
1441 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
1442 THEN ASM_REWRITE_TAC[VECTOR_ARITH`(A%B%C=(A*B)%C) /\ &1 %C=C`]
1443 THEN DISCH_TAC THEN SUBGOAL_THEN`u IN aff_gt{(x:real^3)}{y,z}` ASSUME_TAC;
1444 POP_ASSUM(fun th-> REWRITE_TAC[th])
1445 THEN ASM_SIMP_TAC[INTER;EXTENSION;IN_ELIM_THM;affine_hull_2_fan;AFF_GT_1_2]
1446 THEN EXISTS_TAC`inv t2 *(t1' - t1):real`
1447 THEN EXISTS_TAC`inv t2 *t2':real`
1448 THEN EXISTS_TAC`inv t2 *t3:real`
1449 THEN ASM_REWRITE_TAC[VECTOR_ARITH`inv t2 % ((t1' - t1) % x + t2' % y + t3 % z) =
1450 (inv t2 * (t1' - t1)) % x + (inv t2 * t2') % y + (inv t2 * t3) % z`;
1451 REAL_ARITH`inv t2 * (t1' - t1) + inv t2 * t2' + inv t2 * t3
1452 =inv t2 * (t2+(t1'+t2'+t3) - (t1+t2))/\ A + &1 - &1=A`]
1453 THEN MRESA1_TAC REAL_LT_INV`t2:real`
1454 THEN ASM_SIMP_TAC[REAL_LT_MUL];
1456 THEN ASM_SIMP_TAC[];
1463 let CONTINUOUS_ON_LIFT_PRODUCT=prove(`!k:num. (!i. i IN 1..k==> (lift o (c i)) continuous_on s)
1464 ==> (lift o(\x. product (1..k) (\i. c i x))) continuous_on s`,
1467 SIMP_TAC[PRODUCT_CLAUSES_NUMSEG;ARITH_RULE`~(1=0)`;LIFT_NUM; o_DEF;CONTINUOUS_ON_CONST;];
1468 ASM_SIMP_TAC[PRODUCT_CLAUSES_NUMSEG;FINITE_INSERT;ARITH_RULE`1<= SUC K`]
1469 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
1470 THEN REPEAT STRIP_TAC
1471 THEN ASM_SIMP_TAC[o_DEF;LIFT_CMUL;IN_NUMSEG]
1472 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
1473 THEN POP_ASSUM MP_TAC
1474 THEN POP_ASSUM MP_TAC
1475 THEN ASM_SIMP_TAC[o_DEF;LIFT_CMUL;IN_NUMSEG]
1476 THEN DISCH_THEN(LABEL_TAC"THY")
1478 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC k`[ARITH_RULE`1<= SUC A /\ SUC A<= SUC A`] THEN ASSUME_TAC th)
1479 THEN REMOVE_THEN "THY" MATCH_MP_TAC
1480 THEN POP_ASSUM MP_TAC
1481 THEN DISCH_THEN(LABEL_TAC"THY")
1482 THEN REPEAT STRIP_TAC
1483 THEN REMOVE_THEN "THY" MATCH_MP_TAC
1484 THEN ASM_REWRITE_TAC[]
1485 THEN POP_ASSUM MP_TAC
1489 let CONTINUOUS_ON_DET= prove_by_refinement(`!s:real^(M,M)finite_product->bool. (lift o (\y. det(vecmats y))) continuous_on s`,
1491 THEN SIMP_TAC[det;o_DEF;LIFT_SUM;LIFT_CMUL;FINITE_PERMUTATIONS;FINITE_NUMSEG;]
1492 THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM
1493 THEN SIMP_TAC[FINITE_PERMUTATIONS;FINITE_NUMSEG;]
1494 THEN X_GEN_TAC `p:num->num`
1495 THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC
1496 THEN DISJ_CASES_TAC(SET_RULE`evenperm (p:num->num) \/ ~(evenperm p)`)
1497 THEN ASM_REWRITE_TAC[sign]
1498 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
1499 THEN SIMP_TAC[LIFT_NUM; o_DEF;CONTINUOUS_ON_CONST;]
1500 THEN MRESAL_TAC (GEN_ALL CONTINUOUS_ON_LIFT_PRODUCT)[`(\i. (\x:real^(M,M)finite_product. vecmats (x)$i$p i))`;`s:real^(M,M)finite_product->bool`;`dimindex (:M)`][o_DEF;]
1501 THEN POP_ASSUM MATCH_MP_TAC
1502 THEN REPEAT STRIP_TAC
1503 THEN ASM_SIMP_TAC[vecmats;CONTINUOUS_ON_LIFT_COMPONENT;PERMUTES_IN_NUMSEG;LAMBDA_BETA;LAMBDA_BETA_PERM;]
1504 THEN MRESA_TAC PERMUTES_IN_NUMSEG[`p:num->num`;`dimindex (:M)`;`i:num`]
1505 THEN POP_ASSUM MP_TAC
1506 THEN POP_ASSUM MP_TAC
1507 THEN POP_ASSUM MP_TAC
1508 THEN REWRITE_TAC[IN_NUMSEG]
1509 THEN REPEAT STRIP_TAC
1510 THEN ASM_SIMP_TAC[vecmats;CONTINUOUS_ON_LIFT_COMPONENT;PERMUTES_IN_NUMSEG;LAMBDA_BETA;LAMBDA_BETA_PERM;]
1511 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_COMPONENT
1514 THEN POP_ASSUM MP_TAC
1516 REWRITE_TAC[DIMINDEX_FINITE_PRODUCT]
1517 THEN MP_TAC(ARITH_RULE`i <= dimindex (:M) /\ 1<= i==> i -1<= dimindex (:M)-1 /\ ~(dimindex (:M)=0)/\ 1<= dimindex (:M)`)
1519 THEN MRESA_TAC LE_MULT_RCANCEL[`i-1:num`;`dimindex (:M)-1`;`dimindex (:M)`]
1520 THEN MP_TAC(ARITH_RULE`1<= dimindex (:M)==> dimindex (:M)-1+1=dimindex (:M)`)
1522 THEN MP_TAC(ARITH_RULE`(i-1)* dimindex (:M) <= (dimindex (:M) - 1) * dimindex (:M) /\ p i <= dimindex (:M)/\ 1<= dimindex (:M) ==> (i -1)* dimindex (:M) + p i <= (dimindex (:M)-1+1) * dimindex (:M)`)
1525 THEN POP_ASSUM MP_TAC
1527 REWRITE_TAC[DIMINDEX_FINITE_PRODUCT]
1528 THEN MP_TAC(ARITH_RULE`i <= dimindex (:M) /\ 1<= i==> i -1<= dimindex (:M)-1 /\ ~(dimindex (:M)=0)/\ 1<= dimindex (:M)`)
1530 THEN MRESA_TAC LE_MULT_RCANCEL[`i-1:num`;`dimindex (:M)-1`;`dimindex (:M)`]
1531 THEN MP_TAC(ARITH_RULE`1<= dimindex (:M)==> dimindex (:M)-1+1=dimindex (:M)`)
1533 THEN MP_TAC(ARITH_RULE`(i-1)* dimindex (:M) <= (dimindex (:M) - 1) * dimindex (:M) /\ p i <= dimindex (:M)/\ 1<= dimindex (:M) ==> (i -1)* dimindex (:M) + p i <= (dimindex (:M)-1+1) * dimindex (:M)`)
1536 let ROW_SUB=prove(`1<=i /\ i<= dimindex (:M)==> row i (x-y:real^N^M)= row i x - row i y`,
1537 SIMP_TAC[row;LAMBDA_BETA;CART_EQ;vector_sub;matrix_sub]);;
1540 let LIM_MATVEC=prove_by_refinement(` (!i. 1<=i /\ i <= dimindex(:M) ==> ((\n:num. row i (x n)) --> row i l) sequentially) ==> ((\n:num. matvec(x n )) --> matvec (l:real^K^M)) sequentially`,
1541 [REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist;]
1542 THEN DISCH_THEN(LABEL_TAC"THY")
1543 THEN REPEAT STRIP_TAC
1544 THEN POP_ASSUM MP_TAC
1545 THEN POP_ASSUM MP_TAC
1546 THEN REWRITE_TAC[GSYM RIGHT_FORALL_IMP_THM]
1547 THEN REWRITE_TAC[SET_RULE`A==>B==>C <=> B /\A ==>C`]
1549 THEN POP_ASSUM MP_TAC
1550 THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM]
1551 THEN REWRITE_TAC[SET_RULE`A/\B/\C==>D <=> A==> B/\C ==>D`]
1553 THEN POP_ASSUM(fun th-> MRESA1_TAC th`inv(&(dimindex (:M))) * e/ &2:real`)
1554 THEN POP_ASSUM MP_TAC
1555 THEN REWRITE_TAC[GSYM RIGHT_EXISTS_IMP_THM;SKOLEM_THM;MATVEC_SUB]
1556 THEN REWRITE_TAC[RIGHT_EXISTS_IMP_THM]
1558 THEN POP_ASSUM MP_TAC
1559 THEN DISCH_THEN(LABEL_TAC"THY")
1560 THEN EXISTS_TAC`nsum (1..dimindex (:M)) (\i:num. (N i):num)`
1561 THEN REPEAT STRIP_TAC
1562 THEN MRESA1_TAC NORM_VECMAT_SUM`matvec ((x:num->real^K^M) n - l:real^K^M)`
1563 THEN SUBGOAL_THEN`&0 < inv (&(dimindex (:M))) * e / &2` ASSUME_TAC;
1564 ONCE_REWRITE_TAC[REAL_ARITH`&0< a*b/ &2 <=> &0< a*b`]
1565 THEN MATCH_MP_TAC REAL_LT_MUL
1566 THEN ASM_REWRITE_TAC[]
1567 THEN MATCH_MP_TAC REAL_LT_INV
1568 THEN MRESAL_TAC REAL_OF_NUM_LT[`0`;`dimindex (:M)`][ARITH_RULE`0<A<=> 1<=A`;DIMINDEX_GE_1];
1569 SUBGOAL_THEN`sum (0..dimindex (:M) - 1) (\i. norm (vecmat i (matvec ((x:num->real^K^M) n - l:real^K^M))))< e`ASSUME_TAC;
1570 MP_TAC(ARITH_RULE`1<= dimindex (:M) ==> dimindex (:M)-1+1 = dimindex (:M)/\ ~(dimindex (:M) =0)`)
1571 THEN ASM_SIMP_TAC[DIMINDEX_GE_1]
1573 THEN MRESA_TAC REAL_OF_NUM_EQ[`(dimindex (:M))`;`0`]
1574 THEN MRESA1_TAC REAL_MUL_LINV`&(dimindex (:M))`
1575 THEN MRESAL_TAC SUM_LE_NUMSEG[`(\i:num. norm (vecmat i (matvec ((x:num->real^K^M) n - l:real^K^M))))`;`(\i:num. inv (&(dimindex (:M))) * (e:real) / &2)`;`0`;`dimindex (:M)-1`][SUM_CONST_NUMSEG;ARITH_RULE`A-0=A`;REAL_ARITH` a*b*c/ &2=(b*a)*c/ &2 /\ &1*A=A`]
1576 THEN MATCH_MP_TAC(REAL_ARITH`&0< a /\ b<= a/ &2 ==> b<a`)
1577 THEN ASM_REWRITE_TAC[]
1578 THEN POP_ASSUM MATCH_MP_TAC
1579 THEN REPEAT STRIP_TAC
1580 THEN MP_TAC(ARITH_RULE`0 <= i/\ i <= dimindex (:M) - 1 ==>
1581 1 <= SUC i /\ SUC i <= dimindex (:M)-1+1 /\ i < dimindex (:M)-1+1`)
1583 THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th`SUC i:num`)
1584 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i:num`;`(x:num-> real^K^M) n- l`]
1585 THEN MRESA_TAC (GEN_ALL ROW_SUB)[`(x:num-> real^K^M) n`;`SUC i`;`l:real^K^M`]
1586 THEN REMOVE_ASSUM_TAC
1587 THEN REMOVE_ASSUM_TAC
1588 THEN MATCH_MP_TAC(REAL_ARITH`a<b==> a<=b`)
1589 THEN POP_ASSUM MATCH_MP_TAC
1590 THEN MATCH_MP_TAC(ARITH_RULE`!a b c:num. a<=b/\ b<= c ==> a<=c`)
1591 THEN EXISTS_TAC`nsum (1..dimindex (:M)) (\i:num. (N i):num)`
1592 THEN ASM_REWRITE_TAC[]
1593 THEN REMOVE_ASSUM_TAC
1594 THEN REWRITE_TAC[GSYM REAL_OF_NUM_LE;REAL_OF_NUM_SUM_NUMSEG;ADD1]
1595 THEN MP_TAC(ARITH_RULE`0 <= i/\ i <= dimindex (:M) - 1 ==>
1596 1 <= i+1 /\ i+1 <= dimindex (:M)-1+1 /\ i <= dimindex (:M)-1+1`)
1598 THEN MRESA_TAC SUM_CLAUSES_LEFT[`(\i:num. &(N i))`;`i+1:num`;`dimindex (:M)`]
1599 THEN MRESA_TAC SUM_COMBINE_R[`(\i:num. &(N i))`;`1`;`i:num`;`dimindex (:M)`]
1600 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1601 THEN MATCH_MP_TAC (REAL_ARITH`&0<=a /\ &0<=b ==> c<= a+c+b`)
1602 THEN REWRITE_TAC[REAL_OF_NUM_LE;GSYM REAL_OF_NUM_SUM_NUMSEG;]
1603 THEN MRESAL_TAC NSUM_LE_NUMSEG[`(\i:num. 0)`;`N:num->num`;`1`;`i:num`][ARITH_RULE`0<=A:num`];
1605 THEN REMOVE_ASSUM_TAC
1606 THEN POP_ASSUM MP_TAC
1607 THEN REAL_ARITH_TAC]);;
1609 let LIM_VECMAT=prove(`((\n:num. matvec(x n )) --> matvec (l:real^K^M)) sequentially==> (!i. 1<=i /\ i <= dimindex(:M) ==> ((\n:num. row i (x n)) --> row i l) sequentially) `,
1610 REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist;]
1611 THEN DISCH_THEN(LABEL_TAC"THY")
1612 THEN REPEAT STRIP_TAC
1613 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`e:real`)
1614 THEN POP_ASSUM MP_TAC
1615 THEN DISCH_THEN(LABEL_TAC"THY")
1616 THEN EXISTS_TAC`N:num`
1617 THEN REPEAT STRIP_TAC
1618 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`n:num`)
1619 THEN POP_ASSUM MP_TAC
1620 THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)`)
1622 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1:num`;`(x:num-> real^K^M) n`]
1623 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1:num`;`(l:real^K^M)`]
1624 THEN MRESAL_TAC (GEN_ALL DIST_VECMAT)[`i-1:num`;`matvec ((x:num-> real^K^M) n)`;`matvec (l:real^K^M)`][dist;]
1625 THEN POP_ASSUM MP_TAC
1626 THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> SUC (i -1)= i `)
1628 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1629 THEN REAL_ARITH_TAC);;
1633 let CROSS_DOT_SEQUENTIALLY=prove(`((\n:num. f n) --> a) sequentially /\ ((\n:num. g n) --> b) sequentially /\ ((\n:num. h n) --> c) sequentially
1634 ==> ((lift o (\n:num. (f(n) cross g(n)) dot h(n)))--> lift ((a cross b) dot c)) sequentially`,
1635 ONCE_REWRITE_TAC[DOT_SYM]
1636 THEN REWRITE_TAC[DOT_CROSS_DET]
1637 THEN REPEAT STRIP_TAC
1638 THEN ABBREV_TAC`x=(\n:num. (vector [(h:num->real^3) n; f n; g n]:real^3^3))`
1639 THEN ABBREV_TAC`l= vector [c;a;b:real^3]:real^3^3`
1640 THEN SUBGOAL_THEN`(!i. 1 <= i /\ i <= dimindex (:3)
1641 ==> ((\n. row i ((x:num->real^3^3) n)) --> row i (l:real^3^3)) sequentially)` ASSUME_TAC
1645 THEN SIMP_TAC[DIMINDEX_3;row]
1646 THEN REPEAT STRIP_TAC
1647 THEN MP_TAC(ARITH_RULE`1<= i /\ i<= 3==> i=1 \/ i=2 \/ i=3`)
1650 THEN SIMP_TAC[VECTOR_3;]
1651 THEN ASM_SIMP_TAC[LAMBDA_ETA]
1652 THEN ASM_MESON_TAC[];
1653 MRESA_TAC(GEN_ALL LIM_MATVEC)[`x:num->real^3^3`;`l:real^3^3`]
1654 THEN MRESAL1_TAC CONTINUOUS_ON_DET`(:real^(3,3)finite_product)`[CONTINUOUS_ON_SEQUENTIALLY]
1655 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\n. matvec ((x:num->real^3^3) n))`;`matvec (l:real^3^3)`][SET_RULE`(a:A) IN(:A)`;o_DEF;VECMATS_MATVEC_ID])
1656 THEN POP_ASSUM MP_TAC
1658 THEN REWRITE_TAC[]]);;
1660 let ABS_LT_EPSI=prove(`!a b. abs(a-b)< b/ &4 /\ &0< b==> &0<a`,
1662 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= a-b \/ &0<= --(a-b)`)
1663 THENL[POP_ASSUM MP_TAC
1664 THEN REAL_ARITH_TAC;
1665 MRESAL1_TAC REAL_ABS_REFL`--(a-b)`[REAL_ABS_NEG]
1666 THEN REAL_ARITH_TAC]);;
1668 let LIM_SUBSEQUENCE1 = prove
1669 (`!s r. (!n. n <= r(n)) /\ (s --> l) sequentially
1670 ==> (s o r --> l) sequentially`,
1671 REWRITE_TAC[LIM_SEQUENTIALLY; o_THM] THEN
1672 MESON_TAC[MONOTONE_BIGGER; LE_TRANS]);;
1674 let SEQUENTIALLY_EQ_2POINT=prove(`!(h:num->A) f g. (!n:num. ((h:num->A) n) IN {f n, g n}) ==> (?r. !n. n<= r n/\ h (r n)= f (r n))\/ ?r. !n. n<= r n/\ h (r n)= g (r n)`,
1675 REPEAT GEN_TAC THEN REWRITE_TAC[SET_RULE`a IN {B,C}<=> a=B \/ a=C`]
1676 THEN MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`?r. !n:num. n<= r n/\ (h:num->A) (r n)= f (r n)`
1679 THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;GSYM SKOLEM_THM;DE_MORGAN_THM;NOT_IMP]
1680 THEN DISCH_THEN(LABEL_TAC"THY1")
1681 THEN DISCH_THEN(LABEL_TAC"THY2")
1683 THEN REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(\m:num. n+SUC m:num)`)
1684 THENL[POP_ASSUM MP_TAC
1686 REMOVE_THEN"THY2"(fun th-> MRESA1_TAC th`n+SUC n':num`)
1687 THEN EXISTS_TAC`n+SUC n'`
1688 THEN ASM_REWRITE_TAC[]
1691 THEN MESON_TAC[]]);;
1695 let LIM_IN_SET=prove(`!f g (h:num->real^N) a b c. ((\n. f n)--> a) sequentially /\ ((\n. g n)--> b) sequentially
1696 /\ ((\n. h n)--> c) sequentially /\ (!n. (h n) IN {f n, g n})
1699 THEN MRESA_TAC SEQUENTIALLY_EQ_2POINT[`h:num-> real^N`;`f:num-> real^N`;`g:num-> real^N`]
1701 MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`c:real^N`;`(\n. (h:num->real^N) n)`;`r:num->num`][o_DEF]
1702 THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`a:real^N`;`(\n. (f:num->real^N) n)`;`r:num->num`][o_DEF]
1703 THEN MRESAL_TAC LIM_UNIQUE[`sequentially`;`(\n:num. (f:num->real^N) (r(n)))`;`a:real^N`;`c:real^N`][TRIVIAL_LIMIT_SEQUENTIALLY;SET_RULE`a IN {a,b}`];
1704 MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`c:real^N`;`(\n. (h:num->real^N) n)`;`r:num->num`][o_DEF]
1705 THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`b:real^N`;`(\n. (g:num->real^N) n)`;`r:num->num`][o_DEF]
1706 THEN MRESAL_TAC LIM_UNIQUE[`sequentially`;`(\n:num. (g:num->real^N) (r(n)))`;`b:real^N`;`c:real^N`][TRIVIAL_LIMIT_SEQUENTIALLY;SET_RULE`b IN {a,b}`]]);;
1708 let POINT_COM_AFF_GT_INTER=prove(`!y z z1 w. ~collinear{vec 0,y,z:real^3} /\ ~collinear{ vec 0,y,z1}
1709 /\ w IN aff_gt {vec 0} {y,z} INTER aff_gt{vec 0}{y,z1}
1710 ==> z1 IN aff_ge {vec 0,y} {z}`,
1712 THEN POP_ASSUM MP_TAC
1713 THEN ASM_SIMP_TAC[th3; AFF_GT_1_2;AFF_GE_2_1;IN_ELIM_THM;INTER;VECTOR_ARITH`a % vec 0+A=A`]
1715 THEN POP_ASSUM MP_TAC
1716 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % y + t3 % z = t2' % y + t3' % z1
1717 <=> t3' % z1= (t2- t2') % y + t3 % z`]
1718 THEN MP_TAC(REAL_ARITH`&0< t3' ==> ~(t3'= &0)`)
1720 THEN MRESA1_TAC REAL_MUL_LINV`t3':real`
1722 THEN MP_TAC(SET_RULE`t3' % z1= (t2- t2') % y + t3 % z
1723 ==> inv t3' %(t3' % z1)= inv(t3') % ((t2- t2') % y + t3 % z:real^3)`)
1724 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
1725 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B %C=(A*B)%C /\ &1 %C=C/\ A%(C+D)=A%C+A%D`;]
1727 THEN EXISTS_TAC`&1-(inv t3' * (t2 - t2'))-(inv t3' * t3):real`
1728 THEN EXISTS_TAC`(inv t3' * (t2 - t2')):real`
1729 THEN EXISTS_TAC`(inv t3' * t3):real`
1730 THEN ASM_REWRITE_TAC[REAL_ARITH`&1-A-B+A+B= &1`]
1731 THEN MATCH_MP_TAC REAL_LE_MUL
1734 MATCH_MP_TAC REAL_LE_INV
1736 THEN REAL_ARITH_TAC;
1738 THEN REAL_ARITH_TAC]);;
1745 let DART_FAN_SY=prove(`FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
1746 /\ 1<= i /\ i<= dimindex (:M)
1747 /\ x = (row i (vecmats l),row (SUC (i MOD dimindex (:M))) (vecmats l))
1748 ==> x IN dart (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l))))`,
1750 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
1751 THEN SIMP_TAC[darts_of_hyp;ord_pairs;E_SY;]
1752 THEN MATCH_MP_TAC(SET_RULE`A IN B ==> A IN B UNION C`)
1753 THEN REWRITE_TAC[IN_ELIM_THM]
1754 THEN EXISTS_TAC`row i (vecmats (l:real^(M,3)finite_product))`
1755 THEN EXISTS_TAC`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
1756 THEN ASM_REWRITE_TAC[]
1757 THEN EXISTS_TAC`i:num`
1758 THEN ASM_SIMP_TAC[]);;
1760 let DART_FAN_SY1=prove(`FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
1761 /\ 1<= i /\ i<= dimindex (:M)
1762 /\ x = (row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l))
1763 ==> x IN dart (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l))))`,
1765 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
1766 THEN SIMP_TAC[darts_of_hyp;ord_pairs;E_SY;]
1767 THEN MATCH_MP_TAC(SET_RULE`A IN B ==> A IN B UNION C`)
1768 THEN REWRITE_TAC[IN_ELIM_THM]
1769 THEN EXISTS_TAC`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
1770 THEN EXISTS_TAC`row i (vecmats (l:real^(M,3)finite_product))`
1771 THEN ASM_REWRITE_TAC[]
1772 THEN EXISTS_TAC`i:num`
1773 THEN ASM_SIMP_TAC[SET_RULE`{A,B}={B,A}`]);;
1776 let EDGE_IN_E_SY=prove(`!(l:real^(M,3)finite_product). 1<= i /\ i<= dimindex (:M)
1777 /\ u = row i (vecmats l)
1778 /\ v= row (SUC (i MOD dimindex (:M))) (vecmats l)
1779 ==> {u,v} IN E_SY (vecmats l)`,
1782 THEN REWRITE_TAC[E_SY;IN_ELIM_THM]
1783 THEN EXISTS_TAC`i:num`
1784 THEN ASM_REWRITE_TAC[]);;
1788 let EQ_EDGE_E_SY=prove(`!(l:real^(M,3)finite_product).FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
1790 /\ 1<= i /\ i<= dimindex (:M)
1791 /\ row i (vecmats l)=v
1792 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=x
1794 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
1795 /\ row i (vecmats l)= row j (vecmats l)
1799 THEN POP_ASSUM MP_TAC
1800 THEN DISCH_THEN(LABEL_TAC"THY")
1801 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
1802 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
1804 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1805 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1806 THEN POP_ASSUM MP_TAC
1808 DISJ_CASES_TAC(SET_RULE`~(x=w:real^3) \/ x=w`)
1810 MP_TAC(SET_RULE`{v, x} = {v, w} /\ ~(x=w:real^3)==> x= v`)
1812 THEN REMOVE_THEN "THY"(fun th-> MRESA_TAC th[`(SUC (i MOD dimindex (:M))):num`;`i:num`])
1813 THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`dimindex (:M):num`];
1814 ASM_REWRITE_TAC[]]]);;
1818 let EQ_EDGE_E_SY1=prove(`!(l:real^(M,3)finite_product). 1<dimindex (:M)
1819 /\ 1<= i /\ i<= dimindex (:M)
1820 /\ row i (vecmats l)=v
1821 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=x
1823 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
1824 /\ row i (vecmats l)= row j (vecmats l)
1828 THEN POP_ASSUM MP_TAC
1829 THEN DISCH_THEN(LABEL_TAC"THY")
1830 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
1831 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
1833 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1834 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1835 THEN POP_ASSUM MP_TAC
1837 DISJ_CASES_TAC(SET_RULE`~(v=w:real^3) \/ v=w`)
1839 MP_TAC(SET_RULE`{v, x} = {w,x} /\ ~(v=w:real^3)==> x= v`)
1841 THEN REMOVE_THEN "THY"(fun th-> MRESA_TAC th[`(SUC (i MOD dimindex (:M))):num`;`i:num`])
1842 THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`dimindex (:M):num`];
1843 ASM_REWRITE_TAC[]]]);;
1845 let MOD_IMP_EQ=prove_by_refinement(`!i j. 1<= i /\ i<= k /\ 1<= j /\ j<= k
1846 /\ (i MOD k)= (j MOD k)
1848 [REWRITE_TAC[ARITH_RULE`SUC i= SUC j<=> i= j`]
1849 THEN REPEAT STRIP_TAC
1850 THEN POP_ASSUM MP_TAC
1851 THEN MP_TAC(ARITH_RULE`i<=k ==> i=k \/ i< k:num`)
1853 MP_TAC(ARITH_RULE`1<= i /\ i<=k ==> ~(k=0)`)
1855 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`]
1856 THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
1857 THEN MRESA_TAC MOD_EQ_0[`j:num`;`k:num`]
1859 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1860 THEN DISJ_CASES_TAC(ARITH_RULE`1< q \/ q=0 \/ q=1`);
1861 MRESAL_TAC LT_LMULT[`k:num`;`1`;`q:num`][ARITH_RULE` A*1 =A`]
1866 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`0*A=0`])
1870 MRESA_TAC MOD_LT[`i:num`;`k:num`]
1871 THEN MP_TAC(ARITH_RULE`j<=k ==> j=k \/ j< k:num`)
1873 MP_TAC(ARITH_RULE`1<= i /\ i<=k ==> ~(k=0)`)
1875 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`]
1877 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;])
1879 MRESA_TAC MOD_LT[`j:num`;`k:num`]]);;
1881 let SET_OF_EDGE_CARD_EQ2=prove_by_refinement(`!(l:real^(M,3)finite_product). 1<dimindex (:M)
1882 /\ 1<= i /\ i<= dimindex (:M)
1883 /\ row i (vecmats l)=u
1884 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
1885 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
1886 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
1887 /\ row i (vecmats l)= row j (vecmats l)
1889 ==> set_of_edge v (V_SY (vecmats l)) (E_SY (vecmats l)) ={u,w}`,
1891 THEN POP_ASSUM MP_TAC
1892 THEN DISCH_THEN(LABEL_TAC"THY")
1893 THEN ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM;EXTENSION]
1894 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
1895 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
1896 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1897 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1898 THEN POP_ASSUM MP_TAC
1902 REWRITE_TAC[E_SY;IN_ELIM_THM]
1903 THEN REPEAT STRIP_TAC
1904 THEN MP_TAC(SET_RULE`
1906 {row i' (vecmats l), row (SUC (i' MOD dimindex (:M))) (vecmats l)}
1907 ==> v = row i' (vecmats l) \/ v= row (SUC (i' MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`)
1909 REMOVE_THEN "THY"(fun th-> MRESA_TAC th[`(SUC (i MOD dimindex (:M))):num`;`i':num`]
1910 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1911 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC THEN ASSUME_TAC th)
1913 THEN MRESA_TAC (GEN_ALL EQ_EDGE_E_SY)[`i':num`;`v:real^3`;`row (SUC (i' MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`x:real^3`;`l:real^(M,3)finite_product`]
1915 REMOVE_THEN "THY"(fun th-> MRESA_TAC th[`(SUC (i MOD dimindex (:M))):num`;`(SUC (i' MOD dimindex (:M))):num`]
1916 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1917 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC THEN ASSUME_TAC (SYM th))
1918 THEN ASSUME_TAC (th))
1919 THEN MRESAL_TAC (GEN_ALL EQ_EDGE_E_SY1)[`i':num`;`v:real^3`;`row i' (vecmats (l:real^(M,3)finite_product))`;`x:real^3`;`l:real^(M,3)finite_product`][SET_RULE`{A,B}={B,A}`]
1920 THEN POP_ASSUM MP_TAC
1921 THEN POP_ASSUM MP_TAC
1922 THEN SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\
1923 SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
1924 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1925 THEN MRESAL_TAC DIVISION[`i':num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1926 THEN POP_ASSUM MP_TAC
1929 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`(SUC (i MOD dimindex (:M))):num`;`(SUC (i' MOD dimindex (:M))):num`][ARITH_RULE`SUC i= SUC j<=> i=j`] )
1930 THEN MRESA_TAC (GEN_ALL MOD_IMP_EQ)[`dimindex (:M)`;`i':num`;`i:num`]
1932 REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b \/ a=c`]
1934 ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1936 REWRITE_TAC[E_SY;IN_ELIM_THM]
1937 THEN EXISTS_TAC`i:num`
1938 THEN ASM_REWRITE_TAC[];
1939 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1940 THEN EXISTS_TAC`i:num`
1941 THEN ASM_REWRITE_TAC[];
1943 REWRITE_TAC[E_SY;IN_ELIM_THM]
1944 THEN EXISTS_TAC`SUC (i MOD dimindex (:M)):num`
1945 THEN ASM_REWRITE_TAC[];
1946 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1947 THEN EXISTS_TAC`(SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))):num`
1948 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1949 THEN MRESAL_TAC DIVISION[`SUC (i MOD dimindex (:M)):num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1950 THEN POP_ASSUM MP_TAC
1955 let INV_AZIM_CYCLE_EQ=prove_by_refinement(`!(l:real^(M,3)finite_product).FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
1956 /\ 1 < dimindex (:M)
1957 /\ 1<= i /\ i<= dimindex (:M)
1958 /\ row i (vecmats l)=u
1959 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
1960 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
1961 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
1962 /\ row i (vecmats l)= row j (vecmats l)
1964 ==> ivs_azim_cycle (EE v (E_SY (vecmats l))) (vec 0) v u =w`,
1966 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u:real^3`;`v:real^3`;`(l:real^(M,3)finite_product)`]
1967 THEN POP_ASSUM MP_TAC
1968 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1970 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
1971 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
1972 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1973 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1974 THEN POP_ASSUM MP_TAC
1976 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`(SUC (i MOD dimindex (:M))):num`;`v:real^3`;`w:real^3`;`(l:real^(M,3)finite_product)`]
1977 THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`u:real^3`]
1978 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.SIG_AND_INVERSE1_SIG)
1979 [`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`u:real^3`;`w:real^3`]
1980 THEN POP_ASSUM MATCH_MP_TAC
1981 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`w:real^3`;`v:real^3`]
1982 THEN MRESA_TAC(GEN_ALL SET_OF_EDGE_CARD_EQ2)[`i:num`;`v:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]
1983 THEN MRESA_TAC Fan.sigma_fan_in_set_of_edge[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`w:real^3`]
1984 THEN POP_ASSUM MP_TAC
1985 THEN DISJ_CASES_TAC(SET_RULE`u=w \/ ~({u,w}={w:real^3})`);
1988 MRESA_TAC SIGMA_FAN [`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`w:real^3`]
1989 THEN REMOVE_ASSUM_TAC
1990 THEN POP_ASSUM MP_TAC
1991 THEN POP_ASSUM MP_TAC
1994 let INV_AZIM_CYCLE_EQ1=prove_by_refinement(
1995 `!(l:real^(M,3)finite_product).FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
1996 /\ 1 < dimindex (:M)
1997 /\ 1<= i /\ i<= dimindex (:M)
1998 /\ row i (vecmats l)=u
1999 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2000 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
2001 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2002 /\ row i (vecmats l)= row j (vecmats l)
2004 ==> ivs_azim_cycle (EE v (E_SY (vecmats l))) (vec 0) v w =u`,
2006 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u:real^3`;`v:real^3`;`(l:real^(M,3)finite_product)`]
2007 THEN POP_ASSUM MP_TAC
2008 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2010 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2011 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
2012 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2013 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2014 THEN POP_ASSUM MP_TAC
2016 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`(SUC (i MOD dimindex (:M))):num`;`v:real^3`;`w:real^3`;`(l:real^(M,3)finite_product)`]
2017 THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`w:real^3`]
2018 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.SIG_AND_INVERSE1_SIG)
2019 [`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`w:real^3`;`u:real^3`]
2020 THEN POP_ASSUM MATCH_MP_TAC
2021 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`v:real^3`]
2022 THEN MRESA_TAC(GEN_ALL SET_OF_EDGE_CARD_EQ2)[`i:num`;`v:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]
2023 THEN MRESA_TAC Fan.sigma_fan_in_set_of_edge[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`u:real^3`]
2024 THEN POP_ASSUM MP_TAC
2025 THEN DISJ_CASES_TAC(SET_RULE`u=w \/ ~({u,w}={u:real^3})`);
2028 MRESA_TAC SIGMA_FAN [`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`u:real^3`]
2029 THEN REMOVE_ASSUM_TAC
2030 THEN POP_ASSUM MP_TAC
2031 THEN POP_ASSUM MP_TAC
2037 let FF_OF_HYP_EQ=prove(`FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2039 /\ 1<= i /\ i<= dimindex (:M)
2040 /\ row i (vecmats l)=u
2041 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2042 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
2043 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2044 /\ row i (vecmats l)= row j (vecmats l)
2047 (ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) (u,v)`,
2048 REWRITE_TAC[ff_of_hyp]
2049 THEN REPEAT STRIP_TAC
2050 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2051 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
2052 THENL[ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2053 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2054 THEN POP_ASSUM MP_TAC
2056 MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2057 THEN MRESAL_TAC (GEN_ALL DART_FAN_SY)[`i:num`;`(u:real^3,v:real^3)`;`l:real^(M,3)finite_product`][PAIR_EQ]
2058 THEN MRESA_TAC(GEN_ALL INV_AZIM_CYCLE_EQ)[`i:num`;`v:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]]);;
2065 let POWER_FF_OF_HYP_EQ=prove(`!i u v l x. FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2067 /\ 1<= i /\ i<= dimindex (:M)
2068 /\ row i (vecmats l)=u
2069 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2070 /\ x= (row 1 (vecmats l),row (SUC (1 MOD dimindex (:M))) (vecmats l))
2071 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2072 /\ row i (vecmats l)= row j (vecmats l)
2075 (ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER (i - 1)) x`,
2079 THEN DISCH_THEN(LABEL_TAC"THY")
2080 THEN REPEAT STRIP_TAC
2081 THEN DISJ_CASES_TAC(ARITH_RULE`i=0\/ 1<= i`)
2083 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
2085 THEN ONCE_REWRITE_TAC[ARITH_RULE`SUC 0=1 /\ SUC 0 -1=0`]
2086 THEN REPEAT RESA_TAC
2087 THEN REWRITE_TAC[POWER;I_DEF];
2088 MP_TAC(ARITH_RULE`SUC i <= dimindex (:M)==> i <= dimindex (:M) /\ i < dimindex (:M)`)
2090 THEN REMOVE_THEN"THY"(fun th-> MRESA_TAC th[`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`;`row 1 (vecmats (l:real^(M,3)finite_product)),row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`])
2091 THEN MP_TAC(ARITH_RULE`1<=i ==> SUC i-1= SUC (i-1)`)
2093 THEN ASM_REWRITE_TAC[Hypermap.COM_POWER;o_DEF]
2094 THEN REMOVE_ASSUM_TAC
2095 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2096 THEN MRESA_TAC(GEN_ALL FF_OF_HYP_EQ)[`i:num`;`(row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(l:real^(M,3)finite_product)`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
2097 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2098 THEN MRESA_TAC MOD_LT[`i:num`;`dimindex (:M)`]]]);;
2102 let POWER_FF_HYP_ID=prove(`!k l x. FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2105 /\ (row 1 (vecmats l),row (SUC (1 MOD dimindex (:M))) (vecmats l))= x
2106 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2107 /\ row i (vecmats l)= row j (vecmats l)
2110 (ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER k) x`,
2112 THEN MP_TAC(ARITH_RULE`1<k ==> ~(k=0)/\ 1<= k /\ k <= k/\ k= SUC (k-1)`)
2114 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
2115 THEN REWRITE_TAC[Hypermap.COM_POWER;o_DEF]
2116 THEN MRESAL_TAC POWER_FF_OF_HYP_EQ[`k:num`;`(row (k:num) (vecmats (l:real^(M,3)finite_product)))`;`row (SUC ((k) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`;`x:real^3#real^3`][ARITH_RULE`dimindex (:M)<=dimindex (:M)`]
2117 THEN POP_ASSUM MP_TAC
2119 THEN REWRITE_TAC[ARITH_RULE`dimindex (:M)<=dimindex (:M)`]
2121 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
2122 THEN MRESA_TAC(GEN_ALL FF_OF_HYP_EQ)[`k:num`;`(row (SUC ((SUC (k MOD dimindex (:M))) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(l:real^(M,3)finite_product)`;`row k (vecmats (l:real^(M,3)finite_product))`;`row (SUC (k MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
2123 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2124 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`]
2125 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
2127 THEN REWRITE_TAC[PAIR_EQ]
2128 THEN ASM_REWRITE_TAC[]);;
2132 let FACE_HYP_FAN_SY=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2134 /\ (row 1 (vecmats l),row (SUC (1 MOD dimindex (:M))) (vecmats l))=x
2135 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2136 /\ row i (vecmats l)= row j (vecmats l)
2138 ==> F_SY (vecmats l) =
2139 face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x`,
2141 THEN ASM_REWRITE_TAC[face;EXTENSION;IN_ELIM_THM;F_SY;]
2145 MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`][orbit_map;IN_ELIM_THM]
2146 THEN REPEAT STRIP_TAC
2147 THEN EXISTS_TAC`i-1:num`
2148 THEN MP_TAC(ARITH_RULE`1<= i==> i-1>= 0`)
2150 THEN MATCH_MP_TAC POWER_FF_OF_HYP_EQ
2151 THEN ASM_REWRITE_TAC[];
2152 MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2153 THEN MP_TAC(ARITH_RULE`1<dimindex (:M) ==> ~(dimindex (:M)=0)`)
2155 THEN MRESA_TAC POWER_FF_HYP_ID[`dimindex (:M)`;`(l:real^(M,3)finite_product)`;`x:real^3#real^3`]
2156 THEN POP_ASSUM MP_TAC
2157 THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
2159 THEN MRESA_TAC Hypermap.orbit_cyclic [`(face_map (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product))))))`;`dimindex (:M)`;`x:real^3#real^3`]
2160 THEN REWRITE_TAC[IN_ELIM_THM]
2162 THEN MP_TAC(ARITH_RULE`k<dimindex (:M) ==> SUC k<= dimindex (:M) /\ SUC(SUC k -1)= SUC k/\ k = SUC k -1`)
2164 THEN EXISTS_TAC`SUC k`
2165 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC k`]
2166 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
2167 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
2168 THEN MATCH_MP_TAC POWER_FF_OF_HYP_EQ
2169 THEN ASM_REWRITE_TAC[]
2173 let CARD_F_SY_EQ=prove(`1< dimindex (:M)
2174 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2175 /\ row i (vecmats l)= row j (vecmats (l:real^(M,3)finite_product))
2177 ==> CARD (F_SY (vecmats l))= dimindex (:M)`,
2179 THEN REPEAT STRIP_TAC
2180 THEN POP_ASSUM MP_TAC
2181 THEN DISCH_THEN(LABEL_TAC"THY")
2182 THEN SUBGOAL_THEN`{y | ?x. x IN 1..dimindex (:M) /\
2185 row (SUC (x MOD dimindex (:M))) (vecmats l)}
2186 ={row i (vecmats l),row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)) | 1 <= i /\
2191 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
2192 MRESAL_TAC CARD_IMAGE_INJ[`(\i:num. (row i (vecmats l),row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))))`;`1..dimindex (:M)`]
2193 [FINITE_NUMSEG;IMAGE;CARD_NUMSEG_1]
2194 THEN POP_ASSUM MATCH_MP_TAC
2195 THEN REWRITE_TAC[IN_NUMSEG;PAIR_EQ]
2196 THEN REPEAT STRIP_TAC
2197 THEN REMOVE_THEN"THY"(fun th-> MRESA_TAC th[`x:num`;`y:num`])]);;
2201 let AZIM_CYCLE_EQ1=prove_by_refinement( `!(l:real^(M,3)finite_product).FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2202 /\ 1 < dimindex (:M)
2203 /\ 1<= i /\ i<= dimindex (:M)
2204 /\ row i (vecmats l)=u
2205 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2206 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
2207 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2208 /\ row i (vecmats l)= row j (vecmats l)
2210 ==> azim_cycle (EE v (E_SY (vecmats l))) (vec 0) v w =u`,
2212 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u:real^3`;`v:real^3`;`(l:real^(M,3)finite_product)`]
2213 THEN POP_ASSUM MP_TAC
2214 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2216 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2217 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
2218 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2219 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2220 THEN POP_ASSUM MP_TAC
2222 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`(SUC (i MOD dimindex (:M))):num`;`v:real^3`;`w:real^3`;`(l:real^(M,3)finite_product)`]
2223 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`w:real^3`;`v:real^3`]
2224 THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`w:real^3`]
2225 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`v:real^3`]
2226 THEN MRESA_TAC(GEN_ALL SET_OF_EDGE_CARD_EQ2)[`i:num`;`v:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]
2227 THEN MRESA_TAC Fan.sigma_fan_in_set_of_edge[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`w:real^3`]
2228 THEN POP_ASSUM MP_TAC
2229 THEN DISJ_CASES_TAC(SET_RULE`u=w \/ ~({u,w}={w:real^3})`);
2232 MRESA_TAC SIGMA_FAN [`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`w:real^3`]
2233 THEN REMOVE_ASSUM_TAC
2234 THEN POP_ASSUM MP_TAC
2235 THEN POP_ASSUM MP_TAC
2239 let AZIM_CYCLE_EQ=prove_by_refinement( `!(l:real^(M,3)finite_product).FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2240 /\ 1 < dimindex (:M)
2241 /\ 1<= i /\ i<= dimindex (:M)
2242 /\ row i (vecmats l)=u
2243 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2244 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
2245 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2246 /\ row i (vecmats l)= row j (vecmats l)
2248 ==> azim_cycle (EE v (E_SY (vecmats l))) (vec 0) v u =w`,
2250 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u:real^3`;`v:real^3`;`(l:real^(M,3)finite_product)`]
2251 THEN POP_ASSUM MP_TAC
2252 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2254 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2255 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
2256 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2257 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2258 THEN POP_ASSUM MP_TAC
2260 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`(SUC (i MOD dimindex (:M))):num`;`v:real^3`;`w:real^3`;`(l:real^(M,3)finite_product)`]
2261 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`v:real^3`]
2262 THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`u:real^3`]
2263 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`w:real^3`;`v:real^3`]
2264 THEN MRESA_TAC(GEN_ALL SET_OF_EDGE_CARD_EQ2)[`i:num`;`v:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]
2265 THEN MRESA_TAC Fan.sigma_fan_in_set_of_edge[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`u:real^3`]
2266 THEN POP_ASSUM MP_TAC
2267 THEN DISJ_CASES_TAC(SET_RULE`u=w \/ ~({u,w}={u:real^3})`);
2270 MRESA_TAC SIGMA_FAN [`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;`u:real^3`]
2271 THEN REMOVE_ASSUM_TAC
2272 THEN POP_ASSUM MP_TAC
2273 THEN POP_ASSUM MP_TAC
2276 let NN_OF_HYP_EQ1=prove(`FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2278 /\ 1<= i /\ i<= dimindex (:M)
2279 /\ row i (vecmats l)=u
2280 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2281 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
2282 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2283 /\ row i (vecmats l)= row j (vecmats l)
2286 (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) (v,w)`,
2287 REWRITE_TAC[nn_of_hyp]
2288 THEN REPEAT STRIP_TAC
2289 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2290 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
2292 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2293 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2294 THEN POP_ASSUM MP_TAC
2296 MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2297 THEN MRESAL_TAC (GEN_ALL DART_FAN_SY)[`(SUC (i MOD dimindex (:M)))`;`(v:real^3,w:real^3)`;`l:real^(M,3)finite_product`][PAIR_EQ]
2298 THEN MRESA_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`i:num`;`v:real^3`;`w:real^3`;`u:real^3`;`l:real^(M,3)finite_product`]]);;
2302 let NN_OF_HYP_EQ=prove(`FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2304 /\ 1<= i /\ i<= dimindex (:M)
2305 /\ row i (vecmats l)=u
2306 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2307 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
2308 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2309 /\ row i (vecmats l)= row j (vecmats l)
2312 (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) (v,u)`,
2313 REWRITE_TAC[nn_of_hyp]
2314 THEN REPEAT STRIP_TAC
2315 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2316 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
2318 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2319 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2320 THEN POP_ASSUM MP_TAC
2322 MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2323 THEN MRESAL_TAC (GEN_ALL DART_FAN_SY1)[`i:num`;`(v:real^3,u:real^3)`;`l:real^(M,3)finite_product`][PAIR_EQ]
2324 THEN MRESA_TAC(GEN_ALL AZIM_CYCLE_EQ)[`i:num`;`v:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]]);;
2327 let DART_OF_HYP_SY_EQ=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2329 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2330 /\ row i (vecmats l)= row j (vecmats l)
2332 ==> darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l)) = (F_SY (vecmats l)) UNION (IMAGE (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) (F_SY (vecmats l)))`,
2334 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2335 THEN REWRITE_TAC[EXTENSION;]
2338 REWRITE_TAC[darts_of_hyp;UNION;IN_ELIM_THM;ord_pairs;self_pairs]
2339 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[E_SY;]
2340 THEN REWRITE_TAC[IN_ELIM_THM]
2341 THEN REPEAT STRIP_TAC;
2342 MP_TAC(SET_RULE`{a, b} =
2343 {row i (vecmats l), row (SUC (i MOD dimindex (:M))) (vecmats l)}
2344 ==> a = row i (vecmats (l:real^(M,3)finite_product))\/ a= row (SUC (i MOD dimindex (:M))) (vecmats l)`)
2346 MRESA_TAC (GEN_ALL EQ_EDGE_E_SY)[`i:num`;`a:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`b:real^3`;`l:real^(M,3)finite_product`]
2347 THEN MATCH_MP_TAC(SET_RULE`A IN B==> A IN B \/ A IN C`)
2348 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
2349 THEN EXISTS_TAC`i:num`
2350 THEN ASM_REWRITE_TAC[];
2351 MRESAL_TAC (GEN_ALL EQ_EDGE_E_SY1)[`i:num`;`a:real^3`;`row i (vecmats (l:real^(M,3)finite_product))`;`b:real^3`;`l:real^(M,3)finite_product`][SET_RULE`{A,B}={B,A}`]
2352 THEN MATCH_MP_TAC(SET_RULE`A IN C==> A IN B \/ A IN C`)
2353 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2354 THEN EXISTS_TAC`a:real^3,(row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`
2356 REWRITE_TAC[F_SY;IN_ELIM_THM]
2357 THEN EXISTS_TAC`(SUC (i MOD dimindex (:M)))`
2358 THEN ASM_REWRITE_TAC[]
2359 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2360 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2361 THEN POP_ASSUM MP_TAC
2363 MRESA_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i:num`;`b:real^3`;`l:real^(M,3)finite_product`;`a:real^3`;`(row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`];
2364 MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)
2365 [`vec 0:real^3`;`v:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2366 THEN POP_ASSUM MP_TAC
2367 THEN REMOVE_ASSUM_TAC
2368 THEN REMOVE_ASSUM_TAC
2369 THEN POP_ASSUM MP_TAC
2370 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[V_SY;]
2371 THEN REWRITE_TAC[IN_ELIM_THM;rows]
2373 THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)
2375 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
2376 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
2377 THEN MRESAL_TAC(GEN_ALL SET_OF_EDGE_CARD_EQ2)[`dimindex (:M):num`;`(row
2378 1 (vecmats (l:real^(M,3)finite_product)))`;`(row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`(row
2379 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
2381 MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ i= SUC (i-1)`)
2383 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
2384 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
2385 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
2386 THEN MRESAL_TAC(GEN_ALL SET_OF_EDGE_CARD_EQ2)[`i-1:num`;`(row
2387 (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row (i-1) (vecmats (l:real^(M,3)finite_product)))`;`(row
2388 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
2390 REWRITE_TAC[UNION;IN_ELIM_THM]
2393 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
2395 MRESA_TAC (GEN_ALL DART_FAN_SY)[`i:num`;`x:real^3#real^3`;`l:real^(M,3)finite_product`];
2397 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;F_SY]
2399 THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)
2401 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
2402 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
2403 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`dimindex (:M):num`;`(row
2404 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
2405 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
2406 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2407 THEN MRESAL_TAC (GEN_ALL DART_FAN_SY1)[`dimindex (:M):num`;`row 1 (vecmats l),row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1];
2408 MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ i= SUC (i-1)`)
2410 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
2411 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
2412 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
2413 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i-1:num`;`(row
2414 (i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
2415 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
2416 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2417 THEN MRESAL_TAC (GEN_ALL DART_FAN_SY1)[`i-1:num`;`row (SUC ((i-1) MOD dimindex (:M))) (vecmats l),row (i-1) (vecmats (l:real^(M,3)finite_product))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]]);;
2420 let IMAGE_NN_OF_HYP_F_SY=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2422 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2423 /\ row i (vecmats l)= row j (vecmats l)
2425 ==> (IMAGE (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) (F_SY (vecmats l)))={row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2426 i <= dimindex (:M)}`,
2428 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION; F_SY]
2432 THEN ASM_REWRITE_TAC[]
2433 THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)
2435 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
2436 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
2437 THEN EXISTS_TAC`dimindex (:M)`
2438 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`dimindex (:M):num`;`(row
2439 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
2440 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1];
2441 MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ i= SUC (i-1)`)
2443 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
2444 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
2445 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
2446 THEN EXISTS_TAC`i-1:num`
2447 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i-1:num`;`(row
2448 (i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
2449 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1];
2451 THEN ASM_REWRITE_TAC[]
2452 THEN EXISTS_TAC`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)),row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
2454 EXISTS_TAC`(SUC (i MOD dimindex (:M)))`
2455 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2456 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2457 THEN POP_ASSUM MP_TAC
2459 MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i:num`;`(row
2460 (i) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
2461 (SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]]);;
2464 let CARD_IMAGE_F_SY_EQ=prove(`1< dimindex (:M)
2465 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2466 /\ row i (vecmats l)= row j (vecmats (l:real^(M,3)finite_product))
2468 ==> CARD ({row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2469 i <= dimindex (:M)})= dimindex (:M)`,
2471 THEN POP_ASSUM MP_TAC
2472 THEN DISCH_THEN(LABEL_TAC"THY")
2473 THEN SUBGOAL_THEN`{y | ?x. x IN 1..dimindex (:M) /\
2475 row (SUC (x MOD dimindex (:M))) (vecmats l),
2477 ={row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)),row i (vecmats l) | 1 <= i /\
2482 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
2483 MRESAL_TAC CARD_IMAGE_INJ[`(\i:num. row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)),(row i (vecmats l)))`;`1..dimindex (:M)`]
2484 [FINITE_NUMSEG;IMAGE;CARD_NUMSEG_1]
2485 THEN POP_ASSUM MATCH_MP_TAC
2486 THEN REWRITE_TAC[IN_NUMSEG;PAIR_EQ]
2487 THEN REPEAT STRIP_TAC
2488 THEN REMOVE_THEN"THY"(fun th-> MRESA_TAC th[`x:num`;`y:num`])]);;
2491 let SUC_POWER2_NOT=prove_by_refinement(`2< k /\ i<=k ==> ~(i= SUC(SUC(i MOD k) MOD k))`,
2493 THEN POP_ASSUM MP_TAC
2494 THEN MP_TAC(ARITH_RULE`i<=k/\ 2<k ==> i=k \/ SUC i=k\/ SUC i< k`)
2496 MP_TAC(ARITH_RULE`2<k ==> ~(k=0)/\ 1<k /\ ~(k=SUC 1)`)
2498 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
2499 THEN MRESAL_TAC MOD_LT[`1:num`;`k:num`][ARITH_RULE`0<1`];
2500 MP_TAC(ARITH_RULE`SUC i=k==> i<k/\ ~(k=0)`)
2502 THEN MRESAL_TAC MOD_LT[`i:num`;`k:num`][ARITH_RULE`0<1`]
2503 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
2505 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`SUC 1=2`])
2507 MP_TAC(ARITH_RULE`SUC i<k==> i<k/\ ~(k=0)`)
2509 THEN MRESAL_TAC MOD_LT[`i:num`;`k:num`][ARITH_RULE`0<1`]
2510 THEN MRESAL_TAC MOD_LT[`SUC i:num`;`k:num`][ARITH_RULE`0<1`]
2514 let F_SY_INTER_IMAGE_NN_EMPTY=prove(`2< dimindex (:M)
2515 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2516 /\ row i (vecmats l)= row j (vecmats (l:real^(M,3)finite_product))
2518 ==> F_SY(vecmats l) INTER {row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2519 i <= dimindex (:M)}= {}`,
2520 REWRITE_TAC[F_SY;INTER;EXTENSION;EMPTY;IN_ELIM_THM]
2522 THEN POP_ASSUM MP_TAC
2523 THEN DISCH_THEN(LABEL_TAC"THY")
2524 THEN REPEAT STRIP_TAC
2525 THEN POP_ASSUM MP_TAC
2526 THEN ASM_REWRITE_TAC[PAIR_EQ]
2528 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2529 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
2531 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2532 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2533 THEN POP_ASSUM MP_TAC
2535 SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\
2536 SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
2538 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2539 THEN MRESAL_TAC DIVISION[`i':num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2540 THEN POP_ASSUM MP_TAC
2542 REMOVE_THEN"THY"(fun th-> MRESA_TAC th[`i:num `;`(SUC (i' MOD dimindex (:M)))`] THEN MRESA_TAC th[`i':num `;`(SUC (i MOD dimindex (:M)))`])
2543 THEN POP_ASSUM MP_TAC
2544 THEN MRESA_TAC (GEN_ALL SUC_POWER2_NOT)[`i':num`;`dimindex (:M)`]]]);;
2546 let FINITE_F_SY=prove(` FINITE (F_SY(vecmats (l:real^(M,N)finite_product)))`,
2548 THEN SUBGOAL_THEN`{y | ?x. x IN 1..dimindex (:M) /\
2551 row (SUC (x MOD dimindex (:M))) (vecmats l)}
2552 ={row i (vecmats l),row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,N)finite_product)) | 1 <= i /\
2557 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
2558 MRESAL_TAC FINITE_IMAGE
2559 [`(\i:num. (row i (vecmats l),row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,N)finite_product))))`;`1..dimindex (:M)`]
2560 [FINITE_NUMSEG;IMAGE;CARD_NUMSEG_1]
2561 THEN POP_ASSUM MATCH_MP_TAC]);;
2565 let FINITE_IMAGE_F_SY=prove(`1< dimindex (:M)
2566 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2567 /\ row i (vecmats l)= row j (vecmats (l:real^(M,3)finite_product))
2569 ==> FINITE({row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2570 i <= dimindex (:M)})`,
2572 THEN POP_ASSUM MP_TAC
2573 THEN DISCH_THEN(LABEL_TAC"THY")
2574 THEN SUBGOAL_THEN`{y | ?x. x IN 1..dimindex (:M) /\
2576 row (SUC (x MOD dimindex (:M))) (vecmats l),
2578 ={row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)),row i (vecmats l) | 1 <= i /\
2583 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
2584 MRESAL_TAC FINITE_IMAGE[`(\i:num. row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)),(row i (vecmats l)))`;`1..dimindex (:M)`]
2585 [FINITE_NUMSEG;IMAGE;CARD_NUMSEG_1]
2586 THEN POP_ASSUM MATCH_MP_TAC
2587 THEN REWRITE_TAC[IN_NUMSEG;PAIR_EQ]
2588 THEN REPEAT STRIP_TAC
2589 THEN REMOVE_THEN"THY"(fun th-> MRESA_TAC th[`x:num`;`y:num`])]);;
2596 let CARD_DART_OF_HYP=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2598 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2599 /\ row i (vecmats l)= row j (vecmats l)
2601 ==> CARD (darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))) = 2 * dimindex (:M)`,
2603 THEN MP_TAC(ARITH_RULE`2< dimindex(:M)==> 1< dimindex(:M)`)
2605 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
2606 THEN MRESA1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`
2607 THEN MRESA1_TAC(GEN_ALL F_SY_INTER_IMAGE_NN_EMPTY)`l:real^(M,3)finite_product`
2608 THEN MRESA1_TAC(GEN_ALL FINITE_F_SY)`l:real^(M,3)finite_product`
2609 THEN MRESA1_TAC(GEN_ALL FINITE_IMAGE_F_SY)`l:real^(M,3)finite_product`
2610 THEN MRESA_TAC CARD_UNION[`F_SY (vecmats (l:real^(M,3)finite_product))`;`IMAGE (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)))
2611 (F_SY (vecmats (l:real^(M,3)finite_product)))`]
2612 THEN MRESA1_TAC(GEN_ALL CARD_IMAGE_F_SY_EQ)`l:real^(M,3)finite_product`
2613 THEN MRESA1_TAC(GEN_ALL CARD_F_SY_EQ)`l:real^(M,3)finite_product`
2617 let IMAGE_NN_OF_HYP_EQ_F_SY=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2619 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2620 /\ row i (vecmats l)= row j (vecmats l)
2622 ==> IMAGE (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) {row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2626 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION; F_SY]
2630 THEN ASM_REWRITE_TAC[]
2631 THEN EXISTS_TAC`(SUC (i MOD dimindex (:M)))`
2632 THEN MRESA_TAC(GEN_ALL NN_OF_HYP_EQ)[`i:num`;`(row
2633 (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row
2634 (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row i (vecmats (l:real^(M,3)finite_product)))`]
2635 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2636 THEN MRESAL_TAC DIVISION[`i':num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2637 THEN POP_ASSUM MP_TAC
2640 THEN ASM_REWRITE_TAC[]
2641 THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)
2643 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
2644 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
2645 THEN EXISTS_TAC`row 1 (vecmats l),row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`
2647 EXISTS_TAC`dimindex (:M)`
2648 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1];
2649 MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`dimindex (:M):num`;`(row
2650 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
2651 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1];
2652 MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ i= SUC (i-1)`)
2654 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
2655 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
2656 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
2657 THEN EXISTS_TAC`row (SUC ((i - 1) MOD dimindex (:M))) (vecmats l),row (i-1) (vecmats (l:real^(M,3)finite_product))`
2660 THEN ASM_REWRITE_TAC[];
2661 MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`i-1:num`;`(row
2662 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
2663 (i-1) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]]);;
2666 let DART_OF_HYP_SY_EQ1=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2668 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2669 /\ row i (vecmats l)= row j (vecmats l)
2671 /\ {row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2672 i <= dimindex (:M)}=S
2673 ==> darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l)) = S UNION (IMAGE (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) S)`,
2675 THEN MRESA1_TAC (GEN_ALL IMAGE_NN_OF_HYP_EQ_F_SY)`l:real^(M,3)finite_product`
2676 THEN MRESA1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`
2677 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2678 THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`]
2679 THEN MATCH_MP_TAC DART_OF_HYP_SY_EQ
2680 THEN ASM_REWRITE_TAC[]);;
2682 let F_SY_EQ_FACE=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2684 /\ 1<= i /\ i<= dimindex (:M)
2685 /\ (row i (vecmats l),row (SUC (i MOD dimindex (:M))) (vecmats l))=x
2686 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2687 /\ row i (vecmats l)= row j (vecmats l)
2689 ==> F_SY (vecmats l) =
2690 face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x`,
2692 THEN MRESA_TAC (GEN_ALL FACE_HYP_FAN_SY)[`l:real^(M,3)finite_product`;`row 1 (vecmats l),row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`]
2693 THEN MATCH_MP_TAC lemma_face_identity
2694 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2695 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
2696 THEN EXISTS_TAC`i:num`
2697 THEN ASM_REWRITE_TAC[]);;
2700 let FF_OF_HYP_EQ1=prove(`FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2702 /\ 1<= i /\ i<= dimindex (:M)
2703 /\ row i (vecmats l)=u
2704 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2705 /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w
2706 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2707 /\ row i (vecmats l)= row j (vecmats l)
2710 (ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) (w,v)`,
2711 REWRITE_TAC[ff_of_hyp]
2712 THEN REPEAT STRIP_TAC
2713 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
2714 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
2716 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
2717 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
2718 THEN POP_ASSUM MP_TAC
2720 MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2721 THEN MRESAL_TAC (GEN_ALL DART_FAN_SY1)[`(SUC (i MOD dimindex (:M))):num`;`(w:real^3,v:real^3)`;`l:real^(M,3)finite_product`][PAIR_EQ]
2722 THEN MRESA_TAC(GEN_ALL INV_AZIM_CYCLE_EQ1)[`i:num`;`v:real^3`;`w:real^3`;`u:real^3`;`l:real^(M,3)finite_product`]]);;
2729 let POWER_FF_OF_HYP_EQ1=prove(`!j i u v l x. FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2731 /\ 1<= i /\ i<= dimindex (:M)
2732 /\ j= (dimindex (:M)-i + 1)
2733 /\ row i (vecmats l)=u
2734 /\ row (SUC (i MOD dimindex (:M))) (vecmats l)=v
2735 /\ x= row (SUC (1 MOD dimindex (:M))) (vecmats l),row 1 (vecmats l)
2736 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2737 /\ row i (vecmats l)= row j (vecmats l)
2740 (ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER j) x`,
2745 THEN DISCH_THEN(LABEL_TAC"THY")
2746 THEN REPEAT STRIP_TAC
2747 THEN MP_TAC(ARITH_RULE`i<= dimindex (:M)==> i= dimindex (:M)\/ i< dimindex (:M)`)
2748 THEN FIND_ASSUM(fun th-> REWRITE_TAC[th])`i<= dimindex (:M)`
2751 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
2752 THEN ASM_REWRITE_TAC[ARITH_RULE`dimindex (:M) - dimindex (:M) + 1=1`;POWER_1]
2753 THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
2754 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
2755 THEN MRESAL_TAC(GEN_ALL FF_OF_HYP_EQ1)[`dimindex (:M):num`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`;`row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`row (SUC (dimindex (:M) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;][ARITH_RULE`SUC 0=1`]
2756 THEN REMOVE_ASSUM_TAC
2757 THEN POP_ASSUM MP_TAC
2758 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
2759 THEN ASM_REWRITE_TAC[ARITH_RULE`1= SUC 0`];
2760 ASM_REWRITE_TAC[Hypermap.COM_POWER;o_DEF]
2761 THEN MP_TAC(ARITH_RULE`SUC j = dimindex (:M) - i + 1 /\ i< dimindex (:M)==> dimindex (:M) - j + 1= SUC i/\ SUC i<= dimindex (:M) /\ 1<= SUC i/\ j = dimindex (:M) - SUC i + 1`)
2763 THEN MRESA_TAC MOD_LT[`i:num`;`dimindex (:M)`]
2764 THEN REMOVE_THEN"THY"(fun th-> MRESA_TAC th[`dimindex (:M) -j +1`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`;`x:real^3#real^3`])
2765 THEN POP_ASSUM MP_TAC
2766 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
2768 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2769 THEN MRESA_TAC(GEN_ALL FF_OF_HYP_EQ1)[`i:num`;`row i (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`v:real^3`;]]]);;
2774 let POWER_FF_HYP_ID1=prove(`!k l x. FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2777 /\ row (SUC (1 MOD dimindex (:M))) (vecmats l),row 1 (vecmats l)= x
2778 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2779 /\ row i (vecmats l)= row j (vecmats l)
2782 (ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER k) x`,
2784 THEN MP_TAC(ARITH_RULE`1<k ==> k=k-1+1/\ 1<=k`)
2786 THEN MRESAL_TAC POWER_FF_OF_HYP_EQ1[`k:num`;`1`;`(row (1:num) (vecmats (l:real^(M,3)finite_product)))`;`row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`;`x:real^3#real^3`][ARITH_RULE`dimindex (:M)<=dimindex (:M)/\ 1<=1`]
2787 THEN POP_ASSUM MATCH_MP_TAC
2788 THEN POP_ASSUM MP_TAC
2792 let FACE_HYP_FAN_SY1=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2794 /\ row (SUC (1 MOD dimindex (:M))) (vecmats l),row 1 (vecmats l)=x
2795 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2796 /\ row i (vecmats l)= row j (vecmats l)
2798 /\ S={row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2801 face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x`,
2803 THEN ASM_REWRITE_TAC[face;EXTENSION;IN_ELIM_THM;F_SY;]
2807 MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`][orbit_map;IN_ELIM_THM]
2808 THEN REPEAT STRIP_TAC
2809 THEN EXISTS_TAC`(dimindex (:M)-i + 1):num`
2810 THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> dimindex (:M) - i + 1 >= 0`)
2812 THEN MATCH_MP_TAC POWER_FF_OF_HYP_EQ1
2813 THEN EXISTS_TAC`i:num`
2814 THEN ASM_REWRITE_TAC[];
2815 MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2816 THEN MP_TAC(ARITH_RULE`1<dimindex (:M) ==> ~(dimindex (:M)=0)`)
2818 THEN MRESA_TAC POWER_FF_HYP_ID1[`dimindex (:M)`;`(l:real^(M,3)finite_product)`;`x:real^3#real^3`]
2819 THEN POP_ASSUM MP_TAC
2820 THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
2822 THEN MRESA_TAC Hypermap.orbit_cyclic [`(face_map (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product))))))`;`dimindex (:M)`;`x:real^3#real^3`]
2823 THEN REWRITE_TAC[IN_ELIM_THM]
2825 THEN MP_TAC(ARITH_RULE`k< dimindex (:M) ==> 1 <= dimindex (:M) - k + 1 `)
2827 THEN MP_TAC(ARITH_RULE`k< dimindex (:M) ==> k=0\/ dimindex (:M) - k + 1 <= dimindex (:M)`)
2830 REWRITE_TAC[POWER;I_DEF]
2832 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1`;DIMINDEX_GE_1];
2833 EXISTS_TAC`(dimindex (:M)-k + 1):num`
2834 THEN ASM_REWRITE_TAC[]
2835 THEN MRESAL_TAC POWER_FF_OF_HYP_EQ1[`k:num`;`dimindex (:M) - k + 1`;`(row (dimindex (:M) - k + 1:num) (vecmats (l:real^(M,3)finite_product)))`;`row (SUC ((dimindex (:M) - k + 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`;`x:real^3#real^3`][ARITH_RULE`dimindex (:M)<=dimindex (:M)/\ 1<=1`]
2836 THEN POP_ASSUM MATCH_MP_TAC
2842 let F_SY_EQ_FACE1=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2844 /\ 1<= i /\ i<= dimindex (:M)
2845 /\ row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l)=x
2846 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2847 /\ row i (vecmats l)= row j (vecmats l)
2849 /\ S={row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats l) | 1 <= i /\
2852 face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x`,
2854 THEN MRESA_TAC (GEN_ALL FACE_HYP_FAN_SY1)[`S:(real^3#real^3->bool)`;`l:real^(M,3)finite_product`;`row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)),row 1 (vecmats l)`]
2855 THEN MATCH_MP_TAC lemma_face_identity
2856 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2857 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
2858 THEN EXISTS_TAC`i:num`
2859 THEN ASM_REWRITE_TAC[]);;
2863 let DART_OF_HYP_EQ_FACE_SY=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2865 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2866 /\ row i (vecmats l)= row j (vecmats l)
2868 /\ x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))
2869 /\ S= face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x
2870 ==> darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))= S UNION IMAGE (nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l))) S`,
2872 THEN POP_ASSUM MP_TAC
2873 THEN POP_ASSUM MP_TAC
2874 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M)`)
2876 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
2877 THEN POP_ASSUM MP_TAC
2878 THEN DISCH_THEN(LABEL_TAC"THY")
2879 THEN GEN_REWRITE_TAC( LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM]
2883 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[F_SY;]
2884 THEN REWRITE_TAC[IN_ELIM_THM]
2886 THEN REMOVE_THEN"THY"(fun th-> REWRITE_TAC[SYM th])
2887 THEN MRESA_TAC (GEN_ALL F_SY_EQ_FACE)[`i:num`;`l:real^(M,3)finite_product`;`x:real^3#real^3`]
2888 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2890 THEN MATCH_MP_TAC DART_OF_HYP_SY_EQ
2891 THEN ASM_REWRITE_TAC[];
2893 THEN REMOVE_THEN"THY"(fun th-> REWRITE_TAC[SYM th])
2894 THEN MRESA1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`
2895 THEN REWRITE_TAC[IN_ELIM_THM]
2897 THEN MRESA_TAC (GEN_ALL F_SY_EQ_FACE1)[`i:num`;`{row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats (l:real^(M,3)finite_product)) |
2899 i <= dimindex (:M)}`;`l:real^(M,3)finite_product`;`x:real^3#real^3`]
2900 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2902 THEN MATCH_MP_TAC DART_OF_HYP_SY_EQ1
2903 THEN ASM_REWRITE_TAC[]]);;
2905 let ID_FF_OF_HYP_NOT_DARTS=prove(`!n. FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2907 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2908 /\ row i (vecmats l)= row j (vecmats l)
2910 /\ ~(v,u IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l)))
2911 ==>(ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER n) (v,u) =
2915 REWRITE_TAC[POWER;I_DEF];
2917 THEN DISCH_THEN(LABEL_TAC"THY")
2918 THEN REPEAT STRIP_TAC
2919 THEN REMOVE_THEN"THY"MP_TAC
2920 THEN ASM_REWRITE_TAC[Hypermap.COM_POWER;o_DEF]
2922 THEN ASM_REWRITE_TAC[ff_of_hyp]]);;
2926 let CARD_FACE_SY=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2928 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2929 /\ row i (vecmats l)= row j (vecmats l)
2931 /\ x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))
2932 /\ S= face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x
2933 ==> CARD S= dimindex (:M)`,
2935 THEN POP_ASSUM MP_TAC
2936 THEN POP_ASSUM MP_TAC
2937 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M)`)
2939 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
2940 THEN POP_ASSUM MP_TAC
2941 THEN DISCH_THEN(LABEL_TAC"THY")
2942 THEN GEN_REWRITE_TAC( LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM]
2946 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[F_SY;]
2947 THEN REWRITE_TAC[IN_ELIM_THM]
2949 THEN REMOVE_THEN"THY"(fun th-> REWRITE_TAC[SYM th])
2950 THEN MRESA_TAC (GEN_ALL F_SY_EQ_FACE)[`i:num`;`l:real^(M,3)finite_product`;`x:real^3#real^3`]
2951 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2953 THEN MRESA1_TAC(GEN_ALL CARD_F_SY_EQ)`l:real^(M,3)finite_product`;
2955 THEN REMOVE_THEN"THY"(fun th-> REWRITE_TAC[SYM th])
2956 THEN MRESA1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`
2957 THEN REWRITE_TAC[IN_ELIM_THM]
2959 THEN MRESA_TAC (GEN_ALL F_SY_EQ_FACE1)[`i:num`;`{row (SUC (i MOD dimindex (:M))) (vecmats l),row i (vecmats (l:real^(M,3)finite_product)) |
2961 i <= dimindex (:M)}`;`l:real^(M,3)finite_product`;`x:real^3#real^3`]
2962 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2964 THEN MRESA1_TAC(GEN_ALL CARD_IMAGE_F_SY_EQ)`l:real^(M,3)finite_product`]);;
2968 let FF_OF_HYP_POWER_EQ_ID=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2970 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2971 /\ row i (vecmats l)= row j (vecmats l)
2973 ==>ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER dimindex (:M) =
2975 REWRITE_TAC[FUN_EQ_THM;I_DEF]
2976 THEN REPEAT STRIP_TAC
2977 THEN DISJ_CASES_TAC(SET_RULE`~(x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))) \/ x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats (l:real^(M,3)finite_product)))`)
2980 THEN ONCE_REWRITE_TAC[GSYM PAIR]
2982 THEN MRESA_TAC (GEN_ALL ID_FF_OF_HYP_NOT_DARTS)[`l:real^(M,3)finite_product`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`dimindex (:M)`];
2983 MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
2984 THEN MRESAL_TAC (Hypermap.lemma_in_face)[`(hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))))`;`x:real^3#real^3`;`0`][POWER;I_DEF]
2985 THEN MRESA_TAC (GEN_ALL CARD_FACE_SY)[`l:real^(M,3)finite_product`;`x:real^3#real^3`;`face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product))))) x`]
2986 THEN MRESA_TAC (Lvducxu.FACE_CYCLE_CARD)[`x:real^3#real^3`;`x:real^3#real^3`;`(hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))))`]]);;
2991 let EXISTS_POINT_DART_OF_HYP=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
2993 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
2994 /\ row i (vecmats l)= row j (vecmats l)
2996 ==> ?x. x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))`,
2998 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M)`)
3000 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
3001 THEN EXISTS_TAC`row 1 (vecmats l), row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
3002 THEN MATCH_MP_TAC(SET_RULE`a IN A ==> a IN A UNION B`)
3003 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
3005 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1`]
3006 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1<= dimindex (:M)`)
3009 let FF_OF_HYP_NOT_EQ_ID=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3011 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3012 /\ row i (vecmats l)= row j (vecmats l)
3014 ==>(!i. 0 < i /\ i < dimindex (:M)
3015 ==> ~(ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER i =
3017 REWRITE_TAC[FUN_EQ_THM;I_DEF]
3018 THEN REPEAT STRIP_TAC
3019 THEN POP_ASSUM MP_TAC
3020 THEN MRESA1_TAC (GEN_ALL EXISTS_POINT_DART_OF_HYP)`l:real^(M,3)finite_product`
3022 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:real^3#real^3`)
3023 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
3024 THEN MRESA_TAC (GEN_ALL CARD_FACE_SY)[`l:real^(M,3)finite_product`;`x:real^3#real^3`;`face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product))))) x`]
3025 THEN MRESAL_TAC (Hypermap.lemma_congruence_on_face)[`(hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))))`;`x:real^3#real^3`;`i:num`;`0`][POWER;I_DEF]
3026 THEN POP_ASSUM MP_TAC
3027 THEN FIND_ASSUM MP_TAC`0< i`
3031 let FF_OF_HYP_HAS_ORDERS=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3033 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3034 /\ row i (vecmats l)= row j (vecmats l)
3036 ==> ff_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) has_orders (dimindex (:M))`,
3037 REWRITE_TAC[has_orders;GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
3038 THEN STRIP_TAC THEN STRIP_TAC
3039 THEN MRESA1_TAC (GEN_ALL FF_OF_HYP_NOT_EQ_ID)`l:real^(M,3)finite_product`
3040 THEN MRESA1_TAC (GEN_ALL FF_OF_HYP_POWER_EQ_ID)`l:real^(M,3)finite_product`);;
3045 let CARD_NODE_SY=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3047 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3048 /\ row i (vecmats l)= row j (vecmats l)
3050 /\ x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))
3051 ==> CARD (node (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x)= 2`,
3053 THEN POP_ASSUM MP_TAC
3054 THEN POP_ASSUM MP_TAC
3055 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
3056 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M) /\ 1<= dimindex (:M)/\ SUC 1 <= dimindex (:M) /\ ~(SUC 1= dimindex(:M))`)
3058 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
3059 THEN POP_ASSUM MP_TAC
3060 THEN DISCH_THEN(LABEL_TAC"THY")
3061 THEN REWRITE_TAC[Hypermap.NODE_OF_SIZE_2]
3062 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
3063 THEN GEN_REWRITE_TAC( LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM]
3066 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[F_SY;]
3067 THEN REWRITE_TAC[IN_ELIM_THM]
3069 THEN ABBREV_TAC`u=row i (vecmats (l:real^(M,3)finite_product))`
3070 THEN ABBREV_TAC`v=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
3071 THEN POP_ASSUM MP_TAC
3072 THEN POP_ASSUM MP_TAC
3073 THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)
3075 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
3076 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
3079 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`dimindex (:M):num`;`(row
3080 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
3081 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3082 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3083 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`dimindex (:M):num`;`(row
3084 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
3085 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3086 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;PAIR_EQ])
3088 THEN REMOVE_THEN"THYGIANG"(fun th-> MRESAL_TAC th[`SUC 1`;`dimindex(:M)`][ARITH_RULE`1<= SUC 1/\ dimindex (:M)<= dimindex(:M)`]);
3089 MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ i= SUC (i-1)`)
3091 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
3092 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
3093 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
3096 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i-1:num`;`(row
3097 (i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3098 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3099 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3100 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`i-1:num`;`(row
3101 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3102 (i-1) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3103 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;PAIR_EQ])
3104 THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> SUC (i-1)= i`)
3106 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
3107 THEN MRESA_TAC (GEN_ALL SUC_POWER2_NOT)[`i-1:num`;`dimindex (:M)`]
3108 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
3109 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3110 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3111 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3112 THEN POP_ASSUM MP_TAC
3114 REMOVE_THEN"THYGIANG"(fun th-> MRESAL_TAC th[`i-1`;`(SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M)))`][ARITH_RULE`1<= SUC i/\ dimindex (:M)<= dimindex(:M)`]);
3116 THEN MRESAL1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`[IN_ELIM_THM]
3118 THEN ABBREV_TAC`u=row i (vecmats (l:real^(M,3)finite_product))`
3119 THEN ABBREV_TAC`v=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
3120 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`i:num`;`(row
3121 (SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3122 (i) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3123 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3124 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i:num`;`(row
3125 (i) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i ) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3126 (SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3127 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;PAIR_EQ])
3128 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
3129 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3130 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3131 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3132 THEN POP_ASSUM MP_TAC
3134 SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
3135 SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3136 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3137 THEN MRESAL_TAC DIVISION[`SUC (i MOD dimindex (:M)):num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3138 THEN POP_ASSUM MP_TAC
3140 MRESA_TAC (GEN_ALL SUC_POWER2_NOT)[`i:num`;`dimindex (:M)`]
3141 THEN REMOVE_THEN"THYGIANG"(fun th-> MRESAL_TAC th[`i:num`;`(SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M)))`][ARITH_RULE`1<= SUC i/\ dimindex (:M)<= dimindex(:M)`])]);;
3148 let NODE_SY_POWER_ID=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3150 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3151 /\ row i (vecmats l)= row j (vecmats l)
3153 /\ x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))
3154 ==> node_map (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l))))
3155 (node_map (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x) =
3158 THEN POP_ASSUM MP_TAC
3159 THEN POP_ASSUM MP_TAC
3160 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
3161 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M) /\ 1<= dimindex (:M)/\ SUC 1 <= dimindex (:M) /\ ~(SUC 1= dimindex(:M))`)
3163 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
3164 THEN POP_ASSUM MP_TAC
3165 THEN DISCH_THEN(LABEL_TAC"THY")
3166 THEN REWRITE_TAC[Hypermap.NODE_OF_SIZE_2]
3167 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
3168 THEN GEN_REWRITE_TAC( LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM]
3171 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[F_SY;]
3172 THEN REWRITE_TAC[IN_ELIM_THM]
3174 THEN ABBREV_TAC`u=row i (vecmats (l:real^(M,3)finite_product))`
3175 THEN ABBREV_TAC`v=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
3176 THEN POP_ASSUM MP_TAC
3177 THEN POP_ASSUM MP_TAC
3178 THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)
3180 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
3181 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
3184 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`dimindex (:M):num`;`(row
3185 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
3186 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3187 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3188 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`dimindex (:M):num`;`(row
3189 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
3190 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1];
3191 MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ i= SUC (i-1)`)
3193 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
3194 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
3195 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
3198 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i-1:num`;`(row
3199 (i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3200 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3201 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3202 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`i-1:num`;`(row
3203 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3204 (i-1) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1];
3206 THEN MRESAL1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`[IN_ELIM_THM]
3208 THEN ABBREV_TAC`u=row i (vecmats (l:real^(M,3)finite_product))`
3209 THEN ABBREV_TAC`v=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
3210 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`i:num`;`(row
3211 (SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3212 (i) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3213 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3214 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i:num`;`(row
3215 (i) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i ) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3216 (SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3217 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;PAIR_EQ])
3230 let ID_NN_OF_HYP_NOT_DARTS=prove(`!n. FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3232 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3233 /\ row i (vecmats l)= row j (vecmats l)
3235 /\ ~(v,u IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l)))
3236 ==>(nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER n) (v,u) =
3240 REWRITE_TAC[POWER;I_DEF];
3242 THEN DISCH_THEN(LABEL_TAC"THY")
3243 THEN REPEAT STRIP_TAC
3244 THEN REMOVE_THEN"THY"MP_TAC
3245 THEN ASM_REWRITE_TAC[Hypermap.COM_POWER;o_DEF]
3247 THEN ASM_REWRITE_TAC[nn_of_hyp]]);;
3253 let NN_OF_HYP_POWER_EQ_ID=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3255 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3256 /\ row i (vecmats l)= row j (vecmats l)
3258 ==>nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER 2 =
3260 REWRITE_TAC[FUN_EQ_THM;I_DEF]
3261 THEN REPEAT STRIP_TAC
3262 THEN DISJ_CASES_TAC(SET_RULE`~(x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))) \/ x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats (l:real^(M,3)finite_product)))`)
3265 THEN ONCE_REWRITE_TAC[GSYM PAIR]
3267 THEN MRESA_TAC (GEN_ALL ID_NN_OF_HYP_NOT_DARTS)[`l:real^(M,3)finite_product`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`2`];
3268 REWRITE_TAC[ARITH_RULE`2=SUC(SUC 0)`;POWER;I_DEF;o_DEF]
3269 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
3270 THEN MRESA_TAC (GEN_ALL NODE_SY_POWER_ID)[`l:real^(M,3)finite_product`;`x:real^3#real^3`]]);;
3277 let NODE_SY_NOT_ID=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3279 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3280 /\ row i (vecmats l)= row j (vecmats l)
3282 /\ x IN darts_of_hyp (E_SY (vecmats l)) (V_SY (vecmats l))
3283 ==> ~(node_map (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l)))) x =
3287 THEN POP_ASSUM MP_TAC
3288 THEN POP_ASSUM MP_TAC
3289 THEN POP_ASSUM MP_TAC
3290 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
3291 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M) /\ 1<= dimindex (:M)/\ SUC 1 <= dimindex (:M) /\ ~(SUC 1= dimindex(:M))`)
3293 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
3294 THEN POP_ASSUM MP_TAC
3295 THEN DISCH_THEN(LABEL_TAC"THY")
3296 THEN REWRITE_TAC[Hypermap.NODE_OF_SIZE_2]
3297 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
3298 THEN GEN_REWRITE_TAC( LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM]
3301 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[F_SY;]
3302 THEN REWRITE_TAC[IN_ELIM_THM]
3304 THEN ABBREV_TAC`u=row i (vecmats (l:real^(M,3)finite_product))`
3305 THEN ABBREV_TAC`v=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
3306 THEN POP_ASSUM MP_TAC
3307 THEN POP_ASSUM MP_TAC
3308 THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`)
3310 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
3311 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
3314 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`dimindex (:M):num`;`(row
3315 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
3316 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3317 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3318 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`dimindex (:M):num`;`(row
3319 (SUC 1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row
3320 (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3321 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;PAIR_EQ])
3323 THEN REMOVE_THEN"THYGIANG"(fun th-> MRESAL_TAC th[`SUC 1`;`dimindex(:M)`][ARITH_RULE`1<= SUC 1/\ dimindex (:M)<= dimindex(:M)`]);
3324 MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ i= SUC (i-1)`)
3326 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
3327 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
3328 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
3331 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i-1:num`;`(row
3332 (i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3333 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3334 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3335 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`i-1:num`;`(row
3336 (SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i - 1) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3337 (i-1) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3338 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;PAIR_EQ])
3339 THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> SUC (i-1)= i`)
3341 THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
3342 THEN MRESA_TAC (GEN_ALL SUC_POWER2_NOT)[`i-1:num`;`dimindex (:M)`]
3343 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
3344 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3345 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3346 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3347 THEN POP_ASSUM MP_TAC
3349 REMOVE_THEN"THYGIANG"(fun th-> MRESAL_TAC th[`i-1`;`(SUC (SUC ((i - 1) MOD dimindex (:M)) MOD dimindex (:M)))`][ARITH_RULE`1<= SUC i/\ dimindex (:M)<= dimindex(:M)`]);
3351 THEN MRESAL1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`[IN_ELIM_THM]
3353 THEN ABBREV_TAC`u=row i (vecmats (l:real^(M,3)finite_product))`
3354 THEN ABBREV_TAC`v=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
3355 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ)[`i:num`;`(row
3356 (SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3357 (i) (vecmats (l:real^(M,3)finite_product)))`;][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3358 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3359 THEN MRESAL_TAC(GEN_ALL NN_OF_HYP_EQ1)[`i:num`;`(row
3360 (i) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`;`(row (SUC ((i ) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row
3361 (SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]
3362 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;PAIR_EQ])
3363 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
3364 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3365 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3366 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3367 THEN POP_ASSUM MP_TAC
3369 SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
3370 SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3371 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3372 THEN MRESAL_TAC DIVISION[`SUC (i MOD dimindex (:M)):num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3373 THEN POP_ASSUM MP_TAC
3375 MRESA_TAC (GEN_ALL SUC_POWER2_NOT)[`i:num`;`dimindex (:M)`]
3376 THEN REMOVE_THEN"THYGIANG"(fun th-> MRESAL_TAC th[`i:num`;`(SUC (SUC ((i) MOD dimindex (:M)) MOD dimindex (:M)))`][ARITH_RULE`1<= SUC i/\ dimindex (:M)<= dimindex(:M)`])]);;
3384 let NN_OF_HYP_NOT_EQ_ID=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3386 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3387 /\ row i (vecmats l)= row j (vecmats l)
3389 ==>(!i. 0 < i /\ i < 2
3390 ==> ~(nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) POWER i =
3392 REWRITE_TAC[FUN_EQ_THM;I_DEF;ARITH_RULE`0<i /\ i< 2<=> i=1`]
3393 THEN REPEAT STRIP_TAC
3394 THEN POP_ASSUM MP_TAC
3395 THEN ASM_REWRITE_TAC[POWER_1]
3396 THEN MRESA1_TAC (GEN_ALL EXISTS_POINT_DART_OF_HYP)`l:real^(M,3)finite_product`
3398 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:real^3#real^3`)
3399 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
3400 THEN MRESA_TAC (GEN_ALL NODE_SY_NOT_ID)[`l:real^(M,3)finite_product`;`x:real^3#real^3`]);;
3405 let NN_OF_HYP_HAS_ORDERS=prove(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3407 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3408 /\ row i (vecmats l)= row j (vecmats l)
3410 ==> nn_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) has_orders 2`,
3411 REWRITE_TAC[has_orders;GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
3412 THEN STRIP_TAC THEN STRIP_TAC
3413 THEN MRESA1_TAC (GEN_ALL NN_OF_HYP_NOT_EQ_ID)`l:real^(M,3)finite_product`
3414 THEN MRESA1_TAC (GEN_ALL NN_OF_HYP_POWER_EQ_ID)`l:real^(M,3)finite_product`);;
3417 let EE_OF_HYP_HAS_ORDERS=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3419 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3420 /\ row i (vecmats l)= row j (vecmats l)
3422 ==> ee_of_hyp (vec 0,V_SY (vecmats l),E_SY (vecmats l)) has_orders 2`,
3423 [REWRITE_TAC[has_orders;GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER;ARITH_RULE`2= SUC(SUC 0)`;POWER;I_DEF;o_DEF]
3424 THEN REWRITE_TAC[ARITH_RULE`SUC(SUC 0)=2`]
3426 THEN POP_ASSUM MP_TAC
3427 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
3428 THEN MRESAL_TAC(GEN_ALL Lvducxu.FIRST_AAUHTVE2)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`][o_DEF;I_DEF]
3430 REWRITE_TAC[FUN_EQ_THM;I_DEF;ARITH_RULE`0<i /\ i< 2<=> i=1`]
3431 THEN REPEAT STRIP_TAC
3432 THEN POP_ASSUM MP_TAC
3433 THEN ASM_REWRITE_TAC[POWER_1]
3434 THEN MRESA1_TAC (GEN_ALL EXISTS_POINT_DART_OF_HYP)`l:real^(M,3)finite_product`
3436 THEN POP_ASSUM(fun th-> MRESA1_TAC th`FST (x:real^3#real^3),SND x`)
3437 THEN POP_ASSUM MP_TAC
3439 THEN ASM_REWRITE_TAC[ee_of_hyp2;PAIR_EQ]
3440 THEN MRESA_TAC PAIR_EQ[`SND (x:real^3#real^3)`;`FST (x:real^3#real^3)`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`]
3441 THEN REMOVE_ASSUM_TAC
3442 THEN POP_ASSUM MP_TAC
3443 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M) /\ 1<= dimindex (:M)/\ SUC 1 <= dimindex (:M) /\ ~(SUC 1= dimindex(:M))`)
3445 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
3446 THEN REWRITE_TAC[UNION;IN_ELIM_THM]
3449 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
3452 THEN REMOVE_ASSUM_TAC
3453 THEN SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\
3454 SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3455 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3456 THEN MRESAL_TAC DIVISION[`i':num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3457 THEN POP_ASSUM MP_TAC
3459 REMOVE_THEN"THYGIANG"(fun th-> MRESA_TAC th[`i':num`;`(SUC (i' MOD dimindex (:M)))`])
3460 THEN POP_ASSUM MP_TAC
3461 THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i':num`;`dimindex (:M):num`];
3463 THEN MRESAL1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`[IN_ELIM_THM]
3466 THEN REMOVE_ASSUM_TAC
3467 THEN SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\
3468 SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3469 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3470 THEN MRESAL_TAC DIVISION[`i':num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3471 THEN POP_ASSUM MP_TAC
3473 REMOVE_THEN"THYGIANG"(fun th-> MRESA_TAC th[`i':num`;`(SUC (i' MOD dimindex (:M)))`])
3474 THEN POP_ASSUM MP_TAC
3475 THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i':num`;`dimindex (:M):num`];
3477 THEN REWRITE_TAC[FUN_EQ_THM;I_DEF;ARITH_RULE`0<i /\ i< 2<=> i=1`]
3478 THEN REPEAT STRIP_TAC
3479 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:real^3#real^3`)
3480 THEN POP_ASSUM MP_TAC
3481 THEN REWRITE_TAC[ee_of_hyp2]]);;
3484 let DIH2K_FAN_HYP_SY=prove_by_refinement(` FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))
3486 /\ (!i j. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M)
3487 /\ row i (vecmats l)= row j (vecmats l)
3489 ==> dih2k (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats l))))
3490 (CARD (F_SY (vecmats l)))`,
3493 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
3494 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M) /\ 1<= dimindex (:M)/\ SUC 1 <= dimindex (:M) /\ ~(SUC 1= dimindex(:M))`)
3496 THEN MRESA1_TAC (GEN_ALL FF_OF_HYP_HAS_ORDERS)`l:real^(M,3)finite_product`
3497 THEN MRESA1_TAC (GEN_ALL NN_OF_HYP_HAS_ORDERS)`l:real^(M,3)finite_product`
3498 THEN MRESA1_TAC (GEN_ALL EE_OF_HYP_HAS_ORDERS)`l:real^(M,3)finite_product`
3499 THEN MRESA1_TAC (GEN_ALL CARD_DART_OF_HYP)`l:real^(M,3)finite_product`
3500 THEN MRESA1_TAC (GEN_ALL CARD_F_SY_EQ)`l:real^(M,3)finite_product`
3502 CONV_TAC(TOP_DEPTH_CONV let_CONV)
3503 THEN REPEAT STRIP_TAC
3504 THEN MRESA_TAC (GEN_ALL DART_OF_HYP_EQ_FACE_SY)[`x:real^3#real^3`;`l:real^(M,3)finite_product`;`face (hypermap (HYP (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product))))) x`];
3506 THEN REMOVE_ASSUM_TAC
3507 THEN REMOVE_ASSUM_TAC
3508 THEN REMOVE_ASSUM_TAC
3509 THEN REMOVE_ASSUM_TAC
3510 THEN REMOVE_ASSUM_TAC
3511 THEN REMOVE_ASSUM_TAC
3512 THEN REMOVE_ASSUM_TAC
3513 THEN REMOVE_ASSUM_TAC
3514 THEN REMOVE_ASSUM_TAC
3515 THEN REMOVE_ASSUM_TAC
3516 THEN REMOVE_ASSUM_TAC
3517 THEN REMOVE_ASSUM_TAC
3519 THEN REWRITE_TAC[has_orders;GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER;ARITH_RULE`2= SUC(SUC 0)`;POWER;I_DEF;o_DEF]
3520 THEN REWRITE_TAC[ARITH_RULE`SUC(SUC 0)=2`]
3524 THEN POP_ASSUM MP_TAC
3525 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
3526 THEN MRESAL_TAC(GEN_ALL Lvducxu.FIRST_AAUHTVE2)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`][o_DEF;I_DEF]
3528 REWRITE_TAC[FUN_EQ_THM;I_DEF;ARITH_RULE`0<i /\ i< 2<=> i=1`]
3529 THEN REPEAT STRIP_TAC
3530 THEN POP_ASSUM MP_TAC
3531 THEN ASM_REWRITE_TAC[POWER_1]
3532 THEN MRESA1_TAC (GEN_ALL EXISTS_POINT_DART_OF_HYP)`l:real^(M,3)finite_product`
3534 THEN POP_ASSUM(fun th-> MRESA1_TAC th`FST (x:real^3#real^3),SND x`)
3535 THEN POP_ASSUM MP_TAC
3537 THEN ASM_REWRITE_TAC[ee_of_hyp2;PAIR_EQ]
3538 THEN MRESA_TAC PAIR_EQ[`SND (x:real^3#real^3)`;`FST (x:real^3#real^3)`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`]
3539 THEN REMOVE_ASSUM_TAC
3540 THEN POP_ASSUM MP_TAC
3541 THEN MP_TAC(ARITH_RULE`2< dimindex (:M)==> 1< dimindex (:M) /\ 1<= dimindex (:M)/\ SUC 1 <= dimindex (:M) /\ ~(SUC 1= dimindex(:M))`)
3543 THEN MRESA1_TAC (GEN_ALL DART_OF_HYP_SY_EQ)`l:real^(M,3)finite_product`
3544 THEN REWRITE_TAC[UNION;IN_ELIM_THM]
3547 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
3550 THEN REMOVE_ASSUM_TAC
3551 THEN SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\
3552 SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3553 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3554 THEN MRESAL_TAC DIVISION[`i':num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3555 THEN POP_ASSUM MP_TAC
3557 REMOVE_THEN"THYGIANG"(fun th-> MRESA_TAC th[`i':num`;`(SUC (i' MOD dimindex (:M)))`])
3558 THEN POP_ASSUM MP_TAC
3559 THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i':num`;`dimindex (:M):num`];
3561 THEN MRESAL1_TAC (GEN_ALL IMAGE_NN_OF_HYP_F_SY)`l:real^(M,3)finite_product`[IN_ELIM_THM]
3564 THEN REMOVE_ASSUM_TAC
3565 THEN SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\
3566 SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
3567 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
3568 THEN MRESAL_TAC DIVISION[`i':num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
3569 THEN POP_ASSUM MP_TAC
3571 REMOVE_THEN"THYGIANG"(fun th-> MRESA_TAC th[`i':num`;`(SUC (i' MOD dimindex (:M)))`])
3572 THEN POP_ASSUM MP_TAC
3573 THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i':num`;`dimindex (:M):num`]]);;