legacy/oldfan/DWWUTKW.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2010-02-09                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 module  Dwwutkw = struct
  14
  15
  16
  17 open Sphere;;
  18 open Fan_defs;;
  19 open Hypermap_of_fan;;
  20 open Tactic_fan;;
  21 open Lemma_fan;;
  22 open Fan;;
  23 open Hypermap_of_fan;;
  24 open Node_fan;;
  25 open Azim_node;;
  26 open Sum_azim_node;;
  27 open Disjoint_fan;;
  28 open Lead_fan;;
  29 open Fan_misc;;
  30 open Leads_into_fan;;
  31 open Fully_surrounded;;
  32 open Sin_azim_cross_dot;;
  33 open Leads_intos;;
  34 open Hypermap;;
  35 open Dartset_leads_into;;
  36
  37
  38
  39
  40
  41
  42 let condition_not_edge_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds.
  43 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
  44 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
  45 /\ fan80(x,V,E)
  46 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
  47 /\ e1 IN E /\ e2 = {v, u}
  48 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
  49 ==> ~(e1=e2)`,
  50
  51
  52 REPEAT STRIP_TAC
  53 THEN POP_ASSUM MP_TAC
  54 THEN ASM_REWRITE_TAC[]
  55 THEN POP_ASSUM MP_TAC
  56 THEN DISCH_THEN(LABEL_TAC"YEU")
  57 THEN STRIP_TAC
  58 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
  59 THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
  60 THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
  61 THEN RESA_TAC
  62 THEN POP_ASSUM MP_TAC
  63 THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
  64 THEN DISCH_TAC
  65 THEN SUBGOAL_THEN`aff_ge {x} e1 SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
  66 THENL[REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
  67 THEN REPEAT STRIP_TAC
  68 THEN EXISTS_TAC `e1:real^3->bool`
  69 THEN ASM_REWRITE_TAC[]
  70 THEN FIND_ASSUM MP_TAC(`(e1:real^3->bool) IN E`)
  71 THEN REWRITE_TAC[IN]
  72 THEN ASM_REWRITE_TAC[];
  73 ASSUME_TAC(SET_RULE`aff_gt {x} {v, u} INTER
  74       (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u})
  75 =aff_gt {x} {v, u} `)
  76 THEN MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} e1 SUBSET xfan (x,V,E)
  77 ==> aff_gt {x} {v, u} INTER aff_ge {x} e1={}`)
  78 THEN RESA_TAC
  79 THEN POP_ASSUM MP_TAC
  80 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
  81 THEN MATCH_MP_TAC exists_in_aff_gt
  82 THEN ASM_REWRITE_TAC[]]);;
  83
  84
  85
  86 let condition_not_intersection_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds e1:real^3->bool e2:real^3->bool.
  87 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
  88 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
  89 /\ fan80(x,V,E)
  90 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
  91 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
  92 /\ e1 IN E /\ e2 = {v, u}
  93 ==>aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} (e1 INTER e2)`,
  94 REPEAT STRIP_TAC
  95 THEN ASM_REWRITE_TAC[]
  96 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
  97 THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
  98 THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
  99 THEN RESA_TAC
 100 THEN POP_ASSUM MP_TAC
 101 THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
 102 THEN DISCH_TAC
 103 THEN SUBGOAL_THEN`aff_ge {x} e1 SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
 104 THENL[
 105 REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
 106 THEN REPEAT STRIP_TAC
 107 THEN EXISTS_TAC `e1:real^3->bool`
 108 THEN ASM_REWRITE_TAC[]
 109 THEN ASM_TAC THEN SET_TAC[IN];
 110 MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} e1 SUBSET xfan (x,V,E)
 111 ==> aff_gt {x} {v, u} INTER aff_ge {x} e1={}`)
 112 THEN RESA_TAC
 113 THEN MP_TAC(SET_RULE`
 114 aff_gt {x:real^3} {v, u} INTER aff_ge {x} e1={}==>
 115 aff_ge {x} e1 INTER (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u})
 116 = (aff_ge {x} e1 INTER aff_ge {x} {v}) UNION (aff_ge {x} e1 INTER aff_ge {x} {u})`)
 117 THEN RESA_TAC
 118 THEN MP_TAC(SET_RULE`e1 IN E==> e1 IN E UNION {{v:real^3} | v IN V}`)
 119 THEN RESA_TAC
 120 THEN MP_TAC(SET_RULE`v:real^3 IN V==> {v} IN E UNION {{v} | v IN V}`)
 121 THEN RESA_TAC
 122 THEN MP_TAC(SET_RULE`u:real^3 IN V==> {u} IN E UNION {{v} | v IN V}`)
 123 THEN RESA_TAC
 124 THEN FIND_ASSUM MP_TAC(`FAN(x:real^3,V,E)`)
 125 THEN REWRITE_TAC[FAN;fan7]
 126 THEN STRIP_TAC
 127 THEN POP_ASSUM(fun th-> MRESA_TAC th [`e1:real^3->bool`;`{v:real^3}`]THEN ASSUME_TAC th)
 128 THEN POP_ASSUM(fun th-> MRESA_TAC th [`e1:real^3->bool`;`{u:real^3}`])
 129 THEN MRESA_TAC condition_not_edge_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`;`ds:real^3#real^3#real^3#real^3->bool`]
 130 THEN FIND_ASSUM MP_TAC (`graph (E:(real^3->bool)->bool)`)
 131 THEN REWRITE_TAC[GRAPH]
 132 THEN STRIP_TAC
 133 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `e1:real^3->bool`[HAS_SIZE])
 134 THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
 135 THEN POP_ASSUM MP_TAC
 136 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
 137 THEN RESA_TAC
 138 THEN MRESA_TAC properties_edges_eq_fan[`e1:real^3->bool`; `v:real^3`;`u:real^3`]
 139 THENL[MP_TAC(SET_RULE`~(v IN e1)==> e1 INTER {v:real^3}={} /\ e1 INTER {v, u}=e1 INTER {u}`)
 140 THEN RESA_TAC
 141 THEN ASSUME_TAC(SET_RULE`{} SUBSET e1 INTER {u}:real^3->bool`)
 142 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} (e1 INTER {u})`)
 143 THEN RESA_TAC
 144 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`e1 INTER {u}:real^3->bool`]
 145 THEN POP_ASSUM MP_TAC THEN SET_TAC[];
 146 MP_TAC(SET_RULE`~(u IN e1)==> e1 INTER {u:real^3}={} /\ e1 INTER {v, u}=e1 INTER {v}`)
 147 THEN RESA_TAC
 148 THEN ASSUME_TAC(SET_RULE`{} SUBSET e1 INTER {v}:real^3->bool`)
 149 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} (e1 INTER {v})`)
 150 THEN RESA_TAC
 151 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`e1 INTER {v}:real^3->bool`]
 152 THEN POP_ASSUM MP_TAC THEN SET_TAC[]]]);;
 153
 154
 155
 156
 157
 158 let condition_not_intersection_point_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds:real^3#real^3#real^3#real^3->bool e1:real^3->bool w:real^3.
 159 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
 160 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 161 /\ fan80(x,V,E)
 162 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
 163 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
 164 /\ w IN V /\ e1 = {v, u}
 165 ==>aff_ge {x} e1 INTER aff_ge {x} {w} = aff_ge {x} (e1 INTER {w})`,
 166 REPEAT STRIP_TAC
 167 THEN ASM_REWRITE_TAC[]
 168 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
 169 THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
 170 THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
 171 THEN RESA_TAC
 172 THEN POP_ASSUM MP_TAC
 173 THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
 174 THEN DISCH_TAC
 175 THEN SUBGOAL_THEN`aff_ge {x} {w} SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
 176 THENL[
 177 REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
 178 THEN REPEAT STRIP_TAC
 179 THEN MRESA_TAC exists_edge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` w:real^3`]
 180 THEN EXISTS_TAC `{w,v'}:real^3->bool`
 181 THEN ASM_REWRITE_TAC[]
 182 THEN REMOVE_ASSUM_TAC
 183 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v':real^3)`;
 184 ` (w:real^3)`]
 185 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(w:real^3)`;` (v':real^3)`]
 186 THEN ASM_TAC THEN SET_TAC[IN];
 187 MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} {w} SUBSET xfan (x,V,E)
 188 ==> aff_gt {x} {v, u} INTER aff_ge {x} {w}={}`)
 189 THEN RESA_TAC
 190 THEN MP_TAC(SET_RULE`
 191 aff_gt {x:real^3} {v, u} INTER aff_ge {x} {w}={}==>
 192 (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u}) INTER aff_ge {x} {w}
 193 = (aff_ge {x} {w} INTER aff_ge {x} {v}) UNION (aff_ge {x} {w} INTER aff_ge {x} {u})`)
 194 THEN RESA_TAC
 195 THEN MP_TAC(SET_RULE`w IN V==> {w} IN E UNION {{v:real^3} | v IN V}`)
 196 THEN RESA_TAC
 197 THEN MP_TAC(SET_RULE`v:real^3 IN V==> {v} IN E UNION {{v} | v IN V}`)
 198 THEN RESA_TAC
 199 THEN MP_TAC(SET_RULE`u:real^3 IN V==> {u} IN E UNION {{v} | v IN V}`)
 200 THEN RESA_TAC
 201 THEN FIND_ASSUM MP_TAC(`FAN(x:real^3,V,E)`)
 202 THEN REWRITE_TAC[FAN;fan7]
 203 THEN STRIP_TAC
 204 THEN POP_ASSUM(fun th-> MRESA_TAC th [`{w}:real^3->bool`;`{v:real^3}`]THEN ASSUME_TAC th)
 205 THEN POP_ASSUM(fun th-> MRESA_TAC th [`{w}:real^3->bool`;`{u:real^3}`])
 206 THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
 207 THEN POP_ASSUM MP_TAC
 208 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
 209 THEN RESA_TAC
 210 THEN MP_TAC(SET_RULE`~(v=u:real^3)==> ({v, u} INTER {w}= {w} INTER {v} /\ {w} INTER {u}={}) \/ ({v, u} INTER {w}= {w} INTER {u} /\ {w} INTER {v}={})`)
 211 THEN RESA_TAC
 212 THENL[ ASSUME_TAC(SET_RULE`{} SUBSET {w} INTER {v}:real^3->bool`)
 213 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} ({w} INTER {v})`)
 214 THEN RESA_TAC
 215 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`{w} INTER {v}:real^3->bool`]
 216 THEN POP_ASSUM MP_TAC THEN SET_TAC[];
 217 ASSUME_TAC(SET_RULE`{} SUBSET {w} INTER {u}:real^3->bool`)
 218 THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} ({w} INTER {u})`)
 219 THEN RESA_TAC
 220 THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`{w} INTER {u}:real^3->bool`]
 221 THEN POP_ASSUM MP_TAC THEN SET_TAC[]]]);;
 222
 223
 224
 225 let DWWUTKW=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds.
 226 FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
 227 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 228 /\ fan80(x,V,E)
 229 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
 230 /\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
 231 /\ E1=E UNION {{v,u}}
 232 ==> FAN (x,V,E1)`,
 233 REPEAT STRIP_TAC
 234 THEN FIND_ASSUM MP_TAC`FAN(x:real^3,V,E)`
 235 THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7]
 236 THEN STRIP_TAC
 237 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
 238 THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
 239 THEN POP_ASSUM MP_TAC
 240 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
 241 THEN RESA_TAC
 242 THEN MRESA_TAC add_edge_graph_fan[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 243 THEN MRESA_TAC garph_add_edge_is_garph[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 244 THEN MRESA_TAC add_edge_into_collinear_fan[`x:real^3`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
 245 THEN REWRITE_TAC[UNION;IN_ELIM_THM;IN_SING]
 246 THEN REPEAT GEN_TAC
 247 THEN STRIP_TAC
 248 THENL[ REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
 249 THEN POP_ASSUM MATCH_MP_TAC
 250 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];
 251
 252 MRESA_TAC condition_not_intersection_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e1:real^3->bool`;`e2:real^3->bool`];
 253
 254 REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
 255 THEN POP_ASSUM MATCH_MP_TAC
 256 THEN POP_ASSUM MP_TAC
 257 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];
 258
 259 MRESA_TAC condition_not_intersection_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e2:real^3->bool`;`e1:real^3->bool`]
 260 THEN ASM_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`];
 261
 262 ASM_REWRITE_TAC[SET_RULE`A INTER A=A`];
 263
 264 MRESA_TAC condition_not_intersection_point_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e1:real^3->bool`;`v':real^3`];
 265
 266 REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e2:real^3->bool`;`e1:real^3->bool`])
 267 THEN ASM_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`]
 268 THEN POP_ASSUM MATCH_MP_TAC
 269 THEN POP_ASSUM MP_TAC
 270 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];
 271
 272 MRESA_TAC condition_not_intersection_point_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e2:real^3->bool`;`v':real^3`]
 273 THEN ASM_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`];
 274
 275 REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
 276 THEN POP_ASSUM MATCH_MP_TAC
 277 THEN POP_ASSUM MP_TAC
 278 THEN POP_ASSUM MP_TAC
 279 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);;
 280
 281
 282
 283
 284 end;;
 285
 286