text_formalization/nonlinear/functional_equation.hl

   1 (* ========================================================================= *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                             *)
   3 (*                                                                           *)
   4 (* Chapter: nonlinear inequalities                                           *)
   5 (* Author:  Thomas Hales      *)
   6 (* Date: 2012-05-20                                                          *)
   7 (* ========================================================================= *)
   8
   9
  10 (* May 2012 functional equational definitions of
  11    inequality functions.
  12
  13    This code is to be used in automated generation of C++
  14    taylorFunctions.
  15
  16    scripts.hl generates ocaml Sphere2 module based on these lemmas.
  17
  18    June 2012: truncate_* are all deprecated.  They can be deleted.
  19
  20 autogen:
  21    see functional_* lemmas in this file.
  22    see functional1_* lemmas in this file for univariate functions.
  23
  24 native_c:
  25         unit,x1,x2,x3,x4,x5,x6,
  26                 y1,y2,y3,y4,y5,y6,
  27           delta_x,delta_x4,
  28           dih_x, sol_x,rad2_x,
  29           num1,
  30           norm2hh_x,
  31
  32  *)
  33
  34 (* failwith "moodule";; *)
  35
  36  module Functional_equation = struct
  37
  38   open Hales_tactic;;
  39   open Nonlinear_lemma;;
  40
  41   let GMATCH = GMATCH_SIMP_TAC;;
  42
  43 let uni = new_definition `uni (f,x) x1 x2 x3 x4 x5 x6 =
  44   (f:A->B) ( x x1 x2 x3 x4 x5 x6)`;;
  45
  46 let constant6 = new_definition `constant6 c x1 x2 x3 x4 x5 x6 = c`;;
  47
  48 let promote3_to_6 = new_definition
  49     `promote3_to_6 f x1 x2 x3 x4 x5 x6 = f x1 x2 x3`;;
  50
  51 let promote1_to_6 = new_definition
  52   `promote1_to_6 f x1 x2 x3 x4 x5 x6 = f x1`;;
  53
  54 let functional_proj_x1 = prove_by_refinement(
  55   `proj_x1 = promote1_to_6 I`,
  56   (* {{{ proof *)
  57   [
  58   REWRITE_TAC[FUN_EQ_THM;promote1_to_6;proj_x1;I_DEF];
  59   ]);;
  60   (* }}} *)
  61
  62 (* these are circular, because we will define rotatek
  63    as a composition of proj_xm *)
  64
  65 let functional_proj_x2 = prove_by_refinement(
  66   `proj_x2 = rotate2 proj_x1`,
  67   (* {{{ proof *)
  68   [
  69   REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x2;Sphere.rotate2];
  70   ]);;
  71   (* }}} *)
  72
  73 let functional_proj_x3 = prove_by_refinement(
  74   `proj_x3 = rotate3 proj_x1`,
  75   (* {{{ proof *)
  76   [
  77   REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x3;Sphere.rotate3];
  78   ]);;
  79   (* }}} *)
  80
  81 let functional_proj_x4 = prove_by_refinement(
  82   `proj_x4 = rotate4 proj_x1`,
  83   (* {{{ proof *)
  84   [
  85   REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x4;Sphere.rotate4];
  86   ]);;
  87   (* }}} *)
  88
  89 let functional_proj_x5 = prove_by_refinement(
  90   `proj_x5 = rotate5 proj_x1`,
  91   (* {{{ proof *)
  92   [
  93   REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x5;Sphere.rotate5];
  94   ]);;
  95   (* }}} *)
  96
  97 let functional_proj_x6 = prove_by_refinement(
  98   `proj_x6 = rotate6 proj_x1`,
  99   (* {{{ proof *)
 100   [
 101   REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x6;Sphere.rotate6];
 102   ]);;
 103   (* }}} *)
 104
 105 let rh0 = new_definition `rh0 = &1/(h0 - &1)`;;
 106
 107 let two6 = new_definition `two6 = constant6 ( &2)`;;
 108
 109 let zero6 = new_definition `zero6 = constant6 ( &0)`;;
 110
 111 let dummy6 = new_definition `dummy6 = constant6 ( &0)`;;
 112
 113 let four6 = new_definition `four6 = constant6 ( &4)`;;
 114
 115 let mk_126 = new_definition `mk_126 f =
 116   compose6 f proj_x1 proj_x2 two6 two6 two6 proj_x6`;;
 117
 118 let mk_456 = new_definition `mk_456 f =
 119   compose6 f two6 two6 two6 proj_x4 proj_x5 proj_x6`;;
 120
 121 let mk_135 = new_definition `mk_135 f =
 122   compose6 f proj_x1 two6 proj_x3 two6 proj_x5 two6`;;
 123
 124 let add6 = new_definition `add6 f g x1 x2 x3 x4 x5 x6 =
 125   f x1 x2 x3 x4 x5 x6 + g x1 x2 x3 x4 x5 x6`;;
 126
 127 let scalar6 = new_definition `scalar6 f r x1 x2 x3 x4 x5 x6 =
 128   (f x1 x2 x3 x4 x5 x6) * (r:real)`;;
 129
 130 let mul6 = new_definition `mul6 f g x1 x2 x3 x4 x5 x6 =
 131   f x1 x2 x3 x4 x5 x6 * g x1 x2 x3 x4 x5 x6`;;
 132
 133 let div6 = new_definition `div6 f g x1 x2 x3 x4 x5 x6 =
 134   f x1 x2 x3 x4 x5 x6 / g x1 x2 x3 x4 x5 x6`;;
 135
 136 let sub6 = new_definition `sub6 f g x1 x2 x3 x4 x5 x6 =
 137   f x1 x2 x3 x4 x5 x6  -  g x1 x2 x3 x4 x5 x6`;;
 138
 139 let proj_y1 = new_definition `proj_y1 x1 x2 x3 x4 x5 x6 =
 140   sqrt(x1)`;;
 141
 142 let proj_y2 = new_definition `proj_y2 x1 x2 x3 x4 x5 x6 =
 143   sqrt(x2)`;;
 144
 145 let proj_y3 = new_definition `proj_y3 x1 x2 x3 x4 x5 x6 =
 146   sqrt(x3)`;;
 147
 148 let proj_y4 = new_definition `proj_y4 x1 x2 x3 x4 x5 x6 =
 149   sqrt(x4)`;;
 150
 151 let proj_y5 = new_definition `proj_y5 x1 x2 x3 x4 x5 x6 =
 152   sqrt(x5)`;;
 153
 154 let proj_y6 = new_definition `proj_y6 x1 x2 x3 x4 x5 x6 =
 155   sqrt(x6)`;;
 156
 157
 158 let domain6 = new_definition `domain6 h f g =
 159   (!x1 x2 x3 x4 x5 x6. h x1 x2 x3 x4 x5 x6 ==>
 160       (f x1 x2 x3 x4 x5 x6 = g x1 x2 x3 x4 x5 x6))`;;
 161
 162 (* should be called something different, because we project out 3 coords *)
 163
 164 let rotate234 = new_definition `rotate234 f =
 165   compose6 f proj_x2 proj_x3 proj_x4 unit6 unit6 unit6`;;
 166
 167 let rotate126 = new_definition `rotate126 f =
 168   compose6 f proj_x1 proj_x2 proj_x6 unit6 unit6 unit6`;;
 169
 170 let rotate345 = new_definition `rotate345 f =
 171   compose6 f proj_x3 proj_x4 proj_x5 unit6 unit6 unit6`;;
 172
 173 let functional_overload() = (
 174   overload_interface ("+",`add6`);
 175   overload_interface ("-",`sub6`);
 176   overload_interface ("/",`div6`);
 177   overload_interface ("*",`mul6`));;
 178
 179 let _ = functional_overload();;
 180
 181 let proj_x1 = Nonlinear_lemma.proj_x1;;
 182 let proj_x2 = Nonlinear_lemma.proj_x2;;
 183 let proj_x3 = Nonlinear_lemma.proj_x3;;
 184 let proj_x4 = Nonlinear_lemma.proj_x4;;
 185 let proj_x5 = Nonlinear_lemma.proj_x5;;
 186 let proj_x6 = Nonlinear_lemma.proj_x6;;
 187 let unit6 = Nonlinear_lemma.unit6;;
 188 let compose6 = Nonlinear_lemma.compose6;;
 189
 190 let h0cut = new_definition `h0cut y = if (y <= &2 * h0) then &1 else &0`;;
 191
 192 let functional_proj_y1 = prove_by_refinement(
 193   `proj_y1 = promote1_to_6 sqrt`,
 194   (* {{{ proof *)
 195   [
 196   REWRITE_TAC[FUN_EQ_THM;promote1_to_6;proj_y1];
 197   ]);;
 198   (* }}} *)
 199
 200 let functional_proj_y2 = prove_by_refinement(
 201   `proj_y2 = rotate2 proj_y1`,
 202   (* {{{ proof *)
 203   [
 204   REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y2;Sphere.rotate2];
 205   ]);;
 206   (* }}} *)
 207
 208 let functional_proj_y3 = prove_by_refinement(
 209   `proj_y3 = rotate3 proj_y1`,
 210   (* {{{ proof *)
 211   [
 212   REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y3;Sphere.rotate3];
 213   ]);;
 214   (* }}} *)
 215
 216 let functional_proj_y4 = prove_by_refinement(
 217   `proj_y4 = rotate4 proj_y1`,
 218   (* {{{ proof *)
 219   [
 220   REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y4;Sphere.rotate4];
 221   ]);;
 222   (* }}} *)
 223
 224 let functional_proj_y5 = prove_by_refinement(
 225   `proj_y5 = rotate5 proj_y1`,
 226   (* {{{ proof *)
 227   [
 228   REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y5;Sphere.rotate5];
 229   ]);;
 230   (* }}} *)
 231
 232 let functional_proj_y6 = prove_by_refinement(
 233   `proj_y6 = rotate6 proj_y1`,
 234   (* {{{ proof *)
 235   [
 236   REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y6;Sphere.rotate6];
 237   ]);;
 238   (* }}} *)
 239
 240 let sqrt_sqrt = prove_by_refinement(
 241   `!x. &0 <= x ==> (sqrt x * sqrt x = x)`,
 242   (* {{{ proof *)
 243   [
 244   MESON_TAC[arith `&0 pow 2 = &0`;(SPEC `&0` Nonlinear_lemma.sq_pow2)];
 245   ]);;
 246   (* }}} *)
 247
 248 let functional_norm2hh_x = prove_by_refinement(
 249   `norm2hh_x = uni(pow2,(proj_y1 - constant6 (hminus + hplus))) +
 250     uni(pow2, proj_y2 - two6) + uni(pow2,proj_y3 - two6) +
 251     uni(pow2, proj_y4 - two6) + uni(pow2,proj_y5 - two6) +
 252     uni(pow2, proj_y6 - two6)`,
 253   (* {{{ proof *)
 254   [
 255   REWRITE_TAC[FUN_EQ_THM; add6; sub6; uni;proj_y1;Nonlinear_lemma.pow2; two6;Sphere.norm2hh_x;Sphere.norm2hh;proj_y1;proj_y2;proj_y3;proj_y4;proj_y5;proj_y6;constant6];
 256   BY(REAL_ARITH_TAC)
 257   ]);;
 258   (* }}} *)
 259
 260 let functional_eta2_126 = prove_by_refinement(
 261   `domain6
 262     (\x1 x2 x3 x4 x5 x6.
 263        (&0 <= x1 /\ &0 <= x2 /\ &0 <= x6))
 264     eta2_126  (uni(pow2,rotate126 (promote3_to_6 eta_x)))`,
 265   (* {{{ proof *)
 266   [
 267  REWRITE_TAC[domain6;Sphere.eta2_126;Sphere.eta_y; uni; rotate126;compose6;promote3_to_6;proj_x1;proj_x2;proj_x6;unit6;LET_END_DEF;LET_DEF;Nonlinear_lemma.pow2];
 268   BY(ASM_SIMP_TAC[sqrt_sqrt])
 269   ]);;
 270   (* }}} *)
 271
 272
 273 let functional_rotate2 = prove_by_refinement(
 274   `!f. rotate2 f = compose6 f proj_x2 proj_x3 proj_x1 proj_x5 proj_x6 proj_x4`,
 275   (* {{{ proof *)
 276   [
 277   BY(REWRITE_TAC[Sphere.rotate2;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
 278   ]);;
 279   (* }}} *)
 280
 281 let functional_rotate3 = prove_by_refinement(
 282   `!f. rotate3 f = compose6 f proj_x3 proj_x1 proj_x2 proj_x6 proj_x4 proj_x5`,
 283   (* {{{ proof *)
 284   [
 285   BY(REWRITE_TAC[Sphere.rotate3;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
 286   ]);;
 287   (* }}} *)
 288
 289 let functional_rotate4 = prove_by_refinement(
 290   `!f. rotate4 f = compose6 f proj_x4 proj_x2 proj_x6 proj_x1 proj_x5 proj_x3`,
 291   (* {{{ proof *)
 292   [
 293   BY(REWRITE_TAC[Sphere.rotate4;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
 294   ]);;
 295   (* }}} *)
 296
 297 let functional_rotate5 = prove_by_refinement(
 298   `!f. rotate5 f = compose6 f proj_x5 proj_x3 proj_x4 proj_x2 proj_x6 proj_x1`,
 299   (* {{{ proof *)
 300   [
 301   BY(REWRITE_TAC[Sphere.rotate5;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
 302   ]);;
 303   (* }}} *)
 304
 305 let functional_rotate6 = prove_by_refinement(
 306   `!f. rotate6 f = compose6 f proj_x6 proj_x1 proj_x5 proj_x3 proj_x4 proj_x2`,
 307   (* {{{ proof *)
 308   [
 309   BY(REWRITE_TAC[Sphere.rotate6;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
 310   ]);;
 311   (* }}} *)
 312
 313 let functional_x1_delta_x = prove_by_refinement(
 314   `x1_delta_x = proj_x1 * delta_x`,
 315   (* {{{ proof *)
 316   [
 317   REWRITE_TAC[FUN_EQ_THM];
 318    BY(REWRITE_TAC[proj_x1;Sphere.x1_delta_x;mul6])
 319   ]);;
 320   (* }}} *)
 321
 322 let functional_delta4_squared_x = prove_by_refinement(
 323   `delta4_squared_x = uni(pow2,delta_x4)`,
 324   (* {{{ proof *)
 325   [
 326 BY(REWRITE_TAC[FUN_EQ_THM;uni;Nonlinear_lemma.pow2;Sphere.delta4_squared_x])
 327   ]);;
 328   (* }}} *)
 329
 330 let functional_vol_x = prove_by_refinement(
 331   `vol_x = scalar6 (uni(sqrt,delta_x)) (&1 / &12)`,
 332   (* {{{ proof *)
 333   [
 334   (REWRITE_TAC[FUN_EQ_THM;uni;Sphere.vol_x;scalar6]);
 335   BY(REAL_ARITH_TAC)
 336   ]);;
 337   (* }}} *)
 338
 339 let functional_dih2_x = prove_by_refinement(
 340   `dih2_x = rotate2 dih_x`,
 341   (* {{{ proof *)
 342   [
 343   REWRITE_TAC[FUN_EQ_THM];
 344   REWRITE_TAC[Sphere.dih2_x;Sphere.rotate2];
 345   BY(MESON_TAC[Nonlinear_lemma.dih_x_sym])
 346   ]);;
 347   (* }}} *)
 348
 349 let functional_dih3_x = prove_by_refinement(
 350   `dih3_x = rotate3 dih_x`,
 351   (* {{{ proof *)
 352   [
 353   REWRITE_TAC[FUN_EQ_THM];
 354   REWRITE_TAC[Sphere.dih3_x;Sphere.rotate3];
 355   ]);;
 356   (* }}} *)
 357
 358 let functional_dih4_x = prove_by_refinement(
 359   `domain6 (\x1 x2 x3 x4 x5 x6.
 360    &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
 361        &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
 362               dih4_x  (rotate4 dih_x)`,
 363   (* {{{ proof *)
 364   [
 365   REWRITE_TAC[domain6];
 366     REWRITE_TAC[Sphere.dih4_x; Sphere.rotate4;Sphere.dih4_y; Sphere.dih_y; LET_DEF;LET_END_DEF];
 367   REPEAT WEAK_STRIP_TAC;
 368   REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
 369   BY(ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`])
 370   ]);;
 371   (* }}} *)
 372
 373 let functional_dih5_x = prove_by_refinement(
 374   `domain6 (\x1 x2 x3 x4 x5 x6.
 375    &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
 376        &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
 377               dih5_x  (rotate5 dih_x)`,
 378   (* {{{ proof *)
 379   [
 380     REWRITE_TAC[domain6];
 381     REWRITE_TAC[Sphere.dih5_x; Sphere.rotate5;Sphere.dih5_y; Sphere.dih_y; LET_DEF;LET_END_DEF];
 382     REPEAT WEAK_STRIP_TAC;
 383     REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
 384     (ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`]);
 385     MESON_TAC[Nonlinear_lemma.dih_x_sym;Nonlinear_lemma.dih_x_sym2];
 386   ]);;
 387   (* }}} *)
 388
 389 let functional_dih6_x = prove_by_refinement(
 390   `domain6 (\x1 x2 x3 x4 x5 x6.
 391    &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
 392        &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
 393               dih6_x  (rotate6 dih_x)`,
 394   (* {{{ proof *)
 395   [
 396   REWRITE_TAC[domain6];
 397     REWRITE_TAC[Sphere.dih6_x; Sphere.rotate6;Sphere.dih6_y;Sphere.dih_y; LET_DEF;LET_END_DEF];
 398   REPEAT WEAK_STRIP_TAC;
 399   REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
 400   (ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`]);
 401   ]);;
 402   (* }}} *)
 403
 404 (*
 405
 406 let dih6_x' = new_definition `dih6_x' = rotate6 dih_x`;;
 407
 408 let ldih6_x' = new_definition `!x1 x2 x3 x4 x5 x6.
 409             ldih6_x' x1 x2 x3 x4 x5 x6 =
 410             lfun (sqrt x6 / &2) * dih6_x' x1 x2 x3 x4 x5 x6`;;
 411
 412 let gchi6_x' = new_definition `!x1 x2 x3 x4 x5 x6.
 413             gchi6_x x1 x2 x3 x4 x5 x6 =
 414             gchi (sqrt x6) * dih6_x' x1 x2 x3 x4 x5 x6`;;
 415
 416 *)
 417
 418 let functional_lfun_y1 = prove_by_refinement(
 419   `lfun_y1 = scalar6 (scalar6 unit6 h0 - proj_x1) rh0`,
 420   (* {{{ proof *)
 421   [
 422     REWRITE_TAC[FUN_EQ_THM];
 423     REWRITE_TAC[add6;scalar6;mul6;div6;sub6;constant6;rh0];
 424     REWRITE_TAC[Sphere.lfun_y1;Sphere.lfun;             Nonlinear_lemma.unit6;Nonlinear_lemma.proj_x1];
 425 REAL_ARITH_TAC;
 426   ]);;
 427   (* }}} *)
 428
 429 let functional_ldih_x = prove_by_refinement(
 430   `ldih_x =
 431     (scalar6 (scalar6 unit6 h0 - scalar6 proj_y1 (#0.5)) rh0) * dih_x`,
 432   (* {{{ proof *)
 433   [
 434      REWRITE_TAC[FUN_EQ_THM];
 435     REWRITE_TAC[add6;mul6;div6;sub6;constant6;rh0;scalar6];
 436     REWRITE_TAC[proj_y1;Sphere.ldih_x;Nonlinear_lemma.unit6;Sphere.lfun];
 437     REAL_ARITH_TAC;
 438   ]);;
 439   (* }}} *)
 440
 441 let functional_ldih2_x = prove_by_refinement(
 442   `ldih2_x = rotate2 ldih_x`,
 443   (* {{{ proof *)
 444   [
 445     REWRITE_TAC[FUN_EQ_THM];
 446   REWRITE_TAC[Sphere.rotate2;Sphere.ldih2_x;Sphere.ldih_x;Sphere.dih2_x];
 447   MESON_TAC[Nonlinear_lemma.dih_x_sym];
 448   ]);;
 449   (* }}} *)
 450
 451 let functional_ldih3_x = prove_by_refinement(
 452   `ldih3_x = rotate3 ldih_x`,
 453   (* {{{ proof *)
 454   [
 455     REWRITE_TAC[FUN_EQ_THM];
 456   REWRITE_TAC[Sphere.rotate3;Sphere.ldih3_x;Sphere.ldih_x;Sphere.dih3_x];
 457   ]);;
 458   (* }}} *)
 459
 460 let functional_ldih6_x = prove_by_refinement(
 461   `domain6
 462     (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
 463        &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
 464     ldih6_x
 465     (rotate6 ldih_x)`,
 466   (* {{{ proof *)
 467   [
 468   REWRITE_TAC[domain6 ];
 469   REWRITE_TAC[Sphere.rotate6;Sphere.ldih6_x;Sphere.ldih_x;Sphere.dih6_x;Sphere.dih6_y; Sphere.dih_y;LET_DEF;LET_END_DEF];
 470   BY(ASM_SIMP_TAC[sqrt_sqrt])
 471   ]);;
 472   (* }}} *)
 473
 474 let functional_eulerA_x = prove_by_refinement(
 475   `eulerA_x = proj_y1 * proj_y2 * proj_y3 +
 476      scalar6 (proj_y1 * (proj_x2 + proj_x3 - proj_x4)) (#0.5) +
 477      scalar6 (proj_y2 * (proj_x1 + proj_x3 - proj_x5)) (#0.5) +
 478      scalar6 (proj_y3 * (proj_x1 + proj_x2 - proj_x6)) (#0.5)
 479     `,
 480   (* {{{ proof *)
 481   [
 482     REWRITE_TAC[FUN_EQ_THM;mul6;add6; sub6;proj_y1;proj_y2;proj_y3;scalar6; constant6;proj_x1;proj_x2; proj_x3;proj_x4; proj_x5;proj_x6;Sphere.eulerA_x];
 483   BY(REAL_ARITH_TAC)
 484   ]);;
 485   (* }}} *)
 486
 487 let functional_gchi1_x = prove_by_refinement(
 488   `gchi1_x = uni (gchi,proj_y1) * dih_x`,
 489   (* {{{ proof *)
 490   [
 491   BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi1_x;uni;proj_y1;mul6]);
 492   ]);;
 493   (* }}} *)
 494
 495 let functional_gchi2_x = prove_by_refinement(
 496   `gchi2_x = uni (gchi,proj_y2) * dih2_x`,
 497   (* {{{ proof *)
 498   [
 499   BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi2_x;uni;proj_y2;mul6]);
 500   ]);;
 501   (* }}} *)
 502
 503 let functional_gchi3_x = prove_by_refinement(
 504   `gchi3_x = uni (gchi,proj_y3) * dih3_x`,
 505   (* {{{ proof *)
 506   [
 507   BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi3_x;uni;proj_y3;mul6]);
 508   ]);;
 509   (* }}} *)
 510
 511 let functional_gchi4_x = prove_by_refinement(
 512   `gchi4_x = uni (gchi,proj_y4) * dih4_x`,
 513   (* {{{ proof *)
 514   [
 515   BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi4_x;uni;proj_y4;mul6]);
 516   ]);;
 517   (* }}} *)
 518
 519 let functional_gchi5_x = prove_by_refinement(
 520   `gchi5_x = uni (gchi,proj_y5) * dih5_x`,
 521   (* {{{ proof *)
 522   [
 523   BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi5_x;uni;proj_y5;mul6]);
 524   ]);;
 525   (* }}} *)
 526
 527 let functional_gchi6_x = prove_by_refinement(
 528   `gchi6_x = uni (gchi,proj_y6) * dih6_x`,
 529   (* {{{ proof *)
 530   [
 531   BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi6_x;uni;proj_y6;mul6]);
 532   ]);;
 533   (* }}} *)
 534
 535 let functional_eta2_135 = prove_by_refinement(
 536   `eta2_135 = rotate3 eta2_126`,
 537   (* {{{ proof *)
 538   [
 539   REWRITE_TAC[FUN_EQ_THM;Sphere.rotate3;Sphere.eta2_135;Sphere.eta2_126];
 540   BY(MESON_TAC[Collect_geom.ETA_Y_SYYM])
 541   ]);;
 542   (* }}} *)
 543
 544 let functional_eta2_456 = prove_by_refinement(
 545   `eta2_456 = rotate4 eta2_135`,
 546   (* {{{ proof *)
 547   [
 548   REWRITE_TAC[FUN_EQ_THM;Sphere.rotate4;Sphere.eta2_456;Sphere.eta2_135;Sphere.rotate3;Sphere.eta2_126];
 549   BY(MESON_TAC[Collect_geom.ETA_Y_SYYM])
 550   ]);;
 551   (* }}} *)
 552
 553 let functional_vol3_x_sqrt = prove_by_refinement(
 554   `domain6
 555     (\x1 x2 x3 x4 x5 x6.
 556        &0 <= x1 /\ &0 <= x2 /\ &0 <=x6)
 557     vol3_x_sqrt
 558     (mk_126 vol_x)`,
 559   (* {{{ proof *)
 560   [
 561 BY(REWRITE_TAC[domain6;mk_126;two6;constant6;proj_x1;proj_x2;proj_x6;compose6;Nonlinear_lemma.vol3_vol_x])
 562   ]);;
 563   (* }}} *)
 564
 565 let functional_vol3f_x_lfun = prove_by_refinement(
 566   `domain6
 567        (\x1 x2 x3 x4 x5 x6.
 568         &0 <= x1 /\ &0 <= x2 /\ &0 <=x6)
 569        vol3f_x_lfun
 570        (constant6 ( &2 * mm1 / pi ) *
 571     (two6 * mk_126  dih_x + two6 * mk_126 dih2_x + two6 * mk_126 dih6_x +
 572        mk_126 dih3_x + mk_126 dih4_x + mk_126 dih5_x -
 573        constant6 ( &3 * pi))
 574     - (constant6 (&8 * mm2 / pi)) *
 575      (mk_126 ldih_x +   mk_126 ldih2_x + mk_126 ldih6_x ))
 576     `,
 577   (* {{{ proof *)
 578   [
 579     REWRITE_TAC[LET_DEF;LET_END_DEF;mk_126; two6; domain6;constant6;mul6;add6;sub6;proj_x1; compose6;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6];
 580   BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_lfun_alt])
 581   ]);;
 582   (* }}} *)
 583
 584 let functional_vol3f_x_sqrt2_lmplus = prove_by_refinement(
 585   `    (domain6
 586        (\x1 x2 x3 x4 x5 x6.
 587         (&2 * h0) pow 2 <= x1 /\ &0 <= x2 /\ &0 <=x6)
 588        vol3f_x_sqrt2_lmplus
 589        (constant6 ( &2 * mm1 / pi ) *
 590     (two6 * mk_126 dih_x  +
 591        two6 * mk_126 dih2_x +
 592        two6 * mk_126 dih6_x +
 593        mk_126 dih3_x +
 594         mk_126 dih4_x +
 595         mk_126 dih5_x -
 596        constant6 ( &3 * pi))
 597     - (constant6 (&8 * mm2 / pi)) *
 598      (mk_126 ldih2_x +
 599         mk_126 ldih6_x)))`,
 600   (* {{{ proof *)
 601   [
 602     REWRITE_TAC[LET_DEF;LET_END_DEF;mk_126;domain6; two6;constant6;mul6;add6;sub6;proj_x1;compose6;proj_x2; proj_x3;proj_x4;proj_x5;proj_x6];
 603   BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_sqrt2_lmplus_alt])
 604   ]);;
 605   (* }}} *)
 606
 607 let cos797 = new_definition `cos797 = cos(#0.797)`;;
 608
 609 let functional_asn797k = prove_by_refinement(
 610   `asn797k =
 611     proj_x1 * uni(asn,constant6 (cos797) *
 612                      uni(sin, constant6(pi) / proj_x1))`,
 613   (* {{{ proof *)
 614   [
 615   BY(REWRITE_TAC[FUN_EQ_THM;mul6;div6;uni;cos797;constant6;proj_x1;Sphere.asn797k]);
 616   ]);;
 617   (* }}} *)
 618
 619 let functional_asnFnhk = prove_by_refinement(
 620   `asnFnhk =
 621     proj_x2 * uni(asn,(proj_x1 * constant6 (sqrt3 / #4.0) +
 622                      (uni(sqrt,unit6 -
 623                              uni(pow2,(proj_x1 * constant6 (#0.5))))) *
 624                      constant6 (#0.5)) * uni(sin,constant6(pi)/proj_x2))`,
 625   (* {{{ proof *)
 626   [
 627     (REWRITE_TAC[FUN_EQ_THM;sub6;mul6; div6;Nonlinear_lemma.pow2;add6;unit6; uni;constant6;proj_x1; proj_x2;Sphere.asnFnhk]);
 628   BY(REWRITE_TAC[REAL_ARITH `x * #0.5 = x/ &2`])
 629   ]);;
 630   (* }}} *)
 631
 632 let functional_acs_sqrt_x1_d4 = prove_by_refinement(
 633   `acs_sqrt_x1_d4 = uni(acs,scalar6 proj_y1 (#0.25))`,
 634   (* {{{ proof *)
 635   [
 636     BY(REWRITE_TAC[FUN_EQ_THM;uni;mul6;constant6;scalar6;proj_y1; Sphere.acs_sqrt_x1_d4;arith `x * #0.25 = x/ &4`])
 637   ]);;
 638   (* }}} *)
 639
 640 let functional_acs_sqrt_x2_d4 = prove_by_refinement(
 641   `acs_sqrt_x2_d4 = uni(acs,scalar6 proj_y2 (#0.25))`,
 642   (* {{{ proof *)
 643   [
 644     BY(REWRITE_TAC[FUN_EQ_THM;uni;mul6;constant6;scalar6;proj_y2; Sphere.acs_sqrt_x2_d4;arith `x * #0.25 = x/ &4`])
 645   ]);;
 646   (* }}} *)
 647
 648 (* ldih5_x ldih6_x not in HOL Light*)
 649
 650 let functional_arclength_x_123 = prove_by_refinement(
 651   `let al_num = proj_x1 + proj_x2 - proj_x3  in
 652   let al_den = uni(sqrt,scalar6 (proj_x1 * proj_x2) ( &4)) in
 653   let domain =
 654     (\x1 x2 x3 x4 x5 x6. (&0 < x1 /\ &0 < x2 /\ &0 <= x3) /\
 655      (sqrt  x3 <= sqrt x1 + sqrt x2 /\ sqrt x1 <= sqrt x2 + sqrt x3 /\
 656       sqrt x2 <= sqrt x3 + sqrt x1)) in
 657     domain6 domain (arclength_x_123)  ( uni(acs, al_num / al_den ) )`,
 658   (* {{{ proof *)
 659   [
 660     REWRITE_TAC[LET_DEF;LET_END_DEF;];
 661      REWRITE_TAC[domain6];
 662     REWRITE_TAC[add6;mul6;div6;sub6;scalar6;constant6;uni];
 663     REWRITE_TAC[proj_x1;proj_x2;proj_x3;Sphere.arclength_x_123;];
 664     REPEAT STRIP_TAC;
 665     GMATCH_SIMP_TAC Trigonometry1.ACS_ARCLENGTH;
 666    ASM_REWRITE_TAC[];
 667    ASM_SIMP_TAC[SQRT_POS_LT;SQRT_POS_LE];
 668    AP_TERM_TAC;
 669    REPEAT(   GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
 670    ASM_SIMP_TAC[REAL_ARITH `&0 pow 2 = &0`;REAL_ARITH `&0 < x ==> &0 <= x`;REAL_ARITH `u + x * -- &1 = u - x`];
 671    AP_TERM_TAC;
 672    MATCH_MP_TAC EQ_SYM;
 673    REWRITE_TAC[REAL_ARITH `(x1 * x2)* &4 = x1 * (x2 * (&2 pow 2))`];
 674    REPEAT (GMATCH SQRT_MUL);
 675    GMATCH Euler_complement.SQRT_OF_POW_2_LE;
 676    REPEAT (GMATCH Real_ext.REAL_PROP_NN_MUL2);
 677    ASM_SIMP_TAC[REAL_ARITH `&0 <= &2 pow 2 /\ &0 <= &2`;REAL_ARITH `&0 < x ==> &0 <= x`];
 678    REAL_ARITH_TAC;
 679   ]);;
 680   (* }}} *)
 681
 682 let functional_arclength_234 = prove_by_refinement(
 683   `arclength_x_234 = rotate234 arclength_x_123`,
 684   (* {{{ proof *)
 685   [
 686   REWRITE_TAC[rotate234;Sphere.arclength_x_123];
 687     REWRITE_TAC[FUN_EQ_THM];
 688     REWRITE_TAC[add6;mul6;div6;sub6; constant6;Nonlinear_lemma.compose6;uni;Nonlinear_lemma.arclength_x_234; Sphere.arclength_x_123;];
 689     REWRITE_TAC[proj_x1;proj_x2;proj_x3;proj_x4];
 690   ]);;
 691   (* }}} *)
 692
 693 let functional_arclength_126 = prove_by_refinement(
 694   `arclength_x_126 = rotate126 arclength_x_123`,
 695   (* {{{ proof *)
 696   [
 697   REWRITE_TAC[rotate126];
 698     REWRITE_TAC[FUN_EQ_THM];
 699     REWRITE_TAC[add6;mul6;div6;sub6; constant6;Nonlinear_lemma.compose6;uni; Nonlinear_lemma.arclength_x_126; Sphere.arclength_x_123;];
 700     REWRITE_TAC[proj_x1;proj_x2;proj_x3;proj_x6];
 701   ]);;
 702   (* }}} *)
 703
 704 let functional_sol_euler_x_divsqrtdelta = prove_by_refinement(
 705   `domain6
 706     (\x1 x2 x3 x4 x5 x6.
 707        (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3))
 708     sol_euler_x_div_sqrtdelta
 709         ((uni(matan,(delta_x / (scalar6 (eulerA_x * eulerA_x) (&4))))) / eulerA_x)`,
 710   (* {{{ proof *)
 711   [
 712   REWRITE_TAC[domain6];
 713   REWRITE_TAC[uni;scalar6;Nonlin_def.sol_euler_x_div_sqrtdelta; functional_eulerA_x;div6;mul6;add6;sub6;constant6;proj_y1;proj_y2; proj_y3;proj_x1;proj_x2;proj_x3; proj_x4;proj_x5;proj_x6];
 714   REWRITE_TAC[REAL_ARITH ` (x/ &2 = x * (#0.5)) /\ ((a*b)*(c:real) = a*b*c)`;REAL_ARITH `&4 * a pow 2 = a* a * &4`;LET_DEF;LET_END_DEF];
 715   REPEAT STRIP_TAC;
 716   BY(ASM_SIMP_TAC[SQRT_MUL;Real_ext.REAL_PROP_NN_MUL2])
 717   ]);;
 718   (* }}} *)
 719
 720
 721 let functional_sol246_euler_x_div_sqrtdelta = prove_by_refinement(
 722   `sol_euler246_x_div_sqrtdelta = rotate4 sol_euler_x_div_sqrtdelta`,
 723   (* {{{ proof *)
 724   [
 725     REWRITE_TAC[FUN_EQ_THM];
 726     BY(REWRITE_TAC[Sphere.rotate4; Nonlin_def.sol_euler246_x_div_sqrtdelta])
 727   ]);;
 728   (* }}} *)
 729
 730 let functional_sol345_euler_x_div_sqrtdelta = prove_by_refinement(
 731   `sol_euler345_x_div_sqrtdelta = rotate5 sol_euler_x_div_sqrtdelta`,
 732   (* {{{ proof *)
 733   [
 734   REWRITE_TAC[FUN_EQ_THM];
 735   BY(REWRITE_TAC[Sphere.rotate5;Nonlin_def.sol_euler345_x_div_sqrtdelta])
 736   ]);;
 737   (* }}} *)
 738
 739 let functional_sol156_euler_x_div_sqrtdelta = prove_by_refinement(
 740   `sol_euler156_x_div_sqrtdelta = rotate6 sol_euler_x_div_sqrtdelta`,
 741   (* {{{ proof *)
 742   [
 743   REWRITE_TAC[FUN_EQ_THM];
 744   BY(REWRITE_TAC[Sphere.rotate6;Nonlin_def.sol_euler156_x_div_sqrtdelta])
 745   ]);;
 746   (* }}} *)
 747
 748 let functional_dih_x_div_sqrtdelta_posbranch = prove_by_refinement(
 749   `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1))
 750     dih_x_div_sqrtdelta_posbranch
 751     ((scalar6 proj_y1 (&2)) / (delta_x4) *
 752       uni(matan, (scalar6 (proj_x1 * delta_x) (&4)) / (uni(pow2,delta_x4))))`,
 753   (* {{{ proof *)
 754   [
 755   REWRITE_TAC[domain6];
 756   REWRITE_TAC[proj_y1;constant6;proj_x1;uni;scalar6;mul6;div6;Nonlin_def.dih_x_div_sqrtdelta_posbranch;];
 757   REWRITE_TAC[LET_DEF;LET_END_DEF;Nonlinear_lemma.pow2;arith `&4 * x * y = (x*y)* &4`];
 758   REPEAT WEAK_STRIP_TAC;
 759   ASM_SIMP_TAC[SQRT_MUL;arith `&0 <= &4`];
 760   (REWRITE_TAC[Collect_geom2.SQRT4_EQ2]);
 761   BY(REAL_ARITH_TAC)
 762   ]);;
 763   (* }}} *)
 764
 765
 766 (* dih2_x_div_sqrtdelta_posbranch not defined in HOL-Light *)
 767
 768 let functional_dih3_x_div_sqrtdelta_posbranch = prove_by_refinement(
 769   `dih3_x_div_sqrtdelta_posbranch = rotate3 dih_x_div_sqrtdelta_posbranch`,
 770   (* {{{ proof *)
 771   [
 772 BY(REWRITE_TAC[FUN_EQ_THM;Sphere.rotate3;Nonlin_def.dih3_x_div_sqrtdelta_posbranch]);
 773   ]);;
 774   (* }}} *)
 775
 776 let functional_dih4_x_div_sqrtdelta_posbranch =
 777   Nonlin_def.dih4_x_div_sqrtdelta_posbranch;;
 778
 779 let functional_dih5_x_div_sqrtdelta_posbranch = prove_by_refinement(
 780   `dih5_x_div_sqrtdelta_posbranch = rotate5 dih_x_div_sqrtdelta_posbranch`,
 781   (* {{{ proof *)
 782   [
 783 BY(REWRITE_TAC[FUN_EQ_THM;Sphere.rotate5;Nonlin_def.dih5_x_div_sqrtdelta_posbranch]);
 784   ]);;
 785   (* }}} *)
 786
 787 let functional_edge_flat2_x = prove_by_refinement(
 788   `domain6
 789    (\x1 x2 x3 x4 x5 x6.
 790             &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x5 /\ &0 <= x6)
 791     edge_flat2_x
 792     (uni(pow2,(uni(sqrt,
 793                    compose6(promote3_to_6 quadratic_root_plus_curry)
 794                      proj_x1
 795                  (proj_x1 * proj_x1 +
 796                     (proj_x3 - proj_x5) * (proj_x2 - proj_x6) -
 797                     proj_x1 * (proj_x2 + proj_x3 + proj_x5 + proj_x6))
 798 (                 proj_x1 * proj_x3 * proj_x5 +
 799                  proj_x1 * proj_x2 * proj_x6 -
 800                  proj_x3 * (proj_x1 + proj_x2 - proj_x3 + proj_x5 - proj_x6) *
 801                  proj_x6 -
 802                  proj_x2 * proj_x5 * (proj_x1 - proj_x2 + proj_x3 -
 803                                         proj_x5 + proj_x6))
 804                      zero6 zero6 zero6))))
 805     `,
 806   (* {{{ proof *)
 807   [
 808     BY(REWRITE_TAC[domain6; Nonlinear_lemma.edge_flat2_x_rewrite; compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6; zero6;constant6;add6;mul6; sub6;uni;promote3_to_6; Nonlinear_lemma.quadratic_root_plus_curry; Nonlinear_lemma.pow2])
 809   ]);;
 810   (* }}} *)
 811
 812 let functional_ldih_x_div_sqrtdelta_posbranch = prove_by_refinement(
 813   `ldih_x_div_sqrtdelta_posbranch =
 814     (scalar6 (constant6 h0 - scalar6 proj_y1 ( #0.5))  rh0)
 815     * dih_x_div_sqrtdelta_posbranch`,
 816   (* {{{ proof *)
 817 [
 818   REWRITE_TAC[FUN_EQ_THM;mul6;scalar6;rh0;Nonlin_def.ldih_x_div_sqrtdelta_posbranch;Sphere.lfun;constant6;mul6;sub6;proj_y1;];
 819   BY(REAL_ARITH_TAC)
 820   ]);;
 821   (* }}} *)
 822
 823 let functional_ldih2_x_div_sqrtdelta_posbranch =
 824   Nonlin_def.ldih2_x_div_sqrtdelta_posbranch;;
 825
 826 let functional_ldih3_x_div_sqrtdelta_posbranch =
 827   Nonlin_def.ldih3_x_div_sqrtdelta_posbranch;;
 828
 829
 830 let functional_ldih5_x_div_sqrtdelta_posbranch =
 831   Nonlin_def.ldih5_x_div_sqrtdelta_posbranch;;
 832
 833 let functional_ldih6_x_div_sqrtdelta_posbranch =
 834   Nonlin_def.ldih6_x_div_sqrtdelta_posbranch;;
 835
 836
 837 let functional1_rho = prove_by_refinement(
 838   `!y. rho y = y * (const1 * rh0 * (#0.5)) + (&1 - const1 * rh0)`,
 839   (* {{{ proof *)
 840   [
 841   REWRITE_TAC[Nonlinear_lemma.rho_alt;Sphere.h0;rh0];
 842   REPEAT WEAK_STRIP_TAC;
 843   BY(CONV_TAC REAL_RING)
 844   ]);;
 845   (* }}} *)
 846
 847 let functional1_flat_term_x = prove_by_refinement(
 848   `!y. flat_term_x y = (sqrt y - &2 * h0) * rh0 * sol0 * (#0.5)`,
 849   (* {{{ proof *)
 850   [
 851   REWRITE_TAC[Sphere.flat_term_x;Sphere.flat_term;Sphere.h0;rh0];
 852   REPEAT WEAK_STRIP_TAC;
 853   BY(BY(CONV_TAC REAL_RING))
 854   ]);;
 855   (* }}} *)
 856
 857 let functional1_lfun = prove_by_refinement(
 858   `!y. lfun y = ( h0 - y)*rh0`,
 859   (* {{{ proof *)
 860   [
 861   REWRITE_TAC[Sphere.lfun;rh0];
 862   BY(REAL_ARITH_TAC)
 863   ]);;
 864   (* }}} *)
 865
 866
 867 let functional_rhazim_x = prove_by_refinement(
 868   `domain6
 869     (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
 870        &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
 871     rhazim_x
 872     (uni (rho,proj_y1) * dih_x)`,
 873   (* {{{ proof *)
 874   [
 875   REWRITE_TAC[domain6];
 876   REWRITE_TAC[Sphere.rhazim_x;Sphere.rhazim;uni;proj_y1;mul6;Sphere.dih_y;LET_DEF;LET_END_DEF];
 877   REPEAT WEAK_STRIP_TAC;
 878   AP_TERM_TAC;
 879   REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
 880   BY(ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`;])
 881   ]);;
 882   (* }}} *)
 883
 884 let functional_rhazim2_x = prove_by_refinement(
 885   `rhazim2_x = rotate2 rhazim_x`,
 886   (* {{{ proof *)
 887   [
 888  REWRITE_TAC[FUN_EQ_THM];
 889   BY(REWRITE_TAC[Sphere.node2_y;Sphere.rotate2;Sphere.rhazim2_x;Sphere.rhazim_x;Sphere.rhazim2])
 890   ]);;
 891   (* }}} *)
 892
 893 let functional_rhazim3_x = prove_by_refinement(
 894   `rhazim3_x = rotate3 rhazim_x`,
 895   (* {{{ proof *)
 896   [
 897  REWRITE_TAC[FUN_EQ_THM];
 898   BY(REWRITE_TAC[Sphere.node3_y;Sphere.rotate3;Sphere.rhazim3_x;Sphere.rhazim_x;Sphere.rhazim3])
 899   ]);;
 900   (* }}} *)
 901
 902 let functional_taum_x = prove_by_refinement(
 903   `taum_x = rhazim_x + rhazim2_x +
 904     rhazim3_x - constant6 ((&1 + const1)*pi)`,
 905   (* {{{ proof *)
 906   [
 907  REWRITE_TAC[FUN_EQ_THM];
 908   (REWRITE_TAC[Sphere.taum_x;add6;sub6;mul6;constant6;unit6]);
 909   ]);;
 910   (* }}} *)
 911
 912 (* extra parameter cases *)
 913
 914 let functional_arclength_x1 = prove_by_refinement(
 915   `!a b.
 916     domain6    (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
 917     (arclength_x1 a b)
 918     (compose6
 919        arclength_x_123 proj_x1 (constant6 (a*a)) (constant6 (b*b))
 920        dummy6 dummy6 dummy6)`,
 921   (* {{{ proof *)
 922   [
 923   REWRITE_TAC[domain6;Sphere.arclength_x_123; compose6; Sphere.arclength_x1;proj_x1;constant6;dummy6; Sphere.arclength_y1];
 924   BY(BY(SIMP_TAC[Nonlinear_lemma.sqrtxx]))
 925   ]);;
 926   (* }}} *)
 927
 928 let functional_arclength_x2 = prove_by_refinement(
 929   `!a b.
 930     domain6    (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
 931     (arclength_x2 a b)
 932     (compose6
 933        arclength_x_123 proj_x2 (constant6 (a*a))  (constant6 (b*b))
 934        dummy6 dummy6 dummy6)`,
 935   (* {{{ proof *)
 936   [
 937   REWRITE_TAC[domain6;Sphere.arclength_x_123; compose6; Sphere.arclength_x2;proj_x2;constant6;dummy6; Sphere.arclength_y2];
 938   BY(BY(SIMP_TAC[Nonlinear_lemma.sqrtxx]))
 939   ]);;
 940   (* }}} *)
 941
 942 let functional_delta_126_x = prove_by_refinement(
 943   `!a b c. delta_126_x a b c = compose6 delta_x proj_x1 proj_x2
 944     (constant6 a) (constant6 b) (constant6 c) proj_x6`,
 945   (* {{{ proof *)
 946   [
 947   BY(REWRITE_TAC[FUN_EQ_THM; Sphere.delta_126_x;constant6;compose6;proj_x1;proj_x2;proj_x6 ])
 948   ]);;
 949   (* }}} *)
 950
 951 let functional_delta_234_x = prove_by_refinement(
 952   `!a b c. delta_234_x a b c = compose6 delta_x
 953     (constant6 a) proj_x2 proj_x3 proj_x4 (constant6 b) (constant6 c)`,
 954   (* {{{ proof *)
 955   [
 956   (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_234_x;constant6;compose6;proj_x2;proj_x3;proj_x4 ])
 957   ]);;
 958   (* }}} *)
 959
 960 let functional_delta_135_x = prove_by_refinement(
 961   `!a b c. delta_135_x a b c = compose6 delta_x
 962     proj_x1 (constant6 a) proj_x3 (constant6 b) proj_x5 (constant6 c)`,
 963   (* {{{ proof *)
 964   [
 965   (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_135_x;constant6;compose6;proj_x1;proj_x3;proj_x5 ])
 966   ]);;
 967   (* }}} *)
 968
 969 let functional_rhazim_x_div_sqrt_delta_posbranch = prove_by_refinement(
 970   `rhazim_x_div_sqrtdelta_posbranch =
 971     uni(rho,proj_y1) * dih_x_div_sqrtdelta_posbranch`,
 972   (* {{{ proof *)
 973   [
 974   BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]);
 975   ]);;
 976   (* }}} *)
 977
 978 let functional_rhazim2_x_div_sqrt_delta_posbranch = prove_by_refinement(
 979   `rhazim2_x_div_sqrtdelta_posbranch =
 980     rotate2 rhazim_x_div_sqrtdelta_posbranch`,
 981   (* {{{ proof *)
 982   [
 983   BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim2_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]);
 984   ]);;
 985   (* }}} *)
 986
 987 let functional_rhazim3_x_div_sqrt_delta_posbranch = prove_by_refinement(
 988   `rhazim3_x_div_sqrtdelta_posbranch =
 989     rotate3 rhazim_x_div_sqrtdelta_posbranch`,
 990   (* {{{ proof *)
 991   [
 992   BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim3_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]);
 993   ]);;
 994   (* }}} *)
 995
 996 let functional_tau_residual = prove_by_refinement(
 997   `tau_residual_x = rhazim_x_div_sqrtdelta_posbranch +
 998     rhazim2_x_div_sqrtdelta_posbranch + rhazim3_x_div_sqrtdelta_posbranch `,
 999   (* {{{ proof *)
1000   [
1001   (REWRITE_TAC[FUN_EQ_THM;Nonlin_def.tau_residual_x;add6]);
1002   ]);;
1003   (* }}} *)
1004
1005 let functional_halfbump_x1 = prove_by_refinement(
1006   `halfbump_x1 = promote1_to_6 halfbump_x`,
1007   (* {{{ proof *)
1008   [
1009   REWRITE_TAC[promote1_to_6;Nonlinear_lemma.halfbump_x1;FUN_EQ_THM];
1010   ]);;
1011   (* }}} *)
1012
1013 let functional_halfbump_x4 = prove_by_refinement(
1014   `halfbump_x4 = rotate4 halfbump_x1`,
1015   (* {{{ proof *)
1016   [
1017   BY(REWRITE_TAC[Sphere.rotate4;Nonlinear_lemma.halfbump_x4;Nonlinear_lemma.halfbump_x1;FUN_EQ_THM])
1018   ]);;
1019   (* }}} *)
1020
1021 (* two repeated defs =gamma2= deprecated. *)
1022 let gamma2_x_div_azim =  (* same as truncate_gamma2_x *)
1023   new_definition `gamma2_x_div_azim m x = (&8 - x)* sqrt x / (&24) -
1024   ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) -
1025       (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
1026
1027 let gamma2_x1_div_a = new_definition `gamma2_x1_div_a m =
1028   promote1_to_6 (gamma2_x_div_azim m)`;;
1029
1030 let nonf_gamma2_x1_div_a = prove_by_refinement(
1031   `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real).
1032     gamma2_x1_div_a m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim m x1`,
1033   (* {{{ proof *)
1034   [
1035   BY(REWRITE_TAC[FUN_EQ_THM;promote1_to_6;gamma2_x1_div_a])
1036   ]);;
1037   (* }}} *)
1038
1039 let nonf_gamma2_x1_div_a_v2 = prove_by_refinement(
1040   `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real).
1041     gamma2_x1_div_a_v2 m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim_v2 m x1`,
1042   (* {{{ proof *)
1043   [
1044   BY(REWRITE_TAC[FUN_EQ_THM;promote1_to_6;Nonlin_def.gamma2_x1_div_a_v2])
1045   ]);;
1046   (* }}} *)
1047
1048 let gamma3f_x_div_sqrtdelta = new_definition `gamma3f_x_div_sqrtdelta m4 m5 m6  =
1049   constant6 (&1/ &12)  -
1050     (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) +
1051                 mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) +
1052                 mk_456 (rotate4 (sol_euler_x_div_sqrtdelta))
1053                )  (&2 * mm1/ pi)
1054     -
1055       scalar6 (
1056         (scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) *
1057           mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch)) +
1058         (scalar6 (uni(lfun,(scalar6 proj_y5  #0.5))) m5) *
1059           mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch)) +
1060         (scalar6 (uni(lfun,(scalar6 proj_y6  #0.5))) m6) *
1061           mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch))
1062       )  (&8 * mm2 / pi))`;;
1063
1064 let shift_scalar6 = prove_by_refinement(
1065   `!f g m. (scalar6 f m) * g = f * (scalar6 g m)`,
1066   (* {{{ proof *)
1067   [
1068   REPEAT GEN_TAC;
1069   REWRITE_TAC[FUN_EQ_THM];
1070   REWRITE_TAC[mul6;scalar6];
1071   BY(REAL_ARITH_TAC)
1072   ]);;
1073   (* }}} *)
1074
1075 let gamma3f_x_div_sqrtdelta_alt = prove_by_refinement(
1076   `!m4 m5 m6. gamma3f_x_div_sqrtdelta m4 m5 m6  =
1077   constant6 (&1/ &12)  -
1078     (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) +
1079                 mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) +
1080                 mk_456 (rotate4 (sol_euler_x_div_sqrtdelta))
1081                )  (&2 * mm1/ pi)
1082     -
1083       scalar6 (
1084         ( (uni(lfun,(scalar6 proj_y4  #0.5))) ) *
1085           (scalar6 (mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch))) m4) +
1086         ( (uni(lfun,(scalar6 proj_y5  #0.5))) ) *
1087           (scalar6 ( mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch))) m5) +
1088         ( (uni(lfun,(scalar6 proj_y6  #0.5)))) *
1089           (scalar6 (mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch))) m6)
1090       )  (&8 * mm2 / pi)) `,
1091   (* {{{ proof *)
1092   [
1093   REPEAT WEAK_STRIP_TAC;
1094   REWRITE_TAC[gamma3f_x_div_sqrtdelta];
1095   BY(REWRITE_TAC[shift_scalar6])
1096   ]);;
1097   (* }}} *)
1098
1099 let vol3f_456 = new_definition `vol3f_456 m4 =
1100   scalar6 ( mk_456 (rotate5 sol_x) +
1101                 mk_456 (rotate6 sol_x) +
1102                 mk_456 (rotate4 sol_x)
1103                )  (&2 * mm1/ pi)
1104     -
1105       scalar6 (
1106         (scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) *
1107           mk_456 (rotate4 dih_x) +
1108         (uni(lfun,(scalar6 proj_y5  #0.5))) *
1109           mk_456 (rotate5 dih_x) +
1110         (uni(lfun,(scalar6 proj_y6  #0.5))) *
1111           mk_456 (rotate6 dih_x)
1112       )  (&8 * mm2 / pi)`;;
1113
1114 let gamma3_x = new_definition `gamma3_x m4  =
1115   mk_456 vol_x  -     vol3f_456 m4`;;
1116
1117 let gamma23_full8_x = new_definition `gamma23_full8_x m1 =
1118      (compose6 (gamma3_x m1)
1119        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) +
1120      (compose6 (gamma3_x m1)
1121        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
1122        scalar6 (dih_x -(mk_126 dih_x + mk_135 dih_x)) (#0.008)`;;
1123
1124 let gamma23_keep135_x = new_definition `gamma23_keep135_x m1 =
1125      (compose6 (gamma3_x m1)
1126        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
1127        scalar6 (dih_x - mk_135 dih_x) (#0.008)`;;
1128
1129 let nonf_gamma3_x = prove_by_refinement(
1130   `!m1 x1 x2 x3 x4 x5 x6.
1131     gamma3_x m1 x1 x2 x3 x4 x5 x6 =  vol_x (&2) (&2) (&2) x4 x5 x6 -
1132      ((sol_x x5 (&2) x4 (&2) x6 (&2) +
1133        sol_x x6 (&2) x5 (&2) x4 (&2) +
1134        sol_x x4 (&2) x6 (&2) x5 (&2)) *
1135       &2 *
1136       mm1 / pi -
1137       ((lfun (sqrt x4 * #0.5) * m1) * dih_x x4 (&2) x6 (&2) x5 (&2) +
1138        lfun (sqrt x5 * #0.5) * dih_x x5 (&2) x4 (&2) x6 (&2) +
1139        lfun (sqrt x6 * #0.5) * dih_x x6 (&2) x5 (&2) x4 (&2)) *
1140       &8 *
1141       mm2 / pi)`,
1142   (* {{{ proof *)
1143   [
1144 (REWRITE_TAC[gamma3_x;vol3f_456;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135])
1145   ]);;
1146   (* }}} *)
1147
1148 let nonf_gamma23_full8_x = prove_by_refinement(
1149   `!m1 x1 x2 x3 x4 x5 x6.
1150     gamma23_full8_x m1 x1 x2 x3 x4 x5 x6 =
1151     gamma3_x m1 (&0) (&0) (&0) x1 x2 x6 +
1152      gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 +
1153      (dih_x x1 x2 x3 x4 x5 x6 -
1154       (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) *
1155      #0.008`,
1156   (* {{{ proof *)
1157   [
1158 (REWRITE_TAC[gamma23_full8_x;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135])
1159   ]);;
1160   (* }}} *)
1161
1162 let nonf_gamma23_keep135_x = prove_by_refinement(
1163   `!m1 x1 x2 x3 x4 x5 x6.
1164     gamma23_keep135_x m1 x1 x2 x3 x4 x5 x6 =
1165   gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 +
1166      (dih_x x1 x2 x3 x4 x5 x6 - dih_x x1 (&2) x3 (&2) x5 (&2)) * #0.008
1167     `,
1168   (* {{{ proof *)
1169   [
1170 (REWRITE_TAC[gamma23_keep135_x;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135])
1171   ]);;
1172   (* }}} *)
1173
1174 let nonf_gamma3f_x_div_sqrtdelta = prove_by_refinement(
1175   `!m4 m5 m6 x1 x2 x3 x4 x5 x6.
1176     gamma3f_x_div_sqrtdelta m4 m5 m6 x1 x2 x3 x4 x5 x6 = &1 / &12 -
1177      ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) +
1178        sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) +
1179        sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) *
1180       &2 *
1181       mm1 / pi -
1182       ((lfun (sqrt x4 * #0.5) * m4) *
1183        dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) +
1184        (lfun (sqrt x5 * #0.5) * m5) *
1185        dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) +
1186        (lfun (sqrt x6 * #0.5) * m6) *
1187        dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) *
1188       &8 *
1189       mm2 / pi)`,
1190   (* {{{ proof *)
1191   [
1192 BY(REWRITE_TAC[gamma3f_x_div_sqrtdelta;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6])
1193   ]);;
1194   (* }}} *)
1195
1196
1197 (*
1198 extra parameter cases scratch
1199 *)
1200
1201 (* added 2013-May *)
1202
1203     let F_REWRITE_TAC = REWRITE_TAC[
1204       Nonlin_def.mud_126_x;Nonlin_def.mu6_x;Nonlin_def.mu_y;Nonlin_def.taud;Nonlin_def.taud_x;
1205                                     Nonlin_def.ups_126;Nonlin_def.edge2_126_x;Nonlin_def.edge2_flatD_x1;
1206                                     Nonlin_def.edge2_135_x;Nonlin_def.edge2_234_x;
1207                                     Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;Nonlin_def.mud_234_x;
1208                                     Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x;Nonlin_def.mudLs_135_x;
1209                                     LET_DEF;LET_END_DEF;
1210                                     Sphere.delta_y;
1211         Sphere.y_of_x;Sphere.flat_term_x;Sphere.flat_term;
1212         compose6;promote3_to_6;
1213         promote1_to_6;  domain6;
1214         constant6;
1215         uni;
1216         add6;mul6;
1217         sub6;div6;
1218         proj_y1;proj_y2;
1219         proj_y3;proj_y4;
1220         proj_y5;proj_y6;
1221         dummy6; zero6;
1222         proj_x1;proj_x2;
1223         proj_x4;proj_x3;
1224         proj_x5;        proj_x6;
1225 ];;
1226
1227     let taud_x_taud = prove_by_refinement(
1228   `!y1 y2 y3 y4 y5 y6.
1229     &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==>
1230     y_of_x taud_x y1 y2 y3 y4 y5 y6 = taud y1 y2 y3 y4 y5 y6`,
1231   (* {{{ proof *)
1232   [
1233     F_REWRITE_TAC;
1234   REPEAT WEAKER_STRIP_TAC;
1235   BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
1236   ]);;
1237   (* }}} *)
1238
1239 let mu6_x_mu_y = prove_by_refinement(
1240   `!y1 y2 y3 x4 x5 x6. &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==>
1241     mu_y y1 y2 y3 = mu6_x (y1 * y1) ( y2 * y2) (y3 * y3) x4 x5 x6 `,
1242   (* {{{ proof *)
1243   [
1244   F_REWRITE_TAC;
1245   REPEAT WEAKER_STRIP_TAC;
1246   BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
1247   ]);;
1248   (* }}} *)
1249
1250 let taud_x_ALT = prove_by_refinement(
1251   `domain6
1252     (\x1 x2 x3 x4 x5 x6.
1253        (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3))
1254     taud_x ( (promote1_to_6 flat_term_x) +
1255          (uni(sqrt,delta_x)) * mu6_x)`,
1256   (* {{{ proof *)
1257   [
1258     F_REWRITE_TAC;
1259   ]);;
1260   (* }}} *)
1261
1262 let functional_edge2_126_x = prove_by_refinement(
1263   `!d x4 x5.
1264     (edge2_126_x d x4 x5) =
1265     (let a =  proj_x6 in
1266      let c4 = constant6 x4 in
1267      let c5 = constant6 x5 in
1268      let b = constant6(-- &1) * compose6 delta_x1 zero6 proj_x2 proj_x1 proj_x6 (c5) (c4) in
1269      let c = constant6 ( d) - compose6 delta_x proj_x1 proj_x2 zero6 (c4) (c5)  proj_x6  in
1270      let ups_456 = compose6 ups_126 (c4) (c5) dummy6 dummy6 dummy6 proj_x6 in
1271      let discr = ups_456 * ups_126 + constant6( -- &4*d) * a in
1272         (uni(sqrt,discr) - b) /  (constant6 (&2) * a))`,
1273   (* {{{ proof *)
1274   [
1275     REWRITE_TAC[FUN_EQ_THM];
1276     F_REWRITE_TAC;
1277   REPEAT WEAKER_STRIP_TAC;
1278   TYPIFY_GOAL_THEN `!x1 x2 x3 x4 x5 x6.  d - delta_x x3 x1 x2 x6 x4 x5 = (x6) * x3 pow 2 + ( -- delta_x1 (&0) x2 x1 x6 x5 x4) * x3 + (d - delta_x (&0) x2 x1 x6 x5 x4)` (unlist ONCE_REWRITE_TAC);
1279     REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
1280     BY(REAL_ARITH_TAC);
1281   REWRITE_TAC[Nonlinear_lemma.abc_quadratic;Sphere.quadratic_root_plus];
1282   AP_THM_TAC;
1283   AP_TERM_TAC;
1284   MATCH_MP_TAC (arith `s1 = s2 ==> -- -- d + s1 = s2 - -- &1 * d`);
1285   AP_TERM_TAC;
1286   REWRITE_TAC[Nonlin_def.delta_x1;Sphere.ups_x;Sphere.delta_x];
1287   BY(REAL_ARITH_TAC)
1288   ]);;
1289   (* }}} *)
1290
1291 let functional_edge2_135_x = prove_by_refinement(
1292   `!d x4 x6.
1293     (edge2_135_x d x4 x6) =
1294     compose6 (edge2_126_x d x4 x6) (proj_x1) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x5)`,
1295   (* {{{ proof *)
1296   [
1297     REWRITE_TAC[FUN_EQ_THM];
1298     F_REWRITE_TAC;
1299   ]);;
1300   (* }}} *)
1301
1302 let functional_edge2_234_x = prove_by_refinement(
1303   `!d x5 x6.
1304     edge2_234_x d x5 x6 =
1305     compose6 (edge2_126_x d x5 x6) (proj_x2) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x4)`,
1306   (* {{{ proof *)
1307   [
1308     REWRITE_TAC[FUN_EQ_THM];
1309     F_REWRITE_TAC;
1310   ]);;
1311   (* }}} *)
1312
1313 let nonfunctional_edge2_126_x = prove_by_refinement(
1314   `!d x1 x2 a b c x4 x5 x6.
1315     (edge2_126_x d x4 x5) x1 x2 a b c x6 =
1316      ((sqrt (ups_x x4 x5 x6 * ups_x x1 x2 x6 + (-- &4 * d) * x6) -
1317        -- &1 * delta_x1 (&0) x2 x1 x6 x5 x4) /
1318       (&2 * x6))`,
1319   (* {{{ proof *)
1320   [
1321     REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x];
1322         F_REWRITE_TAC;
1323   ]);;
1324   (* }}} *)
1325
1326 let nonfunctional_edge2_135_x = prove_by_refinement(
1327   `!d x1 x3 x5 x4 x6 a b c.
1328     (edge2_135_x d x4 x6) x1 a x3 b x5 c = (sqrt (ups_x x4 x6 x5 * ups_x x1 x3 x5 + (-- &4 * d) * x5) -
1329       -- &1 * delta_x1 (&0) x3 x1 x5 x6 x4) /
1330      (&2 * x5)`,
1331   (* {{{ proof *)
1332   [
1333     REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x;functional_edge2_135_x];
1334         F_REWRITE_TAC;
1335   ]);;
1336   (* }}} *)
1337
1338 let nonfunctional_edge2_234_x = prove_by_refinement(
1339   `!d x2 x3 x4 x5 x6 a b c.
1340     (edge2_234_x d x5 x6) a x2 x3 x4 b c =
1341     (sqrt (ups_x x5 x6 x4 * ups_x x2 x3 x4 + (-- &4 * d) * x4) -
1342       -- &1 * delta_x1 (&0) x3 x2 x4 x6 x5) /
1343      (&2 * x4)`,
1344   (* {{{ proof *)
1345   [
1346     REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x;functional_edge2_234_x];
1347         F_REWRITE_TAC;
1348   ]);;
1349   (* }}} *)
1350
1351 let functional_mud_135_x = prove_by_refinement(
1352   `!y2 y4 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y2))
1353     (mud_135_x_v1 y2 y4 y6)
1354       (mul6 (compose6 (mu6_x) (constant6 (y2*y2)) proj_x1 proj_x3 dummy6 dummy6 dummy6)
1355         (uni(sqrt,(delta_135_x (y2*y2) (y4*y4) (y6*y6)))))`,
1356   (* {{{ proof *)
1357   [
1358     F_REWRITE_TAC;
1359   REPEAT WEAKER_STRIP_TAC;
1360   BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
1361   ]);;
1362   (* }}} *)
1363
1364 let functional_mud_126_x = prove_by_refinement(
1365   `!y3 y4 y5. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y3))
1366     (mud_126_x_v1 y3 y4 y5)
1367       (mul6 (compose6 (mu6_x) (constant6 (y3*y3)) proj_x1 proj_x2 dummy6 dummy6 dummy6)
1368         (uni(sqrt,(delta_126_x (y3*y3) (y4*y4) (y5*y5)))))`,
1369   (* {{{ proof *)
1370   [
1371     F_REWRITE_TAC;
1372   REPEAT WEAKER_STRIP_TAC;
1373   BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
1374   ]);;
1375   (* }}} *)
1376
1377 let functional_mud_234_x = prove_by_refinement(
1378   `!y1 y5 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y1))
1379     (mud_234_x_v1 y1 y5 y6)
1380       (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6)
1381         (uni(sqrt,(delta_234_x (y1*y1) (y5*y5) (y6*y6)))))`,
1382   (* {{{ proof *)
1383   [
1384     F_REWRITE_TAC;
1385   REPEAT WEAKER_STRIP_TAC;
1386   BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
1387   ]);;
1388   (* }}} *)
1389
1390 let nonfunctional_taud_D2 = prove_by_refinement(
1391   `!x1 x2 x3 x4 x5 x6. taud_D2_num_x x1 x2 x3 x4 x5 x6 = -- #0.07 *
1392      delta_x x1 x2 x3 x4 x5 x6 *
1393      delta_x1 x1 x2 x3 x4 x5 x6 *
1394      &2 *
1395      sqrt x1 -
1396      &1 / &4 *
1397      mu6_x x1 x2 x3 x4 x5 x6 *
1398      (delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1) pow 2 +
1399      &1 / &2 *
1400      mu6_x x1 x2 x3 x4 x5 x6 *
1401      delta_x x1 x2 x3 x4 x5 x6 *
1402      (-- &8 * x1 * x4 + delta_x1 x1 x2 x3 x4 x5 x6 * &2)`,
1403   (* {{{ proof *)
1404   [
1405     REWRITE_TAC[Nonlin_def.taud_D2_num_x];
1406       F_REWRITE_TAC;
1407   BY(REAL_ARITH_TAC)
1408   ]);;
1409   (* }}} *)
1410
1411 let nonfunctional_taud_D1 = prove_by_refinement(
1412   `!x1 x2 x3 x4 x5 x6. taud_D1_num_x x1 x2 x3 x4 x5 x6 =
1413      -- #0.07 * delta_x x1 x2 x3 x4 x5 x6 +
1414      &1 / &2 *
1415      mu6_x x1 x2 x3 x4 x5 x6 *
1416      delta_x1 x1 x2 x3 x4 x5 x6 *
1417      &2 *
1418      sqrt x1 +
1419      sol0 /  #0.52 * sqrt (delta_x x1 x2 x3 x4 x5 x6)`,
1420   (* {{{ proof *)
1421   [
1422     REWRITE_TAC[Nonlin_def.taud_D1_num_x];
1423     F_REWRITE_TAC;
1424   ]);;
1425   (* }}} *)
1426
1427 let nonfunctional_mu6_x = prove_by_refinement(
1428   `!x1 x2 x3 x4 x5 x6.
1429     mu6_x x1 x2 x3 x4 x5 x6 =
1430      (#0.012 + #0.07 * (#2.52 - sqrt(x1)) + #0.01 * (#2.52 * &2 - sqrt(x2) - sqrt(x3) ))`,
1431   (* {{{ proof *)
1432   [
1433     F_REWRITE_TAC;
1434   ]);;
1435   (* }}} *)
1436
1437 let functional_delta_x1 = prove_by_refinement(
1438   `delta_x1 = rotate4 delta_x4`,
1439   (* {{{ proof *)
1440   [
1441   REWRITE_TAC[FUN_EQ_THM;Sphere.rotate4;Nonlin_def.delta_x1;Sphere.delta_x4];
1442   BY(REAL_ARITH_TAC)
1443   ]);;
1444   (* }}} *)
1445
1446 let functional_dnum1 = prove_by_refinement(
1447   `dnum1 = (constant6 (&16) - constant6 (&2) * proj_x4) * proj_x1 +
1448     (proj_x5 - constant6 (&8)) * proj_x2 + (proj_x6 - constant6(&8)) * proj_x3`,
1449   (* {{{ proof *)
1450   [
1451   REWRITE_TAC[FUN_EQ_THM;Nonlin_def.dnum1];
1452   BY(F_REWRITE_TAC)
1453   ]);;
1454   (* }}} *)
1455
1456 let functional_ups_126 = prove_by_refinement(
1457   `ups_126=  two6 * proj_x1 * proj_x6 + two6 * proj_x2 * proj_x6 + two6 * proj_x1 * proj_x2
1458     - proj_x1 * proj_x1 - proj_x2 * proj_x2 - proj_x6 * proj_x6`,
1459   (* {{{ proof *)
1460   [
1461   REWRITE_TAC[FUN_EQ_THM;two6];
1462   F_REWRITE_TAC;
1463   REWRITE_TAC[Sphere.ups_x];
1464   BY(REAL_ARITH_TAC)
1465   ]);;
1466   (* }}} *)
1467
1468 let nonf_ups_126 = prove_by_refinement(
1469   `!x1 x2 x3 x4 x5 x6. ups_126 x1 x2 x3 x4 x5 x6 = ups_x x1 x2 x6`,
1470   (* {{{ proof *)
1471   [
1472   REWRITE_TAC[Nonlin_def.ups_126];
1473   BY(F_REWRITE_TAC)
1474   ]);;
1475   (* }}} *)
1476
1477
1478 let nonf_gamma3f_x_div_sqrt_delta = prove_by_refinement(
1479   `!p1 p2 p3 x1 x2 x3 x4 x5 x6.
1480     gamma3f_x_div_sqrtdelta p1 p2 p3 x1 x2 x3 x4 x5 x6 = &1 / &12 -
1481  ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) +
1482    sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) +
1483    sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) *
1484   &2 *
1485   mm1 / pi -
1486   ((lfun (sqrt x4 *  #0.5) * p1) *
1487    dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) +
1488    (lfun (sqrt x5 *  #0.5) * p2) *
1489    dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) +
1490    (lfun (sqrt x6 *  #0.5) * p3) *
1491    dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) *
1492   &8 *
1493   mm2 / pi)`,
1494   (* {{{ proof *)
1495   [
1496   REPEAT WEAKER_STRIP_TAC;
1497   REWRITE_TAC[Nonlin_def.gamma3f_x_div_sqrtdelta];
1498   F_REWRITE_TAC;
1499   REWRITE_TAC[Nonlin_def.scalar6];
1500   F_REWRITE_TAC;
1501   REWRITE_TAC[Nonlin_def.mk_456;Nonlin_def.scalar6];
1502   F_REWRITE_TAC;
1503   BY(REWRITE_TAC[Nonlin_def.two6;Nonlin_def.scalar6;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;Nonlin_def.constant6;Nonlin_def.proj_y4;Nonlin_def.proj_y5;Nonlin_def.proj_y6])
1504   ]);;
1505   (* }}} *)
1506
1507
1508  end;;