legacy/oldfan/fully_surrounded.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  Fully_surrounded = 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 open Disjoint_fan;;
  27 open Lead_fan;;
  28 open Fan_misc;;
  29 open Leads_into_fan;;
  30
  31
  32 (* ========================================================================== *)
  33 (*   FAN  AND CONVEX              *)
  34 (* ========================================================================== *)
  35
  36
  37 let fan81=new_definition`fan81 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> azim_fan x V E v u <pi)`;;
  38
  39 let fan80=new_definition`fan80 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> &0< azim x v u (sigma_fan x V E v u) /\ azim x v u (sigma_fan x V E v u) <pi)`;;
  40
  41
  42
  43
  44 let dartset_fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
  45 FAN(x,V,E)
  46 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
  47 ==> d_fan(x,V,E)=d1_fan(x,V,E)`,
  48 REPEAT STRIP_TAC
  49 THEN MRESA_TAC fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
  50 THEN ASM_REWRITE_TAC[d_fan;]
  51 THEN SET_TAC[]);;
  52
  53
  54 let properties_of_elements_in_face_fully_surroundedfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
  55 FAN(x,V,E)
  56 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
  57 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
  58 /\ y IN ds
  59 ==> {pr2 y, pr3 y} IN E`,
  60 REPEAT GEN_TAC THEN STRIP_TAC
  61 THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
  62 THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`)
  63 THEN RESA_TAC
  64 THEN POP_ASSUM MP_TAC
  65 THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
  66 THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
  67 THEN STRIP_TAC
  68 THEN ASM_REWRITE_TAC[pr2;pr3]);;
  69
  70
  71
  72
  73
  74 let properties_fully_surrounded=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
  75 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
  76 /\ (&0< azim x u w v ) /\ (azim x u w v <pi)
  77 ==> ~coplanar {x,v,u,w}`,
  78 REPEAT STRIP_TAC
  79 THEN POP_ASSUM MP_TAC
  80 THEN REWRITE_TAC[SET_RULE`{x,v,u,w}={x,u,w,v}`]
  81 THEN STRIP_TAC
  82 THEN FIND_ASSUM MP_TAC`{v,u} IN (E:(real^3->bool)->bool)`
  83 THEN REWRITE_TAC[SET_RULE`{v,u}={u,v}`]
  84 THEN STRIP_TAC
  85 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;
  86 ` (u:real^3)`]
  87 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
  88 ` (u:real^3)`]
  89 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
  90 THEN ASM_TAC
  91 THEN REAL_ARITH_TAC);;
  92
  93
  94
  95
  96
  97
  98 let exists_edge_fully_surround_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) w:real^3.
  99 FAN(x,V,E) /\ w IN V
 100 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 101 ==> ?v. {w,v} IN E /\ v IN V`,
 102 REPEAT STRIP_TAC
 103 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`)
 104 THEN SUBGOAL_THEN`~(set_of_edge (w:real^3) V E={})`ASSUME_TAC
 105 THENL[ POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "YEU") THEN STRIP_TAC THEN REMOVE_THEN "YEU" MP_TAC
 106 THEN ASM_REWRITE_TAC[CARD_CLAUSES] THEN ARITH_TAC;
 107 POP_ASSUM MP_TAC
 108 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`; set_of_edge;IN_ELIM_THM]]);;
 109
 110
 111
 112
 113 let nonsetedge_fully_surround_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 114 (!v. v IN V==>CARD (set_of_edge v V E) >1)/\ FAN(x,V,E)
 115 ==> ~(E={})`,
 116 REPEAT STRIP_TAC
 117 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
 118 THEN POP_ASSUM (fun th-> MP_TAC th THEN REWRITE_TAC[FAN;fan1]  THEN STRIP_TAC THEN ASSUME_TAC(th))
 119 THEN FIND_ASSUM MP_TAC(`~((V:real^3->bool) SUBSET {})`)
 120 THEN REWRITE_TAC[SET_RULE`~(V SUBSET {})<=> ?w. w IN V`]
 121 THEN STRIP_TAC
 122 THEN MRESA_TAC exists_edge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w:real^3`]
 123 THEN ASM_TAC THEN SET_TAC[]);;
 124
 125 let v_subset_xfan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool).
 126 FAN(x,V,E) /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 127 ==> V SUBSET xfan(x,V,E)`,
 128 REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
 129 THEN REPEAT STRIP_TAC
 130 THEN MRESA_TAC exists_edge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` x':real^3`]
 131 THEN EXISTS_TAC`{x',v:real^3}`
 132 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`x':real^3`]
 133 THEN MRESA_TAC point_in_aff_ge[`(x:real^3)`;`(x':real^3)`;`(v:real^3)`]
 134 THEN ASM_TAC THEN SET_TAC[IN]);;
 135
 136
 137
 138
 139 end;;