168 thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5) |
168 thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5) |
169 by(auto simp add: setsum_clauses(2)) |
169 by(auto simp add: setsum_clauses(2)) |
170 next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s) |
170 next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s) |
171 case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real" |
171 case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real" |
172 assume IA:"\<And>u s. \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s; |
172 assume IA:"\<And>u s. \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s; |
173 s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n \<equiv> card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and |
173 s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and |
174 as:"Suc n \<equiv> card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" |
174 as:"Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" |
175 "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1" |
175 "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1" |
176 have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr) |
176 have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr) |
177 assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto |
177 assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto |
178 thus False using as(7) and `card s > 2` by (metis Numeral1_eq1_nat less_0_number_of less_int_code(15) |
178 thus False using as(7) and `card s > 2` by (metis Numeral1_eq1_nat less_0_number_of less_int_code(15) |
179 less_nat_number_of not_less_iff_gr_or_eq of_nat_1 of_nat_eq_iff pos2 rel_simps(4)) qed |
179 less_nat_number_of not_less_iff_gr_or_eq of_nat_1 of_nat_eq_iff pos2 rel_simps(4)) qed |
1343 proof(cases "s={}") |
1343 proof(cases "s={}") |
1344 case True thus ?thesis using compact_empty by simp |
1344 case True thus ?thesis using compact_empty by simp |
1345 next |
1345 next |
1346 case False then obtain w where "w\<in>s" by auto |
1346 case False then obtain w where "w\<in>s" by auto |
1347 show ?thesis unfolding caratheodory[of s] |
1347 show ?thesis unfolding caratheodory[of s] |
1348 proof(induct "CARD('n) + 1") |
1348 proof(induct ("CARD('n) + 1")) |
1349 have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" |
1349 have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" |
1350 using compact_empty by (auto simp add: convex_hull_empty) |
1350 using compact_empty by (auto simp add: convex_hull_empty) |
1351 case 0 thus ?case unfolding * by simp |
1351 case 0 thus ?case unfolding * by simp |
1352 next |
1352 next |
1353 case (Suc n) |
1353 case (Suc n) |