(* ========================================================================= *)
(* Examples of using the "without loss of generality" tactics.               *)
(* ========================================================================= *)

needs "Multivariate/wlog.ml";;

(* ------------------------------------------------------------------------- *)
(* Example 1.                                                                *)
(* ------------------------------------------------------------------------- *)

let lemma = 
prove (`(?y. y pow 2 = a) <=> &0 <= a`,
MESON_TAC[SQRT_POW_2; REAL_LE_SQUARE; REAL_POW_2]);;
let TRUONG_1 = 
prove (`!u1:real^3 u2 p a b. ~(u1 = u2) /\ plane p /\ {u1,u2} SUBSET p /\ dist(u1,u2) <= a + b /\ abs(a - b) < dist(u1,u2) /\ &0 <= a /\ &0 <= b ==> (?d1 d2. {d1, d2} SUBSET p /\ &1 / &2 % (d1 + d2) IN affine hull {u1, u2} /\ dist(d1,u1) = a /\ dist(d1,u2) = b /\ dist(d2,u1) = a /\ dist(d2,u2) = b)`,
(*** First, rotate the plane p to the special case z$3 = &0 ***) GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN (*** Now reshuffle the goal to have explicit restricted quantifiers ***) ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d ==> e <=> c /\ a /\ b /\ d ==> e`] THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN REWRITE_TAC[IN_ELIM_THM] THEN (*** Now replace quantifiers over real^3 with those over real^2 ***) PAD2D3D_TAC THEN (*** Tidy the goal a little ***) REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN (*** Choose u1 as the origin ***) GEOM_ORIGIN_TAC `u1:real^2` THEN (*** Rotate the point u2 onto the x-axis ***) GEOM_HORIZONTAL_LINE_TAC `u2:real^2` THEN (*** Only now introduce coordinates ***) X_GEN_TAC `u2:real^2` THEN DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN REWRITE_TAC[dist; VECTOR_SUB_RZERO; VECTOR_SUB_LZERO; NORM_NEG] THEN SIMP_TAC[GSYM real_gt; NORM_GT_SQUARE; NORM_EQ_SQUARE; NORM_LE_SQUARE] THEN REWRITE_TAC[real_gt; REAL_ARITH `~(abs x < &0)`] THEN ASM_SIMP_TAC[DOT_2; REAL_MUL_RZERO; REAL_ADD_RID; CART_EQ; DIMINDEX_2; FORALL_2; AFFINE_HULL_2; CART_EQ; VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT; VEC_COMPONENT; ARITH; IN_ELIM_THM; VECTOR_ADD_COMPONENT; REAL_SUB_RZERO; REAL_ADD_LID; REAL_POW2_ABS] THEN DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o GSYM) STRIP_ASSUME_TAC) THEN REWRITE_TAC[EXISTS_VECTOR_2] THEN MATCH_MP_TAC(MESON[] `(?x y:real. P x y x (--y)) ==> (?x y x' y'. P x y x' y')`) THEN SIMP_TAC[AFFINE_HULL_2; IN_ELIM_THM; CART_EQ; DIMINDEX_2; FORALL_2; VECTOR_2; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT; ARITH] THEN ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; REAL_ADD_RINV] THEN ASM_SIMP_TAC[REAL_FIELD `~(a = &0) ==> (u + v = &1 /\ b = v * a <=> u = &1 - b / a /\ v = b / a)`] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN ABBREV_TAC `u = (u2:real^2)$1` THEN REWRITE_TAC[REAL_ARITH `x + --y * --y:real = x + y * y`] THEN REWRITE_TAC[TAUT `a /\ b /\ a /\ b <=> a /\ b`] THEN (*** Now finally dive in and solve the algebraic problem ***) ASM_SIMP_TAC[REAL_FIELD `~(u = &0) ==> (x * x + y * y = a pow 2 /\ (x - u) * (x - u) + y * y = b pow 2 <=> x = (u pow 2 + a pow 2 - b pow 2) / (&2 * u) /\ y pow 2 = b pow 2 - (x - u) pow 2)`] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM2; lemma] THEN ASM_SIMP_TAC[REAL_SUB_LE; REAL_FIELD `(u pow 2 + a - b) / (&2 * u) - u = (a - b - u pow 2) / (&2 * u)`] THEN REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN ASM_SIMP_TAC[REAL_ABS_DIV; REAL_LE_LDIV_EQ; REAL_ARITH `~(u = &0) ==> &0 < abs(&2 * u)`] THEN REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_LE_SQUARE_ABS] THEN (*** Can just use SOS: this proof was found by SOS_RULE ***) MAP_EVERY UNDISCH_TAC [`u * u <= (a + b) pow 2`; `(a - b) pow 2 < u * u`] THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_LE) THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LE] THEN REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_MUL) THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Definition of "opposite" for example 2, and its invariance theorems. *) (* ------------------------------------------------------------------------- *)
let opposite = new_definition
  `opposite a b p <=>
        (&1 / &2 % (a + b)) IN p /\
        (!x y:real^N. {x,y} SUBSET p ==> (x - y) dot (a - b) = &0)`;;
let OPPOSITE_TRANSLATION_EQ = 
prove (`!c a b p. opposite (c + a) (c + b) (IMAGE (\x. c + x) p) <=> opposite a b p`,
REWRITE_TAC[opposite] THEN GEOM_TRANSLATE_TAC[]);;
add_translation_invariants [OPPOSITE_TRANSLATION_EQ];;
let OPPOSITE_LINEAR_IMAGE_EQ = 
prove (`!f a b p. linear f /\ (!x. norm(f x) = norm x) ==> (opposite (f a) (f b) (IMAGE f p) <=> opposite a b p)`,
SIMP_TAC[opposite; INSERT_SUBSET; EMPTY_SUBSET; GSYM orthogonal] THEN REWRITE_TAC[IMP_CONJ; FORALL_IN_IMAGE; RIGHT_FORALL_IMP_THM] THEN SIMP_TAC[GSYM LINEAR_ADD; GSYM LINEAR_SUB; ORTHOGONAL_LINEAR_IMAGE_EQ] THEN SIMP_TAC[GSYM LINEAR_CMUL; IN_IMAGE] THEN MESON_TAC[PRESERVES_NORM_INJECTIVE]);;
add_linear_invariants [OPPOSITE_LINEAR_IMAGE_EQ];; (* ------------------------------------------------------------------------- *) (* Example 2. *) (* ------------------------------------------------------------------------- *)
let AFFINE_PLANE = 
prove (`!p. plane p ==> affine p`,
let lemma = 
prove (`!a b:real^2. a$2 <= &0 /\ &0 <= b$2 ==> ?x. x IN convex hull {a,b} /\ x$2 = &0`,
REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH `a <= &0 /\ &0 <= b ==> a = &0 /\ b = &0 \/ &0 < b - a`)) THENL [EXISTS_TAC `a:real^2` THEN ASM_SIMP_TAC[HULL_INC; IN_INSERT]; REWRITE_TAC[CONVEX_HULL_2_ALT; EXISTS_IN_GSPEC] THEN SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT; DIMINDEX_2; ARITH] THEN EXISTS_TAC `--(a$2) / ((b:real^2)$2 - (a:real^2)$2)` THEN ASM_SIMP_TAC[REAL_LT_IMP_NZ; REAL_DIV_RMUL; REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ] THEN ASM_REAL_ARITH_TAC]);;
let TRUONG_OPPOSITE_LEMMA = 
prove (`!p a b bb m x y:real^3. plane p /\ {a, b, bb, m, x, y} SUBSET p /\ ~(x = y) /\ m IN affine hull {x,y} /\ midpoint(b,bb) = m ==> ~(convex hull {a, b} INTER affine hull {x, y} = {}) \/ ~(convex hull {a, bb} INTER affine hull {x, y} = {})`,
(*** Make the plane p the xy-plane ***) GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN (*** Rewrite with explicit restricted quantifiers ***) REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(K ALL_TAC) THEN (*** Now replace quantifiers over real^3 with those over real^2 ***) PAD2D3D_TAC THEN (*** Let x be the origin, and y on the x-axis ***) GEOM_ORIGIN_TAC `x:real^2` THEN GEOM_HORIZONTAL_LINE_TAC `y:real^2` THEN (*** Make a few simplifications ***) GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; VEC_COMPONENT] THEN DISCH_THEN(ASSUME_TAC o GSYM) THEN SIMP_TAC[midpoint; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH] THEN (*** Show aff{x,y} is now exactly the x-axis ***) SUBGOAL_THEN `affine hull {vec 0,y} = {u:real^2 | u$2 = &0}` SUBST1_TAC THENL [MATCH_MP_TAC HULL_UNIQUE THEN REWRITE_TAC[affine; INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN ASM_SIMP_TAC[VEC_COMPONENT; DIMINDEX_2; ARITH; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; REAL_MUL_RZERO; REAL_ADD_RID] THEN X_GEN_TAC `s:real^2->bool` THEN STRIP_TAC THEN REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN X_GEN_TAC `u:real^2` THEN DISCH_TAC THEN SUBGOAL_THEN `u = (&1 - u$1 / (y:real^2)$1) % vec 0 + (u$1 / (y:real^2)$1) % y` SUBST1_TAC THENL [REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN ASM_SIMP_TAC[CART_EQ; VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH; FORALL_2; REAL_MUL_RZERO; REAL_DIV_RMUL]; FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]; ALL_TAC] THEN (*** Simplify a bit more ***) SIMP_TAC[IN_ELIM_THM; REAL_ARITH `inv(&2) * (x + y) = &0 <=> y = --x`] THEN REPEAT STRIP_TAC THEN (*** Finally, make a 4-way case split then apply the lemma to each ***) REWRITE_TAC[SET_RULE `~(s INTER t = {}) <=> ?x. x IN s /\ x IN t`] THEN REWRITE_TAC[IN_ELIM_THM] THEN FIRST_ASSUM(MP_TAC o SPEC `(a:real^2)$2` o MATCH_MP (REAL_ARITH `b' = --b ==> !a. a <= &0 /\ &0 <= b \/ a <= &0 /\ &0 <= b' \/ b <= &0 /\ &0 <= a \/ b' <= &0 /\ &0 <= a`)) THEN MESON_TAC[lemma; SET_RULE `{a,b} = {b,a}`]);;
let TRUONG_OPPOSITE_THM = 
prove (`!a b bb x y:real^3 p. ~(x = y) /\ plane p /\ {a, b, x, y} SUBSET p /\ opposite b bb (affine hull {x, y}) ==> ~(convex hull {a, b} INTER affine hull {x, y} = {}) \/ ~(convex hull {a, bb} INTER affine hull {x, y} = {})`,
REWRITE_TAC[opposite; INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC TRUONG_OPPOSITE_LEMMA THEN MAP_EVERY EXISTS_TAC [`p:real^3->bool`; `&1 / &2 % (b + bb):real^3`] THEN ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; midpoint] THEN CONJ_TAC THENL [ALL_TAC; VECTOR_ARITH_TAC] THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP AFFINE_PLANE) THEN MATCH_MP_TAC(TAUT `b /\ (b ==> a) ==> a /\ b`) THEN CONJ_TAC THENL [MATCH_MP_TAC(SET_RULE `!t. x IN t /\ t SUBSET s ==> x IN s`) THEN EXISTS_TAC `affine hull {x:real^3,y}` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC HULL_MINIMAL THEN ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET]; DISCH_TAC THEN SUBST1_TAC(VECTOR_ARITH `bb:real^3 = -- &1 % b + &2 % &1 / &2 % (b + bb)`) THEN FIRST_X_ASSUM(MATCH_MP_TAC o REWRITE_RULE[affine]) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *) (* Affsign variants for example 3, and invariance theorems. *) (* ------------------------------------------------------------------------- *)
let lin_combo = new_definition
  `lin_combo V f = vsum V (\v. f v % (v:real^N))`;;
let affsign = new_definition
  `affsign sgn s t (v:real^A) <=>
     (?f. (v = lin_combo (s UNION t) f) /\
          (!w. t w ==> sgn (f w)) /\
          (sum (s UNION t) f = &1))`;;
let sgn_gt = new_definition `sgn_gt = (\t. (&0 < t))`;;
let sgn_ge = new_definition `sgn_ge = (\t. (&0 <= t))`;;
let sgn_lt = new_definition `sgn_lt = (\t. (t < &0))`;;
let sgn_le = new_definition `sgn_le = (\t. (t <= &0))`;;
let aff_gt_def = new_definition `aff_gt = affsign sgn_gt`;;
let aff_ge_def = new_definition `aff_ge = affsign sgn_ge`;;
let aff_lt_def = new_definition `aff_lt = affsign sgn_lt`;;
let aff_le_def = new_definition `aff_le = affsign sgn_le`;;
let AFFSIGN = 
prove (`affsign sgn s t = {y | ?f. y = vsum (s UNION t) (\v. f v % v) /\ (!w. w IN t ==> sgn(f w)) /\ sum (s UNION t) f = &1}`,
REWRITE_TAC[FUN_EQ_THM; affsign; lin_combo; IN_ELIM_THM] THEN REWRITE_TAC[IN]);;
let AFFSIGN_ALT = 
prove (`affsign sgn s t = {y | ?f. (!w. w IN (s UNION t) ==> w IN t ==> sgn(f w)) /\ sum (s UNION t) f = &1 /\ vsum (s UNION t) (\v. f v % v) = y}`,
REWRITE_TAC[SET_RULE `(w IN (s UNION t) ==> w IN t ==> P w) <=> (w IN t ==> P w)`] THEN REWRITE_TAC[AFFSIGN; EXTENSION; IN_ELIM_THM] THEN MESON_TAC[]);;
let IN_AFFSIGN = 
prove (`y IN affsign sgn s t <=> ?u. (!x. x IN t ==> sgn(u x)) /\ sum (s UNION t) u = &1 /\ vsum (s UNION t) (\x. u(x) % x) = y`,
REWRITE_TAC[AFFSIGN; IN_ELIM_THM] THEN SET_TAC[]);;
let AFFSIGN_INJECTIVE_LINEAR_IMAGE = 
prove (`!f:real^M->real^N sgn s t v. linear f /\ (!x y. f x = f y ==> x = y) ==> (affsign sgn (IMAGE f s) (IMAGE f t) = IMAGE f (affsign sgn s t))`,
let lemma0 = prove
   (`vsum s (\x. u x % x) = vsum {x | x IN s /\ ~(u x = &0)} (\x. u x % x)`,
    MATCH_MP_TAC VSUM_SUPERSET THEN SIMP_TAC[SUBSET; IN_ELIM_THM] THEN
    REWRITE_TAC[TAUT `p /\ ~(p /\ ~q) <=> p /\ q`] THEN
    SIMP_TAC[o_THM; VECTOR_MUL_LZERO]) in
  let lemma1 = prove
   (`!f:real^M->real^N s.
           linear f /\ (!x y. f x = f y ==> x = y)
           ==> (sum(IMAGE f s) u = &1 /\ vsum(IMAGE f s) (\x. u x % x) = y <=>
                sum s (u o f) = &1 /\ f(vsum s (\x. (u o f) x % x)) = y)`,
    REPEAT STRIP_TAC THEN
    W(MP_TAC o PART_MATCH (lhs o rand) SUM_IMAGE o funpow 3 lhand o snd) THEN
    ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST1_TAC] THEN
    MATCH_MP_TAC(MESON[] `(p ==> z = x) ==> (p /\ x = y <=> p /\ z = y)`) THEN
    DISCH_TAC THEN ONCE_REWRITE_TAC[lemma0] THEN
    SUBGOAL_THEN
     `{y | y IN IMAGE (f:real^M->real^N) s /\ ~(u y = &0)} =
      IMAGE f {x | x IN s /\ ~(u(f x) = &0)}`
    SUBST1_TAC THENL [ASM SET_TAC[]; CONV_TAC SYM_CONV] THEN
    SUBGOAL_THEN `FINITE {x | x IN s /\ ~(u((f:real^M->real^N) x) = &0)}`
    ASSUME_TAC THENL
     [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE
       (LAND_CONV o RATOR_CONV o RATOR_CONV) [sum]) THEN
      ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
      REWRITE_TAC[GSYM sum; support; NEUTRAL_REAL_ADD; o_THM] THEN
      COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_OF_NUM_EQ; ARITH_EQ];
      W(MP_TAC o PART_MATCH (lhs o rand) VSUM_IMAGE o lhand o snd) THEN
      ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
      DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
      ASM_SIMP_TAC[LINEAR_VSUM; o_DEF; GSYM LINEAR_CMUL]]) in
  REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[EXTENSION; IN_AFFSIGN] THEN
  REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE; IN_AFFSIGN] THEN
  REWRITE_TAC[GSYM IMAGE_UNION] THEN
  FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP lemma1 th]) THEN
  X_GEN_TAC `y:real^N` THEN EQ_TAC THENL
   [DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `vsum (s UNION t) (\x. (u o (f:real^M->real^N)) x % x)` THEN
    ASM_REWRITE_TAC[] THEN
    EXISTS_TAC `(u:real^N->real) o (f:real^M->real^N)` THEN
    ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[o_THM];
    MP_TAC(ISPEC `f:real^M->real^N` LINEAR_INJECTIVE_LEFT_INVERSE) THEN
    ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
    DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^M` STRIP_ASSUME_TAC) THEN
    DISCH_THEN(X_CHOOSE_THEN `x:real^M`
     (CONJUNCTS_THEN2 SUBST1_TAC MP_TAC)) THEN
    DISCH_THEN(X_CHOOSE_THEN `u:real^M->real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `(u:real^M->real) o (g:real^N->real^M)` THEN
    ASM_REWRITE_TAC[o_DEF; ETA_AX]]);;
let AFF_GE_INJECTIVE_LINEAR_IMAGE = 
prove (`!f:real^M->real^N s t. linear f /\ (!x y. f x = f y ==> x = y) ==> aff_ge (IMAGE f s) (IMAGE f t) = IMAGE f (aff_ge s t)`,
let AFF_GT_INJECTIVE_LINEAR_IMAGE = 
prove (`!f:real^M->real^N s t. linear f /\ (!x y. f x = f y ==> x = y) ==> aff_gt (IMAGE f s) (IMAGE f t) = IMAGE f (aff_gt s t)`,
let AFF_LE_INJECTIVE_LINEAR_IMAGE = 
prove (`!f:real^M->real^N s t. linear f /\ (!x y. f x = f y ==> x = y) ==> aff_le (IMAGE f s) (IMAGE f t) = IMAGE f (aff_le s t)`,
let AFF_LT_INJECTIVE_LINEAR_IMAGE = 
prove (`!f:real^M->real^N s t. linear f /\ (!x y. f x = f y ==> x = y) ==> aff_lt (IMAGE f s) (IMAGE f t) = IMAGE f (aff_lt s t)`,
add_linear_invariants [AFFSIGN_INJECTIVE_LINEAR_IMAGE; AFF_GE_INJECTIVE_LINEAR_IMAGE; AFF_GT_INJECTIVE_LINEAR_IMAGE; AFF_LE_INJECTIVE_LINEAR_IMAGE; AFF_LT_INJECTIVE_LINEAR_IMAGE];;
let IN_AFFSIGN_TRANSLATION = 
prove (`!sgn s t a v:real^N. affsign sgn s t v ==> affsign sgn (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) (a + v)`,
REPEAT GEN_TAC THEN REWRITE_TAC[affsign; lin_combo] THEN ONCE_REWRITE_TAC[SET_RULE `(!x. s x ==> p x) <=> (!x. x IN s ==> p x)`] THEN DISCH_THEN(X_CHOOSE_THEN `f:real^N->real` (CONJUNCTS_THEN2 SUBST_ALL_TAC STRIP_ASSUME_TAC)) THEN EXISTS_TAC `\x. (f:real^N->real)(x - a)` THEN ASM_REWRITE_TAC[GSYM IMAGE_UNION] THEN REPEAT CONJ_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[FORALL_IN_IMAGE; ETA_AX; VECTOR_ARITH `(a + x) - a:real^N = x`]; W(MP_TAC o PART_MATCH (lhs o rand) SUM_IMAGE o lhs o snd) THEN SIMP_TAC[VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN ASM_REWRITE_TAC[o_DEF; VECTOR_ADD_SUB; ETA_AX]] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `a + vsum {x | x IN s UNION t /\ ~(f x = &0)} (\v:real^N. f v % v)` THEN CONJ_TAC THENL [AP_TERM_TAC THEN MATCH_MP_TAC VSUM_SUPERSET THEN REWRITE_TAC[VECTOR_MUL_EQ_0; SUBSET; IN_ELIM_THM] THEN MESON_TAC[]; ALL_TAC] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `vsum (IMAGE (\x:real^N. a + x) {x | x IN s UNION t /\ ~(f x = &0)}) (\v. f(v - a) % v)` THEN CONJ_TAC THENL [ALL_TAC; CONV_TAC SYM_CONV THEN MATCH_MP_TAC VSUM_SUPERSET THEN CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN ASM_REWRITE_TAC[IMP_CONJ; FORALL_IN_IMAGE; VECTOR_MUL_EQ_0] THEN REWRITE_TAC[VECTOR_ADD_SUB] THEN SET_TAC[]] THEN SUBGOAL_THEN `FINITE {x:real^N | x IN s UNION t /\ ~(f x = &0)}` ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE (LAND_CONV o RATOR_CONV o RATOR_CONV) [sum]) THEN ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN REWRITE_TAC[GSYM sum; support; NEUTRAL_REAL_ADD] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_OF_NUM_EQ; ARITH_EQ]; ALL_TAC] THEN W(MP_TAC o PART_MATCH (lhs o rand) VSUM_IMAGE o rhs o snd) THEN ASM_SIMP_TAC[VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[o_DEF; VECTOR_ADD_SUB] THEN ASM_SIMP_TAC[VECTOR_ADD_LDISTRIB; VSUM_ADD] THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[VSUM_RMUL] THEN GEN_REWRITE_TAC LAND_CONV [GSYM VECTOR_MUL_LID] THEN AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN MATCH_MP_TAC SUM_SUPERSET THEN SET_TAC[]);;
let AFFSIGN_TRANSLATION = 
prove (`!a:real^N sgn s t. affsign sgn (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) = IMAGE (\x. a + x) (affsign sgn s t)`,
REPEAT GEN_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL [REWRITE_TAC[SUBSET; IN] THEN GEN_TAC THEN DISCH_THEN(MP_TAC o SPEC `--a:real^N` o MATCH_MP IN_AFFSIGN_TRANSLATION) THEN REWRITE_TAC[GSYM IMAGE_o; o_DEF; VECTOR_ARITH `--a + a + x:real^N = x`; IMAGE_ID] THEN DISCH_TAC THEN REWRITE_TAC[IMAGE; IN_ELIM_THM] THEN EXISTS_TAC `--a + x:real^N` THEN ASM_REWRITE_TAC[IN] THEN VECTOR_ARITH_TAC; REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN GEN_TAC THEN REWRITE_TAC[IN] THEN DISCH_THEN(MP_TAC o SPEC `a:real^N` o MATCH_MP IN_AFFSIGN_TRANSLATION) THEN REWRITE_TAC[]]);;
let AFF_GE_TRANSLATION = 
prove (`!a:real^N s t. aff_ge (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) = IMAGE (\x. a + x) (aff_ge s t)`,
let AFF_GT_TRANSLATION = 
prove (`!a:real^N s t. aff_gt (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) = IMAGE (\x. a + x) (aff_gt s t)`,
let AFF_LE_TRANSLATION = 
prove (`!a:real^N s t. aff_le (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) = IMAGE (\x. a + x) (aff_le s t)`,
let AFF_LT_TRANSLATION = 
prove (`!a:real^N s t. aff_lt (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) = IMAGE (\x. a + x) (aff_lt s t)`,
add_translation_invariants [AFFSIGN_TRANSLATION; AFF_GE_TRANSLATION; AFF_GT_TRANSLATION; AFF_LE_TRANSLATION; AFF_LT_TRANSLATION];; (* ------------------------------------------------------------------------- *) (* Example 3. *) (* ------------------------------------------------------------------------- *)
let NOT_COPLANAR_NOT_COLLINEAR = 
prove (`!v1 v2 v3 w:real^N. ~coplanar {v1, v2, v3, w} ==> ~collinear {v1, v2, v3}`,
REPEAT GEN_TAC THEN REWRITE_TAC[COLLINEAR_AFFINE_HULL; coplanar; CONTRAPOS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:real^N` THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN STRIP_TAC THEN EXISTS_TAC `w:real^N` THEN ASM_SIMP_TAC[HULL_INC; IN_INSERT] THEN REPEAT CONJ_TAC THEN MATCH_MP_TAC(SET_RULE `!t. t SUBSET s /\ x IN t ==> x IN s`) THEN EXISTS_TAC `affine hull {x:real^N,y}` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC HULL_MONO THEN SET_TAC[]);;
let AFFSIGN = 
prove (`affsign sgn s t = {y | ?f. y = vsum (s UNION t) (\v. f v % v) /\ (!w. w IN t ==> sgn(f w)) /\ sum (s UNION t) f = &1}`,
REWRITE_TAC[FUN_EQ_THM; affsign; lin_combo; IN_ELIM_THM] THEN REWRITE_TAC[IN]);;
let IN_AFFSIGN = 
prove (`y IN affsign sgn s t <=> ?u. (!x. x IN (s UNION t) ==> x IN t ==> sgn(u x)) /\ sum (s UNION t) u = &1 /\ vsum (s UNION t) (\x. u(x) % x) = y`,
REWRITE_TAC[AFFSIGN; IN_ELIM_THM] THEN SET_TAC[]);;
let LEMMA = 
prove (`!v1 v2 v3 w:real^3 p. plane p /\ {v1, v2, v3} SUBSET p /\ ~coplanar {v1, v2, v3, w} ==> (?n n'. norm(n - n') = &1 /\ (!x. x IN aff_ge {v1, v2, v3} {w} <=> (?xx h. xx IN affine hull {v1, v2, v3} /\ &0 <= h /\ x - xx = h % (n - n'))) /\ (!x y. {x, y} SUBSET affine hull {v1, v2, v3} ==> (n - n') dot (x - y) = &0))`,
GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN MAP_EVERY (fun t -> ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[INSERT_AC; COPLANAR_3]; ALL_TAC]) [`v1:real^3 = v2`; `v1:real^3 = v3`; `v2:real^3 = v3`; `v1:real^3 = w`; `v2:real^3 = w`; `v3:real^3 = w`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN EXISTS_TAC `vec 0:real^3` THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN SUBGOAL_THEN `~((w:real^3)$3 = &0)` ASSUME_TAC THENL [DISCH_TAC THEN UNDISCH_TAC `~coplanar{v1:real^3,v2,v3,w}` THEN REWRITE_TAC[coplanar] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [plane]) THEN REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM]; ALL_TAC] THEN SUBGOAL_THEN `(vec 0:real^3) IN affine hull {v1,v2,v3}` ASSUME_TAC THENL [MP_TAC(ISPEC `{v1:real^3,v2,v3}` DEPENDENT_BIGGERSET_GENERAL) THEN ANTS_TAC THENL [DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[GT] THEN MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `dim {z:real^3 | z$3 = &0}` THEN CONJ_TAC THENL [MATCH_MP_TAC DIM_SUBSET THEN ASM SET_TAC[]; ALL_TAC] THEN SIMP_TAC[DIM_SPECIAL_HYPERPLANE; DIMINDEX_3; ARITH] THEN REWRITE_TAC[GSYM NOT_LE] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP NOT_COPLANAR_NOT_COLLINEAR) THEN REWRITE_TAC[] THEN MATCH_MP_TAC COLLINEAR_SMALL THEN ASM_REWRITE_TAC[FINITE_INSERT; FINITE_RULES]; ALL_TAC] THEN REWRITE_TAC[DEPENDENT_AFFINE_DEPENDENT_CASES] THEN ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3; NOT_COPLANAR_NOT_COLLINEAR]; ALL_TAC] THEN SUBGOAL_THEN `affine hull {v1,v2,v3} = {z:real^3 | z$3 = &0}` ASSUME_TAC THENL [ASM_SIMP_TAC[AFFINE_HULL_EQ_SPAN] THEN MATCH_MP_TAC(SET_RULE `!s. t SUBSET u /\ s SUBSET t /\ u SUBSET s ==> t = u`) THEN EXISTS_TAC `span {x - v1:real^3 | x IN {v2,v3}}` THEN CONJ_TAC THENL [REWRITE_TAC[SUBSET] THEN MATCH_MP_TAC SPAN_INDUCT THEN REWRITE_TAC[SET_RULE `(\x. x IN s) = s`] THEN SIMP_TAC[SUBSPACE_SPECIAL_HYPERPLANE; DIMINDEX_3; ARITH] THEN ASM_SIMP_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM]; ALL_TAC] THEN CONJ_TAC THENL [GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_SPAN] THEN MATCH_MP_TAC SPAN_MONO THEN REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[SPAN_SUB; SPAN_INC; IN_INSERT; SUBSET]; ALL_TAC] THEN MATCH_MP_TAC CARD_GE_DIM_INDEPENDENT THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; IN_ELIM_THM; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; DIMINDEX_3; ARITH; REAL_SUB_REFL]; REWRITE_TAC[independent] THEN DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] DEPENDENT_IMP_AFFINE_DEPENDENT)) THEN ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3; NOT_COPLANAR_NOT_COLLINEAR]; SIMP_TAC[DIM_SPECIAL_HYPERPLANE; DIMINDEX_3; ARITH] THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN SIMP_TAC[CARD_IMAGE_INJ; FINITE_INSERT; FINITE_RULES; VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN ASM_SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_RULES; IN_INSERT; NOT_IN_EMPTY; ARITH]]; ALL_TAC] THEN FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH `~(x = &0) ==> &0 < x \/ &0 < --x`)) THENL [EXISTS_TAC `basis 3:real^3`; EXISTS_TAC `--(basis 3):real^3`] THEN ASM_SIMP_TAC[NORM_BASIS; DIMINDEX_3; ARITH; IN_ELIM_THM; DOT_BASIS; NORM_NEG; DOT_LNEG; DIMINDEX_3; ARITH; VECTOR_SUB_COMPONENT; REAL_SUB_REFL; REAL_NEG_0] THEN X_GEN_TAC `x:real^3` THEN REWRITE_TAC[aff_ge_def; IN_AFFSIGN; sgn_ge] THEN REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`] THEN REWRITE_TAC[SET_RULE `x IN {a} <=> a = x`] THEN SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN; REAL_LE_ADD; FINITE_INSERT; CONJUNCT1 FINITE_RULES; REAL_ARITH `&0 <= x / &2 <=> &0 <= x`; RIGHT_EXISTS_AND_THM] THEN ASM_REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ARITH `x - y:real^3 = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN REWRITE_TAC[REAL_ARITH `&1 = x + y <=> x + y = &1`] THEN EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL [MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`; `h:real`] THEN STRIP_TAC THEN EXISTS_TAC `a % v1 + b % v2 + c % v3 + h % ((w:real^3)$1 % basis 1 + w$2 % basis 2):real^3` THEN EXISTS_TAC `h * (w:real^3)$3` THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE] THEN ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_3; ARITH; REAL_MUL_RZERO; REAL_ADD_RID] THEN REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN REPLICATE_TAC 4 AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM BASIS_EXPANSION] THEN REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID]; MAP_EVERY X_GEN_TAC [`y:real^3`; `h:real`] THEN STRIP_TAC THEN UNDISCH_TAC `(vec 0:real^3) IN affine hull {v1,v2,v3}` THEN SUBGOAL_THEN `(y - h / (w:real^3)$3 % (w$1 % basis 1 + w$2 % basis 2)) IN affine hull {v1:real^3,v2,v3}` MP_TAC THENL [ASM_SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT; BASIS_COMPONENT; ARITH; DIMINDEX_3] THEN REAL_ARITH_TAC; ALL_TAC] THEN SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; CONJUNCT1 FINITE_RULES; AFFINE_HULL_FINITE_STEP; IN_ELIM_THM] THEN REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ARITH `x - y:real^3 = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID; LEFT_IMP_EXISTS_THM] THEN REWRITE_TAC[REAL_ARITH `&1 = x + y <=> x + y = &1`] THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`] THEN STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`a':real`; `b':real`; `c':real`] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o SYM)) THEN MAP_EVERY EXISTS_TAC [`a + (&1 - (a + b + c + h / (w:real^3)$3)) * a'`; `b + (&1 - (a + b + c + h / (w:real^3)$3)) * b'`; `c + (&1 - (a + b + c + h / (w:real^3)$3)) * c'`; `h / (w:real^3)$3`] THEN ASM_REWRITE_TAC[REAL_ARITH `(a + x * a') + (b + x * b') + (c + x * c') + h:real = (a + b + c + h) + x * (a' + b' + c')`] THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE] THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[VECTOR_ARITH `(a + x * a') % v1 + (b + x * b') % v2 + (c + x * c') % v3 + h:real^N = (a % v1 + b % v2 + c % v3) + x % (a' % v1 + b' % v2 + c' % v3) + h`] THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN REWRITE_TAC[VECTOR_ARITH `(x + a) + y:real^3 = a + z <=> x + y = z`] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM BASIS_EXPANSION] THEN REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID] THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_DIV_RMUL; REAL_LT_IMP_NZ]; MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`; `h:real`] THEN STRIP_TAC THEN EXISTS_TAC `a % v1 + b % v2 + c % v3 + h % ((w:real^3)$1 % basis 1 + w$2 % basis 2):real^3` THEN EXISTS_TAC `h * --((w:real^3)$3)` THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE] THEN REWRITE_TAC[VECTOR_ARITH `(x * --y) % --z:real^N = (x * y) % z`] THEN ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_3; ARITH; REAL_MUL_RZERO; REAL_ADD_RID] THEN REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN REPLICATE_TAC 4 AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM BASIS_EXPANSION] THEN REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID]; MAP_EVERY X_GEN_TAC [`y:real^3`; `h:real`] THEN STRIP_TAC THEN UNDISCH_TAC `(vec 0:real^3) IN affine hull {v1,v2,v3}` THEN SUBGOAL_THEN `(y - h / --((w:real^3)$3) % (w$1 % basis 1 + w$2 % basis 2)) IN affine hull {v1:real^3,v2,v3}` MP_TAC THENL [ASM_SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT; BASIS_COMPONENT; ARITH; DIMINDEX_3] THEN REAL_ARITH_TAC; ALL_TAC] THEN SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; CONJUNCT1 FINITE_RULES; AFFINE_HULL_FINITE_STEP; IN_ELIM_THM] THEN REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ARITH `x - y:real^3 = z <=> x = y + z`] THEN REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID; LEFT_IMP_EXISTS_THM] THEN REWRITE_TAC[REAL_ARITH `&1 = x + y <=> x + y = &1`] THEN MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`] THEN STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`a':real`; `b':real`; `c':real`] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o SYM)) THEN MAP_EVERY EXISTS_TAC [`a + (&1 - (a + b + c + h / --((w:real^3)$3))) * a'`; `b + (&1 - (a + b + c + h / --((w:real^3)$3))) * b'`; `c + (&1 - (a + b + c + h / --((w:real^3)$3))) * c'`; `h / --((w:real^3)$3)`] THEN ASM_REWRITE_TAC[REAL_ARITH `(a + x * a') + (b + x * b') + (c + x * c') + h:real = (a + b + c + h) + x * (a' + b' + c')`] THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE] THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[VECTOR_ARITH `(a + x * a') % v1 + (b + x * b') % v2 + (c + x * c') % v3 + h:real^N = (a % v1 + b % v2 + c % v3) + x % (a' % v1 + b' % v2 + c' % v3) + h`] THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN REWRITE_TAC[VECTOR_ARITH `(x + a) + y:real^3 = a + z <=> x + y = z`] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM BASIS_EXPANSION] THEN REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID] THEN REWRITE_TAC[VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN REWRITE_TAC[real_div; REAL_INV_NEG; REAL_MUL_RNEG] THEN REWRITE_TAC[VECTOR_MUL_RNEG; VECTOR_MUL_LNEG; GSYM real_div] THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_DIV_RMUL; REAL_LT_IMP_NZ]]);;
let THEOREM = 
prove (`!v1 v2 v3 w:real^3. ~coplanar {v1, v2, v3, w} ==> (?nor. norm nor = &1 /\ (!x. x IN aff_ge {v1, v2, v3} {w} <=> (?xx h. xx IN affine hull {v1, v2, v3} /\ &0 <= h /\ x = xx + h % nor)) /\ (!x y. {x, y} SUBSET affine hull {v1, v2, v3} ==> nor dot (x - y) = &0))`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[VECTOR_ARITH `x:real^3 = y + h % z <=> x - y = h % z`] THEN MATCH_MP_TAC(MESON[] `(?a b. P(a - b)) ==> ?a:real^3. P a`) THEN MATCH_MP_TAC LEMMA THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC `affine hull {v1:real^3,v2,v3}` THEN REWRITE_TAC[HULL_SUBSET; plane] THEN ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);;