(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: nonlinear inequalities                                            *)
(* Author:  Thomas Hales     *)
(* Date: 2010-10-17                                                         *)
(* ========================================================================== *)

(*
Definitions and Lemmas used in the generation of interval arithmetic
code from the HOL Light specifications.

*)

(* ========================================================================== *)
(*    DEFINITIONS                                                            *)
(* ========================================================================== *)

module Nonlinear_lemma = struct

let ineq = Sphere.ineq;;


let NONLIN = new_definition `NONLIN = T`;;


let sqrt_x1 = define `sqrt_x1 x1 x2 x3 x4 x5 x6 = sqrt x1`;;


let sqrt_x2 = define `sqrt_x2 x1 x2 x3 x4 x5 x6 = sqrt x2`;;


let sqrt_x3 = define `sqrt_x3 x1 x2 x3 x4 x5 x6 = sqrt x3`;;


let sqrt_x4 = define `sqrt_x4 x1 x2 x3 x4 x5 x6 = sqrt x4`;;


let sqrt_x5 = define `sqrt_x5 x1 x2 x3 x4 x5 x6 = sqrt x5`;;


let sqrt_x6 = define `sqrt_x6 x1 x2 x3 x4 x5 x6 = sqrt x6`;;


let halfbump_x = new_definition `halfbump_x x = bump (sqrt x / &2)`;;


let halfbump_x1 = new_definition `halfbump_x1 x1 x2 x3 x4 x5 x6 = halfbump_x x1`;;


let halfbump_x4 = new_definition `halfbump_x4 x1 x2 x3 x4 x5 x6 = halfbump_x x4`;;


let unit6 = define `unit6 x1 x2 x3 x4 x5 x6 = &1`;;


let proj_x1 = define `proj_x1 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x1`;;


let proj_x2 = define `proj_x2 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x2`;;


let proj_x3 = define `proj_x3 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x3`;;


let proj_x4 = define `proj_x4 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x4`;;


let proj_x5 = define `proj_x5 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x5`;;


let proj_x6 = define `proj_x6 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x6`;;


let promote = define `promote f (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = f x1`;;


let unit0 = define `unit0 = &1`;;
 


let pow1 = new_definition `pow1 y = y pow 1`;;


let pow2 = new_definition `pow2 y = y pow 2`;;


let pow3 = new_definition `pow3 y = y pow 3`;;


let pow4 = new_definition `pow4 y = y pow 4`;;


let promote_pow2 = new_definition `promote_pow2 x1 (x2:A) (x3:B) (x4:C) (x5:D) (x6:E) = x1 pow 2`;;


let promote_pow3 = new_definition `promote_pow3 x1 (x2:A) (x3:B) (x4:C) (x5:D) (x6:E) = x1 pow 3`;;


let compose6 = new_definition `compose6 f p1 p2 p3 p4 p5 p6 
  (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
  (f:real->real->real->real->real->real->real)
  (p1 x1 x2 x3 x4 x5 x6)
    (p2 x1 x2 x3 x4 x5 x6)
    (p3 x1 x2 x3 x4 x5 x6)
    (p4 x1 x2 x3 x4 x5 x6)
    (p5 x1 x2 x3 x4 x5 x6)
    (p6 x1 x2 x3 x4 x5 x6)`;;


let scale6 = new_definition `scale6 f
   (r:real)   (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
   (f x1 x2 x3 x4 x5 x6) * r`;;


let quadratic_root_plus_curry = 
  new_definition `quadratic_root_plus_curry a b c = quadratic_root_plus (a,b,c)`;;


let sq_pow2 = 
prove_by_refinement(
  `!a x. a pow 2 <= x ==> (sqrt x * sqrt x = x)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[GSYM REAL_POW_2;SQRT_POW2];
  MESON_TAC[REAL_LE_TRANS;Collect_geom.REAL_LE_SQUARE_POW];
  ]);;
  (* }}} *)


let sqrt2_sqrt2 = 
prove_by_refinement(
  `sqrt2 * sqrt2 = &2`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.sqrt2];
    MATCH_MP_TAC sq_pow2;
  EXISTS_TAC`&0`;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)

(* SOME DEFINITIONS *)


let vol3f_sqrt2_lmplus = new_definition 
  `vol3f_sqrt2_lmplus y1 y2 (y3:real) (y4:real) (y5:real) y6 = 
    (&2 * mm1 / pi) *
             (&2 * dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
              &2 * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
              &2 * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
              dih3_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
              dih4_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
              dih5_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - &3 * pi) -
             (&8 * mm2 / pi) *
             (
              lfun (y2 / &2) * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
              lfun (y6 / &2) * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6)`;;


let vol3f_x_sqrt2_lmplus = new_definition
  `vol3f_x_sqrt2_lmplus x1 x2 x3 x4 x5 x6 =
   vol3f_sqrt2_lmplus (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)      (sqrt x6)`;;


let vol3f_x_lfun = new_definition 
 `vol3f_x_lfun x1 x2 (x3:real) (x4:real) (x5:real) x6 = vol3f (sqrt x1) (sqrt x2) (sqrt x6)  sqrt2 lfun `;;


let vol3_x_sqrt = new_definition
 `vol3_x_sqrt x1 x2 (x3:real) (x4:real) (x5:real) x6  = vol_y sqrt2 sqrt2 sqrt2 (sqrt x1) (sqrt x2) (sqrt x6) `;;


let monomial = new_definition `monomial n1 n2 n3 n4 n5 n6 y1 y2 y3 y4 y5 y6 = 
   (y1 pow n1) * (y2 pow n2) * (y3 pow n3) * (y4 pow n4) * (y5 pow n5) * (y6 pow n6)`;;


let arclength_x_234 = new_definition `arclength_x_234  (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = arclength (sqrt x2) (sqrt x3) (sqrt x4)`;;


let arclength_x_126 = new_definition `arclength_x_126  (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = arclength (sqrt x1) (sqrt x2) (sqrt x6)`;;


(* ========================================================================== *)
(*    BASIC LEMMAS                                                            *)
(* ========================================================================== *)

let strip_let_tm t = snd(dest_eq(concl(REDEPTH_CONV let_CONV t)));;

let strip_let t = REWRITE_RULE[REDEPTH_CONV let_CONV (concl t )] t;;


let tame_table_d_values = 
prove_by_refinement(
  `tame_table_d 2 1 = #0.103 /\ tame_table_d 1 2 = #0.2759 /\ tame_table_d 0 3 = #0.4488 /\ tame_table_d 4 1 = #0.6548  /\
    tame_table_d 6 0 = #0.7578 /\
    tame_table_d 3 1 = #0.3789 /\
    tame_table_d 2 2 = #0.5518 /\
   tame_table_d 1 3 = #0.7247 /\
   tame_table_d 0 4 = #0.8976 /\
   tame_table_d 5 0 = #0.4819 /\
   tame_table_d 4 1 = #0.6548 /\
   tame_table_d 3 2 = #0.8277 /\
   tame_table_d 2 3 = #1.0006
 `,

  (* {{{ proof *)
  [
    REWRITE_TAC[Sphere.tame_table_d;ARITH_RULE `2 + 2 * 1 > 3 /\ 1 + 2 * 2 > 3 /\ 0 + 2 * 3 > 3 /\ 4 + 2 *1 > 3 /\ 6 + 2 * 0 > 3 /\ (2 + 2 * 3 > 3) /\ (3 + 2 * 2 > 3) /\ (5 + 2 * 0 > 3) /\ (0 + 2 * 4 > 3) /\ (1 + 2 * 3 > 3) /\ (2 + 2 * 2 > 3) /\ (3 + 2 * 1 > 3)` ];
    REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let unit0f = 
prove_by_refinement(
  `f x1 x2 x3 x4 x5 x6 * unit0 = f x1 x2 x3 x4 x5 x6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[unit0] THEN REAL_ARITH_TAC
  ]);;
  (* }}} *)


let sqrt8_sqrt2 = 
prove_by_refinement(
  `sqrt8 = &2 * sqrt2`,

  (* {{{ proof *)
  [
  SIMP_TAC[Sphere.sqrt8;Sphere.sqrt2;SQRT_MUL;
	   REAL_ARITH `&8 = &2 pow 2 * &2 /\ &0 <= &2 /\ &0 <= &2 pow 2 /\ 
      abs(&2) = &2`;POW_2_SQRT_ABS];
  ]);;
  (* }}} *)


let sqrt2_sqrt8 = 
prove_by_refinement(
  `sqrt2 = #0.5 * sqrt8`,

  (* {{{ proof *)
  [
  REWRITE_TAC[sqrt8_sqrt2];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let SQRT_MUL_POW_2= 
prove_by_refinement(`!(a:real) b. (a>= &0) /\ (b>= &0) ==> sqrt((a*a)*b)= a* sqrt(b)`,

[
SIMP_TAC[SQRT_MUL;REAL_LE_SQUARE;real_ge];
MESON_TAC[sq_pow2;REAL_ARITH `&0 pow 2 = &0`];
]);;

(* sol0 = const1 * pi, repeated from TameGeneral.hl *)

let sol0_EQ_sol_y = 
prove(`sol0 = sol_y (&2) (&2) (&2) (&2) (&2) (&2)`,

    REWRITE_TAC[Sphere.sol0; Sphere.sol_y; Sphere.dih_y; Sphere.dih_x; Sphere.delta_x4; Sphere.delta_x] THEN
      CONV_TAC (DEPTH_CONV let_CONV) THEN
      CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
      MP_TAC (SPEC `&1 / &3` Trigonometry2.acs_atn2) THEN
      CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
      REWRITE_TAC [REAL_ARITH `&3 * (a - b) - c = (a + d) + (a + d) + (a + d) - c <=> --b = d`] THEN
      MP_TAC (SPECL [`sqrt (&8 / &9)`; `&1 / &3`] Trigonometry1.ATN2_RNEG) THEN
      CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
      SUBGOAL_THEN `sqrt (&2048) = &48 * sqrt (&8 / &9) /\ -- &16 = &48 * (-- &1 / &3)` ASSUME_TAC THENL
      [
	MP_TAC (SPECL [`&48`; `&8 / &9`] SQRT_MUL_POW_2) THEN
	  CONV_TAC (REAL_RAT_REDUCE_CONV);
	ALL_TAC
      ] THEN
      ASM_REWRITE_TAC[] THEN
      MATCH_MP_TAC (GSYM Trigonometry1.ATN2_LMUL_EQ) THEN
      REAL_ARITH_TAC);;


let sol0_over_pi_EQ_const1 = 
prove(`sol0 / pi = const1`,

   REWRITE_TAC[sol0_EQ_sol_y; Sphere.const1]);;


let sol0_const1 = 
prove_by_refinement(
  `sol0 = pi * const1`,

  (* {{{ proof *)
  [
  REWRITE_TAC[GSYM sol0_over_pi_EQ_const1];
  MP_TAC PI_POS;
  CONV_TAC REAL_FIELD;
  ]);;
  (* }}} *)


let ineq_lemma_b = 
prove_by_refinement(
  `!a y b. (&0 <= a  /\  &0 <= b /\  a <= y /\ y <= b)  ==> 
    a pow 2 <= y pow 2 /\ y pow 2 <= b pow 2 /\ (sqrt (y pow 2) = y)`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
    STRIP_TAC;
    SUBGOAL_THEN `&0 <= y` MP_TAC;
  ASM_MESON_TAC [REAL_LE_TRANS];
  ASM_MESON_TAC[Collect_geom.POW2_COND;POW_2_SQRT_ABS;
		REAL_ARITH `&0 <= x ==> (x = abs x)`];
  ]);;
  (* }}} *)


let ineq_square2  = 
prove_by_refinement(
  `(&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4 /\ &0 <= a5 /\ &0 <= a6 /\
      &0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ &0 <= b4 /\ &0 <= b5 /\ &0 <= b6 )
   /\ 
    (!x1 x2 x3 x4 x5 x6. 
       ineq [(a1 pow 2,x1,b1 pow 2);(a2 pow 2,x2,b2 pow 2);(a3 pow 2,x3,b3 pow 2);
        (a4 pow 2,x4,b4 pow 2);(a5 pow 2,x5,b5 pow 2);(a6 pow 2,x6,b6 pow 2)]
          (P (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6))) ==>
    (!y1 y2 y3 y4 y5 y6.
      ineq 
        [(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6)]
          (P y1 y2 y3 y4 y5 y6))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[ineq];
  REPEAT STRIP_TAC;
  FIRST_X_ASSUM (fun t-> MP_TAC (SPECL [`y1 pow 2`;`y2 pow 2`;`y3 pow 2`;`y4 pow 2`;`y5 pow 2`;`y6 pow 2`] t));
  SUBGOAL_THEN `(sqrt (y1 pow 2) = y1) /\ (sqrt (y2 pow 2) = y2) /\  (sqrt (y3 pow 2) = y3) /\   (sqrt (y4 pow 2) = y4) /\   (sqrt (y5 pow 2) = y5) /\   (sqrt (y6 pow 2) = y6)` (fun t -> REWRITE_TAC[t]);
  ASM_MESON_TAC[ineq_lemma_b];
  REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`];
  DISCH_THEN MATCH_MP_TAC;
  ASM_MESON_TAC[ineq_lemma_b];
  ]);;
  (* }}} *)


let ineq_square2_9  = 
prove_by_refinement(
  `(&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4 /\ &0 <= a5 /\ &0 <= a6 /\
     &0 <= a7 /\ &0 <= a8 /\ &0 <= a9 /\
      &0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ &0 <= b4 /\ &0 <= b5 /\ &0 <= b6 /\
    &0 <= b7 /\ &0 <= b8 /\ &0 <= b9
)
   /\ 
    (!x1 x2 x3 x4 x5 x6 x7 x8 x9. 
       ineq [(a1 pow 2,x1,b1 pow 2);(a2 pow 2,x2,b2 pow 2);(a3 pow 2,x3,b3 pow 2);
        (a4 pow 2,x4,b4 pow 2);(a5 pow 2,x5,b5 pow 2);(a6 pow 2,x6,b6 pow 2);
        (a7 pow 2,x7,b7 pow 2);(a8 pow 2,x8,b8 pow 2);(a9 pow 2,x9,b9 pow 2)]
          (P (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) (sqrt x7) (sqrt x8) (sqrt x9))) ==>
    (!y1 y2 y3 y4 y5 y6 y7 y8 y9.
      ineq 
        [(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6);(a7,y7,b7);(a8,y8,b8);(a9,y9,b9)]
          (P y1 y2 y3 y4 y5 y6 y7 y8 y9))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[ineq];
  REPEAT STRIP_TAC;
  FIRST_X_ASSUM (fun t-> MP_TAC (SPECL [`y1 pow 2`;`y2 pow 2`;`y3 pow 2`;`y4 pow 2`;`y5 pow 2`;`y6 pow 2`;`y7 pow 2`;`y8 pow 2`;`y9 pow 2`] t));
  SUBGOAL_THEN `(sqrt (y1 pow 2) = y1) /\ (sqrt (y2 pow 2) = y2) /\  (sqrt (y3 pow 2) = y3) /\   (sqrt (y4 pow 2) = y4) /\   (sqrt (y5 pow 2) = y5) /\   (sqrt (y6 pow 2) = y6) /\  (sqrt (y7 pow 2) = y7) /\  (sqrt (y8 pow 2) = y8) /\  (sqrt (y9 pow 2) = y9)` (fun t -> REWRITE_TAC[t]);
  ASM_MESON_TAC[ineq_lemma_b];
  REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`];
  DISCH_THEN MATCH_MP_TAC;
  ASM_MESON_TAC[ineq_lemma_b];
  ]);;
  (* }}} *)


let sqrt8_nn = 
prove_by_refinement(
  `&0 <= sqrt8`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.sqrt8];
  MATCH_MP_TAC SQRT_POS_LE;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let sqrt2_nn = 
prove_by_refinement(
  `&0 <= sqrt2`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.sqrt2];
  MATCH_MP_TAC SQRT_POS_LE;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let sqrt3_nn = 
prove_by_refinement(
  `&0 <= sqrt(&3)`,

  (* {{{ proof *)
  [
  MATCH_MP_TAC SQRT_POS_LE;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)

let basic_constants_nn = [
 REAL_ARITH `&0 <= #2.18 /\ &0 <= &2 /\ &0 <= #2.52 /\ #2.0 = &2 /\ #2 = &2 /\ &0 <= #2.25 `;
 sqrt8_nn;sqrt2_nn;
 ];;


let abc_quadratic = 
prove (`abc_of_quadratic (\x. a * (x pow 2) + b * x + c) = (a,b,c)`,

 REWRITE_TAC[Sphere.abc_of_quadratic] THEN
 (REPEAT LET_TAC) THEN
 REWRITE_TAC[PAIR_EQ] THEN
 REPEAT(FIRST_X_ASSUM MP_TAC)THEN
 ARITH_TAC);;


let delta_quadratic = 
prove( `-- delta_x x1 x2 x3 x4 x5 x6 = 
  (x1) * (x4 pow 2) + (x1*x1 + (x3 - x5)*(x2 - x6) 
   - x1*(x2 + x3 + x5 + x6)) * x4 
   + ( x1*x3*x5 + x1*x2*x6 - x3*(x1 + x2 - x3 + x5 - x6)*x6 
    - x2*x5*(x1 - x2 + x3 - x5 + x6) ) `,

REWRITE_TAC[Sphere.delta_x] THEN
ARITH_TAC);;

let edge_flat_rewrite = 
 REWRITE_RULE[abc_quadratic;delta_quadratic] Sphere.edge_flat;;

let enclosed_rewrite = 
  REWRITE_RULE[abc_quadratic] 
  (strip_let(REWRITE_RULE[Mur.muRa;Cayleyr.cayleyR_quadratic] Enclosed.enclosed));;

let quad_root_plus_curry = 
  REWRITE_RULE[Sphere.quadratic_root_plus] quadratic_root_plus_curry;;


let y_of_x_e = 
prove(`!y1 y2 y3 y4 y5 y6. y_of_x f y1 y2 y3 y4 y5 y6 =
     f (y1*y1) (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6)`,

     REWRITE_TAC[Sphere.y_of_x]);;


let vol_y_e = 
prove(`!y1 y2 y3 y4 y5 y6. vol_y y1 y2 y3 y4 y5 y6 = 
    y_of_x vol_x y1 y2 y3 y4 y5 y6`,

    REWRITE_TAC[Sphere.vol_y]);;


let rad2_y_e = 
prove(`!y1 y2 y3 y4 y5 y6. rad2_y y1 y2 y3 y4 y5 y6 = 
    y_of_x rad2_x y1 y2 y3 y4 y5 y6`,

    REWRITE_TAC[Sphere.rad2_y]);;


let rad2_x_y = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
    (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
    (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> 
    (rad2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
         rad2_x x1 x2 x3 x4 x5 x6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rad2_y;y_of_x_e;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[sq_pow2];
  ]);;
  (* }}} *)


let delta_x4_delta4_y = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
    (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
    (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> 
  (delta4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = delta_x4 x1 x2 x3 x4 x5 x6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.delta4_y;y_of_x_e;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[sq_pow2];
  ]);;
  (* }}} *)


let dih_x_y = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
    (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
    (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> 
    (dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
         dih_x x1 x2 x3 x4 x5 x6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[sq_pow2];
  ]);;
  (* }}} *)


let dih2_x_y = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
    (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
    (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> 
    (dih2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
         dih2_x x1 x2 x3 x4 x5 x6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih2_y;Sphere.dih2_x;Sphere.dih_y;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[sq_pow2];
  ]);;
  (* }}} *)


let dih3_x_y = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
    (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
    (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> 
    (dih3_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
         dih3_x x1 x2 x3 x4 x5 x6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih3_y;Sphere.dih3_x;Sphere.dih_y;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[sq_pow2];
  ]);;
  (* }}} *)


let delta_x_y = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
    (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
    (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> 
    (delta_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
         delta_x x1 x2 x3 x4 x5 x6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.delta_y;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[sq_pow2];
  ]);;
  (* }}} *)


let vol_x_y = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
    (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
    (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> 
    (vol_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = 
         vol_x x1 x2 x3 x4 x5 x6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.vol_y;Sphere.y_of_x;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[sq_pow2];
  ]);;
  (* }}} *)



let sqrt8_2 = 
prove_by_refinement(
  `sqrt8 * sqrt8 = #8.0`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.sqrt8];
  MESON_TAC[REAL_POW_2;SQRT_WORKS;REAL_ARITH `&8 = #8.0 /\ &0 <= &8`];
  ]);;
  (* }}} *)


let dih_x_sym = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. dih_x x1 x2 x3 x4 x5 x6 = dih_x x1 x3 x2 x4 x6 x5`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih_x;LET_DEF;LET_END_DEF];
  REPEAT GEN_TAC;
  REPEAT AP_TERM_TAC;
  REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4;PAIR_EQ];
  CONJ_TAC THEN AP_TERM_TAC THEN REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let dih_x_sym2 = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. dih_x x1 x2 x3 x4 x5 x6 = dih_x x1 x5 x6 x4 x2 x3`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih_x;LET_DEF;LET_END_DEF];
  REPEAT GEN_TAC;
  REPEAT AP_TERM_TAC;
  REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4;PAIR_EQ];
  CONJ_TAC THEN AP_TERM_TAC THEN REAL_ARITH_TAC;
  ]);;
  (* }}} *)



let dih_y_sym = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. dih_y y1 y2 y3 y4 y5 y6 = dih_y y1 y3 y2 y4 y6 y5`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
  MESON_TAC[dih_x_sym];
  ]);;
  (* }}} *)


let dih_y_sym2 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. dih_y y1 y2 y3 y4 y5 y6 = dih_y y1 y5 y6 y4 y2 y3`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
  MESON_TAC[dih_x_sym2];
  ]);;
  (* }}} *)


let sol_y_123 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. sol_y y1 y2 y3 y4 y5 y6 = 
    dih_y y1 y2 y3 y4 y5 y6 + dih2_y y1 y2 y3 y4 y5 y6 + dih3_y y1  y2 y3 y4 y5 y6 - pi`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.sol_y;Sphere.dih2_y;Sphere.dih3_y];
  REPEAT GEN_TAC;
  MATCH_MP_TAC (REAL_ARITH `(b = b') ==> (a + b + c -pi = a + b' + c - pi)`);
  REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
  MESON_TAC[dih_x_sym];
  ]);;
  (* }}} *)


let rhazim2_alt = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. rhazim2 y1 y2 y3 y4 y5 y6 = rho y2 * dih2_y y1 y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rhazim2;Sphere.node2_y;Sphere.rhazim;Sphere.dih2_y;Sphere.dih_y;LET_DEF;LET_END_DEF];
  MESON_TAC[dih_x_sym];
  ]);;
  (* }}} *)


let rhazim3_alt = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. rhazim3 y1 y2 y3 y4 y5 y6 = rho y3 * dih3_y y1 y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rhazim3;Sphere.node3_y;Sphere.rhazim;Sphere.dih3_y;Sphere.dih_y;LET_DEF;LET_END_DEF];
  ]);;
  (* }}} *)


let taum_123 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. taum y1 y2 y3 y4 y5 y6 = rhazim y1 y2 y3 y4 y5 y6 + rhazim2 y1 y2 y3 y4 y5 y6 + rhazim3 y1  y2 y3 y4 y5 y6 - (&1 + const1)* pi`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[Sphere.taum;sol_y_123;Sphere.lnazim];
    SUBGOAL_THEN `dih_y y2 y3 y1 y5 y6 y4 = dih2_y y1 y2 y3 y4 y5 y6 /\ dih_y y3 y1 y2 y6 y4 y5 = dih3_y y1 y2 y3 y4 y5 y6` (fun t-> REWRITE_TAC[t]);
  REWRITE_TAC[Sphere.dih_y;Sphere.dih2_y;Sphere.dih3_y;LET_DEF;LET_END_DEF] THEN MESON_TAC[dih_x_sym];
  REWRITE_TAC[Sphere.rhazim;rhazim2_alt;rhazim3_alt;Sphere.rho];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let tauq_x_y = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6 x7 x8 x9.
   (tauq (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) (sqrt x7) (sqrt x8) (sqrt x9) = 
    taum_x x1 x2 x3 x4 x5 x6 + taum_x x7 x2 x3 x4 x8 x9)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.tauq;Sphere.taum_x;taum_123;LET_DEF;LET_END_DEF;Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x];
  ]);;
					   	  
  (* }}} *)					   



let rho_alt = 
prove_by_refinement(
  `!y. rho y = &1 + const1 *(y - &2) / (#0.52)`,

  (* {{{ proof *)
  [
  GEN_TAC;
  REWRITE_TAC[Sphere.rho;Sphere.ly;Sphere.interp;REAL_ARITH `#2.52 - &2 = #0.52`];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)

(* renamed from rho_x to avoid clash with rho_x in sphere.hl *)


let rho_sqrtx = 
prove_by_refinement(
  `!x. rho (sqrt x) = &1 + const1 * (sqrt x - &2) / (#0.52)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[rho_alt];
  ]);;
  (* }}} *)


let lfun_ly = 
prove_by_refinement(
  `!h. lfun h = ly (&2 * h)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.lfun;Sphere.ly;Sphere.interp;Sphere.h0];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let lfun1 = 
prove_by_refinement(
  `lfun (&1) = (&1)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.lfun;Sphere.h0];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let rhazim2_alt = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. rhazim2 y1 y2 y3 y4 y5 y6 = rho y2 * dih2_y y1 y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rhazim2;Sphere.node2_y;Sphere.rhazim;Sphere.dih2_y;];
  MESON_TAC[dih_y_sym];
  ]);;
  (* }}} *)


let rhazim3_alt = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. rhazim3 y1 y2 y3 y4 y5 y6 = rho y3 * dih3_y y1 y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rhazim3;Sphere.node3_y;Sphere.rhazim;Sphere.dih3_y;];
  ]);;
  (* }}} *)


let beta_bump_force_x = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. beta_bump_force_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
    halfbump_x1 x1 x2 x3 x4 x5 x6 - halfbump_x4 x1 x2 x3 x4 x5 x6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.beta_bump_force_y;halfbump_x1;halfbump_x4;halfbump_x];
  ]);;
  (* }}} *)


let halfbump_x_expand = 
prove_by_refinement(
  `!x. &0 <= x ==> (halfbump_x x = 
   -- (&4398119 / &2376200) + (&17500 / &11881) * sqrt x - (&31250 / &106929) * x)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[halfbump_x;Sphere.bump;Sphere.h0;Sphere.hplus];
  REPEAT STRIP_TAC;
  REWRITE_TAC[REAL_ARITH`(a/ &2 - b) pow 2 = (a pow 2) / &4 - a * b + b pow 2`];
  ASM_SIMP_TAC[SQRT_POW_2];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let vol4f_palt = 
prove_by_refinement(
  `!f y1 y2 y3 y4 y5 y6. vol4f y1 y2 y3 y4 y5 y6 f  = 
    (-- &8 * mm1)
    + 
    (&4 * mm1 / pi) * 
    (dih_y y1 y2 y3 y4 y5 y6 + dih2_y y1 y2 y3 y4 y5 y6 +
    dih3_y y1 y2 y3 y4 y5 y6 +
    dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 + 
     dih6_y y1 y2 y3 y4 y5 y6)
    +
    (-- &8 * mm2 / pi) * 
    (f (y1/ &2) * dih_y y1 y2 y3 y4 y5 y6 + 
    f(y2/ &2) * dih2_y y1 y2 y3 y4 y5 y6 +  
    f (y3/ &2) * dih3_y y1 y2 y3 y4 y5 y6 +
    f (y4/ &2) * dih4_y y1 y2 y3 y4 y5 y6 + 
    f(y5/ &2) * dih5_y y1 y2 y3 y4 y5 y6 + 
    f(y6/ &2) * dih6_y y1 y2 y3 y4 y5 y6)
    `,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[Sphere.vol4f;Sphere.sol_y;lfun_ly;REAL_ARITH `&2 * y / &2 = y`;Sphere.rhazim;rhazim2_alt;rhazim3_alt;Sphere.rhazim4;Sphere.rhazim5;Sphere.rhazim6;];
  SUBGOAL_THEN `dih_y y2 y3 y1 y5 y6 y4 = dih2_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y3 y1 y2 y6 y4 y5 = dih3_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y3 y1 y2 y6 y4 y5 = dih3_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y4 y3 y5 y1 y6 y2 = dih4_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y5 y1 y6 y2 y4 y3 = dih5_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y6 y1 y5 y3 y4 y2 = dih6_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y6 y4 y2 y3 y1 y5 = dih6_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y2 y6 y4 y5 y3 y1 = dih2_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y1 y5 y6  y4 y2 y3 = dih_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y5 y6 y1 y2 y3 y4 = dih5_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y4 y5 y3 y1 y2 y6 = dih4_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y5 y3 y4 y2 y6 y1 = dih5_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y3 y4 y5 y6 y1 y2 = dih3_y y1 y2 y3 y4 y5 y6 /\ 
   dih_y y4 y2 y6 y1 y5 y3 = dih4_y y1 y2 y3 y4 y5 y6` (fun t-> REWRITE_TAC[t]);
  REWRITE_TAC[Sphere.dih2_y;Sphere.dih3_y;Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y];
  MESON_TAC[dih_y_sym;dih_y_sym2];
  ONCE_REWRITE_TAC[REAL_ARITH `x  = y <=> x - y = &0`];
  ABBREV_TAC `a = mm1/pi `;
  SUBGOAL_THEN `mm1 = a * pi ` (fun t->REWRITE_TAC[t]);
  POP_ASSUM MP_TAC;
  SUBGOAL_THEN  `~(pi = &0)` MP_TAC;
  SIMP_TAC[PI_POS;REAL_ARITH `&0 < x ==> ~(x= &0)`];
  CONV_TAC REAL_FIELD;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)



let edge_flat2_x_rewrite = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x5 /\
    &0 <= x6) ==> (edge_flat2_x x1 x2 x3 x4 x5 x6 = 
    (sqrt (quadratic_root_plus
           (x1,
            (x1) * x1 +
            (x3 - x5) * (x2 - x6) -
            (x1) * (x2 + x3 + x5 + x6),
            (x1) * (x3) * x5 +
            (x1) * (x2) * x6 -
            (x3) *
            (x1 + x2 - x3 + x5 - x6) * x6 -
            (x2) *
            (x5) *
            (x1 - x2 + x3 - x5 + x6)))) pow 2)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.edge_flat2_x];
  REPEAT STRIP_TAC;
  AP_THM_TAC;
  AP_TERM_TAC;
  REWRITE_TAC[edge_flat_rewrite];
  ASM_SIMP_TAC[REAL_ARITH `sqrt x * sqrt x = (sqrt x) pow 2`;SQRT_POW2;SQRT_WORKS];
  ]);;
  (* }}} *)


let edge_quadratic = 
prove_by_refinement(
  `!x1 x2 x3 x5 x6. quadratic_root_plus (x1,
            x1 * x1 +
            (x3 - x5) * (x2 - x6) -
            x1 * (x2 + x3 + x5 + x6),
            x1 * x3 * x5 +
            (x1) * (x2) * x6 -  (x3) * (x1 + x2 - x3 + x5 - x6) * x6 -
	      (x2) * (x5) * (x1 - x2 + x3 - x5 + x6)) =
  (-- (x1 * x1) + x1*x2 + x1*x3 - x2*x3 + x1*x5 + x2*x5 + x1*x6 + x3*x6 - 
  x5*x6 + sqrt(ups_x x1 x3 x5 * ups_x x1 x2 x6))/(&2*x1)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.quadratic_root_plus;Sphere.ups_x];
  REPEAT STRIP_TAC;
  AP_THM_TAC;
  AP_TERM_TAC;
  REWRITE_TAC[REAL_ARITH `--(x1 * x1 + (x3 - x5) * (x2 - x6) - x1 * (x2 + x3 + x5 + x6)) + a = -- (x1 * x1) + x1 * x2 + x1 * x3 - x2 * x3 + x1 * x5 + x2 * x5 + x1 * x6 + x3 * x6 - x5 * x6 + a`];
  REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let lmfun0 = 
prove_by_refinement(
  `!y. &2 * h0 <= y ==> (lmfun (y/ &2)  = &0)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.lmfun;REAL_ARITH `&2 * h0 <= y <=> (~(y/ &2 <= h0) \/ (y/ &2 = h0))`];
  GEN_TAC;
  DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `h0 <= h0`;REAL_FIELD `(h0 - h0)/(h0 - &1) = &0`];
  ]);;
  (* }}} *)


let lmfun_lfun = 
prove_by_refinement(
  `!y. y <= &2 * h0 ==> (lmfun (y/ &2) = lfun(y/ &2))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.lmfun;Sphere.lfun;REAL_ARITH `y <= &2 * h0 <=> y/ &2 <= h0`];
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
  ]);;
  (* }}} *)


let lmfun_lfun2 = 
prove_by_refinement(
  `!y. y <=  h0 ==> (lmfun (y) = lfun(y))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.lmfun;Sphere.lfun];
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
  ]);;
  (* }}} *)

(* compute hminus *)


let quartic_has_real_derivative = 
prove_by_refinement(
  `!x c0 c1 c2 c3 c4 . ((\x. c0 * &1 + c1 * x pow 1 + c2 * x pow 2 + c3 * x pow 3 + c4 * x pow 4) has_real_derivative (c0 * &0 + c1 * (&1 * x pow (1-1) * &1) + c2 * (&2 * x pow (2-1)) * &1 + c3 * (&3 * x pow (3-1)) * &1 + c4 * (&4 * x pow (4-1)) * &1)) (atreal x)`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC THEN 
REPEAT (MATCH_MP_TAC HAS_REAL_DERIVATIVE_ADD THEN CONJ_TAC) THEN MATCH_MP_TAC (HAS_REAL_DERIVATIVE_LMUL_ATREAL) THEN REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]  THEN REWRITE_TAC[REAL_ARITH `(a * b) * c = a * b * (c:real)`] THEN MATCH_MP_TAC (HAS_REAL_DERIVATIVE_POW_ATREAL) THEN REWRITE_TAC[HAS_REAL_DERIVATIVE_ID];
  ]);;
  (* }}} *)

let POLY_CONTINUITY_TAC =  
 REPEAT (MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN 
 CONJ_TAC) THEN 
 REPEAT (MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL) THEN 
 (MATCH_MP_TAC REAL_CONTINUOUS_ON_POW) THEN 
 REWRITE_TAC[REAL_CONTINUOUS_ON_ID];;


let quartic_continuous_on = 
prove_by_refinement(
  `!s c0 c1 c2 c3 c4 .  (\x. c0 * x pow 0 + c1 * x pow 1 + c2 * x pow 2 + c3 * x pow 3 + c4 * x pow 4) real_continuous_on s`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  POLY_CONTINUITY_TAC;
  ]);;
  (* }}} *)


let marchal_minus_lfun = 
prove_by_refinement(
  `!h. marchal_quartic h - lfun h = 
   (inv(&65 * &1627 * (sqrt(&2) - &1))) * (h - &1)*
    (( -- &512505 + &770958*sqrt(&2)) * h pow 0 + 
    ( -- &364208 -  &1295359*sqrt(&2)) * h pow 1 +
   ( &1295359 + &585000*sqrt(&2))* h pow 2 + 
   (-- &585000) * h pow 3)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.marchal_quartic;Sphere.lfun;REAL_ARITH `x/y = x * inv y /\ #1.26 - &1 = &13/ &50 /\ #1.3254 - &1 = &1627/ &5000 /\ &65 = &5 * &13`;REAL_INV_INV;REAL_INV_MUL;Sphere.hplus;Sphere.h0];
  GEN_TAC;
  SUBGOAL_THEN `&0 < sqrt(&2) - &1 ` MP_TAC THENL [ALL_TAC;CONV_TAC REAL_FIELD];
  SUBGOAL_THEN `#1.414213 < sqrt(&2) ` MP_TAC THENL[ALL_TAC;REAL_ARITH_TAC];
  REWRITE_TAC[GSYM Sphere.sqrt2;Flyspeck_constants.bounds];
  ]);;
  (* }}} *)


let hminus_cont = 
prove_by_refinement(
  `!s. (\h. marchal_quartic h - lfun h) real_continuous_on s`,

  (* {{{ proof *)
  [
  GEN_TAC;
  REWRITE_TAC[marchal_minus_lfun];
  MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL;
 MATCH_MP_TAC REAL_CONTINUOUS_ON_MUL THEN REWRITE_TAC[REAL_ARITH `h - &1 = (-- &1) * h pow 0 + &1 * h pow 1`] THEN CONJ_TAC THEN POLY_CONTINUITY_TAC;
  ]);;
  (* }}} *)


let sqrt2_lb = 
prove_by_refinement(
  `#1.414213 < sqrt2 `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Flyspeck_constants.bounds];
  ]);;
  (* }}} *)

let STRIP_NN_TAC = REPEAT (CONJ_TAC ORELSE MATCH_MP_TAC REAL_LE_MUL ORELSE CHANGED_TAC (REWRITE_TAC[REAL_LE_INV_EQ;REAL_ARITH `a >= &0 <=> &0 <= a /\ ((a*b)*c = a*b*c)`;REAL_INV_MUL]));;


let hminus_exists = 
prove_by_refinement(
  `?x. (#1.2 <= x /\ x < #1.3 /\ marchal_quartic x = lmfun x)`,

  (* {{{ proof *)
  [
    SUBGOAL_THEN `(?x. x IN real_interval [#1.2,#1.26] /\ (\x. marchal_quartic x - lfun x) x = &0)` MP_TAC;
    MATCH_MP_TAC REAL_IVT_INCREASING;
    BETA_TAC;
    REWRITE_TAC[hminus_cont];
    REWRITE_TAC[marchal_minus_lfun;GSYM Sphere.sqrt2];
   ASSUME_TAC sqrt2_lb;
   SUBGOAL_THEN `&0 < sqrt2 - &1` ASSUME_TAC;
   POP_ASSUM MP_TAC;
   REAL_ARITH_TAC;
   REWRITE_TAC[(* REAL_INV_MUL;REAL_INV_INV; *) REAL_ARITH `#1.2- &1 = &1 / &5 /\ #1.26 - &1 = &13 / &50`];
    CONJ_TAC THENL[REAL_ARITH_TAC;ALL_TAC];
    SUBGOAL_THEN `sqrt2 < #1.414214` ASSUME_TAC;
   REWRITE_TAC[Flyspeck_constants.bounds];
   SUBGOAL_THEN ` ((-- &512505 + &770958 * sqrt2) * #1.26 pow 0 +  (-- &364208 - &1295359 * sqrt2) * #1.26 pow 1 +  (&1295359 + &585000 * sqrt2) * #1.26 pow 2 +  -- &585000 * #1.26 pow 3) = -- &212787729/ &2500 + &3377583 *sqrt2 /(&50)` (fun t-> REWRITE_TAC[t]);
   REAL_ARITH_TAC;
   SUBGOAL_THEN `((-- &512505 + &770958 * sqrt2) * #1.2 pow 0 +  (-- &364208 - &1295359 * sqrt2) * #1.2 pow 1 +  (&1295359 + &585000 * sqrt2) * #1.2 pow 2 +  -- &585000 * #1.2 pow 3) = -- &2377941/ &25 + (& 294636* sqrt2)/ &5`  (fun t-> REWRITE_TAC[t]);
   REAL_ARITH_TAC;
   REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> (&0 <= a * b * (-- c))`];
   STRIP_NN_TAC THEN (REPEAT (POP_ASSUM MP_TAC)) THEN TRY REAL_ARITH_TAC; 
   (* last subgoal *)
   REWRITE_TAC[real_interval;IN_ELIM_THM];
   REPEAT STRIP_TAC;
   EXISTS_TAC `x:real`;
   SUBGOAL_THEN `x <= &2 * h0` ASSUME_TAC;
   REWRITE_TAC[Sphere.h0];
   UNDISCH_TAC `x <= #1.26` THEN REAL_ARITH_TAC;
   ASM_SIMP_TAC [Sphere.h0;lmfun_lfun2];
   REPEAT (POP_ASSUM MP_TAC);
   REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let hminus_prop = 
prove_by_refinement(
  `#1.2 <= hminus /\ hminus < #1.3 /\ marchal_quartic hminus = lmfun hminus`,

  (* {{{ proof *)
  [
  MP_TAC hminus_exists;
  MP_TAC Sphere.hminus;
  MESON_TAC[];
  ]);;
  (* }}} *)


let hminus_high = 
prove_by_refinement(
  `!h. (h0 <= h) ==> lmfun h = &0`,

  (* {{{ proof *)
  [
    REWRITE_TAC[Sphere.lmfun;REAL_ARITH `h0 <= h <=> (~(h <= h0) \/ (h = h0))`];
  GEN_TAC;
  DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `h0 <= h0`;REAL_FIELD `(h0 - h0)/(h0 - &1) = &0`];
  ]);;
  (* }}} *)


let hminus_lt_h0 = 
prove_by_refinement(
  `!h. (&1 <= h) /\ (h < hplus) ==> (marchal_quartic h > &0)`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  REWRITE_TAC[Sphere.marchal_quartic];
  REWRITE_TAC[REAL_ARITH `(h-hplus)*(&9 * h pow 2 - &17 * h + &3)/u = (hplus - h)*(&17 * h - &9 * h pow 2 -  &3)/u /\ (u > &0 <=> &0 < u)`];
  MATCH_MP_TAC REAL_LT_MUL;
  CONJ_TAC;
  POP_ASSUM MP_TAC;
  SUBGOAL_THEN `&0 < sqrt(&2) - hplus` MP_TAC;
  REWRITE_TAC[Flyspeck_constants.bounds];
  REAL_ARITH_TAC;
MATCH_MP_TAC REAL_LT_MUL;
  CONJ_TAC;
  POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  MATCH_MP_TAC REAL_LT_DIV;
  REWRITE_TAC[Flyspeck_constants.bounds];
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[Sphere.hplus];
  ABBREV_TAC `u = h - &1`;
  SUBGOAL_THEN `h = u + &1` (fun t->REWRITE_TAC[t]);
  POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_FIELD `(&1 <= u + &1 <=> &0 <= u) /\ (u + &1 < #1.3254 <=> u < #0.3254) /\ (&17 * (u + &1) - &9 * (u+ &1) pow 2 - &3 = -- &9 * u pow 2 - u + &5)`];
  POP_ASSUM (fun t->ALL_TAC);
  REPEAT STRIP_TAC;
  SUBGOAL_THEN `u pow 2 < #0.3254 pow 2` MP_TAC;
  REWRITE_TAC[ GSYM REAL_LT_SQUARE_ABS];
  REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
  REPEAT (POP_ASSUM MP_TAC);
  ABBREV_TAC `v = u pow 2`;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let hminus_lt_h0 = 
prove_by_refinement(
  `hminus < h0`,

  (* {{{ proof *)
  [
  REWRITE_TAC [REAL_ARITH `x < y <=> ~(x >= y)`];
  STRIP_TAC;
  MP_TAC hminus_prop;
  REPEAT STRIP_TAC;
  POP_ASSUM MP_TAC;
  MATCH_MP_TAC (REAL_ARITH `a > b ==>((a:real) = b ==> F)`);
  SUBGOAL_THEN `lmfun hminus = &0` (fun t -> REWRITE_TAC[t]);
  MATCH_MP_TAC hminus_high;
  UNDISCH_TAC `hminus >= h0` THEN REAL_ARITH_TAC;
  MATCH_MP_TAC   hminus_lt_h0;
  REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[Sphere.hplus;Sphere.h0];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let h0_lt_hplus = 
prove_by_refinement(
  `h0 < hplus`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.h0;Sphere.hplus];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let hminus_gt = 
prove_by_refinement(
  `#1.2 <= hminus`,

  (* {{{ proof *)
  [
  REWRITE_TAC[hminus_prop];
  ]);;
  (* }}} *)


let lminus_ge_h0 = 
prove_by_refinement(
  `!h. (hplus <= h) /\ (h <= sqrt (&2)) ==> (marchal_quartic h <= &0)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.marchal_quartic];
  REWRITE_TAC[REAL_ARITH `a * b * c /d <= &0 <=> &0 <= a * b * (-- c)/d`];
  REPEAT STRIP_TAC;
  MATCH_MP_TAC REAL_LE_MUL;
  CONJ_TAC;
  POP_ASSUM MP_TAC;
  REAL_ARITH_TAC;
  MATCH_MP_TAC REAL_LE_MUL;
  CONJ_TAC;
  REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
  MATCH_MP_TAC REAL_LE_DIV;
  CONJ_TAC;
  (* *)
    REPEAT (POP_ASSUM MP_TAC);
  REWRITE_TAC[Sphere.hplus];
  ABBREV_TAC `u = h - &1`;
  SUBGOAL_THEN `h = u + &1` (fun t->REWRITE_TAC[t]);
  POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  REWRITE_TAC[REAL_FIELD `(&1 <= u + &1 <=> &0 <= u) /\ (#1.3254 <= u + &1 <=>  #0.3254 <= u) /\ (-- (&9* (u + &1) pow 2 - &17 * (u+ &1)  + &3) = -- &9 * u pow 2 - u + &5)`];
  REPEAT STRIP_TAC;
  SUBGOAL_THEN `u pow 2 < #0.42 pow 2` MP_TAC;
  REWRITE_TAC[ GSYM REAL_LT_SQUARE_ABS];
  POP_ASSUM MP_TAC;
  POP_ASSUM MP_TAC;
  EXPAND_TAC "u";
  SUBGOAL_THEN `sqrt(&2) - &1 < #0.42` (fun t-> (MP_TAC t) THEN REAL_ARITH_TAC);
  SUBGOAL_THEN `sqrt(&2) <  #1.414214` MP_TAC;
  REWRITE_TAC[GSYM Sphere.sqrt2;Flyspeck_constants.bounds];
  REAL_ARITH_TAC;
  SUBGOAL_THEN `u < #0.414214` MP_TAC;
  SUBGOAL_THEN `sqrt(&2) <  #1.414214` MP_TAC;
  REWRITE_TAC[GSYM Sphere.sqrt2;Flyspeck_constants.bounds];
  POP_ASSUM MP_TAC;
  REAL_ARITH_TAC;
  REAL_ARITH_TAC;
  MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`);
  REWRITE_TAC[Flyspeck_constants.bounds];
  ]);;
  (* }}} *)


let gcy_high  = 
prove_by_refinement(
  `!y. (&2 * h0 <= y) ==> (gcy y = &4 * mm1/pi)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.gcy];
  SIMP_TAC[lmfun0];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let gcy_low = 
prove_by_refinement(
  `!y. (y <= &2 * h0) ==> (gcy y = gchi y)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.gcy;Sphere.gchi];
  SIMP_TAC[lmfun_lfun];
  REWRITE_TAC[Sphere.lfun;Sphere.h0];
  REPEAT STRIP_TAC;
  ABBREV_TAC `m = mm2/pi`;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let gcy_low_hminus = 
prove_by_refinement(
  `!y. (y <= &2 * hminus) ==> (gcy y = gchi y)`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  MATCH_MP_TAC gcy_low;
  POP_ASSUM MP_TAC;
  MP_TAC hminus_lt_h0;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let c2001 = 
prove_by_refinement(
  `!y. (y <= #2.001) ==> (y <= &2 * h0)`,

  [
    REWRITE_TAC[Sphere.h0];
  REAL_ARITH_TAC;
  ]
);;


let gcy_low_const = 
prove_by_refinement(
  `!y. (y <= #2.001) ==> (gcy y = gchi y)`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  MATCH_MP_TAC gcy_low;
  POP_ASSUM MP_TAC;
  REWRITE_TAC[Sphere.h0];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let gcy_high_hplus = 
prove_by_refinement(
  `!y. (&2 * hplus <= y) ==> (gcy y = &4 * mm1/pi)`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  MATCH_MP_TAC gcy_high;
  FIRST_X_ASSUM MP_TAC;
  MP_TAC h0_lt_hplus;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let hm0 = 
prove_by_refinement(
  `!y. ((y <= &2 * hminus) ==> (y <= &2 * h0))`,

  (* {{{ proof *)
  [
   MP_TAC hminus_lt_h0;
  CONV_TAC REAL_FIELD;
  ]);;
  (* }}} *)


let h0_lt_gt = 
prove_by_refinement(
  `((y <= #2.01) ==> (y <= &2 * h0)) /\
   ((#2.8 <= y) ==> (&2 * h0 <= y)) /\
  (( y <= &2) ==> (y <= &2 * h0)) /\
    ((sqrt8 <= y) ==> (&2 * h0 <= y)) /\   ((&2 * h0 <= y) ==> (&0 <= y)) /\
   ((&2 <= y) ==> (&0 <= y)) /\
   ((y <= &2 * hminus) ==> (y <= &2 * h0)) /\
   ((&2 * hminus <= y) ==> (&0 <= y))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.h0;sqrt8_sqrt2;hm0];
    MP_TAC sqrt2_lb;
  MP_TAC hminus_gt;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let sqrtxx = 
prove_by_refinement(
  `!x. &0 <= x ==> (sqrt(x * x) = x)`,

  (* {{{ proof *)
  [
    REWRITE_TAC[POW_2_SQRT_ABS;REAL_ARITH `x * x = x pow 2`];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let lmdih_ldih = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. (&0 <= y1 /\ y1 <= &2 * h0) ==>(y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  y_of_x ldih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 )`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch];
  MESON_TAC[sqrtxx;lmfun_lfun];
  ]);;
  (* }}} *)


let lmdih3_ldih3 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. (&0 <= y3 /\ y3 <= &2 * h0) ==>(y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  y_of_x ldih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 )`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rotate3;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch;Sphere.y_of_x;Nonlin_def.lmdih3_x_div_sqrtdelta_posbranch;Nonlin_def.ldih3_x_div_sqrtdelta_posbranch];
  MESON_TAC[sqrtxx;lmfun_lfun];
  ]);;
  (* }}} *)


let lmdih5_ldih5 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. (&0 <= y5 /\ y5 <= &2 * h0) ==>(y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  y_of_x ldih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 )`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.rotate5;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch;Sphere.y_of_x;Nonlin_def.lmdih5_x_div_sqrtdelta_posbranch;Nonlin_def.ldih5_x_div_sqrtdelta_posbranch];
  MESON_TAC[sqrtxx;lmfun_lfun];
  ]);;
  (* }}} *)

let lmdih_ldih' = REWRITE_RULE[Sphere.y_of_x] lmdih_ldih;;
let lmdih3_ldih3' = REWRITE_RULE[Sphere.y_of_x] lmdih3_ldih3;;
let lmdih5_ldih5' = REWRITE_RULE[Sphere.y_of_x] lmdih5_ldih5;;


let lmdih0 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y1 ) ==>(y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  &0 )`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch];
  MESON_TAC[sqrtxx;lmfun0;REAL_ARITH `&0 * x = &0 `;h0_lt_gt];
  ]);;
  (* }}} *)


let lmdih3_0 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y3 ) ==>(y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  &0 )`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Nonlin_def.lmdih3_x_div_sqrtdelta_posbranch;Sphere.rotate3;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch];
  MESON_TAC[sqrtxx;lmfun0;REAL_ARITH `&0 * x = &0 `;h0_lt_gt];
  ]);;
  (* }}} *)


let lmdih5_0 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y5 ) ==>(y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  &0 )`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Nonlin_def.lmdih5_x_div_sqrtdelta_posbranch;Sphere.rotate5;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch];
  MESON_TAC[sqrtxx;lmfun0;REAL_ARITH `&0 * x = &0 `;h0_lt_gt];
  ]);;
  (* }}} *)

let lmdih1_0' = REWRITE_RULE[Sphere.y_of_x] lmdih0;;
let lmdih3_0' = REWRITE_RULE[Sphere.y_of_x] lmdih3_0;;
let lmdih5_0' = REWRITE_RULE[Sphere.y_of_x] lmdih5_0;;


let vol4f_lmfun = 
prove_by_refinement(
  `! y1 y2 y3 y4 y5 y6. vol4f y1 y2 y3 y4 y5 y6 lmfun  = 
    (-- &8 * mm1)
    + 
    gcy y1 * dih_y y1 y2 y3 y4 y5 y6 + gcy y2 * dih2_y y1 y2 y3 y4 y5 y6 +
    gcy y3 * dih3_y y1 y2 y3 y4 y5 y6 +
    gcy y4 * dih4_y y1 y2 y3 y4 y5 y6 + 
      gcy y5 * dih5_y y1 y2 y3 y4 y5 y6 + 
    gcy y6 * dih6_y y1 y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
    REWRITE_TAC[vol4f_palt;Sphere.gcy];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let gamma4fgcy_alt = 
prove_by_refinement(`gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun =
    vol_y y1 y2 y3 y4 y5 y6 - 
    ((-- &8 * mm1)
    + 
    gcy y1 * dih_y y1 y2 y3 y4 y5 y6 + gcy y2 * dih2_y y1 y2 y3 y4 y5 y6 +
    gcy y3 * dih3_y y1 y2 y3 y4 y5 y6 +
    gcy y4 * dih4_y y1 y2 y3 y4 y5 y6 + 
      gcy y5 * dih5_y y1 y2 y3 y4 y5 y6 + 
    gcy y6 * dih6_y y1 y2 y3 y4 y5 y6)`,

[
REWRITE_TAC[Sphere.gamma4fgcy;Sphere.gamma4f;vol4f_lmfun];
]);;


let vol3f_palt = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6 r f. 
      (y3 = r) /\ (y4 = r) /\ (y5 = r) ==>
     (vol3f y1 y2 y6 r f =       (&2 * mm1 / pi) *
         (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
          &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
	  dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
         (&8 * mm2 / pi) *
         (f (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
          f (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
          f (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6))`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[Sphere.vol3f;Sphere.sol_y];
  DISCH_THEN (fun t->REWRITE_TAC[t]);
  REWRITE_TAC[Sphere.dih2_y;Sphere.dih3_y;Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y];
  ABBREV_TAC `a = &8 * mm2/pi`;
  ABBREV_TAC `b = &2 * mm1/pi`;
  SUBGOAL_THEN `dih_y y2 r y1 r y6 r = dih_y y2 y1 r r r y6 /\ dih_y y2 y6 r r r y1 = dih_y y2 y1 r r r y6 /\ dih_y y6 r y2 r y1 r = dih_y y6 y1 r r r y2 /\  dih_y y1 r y6 r y2 r = dih_y y1 y2 r r r y6 /\ dih_y r y6 y1 y2 r r = dih_y r y1 y6 y2 r r` (fun t->REWRITE_TAC[t]);
 MESON_TAC[dih_y_sym2;dih_y_sym];
 MATCH_MP_TAC (REAL_ARITH `(a = a') ==> (a - c = a' - c)`);
 REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let vol3f_135_palt = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6 r f. 
      (y2 = r) /\ (y4 = r) /\ (y6 = r) ==>
     (vol3f y1 y3 y5 r f =       (&2 * mm1 / pi) *
         (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih3_y y1 y2 y3 y4 y5 y6 +
          &2 * dih5_y y1 y2 y3 y4 y5 y6 + dih2_y y1 y2 y3 y4 y5 y6 +
	  dih4_y y1 y2 y3 y4 y5 y6 + dih6_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
         (&8 * mm2 / pi) *
         (f (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
          f (y3 / &2) * dih3_y y1 y2 y3 y4 y5 y6 +
          f (y5 / &2) * dih5_y y1 y2 y3 y4 y5 y6))`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[Sphere.vol3f;Sphere.sol_y];
  DISCH_THEN (fun t->REWRITE_TAC[t]);
  REWRITE_TAC[Sphere.dih2_y;Sphere.dih3_y;Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y];
  ABBREV_TAC `a = &8 * mm2/pi`;
  ABBREV_TAC `b = &2 * mm1/pi`;
  SUBGOAL_THEN `dih_y y3 r y1 r y5 r = dih_y y3 y5 r r r y1 /\ dih_y y5 r y3 r y1 r = dih_y y5 y1 r r r y3 /\ dih_y y1 r y5 r y3 r = dih_y y1 y3 r r r y5 /\ dih_y y1 r y3 r y5 r = dih_y y1 y3 r r r y5 /\ dih_y y3 y1 r r r y5 = dih_y y3 y5 r r r y1 /\ dih_y r r r y1 y5 y3 = dih_y r y3 y5 y1 r r /\ dih_y r y1 y5 y3 r r = dih_y r y5 y1 y3 r r` (fun t->REWRITE_TAC[t]);
 MESON_TAC[dih_y_sym2;dih_y_sym];
 MATCH_MP_TAC (REAL_ARITH `(a = a') ==> (a - c = a' - c)`);
 REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let vol3r_alt = 
prove_by_refinement(
  `! y1 y2 y3 y4 y5 y6 r. (y3 = r ) /\ (y4 = r) /\ (y5 = r) ==> 
   (vol3r y1 y2 y6 r  = vol_y y1 y2 y3 y4 y5 y6)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.vol3r;Sphere.vol_y;Sphere.y_of_x;Sphere.vol_x;Sphere.delta_x];
  REPEAT GEN_TAC;
  DISCH_THEN (fun t->REWRITE_TAC[t]);
  AP_THM_TAC;
  AP_TERM_TAC;
  AP_TERM_TAC;
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)

(* a few lemmas copied  from TameGeneral *)


let COS_PI3 = 
prove(`cos (pi / &3) = &1 / &2`,

   REWRITE_TAC[COS_SIN] THEN
     REWRITE_TAC[REAL_ARITH `pi / &2 - pi / &3 = pi / &6`] THEN
     REWRITE_TAC[SIN_PI6]);;


let ACS_2 = 
prove(`acs (&1 / &2) = pi / &3`,

   REWRITE_TAC[SYM COS_PI3] THEN
     MATCH_MP_TAC ACS_COS THEN
     REWRITE_TAC[REAL_ARITH `(&0 <= a / &3 <=> &0 <= a) /\ (a / &3 <= a <=> &0 <= a)`] THEN
     MATCH_MP_TAC REAL_LT_IMP_LE THEN
     REWRITE_TAC[PI_POS]);;


let sol0_POS = 
prove(`&0 < sol0`,

   REWRITE_TAC[Sphere.sol0] THEN
     REWRITE_TAC[REAL_ARITH `&0 < &3 * a - pi <=> pi / &3 < a`] THEN
     REWRITE_TAC[SYM ACS_2] THEN
     MATCH_MP_TAC ACS_MONO_LT THEN
     REAL_ARITH_TAC);;


let vol4f_alt = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. vol4f y1 y2 y3 y4 y5 y6 lfun  = 
    (-- &8 * mm1)
    + 
    (&4 * mm1/pi - &8 * mm2 *(&1+const1)/(pi * const1) ) *
    (dih_y y1 y2 y3 y4 y5 y6 + dih2_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
    dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 + dih6_y y1 y2 y3 y4 y5 y6)
    +
    (&8 * mm2 / (pi * const1)) * 
    (rhazim y1 y2 y3 y4 y5 y6 + rhazim2 y1 y2 y3 y4 y5 y6 + rhazim3 y1 y2 y3 y4 y5 y6 +
    rhazim4 y1 y2 y3 y4 y5 y6 + rhazim5 y1 y2 y3 y4 y5 y6 + rhazim6 y1 y2 y3 y4 y5 y6)
    `,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
    REWRITE_TAC[vol4f_palt];
  REWRITE_TAC[Sphere.sol_y;lfun_ly;REAL_ARITH `&2 * y / &2 = y`;Sphere.rhazim;rhazim2_alt;rhazim3_alt;Sphere.rhazim4;Sphere.rhazim5;Sphere.rhazim6;];
  REWRITE_TAC[Sphere.rho;Sphere.node2_y;Sphere.node3_y;Sphere.rhazim];
  ONCE_REWRITE_TAC[REAL_ARITH `x  = y <=> x - y = &0`];
  SUBGOAL_THEN  `~(pi = &0)` ASSUME_TAC;
  SIMP_TAC[PI_POS;REAL_ARITH `&0 < x ==> ~(x= &0)`];
  SUBGOAL_THEN `~(const1 = &0)`   MP_TAC;
  REWRITE_TAC[GSYM sol0_over_pi_EQ_const1];
  MP_TAC sol0_POS;
  FIRST_X_ASSUM MP_TAC;
  CONV_TAC REAL_FIELD;
  FIRST_X_ASSUM MP_TAC;
  CONV_TAC REAL_FIELD;
  ]);;
  (* }}} *)


let vol2f_marchal_pow_y = 
prove_by_refinement(
  `!r y. vol2f y r marchal_quartic = 
       let fac = (-- (&8 * mm2/pi) * &2 * pi * inv ( #1.627 * (sqrt2 - &1)))  in 
    (&2 * mm1 / pi)  * &2 * pi 
     - (&2 * mm1 /pi) * &2 * pi * inv(r * &2) * y pow 1
   - fac * &3 * sqrt2 *hplus 
    + fac *(#1.5 * sqrt2 + #1.5 * hplus + #8.5 * sqrt2 * hplus) * y pow 1
   + fac * (-- #0.75  - #8.5 * sqrt2 * inv(&2) - #8.5 * hplus * inv(&2) - &9 * hplus * sqrt2 * inv (&4)) * y pow 2 
    + fac* ( #17.0 * inv (&8) + #9.0 * sqrt2 * inv(&8) + #9.0 * hplus * inv(&8)) * y pow 3 
    - fac * #9.0 * inv(&16) * y pow 4`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.vol2f;Sphere.marchal_quartic;LET_DEF;LET_END_DEF;Sphere.hplus;GSYM Sphere.sqrt2;REAL_ARITH `(sqrt2 - &1) * &5 * (#1.3254 - &1) = #1.627 * (sqrt2- &1)`];
    REPEAT GEN_TAC;
  REWRITE_TAC[GSYM Sphere.hplus;real_div];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let vol2r_y = 
prove_by_refinement(
  `!y r. vol2r y r = &2 * pi * r * r * inv (&3) - #0.5 * pi * inv(&3) * y pow 2`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.vol2r;real_div];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let ineq_expand6 = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 b1 b2 b3 b4 b5 b6 x1 x2 x3 x4 x5 x6 P. (ineq [(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6)] P) <=> 
  (a1 <= y1 /\ y1 <= b1
     ==> a2 <= y2 /\ y2 <= b2
     ==> a3 <= y3 /\ y3 <= b3
     ==> a4 <= y4 /\ y4 <= b4
     ==> a5 <= y5 /\ y5 <= b5
     ==> a6 <= y6 /\ y6 <= b6
     ==> P)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[ineq];
  ]);;
  (* }}} *)


let ineq_expand9 = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 a6 a7 a8 a9 b1 b2 b3 b4 b5 b6 b7 b8 b9 x1 x2 x3 x4 x5 x6 x7 x8 x9 P. (ineq [(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6);(a7,y7,b7);(a8,y8,b8);(a9,y9,b9)] P) <=> 
  (a1 <= y1 /\ y1 <= b1
     ==> a2 <= y2 /\ y2 <= b2
     ==> a3 <= y3 /\ y3 <= b3
     ==> a4 <= y4 /\ y4 <= b4
     ==> a5 <= y5 /\ y5 <= b5
     ==> a6 <= y6 /\ y6 <= b6
     ==> a7 <= y7 /\ y7 <= b7
     ==> a8 <= y8 /\ y8 <= b8
     ==> a9 <= y9 /\ y9 <= b9
     ==> P)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[ineq];
  ]);;
  (* }}} *)


let pathL_bound = 
prove_by_refinement(
  `!y a.  FST (pathL a) <= y /\ y <= SND (pathL a) ==>
    FST a <= y /\ y <= SND a`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
    SUBGOAL_THEN `pathL a = pathL (FST a, SND a)` (fun t->ONCE_REWRITE_TAC[t]);
  REWRITE_TAC[PAIR];
    REWRITE_TAC[Sphere.pathL];
    REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let pathR_bound = 
prove_by_refinement(
  `!y a. FST (pathR a) <= y /\ y <= SND (pathR a) ==>
    FST a <= y /\ y <= SND a`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
    SUBGOAL_THEN `pathR a = pathR (FST a, SND a)` (fun t->ONCE_REWRITE_TAC[t]);
  REWRITE_TAC[PAIR];
    REWRITE_TAC[Sphere.pathR];
    REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let delta_x_eq0 = 
prove_by_refinement(
  `delta_x (&8) (&4) (&4) (&8) (&4) (&4) = &0 /\
   delta_x (&4) (&8) (&4) (&4) (&8) (&4) = &0
  `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.delta_x];
    REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let delta_x4_eq64 = 
prove_by_refinement(
  `delta_x4 (&8) (&4) (&4) (&8) (&4) (&4) = -- &64 /\
   delta_x4 (&4) (&8) (&4) (&4) (&8) (&4) = &64
  `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.delta_x4];
    REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let atn2_0y = 
prove_by_refinement(
  `atn2 (&0,&64) = pi / &2 /\ atn2 (&0 ,-- &64) = -- pi/ &2`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.atn2;REAL_ARITH `~(abs(&64) < &0) /\ &0 < &64 /\ ~(abs (-- &64) < &0) /\ ~(&0 < -- &64) /\ (-- &64 < &0) /\ (&0 / &64 = &0) /\ (&0 / -- &64 = &0)`;ATN_0];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)

let OR_RULE rule1 rule2 th = try rule1 th with _ -> rule2 th;;

let rec REPEAT_RULE rule =
  fun t -> if can rule t then REPEAT_RULE rule (rule t) else t;;


let vol3f_lmln = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. (y1 <= &2 * h0) /\ (y2 <= &2 * h0) /\ (y6 <= &2 * h0) ==> (vol3f y1 y2 y6 sqrt2 lmfun = vol3f y1 y2 y6 sqrt2 lfun)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.vol3f];
  MESON_TAC[lmfun_lfun];
  ]);;
  (* }}} *)


let vol3_vol_x = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.  
   &0 <= x1 /\ &0 <= x2 /\ &0 <= x6 ==>
    (vol3_x_sqrt x1 x2 x3 x4 x5 x6 = vol_x x1 x2 (&2) (&2) (&2) x6)`,

  (* {{{ proof *)
  [
   MP_TAC (REAL_ARITH `&0 <= &2`);
  ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 pow 2`];
  REPEAT STRIP_TAC;
  REWRITE_TAC[vol3_x_sqrt;Sphere.vol_x;Sphere.vol_y;Sphere.y_of_x;Sphere.sqrt2];
  REPEAT AP_THM_TAC;
  AP_TERM_TAC ;
  AP_TERM_TAC;
  ASM_SIMP_TAC[SPEC `&0` sq_pow2];
  REWRITE_TAC[Sphere.delta_x];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)

let spec0 = SPECL [`&0`;`&0`;`&0`;`&0`;`&0`;`&0`;];;


let vol3f_x_lfun_alt = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.  
   &0 <= x1 /\ &0 <= x2 /\ &0 <= x6 ==>
   vol3f_x_lfun x1 x2 x3 x4 x5 x6 =   (&2 * mm1 / pi) *
             (&2 * dih_x x1 x2 (&2) (&2) (&2) x6 +
              &2 * dih2_x x1 x2 (&2) (&2) (&2) x6 +
              &2 * dih6_x x1 x2 (&2) (&2) (&2) x6 +
              dih3_x x1 x2 (&2) (&2) (&2) x6 +
              dih4_x x1 x2 (&2) (&2) (&2) x6 +
              dih5_x x1 x2 (&2) (&2) (&2) x6 - &3 * pi) -
             (&8 * mm2 / pi) *
             ( ldih_x x1 x2 (&2) (&2) (&2) x6 +
              ldih2_x x1 x2 (&2) (&2) (&2) x6 +
              ldih6_x x1 x2 (&2) (&2) (&2) x6)`,

  (* {{{ proof *)
  [
   MP_TAC (REAL_ARITH `&0 <= &2`);
  ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 pow 2`];
  REPEAT STRIP_TAC;
  REWRITE_TAC[vol3f_x_lfun;];
  MP_TAC (SPECL [`sqrt x1`;`sqrt x2`;`sqrt2`;`sqrt2`;`sqrt2`;`sqrt x6`;`sqrt2`;`lfun`] vol3f_palt);
  REWRITE_TAC[];
  DISCH_THEN (fun t->REWRITE_TAC[t]);
  REWRITE_TAC[Sphere.sqrt2;Sphere.ldih_x;Sphere.ldih2_x;Sphere.ldih6_x;Sphere.dih4_x;Sphere.dih5_x;Sphere.dih6_x];
  ASM_SIMP_TAC[spec0 dih_x_y;spec0 dih2_x_y;spec0 dih3_x_y];
  ]);;
  (* }}} *)

let spech0 = SPECL [`&2 * h0`;`&0`;`&0`;`&0`;`&0`;`&0`;];;


let vol3f_x_sqrt2_lmplus_alt = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.  
   ((&2 * h0) pow 2 <= x1) /\ &0 <= x2 /\ &0 <= x6 ==>
   vol3f_x_sqrt2_lmplus x1 x2 x3 x4 x5 x6 =   (&2 * mm1 / pi) *
             (&2 * dih_x x1 x2 (&2) (&2) (&2) x6 +
              &2 * dih2_x x1 x2 (&2) (&2) (&2) x6 +
              &2 * dih6_x x1 x2 (&2) (&2) (&2) x6 +
              dih3_x x1 x2 (&2) (&2) (&2) x6 +
              dih4_x x1 x2 (&2) (&2) (&2) x6 +
              dih5_x x1 x2 (&2) (&2) (&2) x6 - &3 * pi) -
             (&8 * mm2 / pi) *
             (
              ldih2_x x1 x2 (&2) (&2) (&2) x6 +
              ldih6_x x1 x2 (&2) (&2) (&2) x6)`,

  (* {{{ proof *)
  [
   MP_TAC (REAL_ARITH `&0 <= &2`);
  ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 pow 2`];
  REPEAT STRIP_TAC;
  REWRITE_TAC[vol3f_x_sqrt2_lmplus;vol3f_sqrt2_lmplus];
  REWRITE_TAC[Sphere.sqrt2;Sphere.ldih_x;Sphere.ldih2_x;Sphere.ldih6_x;Sphere.dih4_x;Sphere.dih5_x;Sphere.dih6_x];
  ASM_SIMP_TAC[spech0 dih_x_y;spech0 dih2_x_y;spech0 dih3_x_y];
  ]);;
  (* }}} *)


let vol3f_lm0 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. 
  ( &2 * h0 <= y1) /\ (y2 <= &2 * h0) /\ (y6 <= &2 * h0) ==>
  (vol3f y1 y2 y6 sqrt2 lmfun = vol3f_sqrt2_lmplus y1 y2 y3 y4 y5 y6)`,

  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
  REWRITE_TAC[vol3f_sqrt2_lmplus];
  MP_TAC (SPECL [`y1:real`;`y2:real`;`sqrt2`;`sqrt2`;`sqrt2`;`y6:real`; `sqrt2`;`lmfun`] vol3f_palt);
  REWRITE_TAC[];
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  ASM_SIMP_TAC[lmfun_lfun;lmfun0];
  REWRITE_TAC[REAL_ARITH `&0 * x = &0 /\ &0 + y = y`];
  ]);;
  (* }}} *)


let vol3r_126_x = 
prove_by_refinement(
  `vol3r (sqrt x1) (sqrt x2) (sqrt x6) sqrt2 = vol3_x_sqrt x1 x2 (x3:real) (x4:real) (x5:real) x6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[vol3_x_sqrt;Sphere.vol3r;Sphere.vol_y];
  ]);;
  (* }}} *)


let num1_poly = 
prove_by_refinement(
  `! x1 x2 x3 x4 x5 x6. num1 x1 x2 x3 x4 x5 x6 =
     &64*x1*x4 - &32*x2*x4 - &32*x3*x4 - &4*x1*(x4 pow 2) - &32*x2*x5 + &32*x3*x5 + 
   &4*x2*x4*x5 + &32*x2*x6 - &32*x3*x6 + &4*x3*x4*x6 `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.num1];
  REAL_ARITH_TAC;
  ]);;
  (* }}} *)


let ineq6_of_ineq5 = 
prove_by_refinement(
  `!a1 a2 a3 a4 a5 y1 y2 y3 y4 y5 b1 b2 b3 b4 b5 P. 
((!x1 x2 x3 x4 x5 x6. ineq[(a1,x1,b1);(a2,x2,b2);(a3,x3,b3);(a4,x4,b4);(a5,x5,b5);(&1,x6,&1)] 
   (P x1 x2 x3 x4 x5)) ==> 
    ineq[(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5)]
   (P y1 y2 y3 y4 y5))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[ineq];
  MESON_TAC[REAL_ARITH `&1 <= &1`];
  ]);;
  (* }}} *)


let ineq6_of_ineq1 = 
prove_by_refinement(
  `!a1 y1 b1 P. 
((!x1 x2 x3 x4 x5 x6. ineq[(a1,x1,b1);(&1,x2,&1);(&1,x3,&1);(&1,x4,&1);(&1,x5,&1);(&1,x6,&1)] 
   (P x1)) ==> ineq[(a1,y1,b1)]  (P y1))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[ineq];
  MESON_TAC[REAL_ARITH `&1 <= &1`];
  ]);;
  (* }}} *)


let dih_x_alt = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. dih_x x1 x2 x3 x4 x5 x6 = pi / &2 +
     atn2
     (sqrt (&4 * x1 * delta_x x1 x2 x3 x4 x5 x6),
      --delta_x4 x1 x2 x3 x4 x5 x6) `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.dih_x];
  REPEAT LET_TAC;
  REWRITE_TAC[];
  ]);;
  (* }}} *)

end;;