text_formalization/fan/polyhedron.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: AJXXAWK, EDANAOL,   QLITJET MUGGQUF QSRHLXB LTHQIAA                 *)
   5 (*   CZZHBLI QOEPBJD NEHRQPR ZMQQFUP JLIGZGS                                  *)
   6 (* Section: Polyhedron                                                        *)
   7 (* Chapter: Packing                                                           *)
   8 (* Author: John Harrison, Hoang Le Truong                                     *)
   9 (* Date: 2010-07-15                                                           *)
  10 (* ========================================================================== *)
  11
  12
  13 (*
  14
  15 John Harrison's material on polyhedra in mostly in Multivariate/flyspeck.ml
  16
  17 AJXXAWK
  18 Definition 4.5:   IS_AFFINE_HULL
  19                    affine / hull
  20                    aff_dim
  21                    AFF_DIM_EMPTY
  22
  23 EDANAOL
  24  Definition 4.6 :  IN_INTERIOR
  25                    IN_RELATIVE_INTERIOR
  26                    CLOSURE_APPROACHABLE
  27                    (Don't have definition of relative boundary, but
  28                     several theorems use closure s DIFF relative_interior s.)
  29
  30 QLITJET
  31  Definition 4.7:   face_of
  32                    extreme_point_of (presumably it's meant to be the point not
  33                    the singleton set, which the definition literally gives)
  34                    facet_of
  35                    edge_of
  36                    (Don't have a definition of "proper"; I just use
  37                     ~(f = {}) and/or ~(f = P) as needed.)
  38
  39 MUGGQUF
  40  Lemma 4.18:       KREIN_MILMAN_MINKOWSKI
  41
  42 QSRHLXB
  43  Definition 4.8:   polyhedron
  44                    vertices
  45
  46 LTHQIAA
  47  Lemma 4.19:       AFFINE_IMP_POLYHEDRON
  48
  49 CZZHBLI
  50  Lemma 4.20 (i):   FACET_OF_POLYHEDRON_EXPLICIT
  51
  52  Lemma 4.20 (ii):  Direct consequence of RELATIVE_INTERIOR_POLYHEDRON
  53
  54  Lemma 4.20 (iii): FACE_OF_POLYHEDRON_EXPLICIT / FACE_OF_POLYHEDRON
  55
  56  Lemma 4.20 (iv):  FACE_OF_TRANS
  57
  58  Lemma 4.20 (v):   EXTREME_POINT_OF_FACE
  59
  60  Lemma 4.20 (vi):  FACE_OF_EQ
  61
  62 QOEPBJD
  63  Corr. 4.7:        FACE_OF_POLYHEDRON_POLYHEDRON
  64
  65 NEHRQPR:
  66  Lemma 4.21:       POLYHEDRON_COLLINEAR_FACES
  67
  68 ZMQQFUP:
  69  Def 4.9:          vertices
  70                    edges
  71
  72 JLIGZGS:
  73                    POLYHEDRON_FAN
  74
  75 [Library completed by HLT, July 2011].
  76
  77 AMHFNXP:
  78                    AMHFNXP_BIJ
  79
  80 WBLARHH:
  81                    WBLARHH_BIJ
  82
  83 BSXAQBQ:
  84                    BSXAQBQ
  85
  86
  87
  88
  89 Email tchales<->John Harrison: July 15, 2010:
  90
  91 |I'm not sure whether your work covers the results
  92 | relating polyhedra to fans.  I wasn't able to find any theorems on that
  93 | topic, but I recall that you had mentioned it in an earlier email.  I want
  94 | to confirm with you that this still needs to be formalized.
  95
  96 I believe that I just did the most basic of these theorems, that a
  97 polyhedron gives rise to a fan, together with a bunch of invariance
  98 emmas for some relevant concepts.
  99
 100 *)
 101
 102
 103 (* ************************************************* *)
 104 (* Invariance theorems *)
 105
 106 module Polyhedron = struct
 107
 108   open Sphere;;
 109   open Fan;;
 110
 111   open Topology;;
 112   open Sphere;;
 113   open Hypermap;;
 114   open Fan;;
 115   open Planarity;;
 116   open Topology;;
 117   open Fan_defs;;
 118   open Conforming;;
 119
 120
 121
 122 let GRAPH = prove
 123  (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
 124   REWRITE_TAC[graph; IN]);;
 125
 126 let CYCLIC_SET = prove
 127  (`cyclic_set W v w <=>
 128          ~(v = w) /\
 129          FINITE W /\
 130          (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\
 131          W INTER affine hull {v, w} = {}`,
 132   REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
 133
 134 let CYCLIC_SET_TRANSLATION_EQ = prove
 135  (`!a:real^N s x y.
 136     cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
 137   REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
 138
 139 let CYCLIC_SET_LINEAR_IMAGE = prove
 140  (`!f:real^M->real^N s x y.
 141         linear f /\ (!x y. f x = f y ==> x = y)
 142         ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
 143   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 144    [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN
 145   GEOM_TRANSFORM_TAC[]);;
 146
 147 add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];;
 148
 149 add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
 150
 151 let GRAPH_TRANSLATION_EQ = prove
 152  (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
 153   REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
 154
 155 let GRAPH_LINEAR_IMAGE_EQ = prove
 156  (`!f:real^M->real^N E.
 157     linear f /\ (!x y. f x = f y ==> x = y)
 158     ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
 159   REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
 160
 161 let FAN1_TRANSLATION_EQ = prove
 162  (`!a:real^N x V E.
 163         fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 164         fan1(x,V,E)`,
 165   REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
 166
 167 let FAN1_LINEAR_IMAGE_EQ = prove
 168  (`!f:real^M->real^N x V E.
 169     linear f /\ (!x y. f x = f y ==> x = y)
 170     ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
 171   REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
 172
 173 let FAN2_TRANSLATION_EQ = prove
 174  (`!a:real^N x V E.
 175         fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 176         fan2(x,V,E)`,
 177   REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
 178
 179 let FAN2_LINEAR_IMAGE_EQ = prove
 180  (`!f:real^M->real^N x V E.
 181     linear f /\ (!x y. f x = f y ==> x = y)
 182     ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
 183   REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
 184
 185 let FAN3_TRANSLATION_EQ = prove
 186  (`!a:real^N x V E.
 187         fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 188         fan3(x,V,E)`,
 189   REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
 190
 191 let FAN3_LINEAR_IMAGE_EQ = prove
 192  (`!f:real^M->real^N x V E.
 193     linear f /\ (!x y. f x = f y ==> x = y)
 194     ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
 195   let lemma = prove
 196    (`{w | {a,w} IN IMAGE (IMAGE f) s} =
 197      IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
 198     MATCH_MP_TAC(SET_RULE
 199      `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
 200     REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
 201     MESON_TAC[]) in
 202   REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
 203
 204 let FAN4_TRANSLATION_EQ = prove
 205  (`!a:real^N x V E.
 206         fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 207         fan4(x,V,E)`,
 208   REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
 209
 210 let FAN4_LINEAR_IMAGE_EQ = prove
 211  (`!f:real^M->real^N x V E.
 212     linear f /\ (!x y. f x = f y ==> x = y)
 213     ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
 214   REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
 215
 216 let FAN5_TRANSLATION_EQ = prove
 217  (`!a:real^N x V E.
 218         fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 219         fan5(x,V,E)`,
 220   REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
 221
 222 let FAN5_LINEAR_IMAGE_EQ = prove
 223  (`!f:real^M->real^N x V E.
 224     linear f /\ (!x y. f x = f y ==> x = y)
 225     ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
 226   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 227    [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
 228   GEOM_TRANSFORM_TAC[]);;
 229
 230 let FAN6_TRANSLATION_EQ = prove
 231  (`!a:real^N x V E.
 232         fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 233         fan6(x,V,E)`,
 234   REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
 235
 236 let FAN6_LINEAR_IMAGE_EQ = prove
 237  (`!f:real^M->real^N x V E.
 238     linear f /\ (!x y. f x = f y ==> x = y)
 239     ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
 240   REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
 241
 242 let FAN7_TRANSLATION_EQ = prove
 243  (`!a:real^N x V E.
 244         fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 245         fan7(x,V,E)`,
 246   REWRITE_TAC[fan7] THEN
 247   REWRITE_TAC[SET_RULE
 248    `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN
 249   GEOM_TRANSLATE_TAC[]);;
 250
 251 let FAN7_LINEAR_IMAGE_EQ = prove
 252  (`!f:real^M->real^N x V E.
 253     linear f /\ (!x y. f x = f y ==> x = y)
 254     ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
 255   REWRITE_TAC[fan7; IN_UNION] THEN
 256   REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB;
 257               TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 258   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 259    [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 260   REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN
 261   GEOM_TRANSFORM_TAC[]);;
 262
 263 add_translation_invariants
 264  [GRAPH_TRANSLATION_EQ;
 265   FAN1_TRANSLATION_EQ;
 266   FAN2_TRANSLATION_EQ;
 267   FAN3_TRANSLATION_EQ;
 268   FAN4_TRANSLATION_EQ;
 269   FAN5_TRANSLATION_EQ;
 270   FAN6_TRANSLATION_EQ;
 271   FAN7_TRANSLATION_EQ];;
 272
 273 add_linear_invariants
 274  [GRAPH_LINEAR_IMAGE_EQ;
 275   FAN1_LINEAR_IMAGE_EQ;
 276   FAN2_LINEAR_IMAGE_EQ;
 277   FAN3_LINEAR_IMAGE_EQ;
 278   FAN4_LINEAR_IMAGE_EQ;
 279   FAN5_LINEAR_IMAGE_EQ;
 280   FAN6_LINEAR_IMAGE_EQ;
 281   FAN7_LINEAR_IMAGE_EQ];;
 282
 283 let FAN_TRANSLATION_EQ = prove
 284  (`!a:real^N x V E.
 285         FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 286         FAN(x,V,E)`,
 287   REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
 288
 289 let FAN_LINEAR_IMAGE_EQ = prove
 290  (`!f:real^M->real^N x V E.
 291     linear f /\ (!x y. f x = f y ==> x = y)
 292     ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
 293   REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
 294
 295 add_translation_invariants [FAN_TRANSLATION_EQ];;
 296 add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
 297
 298 let BASE_POINT_FAN_TRANSLATION_EQ = prove
 299  (`!a x V E.
 300     base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) =
 301     a + base_point_fan(x,V,E)`,
 302   REWRITE_TAC[base_point_fan]);;
 303
 304 let BASE_POINT_FAN_LINEAR_IMAGE_EQ = prove
 305  (`!f:real^M->real^N x V E.
 306         linear f
 307         ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) =
 308             f(base_point_fan(x,V,E))`,
 309   REWRITE_TAC[base_point_fan]);;
 310
 311 let SET_OF_EDGE_TRANSLATION_EQ = prove
 312  (`!a:real^N x V E.
 313         set_of_edge (a + x) (IMAGE (\x. a + x) V)
 314                     (IMAGE (IMAGE (\x. a + x)) E) =
 315         IMAGE (\x. a + x) (set_of_edge x V E)`,
 316   REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
 317
 318 let SET_OF_EDGE_LINEAR_IMAGE_EQ = prove
 319  (`!f:real^M->real^N x V E.
 320         linear f /\ (!x y. f x = f y ==> x = y)
 321         ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) =
 322             IMAGE f (set_of_edge x V E)`,
 323   let lemma = prove
 324    (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
 325      {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
 326     MATCH_MP_TAC(SET_RULE
 327      `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
 328     REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
 329     MESON_TAC[]) in
 330   REWRITE_TAC[set_of_edge; lemma] THEN
 331   GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
 332
 333 add_translation_invariants
 334  [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];;
 335
 336 add_linear_invariants
 337  [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];;
 338
 339 (* ************************************************* *)
 340 (* Polyhedron gives rise to a fan *)
 341
 342 let POLYHEDRON_FAN = prove
 343  (`!p z:real^3.
 344        bounded p /\ polyhedron p /\ z IN interior p
 345        ==> FAN(z,vertices p,edges p)`,
 346   let lemma = prove
 347    (`!s a b c d:real^N.
 348           segment[a,b] face_of s /\ segment[c,d] face_of s
 349           ==> {a,b} = {c,d} \/
 350               segment[a,b] INTER segment[c,d] = {a,b} INTER {c,d}`,
 351     REPEAT STRIP_TAC THEN
 352     MP_TAC(ISPECL [`s:real^N->bool`; `segment[a:real^N,b]`;
 353                   `segment[c:real^N,d]`] SUBSET_OF_FACE_OF) THEN
 354     MP_TAC(ISPECL [`s:real^N->bool`; `segment[c:real^N,d]`;
 355                   `segment[a:real^N,b]`] SUBSET_OF_FACE_OF) THEN
 356     ASM_SIMP_TAC[FACE_OF_IMP_SUBSET; RELATIVE_INTERIOR_SEGMENT] THEN
 357     REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[SEGMENT_REFL; INSERT_AC]) THEN
 358     MP_TAC(ISPECL [`a:real^N`; `b:real^N`; `c:real^N`; `d:real^N`]
 359         SUBSET_SEGMENT_OPEN_CLOSED) THEN
 360     MP_TAC(ISPECL [`c:real^N`; `d:real^N`; `a:real^N`; `b:real^N`]
 361         SUBSET_SEGMENT_OPEN_CLOSED) THEN
 362     ASM_REWRITE_TAC[open_segment] THEN
 363     MP_TAC(ISPECL [`a:real^N`; `b:real^N`] ENDS_IN_SEGMENT) THEN
 364     MP_TAC(ISPECL [`c:real^N`; `d:real^N`] ENDS_IN_SEGMENT) THEN
 365     ASM SET_TAC[]) in
 366   REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `z:real^3` THEN
 367   REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 368   SUBGOAL_THEN `polytope(p:real^3->bool)` ASSUME_TAC THENL
 369    [ASM_REWRITE_TAC[POLYTOPE_EQ_BOUNDED_POLYHEDRON]; ALL_TAC] THEN
 370   FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLYTOPE_IMP_COMPACT) THEN
 371   FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLYTOPE_IMP_CONVEX) THEN
 372   SUBGOAL_THEN `(vec 0:real^3) IN p` ASSUME_TAC THENL
 373    [ASM_MESON_TAC[INTERIOR_SUBSET; SUBSET]; ALL_TAC] THEN
 374   SUBGOAL_THEN `!a b:real^3. ~(p = segment[a,b])` ASSUME_TAC THENL
 375    [REPEAT GEN_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
 376     RULE_ASSUM_TAC(REWRITE_RULE[INTERIOR_SEGMENT; DIMINDEX_3; ARITH]) THEN
 377     ASM SET_TAC[];
 378     ALL_TAC] THEN
 379   REPEAT STRIP_TAC THENL
 380    [REWRITE_TAC[SUBSET; FORALL_IN_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 381     REWRITE_TAC[edges; FORALL_IN_GSPEC; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
 382     REWRITE_TAC[vertices; edge_of; IN_ELIM_THM; GSYM FACE_OF_SING] THEN
 383     MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN REPEAT STRIP_TAC THEN
 384     MATCH_MP_TAC FACE_OF_TRANS THEN EXISTS_TAC `segment[v:real^3,w]` THEN
 385     ASM_REWRITE_TAC[FACE_OF_SING; EXTREME_POINT_OF_SEGMENT];
 386     REWRITE_TAC[GRAPH; edges; edge_of; FORALL_IN_GSPEC] THEN
 387     MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN
 388     ASM_CASES_TAC `w:real^3 = v` THEN
 389     ASM_REWRITE_TAC[SEGMENT_REFL; AFF_DIM_SING] THEN
 390     CONV_TAC INT_REDUCE_CONV THEN STRIP_TAC THEN
 391     ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 392                  IN_INSERT; NOT_IN_EMPTY] THEN
 393     CONV_TAC NUM_REDUCE_CONV;
 394     REWRITE_TAC[fan1; SUBSET_EMPTY; vertices] THEN
 395     ASM_SIMP_TAC[FINITE_POLYHEDRON_EXTREME_POINTS] THEN
 396     REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_ELIM_THM] THEN
 397     MATCH_MP_TAC EXTREME_POINT_EXISTS_CONVEX THEN
 398     ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
 399     REWRITE_TAC[fan2; vertices; IN_ELIM_THM] THEN
 400     ASM_MESON_TAC[EXTREME_POINT_NOT_IN_INTERIOR];
 401     REWRITE_TAC[fan6; edges; FORALL_IN_GSPEC; edge_of] THEN
 402     MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN
 403     ASM_CASES_TAC `w:real^3 = v` THEN
 404     ASM_REWRITE_TAC[SEGMENT_REFL; AFF_DIM_SING] THEN
 405     CONV_TAC INT_REDUCE_CONV THEN STRIP_TAC THEN
 406     SUBGOAL_THEN `(v:real^3) extreme_point_of p /\ w extreme_point_of p`
 407     STRIP_ASSUME_TAC THENL
 408      [REWRITE_TAC[GSYM FACE_OF_SING] THEN CONJ_TAC THEN
 409       MATCH_MP_TAC FACE_OF_TRANS THEN EXISTS_TAC `segment[v:real^3,w]` THEN
 410       ASM_REWRITE_TAC[FACE_OF_SING; EXTREME_POINT_OF_SEGMENT];
 411       ALL_TAC] THEN
 412     SUBGOAL_THEN `~(v:real^3 = vec 0) /\ ~(w:real^3 = vec 0)`
 413     STRIP_ASSUME_TAC THENL
 414      [ASM_MESON_TAC[EXTREME_POINT_NOT_IN_INTERIOR]; ALL_TAC] THEN
 415     REWRITE_TAC[SET_RULE `{a} UNION {b,c} = {a,b,c}`] THEN
 416     ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT; NOT_EXISTS_THM] THEN
 417     X_GEN_TAC `t:real` THEN
 418     ASM_CASES_TAC `t = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
 419     DISCH_THEN SUBST_ALL_TAC THEN
 420     FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
 421      `~(x = &0) ==> x < &0 \/ &0 < x`))
 422     THENL
 423      [MP_TAC(ISPECL [`segment[v:real^3,t % v]`; `p:real^3->bool`]
 424         FACE_OF_DISJOINT_INTERIOR) THEN
 425       ASM_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
 426       EXISTS_TAC `vec 0:real^3` THEN ASM_REWRITE_TAC[IN_INTER] THEN
 427       REWRITE_TAC[IN_SEGMENT] THEN EXISTS_TAC `&1 / (&1 - t)` THEN
 428       ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ;
 429                    REAL_ARITH `t < &0 ==> &0 < &1 - t`] THEN
 430       REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
 431       CONV_TAC SYM_CONV THEN
 432       REWRITE_TAC[VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_RDISTRIB] THEN
 433       REWRITE_TAC[VECTOR_MUL_EQ_0] THEN DISJ1_TAC THEN
 434       UNDISCH_TAC `t < &0` THEN CONV_TAC REAL_FIELD;
 435       MP_TAC(ISPECL [`p:real^3->bool`; `segment[v:real^3,t % v]`;
 436                      `segment[v:real^3,t % v]`; `v:real^3`; `t % v:real^3`;
 437                      `t:real`; `&1`] POLYHEDRON_COLLINEAR_FACES) THEN
 438       ASM_REWRITE_TAC[ENDS_IN_SEGMENT; real_gt; REAL_LT_01] THEN
 439       ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_MUL_RCANCEL; REAL_MUL_LID] THEN
 440       ASM_MESON_TAC[VECTOR_MUL_LID]];
 441     REWRITE_TAC[fan7] THEN
 442     MAP_EVERY X_GEN_TAC [`e1:real^3->bool`; `e2:real^3->bool`] THEN
 443     DISCH_TAC THEN
 444     SUBGOAL_THEN
 445      `(?x1 y1:real^3. e1 = {x1,y1} /\ segment[x1,y1] face_of p) /\
 446       (?x2 y2:real^3. e2 = {x2,y2} /\ segment[x2,y2] face_of p)`
 447     STRIP_ASSUME_TAC THENL
 448      [FIRST_X_ASSUM(fun th -> MP_TAC th THEN MATCH_MP_TAC MONO_AND) THEN
 449       SIMP_TAC[IN_UNION; TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
 450       REWRITE_TAC[edges; edge_of; vertices; IN_ELIM_THM] THEN
 451       REPEAT CONJ_TAC THENL
 452        [MESON_TAC[]; ALL_TAC; MESON_TAC[]; ALL_TAC] THEN
 453       DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN
 454       REPEAT(EXISTS_TAC `v:real^3`) THEN
 455       ASM_REWRITE_TAC[SEGMENT_REFL; FACE_OF_SING; INSERT_AC];
 456       ALL_TAC] THEN
 457     SUBGOAL_THEN
 458      `(x1:real^3) extreme_point_of p /\ y1 extreme_point_of p /\
 459       x2 extreme_point_of p /\ y2 extreme_point_of p`
 460     STRIP_ASSUME_TAC THENL
 461      [REWRITE_TAC[GSYM FACE_OF_SING] THEN REPEAT CONJ_TAC THEN
 462       MATCH_MP_TAC FACE_OF_TRANS THEN
 463       ASM_MESON_TAC[FACE_OF_SING; EXTREME_POINT_OF_SEGMENT];
 464       ALL_TAC] THEN
 465     SUBGOAL_THEN
 466      `~(x1:real^3 = vec 0) /\ ~(y1:real^3 = vec 0) /\
 467       ~(x2:real^3 = vec 0) /\ ~(y2:real^3 = vec 0)`
 468     STRIP_ASSUME_TAC THENL
 469      [ASM_MESON_TAC[EXTREME_POINT_NOT_IN_INTERIOR]; ALL_TAC] THEN
 470     ASM_SIMP_TAC[AFF_GE_0_CONVEX_HULL_ALT; FINITE_INTER; IN_INTER;
 471                  IN_INSERT; NOT_IN_EMPTY; FINITE_INSERT; FINITE_EMPTY] THEN
 472     MATCH_MP_TAC(SET_RULE
 473      `s INTER t = u ==> (a INSERT s) INTER (a INSERT t) = a INSERT u`) THEN
 474     MATCH_MP_TAC EQ_TRANS THEN
 475     EXISTS_TAC `{t % y:real^3 | &0 < t /\
 476                                 y IN (convex hull {x1,y1}) INTER
 477                                      (convex hull {x2,y2})}` THEN
 478     CONJ_TAC THENL
 479      [REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL] THEN
 480       MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 481        [ALL_TAC; SET_TAC[]] THEN
 482       REWRITE_TAC[SUBSET; IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN
 483       MAP_EVERY X_GEN_TAC [`s:real`; `x:real^3`] THEN
 484       DISCH_TAC THEN DISCH_TAC THEN
 485       REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 486       MAP_EVERY X_GEN_TAC [`t:real`; `y:real^3`] THEN STRIP_TAC THEN
 487       MP_TAC(ISPECL [`p:real^3->bool`; `segment[x1:real^3,y1]`;
 488                      `segment[x2:real^3,y2]`; `x:real^3`; `y:real^3`;
 489                      `s:real`; `t:real`] POLYHEDRON_COLLINEAR_FACES) THEN
 490       ASM_REWRITE_TAC[real_gt] THEN DISCH_THEN SUBST_ALL_TAC THEN
 491       MAP_EVERY EXISTS_TAC [`t:real`; `y:real^3`] THEN ASM_REWRITE_TAC[] THEN
 492       UNDISCH_TAC `t % x:real^3 = t % y` THEN
 493       ASM_SIMP_TAC[VECTOR_MUL_LCANCEL; REAL_LT_IMP_NZ] THEN ASM_MESON_TAC[];
 494       SUBGOAL_THEN
 495        `(convex hull {x1,y1}) INTER (convex hull {x2,y2}) :real^3->bool =
 496         convex hull ({x1, y1} INTER {x2, y2})`
 497        (fun th -> REWRITE_TAC[th]) THEN
 498       MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 499        [ALL_TAC;
 500         REWRITE_TAC[SUBSET_INTER] THEN CONJ_TAC THEN
 501         MATCH_MP_TAC HULL_MONO THEN SET_TAC[]] THEN
 502       MP_TAC(ISPECL [`p:real^3->bool`; `x1:real^3`; `y1:real^3`;
 503                      `x2:real^3`; `y2:real^3`] lemma) THEN
 504       ASM_REWRITE_TAC[] THEN STRIP_TAC THENL
 505        [ASM_REWRITE_TAC[INTER_IDEMPOT; SUBSET_REFL];
 506         ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; HULL_SUBSET]]]]);;
 507
 508
 509
 510 (* Hoang Le Truong's additions start here. *)
 511
 512 let fchanged=new_definition`fchanged f={v| ?v1 t. v=t% v1 /\ v1 IN (relative_interior f)/\ t> &0}`;;
 513
 514 let CONVEX_RELATIVE_INTERIOR=prove(`!p:real^3->bool.
 515  polyhedron p
 516 ==> convex (relative_interior p) `,
 517 let LEMMA=prove(`!f:(real^3->bool)->bool (a:(real^3->bool)->real^3) (b:(real^3->bool)->real).
 518 {x | !h. h IN f ==> a h dot x < b h}=INTERS{{x | a h dot x < b h}| h IN f} `,
 519
 520 REPEAT STRIP_TAC
 521 THEN REWRITE_TAC[INTERS;IN_ELIM_THM;]
 522 THEN ONCE_REWRITE_TAC[EXTENSION]
 523 THEN REWRITE_TAC[IN_ELIM_THM]
 524 THEN GEN_TAC
 525 THEN EQ_TAC
 526 THENL[
 527 REPEAT STRIP_TAC
 528 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 529 THEN ASM_TAC
 530 THEN DISCH_THEN(LABEL_TAC"LINH")
 531 THEN REPEAT STRIP_TAC
 532 THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`h:real^3->bool`);
 533  DISCH_THEN(LABEL_TAC"LINH")
 534 THEN REPEAT STRIP_TAC
 535 THEN SUBGOAL_THEN`?(h':real^3->bool). h' IN f /\ {x | (a:(real^3->bool)->real^3) h dot x < (b:(real^3->bool)->real) h} = {x | a h' dot x < b h'}`ASSUME_TAC
 536 THENL[
 537 EXISTS_TAC`h:real^3->bool`
 538 THEN ASM_REWRITE_TAC[];
 539 REMOVE_THEN "LINH"(fun th-> MRESAL1_TAC th`{x:real^3 | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x < (b:(real^3->bool)->real) h}`[IN_ELIM_THM])]])in
 540
 541 REPEAT STRIP_TAC THEN FIRST_ASSUM
 542    (MP_TAC o GEN_REWRITE_RULE I [POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN
 543   REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
 544   SIMP_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM]
 545 THEN REPEAT STRIP_TAC
 546 THEN MRESA_TAC RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT[`p:real^3->bool`;`f:(real^3->bool)->bool`;`a:(real^3->bool)->real^3`;`b:(real^3->bool)->real`]
 547 THEN POP_ASSUM MP_TAC
 548 THEN FIND_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])`(p:real^3->bool) = affine hull p INTER INTERS f`
 549 THEN REWRITE_TAC[]
 550 THEN STRIP_TAC
 551 THEN ASM_REWRITE_TAC[SET_RULE`{x | x IN p /\ (!h. h IN f ==> a h dot x < b h)}= p INTER {x | (!h. h IN f ==> a h dot x < b h)}`]
 552 THEN MATCH_MP_TAC CONVEX_INTER
 553 THEN MRESA1_TAC POLYHEDRON_EQ_FINITE_FACES`p:real^3->bool`
 554 THEN MRESA_TAC LEMMA [`f:(real^3->bool)->bool`;`(a:(real^3->bool)->real^3)`; `(b:(real^3->bool)->real)`]
 555 THEN MATCH_MP_TAC CONVEX_INTERS
 556 THEN REWRITE_TAC[IN_ELIM_THM]
 557 THEN REPEAT STRIP_TAC
 558 THEN ASM_REWRITE_TAC[CONVEX_HALFSPACE_LT]);;
 559
 560
 561 let CONVEX_RELATIVE_INTERIOR_FACE=prove(`!p f:(real^3->bool).
 562  polyhedron p
 563 /\ f face_of p
 564 ==> convex (relative_interior f) `,
 565
 566 REPEAT STRIP_TAC
 567 THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:(real^3->bool)`;`f:real^3->bool`]
 568 THEN MRESA1_TAC CONVEX_RELATIVE_INTERIOR`f:(real^3->bool)`);;
 569
 570 let CONVEX_RELATIVE_INTERIOR_FACET=prove(`!p f:(real^3->bool).
 571  polyhedron p
 572 /\ f facet_of p
 573 ==> convex (relative_interior f) `,
 574 REPEAT STRIP_TAC
 575 THEN MRESA_TAC CONVEX_RELATIVE_INTERIOR_FACE[`p:(real^3->bool)`;`f:real^3->bool`]
 576 THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`f:(real^3->bool)`;`p:(real^3->bool)`]);;
 577
 578 let CONNECTED_RELATIVE_INTERIOR_FACET=prove(`!p f:(real^3->bool).
 579  polyhedron p
 580 /\ f facet_of p
 581 ==> connected (relative_interior f) `,
 582 REPEAT STRIP_TAC
 583 THEN MRESA_TAC CONVEX_RELATIVE_INTERIOR_FACET[`p:(real^3->bool)`;`f:real^3->bool`]
 584 THEN MRESA1_TAC CONVEX_CONNECTED `relative_interior f:(real^3->bool)`);;
 585
 586 let CONNECTED_HALF_LINE=prove(`!x:real^3 v. connected(aff_gt {x} {v})`,
 587 REPEAT STRIP_TAC
 588 THEN MATCH_MP_TAC CONVEX_CONNECTED
 589 THEN SIMP_TAC[CONVEX_AFF_GT]);;
 590
 591
 592
 593 let RELATIVE_SUBSET_FCHANGE=prove(`!p x f:(real^3->bool).
 594   bounded p /\ polyhedron p /\ x IN interior p
 595 /\ f facet_of p
 596 ==> (relative_interior f) SUBSET fchanged f`,
 597
 598 REPEAT STRIP_TAC
 599 THEN REWRITE_TAC[SUBSET; fchanged;IN_ELIM_THM]
 600 THEN REPEAT STRIP_TAC
 601 THEN EXISTS_TAC`x':real^3`
 602 THEN EXISTS_TAC `&1`
 603 THEN ASM_REWRITE_TAC[REAL_ARITH`&1> &0`;VECTOR_ARITH`A= &1 %A`]);;
 604
 605
 606
 607 let AFF_GT_SUBSET_FCHANGED=prove(`!p x f:(real^3->bool) y.
 608   bounded p /\ polyhedron p /\ x IN interior p
 609 /\ f facet_of p
 610 /\ y IN (relative_interior f)
 611 ==>  {v| ?t. &0< t /\ v=t%y} SUBSET fchanged f  `,
 612 REWRITE_TAC[fchanged;SUBSET;IN_ELIM_THM]
 613 THEN REPEAT STRIP_TAC
 614 THEN EXISTS_TAC`y:real^3`
 615 THEN EXISTS_TAC`t:real`
 616 THEN ASM_REWRITE_TAC[REAL_ARITH` t> &0<=> &0< t`]);;
 617
 618
 619
 620 let CONNECTED_HALF_LINE1=prove(`!y:real^3. connected {v| ?t. &0< t /\ v=t%y}`,
 621 let LEMMA=prove(`!x:real^3. ~(x= vec 0)==>aff_gt {vec 0} {x}= {v| ?t. &0< t /\ v=t%x}`,
 622
 623 REPEAT STRIP_TAC
 624 THEN MRESAL_TAC AFF_GT_1_1[`(vec 0):real^3`;`x:real^3`][SET_RULE`DISJOINT {vec 0} {x} <=> ~(x= vec 0)`;VECTOR_ARITH`t % (vec 0)+A=A:real^3`;EXTENSION;IN_ELIM_THM]
 625 THEN GEN_TAC
 626 THEN EQ_TAC
 627 THENL[
 628 REPEAT STRIP_TAC
 629 THEN EXISTS_TAC`t2:real`
 630 THEN ASM_REWRITE_TAC[];
 631 REPEAT STRIP_TAC
 632 THEN EXISTS_TAC`&1-t:real`
 633 THEN EXISTS_TAC`t:real`
 634 THEN ASM_REWRITE_TAC[REAL_ARITH`&1-t+t= &1`]]) in
 635
 636 REPEAT STRIP_TAC
 637 THEN DISJ_CASES_TAC(SET_RULE`(y= vec 0)\/ ~(y:real^3 = vec 0)`)
 638 THENL[
 639 ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0= vec 0`]
 640 THEN SUBGOAL_THEN`{v:real^3 | ?t. &0 < t /\ v = vec 0}= {vec 0}` ASSUME_TAC
 641 THENL[
 642 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
 643 THEN GEN_TAC
 644 THEN EQ_TAC
 645 THENL[
 646 STRIP_TAC THEN ASM_REWRITE_TAC[];
 647 STRIP_TAC THEN EXISTS_TAC`&1`
 648 THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1`]];
 649
 650 ASM_REWRITE_TAC[CONNECTED_SING]];
 651
 652 MRESA1_TAC LEMMA`y:real^3`
 653 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 654 THEN MRESA_TAC CONNECTED_HALF_LINE[`vec 0:real^3`;`y:real^3`]]);;
 655
 656
 657 let CONNECTED_COMPONENT_OF_SUBSET = prove
 658  (`!s t x y. s SUBSET t /\ connected_component s x y
 659            ==> connected_component t x y`,
 660   REWRITE_TAC[connected_component] THEN SET_TAC[]);;
 661
 662 let CONNECTED_COMPONENT_TRANS = prove
 663  (`!s x y z:real^N.
 664     connected_component s x y /\ connected_component s y z
 665     ==> connected_component s x z`,
 666   REPEAT GEN_TAC THEN REWRITE_TAC[connected_component] THEN
 667   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `t:real^N->bool`)
 668                              (X_CHOOSE_TAC `u:real^N->bool`)) THEN
 669   EXISTS_TAC `t UNION u:real^N->bool` THEN
 670   ASM_REWRITE_TAC[IN_UNION; UNION_SUBSET] THEN
 671   MATCH_MP_TAC CONNECTED_UNION THEN ASM SET_TAC[]);;
 672
 673
 674
 675 let CONNECTED_FCHANGED=prove(`!p x f:(real^3->bool).
 676   bounded p /\ polyhedron p /\ x IN interior p
 677 /\ f facet_of p
 678 ==> connected (fchanged f) `,
 679
 680 REPEAT STRIP_TAC
 681 THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT;IN_ELIM_THM]
 682 THEN REPEAT STRIP_TAC
 683 THEN POP_ASSUM MP_TAC
 684 THEN POP_ASSUM MP_TAC
 685 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[fchanged]
 686 THEN REWRITE_TAC[IN_ELIM_THM]
 687 THEN STRIP_TAC
 688 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[fchanged]
 689 THEN REWRITE_TAC[IN_ELIM_THM]
 690 THEN STRIP_TAC
 691 THEN SUBGOAL_THEN`x' IN {v| ?t. &0< t /\ v=t % v1:real^3}`ASSUME_TAC
 692 THENL[
 693 REWRITE_TAC[IN_ELIM_THM]
 694 THEN EXISTS_TAC`t:real`
 695 THEN ASM_REWRITE_TAC[REAL_ARITH`&0< t<=> t> &0`];
 696
 697 SUBGOAL_THEN`v1 IN {v| ?t. &0< t /\ v=t % v1:real^3}`ASSUME_TAC
 698 THENL[
 699 REWRITE_TAC[IN_ELIM_THM]
 700 THEN EXISTS_TAC`&1:real`
 701 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 %A=A`]
 702 THEN POP_ASSUM MP_TAC
 703 THEN REAL_ARITH_TAC;
 704
 705 MRESA1_TAC CONNECTED_HALF_LINE1`v1:real^3`
 706 THEN POP_ASSUM MP_TAC
 707 THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT]
 708 THEN STRIP_TAC
 709 THEN POP_ASSUM (fun th-> MRESA_TAC th[`x':real^3`;`v1:real^3`])
 710 THEN SUBGOAL_THEN`y IN {v| ?t. &0< t /\ v=t % v1':real^3}`ASSUME_TAC
 711 THENL[
 712 REWRITE_TAC[IN_ELIM_THM]
 713 THEN EXISTS_TAC`t':real`
 714 THEN ASM_REWRITE_TAC[REAL_ARITH`&0< t' <=> t'> &0`];
 715
 716 SUBGOAL_THEN`v1' IN {v| ?t. &0< t /\ v=t % v1':real^3}`ASSUME_TAC
 717 THENL[
 718 REWRITE_TAC[IN_ELIM_THM]
 719 THEN EXISTS_TAC`&1:real`
 720 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 %A=A`]
 721 THEN POP_ASSUM MP_TAC
 722 THEN REAL_ARITH_TAC;
 723
 724
 725 MRESA1_TAC CONNECTED_HALF_LINE1`v1':real^3`
 726 THEN POP_ASSUM MP_TAC
 727 THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT]
 728 THEN STRIP_TAC
 729 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v1':real^3`;`y:real^3`;])
 730 THEN MRESA_TAC CONNECTED_RELATIVE_INTERIOR_FACET[`p:real^3->bool`;`f:real^3->bool`]
 731 THEN POP_ASSUM MP_TAC
 732 THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT]
 733 THEN STRIP_TAC
 734 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v1:real^3`;`v1':real^3`;])
 735 THEN MRESA_TAC AFF_GT_SUBSET_FCHANGED[`p:real^3->bool`;`x:real^3`;`f:real^3->bool`;`v1:real^3`]
 736 THEN MRESA_TAC AFF_GT_SUBSET_FCHANGED[`p:real^3->bool`;`x:real^3`;`f:real^3->bool`;`v1':real^3`]
 737 THEN MRESA_TAC RELATIVE_SUBSET_FCHANGE[`p:real^3->bool`;`x:real^3`;`f:real^3->bool`;]
 738  THEN MRESA_TAC CONNECTED_COMPONENT_OF_SUBSET[`{v | ?t. &0 < t /\ v = t % v1:real^3}`;`fchanged (f:real^3->bool)`;`t% v1:real^3`;`v1:real^3`]
 739  THEN MRESA_TAC CONNECTED_COMPONENT_OF_SUBSET[`{v | ?t. &0 < t /\ v = t % v1':real^3}`;`fchanged (f:real^3->bool)`;`v1':real^3`;`t'% v1':real^3`]
 740  THEN MRESA_TAC CONNECTED_COMPONENT_OF_SUBSET[`relative_interior (f:real^3->bool)`;`fchanged (f:real^3->bool)`;`v1:real^3`;` v1':real^3`]
 741 THEN MRESA_TAC CONNECTED_COMPONENT_TRANS[`fchanged f:real^3->bool`;`t % v1:real^3`;`v1:real^3`;`v1':real^3`]
 742 THEN MRESA_TAC CONNECTED_COMPONENT_TRANS[`fchanged f:real^3->bool`;`t % v1:real^3`;`v1':real^3`;`t' % v1':real^3`]]]]]);;
 743
 744
 745 let CONTINUOUS_ON_LIFT_DOT = prove
 746  (`!s a. (lift o (\y. a dot y)) continuous_on s`,
 747   SIMP_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_ON; CONTINUOUS_AT_LIFT_DOT]);;
 748
 749
 750
 751
 752 let AFFINITE_HULL_BALL_EQ_UNIV=prove(`!x e. &0< e ==> affine hull ball (x,e) =(:real^3)`,
 753 let delta_func=new_definition`delta_func x y= (if x=y then &1 else &0) ` in
 754 (let func1=new_definition`func1 a x y z= (if x=z then a else  (if  y= z then (&1- a) else &0)) ` in
 755
 756 REPEAT STRIP_TAC
 757 THEN  REWRITE_TAC[EXTENSION]
 758 THEN REWRITE_TAC[AFFINE_HULL_EXPLICIT;IN_ELIM_THM]
 759 THEN GEN_TAC
 760 THEN EQ_TAC
 761 THENL[
 762 SET_TAC[];
 763 STRIP_TAC
 764 THEN DISJ_CASES_TAC(SET_RULE`x'= x:real^3\/ ~(x'=x)`)
 765 THENL[
 766 ASM_REWRITE_TAC[]
 767 THEN EXISTS_TAC`{x:real^3}`
 768 THEN EXISTS_TAC`(delta_func (x:real^3))`
 769 THEN REWRITE_TAC[FINITE_SING;SET_RULE`~({x}={})`;SUM_SING;VSUM_SING;delta_func;VECTOR_ARITH`&1 % x=x`;SUBSET;IN_SING]
 770 THEN STRIP_TAC
 771 THEN STRIP_TAC
 772 THEN ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist; VECTOR_ARITH`x-x= vec 0`;NORM_0];
 773
 774 ABBREV_TAC`v =(inv(norm (x'-x)) * e/ &2) % (x'-x) +x:real^3`
 775 THEN SUBGOAL_THEN `~(x=v:real^3)` ASSUME_TAC
 776 THENL[
 777 POP_ASSUM (fun th-> REWRITE_TAC[SYM th; VECTOR_ARITH`A= B+A<=> B= vec 0`; GSYM NORM_EQ_0;NORM_MUL;])
 778 THEN REWRITE_TAC[REAL_ENTIRE; REAL_ABS_MUL;REAL_ABS_INV;REAL_ABS_NORM;DE_MORGAN_THM]
 779 THEN MRESA_TAC imp_norm_not_zero_fan[`x':real^3`;`x:real^3`]
 780 THEN MRESA_TAC imp_inv_norm_not_zero_fan[`x':real^3`;`x:real^3`]
 781 THEN ASM_TAC
 782 THEN REAL_ARITH_TAC;
 783
 784 ABBREV_TAC`a=  (norm(x'-x:real^3) *inv e * &2)`
 785 THEN EXISTS_TAC`{x,v:real^3}`
 786 THEN EXISTS_TAC `func1 (a:real) v (x:real^3)`
 787 THEN ASM_REWRITE_TAC[SET_RULE`~({x, v} = {})`]
 788 THEN SIMP_TAC[HAS_SIZE;  FINITE_INSERT; FINITE_EMPTY;
 789                  IN_INSERT; NOT_IN_EMPTY;VSUM_CLAUSES;SUM_CLAUSES;func1]
 790 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - a + a + &0 = &1`; VECTOR_ARITH`(&1 - a) % x + a % v + vec 0 = x'<=>  a % (v-x) = x'- x`]
 791 THEN EXPAND_TAC"v"
 792 THEN REWRITE_TAC[VECTOR_ARITH`(A+B)-B=A:real^3 /\ a % b % v=(a*b)%v`]
 793 THEN EXPAND_TAC"a"
 794 THEN REWRITE_TAC[REAL_ARITH`(norm (x' - x) * inv e * &2) * inv (norm (x' - x)) * e / &2= ( inv (norm (x' - x)) * norm (x' - x)) *( inv e * e) `]
 795 THEN MRESA_TAC IMP_NORM_FAN[`x':real^3`;`x:real^3`]
 796 THEN MP_TAC(REAL_ARITH`&0< e==> ~(e= &0) /\ &0 <= e`)
 797 THEN RESA_TAC
 798 THEN MRESA1_TAC REAL_MUL_LINV`e:real`
 799 THEN REWRITE_TAC[VECTOR_ARITH`(&1 * &1) %v= v`;SUBSET;SET_RULE`x IN {y,z}<=> x= y \/ x= z`]
 800 THEN GEN_TAC
 801 THEN STRIP_TAC
 802 THENL[
 803 ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist; VECTOR_ARITH`x-x= vec 0`;NORM_0];
 804 ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist; ]
 805 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 806 THEN EXPAND_TAC"v"
 807 THEN REWRITE_TAC[VECTOR_ARITH`A-(B+A)= -- B:real^3`; NORM_NEG;NORM_MUL;REAL_ABS_MUL;REAL_ABS_INV;REAL_ABS_NORM;]
 808 THEN ONCE_REWRITE_TAC[ REAL_ARITH`(a * b)* c= (a * c) * b`]
 809 THEN ASM_REWRITE_TAC[REAL_ARITH`abs(e/ &2)= abs(e)/ &2`]
 810 THEN MRESA1_TAC REAL_ABS_REFL`e:real`
 811 THEN ASM_TAC
 812 THEN REAL_ARITH_TAC]]]]));;
 813
 814
 815 let INTERIOR_AFFINIE_HUL_EQ_UNIV=prove(`!x p:(real^3->bool).
 816  x IN interior p
 817 ==>  affine hull p= (:real^3)`,
 818
 819 REWRITE_TAC[IN_INTERIOR]
 820 THEN REPEAT STRIP_TAC
 821 THEN MRESA_TAC AFFINITE_HULL_BALL_EQ_UNIV[`x:real^3`;`e:real`]
 822 THEN MRESA_TAC HULL_MONO [`affine:(real^3->bool)->bool`;`ball(x:real^3,e)`;`p:real^3->bool`]
 823 THEN POP_ASSUM MP_TAC
 824 THEN SET_TAC[]);;
 825
 826
 827
 828 let AFF_DIM_INTERIOR_EQ_3=prove(`!x p:(real^3->bool).
 829  x IN interior p
 830 ==>  aff_dim p= &3`,
 831
 832 REPEAT STRIP_TAC
 833 THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`x:real^3`;`p:real^3->bool`]
 834 THEN MRESA1_TAC AFF_DIM_AFFINE_HULL`p:real^3->bool`
 835 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 836 THEN SIMP_TAC[AFF_DIM_UNIV;DIMINDEX_3]);;
 837
 838
 839
 840 let INTERIOR_IMP_RELATIVE_INTERIOR=prove(`!x p:(real^3->bool).
 841    x IN interior p
 842 ==> x IN relative_interior p`,
 843 REPEAT STRIP_TAC
 844 THEN REWRITE_TAC[RELATIVE_INTERIOR;IN_ELIM_THM]
 845 THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
 846 THEN MP_TAC(SET_RULE`x IN interior p /\ interior p SUBSET p ==> (x:real^3) IN p`)
 847 THEN RESA_TAC
 848 THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`x:real^3`;`p:real^3->bool`]
 849 THEN REMOVE_ASSUM_TAC
 850 THEN REMOVE_ASSUM_TAC
 851 THEN REMOVE_ASSUM_TAC
 852 THEN POP_ASSUM MP_TAC
 853 THEN REWRITE_TAC[interior;IN_ELIM_THM; SET_RULE`t INTER (:real^3)= (t:real^3->bool)`]);;
 854
 855
 856
 857
 858 let IN_RELATIVE_INTERIOR1 = prove
 859  (`!x:real^N s.
 860         x IN relative_interior s ==>
 861          ?e. &0 < e /\ (ball(x,e) INTER (affine hull s)) SUBSET relative_interior s`,
 862
 863   REPEAT GEN_TAC THEN REWRITE_TAC[IN_RELATIVE_INTERIOR; IN_ELIM_THM]
 864 THEN STRIP_TAC
 865 THEN EXISTS_TAC`e:real`
 866 THEN ASM_REWRITE_TAC[SUBSET ;IN_RELATIVE_INTERIOR; IN_ELIM_THM]
 867 THEN REPEAT STRIP_TAC
 868 THENL[ASM_TAC THEN SET_TAC[];
 869
 870
 871 MP_TAC(SET_RULE`x' IN ball (x,e) INTER affine hull s ==> x' IN ball (x:real^N,e)`)
 872 THEN RESA_TAC
 873 THEN MRESAL_TAC OPEN_BALL[`x:real^N`;`e:real`][open_def]
 874 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x':real^N`)
 875 THEN SUBGOAL_THEN`ball(x':real^N,e') SUBSET ball(x,e)` ASSUME_TAC
 876 THENL[
 877 REWRITE_TAC[SUBSET]
 878 THEN GEN_TAC
 879 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[ball;IN_ELIM_THM;]
 880 THEN ONCE_REWRITE_TAC[DIST_SYM]
 881 THEN ASM_REWRITE_TAC[];
 882  EXISTS_TAC`e':real`
 883 THEN ASM_REWRITE_TAC[]
 884 THEN REPEAT STRIP_TAC
 885 THEN ASM_TAC
 886 THEN SET_TAC[]]]);;
 887
 888
 889
 890
 891 let FCHANGED_OPEN=prove(`!p f:(real^3->bool).
 892   bounded p /\ polyhedron p /\ vec 0 IN interior p
 893 /\ f facet_of p
 894 ==> open (fchanged f) `,
 895
 896 REPEAT STRIP_TAC THEN FIRST_ASSUM
 897    (MP_TAC o GEN_REWRITE_RULE I [POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN
 898   REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
 899   SIMP_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM]
 900 THEN REPEAT STRIP_TAC
 901 THEN POP_ASSUM MP_TAC
 902 THEN POP_ASSUM MP_TAC
 903 THEN DISCH_THEN(LABEL_TAC"LINH1")
 904 THEN STRIP_TAC
 905 THEN MRESA_TAC FACET_OF_POLYHEDRON_EXPLICIT[`p:real^3->bool`;`f':(real^3->bool)->bool`;`a:(real^3->bool)->real^3`;`b:(real^3->bool)->real`]
 906 THEN POP_ASSUM MP_TAC
 907 THEN FIND_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])`p = affine hull p INTER INTERS (f':(real^3->bool)->bool)`
 908 THEN REWRITE_TAC[open_def]
 909 THEN STRIP_TAC
 910 THEN POP_ASSUM (fun th-> MRESA1_TAC th `f:real^3->bool`)
 911 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN ASSUME_TAC(SYM th))
 912 THEN GEN_TAC
 913 THEN GEN_REWRITE_TAC(LAND_CONV  o DEPTH_CONV)[fchanged]
 914 THEN REWRITE_TAC[IN_ELIM_THM]
 915 THEN STRIP_TAC
 916 THEN ASM_REWRITE_TAC[]
 917 THEN MRESA_TAC CONTINUOUS_ON_LIFT_DOT[`(:real^3)`;`(a:(real^3->bool)->real^3) (h:real^3->bool)`]
 918 THEN POP_ASSUM MP_TAC
 919 THEN REWRITE_TAC[continuous_on;]
 920 THEN STRIP_TAC
 921 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `v1:real^3`[SET_RULE`v1 IN (:real^3)`;o_DEF;dist;GSYM LIFT_SUB])
 922 THEN POP_ASSUM MP_TAC
 923 THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool`
 924 THEN MP_TAC(SET_RULE`(v1:real^3) IN relative_interior f /\ relative_interior f SUBSET f /\ p INTER {x | a h dot x = b h} = f
 925 ==> v1 IN {x | a (h:real^3->bool) dot x = b h}`)
 926 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 927 THEN RESA_TAC
 928 THEN DISCH_THEN(LABEL_TAC"LINH")
 929 THEN SUBGOAL_THEN`affine hull f= {x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}` ASSUME_TAC
 930 THENL(*1*)[
 931
 932 FIND_ASSUM(MP_TAC)`f facet_of (p:real^3->bool)`
 933 THEN REWRITE_TAC[facet_of]
 934 THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
 935 THEN STRIP_TAC
 936 THEN USE_THEN "LINH1"(fun th-> MP_TAC(ISPEC `h:real^3->bool` th))
 937 THEN FIND_ASSUM (fun th-> REWRITE_TAC[th])`(h:real^3->bool) IN f'`
 938 THEN STRIP_TAC
 939 THEN MRESA_TAC AFF_DIM_HYPERPLANE[`(a:(real^3->bool)->real^3) (h:real^3->bool)`;
 940 `(b:(real^3->bool)->real) (h:real^3->bool)`]
 941 THEN POP_ASSUM MP_TAC
 942 THEN REWRITE_TAC[DIMINDEX_3]
 943 THEN STRIP_TAC
 944 THEN MRESA_TAC AFFINE_HYPERPLANE[`(a:(real^3->bool)->real^3) (h:real^3->bool)`;
 945 `(b:(real^3->bool)->real) (h:real^3->bool)`]
 946 THEN MRESA1_TAC AFFINE_HULL_EQ`{x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}`
 947 THEN MRESA_TAC AFF_DIM_EQ_AFFINE_HULL[`f:real^3->bool`;`{x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}`]
 948 THEN POP_ASSUM MATCH_MP_TAC
 949 THEN STRIP_TAC
 950 THENL[ ASM_TAC THEN SET_TAC[];ARITH_TAC];(*1*)
 951
 952 MRESA_TAC IN_RELATIVE_INTERIOR1[`v1:real^3`;`f:real^3->bool`]
 953 THEN MRESA_TAC IN_RELATIVE_INTERIOR[`v1:real^3`;`f:real^3->bool`]
 954 THEN ABBREV_TAC`r1= min (inv(norm (v1:real^3)) *e / &6) (&1) / &2 `
 955 THEN ABBREV_TAC`r2= abs((b:(real^3->bool)->real) (h:real^3->bool)) * r1 / &2`
 956 THEN MRESA1_TAC RELATIVE_INTERIOR_OF_POLYHEDRON`p:real^3->bool`
 957 THEN MRESA_TAC INTERIOR_IMP_RELATIVE_INTERIOR[`vec 0:real^3`;`p:real^3->bool`]
 958 THEN POP_ASSUM MP_TAC
 959 THEN REWRITE_TAC[DIFF;IN_ELIM_THM]
 960 THEN STRIP_TAC
 961 THEN MP_TAC(SET_RULE`~(vec 0 IN UNIONS {f | f facet_of p}) /\ v1 IN f /\ f facet_of p==> ~(v1 = vec 0:real^3)`)
 962 THEN RESA_TAC
 963 THEN MRESAL_TAC IMP_NORM_FAN[`v1:real^3`;`vec 0:real^3`][VECTOR_ARITH`a - vec 0 = a`]
 964 THEN MRESA_TAC REAL_LT_MUL[`inv(norm (v1:real^3))`;`e:real`]
 965 THEN MP_TAC(REAL_ARITH`&0< inv (norm (v1:real^3)) * e ==> &0 < min (inv (norm v1) * e / &6) (&1) / &2 `)
 966 THEN RESA_TAC
 967 THEN USE_THEN "LINH1"(fun th-> MP_TAC(ISPEC `h:real^3->bool` th))
 968 THEN FIND_ASSUM (fun th-> REWRITE_TAC[th])`(h:real^3->bool) IN f'`
 969 THEN STRIP_TAC
 970 THEN MRESA1_TAC REAL_ABS_CASES`(b:(real^3->bool)->real) (h:real^3->bool)`
 971 THENL(*2*)[
 972
 973 SUBGOAL_THEN `vec 0 IN {x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}` ASSUME_TAC
 974 THENL[
 975 ASM_REWRITE_TAC[IN_ELIM_THM;DOT_RZERO];
 976
 977 MP_TAC(SET_RULE`p INTER {x | a h dot x = b h} = f /\ vec 0 IN {x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h} /\ vec 0 IN p ==> vec 0 IN f `)
 978 THEN RESA_TAC
 979 THEN MP_TAC(SET_RULE`~(vec 0 IN UNIONS {f | f facet_of (p:real^3->bool)}) /\ vec 0 IN f /\ f facet_of p ==> F`)
 980 THEN ASM_REWRITE_TAC[]];(*2*)
 981
 982 MRESA_TAC REAL_LT_MUL[`abs ((b:(real^3->bool)->real) (h:real^3->bool))`;`r1:real`]
 983 THEN MP_TAC(REAL_ARITH`&0 < abs ((b:(real^3->bool)->real) (h:real^3->bool)) * r1 ==> &0 < abs (b h) * r1/ &2`)
 984 THEN ASM_REWRITE_TAC[]
 985 THEN STRIP_TAC
 986 THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`r2:real`)
 987 THEN SUBGOAL_THEN`!y:real^3. norm(y-v1)< d ==> ?t1. abs(&1- t1)< r1 /\ &0 < t1 /\  t1 % y IN {x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}`
 988 ASSUME_TAC
 989 THENL(*3*)[
 990 POP_ASSUM MP_TAC
 991 THEN DISCH_THEN (LABEL_TAC"LINH2")
 992 THEN REPEAT STRIP_TAC
 993 THEN REMOVE_THEN "LINH2"(fun th-> MRESA1_TAC th`y:real^3`)
 994 THEN REWRITE_TAC[IN_ELIM_THM;DOT_RMUL]
 995 THEN POP_ASSUM MP_TAC
 996 THEN REWRITE_TAC[NORM_LIFT]
 997 THEN STRIP_TAC
 998 THEN MP_TAC(REAL_ARITH`min (inv (norm (v1:real^3)) * e / &6) (&1) / &2 = r1 ==> r1< &1`)
 999 THEN RESA_TAC
1000 THEN MRESAL_TAC REAL_LT_LMUL[`abs ((b:(real^3->bool)->real) (h:real^3->bool))`;`r1:real`;`&1`][REAL_ARITH`a* &1=a`]
1001 THEN MP_TAC(REAL_ARITH`abs ((b:(real^3->bool)->real) (h:real^3->bool)) * r1 < abs (b h) ==> abs (b h) * r1 / &2 < abs (b h)/ &2`)
1002 THEN RESA_TAC
1003 THEN MRESAL_TAC REAL_SUB_ABS[`(b:(real^3->bool)->real) (h:real^3->bool)`;`(b:(real^3->bool)->real) (h:real^3->bool) - (a:(real^3->bool)->real^3) (h:real^3->bool) dot y`;][REAL_ARITH`A- (A-B)=B`]
1004 THEN MP_TAC(REAL_ARITH`abs ((a:(real^3->bool)->real^3) (h:real^3->bool) dot y - b h) < r2 /\ r2 < abs ((b:(real^3->bool)->real) (h:real^3->bool)) / &2 /\ abs (b h) - abs (b h - a h dot y) <= abs (a h dot y)==> &0 <  abs (a h dot y ) /\ abs((b:(real^3->bool)->real) (h:real^3->bool))/ &2 < abs (a h dot y )`)
1005 THEN RESA_TAC
1006 THEN MRESA1_TAC REAL_ABS_NZ`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y`
1007 THEN MRESA1_TAC REAL_ABS_NZ`(b:(real^3->bool)->real) (h:real^3->bool) `
1008 THEN EXISTS_TAC`inv((a:(real^3->bool)->real^3) (h:real^3->bool) dot y) * (b:(real^3->bool)->real) (h:real^3->bool)`
1009 THEN ONCE_REWRITE_TAC[REAL_ARITH`(a * b)* c= (a * c) * b`]
1010 THEN MRESA1_TAC REAL_MUL_LINV`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y`
1011 THEN REWRITE_TAC[REAL_ARITH`&1 * a= a`]
1012 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1013 THEN REWRITE_TAC[REAL_ARITH`a * b - a * c= a*(b-c)`]
1014 THEN MP_TAC(REAL_ARITH`&0< abs((b:(real^3->bool)->real) (h:real^3->bool)) ==> &0< abs((b:(real^3->bool)->real) (h:real^3->bool))/ &2`)
1015 THEN RESA_TAC
1016 THEN MRESAL_TAC REAL_LT_INV2[`abs((b:(real^3->bool)->real) (h:real^3->bool)/ &2)`;`abs((a:(real^3->bool)->real^3) (h:real^3->bool) dot y)`][REAL_ARITH`abs(a/ &2)= abs a/ &2`]
1017 THEN REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV]
1018 THEN MRESAL_TAC REAL_LT_MUL2[`inv(abs((a:(real^3->bool)->real^3) (h:real^3->bool) dot y))`;`inv (abs ((b:(real^3->bool)->real) (h:real^3->bool)) / &2)`;`abs ((a:(real^3->bool)->real^3) (h:real^3->bool) dot y- (b:(real^3->bool)->real) (h:real^3->bool))`;`r2:real`][REAL_ABS_POS]
1019 THEN POP_ASSUM MP_TAC
1020 THEN REWRITE_TAC[GSYM REAL_ABS_INV;REAL_ABS_POS]
1021 THEN REWRITE_TAC[REAL_ABS_INV]
1022 THEN MP_TAC(REAL_ARITH`&0< abs((b:(real^3->bool)->real) (h:real^3->bool))/ &2 ==> ~(abs(b h)/ &2 = &0)`)
1023 THEN RESA_TAC
1024 THEN MRESA1_TAC REAL_MUL_LINV`abs((b:(real^3->bool)->real) (h:real^3->bool))/ &2`
1025 THEN EXPAND_TAC"r2"
1026 THEN REWRITE_TAC[REAL_ARITH`inv (abs (b h) / &2) * abs (b h) * r1 / &2= (inv (abs (b h) / &2) * (abs (b h)  / &2)) * r1`]
1027 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 * a= a`]
1028 THEN RESA_TAC
1029 THEN MP_TAC (REAL_ARITH`~((b:(real^3->bool)->real) (h:real^3->bool) = &0)==> &0< (b:(real^3->bool)->real) (h:real^3->bool) \/  &0< -- (b:(real^3->bool)->real) (h:real^3->bool)`)
1030 THEN RESA_TAC
1031
1032 THENL[
1033
1034 MRESA_TAC REAL_ABS_BETWEEN[`(b:(real^3->bool)->real) (h:real^3->bool)`;`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y`;`r2:real`]
1035 THEN MP_TAC(REAL_ARITH`r2 < abs ((b:(real^3->bool)->real) (h:real^3->bool)) / &2 /\ &0< b h /\ b h - r2 < a h dot y ==> &0 <  (a:(real^3->bool)->real^3) (h:real^3->bool) dot y`)
1036 THEN RESA_TAC
1037 THEN MRESA1_TAC REAL_LT_INV`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y`
1038 THEN MATCH_MP_TAC REAL_LT_MUL
1039 THEN ASM_REWRITE_TAC[];
1040
1041
1042 MRESA_TAC REAL_ABS_BETWEEN[`(b:(real^3->bool)->real) (h:real^3->bool)`;`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y`;`r2:real`]
1043 THEN MP_TAC(REAL_ARITH`r2 < abs ((b:(real^3->bool)->real) (h:real^3->bool)) / &2 /\ &0< --b h /\ a h dot y<  b h + r2  ==> &0 <  -- ((a:(real^3->bool)->real^3) (h:real^3->bool) dot y)`)
1044 THEN RESA_TAC
1045 THEN MRESAL1_TAC REAL_LT_INV`--((a:(real^3->bool)->real^3) (h:real^3->bool) dot y)`[REAL_INV_NEG]
1046 THEN MRESAL_TAC REAL_LT_MUL[`-- inv ((a:(real^3->bool)->real^3) (h:real^3->bool) dot y)`;`--((b:(real^3->bool)->real) (h:real^3->bool) )`][REAL_ARITH`-- a * -- b= a* b`]]; (*3*)
1047
1048 POP_ASSUM MP_TAC
1049 THEN DISCH_THEN(LABEL_TAC"LINH2")
1050 THEN ABBREV_TAC`r3= min (e:real / &12) (d/ &2)`
1051 THEN SUBGOAL_THEN `!y:real^3. norm(y- v1)< r3 ==> ?t1. &0< t1/\ t1 % y IN relative_interior (f:real^3->bool)  ` ASSUME_TAC
1052 THENL(*4*)[
1053
1054 REPEAT STRIP_TAC
1055 THEN MP_TAC(REAL_ARITH`&0< d /\ min (e / &12) (d / &2) = r3 /\ norm (y - (v1:real^3)) < r3 ==> norm (y - v1) < d`)
1056 THEN RESA_TAC
1057 THEN REMOVE_THEN "LINH2"(fun th-> MRESA1_TAC th `y:real^3`)
1058 THEN EXISTS_TAC `t1:real`
1059 THEN ASM_REWRITE_TAC[]
1060 THEN MATCH_MP_TAC (SET_RULE`!A B C x. A INTER B SUBSET C /\ x IN A /\ x IN B==> x IN C`)
1061 THEN EXISTS_TAC `ball(v1:real^3,e)`
1062 THEN EXISTS_TAC`{x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = (b:(real^3->bool)->real) (h:real^3->bool)}`
1063 THEN ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist]
1064 THEN MRESAL_TAC NORM_TRIANGLE[`(&1- t1) % v1:real^3`;`t1%(v1- y:real^3)`][VECTOR_ARITH`(&1 - t1) % v1 + t1 % (v1 - y)= v1- t1 % y`; NORM_MUL]
1065 THEN MRESA_TAC REAL_LT_RMUL [`abs(&1- t1:real)`;`r1:real`;`norm (v1:real^3)`]
1066 THEN MP_TAC (REAL_ARITH`&0< r1 /\ min (inv (norm (v1:real^3)) * e / &6) (&1) / &2 = r1 ==> r1 <= inv (norm v1) * e / &6/\ r1<= &1/ &2`)
1067 THEN RESA_TAC
1068 THEN MRESA_TAC REAL_LE_RMUL [`r1:real`;`(inv (norm( v1:real^3)) * e / &6)`;`norm (v1:real^3)`]
1069 THEN POP_ASSUM MP_TAC
1070 THEN ONCE_REWRITE_TAC[REAL_ARITH`(a * b/ &6) *c= (a * c) * b/ &6`]
1071 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 *A=A`]
1072 THEN STRIP_TAC
1073 THEN MP_TAC(REAL_ARITH`abs (&1 - t1) * norm v1 < r1 * norm (v1:real^3) /\
1074  r1 * norm v1<= e/ &6 ==> abs (&1 - t1) * norm v1 < e/ &6`)
1075 THEN RESA_TAC
1076 THEN MRESA_TAC REAL_ABS_BETWEEN[`t1:real`;`&1`;`r1:real`]
1077 THEN MP_TAC(REAL_ARITH`t1- r1< &1 /\  r1<= &1/ &2 ==> t1< &2`)
1078 THEN ASM_REWRITE_TAC[]
1079 THEN STRIP_TAC
1080 THEN MP_TAC(REAL_ARITH`&0< t1==> &0<= t1`)
1081 THEN RESA_TAC
1082 THEN MRESAL_TAC REAL_LT_MUL2[`t1:real`;`&2`;`norm(y- v1:real^3)`;`r3:real`][NORM_POS_LE; NORM_SUB]
1083 THEN MP_TAC(REAL_ARITH`min (e / &12) (d / &2) = r3 /\ &0< e /\ &0< d ==> &2 * r3<=  e/ &6 `)
1084 THEN RESA_TAC
1085 THEN MP_TAC(REAL_ARITH`t1 * norm (v1 - y:real^3) < &2 * r3 /\ &2 * r3<= e/ &6 ==> t1 * norm (v1 - y) < e/ &6 `)
1086 THEN RESA_TAC
1087 THEN MRESA1_TAC REAL_ABS_REFL`t1:real`
1088 THEN MRESA_TAC REAL_LT_ADD2[`abs (&1 - t1) * norm (v1:real^3)`;`e/ &6`;`abs t1 * norm (v1 - y:real^3)`;`e/ &6`;]
1089 THEN MP_TAC(REAL_ARITH`  abs (&1 - t1) * norm v1 + abs t1 * norm (v1 - y) < e/ &6 + e/ &6 /\ &0< e
1090 /\ norm (v1 - t1 % y) <= abs (&1 - t1) * norm v1 + abs t1 * norm (v1 - y) ==> norm (v1 - t1 % y:real^3) < e`)
1091 THEN ASM_REWRITE_TAC[];
1092
1093
1094 POP_ASSUM MP_TAC
1095 THEN DISCH_THEN(LABEL_TAC"LINH3")
1096 THEN EXISTS_TAC`t * r3:real`
1097 THEN MP_TAC(REAL_ARITH`&0< e /\ &0< d==> &0< min (e / &12) (d / &2)`)
1098 THEN RESA_TAC
1099 THEN STRIP_TAC
1100 THENL(*5*)[
1101 MATCH_MP_TAC REAL_LT_MUL
1102 THEN ASM_REWRITE_TAC[]
1103 THEN ONCE_REWRITE_TAC[REAL_ARITH`&0< t<=> t> &0`]
1104 THEN ASM_REWRITE_TAC[];
1105 REPEAT STRIP_TAC
1106 THEN REWRITE_TAC[fchanged;IN_ELIM_THM]
1107 THEN MP_TAC(REAL_ARITH`t > &0 ==>  &0< t /\ ~(t= &0) /\ &0<= t`)
1108 THEN RESA_TAC
1109 THEN MRESA1_TAC REAL_LT_INV`t:real`
1110 THEN MRESA1_TAC REAL_LE_INV`t:real`
1111 THEN MRESA1_TAC REAL_MUL_LINV`t:real`
1112 THEN MRESA1_TAC REAL_ABS_REFL`inv t:real`
1113 THEN MRESAL_TAC NORM_MUL[`inv t:real`;`x' - t % v1:real^3`][VECTOR_ARITH`inv t % (x' - t % v1)=inv t % x' -(inv t * t) % v1 /\ &1 %a=a`]
1114 THEN MRESAL_TAC REAL_LT_LMUL[`inv (t:real)`;`norm (x' - t % v1:real^3)`;`t * r3:real`][REAL_ARITH`A *B *C= (A* B) *C/\ &1 *A=A`]
1115 THEN POP_ASSUM MP_TAC
1116 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1117 THEN STRIP_TAC
1118 THEN REMOVE_THEN "LINH3"(fun th-> MRESAL1_TAC th `(inv t) % (x':real^3)`[VECTOR_ARITH`a %b % v= (a * b)%v`])
1119 THEN MRESA_TAC REAL_LT_MUL[`t1:real`;`inv t:real`]
1120 THEN MRESA1_TAC REAL_LT_INV`t1 * inv t:real`
1121 THEN EXISTS_TAC`(t1 * inv t) % x':real^3`
1122 THEN EXISTS_TAC`inv(t1 * inv t) :real`
1123 THEN ASM_REWRITE_TAC[REAL_ARITH`t> &0 <=> &0 < t`;VECTOR_ARITH`a %b % v= (a * b)%v`]
1124 THEN MP_TAC(REAL_ARITH`&0 < t1 * inv t==> ~(t1 * inv t= &0)`)
1125 THEN RESA_TAC
1126 THEN MRESA1_TAC REAL_MUL_LINV`t1 * inv t:real`
1127 THEN VECTOR_ARITH_TAC]]]]]);;
1128
1129
1130
1131
1132 let FCHANGED_ONE_TO_ONE=prove(`!p f1 f2:real^3->bool.
1133          bounded p /\ polyhedron p /\ vec 0 IN interior p /\ f1 facet_of p
1134  /\ f2 facet_of p /\  ~(fchanged f1 INTER fchanged f2= {})
1135 ==> f1=f2`,
1136
1137 REWRITE_TAC[SET_RULE`~(A= {})<=> ?y. y IN A`; fchanged;INTER;IN_ELIM_THM]
1138 THEN REPEAT STRIP_TAC
1139 THEN POP_ASSUM MP_TAC
1140 THEN POP_ASSUM MP_TAC
1141 THEN POP_ASSUM MP_TAC
1142 THEN ASM_REWRITE_TAC[]
1143 THEN DISCH_THEN(LABEL_TAC"LINH1")
1144 THEN REPEAT STRIP_TAC
1145 THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f1:real^3->bool`
1146 THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f2:real^3->bool`
1147 THEN MP_TAC(SET_RULE`v1 IN relative_interior f1 /\ v1' IN relative_interior f2 /\ relative_interior f2 SUBSET f2 /\ relative_interior f1 SUBSET f1
1148 ==> v1 IN (f1:real^3->bool) /\ v1' IN (f2:real^3->bool)`)
1149 THEN RESA_TAC
1150 THEN FIND_ASSUM(MP_TAC)`f1 facet_of (p:real^3->bool)`
1151 THEN FIND_ASSUM(MP_TAC)`f2 facet_of (p:real^3->bool)`
1152 THEN REWRITE_TAC[facet_of]
1153 THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
1154 THEN DISJ_CASES_TAC(SET_RULE`f1= p \/ ~(f1= p:real^3->bool)`)
1155 THENL[
1156 ASM_REWRITE_TAC[]
1157 THEN ARITH_TAC;
1158 DISJ_CASES_TAC(SET_RULE`f2= p \/ ~(f2= p:real^3->bool)`)
1159 THENL[
1160
1161 ASM_REWRITE_TAC[]
1162 THEN ARITH_TAC;
1163 REPEAT STRIP_TAC
1164 THEN MRESA_TAC POLYHEDRON_COLLINEAR_FACES[`p:real^3->bool`;`f1:real^3->bool`;`f2:real^3->bool`;`v1:real^3`;`v1':real^3`;`t:real`;`t':real`]
1165 THEN REMOVE_THEN "LINH1" MP_TAC
1166 THEN RESA_TAC
1167 THEN MP_TAC(SET_RULE`t' % v1 = t' % v1'==> inv t' % (t' % v1) = inv t' % (t' % v1':real^3)`)
1168 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
1169 THEN REWRITE_TAC[VECTOR_ARITH`A%B%v=(A*B)%v`]
1170 THEN MP_TAC(REAL_ARITH`t'> &0 ==> ~(t'= &0)`)
1171 THEN RESA_TAC
1172 THEN MRESA1_TAC REAL_MUL_LINV`t':real`
1173 THEN REWRITE_TAC[VECTOR_ARITH`&1 %A=A`]
1174 THEN STRIP_TAC
1175 THEN MATCH_MP_TAC FACE_OF_EQ
1176 THEN EXISTS_TAC`p:real^3->bool`
1177 THEN ASM_REWRITE_TAC[DISJOINT;SET_RULE`~(A= {})<=> ?y. y IN A`;INTER;IN_ELIM_THM]
1178 THEN EXISTS_TAC `v1:real^3`
1179 THEN ASM_REWRITE_TAC[]]]);;
1180
1181
1182
1183
1184 let CARD_EXISTS_2=prove(`!e:A->bool.
1185  FINITE e /\ CARD e=2
1186 ==> ?v:A w:A. e={v,w}`,
1187
1188 REPEAT GEN_TAC
1189 THEN STRIP_TAC
1190 THEN SUBGOAL_THEN `~((e:A->bool)={})` ASSUME_TAC
1191 THENL[
1192 STRIP_TAC
1193 THEN MP_TAC(ISPEC`(e:A->bool)`CARD_EQ_0)
1194 THEN RESA_TAC
1195 THEN POP_ASSUM MP_TAC
1196 THEN ARITH_TAC;
1197 MP_TAC(SET_RULE `~((e:A->bool)={})==> ?v:A. v IN e`)
1198 THEN RESA_TAC
1199 THEN SUBGOAL_THEN`~((e:A->bool) DELETE v={})` ASSUME_TAC
1200 THENL[
1201 STRIP_TAC
1202 THEN MP_TAC(ISPECL[`v:A`;`(e:A->bool)`;]CARD_DELETE)
1203 THEN RESA_TAC
1204 THEN MP_TAC(ISPECL[`(e:A->bool)`;`v:A`] FINITE_DELETE)
1205 THEN RESA_TAC
1206 THEN MP_TAC(ISPEC`(e:A->bool) DELETE v`CARD_EQ_0)
1207 THEN RESA_TAC
1208 THEN POP_ASSUM MP_TAC
1209 THEN ARITH_TAC;
1210 MP_TAC(SET_RULE `~((e:A->bool)DELETE v={})==> ?w:A. w IN (e:A->bool)DELETE v/\ w IN e`)
1211 THEN RESA_TAC
1212 THEN MP_TAC(SET_RULE `(v IN (e:A->bool))/\ (w IN (e:A->bool))==> {v,w} SUBSET e`)
1213 THEN RESA_TAC
1214 THEN MP_TAC(SET_RULE `(w IN (e:A->bool)DELETE v)==> ~(v=w)`)
1215 THEN RESA_TAC
1216 THEN MP_TAC(ISPECL [`{v:A,w:A}`;`(e:(A->bool))`] FINITE_SUBSET)
1217 THEN RESA_TAC
1218 THEN ASSUME_TAC(SET_RULE `v:A IN {v:A,w:A} `)
1219 THEN MP_TAC(ISPECL[`v:A`;`{v:A,w:A}`;]CARD_DELETE)
1220 THEN RESA_TAC
1221 THEN MP_TAC(SET_RULE `v IN {v,w}==>{v:A,w:A} DELETE v PSUBSET {v,w}`)
1222 THEN RESA_TAC
1223 THEN MP_TAC(ISPECL[`{v:A,w:A} DELETE v`;`{v:A,w:A}`]CARD_PSUBSET)
1224 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
1225 THEN FIND_ASSUM MP_TAC`FINITE {v:A,w:A}`
1226 THEN DISCH_TAC
1227 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
1228 THEN DISCH_TAC
1229 THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v) < CARD {v, w}/\ CARD ({v, w} DELETE v) = CARD {v, w}-1
1230 <=>CARD ({v, w} DELETE v) +1= CARD {v:A, w:A}`)
1231 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
1232 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
1233 THEN REWRITE_TAC[ARITH_RULE`A=A`]
1234 THEN DISCH_TAC
1235 THEN SUBGOAL_THEN `w:A IN ({v:A,w:A} DELETE v)` ASSUME_TAC
1236 THENL[
1237 ASM_SET_TAC[];
1238 MP_TAC(ISPECL[`{v:A,w:A}`;`v:A`] FINITE_DELETE)
1239 THEN RESA_TAC
1240 THEN MP_TAC(ISPECL[`w:A`;`{v:A,w:A} DELETE v`;]CARD_DELETE)
1241 THEN RESA_TAC
1242 THEN MP_TAC(SET_RULE `w IN ({v,w} DELETE v)==>{v:A,w:A} DELETE v DELETE w PSUBSET {v,w} DELETE v`)
1243 THEN RESA_TAC
1244 THEN MP_TAC(ISPECL[`{v:A,w:A} DELETE v DELETE w`;`{v:A,w:A} DELETE v`]CARD_PSUBSET)
1245 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
1246 THEN FIND_ASSUM MP_TAC`FINITE ({v:A,w:A} DELETE v)`
1247 THEN DISCH_TAC
1248 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
1249 THEN DISCH_TAC
1250 THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v DELETE w) < CARD ({v, w} DELETE v)/\ CARD ({v, w} DELETE v DELETE w) = CARD ({v, w} DELETE v)-1
1251 <=>CARD ({v, w} DELETE v DELETE w) +1= CARD ({v:A, w:A} DELETE v)`)
1252 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
1253 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
1254 THEN REWRITE_TAC[ARITH_RULE`A=A`]
1255 THEN DISCH_TAC
1256 THEN POP_ASSUM MP_TAC
1257 THEN POP_ASSUM (fun th->REWRITE_TAC[])
1258 THEN POP_ASSUM (fun th->REWRITE_TAC[])
1259 THEN ASSUME_TAC(SET_RULE `{v, w} DELETE v:A DELETE w:A={}`)
1260 THEN POP_ASSUM (fun th->REWRITE_TAC[th;CARD_CLAUSES; ARITH_RULE `0+1=1`])
1261 THEN POP_ASSUM MP_TAC
1262 THEN DISCH_THEN(LABEL_TAC"B")
1263 THEN DISCH_TAC
1264 THEN REMOVE_THEN "B" MP_TAC
1265 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th);ARITH_RULE` 1+1=2`])
1266 THEN FIND_ASSUM MP_TAC`CARD (e:A->bool)=2`
1267 THEN DISCH_TAC
1268 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
1269 THEN DISCH_TAC
1270 THEN MP_TAC(ISPECL[`{v:A,w:A}`;`e:A->bool`]CARD_SUBSET_EQ)
1271 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
1272 THEN RESA_TAC
1273 THEN EXISTS_TAC`v:A`
1274 THEN EXISTS_TAC`w:A`
1275 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])]]]);;
1276
1277
1278 let EXISTS_EDGE_POLYTOPE=prove(`!p:real^3->bool.
1279          bounded p /\ polyhedron p /\ vec 0 IN interior p
1280 ==> ?e. e IN edges p`,
1281
1282 REPEAT STRIP_TAC
1283 THEN REWRITE_TAC[edges;IN_ELIM_THM]
1284 THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
1285 THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
1286 THEN MRESAL1_TAC POLYTOPE_FACET_EXISTS`p:real^3->bool`[ARITH_RULE`&0:int < &3`; facet_of; ARITH_RULE`&3- &1= &2:int`]
1287 THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^3->bool`;`p:real^3->bool`]
1288 THEN MRESAL1_TAC POLYTOPE_FACET_EXISTS`f:real^3->bool`[ARITH_RULE`&0:int < &2`; facet_of; ARITH_RULE`&2- &1= &1:int`]
1289 THEN MRESA1_TAC AFF_DIM`f':real^3->bool`
1290 THEN POP_ASSUM MP_TAC
1291 THEN REWRITE_TAC[ARITH_RULE`&1=A - &1:int <=> A= &2`;INT_OF_NUM_EQ]
1292 THEN STRIP_TAC
1293 THEN MRESA1_TAC AFFINE_INDEPENDENT_IMP_FINITE`b:real^3->bool`
1294 THEN MRESA1_TAC CARD_EXISTS_2`b:real^3->bool`
1295 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1296 THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f':real^3->bool`;`f:real^3->bool`]
1297 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`f':real^3->bool`
1298 THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`f':real^3->bool`
1299 THEN SUBGOAL_THEN`?u v. f' SUBSET affine hull {u,v:real^3}` ASSUME_TAC
1300 THENL[
1301  EXISTS_TAC`v:real^3`
1302 THEN EXISTS_TAC`w:real^3`
1303 THEN ASM_REWRITE_TAC[HULL_SUBSET];
1304  MRESAL1_TAC COMPACT_CONVEX_COLLINEAR_SEGMENT`f':real^3->bool`[COLLINEAR_AFFINE_HULL]
1305 THEN MRESA_TAC FACE_OF_TRANS[`f':real^3->bool`;`f:real^3->bool`;`p:real^3->bool`]
1306 THEN EXISTS_TAC`{a,b:real^3}`
1307 THEN EXISTS_TAC`a:real^3`
1308 THEN EXISTS_TAC`b:real^3`
1309 THEN ASM_REWRITE_TAC[edge_of]
1310 THEN REMOVE_ASSUM_TAC
1311 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])]);;
1312
1313
1314
1315 let EXISTS_EDGE_POLYTOPE1=prove(`!p:real^3->bool.
1316          bounded p /\ polyhedron p /\ vec 0 IN interior p
1317 ==> ~(edges p= {})`,
1318 REWRITE_TAC[SET_RULE`~(A= {})<=> ?x. x IN A`;EXISTS_EDGE_POLYTOPE]);;
1319
1320
1321
1322
1323 let REDUCE_POINT_FACET=prove(`!x p:real^3->bool.
1324          bounded p /\ polyhedron p /\ vec 0 IN interior p
1325 /\ x IN yfan(vec 0,vertices p,edges p)
1326 ==> ?f t.  &0< t /\  f facet_of p /\ t % x IN f `,
1327
1328
1329 REPEAT STRIP_TAC
1330 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1331 THEN MRESA1_TAC EXISTS_EDGE_POLYTOPE1`p:real^3->bool`
1332 THEN MRESA_TAC x_in_xfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
1333 THEN SUBGOAL_THEN`~(x= vec 0:real^3)`ASSUME_TAC
1334 THENL[
1335 ASM_TAC
1336 THEN REWRITE_TAC[yfan; DIFF;IN_ELIM_THM]
1337 THEN SET_TAC[];
1338 MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
1339 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool`
1340 THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
1341 THEN MP_TAC(SET_RULE`interior p SUBSET p /\ vec 0 IN interior p ==> vec 0 IN (p:real^3->bool)`)
1342 THEN RESA_TAC
1343 THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`]
1344 THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool`
1345 THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool`
1346 THEN MRESA1_TAC COMPACT_IMP_CLOSED`p:real^3->bool`
1347 THEN MRESA1_TAC CLOSURE_CLOSED`p:real^3->bool`
1348 THEN MRESAL_TAC COMPACT_FRONTIER_LINE_LEMMA[`p:real^3->bool`;`x:real^3`][frontier;UNIONS;IN_ELIM_THM]
1349 THEN EXISTS_TAC`u':real^3->bool`
1350 THEN EXISTS_TAC`u:real`
1351 THEN ASM_REWRITE_TAC[]
1352 THEN MP_TAC(REAL_ARITH`&0<= u==> u= &0 \/ &0< u`)
1353 THEN RESA_TAC
1354 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; VECTOR_ARITH`&0 % v= vec 0:real^3`] THEN REPEAT STRIP_TAC)
1355 THEN ASM_TAC THEN SET_TAC[]]);;
1356
1357
1358
1359 let aff_ge_1_1_subset_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y:real^3.
1360 FAN(x,V,E)
1361 /\ y IN xfan(x,V,E) /\ ~(x=y)
1362 ==>  aff_ge {x} {y} SUBSET xfan(x,V,E)`,
1363
1364 REWRITE_TAC[xfan;IN_ELIM_THM;SUBSET]
1365 THEN REPEAT STRIP_TAC
1366 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`]
1367 THEN POP_ASSUM MP_TAC
1368 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[IN]
1369 THEN RESA_TAC
1370 THEN EXISTS_TAC`e:real^3->bool`
1371 THEN ASM_REWRITE_TAC[]
1372 THEN MRESA_TAC aff_ge_1_1_subset_aff_ge_fan[`x:real^3`;`v:real^3`;`w:real^3`;`y:real^3`]
1373 THEN POP_ASSUM MP_TAC
1374 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC(th))
1375 THEN ASM_REWRITE_TAC[]
1376 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
1377 ` (v:real^3)`]
1378 THEN POP_ASSUM MP_TAC
1379 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
1380 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[IN]THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC(th))
1381 THEN STRIP_TAC
1382 THEN ASM_REWRITE_TAC[]
1383 THEN ASM_TAC THEN SET_TAC[]);;
1384
1385
1386 let YFAN_SUBSET_UNIONS_FCHANGED=prove(`!y p:real^3->bool.
1387          bounded p /\ polyhedron p /\ vec 0 IN interior p
1388 /\ y IN yfan(vec 0,vertices p,edges p)
1389 ==> y IN UNIONS {fchanged f| f facet_of p}`,
1390
1391 REPEAT STRIP_TAC
1392 THEN ASM_REWRITE_TAC[UNIONS;IN_ELIM_THM]
1393 THEN MRESA_TAC REDUCE_POINT_FACET[`y:real^3`;`p:real^3->bool`]
1394 THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`f:real^3->bool`;`p:real^3->bool`]
1395 THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
1396 THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`f:real^3->bool`
1397 THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool`
1398 THEN MP_TAC(SET_RULE`t % y IN f ==> t % y IN relative_interior f \/ t % (y:real^3) IN f DIFF relative_interior f `)
1399 THEN RESA_TAC
1400 THENL[
1401 EXISTS_TAC`fchanged (f:real^3->bool)`
1402 THEN STRIP_TAC
1403 THENL[
1404 EXISTS_TAC`f:real^3->bool`
1405 THEN ASM_REWRITE_TAC[];
1406
1407 ASM_REWRITE_TAC[fchanged;IN_ELIM_THM]
1408 THEN EXISTS_TAC`t % y:real^3`
1409 THEN EXISTS_TAC`inv t :real`
1410 THEN MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`)
1411 THEN RESA_TAC
1412 THEN MRESA1_TAC REAL_MUL_LINV`t:real`
1413 THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % b % v= (a* b)% v/\ &1 % w= w`;]
1414 THEN ONCE_REWRITE_TAC[REAL_ARITH`t> &0<=> &0< t`]
1415 THEN MATCH_MP_TAC REAL_LT_INV
1416 THEN ASM_REWRITE_TAC[]];
1417
1418 POP_ASSUM MP_TAC
1419 THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
1420 THEN FIND_ASSUM MP_TAC`f facet_of p:real^3->bool`
1421 THEN REWRITE_TAC[UNIONS;IN_ELIM_THM; facet_of]
1422 THEN ASM_REWRITE_TAC[ARITH_RULE`&3- &1= &2:int`]
1423 THEN RESA_TAC
1424 THEN ASM_REWRITE_TAC[ARITH_RULE`&2- &1= &1:int`]
1425 THEN RESA_TAC
1426 THEN MRESA1_TAC AFF_DIM`u:real^3->bool`
1427 THEN POP_ASSUM MP_TAC
1428 THEN REWRITE_TAC[ARITH_RULE`&1=A - &1:int <=> A= &2`;INT_OF_NUM_EQ]
1429 THEN STRIP_TAC
1430 THEN MRESA1_TAC AFFINE_INDEPENDENT_IMP_FINITE`b:real^3->bool`
1431 THEN MRESA1_TAC CARD_EXISTS_2`b:real^3->bool`
1432 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1433 THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
1434 THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^3->bool`;`p:real^3->bool`]
1435 THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`u:real^3->bool`;`f:real^3->bool`]
1436 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`u:real^3->bool`
1437 THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`u:real^3->bool`
1438 THEN SUBGOAL_THEN`?u1 v. u SUBSET affine hull {u1,v:real^3}` ASSUME_TAC
1439 THENL[
1440  EXISTS_TAC`v:real^3`
1441 THEN EXISTS_TAC`w:real^3`
1442 THEN ASM_REWRITE_TAC[HULL_SUBSET];
1443  MRESAL1_TAC COMPACT_CONVEX_COLLINEAR_SEGMENT`u:real^3->bool`[COLLINEAR_AFFINE_HULL]
1444 THEN MRESA_TAC FACE_OF_TRANS[`u:real^3->bool`;`f:real^3->bool`;`p:real^3->bool`]
1445 THEN SUBGOAL_THEN `{a,b} IN edges (p:real^3->bool)`ASSUME_TAC
1446 THENL[
1447 REWRITE_TAC[edges;edge_of;IN_ELIM_THM]
1448 THEN EXISTS_TAC`a:real^3`
1449 THEN EXISTS_TAC`b:real^3`
1450 THEN ASM_REWRITE_TAC[]
1451 THEN REMOVE_ASSUM_TAC
1452 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) ;
1453
1454 MRESA_TAC AFF_GE_SUBSET_XFAN[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`a:real^3`;`b:real^3`]
1455 THEN MRESAL_TAC CONVEX_AFF_GE[`{vec 0:real^3}`;`{a,b:real^3}`][GSYM CONVEX_HULL_EQ]
1456 THEN MRESA_TAC SEGMENT_CONVEX_HULL[`a:real^3`;`b:real^3`]
1457 THEN POP_ASSUM (fun th-> MP_TAC(SYM th) THEN STRIP_TAC)
1458 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1459 THEN POP_ASSUM MP_TAC
1460 THEN REWRITE_TAC[FAN; fan6]
1461 THEN STRIP_TAC
1462 THEN REMOVE_ASSUM_TAC
1463 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`{a,b:real^3}`[SET_RULE`{x} UNION {a,b}={x,a,b}`])
1464 THEN MRESA_TAC point_in_aff_ge[`vec 0:real^3`;`a:real^3`;`b:real^3`]
1465 THEN MP_TAC(SET_RULE`a IN aff_ge {vec 0} {a, b} /\ b IN aff_ge {vec 0} {a, b}
1466 ==> {a,b:real^3} SUBSET  aff_ge {vec 0} {a, b}`)
1467 THEN RESA_TAC
1468 THEN MRESA_TAC HULL_MONO[`convex:(real^3->bool)->bool`;`{a,b:real^3}`;`aff_ge {vec 0} {a, b:real^3}`]
1469 THEN MP_TAC(SET_RULE`segment [a,b] SUBSET aff_ge {vec 0} {a, b}
1470 /\ aff_ge {vec 0} {a, b} SUBSET xfan (vec 0,vertices p,edges p)
1471 /\ u = segment [a,b] /\ t % y IN u
1472 ==>  t % y IN xfan (vec 0,vertices p,edges (p:real^3->bool))`)
1473 THEN ASM_REWRITE_TAC[]
1474 THEN STRIP_TAC
1475 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1476 THEN DISJ_CASES_TAC(SET_RULE`(vec 0 = t % y:real^3) \/ ~(vec 0 = t % y) `)
1477 THENL[
1478 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC)
1479 THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`]
1480 THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool`
1481 THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool`
1482 THEN MP_TAC (SET_RULE`vec 0 IN interior (p:real^3->bool)
1483 /\ p DIFF interior p = UNIONS {f | f facet_of p}
1484 ==> ~(vec 0 IN UNIONS {f | f facet_of p})`)
1485 THEN ASM_REWRITE_TAC[UNIONS;IN_ELIM_THM]
1486 THEN ASM_TAC
1487 THEN SET_TAC[];
1488
1489 MRESA_TAC aff_ge_1_1_subset_xfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`t % y:real^3`]
1490 THEN SUBGOAL_THEN`y IN aff_ge {vec 0} {t % y:real^3}`ASSUME_TAC
1491 THENL[
1492 MRESAL_TAC AFF_GE_1_1[`vec 0:real^3`;`t % y:real^3`][IN_ELIM_THM]
1493 THEN EXISTS_TAC`&1- inv t:real`
1494 THEN EXISTS_TAC`inv t`
1495 THEN MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`)
1496 THEN RESA_TAC
1497 THEN MRESA1_TAC REAL_MUL_LINV`t:real`
1498 THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % b % v= (a* b)% v/\ &1 % w= w/\ y = (&1 - inv t) % vec 0 + y`; REAL_ARITH`&1 - a+ a= &1`;REAL_LE_INV_EQ]
1499 THEN ASM_TAC THEN REAL_ARITH_TAC;
1500
1501 ASM_TAC
1502 THEN REWRITE_TAC[yfan; DIFF; IN_ELIM_THM]
1503 THEN SET_TAC[]]]]]]);;
1504
1505 let in_aff_ge_fan=prove(`!x:real^3 v:real^3 u:real^3 a:real.
1506 DISJOINT {x} {v,u}
1507 /\ &0<=a /\ a<= &1
1508 ==>
1509 (&1-a)%v + a % u IN aff_ge {x} {v,u:real^3}`,
1510
1511 REPEAT STRIP_TAC
1512 THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM]
1513 THEN EXISTS_TAC`&0`
1514 THEN EXISTS_TAC`&1 -a:real`
1515 THEN EXISTS_TAC`a:real`
1516 THEN MP_TAC(REAL_ARITH`&0<= a /\ a  <= &1 ==> &0 <= &1 - a /\ &0 <= a`)
1517 THEN RESA_TAC
1518 THEN ASM_REWRITE_TAC[]
1519 THEN REDUCE_VECTOR_TAC
1520 THEN REAL_ARITH_TAC);;
1521
1522
1523
1524 let REDUCE_POINT_FACET_EXISTS=prove(`!x p:real^3->bool.
1525          bounded p /\ polyhedron p /\ vec 0 IN interior p
1526 /\ ~(x= vec 0)
1527 ==> ?f t.  &0< t /\  f facet_of p /\ t % x IN f `,
1528
1529
1530 REPEAT STRIP_TAC
1531 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1532 THEN MRESA1_TAC EXISTS_EDGE_POLYTOPE1`p:real^3->bool`
1533 THEN MRESA_TAC x_in_xfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
1534 THEN SUBGOAL_THEN`~(x= vec 0:real^3)`ASSUME_TAC
1535 THENL[
1536 ASM_TAC
1537 THEN REWRITE_TAC[yfan; DIFF;IN_ELIM_THM]
1538 THEN SET_TAC[];
1539 MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
1540 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool`
1541 THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
1542 THEN MP_TAC(SET_RULE`interior p SUBSET p /\ vec 0 IN interior p ==> vec 0 IN (p:real^3->bool)`)
1543 THEN RESA_TAC
1544 THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`]
1545 THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool`
1546 THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool`
1547 THEN MRESA1_TAC COMPACT_IMP_CLOSED`p:real^3->bool`
1548 THEN MRESA1_TAC CLOSURE_CLOSED`p:real^3->bool`
1549 THEN MRESAL_TAC COMPACT_FRONTIER_LINE_LEMMA[`p:real^3->bool`;`x:real^3`][frontier;UNIONS;IN_ELIM_THM]
1550 THEN EXISTS_TAC`u':real^3->bool`
1551 THEN EXISTS_TAC`u:real`
1552 THEN ASM_REWRITE_TAC[]
1553 THEN MP_TAC(REAL_ARITH`&0<= u==> u= &0 \/ &0< u`)
1554 THEN RESA_TAC
1555 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; VECTOR_ARITH`&0 % v= vec 0:real^3`] THEN REPEAT STRIP_TAC)
1556 THEN ASM_TAC THEN SET_TAC[]]);;
1557
1558
1559
1560
1561
1562
1563
1564 let FCHANGED_SUBSET_YFAN=prove(`!x p:real^3->bool.
1565          bounded p /\ polyhedron p /\ vec 0 IN interior p
1566 /\ x IN UNIONS {fchanged f| f facet_of p}
1567 ==> x IN yfan(vec 0,vertices p,edges p)`,
1568
1569 REWRITE_TAC[UNIONS;IN_ELIM_THM]
1570 THEN REPEAT STRIP_TAC
1571 THEN POP_ASSUM MP_TAC
1572 THEN ASM_REWRITE_TAC[fchanged;IN_ELIM_THM;yfan;DIFF;SET_RULE`x:real^3 IN (:real^3)`;XFAN_EQ_UNIONS_AFF_GE_1_2;UNIONS;]
1573 THEN REPEAT STRIP_TAC
1574 THEN POP_ASSUM MP_TAC
1575 THEN POP_ASSUM MP_TAC
1576 THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[edges;edge_of;IN_ELIM_THM]  THEN STRIP_TAC THEN MP_TAC th THEN RESA_TAC)
1577 THEN RESA_TAC
1578 THEN RESA_TAC
1579 THEN SUBGOAL_THEN`?t1.  &0< t1 /\ t1 % x IN  segment[v,w:real^3]`ASSUME_TAC
1580 THENL[
1581 POP_ASSUM MP_TAC
1582 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1583 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`;
1584 ` (v:real^3)`]
1585 THEN MRESAL_TAC  AFF_GE_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;VECTOR_ARITH`t% vec 0+A+B=A+B`;]
1586 THEN RESA_TAC
1587 THEN EXISTS_TAC`inv (t2+ t3)`
1588 THEN REWRITE_TAC[segment;IN_ELIM_THM;VECTOR_ARITH`a%(b % v+ c % w)=(a*b)%v+(a* c)%w`]
1589 THEN MP_TAC(REAL_ARITH`&0<= t2/\ &0<= t3:real ==> (t2= &0 /\ t3= &0)\/ &0< t2+t3`)
1590 THEN RESA_TAC
1591 THENL[
1592 POP_ASSUM (fun th -> POP_ASSUM (fun th1 -> POP_ASSUM MP_TAC THEN REWRITE_TAC[th; th1; VECTOR_ARITH`&0 % v= vec 0/\  vec 0 + vec 0= vec 0`;VECTOR_MUL_EQ_0]))
1593 THEN MP_TAC(REAL_ARITH`t> &0 ==> ~(t= &0)`)
1594 THEN RESA_TAC
1595 THEN STRIP_TAC
1596 THEN POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1597 THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool`
1598 THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`]
1599 THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool`
1600 THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool`
1601 THEN MP_TAC (SET_RULE`vec 0 IN interior (p:real^3->bool)
1602 /\ p DIFF interior p = UNIONS {f | f facet_of p}
1603 ==> ~(vec 0 IN UNIONS {f | f facet_of p})`)
1604 THEN ASM_REWRITE_TAC[UNIONS;IN_ELIM_THM]
1605 THEN ASM_TAC
1606 THEN SET_TAC[];
1607
1608 MRESA1_TAC REAL_LT_INV`t2+t3:real`
1609 THEN MP_TAC(REAL_ARITH`&0< inv(t2+t3)/\ &0< t2+t3==> &0<= inv(t2+t3:real) /\ ~(t2+ t3= &0) `)
1610 THEN RESA_TAC
1611 THEN MRESA_TAC REAL_LE_MUL[`inv(t2+ t3):real`;`t2:real`]
1612 THEN MRESA_TAC REAL_LE_MUL[`inv(t2+ t3):real`;`t3:real`]
1613 THEN MRESAL1_TAC REAL_MUL_LINV`t2+ t3:real`[REAL_ARITH`c*(a+b)=c*a+ c*b`]
1614 THEN EXISTS_TAC`inv(t2+t3) * t3`
1615 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; REAL_ARITH`(a+b)-b=a`])
1616 THEN POP_ASSUM MP_TAC
1617 THEN POP_ASSUM MP_TAC
1618 THEN REAL_ARITH_TAC];
1619
1620 POP_ASSUM MP_TAC
1621 THEN RESA_TAC
1622 THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
1623 THEN FIND_ASSUM MP_TAC`f facet_of (p:real^3->bool)`
1624 THEN REWRITE_TAC[facet_of; ]
1625 THEN DISJ_CASES_TAC(SET_RULE`f= p\/ ~(f=p:real^3->bool)`)
1626 THENL[
1627 ASM_REWRITE_TAC[]
1628 THEN ARITH_TAC;
1629
1630 RESA_TAC
1631 THEN DISJ_CASES_TAC(SET_RULE`segment [v,w]= p\/ ~(segment [v,w]=p:real^3->bool)`)
1632 THENL[
1633 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] )
1634 THEN ARITH_TAC;
1635
1636 MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool`
1637 THEN MP_TAC(SET_RULE`v1 IN relative_interior (f:real^3->bool) /\ relative_interior f SUBSET f ==> v1 IN f`)
1638 THEN RESA_TAC
1639 THEN MRESAL_TAC REAL_LT_MUL[`t:real`;`t1:real`][REAL_ARITH`&0< t<=> t> &0`]
1640 THEN MRESAL_TAC POLYHEDRON_COLLINEAR_FACES[`p:real^3->bool`;`f:real^3->bool`;`segment[v,w]:real^3->bool`;`v1:real^3`;`t1% x:real^3`;`t * t1:real`;`&1:real`][VECTOR_ARITH`(t * t1) % v1 = &1 % t1 % t % v1`;REAL_ARITH`&1> &0`]
1641 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th; VECTOR_ARITH`a%b % v= (b*a)%v/\ &1 %v=v`] THEN REPEAT STRIP_TAC)
1642 THEN MRESA_TAC SEGMENT_CLOSED_OPEN[`v:real^3`;`w:real^3`]
1643 THEN MP_TAC(SET_RULE`segment [v,w] = segment (v,w) UNION {v, w}
1644 /\ v1 IN segment [v,w] ==> v1 IN segment (v,w:real^3) \/ v1=v \/ v1= w`)
1645 THEN RESA_TAC
1646 THENL[
1647 POP_ASSUM MP_TAC
1648 THEN REMOVE_ASSUM_TAC
1649 THEN STRIP_TAC
1650 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1651 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`;
1652 ` (v:real^3)`]
1653 THEN REMOVE_ASSUM_TAC
1654 THEN POP_ASSUM MP_TAC
1655 THEN MP_TAC(SET_RULE`v1 IN segment (v,w) /\ v1 IN relative_interior f
1656 ==> ~DISJOINT (relative_interior f) (segment (v,w:real^3))`)
1657 THEN ASM_REWRITE_TAC[]
1658 THEN REPEAT STRIP_TAC
1659 THEN MRESAL_TAC FACE_OF_EQ[`p:real^3->bool`;`f:real^3->bool`;`segment[v,w:real^3]`][RELATIVE_INTERIOR_SEGMENT;]
1660 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC)
1661 THEN ASM_TAC
1662 THEN ARITH_TAC;
1663
1664 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1665 THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`]
1666 THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`v:real^3`]
1667 THEN MP_TAC( ISPECL [`f:real^3->bool`;`v:real^3`]EXTREME_POINT_NOT_IN_RELATIVE_INTERIOR)
1668 THEN RESA_TAC
1669 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;
1670 AFF_DIM_SING])
1671 THEN ARITH_TAC;
1672
1673 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1674 THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`]
1675 THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`w:real^3`]
1676 THEN MP_TAC( ISPECL [`f:real^3->bool`;`w:real^3`]EXTREME_POINT_NOT_IN_RELATIVE_INTERIOR)
1677 THEN RESA_TAC
1678 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;
1679 AFF_DIM_SING])
1680 THEN ARITH_TAC]]]]);;
1681
1682
1683
1684
1685 let FCHANGED_EQ_YFAN=prove(`!p:real^3->bool.
1686          bounded p /\ polyhedron p /\ vec 0 IN interior p
1687 ==> UNIONS {fchanged f| f facet_of p}= yfan(vec 0,vertices p,edges p)`,
1688 REPEAT STRIP_TAC
1689 THEN REWRITE_TAC[EXTENSION]
1690 THEN GEN_TAC
1691 THEN EQ_TAC
1692 THENL[ ASM_SIMP_TAC[FCHANGED_SUBSET_YFAN];
1693 ASM_SIMP_TAC[YFAN_SUBSET_UNIONS_FCHANGED]]);;
1694
1695
1696
1697 let EXISTS_POINT_IN_FCHANGED=prove(`!f p:real^3->bool.
1698          bounded p /\ polyhedron p /\ vec 0 IN interior p /\
1699  f facet_of p
1700 ==> ?y. y IN fchanged f `,
1701
1702 REPEAT STRIP_TAC
1703 THEN POP_ASSUM MP_TAC
1704 THEN REWRITE_TAC[fchanged;IN_ELIM_THM;IN_ELIM_THM;facet_of]
1705 THEN STRIP_TAC
1706 THEN MRESA_TAC FACE_OF_IMP_CONVEX[`p:real^3->bool`;`f:real^3->bool`]
1707 THEN MRESAL1_TAC  RELATIVE_INTERIOR_EQ_EMPTY`f:real^3->bool`[SET_RULE`~(A={})<=> ?v1. v1 IN A`]
1708 THEN EXISTS_TAC`v1:real^3`
1709 THEN EXISTS_TAC`v1:real^3`
1710 THEN EXISTS_TAC`&1`
1711 THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 % v= v`;REAL_ARITH`&1> &0`]);;
1712
1713
1714
1715 let FCHANGED_IN_COMPONENT=prove(`!f p:real^3->bool.
1716          bounded p /\ polyhedron p /\ vec 0 IN interior p /\
1717  f facet_of p
1718 ==> fchanged f IN topological_component_yfan(vec 0:real^3,vertices (p:real^3->bool),edges (p:real^3->bool))`,
1719
1720 REPEAT STRIP_TAC
1721 THEN REWRITE_TAC[topological_component_yfan;IN_ELIM_THM]
1722 THEN MRESA1_TAC FCHANGED_EQ_YFAN`p:real^3->bool`
1723 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1724 THEN MRESA_TAC EXISTS_POINT_IN_FCHANGED[`f:real^3->bool`;`p:real^3->bool`]
1725 THEN EXISTS_TAC`y:real^3`
1726 THEN MP_TAC(SET_RULE`f facet_of (p:real^3->bool) /\ y IN fchanged f ==> y IN UNIONS{fchanged f| f facet_of p} /\ fchanged f SUBSET UNIONS{fchanged f| f facet_of p}`)
1727 THEN RESA_TAC
1728 THEN MRESAL_TAC CONNECTED_FCHANGED[`p:real^3->bool`;`vec 0:real^3`;`f:real^3->bool`][CONNECTED_CONNECTED_COMPONENT_SET]
1729 THEN POP_ASSUM (fun th-> MRESA1_TAC th`y:real^3`)
1730 THEN MRESA_TAC CONNECTED_COMPONENT_MONO[`fchanged (f:real^3->bool)`;`UNIONS{fchanged f| f facet_of (p:real^3->bool)}`;`y:real^3`]
1731 THEN REWRITE_TAC[EXTENSION;]
1732 THEN GEN_TAC
1733 THEN EQ_TAC
1734 THENL[
1735 POP_ASSUM MP_TAC
1736 THEN SET_TAC[];
1737
1738
1739 STRIP_TAC
1740 THEN DISJ_CASES_TAC(SET_RULE`~(x IN fchanged (f:real^3->bool))\/ (x IN fchanged (f:real^3->bool))`)
1741 THENL[
1742
1743 ASM_REWRITE_TAC[]
1744 THEN MRESAL_TAC CONNECTED_COMPONENT_SUBSET[`UNIONS{fchanged f| f facet_of (p:real^3->bool)}`;`y:real^3`][SUBSET]
1745 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:real^3`[UNIONS;IN_ELIM_THM])
1746 THEN POP_ASSUM MP_TAC
1747 THEN RESA_TAC
1748 THEN DISJ_CASES_TAC(SET_RULE`f= f'\/ ~(f= f':real^3->bool)`)
1749 THENL[
1750 POP_ASSUM (fun th-> POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SYM th]);
1751
1752
1753 MRESA_TAC CONNECTED_CONNECTED_COMPONENT[`UNIONS{fchanged f| f facet_of (p:real^3->bool)}`;`y:real^3`]
1754 THEN POP_ASSUM MP_TAC
1755 THEN REWRITE_TAC[connected]
1756 THEN ABBREV_TAC`e1=UNIONS {fchanged f1 | f1 facet_of (p:real^3->bool) /\ ~(f1= f)}`
1757 THEN MRESA_TAC FCHANGED_OPEN[`p:real^3->bool`;`f:real^3->bool`]
1758 THEN EXISTS_TAC`fchanged (f:real^3->bool)`
1759 THEN EXISTS_TAC`e1:real^3->bool`
1760 THEN ASM_REWRITE_TAC[]
1761 THEN STRIP_TAC
1762 THENL[
1763
1764 EXPAND_TAC "e1"
1765 THEN MATCH_MP_TAC OPEN_UNIONS
1766 THEN REWRITE_TAC[IN_ELIM_THM]
1767 THEN REPEAT STRIP_TAC
1768 THEN MRESA_TAC FCHANGED_OPEN[`p:real^3->bool`;`f1:real^3->bool`];
1769
1770 STRIP_TAC
1771 THENL[
1772
1773 MATCH_MP_TAC (SET_RULE`!A B C. A SUBSET B/\  B SUBSET C==> A SUBSET C`)
1774 THEN EXISTS_TAC`UNIONS{fchanged f| f facet_of (p:real^3->bool)}`
1775 THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_SUBSET]
1776 THEN EXPAND_TAC"e1"
1777 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;UNION;UNIONS;EX]
1778 THEN REPEAT STRIP_TAC
1779 THEN POP_ASSUM MP_TAC
1780 THEN RESA_TAC
1781 THEN DISJ_CASES_TAC(SET_RULE`f= f'' \/ ~(f''= f:real^3->bool )`)
1782 THENL[
1783 ASM_REWRITE_TAC[];
1784
1785 MATCH_MP_TAC(SET_RULE`A==> B\/ A`)
1786 THEN EXISTS_TAC`fchanged (f'':real^3->bool)`
1787 THEN ASM_REWRITE_TAC[]
1788 THEN EXISTS_TAC`f'':real^3->bool`
1789 THEN ASM_REWRITE_TAC[]];
1790
1791 STRIP_TAC
1792 THENL[
1793
1794 MATCH_MP_TAC(SET_RULE`A INTER B= {}==> A INTER B INTER C= {}`)
1795 THEN EXPAND_TAC"e1"
1796 THEN MATCH_MP_TAC(SET_RULE`(!s. s IN B==> A INTER s= {} )==> A INTER UNIONS B={}`)
1797 THEN REWRITE_TAC[IN_ELIM_THM]
1798 THEN REPEAT STRIP_TAC
1799 THEN ASM_REWRITE_TAC[]
1800 THEN MRESA_TAC FCHANGED_ONE_TO_ONE[`p:real^3->bool`;`f:real^3->bool`;`f1:real^3->bool`];
1801
1802
1803
1804 STRIP_TAC
1805 THENL[
1806
1807 ASM_TAC
1808 THEN SET_TAC[];
1809 REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;INTER; IN_ELIM_THM]
1810 THEN EXISTS_TAC`x:real^3`
1811 THEN ASM_REWRITE_TAC[]
1812 THEN EXPAND_TAC"e1"
1813 THEN REWRITE_TAC[UNIONS;IN_ELIM_THM]
1814 THEN EXISTS_TAC`fchanged (f':real^3->bool)`
1815 THEN ASM_REWRITE_TAC[]
1816 THEN EXISTS_TAC`f':real^3->bool`
1817 THEN ASM_REWRITE_TAC[]]]]]];
1818
1819 ASM_REWRITE_TAC[]]]);;
1820
1821
1822
1823 let SUR_FCHANGED=prove(`!s p:real^3->bool.
1824          bounded p /\ polyhedron p /\ vec 0 IN interior p /\
1825  s IN topological_component_yfan(vec 0:real^3,vertices (p:real^3->bool),edges (p:real^3->bool))
1826 ==> ?f. f facet_of p /\ s= fchanged f`,
1827
1828 REPEAT STRIP_TAC
1829 THEN MRESA1_TAC FCHANGED_EQ_YFAN`p:real^3->bool`
1830 THEN MRESA_TAC topological_component_subset_yfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`s:real^3->bool`]
1831 THEN POP_ASSUM MP_TAC
1832 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SUBSET;IN_ELIM_THM;UNIONS])
1833 THEN MRESA_TAC exists_point_in_component_yfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`s:real^3->bool`]
1834 THEN STRIP_TAC
1835 THEN POP_ASSUM(fun th-> MRESA1_TAC th`z:real^3`)
1836 THEN POP_ASSUM MP_TAC
1837 THEN RESA_TAC
1838 THEN EXISTS_TAC`f:real^3->bool`
1839 THEN ASM_REWRITE_TAC[]
1840 THEN MRESA_TAC FCHANGED_IN_COMPONENT[`f:real^3->bool`;`p:real^3->bool`]
1841 THEN ASM_TAC
1842 THEN REWRITE_TAC[topological_component_yfan;IN_ELIM_THM]
1843 THEN REPEAT RESA_TAC
1844 THEN MP_TAC(SET_RULE`z IN connected_component (yfan (vec 0,vertices p,edges p)) y
1845 /\ z IN fchanged f /\ fchanged f=connected_component (yfan (vec 0,vertices p,edges p)) y'
1846 ==> ~(connected_component (yfan (vec 0,vertices p,edges p)) y INTER connected_component (yfan (vec 0,vertices p,edges p)) y'= {})
1847 `)
1848 THEN RESA_TAC
1849 THEN MRESA_TAC CONNECTED_COMPONENT_OVERLAP[`yfan (vec 0,vertices p,edges p)`;`y:real^3`;`y':real^3`]);;
1850
1851
1852
1853
1854
1855 let AMHFNXP= prove(`!p:real^3->bool.
1856          bounded p /\ polyhedron p /\ vec 0 IN interior p
1857 ==>
1858 (!s. s IN topological_component_yfan (vec 0,vertices (p:real^3->bool),edges (p:real^3->bool)) ==> (?!f. f facet_of p /\
1859                                                          s = fchanged f))`,
1860
1861 REWRITE_TAC[EXISTS_UNIQUE]
1862 THEN REPEAT STRIP_TAC
1863 THEN MRESA_TAC SUR_FCHANGED[`s:real^3->bool`;`p:real^3->bool`]
1864 THEN EXISTS_TAC`f:real^3->bool`
1865 THEN ASM_REWRITE_TAC[]
1866 THEN REPEAT STRIP_TAC
1867 THEN MRESA_TAC FCHANGED_ONE_TO_ONE[`p:real^3->bool`;`y:real^3->bool`;`f:real^3->bool`]
1868 THEN POP_ASSUM MATCH_MP_TAC
1869 THEN REWRITE_TAC[SET_RULE`A INTER A= A`]
1870 THEN MRESA_TAC EXISTS_POINT_IN_FCHANGED[`y:real^3->bool`;`p:real^3->bool`]
1871 THEN POP_ASSUM MP_TAC
1872 THEN SET_TAC[]);;
1873
1874
1875 let AMHFNXP_BIJ = prove_by_refinement(
1876   `!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==>
1877   (BIJ fchanged (\f. f facet_of p) (topological_component_yfan (vec 0,vertices p,edges p)))`,
1878   (* {{{ proof *)
1879   [
1880 REWRITE_TAC [BIJ;INJ;SURJ;IN;IN_ELIM_THM];
1881 STRIP_TAC ;
1882 STRIP_TAC ;
1883 ASM_SIMP_TAC [REWRITE_RULE[IN] FCHANGED_IN_COMPONENT];
1884 MP_TAC (REWRITE_RULE[IN] FCHANGED_IN_COMPONENT);
1885 MP_TAC (SPEC `p:real^3->bool` (REWRITE_RULE[IN] AMHFNXP));
1886 ASM_REWRITE_TAC [EXISTS_UNIQUE];
1887 ASM_MESON_TAC []
1888   ]);;
1889   (* }}} *)
1890
1891
1892
1893 let EXPAND_EDGE_POLYTOPE=prove(`!f p:real^N->bool.
1894 polytope p /\ f face_of p /\ aff_dim f= &1
1895 ==> ?a b. f= segment[a,b]`,
1896 REPEAT STRIP_TAC
1897 THEN MRESA1_TAC AFF_DIM`f:real^N->bool`
1898 THEN POP_ASSUM MP_TAC
1899 THEN REWRITE_TAC[ARITH_RULE`&1=A - &1:int <=> A= &2`;INT_OF_NUM_EQ]
1900 THEN STRIP_TAC
1901 THEN MRESA1_TAC AFFINE_INDEPENDENT_IMP_FINITE`b:real^N->bool`
1902 THEN MRESA1_TAC CARD_EXISTS_2`b:real^N->bool`
1903 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1904 THEN MATCH_MP_TAC COMPACT_CONVEX_COLLINEAR_SEGMENT
1905 THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^N->bool`;`p:real^N->bool`]
1906 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`f:real^N->bool`
1907 THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`f:real^N->bool`
1908 THEN SUBGOAL_THEN`?u v. f SUBSET affine hull {u,v:real^N}` ASSUME_TAC
1909 THENL[ EXISTS_TAC`v:real^N`
1910 THEN EXISTS_TAC`w:real^N`
1911 THEN ASM_REWRITE_TAC[HULL_SUBSET];
1912 ASM_REWRITE_TAC[COLLINEAR_AFFINE_HULL]
1913 THEN STRIP_TAC
1914 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;AFF_DIM_EMPTY])
1915 THEN ARITH_TAC]);;
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932 let EXISTS_EDGE_AT_VERTICES=prove(`!p:real^3->bool.
1933          bounded p /\ polyhedron p /\ vec 0 IN interior p
1934 ==>  (!v. v IN vertices p ==> ~(set_of_edge v (vertices p) (edges p) ={}) )`,
1935
1936 REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;]
1937 THEN REPEAT STRIP_TAC
1938 THEN POP_ASSUM MP_TAC
1939 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[vertices; IN_ELIM_THM;GSYM FACE_OF_SING]
1940 THEN STRIP_TAC
1941 THEN MRESA1_TAC AFF_DIM_SING`v:real^3`
1942 THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
1943 THEN POP_ASSUM MP_TAC
1944 THEN DISJ_CASES_TAC(SET_RULE`p ={v}\/ ~({v}=p:real^3->bool) `)
1945 THENL[
1946 ASM_REWRITE_TAC[]
1947 THEN ARITH_TAC;
1948 STRIP_TAC
1949 THEN MRESAL_TAC FACE_OF_POLYHEDRON_SUBSET_FACET[`p:real^3->bool`;`{v:real^3}`][SET_RULE`~({v}={})`]
1950 THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`p:real^3->bool`]
1951 THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f==> v IN f`)
1952 THEN RESA_TAC
1953 THEN FIND_ASSUM MP_TAC`f facet_of (p:real^3->bool)`
1954 THEN REWRITE_TAC[facet_of]
1955 THEN STRIP_TAC
1956 THEN MRESAL_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`v:real^3`][GSYM FACE_OF_SING]
1957 THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`f:real^3->bool`]
1958 THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
1959 THEN DISJ_CASES_TAC(SET_RULE`f ={v}\/ ~({v}=f:real^3->bool) `)
1960 THENL[
1961 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC)
1962 THEN ASM_TAC
1963 THEN ARITH_TAC;
1964  MRESAL_TAC FACE_OF_POLYHEDRON_SUBSET_FACET[`f:real^3->bool`;`{v:real^3}`][SET_RULE`~({v}={})`]
1965 THEN POP_ASSUM MP_TAC
1966 THEN POP_ASSUM MP_TAC
1967 THEN ASM_REWRITE_TAC[facet_of;ARITH_RULE`&3- &1- &1= &1:int`]
1968 THEN STRIP_TAC
1969 THEN MRESA_TAC FACE_OF_TRANS[`f':real^3->bool`;`f:real^3->bool`;`p:real^3->bool`]
1970 THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
1971 THEN STRIP_TAC
1972 THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f' ==> v IN f'`)
1973 THEN RESA_TAC
1974 THEN MRESAL_TAC EXTREME_POINT_OF_FACE[`f':real^3->bool`;`f:real^3->bool`;`v:real^3`][GSYM FACE_OF_SING]
1975 THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`f':real^3->bool`]
1976 THEN POP_ASSUM MP_TAC
1977 THEN MRESA_TAC EXPAND_EDGE_POLYTOPE[`f':real^3->bool`;`p:real^3->bool`]
1978 THEN REWRITE_TAC[EXTREME_POINT_OF_SEGMENT]
1979 THEN STRIP_TAC
1980 THENL[
1981 POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1982 THEN POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1983 THEN EXISTS_TAC`b:real^3`
1984 THEN ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM;edges;vertices]
1985 THEN MRESAL_TAC SEGMENT_EDGE_OF[`p:real^3->bool`;`a:real^3`;`b:real^3`][edge_of]
1986 THEN EXISTS_TAC`a:real^3`
1987 THEN EXISTS_TAC`b:real^3`
1988 THEN ASM_REWRITE_TAC[];
1989 POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1990 THEN POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1991 THEN EXISTS_TAC`a:real^3`
1992 THEN ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM;edges;vertices]
1993 THEN MRESAL_TAC SEGMENT_EDGE_OF[`p:real^3->bool`;`a:real^3`;`b:real^3`][edge_of]
1994 THEN EXISTS_TAC`a:real^3`
1995 THEN EXISTS_TAC`b:real^3`
1996 THEN ASM_REWRITE_TAC[]
1997 THEN SET_TAC[]]]]);;
1998
1999
2000
2001
2002
2003
2004
2005 let FLVNSME=prove(`!v A a b p:real^3->bool.
2006          bounded p /\ polyhedron p /\ vec 0 IN interior p
2007  /\ A={x| a dot x < b } /\ ~(a= vec 0)
2008 /\ v IN {x| a dot x = b } /\ vec 0 IN {x| a dot x = b }
2009 /\ v IN vertices p
2010 ==> ?w. w IN vertices p /\ w IN A/\ {v,w} IN edges p`,
2011 (let lemma = prove
2012    (`!X:real->bool.
2013           FINITE X /\ ~(X = {})
2014           ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
2015     MESON_TAC[INF_FINITE]) in
2016
2017
2018 REPEAT STRIP_TAC
2019 THEN POP_ASSUM (fun th-> MP_TAC th
2020 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[vertices; IN_ELIM_THM;GSYM FACE_OF_SING] THEN ASSUME_TAC(th)
2021 THEN STRIP_TAC)
2022 THEN MRESA1_TAC AFF_DIM_SING`v:real^3`
2023 THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
2024 THEN POP_ASSUM MP_TAC
2025 THEN DISJ_CASES_TAC(SET_RULE`p ={v}\/ ~({v}=p:real^3->bool) `)
2026
2027 THENL(*1*)[
2028
2029 ASM_REWRITE_TAC[]
2030 THEN ARITH_TAC;(*1*)
2031
2032 STRIP_TAC
2033 THEN MRESAL_TAC FACE_OF_POLYHEDRON_SUBSET_FACET[`p:real^3->bool`;`{v:real^3}`][SET_RULE`~({v}={})`]
2034 THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`p:real^3->bool`]
2035 THEN MRESAL_TAC EXPOSED_FACE_OF_POLYHEDRON[`p:real^3->bool`;`{v:real^3}`][EXPOSED_FACE_OF;SET_RULE`~({v}={})`]
2036 THEN ABBREV_TAC`s={-- (a':real^3) dot w| w IN vertices p /\ ~(v=w)}`
2037 THEN SUBGOAL_THEN`~(s:real->bool={})`ASSUME_TAC
2038
2039 THENL(*2*)[
2040
2041 MRESA1_TAC EXISTS_EDGE_AT_VERTICES`p:real^3->bool`
2042 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2043 THEN POP_ASSUM MP_TAC
2044 THEN EXPAND_TAC"s"
2045 THEN REWRITE_TAC[set_of_edge;SET_RULE`~(A={})<=> ?a. a IN A`;IN_ELIM_THM; edges; ]
2046 THEN STRIP_TAC
2047 THEN EXISTS_TAC`-- a' dot (a'':real^3)`
2048 THEN EXISTS_TAC`a'':real^3`
2049 THEN ASM_REWRITE_TAC[]
2050 THEN MRESA_TAC SEGMENT_EDGE_OF[`p:real^3->bool`;`v':real^3`;`w':real^3`]
2051 THEN STRIP_TAC
2052 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; SET_RULE`{v,v}={v}`]
2053 THEN REPEAT STRIP_TAC)
2054 THEN MP_TAC(SET_RULE`{a''} = {v', w':real^3}==> v'=w'`)
2055 THEN ASM_REWRITE_TAC[]
2056 THEN ASM_TAC
2057 THEN SET_TAC[];(*2*)
2058
2059  MRESAL_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`][FAN;fan1]
2060 THEN ASSUME_TAC(SET_RULE`{w|w IN vertices p /\ ~(v = w:real^3)} SUBSET vertices p`)
2061 THEN MRESA_TAC FINITE_SUBSET[`{w|w IN vertices p /\ ~(v = w:real^3)}`;`vertices (p:real^3->bool)`]
2062 THEN MRESAL_TAC FINITE_IMAGE[`(\w:real^3. -- a' dot w)`;`{w|w IN vertices p /\ ~(v = w:real^3)}`][IMAGE;IN_ELIM_THM;SET_RULE`{y | ?x. (x IN vertices p /\ ~(v = x)) /\ y = -- a' dot x}={-- a' dot w | w IN vertices p /\ ~(v = w)}`]
2063 THEN MRESA1_TAC lemma`s:real->bool`
2064 THEN SUBGOAL_THEN(`-- a''< b':real`)ASSUME_TAC
2065
2066 THENL(*3*)[
2067
2068 POP_ASSUM MP_TAC
2069 THEN POP_ASSUM MP_TAC
2070 THEN EXPAND_TAC"s"
2071 THEN REWRITE_TAC[IN_ELIM_THM;vertices;GSYM FACE_OF_SING]
2072 THEN RESA_TAC
2073 THEN MRESA_TAC FACE_OF_IMP_SUBSET[`p:real^3->bool`;`{w:real^3}`]
2074 THEN MP_TAC(SET_RULE`p SUBSET {x | a' dot x <= b'} /\ {w:real^3} SUBSET p==> w IN {x | a' dot x <= b'}`)
2075 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
2076 THEN STRIP_TAC
2077 THEN MP_TAC(REAL_ARITH`a' dot (w:real^3) <= b'==> a' dot w = b' \/ a' dot w < b'`)
2078 THEN ASM_REWRITE_TAC[]
2079 THEN STRIP_TAC
2080 THENL(*4*)[
2081
2082 MP_TAC(SET_RULE`a' dot w = b'/\ {w} SUBSET p /\{v}=p INTER {x | a' dot (x:real^3) = b'}==> w =v`)
2083 THEN RESA_TAC;(*4*)
2084
2085 ASM_REWRITE_TAC[VECTOR_ARITH`--(-- a dot w)= a dot w`]](*4*);(*3*)
2086
2087 MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
2088 THEN MP_TAC(SET_RULE` interior p SUBSET p /\ p SUBSET {x:real^3 | a' dot x <= b'} ==>  interior p  SUBSET {x | a' dot x <= b'} `)
2089 THEN RESA_TAC
2090 THEN MP_TAC(SET_RULE`(vec 0) IN interior (p:real^3->bool) /\ interior p  SUBSET {x | a' dot x <= b'}==> (vec 0) IN {x:real^3 | a' dot x <= b'}`)
2091 THEN RESA_TAC
2092 THEN POP_ASSUM MP_TAC
2093 THEN REWRITE_TAC[IN_ELIM_THM; DOT_RZERO]
2094 THEN STRIP_TAC
2095 THEN MP_TAC(REAL_ARITH`&0<= b' ==> b'= &0 \/ &0< b'`)
2096 THEN RESA_TAC
2097 THENL(*6*)[
2098
2099 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2100 THEN SUBGOAL_THEN`vec 0 IN  {x:real^3 | a' dot x = &0}` ASSUME_TAC
2101
2102 THENL(*7*)[
2103 REWRITE_TAC[IN_ELIM_THM; DOT_RZERO];(*7*)
2104
2105 MP_TAC(SET_RULE`(vec 0) IN interior (p:real^3->bool) /\ interior p SUBSET p ==> (vec 0) IN p`)
2106 THEN RESA_TAC
2107 THEN MP_TAC(SET_RULE`(vec 0) IN  (p:real^3->bool) /\ vec 0 IN  {x:real^3 | a' dot x = &0} ==> (vec 0) IN p INTER  {x:real^3 | a' dot x = &0}`)
2108 THEN RESA_TAC
2109 THEN MP_TAC(SET_RULE`(vec 0) IN p INTER  {x:real^3 | a' dot x = &0} /\
2110  p INTER  {x:real^3 | a' dot x = &0} = {v} ==> v= vec 0`)
2111 THEN RESA_TAC
2112 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2113 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`vec 0:real^3`]](*7*);(*6*)
2114
2115
2116
2117 ABBREV_TAC`b1= max (-- a'') (&0) + (b'- max (-- a'') (&0))/ &2`
2118 THEN MP_TAC(REAL_ARITH`max (-- a'') (&0) + (b'- max (-- a'') (&0))/ &2 = b1 /\ -- a''< b' /\  &0< b' ==> -- a''< b1 /\ b1< b' /\ &0< b1`)
2119 THEN RESA_TAC
2120 THEN SUBGOAL_THEN`vertices (p:real^3->bool) INTER {x| a' dot x >= b1}={v}` ASSUME_TAC
2121 THENL(*7*)[
2122
2123 REWRITE_TAC[EXTENSION; IN_SING; INTER;IN_ELIM_THM]
2124 THEN GEN_TAC
2125 THEN EQ_TAC
2126
2127 THENL(*8*)[
2128
2129 STRIP_TAC
2130 THEN MP_TAC(REAL_ARITH`--a'' < b1 /\ a' dot (x:real^3) >= b1 ==> -- (a' dot x) < a''`)
2131 THEN RESA_TAC
2132 THEN DISJ_CASES_TAC(SET_RULE`~(v= x) \/ x=v:real^3`)
2133
2134 THENL(*9*)[
2135
2136 MP_TAC(SET_RULE`~(v = x) /\ x IN vertices p ==> -- a' dot x IN {--a' dot w | w IN vertices p /\ ~(v = w:real^3)}`)
2137 THEN RESA_TAC
2138 THEN FIND_ASSUM (fun th-> MP_TAC(ISPEC `--a' dot x:real^3` th))`!x. x IN s ==> a'' <= x`
2139 THEN POP_ASSUM(fun th-> REWRITE_TAC[th; VECTOR_ARITH`--a' dot x= --(a' dot x)`])
2140 THEN ASM_TAC
2141 THEN REAL_ARITH_TAC;(*9*)
2142
2143 ASM_REWRITE_TAC[]](*9*);(*8*)
2144
2145
2146 RESA_TAC
2147 THEN MP_TAC(SET_RULE`{v} = p INTER {x | a' dot x:real^3 = b'} ==> a' dot v= b'`)
2148 THEN RESA_TAC
2149 THEN ASM_TAC
2150 THEN REAL_ARITH_TAC](*8*);(*7*)
2151
2152 ABBREV_TAC`p'= p INTER {x | a' dot x:real^3 = b1}`
2153 THEN SUBGOAL_THEN `vec 0 IN {x:real^3 | a' dot x < b1}`ASSUME_TAC
2154 THENL(*8*)[
2155 ASM_REWRITE_TAC[IN_ELIM_THM; DOT_RZERO];(*8*)
2156
2157
2158 MRESAL_TAC OPEN_HALFSPACE_LT[`a':real^3`;`b1:real`][open_def]
2159 THEN POP_ASSUM (fun th-> MRESA1_TAC th`vec 0:real^3`)
2160 THEN POP_ASSUM MP_TAC
2161 THEN DISCH_THEN(LABEL_TAC"LINH")
2162 THEN FIND_ASSUM MP_TAC`vec 0 IN interior p:real^3->bool`
2163 THEN REWRITE_TAC[IN_INTERIOR]
2164 THEN STRIP_TAC
2165 THEN POP_ASSUM MP_TAC
2166 THEN DISCH_THEN(LABEL_TAC"LINH1")
2167 THEN SUBGOAL_THEN`vec 0 IN closure {x:real^3 | a dot x < b}`ASSUME_TAC
2168 THENL(*9*)[
2169
2170 MRESAL_TAC CLOSURE_HALFSPACE_LT[`a:real^3`;`b:real`][IN_ELIM_THM]
2171 THEN ASM_TAC
2172 THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC
2173 THEN REAL_ARITH_TAC;(*9*)
2174
2175 POP_ASSUM MP_TAC
2176 THEN REWRITE_TAC[CLOSURE_APPROACHABLE]
2177 THEN MP_TAC(REAL_ARITH`&0< e /\ &0< e'==> &0< min (e:real) e'/ &2 /\  min (e:real) e'/ &2< e/\ min (e:real) e'/ &2< e'`)
2178 THEN RESA_TAC
2179 THEN STRIP_TAC
2180 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(min (e:real) e') / &2`)
2181 THEN MP_TAC(REAL_ARITH`dist (y:real^3,vec 0) < min e e' / &2 /\  min e e' / &2 < e
2182 /\ min e e' / &2 < e'==> dist (y,vec 0) < e /\ dist (y,vec 0) < e'`)
2183 THEN RESA_TAC
2184 THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`y:real^3`)
2185 THEN SUBGOAL_THEN `y:real^3 IN ball(vec 0, e')` ASSUME_TAC
2186
2187 THENL(*10*)[
2188
2189 ASM_REWRITE_TAC[SUBSET;ball;IN_ELIM_THM; DIST_SYM];(*10*)
2190
2191 MRESAL_TAC OPEN_BALL[`vec 0:real^3`;`e':real`][open_def]
2192 THEN POP_ASSUM(fun th-> MRESA1_TAC th`y:real^3`)
2193 THEN SUBGOAL_THEN`y IN interior p:real^3->bool` ASSUME_TAC
2194 THENL(*11*)[
2195
2196 REWRITE_TAC[IN_INTERIOR]
2197 THEN EXISTS_TAC`e'':real`
2198 THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;ball;DIST_SYM]
2199 THEN GEN_TAC
2200 THEN POP_ASSUM MP_TAC
2201 THEN DISCH_THEN(LABEL_TAC"LINH2")
2202 THEN STRIP_TAC
2203 THEN REMOVE_THEN"LINH2"(fun th-> MRESA1_TAC th`x:real^3`)
2204 THEN ASM_TAC
2205 THEN SET_TAC[];(*11*)
2206
2207 MP_TAC(SET_RULE`y IN interior p /\ interior p SUBSET p ==>  y IN (p:real^3->bool)`)
2208 THEN RESA_TAC
2209 THEN SUBGOAL_THEN`?z. z IN segment[y,v:real^3] INTER {x| a' dot x= b1} /\ ~(z= v)` ASSUME_TAC
2210 THENL(*12*)[
2211
2212 MP_TAC(SET_RULE`vertices p INTER {x | a' dot x >= b1} = {v:real^3} ==> v IN {x | a' dot x >= b1}`)
2213 THEN RESA_TAC
2214 THEN REWRITE_TAC[INTER;IN_SEGMENT;IN_ELIM_THM]
2215 THEN ASM_TAC
2216 THEN REWRITE_TAC[IN_ELIM_THM]
2217 THEN REPEAT RESA_TAC
2218 THEN MP_TAC(SET_RULE`{v} = p INTER {x | a' dot x = b'}==> a' dot (v:real^3)= b'`)
2219 THEN RESA_TAC
2220 THEN  MP_TAC(REAL_ARITH`a' dot y < b1 /\ a' dot v >= b1 /\ a' dot v = b' /\ b1< b' ==> &0< a' dot v - a' dot (y:real^3) /\ &0< b1- a' dot y/\ b1- a' dot y < a' dot v - a' dot (y:real^3) /\ ~(a' dot v - a' dot (y:real^3)= &0)`)
2221 THEN RESA_TAC
2222 THEN MRESA1_TAC REAL_LT_INV`a' dot v - a' dot (y:real^3)`
2223 THEN MRESA_TAC REAL_LT_MUL[`inv(a' dot v - a' dot (y:real^3))`;`b1 - a' dot (y:real^3)`]
2224 THEN MP_TAC(REAL_ARITH`&0< inv(a' dot v - a' dot (y:real^3))==> &0<= inv(a' dot v - a' dot (y:real^3))`)
2225 THEN RESA_TAC
2226 THEN MRESA1_TAC REAL_MUL_LINV`a' dot v - a' dot (y:real^3)`
2227 THEN MRESA_TAC REAL_LT_LMUL[`inv(a' dot v - a' dot (y:real^3))`;`b1 - a' dot (y:real^3)`;`a' dot v - a' dot (y:real^3)`]
2228 THEN EXISTS_TAC`(&1- inv (a' dot v - a' dot y) * (b1 - a' dot y)) % (y:real^3)+ (inv (a' dot v - a' dot y) * (b1 - a' dot y))% v`
2229 THEN REWRITE_TAC[DOT_RMUL; DOT_RADD; REAL_ARITH`(&1- b)* c+b * d=a<=>b*(d-c)= a- c`;]
2230 THEN ASM_REWRITE_TAC[ REAL_ARITH`(a*b)*c= b*(a*c)`; REAL_ARITH`a * &1= a`]
2231 THEN STRIP_TAC
2232 THENL(*13*)[
2233
2234
2235  EXISTS_TAC`inv (a' dot v - a' dot y) * (b1 - a' dot (y:real^3))`
2236 THEN ASM_REWRITE_TAC[]
2237 THEN ASM_TAC
2238 THEN REAL_ARITH_TAC;(*13*)
2239
2240 REWRITE_TAC[VECTOR_ARITH`(&1- b)%a + b % v= v<=> (&1-b)%(a-v)= vec 0`;VECTOR_MUL_EQ_0]
2241 THEN STRIP_TAC
2242
2243 THENL(*14*)[
2244 ASM_TAC THEN REAL_ARITH_TAC;(*14*)
2245
2246 POP_ASSUM MP_TAC
2247 THEN REWRITE_TAC[VECTOR_ARITH`y- v= vec 0<=> y= v`]
2248 THEN STRIP_TAC
2249 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] )
2250 THEN REAL_ARITH_TAC](*14*)](*13*);(*12*)
2251
2252 POP_ASSUM MP_TAC
2253 THEN STRIP_TAC
2254 THEN MRESA_TAC FACET_OF_IMP_SUBSET[`f:real^3->bool`;`p:real^3->bool`]
2255 THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f /\ f SUBSET p/\ y IN p==> {v,y} SUBSET p `)
2256 THEN RESA_TAC
2257 THEN MRESA1_TAC POLYHEDRON_IMP_CONVEX`p:real^3->bool`
2258 THEN  MRESAL_TAC SUBSET_HULL [`convex:(real^3->bool)->bool`;`{v,y:real^3}`;`p:real^3->bool`] [GSYM SEGMENT_CONVEX_HULL;]
2259 THEN POP_ASSUM MP_TAC
2260 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
2261 THEN STRIP_TAC
2262 THEN MP_TAC(SET_RULE`z IN segment [y,v] INTER {x | a' dot x = b1}
2263 /\ segment [y,v:real^3] SUBSET p ==> z IN  p INTER {x | a' dot x = b1}`)
2264 THEN RESA_TAC
2265 THEN MP_TAC(SET_RULE`y IN {x | a dot x < b}==>  a dot (y:real^3) < b`)
2266 THEN RESA_TAC
2267 THEN MP_TAC(REAL_ARITH`a dot (y:real^3) < b==> a dot (y:real^3) <= b `)
2268 THEN RESA_TAC
2269 THEN MP_TAC(SET_RULE`v IN {x | a dot x = b} ==>  a dot (v:real^3) = b`)
2270 THEN RESA_TAC
2271 THEN MP_TAC(REAL_ARITH`a dot (v:real^3) = b==> a dot (v:real^3) <= b `)
2272 THEN RESA_TAC
2273 THEN MP_TAC(SET_RULE`  a dot (y:real^3) <= b /\  a dot v <= b ==> {v,y} SUBSET {x | a dot x <= b}`)
2274 THEN RESA_TAC
2275 THEN MRESA_TAC CONVEX_HALFSPACE_LE[`a:real^3`;`b:real`]
2276 THEN  MRESAL_TAC SUBSET_HULL [`convex:(real^3->bool)->bool`;`{v,y:real^3}`;`{x | a dot x <= b}:real^3->bool`] [GSYM SEGMENT_CONVEX_HULL;]
2277 THEN POP_ASSUM MP_TAC
2278 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
2279 THEN STRIP_TAC
2280 THEN MP_TAC(SET_RULE`z IN segment [y,v] INTER {x | a' dot x = b1}
2281 /\ segment [y,v:real^3] SUBSET {x | a dot x <= b} ==>   z IN {x | a dot x <= b}/\ z IN segment [y,v] `)
2282 THEN RESA_TAC
2283 THEN POP_ASSUM MP_TAC
2284 THEN POP_ASSUM MP_TAC
2285 THEN REWRITE_TAC[IN_ELIM_THM; REAL_ARITH`a<=b<=> a=b\/ a<b`]
2286 THEN STRIP_TAC
2287 THENL(*13*)[
2288
2289 REWRITE_TAC[segment;IN_ELIM_THM;]
2290 THEN STRIP_TAC
2291 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC
2292 THEN POP_ASSUM MP_TAC
2293 THEN POP_ASSUM MP_TAC
2294 THEN POP_ASSUM MP_TAC
2295 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;REAL_ARITH`(&1-a) *b+a*c=c<=> (&1-a)*(b-c)= &0`;REAL_ENTIRE; REAL_ARITH`a-b= &0<=> b=a`]
2296 THEN ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC THEN ASSUME_TAC th)
2297 THEN POP_ASSUM MP_TAC
2298 THEN ASM_REWRITE_TAC[VECTOR_ARITH`z = (&1 - &1) % y + &1 % v <=> z=v `]
2299 THEN ASM_TAC THEN REAL_ARITH_TAC;(*13*)
2300
2301
2302 STRIP_TAC
2303 THEN  MP_TAC(SET_RULE`  a dot z < b ==> z IN {x:real^3 | a dot x < b}`)
2304 THEN RESA_TAC
2305 THEN MRESA_TAC POLYHEDRON_HYPERPLANE[`a':real^3`;`b1:real`]
2306 THEN MRESA_TAC POLYHEDRON_INTER[`p:real^3->bool`;`{x:real^3 | a' dot x = b1}`]
2307 THEN MRESAL_TAC BOUNDED_SUBSET[`p INTER {x:real^3 | a' dot x = b1}`;`p:real^3->bool`;][SET_RULE`p INTER {x:real^3 | a' dot x = b1} SUBSET p`]
2308 THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p':real^3->bool`
2309 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p':real^3->bool`
2310 THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`p':real^3->bool`
2311 THEN MRESA1_TAC KREIN_MILMAN_MINKOWSKI `p':real^3->bool`
2312 THEN POP_ASSUM (fun th-> MP_TAC(SYM th))
2313 THEN STRIP_TAC
2314 THEN DISJ_CASES_TAC(SET_RULE` ({x:real^3 | x extreme_point_of p'} SUBSET {x | a dot x>=b}) \/ (?w. w extreme_point_of p' /\ ~(w IN  {x | a dot x>=b})) `)
2315 THENL(*14*)[
2316
2317 MRESA_TAC CONVEX_HALFSPACE_GE[`a:real^3`;`b:real`]
2318 THEN  MRESA_TAC SUBSET_HULL [`convex:(real^3->bool)->bool`;`{x:real^3 | x extreme_point_of p'}`;`{x | a dot x >= b}:real^3->bool`]
2319 THEN MP_TAC(SET_RULE`convex hull {x:real^3 | x extreme_point_of p'} SUBSET {x | a dot x >= b}
2320 /\ p' = convex hull {x | x extreme_point_of p'} /\ z IN p' ==> a dot z>= b`)
2321 THEN RESA_TAC
2322 THEN ASM_TAC
2323 THEN REAL_ARITH_TAC;(*14*)
2324
2325 POP_ASSUM MP_TAC
2326 THEN REWRITE_TAC[IN_ELIM_THM;REAL_ARITH`~(a>=b)<=> a< b`]
2327 THEN STRIP_TAC
2328 THEN MP_TAC(SET_RULE`  a dot w < b ==> w IN {x:real^3 | a dot x < b}`)
2329 THEN RESA_TAC
2330 THEN ABBREV_TAC`p1= p INTER {x:real^3| a' dot x >= b1}`
2331 THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
2332 THEN MRESA1_TAC POLYTOPE_IMP_CLOSED`p:real^3->bool`
2333 THEN MRESA1_TAC CLOSURE_CLOSED`p:real^3->bool`
2334 THEN MRESAL_TAC IN_INTERIOR_CLOSURE_CONVEX_SEGMENT[`p:real^3->bool`;`y:real^3`;`v:real^3`][SET_RULE`v IN p<=> {v} SUBSET p`; SET_RULE`A INTER B SUBSET A`]
2335 THEN MRESA_TAC CONVEX_HALFSPACE_GE[`a':real^3`;`b1:real`]
2336 THEN MRESA_TAC CLOSED_HALFSPACE_GE[`a':real^3`;`b1:real`]
2337 THEN MRESA1_TAC CLOSURE_CLOSED`{x:real^3| a' dot x >= b1}:real^3->bool`
2338 THEN MRESA_TAC INTERIOR_HALFSPACE_GE[`a':real^3`;`b1:real`]
2339 THEN MP_TAC(SET_RULE`{v:real^3} = p INTER {x | a' dot x = b'}==> a' dot v = b'`)
2340 THEN RESA_TAC
2341 THEN MP_TAC(SET_RULE`z IN segment [y,v:real^3] INTER {x | a' dot x = b1}==> a' dot z = b1`)
2342 THEN RESA_TAC
2343 THEN MRESAL_TAC IN_INTERIOR_CLOSURE_CONVEX_SEGMENT[`{x:real^3| a' dot x >= b1}:real^3->bool`;`v:real^3`;`z:real^3`][IN_ELIM_THM; REAL_ARITH`a>b<=> b<a`;REAL_ARITH`b>=b`; ]
2344 THEN POP_ASSUM MP_TAC
2345 THEN REWRITE_TAC[REAL_ARITH`a< b<=> b> a`]
2346 THEN STRIP_TAC
2347 THEN MRESA_TAC SUBSET_SEGMENT_OPEN_CLOSED [`v:real^3`;`z:real^3`;`y:real^3`;`v:real^3`]
2348 THEN POP_ASSUM MP_TAC
2349 THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SUBSET_SEGMENT]
2350 THEN ASM_REWRITE_TAC[ENDS_IN_SEGMENT]
2351 THEN STRIP_TAC
2352 THEN MP_TAC(SET_RULE`segment (v,z) SUBSET segment (y,v) /\  segment (y,v) SUBSET interior (p:real^3->bool)==> segment (v,z) SUBSET interior p`)
2353 THEN RESA_TAC
2354 THEN FIND_ASSUM MP_TAC`~(z = v:real^3)`
2355 THEN REWRITE_TAC[GSYM SEGMENT_EQ_EMPTY;SEGMENT_SYM;SET_RULE`~(A={})<=> ?v1. v1 IN A`]
2356 THEN STRIP_TAC
2357 THEN SUBGOAL_THEN` v1:real^3 IN interior p1`ASSUME_TAC
2358 THENL(*15*)[
2359
2360 EXPAND_TAC"p1"
2361 THEN REWRITE_TAC[INTERIOR_INTER]
2362 THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM]
2363 THEN ASM_TAC
2364 THEN SET_TAC[];(*15*)
2365
2366
2367
2368 MRESAL_TAC POLYHEDRON_INTER[`p:real^3->bool`;`{x:real^3| a' dot x >= b1}`][POLYHEDRON_HALFSPACE_GE]
2369 THEN MRESAL_TAC BOUNDED_SUBSET[`p INTER {x:real^3| a' dot x >= b1} `;`p:real^3->bool`;][SET_RULE`(A INTER B) SUBSET A`]
2370 THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p1:real^3->bool`
2371 THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`p1:real^3->bool`
2372 THEN MRESA_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_GE[`p1:real^3->bool`;`a':real^3`;`b1:real`]
2373 THEN POP_ASSUM MP_TAC
2374 THEN EXPAND_TAC"p1"
2375 THEN GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o DEPTH_CONV)[INTER;IN_ELIM_THM]
2376 THEN ASM_REWRITE_TAC[IN_ELIM_THM;SET_RULE`(!x. x IN p /\ a' dot x >= b1 ==> a' dot x >= b1)`]
2377 THEN SUBGOAL_THEN`p1 INTER {x:real^3 | a' dot x = b1}= p'`ASSUME_TAC
2378 THENL(*16*)[
2379
2380 EXPAND_TAC"p1"
2381 THEN REWRITE_TAC[INTER;IN_ELIM_THM;SET_RULE`(A INTER B) INTER C= A INTER (B INTER C)`
2382 ; REAL_ARITH`(a>=b /\ a=b) <=>  a = b`]
2383 THEN ASM_TAC
2384 THEN REWRITE_TAC[INTER;IN_ELIM_THM]
2385 THEN REPEAT RESA_TAC;(*16*)
2386
2387 ASM_REWRITE_TAC[]
2388 THEN STRIP_TAC
2389 THEN MRESA_TAC EXPOSED_FACE_OF_POLYHEDRON[`p1:real^3->bool`;`p':real^3->bool`]
2390 THEN MRESA_TAC FACE_OF_SING[`w:real^3`;`p':real^3->bool`]
2391 THEN MRESA_TAC EXPOSED_FACE_OF_POLYHEDRON[`p':real^3->bool`;`{w}:real^3->bool`]
2392 THEN POP_ASSUM MP_TAC
2393 THEN REWRITE_TAC[exposed_face_of]
2394 THEN STRIP_TAC
2395 THEN POP_ASSUM MP_TAC
2396 THEN DISCH_THEN(LABEL_TAC"LINH10")
2397 THEN ABBREV_TAC`a2= (v-w:real^3) cross (a''' cross a')`
2398 THEN ABBREV_TAC`b2= a2 dot w:real^3`
2399 THEN SUBGOAL_THEN`{x| a' dot x =b1} INTER {x | a''' dot x <= b''}= {x| a' dot x =b1} INTER  {x:real^3 | a2 dot x <= b2}`ASSUME_TAC
2400 THENL(*17*)[
2401
2402 REWRITE_TAC[INTER;IN_ELIM_THM]
2403 THEN EXPAND_TAC "b2"
2404 THEN EXPAND_TAC "a2"
2405 THEN REWRITE_TAC[CROSS_LADD;VECTOR_ARITH`A-B=A+(-- B:real^3)`;DOT_LADD;CROSS_LNEG;DOT_LNEG;DOT_CROSS_SELF;]
2406 THEN REWRITE_TAC[CROSS_LAGRANGE;DOT_LSUB;DOT_LMUL;EXTENSION;IN_ELIM_THM]
2407 THEN GEN_TAC
2408 THEN EQ_TAC
2409 THENL(*18*)[
2410
2411
2412 RESA_TAC
2413 THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
2414 /\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
2415 THEN RESA_TAC
2416 THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) <=
2417  b' * b'' - (a''' dot v) * b1 + -- &0
2418 <=>
2419 &0<= ( b'-b1) * (b''- a''' dot x)
2420 `]
2421 THEN MATCH_MP_TAC REAL_LE_MUL
2422 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= a-b<=> b<=a`]
2423 THEN ASM_TAC
2424 THEN REAL_ARITH_TAC;(*18*)
2425
2426 RESA_TAC
2427 THEN POP_ASSUM MP_TAC
2428 THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
2429 /\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
2430 THEN RESA_TAC
2431 THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) <=
2432  b' * b'' - (a''' dot v) * b1 + -- &0
2433 <=>
2434 &0<= ( b'-b1) * (b''- a''' dot x)
2435 `]
2436 THEN STRIP_TAC
2437 THEN MP_TAC(ARITH_RULE`b1< b' ==> ~(b'- b1= &0) /\ &0< b'-b1`)
2438 THEN RESA_TAC
2439 THEN MRESA1_TAC REAL_MUL_LINV`b'-b1:real`
2440 THEN MRESA1_TAC REAL_LT_INV_EQ`b'-b1:real`
2441 THEN MP_TAC(ARITH_RULE` &0< inv(b'-b1)==> &0<= inv(b'- b1)`)
2442 THEN RESA_TAC
2443 THEN MRESAL_TAC REAL_LE_MUL[`inv(b'-b1)`;`(b' - b1) * (b'' - a''' dot (x:real^3))`][REAL_ARITH`A*B*C=(A*B)*C`;REAL_ARITH`&1*A=A`]
2444 THEN POP_ASSUM MP_TAC
2445 THEN REAL_ARITH_TAC](*18*);(*17*)
2446
2447
2448 SUBGOAL_THEN`{x| a' dot x =b1} INTER {x | a''' dot x = b''}= {x| a' dot x =b1} INTER  {x:real^3 | a2 dot x = b2}`ASSUME_TAC
2449 THENL(*18*)[
2450
2451 REWRITE_TAC[INTER;IN_ELIM_THM]
2452 THEN EXPAND_TAC "b2"
2453 THEN EXPAND_TAC "a2"
2454 THEN REWRITE_TAC[CROSS_LADD;VECTOR_ARITH`A-B=A+(-- B:real^3)`;DOT_LADD;CROSS_LNEG;DOT_LNEG;DOT_CROSS_SELF;]
2455 THEN REWRITE_TAC[CROSS_LAGRANGE;DOT_LSUB;DOT_LMUL;EXTENSION;IN_ELIM_THM]
2456 THEN GEN_TAC
2457 THEN EQ_TAC
2458 THENL(*19*)[
2459
2460 RESA_TAC
2461 THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
2462 /\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
2463 THEN RESA_TAC
2464 THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) =
2465  b' * b'' - (a''' dot v) * b1 + -- &0
2466 <=>
2467 &0= ( b'-b1) * (b''- a''' dot x)
2468 `]
2469 THEN REAL_ARITH_TAC;(*19*)
2470
2471 RESA_TAC
2472 THEN POP_ASSUM MP_TAC
2473 THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
2474 /\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
2475 THEN RESA_TAC
2476 THEN MP_TAC(ARITH_RULE`b1< b' ==> ~(b'- b1= &0) `)
2477 THEN RESA_TAC
2478 THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) =
2479  b' * b'' - (a''' dot v) * b1 + -- &0
2480 <=>
2481  ( b'-b1) * (b''- a''' dot x) = &0
2482 `;REAL_ENTIRE]
2483 THEN REAL_ARITH_TAC](*19*);(*18*)
2484
2485
2486
2487
2488 REMOVE_THEN "LINH10" MP_TAC
2489 THEN EXPAND_TAC"p'"
2490 THEN REWRITE_TAC[SET_RULE`(A INTER B) INTER C=A INTER(B INTER C)`]
2491 THEN ASM_REWRITE_TAC[]
2492 THEN ASM_REWRITE_TAC[SET_RULE`A INTER(B INTER C)= (A INTER B) INTER C`]
2493 THEN MP_TAC(SET_RULE`p' SUBSET {x | a''' dot x <= b''} /\ p1 INTER {x | a' dot x = b1} = p' ==> p' SUBSET {x:real^3 | a' dot x = b1} INTER {x | a''' dot x <= b''} `)
2494 THEN RESA_TAC
2495 THEN MP_TAC(SET_RULE`p' SUBSET {x | a' dot x = b1} INTER {x | a2 dot x <= b2}
2496 ==> p' SUBSET  {x:real^3 | a2 dot x <= b2}`)
2497 THEN RESA_TAC
2498 THEN RESA_TAC
2499 THEN SUBGOAL_THEN`v IN {x:real^3 | a2 dot x = b2}`ASSUME_TAC
2500 THENL(*19*)[
2501
2502 REWRITE_TAC[IN_ELIM_THM]
2503 THEN EXPAND_TAC "b2"
2504 THEN EXPAND_TAC "a2"
2505 THEN REWRITE_TAC[CROSS_LADD;VECTOR_ARITH`A-B=A+(-- B:real^3)`;DOT_LADD;CROSS_LNEG;DOT_LNEG;DOT_CROSS_SELF;]
2506 THEN REWRITE_TAC[CROSS_LAGRANGE;DOT_LSUB;DOT_LMUL;EXTENSION;IN_ELIM_THM]
2507 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DOT_SYM]
2508 THEN REAL_ARITH_TAC;(*19*)
2509
2510
2511 SUBGOAL_THEN`!v3:real^3. v3 IN p /\ ~(v3=v)==> ?v4. v4 IN p' /\ v4 IN aff_ge {v} {v3}`ASSUME_TAC
2512 THENL(*10*)[
2513
2514 REPEAT STRIP_TAC
2515 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool`
2516 THEN MRESAL1_TAC KREIN_MILMAN_MINKOWSKI`p:real^3->bool`[GSYM vertices]
2517 THEN MP_TAC(SET_RULE`(v3:real^3) IN p /\ (p:real^3->bool) = convex hull vertices p ==> v3 IN convex hull vertices p`)
2518 THEN ASM_REWRITE_TAC[]
2519 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
2520 THEN ASM_REWRITE_TAC[CONVEX_HULL_EXPLICIT;IN_ELIM_THM]
2521 THEN STRIP_TAC
2522 THEN ABBREV_TAC`s1= s' DELETE (v:real^3)`
2523 THEN MRESA_TAC FINITE_DELETE[`s':real^3->bool`;`v:real^3`]
2524 THEN ABBREV_TAC`v12=vsum s1 (\v:real^3. u v % v)`
2525 THEN ABBREV_TAC`t12=sum (s1:real^3->bool) (u:real^3->real)`
2526 THEN MP_TAC(SET_RULE`(!x. x IN s' ==> &0 <= u x) ==>(!x:real^3. x IN s' DELETE v ==> &0 <= u x)`)
2527 THEN RESA_TAC
2528 THEN MRESA_TAC SUM_POS_LE[`u:real^3->real`;`s1:real^3->bool`]
2529 THEN MP_TAC(REAL_ARITH`&0<= t12==> t12= &0 \/ &0< t12`)
2530 THEN RESA_TAC
2531 THENL(*11*)[
2532
2533 MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
2534 THEN MP_TAC(SET_RULE`&0 = (if (v:real^3) IN s' then &1 - (u:real^3->real) v else &1) /\ ~(&0= &1)==> v IN s' /\ &1- u v= &0`)
2535 THEN REWRITE_TAC[REAL_ARITH`~(&0= &1) `;REAL_ARITH`A- B= &0<=> B=A` ]
2536 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2537 THEN RESA_TAC
2538 THEN MRESA_TAC VSUM_DELETE_CASES[`v:real^3`;`(\v:real^3. (u:real^3->real) v % v)`;`s':real^3->bool`]
2539 THEN MRESA_TAC SUM_POS_EQ_0[`u:real^3->real`;`s1:real^3->bool`]
2540 THEN SUBGOAL_THEN`(!x:real^3. x IN s1 ==> (u x) % x = vec 0)`ASSUME_TAC
2541 THENL(*12*)[
2542
2543 POP_ASSUM MP_TAC
2544 THEN DISCH_THEN(LABEL_TAC"LINH")
2545 THEN REPEAT STRIP_TAC
2546 THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`x:real^3`)
2547 THEN VECTOR_ARITH_TAC;(*12*)
2548
2549 MRESAL_TAC VSUM_EQ_0[`(\v. (u:real^3->real) v % v)`;`s1:real^3->bool`][VECTOR_ARITH`v3 - &1 % v = vec 0 <=> v3=v`]](*12*);(*11*)
2550
2551
2552 SUBGOAL_THEN`(inv t12) % v12 IN p:real^3->bool`ASSUME_TAC
2553 THENL(*12*)[
2554
2555 MRESAL1_TAC KREIN_MILMAN_MINKOWSKI`p:real^3->bool`[GSYM vertices]
2556 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th;])
2557 THEN ASM_REWRITE_TAC[CONVEX_HULL_EXPLICIT;IN_ELIM_THM]
2558 THEN MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
2559 THEN RESA_TAC
2560 THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
2561 THEN EXISTS_TAC`s1:real^3->bool`
2562 THEN EXISTS_TAC`(\v. inv(t12) * (u:real^3->real) v)`
2563 THEN ASM_REWRITE_TAC[SUM_LMUL;VECTOR_ARITH`(a*b) %v=a%(b%v)`;VSUM_LMUL]
2564 THEN MP_TAC(SET_RULE`s1= s' DELETE v:real^3 /\ s' SUBSET vertices p ==> s1 SUBSET vertices p`)
2565 THEN RESA_TAC
2566 THEN REPEAT STRIP_TAC
2567 THEN MATCH_MP_TAC REAL_LE_MUL
2568 THEN ASM_REWRITE_TAC[REAL_LE_INV_EQ]
2569 THEN POP_ASSUM MP_TAC
2570 THEN ASM_REWRITE_TAC[];(*12*)
2571
2572
2573
2574
2575 SUBGOAL_THEN`a' dot inv t12 % v12:real^3 <= b1`ASSUME_TAC
2576 THENL(*13*)[
2577
2578 EXPAND_TAC"v12"
2579 THEN REWRITE_TAC[GSYM VSUM_LMUL]
2580 THEN MRESA_TAC DOT_RSUM[`s1:real^3->bool`;`(\x:real^3. inv t12 % u x % x)`;`a':real^3`]
2581 THEN REWRITE_TAC[DOT_RMUL]
2582 THEN SUBGOAL_THEN`!x:real^3. x IN s1 ==> (\y. inv t12 * u y * (a' dot y)) x<= (\y. inv t12 * u y * b1) x` ASSUME_TAC
2583 THENL(*14*)[
2584
2585 REPEAT STRIP_TAC
2586 THEN POP_ASSUM MP_TAC
2587 THEN EXPAND_TAC"s1"
2588 THEN REWRITE_TAC[DELETE;IN_ELIM_THM]
2589 THEN STRIP_TAC
2590 THEN MP_TAC(SET_RULE`vertices p INTER {x:real^3 | a' dot x >= b1} = {v:real^3} /\ x IN s' /\ s' SUBSET vertices p /\ ~(x=v) ==> ~(a' dot x >= b1)`)
2591 THEN RESA_TAC
2592 THEN POP_ASSUM MP_TAC
2593 THEN REWRITE_TAC[REAL_ARITH`~(a>= b)<=> a<b`; REAL_ARITH`a*b*c=(a*b)*c`]
2594 THEN STRIP_TAC
2595 THEN MATCH_MP_TAC REAL_LE_LMUL
2596 THEN ASM_REWRITE_TAC[]
2597 THEN MP_TAC(REAL_ARITH`a' dot x < b1==> a' dot x:real^3 <= b1`)
2598 THEN RESA_TAC
2599 THEN MATCH_MP_TAC REAL_LE_MUL
2600 THEN ASM_REWRITE_TAC[REAL_LE_INV_EQ]
2601 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
2602 THEN POP_ASSUM MP_TAC
2603 THEN ASM_REWRITE_TAC[];(*14*)
2604
2605 MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
2606 THEN RESA_TAC
2607 THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
2608 THEN MRESA_TAC SUM_LE[`(\y:real^3. inv t12 * u y * (a' dot y))`;`(\y:real^3. inv t12 * u y * b1)`;`s1:real^3->bool`]
2609 THEN POP_ASSUM MP_TAC
2610 THEN REWRITE_TAC[REAL_ARITH`a*b*c= (a*c) *b`;]
2611 THEN ASM_REWRITE_TAC[SUM_LMUL; REAL_ARITH`(a*b)*c= b*(a*c)`; REAL_ARITH`a* &1=a` ]](*14*);(*13*)
2612
2613 SUBGOAL_THEN`~(inv t12 % v12= v:real^3)` ASSUME_TAC
2614 THENL(*14*)[
2615
2616 STRIP_TAC
2617 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2618 THEN POP_ASSUM MP_TAC
2619 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b)<=> b< a`];(*14*)
2620
2621 SUBGOAL_THEN `aff_ge {v:real^3} {inv t12 % v12}= aff_ge {v:real^3} {v3}` ASSUME_TAC
2622 THENL(*15*)[
2623
2624 MRESA_TAC AFF_GE_1_1[`v:real^3`;`inv t12 % v12:real^3`]
2625 THEN MRESA_TAC AFF_GE_1_1[`v:real^3`;`v3:real^3`]
2626 THEN EXPAND_TAC"v3"
2627 THEN MRESAL_TAC VSUM_DELETE_CASES[`v:real^3`;`(\v:real^3. (u:real^3->real) v % v)`;`s':real^3->bool`][VECTOR_ARITH`a= b-c<=> b=a+c:real^3`]
2628 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]
2629 THEN GEN_TAC
2630 THEN EQ_TAC
2631 THENL(*16*)[
2632
2633
2634 DISJ_CASES_TAC(SET_RULE`v IN (s':real^3->bool) \/ ~(v IN s')`)
2635 THENL(*17*)[
2636
2637 RESA_TAC
2638 THEN EXISTS_TAC`t1 - t2 * inv t12 * (u (v:real^3))`
2639 THEN EXISTS_TAC`t2* inv t12:real`
2640 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1 % v + t2 % inv t12 % (v3 - u v % v) =
2641  (t1 - t2 * inv t12 * u v) % v + (t2 * inv t12) % v3`;REAL_ARITH`t1 - t2 * inv t12 * u v + t2 * inv t12= t1 +t2 * inv t12 *(&1- u v)`]
2642 THEN MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
2643 THEN MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
2644 THEN RESA_TAC
2645 THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
2646 THEN ASM_REWRITE_TAC[REAL_ARITH`a* &1=a`]
2647 THEN MATCH_MP_TAC REAL_LE_MUL
2648 THEN ASM_REWRITE_TAC[]
2649 THEN MATCH_MP_TAC REAL_LE_INV
2650 THEN REMOVE_ASSUM_TAC
2651 THEN REMOVE_ASSUM_TAC
2652 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);(*17*)
2653
2654
2655
2656 MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
2657 THEN REWRITE_TAC[VECTOR_ARITH`a % inv (&1) %v=a %v`]](*17*);(*16*)
2658
2659 DISJ_CASES_TAC(SET_RULE`v IN (s':real^3->bool) \/ ~(v IN s')`)
2660 THENL(*17*)[
2661
2662 ASM_REWRITE_TAC[VECTOR_ARITH`t1 % v + t2 % inv t12 % (v3 - u v % v)= (t1 - t2 * inv t12 * u v) %v+ (inv t12 * t2)% v3`]
2663 THEN STRIP_TAC
2664 THEN EXISTS_TAC`&1- t12 * t2:real`
2665 THEN EXISTS_TAC`t12 * t2:real`
2666 THEN ASM_REWRITE_TAC[REAL_ARITH`&1- a+a= &1`;]
2667 THEN MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
2668 THEN RESA_TAC
2669 THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
2670 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 *a=a`;REAL_ARITH`a * b * c=(a*b)*c`]
2671 THEN ASM_REWRITE_TAC[REAL_ARITH`((a*b)*c)*d=(c*a)*(b*d)`;REAL_ARITH`&1 *a=a`;REAL_ARITH`&1- a*b-b*c= &1- (c+a)*b`]
2672 THEN MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
2673 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - (u v + &1 - u v) * t2) = &1-(t1+t2) +t1`;REAL_ARITH`&1- &1+a=a`]
2674 THEN MATCH_MP_TAC REAL_LE_MUL
2675 THEN ASM_REWRITE_TAC[]
2676 THEN POP_ASSUM (fun th-> ASM_REWRITE_TAC[SYM th]);(*17*)
2677
2678 MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
2679 THEN REWRITE_TAC[VECTOR_ARITH`a % inv (&1) %v=a %v`]](*17*)](*16*);(*15*)
2680
2681
2682 ABBREV_TAC`v31=inv t12 % (v12:real^3)`
2683 THEN MP_TAC(REAL_ARITH`(a':real^3) dot v31<= b1 ==> a' dot v31:real^3< b1\/ a' dot v31 = b1`)
2684 THEN RESA_TAC
2685 THENL(*16*)[
2686
2687
2688 SUBGOAL_THEN`?z. z IN segment[v31,v:real^3] INTER {x| a' dot x= b1} /\ ~(z= v)` ASSUME_TAC
2689 THENL(*17*)[
2690
2691 MP_TAC(SET_RULE`vertices p INTER {x | a' dot x >= b1} = {v:real^3} ==> v IN {x | a' dot x >= b1}`)
2692 THEN RESA_TAC
2693 THEN REWRITE_TAC[INTER;IN_SEGMENT;IN_ELIM_THM]
2694 THEN ASM_TAC
2695 THEN REWRITE_TAC[IN_ELIM_THM]
2696 THEN REPEAT RESA_TAC
2697 THEN  MP_TAC(REAL_ARITH`a' dot v31 < b1 /\ a' dot v >= b1 /\ a' dot v = b' /\ b1< b' ==> &0< a' dot v - a' dot (v31:real^3) /\ &0< b1- a' dot v31 /\ b1- a' dot v31 < a' dot v - a' dot (v31:real^3) /\ ~(a' dot v - a' dot (v31:real^3)= &0)`)
2698 THEN RESA_TAC
2699 THEN MRESA1_TAC REAL_LT_INV`a' dot v - a' dot (v31:real^3)`
2700 THEN MRESA_TAC REAL_LT_MUL[`inv(a' dot v - a' dot (v31:real^3))`;`b1 - a' dot (v31:real^3)`]
2701 THEN MP_TAC(REAL_ARITH`&0< inv(a' dot v - a' dot (v31:real^3))==> &0<= inv(a' dot v - a' dot (v31:real^3))`)
2702 THEN RESA_TAC
2703 THEN MRESA1_TAC REAL_MUL_LINV`a' dot v - a' dot (v31:real^3)`
2704 THEN MRESA_TAC REAL_LT_LMUL[`inv(a' dot v - a' dot (v31:real^3))`;`b1 - a' dot (v31:real^3)`;`a' dot v - a' dot (v31:real^3)`]
2705 THEN EXISTS_TAC`(&1- inv (a' dot v - a' dot v31) * (b1 - a' dot v31)) % (v31:real^3)+ (inv (a' dot v - a' dot v31) * (b1 - a' dot v31))% v`
2706 THEN REWRITE_TAC[DOT_RMUL; DOT_RADD; REAL_ARITH`(&1- b)* c+b * d=a<=>b*(d-c)= a- c`;]
2707 THEN ASM_REWRITE_TAC[ REAL_ARITH`(a*b)*c= b*(a*c)`; REAL_ARITH`a * &1= a`]
2708 THEN STRIP_TAC
2709 THENL(*18*)[
2710
2711
2712  EXISTS_TAC`inv (a' dot v - a' dot v31) * (b1 - a' dot (v31:real^3))`
2713 THEN ASM_REWRITE_TAC[]
2714 THEN ASM_TAC
2715 THEN REAL_ARITH_TAC;(*18*)
2716
2717 REWRITE_TAC[VECTOR_ARITH`(&1- b)%a + b % v= v<=> (&1-b)%(a-v)= vec 0`;VECTOR_MUL_EQ_0]
2718 THEN STRIP_TAC
2719 THENL(*19*)[
2720
2721 ASM_TAC THEN REAL_ARITH_TAC;(*19*)
2722
2723
2724 POP_ASSUM MP_TAC
2725 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0 <=> A=B`]](*19*)](*18*);(*17*)
2726
2727 POP_ASSUM MP_TAC
2728 THEN STRIP_TAC
2729 THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f /\ f SUBSET p/\ v31 IN p==> {v,v31} SUBSET p `)
2730 THEN RESA_TAC
2731 THEN  MRESAL_TAC SUBSET_HULL [`convex:(real^3->bool)->bool`;`{v,v31:real^3}`;`p:real^3->bool`] [GSYM
2732 SEGMENT_CONVEX_HULL;]
2733 THEN MRESA_TAC SEGMENT_SUBSET_HALFLINE[`v:real^3`;`v31:real^3`]
2734 THEN EXISTS_TAC`z':real^3`
2735 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
2736 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
2737 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
2738 THEN ASM_TAC
2739 THEN SET_TAC[]](*17*);(*16*)
2740
2741
2742 EXISTS_TAC`v31:real^3`
2743 THEN MP_TAC(SET_RULE`a' dot v31 = b1 /\ v31 IN p ==> v31 IN p INTER {x:real^3| a' dot x= b1}`)
2744 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1`]
2745 THEN RESA_TAC
2746 THEN MRESA_TAC point_in_aff_ge_1_1[`v:real^3`;`v31:real^3`]](*16*)](*15*)](*14*)](*13*)](*12*)](*11*);(*10*)
2747
2748
2749 SUBGOAL_THEN`p SUBSET {x:real^3| a2 dot x <= b2}` ASSUME_TAC
2750 THENL(*11*)[
2751
2752 POP_ASSUM MP_TAC
2753 THEN DISCH_THEN(LABEL_TAC"LINH")
2754 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
2755 THEN GEN_TAC
2756 THEN STRIP_TAC
2757 THEN DISJ_CASES_TAC(SET_RULE`x=v \/ ~(x=v:real^3)`)
2758 THENL(*12*)[
2759
2760 ASM_TAC
2761 THEN REWRITE_TAC[IN_ELIM_THM]
2762 THEN REPEAT STRIP_TAC
2763 THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`];(*12*)
2764
2765 MRESA_TAC AFF_GE_1_1[`v:real^3`;`x:real^3`]
2766 THEN REMOVE_THEN "LINH" (fun th-> MRESAL1_TAC th`x:real^3`[IN_ELIM_THM])
2767 THEN MP_TAC(SET_RULE`v4 IN p' /\p' SUBSET {x:real^3 | a2 dot x <= b2} ==> a2 dot v4<= b2`)
2768 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL]
2769 THEN ASM_TAC
2770 THEN REWRITE_TAC[IN_ELIM_THM]
2771 THEN REPEAT STRIP_TAC
2772 THEN POP_ASSUM MP_TAC
2773 THEN ASM_REWRITE_TAC[REAL_ARITH`t1 * b2 + t2 * (a2 dot x) <= b2<=>  t2 * (a2 dot x) <= (t2+ &1 -(t1+t2))*b2`; REAL_ARITH`a + &1- &1=a`]
2774 THEN POP_ASSUM MP_TAC
2775 THEN POP_ASSUM MP_TAC
2776 THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0< t2`)
2777 THEN RESA_TAC
2778 THENL(*13*)[
2779
2780 ASM_REWRITE_TAC[REAL_ARITH`t1+ &0= &1<=> t1= &1`]
2781 THEN RESA_TAC
2782 THEN ASM_REWRITE_TAC[VECTOR_ARITH`v4 = &1 % v + &0 % x<=> v4=v`]
2783 THEN STRIP_TAC
2784 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2785 THEN MP_TAC(SET_RULE`v IN p' /\ p INTER {x:real^3 | a' dot x = b1}= p' ==> a' dot v =b1`)
2786 THEN RESA_TAC
2787 THEN ASM_TAC
2788 THEN REAL_ARITH_TAC;(*13*)
2789
2790 REPEAT STRIP_TAC
2791 THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)`)
2792 THEN RESA_TAC
2793 THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
2794 THEN MRESAL_TAC REAL_LE_LMUL[`inv t2`;`t2 * (a2 dot (x:real^3))`;`t2 * b2`][REAL_LE_INV_EQ;REAL_ARITH`a*b*c=(a*b)*c`;REAL_ARITH`&1 * a=a`]
2795 ](*13*)](*12*);(*11*)
2796
2797
2798
2799
2800
2801 SUBGOAL_THEN`p INTER {x| a2 dot x = b2} SUBSET aff_ge {v:real^3} {w}`ASSUME_TAC
2802 THENL(*12*)[
2803 POP_ASSUM MP_TAC
2804 THEN POP_ASSUM MP_TAC
2805 THEN DISCH_THEN(LABEL_TAC"LINH")
2806 THEN STRIP_TAC
2807 THEN REWRITE_TAC[INTER;SUBSET;IN_ELIM_THM]
2808 THEN DISJ_CASES_TAC(SET_RULE`w=v \/ ~(v=(w:real^3))`)
2809 THENL(*13*)[
2810  MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a2 dot x = b2} /\ p INTER {x :real^3| a' dot x = b1} = p'==> a' dot w= b1`)
2811 THEN RESA_TAC
2812 THEN POP_ASSUM MP_TAC
2813 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2814 THEN ASM_TAC
2815 THEN REAL_ARITH_TAC;(*13*)
2816
2817 MRESAL_TAC AFF_GE_1_1[`v:real^3`;`w:real^3`][IN_ELIM_THM]
2818 THEN REPEAT STRIP_TAC
2819 THEN DISJ_CASES_TAC(SET_RULE`x=v \/ ~(x=(v:real^3))`)
2820 THENL(*14*)[
2821
2822 EXISTS_TAC`&1:real`
2823 THEN EXISTS_TAC`&0:real`
2824 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &0 /\ &1 + &0= &1`]
2825 THEN VECTOR_ARITH_TAC;(*14*)
2826
2827 MRESA_TAC AFF_GE_1_1[`v:real^3`;`x:real^3`]
2828 THEN REMOVE_THEN "LINH" (fun th-> MRESAL1_TAC th`x:real^3`[IN_ELIM_THM])
2829 THEN SUBGOAL_THEN`v4 IN {x:real^3 | a2 dot x=b2}` ASSUME_TAC
2830 THENL(*15*)[
2831
2832 ASM_REWRITE_TAC[IN_ELIM_THM;DOT_RADD;DOT_RMUL]
2833 THEN ASM_TAC
2834 THEN REWRITE_TAC[IN_ELIM_THM]
2835 THEN REPEAT STRIP_TAC
2836 THEN ASM_REWRITE_TAC[REAL_ARITH`t1 * b2 + t2 * b2 =(t1+ t2) * b2`]
2837 THEN REAL_ARITH_TAC;(*15*)
2838
2839 MP_TAC(SET_RULE`{w} = p' INTER {x | a2 dot x = b2} /\ v4 IN p'/\ v4 IN {x:real^3 | a2 dot x = b2}==> v4=w`)
2840 THEN RESA_TAC
2841 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN MP_TAC(SYM th))
2842 THEN POP_ASSUM MP_TAC
2843 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC )
2844 THEN POP_ASSUM MP_TAC
2845 THEN POP_ASSUM MP_TAC
2846 THEN POP_ASSUM MP_TAC
2847 THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0<t2`)
2848 THEN RESA_TAC
2849 THENL(*16*)[
2850
2851 ASM_REWRITE_TAC[REAL_ARITH`t1+ &0= &1<=> t1= &1`]
2852 THEN RESA_TAC
2853 THEN ASM_REWRITE_TAC[VECTOR_ARITH`v4 = &1 % v + &0 % x<=> v4=v`]
2854 THEN STRIP_TAC
2855 THEN STRIP_TAC
2856 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC);(*16*)
2857
2858 REPEAT RESA_TAC
2859 THEN EXISTS_TAC`&1 - inv t2:real`
2860 THEN EXISTS_TAC`inv t2:real`
2861 THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)`)
2862 THEN RESA_TAC
2863 THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
2864 THEN ASM_REWRITE_TAC[REAL_ARITH`&1- a +a= &1`;REAL_LE_INV_EQ;VECTOR_ARITH`(&1 - inv t2) % v + inv t2 % (t1 % v + t2 % x)= (&1 - inv t2*(t2 + &1-(t1+t2))) % v + (inv t2 * t2) % x`;REAL_ARITH`a+ &1- &1=a`]
2865 THEN VECTOR_ARITH_TAC](*16*)](*15*)](*14*)](*13*);(*12*)
2866
2867
2868
2869
2870 SUBGOAL_THEN`aff_ge {v:real^3} {w}  SUBSET {x | a2 dot x = b2}` ASSUME_TAC
2871 THENL(*13*)[
2872
2873 DISJ_CASES_TAC(SET_RULE`w=v \/ ~(v=w:real^3)`)
2874 THENL(*14*)[
2875
2876  MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a2 dot x = b2} /\ p INTER {x :real^3| a' dot x = b1} = p'==> a' dot w= b1`)
2877 THEN RESA_TAC
2878 THEN POP_ASSUM MP_TAC
2879 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2880 THEN ASM_TAC
2881 THEN REAL_ARITH_TAC;(*14*)
2882
2883 MRESA_TAC AFF_GE_1_1[`v:real^3`;`w:real^3`]
2884 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
2885 THEN REPEAT STRIP_TAC
2886 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL]
2887 THEN ASM_TAC
2888 THEN REWRITE_TAC[IN_ELIM_THM]
2889 THEN REPEAT STRIP_TAC
2890 THEN ASM_REWRITE_TAC[REAL_ARITH`a*b+c*b=(a+c)*b`;REAL_ARITH`&1 *a=a`]
2891 ](*14*);(*13*)
2892
2893 MP_TAC(SET_RULE`p INTER {x | a2 dot x = b2} SUBSET aff_ge {v} {w}
2894 /\ aff_ge {v} {w} SUBSET {x | a2 dot x = b2}/\ {v, y} SUBSET p
2895 ==>  aff_ge {v} {w} INTER p= p INTER {x:real^3 | a2 dot x = b2} /\ v IN p `)
2896 THEN RESA_TAC
2897 THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool`
2898 THEN MRESA_TAC HALFLINE_INTER_COMPACT_SEGMENT[`p:real^3->bool`;`v:real^3`;`w:real^3`]
2899 THEN MRESAL_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE_STRONG[`p:real^3->bool`;`a2:real^3`;`b2:real`][SET_RULE`(!x. x IN p ==> a2 dot x <= b2)<=> p SUBSET {x| a2 dot x<= b2}`;CONVEX_SEGMENT;SET_RULE`{a} SUBSET A<=> a IN A`]
2900 THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`c:real^3`]
2901 THEN MP_TAC(SET_RULE`p INTER {x | a2 dot x = b2} SUBSET aff_ge {v} {w}
2902 /\ p INTER {x | a2 dot x = b2} =segment[v,c] /\ c IN segment[v,c] ==> c IN aff_ge {v} {w:real^3}`)
2903 THEN ASM_REWRITE_TAC[ENDS_IN_SEGMENT]
2904 THEN DISJ_CASES_TAC(SET_RULE`w=v \/ ~(v=w:real^3)`)
2905 THENL(*14*)[
2906
2907  MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a2 dot x = b2} /\ p INTER {x :real^3| a' dot x = b1} = p'==> a' dot w= b1`)
2908 THEN RESA_TAC
2909 THEN POP_ASSUM MP_TAC
2910 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2911 THEN ASM_TAC
2912 THEN REAL_ARITH_TAC;(*14*)
2913
2914 MRESA_TAC AFF_GE_1_1[`v:real^3`;`w:real^3`]
2915 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
2916 THEN DISCH_TAC
2917 THEN EXISTS_TAC`c:real^3`
2918 THEN POP_ASSUM MP_TAC
2919 THEN ASM_REWRITE_TAC[edges; IN_ELIM_THM;vertices]
2920 THEN MP_TAC(SET_RULE`{w} = p' INTER {x | a2 dot x = b2} /\ p INTER {x | a' dot x = b1} = p' ==> w IN p INTER {x:real^3| a2 dot x = b2}`)
2921 THEN RESA_TAC
2922 THEN MP_TAC(SET_RULE`~(v:real^3 = w) /\ w IN segment [v,c] ==> ~(segment [v,c]={v})`)
2923 THEN REWRITE_TAC[SEGMENT_EQ_SING]
2924 THEN RESA_TAC
2925 THEN DISCH_TAC
2926 THEN STRIP_TAC
2927 THENL(*15*)[
2928
2929 POP_ASSUM MP_TAC
2930 THEN RESA_TAC
2931 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL]
2932 THEN POP_ASSUM MP_TAC
2933 THEN POP_ASSUM MP_TAC
2934 THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0< t2 `)
2935 THEN RESA_TAC
2936 THENL(*16*)[
2937
2938 REWRITE_TAC[REAL_ARITH`t+ &0= &1<=> t= &1`]
2939 THEN RESA_TAC
2940 THEN ASM_REWRITE_TAC[VECTOR_ARITH` &1 % v + &0 % w= v`];(*16*)
2941
2942 REPEAT STRIP_TAC
2943 THEN MRESA_TAC REAL_LT_LMUL[`t2:real`;`a dot w:real^3`;`b:real`]
2944 THEN MP_TAC(REAL_ARITH`t2 * (a dot w:real^3) < t2 * b ==> t1 * b+ t2 * (a dot w) < (t1+t2) * b`)
2945 THEN RESA_TAC
2946 THEN POP_ASSUM MP_TAC
2947 THEN REAL_ARITH_TAC](*16*);(*15*)
2948
2949 EXISTS_TAC`v:real^3`
2950 THEN EXISTS_TAC`c:real^3`
2951 THEN ASM_REWRITE_TAC[edge_of]
2952 THEN ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]
2953 THEN REWRITE_TAC[AFFINE_HULL_SEGMENT]
2954 THEN ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL;AFF_DIM_2]
2955 ]]]]]]]]]]]]]]]]]]]]]]]));;
2956
2957
2958
2959 let CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON=prove(`!p:real^3->bool.
2960          bounded p /\ polyhedron p /\ vec 0 IN interior p
2961 ==>  (!v. v IN vertices p ==>CARD (set_of_edge v (vertices p) (edges p)) >1)`,
2962 REPEAT STRIP_TAC
2963 THEN MRESA1_TAC EXISTS_EDGE_AT_VERTICES`p:real^3->bool`
2964 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`~(A={})<=> ?w. w IN A`])
2965 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
2966 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`;
2967 ` (v:real^3)`]
2968 THEN POP_ASSUM MP_TAC
2969 THEN RESA_TAC
2970 THEN MRESAL_TAC properties_coordinate[`((vec 0):real^3)`;` (v:real^3)`;` (w:real^3)`][VECTOR_ARITH`a - vec 0=a`]
2971 THEN ABBREV_TAC`a= e2_fan (vec 0) v (w:real^3)`
2972 THEN MRESA_TAC ORTHONORMAL_IMP_NONZERO [`e1_fan ((vec 0):real^3) (v:real^3) (w:real^3)`;`e2_fan ((vec 0):real^3) (v:real^3) (w:real^3)`;`e3_fan ((vec 0):real^3) (v:real^3) (w:real^3)`]
2973 THEN MRESAL_TAC FLVNSME[`v:real^3`;`{x:real^3| a dot x < &0}`;`a:real^3`;`&0`;`p:real^3->bool`][IN_ELIM_THM; DOT_RZERO]
2974 THEN POP_ASSUM MP_TAC
2975 THEN ONCE_REWRITE_TAC[DOT_SYM]
2976 THEN RESA_TAC
2977 THEN DISJ_CASES_TAC(SET_RULE`w =w' \/ ~(w= w':real^3)`)
2978 THENL[
2979 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REAL_ARITH_TAC);
2980 MRESA_TAC CARD_2_FAN[`w:real^3`;`w':real^3`]
2981 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w':real^3)`;
2982 ` (v:real^3)`]
2983 THEN MP_TAC(SET_RULE`w' IN set_of_edge v (vertices p) (edges p) /\ w IN set_of_edge v (vertices p) (edges p)
2984 ==> {w,w':real^3} SUBSET set_of_edge v (vertices p) (edges p)`)
2985 THEN RESA_TAC
2986 THEN MRESA_TAC CARD_SUBSET[`{w,w':real^3}`;`set_of_edge v (vertices p) (edges (p:real^3->bool))`]
2987 THEN POP_ASSUM MP_TAC
2988 THEN ARITH_TAC]);;
2989
2990
2991 let BSXAQBQ=prove(`!p:real^3->bool x.
2992          bounded p /\ polyhedron p /\ vec 0 IN interior p
2993 /\ x IN d_fan((vec 0),(vertices p),(edges p))
2994 ==> azim_fan (vec 0) (vertices p) (edges p) (pr2 x) (pr3 x) < pi`,
2995
2996 REPEAT STRIP_TAC
2997 THEN POP_ASSUM MP_TAC
2998 THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
2999 THEN POP_ASSUM MP_TAC
3000 THEN DISCH_THEN(LABEL_TAC"LINH")
3001 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
3002 THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
3003 THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
3004 THEN RESA_TAC
3005 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`;
3006 ` (v:real^3)`]
3007 THEN REMOVE_ASSUM_TAC
3008 THEN REMOVE_THEN"LINH"(fun th-> MP_TAC(ISPEC `v:real^3` th))
3009 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
3010 THEN RESA_TAC
3011 THEN ASM_REWRITE_TAC[azim_fan;pr2;pr3]
3012 THEN ABBREV_TAC`a= v cross w:real^3`
3013 THEN MRESAL_TAC FLVNSME[`v:real^3`;`{x:real^3| (-- a) dot x < &0}`;`(-- a):real^3`;`&0`;`p:real^3->bool`][IN_ELIM_THM; DOT_LNEG; DOT_RZERO; VECTOR_ARITH`((-- A:real^3)= vec 0) <=> (A = vec 0)`;REAL_ARITH`(-- a= &0) <=> (a= &0)`]
3014 THEN POP_ASSUM MP_TAC
3015 THEN ONCE_REWRITE_TAC[DOT_SYM]
3016 THEN REWRITE_TAC[REAL_ARITH`-- a< &0<=> &0< a`]
3017 THEN EXPAND_TAC"a"
3018 THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF]
3019 THEN RESA_TAC
3020 THEN DISJ_CASES_TAC(SET_RULE`w =w' \/ ~(w'= w:real^3)`)
3021 THENL[
3022 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
3023 THEN POP_ASSUM MP_TAC
3024 THEN EXPAND_TAC"a"
3025 THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF]
3026 THEN REAL_ARITH_TAC;
3027  MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w':real^3)`;
3028 ` (v:real^3)`]
3029 THEN MP_TAC(SET_RULE`w' IN set_of_edge v (vertices p) (edges p) /\ w IN set_of_edge v (vertices p) (edges p)/\ ~(w'=w:real^3)
3030 ==> ~( set_of_edge v (vertices p) (edges p)= {w})`)
3031 THEN RESA_TAC
3032 THEN MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (v:real^3)`;
3033 ` (w:real^3)`]
3034 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w':real^3`)
3035 THEN MRESA_TAC JBDNJJB[`v:real^3`;`w:real^3`;`w':real^3`]
3036 THEN MRESA_TAC REAL_LT_MUL[`t:real`;`a dot w':real^3`]
3037 THEN POP_ASSUM MP_TAC
3038 THEN POP_ASSUM(fun th->  ASM_REWRITE_TAC[SYM th;])
3039 THEN ONCE_REWRITE_TAC[DOT_SYM]
3040 THEN RESA_TAC
3041 THEN MP_TAC(REAL_ARITH`azim (vec 0) v w w' < &2 * pi ==> (&0 <= azim (vec 0) v w w' -pi /\ azim (vec 0) v w w' - pi <= pi) \/ azim (vec 0) v w w'< pi`)
3042 THEN ASM_REWRITE_TAC[azim]
3043 THEN STRIP_TAC
3044 THENL[
3045 MRESA1_TAC SIN_POS_PI_LE`azim (vec 0) v w w' - pi`
3046 THEN POP_ASSUM MP_TAC
3047 THEN ASM_REWRITE_TAC[SIN_SUB; SIN_PI;COS_PI; REAL_ARITH`&0<= a * -- &1- b * &0<=> ~( &0< a)`];
3048  ASM_TAC
3049 THEN REAL_ARITH_TAC]]);;
3050
3051
3052
3053 let POLYTOPE_FAN80=prove(`!p:real^3->bool.
3054          bounded p /\ polyhedron p /\ vec 0 IN interior p
3055 ==> fan80 (vec 0,vertices p,edges p)`,
3056
3057 REWRITE_TAC[fan80]
3058 THEN REPEAT  GEN_TAC
3059 THEN STRIP_TAC
3060 THEN REPEAT  GEN_TAC
3061 THEN STRIP_TAC
3062 THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
3063 THEN POP_ASSUM MP_TAC
3064 THEN DISCH_THEN(LABEL_TAC"LINH")
3065 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
3066 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (u:real^3)`;
3067 ` (v:real^3)`]
3068 THEN ABBREV_TAC`a= v cross u:real^3`
3069 THEN MRESAL_TAC FLVNSME[`v:real^3`;`{x:real^3| (-- a) dot x < &0}`;`(-- a):real^3`;`&0`;`p:real^3->bool`][IN_ELIM_THM; DOT_LNEG; DOT_RZERO; VECTOR_ARITH`((-- A:real^3)= vec 0) <=> (A = vec 0)`;REAL_ARITH`(-- a= &0) <=> (a= &0)`]
3070 THEN POP_ASSUM MP_TAC
3071 THEN ONCE_REWRITE_TAC[DOT_SYM]
3072 THEN REWRITE_TAC[REAL_ARITH`-- a< &0<=> &0< a`]
3073 THEN EXPAND_TAC"a"
3074 THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF]
3075 THEN RESA_TAC
3076 THEN DISJ_CASES_TAC(SET_RULE`u =w \/ ~(w= u:real^3)`)
3077 THENL[
3078 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
3079 THEN POP_ASSUM MP_TAC
3080 THEN EXPAND_TAC"a"
3081 THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF]
3082 THEN REAL_ARITH_TAC;
3083
3084
3085  MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`;
3086 ` (v:real^3)`]
3087 THEN MP_TAC(SET_RULE`w IN set_of_edge v (vertices p) (edges p) /\ u IN set_of_edge v (vertices p) (edges p)/\ ~(w=u:real^3)
3088 ==> ~( set_of_edge v (vertices p) (edges p)= {u})`)
3089 THEN RESA_TAC
3090 THEN MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (v:real^3)`;
3091 ` (u:real^3)`]
3092 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`)
3093 THEN MRESA_TAC JBDNJJB[`v:real^3`;`u:real^3`;`w:real^3`]
3094 THEN MRESA_TAC REAL_LT_MUL[`t:real`;`a dot w:real^3`]
3095 THEN POP_ASSUM MP_TAC
3096 THEN POP_ASSUM(fun th->  ASM_REWRITE_TAC[SYM th;])
3097 THEN ONCE_REWRITE_TAC[DOT_SYM]
3098 THEN RESA_TAC
3099 THEN MP_TAC(REAL_ARITH`azim (vec 0) v u w < &2 * pi ==> (&0 <= azim (vec 0) v u w -pi /\ azim (vec 0) v u w - pi <= pi) \/ azim (vec 0) v u w< pi`)
3100 THEN ASM_REWRITE_TAC[azim]
3101 THEN STRIP_TAC
3102 THENL[
3103
3104 MRESA1_TAC SIN_POS_PI_LE`azim (vec 0) v u w - pi`
3105 THEN POP_ASSUM MP_TAC
3106 THEN ASM_REWRITE_TAC[SIN_SUB; SIN_PI;COS_PI; REAL_ARITH`&0<= a * -- &1- b * &0<=> ~( &0< a)`];
3107 MP_TAC(REAL_ARITH`azim (vec 0) v u w < pi /\ azim (vec 0) v u (sigma_fan (vec 0) (vertices p) (edges p) v u) <= azim (vec 0) v u w ==> azim (vec 0) v u (sigma_fan (vec 0) (vertices p) (edges p) v u)< pi `)
3108 THEN RESA_TAC
3109 THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) v u (sigma_fan (vec 0) (vertices p) (edges p) v u) ==> (azim (vec 0) v u (sigma_fan (vec 0) (vertices p) (edges p) v u)= &0) \/ &0< azim (vec 0) v u (sigma_fan (vec 0) (vertices p) (edges p) v u)`)
3110 THEN ASM_REWRITE_TAC[azim]
3111 THEN STRIP_TAC
3112 THEN
3113  MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`(sigma_fan (vec 0) (vertices p) (edges p) v u):real^3`;
3114 ` (v:real^3)`]
3115 THEN  MRESA_TAC UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (v:real^3)`;
3116 ` (u:real^3)`; `(sigma_fan (vec 0) (vertices p) (edges p) v u):real^3`]]]);;
3117
3118
3119
3120
3121 let WBLARHH=prove(`!p:real^3->bool.
3122          bounded p /\ polyhedron p /\ vec 0 IN interior p
3123 ==>
3124  (!f. f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p)) ==> (?!f1. f1 facet_of p /\                                                          dartset_leads_into_fan (vec 0) (vertices p) (edges p) f = fchanged f1))`,
3125
3126 REPEAT STRIP_TAC
3127 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
3128 THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
3129 THEN POP_ASSUM MP_TAC
3130 THEN DISCH_THEN(LABEL_TAC"LINH")
3131 THEN MRESA1_TAC POLYTOPE_FAN80`p:real^3->bool`
3132 THEN MRESA_TAC dartset_leads_into_is_topological_component_yfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`f:real^3#real^3#real^3#real^3->bool`]
3133 THEN ABBREV_TAC`s= dartset_leads_into_fan (vec 0) (vertices p) (edges (p:real^3->bool)) f`
3134 THEN MRESAL_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;][conforming_fan;conforming_bijection_fan]
3135 THEN REMOVE_ASSUM_TAC
3136 THEN REMOVE_ASSUM_TAC
3137 THEN REMOVE_ASSUM_TAC
3138 THEN POP_ASSUM (fun th-> MRESA1_TAC th`s:real^3->bool`)
3139 THEN POP_ASSUM MP_TAC
3140 THEN MRESA1_TAC AMHFNXP`p:real^3->bool`
3141 THEN POP_ASSUM (fun th-> MRESA1_TAC th`s:real^3->bool`));;
3142
3143 let WBLARHH_BIJ = prove_by_refinement(
3144   `!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==>
3145  (BIJ
3146    (dartset_leads_into_fan (vec 0) (vertices p) (edges p))
3147    (face_set (hypermap1_of_fanx(vec 0,vertices p,edges p)))
3148    (topological_component_yfan (vec 0,vertices p, edges p)))`,
3149   (* {{{ proof *)
3150   [
3151 REWRITE_TAC [BIJ;INJ;SURJ;IN;IN_ELIM_THM];
3152 GEN_TAC ;
3153 STRIP_TAC ;
3154 MRESA_TAC (REWRITE_RULE[IN] POLYHEDRON_FAN) [`p:real^3->bool`;`vec 0:real^3`];
3155 MRESA1_TAC (REWRITE_RULE[IN] CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON)`p:real^3->bool`;
3156  MRESA1_TAC (REWRITE_RULE[IN] POLYTOPE_FAN80) `p:real^3->bool`;
3157 MRESA_TAC (REWRITE_RULE[IN] dartset_leads_into_is_topological_component_yfan) [`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`];
3158  MRESAL_TAC (REWRITE_RULE[IN] Conforming.PIIJBJK)[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;][REWRITE_RULE[IN] Conforming.conforming_fan;REWRITE_RULE[IN] Conforming.conforming_bijection_fan];
3159 ASM_MESON_TAC []
3160   ]);;
3161   (* }}} *)
3162
3163 end;;