(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Lemma: AJXXAWK, EDANAOL,   QLITJET MUGGQUF QSRHLXB LTHQIAA                 *)
(*   CZZHBLI QOEPBJD NEHRQPR ZMQQFUP JLIGZGS                                  *)
(* Section: Polyhedron                                                        *)
(* Chapter: Packing                                                           *)
(* Author: John Harrison, Hoang Le Truong                                     *)
(* Date: 2010-07-15                                                           *)
(* ========================================================================== *)


(*

John Harrison's material on polyhedra in mostly in Multivariate/flyspeck.ml

AJXXAWK
Definition 4.5:   IS_AFFINE_HULL
                   affine / hull
                   aff_dim
                   AFF_DIM_EMPTY

EDANAOL
 Definition 4.6 :  IN_INTERIOR
                   IN_RELATIVE_INTERIOR
                   CLOSURE_APPROACHABLE
                   (Don't have definition of relative boundary, but
                    several theorems use closure s DIFF relative_interior s.)

QLITJET
 Definition 4.7:   face_of
                   extreme_point_of (presumably it's meant to be the point not
                   the singleton set, which the definition literally gives)
                   facet_of
                   edge_of
                   (Don't have a definition of "proper"; I just use
                    ~(f = {}) and/or ~(f = P) as needed.)

MUGGQUF
 Lemma 4.18:       KREIN_MILMAN_MINKOWSKI

QSRHLXB
 Definition 4.8:   polyhedron
                   vertices

LTHQIAA
 Lemma 4.19:       AFFINE_IMP_POLYHEDRON

CZZHBLI
 Lemma 4.20 (i):   FACET_OF_POLYHEDRON_EXPLICIT

 Lemma 4.20 (ii):  Direct consequence of RELATIVE_INTERIOR_POLYHEDRON

 Lemma 4.20 (iii): FACE_OF_POLYHEDRON_EXPLICIT / FACE_OF_POLYHEDRON

 Lemma 4.20 (iv):  FACE_OF_TRANS

 Lemma 4.20 (v):   EXTREME_POINT_OF_FACE

 Lemma 4.20 (vi):  FACE_OF_EQ

QOEPBJD
 Corr. 4.7:        FACE_OF_POLYHEDRON_POLYHEDRON

NEHRQPR:
 Lemma 4.21:       POLYHEDRON_COLLINEAR_FACES

ZMQQFUP:
 Def 4.9:          vertices
                   edges

JLIGZGS:
                   POLYHEDRON_FAN

[Library completed by HLT, July 2011].

AMHFNXP:
                   AMHFNXP_BIJ

WBLARHH:
                   WBLARHH_BIJ

BSXAQBQ:
                   BSXAQBQ




Email tchales<->John Harrison: July 15, 2010:

|I'm not sure whether your work covers the results
| relating polyhedra to fans.  I wasn't able to find any theorems on that
| topic, but I recall that you had mentioned it in an earlier email.  I want
| to confirm with you that this still needs to be formalized.

I believe that I just did the most basic of these theorems, that a
polyhedron gives rise to a fan, together with a bunch of invariance
emmas for some relevant concepts.

*)


(* ************************************************* *)
(* Invariance theorems *)

module Polyhedron = struct

  open Sphere;;
  open Fan;;

  open Topology;;
  open Sphere;;
  open Hypermap;;
  open Fan;;
  open Planarity;;
  open Topology;;
  open Fan_defs;;
  open Conforming;;



let GRAPH = 
prove (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
REWRITE_TAC[graph; IN]);;
let CYCLIC_SET = 
prove (`cyclic_set W v w <=> ~(v = w) /\ FINITE W /\ (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\ W INTER affine hull {v, w} = {}`,
REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
let CYCLIC_SET_TRANSLATION_EQ = 
prove (`!a:real^N s x y. cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
let CYCLIC_SET_LINEAR_IMAGE = 
prove (`!f:real^M->real^N s x y. linear f /\ (!x y. f x = f y ==> x = y) ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];; add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
let GRAPH_TRANSLATION_EQ = 
prove (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
let GRAPH_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N E. linear f /\ (!x y. f x = f y ==> x = y) ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
let FAN1_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan1(x,V,E)`,
REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
let FAN1_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
let FAN2_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan2(x,V,E)`,
REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
let FAN2_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
let FAN3_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan3(x,V,E)`,
REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
let FAN3_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s} =
     IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
let FAN4_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan4(x,V,E)`,
REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
let FAN4_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
let FAN5_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan5(x,V,E)`,
REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
let FAN5_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN GEOM_TRANSFORM_TAC[]);;
let FAN6_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan6(x,V,E)`,
REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
let FAN6_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
let FAN7_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan7(x,V,E)`,
REWRITE_TAC[fan7] THEN REWRITE_TAC[SET_RULE `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN GEOM_TRANSLATE_TAC[]);;
let FAN7_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
REWRITE_TAC[fan7; IN_UNION] THEN REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB; TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [GRAPH_TRANSLATION_EQ; FAN1_TRANSLATION_EQ; FAN2_TRANSLATION_EQ; FAN3_TRANSLATION_EQ; FAN4_TRANSLATION_EQ; FAN5_TRANSLATION_EQ; FAN6_TRANSLATION_EQ; FAN7_TRANSLATION_EQ];; add_linear_invariants [GRAPH_LINEAR_IMAGE_EQ; FAN1_LINEAR_IMAGE_EQ; FAN2_LINEAR_IMAGE_EQ; FAN3_LINEAR_IMAGE_EQ; FAN4_LINEAR_IMAGE_EQ; FAN5_LINEAR_IMAGE_EQ; FAN6_LINEAR_IMAGE_EQ; FAN7_LINEAR_IMAGE_EQ];;
let FAN_TRANSLATION_EQ = 
prove (`!a:real^N x V E. FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> FAN(x,V,E)`,
REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
let FAN_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [FAN_TRANSLATION_EQ];; add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
let BASE_POINT_FAN_TRANSLATION_EQ = 
prove (`!a x V E. base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) = a + base_point_fan(x,V,E)`,
REWRITE_TAC[base_point_fan]);;
let BASE_POINT_FAN_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) = f(base_point_fan(x,V,E))`,
REWRITE_TAC[base_point_fan]);;
let SET_OF_EDGE_TRANSLATION_EQ = 
prove (`!a:real^N x V E. set_of_edge (a + x) (IMAGE (\x. a + x) V) (IMAGE (IMAGE (\x. a + x)) E) = IMAGE (\x. a + x) (set_of_edge x V E)`,
REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
let SET_OF_EDGE_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) = IMAGE f (set_of_edge x V E)`,
let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
     {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[set_of_edge; lemma] THEN
  GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
add_translation_invariants [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];; add_linear_invariants [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];; (* ************************************************* *) (* Polyhedron gives rise to a fan *)
let POLYHEDRON_FAN = 
prove (`!p z:real^3. bounded p /\ polyhedron p /\ z IN interior p ==> FAN(z,vertices p,edges p)`,
let lemma = prove
   (`!s a b c d:real^N.
          segment[a,b] face_of s /\ segment[c,d] face_of s
          ==> {a,b} = {c,d} \/
              segment[a,b] INTER segment[c,d] = {a,b} INTER {c,d}`,
    REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`s:real^N->bool`; `segment[a:real^N,b]`;
                  `segment[c:real^N,d]`] SUBSET_OF_FACE_OF) THEN
    MP_TAC(ISPECL [`s:real^N->bool`; `segment[c:real^N,d]`;
                  `segment[a:real^N,b]`] SUBSET_OF_FACE_OF) THEN
    ASM_SIMP_TAC[FACE_OF_IMP_SUBSET; RELATIVE_INTERIOR_SEGMENT] THEN
    REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[SEGMENT_REFL; INSERT_AC]) THEN
    MP_TAC(ISPECL [`a:real^N`; `b:real^N`; `c:real^N`; `d:real^N`]
        SUBSET_SEGMENT_OPEN_CLOSED) THEN
    MP_TAC(ISPECL [`c:real^N`; `d:real^N`; `a:real^N`; `b:real^N`]
        SUBSET_SEGMENT_OPEN_CLOSED) THEN
    ASM_REWRITE_TAC[open_segment] THEN
    MP_TAC(ISPECL [`a:real^N`; `b:real^N`] ENDS_IN_SEGMENT) THEN
    MP_TAC(ISPECL [`c:real^N`; `d:real^N`] ENDS_IN_SEGMENT) THEN
    ASM SET_TAC[]) in
  REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `z:real^3` THEN
  REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
  SUBGOAL_THEN `polytope(p:real^3->bool)` ASSUME_TAC THENL
   [ASM_REWRITE_TAC[POLYTOPE_EQ_BOUNDED_POLYHEDRON]; ALL_TAC] THEN
  FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLYTOPE_IMP_COMPACT) THEN
  FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLYTOPE_IMP_CONVEX) THEN
  SUBGOAL_THEN `(vec 0:real^3) IN p` ASSUME_TAC THENL
   [ASM_MESON_TAC[INTERIOR_SUBSET; SUBSET]; ALL_TAC] THEN
  SUBGOAL_THEN `!a b:real^3. ~(p = segment[a,b])` ASSUME_TAC THENL
   [REPEAT GEN_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
    RULE_ASSUM_TAC(REWRITE_RULE[INTERIOR_SEGMENT; DIMINDEX_3; ARITH]) THEN
    ASM SET_TAC[];
    ALL_TAC] THEN
  REPEAT STRIP_TAC THENL
   [REWRITE_TAC[SUBSET; FORALL_IN_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
    REWRITE_TAC[edges; FORALL_IN_GSPEC; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
    REWRITE_TAC[vertices; edge_of; IN_ELIM_THM; GSYM FACE_OF_SING] THEN
    MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC FACE_OF_TRANS THEN EXISTS_TAC `segment[v:real^3,w]` THEN
    ASM_REWRITE_TAC[FACE_OF_SING; EXTREME_POINT_OF_SEGMENT];
    REWRITE_TAC[GRAPH; edges; edge_of; FORALL_IN_GSPEC] THEN
    MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN
    ASM_CASES_TAC `w:real^3 = v` THEN
    ASM_REWRITE_TAC[SEGMENT_REFL; AFF_DIM_SING] THEN
    CONV_TAC INT_REDUCE_CONV THEN STRIP_TAC THEN
    ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY] THEN
    CONV_TAC NUM_REDUCE_CONV;
    REWRITE_TAC[fan1; SUBSET_EMPTY; vertices] THEN
    ASM_SIMP_TAC[FINITE_POLYHEDRON_EXTREME_POINTS] THEN
    REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_ELIM_THM] THEN
    MATCH_MP_TAC EXTREME_POINT_EXISTS_CONVEX THEN
    ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
    REWRITE_TAC[fan2; vertices; IN_ELIM_THM] THEN
    ASM_MESON_TAC[EXTREME_POINT_NOT_IN_INTERIOR];
    REWRITE_TAC[fan6; edges; FORALL_IN_GSPEC; edge_of] THEN
    MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN
    ASM_CASES_TAC `w:real^3 = v` THEN
    ASM_REWRITE_TAC[SEGMENT_REFL; AFF_DIM_SING] THEN
    CONV_TAC INT_REDUCE_CONV THEN STRIP_TAC THEN
    SUBGOAL_THEN `(v:real^3) extreme_point_of p /\ w extreme_point_of p`
    STRIP_ASSUME_TAC THENL
     [REWRITE_TAC[GSYM FACE_OF_SING] THEN CONJ_TAC THEN
      MATCH_MP_TAC FACE_OF_TRANS THEN EXISTS_TAC `segment[v:real^3,w]` THEN
      ASM_REWRITE_TAC[FACE_OF_SING; EXTREME_POINT_OF_SEGMENT];
      ALL_TAC] THEN
    SUBGOAL_THEN `~(v:real^3 = vec 0) /\ ~(w:real^3 = vec 0)`
    STRIP_ASSUME_TAC THENL
     [ASM_MESON_TAC[EXTREME_POINT_NOT_IN_INTERIOR]; ALL_TAC] THEN
    REWRITE_TAC[SET_RULE `{a} UNION {b,c} = {a,b,c}`] THEN
    ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT; NOT_EXISTS_THM] THEN
    X_GEN_TAC `t:real` THEN
    ASM_CASES_TAC `t = &0` THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
    DISCH_THEN SUBST_ALL_TAC THEN
    FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
     `~(x = &0) ==> x < &0 \/ &0 < x`))
    THENL
     [MP_TAC(ISPECL [`segment[v:real^3,t % v]`; `p:real^3->bool`]
        FACE_OF_DISJOINT_INTERIOR) THEN
      ASM_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
      EXISTS_TAC `vec 0:real^3` THEN ASM_REWRITE_TAC[IN_INTER] THEN
      REWRITE_TAC[IN_SEGMENT] THEN EXISTS_TAC `&1 / (&1 - t)` THEN
      ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ;
                   REAL_ARITH `t < &0 ==> &0 < &1 - t`] THEN
      REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
      CONV_TAC SYM_CONV THEN
      REWRITE_TAC[VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_RDISTRIB] THEN
      REWRITE_TAC[VECTOR_MUL_EQ_0] THEN DISJ1_TAC THEN
      UNDISCH_TAC `t < &0` THEN CONV_TAC REAL_FIELD;
      MP_TAC(ISPECL [`p:real^3->bool`; `segment[v:real^3,t % v]`;
                     `segment[v:real^3,t % v]`; `v:real^3`; `t % v:real^3`;
                     `t:real`; `&1`] POLYHEDRON_COLLINEAR_FACES) THEN
      ASM_REWRITE_TAC[ENDS_IN_SEGMENT; real_gt; REAL_LT_01] THEN
      ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_MUL_RCANCEL; REAL_MUL_LID] THEN
      ASM_MESON_TAC[VECTOR_MUL_LID]];
    REWRITE_TAC[fan7] THEN
    MAP_EVERY X_GEN_TAC [`e1:real^3->bool`; `e2:real^3->bool`] THEN
    DISCH_TAC THEN
    SUBGOAL_THEN
     `(?x1 y1:real^3. e1 = {x1,y1} /\ segment[x1,y1] face_of p) /\
      (?x2 y2:real^3. e2 = {x2,y2} /\ segment[x2,y2] face_of p)`
    STRIP_ASSUME_TAC THENL
     [FIRST_X_ASSUM(fun th -> MP_TAC th THEN MATCH_MP_TAC MONO_AND) THEN
      SIMP_TAC[IN_UNION; TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
      REWRITE_TAC[edges; edge_of; vertices; IN_ELIM_THM] THEN
      REPEAT CONJ_TAC THENL
       [MESON_TAC[]; ALL_TAC; MESON_TAC[]; ALL_TAC] THEN
      DISCH_THEN(X_CHOOSE_TAC `v:real^3`) THEN
      REPEAT(EXISTS_TAC `v:real^3`) THEN
      ASM_REWRITE_TAC[SEGMENT_REFL; FACE_OF_SING; INSERT_AC];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `(x1:real^3) extreme_point_of p /\ y1 extreme_point_of p /\
      x2 extreme_point_of p /\ y2 extreme_point_of p`
    STRIP_ASSUME_TAC THENL
     [REWRITE_TAC[GSYM FACE_OF_SING] THEN REPEAT CONJ_TAC THEN
      MATCH_MP_TAC FACE_OF_TRANS THEN
      ASM_MESON_TAC[FACE_OF_SING; EXTREME_POINT_OF_SEGMENT];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `~(x1:real^3 = vec 0) /\ ~(y1:real^3 = vec 0) /\
      ~(x2:real^3 = vec 0) /\ ~(y2:real^3 = vec 0)`
    STRIP_ASSUME_TAC THENL
     [ASM_MESON_TAC[EXTREME_POINT_NOT_IN_INTERIOR]; ALL_TAC] THEN
    ASM_SIMP_TAC[AFF_GE_0_CONVEX_HULL_ALT; FINITE_INTER; IN_INTER;
                 IN_INSERT; NOT_IN_EMPTY; FINITE_INSERT; FINITE_EMPTY] THEN
    MATCH_MP_TAC(SET_RULE
     `s INTER t = u ==> (a INSERT s) INTER (a INSERT t) = a INSERT u`) THEN
    MATCH_MP_TAC EQ_TRANS THEN
    EXISTS_TAC `{t % y:real^3 | &0 < t /\
                                y IN (convex hull {x1,y1}) INTER
                                     (convex hull {x2,y2})}` THEN
    CONJ_TAC THENL
     [REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL] THEN
      MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
       [ALL_TAC; SET_TAC[]] THEN
      REWRITE_TAC[SUBSET; IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN
      MAP_EVERY X_GEN_TAC [`s:real`; `x:real^3`] THEN
      DISCH_TAC THEN DISCH_TAC THEN
      REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
      MAP_EVERY X_GEN_TAC [`t:real`; `y:real^3`] THEN STRIP_TAC THEN
      MP_TAC(ISPECL [`p:real^3->bool`; `segment[x1:real^3,y1]`;
                     `segment[x2:real^3,y2]`; `x:real^3`; `y:real^3`;
                     `s:real`; `t:real`] POLYHEDRON_COLLINEAR_FACES) THEN
      ASM_REWRITE_TAC[real_gt] THEN DISCH_THEN SUBST_ALL_TAC THEN
      MAP_EVERY EXISTS_TAC [`t:real`; `y:real^3`] THEN ASM_REWRITE_TAC[] THEN
      UNDISCH_TAC `t % x:real^3 = t % y` THEN
      ASM_SIMP_TAC[VECTOR_MUL_LCANCEL; REAL_LT_IMP_NZ] THEN ASM_MESON_TAC[];
      SUBGOAL_THEN
       `(convex hull {x1,y1}) INTER (convex hull {x2,y2}) :real^3->bool =
        convex hull ({x1, y1} INTER {x2, y2})`
       (fun th -> REWRITE_TAC[th]) THEN
      MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
       [ALL_TAC;
        REWRITE_TAC[SUBSET_INTER] THEN CONJ_TAC THEN
        MATCH_MP_TAC HULL_MONO THEN SET_TAC[]] THEN
      MP_TAC(ISPECL [`p:real^3->bool`; `x1:real^3`; `y1:real^3`;
                     `x2:real^3`; `y2:real^3`] lemma) THEN
      ASM_REWRITE_TAC[] THEN STRIP_TAC THENL
       [ASM_REWRITE_TAC[INTER_IDEMPOT; SUBSET_REFL];
        ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; HULL_SUBSET]]]]);;
(* Hoang Le Truong's additions start here. *)
let fchanged=new_definition`fchanged f={v| ?v1 t. v=t% v1 /\ v1 IN (relative_interior f)/\ t> &0}`;;
let CONVEX_RELATIVE_INTERIOR=
prove(`!p:real^3->bool. polyhedron p ==> convex (relative_interior p) `,
let LEMMA=prove(`!f:(real^3->bool)->bool (a:(real^3->bool)->real^3) (b:(real^3->bool)->real).
{x | !h. h IN f ==> a h dot x < b h}=INTERS{{x | a h dot x < b h}| h IN f} `,

REPEAT STRIP_TAC
THEN REWRITE_TAC[INTERS;IN_ELIM_THM;]
THEN ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THENL[
REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN ASM_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`h:real^3->bool`);
 DISCH_THEN(LABEL_TAC"LINH")
THEN REPEAT STRIP_TAC
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
THENL[
EXISTS_TAC`h:real^3->bool`
THEN ASM_REWRITE_TAC[];
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

REPEAT STRIP_TAC THEN FIRST_ASSUM
   (MP_TAC o GEN_REWRITE_RULE I [POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN
  REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
  SIMP_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] 
THEN REPEAT STRIP_TAC
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`]
THEN POP_ASSUM MP_TAC
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`
THEN REWRITE_TAC[]
THEN STRIP_TAC
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)}`]
THEN MATCH_MP_TAC CONVEX_INTER
THEN MRESA1_TAC POLYHEDRON_EQ_FINITE_FACES`p:real^3->bool`
THEN MRESA_TAC LEMMA [`f:(real^3->bool)->bool`;`(a:(real^3->bool)->real^3)`; `(b:(real^3->bool)->real)`]
THEN MATCH_MP_TAC CONVEX_INTERS
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[CONVEX_HALFSPACE_LT]);;
let CONVEX_RELATIVE_INTERIOR_FACE=
prove(`!p f:(real^3->bool). polyhedron p /\ f face_of p ==> convex (relative_interior f) `,
REPEAT STRIP_TAC THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:(real^3->bool)`;`f:real^3->bool`] THEN MRESA1_TAC CONVEX_RELATIVE_INTERIOR`f:(real^3->bool)`);;
let CONVEX_RELATIVE_INTERIOR_FACET=
prove(`!p f:(real^3->bool). polyhedron p /\ f facet_of p ==> convex (relative_interior f) `,
REPEAT STRIP_TAC THEN MRESA_TAC CONVEX_RELATIVE_INTERIOR_FACE[`p:(real^3->bool)`;`f:real^3->bool`] THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`f:(real^3->bool)`;`p:(real^3->bool)`]);;
let CONNECTED_RELATIVE_INTERIOR_FACET=
prove(`!p f:(real^3->bool). polyhedron p /\ f facet_of p ==> connected (relative_interior f) `,
REPEAT STRIP_TAC THEN MRESA_TAC CONVEX_RELATIVE_INTERIOR_FACET[`p:(real^3->bool)`;`f:real^3->bool`] THEN MRESA1_TAC CONVEX_CONNECTED `relative_interior f:(real^3->bool)`);;
let CONNECTED_HALF_LINE=
prove(`!x:real^3 v. connected(aff_gt {x} {v})`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC CONVEX_CONNECTED THEN SIMP_TAC[CONVEX_AFF_GT]);;
let RELATIVE_SUBSET_FCHANGE=
prove(`!p x f:(real^3->bool). bounded p /\ polyhedron p /\ x IN interior p /\ f facet_of p ==> (relative_interior f) SUBSET fchanged f`,
REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET; fchanged;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`x':real^3` THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[REAL_ARITH`&1> &0`;VECTOR_ARITH`A= &1 %A`]);;
let AFF_GT_SUBSET_FCHANGED=
prove(`!p x f:(real^3->bool) y. bounded p /\ polyhedron p /\ x IN interior p /\ f facet_of p /\ y IN (relative_interior f) ==> {v| ?t. &0< t /\ v=t%y} SUBSET fchanged f `,
REWRITE_TAC[fchanged;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`y:real^3` THEN EXISTS_TAC`t:real` THEN ASM_REWRITE_TAC[REAL_ARITH` t> &0<=> &0< t`]);;
let CONNECTED_HALF_LINE1=
prove(`!y:real^3. connected {v| ?t. &0< t /\ v=t%y}`,
let LEMMA=prove(`!x:real^3. ~(x= vec 0)==>aff_gt {vec 0} {x}= {v| ?t. &0< t /\ v=t%x}`,

REPEAT STRIP_TAC
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]
THEN GEN_TAC
THEN EQ_TAC
THENL[
REPEAT STRIP_TAC
THEN EXISTS_TAC`t2:real`
THEN ASM_REWRITE_TAC[];
REPEAT STRIP_TAC
THEN EXISTS_TAC`&1-t:real`
THEN EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1-t+t= &1`]]) in

REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`(y= vec 0)\/ ~(y:real^3 = vec 0)`)
THENL[
ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0= vec 0`]
THEN SUBGOAL_THEN`{v:real^3 | ?t. &0 < t /\ v = vec 0}= {vec 0}` ASSUME_TAC
THENL[
REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
THEN GEN_TAC
THEN EQ_TAC
THENL[
STRIP_TAC THEN ASM_REWRITE_TAC[];
STRIP_TAC THEN EXISTS_TAC`&1`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1`]];

ASM_REWRITE_TAC[CONNECTED_SING]];

MRESA1_TAC LEMMA`y:real^3`
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC CONNECTED_HALF_LINE[`vec 0:real^3`;`y:real^3`]]);;
let CONNECTED_COMPONENT_OF_SUBSET = 
prove (`!s t x y. s SUBSET t /\ connected_component s x y ==> connected_component t x y`,
REWRITE_TAC[connected_component] THEN SET_TAC[]);;
let CONNECTED_COMPONENT_TRANS = 
prove (`!s x y z:real^N. connected_component s x y /\ connected_component s y z ==> connected_component s x z`,
REPEAT GEN_TAC THEN REWRITE_TAC[connected_component] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `t:real^N->bool`) (X_CHOOSE_TAC `u:real^N->bool`)) THEN EXISTS_TAC `t UNION u:real^N->bool` THEN ASM_REWRITE_TAC[IN_UNION; UNION_SUBSET] THEN MATCH_MP_TAC CONNECTED_UNION THEN ASM SET_TAC[]);;
let CONNECTED_FCHANGED=
prove(`!p x f:(real^3->bool). bounded p /\ polyhedron p /\ x IN interior p /\ f facet_of p ==> connected (fchanged f) `,
REPEAT STRIP_TAC THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[fchanged] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[fchanged] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN`x' IN {v| ?t. &0< t /\ v=t % v1:real^3}`ASSUME_TAC THENL[ REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`t:real` THEN ASM_REWRITE_TAC[REAL_ARITH`&0< t<=> t> &0`]; SUBGOAL_THEN`v1 IN {v| ?t. &0< t /\ v=t % v1:real^3}`ASSUME_TAC THENL[ REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`&1:real` THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 %A=A`] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MRESA1_TAC CONNECTED_HALF_LINE1`v1:real^3` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA_TAC th[`x':real^3`;`v1:real^3`]) THEN SUBGOAL_THEN`y IN {v| ?t. &0< t /\ v=t % v1':real^3}`ASSUME_TAC THENL[ REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`t':real` THEN ASM_REWRITE_TAC[REAL_ARITH`&0< t' <=> t'> &0`]; SUBGOAL_THEN`v1' IN {v| ?t. &0< t /\ v=t % v1':real^3}`ASSUME_TAC THENL[ REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`&1:real` THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 %A=A`] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MRESA1_TAC CONNECTED_HALF_LINE1`v1':real^3` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA_TAC th[`v1':real^3`;`y:real^3`;]) THEN MRESA_TAC CONNECTED_RELATIVE_INTERIOR_FACET[`p:real^3->bool`;`f:real^3->bool`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA_TAC th[`v1:real^3`;`v1':real^3`;]) THEN MRESA_TAC AFF_GT_SUBSET_FCHANGED[`p:real^3->bool`;`x:real^3`;`f:real^3->bool`;`v1:real^3`] THEN MRESA_TAC AFF_GT_SUBSET_FCHANGED[`p:real^3->bool`;`x:real^3`;`f:real^3->bool`;`v1':real^3`] THEN MRESA_TAC RELATIVE_SUBSET_FCHANGE[`p:real^3->bool`;`x:real^3`;`f:real^3->bool`;] 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`] 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`] THEN MRESA_TAC CONNECTED_COMPONENT_OF_SUBSET[`relative_interior (f:real^3->bool)`;`fchanged (f:real^3->bool)`;`v1:real^3`;` v1':real^3`] THEN MRESA_TAC CONNECTED_COMPONENT_TRANS[`fchanged f:real^3->bool`;`t % v1:real^3`;`v1:real^3`;`v1':real^3`] THEN MRESA_TAC CONNECTED_COMPONENT_TRANS[`fchanged f:real^3->bool`;`t % v1:real^3`;`v1':real^3`;`t' % v1':real^3`]]]]]);;
let CONTINUOUS_ON_LIFT_DOT = 
prove (`!s a. (lift o (\y. a dot y)) continuous_on s`,
let AFFINITE_HULL_BALL_EQ_UNIV=
prove(`!x e. &0< e ==> affine hull ball (x,e) =(:real^3)`,
let delta_func=new_definition`delta_func x y= (if x=y then &1 else &0) ` in
(let func1=new_definition`func1 a x y z= (if x=z then a else  (if  y= z then (&1- a) else &0)) ` in

REPEAT STRIP_TAC
THEN  REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[AFFINE_HULL_EXPLICIT;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THENL[
SET_TAC[];
STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x'= x:real^3\/ ~(x'=x)`)
THENL[
ASM_REWRITE_TAC[]
THEN EXISTS_TAC`{x:real^3}`
THEN EXISTS_TAC`(delta_func (x:real^3))`
THEN REWRITE_TAC[FINITE_SING;SET_RULE`~({x}={})`;SUM_SING;VSUM_SING;delta_func;VECTOR_ARITH`&1 % x=x`;SUBSET;IN_SING]
THEN STRIP_TAC
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist; VECTOR_ARITH`x-x= vec 0`;NORM_0];

ABBREV_TAC`v =(inv(norm (x'-x)) * e/ &2) % (x'-x) +x:real^3`
THEN SUBGOAL_THEN `~(x=v:real^3)` ASSUME_TAC
THENL[
POP_ASSUM (fun th-> REWRITE_TAC[SYM th; VECTOR_ARITH`A= B+A<=> B= vec 0`; GSYM NORM_EQ_0;NORM_MUL;])
THEN REWRITE_TAC[REAL_ENTIRE; REAL_ABS_MUL;REAL_ABS_INV;REAL_ABS_NORM;DE_MORGAN_THM]
THEN MRESA_TAC imp_norm_not_zero_fan[`x':real^3`;`x:real^3`]
THEN MRESA_TAC imp_inv_norm_not_zero_fan[`x':real^3`;`x:real^3`]
THEN ASM_TAC
THEN REAL_ARITH_TAC;

ABBREV_TAC`a=  (norm(x'-x:real^3) *inv e * &2)`
THEN EXISTS_TAC`{x,v:real^3}`
THEN EXISTS_TAC `func1 (a:real) v (x:real^3)`
THEN ASM_REWRITE_TAC[SET_RULE`~({x, v} = {})`]
THEN SIMP_TAC[HAS_SIZE;  FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY;VSUM_CLAUSES;SUM_CLAUSES;func1]
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`]
THEN EXPAND_TAC"v"
THEN REWRITE_TAC[VECTOR_ARITH`(A+B)-B=A:real^3 /\ a % b % v=(a*b)%v`]
THEN EXPAND_TAC"a"
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) `]
THEN MRESA_TAC IMP_NORM_FAN[`x':real^3`;`x:real^3`]
THEN MP_TAC(REAL_ARITH`&0< e==> ~(e= &0) /\ &0 <= e`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`e:real`
THEN REWRITE_TAC[VECTOR_ARITH`(&1 * &1) %v= v`;SUBSET;SET_RULE`x IN {y,z}<=> x= y \/ x= z`]
THEN GEN_TAC
THEN STRIP_TAC
THENL[
ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist; VECTOR_ARITH`x-x= vec 0`;NORM_0];
ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist; ]
THEN POP_ASSUM (fun th-> REWRITE_TAC[])
THEN EXPAND_TAC"v"
THEN REWRITE_TAC[VECTOR_ARITH`A-(B+A)= -- B:real^3`; NORM_NEG;NORM_MUL;REAL_ABS_MUL;REAL_ABS_INV;REAL_ABS_NORM;]
THEN ONCE_REWRITE_TAC[ REAL_ARITH`(a * b)* c= (a * c) * b`]
THEN ASM_REWRITE_TAC[REAL_ARITH`abs(e/ &2)= abs(e)/ &2`]
THEN MRESA1_TAC REAL_ABS_REFL`e:real`
THEN ASM_TAC
THEN REAL_ARITH_TAC]]]]));;
let INTERIOR_AFFINIE_HUL_EQ_UNIV=
prove(`!x p:(real^3->bool). x IN interior p ==> affine hull p= (:real^3)`,
REWRITE_TAC[IN_INTERIOR] THEN REPEAT STRIP_TAC THEN MRESA_TAC AFFINITE_HULL_BALL_EQ_UNIV[`x:real^3`;`e:real`] THEN MRESA_TAC HULL_MONO [`affine:(real^3->bool)->bool`;`ball(x:real^3,e)`;`p:real^3->bool`] THEN POP_ASSUM MP_TAC THEN SET_TAC[]);;
let AFF_DIM_INTERIOR_EQ_3=
prove(`!x p:(real^3->bool). x IN interior p ==> aff_dim p= &3`,
REPEAT STRIP_TAC THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`x:real^3`;`p:real^3->bool`] THEN MRESA1_TAC AFF_DIM_AFFINE_HULL`p:real^3->bool` THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN SIMP_TAC[AFF_DIM_UNIV;DIMINDEX_3]);;
let INTERIOR_IMP_RELATIVE_INTERIOR=
prove(`!x p:(real^3->bool). x IN interior p ==> x IN relative_interior p`,
REPEAT STRIP_TAC THEN REWRITE_TAC[RELATIVE_INTERIOR;IN_ELIM_THM] THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool` THEN MP_TAC(SET_RULE`x IN interior p /\ interior p SUBSET p ==> (x:real^3) IN p`) THEN RESA_TAC THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`x:real^3`;`p:real^3->bool`] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[interior;IN_ELIM_THM; SET_RULE`t INTER (:real^3)= (t:real^3->bool)`]);;
let IN_RELATIVE_INTERIOR1 = 
prove (`!x:real^N s. x IN relative_interior s ==> ?e. &0 < e /\ (ball(x,e) INTER (affine hull s)) SUBSET relative_interior s`,
REPEAT GEN_TAC THEN REWRITE_TAC[IN_RELATIVE_INTERIOR; IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`e:real` THEN ASM_REWRITE_TAC[SUBSET ;IN_RELATIVE_INTERIOR; IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL[ASM_TAC THEN SET_TAC[]; MP_TAC(SET_RULE`x' IN ball (x,e) INTER affine hull s ==> x' IN ball (x:real^N,e)`) THEN RESA_TAC THEN MRESAL_TAC OPEN_BALL[`x:real^N`;`e:real`][open_def] THEN POP_ASSUM(fun th-> MRESA1_TAC th`x':real^N`) THEN SUBGOAL_THEN`ball(x':real^N,e') SUBSET ball(x,e)` ASSUME_TAC THENL[ REWRITE_TAC[SUBSET] THEN GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[ball;IN_ELIM_THM;] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; EXISTS_TAC`e':real` THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN ASM_TAC THEN SET_TAC[]]]);;
let FCHANGED_OPEN=
prove(`!p f:(real^3->bool). bounded p /\ polyhedron p /\ vec 0 IN interior p /\ f facet_of p ==> open (fchanged f) `,
REPEAT STRIP_TAC THEN FIRST_ASSUM (MP_TAC o GEN_REWRITE_RULE I [POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN SIMP_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"LINH1") THEN STRIP_TAC 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`] THEN POP_ASSUM MP_TAC 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)` THEN REWRITE_TAC[open_def] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th `f:real^3->bool`) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN ASSUME_TAC(SYM th)) THEN GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[fchanged] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESA_TAC CONTINUOUS_ON_LIFT_DOT[`(:real^3)`;`(a:(real^3->bool)->real^3) (h:real^3->bool)`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[continuous_on;] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL1_TAC th `v1:real^3`[SET_RULE`v1 IN (:real^3)`;o_DEF;dist;GSYM LIFT_SUB]) THEN POP_ASSUM MP_TAC THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool` 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 ==> v1 IN {x | a (h:real^3->bool) dot x = b h}`) THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN RESA_TAC THEN DISCH_THEN(LABEL_TAC"LINH") THEN SUBGOAL_THEN`affine hull f= {x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}` ASSUME_TAC THENL(*1*)[ FIND_ASSUM(MP_TAC)`f facet_of (p:real^3->bool)` THEN REWRITE_TAC[facet_of] THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`] THEN STRIP_TAC THEN USE_THEN "LINH1"(fun th-> MP_TAC(ISPEC `h:real^3->bool` th)) THEN FIND_ASSUM (fun th-> REWRITE_TAC[th])`(h:real^3->bool) IN f'` THEN STRIP_TAC THEN MRESA_TAC AFF_DIM_HYPERPLANE[`(a:(real^3->bool)->real^3) (h:real^3->bool)`; `(b:(real^3->bool)->real) (h:real^3->bool)`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[DIMINDEX_3] THEN STRIP_TAC THEN MRESA_TAC AFFINE_HYPERPLANE[`(a:(real^3->bool)->real^3) (h:real^3->bool)`; `(b:(real^3->bool)->real) (h:real^3->bool)`] THEN MRESA1_TAC AFFINE_HULL_EQ`{x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}` 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}`] THEN POP_ASSUM MATCH_MP_TAC THEN STRIP_TAC THENL[ ASM_TAC THEN SET_TAC[];ARITH_TAC];(*1*) MRESA_TAC IN_RELATIVE_INTERIOR1[`v1:real^3`;`f:real^3->bool`] THEN MRESA_TAC IN_RELATIVE_INTERIOR[`v1:real^3`;`f:real^3->bool`] THEN ABBREV_TAC`r1= min (inv(norm (v1:real^3)) *e / &6) (&1) / &2 ` THEN ABBREV_TAC`r2= abs((b:(real^3->bool)->real) (h:real^3->bool)) * r1 / &2` THEN MRESA1_TAC RELATIVE_INTERIOR_OF_POLYHEDRON`p:real^3->bool` THEN MRESA_TAC INTERIOR_IMP_RELATIVE_INTERIOR[`vec 0:real^3`;`p:real^3->bool`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[DIFF;IN_ELIM_THM] THEN STRIP_TAC 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)`) THEN RESA_TAC THEN MRESAL_TAC IMP_NORM_FAN[`v1:real^3`;`vec 0:real^3`][VECTOR_ARITH`a - vec 0 = a`] THEN MRESA_TAC REAL_LT_MUL[`inv(norm (v1:real^3))`;`e:real`] THEN MP_TAC(REAL_ARITH`&0< inv (norm (v1:real^3)) * e ==> &0 < min (inv (norm v1) * e / &6) (&1) / &2 `) THEN RESA_TAC THEN USE_THEN "LINH1"(fun th-> MP_TAC(ISPEC `h:real^3->bool` th)) THEN FIND_ASSUM (fun th-> REWRITE_TAC[th])`(h:real^3->bool) IN f'` THEN STRIP_TAC THEN MRESA1_TAC REAL_ABS_CASES`(b:(real^3->bool)->real) (h:real^3->bool)` THENL(*2*)[ SUBGOAL_THEN `vec 0 IN {x | (a:(real^3->bool)->real^3) (h:real^3->bool) dot x = b h}` ASSUME_TAC THENL[ ASM_REWRITE_TAC[IN_ELIM_THM;DOT_RZERO]; 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 `) THEN RESA_TAC 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`) THEN ASM_REWRITE_TAC[]];(*2*) MRESA_TAC REAL_LT_MUL[`abs ((b:(real^3->bool)->real) (h:real^3->bool))`;`r1:real`] THEN MP_TAC(REAL_ARITH`&0 < abs ((b:(real^3->bool)->real) (h:real^3->bool)) * r1 ==> &0 < abs (b h) * r1/ &2`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`r2:real`) 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}` ASSUME_TAC THENL(*3*)[ POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"LINH2") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "LINH2"(fun th-> MRESA1_TAC th`y:real^3`) THEN REWRITE_TAC[IN_ELIM_THM;DOT_RMUL] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NORM_LIFT] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`min (inv (norm (v1:real^3)) * e / &6) (&1) / &2 = r1 ==> r1< &1`) THEN RESA_TAC THEN MRESAL_TAC REAL_LT_LMUL[`abs ((b:(real^3->bool)->real) (h:real^3->bool))`;`r1:real`;`&1`][REAL_ARITH`a* &1=a`] 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`) THEN RESA_TAC 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`] 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 )`) THEN RESA_TAC THEN MRESA1_TAC REAL_ABS_NZ`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y` THEN MRESA1_TAC REAL_ABS_NZ`(b:(real^3->bool)->real) (h:real^3->bool) ` 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)` THEN ONCE_REWRITE_TAC[REAL_ARITH`(a * b)* c= (a * c) * b`] THEN MRESA1_TAC REAL_MUL_LINV`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y` THEN REWRITE_TAC[REAL_ARITH`&1 * a= a`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REWRITE_TAC[REAL_ARITH`a * b - a * c= a*(b-c)`] 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`) THEN RESA_TAC 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`] THEN REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV] 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] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM REAL_ABS_INV;REAL_ABS_POS] THEN REWRITE_TAC[REAL_ABS_INV] THEN MP_TAC(REAL_ARITH`&0< abs((b:(real^3->bool)->real) (h:real^3->bool))/ &2 ==> ~(abs(b h)/ &2 = &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_MUL_LINV`abs((b:(real^3->bool)->real) (h:real^3->bool))/ &2` THEN EXPAND_TAC"r2" 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`] THEN ASM_REWRITE_TAC[REAL_ARITH`&1 * a= a`] THEN RESA_TAC 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)`) THEN RESA_TAC THENL[ 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`] 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`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`(a:(real^3->bool)->real^3) (h:real^3->bool) dot y` THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]; 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`] 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)`) THEN RESA_TAC THEN MRESAL1_TAC REAL_LT_INV`--((a:(real^3->bool)->real^3) (h:real^3->bool) dot y)`[REAL_INV_NEG] 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*) POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"LINH2") THEN ABBREV_TAC`r3= min (e:real / &12) (d/ &2)` THEN SUBGOAL_THEN `!y:real^3. norm(y- v1)< r3 ==> ?t1. &0< t1/\ t1 % y IN relative_interior (f:real^3->bool) ` ASSUME_TAC THENL(*4*)[ REPEAT STRIP_TAC THEN MP_TAC(REAL_ARITH`&0< d /\ min (e / &12) (d / &2) = r3 /\ norm (y - (v1:real^3)) < r3 ==> norm (y - v1) < d`) THEN RESA_TAC THEN REMOVE_THEN "LINH2"(fun th-> MRESA1_TAC th `y:real^3`) THEN EXISTS_TAC `t1:real` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (SET_RULE`!A B C x. A INTER B SUBSET C /\ x IN A /\ x IN B==> x IN C`) THEN EXISTS_TAC `ball(v1:real^3,e)` 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)}` THEN ASM_REWRITE_TAC[ball;IN_ELIM_THM;dist] 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] THEN MRESA_TAC REAL_LT_RMUL [`abs(&1- t1:real)`;`r1:real`;`norm (v1:real^3)`] 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`) THEN RESA_TAC THEN MRESA_TAC REAL_LE_RMUL [`r1:real`;`(inv (norm( v1:real^3)) * e / &6)`;`norm (v1:real^3)`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH`(a * b/ &6) *c= (a * c) * b/ &6`] THEN ASM_REWRITE_TAC[REAL_ARITH`&1 *A=A`] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`abs (&1 - t1) * norm v1 < r1 * norm (v1:real^3) /\ r1 * norm v1<= e/ &6 ==> abs (&1 - t1) * norm v1 < e/ &6`) THEN RESA_TAC THEN MRESA_TAC REAL_ABS_BETWEEN[`t1:real`;`&1`;`r1:real`] THEN MP_TAC(REAL_ARITH`t1- r1< &1 /\ r1<= &1/ &2 ==> t1< &2`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`&0< t1==> &0<= t1`) THEN RESA_TAC THEN MRESAL_TAC REAL_LT_MUL2[`t1:real`;`&2`;`norm(y- v1:real^3)`;`r3:real`][NORM_POS_LE; NORM_SUB] THEN MP_TAC(REAL_ARITH`min (e / &12) (d / &2) = r3 /\ &0< e /\ &0< d ==> &2 * r3<= e/ &6 `) THEN RESA_TAC THEN MP_TAC(REAL_ARITH`t1 * norm (v1 - y:real^3) < &2 * r3 /\ &2 * r3<= e/ &6 ==> t1 * norm (v1 - y) < e/ &6 `) THEN RESA_TAC THEN MRESA1_TAC REAL_ABS_REFL`t1:real` THEN MRESA_TAC REAL_LT_ADD2[`abs (&1 - t1) * norm (v1:real^3)`;`e/ &6`;`abs t1 * norm (v1 - y:real^3)`;`e/ &6`;] THEN MP_TAC(REAL_ARITH` abs (&1 - t1) * norm v1 + abs t1 * norm (v1 - y) < e/ &6 + e/ &6 /\ &0< e /\ norm (v1 - t1 % y) <= abs (&1 - t1) * norm v1 + abs t1 * norm (v1 - y) ==> norm (v1 - t1 % y:real^3) < e`) THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"LINH3") THEN EXISTS_TAC`t * r3:real` THEN MP_TAC(REAL_ARITH`&0< e /\ &0< d==> &0< min (e / &12) (d / &2)`) THEN RESA_TAC THEN STRIP_TAC THENL(*5*)[ MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_ARITH`&0< t<=> t> &0`] THEN ASM_REWRITE_TAC[]; REPEAT STRIP_TAC THEN REWRITE_TAC[fchanged;IN_ELIM_THM] THEN MP_TAC(REAL_ARITH`t > &0 ==> &0< t /\ ~(t= &0) /\ &0<= t`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t:real` THEN MRESA1_TAC REAL_LE_INV`t:real` THEN MRESA1_TAC REAL_MUL_LINV`t:real` THEN MRESA1_TAC REAL_ABS_REFL`inv t:real` 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`] 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`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN STRIP_TAC THEN REMOVE_THEN "LINH3"(fun th-> MRESAL1_TAC th `(inv t) % (x':real^3)`[VECTOR_ARITH`a %b % v= (a * b)%v`]) THEN MRESA_TAC REAL_LT_MUL[`t1:real`;`inv t:real`] THEN MRESA1_TAC REAL_LT_INV`t1 * inv t:real` THEN EXISTS_TAC`(t1 * inv t) % x':real^3` THEN EXISTS_TAC`inv(t1 * inv t) :real` THEN ASM_REWRITE_TAC[REAL_ARITH`t> &0 <=> &0 < t`;VECTOR_ARITH`a %b % v= (a * b)%v`] THEN MP_TAC(REAL_ARITH`&0 < t1 * inv t==> ~(t1 * inv t= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_MUL_LINV`t1 * inv t:real` THEN VECTOR_ARITH_TAC]]]]]);;
let FCHANGED_ONE_TO_ONE=
prove(`!p f1 f2:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ f1 facet_of p /\ f2 facet_of p /\ ~(fchanged f1 INTER fchanged f2= {}) ==> f1=f2`,
REWRITE_TAC[SET_RULE`~(A= {})<=> ?y. y IN A`; fchanged;INTER;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"LINH1") THEN REPEAT STRIP_TAC THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f1:real^3->bool` THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f2:real^3->bool` 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 ==> v1 IN (f1:real^3->bool) /\ v1' IN (f2:real^3->bool)`) THEN RESA_TAC THEN FIND_ASSUM(MP_TAC)`f1 facet_of (p:real^3->bool)` THEN FIND_ASSUM(MP_TAC)`f2 facet_of (p:real^3->bool)` THEN REWRITE_TAC[facet_of] THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`] THEN DISJ_CASES_TAC(SET_RULE`f1= p \/ ~(f1= p:real^3->bool)`) THENL[ ASM_REWRITE_TAC[] THEN ARITH_TAC; DISJ_CASES_TAC(SET_RULE`f2= p \/ ~(f2= p:real^3->bool)`) THENL[ ASM_REWRITE_TAC[] THEN ARITH_TAC; REPEAT STRIP_TAC 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`] THEN REMOVE_THEN "LINH1" MP_TAC THEN RESA_TAC THEN MP_TAC(SET_RULE`t' % v1 = t' % v1'==> inv t' % (t' % v1) = inv t' % (t' % v1':real^3)`) THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th]) THEN REWRITE_TAC[VECTOR_ARITH`A%B%v=(A*B)%v`] THEN MP_TAC(REAL_ARITH`t'> &0 ==> ~(t'= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_MUL_LINV`t':real` THEN REWRITE_TAC[VECTOR_ARITH`&1 %A=A`] THEN STRIP_TAC THEN MATCH_MP_TAC FACE_OF_EQ THEN EXISTS_TAC`p:real^3->bool` THEN ASM_REWRITE_TAC[DISJOINT;SET_RULE`~(A= {})<=> ?y. y IN A`;INTER;IN_ELIM_THM] THEN EXISTS_TAC `v1:real^3` THEN ASM_REWRITE_TAC[]]]);;
let CARD_EXISTS_2=
prove(`!e:A->bool. FINITE e /\ CARD e=2 ==> ?v:A w:A. e={v,w}`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~((e:A->bool)={})` ASSUME_TAC THENL[ STRIP_TAC THEN MP_TAC(ISPEC`(e:A->bool)`CARD_EQ_0) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(SET_RULE `~((e:A->bool)={})==> ?v:A. v IN e`) THEN RESA_TAC THEN SUBGOAL_THEN`~((e:A->bool) DELETE v={})` ASSUME_TAC THENL[ STRIP_TAC THEN MP_TAC(ISPECL[`v:A`;`(e:A->bool)`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(ISPECL[`(e:A->bool)`;`v:A`] FINITE_DELETE) THEN RESA_TAC THEN MP_TAC(ISPEC`(e:A->bool) DELETE v`CARD_EQ_0) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(SET_RULE `~((e:A->bool)DELETE v={})==> ?w:A. w IN (e:A->bool)DELETE v/\ w IN e`) THEN RESA_TAC THEN MP_TAC(SET_RULE `(v IN (e:A->bool))/\ (w IN (e:A->bool))==> {v,w} SUBSET e`) THEN RESA_TAC THEN MP_TAC(SET_RULE `(w IN (e:A->bool)DELETE v)==> ~(v=w)`) THEN RESA_TAC THEN MP_TAC(ISPECL [`{v:A,w:A}`;`(e:(A->bool))`] FINITE_SUBSET) THEN RESA_TAC THEN ASSUME_TAC(SET_RULE `v:A IN {v:A,w:A} `) THEN MP_TAC(ISPECL[`v:A`;`{v:A,w:A}`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(SET_RULE `v IN {v,w}==>{v:A,w:A} DELETE v PSUBSET {v,w}`) THEN RESA_TAC THEN MP_TAC(ISPECL[`{v:A,w:A} DELETE v`;`{v:A,w:A}`]CARD_PSUBSET) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN FIND_ASSUM MP_TAC`FINITE {v:A,w:A}` THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN DISCH_TAC THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v) < CARD {v, w}/\ CARD ({v, w} DELETE v) = CARD {v, w}-1 <=>CARD ({v, w} DELETE v) +1= CARD {v:A, w:A}`) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;]) THEN REWRITE_TAC[ARITH_RULE`A=A`] THEN DISCH_TAC THEN SUBGOAL_THEN `w:A IN ({v:A,w:A} DELETE v)` ASSUME_TAC THENL[ ASM_SET_TAC[]; MP_TAC(ISPECL[`{v:A,w:A}`;`v:A`] FINITE_DELETE) THEN RESA_TAC THEN MP_TAC(ISPECL[`w:A`;`{v:A,w:A} DELETE v`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(SET_RULE `w IN ({v,w} DELETE v)==>{v:A,w:A} DELETE v DELETE w PSUBSET {v,w} DELETE v`) THEN RESA_TAC THEN MP_TAC(ISPECL[`{v:A,w:A} DELETE v DELETE w`;`{v:A,w:A} DELETE v`]CARD_PSUBSET) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN FIND_ASSUM MP_TAC`FINITE ({v:A,w:A} DELETE v)` THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN DISCH_TAC 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 <=>CARD ({v, w} DELETE v DELETE w) +1= CARD ({v:A, w:A} DELETE v)`) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;]) THEN REWRITE_TAC[ARITH_RULE`A=A`] THEN DISCH_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[]) THEN POP_ASSUM (fun th->REWRITE_TAC[]) THEN ASSUME_TAC(SET_RULE `{v, w} DELETE v:A DELETE w:A={}`) THEN POP_ASSUM (fun th->REWRITE_TAC[th;CARD_CLAUSES; ARITH_RULE `0+1=1`]) THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"B") THEN DISCH_TAC THEN REMOVE_THEN "B" MP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th);ARITH_RULE` 1+1=2`]) THEN FIND_ASSUM MP_TAC`CARD (e:A->bool)=2` THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)]) THEN DISCH_TAC THEN MP_TAC(ISPECL[`{v:A,w:A}`;`e:A->bool`]CARD_SUBSET_EQ) THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)]) THEN RESA_TAC THEN EXISTS_TAC`v:A` THEN EXISTS_TAC`w:A` THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])]]]);;
let EXISTS_EDGE_POLYTOPE=
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> ?e. e IN edges p`,
REPEAT STRIP_TAC THEN REWRITE_TAC[edges;IN_ELIM_THM] THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool` THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`] THEN MRESAL1_TAC POLYTOPE_FACET_EXISTS`p:real^3->bool`[ARITH_RULE`&0:int < &3`; facet_of; ARITH_RULE`&3- &1= &2:int`] THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^3->bool`;`p:real^3->bool`] THEN MRESAL1_TAC POLYTOPE_FACET_EXISTS`f:real^3->bool`[ARITH_RULE`&0:int < &2`; facet_of; ARITH_RULE`&2- &1= &1:int`] THEN MRESA1_TAC AFF_DIM`f':real^3->bool` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`&1=A - &1:int <=> A= &2`;INT_OF_NUM_EQ] THEN STRIP_TAC THEN MRESA1_TAC AFFINE_INDEPENDENT_IMP_FINITE`b:real^3->bool` THEN MRESA1_TAC CARD_EXISTS_2`b:real^3->bool` THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f':real^3->bool`;`f:real^3->bool`] THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`f':real^3->bool` THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`f':real^3->bool` THEN SUBGOAL_THEN`?u v. f' SUBSET affine hull {u,v:real^3}` ASSUME_TAC THENL[ EXISTS_TAC`v:real^3` THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[HULL_SUBSET]; MRESAL1_TAC COMPACT_CONVEX_COLLINEAR_SEGMENT`f':real^3->bool`[COLLINEAR_AFFINE_HULL] THEN MRESA_TAC FACE_OF_TRANS[`f':real^3->bool`;`f:real^3->bool`;`p:real^3->bool`] THEN EXISTS_TAC`{a,b:real^3}` THEN EXISTS_TAC`a:real^3` THEN EXISTS_TAC`b:real^3` THEN ASM_REWRITE_TAC[edge_of] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])]);;
let EXISTS_EDGE_POLYTOPE1=
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> ~(edges p= {})`,
REWRITE_TAC[SET_RULE`~(A= {})<=> ?x. x IN A`;EXISTS_EDGE_POLYTOPE]);;
let REDUCE_POINT_FACET=
prove(`!x p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ x IN yfan(vec 0,vertices p,edges p) ==> ?f t. &0< t /\ f facet_of p /\ t % x IN f `,
REPEAT STRIP_TAC THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA1_TAC EXISTS_EDGE_POLYTOPE1`p:real^3->bool` THEN MRESA_TAC x_in_xfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`] THEN SUBGOAL_THEN`~(x= vec 0:real^3)`ASSUME_TAC THENL[ ASM_TAC THEN REWRITE_TAC[yfan; DIFF;IN_ELIM_THM] THEN SET_TAC[]; MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool` THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool` THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool` THEN MP_TAC(SET_RULE`interior p SUBSET p /\ vec 0 IN interior p ==> vec 0 IN (p:real^3->bool)`) THEN RESA_TAC THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`] THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool` THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool` THEN MRESA1_TAC COMPACT_IMP_CLOSED`p:real^3->bool` THEN MRESA1_TAC CLOSURE_CLOSED`p:real^3->bool` THEN MRESAL_TAC COMPACT_FRONTIER_LINE_LEMMA[`p:real^3->bool`;`x:real^3`][frontier;UNIONS;IN_ELIM_THM] THEN EXISTS_TAC`u':real^3->bool` THEN EXISTS_TAC`u:real` THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH`&0<= u==> u= &0 \/ &0< u`) THEN RESA_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; VECTOR_ARITH`&0 % v= vec 0:real^3`] THEN REPEAT STRIP_TAC) THEN ASM_TAC THEN SET_TAC[]]);;
let aff_ge_1_1_subset_xfan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y:real^3. FAN(x,V,E) /\ y IN xfan(x,V,E) /\ ~(x=y) ==> aff_ge {x} {y} SUBSET xfan(x,V,E)`,
REWRITE_TAC[xfan;IN_ELIM_THM;SUBSET] THEN REPEAT STRIP_TAC THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`] THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[IN] THEN RESA_TAC THEN EXISTS_TAC`e:real^3->bool` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC aff_ge_1_1_subset_aff_ge_fan[`x:real^3`;`v:real^3`;`w:real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC(th)) THEN ASM_REWRITE_TAC[] THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`; ` (v:real^3)`] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC 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)) THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN SET_TAC[]);;
let YFAN_SUBSET_UNIONS_FCHANGED=
prove(`!y p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ y IN yfan(vec 0,vertices p,edges p) ==> y IN UNIONS {fchanged f| f facet_of p}`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[UNIONS;IN_ELIM_THM] THEN MRESA_TAC REDUCE_POINT_FACET[`y:real^3`;`p:real^3->bool`] THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`f:real^3->bool`;`p:real^3->bool`] THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`] THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`f:real^3->bool` THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool` 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 `) THEN RESA_TAC THENL[ EXISTS_TAC`fchanged (f:real^3->bool)` THEN STRIP_TAC THENL[ EXISTS_TAC`f:real^3->bool` THEN ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[fchanged;IN_ELIM_THM] THEN EXISTS_TAC`t % y:real^3` THEN EXISTS_TAC`inv t :real` THEN MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_MUL_LINV`t:real` THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % b % v= (a* b)% v/\ &1 % w= w`;] THEN ONCE_REWRITE_TAC[REAL_ARITH`t> &0<=> &0< t`] THEN MATCH_MP_TAC REAL_LT_INV THEN ASM_REWRITE_TAC[]]; POP_ASSUM MP_TAC THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`] THEN FIND_ASSUM MP_TAC`f facet_of p:real^3->bool` THEN REWRITE_TAC[UNIONS;IN_ELIM_THM; facet_of] THEN ASM_REWRITE_TAC[ARITH_RULE`&3- &1= &2:int`] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`&2- &1= &1:int`] THEN RESA_TAC THEN MRESA1_TAC AFF_DIM`u:real^3->bool` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`&1=A - &1:int <=> A= &2`;INT_OF_NUM_EQ] THEN STRIP_TAC THEN MRESA1_TAC AFFINE_INDEPENDENT_IMP_FINITE`b:real^3->bool` THEN MRESA1_TAC CARD_EXISTS_2`b:real^3->bool` THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool` THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^3->bool`;`p:real^3->bool`] THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`u:real^3->bool`;`f:real^3->bool`] THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`u:real^3->bool` THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`u:real^3->bool` THEN SUBGOAL_THEN`?u1 v. u SUBSET affine hull {u1,v:real^3}` ASSUME_TAC THENL[ EXISTS_TAC`v:real^3` THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[HULL_SUBSET]; MRESAL1_TAC COMPACT_CONVEX_COLLINEAR_SEGMENT`u:real^3->bool`[COLLINEAR_AFFINE_HULL] THEN MRESA_TAC FACE_OF_TRANS[`u:real^3->bool`;`f:real^3->bool`;`p:real^3->bool`] THEN SUBGOAL_THEN `{a,b} IN edges (p:real^3->bool)`ASSUME_TAC THENL[ REWRITE_TAC[edges;edge_of;IN_ELIM_THM] THEN EXISTS_TAC`a:real^3` THEN EXISTS_TAC`b:real^3` THEN ASM_REWRITE_TAC[] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) ; 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`] THEN MRESAL_TAC CONVEX_AFF_GE[`{vec 0:real^3}`;`{a,b:real^3}`][GSYM CONVEX_HULL_EQ] THEN MRESA_TAC SEGMENT_CONVEX_HULL[`a:real^3`;`b:real^3`] THEN POP_ASSUM (fun th-> MP_TAC(SYM th) THEN STRIP_TAC) THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[FAN; fan6] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESAL1_TAC th`{a,b:real^3}`[SET_RULE`{x} UNION {a,b}={x,a,b}`]) THEN MRESA_TAC point_in_aff_ge[`vec 0:real^3`;`a:real^3`;`b:real^3`] THEN MP_TAC(SET_RULE`a IN aff_ge {vec 0} {a, b} /\ b IN aff_ge {vec 0} {a, b} ==> {a,b:real^3} SUBSET aff_ge {vec 0} {a, b}`) THEN RESA_TAC THEN MRESA_TAC HULL_MONO[`convex:(real^3->bool)->bool`;`{a,b:real^3}`;`aff_ge {vec 0} {a, b:real^3}`] THEN MP_TAC(SET_RULE`segment [a,b] SUBSET aff_ge {vec 0} {a, b} /\ aff_ge {vec 0} {a, b} SUBSET xfan (vec 0,vertices p,edges p) /\ u = segment [a,b] /\ t % y IN u ==> t % y IN xfan (vec 0,vertices p,edges (p:real^3->bool))`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN DISJ_CASES_TAC(SET_RULE`(vec 0 = t % y:real^3) \/ ~(vec 0 = t % y) `) THENL[ POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC) THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`] THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool` THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool` THEN MP_TAC (SET_RULE`vec 0 IN interior (p:real^3->bool) /\ p DIFF interior p = UNIONS {f | f facet_of p} ==> ~(vec 0 IN UNIONS {f | f facet_of p})`) THEN ASM_REWRITE_TAC[UNIONS;IN_ELIM_THM] THEN ASM_TAC THEN SET_TAC[]; 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`] THEN SUBGOAL_THEN`y IN aff_ge {vec 0} {t % y:real^3}`ASSUME_TAC THENL[ MRESAL_TAC AFF_GE_1_1[`vec 0:real^3`;`t % y:real^3`][IN_ELIM_THM] THEN EXISTS_TAC`&1- inv t:real` THEN EXISTS_TAC`inv t` THEN MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_MUL_LINV`t:real` 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] THEN ASM_TAC THEN REAL_ARITH_TAC; ASM_TAC THEN REWRITE_TAC[yfan; DIFF; IN_ELIM_THM] THEN SET_TAC[]]]]]]);;
let in_aff_ge_fan=
prove(`!x:real^3 v:real^3 u:real^3 a:real. DISJOINT {x} {v,u} /\ &0<=a /\ a<= &1 ==> (&1-a)%v + a % u IN aff_ge {x} {v,u:real^3}`,
REPEAT STRIP_TAC THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM] THEN EXISTS_TAC`&0` THEN EXISTS_TAC`&1 -a:real` THEN EXISTS_TAC`a:real` THEN MP_TAC(REAL_ARITH`&0<= a /\ a <= &1 ==> &0 <= &1 - a /\ &0 <= a`) THEN RESA_TAC THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC THEN REAL_ARITH_TAC);;
let REDUCE_POINT_FACET_EXISTS=
prove(`!x p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ ~(x= vec 0) ==> ?f t. &0< t /\ f facet_of p /\ t % x IN f `,
REPEAT STRIP_TAC THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA1_TAC EXISTS_EDGE_POLYTOPE1`p:real^3->bool` THEN MRESA_TAC x_in_xfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`] THEN SUBGOAL_THEN`~(x= vec 0:real^3)`ASSUME_TAC THENL[ ASM_TAC THEN REWRITE_TAC[yfan; DIFF;IN_ELIM_THM] THEN SET_TAC[]; MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool` THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool` THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool` THEN MP_TAC(SET_RULE`interior p SUBSET p /\ vec 0 IN interior p ==> vec 0 IN (p:real^3->bool)`) THEN RESA_TAC THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`] THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool` THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool` THEN MRESA1_TAC COMPACT_IMP_CLOSED`p:real^3->bool` THEN MRESA1_TAC CLOSURE_CLOSED`p:real^3->bool` THEN MRESAL_TAC COMPACT_FRONTIER_LINE_LEMMA[`p:real^3->bool`;`x:real^3`][frontier;UNIONS;IN_ELIM_THM] THEN EXISTS_TAC`u':real^3->bool` THEN EXISTS_TAC`u:real` THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH`&0<= u==> u= &0 \/ &0< u`) THEN RESA_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; VECTOR_ARITH`&0 % v= vec 0:real^3`] THEN REPEAT STRIP_TAC) THEN ASM_TAC THEN SET_TAC[]]);;
let FCHANGED_SUBSET_YFAN=
prove(`!x p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ x IN UNIONS {fchanged f| f facet_of p} ==> x IN yfan(vec 0,vertices p,edges p)`,
REWRITE_TAC[UNIONS;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC 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;] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 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) THEN RESA_TAC THEN RESA_TAC THEN SUBGOAL_THEN`?t1. &0< t1 /\ t1 % x IN segment[v,w:real^3]`ASSUME_TAC THENL[ POP_ASSUM MP_TAC THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`; ` (v:real^3)`] 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`;] THEN RESA_TAC THEN EXISTS_TAC`inv (t2+ t3)` THEN REWRITE_TAC[segment;IN_ELIM_THM;VECTOR_ARITH`a%(b % v+ c % w)=(a*b)%v+(a* c)%w`] THEN MP_TAC(REAL_ARITH`&0<= t2/\ &0<= t3:real ==> (t2= &0 /\ t3= &0)\/ &0< t2+t3`) THEN RESA_TAC THENL[ 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])) THEN MP_TAC(REAL_ARITH`t> &0 ==> ~(t= &0)`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool` THEN MRESA_TAC INTERIOR_AFFINIE_HUL_EQ_UNIV[`vec 0:real^3`;`p:real^3->bool`] THEN MRESA1_TAC RELATIVE_INTERIOR_INTERIOR`p:real^3->bool` THEN MRESA1_TAC RELATIVE_FRONTIER_OF_POLYHEDRON`p:real^3->bool` THEN MP_TAC (SET_RULE`vec 0 IN interior (p:real^3->bool) /\ p DIFF interior p = UNIONS {f | f facet_of p} ==> ~(vec 0 IN UNIONS {f | f facet_of p})`) THEN ASM_REWRITE_TAC[UNIONS;IN_ELIM_THM] THEN ASM_TAC THEN SET_TAC[]; MRESA1_TAC REAL_LT_INV`t2+t3:real` THEN MP_TAC(REAL_ARITH`&0< inv(t2+t3)/\ &0< t2+t3==> &0<= inv(t2+t3:real) /\ ~(t2+ t3= &0) `) THEN RESA_TAC THEN MRESA_TAC REAL_LE_MUL[`inv(t2+ t3):real`;`t2:real`] THEN MRESA_TAC REAL_LE_MUL[`inv(t2+ t3):real`;`t3:real`] THEN MRESAL1_TAC REAL_MUL_LINV`t2+ t3:real`[REAL_ARITH`c*(a+b)=c*a+ c*b`] THEN EXISTS_TAC`inv(t2+t3) * t3` THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; REAL_ARITH`(a+b)-b=a`]) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]; POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`] THEN FIND_ASSUM MP_TAC`f facet_of (p:real^3->bool)` THEN REWRITE_TAC[facet_of; ] THEN DISJ_CASES_TAC(SET_RULE`f= p\/ ~(f=p:real^3->bool)`) THENL[ ASM_REWRITE_TAC[] THEN ARITH_TAC; RESA_TAC THEN DISJ_CASES_TAC(SET_RULE`segment [v,w]= p\/ ~(segment [v,w]=p:real^3->bool)`) THENL[ POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] ) THEN ARITH_TAC; MRESA1_TAC RELATIVE_INTERIOR_SUBSET`f:real^3->bool` THEN MP_TAC(SET_RULE`v1 IN relative_interior (f:real^3->bool) /\ relative_interior f SUBSET f ==> v1 IN f`) THEN RESA_TAC THEN MRESAL_TAC REAL_LT_MUL[`t:real`;`t1:real`][REAL_ARITH`&0< t<=> t> &0`] 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`] 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) THEN MRESA_TAC SEGMENT_CLOSED_OPEN[`v:real^3`;`w:real^3`] THEN MP_TAC(SET_RULE`segment [v,w] = segment (v,w) UNION {v, w} /\ v1 IN segment [v,w] ==> v1 IN segment (v,w:real^3) \/ v1=v \/ v1= w`) THEN RESA_TAC THENL[ POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN STRIP_TAC THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`; ` (v:real^3)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(SET_RULE`v1 IN segment (v,w) /\ v1 IN relative_interior f ==> ~DISJOINT (relative_interior f) (segment (v,w:real^3))`) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESAL_TAC FACE_OF_EQ[`p:real^3->bool`;`f:real^3->bool`;`segment[v,w:real^3]`][RELATIVE_INTERIOR_SEGMENT;] THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC) THEN ASM_TAC THEN ARITH_TAC; POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`] THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`v:real^3`] THEN MP_TAC( ISPECL [`f:real^3->bool`;`v:real^3`]EXTREME_POINT_NOT_IN_RELATIVE_INTERIOR) THEN RESA_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th; AFF_DIM_SING]) THEN ARITH_TAC; POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`] THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`w:real^3`] THEN MP_TAC( ISPECL [`f:real^3->bool`;`w:real^3`]EXTREME_POINT_NOT_IN_RELATIVE_INTERIOR) THEN RESA_TAC THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th; AFF_DIM_SING]) THEN ARITH_TAC]]]]);;
let FCHANGED_EQ_YFAN=
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> UNIONS {fchanged f| f facet_of p}= yfan(vec 0,vertices p,edges p)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN EQ_TAC THENL[ ASM_SIMP_TAC[FCHANGED_SUBSET_YFAN]; ASM_SIMP_TAC[YFAN_SUBSET_UNIONS_FCHANGED]]);;
let EXISTS_POINT_IN_FCHANGED=
prove(`!f p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ f facet_of p ==> ?y. y IN fchanged f `,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[fchanged;IN_ELIM_THM;IN_ELIM_THM;facet_of] THEN STRIP_TAC THEN MRESA_TAC FACE_OF_IMP_CONVEX[`p:real^3->bool`;`f:real^3->bool`] THEN MRESAL1_TAC RELATIVE_INTERIOR_EQ_EMPTY`f:real^3->bool`[SET_RULE`~(A={})<=> ?v1. v1 IN A`] THEN EXISTS_TAC`v1:real^3` THEN EXISTS_TAC`v1:real^3` THEN EXISTS_TAC`&1` THEN ASM_REWRITE_TAC[VECTOR_ARITH`&1 % v= v`;REAL_ARITH`&1> &0`]);;
let FCHANGED_IN_COMPONENT=
prove(`!f p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ f facet_of p ==> fchanged f IN topological_component_yfan(vec 0:real^3,vertices (p:real^3->bool),edges (p:real^3->bool))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[topological_component_yfan;IN_ELIM_THM] THEN MRESA1_TAC FCHANGED_EQ_YFAN`p:real^3->bool` THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC EXISTS_POINT_IN_FCHANGED[`f:real^3->bool`;`p:real^3->bool`] THEN EXISTS_TAC`y:real^3` 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}`) THEN RESA_TAC THEN MRESAL_TAC CONNECTED_FCHANGED[`p:real^3->bool`;`vec 0:real^3`;`f:real^3->bool`][CONNECTED_CONNECTED_COMPONENT_SET] THEN POP_ASSUM (fun th-> MRESA1_TAC th`y:real^3`) THEN MRESA_TAC CONNECTED_COMPONENT_MONO[`fchanged (f:real^3->bool)`;`UNIONS{fchanged f| f facet_of (p:real^3->bool)}`;`y:real^3`] THEN REWRITE_TAC[EXTENSION;] THEN GEN_TAC THEN EQ_TAC THENL[ POP_ASSUM MP_TAC THEN SET_TAC[]; STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~(x IN fchanged (f:real^3->bool))\/ (x IN fchanged (f:real^3->bool))`) THENL[ ASM_REWRITE_TAC[] THEN MRESAL_TAC CONNECTED_COMPONENT_SUBSET[`UNIONS{fchanged f| f facet_of (p:real^3->bool)}`;`y:real^3`][SUBSET] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:real^3`[UNIONS;IN_ELIM_THM]) THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN DISJ_CASES_TAC(SET_RULE`f= f'\/ ~(f= f':real^3->bool)`) THENL[ POP_ASSUM (fun th-> POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SYM th]); MRESA_TAC CONNECTED_CONNECTED_COMPONENT[`UNIONS{fchanged f| f facet_of (p:real^3->bool)}`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[connected] THEN ABBREV_TAC`e1=UNIONS {fchanged f1 | f1 facet_of (p:real^3->bool) /\ ~(f1= f)}` THEN MRESA_TAC FCHANGED_OPEN[`p:real^3->bool`;`f:real^3->bool`] THEN EXISTS_TAC`fchanged (f:real^3->bool)` THEN EXISTS_TAC`e1:real^3->bool` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL[ EXPAND_TAC "e1" THEN MATCH_MP_TAC OPEN_UNIONS THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN MRESA_TAC FCHANGED_OPEN[`p:real^3->bool`;`f1:real^3->bool`]; STRIP_TAC THENL[ MATCH_MP_TAC (SET_RULE`!A B C. A SUBSET B/\ B SUBSET C==> A SUBSET C`) THEN EXISTS_TAC`UNIONS{fchanged f| f facet_of (p:real^3->bool)}` THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_SUBSET] THEN EXPAND_TAC"e1" THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;UNION;UNIONS;EX] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN DISJ_CASES_TAC(SET_RULE`f= f'' \/ ~(f''= f:real^3->bool )`) THENL[ ASM_REWRITE_TAC[]; MATCH_MP_TAC(SET_RULE`A==> B\/ A`) THEN EXISTS_TAC`fchanged (f'':real^3->bool)` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`f'':real^3->bool` THEN ASM_REWRITE_TAC[]]; STRIP_TAC THENL[ MATCH_MP_TAC(SET_RULE`A INTER B= {}==> A INTER B INTER C= {}`) THEN EXPAND_TAC"e1" THEN MATCH_MP_TAC(SET_RULE`(!s. s IN B==> A INTER s= {} )==> A INTER UNIONS B={}`) THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESA_TAC FCHANGED_ONE_TO_ONE[`p:real^3->bool`;`f:real^3->bool`;`f1:real^3->bool`]; STRIP_TAC THENL[ ASM_TAC THEN SET_TAC[]; REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;INTER; IN_ELIM_THM] THEN EXISTS_TAC`x:real^3` THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC"e1" THEN REWRITE_TAC[UNIONS;IN_ELIM_THM] THEN EXISTS_TAC`fchanged (f':real^3->bool)` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`f':real^3->bool` THEN ASM_REWRITE_TAC[]]]]]]; ASM_REWRITE_TAC[]]]);;
let SUR_FCHANGED=
prove(`!s p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ s IN topological_component_yfan(vec 0:real^3,vertices (p:real^3->bool),edges (p:real^3->bool)) ==> ?f. f facet_of p /\ s= fchanged f`,
REPEAT STRIP_TAC THEN MRESA1_TAC FCHANGED_EQ_YFAN`p:real^3->bool` 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`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SUBSET;IN_ELIM_THM;UNIONS]) 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`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`z:real^3`) THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN EXISTS_TAC`f:real^3->bool` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC FCHANGED_IN_COMPONENT[`f:real^3->bool`;`p:real^3->bool`] THEN ASM_TAC THEN REWRITE_TAC[topological_component_yfan;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN MP_TAC(SET_RULE`z IN connected_component (yfan (vec 0,vertices p,edges p)) y /\ z IN fchanged f /\ fchanged f=connected_component (yfan (vec 0,vertices p,edges p)) y' ==> ~(connected_component (yfan (vec 0,vertices p,edges p)) y INTER connected_component (yfan (vec 0,vertices p,edges p)) y'= {}) `) THEN RESA_TAC THEN MRESA_TAC CONNECTED_COMPONENT_OVERLAP[`yfan (vec 0,vertices p,edges p)`;`y:real^3`;`y':real^3`]);;
let AMHFNXP= 
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> (!s. s IN topological_component_yfan (vec 0,vertices (p:real^3->bool),edges (p:real^3->bool)) ==> (?!f. f facet_of p /\ s = fchanged f))`,
REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC THEN MRESA_TAC SUR_FCHANGED[`s:real^3->bool`;`p:real^3->bool`] THEN EXISTS_TAC`f:real^3->bool` THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MRESA_TAC FCHANGED_ONE_TO_ONE[`p:real^3->bool`;`y:real^3->bool`;`f:real^3->bool`] THEN POP_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[SET_RULE`A INTER A= A`] THEN MRESA_TAC EXISTS_POINT_IN_FCHANGED[`y:real^3->bool`;`p:real^3->bool`] THEN POP_ASSUM MP_TAC THEN SET_TAC[]);;
let AMHFNXP_BIJ = 
prove_by_refinement( `!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> (BIJ fchanged (\f. f facet_of p) (topological_component_yfan (vec 0,vertices p,edges p)))`,
(* {{{ proof *) [ REWRITE_TAC [BIJ;INJ;SURJ;IN;IN_ELIM_THM]; STRIP_TAC ; STRIP_TAC ; ASM_SIMP_TAC [REWRITE_RULE[IN] FCHANGED_IN_COMPONENT]; MP_TAC (REWRITE_RULE[IN] FCHANGED_IN_COMPONENT); MP_TAC (SPEC `p:real^3->bool` (REWRITE_RULE[IN] AMHFNXP)); ASM_REWRITE_TAC [EXISTS_UNIQUE]; ASM_MESON_TAC [] ]);;
(* }}} *)
let EXPAND_EDGE_POLYTOPE=
prove(`!f p:real^N->bool. polytope p /\ f face_of p /\ aff_dim f= &1 ==> ?a b. f= segment[a,b]`,
REPEAT STRIP_TAC THEN MRESA1_TAC AFF_DIM`f:real^N->bool` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`&1=A - &1:int <=> A= &2`;INT_OF_NUM_EQ] THEN STRIP_TAC THEN MRESA1_TAC AFFINE_INDEPENDENT_IMP_FINITE`b:real^N->bool` THEN MRESA1_TAC CARD_EXISTS_2`b:real^N->bool` THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MATCH_MP_TAC COMPACT_CONVEX_COLLINEAR_SEGMENT THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^N->bool`;`p:real^N->bool`] THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`f:real^N->bool` THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`f:real^N->bool` THEN SUBGOAL_THEN`?u v. f SUBSET affine hull {u,v:real^N}` ASSUME_TAC THENL[ EXISTS_TAC`v:real^N` THEN EXISTS_TAC`w:real^N` THEN ASM_REWRITE_TAC[HULL_SUBSET]; ASM_REWRITE_TAC[COLLINEAR_AFFINE_HULL] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;AFF_DIM_EMPTY]) THEN ARITH_TAC]);;
let EXISTS_EDGE_AT_VERTICES=
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> (!v. v IN vertices p ==> ~(set_of_edge v (vertices p) (edges p) ={}) )`,
REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[vertices; IN_ELIM_THM;GSYM FACE_OF_SING] THEN STRIP_TAC THEN MRESA1_TAC AFF_DIM_SING`v:real^3` THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`] THEN POP_ASSUM MP_TAC THEN DISJ_CASES_TAC(SET_RULE`p ={v}\/ ~({v}=p:real^3->bool) `) THENL[ ASM_REWRITE_TAC[] THEN ARITH_TAC; STRIP_TAC THEN MRESAL_TAC FACE_OF_POLYHEDRON_SUBSET_FACET[`p:real^3->bool`;`{v:real^3}`][SET_RULE`~({v}={})`] THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`p:real^3->bool`] THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f==> v IN f`) THEN RESA_TAC THEN FIND_ASSUM MP_TAC`f facet_of (p:real^3->bool)` THEN REWRITE_TAC[facet_of] THEN STRIP_TAC THEN MRESAL_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`v:real^3`][GSYM FACE_OF_SING] THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`f:real^3->bool`] THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`] THEN DISJ_CASES_TAC(SET_RULE`f ={v}\/ ~({v}=f:real^3->bool) `) THENL[ POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC) THEN ASM_TAC THEN ARITH_TAC; MRESAL_TAC FACE_OF_POLYHEDRON_SUBSET_FACET[`f:real^3->bool`;`{v:real^3}`][SET_RULE`~({v}={})`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[facet_of;ARITH_RULE`&3- &1- &1= &1:int`] THEN STRIP_TAC THEN MRESA_TAC FACE_OF_TRANS[`f':real^3->bool`;`f:real^3->bool`;`p:real^3->bool`] THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool` THEN STRIP_TAC THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f' ==> v IN f'`) THEN RESA_TAC THEN MRESAL_TAC EXTREME_POINT_OF_FACE[`f':real^3->bool`;`f:real^3->bool`;`v:real^3`][GSYM FACE_OF_SING] THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`f':real^3->bool`] THEN POP_ASSUM MP_TAC THEN MRESA_TAC EXPAND_EDGE_POLYTOPE[`f':real^3->bool`;`p:real^3->bool`] THEN REWRITE_TAC[EXTREME_POINT_OF_SEGMENT] THEN STRIP_TAC THENL[ POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN EXISTS_TAC`b:real^3` THEN ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM;edges;vertices] THEN MRESAL_TAC SEGMENT_EDGE_OF[`p:real^3->bool`;`a:real^3`;`b:real^3`][edge_of] THEN EXISTS_TAC`a:real^3` THEN EXISTS_TAC`b:real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN ASM_REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN EXISTS_TAC`a:real^3` THEN ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM;edges;vertices] THEN MRESAL_TAC SEGMENT_EDGE_OF[`p:real^3->bool`;`a:real^3`;`b:real^3`][edge_of] THEN EXISTS_TAC`a:real^3` THEN EXISTS_TAC`b:real^3` THEN ASM_REWRITE_TAC[] THEN SET_TAC[]]]]);;
let FLVNSME=
prove(`!v A a b p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ A={x| a dot x < b } /\ ~(a= vec 0) /\ v IN {x| a dot x = b } /\ vec 0 IN {x| a dot x = b } /\ v IN vertices p ==> ?w. w IN vertices p /\ w IN A/\ {v,w} IN edges p`,
(
let lemma = prove
   (`!X:real->bool. 
          FINITE X /\ ~(X = {}) 
          ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
    MESON_TAC[INF_FINITE]) in


REPEAT STRIP_TAC
THEN POP_ASSUM (fun th-> MP_TAC th
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[vertices; IN_ELIM_THM;GSYM FACE_OF_SING] THEN ASSUME_TAC(th)
THEN STRIP_TAC)
THEN MRESA1_TAC AFF_DIM_SING`v:real^3`
THEN MRESA_TAC AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN DISJ_CASES_TAC(SET_RULE`p ={v}\/ ~({v}=p:real^3->bool) `)

THENL(*1*)[

ASM_REWRITE_TAC[]
THEN ARITH_TAC;(*1*)

STRIP_TAC
THEN MRESAL_TAC FACE_OF_POLYHEDRON_SUBSET_FACET[`p:real^3->bool`;`{v:real^3}`][SET_RULE`~({v}={})`]
THEN MRESA_TAC FACE_OF_SING[`v:real^3`;`p:real^3->bool`]
THEN MRESAL_TAC EXPOSED_FACE_OF_POLYHEDRON[`p:real^3->bool`;`{v:real^3}`][EXPOSED_FACE_OF;SET_RULE`~({v}={})`]
THEN ABBREV_TAC`s={-- (a':real^3) dot w| w IN vertices p /\ ~(v=w)}`
THEN SUBGOAL_THEN`~(s:real->bool={})`ASSUME_TAC

THENL(*2*)[

MRESA1_TAC EXISTS_EDGE_AT_VERTICES`p:real^3->bool`
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[set_of_edge;SET_RULE`~(A={})<=> ?a. a IN A`;IN_ELIM_THM; edges; ]
THEN STRIP_TAC
THEN EXISTS_TAC`-- a' dot (a'':real^3)`
THEN EXISTS_TAC`a'':real^3`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC SEGMENT_EDGE_OF[`p:real^3->bool`;`v':real^3`;`w':real^3`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; SET_RULE`{v,v}={v}`]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(SET_RULE`{a''} = {v', w':real^3}==> v'=w'`)
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN SET_TAC[];(*2*)

 MRESAL_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`][FAN;fan1]
THEN ASSUME_TAC(SET_RULE`{w|w IN vertices p /\ ~(v = w:real^3)} SUBSET vertices p`)
THEN MRESA_TAC FINITE_SUBSET[`{w|w IN vertices p /\ ~(v = w:real^3)}`;`vertices (p:real^3->bool)`]
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)}`]
THEN MRESA1_TAC lemma`s:real->bool`
THEN SUBGOAL_THEN(`-- a''< b':real`)ASSUME_TAC

THENL(*3*)[

POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"s"
THEN REWRITE_TAC[IN_ELIM_THM;vertices;GSYM FACE_OF_SING]
THEN RESA_TAC
THEN MRESA_TAC FACE_OF_IMP_SUBSET[`p:real^3->bool`;`{w:real^3}`]
THEN MP_TAC(SET_RULE`p SUBSET {x | a' dot x <= b'} /\ {w:real^3} SUBSET p==> w IN {x | a' dot x <= b'}`)
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`a' dot (w:real^3) <= b'==> a' dot w = b' \/ a' dot w < b'`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THENL(*4*)[

MP_TAC(SET_RULE`a' dot w = b'/\ {w} SUBSET p /\{v}=p INTER {x | a' dot (x:real^3) = b'}==> w =v`)
THEN RESA_TAC;(*4*)

ASM_REWRITE_TAC[VECTOR_ARITH`--(-- a dot w)= a dot w`]](*4*);(*3*)

MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
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'} `)
THEN RESA_TAC
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'}`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM; DOT_RZERO]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0<= b' ==> b'= &0 \/ &0< b'`)
THEN RESA_TAC
THENL(*6*)[ 

POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN SUBGOAL_THEN`vec 0 IN  {x:real^3 | a' dot x = &0}` ASSUME_TAC

THENL(*7*)[
REWRITE_TAC[IN_ELIM_THM; DOT_RZERO];(*7*)

MP_TAC(SET_RULE`(vec 0) IN interior (p:real^3->bool) /\ interior p SUBSET p ==> (vec 0) IN p`)
THEN RESA_TAC
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}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(vec 0) IN p INTER  {x:real^3 | a' dot x = &0} /\
 p INTER  {x:real^3 | a' dot x = &0} = {v} ==> v= vec 0`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`vec 0:real^3`]](*7*);(*6*)



ABBREV_TAC`b1= max (-- a'') (&0) + (b'- max (-- a'') (&0))/ &2`
THEN MP_TAC(REAL_ARITH`max (-- a'') (&0) + (b'- max (-- a'') (&0))/ &2 = b1 /\ -- a''< b' /\  &0< b' ==> -- a''< b1 /\ b1< b' /\ &0< b1`)
THEN RESA_TAC
THEN SUBGOAL_THEN`vertices (p:real^3->bool) INTER {x| a' dot x >= b1}={v}` ASSUME_TAC
THENL(*7*)[

REWRITE_TAC[EXTENSION; IN_SING; INTER;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC

THENL(*8*)[

STRIP_TAC
THEN MP_TAC(REAL_ARITH`--a'' < b1 /\ a' dot (x:real^3) >= b1 ==> -- (a' dot x) < a''`)
THEN RESA_TAC
THEN DISJ_CASES_TAC(SET_RULE`~(v= x) \/ x=v:real^3`)

THENL(*9*)[

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)}`)
THEN RESA_TAC
THEN FIND_ASSUM (fun th-> MP_TAC(ISPEC `--a' dot x:real^3` th))`!x. x IN s ==> a'' <= x`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th; VECTOR_ARITH`--a' dot x= --(a' dot x)`])
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*9*)

ASM_REWRITE_TAC[]](*9*);(*8*)


RESA_TAC
THEN MP_TAC(SET_RULE`{v} = p INTER {x | a' dot x:real^3 = b'} ==> a' dot v= b'`)
THEN RESA_TAC
THEN ASM_TAC
THEN REAL_ARITH_TAC](*8*);(*7*)

ABBREV_TAC`p'= p INTER {x | a' dot x:real^3 = b1}`
THEN SUBGOAL_THEN `vec 0 IN {x:real^3 | a' dot x < b1}`ASSUME_TAC
THENL(*8*)[
ASM_REWRITE_TAC[IN_ELIM_THM; DOT_RZERO];(*8*)
 

MRESAL_TAC OPEN_HALFSPACE_LT[`a':real^3`;`b1:real`][open_def]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`vec 0:real^3`)
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN FIND_ASSUM MP_TAC`vec 0 IN interior p:real^3->bool`
THEN REWRITE_TAC[IN_INTERIOR]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH1")
THEN SUBGOAL_THEN`vec 0 IN closure {x:real^3 | a dot x < b}`ASSUME_TAC
THENL(*9*)[

MRESAL_TAC CLOSURE_HALFSPACE_LT[`a:real^3`;`b:real`][IN_ELIM_THM]
THEN ASM_TAC
THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC;(*9*)

POP_ASSUM MP_TAC
THEN REWRITE_TAC[CLOSURE_APPROACHABLE]
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'`)
THEN RESA_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(min (e:real) e') / &2`)
THEN MP_TAC(REAL_ARITH`dist (y:real^3,vec 0) < min e e' / &2 /\  min e e' / &2 < e
/\ min e e' / &2 < e'==> dist (y,vec 0) < e /\ dist (y,vec 0) < e'`)
THEN RESA_TAC
THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`y:real^3`)
THEN SUBGOAL_THEN `y:real^3 IN ball(vec 0, e')` ASSUME_TAC

THENL(*10*)[

ASM_REWRITE_TAC[SUBSET;ball;IN_ELIM_THM; DIST_SYM];(*10*)

MRESAL_TAC OPEN_BALL[`vec 0:real^3`;`e':real`][open_def]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`y:real^3`)
THEN SUBGOAL_THEN`y IN interior p:real^3->bool` ASSUME_TAC
THENL(*11*)[

REWRITE_TAC[IN_INTERIOR]
THEN EXISTS_TAC`e'':real`
THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;ball;DIST_SYM]
THEN GEN_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH2")
THEN STRIP_TAC
THEN REMOVE_THEN"LINH2"(fun th-> MRESA1_TAC th`x:real^3`)
THEN ASM_TAC
THEN SET_TAC[];(*11*)

MP_TAC(SET_RULE`y IN interior p /\ interior p SUBSET p ==>  y IN (p:real^3->bool)`)
THEN RESA_TAC
THEN SUBGOAL_THEN`?z. z IN segment[y,v:real^3] INTER {x| a' dot x= b1} /\ ~(z= v)` ASSUME_TAC
THENL(*12*)[

MP_TAC(SET_RULE`vertices p INTER {x | a' dot x >= b1} = {v:real^3} ==> v IN {x | a' dot x >= b1}`)
THEN RESA_TAC
THEN REWRITE_TAC[INTER;IN_SEGMENT;IN_ELIM_THM]
THEN ASM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`{v} = p INTER {x | a' dot x = b'}==> a' dot (v:real^3)= b'`)
THEN RESA_TAC
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)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_LT_INV`a' dot v - a' dot (y:real^3)` 
THEN MRESA_TAC REAL_LT_MUL[`inv(a' dot v - a' dot (y:real^3))`;`b1 - a' dot (y:real^3)`]
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))`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`a' dot v - a' dot (y:real^3)` 
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)`]
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`
THEN REWRITE_TAC[DOT_RMUL; DOT_RADD; REAL_ARITH`(&1- b)* c+b * d=a<=>b*(d-c)= a- c`;]
THEN ASM_REWRITE_TAC[ REAL_ARITH`(a*b)*c= b*(a*c)`; REAL_ARITH`a * &1= a`]
THEN STRIP_TAC
THENL(*13*)[


 EXISTS_TAC`inv (a' dot v - a' dot y) * (b1 - a' dot (y:real^3))`
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*13*)

REWRITE_TAC[VECTOR_ARITH`(&1- b)%a + b % v= v<=> (&1-b)%(a-v)= vec 0`;VECTOR_MUL_EQ_0]
THEN STRIP_TAC

THENL(*14*)[
ASM_TAC THEN REAL_ARITH_TAC;(*14*)

POP_ASSUM MP_TAC
THEN REWRITE_TAC[VECTOR_ARITH`y- v= vec 0<=> y= v`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] )
THEN REAL_ARITH_TAC](*14*)](*13*);(*12*)

POP_ASSUM MP_TAC
THEN STRIP_TAC
THEN MRESA_TAC FACET_OF_IMP_SUBSET[`f:real^3->bool`;`p:real^3->bool`]
THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f /\ f SUBSET p/\ y IN p==> {v,y} SUBSET p `)
THEN RESA_TAC
THEN MRESA1_TAC POLYHEDRON_IMP_CONVEX`p:real^3->bool`
THEN  MRESAL_TAC SUBSET_HULL [`convex:(real^3->bool)->bool`;`{v,y:real^3}`;`p:real^3->bool`] [GSYM SEGMENT_CONVEX_HULL;]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`z IN segment [y,v] INTER {x | a' dot x = b1}
/\ segment [y,v:real^3] SUBSET p ==> z IN  p INTER {x | a' dot x = b1}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`y IN {x | a dot x < b}==>  a dot (y:real^3) < b`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`a dot (y:real^3) < b==> a dot (y:real^3) <= b `)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`v IN {x | a dot x = b} ==>  a dot (v:real^3) = b`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`a dot (v:real^3) = b==> a dot (v:real^3) <= b `)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`  a dot (y:real^3) <= b /\  a dot v <= b ==> {v,y} SUBSET {x | a dot x <= b}`)
THEN RESA_TAC
THEN MRESA_TAC CONVEX_HALFSPACE_LE[`a:real^3`;`b:real`]
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;]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`z IN segment [y,v] INTER {x | a' dot x = b1}
/\ segment [y,v:real^3] SUBSET {x | a dot x <= b} ==>   z IN {x | a dot x <= b}/\ z IN segment [y,v] `)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM; REAL_ARITH`a<=b<=> a=b\/ a<b`]
THEN STRIP_TAC
THENL(*13*)[

REWRITE_TAC[segment;IN_ELIM_THM;]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC 
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
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`]
THEN ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC THEN ASSUME_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`z = (&1 - &1) % y + &1 % v <=> z=v `]
THEN ASM_TAC THEN REAL_ARITH_TAC;(*13*)


STRIP_TAC
THEN  MP_TAC(SET_RULE`  a dot z < b ==> z IN {x:real^3 | a dot x < b}`)
THEN RESA_TAC
THEN MRESA_TAC POLYHEDRON_HYPERPLANE[`a':real^3`;`b1:real`]
THEN MRESA_TAC POLYHEDRON_INTER[`p:real^3->bool`;`{x:real^3 | a' dot x = b1}`]
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`]
THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p':real^3->bool`
THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p':real^3->bool`
THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`p':real^3->bool`
THEN MRESA1_TAC KREIN_MILMAN_MINKOWSKI `p':real^3->bool`
THEN POP_ASSUM (fun th-> MP_TAC(SYM th))
THEN STRIP_TAC
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})) `)
THENL(*14*)[

MRESA_TAC CONVEX_HALFSPACE_GE[`a:real^3`;`b:real`]
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`] 
THEN MP_TAC(SET_RULE`convex hull {x:real^3 | x extreme_point_of p'} SUBSET {x | a dot x >= b}
/\ p' = convex hull {x | x extreme_point_of p'} /\ z IN p' ==> a dot z>= b`)
THEN RESA_TAC
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*14*)

POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM;REAL_ARITH`~(a>=b)<=> a< b`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`  a dot w < b ==> w IN {x:real^3 | a dot x < b}`)
THEN RESA_TAC
THEN ABBREV_TAC`p1= p INTER {x:real^3| a' dot x >= b1}`
THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
THEN MRESA1_TAC POLYTOPE_IMP_CLOSED`p:real^3->bool`
THEN MRESA1_TAC CLOSURE_CLOSED`p:real^3->bool`
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`]
THEN MRESA_TAC CONVEX_HALFSPACE_GE[`a':real^3`;`b1:real`]
THEN MRESA_TAC CLOSED_HALFSPACE_GE[`a':real^3`;`b1:real`]
THEN MRESA1_TAC CLOSURE_CLOSED`{x:real^3| a' dot x >= b1}:real^3->bool`
THEN MRESA_TAC INTERIOR_HALFSPACE_GE[`a':real^3`;`b1:real`]
THEN MP_TAC(SET_RULE`{v:real^3} = p INTER {x | a' dot x = b'}==> a' dot v = b'`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`z IN segment [y,v:real^3] INTER {x | a' dot x = b1}==> a' dot z = b1`)
THEN RESA_TAC
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`; ]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`a< b<=> b> a`]
THEN STRIP_TAC
THEN MRESA_TAC SUBSET_SEGMENT_OPEN_CLOSED [`v:real^3`;`z:real^3`;`y:real^3`;`v:real^3`]
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SUBSET_SEGMENT]
THEN ASM_REWRITE_TAC[ENDS_IN_SEGMENT]
THEN STRIP_TAC
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`)
THEN RESA_TAC
THEN FIND_ASSUM MP_TAC`~(z = v:real^3)`
THEN REWRITE_TAC[GSYM SEGMENT_EQ_EMPTY;SEGMENT_SYM;SET_RULE`~(A={})<=> ?v1. v1 IN A`]
THEN STRIP_TAC
THEN SUBGOAL_THEN` v1:real^3 IN interior p1`ASSUME_TAC
THENL(*15*)[

EXPAND_TAC"p1"
THEN REWRITE_TAC[INTERIOR_INTER]
THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM]
THEN ASM_TAC
THEN SET_TAC[];(*15*)



MRESAL_TAC POLYHEDRON_INTER[`p:real^3->bool`;`{x:real^3| a' dot x >= b1}`][POLYHEDRON_HALFSPACE_GE]
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`]
THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p1:real^3->bool`
THEN MRESA1_TAC POLYTOPE_IMP_CONVEX`p1:real^3->bool`
THEN MRESA_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_GE[`p1:real^3->bool`;`a':real^3`;`b1:real`]
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"p1"
THEN GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o DEPTH_CONV)[INTER;IN_ELIM_THM]
THEN ASM_REWRITE_TAC[IN_ELIM_THM;SET_RULE`(!x. x IN p /\ a' dot x >= b1 ==> a' dot x >= b1)`]
THEN SUBGOAL_THEN`p1 INTER {x:real^3 | a' dot x = b1}= p'`ASSUME_TAC
THENL(*16*)[

EXPAND_TAC"p1"
THEN REWRITE_TAC[INTER;IN_ELIM_THM;SET_RULE`(A INTER B) INTER C= A INTER (B INTER C)`
; REAL_ARITH`(a>=b /\ a=b) <=>  a = b`]
THEN ASM_TAC
THEN REWRITE_TAC[INTER;IN_ELIM_THM]
THEN REPEAT RESA_TAC;(*16*)

ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MRESA_TAC EXPOSED_FACE_OF_POLYHEDRON[`p1:real^3->bool`;`p':real^3->bool`]
THEN MRESA_TAC FACE_OF_SING[`w:real^3`;`p':real^3->bool`]
THEN MRESA_TAC EXPOSED_FACE_OF_POLYHEDRON[`p':real^3->bool`;`{w}:real^3->bool`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[exposed_face_of]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH10")
THEN ABBREV_TAC`a2= (v-w:real^3) cross (a''' cross a')`
THEN ABBREV_TAC`b2= a2 dot w:real^3`
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
THENL(*17*)[

REWRITE_TAC[INTER;IN_ELIM_THM]
THEN EXPAND_TAC "b2"
THEN EXPAND_TAC "a2"
THEN REWRITE_TAC[CROSS_LADD;VECTOR_ARITH`A-B=A+(-- B:real^3)`;DOT_LADD;CROSS_LNEG;DOT_LNEG;DOT_CROSS_SELF;]
THEN REWRITE_TAC[CROSS_LAGRANGE;DOT_LSUB;DOT_LMUL;EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THENL(*18*)[


RESA_TAC
THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
/\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) <=
 b' * b'' - (a''' dot v) * b1 + -- &0
<=> 
&0<= ( b'-b1) * (b''- a''' dot x) 
`]
THEN MATCH_MP_TAC REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= a-b<=> b<=a`]
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*18*)

RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
/\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) <=
 b' * b'' - (a''' dot v) * b1 + -- &0
<=> 
&0<= ( b'-b1) * (b''- a''' dot x) 
`]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`b1< b' ==> ~(b'- b1= &0) /\ &0< b'-b1`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`b'-b1:real`
THEN MRESA1_TAC REAL_LT_INV_EQ`b'-b1:real`
THEN MP_TAC(ARITH_RULE` &0< inv(b'-b1)==> &0<= inv(b'- b1)`)
THEN RESA_TAC
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`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC](*18*);(*17*)


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
THENL(*18*)[

REWRITE_TAC[INTER;IN_ELIM_THM]
THEN EXPAND_TAC "b2"
THEN EXPAND_TAC "a2"
THEN REWRITE_TAC[CROSS_LADD;VECTOR_ARITH`A-B=A+(-- B:real^3)`;DOT_LADD;CROSS_LNEG;DOT_LNEG;DOT_CROSS_SELF;]
THEN REWRITE_TAC[CROSS_LAGRANGE;DOT_LSUB;DOT_LMUL;EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THENL(*19*)[

RESA_TAC
THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
/\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) =
 b' * b'' - (a''' dot v) * b1 + -- &0
<=> 
&0= ( b'-b1) * (b''- a''' dot x) 
`]
THEN REAL_ARITH_TAC;(*19*)

RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`{w:real^3} = p' INTER {x | a''' dot x = b''}
/\ p1 INTER {x | a' dot x = b1} = p' ==> a''' dot w = b'' /\ a' dot w= b1`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`b1< b' ==> ~(b'- b1= &0) `)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[DOT_SYM;REAL_ARITH`b' * (a''' dot x) - (a''' dot v) * b1 + --(b1 * (a''' dot x) - b'' * b1) =
 b' * b'' - (a''' dot v) * b1 + -- &0
<=> 
 ( b'-b1) * (b''- a''' dot x) = &0
`;REAL_ENTIRE]
THEN REAL_ARITH_TAC](*19*);(*18*)




REMOVE_THEN "LINH10" MP_TAC
THEN EXPAND_TAC"p'"
THEN REWRITE_TAC[SET_RULE`(A INTER B) INTER C=A INTER(B INTER C)`]
THEN ASM_REWRITE_TAC[]
THEN ASM_REWRITE_TAC[SET_RULE`A INTER(B INTER C)= (A INTER B) INTER C`]
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''} `)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`p' SUBSET {x | a' dot x = b1} INTER {x | a2 dot x <= b2}
==> p' SUBSET  {x:real^3 | a2 dot x <= b2}`)
THEN RESA_TAC
THEN RESA_TAC
THEN SUBGOAL_THEN`v IN {x:real^3 | a2 dot x = b2}`ASSUME_TAC
THENL(*19*)[

REWRITE_TAC[IN_ELIM_THM]
THEN EXPAND_TAC "b2"
THEN EXPAND_TAC "a2"
THEN REWRITE_TAC[CROSS_LADD;VECTOR_ARITH`A-B=A+(-- B:real^3)`;DOT_LADD;CROSS_LNEG;DOT_LNEG;DOT_CROSS_SELF;]
THEN REWRITE_TAC[CROSS_LAGRANGE;DOT_LSUB;DOT_LMUL;EXTENSION;IN_ELIM_THM]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DOT_SYM]
THEN REAL_ARITH_TAC;(*19*)


SUBGOAL_THEN`!v3:real^3. v3 IN p /\ ~(v3=v)==> ?v4. v4 IN p' /\ v4 IN aff_ge {v} {v3}`ASSUME_TAC
THENL(*10*)[

REPEAT STRIP_TAC
THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool`
THEN MRESAL1_TAC KREIN_MILMAN_MINKOWSKI`p:real^3->bool`[GSYM vertices]
THEN MP_TAC(SET_RULE`(v3:real^3) IN p /\ (p:real^3->bool) = convex hull vertices p ==> v3 IN convex hull vertices p`)
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
THEN ASM_REWRITE_TAC[CONVEX_HULL_EXPLICIT;IN_ELIM_THM]
THEN STRIP_TAC
THEN ABBREV_TAC`s1= s' DELETE (v:real^3)`
THEN MRESA_TAC FINITE_DELETE[`s':real^3->bool`;`v:real^3`]
THEN ABBREV_TAC`v12=vsum s1 (\v:real^3. u v % v)`
THEN ABBREV_TAC`t12=sum (s1:real^3->bool) (u:real^3->real)`
THEN MP_TAC(SET_RULE`(!x. x IN s' ==> &0 <= u x) ==>(!x:real^3. x IN s' DELETE v ==> &0 <= u x)`)
THEN RESA_TAC
THEN MRESA_TAC SUM_POS_LE[`u:real^3->real`;`s1:real^3->bool`]
THEN MP_TAC(REAL_ARITH`&0<= t12==> t12= &0 \/ &0< t12`)
THEN RESA_TAC
THENL(*11*)[

MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
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`)
THEN REWRITE_TAC[REAL_ARITH`~(&0= &1) `;REAL_ARITH`A- B= &0<=> B=A` ]
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN RESA_TAC
THEN MRESA_TAC VSUM_DELETE_CASES[`v:real^3`;`(\v:real^3. (u:real^3->real) v % v)`;`s':real^3->bool`]
THEN MRESA_TAC SUM_POS_EQ_0[`u:real^3->real`;`s1:real^3->bool`]
THEN SUBGOAL_THEN`(!x:real^3. x IN s1 ==> (u x) % x = vec 0)`ASSUME_TAC
THENL(*12*)[

POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "LINH"(fun th-> MRESA1_TAC th`x:real^3`)
THEN VECTOR_ARITH_TAC;(*12*)

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*)


SUBGOAL_THEN`(inv t12) % v12 IN p:real^3->bool`ASSUME_TAC 
THENL(*12*)[

MRESAL1_TAC KREIN_MILMAN_MINKOWSKI`p:real^3->bool`[GSYM vertices]
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th;])
THEN ASM_REWRITE_TAC[CONVEX_HULL_EXPLICIT;IN_ELIM_THM]
THEN MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
THEN EXISTS_TAC`s1:real^3->bool`
THEN EXISTS_TAC`(\v. inv(t12) * (u:real^3->real) v)`
THEN ASM_REWRITE_TAC[SUM_LMUL;VECTOR_ARITH`(a*b) %v=a%(b%v)`;VSUM_LMUL]
THEN MP_TAC(SET_RULE`s1= s' DELETE v:real^3 /\ s' SUBSET vertices p ==> s1 SUBSET vertices p`)
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_LE_INV_EQ]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];(*12*)




SUBGOAL_THEN`a' dot inv t12 % v12:real^3 <= b1`ASSUME_TAC
THENL(*13*)[

EXPAND_TAC"v12"
THEN REWRITE_TAC[GSYM VSUM_LMUL]
THEN MRESA_TAC DOT_RSUM[`s1:real^3->bool`;`(\x:real^3. inv t12 % u x % x)`;`a':real^3`]
THEN REWRITE_TAC[DOT_RMUL]
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
THENL(*14*)[

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"s1"
THEN REWRITE_TAC[DELETE;IN_ELIM_THM]
THEN STRIP_TAC
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)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`~(a>= b)<=> a<b`; REAL_ARITH`a*b*c=(a*b)*c`]
THEN STRIP_TAC
THEN MATCH_MP_TAC REAL_LE_LMUL
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(REAL_ARITH`a' dot x < b1==> a' dot x:real^3 <= b1`)
THEN RESA_TAC
THEN MATCH_MP_TAC REAL_LE_MUL
THEN ASM_REWRITE_TAC[REAL_LE_INV_EQ]
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];(*14*)

MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
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`]
THEN POP_ASSUM MP_TAC 
THEN REWRITE_TAC[REAL_ARITH`a*b*c= (a*c) *b`;]
THEN ASM_REWRITE_TAC[SUM_LMUL; REAL_ARITH`(a*b)*c= b*(a*c)`; REAL_ARITH`a* &1=a` ]](*14*);(*13*)

SUBGOAL_THEN`~(inv t12 % v12= v:real^3)` ASSUME_TAC
THENL(*14*)[

STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b)<=> b< a`];(*14*)

SUBGOAL_THEN `aff_ge {v:real^3} {inv t12 % v12}= aff_ge {v:real^3} {v3}` ASSUME_TAC
THENL(*15*)[

MRESA_TAC AFF_GE_1_1[`v:real^3`;`inv t12 % v12:real^3`]
THEN MRESA_TAC AFF_GE_1_1[`v:real^3`;`v3:real^3`]
THEN EXPAND_TAC"v3"
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`]
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THENL(*16*)[


DISJ_CASES_TAC(SET_RULE`v IN (s':real^3->bool) \/ ~(v IN s')`)
THENL(*17*)[

RESA_TAC
THEN EXISTS_TAC`t1 - t2 * inv t12 * (u (v:real^3))`
THEN EXISTS_TAC`t2* inv t12:real`
THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1 % v + t2 % inv t12 % (v3 - u v % v) =
 (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)`]
THEN MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
THEN MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`a* &1=a`]
THEN MATCH_MP_TAC REAL_LE_MUL
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC REAL_LE_INV
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);(*17*)



MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
THEN REWRITE_TAC[VECTOR_ARITH`a % inv (&1) %v=a %v`]](*17*);(*16*)

DISJ_CASES_TAC(SET_RULE`v IN (s':real^3->bool) \/ ~(v IN s')`)
THENL(*17*)[

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`]
THEN STRIP_TAC
THEN EXISTS_TAC`&1- t12 * t2:real`
THEN EXISTS_TAC`t12 * t2:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1- a+a= &1`;]
THEN MP_TAC(REAL_ARITH`&0< t12==> ~(t12= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t12:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 *a=a`;REAL_ARITH`a * b * c=(a*b)*c`]
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`]
THEN MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - (u v + &1 - u v) * t2) = &1-(t1+t2) +t1`;REAL_ARITH`&1- &1+a=a`]
THEN MATCH_MP_TAC REAL_LE_MUL
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM (fun th-> ASM_REWRITE_TAC[SYM th]);(*17*)

MRESA_TAC SUM_DELETE_CASES[`u:real^3->real`;`s':real^3->bool`;`v:real^3`]
THEN REWRITE_TAC[VECTOR_ARITH`a % inv (&1) %v=a %v`]](*17*)](*16*);(*15*)


ABBREV_TAC`v31=inv t12 % (v12:real^3)`
THEN MP_TAC(REAL_ARITH`(a':real^3) dot v31<= b1 ==> a' dot v31:real^3< b1\/ a' dot v31 = b1`)
THEN RESA_TAC
THENL(*16*)[


SUBGOAL_THEN`?z. z IN segment[v31,v:real^3] INTER {x| a' dot x= b1} /\ ~(z= v)` ASSUME_TAC
THENL(*17*)[

MP_TAC(SET_RULE`vertices p INTER {x | a' dot x >= b1} = {v:real^3} ==> v IN {x | a' dot x >= b1}`)
THEN RESA_TAC
THEN REWRITE_TAC[INTER;IN_SEGMENT;IN_ELIM_THM]
THEN ASM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC
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)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_LT_INV`a' dot v - a' dot (v31:real^3)` 
THEN MRESA_TAC REAL_LT_MUL[`inv(a' dot v - a' dot (v31:real^3))`;`b1 - a' dot (v31:real^3)`]
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))`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`a' dot v - a' dot (v31:real^3)` 
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)`]
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`
THEN REWRITE_TAC[DOT_RMUL; DOT_RADD; REAL_ARITH`(&1- b)* c+b * d=a<=>b*(d-c)= a- c`;]
THEN ASM_REWRITE_TAC[ REAL_ARITH`(a*b)*c= b*(a*c)`; REAL_ARITH`a * &1= a`]
THEN STRIP_TAC
THENL(*18*)[


 EXISTS_TAC`inv (a' dot v - a' dot v31) * (b1 - a' dot (v31:real^3))`
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*18*)

REWRITE_TAC[VECTOR_ARITH`(&1- b)%a + b % v= v<=> (&1-b)%(a-v)= vec 0`;VECTOR_MUL_EQ_0]
THEN STRIP_TAC
THENL(*19*)[

ASM_TAC THEN REAL_ARITH_TAC;(*19*)


POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0 <=> A=B`]](*19*)](*18*);(*17*)

POP_ASSUM MP_TAC
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{v:real^3} SUBSET f /\ f SUBSET p/\ v31 IN p==> {v,v31} SUBSET p `)
THEN RESA_TAC
THEN  MRESAL_TAC SUBSET_HULL [`convex:(real^3->bool)->bool`;`{v,v31:real^3}`;`p:real^3->bool`] [GSYM 
SEGMENT_CONVEX_HULL;]
THEN MRESA_TAC SEGMENT_SUBSET_HALFLINE[`v:real^3`;`v31:real^3`]
THEN EXISTS_TAC`z':real^3`
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
THEN ASM_TAC
THEN SET_TAC[]](*17*);(*16*)


EXISTS_TAC`v31:real^3`
THEN MP_TAC(SET_RULE`a' dot v31 = b1 /\ v31 IN p ==> v31 IN p INTER {x:real^3| a' dot x= b1}`)
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &1`]
THEN RESA_TAC
THEN MRESA_TAC point_in_aff_ge_1_1[`v:real^3`;`v31:real^3`]](*16*)](*15*)](*14*)](*13*)](*12*)](*11*);(*10*)


SUBGOAL_THEN`p SUBSET {x:real^3| a2 dot x <= b2}` ASSUME_TAC
THENL(*11*)[

POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN GEN_TAC
THEN STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=v \/ ~(x=v:real^3)`)
THENL(*12*)[

ASM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`];(*12*)

MRESA_TAC AFF_GE_1_1[`v:real^3`;`x:real^3`]
THEN REMOVE_THEN "LINH" (fun th-> MRESAL1_TAC th`x:real^3`[IN_ELIM_THM])
THEN MP_TAC(SET_RULE`v4 IN p' /\p' SUBSET {x:real^3 | a2 dot x <= b2} ==> a2 dot v4<= b2`)
THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL]
THEN ASM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
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`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0< t2`)
THEN RESA_TAC
THENL(*13*)[

ASM_REWRITE_TAC[REAL_ARITH`t1+ &0= &1<=> t1= &1`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`v4 = &1 % v + &0 % x<=> v4=v`]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN MP_TAC(SET_RULE`v IN p' /\ p INTER {x:real^3 | a' dot x = b1}= p' ==> a' dot v =b1`)
THEN RESA_TAC
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*13*)

REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
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`]
](*13*)](*12*);(*11*)





SUBGOAL_THEN`p INTER {x| a2 dot x = b2} SUBSET aff_ge {v:real^3} {w}`ASSUME_TAC
THENL(*12*)[
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"LINH")
THEN STRIP_TAC
THEN REWRITE_TAC[INTER;SUBSET;IN_ELIM_THM]
THEN DISJ_CASES_TAC(SET_RULE`w=v \/ ~(v=(w:real^3))`)
THENL(*13*)[
 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`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*13*)

MRESAL_TAC AFF_GE_1_1[`v:real^3`;`w:real^3`][IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=v \/ ~(x=(v:real^3))`)
THENL(*14*)[

EXISTS_TAC`&1:real`
THEN EXISTS_TAC`&0:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= &0 /\ &1 + &0= &1`]
THEN VECTOR_ARITH_TAC;(*14*)

MRESA_TAC AFF_GE_1_1[`v:real^3`;`x:real^3`]
THEN REMOVE_THEN "LINH" (fun th-> MRESAL1_TAC th`x:real^3`[IN_ELIM_THM])
THEN SUBGOAL_THEN`v4 IN {x:real^3 | a2 dot x=b2}` ASSUME_TAC
THENL(*15*)[

ASM_REWRITE_TAC[IN_ELIM_THM;DOT_RADD;DOT_RMUL]
THEN ASM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`t1 * b2 + t2 * b2 =(t1+ t2) * b2`]
THEN REAL_ARITH_TAC;(*15*)

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`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN MP_TAC(SYM th))
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC )
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0<t2`)
THEN RESA_TAC
THENL(*16*)[

ASM_REWRITE_TAC[REAL_ARITH`t1+ &0= &1<=> t1= &1`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[VECTOR_ARITH`v4 = &1 % v + &0 % x<=> v4=v`]
THEN STRIP_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC);(*16*)

REPEAT RESA_TAC
THEN EXISTS_TAC`&1 - inv t2:real`
THEN EXISTS_TAC`inv t2:real`
THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
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`]
THEN VECTOR_ARITH_TAC](*16*)](*15*)](*14*)](*13*);(*12*)




SUBGOAL_THEN`aff_ge {v:real^3} {w}  SUBSET {x | a2 dot x = b2}` ASSUME_TAC
THENL(*13*)[

DISJ_CASES_TAC(SET_RULE`w=v \/ ~(v=w:real^3)`)
THENL(*14*)[

 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`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*14*)

MRESA_TAC AFF_GE_1_1[`v:real^3`;`w:real^3`]
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL]
THEN ASM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`a*b+c*b=(a+c)*b`;REAL_ARITH`&1 *a=a`]
](*14*);(*13*)

MP_TAC(SET_RULE`p INTER {x | a2 dot x = b2} SUBSET aff_ge {v} {w}
/\ aff_ge {v} {w} SUBSET {x | a2 dot x = b2}/\ {v, y} SUBSET p
==>  aff_ge {v} {w} INTER p= p INTER {x:real^3 | a2 dot x = b2} /\ v IN p `)
THEN RESA_TAC
THEN MRESA1_TAC POLYTOPE_IMP_COMPACT`p:real^3->bool`
THEN MRESA_TAC HALFLINE_INTER_COMPACT_SEGMENT[`p:real^3->bool`;`v:real^3`;`w:real^3`]
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`]
THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`c:real^3`]
THEN MP_TAC(SET_RULE`p INTER {x | a2 dot x = b2} SUBSET aff_ge {v} {w}
/\ p INTER {x | a2 dot x = b2} =segment[v,c] /\ c IN segment[v,c] ==> c IN aff_ge {v} {w:real^3}`)
THEN ASM_REWRITE_TAC[ENDS_IN_SEGMENT]
THEN DISJ_CASES_TAC(SET_RULE`w=v \/ ~(v=w:real^3)`)
THENL(*14*)[

 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`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
THEN ASM_TAC
THEN REAL_ARITH_TAC;(*14*)

MRESA_TAC AFF_GE_1_1[`v:real^3`;`w:real^3`]
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN DISCH_TAC
THEN EXISTS_TAC`c:real^3`
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[edges; IN_ELIM_THM;vertices]
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}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(v:real^3 = w) /\ w IN segment [v,c] ==> ~(segment [v,c]={v})`)
THEN REWRITE_TAC[SEGMENT_EQ_SING]
THEN RESA_TAC
THEN DISCH_TAC
THEN STRIP_TAC
THENL(*15*)[

POP_ASSUM MP_TAC
THEN RESA_TAC
THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0< t2 `)
THEN RESA_TAC
THENL(*16*)[

REWRITE_TAC[REAL_ARITH`t+ &0= &1<=> t= &1`]
THEN RESA_TAC 
THEN ASM_REWRITE_TAC[VECTOR_ARITH` &1 % v + &0 % w= v`];(*16*)

REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_LMUL[`t2:real`;`a dot w:real^3`;`b:real`]
THEN MP_TAC(REAL_ARITH`t2 * (a dot w:real^3) < t2 * b ==> t1 * b+ t2 * (a dot w) < (t1+t2) * b`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC](*16*);(*15*)

EXISTS_TAC`v:real^3`
THEN EXISTS_TAC`c:real^3`
THEN ASM_REWRITE_TAC[edge_of]
THEN ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]
THEN REWRITE_TAC[AFFINE_HULL_SEGMENT]
THEN ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL;AFF_DIM_2]
]]]]]]]]]]]]]]]]]]]]]]]));;
let CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON=
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> (!v. v IN vertices p ==>CARD (set_of_edge v (vertices p) (edges p)) >1)`,
REPEAT STRIP_TAC THEN MRESA1_TAC EXISTS_EDGE_AT_VERTICES`p:real^3->bool` THEN POP_ASSUM (fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`~(A={})<=> ?w. w IN A`]) THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`; ` (v:real^3)`] THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESAL_TAC properties_coordinate[`((vec 0):real^3)`;` (v:real^3)`;` (w:real^3)`][VECTOR_ARITH`a - vec 0=a`] THEN ABBREV_TAC`a= e2_fan (vec 0) v (w:real^3)` 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)`] 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] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[DOT_SYM] THEN RESA_TAC THEN DISJ_CASES_TAC(SET_RULE`w =w' \/ ~(w= w':real^3)`) THENL[ POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REAL_ARITH_TAC); MRESA_TAC CARD_2_FAN[`w:real^3`;`w':real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w':real^3)`; ` (v:real^3)`] 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} SUBSET set_of_edge v (vertices p) (edges p)`) THEN RESA_TAC THEN MRESA_TAC CARD_SUBSET[`{w,w':real^3}`;`set_of_edge v (vertices p) (edges (p:real^3->bool))`] THEN POP_ASSUM MP_TAC THEN ARITH_TAC]);;
let BSXAQBQ=
prove(`!p:real^3->bool x. bounded p /\ polyhedron p /\ vec 0 IN interior p /\ x IN d_fan((vec 0),(vertices p),(edges p)) ==> azim_fan (vec 0) (vertices p) (edges p) (pr2 x) (pr3 x) < pi`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool` THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"LINH") THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`] THEN REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN RESA_TAC THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`; ` (v:real^3)`] THEN REMOVE_ASSUM_TAC THEN REMOVE_THEN"LINH"(fun th-> MP_TAC(ISPEC `v:real^3` th)) THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th) THEN RESA_TAC THEN ASM_REWRITE_TAC[azim_fan;pr2;pr3] THEN ABBREV_TAC`a= v cross w:real^3` 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)`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[DOT_SYM] THEN REWRITE_TAC[REAL_ARITH`-- a< &0<=> &0< a`] THEN EXPAND_TAC"a" THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF] THEN RESA_TAC THEN DISJ_CASES_TAC(SET_RULE`w =w' \/ ~(w'= w:real^3)`) THENL[ POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN POP_ASSUM MP_TAC THEN EXPAND_TAC"a" THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF] THEN REAL_ARITH_TAC; MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w':real^3)`; ` (v:real^3)`] 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) ==> ~( set_of_edge v (vertices p) (edges p)= {w})`) THEN RESA_TAC THEN MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (v:real^3)`; ` (w:real^3)`] THEN POP_ASSUM (fun th-> MRESA1_TAC th`w':real^3`) THEN MRESA_TAC JBDNJJB[`v:real^3`;`w:real^3`;`w':real^3`] THEN MRESA_TAC REAL_LT_MUL[`t:real`;`a dot w':real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;]) THEN ONCE_REWRITE_TAC[DOT_SYM] THEN RESA_TAC 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`) THEN ASM_REWRITE_TAC[azim] THEN STRIP_TAC THENL[ MRESA1_TAC SIN_POS_PI_LE`azim (vec 0) v w w' - pi` THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SIN_SUB; SIN_PI;COS_PI; REAL_ARITH`&0<= a * -- &1- b * &0<=> ~( &0< a)`]; ASM_TAC THEN REAL_ARITH_TAC]]);;
let POLYTOPE_FAN80=
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> fan80 (vec 0,vertices p,edges p)`,
REWRITE_TAC[fan80] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool` THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"LINH") THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (u:real^3)`; ` (v:real^3)`] THEN ABBREV_TAC`a= v cross u:real^3` 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)`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[DOT_SYM] THEN REWRITE_TAC[REAL_ARITH`-- a< &0<=> &0< a`] THEN EXPAND_TAC"a" THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF] THEN RESA_TAC THEN DISJ_CASES_TAC(SET_RULE`u =w \/ ~(w= u:real^3)`) THENL[ POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN POP_ASSUM MP_TAC THEN EXPAND_TAC"a" THEN REWRITE_TAC[CROSS_EQ_0;DOT_CROSS_SELF] THEN REAL_ARITH_TAC; MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (w:real^3)`; ` (v:real^3)`] 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) ==> ~( set_of_edge v (vertices p) (edges p)= {u})`) THEN RESA_TAC THEN MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;` (v:real^3)`; ` (u:real^3)`] THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`) THEN MRESA_TAC JBDNJJB[`v:real^3`;`u:real^3`;`w:real^3`] THEN MRESA_TAC REAL_LT_MUL[`t:real`;`a dot w:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;]) THEN ONCE_REWRITE_TAC[DOT_SYM] THEN RESA_TAC 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`) THEN ASM_REWRITE_TAC[azim] THEN STRIP_TAC THENL[ MRESA1_TAC SIN_POS_PI_LE`azim (vec 0) v u w - pi` THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SIN_SUB; SIN_PI;COS_PI; REAL_ARITH`&0<= a * -- &1- b * &0<=> ~( &0< a)`]; 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 `) THEN RESA_TAC 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)`) THEN ASM_REWRITE_TAC[azim] THEN STRIP_TAC THEN 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`; ` (v:real^3)`] 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)`; ` (u:real^3)`; `(sigma_fan (vec 0) (vertices p) (edges p) v u):real^3`]]]);;
let WBLARHH=
prove(`!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> (!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))`,
REPEAT STRIP_TAC THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`] THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool` THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"LINH") THEN MRESA1_TAC POLYTOPE_FAN80`p:real^3->bool` 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`] THEN ABBREV_TAC`s= dartset_leads_into_fan (vec 0) (vertices p) (edges (p:real^3->bool)) f` THEN MRESAL_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;][conforming_fan;conforming_bijection_fan] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`s:real^3->bool`) THEN POP_ASSUM MP_TAC THEN MRESA1_TAC AMHFNXP`p:real^3->bool` THEN POP_ASSUM (fun th-> MRESA1_TAC th`s:real^3->bool`));;
let WBLARHH_BIJ = 
prove_by_refinement( `!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==> (BIJ (dartset_leads_into_fan (vec 0) (vertices p) (edges p)) (face_set (hypermap1_of_fanx(vec 0,vertices p,edges p))) (topological_component_yfan (vec 0,vertices p, edges p)))`,
(* {{{ proof *) [ REWRITE_TAC [BIJ;INJ;SURJ;IN;IN_ELIM_THM]; GEN_TAC ; STRIP_TAC ; MRESA_TAC (REWRITE_RULE[IN] POLYHEDRON_FAN) [`p:real^3->bool`;`vec 0:real^3`]; MRESA1_TAC (REWRITE_RULE[IN] CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON)`p:real^3->bool`; MRESA1_TAC (REWRITE_RULE[IN] POLYTOPE_FAN80) `p:real^3->bool`; 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)`]; 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]; ASM_MESON_TAC [] ]);;
(* }}} *) end;;