text_formalization/nonlinear/lemma.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: nonlinear inequalities                                            *)
   5 (* Author:  Thomas Hales     *)
   6 (* Date: 2010-10-17                                                         *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 Definitions and Lemmas used in the generation of interval arithmetic
  11 code from the HOL Light specifications.
  12
  13 *)
  14
  15 (* ========================================================================== *)
  16 (*    DEFINITIONS                                                            *)
  17 (* ========================================================================== *)
  18
  19 module Nonlinear_lemma = struct
  20
  21 let ineq = Sphere.ineq;;
  22
  23 let NONLIN = new_definition `NONLIN = T`;;
  24
  25 let sqrt_x1 = define `sqrt_x1 x1 x2 x3 x4 x5 x6 = sqrt x1`;;
  26
  27 let sqrt_x2 = define `sqrt_x2 x1 x2 x3 x4 x5 x6 = sqrt x2`;;
  28
  29 let sqrt_x3 = define `sqrt_x3 x1 x2 x3 x4 x5 x6 = sqrt x3`;;
  30
  31 let sqrt_x4 = define `sqrt_x4 x1 x2 x3 x4 x5 x6 = sqrt x4`;;
  32
  33 let sqrt_x5 = define `sqrt_x5 x1 x2 x3 x4 x5 x6 = sqrt x5`;;
  34
  35 let sqrt_x6 = define `sqrt_x6 x1 x2 x3 x4 x5 x6 = sqrt x6`;;
  36
  37 let halfbump_x = new_definition `halfbump_x x = bump (sqrt x / &2)`;;
  38
  39 let halfbump_x1 = new_definition `halfbump_x1 x1 x2 x3 x4 x5 x6 = halfbump_x x1`;;
  40
  41 let halfbump_x4 = new_definition `halfbump_x4 x1 x2 x3 x4 x5 x6 = halfbump_x x4`;;
  42
  43 let unit6 = define `unit6 x1 x2 x3 x4 x5 x6 = &1`;;
  44
  45 let proj_x1 = define `proj_x1 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x1`;;
  46
  47 let proj_x2 = define `proj_x2 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x2`;;
  48
  49 let proj_x3 = define `proj_x3 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x3`;;
  50
  51 let proj_x4 = define `proj_x4 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x4`;;
  52
  53 let proj_x5 = define `proj_x5 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x5`;;
  54
  55 let proj_x6 = define `proj_x6 (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = x6`;;
  56
  57 let promote = define `promote f (x1:A) (x2:B) (x3:C) (x4:D) (x5:E) (x6:F) = f x1`;;
  58
  59 let unit0 = define `unit0 = &1`;;
  60
  61 let pow1 = new_definition `pow1 y = y pow 1`;;
  62
  63 let pow2 = new_definition `pow2 y = y pow 2`;;
  64
  65 let pow3 = new_definition `pow3 y = y pow 3`;;
  66
  67 let pow4 = new_definition `pow4 y = y pow 4`;;
  68
  69 let promote_pow2 = new_definition `promote_pow2 x1 (x2:A) (x3:B) (x4:C) (x5:D) (x6:E) = x1 pow 2`;;
  70
  71 let promote_pow3 = new_definition `promote_pow3 x1 (x2:A) (x3:B) (x4:C) (x5:D) (x6:E) = x1 pow 3`;;
  72
  73 let compose6 = new_definition `compose6 f p1 p2 p3 p4 p5 p6
  74   (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
  75   (f:real->real->real->real->real->real->real)
  76   (p1 x1 x2 x3 x4 x5 x6)
  77     (p2 x1 x2 x3 x4 x5 x6)
  78     (p3 x1 x2 x3 x4 x5 x6)
  79     (p4 x1 x2 x3 x4 x5 x6)
  80     (p5 x1 x2 x3 x4 x5 x6)
  81     (p6 x1 x2 x3 x4 x5 x6)`;;
  82
  83 let scale6 = new_definition `scale6 f
  84    (r:real)   (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
  85    (f x1 x2 x3 x4 x5 x6) * r`;;
  86
  87 let quadratic_root_plus_curry =
  88   new_definition `quadratic_root_plus_curry a b c = quadratic_root_plus (a,b,c)`;;
  89
  90 let sq_pow2 = prove_by_refinement(
  91   `!a x. a pow 2 <= x ==> (sqrt x * sqrt x = x)`,
  92   (* {{{ proof *)
  93   [
  94   REWRITE_TAC[GSYM REAL_POW_2;SQRT_POW2];
  95   MESON_TAC[REAL_LE_TRANS;Collect_geom.REAL_LE_SQUARE_POW];
  96   ]);;
  97   (* }}} *)
  98
  99 let sqrt2_sqrt2 = prove_by_refinement(
 100   `sqrt2 * sqrt2 = &2`,
 101   (* {{{ proof *)
 102   [
 103   REWRITE_TAC[Sphere.sqrt2];
 104     MATCH_MP_TAC sq_pow2;
 105   EXISTS_TAC`&0`;
 106   REAL_ARITH_TAC;
 107   ]);;
 108   (* }}} *)
 109
 110 (* SOME DEFINITIONS *)
 111
 112 let vol3f_sqrt2_lmplus = new_definition
 113   `vol3f_sqrt2_lmplus y1 y2 (y3:real) (y4:real) (y5:real) y6 =
 114     (&2 * mm1 / pi) *
 115              (&2 * dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 116               &2 * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 117               &2 * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 118               dih3_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 119               dih4_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 120               dih5_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - &3 * pi) -
 121              (&8 * mm2 / pi) *
 122              (
 123               lfun (y2 / &2) * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 124               lfun (y6 / &2) * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6)`;;
 125
 126 let vol3f_x_sqrt2_lmplus = new_definition
 127   `vol3f_x_sqrt2_lmplus x1 x2 x3 x4 x5 x6 =
 128    vol3f_sqrt2_lmplus (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)      (sqrt x6)`;;
 129
 130 let vol3f_x_lfun = new_definition
 131  `vol3f_x_lfun x1 x2 (x3:real) (x4:real) (x5:real) x6 = vol3f (sqrt x1) (sqrt x2) (sqrt x6)  sqrt2 lfun `;;
 132
 133 let vol3_x_sqrt = new_definition
 134  `vol3_x_sqrt x1 x2 (x3:real) (x4:real) (x5:real) x6  = vol_y sqrt2 sqrt2 sqrt2 (sqrt x1) (sqrt x2) (sqrt x6) `;;
 135
 136 let monomial = new_definition `monomial n1 n2 n3 n4 n5 n6 y1 y2 y3 y4 y5 y6 =
 137    (y1 pow n1) * (y2 pow n2) * (y3 pow n3) * (y4 pow n4) * (y5 pow n5) * (y6 pow n6)`;;
 138
 139 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)`;;
 140
 141 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)`;;
 142
 143
 144 (* ========================================================================== *)
 145 (*    BASIC LEMMAS                                                            *)
 146 (* ========================================================================== *)
 147
 148 let strip_let_tm t = snd(dest_eq(concl(REDEPTH_CONV let_CONV t)));;
 149
 150 let strip_let t = REWRITE_RULE[REDEPTH_CONV let_CONV (concl t )] t;;
 151
 152 let tame_table_d_values = prove_by_refinement(
 153   `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  /\
 154     tame_table_d 6 0 = #0.7578 /\
 155     tame_table_d 3 1 = #0.3789 /\
 156     tame_table_d 2 2 = #0.5518 /\
 157    tame_table_d 1 3 = #0.7247 /\
 158    tame_table_d 0 4 = #0.8976 /\
 159    tame_table_d 5 0 = #0.4819 /\
 160    tame_table_d 4 1 = #0.6548 /\
 161    tame_table_d 3 2 = #0.8277 /\
 162    tame_table_d 2 3 = #1.0006
 163  `,
 164   (* {{{ proof *)
 165   [
 166     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)` ];
 167     REAL_ARITH_TAC;
 168   ]);;
 169   (* }}} *)
 170
 171 let unit0f = prove_by_refinement(
 172   `f x1 x2 x3 x4 x5 x6 * unit0 = f x1 x2 x3 x4 x5 x6`,
 173   (* {{{ proof *)
 174   [
 175   REWRITE_TAC[unit0] THEN REAL_ARITH_TAC
 176   ]);;
 177   (* }}} *)
 178
 179 let sqrt8_sqrt2 = prove_by_refinement(
 180   `sqrt8 = &2 * sqrt2`,
 181   (* {{{ proof *)
 182   [
 183   SIMP_TAC[Sphere.sqrt8;Sphere.sqrt2;SQRT_MUL;
 184            REAL_ARITH `&8 = &2 pow 2 * &2 /\ &0 <= &2 /\ &0 <= &2 pow 2 /\
 185       abs(&2) = &2`;POW_2_SQRT_ABS];
 186   ]);;
 187   (* }}} *)
 188
 189 let sqrt2_sqrt8 = prove_by_refinement(
 190   `sqrt2 = #0.5 * sqrt8`,
 191   (* {{{ proof *)
 192   [
 193   REWRITE_TAC[sqrt8_sqrt2];
 194   REAL_ARITH_TAC;
 195   ]);;
 196   (* }}} *)
 197
 198 let SQRT_MUL_POW_2= prove_by_refinement(`!(a:real) b. (a>= &0) /\ (b>= &0) ==> sqrt((a*a)*b)= a* sqrt(b)`,
 199 [
 200 SIMP_TAC[SQRT_MUL;REAL_LE_SQUARE;real_ge];
 201 MESON_TAC[sq_pow2;REAL_ARITH `&0 pow 2 = &0`];
 202 ]);;
 203
 204 (* sol0 = const1 * pi, repeated from TameGeneral.hl *)
 205 let sol0_EQ_sol_y = prove(`sol0 = sol_y (&2) (&2) (&2) (&2) (&2) (&2)`,
 206     REWRITE_TAC[Sphere.sol0; Sphere.sol_y; Sphere.dih_y; Sphere.dih_x; Sphere.delta_x4; Sphere.delta_x] THEN
 207       CONV_TAC (DEPTH_CONV let_CONV) THEN
 208       CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
 209       MP_TAC (SPEC `&1 / &3` Trigonometry2.acs_atn2) THEN
 210       CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
 211       DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 212       REWRITE_TAC [REAL_ARITH `&3 * (a - b) - c = (a + d) + (a + d) + (a + d) - c <=> --b = d`] THEN
 213       MP_TAC (SPECL [`sqrt (&8 / &9)`; `&1 / &3`] Trigonometry1.ATN2_RNEG) THEN
 214       CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
 215       DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 216       SUBGOAL_THEN `sqrt (&2048) = &48 * sqrt (&8 / &9) /\ -- &16 = &48 * (-- &1 / &3)` ASSUME_TAC THENL
 217       [
 218         MP_TAC (SPECL [`&48`; `&8 / &9`] SQRT_MUL_POW_2) THEN
 219           CONV_TAC (REAL_RAT_REDUCE_CONV);
 220         ALL_TAC
 221       ] THEN
 222       ASM_REWRITE_TAC[] THEN
 223       MATCH_MP_TAC (GSYM Trigonometry1.ATN2_LMUL_EQ) THEN
 224       REAL_ARITH_TAC);;
 225
 226 let sol0_over_pi_EQ_const1 = prove(`sol0 / pi = const1`,
 227    REWRITE_TAC[sol0_EQ_sol_y; Sphere.const1]);;
 228
 229 let sol0_const1 = prove_by_refinement(
 230   `sol0 = pi * const1`,
 231   (* {{{ proof *)
 232   [
 233   REWRITE_TAC[GSYM sol0_over_pi_EQ_const1];
 234   MP_TAC PI_POS;
 235   CONV_TAC REAL_FIELD;
 236   ]);;
 237   (* }}} *)
 238
 239 let ineq_lemma_b = prove_by_refinement(
 240   `!a y b. (&0 <= a  /\  &0 <= b /\  a <= y /\ y <= b)  ==>
 241     a pow 2 <= y pow 2 /\ y pow 2 <= b pow 2 /\ (sqrt (y pow 2) = y)`,
 242   (* {{{ proof *)
 243   [
 244   REPEAT GEN_TAC;
 245     STRIP_TAC;
 246     SUBGOAL_THEN `&0 <= y` MP_TAC;
 247   ASM_MESON_TAC [REAL_LE_TRANS];
 248   ASM_MESON_TAC[Collect_geom.POW2_COND;POW_2_SQRT_ABS;
 249                 REAL_ARITH `&0 <= x ==> (x = abs x)`];
 250   ]);;
 251   (* }}} *)
 252
 253 let ineq_square2  = prove_by_refinement(
 254   `(&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4 /\ &0 <= a5 /\ &0 <= a6 /\
 255       &0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ &0 <= b4 /\ &0 <= b5 /\ &0 <= b6 )
 256    /\
 257     (!x1 x2 x3 x4 x5 x6.
 258        ineq [(a1 pow 2,x1,b1 pow 2);(a2 pow 2,x2,b2 pow 2);(a3 pow 2,x3,b3 pow 2);
 259         (a4 pow 2,x4,b4 pow 2);(a5 pow 2,x5,b5 pow 2);(a6 pow 2,x6,b6 pow 2)]
 260           (P (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6))) ==>
 261     (!y1 y2 y3 y4 y5 y6.
 262       ineq
 263         [(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6)]
 264           (P y1 y2 y3 y4 y5 y6))`,
 265   (* {{{ proof *)
 266   [
 267   REWRITE_TAC[ineq];
 268   REPEAT STRIP_TAC;
 269   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));
 270   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]);
 271   ASM_MESON_TAC[ineq_lemma_b];
 272   REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`];
 273   DISCH_THEN MATCH_MP_TAC;
 274   ASM_MESON_TAC[ineq_lemma_b];
 275   ]);;
 276   (* }}} *)
 277
 278 let ineq_square2_9  = prove_by_refinement(
 279   `(&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4 /\ &0 <= a5 /\ &0 <= a6 /\
 280      &0 <= a7 /\ &0 <= a8 /\ &0 <= a9 /\
 281       &0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ &0 <= b4 /\ &0 <= b5 /\ &0 <= b6 /\
 282     &0 <= b7 /\ &0 <= b8 /\ &0 <= b9
 283 )
 284    /\
 285     (!x1 x2 x3 x4 x5 x6 x7 x8 x9.
 286        ineq [(a1 pow 2,x1,b1 pow 2);(a2 pow 2,x2,b2 pow 2);(a3 pow 2,x3,b3 pow 2);
 287         (a4 pow 2,x4,b4 pow 2);(a5 pow 2,x5,b5 pow 2);(a6 pow 2,x6,b6 pow 2);
 288         (a7 pow 2,x7,b7 pow 2);(a8 pow 2,x8,b8 pow 2);(a9 pow 2,x9,b9 pow 2)]
 289           (P (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) (sqrt x7) (sqrt x8) (sqrt x9))) ==>
 290     (!y1 y2 y3 y4 y5 y6 y7 y8 y9.
 291       ineq
 292         [(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)]
 293           (P y1 y2 y3 y4 y5 y6 y7 y8 y9))`,
 294   (* {{{ proof *)
 295   [
 296   REWRITE_TAC[ineq];
 297   REPEAT STRIP_TAC;
 298   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));
 299   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]);
 300   ASM_MESON_TAC[ineq_lemma_b];
 301   REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`];
 302   DISCH_THEN MATCH_MP_TAC;
 303   ASM_MESON_TAC[ineq_lemma_b];
 304   ]);;
 305   (* }}} *)
 306
 307 let sqrt8_nn = prove_by_refinement(
 308   `&0 <= sqrt8`,
 309   (* {{{ proof *)
 310   [
 311   REWRITE_TAC[Sphere.sqrt8];
 312   MATCH_MP_TAC SQRT_POS_LE;
 313   REAL_ARITH_TAC;
 314   ]);;
 315   (* }}} *)
 316
 317 let sqrt2_nn = prove_by_refinement(
 318   `&0 <= sqrt2`,
 319   (* {{{ proof *)
 320   [
 321   REWRITE_TAC[Sphere.sqrt2];
 322   MATCH_MP_TAC SQRT_POS_LE;
 323   REAL_ARITH_TAC;
 324   ]);;
 325   (* }}} *)
 326
 327 let sqrt3_nn = prove_by_refinement(
 328   `&0 <= sqrt(&3)`,
 329   (* {{{ proof *)
 330   [
 331   MATCH_MP_TAC SQRT_POS_LE;
 332   REAL_ARITH_TAC;
 333   ]);;
 334   (* }}} *)
 335
 336 let basic_constants_nn = [
 337  REAL_ARITH `&0 <= #2.18 /\ &0 <= &2 /\ &0 <= #2.52 /\ #2.0 = &2 /\ #2 = &2 /\ &0 <= #2.25 `;
 338  sqrt8_nn;sqrt2_nn;
 339  ];;
 340
 341 let abc_quadratic = prove (`abc_of_quadratic (\x. a * (x pow 2) + b * x + c) = (a,b,c)`,
 342  REWRITE_TAC[Sphere.abc_of_quadratic] THEN
 343  (REPEAT LET_TAC) THEN
 344  REWRITE_TAC[PAIR_EQ] THEN
 345  REPEAT(FIRST_X_ASSUM MP_TAC)THEN
 346  ARITH_TAC);;
 347
 348 let delta_quadratic = prove( `-- delta_x x1 x2 x3 x4 x5 x6 =
 349   (x1) * (x4 pow 2) + (x1*x1 + (x3 - x5)*(x2 - x6)
 350    - x1*(x2 + x3 + x5 + x6)) * x4
 351    + ( x1*x3*x5 + x1*x2*x6 - x3*(x1 + x2 - x3 + x5 - x6)*x6
 352     - x2*x5*(x1 - x2 + x3 - x5 + x6) ) `,
 353 REWRITE_TAC[Sphere.delta_x] THEN
 354 ARITH_TAC);;
 355
 356 let edge_flat_rewrite =
 357  REWRITE_RULE[abc_quadratic;delta_quadratic] Sphere.edge_flat;;
 358
 359 let enclosed_rewrite =
 360   REWRITE_RULE[abc_quadratic]
 361   (strip_let(REWRITE_RULE[Mur.muRa;Cayleyr.cayleyR_quadratic] Enclosed.enclosed));;
 362
 363 let quad_root_plus_curry =
 364   REWRITE_RULE[Sphere.quadratic_root_plus] quadratic_root_plus_curry;;
 365
 366 let y_of_x_e = prove(`!y1 y2 y3 y4 y5 y6. y_of_x f y1 y2 y3 y4 y5 y6 =
 367      f (y1*y1) (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6)`,
 368      REWRITE_TAC[Sphere.y_of_x]);;
 369
 370 let vol_y_e = prove(`!y1 y2 y3 y4 y5 y6. vol_y y1 y2 y3 y4 y5 y6 =
 371     y_of_x vol_x y1 y2 y3 y4 y5 y6`,
 372     REWRITE_TAC[Sphere.vol_y]);;
 373
 374 let rad2_y_e = prove(`!y1 y2 y3 y4 y5 y6. rad2_y y1 y2 y3 y4 y5 y6 =
 375     y_of_x rad2_x y1 y2 y3 y4 y5 y6`,
 376     REWRITE_TAC[Sphere.rad2_y]);;
 377
 378 let rad2_x_y = prove_by_refinement(
 379   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 380     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 381     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 382     (rad2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 383          rad2_x x1 x2 x3 x4 x5 x6)`,
 384   (* {{{ proof *)
 385   [
 386   REWRITE_TAC[Sphere.rad2_y;y_of_x_e;LET_DEF;LET_END_DEF];
 387   ASM_MESON_TAC[sq_pow2];
 388   ]);;
 389   (* }}} *)
 390
 391 let delta_x4_delta4_y = prove_by_refinement(
 392   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 393     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 394     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 395   (delta4_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = delta_x4 x1 x2 x3 x4 x5 x6)`,
 396   (* {{{ proof *)
 397   [
 398   REWRITE_TAC[Sphere.delta4_y;y_of_x_e;LET_DEF;LET_END_DEF];
 399   ASM_MESON_TAC[sq_pow2];
 400   ]);;
 401   (* }}} *)
 402
 403 let dih_x_y = prove_by_refinement(
 404   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 405     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 406     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 407     (dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 408          dih_x x1 x2 x3 x4 x5 x6)`,
 409   (* {{{ proof *)
 410   [
 411   REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
 412   ASM_MESON_TAC[sq_pow2];
 413   ]);;
 414   (* }}} *)
 415
 416 let dih2_x_y = prove_by_refinement(
 417   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 418     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 419     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 420     (dih2_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 421          dih2_x x1 x2 x3 x4 x5 x6)`,
 422   (* {{{ proof *)
 423   [
 424   REWRITE_TAC[Sphere.dih2_y;Sphere.dih2_x;Sphere.dih_y;LET_DEF;LET_END_DEF];
 425   ASM_MESON_TAC[sq_pow2];
 426   ]);;
 427   (* }}} *)
 428
 429 let dih3_x_y = prove_by_refinement(
 430   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 431     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 432     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 433     (dih3_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 434          dih3_x x1 x2 x3 x4 x5 x6)`,
 435   (* {{{ proof *)
 436   [
 437   REWRITE_TAC[Sphere.dih3_y;Sphere.dih3_x;Sphere.dih_y;LET_DEF;LET_END_DEF];
 438   ASM_MESON_TAC[sq_pow2];
 439   ]);;
 440   (* }}} *)
 441
 442 let delta_x_y = prove_by_refinement(
 443   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 444     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 445     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 446     (delta_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 447          delta_x x1 x2 x3 x4 x5 x6)`,
 448   (* {{{ proof *)
 449   [
 450   REWRITE_TAC[Sphere.delta_y;LET_DEF;LET_END_DEF];
 451   ASM_MESON_TAC[sq_pow2];
 452   ]);;
 453   (* }}} *)
 454
 455 let vol_x_y = prove_by_refinement(
 456   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 457     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 458     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 459     (vol_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 460          vol_x x1 x2 x3 x4 x5 x6)`,
 461   (* {{{ proof *)
 462   [
 463   REWRITE_TAC[Sphere.vol_y;Sphere.y_of_x;LET_DEF;LET_END_DEF];
 464   ASM_MESON_TAC[sq_pow2];
 465   ]);;
 466   (* }}} *)
 467
 468
 469 let sqrt8_2 = prove_by_refinement(
 470   `sqrt8 * sqrt8 = #8.0`,
 471   (* {{{ proof *)
 472   [
 473   REWRITE_TAC[Sphere.sqrt8];
 474   MESON_TAC[REAL_POW_2;SQRT_WORKS;REAL_ARITH `&8 = #8.0 /\ &0 <= &8`];
 475   ]);;
 476   (* }}} *)
 477
 478 let dih_x_sym = prove_by_refinement(
 479   `!x1 x2 x3 x4 x5 x6. dih_x x1 x2 x3 x4 x5 x6 = dih_x x1 x3 x2 x4 x6 x5`,
 480   (* {{{ proof *)
 481   [
 482   REWRITE_TAC[Sphere.dih_x;LET_DEF;LET_END_DEF];
 483   REPEAT GEN_TAC;
 484   REPEAT AP_TERM_TAC;
 485   REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4;PAIR_EQ];
 486   CONJ_TAC THEN AP_TERM_TAC THEN REAL_ARITH_TAC;
 487   ]);;
 488   (* }}} *)
 489
 490 let dih_x_sym2 = prove_by_refinement(
 491   `!x1 x2 x3 x4 x5 x6. dih_x x1 x2 x3 x4 x5 x6 = dih_x x1 x5 x6 x4 x2 x3`,
 492   (* {{{ proof *)
 493   [
 494   REWRITE_TAC[Sphere.dih_x;LET_DEF;LET_END_DEF];
 495   REPEAT GEN_TAC;
 496   REPEAT AP_TERM_TAC;
 497   REWRITE_TAC[Sphere.delta_x;Sphere.delta_x4;PAIR_EQ];
 498   CONJ_TAC THEN AP_TERM_TAC THEN REAL_ARITH_TAC;
 499   ]);;
 500   (* }}} *)
 501
 502
 503 let dih_y_sym = prove_by_refinement(
 504   `!y1 y2 y3 y4 y5 y6. dih_y y1 y2 y3 y4 y5 y6 = dih_y y1 y3 y2 y4 y6 y5`,
 505   (* {{{ proof *)
 506   [
 507   REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
 508   MESON_TAC[dih_x_sym];
 509   ]);;
 510   (* }}} *)
 511
 512 let dih_y_sym2 = prove_by_refinement(
 513   `!y1 y2 y3 y4 y5 y6. dih_y y1 y2 y3 y4 y5 y6 = dih_y y1 y5 y6 y4 y2 y3`,
 514   (* {{{ proof *)
 515   [
 516   REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
 517   MESON_TAC[dih_x_sym2];
 518   ]);;
 519   (* }}} *)
 520
 521 let sol_y_123 = prove_by_refinement(
 522   `!y1 y2 y3 y4 y5 y6. sol_y y1 y2 y3 y4 y5 y6 =
 523     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`,
 524   (* {{{ proof *)
 525   [
 526   REWRITE_TAC[Sphere.sol_y;Sphere.dih2_y;Sphere.dih3_y];
 527   REPEAT GEN_TAC;
 528   MATCH_MP_TAC (REAL_ARITH `(b = b') ==> (a + b + c -pi = a + b' + c - pi)`);
 529   REWRITE_TAC[Sphere.dih_y;LET_DEF;LET_END_DEF];
 530   MESON_TAC[dih_x_sym];
 531   ]);;
 532   (* }}} *)
 533
 534 let rhazim2_alt = prove_by_refinement(
 535   `!y1 y2 y3 y4 y5 y6. rhazim2 y1 y2 y3 y4 y5 y6 = rho y2 * dih2_y y1 y2 y3 y4 y5 y6`,
 536   (* {{{ proof *)
 537   [
 538   REWRITE_TAC[Sphere.rhazim2;Sphere.node2_y;Sphere.rhazim;Sphere.dih2_y;Sphere.dih_y;LET_DEF;LET_END_DEF];
 539   MESON_TAC[dih_x_sym];
 540   ]);;
 541   (* }}} *)
 542
 543 let rhazim3_alt = prove_by_refinement(
 544   `!y1 y2 y3 y4 y5 y6. rhazim3 y1 y2 y3 y4 y5 y6 = rho y3 * dih3_y y1 y2 y3 y4 y5 y6`,
 545   (* {{{ proof *)
 546   [
 547   REWRITE_TAC[Sphere.rhazim3;Sphere.node3_y;Sphere.rhazim;Sphere.dih3_y;Sphere.dih_y;LET_DEF;LET_END_DEF];
 548   ]);;
 549   (* }}} *)
 550
 551 let taum_123 = prove_by_refinement(
 552   `!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`,
 553   (* {{{ proof *)
 554   [
 555   REPEAT GEN_TAC;
 556   REWRITE_TAC[Sphere.taum;sol_y_123;Sphere.lnazim];
 557     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]);
 558   REWRITE_TAC[Sphere.dih_y;Sphere.dih2_y;Sphere.dih3_y;LET_DEF;LET_END_DEF] THEN MESON_TAC[dih_x_sym];
 559   REWRITE_TAC[Sphere.rhazim;rhazim2_alt;rhazim3_alt;Sphere.rho];
 560   REAL_ARITH_TAC;
 561   ]);;
 562   (* }}} *)
 563
 564 let tauq_x_y = prove_by_refinement(
 565   `!x1 x2 x3 x4 x5 x6 x7 x8 x9.
 566    (tauq (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) (sqrt x7) (sqrt x8) (sqrt x9) =
 567     taum_x x1 x2 x3 x4 x5 x6 + taum_x x7 x2 x3 x4 x8 x9)`,
 568   (* {{{ proof *)
 569   [
 570   REWRITE_TAC[Sphere.tauq;Sphere.taum_x;taum_123;LET_DEF;LET_END_DEF;Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x];
 571   ]);;
 572   (* }}} *)
 573
 574
 575 let rho_alt = prove_by_refinement(
 576   `!y. rho y = &1 + const1 *(y - &2) / (#0.52)`,
 577   (* {{{ proof *)
 578   [
 579   GEN_TAC;
 580   REWRITE_TAC[Sphere.rho;Sphere.ly;Sphere.interp;REAL_ARITH `#2.52 - &2 = #0.52`];
 581   REAL_ARITH_TAC;
 582   ]);;
 583   (* }}} *)
 584
 585 (* renamed from rho_x to avoid clash with rho_x in sphere.hl *)
 586
 587 let rho_sqrtx = prove_by_refinement(
 588   `!x. rho (sqrt x) = &1 + const1 * (sqrt x - &2) / (#0.52)`,
 589   (* {{{ proof *)
 590   [
 591   REWRITE_TAC[rho_alt];
 592   ]);;
 593   (* }}} *)
 594
 595 let lfun_ly = prove_by_refinement(
 596   `!h. lfun h = ly (&2 * h)`,
 597   (* {{{ proof *)
 598   [
 599   REWRITE_TAC[Sphere.lfun;Sphere.ly;Sphere.interp;Sphere.h0];
 600   REAL_ARITH_TAC;
 601   ]);;
 602   (* }}} *)
 603
 604 let lfun1 = prove_by_refinement(
 605   `lfun (&1) = (&1)`,
 606   (* {{{ proof *)
 607   [
 608   REWRITE_TAC[Sphere.lfun;Sphere.h0];
 609   REAL_ARITH_TAC;
 610   ]);;
 611   (* }}} *)
 612
 613 let rhazim2_alt = prove_by_refinement(
 614   `!y1 y2 y3 y4 y5 y6. rhazim2 y1 y2 y3 y4 y5 y6 = rho y2 * dih2_y y1 y2 y3 y4 y5 y6`,
 615   (* {{{ proof *)
 616   [
 617   REWRITE_TAC[Sphere.rhazim2;Sphere.node2_y;Sphere.rhazim;Sphere.dih2_y;];
 618   MESON_TAC[dih_y_sym];
 619   ]);;
 620   (* }}} *)
 621
 622 let rhazim3_alt = prove_by_refinement(
 623   `!y1 y2 y3 y4 y5 y6. rhazim3 y1 y2 y3 y4 y5 y6 = rho y3 * dih3_y y1 y2 y3 y4 y5 y6`,
 624   (* {{{ proof *)
 625   [
 626   REWRITE_TAC[Sphere.rhazim3;Sphere.node3_y;Sphere.rhazim;Sphere.dih3_y;];
 627   ]);;
 628   (* }}} *)
 629
 630 let beta_bump_force_x = prove_by_refinement(
 631   `!x1 x2 x3 x4 x5 x6. beta_bump_force_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 632     halfbump_x1 x1 x2 x3 x4 x5 x6 - halfbump_x4 x1 x2 x3 x4 x5 x6`,
 633   (* {{{ proof *)
 634   [
 635   REWRITE_TAC[Sphere.beta_bump_force_y;halfbump_x1;halfbump_x4;halfbump_x];
 636   ]);;
 637   (* }}} *)
 638
 639 let halfbump_x_expand = prove_by_refinement(
 640   `!x. &0 <= x ==> (halfbump_x x =
 641    -- (&4398119 / &2376200) + (&17500 / &11881) * sqrt x - (&31250 / &106929) * x)`,
 642   (* {{{ proof *)
 643   [
 644   REWRITE_TAC[halfbump_x;Sphere.bump;Sphere.h0;Sphere.hplus];
 645   REPEAT STRIP_TAC;
 646   REWRITE_TAC[REAL_ARITH`(a/ &2 - b) pow 2 = (a pow 2) / &4 - a * b + b pow 2`];
 647   ASM_SIMP_TAC[SQRT_POW_2];
 648   REAL_ARITH_TAC;
 649   ]);;
 650   (* }}} *)
 651
 652 let vol4f_palt = prove_by_refinement(
 653   `!f y1 y2 y3 y4 y5 y6. vol4f y1 y2 y3 y4 y5 y6 f  =
 654     (-- &8 * mm1)
 655     +
 656     (&4 * mm1 / pi) *
 657     (dih_y y1 y2 y3 y4 y5 y6 + dih2_y y1 y2 y3 y4 y5 y6 +
 658     dih3_y y1 y2 y3 y4 y5 y6 +
 659     dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 +
 660      dih6_y y1 y2 y3 y4 y5 y6)
 661     +
 662     (-- &8 * mm2 / pi) *
 663     (f (y1/ &2) * dih_y y1 y2 y3 y4 y5 y6 +
 664     f(y2/ &2) * dih2_y y1 y2 y3 y4 y5 y6 +
 665     f (y3/ &2) * dih3_y y1 y2 y3 y4 y5 y6 +
 666     f (y4/ &2) * dih4_y y1 y2 y3 y4 y5 y6 +
 667     f(y5/ &2) * dih5_y y1 y2 y3 y4 y5 y6 +
 668     f(y6/ &2) * dih6_y y1 y2 y3 y4 y5 y6)
 669     `,
 670   (* {{{ proof *)
 671   [
 672   REPEAT GEN_TAC;
 673   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;];
 674   SUBGOAL_THEN `dih_y y2 y3 y1 y5 y6 y4 = dih2_y y1 y2 y3 y4 y5 y6 /\
 675    dih_y y3 y1 y2 y6 y4 y5 = dih3_y y1 y2 y3 y4 y5 y6 /\
 676    dih_y y3 y1 y2 y6 y4 y5 = dih3_y y1 y2 y3 y4 y5 y6 /\
 677    dih_y y4 y3 y5 y1 y6 y2 = dih4_y y1 y2 y3 y4 y5 y6 /\
 678    dih_y y5 y1 y6 y2 y4 y3 = dih5_y y1 y2 y3 y4 y5 y6 /\
 679    dih_y y6 y1 y5 y3 y4 y2 = dih6_y y1 y2 y3 y4 y5 y6 /\
 680    dih_y y6 y4 y2 y3 y1 y5 = dih6_y y1 y2 y3 y4 y5 y6 /\
 681    dih_y y2 y6 y4 y5 y3 y1 = dih2_y y1 y2 y3 y4 y5 y6 /\
 682    dih_y y1 y5 y6  y4 y2 y3 = dih_y y1 y2 y3 y4 y5 y6 /\
 683    dih_y y5 y6 y1 y2 y3 y4 = dih5_y y1 y2 y3 y4 y5 y6 /\
 684    dih_y y4 y5 y3 y1 y2 y6 = dih4_y y1 y2 y3 y4 y5 y6 /\
 685    dih_y y5 y3 y4 y2 y6 y1 = dih5_y y1 y2 y3 y4 y5 y6 /\
 686    dih_y y3 y4 y5 y6 y1 y2 = dih3_y y1 y2 y3 y4 y5 y6 /\
 687    dih_y y4 y2 y6 y1 y5 y3 = dih4_y y1 y2 y3 y4 y5 y6` (fun t-> REWRITE_TAC[t]);
 688   REWRITE_TAC[Sphere.dih2_y;Sphere.dih3_y;Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y];
 689   MESON_TAC[dih_y_sym;dih_y_sym2];
 690   ONCE_REWRITE_TAC[REAL_ARITH `x  = y <=> x - y = &0`];
 691   ABBREV_TAC `a = mm1/pi `;
 692   SUBGOAL_THEN `mm1 = a * pi ` (fun t->REWRITE_TAC[t]);
 693   POP_ASSUM MP_TAC;
 694   SUBGOAL_THEN  `~(pi = &0)` MP_TAC;
 695   SIMP_TAC[PI_POS;REAL_ARITH `&0 < x ==> ~(x= &0)`];
 696   CONV_TAC REAL_FIELD;
 697   REAL_ARITH_TAC;
 698   ]);;
 699   (* }}} *)
 700
 701
 702 let edge_flat2_x_rewrite = prove_by_refinement(
 703   `!x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x5 /\
 704     &0 <= x6) ==> (edge_flat2_x x1 x2 x3 x4 x5 x6 =
 705     (sqrt (quadratic_root_plus
 706            (x1,
 707             (x1) * x1 +
 708             (x3 - x5) * (x2 - x6) -
 709             (x1) * (x2 + x3 + x5 + x6),
 710             (x1) * (x3) * x5 +
 711             (x1) * (x2) * x6 -
 712             (x3) *
 713             (x1 + x2 - x3 + x5 - x6) * x6 -
 714             (x2) *
 715             (x5) *
 716             (x1 - x2 + x3 - x5 + x6)))) pow 2)`,
 717   (* {{{ proof *)
 718   [
 719   REWRITE_TAC[Sphere.edge_flat2_x];
 720   REPEAT STRIP_TAC;
 721   AP_THM_TAC;
 722   AP_TERM_TAC;
 723   REWRITE_TAC[edge_flat_rewrite];
 724   ASM_SIMP_TAC[REAL_ARITH `sqrt x * sqrt x = (sqrt x) pow 2`;SQRT_POW2;SQRT_WORKS];
 725   ]);;
 726   (* }}} *)
 727
 728 let edge_quadratic = prove_by_refinement(
 729   `!x1 x2 x3 x5 x6. quadratic_root_plus (x1,
 730             x1 * x1 +
 731             (x3 - x5) * (x2 - x6) -
 732             x1 * (x2 + x3 + x5 + x6),
 733             x1 * x3 * x5 +
 734             (x1) * (x2) * x6 -  (x3) * (x1 + x2 - x3 + x5 - x6) * x6 -
 735               (x2) * (x5) * (x1 - x2 + x3 - x5 + x6)) =
 736   (-- (x1 * x1) + x1*x2 + x1*x3 - x2*x3 + x1*x5 + x2*x5 + x1*x6 + x3*x6 -
 737   x5*x6 + sqrt(ups_x x1 x3 x5 * ups_x x1 x2 x6))/(&2*x1)`,
 738   (* {{{ proof *)
 739   [
 740   REWRITE_TAC[Sphere.quadratic_root_plus;Sphere.ups_x];
 741   REPEAT STRIP_TAC;
 742   AP_THM_TAC;
 743   AP_TERM_TAC;
 744   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`];
 745   REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 746   REAL_ARITH_TAC;
 747   ]);;
 748   (* }}} *)
 749
 750 let lmfun0 = prove_by_refinement(
 751   `!y. &2 * h0 <= y ==> (lmfun (y/ &2)  = &0)`,
 752   (* {{{ proof *)
 753   [
 754   REWRITE_TAC[Sphere.lmfun;REAL_ARITH `&2 * h0 <= y <=> (~(y/ &2 <= h0) \/ (y/ &2 = h0))`];
 755   GEN_TAC;
 756   DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `h0 <= h0`;REAL_FIELD `(h0 - h0)/(h0 - &1) = &0`];
 757   ]);;
 758   (* }}} *)
 759
 760 let lmfun_lfun = prove_by_refinement(
 761   `!y. y <= &2 * h0 ==> (lmfun (y/ &2) = lfun(y/ &2))`,
 762   (* {{{ proof *)
 763   [
 764   REWRITE_TAC[Sphere.lmfun;Sphere.lfun;REAL_ARITH `y <= &2 * h0 <=> y/ &2 <= h0`];
 765   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
 766   ]);;
 767   (* }}} *)
 768
 769 let lmfun_lfun2 = prove_by_refinement(
 770   `!y. y <=  h0 ==> (lmfun (y) = lfun(y))`,
 771   (* {{{ proof *)
 772   [
 773   REWRITE_TAC[Sphere.lmfun;Sphere.lfun];
 774   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
 775   ]);;
 776   (* }}} *)
 777
 778 (* compute hminus *)
 779
 780 let quartic_has_real_derivative = prove_by_refinement(
 781   `!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)`,
 782   (* {{{ proof *)
 783   [
 784   REPEAT STRIP_TAC THEN
 785 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];
 786   ]);;
 787   (* }}} *)
 788
 789 let POLY_CONTINUITY_TAC =
 790  REPEAT (MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN
 791  CONJ_TAC) THEN
 792  REPEAT (MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL) THEN
 793  (MATCH_MP_TAC REAL_CONTINUOUS_ON_POW) THEN
 794  REWRITE_TAC[REAL_CONTINUOUS_ON_ID];;
 795
 796 let quartic_continuous_on = prove_by_refinement(
 797   `!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`,
 798   (* {{{ proof *)
 799   [
 800   REPEAT STRIP_TAC;
 801   POLY_CONTINUITY_TAC;
 802   ]);;
 803   (* }}} *)
 804
 805 let marchal_minus_lfun = prove_by_refinement(
 806   `!h. marchal_quartic h - lfun h =
 807    (inv(&65 * &1627 * (sqrt(&2) - &1))) * (h - &1)*
 808     (( -- &512505 + &770958*sqrt(&2)) * h pow 0 +
 809     ( -- &364208 -  &1295359*sqrt(&2)) * h pow 1 +
 810    ( &1295359 + &585000*sqrt(&2))* h pow 2 +
 811    (-- &585000) * h pow 3)`,
 812   (* {{{ proof *)
 813   [
 814   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];
 815   GEN_TAC;
 816   SUBGOAL_THEN `&0 < sqrt(&2) - &1 ` MP_TAC THENL [ALL_TAC;CONV_TAC REAL_FIELD];
 817   SUBGOAL_THEN `#1.414213 < sqrt(&2) ` MP_TAC THENL[ALL_TAC;REAL_ARITH_TAC];
 818   REWRITE_TAC[GSYM Sphere.sqrt2;Flyspeck_constants.bounds];
 819   ]);;
 820   (* }}} *)
 821
 822 let hminus_cont = prove_by_refinement(
 823   `!s. (\h. marchal_quartic h - lfun h) real_continuous_on s`,
 824   (* {{{ proof *)
 825   [
 826   GEN_TAC;
 827   REWRITE_TAC[marchal_minus_lfun];
 828   MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL;
 829  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;
 830   ]);;
 831   (* }}} *)
 832
 833 let sqrt2_lb = prove_by_refinement(
 834   `#1.414213 < sqrt2 `,
 835   (* {{{ proof *)
 836   [
 837   REWRITE_TAC[Flyspeck_constants.bounds];
 838   ]);;
 839   (* }}} *)
 840
 841 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]));;
 842
 843 let hminus_exists = prove_by_refinement(
 844   `?x. (#1.2 <= x /\ x < #1.3 /\ marchal_quartic x = lmfun x)`,
 845   (* {{{ proof *)
 846   [
 847     SUBGOAL_THEN `(?x. x IN real_interval [#1.2,#1.26] /\ (\x. marchal_quartic x - lfun x) x = &0)` MP_TAC;
 848     MATCH_MP_TAC REAL_IVT_INCREASING;
 849     BETA_TAC;
 850     REWRITE_TAC[hminus_cont];
 851     REWRITE_TAC[marchal_minus_lfun;GSYM Sphere.sqrt2];
 852    ASSUME_TAC sqrt2_lb;
 853    SUBGOAL_THEN `&0 < sqrt2 - &1` ASSUME_TAC;
 854    POP_ASSUM MP_TAC;
 855    REAL_ARITH_TAC;
 856    REWRITE_TAC[(* REAL_INV_MUL;REAL_INV_INV; *) REAL_ARITH `#1.2- &1 = &1 / &5 /\ #1.26 - &1 = &13 / &50`];
 857     CONJ_TAC THENL[REAL_ARITH_TAC;ALL_TAC];
 858     SUBGOAL_THEN `sqrt2 < #1.414214` ASSUME_TAC;
 859    REWRITE_TAC[Flyspeck_constants.bounds];
 860    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]);
 861    REAL_ARITH_TAC;
 862    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]);
 863    REAL_ARITH_TAC;
 864    REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> (&0 <= a * b * (-- c))`];
 865    STRIP_NN_TAC THEN (REPEAT (POP_ASSUM MP_TAC)) THEN TRY REAL_ARITH_TAC;
 866    (* last subgoal *)
 867    REWRITE_TAC[real_interval;IN_ELIM_THM];
 868    REPEAT STRIP_TAC;
 869    EXISTS_TAC `x:real`;
 870    SUBGOAL_THEN `x <= &2 * h0` ASSUME_TAC;
 871    REWRITE_TAC[Sphere.h0];
 872    UNDISCH_TAC `x <= #1.26` THEN REAL_ARITH_TAC;
 873    ASM_SIMP_TAC [Sphere.h0;lmfun_lfun2];
 874    REPEAT (POP_ASSUM MP_TAC);
 875    REAL_ARITH_TAC;
 876   ]);;
 877   (* }}} *)
 878
 879 let hminus_prop = prove_by_refinement(
 880   `#1.2 <= hminus /\ hminus < #1.3 /\ marchal_quartic hminus = lmfun hminus`,
 881   (* {{{ proof *)
 882   [
 883   MP_TAC hminus_exists;
 884   MP_TAC Sphere.hminus;
 885   MESON_TAC[];
 886   ]);;
 887   (* }}} *)
 888
 889 let hminus_high = prove_by_refinement(
 890   `!h. (h0 <= h) ==> lmfun h = &0`,
 891   (* {{{ proof *)
 892   [
 893     REWRITE_TAC[Sphere.lmfun;REAL_ARITH `h0 <= h <=> (~(h <= h0) \/ (h = h0))`];
 894   GEN_TAC;
 895   DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ARITH `h0 <= h0`;REAL_FIELD `(h0 - h0)/(h0 - &1) = &0`];
 896   ]);;
 897   (* }}} *)
 898
 899 let hminus_lt_h0 = prove_by_refinement(
 900   `!h. (&1 <= h) /\ (h < hplus) ==> (marchal_quartic h > &0)`,
 901   (* {{{ proof *)
 902   [
 903   REPEAT STRIP_TAC;
 904   REWRITE_TAC[Sphere.marchal_quartic];
 905   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)`];
 906   MATCH_MP_TAC REAL_LT_MUL;
 907   CONJ_TAC;
 908   POP_ASSUM MP_TAC;
 909   SUBGOAL_THEN `&0 < sqrt(&2) - hplus` MP_TAC;
 910   REWRITE_TAC[Flyspeck_constants.bounds];
 911   REAL_ARITH_TAC;
 912 MATCH_MP_TAC REAL_LT_MUL;
 913   CONJ_TAC;
 914   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 915   MATCH_MP_TAC REAL_LT_DIV;
 916   REWRITE_TAC[Flyspeck_constants.bounds];
 917   REPEAT (POP_ASSUM MP_TAC);
 918   REWRITE_TAC[Sphere.hplus];
 919   ABBREV_TAC `u = h - &1`;
 920   SUBGOAL_THEN `h = u + &1` (fun t->REWRITE_TAC[t]);
 921   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 922   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)`];
 923   POP_ASSUM (fun t->ALL_TAC);
 924   REPEAT STRIP_TAC;
 925   SUBGOAL_THEN `u pow 2 < #0.3254 pow 2` MP_TAC;
 926   REWRITE_TAC[ GSYM REAL_LT_SQUARE_ABS];
 927   REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 928   REPEAT (POP_ASSUM MP_TAC);
 929   ABBREV_TAC `v = u pow 2`;
 930   REAL_ARITH_TAC;
 931   ]);;
 932   (* }}} *)
 933
 934 let hminus_lt_h0 = prove_by_refinement(
 935   `hminus < h0`,
 936   (* {{{ proof *)
 937   [
 938   REWRITE_TAC [REAL_ARITH `x < y <=> ~(x >= y)`];
 939   STRIP_TAC;
 940   MP_TAC hminus_prop;
 941   REPEAT STRIP_TAC;
 942   POP_ASSUM MP_TAC;
 943   MATCH_MP_TAC (REAL_ARITH `a > b ==>((a:real) = b ==> F)`);
 944   SUBGOAL_THEN `lmfun hminus = &0` (fun t -> REWRITE_TAC[t]);
 945   MATCH_MP_TAC hminus_high;
 946   UNDISCH_TAC `hminus >= h0` THEN REAL_ARITH_TAC;
 947   MATCH_MP_TAC   hminus_lt_h0;
 948   REPEAT (POP_ASSUM MP_TAC);
 949   REWRITE_TAC[Sphere.hplus;Sphere.h0];
 950   REAL_ARITH_TAC;
 951   ]);;
 952   (* }}} *)
 953
 954 let h0_lt_hplus = prove_by_refinement(
 955   `h0 < hplus`,
 956   (* {{{ proof *)
 957   [
 958   REWRITE_TAC[Sphere.h0;Sphere.hplus];
 959   REAL_ARITH_TAC;
 960   ]);;
 961   (* }}} *)
 962
 963 let hminus_gt = prove_by_refinement(
 964   `#1.2 <= hminus`,
 965   (* {{{ proof *)
 966   [
 967   REWRITE_TAC[hminus_prop];
 968   ]);;
 969   (* }}} *)
 970
 971 let lminus_ge_h0 = prove_by_refinement(
 972   `!h. (hplus <= h) /\ (h <= sqrt (&2)) ==> (marchal_quartic h <= &0)`,
 973   (* {{{ proof *)
 974   [
 975   REWRITE_TAC[Sphere.marchal_quartic];
 976   REWRITE_TAC[REAL_ARITH `a * b * c /d <= &0 <=> &0 <= a * b * (-- c)/d`];
 977   REPEAT STRIP_TAC;
 978   MATCH_MP_TAC REAL_LE_MUL;
 979   CONJ_TAC;
 980   POP_ASSUM MP_TAC;
 981   REAL_ARITH_TAC;
 982   MATCH_MP_TAC REAL_LE_MUL;
 983   CONJ_TAC;
 984   REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 985   MATCH_MP_TAC REAL_LE_DIV;
 986   CONJ_TAC;
 987   (* *)
 988     REPEAT (POP_ASSUM MP_TAC);
 989   REWRITE_TAC[Sphere.hplus];
 990   ABBREV_TAC `u = h - &1`;
 991   SUBGOAL_THEN `h = u + &1` (fun t->REWRITE_TAC[t]);
 992   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 993   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)`];
 994   REPEAT STRIP_TAC;
 995   SUBGOAL_THEN `u pow 2 < #0.42 pow 2` MP_TAC;
 996   REWRITE_TAC[ GSYM REAL_LT_SQUARE_ABS];
 997   POP_ASSUM MP_TAC;
 998   POP_ASSUM MP_TAC;
 999   EXPAND_TAC "u";
1000   SUBGOAL_THEN `sqrt(&2) - &1 < #0.42` (fun t-> (MP_TAC t) THEN REAL_ARITH_TAC);
1001   SUBGOAL_THEN `sqrt(&2) <  #1.414214` MP_TAC;
1002   REWRITE_TAC[GSYM Sphere.sqrt2;Flyspeck_constants.bounds];
1003   REAL_ARITH_TAC;
1004   SUBGOAL_THEN `u < #0.414214` MP_TAC;
1005   SUBGOAL_THEN `sqrt(&2) <  #1.414214` MP_TAC;
1006   REWRITE_TAC[GSYM Sphere.sqrt2;Flyspeck_constants.bounds];
1007   POP_ASSUM MP_TAC;
1008   REAL_ARITH_TAC;
1009   REAL_ARITH_TAC;
1010   MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`);
1011   REWRITE_TAC[Flyspeck_constants.bounds];
1012   ]);;
1013   (* }}} *)
1014
1015 let gcy_high  = prove_by_refinement(
1016   `!y. (&2 * h0 <= y) ==> (gcy y = &4 * mm1/pi)`,
1017   (* {{{ proof *)
1018   [
1019   REWRITE_TAC[Sphere.gcy];
1020   SIMP_TAC[lmfun0];
1021   REAL_ARITH_TAC;
1022   ]);;
1023   (* }}} *)
1024
1025 let gcy_low = prove_by_refinement(
1026   `!y. (y <= &2 * h0) ==> (gcy y = gchi y)`,
1027   (* {{{ proof *)
1028   [
1029   REWRITE_TAC[Sphere.gcy;Sphere.gchi];
1030   SIMP_TAC[lmfun_lfun];
1031   REWRITE_TAC[Sphere.lfun;Sphere.h0];
1032   REPEAT STRIP_TAC;
1033   ABBREV_TAC `m = mm2/pi`;
1034   REAL_ARITH_TAC;
1035   ]);;
1036   (* }}} *)
1037
1038 let gcy_low_hminus = prove_by_refinement(
1039   `!y. (y <= &2 * hminus) ==> (gcy y = gchi y)`,
1040   (* {{{ proof *)
1041   [
1042   REPEAT STRIP_TAC;
1043   MATCH_MP_TAC gcy_low;
1044   POP_ASSUM MP_TAC;
1045   MP_TAC hminus_lt_h0;
1046   REAL_ARITH_TAC;
1047   ]);;
1048   (* }}} *)
1049
1050 let c2001 = prove_by_refinement(
1051   `!y. (y <= #2.001) ==> (y <= &2 * h0)`,
1052   [
1053     REWRITE_TAC[Sphere.h0];
1054   REAL_ARITH_TAC;
1055   ]
1056 );;
1057
1058 let gcy_low_const = prove_by_refinement(
1059   `!y. (y <= #2.001) ==> (gcy y = gchi y)`,
1060   (* {{{ proof *)
1061   [
1062   REPEAT STRIP_TAC;
1063   MATCH_MP_TAC gcy_low;
1064   POP_ASSUM MP_TAC;
1065   REWRITE_TAC[Sphere.h0];
1066   REAL_ARITH_TAC;
1067   ]);;
1068   (* }}} *)
1069
1070 let gcy_high_hplus = prove_by_refinement(
1071   `!y. (&2 * hplus <= y) ==> (gcy y = &4 * mm1/pi)`,
1072   (* {{{ proof *)
1073   [
1074   REPEAT STRIP_TAC;
1075   MATCH_MP_TAC gcy_high;
1076   FIRST_X_ASSUM MP_TAC;
1077   MP_TAC h0_lt_hplus;
1078   REAL_ARITH_TAC;
1079   ]);;
1080   (* }}} *)
1081
1082 let hm0 = prove_by_refinement(
1083   `!y. ((y <= &2 * hminus) ==> (y <= &2 * h0))`,
1084   (* {{{ proof *)
1085   [
1086    MP_TAC hminus_lt_h0;
1087   CONV_TAC REAL_FIELD;
1088   ]);;
1089   (* }}} *)
1090
1091 let h0_lt_gt = prove_by_refinement(
1092   `((y <= #2.01) ==> (y <= &2 * h0)) /\
1093    ((#2.8 <= y) ==> (&2 * h0 <= y)) /\
1094   (( y <= &2) ==> (y <= &2 * h0)) /\
1095     ((sqrt8 <= y) ==> (&2 * h0 <= y)) /\   ((&2 * h0 <= y) ==> (&0 <= y)) /\
1096    ((&2 <= y) ==> (&0 <= y)) /\
1097    ((y <= &2 * hminus) ==> (y <= &2 * h0)) /\
1098    ((&2 * hminus <= y) ==> (&0 <= y))`,
1099   (* {{{ proof *)
1100   [
1101   REWRITE_TAC[Sphere.h0;sqrt8_sqrt2;hm0];
1102     MP_TAC sqrt2_lb;
1103   MP_TAC hminus_gt;
1104   REAL_ARITH_TAC;
1105   ]);;
1106   (* }}} *)
1107
1108 let sqrtxx = prove_by_refinement(
1109   `!x. &0 <= x ==> (sqrt(x * x) = x)`,
1110   (* {{{ proof *)
1111   [
1112     REWRITE_TAC[POW_2_SQRT_ABS;REAL_ARITH `x * x = x pow 2`];
1113   REAL_ARITH_TAC;
1114   ]);;
1115   (* }}} *)
1116
1117 let lmdih_ldih = prove_by_refinement(
1118   `!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 )`,
1119   (* {{{ proof *)
1120   [
1121   REWRITE_TAC[Sphere.y_of_x;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch];
1122   MESON_TAC[sqrtxx;lmfun_lfun];
1123   ]);;
1124   (* }}} *)
1125
1126 let lmdih3_ldih3 = prove_by_refinement(
1127   `!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 )`,
1128   (* {{{ proof *)
1129   [
1130   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];
1131   MESON_TAC[sqrtxx;lmfun_lfun];
1132   ]);;
1133   (* }}} *)
1134
1135 let lmdih5_ldih5 = prove_by_refinement(
1136   `!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 )`,
1137   (* {{{ proof *)
1138   [
1139   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];
1140   MESON_TAC[sqrtxx;lmfun_lfun];
1141   ]);;
1142   (* }}} *)
1143
1144 let lmdih_ldih' = REWRITE_RULE[Sphere.y_of_x] lmdih_ldih;;
1145 let lmdih3_ldih3' = REWRITE_RULE[Sphere.y_of_x] lmdih3_ldih3;;
1146 let lmdih5_ldih5' = REWRITE_RULE[Sphere.y_of_x] lmdih5_ldih5;;
1147
1148 let lmdih0 = prove_by_refinement(
1149   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y1 ) ==>(y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  &0 )`,
1150   (* {{{ proof *)
1151   [
1152   REWRITE_TAC[Sphere.y_of_x;Nonlin_def.lmdih_x_div_sqrtdelta_posbranch;Nonlin_def.ldih_x_div_sqrtdelta_posbranch];
1153   MESON_TAC[sqrtxx;lmfun0;REAL_ARITH `&0 * x = &0 `;h0_lt_gt];
1154   ]);;
1155   (* }}} *)
1156
1157 let lmdih3_0 = prove_by_refinement(
1158   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y3 ) ==>(y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  &0 )`,
1159   (* {{{ proof *)
1160   [
1161   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];
1162   MESON_TAC[sqrtxx;lmfun0;REAL_ARITH `&0 * x = &0 `;h0_lt_gt];
1163   ]);;
1164   (* }}} *)
1165
1166 let lmdih5_0 = prove_by_refinement(
1167   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y5 ) ==>(y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 =  &0 )`,
1168   (* {{{ proof *)
1169   [
1170   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];
1171   MESON_TAC[sqrtxx;lmfun0;REAL_ARITH `&0 * x = &0 `;h0_lt_gt];
1172   ]);;
1173   (* }}} *)
1174
1175 let lmdih1_0' = REWRITE_RULE[Sphere.y_of_x] lmdih0;;
1176 let lmdih3_0' = REWRITE_RULE[Sphere.y_of_x] lmdih3_0;;
1177 let lmdih5_0' = REWRITE_RULE[Sphere.y_of_x] lmdih5_0;;
1178
1179 let vol4f_lmfun = prove_by_refinement(
1180   `! y1 y2 y3 y4 y5 y6. vol4f y1 y2 y3 y4 y5 y6 lmfun  =
1181     (-- &8 * mm1)
1182     +
1183     gcy y1 * dih_y y1 y2 y3 y4 y5 y6 + gcy y2 * dih2_y y1 y2 y3 y4 y5 y6 +
1184     gcy y3 * dih3_y y1 y2 y3 y4 y5 y6 +
1185     gcy y4 * dih4_y y1 y2 y3 y4 y5 y6 +
1186       gcy y5 * dih5_y y1 y2 y3 y4 y5 y6 +
1187     gcy y6 * dih6_y y1 y2 y3 y4 y5 y6`,
1188   (* {{{ proof *)
1189   [
1190     REWRITE_TAC[vol4f_palt;Sphere.gcy];
1191   REAL_ARITH_TAC;
1192   ]);;
1193   (* }}} *)
1194
1195 let gamma4fgcy_alt = prove_by_refinement(`gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun =
1196     vol_y y1 y2 y3 y4 y5 y6 -
1197     ((-- &8 * mm1)
1198     +
1199     gcy y1 * dih_y y1 y2 y3 y4 y5 y6 + gcy y2 * dih2_y y1 y2 y3 y4 y5 y6 +
1200     gcy y3 * dih3_y y1 y2 y3 y4 y5 y6 +
1201     gcy y4 * dih4_y y1 y2 y3 y4 y5 y6 +
1202       gcy y5 * dih5_y y1 y2 y3 y4 y5 y6 +
1203     gcy y6 * dih6_y y1 y2 y3 y4 y5 y6)`,
1204 [
1205 REWRITE_TAC[Sphere.gamma4fgcy;Sphere.gamma4f;vol4f_lmfun];
1206 ]);;
1207
1208 let vol3f_palt = prove_by_refinement(
1209   `!y1 y2 y3 y4 y5 y6 r f.
1210       (y3 = r) /\ (y4 = r) /\ (y5 = r) ==>
1211      (vol3f y1 y2 y6 r f =       (&2 * mm1 / pi) *
1212          (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih2_y y1 y2 y3 y4 y5 y6 +
1213           &2 * dih6_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
1214           dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
1215          (&8 * mm2 / pi) *
1216          (f (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
1217           f (y2 / &2) * dih2_y y1 y2 y3 y4 y5 y6 +
1218           f (y6 / &2) * dih6_y y1 y2 y3 y4 y5 y6))`,
1219   (* {{{ proof *)
1220   [
1221   REPEAT GEN_TAC;
1222   REWRITE_TAC[Sphere.vol3f;Sphere.sol_y];
1223   DISCH_THEN (fun t->REWRITE_TAC[t]);
1224   REWRITE_TAC[Sphere.dih2_y;Sphere.dih3_y;Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y];
1225   ABBREV_TAC `a = &8 * mm2/pi`;
1226   ABBREV_TAC `b = &2 * mm1/pi`;
1227   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]);
1228  MESON_TAC[dih_y_sym2;dih_y_sym];
1229  MATCH_MP_TAC (REAL_ARITH `(a = a') ==> (a - c = a' - c)`);
1230  REAL_ARITH_TAC;
1231   ]);;
1232   (* }}} *)
1233
1234 let vol3f_135_palt = prove_by_refinement(
1235   `!y1 y2 y3 y4 y5 y6 r f.
1236       (y2 = r) /\ (y4 = r) /\ (y6 = r) ==>
1237      (vol3f y1 y3 y5 r f =       (&2 * mm1 / pi) *
1238          (&2 * dih_y y1 y2 y3 y4 y5 y6 + &2 * dih3_y y1 y2 y3 y4 y5 y6 +
1239           &2 * dih5_y y1 y2 y3 y4 y5 y6 + dih2_y y1 y2 y3 y4 y5 y6 +
1240           dih4_y y1 y2 y3 y4 y5 y6 + dih6_y y1 y2 y3 y4 y5 y6 - &3 * pi) -
1241          (&8 * mm2 / pi) *
1242          (f (y1 / &2) * dih_y y1 y2 y3 y4 y5 y6 +
1243           f (y3 / &2) * dih3_y y1 y2 y3 y4 y5 y6 +
1244           f (y5 / &2) * dih5_y y1 y2 y3 y4 y5 y6))`,
1245   (* {{{ proof *)
1246   [
1247   REPEAT GEN_TAC;
1248   REWRITE_TAC[Sphere.vol3f;Sphere.sol_y];
1249   DISCH_THEN (fun t->REWRITE_TAC[t]);
1250   REWRITE_TAC[Sphere.dih2_y;Sphere.dih3_y;Sphere.dih4_y;Sphere.dih5_y;Sphere.dih6_y];
1251   ABBREV_TAC `a = &8 * mm2/pi`;
1252   ABBREV_TAC `b = &2 * mm1/pi`;
1253   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]);
1254  MESON_TAC[dih_y_sym2;dih_y_sym];
1255  MATCH_MP_TAC (REAL_ARITH `(a = a') ==> (a - c = a' - c)`);
1256  REAL_ARITH_TAC;
1257   ]);;
1258   (* }}} *)
1259
1260 let vol3r_alt = prove_by_refinement(
1261   `! y1 y2 y3 y4 y5 y6 r. (y3 = r ) /\ (y4 = r) /\ (y5 = r) ==>
1262    (vol3r y1 y2 y6 r  = vol_y y1 y2 y3 y4 y5 y6)`,
1263   (* {{{ proof *)
1264   [
1265   REWRITE_TAC[Sphere.vol3r;Sphere.vol_y;Sphere.y_of_x;Sphere.vol_x;Sphere.delta_x];
1266   REPEAT GEN_TAC;
1267   DISCH_THEN (fun t->REWRITE_TAC[t]);
1268   AP_THM_TAC;
1269   AP_TERM_TAC;
1270   AP_TERM_TAC;
1271   REAL_ARITH_TAC;
1272   ]);;
1273   (* }}} *)
1274
1275 (* a few lemmas copied  from TameGeneral *)
1276
1277 let COS_PI3 = prove(`cos (pi / &3) = &1 / &2`,
1278    REWRITE_TAC[COS_SIN] THEN
1279      REWRITE_TAC[REAL_ARITH `pi / &2 - pi / &3 = pi / &6`] THEN
1280      REWRITE_TAC[SIN_PI6]);;
1281
1282 let ACS_2 = prove(`acs (&1 / &2) = pi / &3`,
1283    REWRITE_TAC[SYM COS_PI3] THEN
1284      MATCH_MP_TAC ACS_COS THEN
1285      REWRITE_TAC[REAL_ARITH `(&0 <= a / &3 <=> &0 <= a) /\ (a / &3 <= a <=> &0 <= a)`] THEN
1286      MATCH_MP_TAC REAL_LT_IMP_LE THEN
1287      REWRITE_TAC[PI_POS]);;
1288
1289 let sol0_POS = prove(`&0 < sol0`,
1290    REWRITE_TAC[Sphere.sol0] THEN
1291      REWRITE_TAC[REAL_ARITH `&0 < &3 * a - pi <=> pi / &3 < a`] THEN
1292      REWRITE_TAC[SYM ACS_2] THEN
1293      MATCH_MP_TAC ACS_MONO_LT THEN
1294      REAL_ARITH_TAC);;
1295
1296 let vol4f_alt = prove_by_refinement(
1297   `!y1 y2 y3 y4 y5 y6. vol4f y1 y2 y3 y4 y5 y6 lfun  =
1298     (-- &8 * mm1)
1299     +
1300     (&4 * mm1/pi - &8 * mm2 *(&1+const1)/(pi * const1) ) *
1301     (dih_y y1 y2 y3 y4 y5 y6 + dih2_y y1 y2 y3 y4 y5 y6 + dih3_y y1 y2 y3 y4 y5 y6 +
1302     dih4_y y1 y2 y3 y4 y5 y6 + dih5_y y1 y2 y3 y4 y5 y6 + dih6_y y1 y2 y3 y4 y5 y6)
1303     +
1304     (&8 * mm2 / (pi * const1)) *
1305     (rhazim y1 y2 y3 y4 y5 y6 + rhazim2 y1 y2 y3 y4 y5 y6 + rhazim3 y1 y2 y3 y4 y5 y6 +
1306     rhazim4 y1 y2 y3 y4 y5 y6 + rhazim5 y1 y2 y3 y4 y5 y6 + rhazim6 y1 y2 y3 y4 y5 y6)
1307     `,
1308   (* {{{ proof *)
1309   [
1310   REPEAT GEN_TAC;
1311     REWRITE_TAC[vol4f_palt];
1312   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;];
1313   REWRITE_TAC[Sphere.rho;Sphere.node2_y;Sphere.node3_y;Sphere.rhazim];
1314   ONCE_REWRITE_TAC[REAL_ARITH `x  = y <=> x - y = &0`];
1315   SUBGOAL_THEN  `~(pi = &0)` ASSUME_TAC;
1316   SIMP_TAC[PI_POS;REAL_ARITH `&0 < x ==> ~(x= &0)`];
1317   SUBGOAL_THEN `~(const1 = &0)`   MP_TAC;
1318   REWRITE_TAC[GSYM sol0_over_pi_EQ_const1];
1319   MP_TAC sol0_POS;
1320   FIRST_X_ASSUM MP_TAC;
1321   CONV_TAC REAL_FIELD;
1322   FIRST_X_ASSUM MP_TAC;
1323   CONV_TAC REAL_FIELD;
1324   ]);;
1325   (* }}} *)
1326
1327 let vol2f_marchal_pow_y = prove_by_refinement(
1328   `!r y. vol2f y r marchal_quartic =
1329        let fac = (-- (&8 * mm2/pi) * &2 * pi * inv ( #1.627 * (sqrt2 - &1)))  in
1330     (&2 * mm1 / pi)  * &2 * pi
1331      - (&2 * mm1 /pi) * &2 * pi * inv(r * &2) * y pow 1
1332    - fac * &3 * sqrt2 *hplus
1333     + fac *(#1.5 * sqrt2 + #1.5 * hplus + #8.5 * sqrt2 * hplus) * y pow 1
1334    + fac * (-- #0.75  - #8.5 * sqrt2 * inv(&2) - #8.5 * hplus * inv(&2) - &9 * hplus * sqrt2 * inv (&4)) * y pow 2
1335     + fac* ( #17.0 * inv (&8) + #9.0 * sqrt2 * inv(&8) + #9.0 * hplus * inv(&8)) * y pow 3
1336     - fac * #9.0 * inv(&16) * y pow 4`,
1337   (* {{{ proof *)
1338   [
1339   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)`];
1340     REPEAT GEN_TAC;
1341   REWRITE_TAC[GSYM Sphere.hplus;real_div];
1342   REAL_ARITH_TAC;
1343   ]);;
1344   (* }}} *)
1345
1346 let vol2r_y = prove_by_refinement(
1347   `!y r. vol2r y r = &2 * pi * r * r * inv (&3) - #0.5 * pi * inv(&3) * y pow 2`,
1348   (* {{{ proof *)
1349   [
1350   REWRITE_TAC[Sphere.vol2r;real_div];
1351   REAL_ARITH_TAC;
1352   ]);;
1353   (* }}} *)
1354
1355 let ineq_expand6 = prove_by_refinement(
1356   `!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) <=>
1357   (a1 <= y1 /\ y1 <= b1
1358      ==> a2 <= y2 /\ y2 <= b2
1359      ==> a3 <= y3 /\ y3 <= b3
1360      ==> a4 <= y4 /\ y4 <= b4
1361      ==> a5 <= y5 /\ y5 <= b5
1362      ==> a6 <= y6 /\ y6 <= b6
1363      ==> P)`,
1364   (* {{{ proof *)
1365   [
1366   REWRITE_TAC[ineq];
1367   ]);;
1368   (* }}} *)
1369
1370 let ineq_expand9 = prove_by_refinement(
1371   `!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) <=>
1372   (a1 <= y1 /\ y1 <= b1
1373      ==> a2 <= y2 /\ y2 <= b2
1374      ==> a3 <= y3 /\ y3 <= b3
1375      ==> a4 <= y4 /\ y4 <= b4
1376      ==> a5 <= y5 /\ y5 <= b5
1377      ==> a6 <= y6 /\ y6 <= b6
1378      ==> a7 <= y7 /\ y7 <= b7
1379      ==> a8 <= y8 /\ y8 <= b8
1380      ==> a9 <= y9 /\ y9 <= b9
1381      ==> P)`,
1382   (* {{{ proof *)
1383   [
1384   REWRITE_TAC[ineq];
1385   ]);;
1386   (* }}} *)
1387
1388 let pathL_bound = prove_by_refinement(
1389   `!y a.  FST (pathL a) <= y /\ y <= SND (pathL a) ==>
1390     FST a <= y /\ y <= SND a`,
1391   (* {{{ proof *)
1392   [
1393   REPEAT GEN_TAC;
1394     SUBGOAL_THEN `pathL a = pathL (FST a, SND a)` (fun t->ONCE_REWRITE_TAC[t]);
1395   REWRITE_TAC[PAIR];
1396     REWRITE_TAC[Sphere.pathL];
1397     REAL_ARITH_TAC;
1398   ]);;
1399   (* }}} *)
1400
1401 let pathR_bound = prove_by_refinement(
1402   `!y a. FST (pathR a) <= y /\ y <= SND (pathR a) ==>
1403     FST a <= y /\ y <= SND a`,
1404   (* {{{ proof *)
1405   [
1406   REPEAT GEN_TAC;
1407     SUBGOAL_THEN `pathR a = pathR (FST a, SND a)` (fun t->ONCE_REWRITE_TAC[t]);
1408   REWRITE_TAC[PAIR];
1409     REWRITE_TAC[Sphere.pathR];
1410     REAL_ARITH_TAC;
1411   ]);;
1412   (* }}} *)
1413
1414 let delta_x_eq0 = prove_by_refinement(
1415   `delta_x (&8) (&4) (&4) (&8) (&4) (&4) = &0 /\
1416    delta_x (&4) (&8) (&4) (&4) (&8) (&4) = &0
1417   `,
1418   (* {{{ proof *)
1419   [
1420   REWRITE_TAC[Sphere.delta_x];
1421     REAL_ARITH_TAC;
1422   ]);;
1423   (* }}} *)
1424
1425 let delta_x4_eq64 = prove_by_refinement(
1426   `delta_x4 (&8) (&4) (&4) (&8) (&4) (&4) = -- &64 /\
1427    delta_x4 (&4) (&8) (&4) (&4) (&8) (&4) = &64
1428   `,
1429   (* {{{ proof *)
1430   [
1431   REWRITE_TAC[Sphere.delta_x4];
1432     REAL_ARITH_TAC;
1433   ]);;
1434   (* }}} *)
1435
1436 let atn2_0y = prove_by_refinement(
1437   `atn2 (&0,&64) = pi / &2 /\ atn2 (&0 ,-- &64) = -- pi/ &2`,
1438   (* {{{ proof *)
1439   [
1440   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];
1441   REAL_ARITH_TAC;
1442   ]);;
1443   (* }}} *)
1444
1445 let OR_RULE rule1 rule2 th = try rule1 th with _ -> rule2 th;;
1446
1447 let rec REPEAT_RULE rule =
1448   fun t -> if can rule t then REPEAT_RULE rule (rule t) else t;;
1449
1450 let vol3f_lmln = prove_by_refinement(
1451   `!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)`,
1452   (* {{{ proof *)
1453   [
1454   REWRITE_TAC[Sphere.vol3f];
1455   MESON_TAC[lmfun_lfun];
1456   ]);;
1457   (* }}} *)
1458
1459 let vol3_vol_x = prove_by_refinement(
1460   `!x1 x2 x3 x4 x5 x6.
1461    &0 <= x1 /\ &0 <= x2 /\ &0 <= x6 ==>
1462     (vol3_x_sqrt x1 x2 x3 x4 x5 x6 = vol_x x1 x2 (&2) (&2) (&2) x6)`,
1463   (* {{{ proof *)
1464   [
1465    MP_TAC (REAL_ARITH `&0 <= &2`);
1466   ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 pow 2`];
1467   REPEAT STRIP_TAC;
1468   REWRITE_TAC[vol3_x_sqrt;Sphere.vol_x;Sphere.vol_y;Sphere.y_of_x;Sphere.sqrt2];
1469   REPEAT AP_THM_TAC;
1470   AP_TERM_TAC ;
1471   AP_TERM_TAC;
1472   ASM_SIMP_TAC[SPEC `&0` sq_pow2];
1473   REWRITE_TAC[Sphere.delta_x];
1474   REAL_ARITH_TAC;
1475   ]);;
1476   (* }}} *)
1477
1478 let spec0 = SPECL [`&0`;`&0`;`&0`;`&0`;`&0`;`&0`;];;
1479
1480 let vol3f_x_lfun_alt = prove_by_refinement(
1481   `!x1 x2 x3 x4 x5 x6.
1482    &0 <= x1 /\ &0 <= x2 /\ &0 <= x6 ==>
1483    vol3f_x_lfun x1 x2 x3 x4 x5 x6 =   (&2 * mm1 / pi) *
1484              (&2 * dih_x x1 x2 (&2) (&2) (&2) x6 +
1485               &2 * dih2_x x1 x2 (&2) (&2) (&2) x6 +
1486               &2 * dih6_x x1 x2 (&2) (&2) (&2) x6 +
1487               dih3_x x1 x2 (&2) (&2) (&2) x6 +
1488               dih4_x x1 x2 (&2) (&2) (&2) x6 +
1489               dih5_x x1 x2 (&2) (&2) (&2) x6 - &3 * pi) -
1490              (&8 * mm2 / pi) *
1491              ( ldih_x x1 x2 (&2) (&2) (&2) x6 +
1492               ldih2_x x1 x2 (&2) (&2) (&2) x6 +
1493               ldih6_x x1 x2 (&2) (&2) (&2) x6)`,
1494   (* {{{ proof *)
1495   [
1496    MP_TAC (REAL_ARITH `&0 <= &2`);
1497   ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 pow 2`];
1498   REPEAT STRIP_TAC;
1499   REWRITE_TAC[vol3f_x_lfun;];
1500   MP_TAC (SPECL [`sqrt x1`;`sqrt x2`;`sqrt2`;`sqrt2`;`sqrt2`;`sqrt x6`;`sqrt2`;`lfun`] vol3f_palt);
1501   REWRITE_TAC[];
1502   DISCH_THEN (fun t->REWRITE_TAC[t]);
1503   REWRITE_TAC[Sphere.sqrt2;Sphere.ldih_x;Sphere.ldih2_x;Sphere.ldih6_x;Sphere.dih4_x;Sphere.dih5_x;Sphere.dih6_x];
1504   ASM_SIMP_TAC[spec0 dih_x_y;spec0 dih2_x_y;spec0 dih3_x_y];
1505   ]);;
1506   (* }}} *)
1507
1508 let spech0 = SPECL [`&2 * h0`;`&0`;`&0`;`&0`;`&0`;`&0`;];;
1509
1510 let vol3f_x_sqrt2_lmplus_alt = prove_by_refinement(
1511   `!x1 x2 x3 x4 x5 x6.
1512    ((&2 * h0) pow 2 <= x1) /\ &0 <= x2 /\ &0 <= x6 ==>
1513    vol3f_x_sqrt2_lmplus x1 x2 x3 x4 x5 x6 =   (&2 * mm1 / pi) *
1514              (&2 * dih_x x1 x2 (&2) (&2) (&2) x6 +
1515               &2 * dih2_x x1 x2 (&2) (&2) (&2) x6 +
1516               &2 * dih6_x x1 x2 (&2) (&2) (&2) x6 +
1517               dih3_x x1 x2 (&2) (&2) (&2) x6 +
1518               dih4_x x1 x2 (&2) (&2) (&2) x6 +
1519               dih5_x x1 x2 (&2) (&2) (&2) x6 - &3 * pi) -
1520              (&8 * mm2 / pi) *
1521              (
1522               ldih2_x x1 x2 (&2) (&2) (&2) x6 +
1523               ldih6_x x1 x2 (&2) (&2) (&2) x6)`,
1524   (* {{{ proof *)
1525   [
1526    MP_TAC (REAL_ARITH `&0 <= &2`);
1527   ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 pow 2`];
1528   REPEAT STRIP_TAC;
1529   REWRITE_TAC[vol3f_x_sqrt2_lmplus;vol3f_sqrt2_lmplus];
1530   REWRITE_TAC[Sphere.sqrt2;Sphere.ldih_x;Sphere.ldih2_x;Sphere.ldih6_x;Sphere.dih4_x;Sphere.dih5_x;Sphere.dih6_x];
1531   ASM_SIMP_TAC[spech0 dih_x_y;spech0 dih2_x_y;spech0 dih3_x_y];
1532   ]);;
1533   (* }}} *)
1534
1535 let vol3f_lm0 = prove_by_refinement(
1536   `!y1 y2 y3 y4 y5 y6.
1537   ( &2 * h0 <= y1) /\ (y2 <= &2 * h0) /\ (y6 <= &2 * h0) ==>
1538   (vol3f y1 y2 y6 sqrt2 lmfun = vol3f_sqrt2_lmplus y1 y2 y3 y4 y5 y6)`,
1539   (* {{{ proof *)
1540   [
1541   REPEAT STRIP_TAC;
1542   REWRITE_TAC[vol3f_sqrt2_lmplus];
1543   MP_TAC (SPECL [`y1:real`;`y2:real`;`sqrt2`;`sqrt2`;`sqrt2`;`y6:real`; `sqrt2`;`lmfun`] vol3f_palt);
1544   REWRITE_TAC[];
1545   DISCH_THEN (fun t-> REWRITE_TAC[t]);
1546   ASM_SIMP_TAC[lmfun_lfun;lmfun0];
1547   REWRITE_TAC[REAL_ARITH `&0 * x = &0 /\ &0 + y = y`];
1548   ]);;
1549   (* }}} *)
1550
1551 let vol3r_126_x = prove_by_refinement(
1552   `vol3r (sqrt x1) (sqrt x2) (sqrt x6) sqrt2 = vol3_x_sqrt x1 x2 (x3:real) (x4:real) (x5:real) x6`,
1553   (* {{{ proof *)
1554   [
1555   REWRITE_TAC[vol3_x_sqrt;Sphere.vol3r;Sphere.vol_y];
1556   ]);;
1557   (* }}} *)
1558
1559 let num1_poly = prove_by_refinement(
1560   `! x1 x2 x3 x4 x5 x6. num1 x1 x2 x3 x4 x5 x6 =
1561      &64*x1*x4 - &32*x2*x4 - &32*x3*x4 - &4*x1*(x4 pow 2) - &32*x2*x5 + &32*x3*x5 +
1562    &4*x2*x4*x5 + &32*x2*x6 - &32*x3*x6 + &4*x3*x4*x6 `,
1563   (* {{{ proof *)
1564   [
1565   REWRITE_TAC[Sphere.num1];
1566   REAL_ARITH_TAC;
1567   ]);;
1568   (* }}} *)
1569
1570 let ineq6_of_ineq5 = prove_by_refinement(
1571   `!a1 a2 a3 a4 a5 y1 y2 y3 y4 y5 b1 b2 b3 b4 b5 P.
1572 ((!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)]
1573    (P x1 x2 x3 x4 x5)) ==>
1574     ineq[(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5)]
1575    (P y1 y2 y3 y4 y5))`,
1576   (* {{{ proof *)
1577   [
1578   REWRITE_TAC[ineq];
1579   MESON_TAC[REAL_ARITH `&1 <= &1`];
1580   ]);;
1581   (* }}} *)
1582
1583 let ineq6_of_ineq1 = prove_by_refinement(
1584   `!a1 y1 b1 P.
1585 ((!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)]
1586    (P x1)) ==> ineq[(a1,y1,b1)]  (P y1))`,
1587   (* {{{ proof *)
1588   [
1589   REWRITE_TAC[ineq];
1590   MESON_TAC[REAL_ARITH `&1 <= &1`];
1591   ]);;
1592   (* }}} *)
1593
1594 let dih_x_alt = prove_by_refinement(
1595   `!x1 x2 x3 x4 x5 x6. dih_x x1 x2 x3 x4 x5 x6 = pi / &2 +
1596      atn2
1597      (sqrt (&4 * x1 * delta_x x1 x2 x3 x4 x5 x6),
1598       --delta_x4 x1 x2 x3 x4 x5 x6) `,
1599   (* {{{ proof *)
1600   [
1601   REWRITE_TAC[Sphere.dih_x];
1602   REPEAT LET_TAC;
1603   REWRITE_TAC[];
1604   ]);;
1605   (* }}} *)
1606
1607 end;;