legacy/oldfan/leads_into.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  Leads_into_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 open Disjoint_fan;;
  27 open Lead_fan;;
  28
  29
  30 (****************************************************************************)
  31 (****************************LEADS INTO**************************************)
  32 (****************************************************************************)
  33
  34 let dart_leads_into=new_definition`dart_leads_into (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=
  35 @(U:real^3->bool). ?h:real. &0<h /\
  36 (!(s:real) (y:real^3). &0 <s /\ s<h
  37 /\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s))
  38 ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET U /\  connected_component (yfan(x,V,E)) y=U))`;;
  39
  40
  41
  42
  43
  44
  45 let exists_leads_into_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
  46 FAN(x,V,E)/\ {v,u} IN E
  47 ==>
  48 ?(U:real^3->bool). ?h:real. &0<h /\
  49 (!(s:real) (y:real^3). &0 <s /\ s<h
  50 /\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s))
  51 ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET U /\  connected_component (yfan(x,V,E)) y=U))`,
  52 REPEAT STRIP_TAC
  53 THEN MRESA_TAC JGIYDLE[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
  54 THEN ASM_TAC
  55 THEN DISCH_TAC
  56 THEN DISCH_TAC
  57 THEN DISCH_THEN (LABEL_TAC "BE")
  58 THEN DISCH_THEN (LABEL_TAC "YEU")
  59 THEN DISCH_TAC
  60 THEN DISCH_TAC
  61 THEN DISCH_THEN (LABEL_TAC "EM")
  62 THEN DISCH_THEN (LABEL_TAC "NHIEU")
  63 THEN MP_TAC(REAL_ARITH`h> &0/\ &1>h ==> -- &1< (h:real)/\ -- &1<= (h:real) /\ h< &1 /\ &0 <h /\ h<= &1`)
  64 THEN RESA_TAC
  65 THEN MRESA1_TAC ACS_BOUNDS_LT`h:real`
  66 THEN REMOVE_ASSUM_TAC
  67 THEN MRESAL_TAC ACS_MONO_LT[`&0`;`h:real`][ACS_0;REAL_ARITH`-- &1 <= &0`]
  68 THEN MRESA1_TAC COS_ACS `h:real`
  69 THEN REMOVE_THEN "BE" (fun th-> MRESA1_TAC th `acs(h:real)`)
  70 THEN POP_ASSUM MP_TAC
  71 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[EXTENSION]
  72 THEN REWRITE_TAC[EMPTY;IN;NOT_FORALL_THM]
  73 THEN STRIP_TAC
  74 THEN POP_ASSUM MP_TAC
  75 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
  76 THEN STRIP_TAC
  77 THEN ONCE_REWRITE_TAC[GSYM FUN_EQ_THM]
  78 THEN EXISTS_TAC`(connected_component (yfan((x:real^3),(V:real^3->bool) ,(E:(real^3->bool)->bool))) (x':real^3)):real^3->bool`
  79 THEN EXISTS_TAC`acs(h:real)`
  80 THEN ASM_REWRITE_TAC[]
  81 THEN REPEAT GEN_TAC
  82 THEN STRIP_TAC
  83 THEN POP_ASSUM MP_TAC
  84 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
  85 THEN DISCH_TAC
  86 THEN ASSUME_TAC(PI_WORKS)
  87 THEN MP_TAC(REAL_ARITH` &0< s /\ acs (h:real)< pi/ &2 /\ &0< pi ==>  &0<= (s:real)/\ acs h<= pi`)
  88 THEN RESA_TAC
  89 THEN MRESAL_TAC COS_MONO_LT[`s:real`;`acs(h:real)`][]
  90 THEN MP_TAC(REAL_ARITH` h< cos(s:real)==>h<= cos(s:real)`)
  91 THEN RESA_TAC
  92 THEN REMOVE_THEN "NHIEU"(fun th-> MRESA1_TAC th `acs(h:real)`)
  93 THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`cos(s:real)`;`h:real`])
  94 THEN MRESA_TAC CONNECTED_COMPONENT_MAXIMAL [`yfan(x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool))`;`rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (h:real)`;`x':real^3`]
  95 THEN STRIP_TAC
  96 THENL[
  97 POP_ASSUM MP_TAC
  98 THEN POP_ASSUM MP_TAC
  99 THEN SET_TAC[];
 100 MATCH_MP_TAC CONNECTED_COMPONENT_EQ
 101 THEN ASM_TAC
 102 THEN SET_TAC[]]);;
 103
 104
 105
 106
 107 let DART_LEADS_INTO=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
 108 FAN(x,V,E)/\ {v,u} IN E
 109 ==>
 110 ?h:real. &0<h /\
 111 (!(s:real) (y:real^3). &0 <s /\ s<h
 112 /\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s))
 113 ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET dart_leads_into x V E v u /\  connected_component (yfan(x,V,E)) y=dart_leads_into x V E v u))`,
 114
 115 REPEAT STRIP_TAC
 116 THEN ONCE_REWRITE_TAC[dart_leads_into]
 117 THEN MRESA_TAC exists_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]
 118  THEN SELECT_ELIM_TAC
 119 THEN EXISTS_TAC`U:real^3->bool`
 120 THEN EXISTS_TAC`h:real`
 121  THEN ASM_REWRITE_TAC[]);;
 122
 123
 124 let unique_dart_leads_into=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 (U:real^3->bool).
 125 FAN(x,V,E)/\ {v,u} IN E
 126 /\(?h:real. &0<h /\
 127 (!(s:real) (y:real^3). &0 <s /\ s<h
 128 /\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s))
 129 ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET U /\  connected_component (yfan(x,V,E)) y=U)))
 130 ==> dart_leads_into x V E v u =U`,
 131 REPEAT STRIP_TAC
 132 THEN POP_ASSUM MP_TAC
 133 THEN DISCH_THEN (LABEL_TAC"A")
 134 THEN MRESA_TAC DART_LEADS_INTO [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 135 THEN POP_ASSUM MP_TAC
 136 THEN DISCH_THEN (LABEL_TAC "BE")
 137 THEN MRESA_TAC JGIYDLE[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 138 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 139 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 140 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 141 THEN DISCH_THEN (LABEL_TAC "YEU")
 142 THEN DISCH_THEN (LABEL_TAC "EM")
 143 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
 144 THEN DISCH_THEN (LABEL_TAC "MAI")
 145 THEN ASSUME_TAC(PI_WORKS)
 146 THEN MP_TAC(REAL_ARITH`&0<h /\ &0<h' /\ &0 <pi==>
 147 -- &1< (min (min (h:real) (h':real)/ &2) (pi/ &3))  /\
 148 -- &1<= (min (min (h:real) (h':real)/ &2) (pi/ &3))  /\
 149  (min (min (h:real) (h':real)/ &2) (pi/ &3))< pi/ &2  /\
 150  &0 <(min (min (h:real) (h':real)/ &2) (pi/ &3)) /\
 151  (min (min (h:real) (h':real)/ &2) (pi/ &3))<= pi/ &2 /\
 152  (min (min (h:real) (h':real)/ &2) (pi/ &3))< h /\
 153  (min (min (h:real) (h':real)/ &2) (pi/ &3))< h'
 154 `)
 155 THEN RESA_TAC
 156 THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th ` (min (min (h:real) (h':real)/ &2) (pi/ &3))`)
 157 THEN POP_ASSUM MP_TAC
 158 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[EXTENSION]
 159 THEN REWRITE_TAC[EMPTY;IN;NOT_FORALL_THM]
 160 THEN STRIP_TAC
 161 THEN POP_ASSUM MP_TAC
 162 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
 163 THEN STRIP_TAC
 164 THEN ONCE_REWRITE_TAC[GSYM FUN_EQ_THM]
 165 THEN REMOVE_THEN "BE" (fun th-> MRESA_TAC th[`(min ((min (h:real) (h':real))/ &2) (pi/ &3))`;`x':real^3`])
 166 THEN POP_ASSUM MP_TAC
 167 THEN REMOVE_THEN "A" (fun th-> MRESA_TAC th[`(min ((min (h:real) (h':real))/ &2) (pi/ &3))`;`x':real^3`])
 168 THEN POP_ASSUM MP_TAC
 169 THEN SET_TAC[]);;
 170
 171
 172 let dart_leads_into_fan_in_topological_component_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
 173 FAN(x,V,E)/\ {v,u} IN E
 174 ==> dart_leads_into x V E v u IN topological_component_yfan (x,V,E)`,
 175 REPEAT STRIP_TAC
 176 THEN MRESA_TAC not_empty_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 177 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM")
 178 THEN MRESA_TAC DART_LEADS_INTO[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
 179 `v:real^3`;`u:real^3`;]
 180 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
 181 THEN MRESA_TAC rw_dart_avoids_fan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 182 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"OI")
 183 THEN MP_TAC(REAL_ARITH`&1> h' /\ h' > &0==> -- &1 < h' /\ h'< &1 /\ -- &1 <= h' /\ h'<= &1/\ &0 < h' /\ h' <= &1`) THEN RESA_TAC
 184 THEN MRESA1_TAC ACS_BOUNDS_LT`h':real`
 185 THEN MRESAL_TAC ACS_MONO_LT[`&0`;`h':real`][ACS_0;REAL_ARITH`-- &1 <= &0`]
 186 THEN MRESA1_TAC COS_ACS `h':real`
 187 THEN ABBREV_TAC`h1= min (h:real) (acs h')/ &2`
 188 THEN MP_TAC(REAL_ARITH`h1= min (h:real) (acs h')/ &2 /\ &0<h /\ &0< acs h' /\ acs h'< pi/ &2==> &0< h1 /\ h1< h /\ h1<pi/ &2/\ h1< acs h' /\ acs h' <= pi /\ &0<= h1`)
 189 THEN ASM_REWRITE_TAC[PI_WORKS] THEN STRIP_TAC
 190 THEN MRESAL_TAC COS_MONO_LT[`h1:real`;`acs h':real`][ACS_0;REAL_ARITH`-- &1 <= &0`]
 191 THEN MP_TAC(REAL_ARITH`h'< cos h1==> h'<= cos h1`) THEN RESA_TAC
 192 THEN REMOVE_THEN "EM"(fun th-> MRESAL1_TAC th `h1:real`[SET_RULE`~(A={})<=> ?y. y IN A`])
 193 THEN REMOVE_THEN "YEU"(fun th-> MRESA_TAC th [`h1:real`;`y:real^3`])
 194 THEN POP_ASSUM(fun th -> REWRITE_TAC[SYM(th);IN_ELIM_THM;topological_component_yfan;])
 195 THEN EXISTS_TAC`y:real^3`
 196 THEN ASM_REWRITE_TAC[]
 197 THEN MRESA_TAC continuous_set_fan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`(cos h1:real)`;`(h':real)`]
 198 THEN ASM_TAC THEN SET_TAC[]);;
 199
 200
 201 let connected_dart_leads_into_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
 202 FAN(x,V,E)/\ {v,u} IN E
 203 ==> connected(dart_leads_into x V E v u )`,
 204 REPEAT STRIP_TAC
 205 THEN MRESA_TAC dart_leads_into_fan_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 206 THEN MATCH_MP_TAC in_topological_component_yfan_is_connected
 207 THEN EXISTS_TAC`x:real^3`
 208 THEN EXISTS_TAC`V:real^3->bool`
 209 THEN EXISTS_TAC`E:(real^3->bool)->bool`
 210 THEN ASM_REWRITE_TAC[]);;
 211
 212
 213
 214
 215 end;;