[STATEMENT]
lemma finite_convex_hull_iff_convex_hull_list: assumes Vs: "Vs \<subseteq> carrier_vec n"
  and id': "Vs = set Vsl'"
shows "convex_hull Vs = convex_hull_list Vsl'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have fin: "finite Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite Vs
[PROOF STEP]
unfolding id'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set Vsl')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite Vs

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
from finite_distinct_list fin
[PROOF STATE]
proof (chain)
picking this:
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A \<and> distinct xs
finite Vs
[PROOF STEP]
obtain Vsl
    where id: "Vs = set Vsl" and dist: "distinct Vsl"
[PROOF STATE]
proof (prove)
using this:
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A \<and> distinct xs
finite Vs

goal (1 subgoal):
 1. (\<And>Vsl. \<lbrakk>Vs = set Vsl; distinct Vsl\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vs = set Vsl
distinct Vsl

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
from Vs id
[PROOF STATE]
proof (chain)
picking this:
Vs \<subseteq> carrier_vec n
Vs = set Vsl
[PROOF STEP]
have Vsl: "set Vsl \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
Vs \<subseteq> carrier_vec n
Vs = set Vsl

goal (1 subgoal):
 1. set Vsl \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set Vsl \<subseteq> carrier_vec n

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set Vsl \<subseteq> carrier_vec n

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
fix c :: "nat \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "distinct Vsl \<Longrightarrow>(\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl))) =
                          sum c {0..<length Vsl}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct Vsl \<Longrightarrow> (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl))) = sum c {0..<length Vsl}
[PROOF STEP]
proof (induction Vsl rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
case (snoc v Vsl)
[PROOF STATE]
proof (state)
this:
distinct Vsl \<Longrightarrow> (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl))) = sum c {0..<length Vsl}
distinct (Vsl @ [v])

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
let ?coef = "\<lambda> x. sum_list (map c (find_indices x (Vsl @ [v])))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
let ?coef' = "\<lambda> x. sum_list (map c (find_indices x Vsl))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
have dist: "distinct Vsl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct Vsl
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
distinct (Vsl @ [v])

goal (1 subgoal):
 1. distinct Vsl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct Vsl

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
have "sum ?coef (set (Vsl @ [v])) = sum_list (map ?coef (Vsl @ [v]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<leftarrow>Vsl @ [v]. sum_list (map c (find_indices x (Vsl @ [v]))))
[PROOF STEP]
by (rule sum.distinct_set_conv_list[OF snoc.prems, of ?coef])
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<leftarrow>Vsl @ [v]. sum_list (map c (find_indices x (Vsl @ [v]))))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<leftarrow>Vsl @ [v]. sum_list (map c (find_indices x (Vsl @ [v]))))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
have "\<dots> = sum_list (map ?coef Vsl) + ?coef v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>Vsl @ [v]. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) + sum_list (map c (find_indices v (Vsl @ [v])))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>Vsl @ [v]. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) + sum_list (map c (find_indices v (Vsl @ [v])))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>Vsl @ [v]. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) + sum_list (map c (find_indices v (Vsl @ [v])))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
have "sum_list (map ?coef Vsl) = sum ?coef (set Vsl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v]))))
[PROOF STEP]
using sum.distinct_set_conv_list[OF dist, of ?coef]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v]))))

goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v]))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v]))))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v]))))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
have "\<dots> = sum ?coef' (set Vsl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl)))
[PROOF STEP]
proof (intro R.finsum_restrict[of ?coef] restrict_ext, standard)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
assume "x \<in> set Vsl"
[PROOF STATE]
proof (state)
this:
x \<in> set Vsl

goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set Vsl
[PROOF STEP]
obtain i where i: "i < length Vsl" and x: "x = Vsl ! i"
[PROOF STATE]
proof (prove)
using this:
x \<in> set Vsl

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Vsl; x = Vsl ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using in_set_conv_nth[of x Vsl]
[PROOF STATE]
proof (prove)
using this:
x \<in> set Vsl
(x \<in> set Vsl) = (\<exists>i<length Vsl. Vsl ! i = x)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Vsl; x = Vsl ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i < length Vsl
x = Vsl ! i

goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
hence "(Vsl @ [v]) ! i = x"
[PROOF STATE]
proof (prove)
using this:
i < length Vsl
x = Vsl ! i

goal (1 subgoal):
 1. (Vsl @ [v]) ! i = x
[PROOF STEP]
by (simp add: append_Cons_nth_left)
[PROOF STATE]
proof (state)
this:
(Vsl @ [v]) ! i = x

goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
hence "?coef x = c i"
[PROOF STATE]
proof (prove)
using this:
(Vsl @ [v]) ! i = x

goal (1 subgoal):
 1. sum_list (map c (find_indices x (Vsl @ [v]))) = c i
[PROOF STEP]
using distinct_list_find_indices[OF _ _ snoc.prems] i
[PROOF STATE]
proof (prove)
using this:
(Vsl @ [v]) ! i = x
\<lbrakk>?i < length (Vsl @ [v]); (Vsl @ [v]) ! ?i = ?x\<rbrakk> \<Longrightarrow> find_indices ?x (Vsl @ [v]) = [?i]
i < length Vsl

goal (1 subgoal):
 1. sum_list (map c (find_indices x (Vsl @ [v]))) = c i
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sum_list (map c (find_indices x (Vsl @ [v]))) = c i

goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (map c (find_indices x (Vsl @ [v]))) = c i

goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
have  "c i = ?coef' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c i = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
using distinct_list_find_indices[OF i _ dist] x
[PROOF STATE]
proof (prove)
using this:
Vsl ! i = ?x \<Longrightarrow> find_indices ?x Vsl = [i]
x = Vsl ! i

goal (1 subgoal):
 1. c i = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c i = sum_list (map c (find_indices x Vsl))

goal (1 subgoal):
 1. \<And>x. x \<in> set Vsl \<Longrightarrow> sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
show "?coef x = ?coef' x"
[PROOF STATE]
proof (prove)
using this:
sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))

goal (1 subgoal):
 1. sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum_list (map c (find_indices x (Vsl @ [v]))) = sum_list (map c (find_indices x Vsl))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl)))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x (Vsl @ [v])))) = (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl)))

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
have "\<dots> = sum c {0..<length Vsl}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl))) = sum c {0..<length Vsl}
[PROOF STEP]
by (rule snoc.IH[OF dist])
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl))) = sum c {0..<length Vsl}

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl))) = sum c {0..<length Vsl}

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
have "?coef v = c (length Vsl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map c (find_indices v (Vsl @ [v]))) = c (length Vsl)
[PROOF STEP]
using distinct_list_find_indices[OF _ _ snoc.prems, of "length Vsl" v]
          nth_append_length
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length Vsl < length (Vsl @ [v]); (Vsl @ [v]) ! length Vsl = v\<rbrakk> \<Longrightarrow> find_indices v (Vsl @ [v]) = [length Vsl]
(?xs @ ?x # ?ys) ! length ?xs = ?x

goal (1 subgoal):
 1. sum_list (map c (find_indices v (Vsl @ [v]))) = c (length Vsl)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (map c (find_indices v (Vsl @ [v]))) = c (length Vsl)

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> (\<Sum>x\<in>set xs. sum_list (map c (find_indices x xs))) = sum c {0..<length xs}; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>xa\<in>set (xs @ [x]). sum_list (map c (find_indices xa (xs @ [x])))) = sum c {0..<length (xs @ [x])}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = sum c {0..<length Vsl} + c (length Vsl)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = sum c {0..<length Vsl} + c (length Vsl)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = sum c {0..<length (Vsl @ [v])}
[PROOF STEP]
using sum.atLeast0_lessThan_Suc
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = sum c {0..<length Vsl} + c (length Vsl)
sum ?g {0..<Suc ?n} = sum ?g {0..<?n} + ?g ?n

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = sum c {0..<length (Vsl @ [v])}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Vsl @ [v]). sum_list (map c (find_indices x (Vsl @ [v])))) = sum c {0..<length (Vsl @ [v])}

goal (1 subgoal):
 1. distinct [] \<Longrightarrow> (\<Sum>x\<in>set []. sum_list (map c (find_indices x []))) = sum c {0..<length []}
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
distinct Vsl \<Longrightarrow> (\<Sum>x\<in>set Vsl. sum_list (map c (find_indices x Vsl))) = sum c {0..<length Vsl}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
distinct Vsl \<Longrightarrow> (\<Sum>x\<in>set Vsl. sum_list (map ?c5 (find_indices x Vsl))) = sum ?c5 {0..<length Vsl}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
note sum_sumlist = this
[PROOF STATE]
proof (state)
this:
distinct Vsl \<Longrightarrow> (\<Sum>x\<in>set Vsl. sum_list (map ?c5 (find_indices x Vsl))) = sum ?c5 {0..<length Vsl}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
distinct Vsl \<Longrightarrow> (\<Sum>x\<in>set Vsl. sum_list (map ?c5 (find_indices x Vsl))) = sum ?c5 {0..<length Vsl}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
assume "b \<in> convex_hull_list Vsl"
[PROOF STATE]
proof (state)
this:
b \<in> convex_hull_list Vsl

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> convex_hull_list Vsl
[PROOF STEP]
obtain c where b: "lincomb_list c Vsl = b" and c: "(\<forall> i < length Vsl. c i \<ge> 0)"
      and c1: "sum c {0..<length Vsl} = 1"
[PROOF STATE]
proof (prove)
using this:
b \<in> convex_hull_list Vsl

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>lincomb_list c Vsl = b; \<forall>i<length Vsl. (0::'a) \<le> c i; sum c {0..<length Vsl} = (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
[PROOF STATE]
proof (prove)
using this:
b \<in> {x. \<exists>c. (lincomb_list c Vsl = x \<and> (\<forall>i<length Vsl. (0::'a) \<le> c i)) \<and> sum c {0..<length Vsl} = (1::'a)}

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>lincomb_list c Vsl = b; \<forall>i<length Vsl. (0::'a) \<le> c i; sum c {0..<length Vsl} = (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list c Vsl = b
\<forall>i<length Vsl. (0::'a) \<le> c i
sum c {0..<length Vsl} = (1::'a)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "convex_lincomb (mk_coeff Vsl c) Vs b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_lincomb (mk_coeff Vsl c) Vs b
[PROOF STEP]
unfolding b[symmetric] convex_lincomb_def nonneg_lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lincomb (mk_coeff Vsl c) Vs = lincomb_list c Vsl \<and> mk_coeff Vsl c ` Vs \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum (mk_coeff Vsl c) Vs = (1::'a)
[PROOF STEP]
apply (subst lincomb_list_as_lincomb[OF Vsl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lincomb (mk_coeff Vsl c) Vs = lincomb (mk_coeff Vsl c) (set Vsl) \<and> mk_coeff Vsl c ` Vs \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum (mk_coeff Vsl c) Vs = (1::'a)
[PROOF STEP]
by (insert c c1, auto simp: id mk_coeff_def dist sum_sumlist intro!: sum_list_nonneg)
[PROOF STATE]
proof (state)
this:
convex_lincomb (mk_coeff Vsl c) Vs b

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
hence "b \<in> convex_hull Vs"
[PROOF STATE]
proof (prove)
using this:
convex_lincomb (mk_coeff Vsl c) Vs b

goal (1 subgoal):
 1. b \<in> convex_hull Vs
[PROOF STEP]
unfolding convex_hull_def convex_lincomb_def
[PROOF STATE]
proof (prove)
using this:
nonneg_lincomb (mk_coeff Vsl c) Vs b \<and> sum (mk_coeff Vsl c) Vs = (1::'a)

goal (1 subgoal):
 1. b \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> Vs \<and> nonneg_lincomb c Ws x \<and> sum c Ws = (1::'a)}
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
nonneg_lincomb (mk_coeff Vsl c) Vs b \<and> sum (mk_coeff Vsl c) Vs = (1::'a)
finite Vs

goal (1 subgoal):
 1. b \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> Vs \<and> nonneg_lincomb c Ws x \<and> sum c Ws = (1::'a)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<in> convex_hull Vs

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b5 \<in> convex_hull_list Vsl \<Longrightarrow> ?b5 \<in> convex_hull Vs

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?b5 \<in> convex_hull_list Vsl \<Longrightarrow> ?b5 \<in> convex_hull Vs

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?b5 \<in> convex_hull_list Vsl \<Longrightarrow> ?b5 \<in> convex_hull Vs

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
assume "b \<in> convex_hull Vs"
[PROOF STATE]
proof (state)
this:
b \<in> convex_hull Vs

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> convex_hull Vs
[PROOF STEP]
obtain c Ws where Ws: "Ws \<subseteq> Vs" and b: "lincomb c Ws = b"
      and c: "c ` Ws \<subseteq> {x. x \<ge> 0}" and c1: "sum c Ws = 1"
[PROOF STATE]
proof (prove)
using this:
b \<in> convex_hull Vs

goal (1 subgoal):
 1. (\<And>Ws c. \<lbrakk>Ws \<subseteq> Vs; lincomb c Ws = b; c ` Ws \<subseteq> {x. (0::'a) \<le> x}; sum c Ws = (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def
[PROOF STATE]
proof (prove)
using this:
b \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> Vs \<and> (lincomb c Ws = x \<and> c ` Ws \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum c Ws = (1::'a)}

goal (1 subgoal):
 1. (\<And>Ws c. \<lbrakk>Ws \<subseteq> Vs; lincomb c Ws = b; c ` Ws \<subseteq> {x. (0::'a) \<le> x}; sum c Ws = (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ws \<subseteq> Vs
lincomb c Ws = b
c ` Ws \<subseteq> {x. (0::'a) \<le> x}
sum c Ws = (1::'a)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
let ?d = "\<lambda> x. if x \<in> Ws then c x else 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "lincomb ?d Vs = lincomb c Ws + lincomb (\<lambda> x. 0) (Vs - Ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = lincomb c Ws + lincomb (\<lambda>x. 0::'a) (Vs - Ws)
[PROOF STEP]
using lincomb_union2[OF _ _ Diff_disjoint[of Ws Vs], of c "\<lambda> x. 0"]
        fin Vs Diff_partition[OF Ws]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (Ws \<union> (Vs - Ws)); Ws \<union> (Vs - Ws) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb c Ws + lincomb (\<lambda>x. 0::'a) (Vs - Ws) = lincomb (\<lambda>v. if v \<in> Ws then c v else (0::'a)) (Ws \<union> (Vs - Ws))
finite Vs
Vs \<subseteq> carrier_vec n
Ws \<union> (Vs - Ws) = Vs

goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = lincomb c Ws + lincomb (\<lambda>x. 0::'a) (Vs - Ws)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = lincomb c Ws + lincomb (\<lambda>x. 0::'a) (Vs - Ws)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = lincomb c Ws + lincomb (\<lambda>x. 0::'a) (Vs - Ws)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "lincomb (\<lambda> x. 0) (Vs - Ws) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>x. 0::'a) (Vs - Ws) = 0\<^sub>v n
[PROOF STEP]
using lincomb_zero[of "Vs - Ws" "\<lambda> x. 0"] Vs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Vs - Ws \<subseteq> carrier_vec n; (\<lambda>x. 0::'a) \<in> Vs - Ws \<rightarrow> {0::'a}\<rbrakk> \<Longrightarrow> lincomb (\<lambda>x. 0::'a) (Vs - Ws) = 0\<^sub>v n
Vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb (\<lambda>x. 0::'a) (Vs - Ws) = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. 0::'a) (Vs - Ws) = 0\<^sub>v n

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = lincomb c Ws + 0\<^sub>v n
[PROOF STEP]
have "lincomb ?d Vs = b"
[PROOF STATE]
proof (prove)
using this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = lincomb c Ws + 0\<^sub>v n

goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = b
[PROOF STEP]
using b lincomb_closed Vs Ws
[PROOF STATE]
proof (prove)
using this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = lincomb c Ws + 0\<^sub>v n
lincomb c Ws = b
?S \<subseteq> carrier_vec n \<Longrightarrow> lincomb ?a ?S \<in> carrier_vec n
Vs \<subseteq> carrier_vec n
Ws \<subseteq> Vs

goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = b

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = b

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "?d ` Vs \<subseteq> {t. t \<ge> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> Ws then c x else (0::'a)) ` Vs \<subseteq> {t. (0::'a) \<le> t}
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
c ` Ws \<subseteq> {x. (0::'a) \<le> x}

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> Ws then c x else (0::'a)) ` Vs \<subseteq> {t. (0::'a) \<le> t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> Ws then c x else (0::'a)) ` Vs \<subseteq> {t. (0::'a) \<le> t}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> Ws then c x else (0::'a)) ` Vs \<subseteq> {t. (0::'a) \<le> t}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "sum ?d Vs = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>Vs. if x \<in> Ws then c x else (0::'a)) = (1::'a)
[PROOF STEP]
using  c1 R.extend_sum[OF fin Ws]
[PROOF STATE]
proof (prove)
using this:
sum c Ws = (1::'a)
(\<Sum>x\<in>Vs. if x \<in> Ws then ?a x else (0::'a)) = sum ?a Ws

goal (1 subgoal):
 1. (\<Sum>x\<in>Vs. if x \<in> Ws then c x else (0::'a)) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Vs. if x \<in> Ws then c x else (0::'a)) = (1::'a)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = b
(\<lambda>x. if x \<in> Ws then c x else (0::'a)) ` Vs \<subseteq> {t. (0::'a) \<le> t}
(\<Sum>x\<in>Vs. if x \<in> Ws then c x else (0::'a)) = (1::'a)
[PROOF STEP]
have "\<exists> c. convex_lincomb c Vs b"
[PROOF STATE]
proof (prove)
using this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = b
(\<lambda>x. if x \<in> Ws then c x else (0::'a)) ` Vs \<subseteq> {t. (0::'a) \<le> t}
(\<Sum>x\<in>Vs. if x \<in> Ws then c x else (0::'a)) = (1::'a)

goal (1 subgoal):
 1. \<exists>c. convex_lincomb c Vs b
[PROOF STEP]
unfolding convex_lincomb_def nonneg_lincomb_def
[PROOF STATE]
proof (prove)
using this:
lincomb (\<lambda>x. if x \<in> Ws then c x else (0::'a)) Vs = b
(\<lambda>x. if x \<in> Ws then c x else (0::'a)) ` Vs \<subseteq> {t. (0::'a) \<le> t}
(\<Sum>x\<in>Vs. if x \<in> Ws then c x else (0::'a)) = (1::'a)

goal (1 subgoal):
 1. \<exists>c. (lincomb c Vs = b \<and> c ` Vs \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum c Vs = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>c. convex_lincomb c Vs b

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b5 \<in> convex_hull Vs \<Longrightarrow> \<exists>c. convex_lincomb c Vs ?b5

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?b5 \<in> convex_hull Vs \<Longrightarrow> \<exists>c. convex_lincomb c Vs ?b5

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?b5 \<in> convex_hull Vs \<Longrightarrow> \<exists>c. convex_lincomb c Vs ?b5

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
assume "\<exists> c. convex_lincomb c Vs b"
[PROOF STATE]
proof (state)
this:
\<exists>c. convex_lincomb c Vs b

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. convex_lincomb c Vs b
[PROOF STEP]
obtain c where b: "lincomb c Vs = b" and c: "c ` Vs \<subseteq> {x. x \<ge> 0}"
      and c1: "sum c Vs = 1"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. convex_lincomb c Vs b

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>lincomb c Vs = b; c ` Vs \<subseteq> {x. (0::'a) \<le> x}; sum c Vs = (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding convex_lincomb_def nonneg_lincomb_def
[PROOF STATE]
proof (prove)
using this:
\<exists>c. (lincomb c Vs = b \<and> c ` Vs \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum c Vs = (1::'a)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>lincomb c Vs = b; c ` Vs \<subseteq> {x. (0::'a) \<le> x}; sum c Vs = (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb c Vs = b
c ` Vs \<subseteq> {x. (0::'a) \<le> x}
sum c Vs = (1::'a)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
from lincomb_as_lincomb_list_distinct[OF Vsl dist, of c]
[PROOF STATE]
proof (chain)
picking this:
lincomb c (set Vsl) = lincomb_list (\<lambda>i. c (Vsl ! i)) Vsl
[PROOF STEP]
have b: "lincomb_list (\<lambda>i. c (Vsl ! i)) Vsl = b"
[PROOF STATE]
proof (prove)
using this:
lincomb c (set Vsl) = lincomb_list (\<lambda>i. c (Vsl ! i)) Vsl

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. c (Vsl ! i)) Vsl = b
[PROOF STEP]
unfolding b[symmetric] id
[PROOF STATE]
proof (prove)
using this:
lincomb c (set Vsl) = lincomb_list (\<lambda>i. c (Vsl ! i)) Vsl

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. c (Vsl ! i)) Vsl = lincomb c (set Vsl)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. c (Vsl ! i)) Vsl = b

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "1 = sum c (set Vsl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) = sum c (set Vsl)
[PROOF STEP]
using c1 id
[PROOF STATE]
proof (prove)
using this:
sum c Vs = (1::'a)
Vs = set Vsl

goal (1 subgoal):
 1. (1::'a) = sum c (set Vsl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1::'a) = sum c (set Vsl)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::'a) = sum c (set Vsl)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "\<dots> = sum_list (map c Vsl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum c (set Vsl) = sum_list (map c Vsl)
[PROOF STEP]
by(rule sum.distinct_set_conv_list[OF dist])
[PROOF STATE]
proof (state)
this:
sum c (set Vsl) = sum_list (map c Vsl)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum c (set Vsl) = sum_list (map c Vsl)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "\<dots> = sum ((!) (map c Vsl)) {0..<length Vsl}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map c Vsl) = sum ((!) (map c Vsl)) {0..<length Vsl}
[PROOF STEP]
using sum_list_sum_nth length_map
[PROOF STATE]
proof (prove)
using this:
sum_list ?xs = sum ((!) ?xs) {0..<length ?xs}
length (map ?f ?xs) = length ?xs

goal (1 subgoal):
 1. sum_list (map c Vsl) = sum ((!) (map c Vsl)) {0..<length Vsl}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sum_list (map c Vsl) = sum ((!) (map c Vsl)) {0..<length Vsl}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (map c Vsl) = sum ((!) (map c Vsl)) {0..<length Vsl}

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "\<dots> = sum (\<lambda> i. c (Vsl ! i)) {0..<length Vsl}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) (map c Vsl)) {0..<length Vsl} = (\<Sum>i = 0..<length Vsl. c (Vsl ! i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum ((!) (map c Vsl)) {0..<length Vsl} = (\<Sum>i = 0..<length Vsl. c (Vsl ! i))

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1::'a) = (\<Sum>i = 0..<length Vsl. c (Vsl ! i))
[PROOF STEP]
have sum_1: "(\<Sum>i = 0..<length Vsl. c (Vsl ! i)) = 1"
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (\<Sum>i = 0..<length Vsl. c (Vsl ! i))

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vsl. c (Vsl ! i)) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vsl. c (Vsl ! i)) = (1::'a)

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "\<exists> c. convex_lincomb_list c Vsl b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. convex_lincomb_list c Vsl b
[PROOF STEP]
unfolding convex_lincomb_list_def nonneg_lincomb_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. (lincomb_list c Vsl = b \<and> (\<forall>i<length Vsl. (0::'a) \<le> c i)) \<and> sum c {0..<length Vsl} = (1::'a)
[PROOF STEP]
by (intro exI[of _ "\<lambda>i. c (Vsl ! i)"] conjI b sum_1)
        (insert c, force simp: set_conv_nth id)
[PROOF STATE]
proof (state)
this:
\<exists>c. convex_lincomb_list c Vsl b

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
hence "b \<in> convex_hull_list Vsl"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. convex_lincomb_list c Vsl b

goal (1 subgoal):
 1. b \<in> convex_hull_list Vsl
[PROOF STEP]
unfolding convex_hull_list_def
[PROOF STATE]
proof (prove)
using this:
\<exists>c. convex_lincomb_list c Vsl b

goal (1 subgoal):
 1. b \<in> {x. \<exists>c. convex_lincomb_list c Vsl x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> convex_hull_list Vsl

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>c. convex_lincomb c Vs ?b5 \<Longrightarrow> ?b5 \<in> convex_hull_list Vsl

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?b5 \<in> convex_hull_list Vsl \<Longrightarrow> ?b5 \<in> convex_hull Vs
?b5 \<in> convex_hull Vs \<Longrightarrow> \<exists>c. convex_lincomb c Vs ?b5
\<exists>c. convex_lincomb c Vs ?b5 \<Longrightarrow> ?b5 \<in> convex_hull_list Vsl
[PROOF STEP]
have "convex_hull Vs = convex_hull_list Vsl"
[PROOF STATE]
proof (prove)
using this:
?b5 \<in> convex_hull_list Vsl \<Longrightarrow> ?b5 \<in> convex_hull Vs
?b5 \<in> convex_hull Vs \<Longrightarrow> \<exists>c. convex_lincomb c Vs ?b5
\<exists>c. convex_lincomb c Vs ?b5 \<Longrightarrow> ?b5 \<in> convex_hull_list Vsl

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
convex_hull Vs = convex_hull_list Vsl

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
convex_hull Vs = convex_hull_list Vsl

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
have "convex_hull_list Vsl = convex_hull_list Vsl'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull_list Vsl = convex_hull_list Vsl'
[PROOF STEP]
using convex_hull_list_eq_set[OF Vsl, of Vsl'] id id'
[PROOF STATE]
proof (prove)
using this:
set Vsl = set Vsl' \<Longrightarrow> convex_hull_list Vsl = convex_hull_list Vsl'
Vs = set Vsl
Vs = set Vsl'

goal (1 subgoal):
 1. convex_hull_list Vsl = convex_hull_list Vsl'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
convex_hull_list Vsl = convex_hull_list Vsl'

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
convex_hull Vs = convex_hull_list Vsl'

goal (1 subgoal):
 1. convex_hull Vs = convex_hull_list Vsl'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
convex_hull Vs = convex_hull_list Vsl'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_convex_hull: "convex S \<Longrightarrow> convex_hull S = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex S \<Longrightarrow> convex_hull S = S
[PROOF STEP]
unfolding convex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull S = S \<Longrightarrow> convex_hull S = S
[PROOF STEP]
by auto


[STATEMENT]
lemma convex_hull_convex_hull_listD: assumes A: "A \<subseteq> carrier_vec n"
  and x: "x \<in> convex_hull A"
shows "\<exists> as. set as \<subseteq> A \<and> x \<in> convex_hull_list as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
from x[unfolded convex_hull_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> A \<and> convex_lincomb c Ws x}
[PROOF STEP]
obtain X c where finX: "finite X" and XA: "X \<subseteq> A" and "convex_lincomb c X x"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> A \<and> convex_lincomb c Ws x}

goal (1 subgoal):
 1. (\<And>X c. \<lbrakk>finite X; X \<subseteq> A; convex_lincomb c X x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite X
X \<subseteq> A
convex_lincomb c X x

goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
hence x: "x \<in> convex_hull X"
[PROOF STATE]
proof (prove)
using this:
finite X
X \<subseteq> A
convex_lincomb c X x

goal (1 subgoal):
 1. x \<in> convex_hull X
[PROOF STEP]
unfolding convex_hull_def
[PROOF STATE]
proof (prove)
using this:
finite X
X \<subseteq> A
convex_lincomb c X x

goal (1 subgoal):
 1. x \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> X \<and> convex_lincomb c Ws x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull X

goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
from finite_list[OF finX]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs. set xs = X
[PROOF STEP]
obtain xs where X: "X = set xs"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs. set xs = X

goal (1 subgoal):
 1. (\<And>xs. X = set xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X = set xs

goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
from finite_convex_hull_iff_convex_hull_list[OF _ this] x XA A
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> carrier_vec n \<Longrightarrow> convex_hull X = convex_hull_list xs
x \<in> convex_hull X
X \<subseteq> A
A \<subseteq> carrier_vec n
[PROOF STEP]
have x: "x \<in> convex_hull_list xs"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier_vec n \<Longrightarrow> convex_hull X = convex_hull_list xs
x \<in> convex_hull X
X \<subseteq> A
A \<subseteq> carrier_vec n

goal (1 subgoal):
 1. x \<in> convex_hull_list xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull_list xs

goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull_list xs

goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
using XA
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull_list xs
X \<subseteq> A

goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
unfolding X
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull_list xs
set xs \<subseteq> A

goal (1 subgoal):
 1. \<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_hull_convex_sum: assumes A: "A \<subseteq> carrier_vec n"
  and x: "x \<in> convex_hull A"
  and y: "y \<in> convex_hull A"
  and a: "0 \<le> a" "a \<le> 1"
shows "a \<cdot>\<^sub>v x + (1 - a) \<cdot>\<^sub>v y \<in> convex_hull A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
from convex_hull_convex_hull_listD[OF A x]
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as
[PROOF STEP]
obtain xs where xs: "set xs \<subseteq> A"
    and x: "x \<in> convex_hull_list xs"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. set as \<subseteq> A \<and> x \<in> convex_hull_list as

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs \<subseteq> A; x \<in> convex_hull_list xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> A
x \<in> convex_hull_list xs

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
from convex_hull_convex_hull_listD[OF A y]
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. set as \<subseteq> A \<and> y \<in> convex_hull_list as
[PROOF STEP]
obtain ys where ys: "set ys \<subseteq> A"
    and y: "y \<in> convex_hull_list ys"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. set as \<subseteq> A \<and> y \<in> convex_hull_list as

goal (1 subgoal):
 1. (\<And>ys. \<lbrakk>set ys \<subseteq> A; y \<in> convex_hull_list ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ys \<subseteq> A
y \<in> convex_hull_list ys

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
have fin: "finite (set (xs @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set (xs @ ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set (xs @ ys))

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
have sub: "set (xs @ ys) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs @ ys) \<subseteq> A
[PROOF STEP]
using xs ys
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> A
set ys \<subseteq> A

goal (1 subgoal):
 1. set (xs @ ys) \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (xs @ ys) \<subseteq> A

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
from convex_hull_list_mono[of "xs @ ys" xs] x sub A
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set (xs @ ys) \<subseteq> carrier_vec n; set xs \<subseteq> set (xs @ ys)\<rbrakk> \<Longrightarrow> convex_hull_list xs \<subseteq> convex_hull_list (xs @ ys)
x \<in> convex_hull_list xs
set (xs @ ys) \<subseteq> A
A \<subseteq> carrier_vec n
[PROOF STEP]
have x: "x \<in> convex_hull_list (xs @ ys)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set (xs @ ys) \<subseteq> carrier_vec n; set xs \<subseteq> set (xs @ ys)\<rbrakk> \<Longrightarrow> convex_hull_list xs \<subseteq> convex_hull_list (xs @ ys)
x \<in> convex_hull_list xs
set (xs @ ys) \<subseteq> A
A \<subseteq> carrier_vec n

goal (1 subgoal):
 1. x \<in> convex_hull_list (xs @ ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull_list (xs @ ys)

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
from convex_hull_list_mono[of "xs @ ys" ys] y sub A
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set (xs @ ys) \<subseteq> carrier_vec n; set ys \<subseteq> set (xs @ ys)\<rbrakk> \<Longrightarrow> convex_hull_list ys \<subseteq> convex_hull_list (xs @ ys)
y \<in> convex_hull_list ys
set (xs @ ys) \<subseteq> A
A \<subseteq> carrier_vec n
[PROOF STEP]
have y: "y \<in> convex_hull_list (xs @ ys)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set (xs @ ys) \<subseteq> carrier_vec n; set ys \<subseteq> set (xs @ ys)\<rbrakk> \<Longrightarrow> convex_hull_list ys \<subseteq> convex_hull_list (xs @ ys)
y \<in> convex_hull_list ys
set (xs @ ys) \<subseteq> A
A \<subseteq> carrier_vec n

goal (1 subgoal):
 1. y \<in> convex_hull_list (xs @ ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> convex_hull_list (xs @ ys)

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
from convex_hull_list_combination[OF _ x y a]
[PROOF STATE]
proof (chain)
picking this:
set (xs @ ys) \<subseteq> carrier_vec n \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)
[PROOF STEP]
have "a \<cdot>\<^sub>v x + (1 - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)"
[PROOF STATE]
proof (prove)
using this:
set (xs @ ys) \<subseteq> carrier_vec n \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)
[PROOF STEP]
using sub A
[PROOF STATE]
proof (prove)
using this:
set (xs @ ys) \<subseteq> carrier_vec n \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)
set (xs @ ys) \<subseteq> A
A \<subseteq> carrier_vec n

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
from finite_convex_hull_iff_convex_hull_list[of _ "xs @ ys"] this sub A
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?Vs \<subseteq> carrier_vec n; ?Vs = set (xs @ ys)\<rbrakk> \<Longrightarrow> convex_hull ?Vs = convex_hull_list (xs @ ys)
a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)
set (xs @ ys) \<subseteq> A
A \<subseteq> carrier_vec n
[PROOF STEP]
have "a \<cdot>\<^sub>v x + (1 - a) \<cdot>\<^sub>v y \<in> convex_hull (set (xs @ ys))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?Vs \<subseteq> carrier_vec n; ?Vs = set (xs @ ys)\<rbrakk> \<Longrightarrow> convex_hull ?Vs = convex_hull_list (xs @ ys)
a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull_list (xs @ ys)
set (xs @ ys) \<subseteq> A
A \<subseteq> carrier_vec n

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull (set (xs @ ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull (set (xs @ ys))

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
with convex_hull_mono[OF sub]
[PROOF STATE]
proof (chain)
picking this:
convex_hull (set (xs @ ys)) \<subseteq> convex_hull A
a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull (set (xs @ ys))
[PROOF STEP]
show "a \<cdot>\<^sub>v x + (1 - a) \<cdot>\<^sub>v y \<in> convex_hull A"
[PROOF STATE]
proof (prove)
using this:
convex_hull (set (xs @ ys)) \<subseteq> convex_hull A
a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull (set (xs @ ys))

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convexI: assumes S: "S \<subseteq> carrier_vec n"
  and step: "\<And> a x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a \<cdot>\<^sub>v x + (1 - a) \<cdot>\<^sub>v y \<in> S"
shows "convex S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex S
[PROOF STEP]
unfolding convex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull S = S
[PROOF STEP]
proof (standard, standard)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> convex_hull S \<Longrightarrow> x \<in> S
 2. S \<subseteq> convex_hull S
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> convex_hull S \<Longrightarrow> x \<in> S
 2. S \<subseteq> convex_hull S
[PROOF STEP]
assume "z \<in> convex_hull S"
[PROOF STATE]
proof (state)
this:
z \<in> convex_hull S

goal (2 subgoals):
 1. \<And>x. x \<in> convex_hull S \<Longrightarrow> x \<in> S
 2. S \<subseteq> convex_hull S
[PROOF STEP]
from this[unfolded convex_hull_def]
[PROOF STATE]
proof (chain)
picking this:
z \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> S \<and> convex_lincomb c Ws x}
[PROOF STEP]
obtain W c where "finite W" and WS: "W \<subseteq> S"
    and "convex_lincomb c W z"
[PROOF STATE]
proof (prove)
using this:
z \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> S \<and> convex_lincomb c Ws x}

goal (1 subgoal):
 1. (\<And>W c. \<lbrakk>finite W; W \<subseteq> S; convex_lincomb c W z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite W
W \<subseteq> S
convex_lincomb c W z

goal (2 subgoals):
 1. \<And>x. x \<in> convex_hull S \<Longrightarrow> x \<in> S
 2. S \<subseteq> convex_hull S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite W
W \<subseteq> S
convex_lincomb c W z
[PROOF STEP]
show "z \<in> S"
[PROOF STATE]
proof (prove)
using this:
finite W
W \<subseteq> S
convex_lincomb c W z

goal (1 subgoal):
 1. z \<in> S
[PROOF STEP]
proof (induct W arbitrary: c z)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c z. \<lbrakk>{} \<subseteq> S; convex_lincomb c {} z\<rbrakk> \<Longrightarrow> z \<in> S
 2. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> S
convex_lincomb c {} z

goal (2 subgoals):
 1. \<And>c z. \<lbrakk>{} \<subseteq> S; convex_lincomb c {} z\<rbrakk> \<Longrightarrow> z \<in> S
 2. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> S
convex_lincomb c {} z

goal (1 subgoal):
 1. z \<in> S
[PROOF STEP]
unfolding convex_lincomb_def
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> S
nonneg_lincomb c {} z \<and> sum c {} = (1::'a)

goal (1 subgoal):
 1. z \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> S

goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
case (insert w W c z)
[PROOF STATE]
proof (state)
this:
finite W
w \<notin> W
\<lbrakk>W \<subseteq> S; convex_lincomb ?c3 W ?z3\<rbrakk> \<Longrightarrow> ?z3 \<in> S
insert w W \<subseteq> S
convex_lincomb c (insert w W) z

goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
have "convex_lincomb c (insert w W) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_lincomb c (insert w W) z
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
convex_lincomb c (insert w W) z

goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
hence zl: "z = lincomb c (insert w W)" and nonneg: "\<And> w. w \<in> W \<Longrightarrow> 0 \<le> c w"
      and cw: "c w \<ge> 0"
      and sum: "sum c (insert w W) = 1"
[PROOF STATE]
proof (prove)
using this:
convex_lincomb c (insert w W) z

goal (1 subgoal):
 1. (z = lincomb c (insert w W) &&& (\<And>w. w \<in> W \<Longrightarrow> (0::'a) \<le> c w)) &&& (0::'a) \<le> c w &&& sum c (insert w W) = (1::'a)
[PROOF STEP]
unfolding convex_lincomb_def nonneg_lincomb_def
[PROOF STATE]
proof (prove)
using this:
(lincomb c (insert w W) = z \<and> c ` insert w W \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum c (insert w W) = (1::'a)

goal (1 subgoal):
 1. (z = lincomb c (insert w W) &&& (\<And>w. w \<in> W \<Longrightarrow> (0::'a) \<le> c w)) &&& (0::'a) \<le> c w &&& sum c (insert w W) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = lincomb c (insert w W)
?w3 \<in> W \<Longrightarrow> (0::'a) \<le> c ?w3
(0::'a) \<le> c w
sum c (insert w W) = (1::'a)

goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
have zl: "z = c w \<cdot>\<^sub>v w + lincomb c W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = c w \<cdot>\<^sub>v w + lincomb c W
[PROOF STEP]
unfolding zl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (insert w W) = c w \<cdot>\<^sub>v w + lincomb c W
[PROOF STEP]
by (rule lincomb_insert2, insert insert S, auto)
[PROOF STATE]
proof (state)
this:
z = c w \<cdot>\<^sub>v w + lincomb c W

goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
have sum: "c w + sum c W = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c w + sum c W = (1::'a)
[PROOF STEP]
unfolding sum[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c w + sum c W = sum c (insert w W)
[PROOF STEP]
by (subst sum.insert, insert insert, auto)
[PROOF STATE]
proof (state)
this:
c w + sum c W = (1::'a)

goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
have W: "W \<subseteq> carrier_vec n" and w: "w \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W \<subseteq> carrier_vec n &&& w \<in> carrier_vec n
[PROOF STEP]
using S insert
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier_vec n
finite W
w \<notin> W
\<lbrakk>W \<subseteq> S; convex_lincomb ?c3 W ?z3\<rbrakk> \<Longrightarrow> ?z3 \<in> S
insert w W \<subseteq> S
convex_lincomb c (insert w W) z

goal (1 subgoal):
 1. W \<subseteq> carrier_vec n &&& w \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W \<subseteq> carrier_vec n
w \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x F c z. \<lbrakk>finite F; x \<notin> F; \<And>c z. \<lbrakk>F \<subseteq> S; convex_lincomb c F z\<rbrakk> \<Longrightarrow> z \<in> S; insert x F \<subseteq> S; convex_lincomb c (insert x F) z\<rbrakk> \<Longrightarrow> z \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> S
[PROOF STEP]
proof (cases "sum c W = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sum c W = (0::'a) \<Longrightarrow> z \<in> S
 2. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
sum c W = (0::'a)

goal (2 subgoals):
 1. sum c W = (0::'a) \<Longrightarrow> z \<in> S
 2. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
with nonneg
[PROOF STATE]
proof (chain)
picking this:
?w3 \<in> W \<Longrightarrow> (0::'a) \<le> c ?w3
sum c W = (0::'a)
[PROOF STEP]
have c0: "\<And> w. w \<in> W \<Longrightarrow> c w = 0"
[PROOF STATE]
proof (prove)
using this:
?w3 \<in> W \<Longrightarrow> (0::'a) \<le> c ?w3
sum c W = (0::'a)

goal (1 subgoal):
 1. \<And>w. w \<in> W \<Longrightarrow> c w = (0::'a)
[PROOF STEP]
using insert(1) sum_nonneg_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
?w3 \<in> W \<Longrightarrow> (0::'a) \<le> c ?w3
sum c W = (0::'a)
finite W
\<lbrakk>finite ?A; \<And>x. x \<in> ?A \<Longrightarrow> (0::?'a) \<le> ?f x\<rbrakk> \<Longrightarrow> (sum ?f ?A = (0::?'a)) = (\<forall>x\<in>?A. ?f x = (0::?'a))

goal (1 subgoal):
 1. \<And>w. w \<in> W \<Longrightarrow> c w = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?w3 \<in> W \<Longrightarrow> c ?w3 = (0::'a)

goal (2 subgoals):
 1. sum c W = (0::'a) \<Longrightarrow> z \<in> S
 2. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
with sum
[PROOF STATE]
proof (chain)
picking this:
c w + sum c W = (1::'a)
?w3 \<in> W \<Longrightarrow> c ?w3 = (0::'a)
[PROOF STEP]
have cw: "c w = 1"
[PROOF STATE]
proof (prove)
using this:
c w + sum c W = (1::'a)
?w3 \<in> W \<Longrightarrow> c ?w3 = (0::'a)

goal (1 subgoal):
 1. c w = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c w = (1::'a)

goal (2 subgoals):
 1. sum c W = (0::'a) \<Longrightarrow> z \<in> S
 2. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
have lin0: "lincomb c W = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c W = 0\<^sub>v n
[PROOF STEP]
by (intro lincomb_zero W, insert c0, auto)
[PROOF STATE]
proof (state)
this:
lincomb c W = 0\<^sub>v n

goal (2 subgoals):
 1. sum c W = (0::'a) \<Longrightarrow> z \<in> S
 2. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
have "z = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = w
[PROOF STEP]
unfolding zl cw lin0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<cdot>\<^sub>v w + 0\<^sub>v n = w
[PROOF STEP]
using w
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier_vec n

goal (1 subgoal):
 1. (1::'a) \<cdot>\<^sub>v w + 0\<^sub>v n = w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z = w

goal (2 subgoals):
 1. sum c W = (0::'a) \<Longrightarrow> z \<in> S
 2. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
with insert(4)
[PROOF STATE]
proof (chain)
picking this:
insert w W \<subseteq> S
z = w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insert w W \<subseteq> S
z = w

goal (1 subgoal):
 1. z \<in> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> S

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
sum c W \<noteq> (0::'a)

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
have "sum c W \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> sum c W
[PROOF STEP]
using nonneg
[PROOF STATE]
proof (prove)
using this:
?w3 \<in> W \<Longrightarrow> (0::'a) \<le> c ?w3

goal (1 subgoal):
 1. (0::'a) \<le> sum c W
[PROOF STEP]
by (metis sum_nonneg)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> sum c W

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
sum c W \<noteq> (0::'a)
(0::'a) \<le> sum c W
[PROOF STEP]
have pos: "sum c W > 0"
[PROOF STATE]
proof (prove)
using this:
sum c W \<noteq> (0::'a)
(0::'a) \<le> sum c W

goal (1 subgoal):
 1. (0::'a) < sum c W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) < sum c W

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
define b where "b = (\<lambda> w. inverse (sum c W) * c w)"
[PROOF STATE]
proof (state)
this:
b = (\<lambda>w. inverse (sum c W) * c w)

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
have "convex_lincomb b W (lincomb b W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_lincomb b W (lincomb b W)
[PROOF STEP]
unfolding convex_lincomb_def nonneg_lincomb_def b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lincomb (\<lambda>w. inverse (sum c W) * c w) W = lincomb (\<lambda>w. inverse (sum c W) * c w) W \<and> (\<lambda>w. inverse (sum c W) * c w) ` W \<subseteq> Collect ((\<le>) (0::'a))) \<and> (\<Sum>w\<in>W. inverse (sum c W) * c w) = (1::'a)
[PROOF STEP]
proof (intro conjI refl)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>w. inverse (sum c W) * c w) ` W \<subseteq> Collect ((\<le>) (0::'a))
 2. (\<Sum>w\<in>W. inverse (sum c W) * c w) = (1::'a)
[PROOF STEP]
show "(\<lambda>w. inverse (sum c W) * c w) ` W \<subseteq> Collect ((\<le>) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. inverse (sum c W) * c w) ` W \<subseteq> Collect ((\<le>) (0::'a))
[PROOF STEP]
using nonneg pos
[PROOF STATE]
proof (prove)
using this:
?w3 \<in> W \<Longrightarrow> (0::'a) \<le> c ?w3
(0::'a) < sum c W

goal (1 subgoal):
 1. (\<lambda>w. inverse (sum c W) * c w) ` W \<subseteq> Collect ((\<le>) (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. inverse (sum c W) * c w) ` W \<subseteq> Collect ((\<le>) (0::'a))

goal (1 subgoal):
 1. (\<Sum>w\<in>W. inverse (sum c W) * c w) = (1::'a)
[PROOF STEP]
show "(\<Sum>w\<in>W. inverse (sum c W) * c w) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>w\<in>W. inverse (sum c W) * c w) = (1::'a)
[PROOF STEP]
unfolding sum_distrib_left[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (sum c W) * sum c W = (1::'a)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
sum c W \<noteq> (0::'a)

goal (1 subgoal):
 1. inverse (sum c W) * sum c W = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>W. inverse (sum c W) * c w) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
convex_lincomb b W (lincomb b W)

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
from insert(3)[OF _ this] insert
[PROOF STATE]
proof (chain)
picking this:
W \<subseteq> S \<Longrightarrow> lincomb b W \<in> S
finite W
w \<notin> W
\<lbrakk>W \<subseteq> S; convex_lincomb ?c3 W ?z3\<rbrakk> \<Longrightarrow> ?z3 \<in> S
insert w W \<subseteq> S
convex_lincomb c (insert w W) z
[PROOF STEP]
have IH: "lincomb b W \<in> S"
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> S \<Longrightarrow> lincomb b W \<in> S
finite W
w \<notin> W
\<lbrakk>W \<subseteq> S; convex_lincomb ?c3 W ?z3\<rbrakk> \<Longrightarrow> ?z3 \<in> S
insert w W \<subseteq> S
convex_lincomb c (insert w W) z

goal (1 subgoal):
 1. lincomb b W \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb b W \<in> S

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
have lin: "lincomb c W = sum c W \<cdot>\<^sub>v lincomb b W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c W = sum c W \<cdot>\<^sub>v lincomb b W
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c W = sum c W \<cdot>\<^sub>v lincomb (\<lambda>w. inverse (sum c W) * c w) W
[PROOF STEP]
by (subst lincomb_smult[symmetric, OF W], rule lincomb_cong[OF _ W], insert False, auto)
[PROOF STATE]
proof (state)
this:
lincomb c W = sum c W \<cdot>\<^sub>v lincomb b W

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
from sum cw pos
[PROOF STATE]
proof (chain)
picking this:
c w + sum c W = (1::'a)
(0::'a) \<le> c w
(0::'a) < sum c W
[PROOF STEP]
have sum: "sum c W = 1 - c w" and cw1: "c w \<le> 1"
[PROOF STATE]
proof (prove)
using this:
c w + sum c W = (1::'a)
(0::'a) \<le> c w
(0::'a) < sum c W

goal (1 subgoal):
 1. sum c W = (1::'a) - c w &&& c w \<le> (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum c W = (1::'a) - c w
c w \<le> (1::'a)

goal (1 subgoal):
 1. sum c W \<noteq> (0::'a) \<Longrightarrow> z \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> S
[PROOF STEP]
unfolding zl lin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c w \<cdot>\<^sub>v w + sum c W \<cdot>\<^sub>v lincomb b W \<in> S
[PROOF STEP]
unfolding sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c w \<cdot>\<^sub>v w + ((1::'a) - c w) \<cdot>\<^sub>v lincomb b W \<in> S
[PROOF STEP]
by (rule step[OF _ IH cw cw1], insert insert, auto)
[PROOF STATE]
proof (state)
this:
z \<in> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> S

goal (1 subgoal):
 1. S \<subseteq> convex_hull S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<subseteq> convex_hull S
[PROOF STEP]
show "S \<subseteq> convex_hull S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> convex_hull S
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier_vec n

goal (1 subgoal):
 1. S \<subseteq> convex_hull S
[PROOF STEP]
by (rule set_in_convex_hull)
[PROOF STATE]
proof (state)
this:
S \<subseteq> convex_hull S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_hulls_are_convex: assumes "A \<subseteq> carrier_vec n"
  shows "convex (convex_hull A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex (convex_hull A)
[PROOF STEP]
by (intro convexI convex_hull_convex_sum convex_hull_carrier assms)