(* ========================================================================= *)
(* FLYSPECK - BOOK FORMALIZATION                                             *)
(*                                                                           *)
(* Chapter: nonlinear inequalities                                           *)
(* Author:  Thomas Hales      *)
(* Date: 2012-05-20                                                          *)
(* ========================================================================= *)


(* May 2012 functional equational definitions of 
   inequality functions.

   This code is to be used in automated generation of C++ 
   taylorFunctions.

   scripts.hl generates ocaml Sphere2 module based on these lemmas.

   June 2012: truncate_* are all deprecated.  They can be deleted.

autogen:
   see functional_* lemmas in this file.
   see functional1_* lemmas in this file for univariate functions.

native_c:
	unit,x1,x2,x3,x4,x5,x6,
		y1,y2,y3,y4,y5,y6,
	  delta_x,delta_x4,
	  dih_x, sol_x,rad2_x,	
   	  num1,
	  norm2hh_x,

 *)

(* failwith "moodule";; *)

 module Functional_equation = struct  

  open Hales_tactic;;
  open Nonlinear_lemma;;

  let GMATCH = GMATCH_SIMP_TAC;;

let uni = new_definition `uni (f,x) x1 x2 x3 x4 x5 x6 = 
  (f:A->B) ( x x1 x2 x3 x4 x5 x6)`;;
let constant6 = new_definition `constant6 c x1 x2 x3 x4 x5 x6 = c`;;
let promote3_to_6 = new_definition
    `promote3_to_6 f x1 x2 x3 x4 x5 x6 = f x1 x2 x3`;;
let promote1_to_6 = new_definition
  `promote1_to_6 f x1 x2 x3 x4 x5 x6 = f x1`;;
let functional_proj_x1 = 
prove_by_refinement( `proj_x1 = promote1_to_6 I`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;promote1_to_6;proj_x1;I_DEF]; ]);;
(* }}} *) (* these are circular, because we will define rotatek as a composition of proj_xm *)
let functional_proj_x2 = 
prove_by_refinement( `proj_x2 = rotate2 proj_x1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x2;Sphere.rotate2]; ]);;
(* }}} *)
let functional_proj_x3 = 
prove_by_refinement( `proj_x3 = rotate3 proj_x1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x3;Sphere.rotate3]; ]);;
(* }}} *)
let functional_proj_x4 = 
prove_by_refinement( `proj_x4 = rotate4 proj_x1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x4;Sphere.rotate4]; ]);;
(* }}} *)
let functional_proj_x5 = 
prove_by_refinement( `proj_x5 = rotate5 proj_x1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x5;Sphere.rotate5]; ]);;
(* }}} *)
let functional_proj_x6 = 
prove_by_refinement( `proj_x6 = rotate6 proj_x1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x6;Sphere.rotate6]; ]);;
(* }}} *)
let rh0 = new_definition `rh0 = &1/(h0 - &1)`;;
let two6 = new_definition `two6 = constant6 ( &2)`;;
let zero6 = new_definition `zero6 = constant6 ( &0)`;;
let dummy6 = new_definition `dummy6 = constant6 ( &0)`;;
let four6 = new_definition `four6 = constant6 ( &4)`;;
let mk_126 = new_definition `mk_126 f =
  compose6 f proj_x1 proj_x2 two6 two6 two6 proj_x6`;;
let mk_456 = new_definition `mk_456 f =
  compose6 f two6 two6 two6 proj_x4 proj_x5 proj_x6`;;
let mk_135 = new_definition `mk_135 f = 
  compose6 f proj_x1 two6 proj_x3 two6 proj_x5 two6`;;
let add6 = new_definition `add6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6 + g x1 x2 x3 x4 x5 x6`;;
let scalar6 = new_definition `scalar6 f r x1 x2 x3 x4 x5 x6 = 
  (f x1 x2 x3 x4 x5 x6) * (r:real)`;;
let mul6 = new_definition `mul6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6 * g x1 x2 x3 x4 x5 x6`;;
let div6 = new_definition `div6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6 / g x1 x2 x3 x4 x5 x6`;;
let sub6 = new_definition `sub6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6  -  g x1 x2 x3 x4 x5 x6`;;
let proj_y1 = new_definition `proj_y1 x1 x2 x3 x4 x5 x6 = 
  sqrt(x1)`;;
let proj_y2 = new_definition `proj_y2 x1 x2 x3 x4 x5 x6 = 
  sqrt(x2)`;;
let proj_y3 = new_definition `proj_y3 x1 x2 x3 x4 x5 x6 = 
  sqrt(x3)`;;
let proj_y4 = new_definition `proj_y4 x1 x2 x3 x4 x5 x6 = 
  sqrt(x4)`;;
let proj_y5 = new_definition `proj_y5 x1 x2 x3 x4 x5 x6 = 
  sqrt(x5)`;;
let proj_y6 = new_definition `proj_y6 x1 x2 x3 x4 x5 x6 = 
  sqrt(x6)`;;
let domain6 = new_definition `domain6 h f g = 
  (!x1 x2 x3 x4 x5 x6. h x1 x2 x3 x4 x5 x6 ==>
      (f x1 x2 x3 x4 x5 x6 = g x1 x2 x3 x4 x5 x6))`;;
(* should be called something different, because we project out 3 coords *)
let rotate234 = new_definition `rotate234 f = 
  compose6 f proj_x2 proj_x3 proj_x4 unit6 unit6 unit6`;;
let rotate126 = new_definition `rotate126 f = 
  compose6 f proj_x1 proj_x2 proj_x6 unit6 unit6 unit6`;;
let rotate345 = new_definition `rotate345 f = 
  compose6 f proj_x3 proj_x4 proj_x5 unit6 unit6 unit6`;;
let functional_overload() = ( overload_interface ("+",`add6`); overload_interface ("-",`sub6`); overload_interface ("/",`div6`); overload_interface ("*",`mul6`));; let _ = functional_overload();; let proj_x1 = Nonlinear_lemma.proj_x1;; let proj_x2 = Nonlinear_lemma.proj_x2;; let proj_x3 = Nonlinear_lemma.proj_x3;; let proj_x4 = Nonlinear_lemma.proj_x4;; let proj_x5 = Nonlinear_lemma.proj_x5;; let proj_x6 = Nonlinear_lemma.proj_x6;; let unit6 = Nonlinear_lemma.unit6;; let compose6 = Nonlinear_lemma.compose6;;
let h0cut = new_definition `h0cut y = if (y <= &2 * h0) then &1 else &0`;;
let functional_proj_y1 = 
prove_by_refinement( `proj_y1 = promote1_to_6 sqrt`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;promote1_to_6;proj_y1]; ]);;
(* }}} *)
let functional_proj_y2 = 
prove_by_refinement( `proj_y2 = rotate2 proj_y1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y2;Sphere.rotate2]; ]);;
(* }}} *)
let functional_proj_y3 = 
prove_by_refinement( `proj_y3 = rotate3 proj_y1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y3;Sphere.rotate3]; ]);;
(* }}} *)
let functional_proj_y4 = 
prove_by_refinement( `proj_y4 = rotate4 proj_y1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y4;Sphere.rotate4]; ]);;
(* }}} *)
let functional_proj_y5 = 
prove_by_refinement( `proj_y5 = rotate5 proj_y1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y5;Sphere.rotate5]; ]);;
(* }}} *)
let functional_proj_y6 = 
prove_by_refinement( `proj_y6 = rotate6 proj_y1`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y6;Sphere.rotate6]; ]);;
(* }}} *)
let sqrt_sqrt = 
prove_by_refinement( `!x. &0 <= x ==> (sqrt x * sqrt x = x)`,
(* {{{ proof *) [ MESON_TAC[arith `&0 pow 2 = &0`;(SPEC `&0` Nonlinear_lemma.sq_pow2)]; ]);;
(* }}} *)
let functional_norm2hh_x = 
prove_by_refinement( `norm2hh_x = uni(pow2,(proj_y1 - constant6 (hminus + hplus))) + uni(pow2, proj_y2 - two6) + uni(pow2,proj_y3 - two6) + uni(pow2, proj_y4 - two6) + uni(pow2,proj_y5 - two6) + uni(pow2, proj_y6 - two6)`,
(* {{{ proof *) [ 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]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let functional_eta2_126 = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x6)) eta2_126 (uni(pow2,rotate126 (promote3_to_6 eta_x)))`,
(* {{{ proof *) [ 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]; BY(ASM_SIMP_TAC[sqrt_sqrt]) ]);;
(* }}} *)
let functional_rotate2 = 
prove_by_refinement( `!f. rotate2 f = compose6 f proj_x2 proj_x3 proj_x1 proj_x5 proj_x6 proj_x4`,
(* {{{ proof *) [ BY(REWRITE_TAC[Sphere.rotate2;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]); ]);;
(* }}} *)
let functional_rotate3 = 
prove_by_refinement( `!f. rotate3 f = compose6 f proj_x3 proj_x1 proj_x2 proj_x6 proj_x4 proj_x5`,
(* {{{ proof *) [ BY(REWRITE_TAC[Sphere.rotate3;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]); ]);;
(* }}} *)
let functional_rotate4 = 
prove_by_refinement( `!f. rotate4 f = compose6 f proj_x4 proj_x2 proj_x6 proj_x1 proj_x5 proj_x3`,
(* {{{ proof *) [ BY(REWRITE_TAC[Sphere.rotate4;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]); ]);;
(* }}} *)
let functional_rotate5 = 
prove_by_refinement( `!f. rotate5 f = compose6 f proj_x5 proj_x3 proj_x4 proj_x2 proj_x6 proj_x1`,
(* {{{ proof *) [ BY(REWRITE_TAC[Sphere.rotate5;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]); ]);;
(* }}} *)
let functional_rotate6 = 
prove_by_refinement( `!f. rotate6 f = compose6 f proj_x6 proj_x1 proj_x5 proj_x3 proj_x4 proj_x2`,
(* {{{ proof *) [ BY(REWRITE_TAC[Sphere.rotate6;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]); ]);;
(* }}} *)
let functional_x1_delta_x = 
prove_by_refinement( `x1_delta_x = proj_x1 * delta_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; BY(REWRITE_TAC[proj_x1;Sphere.x1_delta_x;mul6]) ]);;
(* }}} *)
let functional_delta4_squared_x = 
prove_by_refinement( `delta4_squared_x = uni(pow2,delta_x4)`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;uni;Nonlinear_lemma.pow2;Sphere.delta4_squared_x]) ]);;
(* }}} *)
let functional_vol_x = 
prove_by_refinement( `vol_x = scalar6 (uni(sqrt,delta_x)) (&1 / &12)`,
(* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;uni;Sphere.vol_x;scalar6]); BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let functional_dih2_x = 
prove_by_refinement( `dih2_x = rotate2 dih_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[Sphere.dih2_x;Sphere.rotate2]; BY(MESON_TAC[Nonlinear_lemma.dih_x_sym]) ]);;
(* }}} *)
let functional_dih3_x = 
prove_by_refinement( `dih3_x = rotate3 dih_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[Sphere.dih3_x;Sphere.rotate3]; ]);;
(* }}} *)
let functional_dih4_x = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) dih4_x (rotate4 dih_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6]; REWRITE_TAC[Sphere.dih4_x; Sphere.rotate4;Sphere.dih4_y; Sphere.dih_y; LET_DEF;LET_END_DEF]; REPEAT WEAK_STRIP_TAC; REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2)); BY(ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`]) ]);;
(* }}} *)
let functional_dih5_x = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) dih5_x (rotate5 dih_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6]; REWRITE_TAC[Sphere.dih5_x; Sphere.rotate5;Sphere.dih5_y; Sphere.dih_y; LET_DEF;LET_END_DEF]; REPEAT WEAK_STRIP_TAC; REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2)); (ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`]); MESON_TAC[Nonlinear_lemma.dih_x_sym;Nonlinear_lemma.dih_x_sym2]; ]);;
(* }}} *)
let functional_dih6_x = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) dih6_x (rotate6 dih_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6]; REWRITE_TAC[Sphere.dih6_x; Sphere.rotate6;Sphere.dih6_y;Sphere.dih_y; LET_DEF;LET_END_DEF]; REPEAT WEAK_STRIP_TAC; REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2)); (ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`]); ]);;
(* }}} *) (* let dih6_x' = new_definition `dih6_x' = rotate6 dih_x`;; let ldih6_x' = new_definition `!x1 x2 x3 x4 x5 x6. ldih6_x' x1 x2 x3 x4 x5 x6 = lfun (sqrt x6 / &2) * dih6_x' x1 x2 x3 x4 x5 x6`;; let gchi6_x' = new_definition `!x1 x2 x3 x4 x5 x6. gchi6_x x1 x2 x3 x4 x5 x6 = gchi (sqrt x6) * dih6_x' x1 x2 x3 x4 x5 x6`;; *)
let functional_lfun_y1 = 
prove_by_refinement( `lfun_y1 = scalar6 (scalar6 unit6 h0 - proj_x1) rh0`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[add6;scalar6;mul6;div6;sub6;constant6;rh0]; REWRITE_TAC[Sphere.lfun_y1;Sphere.lfun; Nonlinear_lemma.unit6;Nonlinear_lemma.proj_x1]; REAL_ARITH_TAC; ]);;
(* }}} *)
let functional_ldih_x = 
prove_by_refinement( `ldih_x = (scalar6 (scalar6 unit6 h0 - scalar6 proj_y1 (#0.5)) rh0) * dih_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[add6;mul6;div6;sub6;constant6;rh0;scalar6]; REWRITE_TAC[proj_y1;Sphere.ldih_x;Nonlinear_lemma.unit6;Sphere.lfun]; REAL_ARITH_TAC; ]);;
(* }}} *)
let functional_ldih2_x = 
prove_by_refinement( `ldih2_x = rotate2 ldih_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[Sphere.rotate2;Sphere.ldih2_x;Sphere.ldih_x;Sphere.dih2_x]; MESON_TAC[Nonlinear_lemma.dih_x_sym]; ]);;
(* }}} *)
let functional_ldih3_x = 
prove_by_refinement( `ldih3_x = rotate3 ldih_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[Sphere.rotate3;Sphere.ldih3_x;Sphere.ldih_x;Sphere.dih3_x]; ]);;
(* }}} *)
let functional_ldih6_x = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) ldih6_x (rotate6 ldih_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6 ]; REWRITE_TAC[Sphere.rotate6;Sphere.ldih6_x;Sphere.ldih_x;Sphere.dih6_x;Sphere.dih6_y; Sphere.dih_y;LET_DEF;LET_END_DEF]; BY(ASM_SIMP_TAC[sqrt_sqrt]) ]);;
(* }}} *)
let functional_eulerA_x = 
prove_by_refinement( `eulerA_x = proj_y1 * proj_y2 * proj_y3 + scalar6 (proj_y1 * (proj_x2 + proj_x3 - proj_x4)) (#0.5) + scalar6 (proj_y2 * (proj_x1 + proj_x3 - proj_x5)) (#0.5) + scalar6 (proj_y3 * (proj_x1 + proj_x2 - proj_x6)) (#0.5) `,
(* {{{ proof *) [ 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]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let functional_gchi1_x = 
prove_by_refinement( `gchi1_x = uni (gchi,proj_y1) * dih_x`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi1_x;uni;proj_y1;mul6]); ]);;
(* }}} *)
let functional_gchi2_x = 
prove_by_refinement( `gchi2_x = uni (gchi,proj_y2) * dih2_x`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi2_x;uni;proj_y2;mul6]); ]);;
(* }}} *)
let functional_gchi3_x = 
prove_by_refinement( `gchi3_x = uni (gchi,proj_y3) * dih3_x`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi3_x;uni;proj_y3;mul6]); ]);;
(* }}} *)
let functional_gchi4_x = 
prove_by_refinement( `gchi4_x = uni (gchi,proj_y4) * dih4_x`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi4_x;uni;proj_y4;mul6]); ]);;
(* }}} *)
let functional_gchi5_x = 
prove_by_refinement( `gchi5_x = uni (gchi,proj_y5) * dih5_x`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi5_x;uni;proj_y5;mul6]); ]);;
(* }}} *)
let functional_gchi6_x = 
prove_by_refinement( `gchi6_x = uni (gchi,proj_y6) * dih6_x`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi6_x;uni;proj_y6;mul6]); ]);;
(* }}} *)
let functional_eta2_135 = 
prove_by_refinement( `eta2_135 = rotate3 eta2_126`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Sphere.rotate3;Sphere.eta2_135;Sphere.eta2_126]; BY(MESON_TAC[Collect_geom.ETA_Y_SYYM]) ]);;
(* }}} *)
let functional_eta2_456 = 
prove_by_refinement( `eta2_456 = rotate4 eta2_135`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Sphere.rotate4;Sphere.eta2_456;Sphere.eta2_135;Sphere.rotate3;Sphere.eta2_126]; BY(MESON_TAC[Collect_geom.ETA_Y_SYYM]) ]);;
(* }}} *)
let functional_vol3_x_sqrt = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <=x6) vol3_x_sqrt (mk_126 vol_x)`,
(* {{{ proof *) [ BY(REWRITE_TAC[domain6;mk_126;two6;constant6;proj_x1;proj_x2;proj_x6;compose6;Nonlinear_lemma.vol3_vol_x]) ]);;
(* }}} *)
let functional_vol3f_x_lfun = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <=x6) vol3f_x_lfun (constant6 ( &2 * mm1 / pi ) * (two6 * mk_126 dih_x + two6 * mk_126 dih2_x + two6 * mk_126 dih6_x + mk_126 dih3_x + mk_126 dih4_x + mk_126 dih5_x - constant6 ( &3 * pi)) - (constant6 (&8 * mm2 / pi)) * (mk_126 ldih_x + mk_126 ldih2_x + mk_126 ldih6_x )) `,
(* {{{ proof *) [ 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]; BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_lfun_alt]) ]);;
(* }}} *)
let functional_vol3f_x_sqrt2_lmplus = 
prove_by_refinement( ` (domain6 (\x1 x2 x3 x4 x5 x6. (&2 * h0) pow 2 <= x1 /\ &0 <= x2 /\ &0 <=x6) vol3f_x_sqrt2_lmplus (constant6 ( &2 * mm1 / pi ) * (two6 * mk_126 dih_x + two6 * mk_126 dih2_x + two6 * mk_126 dih6_x + mk_126 dih3_x + mk_126 dih4_x + mk_126 dih5_x - constant6 ( &3 * pi)) - (constant6 (&8 * mm2 / pi)) * (mk_126 ldih2_x + mk_126 ldih6_x)))`,
(* {{{ proof *) [ 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]; BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_sqrt2_lmplus_alt]) ]);;
(* }}} *)
let cos797 = new_definition `cos797 = cos(#0.797)`;;
let functional_asn797k = 
prove_by_refinement( `asn797k = proj_x1 * uni(asn,constant6 (cos797) * uni(sin, constant6(pi) / proj_x1))`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;mul6;div6;uni;cos797;constant6;proj_x1;Sphere.asn797k]); ]);;
(* }}} *)
let functional_asnFnhk = 
prove_by_refinement( `asnFnhk = proj_x2 * uni(asn,(proj_x1 * constant6 (sqrt3 / #4.0) + (uni(sqrt,unit6 - uni(pow2,(proj_x1 * constant6 (#0.5))))) * constant6 (#0.5)) * uni(sin,constant6(pi)/proj_x2))`,
(* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;sub6;mul6; div6;Nonlinear_lemma.pow2;add6;unit6; uni;constant6;proj_x1; proj_x2;Sphere.asnFnhk]); BY(REWRITE_TAC[REAL_ARITH `x * #0.5 = x/ &2`]) ]);;
(* }}} *)
let functional_acs_sqrt_x1_d4 = 
prove_by_refinement( `acs_sqrt_x1_d4 = uni(acs,scalar6 proj_y1 (#0.25))`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;uni;mul6;constant6;scalar6;proj_y1; Sphere.acs_sqrt_x1_d4;arith `x * #0.25 = x/ &4`]) ]);;
(* }}} *)
let functional_acs_sqrt_x2_d4 = 
prove_by_refinement( `acs_sqrt_x2_d4 = uni(acs,scalar6 proj_y2 (#0.25))`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;uni;mul6;constant6;scalar6;proj_y2; Sphere.acs_sqrt_x2_d4;arith `x * #0.25 = x/ &4`]) ]);;
(* }}} *) (* ldih5_x ldih6_x not in HOL Light*)
let functional_arclength_x_123 = 
prove_by_refinement( `let al_num = proj_x1 + proj_x2 - proj_x3 in let al_den = uni(sqrt,scalar6 (proj_x1 * proj_x2) ( &4)) in let domain = (\x1 x2 x3 x4 x5 x6. (&0 < x1 /\ &0 < x2 /\ &0 <= x3) /\ (sqrt x3 <= sqrt x1 + sqrt x2 /\ sqrt x1 <= sqrt x2 + sqrt x3 /\ sqrt x2 <= sqrt x3 + sqrt x1)) in domain6 domain (arclength_x_123) ( uni(acs, al_num / al_den ) )`,
(* {{{ proof *) [ REWRITE_TAC[LET_DEF;LET_END_DEF;]; REWRITE_TAC[domain6]; REWRITE_TAC[add6;mul6;div6;sub6;scalar6;constant6;uni]; REWRITE_TAC[proj_x1;proj_x2;proj_x3;Sphere.arclength_x_123;]; REPEAT STRIP_TAC; GMATCH_SIMP_TAC Trigonometry1.ACS_ARCLENGTH; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[SQRT_POS_LT;SQRT_POS_LE]; AP_TERM_TAC; REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2)); ASM_SIMP_TAC[REAL_ARITH `&0 pow 2 = &0`;REAL_ARITH `&0 < x ==> &0 <= x`;REAL_ARITH `u + x * -- &1 = u - x`]; AP_TERM_TAC; MATCH_MP_TAC EQ_SYM; REWRITE_TAC[REAL_ARITH `(x1 * x2)* &4 = x1 * (x2 * (&2 pow 2))`]; REPEAT (GMATCH SQRT_MUL); GMATCH Euler_complement.SQRT_OF_POW_2_LE; REPEAT (GMATCH Real_ext.REAL_PROP_NN_MUL2); ASM_SIMP_TAC[REAL_ARITH `&0 <= &2 pow 2 /\ &0 <= &2`;REAL_ARITH `&0 < x ==> &0 <= x`]; REAL_ARITH_TAC; ]);;
(* }}} *)
let functional_arclength_234 = 
prove_by_refinement( `arclength_x_234 = rotate234 arclength_x_123`,
(* {{{ proof *) [ REWRITE_TAC[rotate234;Sphere.arclength_x_123]; REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[add6;mul6;div6;sub6; constant6;Nonlinear_lemma.compose6;uni;Nonlinear_lemma.arclength_x_234; Sphere.arclength_x_123;]; REWRITE_TAC[proj_x1;proj_x2;proj_x3;proj_x4]; ]);;
(* }}} *)
let functional_arclength_126 = 
prove_by_refinement( `arclength_x_126 = rotate126 arclength_x_123`,
(* {{{ proof *) [ REWRITE_TAC[rotate126]; REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[add6;mul6;div6;sub6; constant6;Nonlinear_lemma.compose6;uni; Nonlinear_lemma.arclength_x_126; Sphere.arclength_x_123;]; REWRITE_TAC[proj_x1;proj_x2;proj_x3;proj_x6]; ]);;
(* }}} *)
let functional_sol_euler_x_divsqrtdelta = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3)) sol_euler_x_div_sqrtdelta ((uni(matan,(delta_x / (scalar6 (eulerA_x * eulerA_x) (&4))))) / eulerA_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6]; 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]; 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]; REPEAT STRIP_TAC; BY(ASM_SIMP_TAC[SQRT_MUL;Real_ext.REAL_PROP_NN_MUL2]) ]);;
(* }}} *)
let functional_sol246_euler_x_div_sqrtdelta = 
prove_by_refinement( `sol_euler246_x_div_sqrtdelta = rotate4 sol_euler_x_div_sqrtdelta`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; BY(REWRITE_TAC[Sphere.rotate4; Nonlin_def.sol_euler246_x_div_sqrtdelta]) ]);;
(* }}} *)
let functional_sol345_euler_x_div_sqrtdelta = 
prove_by_refinement( `sol_euler345_x_div_sqrtdelta = rotate5 sol_euler_x_div_sqrtdelta`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; BY(REWRITE_TAC[Sphere.rotate5;Nonlin_def.sol_euler345_x_div_sqrtdelta]) ]);;
(* }}} *)
let functional_sol156_euler_x_div_sqrtdelta = 
prove_by_refinement( `sol_euler156_x_div_sqrtdelta = rotate6 sol_euler_x_div_sqrtdelta`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; BY(REWRITE_TAC[Sphere.rotate6;Nonlin_def.sol_euler156_x_div_sqrtdelta]) ]);;
(* }}} *)
let functional_dih_x_div_sqrtdelta_posbranch = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1)) dih_x_div_sqrtdelta_posbranch ((scalar6 proj_y1 (&2)) / (delta_x4) * uni(matan, (scalar6 (proj_x1 * delta_x) (&4)) / (uni(pow2,delta_x4))))`,
(* {{{ proof *) [ REWRITE_TAC[domain6]; REWRITE_TAC[proj_y1;constant6;proj_x1;uni;scalar6;mul6;div6;Nonlin_def.dih_x_div_sqrtdelta_posbranch;]; REWRITE_TAC[LET_DEF;LET_END_DEF;Nonlinear_lemma.pow2;arith `&4 * x * y = (x*y)* &4`]; REPEAT WEAK_STRIP_TAC; ASM_SIMP_TAC[SQRT_MUL;arith `&0 <= &4`]; (REWRITE_TAC[Collect_geom2.SQRT4_EQ2]); BY(REAL_ARITH_TAC) ]);;
(* }}} *) (* dih2_x_div_sqrtdelta_posbranch not defined in HOL-Light *)
let functional_dih3_x_div_sqrtdelta_posbranch = 
prove_by_refinement( `dih3_x_div_sqrtdelta_posbranch = rotate3 dih_x_div_sqrtdelta_posbranch`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.rotate3;Nonlin_def.dih3_x_div_sqrtdelta_posbranch]); ]);;
(* }}} *) let functional_dih4_x_div_sqrtdelta_posbranch = Nonlin_def.dih4_x_div_sqrtdelta_posbranch;;
let functional_dih5_x_div_sqrtdelta_posbranch = 
prove_by_refinement( `dih5_x_div_sqrtdelta_posbranch = rotate5 dih_x_div_sqrtdelta_posbranch`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.rotate5;Nonlin_def.dih5_x_div_sqrtdelta_posbranch]); ]);;
(* }}} *)
let functional_edge_flat2_x = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x5 /\ &0 <= x6) edge_flat2_x (uni(pow2,(uni(sqrt, compose6(promote3_to_6 quadratic_root_plus_curry) proj_x1 (proj_x1 * proj_x1 + (proj_x3 - proj_x5) * (proj_x2 - proj_x6) - proj_x1 * (proj_x2 + proj_x3 + proj_x5 + proj_x6)) ( proj_x1 * proj_x3 * proj_x5 + proj_x1 * proj_x2 * proj_x6 - proj_x3 * (proj_x1 + proj_x2 - proj_x3 + proj_x5 - proj_x6) * proj_x6 - proj_x2 * proj_x5 * (proj_x1 - proj_x2 + proj_x3 - proj_x5 + proj_x6)) zero6 zero6 zero6)))) `,
(* {{{ proof *) [ 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]) ]);;
(* }}} *)
let functional_ldih_x_div_sqrtdelta_posbranch = 
prove_by_refinement( `ldih_x_div_sqrtdelta_posbranch = (scalar6 (constant6 h0 - scalar6 proj_y1 ( #0.5)) rh0) * dih_x_div_sqrtdelta_posbranch`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;mul6;scalar6;rh0;Nonlin_def.ldih_x_div_sqrtdelta_posbranch;Sphere.lfun;constant6;mul6;sub6;proj_y1;]; BY(REAL_ARITH_TAC) ]);;
(* }}} *) let functional_ldih2_x_div_sqrtdelta_posbranch = Nonlin_def.ldih2_x_div_sqrtdelta_posbranch;; let functional_ldih3_x_div_sqrtdelta_posbranch = Nonlin_def.ldih3_x_div_sqrtdelta_posbranch;; let functional_ldih5_x_div_sqrtdelta_posbranch = Nonlin_def.ldih5_x_div_sqrtdelta_posbranch;; let functional_ldih6_x_div_sqrtdelta_posbranch = Nonlin_def.ldih6_x_div_sqrtdelta_posbranch;;
let functional1_rho = 
prove_by_refinement( `!y. rho y = y * (const1 * rh0 * (#0.5)) + (&1 - const1 * rh0)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlinear_lemma.rho_alt;Sphere.h0;rh0]; REPEAT WEAK_STRIP_TAC; BY(CONV_TAC REAL_RING) ]);;
(* }}} *)
let functional1_flat_term_x = 
prove_by_refinement( `!y. flat_term_x y = (sqrt y - &2 * h0) * rh0 * sol0 * (#0.5)`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.flat_term_x;Sphere.flat_term;Sphere.h0;rh0]; REPEAT WEAK_STRIP_TAC; BY(BY(CONV_TAC REAL_RING)) ]);;
(* }}} *)
let functional1_lfun = 
prove_by_refinement( `!y. lfun y = ( h0 - y)*rh0`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.lfun;rh0]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let functional_rhazim_x = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) rhazim_x (uni (rho,proj_y1) * dih_x)`,
(* {{{ proof *) [ REWRITE_TAC[domain6]; REWRITE_TAC[Sphere.rhazim_x;Sphere.rhazim;uni;proj_y1;mul6;Sphere.dih_y;LET_DEF;LET_END_DEF]; REPEAT WEAK_STRIP_TAC; AP_TERM_TAC; REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2)); BY(ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`;]) ]);;
(* }}} *)
let functional_rhazim2_x = 
prove_by_refinement( `rhazim2_x = rotate2 rhazim_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; BY(REWRITE_TAC[Sphere.node2_y;Sphere.rotate2;Sphere.rhazim2_x;Sphere.rhazim_x;Sphere.rhazim2]) ]);;
(* }}} *)
let functional_rhazim3_x = 
prove_by_refinement( `rhazim3_x = rotate3 rhazim_x`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; BY(REWRITE_TAC[Sphere.node3_y;Sphere.rotate3;Sphere.rhazim3_x;Sphere.rhazim_x;Sphere.rhazim3]) ]);;
(* }}} *)
let functional_taum_x = 
prove_by_refinement( `taum_x = rhazim_x + rhazim2_x + rhazim3_x - constant6 ((&1 + const1)*pi)`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; (REWRITE_TAC[Sphere.taum_x;add6;sub6;mul6;constant6;unit6]); ]);;
(* }}} *) (* extra parameter cases *)
let functional_arclength_x1 = 
prove_by_refinement( `!a b. domain6 (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b) (arclength_x1 a b) (compose6 arclength_x_123 proj_x1 (constant6 (a*a)) (constant6 (b*b)) dummy6 dummy6 dummy6)`,
(* {{{ proof *) [ REWRITE_TAC[domain6;Sphere.arclength_x_123; compose6; Sphere.arclength_x1;proj_x1;constant6;dummy6; Sphere.arclength_y1]; BY(BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])) ]);;
(* }}} *)
let functional_arclength_x2 = 
prove_by_refinement( `!a b. domain6 (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b) (arclength_x2 a b) (compose6 arclength_x_123 proj_x2 (constant6 (a*a)) (constant6 (b*b)) dummy6 dummy6 dummy6)`,
(* {{{ proof *) [ REWRITE_TAC[domain6;Sphere.arclength_x_123; compose6; Sphere.arclength_x2;proj_x2;constant6;dummy6; Sphere.arclength_y2]; BY(BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])) ]);;
(* }}} *)
let functional_delta_126_x = 
prove_by_refinement( `!a b c. delta_126_x a b c = compose6 delta_x proj_x1 proj_x2 (constant6 a) (constant6 b) (constant6 c) proj_x6`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM; Sphere.delta_126_x;constant6;compose6;proj_x1;proj_x2;proj_x6 ]) ]);;
(* }}} *)
let functional_delta_234_x = 
prove_by_refinement( `!a b c. delta_234_x a b c = compose6 delta_x (constant6 a) proj_x2 proj_x3 proj_x4 (constant6 b) (constant6 c)`,
(* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_234_x;constant6;compose6;proj_x2;proj_x3;proj_x4 ]) ]);;
(* }}} *)
let functional_delta_135_x = 
prove_by_refinement( `!a b c. delta_135_x a b c = compose6 delta_x proj_x1 (constant6 a) proj_x3 (constant6 b) proj_x5 (constant6 c)`,
(* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_135_x;constant6;compose6;proj_x1;proj_x3;proj_x5 ]) ]);;
(* }}} *)
let functional_rhazim_x_div_sqrt_delta_posbranch = 
prove_by_refinement( `rhazim_x_div_sqrtdelta_posbranch = uni(rho,proj_y1) * dih_x_div_sqrtdelta_posbranch`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]); ]);;
(* }}} *)
let functional_rhazim2_x_div_sqrt_delta_posbranch = 
prove_by_refinement( `rhazim2_x_div_sqrtdelta_posbranch = rotate2 rhazim_x_div_sqrtdelta_posbranch`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim2_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]); ]);;
(* }}} *)
let functional_rhazim3_x_div_sqrt_delta_posbranch = 
prove_by_refinement( `rhazim3_x_div_sqrtdelta_posbranch = rotate3 rhazim_x_div_sqrtdelta_posbranch`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim3_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]); ]);;
(* }}} *)
let functional_tau_residual = 
prove_by_refinement( `tau_residual_x = rhazim_x_div_sqrtdelta_posbranch + rhazim2_x_div_sqrtdelta_posbranch + rhazim3_x_div_sqrtdelta_posbranch `,
(* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Nonlin_def.tau_residual_x;add6]); ]);;
(* }}} *)
let functional_halfbump_x1 = 
prove_by_refinement( `halfbump_x1 = promote1_to_6 halfbump_x`,
(* {{{ proof *) [ REWRITE_TAC[promote1_to_6;Nonlinear_lemma.halfbump_x1;FUN_EQ_THM]; ]);;
(* }}} *)
let functional_halfbump_x4 = 
prove_by_refinement( `halfbump_x4 = rotate4 halfbump_x1`,
(* {{{ proof *) [ BY(REWRITE_TAC[Sphere.rotate4;Nonlinear_lemma.halfbump_x4;Nonlinear_lemma.halfbump_x1;FUN_EQ_THM]) ]);;
(* }}} *) (* two repeated defs =gamma2= deprecated. *) let gamma2_x_div_azim = (* same as truncate_gamma2_x *) new_definition `gamma2_x_div_azim m x = (&8 - x)* sqrt x / (&24) - ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) - (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
let gamma2_x1_div_a = new_definition `gamma2_x1_div_a m = 
  promote1_to_6 (gamma2_x_div_azim m)`;;
let nonf_gamma2_x1_div_a = 
prove_by_refinement( `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real). gamma2_x1_div_a m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim m x1`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;promote1_to_6;gamma2_x1_div_a]) ]);;
(* }}} *)
let nonf_gamma2_x1_div_a_v2 = 
prove_by_refinement( `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real). gamma2_x1_div_a_v2 m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim_v2 m x1`,
(* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;promote1_to_6;Nonlin_def.gamma2_x1_div_a_v2]) ]);;
(* }}} *)
let gamma3f_x_div_sqrtdelta = new_definition `gamma3f_x_div_sqrtdelta m4 m5 m6  = 
  constant6 (&1/ &12)  - 
    (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) +
		mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) + 
		mk_456 (rotate4 (sol_euler_x_div_sqrtdelta)) 
	       )  (&2 * mm1/ pi)    
    -       
      scalar6 (
	(scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) * 
	  mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch)) +
	(scalar6 (uni(lfun,(scalar6 proj_y5  #0.5))) m5) * 
	  mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch)) +
	(scalar6 (uni(lfun,(scalar6 proj_y6  #0.5))) m6) * 
	  mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch))
      )  (&8 * mm2 / pi))`;;
let shift_scalar6 = 
prove_by_refinement( `!f g m. (scalar6 f m) * g = f * (scalar6 g m)`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[mul6;scalar6]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let gamma3f_x_div_sqrtdelta_alt = 
prove_by_refinement( `!m4 m5 m6. gamma3f_x_div_sqrtdelta m4 m5 m6 = constant6 (&1/ &12) - (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) + mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) + mk_456 (rotate4 (sol_euler_x_div_sqrtdelta)) ) (&2 * mm1/ pi) - scalar6 ( ( (uni(lfun,(scalar6 proj_y4 #0.5))) ) * (scalar6 (mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch))) m4) + ( (uni(lfun,(scalar6 proj_y5 #0.5))) ) * (scalar6 ( mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch))) m5) + ( (uni(lfun,(scalar6 proj_y6 #0.5)))) * (scalar6 (mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch))) m6) ) (&8 * mm2 / pi)) `,
(* {{{ proof *) [ REPEAT WEAK_STRIP_TAC; REWRITE_TAC[gamma3f_x_div_sqrtdelta]; BY(REWRITE_TAC[shift_scalar6]) ]);;
(* }}} *)
let vol3f_456 = new_definition `vol3f_456 m4 = 
  scalar6 ( mk_456 (rotate5 sol_x) +
		mk_456 (rotate6 sol_x) + 
		mk_456 (rotate4 sol_x) 
	       )  (&2 * mm1/ pi)    
    -       
      scalar6 (
	(scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) * 
	  mk_456 (rotate4 dih_x) +
	(uni(lfun,(scalar6 proj_y5  #0.5))) * 
	  mk_456 (rotate5 dih_x) +
	(uni(lfun,(scalar6 proj_y6  #0.5))) * 
	  mk_456 (rotate6 dih_x)
      )  (&8 * mm2 / pi)`;;
let gamma3_x = new_definition `gamma3_x m4  = 
  mk_456 vol_x  -     vol3f_456 m4`;;
let gamma23_full8_x = new_definition `gamma23_full8_x m1 =
     (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) + 
     (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
       scalar6 (dih_x -(mk_126 dih_x + mk_135 dih_x)) (#0.008)`;;
let gamma23_keep135_x = new_definition `gamma23_keep135_x m1 =
     (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
       scalar6 (dih_x - mk_135 dih_x) (#0.008)`;;
let nonf_gamma3_x = 
prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma3_x m1 x1 x2 x3 x4 x5 x6 = vol_x (&2) (&2) (&2) x4 x5 x6 - ((sol_x x5 (&2) x4 (&2) x6 (&2) + sol_x x6 (&2) x5 (&2) x4 (&2) + sol_x x4 (&2) x6 (&2) x5 (&2)) * &2 * mm1 / pi - ((lfun (sqrt x4 * #0.5) * m1) * dih_x x4 (&2) x6 (&2) x5 (&2) + lfun (sqrt x5 * #0.5) * dih_x x5 (&2) x4 (&2) x6 (&2) + lfun (sqrt x6 * #0.5) * dih_x x6 (&2) x5 (&2) x4 (&2)) * &8 * mm2 / pi)`,
(* {{{ proof *) [ (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]) ]);;
(* }}} *)
let nonf_gamma23_full8_x = 
prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma23_full8_x m1 x1 x2 x3 x4 x5 x6 = gamma3_x m1 (&0) (&0) (&0) x1 x2 x6 + gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 + (dih_x x1 x2 x3 x4 x5 x6 - (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) * #0.008`,
(* {{{ proof *) [ (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]) ]);;
(* }}} *)
let nonf_gamma23_keep135_x = 
prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma23_keep135_x m1 x1 x2 x3 x4 x5 x6 = gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 + (dih_x x1 x2 x3 x4 x5 x6 - dih_x x1 (&2) x3 (&2) x5 (&2)) * #0.008 `,
(* {{{ proof *) [ (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]) ]);;
(* }}} *)
let nonf_gamma3f_x_div_sqrtdelta = 
prove_by_refinement( `!m4 m5 m6 x1 x2 x3 x4 x5 x6. gamma3f_x_div_sqrtdelta m4 m5 m6 x1 x2 x3 x4 x5 x6 = &1 / &12 - ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) + sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) + sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) * &2 * mm1 / pi - ((lfun (sqrt x4 * #0.5) * m4) * dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) + (lfun (sqrt x5 * #0.5) * m5) * dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) + (lfun (sqrt x6 * #0.5) * m6) * dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) * &8 * mm2 / pi)`,
(* {{{ proof *) [ 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]) ]);;
(* }}} *) (* extra parameter cases scratch *) (* added 2013-May *) let F_REWRITE_TAC = REWRITE_TAC[ Nonlin_def.mud_126_x;Nonlin_def.mu6_x;Nonlin_def.mu_y;Nonlin_def.taud;Nonlin_def.taud_x; Nonlin_def.ups_126;Nonlin_def.edge2_126_x;Nonlin_def.edge2_flatD_x1; Nonlin_def.edge2_135_x;Nonlin_def.edge2_234_x; Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;Nonlin_def.mud_234_x; Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x;Nonlin_def.mudLs_135_x; LET_DEF;LET_END_DEF; Sphere.delta_y; Sphere.y_of_x;Sphere.flat_term_x;Sphere.flat_term; compose6;promote3_to_6; promote1_to_6; domain6; constant6; uni; add6;mul6; sub6;div6; proj_y1;proj_y2; proj_y3;proj_y4; proj_y5;proj_y6; dummy6; zero6; proj_x1;proj_x2; proj_x4;proj_x3; proj_x5; proj_x6; ];;
let taud_x_taud = 
prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==> y_of_x taud_x y1 y2 y3 y4 y5 y6 = taud y1 y2 y3 y4 y5 y6`,
(* {{{ proof *) [ F_REWRITE_TAC; REPEAT WEAKER_STRIP_TAC; BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx]) ]);;
(* }}} *)
let mu6_x_mu_y = 
prove_by_refinement( `!y1 y2 y3 x4 x5 x6. &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==> mu_y y1 y2 y3 = mu6_x (y1 * y1) ( y2 * y2) (y3 * y3) x4 x5 x6 `,
(* {{{ proof *) [ F_REWRITE_TAC; REPEAT WEAKER_STRIP_TAC; BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx]) ]);;
(* }}} *)
let taud_x_ALT = 
prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3)) taud_x ( (promote1_to_6 flat_term_x) + (uni(sqrt,delta_x)) * mu6_x)`,
(* {{{ proof *) [ F_REWRITE_TAC; ]);;
(* }}} *)
let functional_edge2_126_x = 
prove_by_refinement( `!d x4 x5. (edge2_126_x d x4 x5) = (let a = proj_x6 in let c4 = constant6 x4 in let c5 = constant6 x5 in let b = constant6(-- &1) * compose6 delta_x1 zero6 proj_x2 proj_x1 proj_x6 (c5) (c4) in let c = constant6 ( d) - compose6 delta_x proj_x1 proj_x2 zero6 (c4) (c5) proj_x6 in let ups_456 = compose6 ups_126 (c4) (c5) dummy6 dummy6 dummy6 proj_x6 in let discr = ups_456 * ups_126 + constant6( -- &4*d) * a in (uni(sqrt,discr) - b) / (constant6 (&2) * a))`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; F_REWRITE_TAC; REPEAT WEAKER_STRIP_TAC; 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); REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1]; BY(REAL_ARITH_TAC); REWRITE_TAC[Nonlinear_lemma.abc_quadratic;Sphere.quadratic_root_plus]; AP_THM_TAC; AP_TERM_TAC; MATCH_MP_TAC (arith `s1 = s2 ==> -- -- d + s1 = s2 - -- &1 * d`); AP_TERM_TAC; REWRITE_TAC[Nonlin_def.delta_x1;Sphere.ups_x;Sphere.delta_x]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let functional_edge2_135_x = 
prove_by_refinement( `!d x4 x6. (edge2_135_x d x4 x6) = compose6 (edge2_126_x d x4 x6) (proj_x1) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x5)`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; F_REWRITE_TAC; ]);;
(* }}} *)
let functional_edge2_234_x = 
prove_by_refinement( `!d x5 x6. edge2_234_x d x5 x6 = compose6 (edge2_126_x d x5 x6) (proj_x2) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x4)`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM]; F_REWRITE_TAC; ]);;
(* }}} *)
let nonfunctional_edge2_126_x = 
prove_by_refinement( `!d x1 x2 a b c x4 x5 x6. (edge2_126_x d x4 x5) x1 x2 a b c x6 = ((sqrt (ups_x x4 x5 x6 * ups_x x1 x2 x6 + (-- &4 * d) * x6) - -- &1 * delta_x1 (&0) x2 x1 x6 x5 x4) / (&2 * x6))`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x]; F_REWRITE_TAC; ]);;
(* }}} *)
let nonfunctional_edge2_135_x = 
prove_by_refinement( `!d x1 x3 x5 x4 x6 a b c. (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) - -- &1 * delta_x1 (&0) x3 x1 x5 x6 x4) / (&2 * x5)`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x;functional_edge2_135_x]; F_REWRITE_TAC; ]);;
(* }}} *)
let nonfunctional_edge2_234_x = 
prove_by_refinement( `!d x2 x3 x4 x5 x6 a b c. (edge2_234_x d x5 x6) a x2 x3 x4 b c = (sqrt (ups_x x5 x6 x4 * ups_x x2 x3 x4 + (-- &4 * d) * x4) - -- &1 * delta_x1 (&0) x3 x2 x4 x6 x5) / (&2 * x4)`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x;functional_edge2_234_x]; F_REWRITE_TAC; ]);;
(* }}} *)
let functional_mud_135_x = 
prove_by_refinement( `!y2 y4 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y2)) (mud_135_x_v1 y2 y4 y6) (mul6 (compose6 (mu6_x) (constant6 (y2*y2)) proj_x1 proj_x3 dummy6 dummy6 dummy6) (uni(sqrt,(delta_135_x (y2*y2) (y4*y4) (y6*y6)))))`,
(* {{{ proof *) [ F_REWRITE_TAC; REPEAT WEAKER_STRIP_TAC; BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx]) ]);;
(* }}} *)
let functional_mud_126_x = 
prove_by_refinement( `!y3 y4 y5. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y3)) (mud_126_x_v1 y3 y4 y5) (mul6 (compose6 (mu6_x) (constant6 (y3*y3)) proj_x1 proj_x2 dummy6 dummy6 dummy6) (uni(sqrt,(delta_126_x (y3*y3) (y4*y4) (y5*y5)))))`,
(* {{{ proof *) [ F_REWRITE_TAC; REPEAT WEAKER_STRIP_TAC; BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx]) ]);;
(* }}} *)
let functional_mud_234_x = 
prove_by_refinement( `!y1 y5 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y1)) (mud_234_x_v1 y1 y5 y6) (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6) (uni(sqrt,(delta_234_x (y1*y1) (y5*y5) (y6*y6)))))`,
(* {{{ proof *) [ F_REWRITE_TAC; REPEAT WEAKER_STRIP_TAC; BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx]) ]);;
(* }}} *)
let nonfunctional_taud_D2 = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6. taud_D2_num_x x1 x2 x3 x4 x5 x6 = -- #0.07 * delta_x x1 x2 x3 x4 x5 x6 * delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1 - &1 / &4 * mu6_x x1 x2 x3 x4 x5 x6 * (delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1) pow 2 + &1 / &2 * mu6_x x1 x2 x3 x4 x5 x6 * delta_x x1 x2 x3 x4 x5 x6 * (-- &8 * x1 * x4 + delta_x1 x1 x2 x3 x4 x5 x6 * &2)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.taud_D2_num_x]; F_REWRITE_TAC; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let nonfunctional_taud_D1 = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6. taud_D1_num_x x1 x2 x3 x4 x5 x6 = -- #0.07 * delta_x x1 x2 x3 x4 x5 x6 + &1 / &2 * mu6_x x1 x2 x3 x4 x5 x6 * delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1 + sol0 / #0.52 * sqrt (delta_x x1 x2 x3 x4 x5 x6)`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.taud_D1_num_x]; F_REWRITE_TAC; ]);;
(* }}} *)
let nonfunctional_mu6_x = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6. mu6_x x1 x2 x3 x4 x5 x6 = (#0.012 + #0.07 * (#2.52 - sqrt(x1)) + #0.01 * (#2.52 * &2 - sqrt(x2) - sqrt(x3) ))`,
(* {{{ proof *) [ F_REWRITE_TAC; ]);;
(* }}} *)
let functional_delta_x1 = 
prove_by_refinement( `delta_x1 = rotate4 delta_x4`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Sphere.rotate4;Nonlin_def.delta_x1;Sphere.delta_x4]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let functional_dnum1 = 
prove_by_refinement( `dnum1 = (constant6 (&16) - constant6 (&2) * proj_x4) * proj_x1 + (proj_x5 - constant6 (&8)) * proj_x2 + (proj_x6 - constant6(&8)) * proj_x3`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Nonlin_def.dnum1]; BY(F_REWRITE_TAC) ]);;
(* }}} *)
let functional_ups_126 = 
prove_by_refinement( `ups_126= two6 * proj_x1 * proj_x6 + two6 * proj_x2 * proj_x6 + two6 * proj_x1 * proj_x2 - proj_x1 * proj_x1 - proj_x2 * proj_x2 - proj_x6 * proj_x6`,
(* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;two6]; F_REWRITE_TAC; REWRITE_TAC[Sphere.ups_x]; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let nonf_ups_126 = 
prove_by_refinement( `!x1 x2 x3 x4 x5 x6. ups_126 x1 x2 x3 x4 x5 x6 = ups_x x1 x2 x6`,
(* {{{ proof *) [ REWRITE_TAC[Nonlin_def.ups_126]; BY(F_REWRITE_TAC) ]);;
(* }}} *)
let nonf_gamma3f_x_div_sqrt_delta = 
prove_by_refinement( `!p1 p2 p3 x1 x2 x3 x4 x5 x6. gamma3f_x_div_sqrtdelta p1 p2 p3 x1 x2 x3 x4 x5 x6 = &1 / &12 - ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) + sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) + sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) * &2 * mm1 / pi - ((lfun (sqrt x4 * #0.5) * p1) * dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) + (lfun (sqrt x5 * #0.5) * p2) * dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) + (lfun (sqrt x6 * #0.5) * p3) * dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) * &8 * mm2 / pi)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Nonlin_def.gamma3f_x_div_sqrtdelta]; F_REWRITE_TAC; REWRITE_TAC[Nonlin_def.scalar6]; F_REWRITE_TAC; REWRITE_TAC[Nonlin_def.mk_456;Nonlin_def.scalar6]; F_REWRITE_TAC; 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]) ]);;
(* }}} *) end;;