(* The following lemmas were removed from hull.ml on
   November 11, 2008 by T Hales, because the proofs are in error.
   They can be returned to hull.ml when the proofs are corrected.
*)


let VSUM_2 = 
prove ( `! (v:num->real^N). vsum (1..2) v = (v 1) + (v 2)`,
GEN_TAC THEN REWRITE_TAC[vsum; SUM_2] THEN VECTOR_ARITH_TAC);;
let affcomb_imp_aff = 
prove ( `!(S:real^N->bool). affine_comb S ==> affine S`,
GEN_TAC THEN REWRITE_TAC[affine;affine_comb] THEN STRIP_TAC THEN REPEAT GEN_TAC THEN FIRST_X_ASSUM (MP_TAC o SPECL [`2`;`(\i. if (i=1) then t else (&1-t))`;`(\i. if (i=1) then (u:real^N) else (v:real^N))`]) THEN SIMP_TAC[SUM_2;VSUM_2;ARITH_RULE `~(1=2)/\(!t. t + (&1 - t) = &1)`] THEN MESON_TAC[]);;
let aff_imp_affcomb = 
prove ( `!(S:real^N->bool). affine S ==> affine_comb S`,
GEN_TAC THEN REWRITE_TAC[affine;affine_comb] THEN DISCH_THEN (LABEL_TAC "1") THEN INDUCT_TAC THENL [ SIMP_TAC[SUM_CLAUSES_NUMSEG; ARITH_RULE `~(1=0) /\ ~ ( &1 = &0)`]; ALL_TAC ] THEN REPEAT GEN_TAC THEN REWRITE_TAC[ADD1] THEN ASM_CASES_TAC `( n = 0)` THENL [ ASM_SIMP_TAC[ARITH_RULE `0+1=1`] THEN REWRITE_TAC[SUM_SING_NUMSEG;NUMSEG_SING;VSUM_SING] THEN STRIP_TAC THEN ASM_SIMP_TAC[VECTOR_MUL_LID] THEN FIRST_ASSUM (MATCH_MP_TAC o SPEC `1`) THEN REWRITE_TAC[IN_SING; GSYM IN]; ALL_TAC ] THEN DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "3") (LABEL_TAC "4")) THEN UNDISCH_TAC (`sum (1..n + 1) (\i. t i) = &1`) THEN UNDISCH_TAC (`~(n=0)`) THEN REWRITE_TAC[IMP_IMP] THEN DISCH_THEN (LABEL_TAC "5") THEN FIRST_ASSUM(MP_TAC o (MATCH_MP comb_trans)) THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN ABBREV_TAC `(f:num->real^N) (i:num) = (&n * (t:num->real) i) % (v:num->real^N) i + (&1 - &n * t i) % v (n + 1)` THEN FIRST_X_ASSUM ((LABEL_TAC "6") o GSYM) THEN ABBREV_TAC `(ts:num->real) (i:num) = &1 / &n` THEN FIRST_X_ASSUM ((LABEL_TAC "7") o GSYM) THEN FIRST_ASSUM(MATCH_MP_TAC o (SPECL [`(ts:num->real)`;`(f:num->real^N)`])) THEN CONJ_TAC THENL [ ASM_REWRITE_TAC[SUM_CONST_NUMSEG; ARITH_RULE ` (n+1) - 1 = n`] THEN USE_THEN "5" (MP_TAC o (MATCH_MP (TAUT ` A/\B ==> A`))) THEN MESON_TAC[REAL_OF_NUM_NOT_EQ;REAL_DIV_LMUL]; GEN_TAC ] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "8") THEN USE_THEN "1" (MATCH_MP_TAC o (SPECL [`(v:num->real^N) (i:num)`;`(v:num->real^N) ((n:num) +1)`;`(&n * t i):real`])) THEN CONJ_TAC THENL [ USE_THEN "4" (MATCH_MP_TAC o (SPEC `i:num`)) THEN UNDISCH_TAC (`(1..n) i`) THEN REWRITE_TAC[numseg;IN_ELIM_THM] THEN ARITH_TAC; USE_THEN "4" (MATCH_MP_TAC o (SPEC `(n+1):num`)) THEN UNDISCH_TAC (`(1..n) i`) THEN REWRITE_TAC[numseg;IN_ELIM_THM] THEN ARITH_TAC]);;
let affine_affcomb = 
prove ( ` !(S:real^N->bool). affine(aff_comb S)`,
REWRITE_TAC[affine;aff_comb] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC `(n:num) + (n':num)` THEN ABBREV_TAC `(ts:num->real) (i:num) = (if ((1..n) i) then ((t:real)*((t':num->real) i)) else (&1 - t)*((t'':num->real)(i - n)) )` THEN FIRST_X_ASSUM(LABEL_TAC "ts" o GSYM) THEN EXISTS_TAC `ts : num->real` THEN ABBREV_TAC `(vs:num->real^N) (i:num) = (if ((1..n) i) then (v':num->real^N) i else (v'':num->real^N) (i - n) )` THEN FIRST_X_ASSUM(LABEL_TAC "vs" o GSYM) THEN EXISTS_TAC `vs:num->real^N` THEN REPEAT CONJ_TAC THENL [ASM_REWRITE_TAC[GSYM (MATCH_MP SUM_COMBINE_R (ARITH_RULE `1 <= n+1 /\ n <= n+n'`))] THEN REWRITE_TAC[MATCH_MP SUM_CASES (SPEC_ALL FINITE_NUMSEG);IN;numseg;IN_ELIM_THM] THEN SIMP_TAC[ARITH_RULE `((1 <= i /\ i <= n) /\ ~(1 <= i /\ i <= n))= F`] THEN SIMP_TAC[ARITH_RULE `((n + 1 <= i /\ i <= n + n')/\1 <= i /\ i <= n)= F`] THEN SIMP_TAC[ARITH_RULE `((n + 1 <= i /\ i <= n + n') /\ ~(1 <= i /\ i <= n))= (1 + n <= i /\ i <= n' + n)`] THEN REWRITE_TAC[EMPTY_GSPEC;SUM_CLAUSES;REAL_ADD_LID;REAL_ADD_RID;REAL_ADD_AC] THEN REWRITE_TAC[SUM_LMUL;SUM_OFFSET;GSYM numseg] THEN UNDISCH_TAC `sum (1..n) (\i. t' i) = &1` THEN REWRITE_TAC[ETA_AX] THEN DISCH_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `!(i:num). (i+n)-n=i`;REAL_MUL_RID] THEN ARITH_TAC; ASM_REWRITE_TAC[VMUL_CASES] THEN REWRITE_TAC [MATCH_MP VSUM_CASES (SPECL [`1`;`n+n':num`] FINITE_NUMSEG)] THEN REWRITE_TAC [IN;IN_ELIM_THM;numseg] THEN REWRITE_TAC [ARITH_RULE `((1 <= i /\ i <= n + n') /\ 1 <= i /\ i <= n) = (1 <= i /\ i <= n)`] THEN REWRITE_TAC [ARITH_RULE `((1 <= i /\ i <= n + n') /\ ~(1 <= i /\ i <= n)) = (1+n <= i /\ i <= n' + n)`] THEN REWRITE_TAC[GSYM VECTOR_MUL_ASSOC;GSYM numseg;VSUM_LMUL;VSUM_OFFSET;ARITH_RULE `!(i:num).(i+n)-n = i`]; ALL_TAC] THEN GEN_TAC THEN ASM_REWRITE_TAC[] THEN COND_CASES_TAC THENL [ UNDISCH_TAC `(1..n) i` ;UNDISCH_TAC `~(1..n) i`] THEN REWRITE_TAC[IMP_IMP;IN;IN_ELIM_THM;numseg] THENL [REWRITE_TAC[ARITH_RULE `((1 <= i /\ i <= n) /\ 1 <= i /\ i <= n + n')=(1 <= i /\ i <= n)`]; REWRITE_TAC[ARITH_RULE `(~(1 <= i /\ i <= n) /\ 1 <= i /\ i <= n + n')=(1 <= (i - n) /\ (i-n) <= n')`]] THEN DISCH_TAC THENL [FIRST_ASSUM(MATCH_MP_TAC o (SPEC `i:num`));FIRST_ASSUM(MATCH_MP_TAC o (SPEC `(i-n):num`))] THEN ASM_REWRITE_TAC[numseg;IN;IN_ELIM_THM]);;
let aff_eq_affcomb = 
prove ( `!(S:real^N->bool). aff S = aff_comb S`,
GEN_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL [ REWRITE_TAC[aff] THEN MATCH_MP_TAC(hull_SUBSET) THEN MESON_TAC[SUBSET_affcomb;affine_affcomb]; REWRITE_TAC[SUBSET;IN;aff_comb] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC ( MATCH_MP aff_imp_affcomb (SPEC `S:real^N->bool` affine_aff)) THEN ASM_REWRITE_TAC[affine_comb] THEN DISCH_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o (SPECL [`n:num`;`t:num->real`;`v:num->real^N`])) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN FIRST_X_ASSUM (MP_TAC o (SPEC `i:num`)) THEN MATCH_MP_TAC(TAUT `(B==>C) ==> ((A==>B)==> A ==> C)`) THEN MP_TAC (SPEC `S:real^N->bool` SUBSET_aff) THEN MESON_TAC [SUBSET;IN]]);;
let aff_2 = 
prove (` ! (a:real^N) (b:real^N). aff {a,b} = {u| ?(t:real). u = t % a + (&1 - t) % b}`,
REPEAT GEN_TAC THEN (ABBREV_TAC `(M:real^N ->bool) = {u| ?(t:real). u = t % a + (&1 - t) % b}`) THEN FIRST_X_ASSUM(LABEL_TAC "M" o GSYM) THEN MATCH_MP_TAC(SUBSET_ANTISYM) THEN CONJ_TAC THENL [ REWRITE_TAC[aff] THEN MATCH_MP_TAC(hull_SUBSET) THEN CONJ_TAC THENL [ ASM_REWRITE_TAC[SET_RULE ` {a,b} SUBSET M <=> (a IN M /\ b IN M)`;IN_ELIM_THM;IN] THEN CONJ_TAC THENL [EXISTS_TAC `&1`; EXISTS_TAC `&0`] THEN VECTOR_ARITH_TAC; ASM_REWRITE_TAC[affine;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC ` t * t' + (&1- t) * t''` THEN REWRITE_TAC[ARITH_RULE ` &1 - (t * t' + (&1 - t) * t'') = t * (&1 - t') + (&1 - t) * (&1 - t'')`] THEN VECTOR_ARITH_TAC ] ; ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;IN;aff_eq_affcomb;aff_comb] THEN GEN_TAC THEN STRIP_TAC THEN ABBREV_TAC `(ts: num ->real) i = ( if ( i = 1) then t else ( &1 - t))` THEN FIRST_X_ASSUM(LABEL_TAC "ts" o GSYM) THEN ABBREV_TAC `(vs: num ->real^N) i = ( if ( i = 1) then a else b)` THEN FIRST_X_ASSUM(LABEL_TAC "vs" o GSYM) THEN EXISTS_TAC `2` THEN EXISTS_TAC `(ts:num->real)` THEN EXISTS_TAC ` (vs:num->real^N) ` THEN ASM_REWRITE_TAC[SUM_2;VSUM_2;ARITH_RULE `~(2=1) /\ (t + &1 - t = &1)`] THEN GEN_TAC THEN STRIP_TAC THEN COND_CASES_TAC THEN ONCE_REWRITE_TAC[GSYM IN] THEN SET_TAC[] ]);;
(* let conv_insert = prove(`!S (v:real^3). FINITE S ==> (conv (v INSERT S) = {x | ?s t. (conv S s) /\ &0 <= t /\ t <= &1 /\ (x = t % s + (&1-t) % v)})`, REWRITE_TAC[conv;affsign;sgn_ge;FUN_EQ_THM;lin_combo;UNION_EMPTY]; SIMP_TAC[FINITE_INSERT;FINITE_RULES;VSUM_CLAUSES;SUM_CLAUSES]; REPEAT STRIP_TAC; ASM_REWRITE_TAC[elimin IN_INSERT;IN_ELIM_THM]; REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] ; (* *) DISJ_CASES_TAC (TAUT `(v IN S) \/ ~((v:real^3) IN S)`);; REPEAT STRIP_TAC; EXISTS_TAC `x:real^3`; EXISTS_TAC `&1`; ASM_REWRITE_TAC[REAL_ARITH `&0 <= (&1) /\ (&1 <= (&1)) /\ (&1 - &1 = &0)`;VECTOR_MUL_LID;VECTOR_MUL_LZERO;VECTOR_ADD_RID;]; ASM_MESON_TAC[]; (* 2 *) ABBREV_TAC `g = \w. (if (w=v:real^3) then (t* f v + (&1 - t)) else t * f w)`; EXISTS_TAC `g:real^3->real`; CONJ_TAC; EXPAND_TAC "g"; ASM_REWRITE_TAC[]; UNDISCH_TAC `FINITE (S:real^3->bool)`; (* to here *) *)