(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Lemma: UBHDEUU                                                             *)
(* Chapter: Tame Hypermap                                                     *)
(* Author: DANG TAT DAT                                                       *)
(* Date: 2010-04-7                                                            *)
(* ========================================================================== *)

needs "/home/nyx/flyspeck/working/flyspeck_needs.hl";;
flyspeck_needs "fan/fan.hl";;

open Fan;;
open Sphere;;

(*Contravening Hypermap*)

let h0 = new_definition `h0 = #1.26`;;  (*Definition Const real number*)

let ESTD = new_definition `ESTD (V:real^3->bool) = {{v,w}|(v IN V) /\ (w IN V)/\ (&0) < dist(v,w) /\ dist(v,w) <= (&2)*h0}`;;

let ECTC = new_definition `ECTC (V:real^3->bool) = {{v,w}|(v IN V) /\ (w IN V)/\dist(v,w) = &2}`;;

let ball_annulus = new_definition
  `ball_annulus = cball((vec 0:real^3) , &2 * h0) DIFF ball(vec 0, &2)`;;


(*-----------Thang Lemma------------------------------------------------------*)
let CKQOWSA_concl = `!(V:real^3 -> bool).(packing V) /\ (V SUBSET ball_annulus) ==> (FAN (vec 0,V,(ESTD V)))`;;

let CKQOWSA = new_axiom CKQOWSA_concl;;

(*---------------------------------------------------------------------------*)

(*UBHDEUU*)

g `!(V:real^3 -> bool).(packing V) /\ (V SUBSET ball_annulus) ==> (ECTC V) SUBSET (ESTD V)`;;
e (PURE_REWRITE_TAC [ECTC;ESTD]);;
e (REPEAT STRIP_TAC);;
e (PURE_REWRITE_TAC [SUBSET]);;
e (GEN_TAC);;
e (REWRITE_TAC [IN_ELIM_THM]);;
e (STRIP_TAC);;
e (EXISTS_TAC `v:real^3`);;
e (EXISTS_TAC `w:real^3`);;
e (ASM_REWRITE_TAC[]);;
e (STRIP_TAC);;
e (ARITH_TAC);;
e (REWRITE_TAC [h0]);;
e (ARITH_TAC);;

let ECTC_SUBSET_ESTD = top_thm();;

g `!(V:real^3 -> bool) (E:(real^3 ->bool)->bool). (packing V) /\ (V SUBSET ball_annulus) /\ ((E = ESTD V) \/ (E = ECTC V)) ==> FAN (vec 0,V,E) `;;

e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ASM_MESON_TAC[CKQOWSA]);;
e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `ECTC (V:real^3 -> bool) SUBSET ESTD V` ASSUME_TAC);;
e (ASM_MESON_TAC [ECTC_SUBSET_ESTD]);;
e (SUBGOAL_THEN `(FAN (vec 0,(V:real^3->bool),(ESTD V)))` ASSUME_TAC);;
e (ASM_MESON_TAC[CKQOWSA]);;
e (ASM_MESON_TAC [CTVTAQA]);;

let UBHDEUU = top_thm();;