text_formalization/fan/GMLWKPK.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Tame Hypermap                                                     *)\r
   5 (* Author: Alexey Solovyev                                                    *)\r
   6 (* Date: 2010-07-07                                                           *)\r
   7 (* (V,ESTD V) is a fan (4-point case)                                         *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 module Gmlwkpk = struct\r
  11 \r
  12   open Fan;;\r
  13 \r
  14 let AFF_GE_1_2_0 = prove\r
  15  (`!v w.\r
  16         ~(v = vec 0) /\ ~(w = vec 0)\r
  17         ==> aff_ge {vec 0} {v,w} = {a % v + b % w | &0 <= a /\ &0 <= b}`,\r
  18   SIMP_TAC[Fan.AFF_GE_1_2;\r
  19            SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN\r
  20   REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN\r
  21   ONCE_REWRITE_TAC[MESON[]\r
  22    `(?a b c. P b c /\ Q b c /\ R a b c /\ S b c) <=>\r
  23     (?b c. P b c /\ Q b c /\ S b c /\ ?a. R a b c)`] THEN\r
  24   REWRITE_TAC[REAL_ARITH `t + s:real = &1 <=> t = &1 - s`; EXISTS_REFL] THEN\r
  25   SET_TAC[]);;\r
  26 \r
  27 let AFF_GE_1_1_0 = prove\r
  28  (`!v. ~(v = vec 0) ==> aff_ge {vec 0} {v} = {a % v | &0 <= a}`,\r
  29   REPEAT STRIP_TAC THEN\r
  30   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SET_RULE `{a} = {a,a}`] THEN\r
  31   ASM_SIMP_TAC[AFF_GE_1_2_0; GSYM VECTOR_ADD_RDISTRIB] THEN\r
  32   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN\r
  33   MESON_TAC[REAL_LE_ADD; REAL_ARITH\r
  34    `&0 <= a ==> &0 <= a / &2 /\ a / &2 + a / &2 = a`]);;\r
  35 \r
  36 let GMLWKPK = prove\r
  37  (`!x:real^N V E.\r
  38         graph E\r
  39         ==> (fan7(x,V,E) <=>\r
  40              !e1 e2. e1 IN E UNION {{v} | v IN V} /\\r
  41                      e2 IN E UNION {{v} | v IN V}\r
  42                      ==> (e1 INTER e2 = {}\r
  43                           ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\\r
  44                          (!v. e1 INTER e2 = {v}\r
  45                               ==> aff_ge {x} e1 INTER aff_ge {x} e2 =\r
  46                                   aff_ge {x} {v}))`,\r
  47   REPEAT STRIP_TAC THEN REWRITE_TAC[Fan.fan7] THEN EQ_TAC THENL\r
  48    [SIMP_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]; ALL_TAC] THEN\r
  49   MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e1:real^N->bool` THEN\r
  50   MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e2:real^N->bool` THEN\r
  51   MATCH_MP_TAC(TAUT `(p ==> q ==> r) ==> (q ==> p) ==> q ==> r`) THEN\r
  52   STRIP_TAC THEN DISCH_TAC THEN\r
  53   SUBGOAL_THEN `e1 = e2 \/ e1 INTER e2 = {} \/ (?v:real^N. e1 INTER e2 = {v})`\r
  54   MP_TAC THENL\r
  55    [ALL_TAC;\r
  56     STRIP_TAC THEN ASM_REWRITE_TAC[INTER_IDEMPOT] THEN\r
  57     ASM_MESON_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]] THEN\r
  58   SUBGOAL_THEN `?a b:real^N c d:real^N. e1 = {a,b} /\ e2 = {c,d}` MP_TAC THENL\r
  59    [ALL_TAC;\r
  60     DISCH_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN SUBST_ALL_TAC)) THEN\r
  61     SET_TAC[]] THEN\r
  62   FIRST_ASSUM(CONJUNCTS_THEN MP_TAC) THEN\r
  63   REWRITE_TAC[IN_UNION; IN_ELIM_THM] THEN\r
  64   SUBGOAL_THEN `!e:real^N->bool. e IN E ==> ?v w. ~(v = w) /\ e = {v,w}`\r
  65   (LABEL_TAC "*") THENL\r
  66    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [graph]) THEN\r
  67     MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN\r
  68     MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[IN] THEN\r
  69     CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[];\r
  70     ASM_MESON_TAC[SET_RULE `{v,v} = {v}`]]);;\r
  71 \r
  72 let GMLWKPK_ALT = prove\r
  73  (`!x:real^N V E.\r
  74         graph E /\ (!e. e IN E ==> ~(x IN e))\r
  75         ==> (fan7(x,V,E) <=>\r
  76              (!e1 e2. e1 IN E UNION {{v} | v IN V} /\\r
  77                       e2 IN E UNION {{v} | v IN V} /\\r
  78                       e1 INTER e2 = {}\r
  79                           ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\\r
  80              (!e1 e2 v. e1 IN E /\ e2 IN E /\ e1 INTER e2 = {v}\r
  81                         ==> aff_ge {x} e1 INTER aff_ge {x} e2 =\r
  82                             aff_ge {x} {v}))`,\r
  83   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN\r
  84   EQ_TAC THEN SIMP_TAC[IN_UNION] THEN STRIP_TAC THEN\r
  85   MATCH_MP_TAC(MESON[]\r
  86    `(!x y. R x y ==> R y x) /\\r
  87     (!x y. P x /\ P y ==> R x y) /\\r
  88     (!x y. Q x /\ Q y ==> R x y) /\\r
  89     (!x y. P x /\ Q y ==> R x y)\r
  90     ==> !x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y`) THEN\r
  91   CONJ_TAC THENL [REWRITE_TAC[INTER_ACI]; ASM_SIMP_TAC[]] THEN CONJ_TAC THEN\r
  92   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THENL\r
  93    [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> a = c /\ b = c`] THEN SET_TAC[];\r
  94     X_GEN_TAC `e1:real^N->bool` THEN DISCH_TAC THEN X_GEN_TAC `v:real^N`] THEN\r
  95   SUBGOAL_THEN `(e1:real^N->bool) HAS_SIZE 2` MP_TAC THENL\r
  96    [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN\r
  97   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN\r
  98   MAP_EVERY X_GEN_TAC [`u:real^N`; `w:real^N`] THEN\r
  99   STRIP_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN\r
 100   SIMP_TAC[SET_RULE `{a,b} INTER {c} = {d} <=> d = c /\ (a = c \/ b = c)`] THEN\r
 101   REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN\r
 102   GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN\r
 103   MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]);;\r
 104 \r
 105 let GMLWKPK_SIMPLE = prove\r
 106  (`!E V x:real^N.\r
 107         UNIONS E SUBSET V /\ graph E /\ fan6(x,V,E) /\\r
 108         (!e. e IN E ==> ~(x IN e))\r
 109         ==> (fan7 (x,V,E) <=>\r
 110              !e1 e2.\r
 111                 e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\\r
 112                 e1 INTER e2 = {}\r
 113                 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x})`,\r
 114   let lemma = prove\r
 115    (`!x u v w:real^N.\r
 116       ~collinear{x,u,v} /\ ~collinear{x,v,w}\r
 117       ==> (~(aff_ge {x} {u,v} INTER aff_ge {x} {v,w} =\r
 118              aff_ge {x} {v}) <=>\r
 119            u IN aff_ge {x} {v,w} \/ w IN aff_ge {x} {u,v})`,\r
 120     REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `x:real^N` THEN\r
 121     REPEAT GEN_TAC THEN\r
 122     MAP_EVERY (fun t ->\r
 123       ASM_CASES_TAC t THENL\r
 124        [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC])\r
 125      [`u:real^N = v`; `w:real^N = v`;\r
 126       `u:real^N = vec 0`; `v:real^N = vec 0`; `w:real^N = vec 0`] THEN\r
 127     STRIP_TAC THEN EQ_TAC THENL\r
 128      [DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE\r
 129        `~(s INTER s' = t)\r
 130         ==> t SUBSET s /\ t SUBSET s' ==> t PSUBSET s INTER s'`)) THEN\r
 131       ANTS_TAC THENL\r
 132        [CONJ_TAC THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];\r
 133         REWRITE_TAC[PSUBSET_ALT]] THEN\r
 134       DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
 135       ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; LEFT_IMP_EXISTS_THM] THEN\r
 136       REWRITE_TAC[IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN\r
 137       MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN\r
 138       DISCH_TAC THEN DISCH_TAC THEN\r
 139       REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN\r
 140       MAP_EVERY X_GEN_TAC [`c:real`; `d:real`] THEN STRIP_TAC THEN\r
 141       ASM_CASES_TAC `a = &0` THENL\r
 142        [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]; ALL_TAC] THEN\r
 143       ASM_CASES_TAC `d = &0` THENL\r
 144        [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID]; ALL_TAC] THEN\r
 145       DISCH_THEN(K ALL_TAC) THEN DISJ_CASES_TAC\r
 146        (REAL_ARITH `b <= c \/ c <= b`)\r
 147       THENL\r
 148        [FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH\r
 149          `a % u + b % v:real^N = c % v + d % w\r
 150           ==> a % u = (c - b) % v + d % w`)) THEN\r
 151         DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a):real^N->real^N`) THEN\r
 152         ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN\r
 153         DISCH_THEN(K ALL_TAC) THEN DISJ1_TAC THEN\r
 154         REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN\r
 155         MAP_EVERY EXISTS_TAC [`inv a * (c - b):real`; `inv a * d:real`] THEN\r
 156         ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE];\r
 157         FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH\r
 158          `a % u + b % v:real^N = c % v + d % w\r
 159           ==> d % w = (b - c) % v + a % u`)) THEN\r
 160         DISCH_THEN(MP_TAC o AP_TERM `(%) (inv d):real^N->real^N`) THEN\r
 161         ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN\r
 162         DISCH_THEN(K ALL_TAC) THEN DISJ2_TAC THEN\r
 163         REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN\r
 164         MAP_EVERY EXISTS_TAC [`inv d * a:real`; `inv d * (b - c):real`] THEN\r
 165         ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE] THEN\r
 166         REWRITE_TAC[VECTOR_ADD_SYM]];\r
 167       STRIP_TAC THEN MATCH_MP_TAC(SET_RULE\r
 168        `(?x. x IN s /\ x IN t /\ ~(x IN u)) ==> ~(s INTER t = u)`)\r
 169       THENL\r
 170        [EXISTS_TAC `u:real^N` THEN ASM_REWRITE_TAC[] THEN\r
 171         ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN\r
 172         CONJ_TAC THENL\r
 173          [MAP_EVERY EXISTS_TAC [`&1`; `&0`] THEN\r
 174           REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;\r
 175           DISCH_THEN(X_CHOOSE_THEN `a:real`\r
 176            (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN\r
 177           UNDISCH_TAC `~collinear{vec 0:real^N,a % v,v}` THEN\r
 178           REWRITE_TAC[] THEN\r
 179           ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN\r
 180           REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]];\r
 181         EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[] THEN\r
 182         ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN\r
 183         CONJ_TAC THENL\r
 184          [MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN\r
 185           REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;\r
 186           DISCH_THEN(X_CHOOSE_THEN `a:real`\r
 187            (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN\r
 188           UNDISCH_TAC `~collinear{vec 0:real^N,v,a % v}` THEN\r
 189           REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]]]]) in\r
 190   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN\r
 191   EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN\r
 192   REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(MESON[]\r
 193    `(!x y. R x y ==> R y x) /\\r
 194     (!x. Q x ==> !y. Q y ==> R x y) /\\r
 195     (!x. P x ==> (!y. Q y ==> R x y) /\ (!y. P y ==> R x y))\r
 196     ==> (!x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y)`) THEN\r
 197   CONJ_TAC THENL [SIMP_TAC[INTER_ACI]; ALL_TAC] THEN\r
 198   REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL\r
 199    [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> c = a /\ b = a`] THEN\r
 200     REWRITE_TAC[INTER_IDEMPOT];\r
 201     ALL_TAC] THEN\r
 202   X_GEN_TAC `ee1:real^N->bool` THEN DISCH_TAC THEN CONJ_TAC THENL\r
 203    [X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN\r
 204     REWRITE_TAC[SET_RULE `s INTER {a} = {b} <=> b = a /\ a IN s`] THEN\r
 205     SIMP_TAC[IMP_CONJ; FORALL_UNWIND_THM2] THEN DISCH_TAC THEN\r
 206     REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN\r
 207     MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];\r
 208     ALL_TAC] THEN\r
 209   X_GEN_TAC `ee2:real^N->bool` THEN DISCH_TAC THEN\r
 210   SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL\r
 211      [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN\r
 212   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN\r
 213   MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN\r
 214   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN\r
 215   SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL\r
 216    [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN\r
 217   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN\r
 218   MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN\r
 219   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN\r
 220   ONCE_REWRITE_TAC[SET_RULE\r
 221    `{a,b} INTER {c,d} = {v} <=>\r
 222     v = a /\ {a,b} INTER {c,d} = {v} \/\r
 223     v = b /\ {a,b} INTER {c,d} = {v}`] THEN\r
 224   REWRITE_TAC[TAUT\r
 225    `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN\r
 226   REWRITE_TAC[FORALL_AND_THM; FORALL_UNWIND_THM2] THEN\r
 227   MAP_EVERY UNDISCH_TAC [`{v1:real^N,w1} IN E`; `~(v1:real^N = w1)`] THEN\r
 228   MAP_EVERY (fun s -> SPEC_TAC(s,s))\r
 229    [`w1:real^N`; `v1:real^N`] THEN\r
 230   REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]\r
 231    `(!v w. P v w ==> P w v) /\\r
 232     (!v w. R v w ==> Q w v) /\\r
 233     (!v w. P v w ==> R v w)\r
 234     ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN\r
 235   REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN\r
 236   MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN\r
 237   ONCE_REWRITE_TAC[SET_RULE\r
 238    `{a,b} INTER {c,d} = {v} <=>\r
 239     v = c /\ {a,b} INTER {c,d} = {v} \/\r
 240     v = d /\ {a,b} INTER {c,d} = {v}`] THEN\r
 241   REWRITE_TAC[TAUT\r
 242    `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN\r
 243   MAP_EVERY UNDISCH_TAC [`{v2:real^N,w2} IN E`; `~(v2:real^N = w2)`] THEN\r
 244   MAP_EVERY (fun s -> SPEC_TAC(s,s)) [`w2:real^N`; `v2:real^N`] THEN\r
 245   REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]\r
 246    `(!v w. P v w ==> P w v) /\\r
 247     (!v w. Q v w ==> R w v) /\\r
 248     (!v w. P v w ==> Q v w)\r
 249     ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN\r
 250   REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN\r
 251   MAP_EVERY X_GEN_TAC [`v':real^N`; `w:real^N`] THEN STRIP_TAC THEN\r
 252   ONCE_REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN\r
 253   ASM_CASES_TAC `u:real^N = w` THENL [ASM SET_TAC[]; ALL_TAC] THEN\r
 254   DISCH_TAC THEN W(MP_TAC o PART_MATCH (rand o lhand o rand) lemma o goal_concl) THEN\r
 255   ANTS_TAC THENL\r
 256    [REWRITE_TAC[SET_RULE `{x,v,w} = {x} UNION {v,w}`] THEN\r
 257     ASM_MESON_TAC[fan6; INSERT_AC];\r
 258     ALL_TAC] THEN\r
 259   MATCH_MP_TAC(TAUT `~q ==> (~p <=> q) ==> p`) THEN\r
 260   REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THEN MATCH_MP_TAC(SET_RULE\r
 261    `aff_ge {x} {v} INTER aff_ge {x} s = {x} /\\r
 262     v IN aff_ge {x} {v} /\ ~(v = x)\r
 263     ==> ~(v IN aff_ge {x} s)`) THEN\r
 264   REPEAT CONJ_TAC THENL\r
 265    [FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 266     ASM_REWRITE_TAC[IN_UNION] THEN\r
 267     CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN\r
 268     REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `u:real^N` THEN\r
 269     REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN\r
 270     FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 271     REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{u:real^N,v}` THEN\r
 272     ASM SET_TAC[];\r
 273     SUBGOAL_THEN `DISJOINT {x:real^N} {u:real^N}` ASSUME_TAC THENL\r
 274      [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN\r
 275       ASM_MESON_TAC[IN_INSERT];\r
 276       ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN\r
 277       MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN\r
 278       REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];\r
 279     ASM_MESON_TAC[IN_INSERT];\r
 280     FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 281     ASM_REWRITE_TAC[IN_UNION] THEN\r
 282     CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN\r
 283     REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `w:real^N` THEN\r
 284     REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN\r
 285     FIRST_X_ASSUM MATCH_MP_TAC THEN\r
 286     REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{v:real^N,w}` THEN\r
 287     ASM SET_TAC[];\r
 288     SUBGOAL_THEN `DISJOINT {x:real^N} {w:real^N}` ASSUME_TAC THENL\r
 289      [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN\r
 290       ASM_MESON_TAC[IN_INSERT];\r
 291       ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN\r
 292       MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN\r
 293       REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];\r
 294     ASM_MESON_TAC[IN_INSERT]]);;\r
 295 \r
 296 \r
 297 end;;\r