1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Main Estimate - Appendix - Terminal Cases *)
4 (* Chapter: Local Fan *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
9 (* Terminal Pent and Hex cases. *)
11 (* pent with 5 top edges=2 *)
16 module Pent_hex = struct
21 (* eventually combine this with the one in Appendix. *)
24 let pent_hex_get_main_nonlinear =
25 let is_main = function
26 | Main_estimate -> true
29 exists (is_main) ind.tags in
31 filter has_main (!Ineq.ineqs) in
32 let id = map (fun t-> t.idv) main_ineq_data1 in
33 let main_ineq_data = map (fun t -> hd(Ineq.getexact t)) id in
34 let ineql = map (fun ind -> ind.ineq) main_ineq_data in
35 let sl = map (fun ind -> ind.idv) main_ineq_data in
36 let main_ineq_conj = end_itlist (curry mk_conj) ineql in
37 let th = new_definition (mk_eq (`main_nonlinear_terminal_v11:bool`,main_ineq_conj)) in
38 let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in
39 let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in
40 let tryindex s sl = try index s sl with _ -> report s; failwith s in
42 let i = tryindex s sl in
43 let th2 = funpow i CONJUNCT2 th1 in
48 let UNDISCH2 = repeat UNDISCH;;
50 let yys = [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`];;
53 let sqrt_secant_approx = prove_by_refinement(
54 `!x1 x2 x. &0 <= x1 /\ x1 <= x /\ x <= x2 ==>
55 (&1 / (sqrt(x1) + sqrt(x2))) * (x - x1) + sqrt(x1) <= sqrt(x)`,
58 REPEAT WEAKER_STRIP_TAC;
59 ASM_CASES_TAC `x2 = &0`;
60 TYPIFY `x1 = &0 /\ x = &0` (C SUBGOAL_THEN ASSUME_TAC);
61 BY(ASM_TAC THEN REAL_ARITH_TAC);
64 TYPIFY `&0 < sqrt x2` (C SUBGOAL_THEN ASSUME_TAC);
65 MATCH_MP_TAC SQRT_POS_LT;
66 BY(ASM_TAC THEN REAL_ARITH_TAC);
67 TYPIFY `&0 <= sqrt x1` (C SUBGOAL_THEN ASSUME_TAC);
68 MATCH_MP_TAC SQRT_POS_LE;
69 BY(ASM_TAC THEN REAL_ARITH_TAC);
70 TYPIFY `&1 / (sqrt x1 + sqrt x2) * (x - x1) = ((sqrt x + sqrt x1)/(sqrt x2 + sqrt x1)) * (sqrt x - sqrt x1)` (C SUBGOAL_THEN SUBST1_TAC);
71 Calc_derivative.CALC_ID_TAC;
73 REWRITE_TAC[REAL_DIFFSQ];
74 REPEAT (GMATCH_SIMP_TAC Functional_equation.sqrt_sqrt);
75 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
76 BY(ASM_TAC THEN REAL_ARITH_TAC);
77 REWRITE_TAC[arith `x + y <= z <=> x <= &1 * (z - y)`];
78 MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL;
80 REWRITE_TAC[arith `&0 <= x - y <=> y <= x`];
81 GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
82 BY(ASM_TAC THEN REAL_ARITH_TAC);
83 GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
85 REWRITE_TAC[arith `&1 * x = x`;arith `x + y <= z + y <=> x <= z`];
86 GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
87 BY(ASM_TAC THEN REAL_ARITH_TAC);
88 BY(ASM_TAC THEN REAL_ARITH_TAC)
92 let flat_term_neg = prove_by_refinement(
93 `!y. y <= &2 * h0 ==> flat_term y <= &0`,
96 REWRITE_TAC[Sphere.flat_term];
97 REPEAT WEAKER_STRIP_TAC;
98 REWRITE_TAC[arith `a * b / c <= &0 <=> &0 <= a * (--b) / c `];
99 GMATCH_SIMP_TAC REAL_LE_MUL;
100 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
101 FIRST_X_ASSUM MP_TAC;
102 REWRITE_TAC[Sphere.h0];
103 MP_TAC Flyspeck_constants.bounds;
108 let mu_y_ft_combine = prove_by_refinement(
110 mu_y y y2 y3 * sd + flat_term y =
111 mu_y (&2 * h0) y2 y3 * sd + (&1 - (&2 * h0 - &2) * #0.07 * sd / sol0) * flat_term y`,
114 REWRITE_TAC[Nonlin_def.mu_y;Sphere.flat_term];
115 REPEAT WEAKER_STRIP_TAC;
116 Calc_derivative.CALC_ID_TAC;
117 MP_TAC Flyspeck_constants.bounds;
118 REWRITE_TAC[Sphere.h0];
123 let mu_y_ft_combine2 = prove_by_refinement(
124 `!y y2 y3. y <= &2 * h0 ==>
125 mu_y (&2 * h0) y2 y3 * sqrt(&20) + #0.705 * flat_term y <=
126 mu_y y y2 y3 * sqrt(&20) + flat_term y
130 REWRITE_TAC[mu_y_ft_combine];
131 REWRITE_TAC[arith `x + y <= x + z <=> y <= z`];
132 REPEAT WEAKER_STRIP_TAC;
133 ONCE_REWRITE_TAC[arith `a * b = (-- a) * (-- b)`];
134 MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL;
136 REWRITE_TAC[arith `&0 <= -- f <=> f <= &0`];
137 BY(ASM_SIMP_TAC[flat_term_neg]);
138 REWRITE_TAC[arith `-- x <= -- (&1 - u) <=> &1 - x <= u`];
139 TYPIFY `#4.472135 <= sqrt(&20)` (C SUBGOAL_THEN MP_TAC);
140 MATCH_MP_TAC REAL_LE_RSQRT;
142 TYPIFY `#0.551285 < sol0 /\ sol0 < #0.551286` (C SUBGOAL_THEN MP_TAC);
143 BY(REWRITE_TAC[ Flyspeck_constants.bounds]);
144 REWRITE_TAC[Sphere.h0];
145 REWRITE_TAC[arith `a * b * c /d = ((a * b) * c) / d`];
146 REPEAT WEAKER_STRIP_TAC;
147 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
149 BY(ASM_TAC THEN REAL_ARITH_TAC);
150 BY(ASM_TAC THEN REAL_ARITH_TAC)
154 let nonfunctional_mu6_x = prove_by_refinement(
155 `!x1 x2 x3 a b c. mu6_x x1 x2 x3 a b c = mu_y (sqrt x1) (sqrt x2) (sqrt x3)`,
158 REWRITE_TAC[Nonlin_def.mu6_x;Nonlin_def.mu_y;];
159 BY(Functional_equation.F_REWRITE_TAC)
163 let tau_x_tau_residual_x_general = prove_by_refinement(
166 sqrt(x1) <= &2 * h0 /\
167 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
168 delta_x4 x1 x2 x3 x4 x5 x6 < &0 /\
169 &0 < delta_x4 x2 x3 x1 x5 x6 x4 /\
170 &0 < delta_x4 x3 x1 x2 x6 x4 x5 /\
171 &0 <= delta_x x1 x2 x3 x4 x5 x6 ==>
172 taum_x x1 x2 x3 x4 x5 x6 = sqrt(delta_x x1 x2 x3 x4 x5 x6) *
173 tau_residual_x x1 x2 x3 x4 x5 x6 + flat_term_x x1`,
176 REPEAT WEAK_STRIP_TAC;
177 FIRST_X_ASSUM MP_TAC;
178 REWRITE_TAC[arith `&0 <= x <=> (&0 = x \/ &0 < x)`];
179 DISCH_THEN DISJ_CASES_TAC;
180 REWRITE_TAC[Sphere.taum_x;Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x;Sphere.rhazim;Sphere.rhazim2;Sphere.rhazim3;Sphere.node2_y;Sphere.node3_y;Sphere.dih_y;LET_DEF;LET_END_DEF;Sphere.dih_x];
181 ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`];
182 SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = &0` SUBST1_TAC;
183 BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
184 SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = &0` SUBST1_TAC;
185 BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
186 FIRST_X_ASSUM (fun t -> SUBST1_TAC (GSYM t));
187 REWRITE_TAC[arith `x * &0 = &0`;arith `&0 * x = &0`;SQRT_0];
188 ASM_SIMP_TAC[Merge_ineq.atn2_0;arith `(-- y < &0 <=> &0 < y) /\ ( &0 < -- y <=> y < &0)`];
189 REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;arith `pi/ &2 + pi/ &2 = pi /\ x + -- x = &0 /\ x * &0 = &0`];
190 REWRITE_TAC[Sphere.flat_term_x;Sphere.flat_term;Nonlinear_lemma.sol0_const1;Sphere.h0];
192 REWRITE_TAC[Sphere.taum_x;Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x;Sphere.rhazim;Sphere.rhazim2;Sphere.rhazim3;Sphere.node2_y;Sphere.node3_y;Sphere.dih_y;LET_DEF;LET_END_DEF];
193 ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`];
194 REWRITE_TAC[Nonlin_def.tau_residual_x];
195 REWRITE_TAC[Nonlin_def.tau_residual_x;Nonlin_def.rhazim_x_div_sqrtdelta_posbranch;Nonlin_def.rhazim2_x_div_sqrtdelta_posbranch;Nonlin_def.rhazim3_x_div_sqrtdelta_posbranch;Sphere.rotate2;Sphere.rotate3];
197 REWRITE_TAC[arith `a + b + c - d = (a - d) + b + c`];
198 REWRITE_TAC[arith `a * (b + c) = a * b + a * c`];
199 ONCE_REWRITE_TAC[arith `(a + b + c) +d = (a + d) + b + c`];
201 ASM_SIMP_TAC[Merge_ineq.dih_x_dih_x_div_sqrtdelta_negbranch];
202 REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;Sphere.flat_term;Sphere.flat_term_x;Nonlinear_lemma.sol0_const1;];
205 ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`];
207 GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch;
209 SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
210 BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
211 BY(ASM_REWRITE_TAC[]);
212 ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`];
214 GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch;
216 SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
217 BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
218 BY(ASM_REWRITE_TAC[])
222 let OWZLKVY4 = prove_by_refinement(
223 ` main_nonlinear_terminal_v11 ==> ( !y1 y2 y3 y4 y5 y6.
224 &2 <= y1 /\ y1 <= &2 * h0 /\
225 &2 <= y2 /\ y2 <= &2 * h0 /\
226 &2 <= y3 /\ y3 <= &2 * h0 /\
227 cstab <= y4 /\ y4 <= #3.915 /\
230 &0 <= delta_y y1 y2 y3 y4 y5 y6 ==>
231 taud y1 y2 y3 y4 y5 y6 <= taum y1 y2 y3 y4 y5 y6)`,
234 REPEAT WEAKER_STRIP_TAC;
235 ASM_CASES_TAC `&80 <= delta_y y1 y2 y3 y4 y5 y6`;
236 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2314572187") yys;
237 REWRITE_TAC[Sphere.ineq;TAUT `(a ==> b==> c) <=> (a /\ b) ==> c `;TAUT `(a /\ b) /\ c <=> a /\ b /\ c`];
239 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
240 ASM_SIMP_TAC[arith `n <= d ==> ~(d < n)`;arith `x > y <=> y < x`];
241 MATCH_MP_TAC (arith `u = v ==> (u < t ==> v <= t)`);
242 MATCH_MP_TAC Functional_equation.taud_x_taud;
243 BY(ASM_TAC THEN REAL_ARITH_TAC);
244 RULE_ASSUM_TAC (REWRITE_RULE[arith `~(n <= d) <=> d < n`]);
245 GMATCH_SIMP_TAC Terminal.taum_taum_x;
247 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab] THEN REAL_ARITH_TAC);
248 REWRITE_TAC[Sphere.y_of_x];
249 GMATCH_SIMP_TAC tau_x_tau_residual_x_general;
250 TYPIFY `&0 <= delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)` (C SUBGOAL_THEN ASSUME_TAC);
251 FIRST_X_ASSUM_ST `&0 <= d` MP_TAC;
252 BY(REWRITE_TAC[Sphere.delta_y] THEN REAL_ARITH_TAC);
253 COMMENT "residue hypotheses";
256 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
257 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
258 REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
259 INTRO_TAC (UNDISCH Terminal.EAR_DELTA_X4) yys;
261 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
263 DISCH_THEN (unlist REWRITE_TAC);
264 REWRITE_TAC[arith `&4 = &2 * &2`];
265 REWRITE_TAC[ REAL_OF_NUM_LT];
266 GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
267 REWRITE_TAC[arith `0 < 2`];
268 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.delta_y;Sphere.h0;Appendix.cstab] THEN REAL_ARITH_TAC);
269 REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term_x;Sphere.flat_term];
270 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
272 BY(ASM_TAC THEN REAL_ARITH_TAC);
273 REWRITE_TAC[arith `v + u <= w + v <=> u <= w`];
274 REWRITE_TAC[GSYM Sphere.delta_y];
275 GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
277 GMATCH_SIMP_TAC SQRT_POS_LE;
278 BY(ASM_REWRITE_TAC[Sphere.delta_y]);
279 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7796879304") yys;
280 REWRITE_TAC[Sphere.ineq;Sphere.y_of_x];
281 REWRITE_TAC[TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
283 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
284 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
288 let OPEN_REAL_INTERVAL_SING = prove_by_refinement(
289 `!a b c. ~(real_interval(a,b) = {c})`,
292 REWRITE_TAC[EXTENSION;IN_SING;IN_REAL_INTERVAL];
293 REPEAT WEAKER_STRIP_TAC;
294 ASM_CASES_TAC `a < b`;
295 FIRST_ASSUM (C INTRO_TAC [`(a + b)/ &2`]);
296 FIRST_X_ASSUM (C INTRO_TAC [`(&3 * a + &1 * b)/ &4`]);
297 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
298 FIRST_X_ASSUM_ST `!` MP_TAC;
299 DISCH_THEN (C INTRO_TAC [`c:real`]);
300 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
307 let cv rw t = rhs(concl (REWRITE_CONV rw t)) in
308 let tm2 = cv rw tm in
309 ( (REWRITE_RULE (map GSYM rw) (Calc_derivative.differentiate tm2 x s)));;
312 let DERIVED_TAC ttac =
314 let (_,[b;f;f';y;s]) = strip_comb (goal_concl gl) in
315 ttac (Calc_derivative.differentiate f y s) gl;;
317 let derived_form_F = prove_by_refinement(
318 `!f f' x s. derived_form F f f' x s`,
321 REWRITE_TAC[Calc_derivative.derived_form]
325 let derived_form_delta_y = prove_by_refinement(
326 `!y1 y2 y3 y4 y5 y6. derived_form T (\q. delta_y q y2 y3 y4 y5 y6)
327 (y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1) y1 (:real) `,
330 REPEAT WEAKER_STRIP_TAC;
331 REWRITE_TAC[Sphere.delta_y;Sphere.delta_x];
333 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
334 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
335 REWRITE_TAC[Nonlin_def.delta_x1;Sphere.y_of_x];
340 let derived_form_delta_x = prove_by_refinement(
341 `!x1 x2 x3 x4 x5 x6 .derived_form T (\q. delta_x q x2 x3 x4 x5 x6)
342 (delta_x1 x1 x2 x3 x4 x5 x6)
347 REPEAT WEAKER_STRIP_TAC;
348 MP_TAC (diff `(\q. delta_x q x2 x3 x4 x5 x6)` [Sphere.delta_x] `x1:real` `(:real)`);
349 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
350 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
351 REWRITE_TAC[Nonlin_def.delta_x1];
356 let derived_form_delta_x1 = prove_by_refinement(
357 `!x1 x2 x3 x4 x5 x6. derived_form T (\q. delta_x1 q x2 x3 x4 x5 x6)
363 REPEAT WEAKER_STRIP_TAC;
364 MP_TAC (diff `(\q. delta_x1 q x2 x3 x4 x5 x6)` [Nonlin_def.delta_x1] `x1:real` `(:real)`);
365 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
366 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
367 REWRITE_TAC[Nonlin_def.delta_x1];
372 let deriv_form_taud = prove_by_refinement(
373 `!y1 y2 y3 y4 y5 y6. derived_form (&0 < delta_y y1 y2 y3 y4 y5 y6)
374 (\q. taud q y2 y3 y4 y5 y6)
375 ((-- #0.07 * delta_y y1 y2 y3 y4 y5 y6 + mu_y y1 y2 y3 * y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * y1 +
376 (sol0 / (&2 * h0 - &2)) * sqrt(delta_y y1 y2 y3 y4 y5 y6))/ sqrt(delta_y y1 y2 y3 y4 y5 y6))
381 REPEAT WEAKER_STRIP_TAC;
382 REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y];
383 DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]));
384 DISCH_THEN (C INTRO_TAC [`(y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1)`;`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]);
385 REWRITE_TAC[derived_form_delta_y];
386 TYPIFY `~(&2 * h0 - &2 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
387 BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
389 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
390 ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`;
392 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
393 Calc_derivative.CALC_ID_TAC;
395 REWRITE_TAC[arith `~(&2 = &0)`];
397 GMATCH_SIMP_TAC SQRT_EQ_0;
398 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
399 TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`;
400 TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`;
401 TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a*a` (C SUBGOAL_THEN SUBST1_TAC);
403 GMATCH_SIMP_TAC (GSYM SQRT_MUL);
404 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
405 BY(ASM_TAC THEN REAL_ARITH_TAC);
406 REWRITE_TAC[GSYM Nonlin_def.mu_y];
407 TYPED_ABBREV_TAC `c = mu_y y1 y2 y3`;
408 TYPED_ABBREV_TAC `d = (&2 * h0 - &2)`;
409 TYPED_ABBREV_TAC `e = #0.07`;
412 BY(REWRITE_TAC[Calc_derivative.derived_form])
416 (* renamed from deriv_form_taud_ALT *)
418 let derived_form_taud_ALT = prove_by_refinement(
419 `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 <= y1 /\ &0 <= y2 /\ &0 <= y3))
420 (\q. taud q y2 y3 y4 y5 y6)
421 (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 / sqrt(delta_y y1 y2 y3 y4 y5 y6))
426 REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
427 REPEAT WEAKER_STRIP_TAC;
428 ASM_CASES_TAC `&0 <= y1 /\ &0 <= y2 /\ &0 <= y3`;
430 ASM_SIMP_TAC[GSYM Functional_equation.mu6_x_mu_y];
431 INTRO_TAC deriv_form_taud yys;
432 ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`;
434 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
435 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
436 Calc_derivative.CALC_ID_TAC;
438 BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
440 REWRITE_TAC[GSYM Sphere.delta_y];
441 REWRITE_TAC[GSYM Sphere.y_of_x];
442 REWRITE_TAC[Sphere.h0];
443 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
446 BY(ASM_REWRITE_TAC[Calc_derivative.derived_form]);
447 BY(ASM_REWRITE_TAC[Calc_derivative.derived_form])
451 let deriv_form_taud_D2 = prove_by_refinement(
452 `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3))
453 (\q. (y_of_x taud_D1_num_x q y2 y3 y4 y5 y6 / sqrt(delta_y q y2 y3 y4 y5 y6)))
454 (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 / (sqrt(delta_y y1 y2 y3 y4 y5 y6) pow 3)) y1 (:real)`,
457 REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D2;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
458 REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
459 REPEAT WEAKER_STRIP_TAC;
460 TYPIFY `(~(sqrt (delta_y y1 y2 y3 y4 y5 y6) = &0))` ((C SUBGOAL_THEN ASSUME_TAC));
461 GMATCH_SIMP_TAC SQRT_EQ_0;
462 BY(ASM_TAC THEN REAL_ARITH_TAC);
463 MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
464 TYPIFY `(\q. (-- #0.07 * delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) + &1 / &2 * mu_y q y2 y3 * delta_x1 (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * q + sol0 / #0.52 * sqrt (delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6))) / sqrt (delta_y q y2 y3 y4 y5 y6))` EXISTS_TAC;
466 TYPIFY `{q | &0 < q}` EXISTS_TAC;
467 ASM_REWRITE_TAC[arith `!q. &0 < q <=> q > &0`;IN_ELIM_THM];
468 REWRITE_TAC[REAL_OPEN_HALFSPACE_GT];
469 REPEAT WEAKER_STRIP_TAC;
470 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
471 RULE_ASSUM_TAC(REWRITE_RULE[arith `y > &0 <=> &0 < y`]);
472 GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y);
473 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
474 BY(ASM_TAC THEN REAL_ARITH_TAC);
475 INTRO_TAC Calc_derivative.derived_form [`T`;`((\q. (-- #0.07 * delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) + &1 / &2 * mu_y q y2 y3 * delta_x1 (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * q + sol0 / #0.52 * sqrt (delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6))) / sqrt (delta_y q y2 y3 y4 y5 y6)))`;`((-- #0.07 * delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * delta_x1 (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * sqrt (y1 * y1) - &1 / &4 * mu6_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * (delta_x1 (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * sqrt (y1 * y1)) pow 2 + &1 / &2 * mu6_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * (-- &8 * (y1 * y1) * y4 * y4 + delta_x1 (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2)) / sqrt (delta_y y1 y2 y3 y4 y5 y6) pow 3)`;`y1:real`;`(:real)`];
476 REWRITE_TAC[WITHINREAL_UNIV];
477 DISCH_THEN ((unlist REWRITE_TAC) o GSYM);
478 DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]));
479 ASM_REWRITE_TAC[GSYM Sphere.delta_y];
480 DISCH_THEN (C INTRO_TAC [`y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1`;`-- &4 * (y4 pow 2) * y1`;`-- #0.07`;`y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1`;`y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1`;`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
481 REWRITE_TAC[derived_form_delta_y];
482 TYPIFY_GOAL_THEN `derived_form T (\q. mu_y q y2 y3) (-- #0.07) y1 (:real)` (unlist REWRITE_TAC);
483 REWRITE_TAC[Nonlin_def.mu_y];
485 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
486 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
489 TYPIFY_GOAL_THEN `derived_form T (\q. delta_x1 (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)) (-- &4 * (y4 pow 2) * y1) y1 (:real)` (unlist REWRITE_TAC);
490 REWRITE_TAC[Nonlin_def.delta_x1];
492 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
493 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
495 MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
496 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
497 REWRITE_TAC[GSYM Sphere.y_of_x];
498 TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`;
499 TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`;
500 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
501 ASM_SIMP_TAC[arith `&0 < y ==> &0 <= y`];
502 TYPIFY `y_of_x mu6_x y1 y2 y3 y4 y5 y6 = mu_y y1 y2 y3` (C SUBGOAL_THEN SUBST1_TAC);
503 REWRITE_TAC[Sphere.y_of_x];
504 GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y);
505 BY(ASM_TAC THEN REAL_ARITH_TAC);
506 TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a * a` (C SUBGOAL_THEN SUBST1_TAC);
508 GMATCH_SIMP_TAC (GSYM SQRT_MUL);
509 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
510 BY(ASM_TAC THEN REAL_ARITH_TAC);
511 Calc_derivative.CALC_ID_TAC;
512 TYPIFY_GOAL_THEN `~(a = &0)` (unlist REWRITE_TAC);
513 BY(ASM_REWRITE_TAC[]);
519 let th1 = (diff `((\q. (-- #0.07 *
520 delta_y q y2 y3 y4 y5 y6 *
521 (--(q * q) * y4 * y4 +
522 (y2 * y2) * y5 * y5 - (y3 * y3) * y5 * y5 - (y2 * y2) * y6 * y6 +
523 (y3 * y3) * y6 * y6 +
525 (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
530 #0.07 * ( #2.52 - sqrt (q * q)) +
531 #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) *
532 ((--(q * q) * y4 * y4 +
533 (y2 * y2) * y5 * y5 -
534 (y3 * y3) * y5 * y5 -
535 (y2 * y2) * y6 * y6 +
536 (y3 * y3) * y6 * y6 +
538 (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
544 #0.07 * ( #2.52 - sqrt (q * q)) +
545 #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) *
546 delta_y q y2 y3 y4 y5 y6 *
547 (-- &8 * (q * q) * y4 * y4 +
548 (--(q * q) * y4 * y4 +
549 (y2 * y2) * y5 * y5 -
550 (y3 * y3) * y5 * y5 -
551 (y2 * y2) * y6 * y6 +
552 (y3 * y3) * y6 * y6 +
554 (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
556 sqrt (delta_y q y2 y3 y4 y5 y6) pow 3)) ` [] `y1:real` `(:real)`) in
557 let fr = frees (concl(GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] th1)) in
558 let th2 = GENL fr th1 in
559 let ddelta_y = `(y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1)` in
560 let th3 = SPECL [ddelta_y;ddelta_y;ddelta_y] th2 in
561 let th4 = REWRITE_RULE[derived_form_delta_y] th3 in
562 let (h,[b;f;f';y;s]) = strip_comb (concl th4) in
563 let tm = list_mk_comb (h,[b;f;`f':real`;y;s]) in
564 GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] ( EXISTS (mk_exists (`f':real`,tm),f') th4);;
566 let derived_form_taud_D3 = prove_by_refinement(
567 `!y1 y2 y3 y4 y5 y6. ?f'. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3))
568 (\q. (y_of_x taud_D2_num_x q y2 y3 y4 y5 y6 / (sqrt(delta_y q y2 y3 y4 y5 y6) pow 3)))
572 REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D2;Nonlin_def.delta_x1;GSYM Sphere.delta_y;nonfunctional_mu6_x;Nonlin_def.mu_y;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
573 REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
574 REPEAT WEAKER_STRIP_TAC;
575 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
576 REPEAT WEAKER_STRIP_TAC;
578 REPEAT WEAKER_STRIP_TAC;
579 TYPIFY `f'` EXISTS_TAC;
580 FIRST_X_ASSUM MP_TAC;
581 REWRITE_TAC[Calc_derivative.derived_form];
583 TYPIFY_GOAL_THEN `&0 < y1 * y1` (unlist REWRITE_TAC);
584 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
585 BY(ASM_REWRITE_TAC[]);
587 GMATCH_SIMP_TAC SQRT_EQ_0;
588 BY(ASM_TAC THEN REAL_ARITH_TAC);
589 BY(REWRITE_TAC[WITHINREAL_UNIV])
593 let SECOND_DERIVATIVE_TEST = prove_by_refinement(
595 z IN s /\ real_open s /\
596 (!x. x IN s ==> (f has_real_derivative f' x) (atreal x)) /\
597 (!x. x IN s ==> (f' has_real_derivative f'' x) (atreal x)) /\
598 (f'' real_continuous atreal z) /\
599 (!x. x IN s ==> f z <= f x) ==>
600 (f' z = &0 /\ &0 <= f'' z)`,
603 REPEAT WEAKER_STRIP_TAC;
605 INTRO_TAC REAL_DERIVATIVE_ZERO_MAXMIN [`f`;`f' z`;`z`;`s`];
606 DISCH_THEN MATCH_MP_TAC;
608 FIRST_X_ASSUM MATCH_MP_TAC;
609 BY(ASM_REWRITE_TAC[]);
611 REWRITE_TAC[arith `&0 <= r <=> ~(r < &0)`];
613 RULE_ASSUM_TAC(REWRITE_RULE[real_continuous_atreal]);
614 FIRST_X_ASSUM_ST `abs` (C INTRO_TAC [`-- f'' z`]);
616 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
617 REPEAT WEAKER_STRIP_TAC;
618 TYPED_ABBREV_TAC `s' = s INTER {x | abs(x - z) < d}` ;
619 TYPIFY `z IN s'` (C SUBGOAL_THEN ASSUME_TAC);
621 BY(ASM_REWRITE_TAC[IN_INTER;IN_ELIM_THM;arith `z - z = &0`;REAL_ABS_0]);
622 TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC);
624 MATCH_MP_TAC REAL_OPEN_INTER;
626 REWRITE_TAC[real_open;IN_ELIM_THM];
627 REPEAT WEAKER_STRIP_TAC;
628 TYPIFY `d - abs (x - z)` EXISTS_TAC;
630 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
631 REPEAT WEAKER_STRIP_TAC;
632 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
633 COMMENT "restrict to an interval";
634 TYPIFY `?a b. real_interval (a,b) SUBSET s' /\ z IN real_interval(a,b)` (C SUBGOAL_THEN MP_TAC);
635 RULE_ASSUM_TAC(REWRITE_RULE[real_open]);
636 FIRST_X_ASSUM (C INTRO_TAC [`z`]);
638 REPEAT WEAKER_STRIP_TAC;
639 GEXISTL_TAC [`z - e`;`z + e`];
640 REWRITE_TAC[SUBSET;IN_REAL_INTERVAL];
641 REPEAT WEAKER_STRIP_TAC;
643 REPEAT WEAKER_STRIP_TAC;
644 FIRST_X_ASSUM MATCH_MP_TAC;
645 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
646 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
647 REPEAT WEAKER_STRIP_TAC;
648 INTRO_TAC REAL_OPEN_REAL_INTERVAL [`a`;`b`];
650 TYPIFY `!x. x IN s' ==> f'' x < &0` (C SUBGOAL_THEN ASSUME_TAC);
651 REPEAT WEAKER_STRIP_TAC;
652 FIRST_X_ASSUM (C INTRO_TAC [`x`]);
654 FIRST_X_ASSUM MP_TAC;
656 BY(REWRITE_TAC[IN_INTER;IN_ELIM_THM] THEN REAL_ARITH_TAC);
658 INTRO_TAC Counting_spheres.REAL_CONVEX_ON_SECOND_SECANT [`(\x. -- f x)`;`(\x. -- f' x)`;`(\x. -- f'' x)`;`real_interval (a,b)`];
660 REWRITE_TAC[IS_REALINTERVAL_INTERVAL;OPEN_REAL_INTERVAL_SING];
661 TYPIFY `!x. x IN real_interval(a,b) ==> x IN s` (C SUBGOAL_THEN ASSUME_TAC);
662 BY(ASM_TAC THEN SET_TAC[]);
664 REPEAT WEAKER_STRIP_TAC;
665 MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG;
666 GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN;
667 BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]);
669 REPEAT WEAKER_STRIP_TAC;
670 MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG;
671 GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN;
672 BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]);
673 REPEAT WEAKER_STRIP_TAC;
674 MATCH_MP_TAC (arith `f < &0 ==> &0 <= -- f`);
675 FIRST_X_ASSUM MATCH_MP_TAC;
676 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
678 TYPIFY `!x. x IN real_interval(a,b) ==> f x = f z` (C SUBGOAL_THEN ASSUME_TAC);
679 REPEAT WEAKER_STRIP_TAC;
680 FIRST_X_ASSUM (C INTRO_TAC [`x`;`z`]);
682 FIRST_X_ASSUM_ST `fz <= fx` (C INTRO_TAC [`x`]);
684 BY(ASM_TAC THEN SET_TAC[]);
686 TYPIFY `!x. x IN real_interval (a,b) ==> (f has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC);
687 REPEAT WEAKER_STRIP_TAC;
688 MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
689 TYPIFY `(\ (x:real). f z)` EXISTS_TAC;
692 BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]);
693 TYPIFY `real_interval(a,b)` EXISTS_TAC;
694 BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]);
695 COMMENT "show f' is zero";
696 TYPIFY `!x. x IN real_interval(a,b) ==> (f' x = &0)` (C SUBGOAL_THEN ASSUME_TAC);
697 REPEAT WEAKER_STRIP_TAC;
698 MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL;
699 GEXISTL_TAC [`f`;`x`];
701 FIRST_X_ASSUM MATCH_MP_TAC;
702 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
703 COMMENT "show f' has zero derivative";
704 TYPIFY `!x. x IN real_interval (a,b) ==> (f' has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC);
705 REPEAT WEAKER_STRIP_TAC;
706 MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
707 TYPIFY `(\ (x:real). &0)` EXISTS_TAC;
710 BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]);
711 TYPIFY `real_interval(a,b)` EXISTS_TAC;
712 BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]);
713 COMMENT "show f'' is zero";
714 TYPIFY `!x. x IN real_interval(a,b) ==> (f'' x = &0)` (C SUBGOAL_THEN ASSUME_TAC);
715 REPEAT WEAKER_STRIP_TAC;
716 MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL;
717 GEXISTL_TAC [`f'`;`x`];
719 FIRST_X_ASSUM MATCH_MP_TAC;
720 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
721 FIRST_X_ASSUM (C INTRO_TAC [`z`]);
723 REPLICATE_TAC 12 (FIRST_X_ASSUM kill);
724 FIRST_X_ASSUM_ST `f'' z < &0` MP_TAC;
729 (* END OF DERIVATIVES *)
734 let continuous_preimage_closed = prove_by_refinement(
735 `!f s t. real_closed s /\ real_closed t /\ f real_continuous_on s ==>
736 real_closed { x | x IN s /\ f x IN t }`,
739 REWRITE_TAC[real_continuous_on];
740 REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM];
741 REPEAT WEAKER_STRIP_TAC;
742 FIRST_X_ASSUM DISJ_CASES_TAC;
744 TYPIFY `~(x IN s)` ASM_CASES_TAC;
746 FIRST_X_ASSUM (C INTRO_TAC [`x`]);
747 RULE_ASSUM_TAC(REWRITE_RULE[TAUT `~ ~ x = x`]);
749 FIRST_X_ASSUM (C INTRO_TAC [`f x`]);
751 REPEAT WEAKER_STRIP_TAC;
752 FIRST_X_ASSUM (C INTRO_TAC [`e`]);
754 REPEAT WEAKER_STRIP_TAC;
755 TYPIFY `d` EXISTS_TAC;
757 REPEAT WEAKER_STRIP_TAC;
758 TYPIFY `(x' IN s)` ASM_CASES_TAC;
760 FIRST_X_ASSUM MATCH_MP_TAC;
761 FIRST_X_ASSUM MATCH_MP_TAC;
762 BY(ASM_REWRITE_TAC[]);
763 BY(ASM_REWRITE_TAC[])
767 let continuous_preimage_open = prove_by_refinement(
768 `!f s t. real_open s /\ real_open t /\ f real_continuous_on s ==>
769 real_open { x | x IN s /\ f x IN t }`,
772 REWRITE_TAC[real_continuous_on];
773 REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM];
774 REPEAT WEAKER_STRIP_TAC;
775 FIRST_X_ASSUM (C INTRO_TAC [`x`]);
777 FIRST_X_ASSUM (C INTRO_TAC [`f x`]);
779 REPEAT WEAKER_STRIP_TAC;
780 FIRST_X_ASSUM_ST `x IN s ==> p` (C INTRO_TAC [`x`]);
782 REPEAT WEAKER_STRIP_TAC;
783 FIRST_X_ASSUM_ST `?` (C INTRO_TAC [`e`]);
785 REPEAT WEAKER_STRIP_TAC;
786 TYPIFY `min d e'` EXISTS_TAC;
788 REWRITE_TAC[real_min];
789 BY(ASM_TAC THEN REAL_ARITH_TAC);
790 REPEAT WEAKER_STRIP_TAC;
792 FIRST_X_ASSUM MATCH_MP_TAC;
793 BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC);
795 FIRST_X_ASSUM MATCH_MP_TAC;
796 FIRST_X_ASSUM MATCH_MP_TAC;
798 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC)
802 let delta_y_continuous = prove_by_refinement(
803 `!y2 y3 y4 y5 y6. (\q. delta_y q y2 y3 y4 y5 y6) real_continuous_on (:real)`,
806 REPEAT WEAKER_STRIP_TAC;
807 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
808 REWRITE_TAC[REAL_OPEN_UNIV;IN_UNIV];
810 INTRO_TAC derived_form_delta_y [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
811 REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
812 DISCH_THEN (MP_TAC o (MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL));
817 let taud_continuous = prove_by_refinement(
818 `!y2 y3 y4 y5 y6. (\q. taud q y2 y3 y4 y5 y6) real_continuous_on {q | &0 <= delta_y q y2 y3 y4 y5 y6}`,
821 REPEAT WEAKER_STRIP_TAC;
822 REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;IN_ELIM_THM];
823 REPEAT WEAKER_STRIP_TAC;
824 REWRITE_TAC[Nonlin_def.taud];
825 REWRITE_TAC[arith `!q. a * (q - b)/ r = (a * inv r) * q + a * (-- b) * inv r`];
826 REWRITE_TAC[arith `!q. a + b * (c - q) + d = (-- b) * q + (a + b*c + d)`];
827 REPEAT (TRY CONJ_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;REAL_CONTINUOUS_WITHIN_ID] THEN ((GMATCH_SIMP_TAC REAL_CONTINUOUS_ADD) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_LMUL) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_MUL)));
829 REWRITE_TAC[MESON [o_THM;FUN_EQ_THM] `(\q. sqrt (delta_y q y2 y3 y4 y5 y6)) = sqrt o (\q. delta_y q y2 y3 y4 y5 y6)`];
830 MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE;
831 REWRITE_TAC[IMAGE;IN_ELIM_THM];
833 MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET;
834 TYPIFY `(:real)` EXISTS_TAC;
835 REWRITE_TAC[delta_y_continuous;SUBSET;IN_UNIV];
836 INTRO_TAC delta_y_continuous [`y2`;`y3`;`y4`;`y5`;`y6`];
837 REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN];
838 DISCH_THEN MATCH_MP_TAC;
839 BY(REWRITE_TAC[IN_UNIV]);
840 TYPED_ABBREV_TAC `u = delta_y x y2 y3 y4 y5 y6` ;
841 MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET;
842 TYPIFY `{u | &0 <= u}` EXISTS_TAC;
843 REWRITE_TAC[REAL_CONTINUOUS_WITHIN_SQRT_STRONG];
844 REWRITE_TAC[SUBSET;IN_ELIM_THM];
846 BY(REPEAT (TRY CONJ_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;REAL_CONTINUOUS_WITHIN_ID] THEN ((GMATCH_SIMP_TAC REAL_CONTINUOUS_ADD) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_LMUL) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_MUL))))
850 let taud_minimizer = prove_by_refinement(
851 `!a b d y2 y3 y4 y5 y6.
852 (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
853 (&0 <= d /\ ~(s = {}) ==>
854 (?z1. z1 IN s /\ (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6))))`,
857 REWRITE_TAC[LET_DEF;LET_END_DEF];
858 REPEAT WEAKER_STRIP_TAC;
859 MATCH_MP_TAC REAL_CONTINUOUS_ATTAINS_INF;
862 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET;
863 TYPIFY `{q | &0 <= delta_y q y2 y3 y4 y5 y6}` EXISTS_TAC;
864 REWRITE_TAC[taud_continuous];
865 REWRITE_TAC[SUBSET;IN_INTER;IN_ELIM_THM];
866 BY(ASM_TAC THEN REAL_ARITH_TAC);
867 REWRITE_TAC[REAL_COMPACT_EQ_BOUNDED_CLOSED];
869 MATCH_MP_TAC REAL_BOUNDED_SUBSET;
870 TYPIFY `real_interval[a,b]` EXISTS_TAC;
871 REWRITE_TAC[REAL_BOUNDED_REAL_INTERVAL];
873 MATCH_MP_TAC REAL_CLOSED_INTER;
874 REWRITE_TAC[REAL_CLOSED_REAL_INTERVAL];
875 TYPIFY_GOAL_THEN `!q. d <= delta_y q y2 y3 y4 y5 y6 <=> q IN (:real) /\ ((\q. delta_y q y2 y3 y4 y5 y6) q IN { t | d <= t})` (unlist REWRITE_TAC);
876 BY(REWRITE_TAC[IN_UNIV;IN_ELIM_THM]);
877 MATCH_MP_TAC continuous_preimage_closed;
878 REWRITE_TAC[delta_y_continuous];
879 REWRITE_TAC[REAL_CLOSED_UNIV];
880 BY(REWRITE_TAC[arith `d <= t <=> t >= d`;REAL_CLOSED_HALFSPACE_GE])
884 let taud_minimizer_cases = prove_by_refinement(
885 `!a b d z1 y2 y3 y4 y5 y6.
886 (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
887 (&0 <= d /\ &0 <= a /\ &0 <= y2 /\ &0 <= y3 /\ z1 IN s /\
888 (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6) ==>
889 ( z1 = a \/ z1 = b \/ d = delta_y z1 y2 y3 y4 y5 y6 \/
890 (y_of_x taud_D1_num_x z1 y2 y3 y4 y5 y6 = &0 /\
891 &0 <= y_of_x taud_D2_num_x z1 y2 y3 y4 y5 y6) )))`,
894 REWRITE_TAC[LET_DEF;LET_END_DEF];
895 REPEAT WEAKER_STRIP_TAC;
896 TYPIFY `z1 = a` ASM_CASES_TAC;
897 BY(ASM_REWRITE_TAC[]);
898 TYPIFY `z1 = b` ASM_CASES_TAC;
899 BY(ASM_REWRITE_TAC[]);
900 TYPIFY `d = delta_y z1 y2 y3 y4 y5 y6` ASM_CASES_TAC;
901 BY(ASM_REWRITE_TAC[]);
903 TYPIFY `a < z1 /\ z1 < b /\ d < delta_y z1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
904 RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL;IN_INTER;IN_ELIM_THM]);
905 BY(ASM_TAC THEN REAL_ARITH_TAC);
906 TYPED_ABBREV_TAC `s' = (real_interval (a,b) INTER {q | d < delta_y q y2 y3 y4 y5 y6})` ;
907 TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC);
908 TYPIFY_GOAL_THEN `s' = { q | q IN real_interval (a,b) /\ (delta_y q y2 y3 y4 y5 y6 IN { t | d < t}) }` (unlist ONCE_REWRITE_TAC);
910 BY(REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INTER]);
911 MATCH_MP_TAC continuous_preimage_open;
912 REWRITE_TAC[REAL_OPEN_REAL_INTERVAL];
914 BY(REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith `d < t <=> t > d`]);
915 MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET;
916 TYPIFY `(:real)` EXISTS_TAC;
917 REWRITE_TAC[delta_y_continuous];
919 INTRO_TAC SECOND_DERIVATIVE_TEST [`(\q. taud q y2 y3 y4 y5 y6)`;`(\q. y_of_x taud_D1_num_x q y2 y3 y4 y5 y6 / sqrt(delta_y q y2 y3 y4 y5 y6))`;`(\q. y_of_x taud_D2_num_x q y2 y3 y4 y5 y6 / (sqrt(delta_y q y2 y3 y4 y5 y6)) pow 3)`;`z1`;`s'`];
925 REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
926 BY(ASM_REWRITE_TAC[]);
929 REPEAT WEAKER_STRIP_TAC;
930 INTRO_TAC derived_form_taud_ALT [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
931 REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
934 FIRST_X_ASSUM MP_TAC;
936 REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
937 BY(ASM_TAC THEN REAL_ARITH_TAC);
940 REPEAT WEAKER_STRIP_TAC;
941 INTRO_TAC deriv_form_taud_D2 [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
942 REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
945 FIRST_X_ASSUM MP_TAC;
947 REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
948 BY(ASM_TAC THEN REAL_ARITH_TAC);
952 REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
953 REPEAT WEAKER_STRIP_TAC;
954 FIRST_X_ASSUM MATCH_MP_TAC;
955 REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
956 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
958 MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
959 INTRO_TAC derived_form_taud_D3 [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
960 REPEAT WEAKER_STRIP_TAC;
961 FIRST_X_ASSUM MP_TAC;
962 REWRITE_TAC[Calc_derivative.derived_form];
964 FIRST_X_ASSUM MP_TAC;
966 REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
967 BY(ASM_TAC THEN REAL_ARITH_TAC);
968 REWRITE_TAC[WITHINREAL_UNIV];
971 REPEAT WEAKER_STRIP_TAC;
972 TYPIFY `&0 < sqrt(delta_y z1 y2 y3 y4 y5 y6)` (C SUBGOAL_THEN ASSUME_TAC);
973 GMATCH_SIMP_TAC REAL_LT_RSQRT;
974 BY(ASM_TAC THEN REAL_ARITH_TAC);
976 FIRST_X_ASSUM_ST `taud_D1_num_x` MP_TAC;
977 REWRITE_TAC[REAL_DIV_EQ_0];
978 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
979 FIRST_X_ASSUM_ST `taud_D2_num_x` MP_TAC;
980 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
982 MATCH_MP_TAC REAL_POW_LT;
983 BY(ASM_REWRITE_TAC[]);
988 let taud_minimizer_terminal_pent_cases = prove_by_refinement(
989 ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6.
990 (let s = real_interval [&2,&2 * h0] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
991 (&0 <= d /\ y1 IN s /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\
992 #3.01 <= y4 /\ y4 <= #3.237 /\ y5 = &2 /\ y6 = &2 ==>
993 (?z1. z1 IN s /\ taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6 /\
994 ( z1 = &2 \/ z1 = &2 * h0 \/ d = delta_y z1 y2 y3 y4 y5 y6 \/
995 #0.12 <= taud z1 y2 y3 y4 y5 y6)))))`,
998 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
999 REPEAT WEAKER_STRIP_TAC;
1000 INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`d`;`y2`;`y3`;`y4`;`y5`;`y6`];
1001 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
1003 BY(ASM_MESON_TAC[]);
1004 REPEAT WEAKER_STRIP_TAC;
1005 TYPIFY `z1` EXISTS_TAC;
1007 BY(ASM_MESON_TAC[]);
1009 FIRST_X_ASSUM MATCH_MP_TAC;
1010 BY(ASM_MESON_TAC[]);
1011 INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`d`;`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1012 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
1014 BY(ASM_MESON_TAC[arith `&0 <= &2`;arith `&2 <= y ==> &0 <= y`]);
1015 ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC);
1016 ASM_CASES_TAC `z1 = &2 * h0` THEN FIRST_ASSUM (unlist REWRITE_TAC);
1017 ASM_CASES_TAC `d = delta_y z1 y2 y3 y4 y5 y6` THEN FIRST_ASSUM (unlist REWRITE_TAC);
1018 ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 y5 y6 < &20)`;
1019 REPEAT WEAKER_STRIP_TAC;
1020 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1347067436") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1021 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1023 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1024 GMATCH_SIMP_TAC (GSYM Functional_equation.taud_x_taud);
1026 BY(ASM_TAC THEN REAL_ARITH_TAC);
1027 BY(REPLICATE_TAC 3(FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1028 COMMENT "second get";
1030 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "6601228004") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1031 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1033 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1034 BY(ASM_TAC THEN REAL_ARITH_TAC)
1038 let taud_mud_126_x = prove_by_refinement(
1039 `!y3' y4' y5' y1 y2 y3 y4 y5 y6.
1040 &0 <= y1 /\ &0 <= y2 ==>
1041 y_of_x (mud_126_x_v1 y3 y4 y5) y1 y2 y3' y4' y5' y6 = taud y3 y1 y2 y6 y4 y5 - flat_term y3
1045 REWRITE_TAC[Nonlin_def.mud_126_x;Nonlin_def.taud;Sphere.flat_term;];
1046 Functional_equation.F_REWRITE_TAC;
1047 REWRITE_TAC[Sphere.delta_126_x;GSYM Sphere.delta_y];
1048 REPEAT WEAKER_STRIP_TAC;
1049 REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);
1051 TYPIFY `delta_y y3 y1 y2 y6 y4 y5 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1052 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1057 let taud_mud_135_x = prove_by_refinement(
1058 `!y2' y4' y6' y1 y2 y3 y4 y5 y6.
1059 &0 <= y1 /\ &0 <= y3 ==>
1060 y_of_x (mud_135_x_v1 y2 y4 y6) y1 y2' y3 y4' y5 y6' = taud y2 y1 y3 y5 y4 y6 - flat_term y2
1064 REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.taud;Sphere.flat_term;];
1065 Functional_equation.F_REWRITE_TAC;
1066 REWRITE_TAC[Sphere.delta_135_x;GSYM Sphere.delta_y];
1067 REPEAT WEAKER_STRIP_TAC;
1068 REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);
1070 TYPIFY `delta_y y2 y1 y3 y5 y4 y6 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1071 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1076 let mud_126_135 = prove_by_refinement(
1077 `!y1 y2 y3 y4 y5 y6 y3' y4' y5'. mud_126_x_v1 y3' y4' y5' y1 y2 y3 y4 y5 y6 =
1078 mud_135_x_v1 y3' y4' y5' y1 y3 y2 y4 y6 y5`,
1081 REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;];
1082 Functional_equation.F_REWRITE_TAC;
1083 REWRITE_TAC[Sphere.delta_135_x;Sphere.delta_126_x;GSYM Sphere.delta_y];
1084 BY(MESON_TAC[Merge_ineq.delta_x_sym]);
1088 let flat_term_2 = prove_by_refinement(
1089 `flat_term(&2) = -- sol0`,
1092 REWRITE_TAC[Sphere.flat_term];
1093 Calc_derivative.CALC_ID_TAC;
1094 BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1098 let flat_term_2h0 = prove_by_refinement(
1099 `flat_term(&2 * h0) = &0`,
1102 REWRITE_TAC[Sphere.flat_term];
1107 let flat_term_sol0 = prove_by_refinement(
1108 `!y. &2 <= y ==> --sol0 <= flat_term y`,
1111 REWRITE_TAC[Sphere.flat_term];
1112 REPEAT WEAKER_STRIP_TAC;
1113 TYPIFY `sol0 * (y - &2 * h0)/(&2 * h0 - &2) = -- sol0 + sol0 * (y - &2) / (&2 * h0 - &2)` (C SUBGOAL_THEN SUBST1_TAC);
1114 Calc_derivative.CALC_ID_TAC;
1115 BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1116 MATCH_MP_TAC (arith `&0 <= x ==> h <= h + x`);
1117 GMATCH_SIMP_TAC REAL_LE_MUL;
1118 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
1119 MP_TAC Flyspeck_constants.bounds;
1120 BY(REWRITE_TAC[Sphere.h0] THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
1124 let taud_2h0 = prove_by_refinement(
1126 &0 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 /\
1127 y2 <= &2 * h0 /\ y3 <= &2 * h0 ==>
1128 &0 <= taud (&2 * h0) y2 y3 y4 y5 y6`,
1131 REWRITE_TAC[Nonlin_def.taud;arith `x - x = &0 /\ &0 / x = &0 /\ x * &0 = &0 /\ &0 + x = x`];
1132 REPEAT WEAKER_STRIP_TAC;
1133 GMATCH_SIMP_TAC REAL_LE_MUL;
1135 GMATCH_SIMP_TAC SQRT_POS_LE;
1136 BY(ASM_REWRITE_TAC[]);
1137 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1141 let quadratic_root_minus_works = prove_by_refinement(
1143 ~(a = &0) /\ &0 <= b pow 2 - &4 * a * c
1144 ==> (let x = -- ( b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a) in
1145 a * x pow 2 + b * x + c = &0)`,
1148 REWRITE_TAC[LET_DEF;LET_END_DEF];
1149 REPEAT WEAKER_STRIP_TAC;
1150 Calc_derivative.CALC_ID_TAC;
1151 ASM_REWRITE_TAC[arith `~(&2 = &0)`];
1152 TYPED_ABBREV_TAC `d = b pow 2 - &4 * a * c`;
1153 TYPIFY `sqrt d * sqrt d = d` (C SUBGOAL_THEN MP_TAC);
1154 GMATCH_SIMP_TAC (GSYM SQRT_MUL);
1155 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
1156 BY(ASM_REWRITE_TAC[]);
1157 FIRST_X_ASSUM MP_TAC;
1158 BY(CONV_TAC REAL_RING)
1162 let quadratic_root_imp_discr_nn = prove_by_refinement(
1163 `!a b c x. (a * x pow 2 + b * x + c = &0) ==>
1164 &0 <= b pow 2 - &4 * a * c`,
1167 REPEAT WEAKER_STRIP_TAC;
1168 TYPIFY `b pow 2 - &4 * a * c = (&2 * a * x + b ) pow 2` (C SUBGOAL_THEN SUBST1_TAC);
1169 FIRST_X_ASSUM MP_TAC;
1170 BY(CONV_TAC REAL_RING);
1171 BY(REWRITE_TAC[ REAL_LE_POW_2])
1175 let quadratic_root_plus_eq = prove_by_refinement(
1177 (&0 < a) /\ (m <= x) /\ a * x pow 2 + b * x + c = &0 /\
1178 (&0 < &2 * m * a + b \/ (&2 * m * a + b) pow 2 < b pow 2 - &4 * a * c) ==>
1179 quadratic_root_plus (a,b,c) = x`,
1182 REPEAT WEAKER_STRIP_TAC;
1183 MATCH_MP_TAC Tame_lemmas.quadratic_root_plus_gt_eq;
1184 TYPED_ABBREV_TAC `y = -- (b + sqrt( b pow 2 - &4 * a * c)) / (&2 * a)` ;
1185 TYPIFY `y` EXISTS_TAC;
1188 MATCH_MP_TAC quadratic_root_imp_discr_nn;
1189 BY(ASM_MESON_TAC[]);
1193 MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] quadratic_root_minus_works);
1194 BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REAL_ARITH_TAC);
1195 COMMENT "both cases";
1196 TYPIFY `y < m` ENOUGH_TO_SHOW_TAC;
1197 BY(ASM_TAC THEN REAL_ARITH_TAC);
1198 TYPIFY `&2 * a * y + b < &2 * a * m + b` ENOUGH_TO_SHOW_TAC;
1199 REWRITE_TAC[arith `&2 * a * y + b < &2 * a * m + b <=> a * y < a * m`];
1200 GMATCH_SIMP_TAC REAL_LT_LMUL_EQ;
1201 BY(ASM_REWRITE_TAC[]);
1202 TYPIFY `&2 * a * y + b = -- sqrt(b pow 2 - &4 * a *c)` (C SUBGOAL_THEN SUBST1_TAC);
1204 Calc_derivative.CALC_ID_TAC;
1205 BY(ASM_TAC THEN REAL_ARITH_TAC);
1206 COMMENT "first case";
1207 ASM_CASES_TAC `&0 < &2 * m * a + b`;
1208 MATCH_MP_TAC REAL_LET_TRANS;
1209 TYPIFY `&0` EXISTS_TAC;
1211 REWRITE_TAC[arith `-- x <= &0 <=> &0 <= x`];
1212 GMATCH_SIMP_TAC SQRT_POS_LE;
1213 BY(ASM_TAC THEN REAL_ARITH_TAC);
1214 FIRST_X_ASSUM DISJ_CASES_TAC;
1215 BY(ASM_MESON_TAC[]);
1216 TYPIFY `(&2 * m * a + b) pow 2 < sqrt (b pow 2 - &4 * a * c) pow 2` (C SUBGOAL_THEN MP_TAC);
1217 GMATCH_SIMP_TAC SQRT_POW_2;
1218 BY(ASM_REWRITE_TAC[]);
1219 TYPED_ABBREV_TAC `d = sqrt(b pow 2 - &4 * a * c) `;
1220 ONCE_REWRITE_TAC[arith `-- d < &2 * a * m + b <=> --d < &2 * m * a +b`];
1221 REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS];
1222 TYPIFY `&0 <= d` (C SUBGOAL_THEN MP_TAC);
1224 GMATCH_SIMP_TAC SQRT_POS_LE;
1225 BY(ASM_REWRITE_TAC[]);
1226 BY(ASM_TAC THEN REAL_ARITH_TAC)
1230 let edge2_flatD_x1_delta_lemma2 = prove_by_refinement(
1231 `!d x1 x2 x3 x4 x5 x6.
1232 delta_x x1 x2 x3 x4 x5 x6 = d /\
1234 (delta_x1 x1 x2 x3 x4 x5 x6 < &0)
1236 edge2_flatD_x1 d x2 x3 x4 x5 x6 = x1`,
1239 REWRITE_TAC[Nonlin_def.edge2_flatD_x1];
1240 REPEAT WEAKER_STRIP_TAC;
1241 TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
1242 TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`;
1243 TYPIFY `!z. d - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC));
1246 REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
1249 REWRITE_TAC[Nonlinear_lemma.abc_quadratic];
1250 TYPIFY `b pow 2 - &4 * x4 * c = ups_x x2 x3 x4 * ups_x x4 x5 x6 - &4 * x4 * d` (C SUBGOAL_THEN ASSUME_TAC);
1253 REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
1255 MATCH_MP_TAC quadratic_root_plus_eq;
1256 TYPIFY `x1` EXISTS_TAC;
1258 REWRITE_TAC[arith `x <= x`];
1260 FIRST_X_ASSUM (C INTRO_TAC [`x1`]);
1261 BY(ASM_TAC THEN REAL_ARITH_TAC);
1264 FIRST_X_ASSUM_ST `d < &0` MP_TAC;
1265 REWRITE_TAC[Nonlin_def.delta_x1];
1270 let edge2_flatD_x1_delta_lemma3 = prove_by_refinement(
1271 ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6.
1272 delta_y y1 y2 y3 y4 y5 y6 = d /\
1273 &0 <= d /\ d <= &20 ==>
1274 (ineq [(&2,y1,#2.52);
1281 ( edge2_flatD_x1 d (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6) = y1*y1)))`,
1284 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1285 REPEAT WEAKER_STRIP_TAC;
1286 MATCH_MP_TAC edge2_flatD_x1_delta_lemma2;
1287 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys;
1288 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1290 BY(ASM_REWRITE_TAC[]);
1292 ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= &20 ==> ~(d > &20)`];
1293 REWRITE_TAC[Sphere.y_of_x;arith `y1 pow 2 = y1 * y1`];
1294 DISCH_THEN (unlist REWRITE_TAC);
1295 REWRITE_TAC[GSYM Sphere.delta_y];
1297 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1298 BY(ASM_TAC THEN REAL_ARITH_TAC)
1302 let delta_diff = prove_by_refinement(
1303 `!x1 z1 x2 x3 x4 x5 x6.
1304 delta_x x1 x2 x3 x4 x5 x6 = delta_x z1 x2 x3 x4 x5 x6 +
1305 delta_x1 x1 x2 x3 x4 x5 x6 * (x1 - z1) + x4 * (x1 - z1) pow 2`,
1308 BY(REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1] THEN REAL_ARITH_TAC)
1312 let delta_2_nn = prove_by_refinement(
1313 `main_nonlinear_terminal_v11 ==> (!z1 y2 y3 y4.
1314 &2 <= z1 /\ z1 <= &2 * h0 /\
1315 &2 <= y2 /\ y2 <= &2 * h0 /\
1316 &2 <= y3 /\ y3 <= &2 * h0 /\
1317 #3.01 <= y4 /\ y4 <= #3.915 /\
1318 delta_y z1 y2 y3 y4 (&2) (&2) = &0 ==>
1319 &0 <= delta_y (&2) y2 y3 y4 (&2) (&2))
1323 REWRITE_TAC[Sphere.delta_y];
1324 REPEAT WEAKER_STRIP_TAC;
1325 INTRO_TAC (UNDISCH2 (Terminal.get_main_nonlinear "3078028960")) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`];
1326 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1328 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1329 REWRITE_TAC[Sphere.y_of_x;Sphere.delta_y];
1330 ASM_REWRITE_TAC[arith `~(&0 > &20)`];
1332 FIRST_X_ASSUM DISJ_CASES_TAC;
1333 INTRO_TAC delta_diff [`&2* &2`;`z1 * z1`;`y2*y2`;`y3*y3`;`y4*y4`;`&2* &2`;`&2 * &2`];
1335 DISCH_THEN SUBST1_TAC;
1336 MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= &0 + x + y`);
1338 ONCE_REWRITE_TAC[arith `&0 <= a * b <=> &0 <= (--a) *(--b)`];
1339 GMATCH_SIMP_TAC REAL_LE_MUL;
1341 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1342 TYPIFY `&2 * &2 <= z1 * z1` ENOUGH_TO_SHOW_TAC;
1344 GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
1345 BY(ASM_TAC THEN REAL_ARITH_TAC);
1346 GMATCH_SIMP_TAC REAL_LE_MUL;
1347 REWRITE_TAC[ REAL_LE_POW_2];
1348 BY(REWRITE_TAC[ REAL_LE_SQUARE]);
1349 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
1353 let delta_mono = prove_by_refinement(
1354 ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6.
1355 &2 <= y1 /\ y1 <= z1 /\ z1 <= &2 * h0 /\
1356 &2 <= y2 /\ y2 <= &2 * h0 /\
1357 &2 <= y3 /\ y3 <= &2 * h0 /\
1358 #3.01 <= y4 /\ y4 <= #3.915 /\
1359 &2 <= y5 /\ y5 <= &2 /\
1360 &2 <= y6 /\ y6 <= &2 /\
1361 &0 <= delta_y y1 y2 y3 y4 y5 y6 /\
1362 delta_y y1 y2 y3 y4 y5 y6 <= &20 ==>
1363 delta_y z1 y2 y3 y4 y5 y6 <= delta_y y1 y2 y3 y4 y5 y6)
1367 REPEAT WEAKER_STRIP_TAC;
1368 REWRITE_TAC[Sphere.delta_y];
1369 INTRO_TAC delta_diff [`y1*y1`;`z1*z1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
1370 DISCH_THEN SUBST1_TAC;
1371 MATCH_MP_TAC (arith `&0 <= b /\ &0 <= c ==> a <= a + b + c`);
1373 GMATCH_SIMP_TAC REAL_LE_MUL;
1374 REWRITE_TAC[ REAL_LE_POW_2];
1375 BY(REWRITE_TAC[ REAL_LE_SQUARE]);
1376 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys;
1377 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1379 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1380 ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= d1 ==> ~(d > d1)`];
1381 REWRITE_TAC[Sphere.y_of_x];
1382 ONCE_REWRITE_TAC[arith `&0 <= x * y <=> &0 <= (-- x) * (-- y)`];
1384 GMATCH_SIMP_TAC REAL_LE_MUL;
1386 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1387 MATCH_MP_TAC (arith `y1 * y1 <= z1 * z1 ==> &0 <= -- (y1 * y1 - z1 * z1)`);
1388 GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
1389 BY(ASM_TAC THEN REAL_ARITH_TAC)
1393 let flat_term2_126_x_eval = prove_by_refinement(
1394 ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6.
1395 delta_y z y1 y2 y6 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\
1396 &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\
1397 &2 <= y2 /\ y2 <= &2 * h0 /\
1398 #3.01 <= y6 /\ y6 <= #3.915 ==>
1399 y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,
1402 REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_126_x;Nonlin_def.edge2_126_x];
1403 REWRITE_TAC[Functional_equation.uni;Functional_equation.compose6;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6];
1404 REPEAT WEAKER_STRIP_TAC;
1405 INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y2`;`y6`;`&2`;`&2`];
1406 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1408 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1409 REWRITE_TAC[arith `&2 * &2 = &4`];
1410 DISCH_THEN SUBST1_TAC;
1411 REWRITE_TAC[Sphere.flat_term_x];
1412 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
1413 BY(ASM_TAC THEN REAL_ARITH_TAC)
1417 let flat_term2_135_x_eval = prove_by_refinement(
1418 ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6.
1419 delta_y z y1 y3 y5 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\
1420 &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\
1421 &2 <= y3 /\ y3 <= &2 * h0 /\
1422 #3.01 <= y5 /\ y5 <= #3.915 ==>
1423 y_of_x (flat_term2_135_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,
1426 REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.edge2_135_x];
1427 REWRITE_TAC[Functional_equation.uni;Functional_equation.compose6;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6;Functional_equation.proj_x5;Functional_equation.proj_x3];
1428 REPEAT WEAKER_STRIP_TAC;
1429 INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y3`;`y5`;`&2`;`&2`];
1430 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1432 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1433 REWRITE_TAC[arith `&2 * &2 = &4`];
1434 DISCH_THEN SUBST1_TAC;
1435 REWRITE_TAC[Sphere.flat_term_x];
1436 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
1437 BY(ASM_TAC THEN REAL_ARITH_TAC)
1441 let delta_126_135 = prove_by_refinement(
1442 `!a b c y1 y2 y3 y4 y5 y6.
1443 delta_126_x a b c y1 y2 y3 y4 y5 y6 = delta_135_x a b c y1 y3 y2 y4 y6 y5`,
1446 REWRITE_TAC[Sphere.delta_126_x;Sphere.delta_135_x];
1447 BY(MESON_TAC[Merge_ineq.delta_x_sym])
1451 let delta_126_x_2h0_le_d = prove_by_refinement(
1452 ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6.
1462 &0 <= d /\ d <= &20 /\
1463 delta_y z1 y1 y2 y6 (&2) (&2) = d ==>
1464 y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,
1467 REPEAT WEAKER_STRIP_TAC;
1468 REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x];
1469 REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
1470 REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
1471 TYPIFY `delta_y y1 y2 (&2 * h0) (&2) (&2) y6 = delta_y (&2 * h0) y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
1472 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1473 INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y2`;`y6`;`&2`;`&2`];
1475 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1476 BY(ASM_REWRITE_TAC[])
1480 let delta_135_x_2h0_le_d = prove_by_refinement(
1481 ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6.
1491 &0 <= d /\ d <= &20 /\
1492 delta_y z1 y1 y3 y5 (&2) (&2) = d ==>
1493 y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,
1496 REPEAT WEAKER_STRIP_TAC;
1497 REWRITE_TAC[Sphere.y_of_x;Sphere.delta_135_x];
1498 REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
1499 REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
1500 TYPIFY `delta_y y1 (&2 * h0) y3 (&2) y5 (&2) = delta_y (&2 * h0) y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
1501 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1502 INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1504 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1505 BY(ASM_REWRITE_TAC[])
1509 let lemma_5546286427 = prove_by_refinement(
1510 ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6. ineq [
1520 &0 = delta_y z1 y1 y2 y6 (&2) (&2) ==>
1521 (taum y1 y2 y3 y4 y5 y6 + flat_term z1 + #0.12 > #0.616)))`,
1524 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1525 REPEAT WEAKER_STRIP_TAC;
1526 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5546286427") yys;
1527 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1529 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1530 GMATCH_SIMP_TAC flat_term2_126_x_eval;
1531 TYPIFY `z1` EXISTS_TAC;
1533 BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1534 COMMENT "remove delta_126_x";
1535 DISCH_THEN DISJ_CASES_TAC;
1536 BY(ASM_REWRITE_TAC[]);
1537 INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1539 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1540 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
1544 let taud_ge_flat_term = prove_by_refinement(
1545 `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 /\ y2 <= &2 * h0 /\ y3 <= &2 * h0 /\
1546 &0 <= delta_y y1 y2 y3 y4 y5 y6 ==>
1547 flat_term y1 <= taud y1 y2 y3 y4 y5 y6`,
1550 REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term];
1551 REPEAT WEAKER_STRIP_TAC;
1552 REWRITE_TAC[arith `a <= a + b <=> &0 <= b`];
1553 GMATCH_SIMP_TAC REAL_LE_MUL;
1554 GMATCH_SIMP_TAC SQRT_POS_LE;
1556 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1560 let terminal_pent_taum126_012 = prove_by_refinement(
1561 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1562 #0.12 <= taud y126 y1 y2 y6 (&2) (&2) /\
1563 &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1574 (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1578 REWRITE_TAC[Sphere.ineq];
1579 REPEAT WEAKER_STRIP_TAC;
1580 INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
1581 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
1583 BY(ASM_TAC THEN REAL_ARITH_TAC);
1584 REPEAT WEAKER_STRIP_TAC;
1585 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
1586 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1588 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1589 REWRITE_TAC[arith `x > y <=> y < x`];
1591 INTRO_TAC (UNDISCH OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`];
1593 BY(REWRITE_TAC[Sphere.cstab] THEN ASM_TAC THEN REAL_ARITH_TAC);
1595 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
1596 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1598 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1601 FIRST_X_ASSUM (DISJ_CASES_TAC);
1602 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7903347843") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1603 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1605 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1606 REWRITE_TAC[Sphere.y_of_x;mud_126_135];
1607 REWRITE_TAC[GSYM Sphere.y_of_x];
1608 TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1609 BY(MESON_TAC[Terminal.taum_sym]);
1610 GMATCH_SIMP_TAC taud_mud_135_x;
1612 BY(ASM_TAC THEN REAL_ARITH_TAC);
1613 MATCH_MP_TAC (arith `x <= a + b ==> t + x > #0.616 ==> #0.616 < a + t + b`);
1614 MATCH_MP_TAC (arith `t2 <= t135 /\ -- s <= f /\ #0.12 <= t126 ==> t2 - f - s + #0.12 <= t126+t135`);
1617 FIRST_X_ASSUM_ST `<=` MP_TAC THEN ASM_REWRITE_TAC[];
1618 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1619 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1620 MATCH_MP_TAC flat_term_sol0;
1622 COMMENT "case &0 <= tau";
1623 ASM_CASES_TAC `&0 <= taud y135 y1 y3 y5 (&2) (&2)`;
1624 BY(ASM_TAC THEN REAL_ARITH_TAC);
1625 COMMENT "case y=&2*h0";
1626 FIRST_X_ASSUM (DISJ_CASES_TAC);
1627 INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
1628 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1629 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1631 BY(ASM_TAC THEN REAL_ARITH_TAC);
1632 BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1633 COMMENT "case delta=0";
1634 FIRST_X_ASSUM DISJ_CASES_TAC;
1635 INTRO_TAC (UNDISCH lemma_5546286427) [`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1636 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1638 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1639 TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1640 BY(MESON_TAC[Terminal.taum_sym]);
1642 INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1644 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1645 BY(ASM_TAC THEN REAL_ARITH_TAC);
1646 COMMENT "final case";
1647 BY(ASM_TAC THEN REAL_ARITH_TAC)
1651 let terminal_pent_tau135_012 = prove_by_refinement(
1652 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1653 #0.12 <= taud y135 y1 y3 y5 (&2) (&2) /\
1654 &0 <= delta_y y126 y1 y2 y6 (&2) (&2) ==>
1665 (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1669 REWRITE_TAC[Sphere.ineq];
1670 REPEAT WEAKER_STRIP_TAC;
1671 INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`];
1672 ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1673 TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1674 BY(REWRITE_TAC[Terminal.taum_sym]);
1679 let sqrt20 = prove_by_refinement(
1680 `#4.47 <= sqrt(&20)`,
1683 MATCH_MP_TAC REAL_LE_RSQRT;
1688 let taud_053 = prove_by_refinement(
1692 &20 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 ==>
1693 #0.053 <= taud (&2 * h0) y2 y3 y4 y5 y6`,
1696 REWRITE_TAC[Nonlin_def.taud];
1697 REPEAT WEAKER_STRIP_TAC;
1698 TYPIFY `sol0 * (&2 * h0 - &2 * h0) / (&2 * h0 - &2) = &0` (C SUBGOAL_THEN SUBST1_TAC);
1700 TYPIFY `#0.053 = #4.47 * (#0.053 / #4.47)` (C SUBGOAL_THEN SUBST1_TAC);
1702 REWRITE_TAC[arith `&0 + x= x`];
1703 MATCH_MP_TAC REAL_LE_MUL2;
1707 MATCH_MP_TAC REAL_LE_TRANS;
1708 TYPIFY `sqrt(&20)` EXISTS_TAC;
1709 REWRITE_TAC[sqrt20];
1710 GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
1711 BY(ASM_TAC THEN REAL_ARITH_TAC);
1714 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1718 let terminal_pent_tau126_2 = prove_by_refinement(
1719 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1721 &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
1722 &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1733 (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1737 REWRITE_TAC[Sphere.ineq];
1738 REPEAT WEAKER_STRIP_TAC;
1739 INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
1740 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
1742 BY(ASM_TAC THEN REAL_ARITH_TAC);
1743 REPEAT WEAKER_STRIP_TAC;
1744 TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
1745 BY(MESON_TAC[Terminal.taum_sym]);
1746 COMMENT "case tau >= 0.12";
1747 ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
1748 INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
1750 BY(ASM_TAC THEN REAL_ARITH_TAC);
1751 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1753 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1755 COMMENT "case z1= &2";
1756 ASM_CASES_TAC `z1 = &2`;
1757 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7997589055") yys;
1758 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1760 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1761 GMATCH_SIMP_TAC taud_mud_126_x;
1762 GMATCH_SIMP_TAC taud_mud_135_x;
1763 REWRITE_TAC[flat_term_2];
1764 TYPIFY_GOAL_THEN ` &0 <= y1 /\ &0 <= y2 /\ &0 <= y3` (unlist REWRITE_TAC);
1765 BY(ASM_TAC THEN REAL_ARITH_TAC);
1767 REPEAT (FIRST_X_ASSUM_ST `x = &2` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1768 BY(ASM_TAC THEN REAL_ARITH_TAC);
1769 COMMENT "case delta=0";
1770 ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
1771 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2565248885") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1772 REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1774 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1775 REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`];
1776 GMATCH_SIMP_TAC (UNDISCH2 delta_126_x_2h0_le_d);
1778 TYPIFY `z1` EXISTS_TAC;
1779 BY(ASM_TAC THEN REAL_ARITH_TAC);
1780 GMATCH_SIMP_TAC taud_mud_135_x;
1781 REWRITE_TAC[flat_term_2];
1782 GMATCH_SIMP_TAC (UNDISCH2 flat_term2_126_x_eval);
1783 TYPIFY `z1` EXISTS_TAC;
1785 BY(ASM_TAC THEN REAL_ARITH_TAC);
1787 BY(ASM_TAC THEN REAL_ARITH_TAC);
1788 INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1790 BY(ASM_TAC THEN REAL_ARITH_TAC);
1791 REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
1793 COMMENT "case delta>=20";
1794 TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC);
1795 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
1797 ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`;
1798 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2320951108") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1799 REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1801 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1802 GMATCH_SIMP_TAC taud_mud_135_x;
1803 REWRITE_TAC[flat_term_2];
1804 INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`];
1806 FIRST_X_ASSUM MP_TAC;
1807 BY(ASM_REWRITE_TAC[]);
1809 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1812 BY(ASM_TAC THEN REAL_ARITH_TAC);
1813 REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
1815 COMMENT "case delta <= 20";
1816 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5429238960") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1817 REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1819 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1820 GMATCH_SIMP_TAC taud_mud_135_x;
1821 REWRITE_TAC[flat_term_2];
1823 BY(ASM_TAC THEN REAL_ARITH_TAC);
1824 INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1826 BY(ASM_TAC THEN REAL_ARITH_TAC);
1827 INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
1829 FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1830 BY(ASM_TAC THEN REAL_ARITH_TAC);
1832 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1833 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1837 let terminal_pent_tau135_2 = prove_by_refinement(
1838 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1840 &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
1841 &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1852 (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1856 REWRITE_TAC[Sphere.ineq];
1857 REPEAT WEAKER_STRIP_TAC;
1858 INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`];
1859 ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1860 TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1861 BY(REWRITE_TAC[Terminal.taum_sym]);
1866 let terminal_pent_tau126_2h0 = prove_by_refinement(
1867 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1869 &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
1870 &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1881 (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1885 REWRITE_TAC[Sphere.ineq];
1886 REPEAT WEAKER_STRIP_TAC;
1887 INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
1888 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
1890 BY(ASM_TAC THEN REAL_ARITH_TAC);
1891 REPEAT WEAKER_STRIP_TAC;
1892 TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
1893 BY(MESON_TAC[Terminal.taum_sym]);
1894 COMMENT "case tau >= 0.12";
1895 ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
1896 INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
1898 BY(ASM_TAC THEN REAL_ARITH_TAC);
1899 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1901 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1903 COMMENT "case z1= &2";
1904 ASM_CASES_TAC `z1 = &2`;
1905 INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`];
1906 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1908 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1909 BY(ASM_TAC THEN REAL_ARITH_TAC);
1910 COMMENT "case delta = 0";
1911 ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
1912 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1948775510") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1913 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1915 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1916 GMATCH_SIMP_TAC (taud_mud_135_x);
1918 BY(ASM_TAC THEN REAL_ARITH_TAC);
1919 REWRITE_TAC[flat_term_2h0];
1920 GMATCH_SIMP_TAC flat_term2_126_x_eval;
1921 TYPIFY `z1` EXISTS_TAC;
1924 BY(ASM_TAC THEN REAL_ARITH_TAC);
1925 INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1927 BY(ASM_TAC THEN REAL_ARITH_TAC);
1928 INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1930 BY(ASM_TAC THEN REAL_ARITH_TAC);
1931 REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`] THEN DISCH_THEN (unlist REWRITE_TAC);
1932 REWRITE_TAC[Sphere.delta_135_x;Sphere.y_of_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
1933 REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
1934 TYPIFY `delta_y y1 (&2 * h0) y2 (&2) y6 (&2) = delta_y y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
1936 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1939 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1940 BY(ASM_TAC THEN REAL_ARITH_TAC);
1941 COMMENT "case z1=2h0, delta>=20";
1942 TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC);
1943 BY(ASM_MESON_TAC[]);
1945 INTRO_TAC taud_053 [`y1`;`y2`;`y6`;`&2`;`&2`];
1948 BY(FIRST_X_ASSUM_ST `&20 <= d` MP_TAC THEN ASM_REWRITE_TAC[]);
1950 ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`;
1951 INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`];
1954 BY(REPEAT (FIRST_X_ASSUM_ST `&20 <= d` MP_TAC) THEN ASM_REWRITE_TAC[]);
1956 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
1957 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1959 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1961 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1962 REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
1964 COMMENT "case z1=2h0, delta<=20";
1965 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5708641738") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1966 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1968 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1969 INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1971 BY(ASM_TAC THEN REAL_ARITH_TAC);
1973 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1974 INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
1976 BY(ASM_TAC THEN ASM_MESON_TAC[]);
1977 BY(ASM_TAC THEN REAL_ARITH_TAC)
1981 let taud_sqrt20 = prove_by_refinement(
1982 ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6.
1993 delta_y z1 y1 y3 y5 (&2) (&2) = &20 ==>
1994 y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1995 (#0.012 + #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 <= taud z1 y1 y3 y5 (&2) (&2))`,
1998 REPEAT WEAKER_STRIP_TAC;
1999 GMATCH_SIMP_TAC flat_term2_135_x_eval;
2000 TYPIFY `z1` EXISTS_TAC;
2002 REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term];
2003 REWRITE_TAC[ (arith `u + c * s <= u + s' * c' <=> c * s <= c' * s'`)];
2004 MATCH_MP_TAC REAL_LE_MUL2;
2006 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2007 ASM_REWRITE_TAC[sqrt20];
2008 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
2012 let terminal_pent_tau126_delta20 = prove_by_refinement(
2013 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
2014 delta_y y126 y1 y2 y6 (&2) (&2) = &20 /\
2015 &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
2026 (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
2030 REWRITE_TAC[Sphere.ineq];
2031 REPEAT WEAKER_STRIP_TAC;
2032 INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
2033 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
2035 BY(ASM_TAC THEN REAL_ARITH_TAC);
2036 REPEAT WEAKER_STRIP_TAC;
2037 TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
2038 BY(MESON_TAC[Terminal.taum_sym]);
2039 COMMENT "case tau >= 0.12";
2040 ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
2041 INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
2043 BY(ASM_TAC THEN REAL_ARITH_TAC);
2044 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2046 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2048 COMMENT "case z1= &2";
2049 ASM_CASES_TAC `z1 = &2`;
2050 INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`];
2051 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2053 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2054 BY(ASM_TAC THEN REAL_ARITH_TAC);
2055 COMMENT "delta issue";
2056 TYPIFY `~( y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y3 y2 y4 y6 y5 > &20 )` (C SUBGOAL_THEN MP_TAC);
2057 REWRITE_TAC[arith `~(x > d) <=> (x<=d)`];
2058 GMATCH_SIMP_TAC delta_135_x_2h0_le_d;
2059 TYPIFY `y126` EXISTS_TAC;
2061 BY(ASM_TAC THEN REAL_ARITH_TAC);
2063 COMMENT "case delta = 0";
2064 ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
2065 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1008824382") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2066 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2068 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2069 GMATCH_SIMP_TAC flat_term2_126_x_eval;
2070 TYPIFY `z1` EXISTS_TAC;
2073 BY(ASM_TAC THEN REAL_ARITH_TAC);
2074 GMATCH_SIMP_TAC flat_term2_135_x_eval;
2075 TYPIFY `y126` EXISTS_TAC;
2077 FIRST_X_ASSUM_ST `d = &20` SUBST1_TAC;
2079 BY(ASM_TAC THEN REAL_ARITH_TAC);
2080 INTRO_TAC mu_y_ft_combine2 [`y126`;`y1`;`y2`];
2082 BY(ASM_REWRITE_TAC[]);
2083 TYPIFY `mu_y y126 y1 y2 * sqrt(&20) + flat_term y126 <= taud y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN MP_TAC);
2084 REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y;Sphere.flat_term];
2085 REWRITE_TAC[ (arith `c * s + u <= u + s' * c <=> c * s <= c * s'`)];
2086 GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
2088 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2089 GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
2090 BY(ASM_TAC THEN REAL_ARITH_TAC);
2091 TYPIFY `(#0.012 + #0.01 * ( #2.52 * &2 - y1 - y2)) * #4.47 <= mu_y (&2 * h0) y1 y2 * sqrt(&20)` (C SUBGOAL_THEN MP_TAC);
2092 REWRITE_TAC[Nonlin_def.mu_y];
2093 MATCH_MP_TAC REAL_LE_MUL2;
2095 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2096 REWRITE_TAC[sqrt20];
2097 BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2098 INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
2100 BY(ASM_TAC THEN REAL_ARITH_TAC);
2101 FIRST_X_ASSUM_ST `~` (unlist REWRITE_TAC);
2102 REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`];
2103 GMATCH_SIMP_TAC delta_126_x_2h0_le_d;
2105 TYPIFY `z1` EXISTS_TAC;
2107 BY(ASM_TAC THEN REAL_ARITH_TAC);
2109 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2110 REWRITE_TAC[flat_term_2h0];
2111 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2112 COMMENT "z1=2h0 and delta <=20";
2113 TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN ASSUME_TAC);
2114 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
2115 ASM_CASES_TAC `delta_y z1 y1 y3 y5 (&2) (&2) <= &20`;
2116 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1586903463") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2117 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2119 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2120 INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
2122 BY(REPEAT (FIRST_X_ASSUM_ST `<=` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2123 INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2125 BY(ASM_TAC THEN REAL_ARITH_TAC);
2127 REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
2128 REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
2129 TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
2131 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
2133 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2134 BY(ASM_TAC THEN REAL_ARITH_TAC);
2135 COMMENT "z1=2h0 and delta> 20";
2136 INTRO_TAC ((*--*)Terminal.get_main_nonlinear "8875146520") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2137 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2139 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2140 GMATCH_SIMP_TAC taud_mud_126_x;
2141 REWRITE_TAC[flat_term_2h0];
2142 INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2144 BY(ASM_TAC THEN REAL_ARITH_TAC);
2145 FIRST_X_ASSUM_ST `y_of_x` (unlist REWRITE_TAC);
2146 REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
2147 REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
2148 TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
2150 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
2152 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2153 BY(ASM_TAC THEN REAL_ARITH_TAC)
2157 let terminal_pent_taum = prove_by_refinement(
2158 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
2159 &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
2160 &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
2171 (#0.616 < taum y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taum y135 y1 y3 y5 (&2) (&2))))
2175 REWRITE_TAC[Sphere.ineq];
2176 REPEAT WEAKER_STRIP_TAC;
2177 INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&20`;`y126`;`y1`;`y2`;`y6`;`(&2)`;`&2`];
2178 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
2180 BY(ASM_TAC THEN REAL_ARITH_TAC);
2181 REPEAT WEAKER_STRIP_TAC;
2182 INTRO_TAC (UNDISCH2 OWZLKVY4) [`y126`;`y1`;`y2`;`y6`;`&2`;`&2`];
2184 BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2185 INTRO_TAC (UNDISCH2 OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`];
2187 BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2188 TYPIFY `#0.616 < taud z1 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2)` ENOUGH_TO_SHOW_TAC;
2189 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2190 COMMENT "case z1=2";
2191 FIRST_X_ASSUM DISJ_CASES_TAC;
2192 INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2193 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2195 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2197 COMMENT "case z1=2h0";
2198 FIRST_X_ASSUM DISJ_CASES_TAC;
2199 INTRO_TAC (UNDISCH2 terminal_pent_tau126_2h0) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2200 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2202 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2204 COMMENT "case delta=20";
2205 FIRST_X_ASSUM DISJ_CASES_TAC;
2206 INTRO_TAC (UNDISCH2 terminal_pent_tau126_delta20) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2207 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2209 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2211 COMMENT "case tau012";
2212 INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2213 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2215 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2220 (* HEXAGON SECTION terminal_hex *)
2222 let taud_minimizer_terminal_hex_cases = prove_by_refinement(
2223 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4.
2224 (&0 <= delta_y y1 y2 y3 y4 (&2) (&2) /\
2225 &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\
2226 #3.01 <= y4 /\ y4 <= #3.915 /\ taum y1 y2 y3 y4 (&2) (&2) < &0 ==>
2227 (?z1. &0 <= delta_y z1 y2 y3 y4 (&2) (&2) /\
2228 &2 <= z1 /\ z1 <= &2 * h0 /\ taud z1 y2 y3 y4 (&2) (&2) <= taud y1 y2 y3 y4 (&2) (&2) /\
2229 ( z1 = &2 \/ &0 = delta_y z1 y2 y3 y4 (&2) (&2) ))))`,
2232 REPEAT WEAKER_STRIP_TAC;
2233 INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`&0`;`y2`;`y3`;`y4`;`&2`;`&2`];
2234 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
2236 REWRITE_TAC[arith `&0 <= &0`;NOT_FORALL_THM];
2237 BY(ASM_MESON_TAC[]);
2238 REPEAT WEAKER_STRIP_TAC;
2239 TYPIFY `z1` EXISTS_TAC;
2242 REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2243 BY(ASM_MESON_TAC[]);
2244 INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2245 REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
2247 BY(ASM_MESON_TAC[arith `&0 <= &2 /\ &0 <= &0`;arith `&2 <= y ==> &0 <= y`]);
2248 ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC);
2249 ASM_CASES_TAC `&0 = delta_y z1 y2 y3 y4 (&2) (&2)` THEN FIRST_ASSUM (unlist ASM_REWRITE_TAC);
2250 ASM_CASES_TAC `z1 = &2 * h0` THEN ASM_REWRITE_TAC[];
2251 INTRO_TAC (UNDISCH OWZLKVY4 ) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2253 BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2254 FIRST_X_ASSUM (C INTRO_TAC [`y1`]);
2256 BY(ASM_REWRITE_TAC[]);
2258 FIRST_X_ASSUM_ST `taum` MP_TAC;
2259 INTRO_TAC taud_2h0 [`y2`;`y3`;`y4`;`&2`;`&2`];
2261 BY(ASM_MESON_TAC[]);
2263 COMMENT "derviative cases";
2264 ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 (&2) (&2) < &15)`;
2265 REPEAT WEAKER_STRIP_TAC;
2266 INTRO_TAC (Terminal.get_main_nonlinear "6877738680") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2267 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2269 GMATCH_SIMP_TAC Functional_equation.taud_x_taud;
2270 INTRO_TAC (UNDISCH OWZLKVY4) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2272 BY(ASM_REWRITE_TAC[Sphere.cstab]);
2273 FIRST_X_ASSUM (C INTRO_TAC [`y1`]);
2275 BY(ASM_REWRITE_TAC[]);
2276 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2277 INTRO_TAC (Terminal.get_main_nonlinear "9692636487") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2278 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2281 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2282 BY(REPEAT (FIRST_X_ASSUM_ST `delta_y` MP_TAC) THEN REAL_ARITH_TAC)
2286 (* next, de-symmetrize everything,
2287 then combine delta ranges. *)
2289 let REAL_WLOG_S3_SIMPLEX = prove_by_refinement(
2290 `!(P:A->A->A->real->real->real->bool). (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y3 y1 y2 y6 y4 y5 /\
2291 P y1 y2 y3 y4 y5 y6 = P y2 y1 y3 y5 y4 y6) /\
2292 (!y1 y2 y3 y4 y5 y6. y4 <= y6 /\ y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==>
2293 (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
2296 REPEAT WEAK_STRIP_TAC;
2297 TYPIFY `(y4 <= y5 /\ y5 <= y6) \/ (y4 <= y6 /\ y6 <= y5) \/ (y5 <= y4 /\ y4 <= y6) \/ (y5 <= y6 /\ y6 <= y4) \/ (y6 <= y5 /\ y5 <= y4) \/ (y6 <= y4 /\ y4 <= y5)` (C SUBGOAL_THEN ASSUME_TAC);
2299 BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
2303 let REAL_WLOG_AAB_SIMPLEX = prove_by_refinement(
2304 `!(P:A->A->A->real->real->real->bool). (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y3 y2 y1 y6 y5 y4) /\
2305 (!y1 y2 y3 y4 y5 y6. y4 <= y6 ==> P y1 y2 y3 y4 y5 y6) ==>
2306 (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
2309 REPEAT WEAK_STRIP_TAC;
2310 TYPIFY `(y4 <= y6 \/ y6 <= y4)` (C SUBGOAL_THEN ASSUME_TAC);
2312 BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
2316 let REAL_WLOG_ABB_SIMPLEX = prove_by_refinement(
2317 `!(P:A->A->A->real->real->real->bool). (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\
2318 (!y1 y2 y3 y4 y5 y6. y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==>
2319 (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
2322 REPEAT WEAK_STRIP_TAC;
2323 TYPIFY `(y5 <= y6 \/ y6 <= y5)` (C SUBGOAL_THEN ASSUME_TAC);
2325 BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
2329 let delta_y_hex_cases = prove_by_refinement(
2330 `!y1 y2 y3 y5 y6 a b. (delta_y y1 y2 a (&2) (&2) y6 = delta_y a y1 y2 y6 (&2) (&2) /\
2331 (delta_y y1 b y3 (&2) y5 (&2) = delta_y b y1 y3 y5 (&2) (&2)))`,
2334 BY(MESON_TAC[Merge_ineq.delta_y_sym])
2338 let delta_y_sym_cases2 = prove_by_refinement(
2339 `!y1 y2 y3 y4 y5 y6 a. delta_y a y3 y1 y5 (&2) (&2) = delta_y a y1 y3 y5 (&2) (&2) /\
2340 delta_y a y3 y2 y4 (&2) (&2) = delta_y a y2 y3 y4 (&2) (&2) /\
2341 delta_y a y2 y1 y6 (&2) (&2) = delta_y a y1 y2 y6 (&2) (&2)`,
2344 BY(MESON_TAC[Merge_ineq.delta_y_sym])
2348 let taum_sym_cases2 = prove_by_refinement(
2349 `!y1 y2 y3 y4 y5 y6. taum y2 y1 y3 y5 y4 y6 = taum y1 y2 y3 y4 y5 y6 /\
2350 taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6 /\
2351 taum y3 y1 y2 y6 y4 y5 = taum y1 y2 y3 y4 y5 y6 /\
2352 taum y3 y2 y1 y6 y5 y4 = taum y1 y2 y3 y4 y5 y6`,
2355 BY(MESON_TAC[Terminal.taum_sym])
2359 let edge2_flatD_sym = prove_by_refinement(
2360 `!d y1 y2 y3 a. edge2_flatD_x1 d y1 y2 y3 a a = edge2_flatD_x1 d y2 y1 y3 a a`,
2363 BY(REWRITE_TAC[Nonlin_def.edge2_flatD_x1;Merge_ineq.delta_x_sym])
2367 let edge2_flatD_x1_sym_cases = prove_by_refinement(
2368 `!y1 y2 y3 y4 y5 y6.
2369 edge2_flatD_x1 (&0) (y3 * y3) (y2 * y2) (y4*y4) (&2 * &2) (&2* &2) =
2370 edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4*y4) (&2 * &2) (&2* &2) /\
2371 edge2_flatD_x1 (&0) (y3 * y3) (y1 * y1) (y5*y5) (&2 * &2) (&2* &2) =
2372 edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5*y5) (&2 * &2) (&2* &2) /\
2373 edge2_flatD_x1 (&0) (y2 * y2) (y1 * y1) (y6*y6) (&2 * &2) (&2* &2) =
2374 edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6*y6) (&2 * &2) (&2* &2)
2378 BY(REWRITE_TAC[edge2_flatD_sym])
2382 let eulerA_x_sym_cases = prove_by_refinement(
2383 `!y1 y2 y3 y4 y5 y6.
2384 eulerA_x (y2 * y2) (y1 * y1) (y3 * y3) (y5 * y5) (y4 * y4) (y6 * y6) =
2385 eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) /\
2386 eulerA_x (y3 * y3) (y1 * y1) (y2 * y2) (y6 * y6) (y4 * y4) (y5 * y5) =
2387 eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) /\
2388 eulerA_x (y3 * y3) (y2 * y2) (y1 * y1) (y6 * y6) (y5 * y5) (y4 * y4) =
2389 eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) /\
2390 eulerA_x (y1 * y1) (y3 * y3) (y2 * y2) (y4 * y4) (y6 * y6) (y5 * y5) =
2391 eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) `,
2394 REWRITE_TAC[Sphere.eulerA_x];
2399 let mu_y_sym = prove_by_refinement(
2400 `!y1 y2 y3. mu_y y1 y2 y3 = mu_y y1 y3 y2`,
2403 REWRITE_TAC[Nonlin_def.mu_y];
2408 let mu_y_sym_cases = prove_by_refinement(
2409 `!y1 y2 y3. mu_y (&2) (sqrt(y2 * y2)) (sqrt(y1*y1)) =
2410 mu_y (&2) (sqrt(y1 * y1)) (sqrt(y2*y2)) /\
2411 mu_y (&2) (sqrt(y3 * y3)) (sqrt(y2*y2)) =
2412 mu_y (&2) (sqrt(y2 * y2)) (sqrt(y3*y3)) /\
2413 mu_y (&2) (sqrt(y3 * y3)) (sqrt(y1*y1)) =
2414 mu_y (&2) (sqrt(y1 * y1)) (sqrt(y3*y3))
2418 BY(REWRITE_TAC[mu_y_sym])
2422 let nonfunctional_mud_126 = prove_by_refinement(
2423 `! a b c y1 y2 y3 y4 y5 y6. y_of_x (mud_126_x_v1 a b c) y1 y2 y3 y4 y5 y6 =
2424 mu_y a (sqrt(y1 * y1)) (sqrt(y2 * y2)) * sqrt(delta_y a y1 y2 y6 b c)`,
2427 REWRITE_TAC[Nonlin_def.mud_126_x;];
2428 Functional_equation.F_REWRITE_TAC;
2429 REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y];
2430 BY(MESON_TAC[Merge_ineq.delta_y_sym])
2434 let nonfunctional_mud_234 = prove_by_refinement(
2435 `! a b c y1 y2 y3 y4 y5 y6. y_of_x (mud_234_x_v1 a b c) y1 y2 y3 y4 y5 y6 =
2436 mu_y a (sqrt(y2 * y2)) (sqrt(y3 * y3)) * sqrt(delta_y a y2 y3 y4 b c)`,
2439 REWRITE_TAC[Nonlin_def.mud_234_x;];
2440 Functional_equation.F_REWRITE_TAC;
2441 REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y];
2445 let nonfunctional_mud_135 = prove_by_refinement(
2446 `! a b c y1 y2 y3 y4 y5 y6. y_of_x (mud_135_x_v1 a b c) y1 y2 y3 y4 y5 y6 =
2447 mu_y a (sqrt(y1 * y1)) (sqrt(y3 * y3)) * sqrt(delta_y a y1 y3 y5 b c)`,
2450 REWRITE_TAC[Nonlin_def.mud_135_x;];
2451 Functional_equation.F_REWRITE_TAC;
2452 REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y];
2453 REWRITE_TAC[mu_y_sym];
2454 BY(MESON_TAC[Merge_ineq.delta_y_sym])
2458 let nonfunctional_flat_term2_126 = prove_by_refinement(
2459 `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_126_x d a b) x1 x2 x3 x4 x5 x6 =
2460 flat_term (sqrt (edge2_flatD_x1 d x1 x2 x6 a b))`,
2463 REWRITE_TAC[Nonlin_def.flat_term2_126_x];
2464 BY(REWRITE_TAC[Functional_equation.uni;Sphere.flat_term_x;Nonlin_def.edge2_126_x;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6;Functional_equation.compose6])
2468 let nonfunctional_flat_term2_234 = prove_by_refinement(
2469 `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_234_x d a b) x1 x2 x3 x4 x5 x6 =
2470 flat_term (sqrt (edge2_flatD_x1 d x2 x3 x4 a b))`,
2473 REWRITE_TAC[Nonlin_def.flat_term2_234_x];
2474 BY(REWRITE_TAC[Functional_equation.uni;Sphere.flat_term_x;Nonlin_def.edge2_234_x;Functional_equation.constant6;Functional_equation.proj_x2;Functional_equation.proj_x3;Functional_equation.proj_x4;Functional_equation.compose6])
2478 let nonfunctional_flat_term2_135 = prove_by_refinement(
2479 `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_135_x d a b) x1 x2 x3 x4 x5 x6 =
2480 flat_term (sqrt (edge2_flatD_x1 d x1 x3 x5 a b))`,
2483 REWRITE_TAC[Nonlin_def.flat_term2_135_x];
2484 BY(REWRITE_TAC[Functional_equation.uni;Sphere.flat_term_x;Nonlin_def.edge2_135_x;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x3;Functional_equation.proj_x5;Functional_equation.compose6])
2488 let nonfunctional_mudLs_126 = prove_by_refinement(
2489 `! y1 y2 x3 x4 x5 y6. mudLs_126_x (&4) (&10) (&2) (&2) (&2) (y1*y1) (y2*y2) x3 x4 x5 (y6*y6) =
2490 mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
2491 (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &4)`,
2494 REWRITE_TAC[Nonlin_def.mudLs_126_x];
2495 Functional_equation.F_REWRITE_TAC;
2496 REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y;delta_y_hex_cases];
2497 REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
2498 TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
2499 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2505 let nonfunctional_mudLs_234 = prove_by_refinement(
2506 `! x1 y2 y3 y4 x5 x6. mudLs_234_x (&4) (&10) (&2) (&2) (&2) x1 (y2*y2) (y3*y3) (y4*y4) x5 x6 =
2507 mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2508 (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &4)`,
2511 REWRITE_TAC[Nonlin_def.mudLs_234_x];
2512 Functional_equation.F_REWRITE_TAC;
2513 REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y;delta_y_hex_cases];
2514 REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
2515 TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
2516 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2522 let nonfunctional_mudLs_135 = prove_by_refinement(
2523 `! y1 x2 y3 x4 y5 x6. mudLs_135_x (&4) (&10) (&2) (&2) (&2) (y1*y1) x2 (y3*y3) x4 (y5*y5) x6 =
2524 mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
2525 (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &4)`,
2528 REWRITE_TAC[Nonlin_def.mudLs_135_x];
2529 Functional_equation.F_REWRITE_TAC;
2530 REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y;delta_y_hex_cases];
2531 REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
2532 TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
2533 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2539 let ineq_sym_s3 = prove_by_refinement(
2541 ineq p (r \/ y6 < y4 \/ y5 < y6) ==>
2542 ((y4 <= y6 /\ y6 <= y5) ==> ineq p r)`,
2545 REPEAT WEAKER_STRIP_TAC;
2546 FIRST_X_ASSUM_ST `ineq` MP_TAC;
2547 BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
2551 let ineq_sym_s2_aab = prove_by_refinement(
2552 `!y4 y6 p r. ineq p (r \/ y6 < y4) ==>
2553 ((y4 <= y6) ==> ineq p r)`,
2556 REPEAT WEAKER_STRIP_TAC;
2557 FIRST_X_ASSUM_ST `ineq` MP_TAC;
2558 BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
2562 let ineq_sym_s2_abb = prove_by_refinement(
2563 `!y5 y6 p r. ineq p (r \/ y5 < y6) ==>
2564 ((y6 <= y5) ==> ineq p r)`,
2567 REPEAT WEAKER_STRIP_TAC;
2568 FIRST_X_ASSUM_ST `ineq` MP_TAC;
2569 BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
2573 let clean_ineq = PURE_REWRITE_RULE[Sphere.y_of_x;Sphere.delta_234_x;Sphere.delta_126_x;Sphere.delta_135_x;
2574 arith `#2.52 pow 2 = #2.52 * #2.52 /\ &4 = &2 * &2`;GSYM Sphere.delta_y;delta_y_hex_cases;
2575 nonfunctional_mud_126;nonfunctional_mud_234;nonfunctional_mud_135;
2576 nonfunctional_flat_term2_126; nonfunctional_flat_term2_234; nonfunctional_flat_term2_135;
2577 nonfunctional_mudLs_135 ;nonfunctional_mudLs_126 ;nonfunctional_mudLs_234];;
2579 let mk_ineq_hex conv i234 i126 i135 =
2580 let nth = List.nth in
2581 let d234 = nth [` y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
2583 `y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
2584 `y_of_x (mudLs_234_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
2585 `&0 - sol0`] i234 in
2586 let d126 = nth [` y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
2588 `y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
2589 `y_of_x (mudLs_126_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
2590 `&0 - sol0`] i126 in
2591 let d135 = nth [` y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
2593 `y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
2594 `y_of_x (mudLs_135_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
2595 `&0 - sol0`] i135 in
2596 let c234 = nth [`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2597 y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
2599 `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
2600 `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
2601 y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
2602 `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2603 y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i234 in
2604 let c126 = nth [`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2605 y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
2607 `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
2608 `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
2609 y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
2610 `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2611 y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i126 in
2612 let c135 = nth [`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2613 y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
2615 `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
2616 `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
2617 y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
2618 `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2619 y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i135 in
2620 let s45 = if (i234= i126) then `y6 < y4` else `F` in
2621 let s56 = if (i126= i135) then `y5 < y6` else `F` in
2622 rhs(concl(conv (Ineq.mk_tplate Main_estimate_ineq.template_hex [d234;d126;d135;c234;c126;c135;s45;s56])));;
2626 let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in
2627 let g' = (mk_imp (`main_nonlinear_terminal_v11`,concl (clean_ineq (ASSUME g)))) in
2631 let get_ineq (a,b,c) =
2632 clean_ineq (Terminal.get_main_nonlinear (Printf.sprintf "7550003505 %d %d %d" a b c));;
2634 let get_ineq_term(a,b,c) =
2635 let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in
2636 concl (clean_ineq (ASSUME g));;
2638 let get_ineq'(a,b,c) =
2639 let g' = mk_imp(`main_nonlinear_terminal_v11`,get_ineq_term(a,b,c)) in
2640 repeat UNDISCH (prove_by_refinement(g',[
2642 BY(REWRITE_TAC[get_ineq(a,b,c)])]));;
2645 let (yys,tm) = (strip_forall (concl(get_ineq' (i,i,i)))) in
2646 let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`y6 < y4 <=> F`);ASSUME (`y5 < y6 <=> F`)] tm)) in
2647 let tm1 = list_mk_forall (yys, tm0) in
2648 let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2649 prove_by_refinement(tm2,
2653 MATCH_MP_TAC REAL_WLOG_S3_SIMPLEX;
2655 REPEAT WEAKER_STRIP_TAC;
2656 INTRO_TAC delta_y_sym_cases2 yys;
2657 DISCH_THEN (unlist REWRITE_TAC);
2658 INTRO_TAC taum_sym_cases2 yys;
2659 DISCH_THEN (unlist REWRITE_TAC);
2660 INTRO_TAC edge2_flatD_x1_sym_cases yys;
2661 DISCH_THEN (unlist REWRITE_TAC);
2662 INTRO_TAC eulerA_x_sym_cases yys;
2663 DISCH_THEN (unlist REWRITE_TAC);
2664 INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2665 DISCH_THEN (unlist REWRITE_TAC);
2666 TYPIFY_GOAL_THEN `!f. f y1 y2 y6 + f y1 y3 y5 + f y2 y3 y4 = f y2 y3 y4 + f y1 y2 y6 + f y1 y3 y5 /\ f y1 y3 y5 + f y1 y2 y6 + f y2 y3 y4 = f y2 y3 y4 + f y1 y2 y6 + f y1 y3 y5` (unlist ONCE_REWRITE_TAC);
2668 BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
2670 MATCH_MP_TAC ineq_sym_s3;
2671 INTRO_TAC (get_ineq(i,i,i)) yys;
2672 BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
2676 let r755_diag = map (fun i -> (i, r755_0 i)) [0;1;2;3;4];;
2680 let (yys,tm) = (strip_forall (concl(get_ineq' (i,i,j)))) in
2681 let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y6 < y4) <=> F`)] tm)) in
2682 let tm1 = list_mk_forall (yys, tm0) in
2683 let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2684 prove_by_refinement(tm2,
2688 MATCH_MP_TAC REAL_WLOG_AAB_SIMPLEX;
2690 REPEAT WEAKER_STRIP_TAC;
2691 INTRO_TAC delta_y_sym_cases2 yys;
2692 DISCH_THEN (unlist REWRITE_TAC);
2693 INTRO_TAC taum_sym_cases2 yys;
2694 DISCH_THEN (unlist REWRITE_TAC);
2695 INTRO_TAC edge2_flatD_x1_sym_cases yys;
2696 DISCH_THEN (unlist REWRITE_TAC);
2697 INTRO_TAC eulerA_x_sym_cases yys;
2698 DISCH_THEN (unlist REWRITE_TAC);
2699 INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2700 DISCH_THEN (unlist REWRITE_TAC);
2701 TYPIFY_GOAL_THEN `!f b. f y1 y2 y6 + f y2 y3 y4 + b = f y2 y3 y4 + f y1 y2 y6 + b` (unlist ONCE_REWRITE_TAC);
2703 BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
2705 MATCH_MP_TAC ineq_sym_s2_aab;
2706 INTRO_TAC (get_ineq(i,i,j)) yys;
2707 BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
2711 let r755_aab_list = map (fun (i,j) -> ((i,j),r755_aab i j)) [(0,1);(0,2);(0,3);(0,4);(1,2);(1,3);(1,4);
2712 (2,3);(2,4);(3,4)];;
2715 let (yys,tm) = (strip_forall (concl(get_ineq' (i,j,j)))) in
2716 let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y5 < y6) <=> F`)] tm)) in
2717 let tm1 = list_mk_forall (yys, tm0) in
2718 let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2719 prove_by_refinement(tm2,
2723 MATCH_MP_TAC REAL_WLOG_ABB_SIMPLEX;
2725 REPEAT WEAKER_STRIP_TAC;
2726 INTRO_TAC delta_y_sym_cases2 yys;
2727 DISCH_THEN (unlist REWRITE_TAC);
2728 INTRO_TAC taum_sym_cases2 yys;
2729 DISCH_THEN (unlist REWRITE_TAC);
2730 INTRO_TAC edge2_flatD_x1_sym_cases yys;
2731 DISCH_THEN (unlist REWRITE_TAC);
2732 INTRO_TAC eulerA_x_sym_cases yys;
2733 DISCH_THEN (unlist REWRITE_TAC);
2734 INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2735 DISCH_THEN (unlist REWRITE_TAC);
2736 TYPIFY_GOAL_THEN `!f. f y1 y2 y6 + f y1 y3 y5 = f y1 y3 y5 + f y1 y2 y6` (unlist ONCE_REWRITE_TAC);
2738 BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
2740 MATCH_MP_TAC ineq_sym_s2_abb;
2741 INTRO_TAC (get_ineq(i,j,j)) yys;
2742 BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
2746 let r755_abb_list = map (fun (i,j) -> ((i,j),r755_abb i j)) [(0,1);(0,2);(0,3);(0,4);(1,2);(1,3);(1,4);
2747 (2,3);(2,4);(3,4)];;
2749 let get_ineq2( i, j, k) =
2750 let _ = (i <= j && j <= k) or failwith "get2 out of range" in
2751 if (i = j && j = k) then UNDISCH (assoc i r755_diag)
2752 else if (i = j) then UNDISCH (assoc (i,k) r755_aab_list)
2753 else if (j = k) then UNDISCH (assoc (i,j) r755_abb_list)
2754 else get_ineq'(i,j,k);;
2758 let (yys,tm) = (strip_forall (concl(get_ineq (i,j,j)))) in
2759 let tm0 = rhs(concl(REWRITE_CONV [ASSUME (`~(y5 < y6) /\ ~(y6 < y4)`)] tm)) in
2760 let tm1 = list_mk_forall (yys, tm0) in
2761 let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2766 (* let inq = (Main_estimate_ineq.make_hex_ear i j k).ineq in
2767 let inq' = concl(clean_ineq (ASSUME inq)) in
2769 let inq' = get_ineq_term (i,j,k) in
2770 let (yys,tm) = strip_forall inq' in
2771 let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME `(y5 < y6) <=> F`;ASSUME `(y6 < y4) <=> F`] tm)) in
2772 let tm1 = list_mk_forall (yys, tm0) in
2773 let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2776 let r755_ikj getter i j k = prove_by_refinement(
2780 REPEAT WEAKER_STRIP_TAC;
2781 INTRO_TAC ( (getter (i, k, j))) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2782 INTRO_TAC delta_y_sym_cases2 yys;
2783 DISCH_THEN (unlist REWRITE_TAC);
2784 INTRO_TAC taum_sym_cases2 yys;
2785 DISCH_THEN (unlist REWRITE_TAC);
2786 INTRO_TAC edge2_flatD_x1_sym_cases yys;
2787 DISCH_THEN (unlist REWRITE_TAC);
2788 INTRO_TAC eulerA_x_sym_cases yys;
2789 DISCH_THEN (unlist REWRITE_TAC);
2790 INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2791 DISCH_THEN (unlist REWRITE_TAC);
2792 REWRITE_TAC[REAL_ADD_AC];
2793 BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[])
2797 let rec cross a = function
2799 | b::bs -> (map (fun i -> (i,b)) a) @ cross a bs;;
2801 let triples = map (fun ((i,j),k)-> (i,j,k)) (cross (cross (0--4) (0--4)) (0--4));;
2804 let ls = map (fun (i,j,k) -> ((i,j,k),
2805 if (i > j or i > k) then TRUTH
2806 else if (j<= k) then get_ineq2 (i,j,k)
2807 else r755_ikj get_ineq2 i j k)) in
2810 let get_ineq3( i, j, k) =
2811 let _ = (i <= j && i <= k) or failwith (Printf.sprintf "get3 out of range %d %d %d" i j k) in
2812 repeat UNDISCH (assoc (i,j,k) r755_ikj_list);;
2814 let r755_jik i j k = prove_by_refinement(
2818 REPEAT WEAKER_STRIP_TAC;
2819 INTRO_TAC ( (get_ineq3 (j, i, k))) [`y3`;`y2`;`y1`;`y6`;`y5`;`y4`];
2820 INTRO_TAC delta_y_sym_cases2 yys;
2821 DISCH_THEN (unlist REWRITE_TAC);
2822 INTRO_TAC taum_sym_cases2 yys;
2823 DISCH_THEN (unlist REWRITE_TAC);
2824 INTRO_TAC edge2_flatD_x1_sym_cases yys;
2825 DISCH_THEN (unlist REWRITE_TAC);
2826 INTRO_TAC eulerA_x_sym_cases yys;
2827 DISCH_THEN (unlist REWRITE_TAC);
2828 INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2829 DISCH_THEN (unlist REWRITE_TAC);
2830 REWRITE_TAC[REAL_ADD_AC];
2831 BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[])
2836 let ls = map (fun (i,j,k) -> ((i,j,k),
2837 if (k < i && k < j) then TRUTH
2838 else if (i<= j) then get_ineq3 (i,j,k)
2839 else r755_jik i j k)) in
2842 let get_ineq4( i, j, k) =
2843 let thm = repeat UNDISCH (assoc (i,j,k) r755_jik_list) in
2844 let _ = (not(thm = TRUTH)) or failwith (Printf.sprintf "get4 out of range %d %d %d" i j k) in
2849 let ls = map (fun (i,j,k) -> ((i,j,k),
2850 if (k < i && k < j) then r755_ikj get_ineq4 i j k
2851 else get_ineq4 (i,j,k))) in
2852 let r755_ikj_list2 = ls triples in
2854 repeat UNDISCH (assoc (i,j,k) r755_ikj_list2);;
2857 let _ = (125 = List.length (filter (fun t -> not (snd t = TRUTH)) r755_ikj_list2));;
2860 let taud_mu_clauses = prove_by_refinement(
2861 `main_nonlinear_terminal_v11 ==> (!y2 y3 y4.
2862 (&2 <= y2 /\ y2 <= #2.52 /\ &2 <= y3 /\ y3 <= #2.52 /\ #3.01 <= y4 /\ y4 <= #3.915) ==>
2863 (let d = delta_y (&2) y2 y3 y4 (&2) (&2) in
2864 let t = taud (&2) y2 y3 y4 (&2) (&2) in
2865 ((&0 <= d /\ d <= &16 ==> -- sol0 <= t) /\
2866 (&16 <= d /\ d <= &100 ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2867 (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) -
2869 (&100 <= d ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2870 sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) -
2874 REWRITE_TAC[LET_DEF;LET_END_DEF];
2875 REPEAT WEAKER_STRIP_TAC;
2878 INTRO_TAC (taud_ge_flat_term) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`];
2880 BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
2881 BY(REWRITE_TAC[flat_term_2]);
2883 REPEAT WEAKER_STRIP_TAC;
2884 REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2];
2885 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2886 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2887 ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`];
2888 TYPED_ABBREV_TAC `d = delta_y (&2) y2 y3 y4 (&2) (&2)`;
2889 MATCH_MP_TAC (arith `m* a <= m * a' ==> m * a - s <= --s + a' * m`);
2890 GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
2892 REWRITE_TAC[Nonlin_def.mu_y];
2893 BY(ASM_TAC THEN REAL_ARITH_TAC);
2894 TYPIFY `&2 * &2 = sqrt(&16)` (C SUBGOAL_THEN SUBST1_TAC);
2895 MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
2897 TYPIFY `&14 = sqrt(&16) + sqrt(&100)` (C SUBGOAL_THEN SUBST1_TAC);
2898 TYPIFY `&4 = sqrt(&16) /\ &10 = sqrt(&100)` ENOUGH_TO_SHOW_TAC;
2901 MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
2903 MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
2905 MATCH_MP_TAC sqrt_secant_approx;
2906 BY(ASM_TAC THEN REAL_ARITH_TAC);
2907 COMMENT "final case";
2908 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2909 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2910 ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`];
2912 REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2];
2917 let terminal_hex_234_reduction = prove_by_refinement(
2918 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 f1 f2 b1 b2.
2919 (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915;
2922 #3.915; #3.01,y6, #3.915] in
2923 (ineq dom (f1 + flat_term
2925 (edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4 * y4) (&2 * &2)
2926 (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/
2927 delta_y #2.52 y2 y3 y4 (&2) (&2) > &0) \/ b2)) /\
2928 (ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\
2930 mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2931 sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) -
2932 sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y2 y3 y4 (&2) (&2) < &100 \/ b2)) /\
2933 (ineq dom (f1 + ( mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2934 (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) -
2935 sol0) + f2 > #0.712 \/
2936 b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &16 \/
2937 delta_y (&2) y2 y3 y4 (&2) (&2) > &100) \/ b2)) /\
2938 (ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/
2939 b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/
2940 delta_y (&2) y2 y3 y4 (&2) (&2) > &16) \/ b2))) ==>
2941 (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915;
2944 #3.915; #3.01,y6, #3.915;&2,y234,#2.52] ((f1 + taum y234 y2 y3 y4 (&2) (&2)) + f2 > #0.712 \/
2945 (delta_y y234 y2 y3 y4 (&2) (&2) < &0 \/ b1) \/ b2)))`,
2948 REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
2949 REPEAT WEAKER_STRIP_TAC;
2950 REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[];
2951 ASM_CASES_TAC `b1:bool`;
2952 BY(ASM_REWRITE_TAC[]);
2954 ASM_CASES_TAC `b2:bool`;
2955 BY(ASM_REWRITE_TAC[]);
2957 REWRITE_TAC[arith `f1 + t + f2 > #0.712 <=> t > #0.712 - f1 - f2`;arith `(f1 + t) + f2 > #0.712 <=> t > #0.712 - f1 - f2`];
2958 TYPED_ABBREV_TAC `c = #0.712 - f1 - f2`;
2959 REPEAT WEAKER_STRIP_TAC;
2960 ASM_CASES_TAC `&0 <= taum y234 y2 y3 y4 (&2) (&2)`;
2961 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2962 ASM_CASES_TAC `delta_y y234 y2 y3 y4 (&2) (&2) < &0`;
2963 BY(ASM_REWRITE_TAC[]);
2965 INTRO_TAC (UNDISCH taud_minimizer_terminal_hex_cases) [`y234`;`y2`;`y3`;`y4`];
2966 ASM_SIMP_TAC[arith `~(d < &0) ==> &0 <= d`;arith `~(&0 <= t) ==> t < &0`];
2968 BY(REWRITE_TAC[Sphere.h0] THEN ASM_TAC THEN REAL_ARITH_TAC);
2969 REPEAT WEAKER_STRIP_TAC;
2970 INTRO_TAC (UNDISCH OWZLKVY4) [`y234`;`y2`;`y3`;`y4`;`&2`;`&2`];
2972 BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
2974 FIRST_X_ASSUM DISJ_CASES_TAC;
2975 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
2976 INTRO_TAC (UNDISCH taud_mu_clauses) [`y2`;`y3`;`y4`];
2978 BY(ASM_REWRITE_TAC[]);
2979 REWRITE_TAC[LET_DEF;LET_END_DEF];
2980 BY(ASM_TAC THEN REAL_ARITH_TAC);
2981 REPEAT (FIRST_X_ASSUM_ST `mu_y` kill);
2982 INTRO_TAC taud_ge_flat_term [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2984 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2986 INTRO_TAC (UNDISCH edge2_flatD_x1_delta_lemma3) [`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2987 REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2989 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2991 FIRST_X_ASSUM_ST `sqrt` MP_TAC;
2993 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2994 ASM_SIMP_TAC [arith `&2 <= z1 ==> &0 <= z1`];
2995 INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2997 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2998 INTRO_TAC (UNDISCH delta_2_nn) [`z1`;`y2`;`y3`;`y4`];
3000 BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
3001 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.h0;arith `#2.52 = &2 * #1.26`] THEN REAL_ARITH_TAC)
3006 let get_spec i j k = ISPECL yys (get_ineq5(i,j,k)) in
3007 let aa i = get_spec i j k in
3008 let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
3009 GENL yys (MATCH_MP (rule (UNDISCH terminal_hex_234_reduction)) (end_itlist CONJ (map aa (0--4))));;
3012 let terminal_hex_25 = map (fun (j,k) -> mk_25 j k) (cross (0--4) (0--4));;
3015 let terminal_hex_126_reduction = prove_by_refinement(
3016 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 f1 f2 b1 b2.
3017 (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915;
3020 #3.915; #3.01,y6, #3.915;&2,y234,#2.52 ] in
3021 (ineq dom (f1 + flat_term
3023 (edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6 * y6) (&2 * &2)
3024 (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/
3025 delta_y #2.52 y1 y2 y6 (&2) (&2) > &0) \/ b2)) /\
3026 (ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\
3028 mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
3029 sqrt (delta_y (&2) y1 y2 y6 (&2) (&2)) -
3030 sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y1 y2 y6 (&2) (&2) < &100 \/ b2)) /\
3031 (ineq dom (f1 + ( mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
3032 (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &2 * &2) -
3033 sol0) + f2 > #0.712 \/
3034 b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &16 \/
3035 delta_y (&2) y1 y2 y6 (&2) (&2) > &100) \/ b2)) /\
3036 (ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/
3037 b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/
3038 delta_y (&2) y1 y2 y6 (&2) (&2) > &16) \/ b2))) ==>
3039 (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915;
3042 #3.915; #3.01,y6, #3.915;&2,y234,#2.52;&2,y126,#2.52] ((f1 + taum y126 y1 y2 y6 (&2) (&2)) + f2 > #0.712 \/
3043 (delta_y y126 y1 y2 y6 (&2) (&2) < &0 \/ b1) \/ b2)))`,
3046 REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
3047 REPEAT WEAKER_STRIP_TAC;
3048 REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[];
3049 ASM_CASES_TAC `b1:bool`;
3050 BY(ASM_REWRITE_TAC[]);
3052 ASM_CASES_TAC `b2:bool`;
3053 BY(ASM_REWRITE_TAC[]);
3055 REPEAT WEAKER_STRIP_TAC;
3056 INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y3`;`y1`;`y2`;`y6`;`y4`;`y5`;`y126`;`f1`;`f2`;`b1`;`b2`];
3057 BY(ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF])
3062 let yys' = yys @ [`y234:real`] in
3063 let get_spec j k = ISPECL (yys') (mk_25 j k) in
3064 let aa j = get_spec j k in
3065 let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
3066 GENL yys' (MATCH_MP (rule (UNDISCH terminal_hex_126_reduction)) (end_itlist CONJ (map aa (0--4))));;
3068 let terminal_hex_135_reduction = prove_by_refinement(
3069 `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 y135 f1 b1 b2.
3070 (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915;
3073 #3.915; #3.01,y6, #3.915;&2,y234,#2.52; &2,y126,#2.52 ] in
3074 (ineq dom (f1 + flat_term
3076 (edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5 * y5) (&2 * &2)
3077 (&2 * &2))) > #0.712 \/ b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/
3078 delta_y #2.52 y1 y3 y5 (&2) (&2) > &0) \/ b2)) /\
3079 (ineq dom (f1 + &0 > #0.712 \/ b1 \/ F \/ b2)) /\
3081 mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
3082 sqrt (delta_y (&2) y1 y3 y5 (&2) (&2)) -
3083 sol0) > #0.712 \/ b1 \/ delta_y (&2) y1 y3 y5 (&2) (&2) < &100 \/ b2)) /\
3084 (ineq dom (f1 + ( mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
3085 (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &2 * &2) -
3087 b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &16 \/
3088 delta_y (&2) y1 y3 y5 (&2) (&2) > &100) \/ b2)) /\
3089 (ineq dom (f1 + ( &0 - sol0) > #0.712 \/
3090 b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/
3091 delta_y (&2) y1 y3 y5 (&2) (&2) > &16) \/ b2))) ==>
3092 (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915;
3095 #3.915; #3.01,y6, #3.915;&2,y234,#2.52;&2,y126,#2.52;&2,y135,#2.52] ((f1 + taum y135 y1 y3 y5 (&2) (&2)) > #0.712 \/
3096 (delta_y y135 y1 y3 y5 (&2) (&2) < &0 \/ b1) \/ b2)))`,
3099 REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
3100 REPEAT WEAKER_STRIP_TAC;
3101 REPEAT (FIRST_X_ASSUM_ST `==>` MP_TAC) THEN ASM_REWRITE_TAC[];
3102 ASM_CASES_TAC `b1:bool`;
3103 BY(ASM_REWRITE_TAC[]);
3105 ASM_CASES_TAC `b2:bool`;
3106 BY(ASM_REWRITE_TAC[]);
3108 REPEAT WEAKER_STRIP_TAC;
3109 INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y2`;`y1`;`y3`;`y5`;`y4`;`y6`;`y135`;`f1`;`&0`;`b1`;`b2`];
3110 ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
3111 RULE_ASSUM_TAC (REWRITE_RULE[arith `a + &0 = a`]);
3112 BY(ASM_REWRITE_TAC[arith `a + &0 = a`])
3116 let terminal_hex_taum =
3117 let yys' = (yys @ [`y234:real`;`y126:real`]) in
3118 let aa k = ISPECL yys' (mk_5 k) in
3119 let rule1 = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
3120 let rule2 = REWRITE_RULE[REAL_ADD_AC] in
3121 GENL yys' (rule2(MATCH_MP (rule1 (UNDISCH terminal_hex_135_reduction)) (end_itlist CONJ (map aa (0--4)))));;