2 let truncate_gamma23_x_A = new_definition `truncate_gamma23_x_A iw1 m1 m2 m6 =
4 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
5 dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
7 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (#0.08))) *
8 uni((truncate_gamma2_x m1), proj_x1)`;;
11 let truncate_gamma23_x_C = new_definition `truncate_gamma23_x_C d iw1 m1 m2 m6 =
13 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
14 dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
16 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (d))) *
17 uni((truncate_gamma2_x m1), proj_x1)`;;
20 let truncate_gamma23_x_B = new_definition
21 `truncate_gamma23_x_B m1 =
22 (dih_x - constant6 (&2 * #0.08)) *
23 uni((truncate_gamma2_x m1),proj_x1)`;;
26 let nonf_truncate_gamma23_x_A = prove_by_refinement(
27 `!iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6.
28 truncate_gamma23_x_A iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6 =
29 truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
30 (dih_x x1 x2 x3 x4 x5 x6 -
31 (truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 + #0.08)) *
32 truncate_gamma2_x m1 x1`,
35 REWRITE_TAC[truncate_gamma23_x_A;add6;scalar6;compose6;sub6;mul6;mk_126;mk_135;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;dummy6;constant6;two6;uni]
40 let nonf_truncate_gamma23_x_B = prove_by_refinement(
41 `! m1 x1 x2 x3 x4 x5 x6.
42 truncate_gamma23_x_B m1 x1 x2 x3 x4 x5 x6 =
43 (dih_x x1 x2 x3 x4 x5 x6 - &2 * #0.08) * truncate_gamma2_x m1 x1 `,
46 REWRITE_TAC[truncate_gamma23_x_B;add6;scalar6;compose6;sub6;mul6;mk_126;mk_135;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;dummy6;constant6;two6;uni]
50 let nonf_truncate_gamma23_x_C = prove_by_refinement(
51 `!iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6.
52 truncate_gamma23_x_C d iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6 =
53 truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
54 (dih_x x1 x2 x3 x4 x5 x6 -
55 (truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 + d)) *
56 truncate_gamma2_x m1 x1`,
59 REWRITE_TAC[truncate_gamma23_x_C;add6;scalar6;compose6;sub6;mul6;mk_126;mk_135;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;dummy6;constant6;two6;uni]
63 let nonf_truncate_gamma3f_x = prove_by_refinement(
64 `!d m4 m5 m6 x1 x2 x3 x4 x5 x6.
65 truncate_gamma3f_x d m4 m5 m6 x1 x2 x3 x4 x5 x6 =
66 truncate_vol3r_456 d x1 x2 x3 x4 x5 x6 -
67 truncate_vol3f d m4 m5 m6 x1 x2 x3 x4 x5 x6`,
70 BY(REWRITE_TAC[truncate_gamma3f_x;sub6])
74 let nonf_truncate_gamma23_x = prove_by_refinement(
75 `!iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 x4 x5 x6.
76 truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 x4 x5 x6 =
77 truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
78 truncate_gamma3f_x #0.14 m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 +
79 (dih_x x1 x2 x3 x4 x5 x6 -
80 (truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 +
81 truncate_dih_x #0.14 x1 (&2) x3 (&2) x5 (&2))) *
82 truncate_gamma2_x m1 x1`,
85 BY(REWRITE_TAC[truncate_gamma23_x;add6;scalar6;compose6;sub6;mul6;mk_126;mk_135;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;dummy6;constant6;two6;uni])
89 let nonf_truncate_sol_x = prove_by_refinement(
90 `!c x1 x2 x3 x4 x5 x6.
91 truncate_sol_x c x1 x2 x3 x4 x5 x6 = truncate_dih_x c x1 x2 x3 x4 x5 x6 +
92 truncate_dih_x c x2 x3 x1 x5 x6 x4 + truncate_dih_x c x3 x1 x2 x6 x4 x5 - pi`,
95 BY(REWRITE_TAC[truncate_sol_x;add6;sub6;constant6;Sphere.rotate2;Sphere.rotate3])
99 let nonf_truncate_vol_x = prove_by_refinement(
100 `!c x1 x2 x3 x4 x5 x6.
101 truncate_vol_x c x1 x2 x3 x4 x5 x6 = (truncate_sqrt c (delta_x x1 x2 x3 x4 x5 x6)) / &12`,
104 REWRITE_TAC[truncate_vol_x;scalar6;uni;];
109 let nonf_truncate_vol3r_456 = prove_by_refinement(
110 `!c x1 x2 x3 x4 x5 x6.
111 truncate_vol3r_456 c x1 x2 x3 x4 x5 x6 =
112 truncate_vol_x c (&2) (&2) (&2) x4 x5 x6`,
115 BY(REWRITE_TAC[mk_456;truncate_vol3r_456;compose6;two6;proj_x4;proj_x5;proj_x6;constant6])
119 let nonf_truncate_vol3f = prove_by_refinement(
120 `!c m4 m5 m6 x1 x2 x3 x4 x5 x6.
121 truncate_vol3f c m4 m5 m6 x1 x2 x3 x4 x5 x6 =
122 ((truncate_sol_x c x5 (&2) x4 (&2) x6 (&2) +
123 truncate_sol_x c x6 (&2) x5 (&2) x4 (&2) +
124 truncate_sol_x c x4 (&2) x6 (&2) x5 (&2)) *
127 ((lfun (sqrt x4 * #0.5) * m4) * truncate_dih_x c x4 (&2) x6 (&2) x5 (&2) +
128 (lfun (sqrt x5 * #0.5) * m5) * truncate_dih_x c x5 (&2) x4 (&2) x6 (&2) +
129 (lfun (sqrt x6 * #0.5) * m6) * truncate_dih_x c x6 (&2) x5 (&2) x4 (&2)) *
134 BY(REWRITE_TAC[truncate_vol3f;add6;scalar6;mul6;uni;proj_y4;proj_y5;proj_y6;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;sub6;mk_456;compose6;two6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6])
138 let functional_delta_pent_x = prove_by_refinement(
139 `delta_pent_x = compose6
140 delta_x proj_x1 proj_x2 proj_x6 four6 four6 (constant6 (#10.4976))`,
143 REWRITE_TAC[FUN_EQ_THM;Sphere.delta_pent_x;proj_x1;proj_x2;proj_x6;four6;constant6;compose6];
144 REPEAT WEAK_STRIP_TAC;
151 let promote_pow3r = INST_TYPE [(`:real`,`:A`);(`:real`,`:B`);(`:real`,`:C`);(`:real`,`:D`);(`:real`,`:E`)] promote_pow3;;
156 let dih_y_div_sqrtdelta_posbranch = new_definition
157 `dih_y_div_sqrtdelta_posbranch = y_of_x dih_x_div_sqrtdelta_posbranch`;;
162 let rhof_x = define `rhof_x x = rho (sqrt x)`;;
167 let ineq_lemma = prove_by_refinement(
168 `!a x b. &0 <= a /\ &0 <= b /\ a pow 2 <= x /\ x <= b pow 2 ==> a <= sqrt x /\ sqrt x <= b`,
173 SUBGOAL_THEN `&0 <= x` MP_TAC;
174 ASM_MESON_TAC [REAL_LE_TRANS;Collect_geom.REAL_LE_SQUARE_POW];
175 ASM_MESON_TAC[Collect_geom.POW2_COND;SQRT_WORKS];
183 let ineq_square = prove_by_refinement(
184 `((!y1 y2 y3 y4 y5 y6.
186 [(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6)]
187 (P y1 y2 y3 y4 y5 y6)) ==>
188 ((&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4 /\ &0 <= a5 /\ &0 <= a6 /\
189 &0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ &0 <= b4 /\ &0 <= b5 /\ &0 <= b6 )) ==>
191 ineq [(a1 pow 2,x1,b1 pow 2);(a2 pow 2,x2,b2 pow 2);(a3 pow 2,x3,b3 pow 2);
192 (a4 pow 2,x4,b4 pow 2);(a5 pow 2,x5,b5 pow 2);(a6 pow 2,x6,b6 pow 2)]
193 (P (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6))))`,
198 FIRST_X_ASSUM (fun t-> MP_TAC (SPECL [`sqrt x1`;`sqrt x2`;`sqrt x3`;`sqrt x4`;`sqrt x5`;`sqrt x6`] t));
199 ASM_MESON_TAC[ineq_lemma];
207 let gamma3f_135_n_alt = prove_by_refinement(
209 gamma3f_135_n y1 y2 y3 y4 y5 y6 = gamma3f_135_s_n y1 y2 y3 y4 y5 y6 +
211 (y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 +
212 y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 +
213 y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6)`,
216 REWRITE_TAC[Sphere.gamma3f_135_n;gamma3f_135_s_n;lmdih_x_n;lmdih3_x_n;lmdih5_x_n;Sphere.y_of_x;Sphere.delta_y];
221 let gamma3f_126_n_alt = prove_by_refinement(
223 gamma3f_126_n y1 y2 y3 y4 y5 y6 = gamma3f_126_s_n y1 y2 y3 y4 y5 y6 +
225 (y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 +
226 y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 +
227 y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6)`,
230 REWRITE_TAC[Sphere.gamma3f_126_n;gamma3f_126_s_n;lmdih_x_n;lmdih2_x_n;lmdih6_x_n;Sphere.y_of_x;Sphere.delta_y];
235 let gamma23f_n_alt = prove_by_refinement(
236 `!y1 y2 y3 y4 y5 y6 w1 w2 f. gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 f =
237 gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
238 gamma3f_135_n y1 sqrt2 y3 sqrt2 y5 sqrt2 / &w2 +
239 gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f`,
242 REWRITE_TAC[gamma3f_vLR_n;Sphere.gamma23f_n];
246 let gamma23f_126_03_n_alt = prove_by_refinement(
247 `!y1 y2 y3 y4 y5 y6 f. gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 sqrt2 f =
248 gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
249 gamma3f_vL_n y1 y2 y3 y4 y5 y6 f`,
252 REWRITE_TAC[gamma3f_vL_n;Sphere.gamma23f_126_03_n];
256 let gamma3f_vLR_n0_case = prove_by_refinement(
257 `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lmfun =
258 gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6`,
262 REWRITE_TAC[gamma3f_vLR_n;gamma3f_vLR_n0;Sphere.vol2f;];
263 ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
267 let gamma3f_vLR_nlfun_case = prove_by_refinement(
268 `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lmfun =
269 gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6`,
273 REWRITE_TAC[gamma3f_vLR_n;Sphere.vol2f;gamma3f_vLR_nlfun];
274 ASM_SIMP_TAC[lmfun_lfun];
278 let gamma3f_vL_n0_case = prove_by_refinement(
279 `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vL_n y1 y2 y3 y4 y5 y6 lmfun =
280 gamma3f_vL_n0 y1 y2 y3 y4 y5 y6`,
284 REWRITE_TAC[gamma3f_vL_n;Sphere.vol2f;gamma3f_vL_n0];
285 ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
289 let gamma3f_vL_nlfun_case = prove_by_refinement(
290 `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vL_n y1 y2 y3 y4 y5 y6 lmfun =
291 gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6`,
295 REWRITE_TAC[gamma3f_vL_n;Sphere.vol2f;gamma3f_vL_nlfun];
296 ASM_SIMP_TAC[lmfun_lfun];
301 let rr f s = REWRITE_RULE[Sphere.y_of_x] (f s);;
303 let lmdih_n0 = rr prove_by_refinement(
304 `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y1 ) ==>(y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
307 REWRITE_TAC[Sphere.y_of_x;lmdih_x_n];
309 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
314 let lmdih2_n0 = rr prove_by_refinement(
315 `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y2 ) ==>(y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
318 REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih2_x_n;Sphere.lmdih2_x_div_sqrtdelta_posbranch;Sphere.rotate2];
320 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
324 let lmdih3_n0 = rr prove_by_refinement(
325 `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y3 ) ==>(y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
328 REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih3_x_n;Sphere.lmdih3_x_div_sqrtdelta_posbranch;Sphere.rotate3];
330 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
334 let lmdih5_n0 = rr prove_by_refinement(
335 `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y5 ) ==>(y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
338 REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih5_x_n;Sphere.lmdih5_x_div_sqrtdelta_posbranch;Sphere.rotate5];
340 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
344 let lmdih6_n0 = rr prove_by_refinement(
345 `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y6 ) ==>(y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
348 REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih6_x_n;Sphere.lmdih6_x_div_sqrtdelta_posbranch;Sphere.rotate6];
350 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
355 let lmdih_ldih_n = rr prove_by_refinement(
356 `!y1 y2 y3 y4 y5 y6. (&0 <= y1 /\ y1 <= &2 * h0) ==>(y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih_x_n y1 y2 y3 y4 y5 y6)`,
359 REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;ldih_x_n];
361 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
365 let lmdih2_ldih2_n = rr prove_by_refinement(
366 `!y1 y2 y3 y4 y5 y6. (&0 <= y2 /\ y2 <= &2 * h0) ==>(y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih2_x_n y1 y2 y3 y4 y5 y6)`,
369 REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih2_x_div_sqrtdelta_posbranch;Sphere.rotate2;Sphere.ldih2_x_div_sqrtdelta_posbranch;lmdih2_x_n;ldih2_x_n];
371 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
375 let lmdih3_ldih3_n = rr prove_by_refinement(
376 `!y1 y2 y3 y4 y5 y6. (&0 <= y3 /\ y3 <= &2 * h0) ==>(y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih3_x_n y1 y2 y3 y4 y5 y6)`,
379 REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih3_x_div_sqrtdelta_posbranch;Sphere.rotate3;Sphere.ldih3_x_div_sqrtdelta_posbranch;lmdih3_x_n;ldih3_x_n];
381 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
385 let lmdih5_ldih5_n = rr prove_by_refinement(
386 `!y1 y2 y3 y4 y5 y6. (&0 <= y5 /\ y5 <= &2 * h0) ==>(y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih5_x_n y1 y2 y3 y4 y5 y6)`,
389 REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih5_x_div_sqrtdelta_posbranch;Sphere.rotate5;Sphere.ldih5_x_div_sqrtdelta_posbranch;lmdih5_x_n;ldih5_x_n];
391 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
395 let lmdih6_ldih6_n = rr prove_by_refinement(
396 `!y1 y2 y3 y4 y5 y6. (&0 <= y6 /\ y6 <= &2 * h0) ==>(y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih6_x_n y1 y2 y3 y4 y5 y6)`,
399 REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih6_x_div_sqrtdelta_posbranch;Sphere.rotate6;Sphere.ldih6_x_div_sqrtdelta_posbranch;lmdih6_x_n;ldih6_x_n];
401 ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
410 let gamma23f' = prove_by_refinement(
411 `!y1 y2 y3 y4 y5 y6 w1 w2 f. gamma23f y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 f =
412 gamma3f_126 y1 y2 y3 y4 y5 y6 f / &w1 + gamma3f_135 y1 y2 y3 y4 y5 y6 f / &w2 +
413 gamma3f_vLR y1 y2 y3 y4 y5 y6 f `,
416 REWRITE_TAC[gamma23f;gamma3f_126;gamma3f_135;gamma3f_vLR];
420 let gamma23f_126_03' = prove_by_refinement(
421 `!y1 y2 y3 y4 y5 y6 w1 f. gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 sqrt2 f =
422 gamma3f_126 y1 y2 y3 y4 y5 y6 f / &w1 + gamma3f_vL y1 y2 y3 y4 y5 y6 f `,
425 REWRITE_TAC[gamma23f_126_03;gamma3f_126;gamma3f_vL];
429 let gamma23f_v' = prove_by_refinement(
430 `!y1 y2 y3 y4 y5 y6 w1 f. gamma23f_red_03 y1 y2 y3 y4 y5 y6 sqrt2 f =
431 gamma3f_v y1 y2 y3 y4 y5 y6 f `,
434 REWRITE_TAC[gamma23f_red_03;gamma3f_v];
439 let gamma3f_vLR0_case = prove_by_refinement(
440 `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vLR y1 y2 y3 y4 y5 y6 lmfun =
441 gamma3f_vLR0 y1 y2 y3 y4 y5 y6`,
445 REWRITE_TAC[gamma3f_vLR;Sphere.vol2f;gamma3f_vLR0];
446 ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
451 let gamma3f_vLR_lfun_case = prove_by_refinement(
452 `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vLR y1 y2 y3 y4 y5 y6 lmfun =
453 gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6`,
457 REWRITE_TAC[gamma3f_vLR;Sphere.vol2f;gamma3f_vLR_lfun];
458 ASM_SIMP_TAC[lmfun_lfun];
462 let gamma3f_vL0_case = prove_by_refinement(
463 `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vL y1 y2 y3 y4 y5 y6 lmfun =
464 gamma3f_vL0 y1 y2 y3 y4 y5 y6`,
468 REWRITE_TAC[gamma3f_vL;Sphere.vol2f;gamma3f_vL0];
469 ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
473 let gamma3f_vL_lfun_case = prove_by_refinement(
474 `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vL y1 y2 y3 y4 y5 y6 lmfun =
475 gamma3f_vL_lfun y1 y2 y3 y4 y5 y6`,
479 REWRITE_TAC[gamma3f_vL;Sphere.vol2f;gamma3f_vL_lfun];
480 ASM_SIMP_TAC[lmfun_lfun];
485 let gamma3f_v0_case = prove_by_refinement(
486 `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_v y1 y2 y3 y4 y5 y6 lmfun =
487 gamma3f_v0 y1 y2 y3 y4 y5 y6`,
491 REWRITE_TAC[gamma3f_v;Sphere.vol2f;gamma3f_v0];
492 ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
496 let gamma3f_v_lfun_case = prove_by_refinement(
497 `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_v y1 y2 y3 y4 y5 y6 lmfun =
498 gamma3f_v_lfun y1 y2 y3 y4 y5 y6`,
502 REWRITE_TAC[gamma3f_v;Sphere.vol2f;gamma3f_v_lfun];
503 ASM_SIMP_TAC[lmfun_lfun];
507 let gamma3f_126_expand = prove_by_refinement(
508 `!y1 y2 y3 y4 y5 y6. gamma3f_126 y1 y2 y3 y4 y5 y6 f =
509 vol3r y1 y2 y6 sqrt2 - ((&2 * mm1 / pi) *
510 (&2 * dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 + &2 * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
511 &2 * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6 + dih3_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
512 dih4_y y1 y2 sqrt2 sqrt2 sqrt2 y6 + dih5_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - &3 * pi) -
514 (f (y1 / &2) * dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
515 f (y2 / &2) * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
516 f (y6 / &2) * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6))`,
520 REWRITE_TAC[gamma3f_126;Sphere.gamma3f;];
521 MESON_TAC[vol3f_palt];
528 let gamma3f_135_expand = prove_by_refinement(
529 `!y1 y2 y3 y4 y5 y6. gamma3f_135 y1 y2 y3 y4 y5 y6 f =
530 vol3r y1 y3 y5 sqrt2 - ( (&2 * mm1 / pi) *
531 (&2 * dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2 + &2 * dih3_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
532 &2 * dih5_y y1 sqrt2 y3 sqrt2 y5 sqrt2 + dih2_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
533 dih4_y y1 sqrt2 y3 sqrt2 y5 sqrt2 + dih6_y y1 sqrt2 y3 sqrt2 y5 sqrt2 - &3 * pi) -
535 (f (y1 / &2) * dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
536 f (y3 / &2) * dih3_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
537 f (y5 / &2) * dih5_y y1 sqrt2 y3 sqrt2 y5 sqrt2))`,
541 REWRITE_TAC[gamma3f_135;Sphere.gamma3f;];
542 MESON_TAC[vol3f_135_palt];
547 let ldih_x_135_s2 = prove_by_refinement(
548 `!x1 x2 x3 x4 x5 x6. ldih_x_135_s2 x1 x2 x3 x4 x5 x6 =
549 lfun (sqrt x1 / #2.0) * dih_x_135_s2 x1 x2 x3 x4 x5 x6`,
552 REWRITE_TAC[ldih_x_135_s2';dih_x_135_s2];
560 let taum_template_B_x_alt = prove_by_refinement(
561 `!x1 x12 x15 x2 x3 x34 x4 x45 x5 x6.
562 taum_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 x6 =
563 taum_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15)
564 (edge_flat2_x x2 x1 x3 (&0) x12 x12) +
570 REWRITE_TAC[Sphere.taum_template_B_x];
577 let dih_template_B_x_alt = prove_by_refinement(
578 `!x6 x25 x34 x5 x4 x45 x15 x2 x1 x3 x12.
579 dih_template_B_x x15 x45 x34 x12 x25 x1 x2 x3 x4 x5 x6 =
580 dih_x x1 x2 x5 x25 x15 x12 -
581 dih_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15)
582 (edge_flat2_x x2 x1 x3 (&0) x12 x12)`,
585 REWRITE_TAC[Sphere.dih_template_B_x];
591 let delta_template_B_x_alt = prove_by_refinement(
592 `!x6 x25 x34 x5 x4 x45 x15 x2 x1 x3 x12.
593 delta_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 x6 =
594 delta_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15)
595 (edge_flat2_x x2 x1 x3 (&0) x12 x12)`,
598 REWRITE_TAC[Sphere.delta_template_B_x];
605 let tau_lowform_x_alt = prove_by_refinement(
607 tau_lowform_x x1 x2 x3 x4 x5 x6 =
608 rho (sqrt x1) * pi - (pi + sol0) +
609 sqp (delta_x x1 x2 x3 x4 x5 x6) * rhazim_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
610 sqn (delta_x x1 x2 x3 x4 x5 x6) * rhazim2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
611 sqn (delta_x x1 x2 x3 x4 x5 x6) * rhazim3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`,
614 REWRITE_TAC[tau_lowform_x];
622 let taum_3flat_x_alt = prove_by_refinement(
623 `!x1 x2 x3 x23 x13 x12.
624 taum_3flat_x x1 x2 x3 x23 x13 x12 =
626 ( edge_flat2_x x23 x2 x3 (&0) (&4) (&4) )
627 ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) )
628 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) +
629 flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`,
632 REWRITE_TAC[Sphere.taum_3flat_x];
639 let taum_2flat_x_alt = prove_by_refinement(
640 `!x1 x2 x3 x4 x13 x12.
641 taum_2flat_x x1 x2 x3 x4 x13 x12 =
643 ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) )
644 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) +
645 flat_term_x x12 + flat_term_x x13)`,
648 REWRITE_TAC[Sphere.taum_2flat_x];
655 let taum_1flat_x_alt = prove_by_refinement(
656 `!x1 x2 x3 x4 x5 x12.
657 taum_1flat_x x1 x2 x3 x4 x5 x12 =
658 (taum_x x1 x2 x3 x4 x5
659 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) +
663 REWRITE_TAC[Sphere.taum_1flat_x];
670 let euler_3flat_x_alt = prove_by_refinement(
671 `!x1 x2 x3 x23 x13 x12.
672 euler_3flat_x x1 x2 x3 x23 x13 x12 =
674 ( edge_flat2_x x23 x2 x3 (&0) (&4) (&4) )
675 ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) )
676 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) )`,
679 REWRITE_TAC[Sphere.euler_3flat_x];
686 let euler_2flat_x_alt = prove_by_refinement(
687 `!x1 x2 x3 x4 x13 x12.
688 euler_2flat_x x1 x2 x3 x4 x13 x12 =
689 (eulerA_x x1 x2 x3 x4
690 ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) )
691 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) )`,
694 REWRITE_TAC[Sphere.euler_2flat_x];
701 let euler_1flat_x_alt = prove_by_refinement(
702 `!x1 x2 x3 x4 x5 x12.
703 euler_1flat_x x1 x2 x3 x4 x5 x12 =
704 (eulerA_x x1 x2 x3 x4 x5
705 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) )`,
708 REWRITE_TAC[Sphere.euler_1flat_x];
714 let upper_dih_x_y = prove_by_refinement(
715 `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
716 (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
717 (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
718 (upper_dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
719 upper_dih_x x1 x2 x3 x4 x5 x6)`,
722 REWRITE_TAC[Sphere.upper_dih_y;Sphere.y_of_x;LET_DEF;LET_END_DEF];
723 ASM_MESON_TAC[sq_pow2];
728 (* function delta_top_x is deprecated:
729 let delta_top_x_alt = prove_by_refinement(
730 `!a. delta_y (sqrt x4) (sqrt x9) (sqrt x6) a (sqrt x5) (sqrt x8) =
731 delta_top_x (a:real) (x1:real) (x2:real) (x3:real) (x4:real)
732 (x5:real) (x6:real) (x7:real) (x8:real) (x9:real)
736 REWRITE_TAC[Sphere.delta_top_x];
742 let functional_euler_3flat_x = prove_by_refinement(
743 `let x4r = compose6 edge_flat2_x proj_x4 proj_x2 proj_x3 zero6 four6 four6 in
744 let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
745 let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
747 compose6 eulerA_x proj_x1 proj_x2 proj_x3 x4r x5r x6r)`,
750 BY(REWRITE_TAC[FUN_EQ_THM;Sphere.euler_3flat_x;compose6;four6;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF])
754 let functional_euler_2flat_x = prove_by_refinement(
756 let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
757 let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
759 compose6 eulerA_x proj_x1 proj_x2 proj_x3 proj_x4 x5r x6r)`,
762 BY(REWRITE_TAC[FUN_EQ_THM;Sphere.euler_2flat_x;compose6;four6;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF])
766 let functional_euler_1flat_x = prove_by_refinement(
768 let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
770 compose6 eulerA_x proj_x1 proj_x2 proj_x3 proj_x4 proj_x5 x6r)`,
773 BY(REWRITE_TAC[FUN_EQ_THM;Sphere.euler_1flat_x;compose6;four6;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF])
778 let functional_taum_3flat_x = prove_by_refinement(
779 `let x4r = compose6 edge_flat2_x proj_x4 proj_x2 proj_x3 zero6 four6 four6 in
780 let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
781 let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
783 compose6 taum_x proj_x1 proj_x2 proj_x3 x4r x5r x6r +
784 uni(flat_term_x,proj_x4) +
785 uni(flat_term_x,proj_x5) +
786 uni(flat_term_x,proj_x6))`,
789 (REWRITE_TAC[FUN_EQ_THM;Sphere.taum_3flat_x;compose6;four6;add6;uni;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]);
795 let functional_taum_2flat_x = prove_by_refinement(
797 let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
798 let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
800 compose6 taum_x proj_x1 proj_x2 proj_x3 proj_x4 x5r x6r +
801 uni(flat_term_x,proj_x5) +
802 uni(flat_term_x,proj_x6))`,
805 (REWRITE_TAC[FUN_EQ_THM;Sphere.taum_2flat_x;compose6;four6;add6;uni;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]);
811 let functional_taum_1flat_x = prove_by_refinement(
813 let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
815 compose6 taum_x proj_x1 proj_x2 proj_x3 proj_x4 proj_x5 x6r +
816 uni(flat_term_x,proj_x6))`,
819 (REWRITE_TAC[FUN_EQ_THM;Sphere.taum_1flat_x;compose6;four6;add6;uni;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]);
823 let functional_delta_x_126_s2 = prove_by_refinement(
826 &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
827 delta_x_126_s2 ( mk_126 delta_x)`,
830 REWRITE_TAC[domain6;Nonlinear_lemma.delta_x_126_s2;Sphere.delta_y;mk_126;compose6;proj_x1;proj_x2;proj_x6;two6;constant6;Nonlinear_lemma.sqrt2_sqrt2];
831 BY(ASM_SIMP_TAC[sqrt_sqrt])
836 let functional_delta_x_135_s2 = prove_by_refinement(
839 &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
840 delta_x_135_s2 ( mk_135 delta_x)`,
843 REWRITE_TAC[domain6;Nonlinear_lemma.delta_x_135_s2;Sphere.delta_y;mk_135;compose6;proj_x1;proj_x3;proj_x5;two6;constant6;Nonlinear_lemma.sqrt2_sqrt2];
844 BY(ASM_SIMP_TAC[sqrt_sqrt])
848 let functional_vol3_x_135_s2 = prove_by_refinement(
851 &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
852 vol3_x_135_s2 ( mk_135 vol_x)`,
855 REWRITE_TAC[domain6;Nonlinear_lemma.vol3_x_135_s2;mk_135;Sphere.vol3r;compose6;proj_x1;proj_x3;proj_x5;two6;constant6;Sphere.vol_y;Sphere.y_of_x;Nonlinear_lemma.sqrt2_sqrt2];
856 ASM_SIMP_TAC[sqrt_sqrt];
857 REPEAT WEAK_STRIP_TAC;
858 REWRITE_TAC[Sphere.vol_x;Sphere.delta_x];
859 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
866 let functional_dih_x_126_s2 = prove_by_refinement(
869 &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
870 dih_x_126_s2 (mk_126 dih_x)`,
873 REWRITE_TAC[domain6;Nonlinear_lemma.dih_x_126_s2;constant6;compose6;mk_126;two6;proj_x1;proj_x2;proj_x6;Sphere.dih_y;LET_DEF;LET_END_DEF;Nonlinear_lemma.sqrt2_sqrt2];
874 BY(ASM_SIMP_TAC[sqrt_sqrt])
878 let functional_dih2_x_126_s2 = prove_by_refinement(
881 &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
882 dih2_x_126_s2 ( mk_126 dih2_x)`,
885 REWRITE_TAC[domain6;Nonlinear_lemma.dih2_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2];
886 REPEAT WEAK_STRIP_TAC;
887 GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih2_x_y);
888 REPEAT (POP_ASSUM MP_TAC);
894 let functional_dih3_x_126_s2 = prove_by_refinement(
897 &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
898 dih3_x_126_s2 ( mk_126 dih3_x)`,
901 REWRITE_TAC[domain6;Nonlinear_lemma.dih3_x_126_s2; mk_126;compose6;proj_x1;proj_x2;two6;proj_x6; constant6;Sphere.sqrt2];
902 REPEAT WEAK_STRIP_TAC;
903 GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih3_x_y);
904 REPEAT (POP_ASSUM MP_TAC);
910 let functional_dih4_x_126_s2 = prove_by_refinement(
911 ` dih4_x_126_s2= ( mk_126 dih4_x)`,
914 REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih4_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;Sphere.dih4_x];
919 let functional_dih5_x_126_s2 = prove_by_refinement(
920 ` dih5_x_126_s2= ( mk_126 dih5_x)`,
923 REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih5_x_126_s2; mk_126;compose6;proj_x1;proj_x2; two6;proj_x6;constant6; Sphere.sqrt2;Sphere.dih5_x];
928 let functional_dih6_x_126_s2 = prove_by_refinement(
929 ` dih6_x_126_s2= ( mk_126 dih6_x)`,
932 REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih6_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;Sphere.dih6_x];
936 let functional_dih_x_135_s2 = prove_by_refinement(
939 &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
940 dih_x_135_s2 (mk_135 dih_x)`,
943 REWRITE_TAC[domain6;Nonlinear_lemma.dih_x_135_s2;constant6;compose6;mk_135;two6;proj_x1;proj_x3;proj_x5;Sphere.dih_y;LET_DEF;LET_END_DEF;Nonlinear_lemma.sqrt2_sqrt2];
944 BY(ASM_SIMP_TAC[sqrt_sqrt])
949 let functional_dih2_x_135_s2 = prove_by_refinement(
952 &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
953 dih2_x_135_s2 ( mk_135 dih2_x)`,
956 REWRITE_TAC[domain6;Nonlinear_lemma.dih2_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2];
957 REPEAT WEAK_STRIP_TAC;
958 GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih2_x_y);
959 REPEAT (POP_ASSUM MP_TAC);
965 let functional_dih3_x_135_s2 = prove_by_refinement(
968 &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
969 dih3_x_135_s2 ( mk_135 dih3_x)`,
972 REWRITE_TAC[domain6;Nonlinear_lemma.dih3_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2];
973 REPEAT WEAK_STRIP_TAC;
974 GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih3_x_y);
975 REPEAT (POP_ASSUM MP_TAC);
981 let functional_dih4_x_135_s2 = prove_by_refinement(
982 ` dih4_x_135_s2= ( mk_135 dih4_x)`,
985 REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih4_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2;Sphere.dih4_x];
990 let functional_dih5_x_135_s2 = prove_by_refinement(
991 ` dih5_x_135_s2= ( mk_135 dih5_x)`,
994 REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih5_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2;Sphere.dih5_x];
999 let functional_dih6_x_135_s2 = prove_by_refinement(
1000 ` dih6_x_135_s2= ( mk_135 dih6_x)`,
1003 REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih6_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2;Sphere.dih6_x];
1009 let functional_ldih_x_126_s2 = prove_by_refinement(
1010 ` ldih_x_126_s2= uni (lfun, (proj_y1 / two6)) * dih_x_126_s2`,
1013 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y1;arith `&2 = #2.0`])
1017 let functional_ldih2_x_126_s2 = prove_by_refinement(
1018 ` ldih2_x_126_s2= uni (lfun, (proj_y2 / two6)) * dih2_x_126_s2`,
1021 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih2_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y2;arith `&2 = #2.0`])
1026 let functional_ldih6_x_126_s2 = prove_by_refinement(
1027 ` ldih6_x_126_s2= uni (lfun, (proj_y6 / two6)) * dih6_x_126_s2`,
1030 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih6_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y6;arith `&2 = #2.0`])
1035 let functional_ldih_x_135_s2 = prove_by_refinement(
1036 ` ldih_x_135_s2= uni (lfun, (proj_y1 / two6)) * dih_x_135_s2`,
1039 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_135_s2;mk_135;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y1;arith `&2 = #2.0`])
1043 let functional_ldih3_x_135_s2 = prove_by_refinement(
1044 ` ldih3_x_135_s2= uni (lfun, (proj_y3 / two6)) * dih3_x_135_s2`,
1047 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih3_x_135_s2;mk_135;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y3;arith `&2 = #2.0`])
1052 let functional_ldih5_x_135_s2 = prove_by_refinement(
1053 ` ldih5_x_135_s2= uni (lfun, (proj_y5 / two6)) * dih5_x_135_s2`,
1056 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih5_x_135_s2;mk_135;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y5;arith `&2 = #2.0`])
1060 let functional_ldih_x_126_n = prove_by_refinement(
1061 `ldih_x_126_n = mk_126 ldih_x_n`,
1064 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_126_n;mk_126;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x2;proj_x6;compose6;two6;constant6])
1068 (* this differs from C++ code? *)
1070 let functional_ldih2_x_126_n = prove_by_refinement(
1071 `ldih2_x_126_n = mk_126 (rotate2 ldih_x_n)`,
1074 (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih2_x_126_n;functional_ldih_x_126_n;mk_126;Sphere.rotate2;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x2;proj_x6;compose6;two6;constant6]);
1075 REWRITE_TAC[Nonlinear_lemma.ldih2_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih2_x_div_sqrtdelta_posbranch;Sphere.rotate2];
1076 REPEAT WEAK_STRIP_TAC;
1077 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1078 REWRITE_TAC[Sphere.delta_x];
1084 let functional_ldih6_x_126_n = prove_by_refinement(
1085 `ldih6_x_126_n = mk_126 (rotate6 ldih_x_n)`,
1088 (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih6_x_126_n;functional_ldih_x_126_n;mk_126;Sphere.rotate6;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x2;proj_x6;compose6;two6;constant6]);
1089 REWRITE_TAC[Nonlinear_lemma.ldih6_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih6_x_div_sqrtdelta_posbranch;Sphere.rotate6];
1090 REPEAT WEAK_STRIP_TAC;
1091 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1092 REWRITE_TAC[Sphere.delta_x];
1097 let functional_ldih_x_135_n = prove_by_refinement(
1098 `ldih_x_135_n = mk_135 ldih_x_n`,
1101 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_135_n;mk_135;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x3;proj_x5;compose6;two6;constant6])
1106 let functional_ldih3_x_135_n = prove_by_refinement(
1107 `ldih3_x_135_n = mk_135 (rotate3 ldih_x_n)`,
1110 (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih3_x_135_n;functional_ldih_x_135_n;mk_135;Sphere.rotate2;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x3;proj_x5;compose6;two6;constant6]);
1111 REWRITE_TAC[Nonlinear_lemma.ldih3_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih3_x_div_sqrtdelta_posbranch;Sphere.rotate3];
1112 REPEAT WEAK_STRIP_TAC;
1113 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1114 REWRITE_TAC[Sphere.delta_x];
1119 let functional_ldih5_x_135_n = prove_by_refinement(
1120 `ldih5_x_135_n = mk_135 (rotate5 ldih_x_n)`,
1123 (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih5_x_135_n;functional_ldih_x_135_n;mk_135;Sphere.rotate5;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x3;proj_x5;compose6;two6;constant6]);
1124 REWRITE_TAC[Nonlinear_lemma.ldih5_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih5_x_div_sqrtdelta_posbranch;Sphere.rotate5];
1125 REPEAT WEAK_STRIP_TAC;
1126 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1127 REWRITE_TAC[Sphere.delta_x];
1132 let functional_taum_x1 = prove_by_refinement(
1135 (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
1137 (compose6 taum_x four6 four6 four6
1138 (constant6 (a*a)) (constant6 (b*b)) proj_x1)`,
1141 REWRITE_TAC[domain6;compose6;four6;constant6;Sphere.taum_x1; Sphere.taum_y1;Sphere.taum_x;Nonlinear_lemma.taum_123;proj_x1; Sphere.rhazim_x;Sphere.rhazim2_x; Collect_geom2.SQRT4_EQ2; Sphere.rhazim3_x];
1142 BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
1146 let functional_taum_x2 = prove_by_refinement(
1149 (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
1151 (compose6 taum_x four6 four6 four6
1152 (constant6 (a*a)) (constant6 (b*b)) proj_x2)`,
1155 REWRITE_TAC[domain6;compose6;four6;constant6;Sphere.taum_x2; Sphere.taum_y2;Sphere.taum_x;Nonlinear_lemma.taum_123;proj_x2; Sphere.rhazim_x;Sphere.rhazim2_x; Collect_geom2.SQRT4_EQ2; Sphere.rhazim3_x];
1156 BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
1161 let functional_taum_x1_x2 = prove_by_refinement(
1164 (\x1 x2 x3 x4 x5 x6. &0 <= a)
1166 (compose6 taum_x four6 four6 four6
1167 (constant6 (a*a)) proj_x1 proj_x2)`,
1170 REWRITE_TAC[domain6;compose6;four6;constant6;Sphere.taum_x1_x2; Sphere.taum_y1_y2;Sphere.taum_x;Nonlinear_lemma.taum_123;proj_x2; proj_x1;Sphere.rhazim_x;Sphere.rhazim2_x; Collect_geom2.SQRT4_EQ2; Sphere.rhazim3_x];
1171 BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
1175 let functional_delta_sub1_x = prove_by_refinement(
1176 `!a. delta_sub1_x a = compose6 delta_x
1177 (constant6 a) proj_x2 proj_x3 proj_x4 proj_x5 proj_x6`,
1180 (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_sub1_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1184 let functional_taum_sub1_x = prove_by_refinement(
1185 `!a. taum_sub1_x a = compose6 taum_x
1186 (constant6 a) proj_x2 proj_x3 proj_x4 proj_x5 proj_x6`,
1189 (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub1_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1195 let functional_taum_sub246_x = prove_by_refinement(
1196 `!a b c. taum_sub246_x a b c = compose6 taum_x
1197 proj_x1 (constant6 a) proj_x3 (constant6 b) proj_x5 (constant6 c)`,
1200 (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub246_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1204 let functional_taum_sub345_x = prove_by_refinement(
1205 `!a b c. taum_sub345_x a b c = compose6 taum_x
1206 proj_x1 proj_x2 (constant6 a) (constant6 b) (constant6 c) proj_x6`,
1209 (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub345_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1215 let functional1_vol2r_x =
1216 new_definition `vol2r_x x = &2 * pi * (&2 - (x / &4)) / &3`;;
1218 let functional_vol2r_x1 =
1219 new_definition `vol2r_x1 = promote1_to_6 vol2r_x`;;
1223 let functional1_vol2_x =
1224 new_definition `vol2_x x = &2 * pi * (&2 - (sqrt x) / &4) / &3`;;
1226 let functional_vol2_x1 =
1227 new_definition `vol2_x1 = promote1_to_6 vol2_x`;;
1230 let functional_gamma3f_x_v_lfun = prove_by_refinement(
1232 let vv_term_m1 = scalar6 (unit6 - scalar6 proj_y1 (&1 / sqrt8)) (&4 * mm1) in
1234 (scalar6 (uni(flat_term_x,proj_x1)) (-- &16 * mm2 /sol0)) in
1236 (\x1 x2 x3 x4 x5 x6.
1237 &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
1238 gamma3f_x_v_lfun ((dih_x - constant6 (&2 * #0.03)) *
1239 ((vol2r_x1 - vv_term_m1 ) + vv_term_m2))`,
1242 rt[domain6;LET_DEF;LET_END_DEF;Nonlinear_lemma.gamma3f_x_v_lfun;mul6;sub6;Nonlinear_lemma.gamma3f_v_lfun;constant6;Sphere.vol2r;functional_vol2_x1;functional1_vol2_x;promote1_to_6;mul6;add6;scalar6;uni;proj_x1;Sphere.dih_y;Nonlinear_lemma.sqrt2_sqrt2;proj_y1;functional_vol2r_x1;functional1_vol2r_x;Sphere.lfun;unit6;Sphere.flat_term_x;Sphere.flat_term;Nonlinear_lemma.sqrt8_sqrt2];
1246 sgthen `(sqrt x1 / &2) pow 2 = x1 / &4` SUBST1_TAC
1247 rt[arith `(sqrt x1 / &2) pow 2 = (sqrt x1 * sqrt x1) / &4`]
1249 ABBREV_TAC `a = &2 * pi * (&2 - x1/ &4) / &3`
1250 rt[arith `((a:real) - b + c = a - (b - c))`]
1258 let taud_D2_num_x_y = prove_by_refinement(
1259 `!y1 y2 y3 y4 y5 y6.
1260 &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==>
1261 taud_v4_D2_num y1 y2 y3 y4 y5 y6 = y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6`,
1264 REWRITE_TAC[Nonlin_def.taud_v4_D2_num;Nonlin_def.taud_D2_num_x];
1266 REWRITE_TAC[GSYM mu_y];
1267 REWRITE_TAC[GSYM Sphere.delta_y];
1268 ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx];
1274 (* arclength_x_345 deprecated *)
1276 (* this could be rewriten further with eulerA_x *)
1279 let functional_sol_euler_x_divsqrtdelta = prove_by_refinement(
1280 `let a = uni(sqrt,proj_x1 * proj_x2 * proj_x3) +
1281 proj_y1 * (proj_x2 + proj_x3 - proj_x4) * constant6 (#0.5) +
1282 proj_y2 * (proj_x1 + proj_x3 - proj_x5) * constant6 (#0.5) +
1283 proj_y3 * (proj_x1 + proj_x2 - proj_x6) * constant6 (#0.5) in
1284 (sol_euler_x_div_sqrtdelta =
1285 (uni(matan,(delta_x / (a * a * constant6 (&4))))) / a)`,
1289 FIRST_X_ASSUM MP_TAC;
1290 REWRITE_TAC[FUN_EQ_THM];
1291 REWRITE_TAC[uni;Sphere.sol_euler_x_div_sqrtdelta; div6;mul6;add6;sub6;constant6;proj_y1;proj_y2; proj_y3;proj_x1;proj_x2;proj_x3; proj_x4;proj_x5;proj_x6];
1292 REWRITE_TAC[REAL_ARITH `x * #0.5 = x/ &2`;REAL_ARITH `&4 * a pow 2 = a* a * &4`];
1294 FIRST_X_ASSUM (ASSUME_TAC o (ISPECL [`x:real`;`x':real`; `x'':real`;`x''':real`;`x'''':real`; `x''''':real`]));
1296 REWRITE_TAC[LET_DEF;LET_END_DEF];
1302 let functional_vol3f_x_sqrt2_lmplus = prove_by_refinement(
1304 (\x1 x2 x3 x4 x5 x6.
1305 (&2 * h0) pow 2 <= x1 /\ &0 <= x2 /\ &0 <=x6)
1306 vol3f_x_sqrt2_lmplus
1307 (constant6 ( &2 * mm1 / pi ) *
1308 (two6 * compose6 dih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1309 two6 * compose6 dih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1310 two6 * compose6 dih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1311 compose6 dih3_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1312 compose6 dih4_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1313 compose6 dih5_x proj_x1 proj_x2 two6 two6 two6 proj_x6 -
1314 constant6 ( &3 * pi))
1315 - (constant6 (&8 * mm2 / pi)) *
1316 (compose6 ldih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1317 compose6 ldih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6)))`,
1320 REWRITE_TAC[LET_DEF;LET_END_DEF;domain6; two6;constant6;mul6;add6;sub6;proj_x1;compose6;proj_x2; proj_x3;proj_x4;proj_x5;proj_x6];
1321 BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_sqrt2_lmplus_alt])
1329 let functional_vol3f_x_lfun = prove_by_refinement(
1331 (\x1 x2 x3 x4 x5 x6.
1332 &0 <= x1 /\ &0 <= x2 /\ &0 <=x6)
1334 (constant6 ( &2 * mm1 / pi ) *
1335 (two6 * compose6 dih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1336 two6 * compose6 dih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1337 two6 * compose6 dih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1338 compose6 dih3_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1339 compose6 dih4_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1340 compose6 dih5_x proj_x1 proj_x2 two6 two6 two6 proj_x6 -
1341 constant6 ( &3 * pi))
1342 - (constant6 (&8 * mm2 / pi)) *
1343 (compose6 ldih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1344 compose6 ldih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1345 compose6 ldih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6)))
1349 REWRITE_TAC[LET_DEF;LET_END_DEF; two6; domain6;constant6;mul6;add6;sub6;proj_x1; compose6;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6];
1350 BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_lfun_alt])
1357 let functional_ldih_x = prove_by_refinement(
1359 (unit6 * constant6 h0 + proj_y1 * constant6 ( -- #0.5))*
1360 (unit6 / (constant6 h0 - unit6)) * dih_x`,
1363 REWRITE_TAC[FUN_EQ_THM];
1364 REWRITE_TAC[add6;mul6;div6;sub6;constant6];
1365 REWRITE_TAC[proj_y1;Sphere.ldih_x;Nonlinear_lemma.unit6;Sphere.lfun];
1373 let functional_lfun_y1 = prove_by_refinement(
1374 `lfun_y1 = (unit6 * constant6 h0 + proj_x1 * constant6 (-- &1))*
1375 (unit6 / (constant6 h0 - unit6))`,
1378 REWRITE_TAC[FUN_EQ_THM];
1379 REWRITE_TAC[add6;mul6;div6;sub6;constant6];
1380 REWRITE_TAC[Sphere.lfun_y1;Sphere.lfun; Nonlinear_lemma.unit6;Nonlinear_lemma.proj_x1];
1387 let functional_vol_x = prove_by_refinement(
1388 `vol_x = uni(sqrt,delta_x) / constant6 (&12)`,
1391 BY(REWRITE_TAC[FUN_EQ_THM;uni;Sphere.vol_x;constant6;div6]);
1396 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
1398 let functional_ldih_x_n = prove_by_refinement(
1399 `ldih_x_n = uni(sqn,delta_x) * ldih_x_div_sqrtdelta_posbranch`,
1402 BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_n;mul6;uni])