module Sharp = struct

(* SHARP CASES *)

(*
let gamma4f_delta0 = prove_by_refinement(
  mk_imp (`NONLIN:bool`,Sphere.all_forall `ineq [(sqrt8,y1,sqrt8);
		    (&2,y2,&2);
		    (&2,y3,&2);
		    (sqrt8,y4,sqrt8);
		    (&2,y5,&2);
		    (&2,y6,&2)]
 		    (gamma4f y1 y2 y3 y4 y5 y6 lmfun = &0)`),
  (* {{{ proof *)
  [
  BRANCH_TAC;
  X_OF_Y_TAC;
  REWRITE_TAC[Sphere.ineq];
  REPEAT STRIP_TAC;
  SUBGOAL_THEN `x1 = &8 /\ x2 = &4 /\ x3 = &4 /\ x4 = &8 /\ x5 = &4 /\ x6 = &4` (fun t -> REWRITE_TAC[t]);
  REPEAT (POP_ASSUM MP_TAC);
  REAL_ARITH_TAC;
  REPEAT (POP_ASSUM (fun t -> ALL_TAC));
  REWRITE_TAC[Sphere.vol_x;Sphere.gchi2_x;Sphere.gchi3_x;Sphere.gchi5_x;
    Sphere.gchi6_x;Sphere.dih_x;Sphere.dih2_x;Sphere.dih3_x;Sphere.dih4_x;
    Sphere.dih4_y;Sphere.dih5_x;Sphere.dih5_y;Sphere.dih6_x;Sphere.dih6_y;
    Sphere.dih_y];
  REWRITE_TAC[LET_DEF;LET_END_DEF];
  SUBGOAL_THEN `sqrt (&4) * sqrt(&4) = &4 /\ sqrt(&8) *sqrt (&8) = &8` 
     (fun t-> REWRITE_TAC[t]);
  CONJ_TAC THEN MATCH_MP_TAC sq_pow2 THEN EXISTS_TAC `&0` 
   THEN REAL_ARITH_TAC;
  REWRITE_TAC[delta_x_eq0;REAL_ARITH `x * &0 = &0 /\ -- -- x = x`;
      SQRT_0;delta_x4_eq64;atn2_0y];
  MP_TAC PI_POS;
  CONV_TAC  REAL_FIELD;    
  ]);;
  (* }}} *)
*)

end;;