legacy/oldfan/IBZWFFH.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11
  12 module  Disjoint_fan = struct
  13
  14
  15
  16 open Sphere;;
  17 open Fan_defs;;
  18 open Hypermap_of_fan;;
  19 open Tactic_fan;;
  20 open Lemma_fan;;
  21 open Fan;;
  22 open Hypermap_of_fan;;
  23 open Node_fan;;
  24 open Azim_node;;
  25 open Sum_azim_node;;
  26
  27
  28
  29
  30 (* ========================================================================== *)
  31 (*                   DISJOINT IN   FAN                        *)
  32 (* ========================================================================== *)
  33
  34 let disjiont_union_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
  35 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
  36 ==>
  37  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
  38  (aff{x,v} UNION aff_gt {x,v} {w1})={}`,
  39
  40 REPEAT STRIP_TAC THEN REWRITE_TAC[UNION_OVER_INTER]
  41   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`  (v:real^3)`;` (w:real^3)`;` (w1:real^3)`] disjoint_set_fan) THEN ASM_REWRITE_TAC[]
  42   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`  (v:real^3)`;` (w:real^3)`;] disjoint_fan1) THEN ASM_REWRITE_TAC[]
  43   THEN ASM_SET_TAC[]);;
  44
  45
  46
  47 let aff_ge_subset_aff_gt_union_aff=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3).
  48 FAN(x,V,E)/\ {v,w} IN E
  49 ==>
  50 aff_ge {x} {v , w} SUBSET  (aff_gt {x , v} {w}) UNION (aff {x, v})`,
  51
  52 REPEAT STRIP_TAC THEN  MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;` (v:real^3)`] remark1_fan)
  53   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  54   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GE_1_2)
  55                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  56                 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GT_2_1)
  57                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  58                 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]affine_hull_2_fan)
  59                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[SUBSET; UNION;IN_ELIM_THM]
  60   THEN GEN_TAC THEN
  61 REWRITE_TAC[REAL_ARITH `(&0 <= (t3:real)) <=> (&0 < t3) \/ ( t3 = &0)`; TAUT `(a \/ b) /\ (c \/ d) /\ e /\ f <=> ((a \/ b)/\ c /\ e /\ f) \/ ((a \/ b) /\ d /\ e /\ f)`; EXISTS_OR_THM] THEN
  62 MATCH_MP_TAC MONO_OR THEN
  63 SUBGOAL_THEN `((?t1:real t2:real t3:real.
  64        (&0 < t2 \/ t2 = &0) /\
  65         &0< t3 /\
  66        t1 + t2 + t3 = &1 /\
  67        (x':real^3) = t1 % x + t2 % v + t3 % w)
  68   ==> (?t1 t2 t3.
  69             &0< t3 /\ t1 + t2 + t3 = &1 /\ x' = t1 % x + t2 % v + t3 % w))` ASSUME_TAC
  70 THENL
  71 [MESON_TAC[];
  72      ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
  73      REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN GEN_TAC THEN
  74      REWRITE_TAC[REAL_ARITH `(&0< (t2:real) \/ (t2 = &0)) <=> ( &0<= t2)`] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN
  75      POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
  76      REWRITE_TAC [REAL_ARITH `(a:real)+ &0 = a`; VECTOR_ARITH  `&0 % (w:real^3) = vec 0`;
  77      VECTOR_ARITH `  ((x':real^3) = (t1:real) % (x:real^3) + (t2:real) % (v:real^3) + vec 0)<=> ( x' = t1 % x + t2 % v )` ]
  78        THEN MESON_TAC[]]);;
  79
  80
  81 let IBZWFFH=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
  82 FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
  83 ==>
  84  w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
  85 aff_ge {x} {v , w1}={}`,
  86 REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w1:real^3)`] aff_ge_subset_aff_gt_union_aff)
  87   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
  88 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;`w:real^3`;` (w1:real^3)`] disjiont_union_fan)
  89   THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);;
  90
  91
  92
  93 end;;