2 (* DEFINITIONS OF AFFINE HULL. *)
\r
3 (* ==================================================================== *)
\r
5 (* -------------------------------------------------------------------- *)
\r
6 (* Two ways to define affine set & affine hull. *)
\r
7 (* -------------------------------------------------------------------- *)
\r
9 (* Define as in convex.ml *)
\r
10 (* -------------------------------------------------------------------- *)
\r
12 (* Define using affine combination *)
\r
13 (* -------------------------------------------------------------------- *)
\r
15 let affine_comb = new_definition `!(s:real^N->bool). affine_comb s = ! (n:num) (t:num->real) (v:num->real^N).
\r
16 ( sum (1..n) (\i. t i) = &1)/\(!i. ((1..n) i) ==>(s (v i)))
\r
17 ==> (s (vsum (1..n) (\i. (t i) % (v i))))`;;
\r
19 let aff_comb = new_definition `! (S:real^N -> bool) (w:real^N). aff_comb S w =(
\r
20 ? (n:num) (t:num->real) (v:num->real^N).
\r
21 ( sum (1..n) (\i. t i) = &1 ) /\
\r
22 (w = vsum (1..n) (\i. (t i) % (v i)))/\ (!i. ((1..n) i) ==> (S (v i))) )`;;
\r
24 (* Some simple properties of affine, aff, affine_comb, aff_comb, hull *)
\r
25 (* -------------------------------------------------------------------- *)
\r
27 let affine_INTERS = prove
\r
28 ( `(!s. s IN f ==> affine s) ==> affine(INTERS f)`,
\r
29 (REWRITE_TAC[affine;INTERS;IN;IN_ELIM_THM] THEN MESON_TAC[]));;
\r
31 let affine_aff = prove
\r
32 ( `!(s:real^N->bool). affine (aff s)`,
\r
33 (GEN_TAC THEN REWRITE_TAC[aff] THEN MESON_TAC[affine_INTERS;P_HULL]));;
\r
35 let aff_affine = prove
\r
36 ( `!s. affine S ==> aff S = S`,
\r
37 (SIMP_TAC[HULL_EQ;aff;affine_INTERS]));;
\r
39 let SUBSET_hull = prove
\r
40 (`! s P. s SUBSET (P hull s)`,
\r
41 REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET;hull;IN_INTERS] THEN SET_TAC[]);;
\r
43 let SUBSET_aff = prove
\r
44 ( `!(S:real^N->bool). S SUBSET aff S`, MESON_TAC [SUBSET;aff;SUBSET_hull]);;
\r
46 let SUBSET_affcomb = prove
\r
47 (`!(S:real^N->bool). S SUBSET (aff_comb S)`,
\r
48 GEN_TAC THEN REWRITE_TAC[SUBSET;IN;aff_comb] THEN GEN_TAC THEN STRIP_TAC THEN
\r
49 EXISTS_TAC `1` THEN EXISTS_TAC `(\(i:num). &1)` THEN EXISTS_TAC `(\(i:num). x:real^N)` THEN
\r
50 ASM_SIMP_TAC[SUM_SING_NUMSEG;NUMSEG_SING;VSUM_SING;VECTOR_MUL_LID;IN;IN_SING]);;
\r
52 let aff_SUBSET = prove
\r
53 (`!A B. A SUBSET B ==> aff A SUBSET aff B`,
\r
54 (REPEAT GEN_TAC THEN
\r
55 REWRITE_TAC [aff; hull;SUBSET;IN;INTERS;IN_INTERS;IN_ELIM_THM] THEN MESON_TAC[]));;
\r
57 let INTERS_SUBSET = prove
\r
58 (`!(S:(A->bool)->bool) (u:A->bool). u IN S ==> (INTERS S) SUBSET u`,
\r
59 REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET;IN_INTERS] THEN MESON_TAC[]);;
\r
61 let hull_SUBSET = prove
\r
62 ( `!(P:(A->bool)->bool) (S:A->bool) (u:A->bool). (S SUBSET u)/\(P u) ==> (P hull S) SUBSET u`,
\r
63 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[hull] THEN MATCH_MP_TAC (INTERS_SUBSET) THEN
\r
64 ASM_REWRITE_TAC[IN;IN_ELIM_THM]);;
\r
66 (* Some lemmas need using *)
\r
67 (* --------------------------------------------------------------- *)
\r
70 (* VSUM_2 -> hull_error.ml *)
\r
72 let REAL_OF_NUM_NOT_EQ = prove
\r
73 ( `!n m. ~(m = n) <=> ~(&m = &n)`, MESON_TAC[REAL_OF_NUM_EQ]);;
\r
75 let VMUL_CASES = prove
\r
76 (`!(P:A->bool) (t:A->real) (t':A->real) (v:A->real^N) (v':A->real^N). (if P i then t i else t' i) % (if P i then v i else v' i) = (if P i then ( t i % v i) else (t' i % v' i))`,
\r
77 REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN ASM_MESON_TAC[]);;
\r
79 (* Relation between affine and affine_comb *)
\r
80 (* --------------------------------------------------------------- *)
\r
82 (* affcomb_imp_aff -> hull_error.ml *)
\r
85 let comb_trans = prove (
\r
86 `! (n:num) (t:num->real) (v:num->real^N).
\r
87 ~(n=0)/\(sum (1..n+1) (\i. t i) = &1)==>
\r
88 (vsum (1..n+1) (\i. (t i) % (v i)) = vsum (1..n) (\i. (&1 / &n) % ((&n * (t i)) % (v i) + (&1 - &n * (t i)) % (v (n+1)))))`,
\r
89 REPEAT GEN_TAC THEN
\r
90 REWRITE_TAC[ REAL_OF_NUM_NOT_EQ;VSUM_CMUL_NUMSEG; VECTOR_ADD_LDISTRIB;VSUM_ADD_NUMSEG] THEN
\r
91 REWRITE_TAC[GSYM VSUM_CMUL_NUMSEG; VECTOR_MUL_ASSOC;REAL_MUL_ASSOC;REAL_SUB_LDISTRIB] THEN
\r
92 STRIP_TAC THEN (FIRST_ASSUM (MP_TAC o MATCH_MP REAL_DIV_RMUL)) THEN STRIP_TAC THEN
\r
93 ASM_REWRITE_TAC[REAL_MUL_LID;REAL_MUL_RID] THEN
\r
94 REWRITE_TAC[MATCH_MP VSUM_CLAUSES_RIGHT (ARITH_RULE ` (0 < (n+1))/\(1 <= (n+1))`)] THEN
\r
95 ASM_REWRITE_TAC[ ARITH_RULE `! (n:num). (n + 1)-1 = n`;VSUM_RMUL] THEN
\r
96 ASM_REWRITE_TAC[SUM_CONST_NUMSEG;SUM_SUB_NUMSEG;REAL_MUL_SYM; ARITH_RULE `(n+1) -1 = n`] THEN
\r
97 (UNDISCH_TAC `sum (1..n + 1) (\i. t i) = &1`) THEN
\r
98 ASM_REWRITE_TAC [MATCH_MP SUM_CLAUSES_RIGHT (ARITH_RULE ` (0 < (n+1))/\(1 <= (n+1))`);ARITH_RULE `(n+1) - 1 = n`] THEN
\r
100 FIRST_ASSUM (MP_TAC o MATCH_MP (ARITH_RULE ` (a + b= &1) ==> (&1 - a = b)`)) THEN REWRITE_TAC[ETA_AX] THEN
\r
105 (* aff_imp_affcomb -> hull_error.ml *)
\r
108 (* The equality between two ways of defining, aff & aff_comb *)
\r
109 (* ------------------------------------------------------------------*)
\r
111 (* affine_affcomb -> hull_error.ml *)
\r
113 (* aff_eq_affcomb -> hull_error.ml *)
\r
115 (* convex, added by thales *)
\r
117 let conv0pt = prove(`conv {} = {}:real^A->bool`,
\r
118 REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]
\r
119 THEN REAL_ARITH_TAC);;
\r
121 let conv1pt = prove(`!u. conv {u:real^A} = {u}`,
\r
122 REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;elimin IN_SING] THEN
\r
123 REPEAT GEN_TAC THEN
\r
124 REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN
\r
125 REPEAT STRIP_TAC THENL
\r
126 [ASM_MESON_TAC[VECTOR_MUL_LID];
\r
127 ASM_REWRITE_TAC[]] THEN
\r
128 EXISTS_TAC `\ (v:real^A). &1` THEN
\r
129 MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`]
\r