(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Main Estimate - Appendix - Terminal Cases                         *)
(* Chapter: Local Fan                                                         *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2013-05-10                                                           *)
(* ========================================================================== *)

(* Terminal Pent and Hex cases.  *)

(* pent with 5 top edges=2 *)




module Pent_hex = struct


  open Hales_tactic;;

(* eventually combine this with the one in Appendix. *)

(*
let pent_hex_get_main_nonlinear = 
  let is_main = function 
    | Main_estimate -> true
    | _ -> false in
  let has_main ind = 
    exists (is_main) ind.tags in
  let main_ineq_data1 = 
    filter has_main (!Ineq.ineqs) in
  let id = map (fun t-> t.idv) main_ineq_data1 in
  let main_ineq_data = map (fun t -> hd(Ineq.getexact t)) id in
  let ineql = map (fun ind -> ind.ineq) main_ineq_data in
  let sl = map (fun ind -> ind.idv) main_ineq_data in
  let main_ineq_conj = end_itlist (curry mk_conj) ineql in
  let th = new_definition (mk_eq (`main_nonlinear_terminal_v11:bool`,main_ineq_conj)) in
  let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in
  let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in
  let tryindex s sl = try index s sl with  _ -> report s; failwith s in
    fun s ->
      let i = tryindex s sl in
      let th2 = funpow i CONJUNCT2 th1 in
	co1 th2;;
*)


let UNDISCH2 = repeat UNDISCH;;

let yys = [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`];;


let sqrt_secant_approx = 
prove_by_refinement( `!x1 x2 x. &0 <= x1 /\ x1 <= x /\ x <= x2 ==> (&1 / (sqrt(x1) + sqrt(x2))) * (x - x1) + sqrt(x1) <= sqrt(x)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `x2 = &0`; TYPIFY `x1 = &0 /\ x = &0` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); TYPIFY `&0 < sqrt x2` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC SQRT_POS_LT; BY(ASM_TAC THEN REAL_ARITH_TAC); TYPIFY `&0 <= sqrt x1` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC SQRT_POS_LE; BY(ASM_TAC THEN REAL_ARITH_TAC); 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); Calc_derivative.CALC_ID_TAC; CONJ2_TAC; REWRITE_TAC[REAL_DIFFSQ]; REPEAT (GMATCH_SIMP_TAC Functional_equation.sqrt_sqrt); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[arith `x + y <= z <=> x <= &1 * (z - y)`]; MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL; CONJ2_TAC; REWRITE_TAC[arith `&0 <= x - y <=> y <= x`]; GMATCH_SIMP_TAC SQRT_MONO_LE_EQ; BY(ASM_TAC THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC REAL_LE_LDIV_EQ; CONJ2_TAC; REWRITE_TAC[arith `&1 * x = x`;arith `x + y <= z + y <=> x <= z`]; GMATCH_SIMP_TAC SQRT_MONO_LE_EQ; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let flat_term_neg = 
prove_by_refinement( `!y. y <= &2 * h0 ==> flat_term y <= &0`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.flat_term]; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[arith `a * b / c <= &0 <=> &0 <= a * (--b) / c `]; GMATCH_SIMP_TAC REAL_LE_MUL; GMATCH_SIMP_TAC REAL_LE_RDIV_EQ; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[Sphere.h0]; MP_TAC Flyspeck_constants.bounds; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let mu_y_ft_combine = 
prove_by_refinement( `!y y2 y3 sd. mu_y y y2 y3 * sd + flat_term y = mu_y (&2 * h0) y2 y3 * sd + (&1 - (&2 * h0 - &2) * #0.07 * sd / sol0) * flat_term y`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mu_y;Sphere.flat_term]; REPEAT WEAKER_STRIP_TAC; Calc_derivative.CALC_ID_TAC; MP_TAC Flyspeck_constants.bounds; REWRITE_TAC[Sphere.h0]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let mu_y_ft_combine2 = 
prove_by_refinement( `!y y2 y3. y <= &2 * h0 ==> mu_y (&2 * h0) y2 y3 * sqrt(&20) + #0.705 * flat_term y <= mu_y y y2 y3 * sqrt(&20) + flat_term y `,
(* {{{ proof *) [ REWRITE_TAC[mu_y_ft_combine]; REWRITE_TAC[arith `x + y <= x + z <=> y <= z`]; REPEAT WEAKER_STRIP_TAC; ONCE_REWRITE_TAC[arith `a * b = (-- a) * (-- b)`]; MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL; CONJ2_TAC; REWRITE_TAC[arith `&0 <= -- f <=> f <= &0`]; BY(ASM_SIMP_TAC[flat_term_neg]); REWRITE_TAC[arith `-- x <= -- (&1 - u) <=> &1 - x <= u`]; TYPIFY `#4.472135 <= sqrt(&20)` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC REAL_LE_RSQRT; BY(REAL_ARITH_TAC); TYPIFY `#0.551285 < sol0 /\ sol0 < #0.551286` (C SUBGOAL_THEN MP_TAC); BY(REWRITE_TAC[ Flyspeck_constants.bounds]); REWRITE_TAC[Sphere.h0]; REWRITE_TAC[arith `a * b * c /d = ((a * b) * c) / d`]; REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC REAL_LE_RDIV_EQ; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let nonfunctional_mu6_x = 
prove_by_refinement( `!x1 x2 x3 a b c. mu6_x x1 x2 x3 a b c = mu_y (sqrt x1) (sqrt x2) (sqrt x3)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mu6_x;Nonlin_def.mu_y;]; BY(Functional_equation.F_REWRITE_TAC) ]);;
(* }}} *)
let tau_x_tau_residual_x_general = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6. &4 <= x1 /\ sqrt(x1) <= &2 * h0 /\ &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\ delta_x4 x1 x2 x3 x4 x5 x6 < &0 /\ &0 < delta_x4 x2 x3 x1 x5 x6 x4 /\ &0 < delta_x4 x3 x1 x2 x6 x4 x5 /\ &0 <= delta_x x1 x2 x3 x4 x5 x6 ==> taum_x x1 x2 x3 x4 x5 x6 = sqrt(delta_x x1 x2 x3 x4 x5 x6) * tau_residual_x x1 x2 x3 x4 x5 x6 + flat_term_x x1`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[arith `&0 <= x <=> (&0 = x \/ &0 < x)`]; DISCH_THEN DISJ_CASES_TAC; 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]; ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`]; SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = &0` SUBST1_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC); SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = &0` SUBST1_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC); FIRST_X_ASSUM (fun t -> SUBST1_TAC (GSYM t)); REWRITE_TAC[arith `x * &0 = &0`;arith `&0 * x = &0`;SQRT_0]; ASM_SIMP_TAC[Merge_ineq.atn2_0;arith `(-- y < &0 <=> &0 < y) /\ ( &0 < -- y <=> y < &0)`]; REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;arith `pi/ &2 + pi/ &2 = pi /\ x + -- x = &0 /\ x * &0 = &0`]; REWRITE_TAC[Sphere.flat_term_x;Sphere.flat_term;Nonlinear_lemma.sol0_const1;Sphere.h0]; BY(REAL_ARITH_TAC); 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]; ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`]; REWRITE_TAC[Nonlin_def.tau_residual_x]; 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]; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `a + b + c - d = (a - d) + b + c`]; REWRITE_TAC[arith `a * (b + c) = a * b + a * c`]; ONCE_REWRITE_TAC[arith `(a + b + c) +d = (a + d) + b + c`]; BINOP_TAC; ASM_SIMP_TAC[Merge_ineq.dih_x_dih_x_div_sqrtdelta_negbranch]; REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;Sphere.flat_term;Sphere.flat_term_x;Nonlinear_lemma.sol0_const1;]; BY(REAL_ARITH_TAC); BINOP_TAC; ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`]; AP_TERM_TAC; GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch; ASM_REWRITE_TAC[]; SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC; BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC); BY(ASM_REWRITE_TAC[]); ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`]; AP_TERM_TAC; GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch; ASM_REWRITE_TAC[]; SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC; BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC); BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let OWZLKVY4 = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> ( !y1 y2 y3 y4 y5 y6. &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ cstab <= y4 /\ y4 <= #3.915 /\ y5 = &2 /\ y6 = &2 /\ &0 <= delta_y y1 y2 y3 y4 y5 y6 ==> taud y1 y2 y3 y4 y5 y6 <= taum y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `&80 <= delta_y y1 y2 y3 y4 y5 y6`; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2314572187") yys; REWRITE_TAC[Sphere.ineq;TAUT `(a ==> b==> c) <=> (a /\ b) ==> c `;TAUT `(a /\ b) /\ c <=> a /\ b /\ c`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC); ASM_SIMP_TAC[arith `n <= d ==> ~(d < n)`;arith `x > y <=> y < x`]; MATCH_MP_TAC (arith `u = v ==> (u < t ==> v <= t)`); MATCH_MP_TAC Functional_equation.taud_x_taud; BY(ASM_TAC THEN REAL_ARITH_TAC); RULE_ASSUM_TAC (REWRITE_RULE[arith `~(n <= d) <=> d < n`]); GMATCH_SIMP_TAC Terminal.taum_taum_x; CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab] THEN REAL_ARITH_TAC); REWRITE_TAC[Sphere.y_of_x]; GMATCH_SIMP_TAC tau_x_tau_residual_x_general; TYPIFY `&0 <= delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `&0 <= d` MP_TAC; BY(REWRITE_TAC[Sphere.delta_y] THEN REAL_ARITH_TAC); COMMENT "residue hypotheses";
CONJ_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ); INTRO_TAC (UNDISCH Terminal.EAR_DELTA_X4) yys; ANTS_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; DISCH_THEN (unlist REWRITE_TAC); REWRITE_TAC[arith `&4 = &2 * &2`]; REWRITE_TAC[ REAL_OF_NUM_LT]; GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; REWRITE_TAC[arith `0 < 2`]; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.delta_y;Sphere.h0;Appendix.cstab] THEN REAL_ARITH_TAC); REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term_x;Sphere.flat_term]; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[arith `v + u <= w + v <=> u <= w`]; REWRITE_TAC[GSYM Sphere.delta_y]; GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP; CONJ_TAC; GMATCH_SIMP_TAC SQRT_POS_LE; BY(ASM_REWRITE_TAC[Sphere.delta_y]); INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7796879304") yys; REWRITE_TAC[Sphere.ineq;Sphere.y_of_x]; REWRITE_TAC[TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab;Sphere.h0] THEN REAL_ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC) ]);; (* }}} *)
let OPEN_REAL_INTERVAL_SING = 
prove_by_refinement( `!a b c. ~(real_interval(a,b) = {c})`,
(* {{{ proof *) [ REWRITE_TAC[EXTENSION;IN_SING;IN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `a < b`; FIRST_ASSUM (C INTRO_TAC [`(a + b)/ &2`]); FIRST_X_ASSUM (C INTRO_TAC [`(&3 * a + &1 * b)/ &4`]); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); FIRST_X_ASSUM_ST `!` MP_TAC; DISCH_THEN (C INTRO_TAC [`c:real`]); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *) (* DERIVATIVES *) let diff tm rw x s = let cv rw t = rhs(concl (REWRITE_CONV rw t)) in let tm2 = cv rw tm in ( (REWRITE_RULE (map GSYM rw) (Calc_derivative.differentiate tm2 x s)));; let DERIVED_TAC ttac = fun gl -> let (_,[b;f;f';y;s]) = strip_comb (goal_concl gl) in ttac (Calc_derivative.differentiate f y s) gl;;
let derived_form_F = 
prove_by_refinement( `!f f' x s. derived_form F f f' x s`,
(* {{{ proof *) [ REWRITE_TAC[Calc_derivative.derived_form] ]);;
(* }}} *)
let derived_form_delta_y = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. derived_form T (\q. delta_y q y2 y3 y4 y5 y6) (y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1) y1 (:real) `,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.delta_y;Sphere.delta_x]; DERIVED_TAC MP_TAC; MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); REWRITE_TAC[Nonlin_def.delta_x1;Sphere.y_of_x]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let derived_form_delta_x = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6 .derived_form T (\q. delta_x q x2 x3 x4 x5 x6) (delta_x1 x1 x2 x3 x4 x5 x6) x1 (:real)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MP_TAC (diff `(\q. delta_x q x2 x3 x4 x5 x6)` [Sphere.delta_x] `x1:real` `(:real)`); MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); REWRITE_TAC[Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let derived_form_delta_x1 = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6. derived_form T (\q. delta_x1 q x2 x3 x4 x5 x6) ( -- &2 * x4) x1 (:real)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MP_TAC (diff `(\q. delta_x1 q x2 x3 x4 x5 x6)` [Nonlin_def.delta_x1] `x1:real` `(:real)`); MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); REWRITE_TAC[Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let deriv_form_taud = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. derived_form (&0 < delta_y y1 y2 y3 y4 y5 y6) (\q. taud q y2 y3 y4 y5 y6) ((-- #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 + (sol0 / (&2 * h0 - &2)) * sqrt(delta_y y1 y2 y3 y4 y5 y6))/ sqrt(delta_y y1 y2 y3 y4 y5 y6)) y1 (:real)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y]; DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`])); 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`]); REWRITE_TAC[derived_form_delta_y]; TYPIFY `~(&2 * h0 - &2 = &0)` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`; ASM_REWRITE_TAC[]; REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); Calc_derivative.CALC_ID_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `~(&2 = &0)`]; CONJ_TAC; GMATCH_SIMP_TAC SQRT_EQ_0; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`; TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`; TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a*a` (C SUBGOAL_THEN SUBST1_TAC); EXPAND_TAC "a";
GMATCH_SIMP_TAC (GSYM SQRT_MUL); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[GSYM Nonlin_def.mu_y]; TYPED_ABBREV_TAC `c = mu_y y1 y2 y3`; TYPED_ABBREV_TAC `d = (&2 * h0 - &2)`; TYPED_ABBREV_TAC `e = #0.07`; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[]; BY(REWRITE_TAC[Calc_derivative.derived_form]) ]);; (* }}} *) (* renamed from deriv_form_taud_ALT *)
let derived_form_taud_ALT = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 <= y1 /\ &0 <= y2 /\ &0 <= y3)) (\q. taud q y2 y3 y4 y5 y6) (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 / sqrt(delta_y y1 y2 y3 y4 y5 y6)) y1 (:real)`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `&0 <= y1 /\ &0 <= y2 /\ &0 <= y3`; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[GSYM Functional_equation.mu6_x_mu_y]; INTRO_TAC deriv_form_taud yys; ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`; ASM_REWRITE_TAC[]; MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); Calc_derivative.CALC_ID_TAC; SUBCONJ_TAC; BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); DISCH_TAC; REWRITE_TAC[GSYM Sphere.delta_y]; REWRITE_TAC[GSYM Sphere.y_of_x]; REWRITE_TAC[Sphere.h0]; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); BY(ASM_REWRITE_TAC[Calc_derivative.derived_form]); BY(ASM_REWRITE_TAC[Calc_derivative.derived_form]) ]);;
(* }}} *)
let deriv_form_taud_D2 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3)) (\q. (y_of_x taud_D1_num_x q y2 y3 y4 y5 y6 / sqrt(delta_y q y2 y3 y4 y5 y6))) (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)`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D2;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF]; REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV]; REPEAT WEAKER_STRIP_TAC; TYPIFY `(~(sqrt (delta_y y1 y2 y3 y4 y5 y6) = &0))` ((C SUBGOAL_THEN ASSUME_TAC)); GMATCH_SIMP_TAC SQRT_EQ_0; BY(ASM_TAC THEN REAL_ARITH_TAC); MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL; 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; CONJ2_TAC; TYPIFY `{q | &0 < q}` EXISTS_TAC; ASM_REWRITE_TAC[arith `!q. &0 < q <=> q > &0`;IN_ELIM_THM]; REWRITE_TAC[REAL_OPEN_HALFSPACE_GT]; REPEAT WEAKER_STRIP_TAC; REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); RULE_ASSUM_TAC(REWRITE_RULE[arith `y > &0 <=> &0 < y`]); GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_TAC THEN REAL_ARITH_TAC); 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)`]; REWRITE_TAC[WITHINREAL_UNIV]; DISCH_THEN ((unlist REWRITE_TAC) o GSYM); DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`])); ASM_REWRITE_TAC[GSYM Sphere.delta_y]; 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`]); REWRITE_TAC[derived_form_delta_y]; TYPIFY_GOAL_THEN `derived_form T (\q. mu_y q y2 y3) (-- #0.07) y1 (:real)` (unlist REWRITE_TAC); REWRITE_TAC[Nonlin_def.mu_y]; DERIVED_TAC MP_TAC; MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[]; 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); REWRITE_TAC[Nonlin_def.delta_x1]; DERIVED_TAC MP_TAC; MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); BY(REAL_ARITH_TAC); MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`); REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); REWRITE_TAC[GSYM Sphere.y_of_x]; TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`; TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; ASM_SIMP_TAC[arith `&0 < y ==> &0 <= y`]; TYPIFY `y_of_x mu6_x y1 y2 y3 y4 y5 y6 = mu_y y1 y2 y3` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[Sphere.y_of_x]; GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y); BY(ASM_TAC THEN REAL_ARITH_TAC); TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a * a` (C SUBGOAL_THEN SUBST1_TAC); EXPAND_TAC "a";
GMATCH_SIMP_TAC (GSYM SQRT_MUL); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_TAC THEN REAL_ARITH_TAC); Calc_derivative.CALC_ID_TAC; TYPIFY_GOAL_THEN `~(a = &0)` (unlist REWRITE_TAC); BY(ASM_REWRITE_TAC[]); BY(REAL_ARITH_TAC) ]);; (* }}} *) let thD3 = let th1 = (diff `((\q. (-- #0.07 * delta_y q y2 y3 y4 y5 y6 * (--(q * q) * y4 * y4 + (y2 * y2) * y5 * y5 - (y3 * y3) * y5 * y5 - (y2 * y2) * y6 * y6 + (y3 * y3) * y6 * y6 + (y4 * y4) * (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) * &2 * sqrt (q * q) - &1 / &4 * ( #0.012 + #0.07 * ( #2.52 - sqrt (q * q)) + #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) * ((--(q * q) * y4 * y4 + (y2 * y2) * y5 * y5 - (y3 * y3) * y5 * y5 - (y2 * y2) * y6 * y6 + (y3 * y3) * y6 * y6 + (y4 * y4) * (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) * &2 * sqrt (q * q)) pow 2 + &1 / &2 * ( #0.012 + #0.07 * ( #2.52 - sqrt (q * q)) + #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) * delta_y q y2 y3 y4 y5 y6 * (-- &8 * (q * q) * y4 * y4 + (--(q * q) * y4 * y4 + (y2 * y2) * y5 * y5 - (y3 * y3) * y5 * y5 - (y2 * y2) * y6 * y6 + (y3 * y3) * y6 * y6 + (y4 * y4) * (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) * &2)) / sqrt (delta_y q y2 y3 y4 y5 y6) pow 3)) ` [] `y1:real` `(:real)`) in let fr = frees (concl(GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] th1)) in let th2 = GENL fr th1 in let ddelta_y = `(y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1)` in let th3 = SPECL [ddelta_y;ddelta_y;ddelta_y] th2 in let th4 = REWRITE_RULE[derived_form_delta_y] th3 in let (h,[b;f;f';y;s]) = strip_comb (concl th4) in let tm = list_mk_comb (h,[b;f;`f':real`;y;s]) in GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] ( EXISTS (mk_exists (`f':real`,tm),f') th4);;
let derived_form_taud_D3 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. ?f'. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3)) (\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))) f' y1 (:real)`,
(* {{{ proof *) [ 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]; REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV]; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC thD3 yys; REPEAT WEAKER_STRIP_TAC; TYPIFY `f'` EXISTS_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[Calc_derivative.derived_form]; ANTS_TAC; TYPIFY_GOAL_THEN `&0 < y1 * y1` (unlist REWRITE_TAC); GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC SQRT_EQ_0; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[WITHINREAL_UNIV]) ]);;
(* }}} *)
let SECOND_DERIVATIVE_TEST = 
prove_by_refinement( `!f f' f'' z s. z IN s /\ real_open s /\ (!x. x IN s ==> (f has_real_derivative f' x) (atreal x)) /\ (!x. x IN s ==> (f' has_real_derivative f'' x) (atreal x)) /\ (f'' real_continuous atreal z) /\ (!x. x IN s ==> f z <= f x) ==> (f' z = &0 /\ &0 <= f'' z)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; SUBCONJ_TAC; INTRO_TAC REAL_DERIVATIVE_ZERO_MAXMIN [`f`;`f' z`;`z`;`s`]; DISCH_THEN MATCH_MP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; REWRITE_TAC[arith `&0 <= r <=> ~(r < &0)`]; DISCH_TAC; RULE_ASSUM_TAC(REWRITE_RULE[real_continuous_atreal]); FIRST_X_ASSUM_ST `abs` (C INTRO_TAC [`-- f'' z`]); ANTS_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `s' = s INTER {x | abs(x - z) < d}` ; TYPIFY `z IN s'` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "s'";
BY(ASM_REWRITE_TAC[IN_INTER;IN_ELIM_THM;arith `z - z = &0`;REAL_ABS_0]); TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "s'"; MATCH_MP_TAC REAL_OPEN_INTER; ASM_REWRITE_TAC[]; REWRITE_TAC[real_open;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `d - abs (x - z)` EXISTS_TAC; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); COMMENT "restrict to an interval"; TYPIFY `?a b. real_interval (a,b) SUBSET s' /\ z IN real_interval(a,b)` (C SUBGOAL_THEN MP_TAC); RULE_ASSUM_TAC(REWRITE_RULE[real_open]); FIRST_X_ASSUM (C INTRO_TAC [`z`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; GEXISTL_TAC [`z - e`;`z + e`]; REWRITE_TAC[SUBSET;IN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; INTRO_TAC REAL_OPEN_REAL_INTERVAL [`a`;`b`]; DISCH_TAC; TYPIFY `!x. x IN s' ==> f'' x < &0` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x`]); ANTS_TAC; FIRST_X_ASSUM MP_TAC; EXPAND_TAC "s'"; BY(REWRITE_TAC[IN_INTER;IN_ELIM_THM] THEN REAL_ARITH_TAC); BY(REAL_ARITH_TAC); INTRO_TAC Counting_spheres.REAL_CONVEX_ON_SECOND_SECANT [`(\x. -- f x)`;`(\x. -- f' x)`;`(\x. -- f'' x)`;`real_interval (a,b)`]; ANTS_TAC; REWRITE_TAC[IS_REALINTERVAL_INTERVAL;OPEN_REAL_INTERVAL_SING]; TYPIFY `!x. x IN real_interval(a,b) ==> x IN s` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_TAC THEN SET_TAC[]); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG; GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN; BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG; GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN; BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]); REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC (arith `f < &0 ==> &0 <= -- f`); FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); DISCH_TAC; TYPIFY `!x. x IN real_interval(a,b) ==> f x = f z` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x`;`z`]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `fz <= fx` (C INTRO_TAC [`x`]); ANTS_TAC; BY(ASM_TAC THEN SET_TAC[]); BY(REAL_ARITH_TAC); TYPIFY `!x. x IN real_interval (a,b) ==> (f has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL; TYPIFY `(\ (x:real). f z)` EXISTS_TAC; REWRITE_TAC[]; CONJ_TAC; BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]); TYPIFY `real_interval(a,b)` EXISTS_TAC; BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]); COMMENT "show f' is zero"; TYPIFY `!x. x IN real_interval(a,b) ==> (f' x = &0)` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL; GEXISTL_TAC [`f`;`x`]; ASM_SIMP_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); COMMENT "show f' has zero derivative"; TYPIFY `!x. x IN real_interval (a,b) ==> (f' has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL; TYPIFY `(\ (x:real). &0)` EXISTS_TAC; REWRITE_TAC[]; CONJ_TAC; BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]); TYPIFY `real_interval(a,b)` EXISTS_TAC; BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]); COMMENT "show f'' is zero"; TYPIFY `!x. x IN real_interval(a,b) ==> (f'' x = &0)` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL; GEXISTL_TAC [`f'`;`x`]; ASM_SIMP_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); FIRST_X_ASSUM (C INTRO_TAC [`z`]); ASM_REWRITE_TAC[]; REPLICATE_TAC 12 (FIRST_X_ASSUM kill); FIRST_X_ASSUM_ST `f'' z < &0` MP_TAC; BY(REAL_ARITH_TAC) ]);; (* }}} *) (* END OF DERIVATIVES *) (* CONTINUITY *)
let continuous_preimage_closed = 
prove_by_refinement( `!f s t. real_closed s /\ real_closed t /\ f real_continuous_on s ==> real_closed { x | x IN s /\ f x IN t }`,
(* {{{ proof *) [ REWRITE_TAC[real_continuous_on]; REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM DISJ_CASES_TAC; BY(ASM_MESON_TAC[]); TYPIFY `~(x IN s)` ASM_CASES_TAC; BY(ASM_MESON_TAC[]); FIRST_X_ASSUM (C INTRO_TAC [`x`]); RULE_ASSUM_TAC(REWRITE_RULE[TAUT `~ ~ x = x`]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM (C INTRO_TAC [`f x`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`e`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `d` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `(x' IN s)` ASM_CASES_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let continuous_preimage_open = 
prove_by_refinement( `!f s t. real_open s /\ real_open t /\ f real_continuous_on s ==> real_open { x | x IN s /\ f x IN t }`,
(* {{{ proof *) [ REWRITE_TAC[real_continuous_on]; REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x`]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM (C INTRO_TAC [`f x`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `x IN s ==> p` (C INTRO_TAC [`x`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `?` (C INTRO_TAC [`e`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `min d e'` EXISTS_TAC; CONJ_TAC; REWRITE_TAC[real_min]; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; SUBCONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC); DISCH_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let delta_y_continuous = 
prove_by_refinement( `!y2 y3 y4 y5 y6. (\q. delta_y q y2 y3 y4 y5 y6) real_continuous_on (:real)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT; REWRITE_TAC[REAL_OPEN_UNIV;IN_UNIV]; GEN_TAC; INTRO_TAC derived_form_delta_y [`x`;`y2`;`y3`;`y4`;`y5`;`y6`]; REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV]; DISCH_THEN (MP_TAC o (MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL)); BY(REWRITE_TAC[]) ]);;
(* }}} *)
let taud_continuous = 
prove_by_refinement( `!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}`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Nonlin_def.taud]; REWRITE_TAC[arith `!q. a * (q - b)/ r = (a * inv r) * q + a * (-- b) * inv r`]; REWRITE_TAC[arith `!q. a + b * (c - q) + d = (-- b) * q + (a + b*c + d)`]; 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))); CONJ_TAC; 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)`]; MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE; REWRITE_TAC[IMAGE;IN_ELIM_THM]; CONJ_TAC; MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET; TYPIFY `(:real)` EXISTS_TAC; REWRITE_TAC[delta_y_continuous;SUBSET;IN_UNIV]; INTRO_TAC delta_y_continuous [`y2`;`y3`;`y4`;`y5`;`y6`]; REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN]; DISCH_THEN MATCH_MP_TAC; BY(REWRITE_TAC[IN_UNIV]); TYPED_ABBREV_TAC `u = delta_y x y2 y3 y4 y5 y6` ; MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET; TYPIFY `{u | &0 <= u}` EXISTS_TAC; REWRITE_TAC[REAL_CONTINUOUS_WITHIN_SQRT_STRONG]; REWRITE_TAC[SUBSET;IN_ELIM_THM]; BY(MESON_TAC[]); 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)))) ]);;
(* }}} *)
let taud_minimizer = 
prove_by_refinement( `!a b d y2 y3 y4 y5 y6. (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in (&0 <= d /\ ~(s = {}) ==> (?z1. z1 IN s /\ (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6))))`,
(* {{{ proof *) [ REWRITE_TAC[LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC REAL_CONTINUOUS_ATTAINS_INF; ASM_REWRITE_TAC[]; CONJ2_TAC; MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET; TYPIFY `{q | &0 <= delta_y q y2 y3 y4 y5 y6}` EXISTS_TAC; REWRITE_TAC[taud_continuous]; REWRITE_TAC[SUBSET;IN_INTER;IN_ELIM_THM]; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[REAL_COMPACT_EQ_BOUNDED_CLOSED]; CONJ_TAC; MATCH_MP_TAC REAL_BOUNDED_SUBSET; TYPIFY `real_interval[a,b]` EXISTS_TAC; REWRITE_TAC[REAL_BOUNDED_REAL_INTERVAL]; BY(SET_TAC[]); MATCH_MP_TAC REAL_CLOSED_INTER; REWRITE_TAC[REAL_CLOSED_REAL_INTERVAL]; 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); BY(REWRITE_TAC[IN_UNIV;IN_ELIM_THM]); MATCH_MP_TAC continuous_preimage_closed; REWRITE_TAC[delta_y_continuous]; REWRITE_TAC[REAL_CLOSED_UNIV]; BY(REWRITE_TAC[arith `d <= t <=> t >= d`;REAL_CLOSED_HALFSPACE_GE]) ]);;
(* }}} *)
let taud_minimizer_cases = 
prove_by_refinement( `!a b d z1 y2 y3 y4 y5 y6. (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in (&0 <= d /\ &0 <= a /\ &0 <= y2 /\ &0 <= y3 /\ z1 IN s /\ (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6) ==> ( z1 = a \/ z1 = b \/ d = delta_y z1 y2 y3 y4 y5 y6 \/ (y_of_x taud_D1_num_x z1 y2 y3 y4 y5 y6 = &0 /\ &0 <= y_of_x taud_D2_num_x z1 y2 y3 y4 y5 y6) )))`,
(* {{{ proof *) [ REWRITE_TAC[LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; TYPIFY `z1 = a` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); TYPIFY `z1 = b` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); TYPIFY `d = delta_y z1 y2 y3 y4 y5 y6` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; TYPIFY `a < z1 /\ z1 < b /\ d < delta_y z1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC); RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL;IN_INTER;IN_ELIM_THM]); BY(ASM_TAC THEN REAL_ARITH_TAC); TYPED_ABBREV_TAC `s' = (real_interval (a,b) INTER {q | d < delta_y q y2 y3 y4 y5 y6})` ; TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC); 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); EXPAND_TAC "s'";
BY(REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INTER]); MATCH_MP_TAC continuous_preimage_open; REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]; CONJ_TAC; BY(REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith `d < t <=> t > d`]); MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET; TYPIFY `(:real)` EXISTS_TAC; REWRITE_TAC[delta_y_continuous]; BY(SET_TAC[]); 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'`]; ASM_REWRITE_TAC[]; COMMENT "big ants"; ANTS_TAC; SUBCONJ_TAC; EXPAND_TAC "s'"; REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL]; BY(ASM_REWRITE_TAC[]); DISCH_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; INTRO_TAC derived_form_taud_ALT [`x`;`y2`;`y3`;`y4`;`y5`;`y6`]; REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV]; ANTS_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MP_TAC; EXPAND_TAC "s'"; REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL]; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; INTRO_TAC deriv_form_taud_D2 [`x`;`y2`;`y3`;`y4`;`y5`;`y6`]; REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV]; ANTS_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MP_TAC; EXPAND_TAC "s'"; REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL]; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); CONJ2_TAC; EXPAND_TAC "s'"; REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL]; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); COMMENT "last ant"; MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL; INTRO_TAC derived_form_taud_D3 [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[Calc_derivative.derived_form]; ANTS_TAC; FIRST_X_ASSUM MP_TAC; EXPAND_TAC "s'"; REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL]; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[WITHINREAL_UNIV]; BY(MESON_TAC[]); COMMENT "down to 1"; REPEAT WEAKER_STRIP_TAC; TYPIFY `&0 < sqrt(delta_y z1 y2 y3 y4 y5 y6)` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC REAL_LT_RSQRT; BY(ASM_TAC THEN REAL_ARITH_TAC); CONJ_TAC; FIRST_X_ASSUM_ST `taud_D1_num_x` MP_TAC; REWRITE_TAC[REAL_DIV_EQ_0]; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); FIRST_X_ASSUM_ST `taud_D2_num_x` MP_TAC; GMATCH_SIMP_TAC REAL_LE_RDIV_EQ; CONJ_TAC; MATCH_MP_TAC REAL_POW_LT; BY(ASM_REWRITE_TAC[]); BY(REAL_ARITH_TAC) ]);; (* }}} *)
let taud_minimizer_terminal_pent_cases = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6. (let s = real_interval [&2,&2 * h0] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in (&0 <= d /\ y1 IN s /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ #3.01 <= y4 /\ y4 <= #3.237 /\ y5 = &2 /\ y6 = &2 ==> (?z1. z1 IN s /\ taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6 /\ ( z1 = &2 \/ z1 = &2 * h0 \/ d = delta_y z1 y2 y3 y4 y5 y6 \/ #0.12 <= taud z1 y2 y3 y4 y5 y6)))))`,
(* {{{ proof *) [ REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`d`;`y2`;`y3`;`y4`;`y5`;`y6`]; 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]; ANTS_TAC; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `z1` EXISTS_TAC; CONJ_TAC; BY(ASM_MESON_TAC[]); CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_MESON_TAC[]); INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`d`;`z1`;`y2`;`y3`;`y4`;`y5`;`y6`]; 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]; ANTS_TAC; BY(ASM_MESON_TAC[arith `&0 <= &2`;arith `&2 <= y ==> &0 <= y`]); ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC); ASM_CASES_TAC `z1 = &2 * h0` THEN FIRST_ASSUM (unlist REWRITE_TAC); ASM_CASES_TAC `d = delta_y z1 y2 y3 y4 y5 y6` THEN FIRST_ASSUM (unlist REWRITE_TAC); ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 y5 y6 < &20)`; REPEAT WEAKER_STRIP_TAC; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1347067436") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC (GSYM Functional_equation.taud_x_taud); CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REPLICATE_TAC 3(FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); COMMENT "second get";
DISCH_TAC; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "6601228004") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *)
let taud_mud_126_x = 
prove_by_refinement( `!y3' y4' y5' y1 y2 y3 y4 y5 y6. &0 <= y1 /\ &0 <= y2 ==> 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 `,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mud_126_x;Nonlin_def.taud;Sphere.flat_term;]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[Sphere.delta_126_x;GSYM Sphere.delta_y]; REPEAT WEAKER_STRIP_TAC; REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx); ASM_REWRITE_TAC[]; TYPIFY `delta_y y3 y1 y2 y6 y4 y5 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let taud_mud_135_x = 
prove_by_refinement( `!y2' y4' y6' y1 y2 y3 y4 y5 y6. &0 <= y1 /\ &0 <= y3 ==> 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 `,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.taud;Sphere.flat_term;]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[Sphere.delta_135_x;GSYM Sphere.delta_y]; REPEAT WEAKER_STRIP_TAC; REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx); ASM_REWRITE_TAC[]; TYPIFY `delta_y y2 y1 y3 y5 y4 y6 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let mud_126_135 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6 y3' y4' y5'. mud_126_x_v1 y3' y4' y5' y1 y2 y3 y4 y5 y6 = mud_135_x_v1 y3' y4' y5' y1 y3 y2 y4 y6 y5`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[Sphere.delta_135_x;Sphere.delta_126_x;GSYM Sphere.delta_y]; BY(MESON_TAC[Merge_ineq.delta_x_sym]); ]);;
(* }}} *)
let flat_term_2 = 
prove_by_refinement( `flat_term(&2) = -- sol0`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.flat_term]; Calc_derivative.CALC_ID_TAC; BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let flat_term_2h0 = 
prove_by_refinement( `flat_term(&2 * h0) = &0`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.flat_term]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let flat_term_sol0 = 
prove_by_refinement( `!y. &2 <= y ==> --sol0 <= flat_term y`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.flat_term]; REPEAT WEAKER_STRIP_TAC; TYPIFY `sol0 * (y - &2 * h0)/(&2 * h0 - &2) = -- sol0 + sol0 * (y - &2) / (&2 * h0 - &2)` (C SUBGOAL_THEN SUBST1_TAC); Calc_derivative.CALC_ID_TAC; BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); MATCH_MP_TAC (arith `&0 <= x ==> h <= h + x`); GMATCH_SIMP_TAC REAL_LE_MUL; GMATCH_SIMP_TAC REAL_LE_RDIV_EQ; MP_TAC Flyspeck_constants.bounds; BY(REWRITE_TAC[Sphere.h0] THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let taud_2h0 = 
prove_by_refinement( `!y2 y3 y4 y5 y6. &0 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 /\ y2 <= &2 * h0 /\ y3 <= &2 * h0 ==> &0 <= taud (&2 * h0) y2 y3 y4 y5 y6`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.taud;arith `x - x = &0 /\ &0 / x = &0 /\ x * &0 = &0 /\ &0 + x = x`]; REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC REAL_LE_MUL; CONJ_TAC; GMATCH_SIMP_TAC SQRT_POS_LE; BY(ASM_REWRITE_TAC[]); BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let quadratic_root_minus_works = 
prove_by_refinement( `!a b c. ~(a = &0) /\ &0 <= b pow 2 - &4 * a * c ==> (let x = -- ( b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a) in a * x pow 2 + b * x + c = &0)`,
(* {{{ proof *) [ REWRITE_TAC[LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; Calc_derivative.CALC_ID_TAC; ASM_REWRITE_TAC[arith `~(&2 = &0)`]; TYPED_ABBREV_TAC `d = b pow 2 - &4 * a * c`; TYPIFY `sqrt d * sqrt d = d` (C SUBGOAL_THEN MP_TAC); GMATCH_SIMP_TAC (GSYM SQRT_MUL); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_REWRITE_TAC[]); FIRST_X_ASSUM MP_TAC; BY(CONV_TAC REAL_RING) ]);;
(* }}} *)
let quadratic_root_imp_discr_nn = 
prove_by_refinement( `!a b c x. (a * x pow 2 + b * x + c = &0) ==> &0 <= b pow 2 - &4 * a * c`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `b pow 2 - &4 * a * c = (&2 * a * x + b ) pow 2` (C SUBGOAL_THEN SUBST1_TAC); FIRST_X_ASSUM MP_TAC; BY(CONV_TAC REAL_RING); BY(REWRITE_TAC[ REAL_LE_POW_2]) ]);;
(* }}} *)
let quadratic_root_plus_eq = 
prove_by_refinement( `!a b c m x. (&0 < a) /\ (m <= x) /\ a * x pow 2 + b * x + c = &0 /\ (&0 < &2 * m * a + b \/ (&2 * m * a + b) pow 2 < b pow 2 - &4 * a * c) ==> quadratic_root_plus (a,b,c) = x`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Tame_lemmas.quadratic_root_plus_gt_eq; TYPED_ABBREV_TAC `y = -- (b + sqrt( b pow 2 - &4 * a * c)) / (&2 * a)` ; TYPIFY `y` EXISTS_TAC; ASM_REWRITE_TAC[]; SUBCONJ_TAC; MATCH_MP_TAC quadratic_root_imp_discr_nn; BY(ASM_MESON_TAC[]); DISCH_TAC; CONJ_TAC; EXPAND_TAC "y";
MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] quadratic_root_minus_works); BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REAL_ARITH_TAC); COMMENT "both cases"; TYPIFY `y < m` ENOUGH_TO_SHOW_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); TYPIFY `&2 * a * y + b < &2 * a * m + b` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[arith `&2 * a * y + b < &2 * a * m + b <=> a * y < a * m`]; GMATCH_SIMP_TAC REAL_LT_LMUL_EQ; BY(ASM_REWRITE_TAC[]); TYPIFY `&2 * a * y + b = -- sqrt(b pow 2 - &4 * a *c)` (C SUBGOAL_THEN SUBST1_TAC); EXPAND_TAC "y"; Calc_derivative.CALC_ID_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "first case"; ASM_CASES_TAC `&0 < &2 * m * a + b`; MATCH_MP_TAC REAL_LET_TRANS; TYPIFY `&0` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `-- x <= &0 <=> &0 <= x`]; GMATCH_SIMP_TAC SQRT_POS_LE; BY(ASM_TAC THEN REAL_ARITH_TAC); FIRST_X_ASSUM DISJ_CASES_TAC; BY(ASM_MESON_TAC[]); TYPIFY `(&2 * m * a + b) pow 2 < sqrt (b pow 2 - &4 * a * c) pow 2` (C SUBGOAL_THEN MP_TAC); GMATCH_SIMP_TAC SQRT_POW_2; BY(ASM_REWRITE_TAC[]); TYPED_ABBREV_TAC `d = sqrt(b pow 2 - &4 * a * c) `; ONCE_REWRITE_TAC[arith `-- d < &2 * a * m + b <=> --d < &2 * m * a +b`]; REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]; TYPIFY `&0 <= d` (C SUBGOAL_THEN MP_TAC); EXPAND_TAC "d"; GMATCH_SIMP_TAC SQRT_POS_LE; BY(ASM_REWRITE_TAC[]); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *)
let edge2_flatD_x1_delta_lemma2 = 
prove_by_refinement( `!d x1 x2 x3 x4 x5 x6. delta_x x1 x2 x3 x4 x5 x6 = d /\ &0 < x4 /\ (delta_x1 x1 x2 x3 x4 x5 x6 < &0) ==> edge2_flatD_x1 d x2 x3 x4 x5 x6 = x1`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.edge2_flatD_x1]; REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`; TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`; TYPIFY `!z. d - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC)); EXPAND_TAC "c";
EXPAND_TAC "b"; REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[]; REWRITE_TAC[Nonlinear_lemma.abc_quadratic]; 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); EXPAND_TAC "b"; EXPAND_TAC "c"; REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x]; BY(REAL_ARITH_TAC); MATCH_MP_TAC quadratic_root_plus_eq; TYPIFY `x1` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `x <= x`]; CONJ_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x1`]); BY(ASM_TAC THEN REAL_ARITH_TAC); DISJ1_TAC; EXPAND_TAC "b"; FIRST_X_ASSUM_ST `d < &0` MP_TAC; REWRITE_TAC[Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC) ]);; (* }}} *)
let edge2_flatD_x1_delta_lemma3 = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6. delta_y y1 y2 y3 y4 y5 y6 = d /\ &0 <= d /\ d <= &20 ==> (ineq [(&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( edge2_flatD_x1 d (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6) = y1*y1)))`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC edge2_flatD_x1_delta_lemma2; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= &20 ==> ~(d > &20)`]; REWRITE_TAC[Sphere.y_of_x;arith `y1 pow 2 = y1 * y1`]; DISCH_THEN (unlist REWRITE_TAC); REWRITE_TAC[GSYM Sphere.delta_y]; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let delta_diff = 
prove_by_refinement( `!x1 z1 x2 x3 x4 x5 x6. delta_x x1 x2 x3 x4 x5 x6 = delta_x z1 x2 x3 x4 x5 x6 + delta_x1 x1 x2 x3 x4 x5 x6 * (x1 - z1) + x4 * (x1 - z1) pow 2`,
(* {{{ proof *) [ BY(REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let delta_2_nn = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!z1 y2 y3 y4. &2 <= z1 /\ z1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ #3.01 <= y4 /\ y4 <= #3.915 /\ delta_y z1 y2 y3 y4 (&2) (&2) = &0 ==> &0 <= delta_y (&2) y2 y3 y4 (&2) (&2)) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.delta_y]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH2 (Terminal.get_main_nonlinear "3078028960")) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); REWRITE_TAC[Sphere.y_of_x;Sphere.delta_y]; ASM_REWRITE_TAC[arith `~(&0 > &20)`]; DISCH_TAC; FIRST_X_ASSUM DISJ_CASES_TAC; INTRO_TAC delta_diff [`&2* &2`;`z1 * z1`;`y2*y2`;`y3*y3`;`y4*y4`;`&2* &2`;`&2 * &2`]; ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= &0 + x + y`); CONJ_TAC; ONCE_REWRITE_TAC[arith `&0 <= a * b <=> &0 <= (--a) *(--b)`]; GMATCH_SIMP_TAC REAL_LE_MUL; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); TYPIFY `&2 * &2 <= z1 * z1` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; BY(ASM_TAC THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC REAL_LE_MUL; REWRITE_TAC[ REAL_LE_POW_2]; BY(REWRITE_TAC[ REAL_LE_SQUARE]); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let delta_mono = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6. &2 <= y1 /\ y1 <= z1 /\ z1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ #3.01 <= y4 /\ y4 <= #3.915 /\ &2 <= y5 /\ y5 <= &2 /\ &2 <= y6 /\ y6 <= &2 /\ &0 <= delta_y y1 y2 y3 y4 y5 y6 /\ delta_y y1 y2 y3 y4 y5 y6 <= &20 ==> delta_y z1 y2 y3 y4 y5 y6 <= delta_y y1 y2 y3 y4 y5 y6) `,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.delta_y]; INTRO_TAC delta_diff [`y1*y1`;`z1*z1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`]; DISCH_THEN SUBST1_TAC; MATCH_MP_TAC (arith `&0 <= b /\ &0 <= c ==> a <= a + b + c`); CONJ2_TAC; GMATCH_SIMP_TAC REAL_LE_MUL; REWRITE_TAC[ REAL_LE_POW_2]; BY(REWRITE_TAC[ REAL_LE_SQUARE]); INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= d1 ==> ~(d > d1)`]; REWRITE_TAC[Sphere.y_of_x]; ONCE_REWRITE_TAC[arith `&0 <= x * y <=> &0 <= (-- x) * (-- y)`]; DISCH_TAC; GMATCH_SIMP_TAC REAL_LE_MUL; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); MATCH_MP_TAC (arith `y1 * y1 <= z1 * z1 ==> &0 <= -- (y1 * y1 - z1 * z1)`); GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let flat_term2_126_x_eval = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6. delta_y z y1 y2 y6 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\ &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ #3.01 <= y6 /\ y6 <= #3.915 ==> y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_126_x;Nonlin_def.edge2_126_x]; REWRITE_TAC[Functional_equation.uni;Functional_equation.compose6;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y2`;`y6`;`&2`;`&2`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); REWRITE_TAC[arith `&2 * &2 = &4`]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[Sphere.flat_term_x]; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let flat_term2_135_x_eval = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6. delta_y z y1 y3 y5 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\ &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ #3.01 <= y5 /\ y5 <= #3.915 ==> y_of_x (flat_term2_135_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.edge2_135_x]; 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]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y3`;`y5`;`&2`;`&2`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); REWRITE_TAC[arith `&2 * &2 = &4`]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[Sphere.flat_term_x]; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let delta_126_135 = 
prove_by_refinement( `!a b c y1 y2 y3 y4 y5 y6. delta_126_x a b c y1 y2 y3 y4 y5 y6 = delta_135_x a b c y1 y3 y2 y4 y6 y5`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.delta_126_x;Sphere.delta_135_x]; BY(MESON_TAC[Merge_ineq.delta_x_sym]) ]);;
(* }}} *)
let delta_126_x_2h0_le_d = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6. &2 <= z1 /\ z1 <= &2 * h0 /\ z1 <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ #3.01 <= y6 /\ y6 <= #3.915 /\ &0 <= d /\ d <= &20 /\ delta_y z1 y1 y2 y6 (&2) (&2) = d ==> y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x]; REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`]; REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y]; TYPIFY `delta_y y1 y2 (&2 * h0) (&2) (&2) y6 = delta_y (&2 * h0) y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y2`;`y6`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let delta_135_x_2h0_le_d = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6. &2 <= z1 /\ z1 <= &2 * h0 /\ z1 <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ #3.01 <= y5 /\ y5 <= #3.915 /\ &0 <= d /\ d <= &20 /\ delta_y z1 y1 y3 y5 (&2) (&2) = d ==> y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.y_of_x;Sphere.delta_135_x]; REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`]; REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y]; TYPIFY `delta_y y1 (&2 * h0) y3 (&2) y5 (&2) = delta_y (&2 * h0) y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Merge_ineq.delta_y_sym]); INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let lemma_5546286427 = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6. ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,z1,#2.52) ] ( &0 = delta_y z1 y1 y2 y6 (&2) (&2) ==> (taum y1 y2 y3 y4 y5 y6 + flat_term z1 + #0.12 > #0.616)))`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5546286427") yys; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC flat_term2_126_x_eval; TYPIFY `z1` EXISTS_TAC; CONJ_TAC; BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); COMMENT "remove delta_126_x";
DISCH_THEN DISJ_CASES_TAC; BY(ASM_REWRITE_TAC[]); INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *)
let taud_ge_flat_term = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 /\ y2 <= &2 * h0 /\ y3 <= &2 * h0 /\ &0 <= delta_y y1 y2 y3 y4 y5 y6 ==> flat_term y1 <= taud y1 y2 y3 y4 y5 y6`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term]; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[arith `a <= a + b <=> &0 <= b`]; GMATCH_SIMP_TAC REAL_LE_MUL; GMATCH_SIMP_TAC SQRT_POS_LE; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let terminal_pent_taum126_012 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135. #0.12 <= taud y126 y1 y2 y6 (&2) (&2) /\ &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==> (ineq [ (&2,y1,&2 * h0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,y126,&2 * h0); (&2,y135,&2 * h0) ] (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2)))) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`]; REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); REWRITE_TAC[arith `x > y <=> y < x`]; DISCH_TAC; INTRO_TAC (UNDISCH OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(REWRITE_TAC[Sphere.cstab] THEN ASM_TAC THEN REAL_ARITH_TAC); DISCH_TAC; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); DISCH_TAC; COMMENT "case y=2";
FIRST_X_ASSUM (DISJ_CASES_TAC); INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7903347843") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); REWRITE_TAC[Sphere.y_of_x;mud_126_135]; REWRITE_TAC[GSYM Sphere.y_of_x]; TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Terminal.taum_sym]); GMATCH_SIMP_TAC taud_mud_135_x; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); MATCH_MP_TAC (arith `x <= a + b ==> t + x > #0.616 ==> #0.616 < a + t + b`); MATCH_MP_TAC (arith `t2 <= t135 /\ -- s <= f /\ #0.12 <= t126 ==> t2 - f - s + #0.12 <= t126+t135`); ASM_REWRITE_TAC[]; CONJ_TAC; FIRST_X_ASSUM_ST `<=` MP_TAC THEN ASM_REWRITE_TAC[]; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); MATCH_MP_TAC flat_term_sol0; BY(REAL_ARITH_TAC); COMMENT "case &0 <= tau"; ASM_CASES_TAC `&0 <= taud y135 y1 y3 y5 (&2) (&2)`; BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "case y=&2*h0"; FIRST_X_ASSUM (DISJ_CASES_TAC); INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); COMMENT "case delta=0"; FIRST_X_ASSUM DISJ_CASES_TAC; INTRO_TAC (UNDISCH lemma_5546286427) [`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[Terminal.taum_sym]); DISCH_TAC; INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "final case"; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *)
let terminal_pent_tau135_012 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135. #0.12 <= taud y135 y1 y3 y5 (&2) (&2) /\ &0 <= delta_y y126 y1 y2 y6 (&2) (&2) ==> (ineq [ (&2,y1,&2 * h0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,y126,&2 * h0); (&2,y135,&2 * h0) ] (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2)))) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`]; ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(REWRITE_TAC[Terminal.taum_sym]); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let sqrt20 = 
prove_by_refinement( `#4.47 <= sqrt(&20)`,
(* {{{ proof *) [ MATCH_MP_TAC REAL_LE_RSQRT; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let taud_053 = 
prove_by_refinement( `! y2 y3 y4 y5 y6. y2 <= &2 * h0 /\ y3 <= &2 * h0 /\ &20 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 ==> #0.053 <= taud (&2 * h0) y2 y3 y4 y5 y6`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.taud]; REPEAT WEAKER_STRIP_TAC; TYPIFY `sol0 * (&2 * h0 - &2 * h0) / (&2 * h0 - &2) = &0` (C SUBGOAL_THEN SUBST1_TAC); BY(REAL_ARITH_TAC); TYPIFY `#0.053 = #4.47 * (#0.053 / #4.47)` (C SUBGOAL_THEN SUBST1_TAC); BY(REAL_ARITH_TAC); REWRITE_TAC[arith `&0 + x= x`]; MATCH_MP_TAC REAL_LE_MUL2; CONJ_TAC; BY(REAL_ARITH_TAC); CONJ_TAC; MATCH_MP_TAC REAL_LE_TRANS; TYPIFY `sqrt(&20)` EXISTS_TAC; REWRITE_TAC[sqrt20]; GMATCH_SIMP_TAC SQRT_MONO_LE_EQ; BY(ASM_TAC THEN REAL_ARITH_TAC); CONJ_TAC; BY(REAL_ARITH_TAC); BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let terminal_pent_tau126_2 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135. y126 = &2 /\ &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\ &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==> (ineq [ (&2,y1,&2 * h0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,y126,&2 * h0); (&2,y135,&2 * h0) ] (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2)))) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`]; REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC); BY(MESON_TAC[Terminal.taum_sym]); COMMENT "case tau >= 0.12";
ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); COMMENT "case z1= &2"; ASM_CASES_TAC `z1 = &2`; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7997589055") yys; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC taud_mud_126_x; GMATCH_SIMP_TAC taud_mud_135_x; REWRITE_TAC[flat_term_2]; TYPIFY_GOAL_THEN ` &0 <= y1 /\ &0 <= y2 /\ &0 <= y3` (unlist REWRITE_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `x = &2` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "case delta=0"; ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2565248885") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`]; GMATCH_SIMP_TAC (UNDISCH2 delta_126_x_2h0_le_d); CONJ_TAC; TYPIFY `z1` EXISTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC taud_mud_135_x; REWRITE_TAC[flat_term_2]; GMATCH_SIMP_TAC (UNDISCH2 flat_term2_126_x_eval); TYPIFY `z1` EXISTS_TAC; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); COMMENT "case delta>=20"; TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC); BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]); DISCH_TAC; ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2320951108") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC taud_mud_135_x; REWRITE_TAC[flat_term_2]; INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; FIRST_X_ASSUM MP_TAC; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); DISCH_TAC; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC); BY(REAL_ARITH_TAC); COMMENT "case delta <= 20"; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5429238960") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC taud_mud_135_x; REWRITE_TAC[flat_term_2]; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_TAC THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC) ]);; (* }}} *)
let terminal_pent_tau135_2 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135. y135 = &2 /\ &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\ &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==> (ineq [ (&2,y1,&2 * h0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,y126,&2 * h0); (&2,y135,&2 * h0) ] (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2)))) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`]; ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC); BY(REWRITE_TAC[Terminal.taum_sym]); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let terminal_pent_tau126_2h0 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135. y126 = &2 * h0 /\ &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\ &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==> (ineq [ (&2,y1,&2 * h0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,y126,&2 * h0); (&2,y135,&2 * h0) ] (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2)))) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`]; REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC); BY(MESON_TAC[Terminal.taum_sym]); COMMENT "case tau >= 0.12";
ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); COMMENT "case z1= &2"; ASM_CASES_TAC `z1 = &2`; INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "case delta = 0"; ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1948775510") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC (taud_mud_135_x); CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[flat_term_2h0]; GMATCH_SIMP_TAC flat_term2_126_x_eval; TYPIFY `z1` EXISTS_TAC; CONJ_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC); INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`] THEN DISCH_THEN (unlist REWRITE_TAC); REWRITE_TAC[Sphere.delta_135_x;Sphere.y_of_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`]; REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y]; TYPIFY `delta_y y1 (&2 * h0) y2 (&2) y6 (&2) = delta_y y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC); ASM_REWRITE_TAC[]; BY(MESON_TAC[Merge_ineq.delta_y_sym]); FIRST_X_ASSUM kill; ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "case z1=2h0, delta>=20"; TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC); BY(ASM_MESON_TAC[]); DISCH_TAC; INTRO_TAC taud_053 [`y1`;`y2`;`y6`;`&2`;`&2`]; ANTS_TAC; ASM_REWRITE_TAC[]; BY(FIRST_X_ASSUM_ST `&20 <= d` MP_TAC THEN ASM_REWRITE_TAC[]); DISCH_TAC; ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; ASM_REWRITE_TAC[]; BY(REPEAT (FIRST_X_ASSUM_ST `&20 <= d` MP_TAC) THEN ASM_REWRITE_TAC[]); DISCH_TAC; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); COMMENT "case z1=2h0, delta<=20"; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5708641738") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN ASM_MESON_TAC[]); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *)
let taud_sqrt20 = 
prove_by_refinement( ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6. &0 <= &20 /\ &20 <= &20 /\ &2 <= z1 /\ z1 <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ #3.01 <= y5 /\ y5 <= #3.915 /\ delta_y z1 y1 y3 y5 (&2) (&2) = &20 ==> y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 + (#0.012 + #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 <= taud z1 y1 y3 y5 (&2) (&2))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC flat_term2_135_x_eval; TYPIFY `z1` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term]; REWRITE_TAC[ (arith `u + c * s <= u + s' * c' <=> c * s <= c' * s'`)]; MATCH_MP_TAC REAL_LE_MUL2; CONJ_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[sqrt20]; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let terminal_pent_tau126_delta20 = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135. delta_y y126 y1 y2 y6 (&2) (&2) = &20 /\ &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==> (ineq [ (&2,y1,&2 * h0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,y126,&2 * h0); (&2,y135,&2 * h0) ] (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2)))) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`]; REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC); BY(MESON_TAC[Terminal.taum_sym]); COMMENT "case tau >= 0.12";
ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); COMMENT "case z1= &2"; ASM_CASES_TAC `z1 = &2`; INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "delta issue"; TYPIFY `~( y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y3 y2 y4 y6 y5 > &20 )` (C SUBGOAL_THEN MP_TAC); REWRITE_TAC[arith `~(x > d) <=> (x<=d)`]; GMATCH_SIMP_TAC delta_135_x_2h0_le_d; TYPIFY `y126` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC); DISCH_TAC; COMMENT "case delta = 0"; ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1008824382") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC flat_term2_126_x_eval; TYPIFY `z1` EXISTS_TAC; CONJ_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC flat_term2_135_x_eval; TYPIFY `y126` EXISTS_TAC; CONJ_TAC; FIRST_X_ASSUM_ST `d = &20` SUBST1_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC); INTRO_TAC mu_y_ft_combine2 [`y126`;`y1`;`y2`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); TYPIFY `mu_y y126 y1 y2 * sqrt(&20) + flat_term y126 <= taud y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN MP_TAC); REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y;Sphere.flat_term]; REWRITE_TAC[ (arith `c * s + u <= u + s' * c <=> c * s <= c * s'`)]; GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP; CONJ_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC SQRT_MONO_LE_EQ; BY(ASM_TAC THEN REAL_ARITH_TAC); 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); REWRITE_TAC[Nonlin_def.mu_y]; MATCH_MP_TAC REAL_LE_MUL2; CONJ_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); REWRITE_TAC[sqrt20]; BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); FIRST_X_ASSUM_ST `~` (unlist REWRITE_TAC); REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`]; GMATCH_SIMP_TAC delta_126_x_2h0_le_d; CONJ_TAC; TYPIFY `z1` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); REWRITE_TAC[flat_term_2h0]; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); COMMENT "z1=2h0 and delta <=20"; TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]); ASM_CASES_TAC `delta_y z1 y1 y3 y5 (&2) (&2) <= &20`; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1586903463") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `<=` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC); INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`]; REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y]; TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC); ASM_REWRITE_TAC[]; BY(MESON_TAC[Merge_ineq.delta_y_sym]); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "z1=2h0 and delta> 20"; INTRO_TAC ((*--*)Terminal.get_main_nonlinear "8875146520") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); GMATCH_SIMP_TAC taud_mud_126_x; REWRITE_TAC[flat_term_2h0]; INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); FIRST_X_ASSUM_ST `y_of_x` (unlist REWRITE_TAC); REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`]; REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y]; TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC); ASM_REWRITE_TAC[]; BY(MESON_TAC[Merge_ineq.delta_y_sym]); ASM_REWRITE_TAC[]; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *)
let terminal_pent_taum = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135. &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\ &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==> (ineq [ (&2,y1,&2 * h0); (&2,y2,&2 * h0); (&2,y3,&2 * h0); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237); (&2,y126,&2 * h0); (&2,y135,&2 * h0) ] (#0.616 < taum y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taum y135 y1 y3 y5 (&2) (&2)))) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&20`;`y126`;`y1`;`y2`;`y6`;`(&2)`;`&2`]; REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM]; ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH2 OWZLKVY4) [`y126`;`y1`;`y2`;`y6`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC); INTRO_TAC (UNDISCH2 OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC); 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; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); COMMENT "case z1=2";
FIRST_X_ASSUM DISJ_CASES_TAC; INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); COMMENT "case z1=2h0"; FIRST_X_ASSUM DISJ_CASES_TAC; INTRO_TAC (UNDISCH2 terminal_pent_tau126_2h0) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); COMMENT "case delta=20"; FIRST_X_ASSUM DISJ_CASES_TAC; INTRO_TAC (UNDISCH2 terminal_pent_tau126_delta20) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); COMMENT "case tau012"; INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]) ]);; (* }}} *) (* HEXAGON SECTION terminal_hex *)
let taud_minimizer_terminal_hex_cases = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4. (&0 <= delta_y y1 y2 y3 y4 (&2) (&2) /\ &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ #3.01 <= y4 /\ y4 <= #3.915 /\ taum y1 y2 y3 y4 (&2) (&2) < &0 ==> (?z1. &0 <= delta_y z1 y2 y3 y4 (&2) (&2) /\ &2 <= z1 /\ z1 <= &2 * h0 /\ taud z1 y2 y3 y4 (&2) (&2) <= taud y1 y2 y3 y4 (&2) (&2) /\ ( z1 = &2 \/ &0 = delta_y z1 y2 y3 y4 (&2) (&2) ))))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`&0`;`y2`;`y3`;`y4`;`&2`;`&2`]; 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]; ANTS_TAC; REWRITE_TAC[arith `&0 <= &0`;NOT_FORALL_THM]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `z1` EXISTS_TAC; ASM_REWRITE_TAC[]; CONJ_TAC; REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE))); BY(ASM_MESON_TAC[]); INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`]; 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]; ANTS_TAC; BY(ASM_MESON_TAC[arith `&0 <= &2 /\ &0 <= &0`;arith `&2 <= y ==> &0 <= y`]); ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC); ASM_CASES_TAC `&0 = delta_y z1 y2 y3 y4 (&2) (&2)` THEN FIRST_ASSUM (unlist ASM_REWRITE_TAC); ASM_CASES_TAC `z1 = &2 * h0` THEN ASM_REWRITE_TAC[]; INTRO_TAC (UNDISCH OWZLKVY4 ) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC); FIRST_X_ASSUM (C INTRO_TAC [`y1`]); ANTS_TAC; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `taum` MP_TAC; INTRO_TAC taud_2h0 [`y2`;`y3`;`y4`;`&2`;`&2`]; ANTS_TAC; BY(ASM_MESON_TAC[]); BY(REAL_ARITH_TAC); COMMENT "derviative cases";
ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 (&2) (&2) < &15)`; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (Terminal.get_main_nonlinear "6877738680") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Functional_equation.taud_x_taud; INTRO_TAC (UNDISCH OWZLKVY4) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`]; ANTS_TAC; BY(ASM_REWRITE_TAC[Sphere.cstab]); FIRST_X_ASSUM (C INTRO_TAC [`y1`]); ANTS_TAC; BY(ASM_REWRITE_TAC[]); BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); INTRO_TAC (Terminal.get_main_nonlinear "9692636487") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM_ST `delta_y` MP_TAC) THEN REAL_ARITH_TAC) ]);; (* }}} *) (* next, de-symmetrize everything, then combine delta ranges. *)
let REAL_WLOG_S3_SIMPLEX = 
prove_by_refinement( `!(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 /\ P y1 y2 y3 y4 y5 y6 = P y2 y1 y3 y5 y4 y6) /\ (!y1 y2 y3 y4 y5 y6. y4 <= y6 /\ y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==> (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; 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); BY(REAL_ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[]) ]);;
(* }}} *)
let REAL_WLOG_AAB_SIMPLEX = 
prove_by_refinement( `!(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) /\ (!y1 y2 y3 y4 y5 y6. y4 <= y6 ==> P y1 y2 y3 y4 y5 y6) ==> (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; TYPIFY `(y4 <= y6 \/ y6 <= y4)` (C SUBGOAL_THEN ASSUME_TAC); BY(REAL_ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[]) ]);;
(* }}} *)
let REAL_WLOG_ABB_SIMPLEX = 
prove_by_refinement( `!(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) /\ (!y1 y2 y3 y4 y5 y6. y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==> (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; TYPIFY `(y5 <= y6 \/ y6 <= y5)` (C SUBGOAL_THEN ASSUME_TAC); BY(REAL_ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[]) ]);;
(* }}} *)
let delta_y_hex_cases = 
prove_by_refinement( `!y1 y2 y3 y5 y6 a b. (delta_y y1 y2 a (&2) (&2) y6 = delta_y a y1 y2 y6 (&2) (&2) /\ (delta_y y1 b y3 (&2) y5 (&2) = delta_y b y1 y3 y5 (&2) (&2)))`,
(* {{{ proof *) [ BY(MESON_TAC[Merge_ineq.delta_y_sym]) ]);;
(* }}} *)
let delta_y_sym_cases2 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6 a. delta_y a y3 y1 y5 (&2) (&2) = delta_y a y1 y3 y5 (&2) (&2) /\ delta_y a y3 y2 y4 (&2) (&2) = delta_y a y2 y3 y4 (&2) (&2) /\ delta_y a y2 y1 y6 (&2) (&2) = delta_y a y1 y2 y6 (&2) (&2)`,
(* {{{ proof *) [ BY(MESON_TAC[Merge_ineq.delta_y_sym]) ]);;
(* }}} *)
let taum_sym_cases2 = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. taum y2 y1 y3 y5 y4 y6 = taum y1 y2 y3 y4 y5 y6 /\ taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6 /\ taum y3 y1 y2 y6 y4 y5 = taum y1 y2 y3 y4 y5 y6 /\ taum y3 y2 y1 y6 y5 y4 = taum y1 y2 y3 y4 y5 y6`,
(* {{{ proof *) [ BY(MESON_TAC[Terminal.taum_sym]) ]);;
(* }}} *)
let edge2_flatD_sym = 
prove_by_refinement( `!d y1 y2 y3 a. edge2_flatD_x1 d y1 y2 y3 a a = edge2_flatD_x1 d y2 y1 y3 a a`,
(* {{{ proof *) [ BY(REWRITE_TAC[Nonlin_def.edge2_flatD_x1;Merge_ineq.delta_x_sym]) ]);;
(* }}} *)
let edge2_flatD_x1_sym_cases = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. edge2_flatD_x1 (&0) (y3 * y3) (y2 * y2) (y4*y4) (&2 * &2) (&2* &2) = edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4*y4) (&2 * &2) (&2* &2) /\ edge2_flatD_x1 (&0) (y3 * y3) (y1 * y1) (y5*y5) (&2 * &2) (&2* &2) = edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5*y5) (&2 * &2) (&2* &2) /\ edge2_flatD_x1 (&0) (y2 * y2) (y1 * y1) (y6*y6) (&2 * &2) (&2* &2) = edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6*y6) (&2 * &2) (&2* &2) `,
(* {{{ proof *) [ BY(REWRITE_TAC[edge2_flatD_sym]) ]);;
(* }}} *)
let eulerA_x_sym_cases = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. eulerA_x (y2 * y2) (y1 * y1) (y3 * y3) (y5 * y5) (y4 * y4) (y6 * y6) = eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) /\ eulerA_x (y3 * y3) (y1 * y1) (y2 * y2) (y6 * y6) (y4 * y4) (y5 * y5) = eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) /\ eulerA_x (y3 * y3) (y2 * y2) (y1 * y1) (y6 * y6) (y5 * y5) (y4 * y4) = eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) /\ eulerA_x (y1 * y1) (y3 * y3) (y2 * y2) (y4 * y4) (y6 * y6) (y5 * y5) = eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) `,
(* {{{ proof *) [ REWRITE_TAC[Sphere.eulerA_x]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let mu_y_sym = 
prove_by_refinement( `!y1 y2 y3. mu_y y1 y2 y3 = mu_y y1 y3 y2`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mu_y]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let mu_y_sym_cases = 
prove_by_refinement( `!y1 y2 y3. mu_y (&2) (sqrt(y2 * y2)) (sqrt(y1*y1)) = mu_y (&2) (sqrt(y1 * y1)) (sqrt(y2*y2)) /\ mu_y (&2) (sqrt(y3 * y3)) (sqrt(y2*y2)) = mu_y (&2) (sqrt(y2 * y2)) (sqrt(y3*y3)) /\ mu_y (&2) (sqrt(y3 * y3)) (sqrt(y1*y1)) = mu_y (&2) (sqrt(y1 * y1)) (sqrt(y3*y3)) `,
(* {{{ proof *) [ BY(REWRITE_TAC[mu_y_sym]) ]);;
(* }}} *)
let nonfunctional_mud_126 = 
prove_by_refinement( `! 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 = mu_y a (sqrt(y1 * y1)) (sqrt(y2 * y2)) * sqrt(delta_y a y1 y2 y6 b c)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mud_126_x;]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y]; BY(MESON_TAC[Merge_ineq.delta_y_sym]) ]);;
(* }}} *)
let nonfunctional_mud_234 = 
prove_by_refinement( `! 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 = mu_y a (sqrt(y2 * y2)) (sqrt(y3 * y3)) * sqrt(delta_y a y2 y3 y4 b c)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mud_234_x;]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y]; ]);;
(* }}} *)
let nonfunctional_mud_135 = 
prove_by_refinement( `! 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 = mu_y a (sqrt(y1 * y1)) (sqrt(y3 * y3)) * sqrt(delta_y a y1 y3 y5 b c)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mud_135_x;]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y]; REWRITE_TAC[mu_y_sym]; BY(MESON_TAC[Merge_ineq.delta_y_sym]) ]);;
(* }}} *)
let nonfunctional_flat_term2_126 = 
prove_by_refinement( `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_126_x d a b) x1 x2 x3 x4 x5 x6 = flat_term (sqrt (edge2_flatD_x1 d x1 x2 x6 a b))`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.flat_term2_126_x]; 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]) ]);;
(* }}} *)
let nonfunctional_flat_term2_234 = 
prove_by_refinement( `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_234_x d a b) x1 x2 x3 x4 x5 x6 = flat_term (sqrt (edge2_flatD_x1 d x2 x3 x4 a b))`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.flat_term2_234_x]; 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]) ]);;
(* }}} *)
let nonfunctional_flat_term2_135 = 
prove_by_refinement( `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_135_x d a b) x1 x2 x3 x4 x5 x6 = flat_term (sqrt (edge2_flatD_x1 d x1 x3 x5 a b))`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.flat_term2_135_x]; 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]) ]);;
(* }}} *)
let nonfunctional_mudLs_126 = 
prove_by_refinement( `! y1 y2 x3 x4 x5 y6. mudLs_126_x (&4) (&10) (&2) (&2) (&2) (y1*y1) (y2*y2) x3 x4 x5 (y6*y6) = mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) * (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &4)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mudLs_126_x]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y;delta_y_hex_cases]; REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`]; TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(REAL_ARITH_TAC); BY(REWRITE_TAC[]) ]);;
(* }}} *)
let nonfunctional_mudLs_234 = 
prove_by_refinement( `! x1 y2 y3 y4 x5 x6. mudLs_234_x (&4) (&10) (&2) (&2) (&2) x1 (y2*y2) (y3*y3) (y4*y4) x5 x6 = mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) * (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &4)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mudLs_234_x]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y;delta_y_hex_cases]; REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`]; TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(REAL_ARITH_TAC); BY(REWRITE_TAC[]) ]);;
(* }}} *)
let nonfunctional_mudLs_135 = 
prove_by_refinement( `! y1 x2 y3 x4 y5 x6. mudLs_135_x (&4) (&10) (&2) (&2) (&2) (y1*y1) x2 (y3*y3) x4 (y5*y5) x6 = mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) * (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &4)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.mudLs_135_x]; Functional_equation.F_REWRITE_TAC; REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y;delta_y_hex_cases]; REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`]; TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC); GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; BY(REAL_ARITH_TAC); BY(REWRITE_TAC[]) ]);;
(* }}} *)
let ineq_sym_s3 = 
prove_by_refinement( `!y4 y5 y6 p r . ineq p (r \/ y6 < y4 \/ y5 < y6) ==> ((y4 <= y6 /\ y6 <= y5) ==> ineq p r)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `ineq` MP_TAC; BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`]) ]);;
(* }}} *)
let ineq_sym_s2_aab = 
prove_by_refinement( `!y4 y6 p r. ineq p (r \/ y6 < y4) ==> ((y4 <= y6) ==> ineq p r)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `ineq` MP_TAC; BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`]) ]);;
(* }}} *)
let ineq_sym_s2_abb = 
prove_by_refinement( `!y5 y6 p r. ineq p (r \/ y5 < y6) ==> ((y6 <= y5) ==> ineq p r)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `ineq` MP_TAC; BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`]) ]);;
(* }}} *) let clean_ineq = PURE_REWRITE_RULE[Sphere.y_of_x;Sphere.delta_234_x;Sphere.delta_126_x;Sphere.delta_135_x; arith `#2.52 pow 2 = #2.52 * #2.52 /\ &4 = &2 * &2`;GSYM Sphere.delta_y;delta_y_hex_cases; nonfunctional_mud_126;nonfunctional_mud_234;nonfunctional_mud_135; nonfunctional_flat_term2_126; nonfunctional_flat_term2_234; nonfunctional_flat_term2_135; nonfunctional_mudLs_135 ;nonfunctional_mudLs_126 ;nonfunctional_mudLs_234];; let mk_ineq_hex conv i234 i126 i135 = let nth = List.nth in let d234 = nth [` y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `; `&0`; `y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`; `y_of_x (mudLs_234_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`; `&0 - sol0`] i234 in let d126 = nth [` y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `; `&0`; `y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`; `y_of_x (mudLs_126_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`; `&0 - sol0`] i126 in let d135 = nth [` y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `; `&0`; `y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`; `y_of_x (mudLs_135_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`; `&0 - sol0`] i135 in let c234 = nth [`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`; `F`; `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`; `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`; `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i234 in let c126 = nth [`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`; `F`; `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`; `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`; `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i126 in let c135 = nth [`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`; `F`; `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`; `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`; `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i135 in let s45 = if (i234= i126) then `y6 < y4` else `F` in let s56 = if (i126= i135) then `y5 < y6` else `F` in rhs(concl(conv (Ineq.mk_tplate Main_estimate_ineq.template_hex [d234;d126;d135;c234;c126;c135;s45;s56])));; (* let tmgg a b c = let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in let g' = (mk_imp (`main_nonlinear_terminal_v11`,concl (clean_ineq (ASSUME g)))) in g';; *) let get_ineq (a,b,c) = clean_ineq (Terminal.get_main_nonlinear (Printf.sprintf "7550003505 %d %d %d" a b c));; let get_ineq_term(a,b,c) = let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in concl (clean_ineq (ASSUME g));; let get_ineq'(a,b,c) = let g' = mk_imp(`main_nonlinear_terminal_v11`,get_ineq_term(a,b,c)) in repeat UNDISCH (prove_by_refinement(g',[ DISCH_TAC; BY(REWRITE_TAC[get_ineq(a,b,c)])]));; let r755_0 i = let (yys,tm) = (strip_forall (concl(get_ineq' (i,i,i)))) in let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`y6 < y4 <=> F`);ASSUME (`y5 < y6 <=> F`)] tm)) in let tm1 = list_mk_forall (yys, tm0) in let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in prove_by_refinement(tm2, (* {{{ proof *) [ DISCH_TAC; MATCH_MP_TAC REAL_WLOG_S3_SIMPLEX; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; INTRO_TAC delta_y_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC taum_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC edge2_flatD_x1_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC eulerA_x_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`]; DISCH_THEN (unlist REWRITE_TAC); 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); BY(REAL_ARITH_TAC); BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]); REPEAT GEN_TAC; MATCH_MP_TAC ineq_sym_s3; INTRO_TAC (get_ineq(i,i,i)) yys; BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`]) ]);; (* }}} *) let r755_diag = map (fun i -> (i, r755_0 i)) [0;1;2;3;4];; let r755_aab i j= let (yys,tm) = (strip_forall (concl(get_ineq' (i,i,j)))) in let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y6 < y4) <=> F`)] tm)) in let tm1 = list_mk_forall (yys, tm0) in let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in prove_by_refinement(tm2, (* {{{ proof *) [ DISCH_TAC; MATCH_MP_TAC REAL_WLOG_AAB_SIMPLEX; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; INTRO_TAC delta_y_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC taum_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC edge2_flatD_x1_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC eulerA_x_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`]; DISCH_THEN (unlist REWRITE_TAC); 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); BY(REAL_ARITH_TAC); BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]); REPEAT GEN_TAC; MATCH_MP_TAC ineq_sym_s2_aab; INTRO_TAC (get_ineq(i,i,j)) yys; BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`]) ]);; (* }}} *) 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); (2,3);(2,4);(3,4)];; let r755_abb i j= let (yys,tm) = (strip_forall (concl(get_ineq' (i,j,j)))) in let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y5 < y6) <=> F`)] tm)) in let tm1 = list_mk_forall (yys, tm0) in let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in prove_by_refinement(tm2, (* {{{ proof *) [ DISCH_TAC; MATCH_MP_TAC REAL_WLOG_ABB_SIMPLEX; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; INTRO_TAC delta_y_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC taum_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC edge2_flatD_x1_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC eulerA_x_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`]; DISCH_THEN (unlist REWRITE_TAC); TYPIFY_GOAL_THEN `!f. f y1 y2 y6 + f y1 y3 y5 = f y1 y3 y5 + f y1 y2 y6` (unlist ONCE_REWRITE_TAC); BY(REAL_ARITH_TAC); BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]); REPEAT GEN_TAC; MATCH_MP_TAC ineq_sym_s2_abb; INTRO_TAC (get_ineq(i,j,j)) yys; BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`]) ]);; (* }}} *) 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); (2,3);(2,4);(3,4)];; let get_ineq2( i, j, k) = let _ = (i <= j && j <= k) or failwith "get2 out of range" in if (i = j && j = k) then UNDISCH (assoc i r755_diag) else if (i = j) then UNDISCH (assoc (i,k) r755_aab_list) else if (j = k) then UNDISCH (assoc (i,j) r755_abb_list) else get_ineq'(i,j,k);; (* let tmg i j = let (yys,tm) = (strip_forall (concl(get_ineq (i,j,j)))) in let tm0 = rhs(concl(REWRITE_CONV [ASSUME (`~(y5 < y6) /\ ~(y6 < y4)`)] tm)) in let tm1 = list_mk_forall (yys, tm0) in let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in tm2;; *) let g755_ i j k = (* let inq = (Main_estimate_ineq.make_hex_ear i j k).ineq in let inq' = concl(clean_ineq (ASSUME inq)) in *) let inq' = get_ineq_term (i,j,k) in let (yys,tm) = strip_forall inq' in let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME `(y5 < y6) <=> F`;ASSUME `(y6 < y4) <=> F`] tm)) in let tm1 = list_mk_forall (yys, tm0) in let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in tm2;; let r755_ikj getter i j k = prove_by_refinement( (g755_ i j k), (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC ( (getter (i, k, j))) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`]; INTRO_TAC delta_y_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC taum_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC edge2_flatD_x1_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC eulerA_x_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`]; DISCH_THEN (unlist REWRITE_TAC); REWRITE_TAC[REAL_ADD_AC]; BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]) ]);; (* }}} *) let rec cross a = function | [] -> [] | b::bs -> (map (fun i -> (i,b)) a) @ cross a bs;; let triples = map (fun ((i,j),k)-> (i,j,k)) (cross (cross (0--4) (0--4)) (0--4));; let r755_ikj_list = let ls = map (fun (i,j,k) -> ((i,j,k), if (i > j or i > k) then TRUTH else if (j<= k) then get_ineq2 (i,j,k) else r755_ikj get_ineq2 i j k)) in ls triples;; let get_ineq3( i, j, k) = let _ = (i <= j && i <= k) or failwith (Printf.sprintf "get3 out of range %d %d %d" i j k) in repeat UNDISCH (assoc (i,j,k) r755_ikj_list);; let r755_jik i j k = prove_by_refinement( (g755_ i j k), (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC ( (get_ineq3 (j, i, k))) [`y3`;`y2`;`y1`;`y6`;`y5`;`y4`]; INTRO_TAC delta_y_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC taum_sym_cases2 yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC edge2_flatD_x1_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC eulerA_x_sym_cases yys; DISCH_THEN (unlist REWRITE_TAC); INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`]; DISCH_THEN (unlist REWRITE_TAC); REWRITE_TAC[REAL_ADD_AC]; BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]) ]);; (* }}} *) let r755_jik_list = let ls = map (fun (i,j,k) -> ((i,j,k), if (k < i && k < j) then TRUTH else if (i<= j) then get_ineq3 (i,j,k) else r755_jik i j k)) in ls triples;; let get_ineq4( i, j, k) = let thm = repeat UNDISCH (assoc (i,j,k) r755_jik_list) in let _ = (not(thm = TRUTH)) or failwith (Printf.sprintf "get4 out of range %d %d %d" i j k) in thm;; let get_ineq5 = let ls = map (fun (i,j,k) -> ((i,j,k), if (k < i && k < j) then r755_ikj get_ineq4 i j k else get_ineq4 (i,j,k))) in let r755_ikj_list2 = ls triples in fun ( i, j, k) -> repeat UNDISCH (assoc (i,j,k) r755_ikj_list2);; (* let _ = (125 = List.length (filter (fun t -> not (snd t = TRUTH)) r755_ikj_list2));; *)
let taud_mu_clauses = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y2 y3 y4. (&2 <= y2 /\ y2 <= #2.52 /\ &2 <= y3 /\ y3 <= #2.52 /\ #3.01 <= y4 /\ y4 <= #3.915) ==> (let d = delta_y (&2) y2 y3 y4 (&2) (&2) in let t = taud (&2) y2 y3 y4 (&2) (&2) in ((&0 <= d /\ d <= &16 ==> -- sol0 <= t) /\ (&16 <= d /\ d <= &100 ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) * (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) - sol0 <= t) /\ (&100 <= d ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) * sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) - sol0 <= t))))`,
(* {{{ proof *) [ REWRITE_TAC[LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; CONJ_TAC; DISCH_TAC; INTRO_TAC (taud_ge_flat_term) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC); BY(REWRITE_TAC[flat_term_2]); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2]; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`]; TYPED_ABBREV_TAC `d = delta_y (&2) y2 y3 y4 (&2) (&2)`; MATCH_MP_TAC (arith `m* a <= m * a' ==> m * a - s <= --s + a' * m`); GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP; CONJ_TAC; REWRITE_TAC[Nonlin_def.mu_y]; BY(ASM_TAC THEN REAL_ARITH_TAC); TYPIFY `&2 * &2 = sqrt(&16)` (C SUBGOAL_THEN SUBST1_TAC); MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma; BY(REAL_ARITH_TAC); TYPIFY `&14 = sqrt(&16) + sqrt(&100)` (C SUBGOAL_THEN SUBST1_TAC); TYPIFY `&4 = sqrt(&16) /\ &10 = sqrt(&100)` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); CONJ_TAC; MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma; BY(REAL_ARITH_TAC); MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma; BY(REAL_ARITH_TAC); MATCH_MP_TAC sqrt_secant_approx; BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "final case";
GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`]; DISCH_TAC; REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2]; BY(REAL_ARITH_TAC) ]);; (* }}} *)
let terminal_hex_234_reduction = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 f1 f2 b1 b2. (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915; #3.01, y5, #3.915; #3.01,y6, #3.915] in (ineq dom (f1 + flat_term (sqrt (edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4 * y4) (&2 * &2) (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/ delta_y #2.52 y2 y3 y4 (&2) (&2) > &0) \/ b2)) /\ (ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\ (ineq dom (f1 + ( mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) * sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) - sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y2 y3 y4 (&2) (&2) < &100 \/ b2)) /\ (ineq dom (f1 + ( mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) * (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) - sol0) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &16 \/ delta_y (&2) y2 y3 y4 (&2) (&2) > &100) \/ b2)) /\ (ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/ delta_y (&2) y2 y3 y4 (&2) (&2) > &16) \/ b2))) ==> (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915; #3.01, y5, #3.915; #3.01,y6, #3.915;&2,y234,#2.52] ((f1 + taum y234 y2 y3 y4 (&2) (&2)) + f2 > #0.712 \/ (delta_y y234 y2 y3 y4 (&2) (&2) < &0 \/ b1) \/ b2)))`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[]; ASM_CASES_TAC `b1:bool`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; ASM_CASES_TAC `b2:bool`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; REWRITE_TAC[arith `f1 + t + f2 > #0.712 <=> t > #0.712 - f1 - f2`;arith `(f1 + t) + f2 > #0.712 <=> t > #0.712 - f1 - f2`]; TYPED_ABBREV_TAC `c = #0.712 - f1 - f2`; REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `&0 <= taum y234 y2 y3 y4 (&2) (&2)`; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); ASM_CASES_TAC `delta_y y234 y2 y3 y4 (&2) (&2) < &0`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; INTRO_TAC (UNDISCH taud_minimizer_terminal_hex_cases) [`y234`;`y2`;`y3`;`y4`]; ASM_SIMP_TAC[arith `~(d < &0) ==> &0 <= d`;arith `~(&0 <= t) ==> t < &0`]; ANTS_TAC; BY(REWRITE_TAC[Sphere.h0] THEN ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH OWZLKVY4) [`y234`;`y2`;`y3`;`y4`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC); DISCH_TAC; FIRST_X_ASSUM DISJ_CASES_TAC; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); INTRO_TAC (UNDISCH taud_mu_clauses) [`y2`;`y3`;`y4`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[LET_DEF;LET_END_DEF]; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT (FIRST_X_ASSUM_ST `mu_y` kill); INTRO_TAC taud_ge_flat_term [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); DISCH_TAC; INTRO_TAC (UNDISCH edge2_flatD_x1_delta_lemma3) [`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`]; REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); DISCH_TAC; FIRST_X_ASSUM_ST `sqrt` MP_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx; ASM_SIMP_TAC [arith `&2 <= z1 ==> &0 <= z1`]; INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); INTRO_TAC (UNDISCH delta_2_nn) [`z1`;`y2`;`y3`;`y4`]; ANTS_TAC; BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC); BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.h0;arith `#2.52 = &2 * #1.26`] THEN REAL_ARITH_TAC) ]);;
(* }}} *) let mk_25 j k = let get_spec i j k = ISPECL yys (get_ineq5(i,j,k)) in let aa i = get_spec i j k in let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in GENL yys (MATCH_MP (rule (UNDISCH terminal_hex_234_reduction)) (end_itlist CONJ (map aa (0--4))));; (* let terminal_hex_25 = map (fun (j,k) -> mk_25 j k) (cross (0--4) (0--4));; *)
let terminal_hex_126_reduction = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 f1 f2 b1 b2. (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915; #3.01, y5, #3.915; #3.01,y6, #3.915;&2,y234,#2.52 ] in (ineq dom (f1 + flat_term (sqrt (edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6 * y6) (&2 * &2) (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/ delta_y #2.52 y1 y2 y6 (&2) (&2) > &0) \/ b2)) /\ (ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\ (ineq dom (f1 + ( mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) * sqrt (delta_y (&2) y1 y2 y6 (&2) (&2)) - sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y1 y2 y6 (&2) (&2) < &100 \/ b2)) /\ (ineq dom (f1 + ( mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) * (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &2 * &2) - sol0) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &16 \/ delta_y (&2) y1 y2 y6 (&2) (&2) > &100) \/ b2)) /\ (ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/ delta_y (&2) y1 y2 y6 (&2) (&2) > &16) \/ b2))) ==> (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915; #3.01, y5, #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 \/ (delta_y y126 y1 y2 y6 (&2) (&2) < &0 \/ b1) \/ b2)))`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[]; ASM_CASES_TAC `b1:bool`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; ASM_CASES_TAC `b2:bool`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y3`;`y1`;`y2`;`y6`;`y4`;`y5`;`y126`;`f1`;`f2`;`b1`;`b2`]; BY(ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF]) ]);;
(* }}} *) let mk_5 k = let yys' = yys @ [`y234:real`] in let get_spec j k = ISPECL (yys') (mk_25 j k) in let aa j = get_spec j k in let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in GENL yys' (MATCH_MP (rule (UNDISCH terminal_hex_126_reduction)) (end_itlist CONJ (map aa (0--4))));;
let terminal_hex_135_reduction = 
prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 y135 f1 b1 b2. (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915; #3.01, y5, #3.915; #3.01,y6, #3.915;&2,y234,#2.52; &2,y126,#2.52 ] in (ineq dom (f1 + flat_term (sqrt (edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5 * y5) (&2 * &2) (&2 * &2))) > #0.712 \/ b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/ delta_y #2.52 y1 y3 y5 (&2) (&2) > &0) \/ b2)) /\ (ineq dom (f1 + &0 > #0.712 \/ b1 \/ F \/ b2)) /\ (ineq dom (f1 + ( mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) * sqrt (delta_y (&2) y1 y3 y5 (&2) (&2)) - sol0) > #0.712 \/ b1 \/ delta_y (&2) y1 y3 y5 (&2) (&2) < &100 \/ b2)) /\ (ineq dom (f1 + ( mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) * (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &2 * &2) - sol0) > #0.712 \/ b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &16 \/ delta_y (&2) y1 y3 y5 (&2) (&2) > &100) \/ b2)) /\ (ineq dom (f1 + ( &0 - sol0) > #0.712 \/ b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/ delta_y (&2) y1 y3 y5 (&2) (&2) > &16) \/ b2))) ==> (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52; #3.01,y4, #3.915; #3.01, y5, #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 \/ (delta_y y135 y1 y3 y5 (&2) (&2) < &0 \/ b1) \/ b2)))`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF]; REPEAT WEAKER_STRIP_TAC; REPEAT (FIRST_X_ASSUM_ST `==>` MP_TAC) THEN ASM_REWRITE_TAC[]; ASM_CASES_TAC `b1:bool`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; ASM_CASES_TAC `b2:bool`; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y2`;`y1`;`y3`;`y5`;`y4`;`y6`;`y135`;`f1`;`&0`;`b1`;`b2`]; ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF]; RULE_ASSUM_TAC (REWRITE_RULE[arith `a + &0 = a`]); BY(ASM_REWRITE_TAC[arith `a + &0 = a`]) ]);;
(* }}} *) let terminal_hex_taum = let yys' = (yys @ [`y234:real`;`y126:real`]) in let aa k = ISPECL yys' (mk_5 k) in let rule1 = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in let rule2 = REWRITE_RULE[REAL_ADD_AC] in GENL yys' (rule2(MATCH_MP (rule1 (UNDISCH terminal_hex_135_reduction)) (end_itlist CONJ (map aa (0--4)))));; end;;