legacy/oldtame/dangtatdatusb/UBHDEUU.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Lemma: UBHDEUU                                                             *)\r
   5 (* Chapter: Tame Hypermap                                                     *)\r
   6 (* Author: DANG TAT DAT                                                       *)\r
   7 (* Date: 2010-04-7                                                            *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 needs "/home/nyx/flyspeck/working/flyspeck_needs.hl";;\r
  11 flyspeck_needs "fan/fan.hl";;\r
  12 \r
  13 open Fan;;\r
  14 open Sphere;;\r
  15 \r
  16 (*Contravening Hypermap*)\r
  17 \r
  18 let h0 = new_definition `h0 = #1.26`;;  (*Definition Const real number*)\r
  19 \r
  20 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}`;;\r
  21 \r
  22 let ECTC = new_definition `ECTC (V:real^3->bool) = {{v,w}|(v IN V) /\ (w IN V)/\dist(v,w) = &2}`;;\r
  23 \r
  24 let ball_annulus = new_definition\r
  25   `ball_annulus = cball((vec 0:real^3) , &2 * h0) DIFF ball(vec 0, &2)`;;\r
  26 \r
  27 \r
  28 (*-----------Thang Lemma------------------------------------------------------*)\r
  29 let CKQOWSA_concl = `!(V:real^3 -> bool).(packing V) /\ (V SUBSET ball_annulus) ==> (FAN (vec 0,V,(ESTD V)))`;;\r
  30 \r
  31 let CKQOWSA = new_axiom CKQOWSA_concl;;\r
  32 \r
  33 (*---------------------------------------------------------------------------*)\r
  34 \r
  35 (*UBHDEUU*)\r
  36 \r
  37 g `!(V:real^3 -> bool).(packing V) /\ (V SUBSET ball_annulus) ==> (ECTC V) SUBSET (ESTD V)`;;\r
  38 e (PURE_REWRITE_TAC [ECTC;ESTD]);;\r
  39 e (REPEAT STRIP_TAC);;\r
  40 e (PURE_REWRITE_TAC [SUBSET]);;\r
  41 e (GEN_TAC);;\r
  42 e (REWRITE_TAC [IN_ELIM_THM]);;\r
  43 e (STRIP_TAC);;\r
  44 e (EXISTS_TAC `v:real^3`);;\r
  45 e (EXISTS_TAC `w:real^3`);;\r
  46 e (ASM_REWRITE_TAC[]);;\r
  47 e (STRIP_TAC);;\r
  48 e (ARITH_TAC);;\r
  49 e (REWRITE_TAC [h0]);;\r
  50 e (ARITH_TAC);;\r
  51 \r
  52 let ECTC_SUBSET_ESTD = top_thm();;\r
  53 \r
  54 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) `;;\r
  55 \r
  56 e (REPEAT GEN_TAC);;\r
  57 e (STRIP_TAC);;\r
  58 e (ASM_REWRITE_TAC[]);;\r
  59 e (ASM_MESON_TAC[CKQOWSA]);;\r
  60 e (ASM_REWRITE_TAC[]);;\r
  61 e (SUBGOAL_THEN `ECTC (V:real^3 -> bool) SUBSET ESTD V` ASSUME_TAC);;\r
  62 e (ASM_MESON_TAC [ECTC_SUBSET_ESTD]);;\r
  63 e (SUBGOAL_THEN `(FAN (vec 0,(V:real^3->bool),(ESTD V)))` ASSUME_TAC);;\r
  64 e (ASM_MESON_TAC[CKQOWSA]);;\r
  65 e (ASM_MESON_TAC [CTVTAQA]);;\r
  66 \r
  67 let UBHDEUU = top_thm();;