text_formalization/nonlinear/sharp.hl

   1
   2
   3 module Sharp = struct
   4
   5 (* SHARP CASES *)
   6
   7 (*
   8 let gamma4f_delta0 = prove_by_refinement(
   9   mk_imp (`NONLIN:bool`,Sphere.all_forall `ineq [(sqrt8,y1,sqrt8);
  10                     (&2,y2,&2);
  11                     (&2,y3,&2);
  12                     (sqrt8,y4,sqrt8);
  13                     (&2,y5,&2);
  14                     (&2,y6,&2)]
  15                     (gamma4f y1 y2 y3 y4 y5 y6 lmfun = &0)`),
  16   (* {{{ proof *)
  17   [
  18   BRANCH_TAC;
  19   X_OF_Y_TAC;
  20   REWRITE_TAC[Sphere.ineq];
  21   REPEAT STRIP_TAC;
  22   SUBGOAL_THEN `x1 = &8 /\ x2 = &4 /\ x3 = &4 /\ x4 = &8 /\ x5 = &4 /\ x6 = &4` (fun t -> REWRITE_TAC[t]);
  23   REPEAT (POP_ASSUM MP_TAC);
  24   REAL_ARITH_TAC;
  25   REPEAT (POP_ASSUM (fun t -> ALL_TAC));
  26   REWRITE_TAC[Sphere.vol_x;Sphere.gchi2_x;Sphere.gchi3_x;Sphere.gchi5_x;
  27     Sphere.gchi6_x;Sphere.dih_x;Sphere.dih2_x;Sphere.dih3_x;Sphere.dih4_x;
  28     Sphere.dih4_y;Sphere.dih5_x;Sphere.dih5_y;Sphere.dih6_x;Sphere.dih6_y;
  29     Sphere.dih_y];
  30   REWRITE_TAC[LET_DEF;LET_END_DEF];
  31   SUBGOAL_THEN `sqrt (&4) * sqrt(&4) = &4 /\ sqrt(&8) *sqrt (&8) = &8`
  32      (fun t-> REWRITE_TAC[t]);
  33   CONJ_TAC THEN MATCH_MP_TAC sq_pow2 THEN EXISTS_TAC `&0`
  34    THEN REAL_ARITH_TAC;
  35   REWRITE_TAC[delta_x_eq0;REAL_ARITH `x * &0 = &0 /\ -- -- x = x`;
  36       SQRT_0;delta_x4_eq64;atn2_0y];
  37   MP_TAC PI_POS;
  38   CONV_TAC  REAL_FIELD;
  39   ]);;
  40   (* }}} *)
  41 *)
  42
  43 end;;