[STATEMENT]
lemma convex_hull_list_combination:
  assumes Vs: "set Vs \<subseteq> carrier_vec n"
    and x: "x \<in> convex_hull_list Vs"
    and y: "y \<in> convex_hull_list Vs"
    and l0: "0 \<le> l" and l1: "l \<le> 1"
  shows "l \<cdot>\<^sub>v x + (1 - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> convex_hull_list Vs
[PROOF STEP]
obtain cx where x: "lincomb_list cx Vs = x" and cx0: "\<forall> i < length Vs. cx i \<ge> 0"
    and cx1: "sum cx {0..<length Vs} = 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull_list Vs

goal (1 subgoal):
 1. (\<And>cx. \<lbrakk>lincomb_list cx Vs = x; \<forall>i<length Vs. (0::'a) \<le> cx i; sum cx {0..<length Vs} = (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:
x \<in> {x. \<exists>c. (lincomb_list c Vs = x \<and> (\<forall>i<length Vs. (0::'a) \<le> c i)) \<and> sum c {0..<length Vs} = (1::'a)}

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

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> convex_hull_list Vs
[PROOF STEP]
obtain cy where y: "lincomb_list cy Vs = y" and cy0: "\<forall> i < length Vs. cy i \<ge> 0"
    and cy1: "sum cy {0..<length Vs} = 1"
[PROOF STATE]
proof (prove)
using this:
y \<in> convex_hull_list Vs

goal (1 subgoal):
 1. (\<And>cy. \<lbrakk>lincomb_list cy Vs = y; \<forall>i<length Vs. (0::'a) \<le> cy i; sum cy {0..<length Vs} = (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:
y \<in> {x. \<exists>c. (lincomb_list c Vs = x \<and> (\<forall>i<length Vs. (0::'a) \<le> c i)) \<and> sum c {0..<length Vs} = (1::'a)}

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

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
let ?c = "\<lambda> i. l * cx i + (1 - l) * cy i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
have "set Vs \<subseteq> carrier_vec n \<Longrightarrow>
        lincomb_list ?c Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + (1 - l) \<cdot>\<^sub>v lincomb_list cy Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs
[PROOF STEP]
proof (induction Vs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
case (snoc v Vs)
[PROOF STATE]
proof (state)
this:
set Vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs
set (Vs @ [v]) \<subseteq> carrier_vec n

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
have v: "v \<in> carrier_vec n" and Vs: "set Vs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> carrier_vec n &&& set Vs \<subseteq> carrier_vec n
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
set (Vs @ [v]) \<subseteq> carrier_vec n

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

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
have "lincomb_list ?c (Vs @ [v]) = lincomb_list ?c Vs + ?c (length Vs) \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs + (l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
set (Vs @ [v]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs + (l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs + (l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs + (l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
have "lincomb_list ?c Vs =
               l \<cdot>\<^sub>v lincomb_list cx Vs + (1 - l) \<cdot>\<^sub>v lincomb_list cy Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs
[PROOF STEP]
by (rule snoc.IH[OF Vs])
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
have "?c (length Vs) \<cdot>\<^sub>v v =
               l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + (1 - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v = l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)
[PROOF STEP]
using add_smult_distrib_vec smult_smult_assoc
[PROOF STATE]
proof (prove)
using this:
(?a + ?b) \<cdot>\<^sub>v ?v = ?a \<cdot>\<^sub>v ?v + ?b \<cdot>\<^sub>v ?v
?a \<cdot>\<^sub>v (?b \<cdot>\<^sub>v ?v) = ?a * ?b \<cdot>\<^sub>v ?v

goal (1 subgoal):
 1. (l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v = l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v = l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(l * cx (length Vs) + ((1::'a) - l) * cy (length Vs)) \<cdot>\<^sub>v v = l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
have "l \<cdot>\<^sub>v lincomb_list cx Vs + (1 - l) \<cdot>\<^sub>v lincomb_list cy Vs + \<dots> =
                  l \<cdot>\<^sub>v (lincomb_list cx Vs + cx (length Vs) \<cdot>\<^sub>v v) +
                  (1 - l) \<cdot>\<^sub>v (lincomb_list cy Vs + cy (length Vs) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs + (l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)) = l \<cdot>\<^sub>v (lincomb_list cx Vs + cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (lincomb_list cy Vs + cy (length Vs) \<cdot>\<^sub>v v)
[PROOF STEP]
using lincomb_list_carrier[OF Vs] v
[PROOF STATE]
proof (prove)
using this:
lincomb_list ?c Vs \<in> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs + (l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)) = l \<cdot>\<^sub>v (lincomb_list cx Vs + cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (lincomb_list cy Vs + cy (length Vs) \<cdot>\<^sub>v v)
[PROOF STEP]
by (simp add: M.add.m_assoc M.add.m_lcomm smult_r_distr)
[PROOF STATE]
proof (state)
this:
l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs + (l \<cdot>\<^sub>v (cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (cy (length Vs) \<cdot>\<^sub>v v)) = l \<cdot>\<^sub>v (lincomb_list cx Vs + cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (lincomb_list cy Vs + cy (length Vs) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) xs = l \<cdot>\<^sub>v lincomb_list cx xs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (xs @ [x]) = l \<cdot>\<^sub>v lincomb_list cx (xs @ [x]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (xs @ [x])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = l \<cdot>\<^sub>v (lincomb_list cx Vs + cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (lincomb_list cy Vs + cy (length Vs) \<cdot>\<^sub>v v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = l \<cdot>\<^sub>v (lincomb_list cx Vs + cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (lincomb_list cy Vs + cy (length Vs) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = l \<cdot>\<^sub>v lincomb_list cx (Vs @ [v]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (Vs @ [v])
[PROOF STEP]
using Vs v
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = l \<cdot>\<^sub>v (lincomb_list cx Vs + cx (length Vs) \<cdot>\<^sub>v v) + ((1::'a) - l) \<cdot>\<^sub>v (lincomb_list cy Vs + cy (length Vs) \<cdot>\<^sub>v v)
set Vs \<subseteq> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = l \<cdot>\<^sub>v lincomb_list cx (Vs @ [v]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (Vs @ [v])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) (Vs @ [v]) = l \<cdot>\<^sub>v lincomb_list cx (Vs @ [v]) + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy (Vs @ [v])

goal (1 subgoal):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) [] = l \<cdot>\<^sub>v lincomb_list cx [] + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
set Vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
hence "lincomb_list ?c Vs = l \<cdot>\<^sub>v x + (1 - l) \<cdot>\<^sub>v y"
[PROOF STATE]
proof (prove)
using this:
set Vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y
[PROOF STEP]
using Vs x y
[PROOF STATE]
proof (prove)
using this:
set Vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v lincomb_list cx Vs + ((1::'a) - l) \<cdot>\<^sub>v lincomb_list cy Vs
set Vs \<subseteq> carrier_vec n
lincomb_list cx Vs = x
lincomb_list cy Vs = y

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
have "\<forall> i < length Vs. ?c i \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length Vs. (0::'a) \<le> l * cx i + ((1::'a) - l) * cy i
[PROOF STEP]
using cx0 cy0 l0 l1
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length Vs. (0::'a) \<le> cx i
\<forall>i<length Vs. (0::'a) \<le> cy i
(0::'a) \<le> l
l \<le> (1::'a)

goal (1 subgoal):
 1. \<forall>i<length Vs. (0::'a) \<le> l * cx i + ((1::'a) - l) * cy i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<length Vs. (0::'a) \<le> l * cx i + ((1::'a) - l) * cy i

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i<length Vs. (0::'a) \<le> l * cx i + ((1::'a) - l) * cy i

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
have "sum ?c {0..<length Vs} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i + ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
proof(simp add: sum.distrib)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
have "(\<Sum>i = 0..<length Vs. (1 - l) * cy i) = (1 - l) * sum cy {0..<length Vs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = ((1::'a) - l) * sum cy {0..<length Vs}
[PROOF STEP]
using sum_distrib_left
[PROOF STATE]
proof (prove)
using this:
?r * sum ?f ?A = (\<Sum>n\<in>?A. ?r * ?f n)

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = ((1::'a) - l) * sum cy {0..<length Vs}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = ((1::'a) - l) * sum cy {0..<length Vs}

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = ((1::'a) - l) * sum cy {0..<length Vs}

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
have "(\<Sum>i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}
[PROOF STEP]
using sum_distrib_left
[PROOF STATE]
proof (prove)
using this:
?r * sum ?f ?A = (\<Sum>n\<in>?A. ?r * ?f n)

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = ((1::'a) - l) * sum cy {0..<length Vs}
(\<Sum>i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}
[PROOF STEP]
show "(\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. (1 - l) * cy i) = 1"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = ((1::'a) - l) * sum cy {0..<length Vs}
(\<Sum>i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
using cx1 cy1
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = ((1::'a) - l) * sum cy {0..<length Vs}
(\<Sum>i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}
sum cx {0..<length Vs} = (1::'a)
sum cy {0..<length Vs} = (1::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. l * cx i) + (\<Sum>i = 0..<length Vs. ((1::'a) - l) * cy i) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. l * cx i + ((1::'a) - l) * cy i) = (1::'a)

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y
\<forall>i<length Vs. (0::'a) \<le> l * cx i + ((1::'a) - l) * cy i
(\<Sum>i = 0..<length Vs. l * cx i + ((1::'a) - l) * cy i) = (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y
\<forall>i<length Vs. (0::'a) \<le> l * cx i + ((1::'a) - l) * cy i
(\<Sum>i = 0..<length Vs. l * cx i + ((1::'a) - l) * cy i) = (1::'a)

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs
[PROOF STEP]
unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>i. l * cx i + ((1::'a) - l) * cy i) Vs = l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y
\<forall>i<length Vs. (0::'a) \<le> l * cx i + ((1::'a) - l) * cy i
(\<Sum>i = 0..<length Vs. l * cx i + ((1::'a) - l) * cy i) = (1::'a)

goal (1 subgoal):
 1. l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> {x. \<exists>c. (lincomb_list c Vs = x \<and> (\<forall>i<length Vs. (0::'a) \<le> c i)) \<and> sum c {0..<length Vs} = (1::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<cdot>\<^sub>v x + ((1::'a) - l) \<cdot>\<^sub>v y \<in> convex_hull_list Vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_hull_list_mono:
  assumes "set Ws \<subseteq> carrier_vec n"
  shows "set Vs \<subseteq> set Ws \<Longrightarrow> convex_hull_list Vs \<subseteq> convex_hull_list Ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Vs \<subseteq> set Ws \<Longrightarrow> convex_hull_list Vs \<subseteq> convex_hull_list Ws
[PROOF STEP]
proof (standard, induction Vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>set [] \<subseteq> set Ws; x \<in> convex_hull_list []\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> set Ws
x \<in> convex_hull_list []

goal (2 subgoals):
 1. \<And>x. \<lbrakk>set [] \<subseteq> set Ws; x \<in> convex_hull_list []\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
from Nil(2)
[PROOF STATE]
proof (chain)
picking this:
x \<in> convex_hull_list []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull_list []

goal (1 subgoal):
 1. x \<in> convex_hull_list Ws
[PROOF STEP]
unfolding convex_hull_list_def convex_lincomb_list_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. \<exists>c. nonneg_lincomb_list c [] x \<and> sum c {0..<length []} = (1::'a)}

goal (1 subgoal):
 1. x \<in> {x. \<exists>c. nonneg_lincomb_list c Ws x \<and> sum c {0..<length Ws} = (1::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull_list Ws

goal (1 subgoal):
 1. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
case (Cons v Vs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set Vs \<subseteq> set Ws; ?x3 \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> ?x3 \<in> convex_hull_list Ws
set (v # Vs) \<subseteq> set Ws
x \<in> convex_hull_list (v # Vs)

goal (1 subgoal):
 1. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have v: "v \<in> set Ws" and Vs: "set Vs \<subseteq> set Ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> set Ws &&& set Vs \<subseteq> set Ws
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
set (v # Vs) \<subseteq> set Ws

goal (1 subgoal):
 1. v \<in> set Ws &&& set Vs \<subseteq> set Ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> set Ws
set Vs \<subseteq> set Ws

goal (1 subgoal):
 1. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence v1: "v \<in> convex_hull_list Ws"
[PROOF STATE]
proof (prove)
using this:
v \<in> set Ws
set Vs \<subseteq> set Ws

goal (1 subgoal):
 1. v \<in> convex_hull_list Ws
[PROOF STEP]
using set_in_convex_hull_list[OF assms]
[PROOF STATE]
proof (prove)
using this:
v \<in> set Ws
set Vs \<subseteq> set Ws
set Ws \<subseteq> convex_hull_list Ws

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

goal (1 subgoal):
 1. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
from Cons.prems(2)
[PROOF STATE]
proof (chain)
picking this:
x \<in> convex_hull_list (v # Vs)
[PROOF STEP]
obtain c
    where x: "lincomb_list c (v # Vs) = x" and c0: "\<forall> i < length Vs + 1. c i \<ge> 0"
      and c1: "sum c {0..<length Vs + 1} = 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull_list (v # Vs)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>lincomb_list c (v # Vs) = x; \<forall>i<length Vs + 1. (0::'a) \<le> c i; sum c {0..<length Vs + 1} = (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:
x \<in> {x. \<exists>c. (lincomb_list c (v # Vs) = x \<and> (\<forall>i<length (v # Vs). (0::'a) \<le> c i)) \<and> sum c {0..<length (v # Vs)} = (1::'a)}

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

goal (1 subgoal):
 1. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have x: "x = c 0 \<cdot>\<^sub>v v + lincomb_list (c \<circ> Suc) Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = c 0 \<cdot>\<^sub>v v + lincomb_list (c \<circ> Suc) Vs
[PROOF STEP]
using Vs v assms x
[PROOF STATE]
proof (prove)
using this:
set Vs \<subseteq> set Ws
v \<in> set Ws
set Ws \<subseteq> carrier_vec n
lincomb_list c (v # Vs) = x

goal (1 subgoal):
 1. x = c 0 \<cdot>\<^sub>v v + lincomb_list (c \<circ> Suc) Vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = c 0 \<cdot>\<^sub>v v + lincomb_list (c \<circ> Suc) Vs

goal (1 subgoal):
 1. \<And>a Vs x. \<lbrakk>\<And>x. \<lbrakk>set Vs \<subseteq> set Ws; x \<in> convex_hull_list Vs\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws; set (a # Vs) \<subseteq> set Ws; x \<in> convex_hull_list (a # Vs)\<rbrakk> \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> convex_hull_list Ws
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
assume P: "c 0 = 1"
[PROOF STATE]
proof (state)
this:
c 0 = (1::'a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "sum (c \<circ> Suc) {0..<length Vs} = 0"
[PROOF STATE]
proof (prove)
using this:
c 0 = (1::'a)

goal (1 subgoal):
 1. sum (c \<circ> Suc) {0..<length Vs} = (0::'a)
[PROOF STEP]
using sum.atLeast0_lessThan_Suc_shift c1
[PROOF STATE]
proof (prove)
using this:
c 0 = (1::'a)
sum ?g {0..<Suc ?n} = ?g 0 + sum (?g \<circ> Suc) {0..<?n}
sum c {0..<length Vs + 1} = (1::'a)

goal (1 subgoal):
 1. sum (c \<circ> Suc) {0..<length Vs} = (0::'a)
[PROOF STEP]
by (metis One_nat_def R.show_r_zero add.right_neutral add_Suc_right)
[PROOF STATE]
proof (state)
this:
sum (c \<circ> Suc) {0..<length Vs} = (0::'a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum (c \<circ> Suc) {0..<length Vs} = (0::'a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have "\<And> i. i \<in> {0..<length Vs} \<Longrightarrow> (c \<circ> Suc) i \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<length Vs} \<Longrightarrow> (0::'a) \<le> (c \<circ> Suc) i
[PROOF STEP]
using c0
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length Vs + 1. (0::'a) \<le> c i

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<length Vs} \<Longrightarrow> (0::'a) \<le> (c \<circ> Suc) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?i3 \<in> {0..<length Vs} \<Longrightarrow> (0::'a) \<le> (c \<circ> Suc) ?i3

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum (c \<circ> Suc) {0..<length Vs} = (0::'a)
?i3 \<in> {0..<length Vs} \<Longrightarrow> (0::'a) \<le> (c \<circ> Suc) ?i3
[PROOF STEP]
have "\<forall> i \<in> {0..<length Vs}. (c \<circ> Suc) i = 0"
[PROOF STATE]
proof (prove)
using this:
sum (c \<circ> Suc) {0..<length Vs} = (0::'a)
?i3 \<in> {0..<length Vs} \<Longrightarrow> (0::'a) \<le> (c \<circ> Suc) ?i3

goal (1 subgoal):
 1. \<forall>i\<in>{0..<length Vs}. (c \<circ> Suc) i = (0::'a)
[PROOF STEP]
using sum_nonneg_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
sum (c \<circ> Suc) {0..<length Vs} = (0::'a)
?i3 \<in> {0..<length Vs} \<Longrightarrow> (0::'a) \<le> (c \<circ> Suc) ?i3
\<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. \<forall>i\<in>{0..<length Vs}. (c \<circ> Suc) i = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..<length Vs}. (c \<circ> Suc) i = (0::'a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "\<And> i. i < length Vs \<Longrightarrow> (c \<circ> Suc) i \<cdot>\<^sub>v Vs ! i = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<length Vs}. (c \<circ> Suc) i = (0::'a)

goal (1 subgoal):
 1. \<And>i. i < length Vs \<Longrightarrow> (c \<circ> Suc) i \<cdot>\<^sub>v Vs ! i = 0\<^sub>v n
[PROOF STEP]
using Vs assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<length Vs}. (c \<circ> Suc) i = (0::'a)
set Vs \<subseteq> set Ws
set Ws \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>i. i < length Vs \<Longrightarrow> (c \<circ> Suc) i \<cdot>\<^sub>v Vs ! i = 0\<^sub>v n
[PROOF STEP]
by (simp add: subset_code(1))
[PROOF STATE]
proof (state)
this:
?i3 < length Vs \<Longrightarrow> (c \<circ> Suc) ?i3 \<cdot>\<^sub>v Vs ! ?i3 = 0\<^sub>v n

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "lincomb_list (c \<circ> Suc) Vs = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
?i3 < length Vs \<Longrightarrow> (c \<circ> Suc) ?i3 \<cdot>\<^sub>v Vs ! ?i3 = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb_list (c \<circ> Suc) Vs = 0\<^sub>v n
[PROOF STEP]
using lincomb_list_eq_0
[PROOF STATE]
proof (prove)
using this:
?i3 < length Vs \<Longrightarrow> (c \<circ> Suc) ?i3 \<cdot>\<^sub>v Vs ! ?i3 = 0\<^sub>v n
(\<And>i. i < length ?vs \<Longrightarrow> ?c i \<cdot>\<^sub>v ?vs ! i = 0\<^sub>v n) \<Longrightarrow> lincomb_list ?c ?vs = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb_list (c \<circ> Suc) Vs = 0\<^sub>v n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb_list (c \<circ> Suc) Vs = 0\<^sub>v n

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "x = v"
[PROOF STATE]
proof (prove)
using this:
lincomb_list (c \<circ> Suc) Vs = 0\<^sub>v n

goal (1 subgoal):
 1. x = v
[PROOF STEP]
using P x v assms
[PROOF STATE]
proof (prove)
using this:
lincomb_list (c \<circ> Suc) Vs = 0\<^sub>v n
c 0 = (1::'a)
x = c 0 \<cdot>\<^sub>v v + lincomb_list (c \<circ> Suc) Vs
v \<in> set Ws
set Ws \<subseteq> carrier_vec n

goal (1 subgoal):
 1. x = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> convex_hull_list Ws
 2. \<not> ?P \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x = v

goal (1 subgoal):
 1. x \<in> convex_hull_list Ws
[PROOF STEP]
using v1
[PROOF STATE]
proof (prove)
using this:
x = v
v \<in> convex_hull_list Ws

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

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
assume P: "c 0 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
c 0 \<noteq> (1::'a)

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have c1: "c 0 + sum (c \<circ> Suc) {0..<length Vs} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c 0 + sum (c \<circ> Suc) {0..<length Vs} = (1::'a)
[PROOF STEP]
using sum.atLeast0_lessThan_Suc_shift[of c] c1
[PROOF STATE]
proof (prove)
using this:
sum c {0..<Suc ?n} = c 0 + sum (c \<circ> Suc) {0..<?n}
sum c {0..<length Vs + 1} = (1::'a)

goal (1 subgoal):
 1. c 0 + sum (c \<circ> Suc) {0..<length Vs} = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c 0 + sum (c \<circ> Suc) {0..<length Vs} = (1::'a)

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have "sum (c \<circ> Suc) {0..<length Vs} \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> sum (c \<circ> Suc) {0..<length Vs}
[PROOF STEP]
by (rule sum_nonneg, insert c0, simp)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> sum (c \<circ> Suc) {0..<length Vs}

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "c 0 < 1"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> sum (c \<circ> Suc) {0..<length Vs}

goal (1 subgoal):
 1. c 0 < (1::'a)
[PROOF STEP]
using P c1
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> sum (c \<circ> Suc) {0..<length Vs}
c 0 \<noteq> (1::'a)
c 0 + sum (c \<circ> Suc) {0..<length Vs} = (1::'a)

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

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
let ?c' = "\<lambda> i. 1 / (1 - c 0) * (c \<circ> Suc) i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have "sum ?c' {0..<length Vs} = 1 / (1 - c 0) * sum (c \<circ> Suc) {0..<length Vs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a) / ((1::'a) - c 0) * sum (c \<circ> Suc) {0..<length Vs}
[PROOF STEP]
using c1 P sum_distrib_left
[PROOF STATE]
proof (prove)
using this:
c 0 + sum (c \<circ> Suc) {0..<length Vs} = (1::'a)
c 0 \<noteq> (1::'a)
?r * sum ?f ?A = (\<Sum>n\<in>?A. ?r * ?f n)

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a) / ((1::'a) - c 0) * sum (c \<circ> Suc) {0..<length Vs}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a) / ((1::'a) - c 0) * sum (c \<circ> Suc) {0..<length Vs}

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "sum ?c' {0..<length Vs} = 1"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a) / ((1::'a) - c 0) * sum (c \<circ> Suc) {0..<length Vs}

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a)
[PROOF STEP]
using P c1
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a) / ((1::'a) - c 0) * sum (c \<circ> Suc) {0..<length Vs}
c 0 \<noteq> (1::'a)
c 0 + sum (c \<circ> Suc) {0..<length Vs} = (1::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a)

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a)

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have "\<forall> i < length Vs. ?c' i \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length Vs. (0::'a) \<le> (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i
[PROOF STEP]
using c0 \<open>c 0 < 1\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length Vs + 1. (0::'a) \<le> c i
c 0 < (1::'a)

goal (1 subgoal):
 1. \<forall>i<length Vs. (0::'a) \<le> (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<length Vs. (0::'a) \<le> (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a)
\<forall>i<length Vs. (0::'a) \<le> (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i
[PROOF STEP]
have c': "lincomb_list ?c' Vs \<in> convex_hull_list Ws"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a)
\<forall>i<length Vs. (0::'a) \<le> (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs \<in> convex_hull_list Ws
[PROOF STEP]
using Cons.IH[OF Vs]
        convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<length Vs. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) = (1::'a)
\<forall>i<length Vs. (0::'a) \<le> (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i
?x3 \<in> convex_hull_list Vs \<Longrightarrow> ?x3 \<in> convex_hull_list Ws
convex_hull_list ?Vs = {x. \<exists>c. convex_lincomb_list c ?Vs x}
convex_lincomb_list ?c ?Vs ?b = (nonneg_lincomb_list ?c ?Vs ?b \<and> sum ?c {0..<length ?Vs} = (1::'a))
nonneg_lincomb_list ?c ?Vs ?b = (lincomb_list ?c ?Vs = ?b \<and> (\<forall>i<length ?Vs. (0::'a) \<le> ?c i))

goal (1 subgoal):
 1. lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs \<in> convex_hull_list Ws
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs \<in> convex_hull_list Ws

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
have "lincomb_list ?c' Vs = 1 / (1 - c 0) \<cdot>\<^sub>v lincomb_list (c \<circ> Suc) Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = (1::'a) / ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (c \<circ> Suc) Vs
[PROOF STEP]
by(rule lincomb_list_smult, insert Vs assms, auto)
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = (1::'a) / ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (c \<circ> Suc) Vs

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "(1 - c 0) \<cdot>\<^sub>v lincomb_list ?c' Vs = lincomb_list (c \<circ> Suc) Vs"
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = (1::'a) / ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (c \<circ> Suc) Vs

goal (1 subgoal):
 1. ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = lincomb_list (c \<circ> Suc) Vs
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = (1::'a) / ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (c \<circ> Suc) Vs
c 0 \<noteq> (1::'a)

goal (1 subgoal):
 1. ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = lincomb_list (c \<circ> Suc) Vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = lincomb_list (c \<circ> Suc) Vs

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
hence "x = c 0 \<cdot>\<^sub>v v + (1 - c 0) \<cdot>\<^sub>v lincomb_list ?c' Vs"
[PROOF STATE]
proof (prove)
using this:
((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = lincomb_list (c \<circ> Suc) Vs

goal (1 subgoal):
 1. x = c 0 \<cdot>\<^sub>v v + ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs = lincomb_list (c \<circ> Suc) Vs
x = c 0 \<cdot>\<^sub>v v + lincomb_list (c \<circ> Suc) Vs

goal (1 subgoal):
 1. x = c 0 \<cdot>\<^sub>v v + ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = c 0 \<cdot>\<^sub>v v + ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs

goal (1 subgoal):
 1. c 0 \<noteq> (1::'a) \<Longrightarrow> x \<in> convex_hull_list Ws
[PROOF STEP]
thus "x \<in> convex_hull_list Ws"
[PROOF STATE]
proof (prove)
using this:
x = c 0 \<cdot>\<^sub>v v + ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs

goal (1 subgoal):
 1. x \<in> convex_hull_list Ws
[PROOF STEP]
using convex_hull_list_combination[OF assms v1 c'] c0 \<open>c 0 < 1\<close>
[PROOF STATE]
proof (prove)
using this:
x = c 0 \<cdot>\<^sub>v v + ((1::'a) - c 0) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs
\<lbrakk>(0::'a) \<le> ?l; ?l \<le> (1::'a)\<rbrakk> \<Longrightarrow> ?l \<cdot>\<^sub>v v + ((1::'a) - ?l) \<cdot>\<^sub>v lincomb_list (\<lambda>i. (1::'a) / ((1::'a) - c 0) * (c \<circ> Suc) i) Vs \<in> convex_hull_list Ws
\<forall>i<length Vs + 1. (0::'a) \<le> c i
c 0 < (1::'a)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_hull_list_eq_set:
  "set Vs \<subseteq> carrier_vec n \<Longrightarrow> set Vs = set Ws \<Longrightarrow> convex_hull_list Vs = convex_hull_list Ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set Vs \<subseteq> carrier_vec n; set Vs = set Ws\<rbrakk> \<Longrightarrow> convex_hull_list Vs = convex_hull_list Ws
[PROOF STEP]
using convex_hull_list_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?Ws \<subseteq> carrier_vec n; set ?Vs \<subseteq> set ?Ws\<rbrakk> \<Longrightarrow> convex_hull_list ?Vs \<subseteq> convex_hull_list ?Ws

goal (1 subgoal):
 1. \<lbrakk>set Vs \<subseteq> carrier_vec n; set Vs = set Ws\<rbrakk> \<Longrightarrow> convex_hull_list Vs = convex_hull_list Ws
[PROOF STEP]
by blast


[STATEMENT]
lemma find_indices_empty: "(find_indices x Vs = []) = (x \<notin> set Vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (find_indices x Vs = []) = (x \<notin> set Vs)
[PROOF STEP]
proof (induction Vs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (find_indices x [] = []) = (x \<notin> set [])
 2. \<And>xa xs. (find_indices x xs = []) = (x \<notin> set xs) \<Longrightarrow> (find_indices x (xs @ [xa]) = []) = (x \<notin> set (xs @ [xa]))
[PROOF STEP]
case (snoc v Vs)
[PROOF STATE]
proof (state)
this:
(find_indices x Vs = []) = (x \<notin> set Vs)

goal (2 subgoals):
 1. (find_indices x [] = []) = (x \<notin> set [])
 2. \<And>xa xs. (find_indices x xs = []) = (x \<notin> set xs) \<Longrightarrow> (find_indices x (xs @ [xa]) = []) = (x \<notin> set (xs @ [xa]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (find_indices x (Vs @ [v]) = []) = (x \<notin> set (Vs @ [v]))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_indices x (Vs @ [v]) = [] \<Longrightarrow> x \<notin> set (Vs @ [v])
 2. x \<notin> set (Vs @ [v]) \<Longrightarrow> find_indices x (Vs @ [v]) = []
[PROOF STEP]
assume "find_indices x (Vs @ [v]) = []"
[PROOF STATE]
proof (state)
this:
find_indices x (Vs @ [v]) = []

goal (2 subgoals):
 1. find_indices x (Vs @ [v]) = [] \<Longrightarrow> x \<notin> set (Vs @ [v])
 2. x \<notin> set (Vs @ [v]) \<Longrightarrow> find_indices x (Vs @ [v]) = []
[PROOF STEP]
hence "x \<noteq> v \<and> find_indices x Vs = []"
[PROOF STATE]
proof (prove)
using this:
find_indices x (Vs @ [v]) = []

goal (1 subgoal):
 1. x \<noteq> v \<and> find_indices x Vs = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> v \<and> find_indices x Vs = []

goal (2 subgoals):
 1. find_indices x (Vs @ [v]) = [] \<Longrightarrow> x \<notin> set (Vs @ [v])
 2. x \<notin> set (Vs @ [v]) \<Longrightarrow> find_indices x (Vs @ [v]) = []
[PROOF STEP]
thus "x \<notin> set (Vs @ [v])"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> v \<and> find_indices x Vs = []

goal (1 subgoal):
 1. x \<notin> set (Vs @ [v])
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
x \<noteq> v \<and> find_indices x Vs = []
(find_indices x Vs = []) = (x \<notin> set Vs)

goal (1 subgoal):
 1. x \<notin> set (Vs @ [v])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> set (Vs @ [v])

goal (1 subgoal):
 1. x \<notin> set (Vs @ [v]) \<Longrightarrow> find_indices x (Vs @ [v]) = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> set (Vs @ [v]) \<Longrightarrow> find_indices x (Vs @ [v]) = []
[PROOF STEP]
assume "x \<notin> set (Vs @ [v])"
[PROOF STATE]
proof (state)
this:
x \<notin> set (Vs @ [v])

goal (1 subgoal):
 1. x \<notin> set (Vs @ [v]) \<Longrightarrow> find_indices x (Vs @ [v]) = []
[PROOF STEP]
hence "x \<noteq> v \<and> find_indices x Vs = []"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (Vs @ [v])

goal (1 subgoal):
 1. x \<noteq> v \<and> find_indices x Vs = []
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (Vs @ [v])
(find_indices x Vs = []) = (x \<notin> set Vs)

goal (1 subgoal):
 1. x \<noteq> v \<and> find_indices x Vs = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> v \<and> find_indices x Vs = []

goal (1 subgoal):
 1. x \<notin> set (Vs @ [v]) \<Longrightarrow> find_indices x (Vs @ [v]) = []
[PROOF STEP]
thus "find_indices x (Vs @ [v]) = []"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> v \<and> find_indices x Vs = []

goal (1 subgoal):
 1. find_indices x (Vs @ [v]) = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_indices x (Vs @ [v]) = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(find_indices x (Vs @ [v]) = []) = (x \<notin> set (Vs @ [v]))

goal (1 subgoal):
 1. (find_indices x [] = []) = (x \<notin> set [])
[PROOF STEP]
qed simp


[STATEMENT]
lemma distinct_list_find_indices:
  shows "\<lbrakk> i < length Vs; Vs ! i = x; distinct Vs \<rbrakk> \<Longrightarrow> find_indices x Vs = [i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length Vs; Vs ! i = x; distinct Vs\<rbrakk> \<Longrightarrow> find_indices x Vs = [i]
[PROOF STEP]
proof (induction Vs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i < length []; [] ! i = x; distinct []\<rbrakk> \<Longrightarrow> find_indices x [] = [i]
 2. \<And>xa xs. \<lbrakk>\<lbrakk>i < length xs; xs ! i = x; distinct xs\<rbrakk> \<Longrightarrow> find_indices x xs = [i]; i < length (xs @ [xa]); (xs @ [xa]) ! i = x; distinct (xs @ [xa])\<rbrakk> \<Longrightarrow> find_indices x (xs @ [xa]) = [i]
[PROOF STEP]
case (snoc v Vs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < length Vs; Vs ! i = x; distinct Vs\<rbrakk> \<Longrightarrow> find_indices x Vs = [i]
i < length (Vs @ [v])
(Vs @ [v]) ! i = x
distinct (Vs @ [v])

goal (2 subgoals):
 1. \<lbrakk>i < length []; [] ! i = x; distinct []\<rbrakk> \<Longrightarrow> find_indices x [] = [i]
 2. \<And>xa xs. \<lbrakk>\<lbrakk>i < length xs; xs ! i = x; distinct xs\<rbrakk> \<Longrightarrow> find_indices x xs = [i]; i < length (xs @ [xa]); (xs @ [xa]) ! i = x; distinct (xs @ [xa])\<rbrakk> \<Longrightarrow> find_indices x (xs @ [xa]) = [i]
[PROOF STEP]
have dist: "distinct Vs" and xVs: "v \<notin> set Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct Vs &&& v \<notin> set Vs
[PROOF STEP]
using snoc.prems(3)
[PROOF STATE]
proof (prove)
using this:
distinct (Vs @ [v])

goal (1 subgoal):
 1. distinct Vs &&& v \<notin> set Vs
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
distinct Vs
v \<notin> set Vs

goal (2 subgoals):
 1. \<lbrakk>i < length []; [] ! i = x; distinct []\<rbrakk> \<Longrightarrow> find_indices x [] = [i]
 2. \<And>xa xs. \<lbrakk>\<lbrakk>i < length xs; xs ! i = x; distinct xs\<rbrakk> \<Longrightarrow> find_indices x xs = [i]; i < length (xs @ [xa]); (xs @ [xa]) ! i = x; distinct (xs @ [xa])\<rbrakk> \<Longrightarrow> find_indices x (xs @ [xa]) = [i]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
 2. \<not> ?P \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
assume i: "i = length Vs"
[PROOF STATE]
proof (state)
this:
i = length Vs

goal (2 subgoals):
 1. ?P \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
 2. \<not> ?P \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
hence "x = v"
[PROOF STATE]
proof (prove)
using this:
i = length Vs

goal (1 subgoal):
 1. x = v
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
i = length Vs
(Vs @ [v]) ! i = x

goal (1 subgoal):
 1. x = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
 2. \<not> ?P \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x = v

goal (1 subgoal):
 1. find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
using xVs find_indices_empty i
[PROOF STATE]
proof (prove)
using this:
x = v
v \<notin> set Vs
(find_indices ?x ?Vs = []) = (?x \<notin> set ?Vs)
i = length Vs

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

goal (1 subgoal):
 1. i \<noteq> length Vs \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> length Vs \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
assume "i \<noteq> length Vs"
[PROOF STATE]
proof (state)
this:
i \<noteq> length Vs

goal (1 subgoal):
 1. i \<noteq> length Vs \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
hence i: "i < length Vs"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> length Vs

goal (1 subgoal):
 1. i < length Vs
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
i \<noteq> length Vs
i < length (Vs @ [v])

goal (1 subgoal):
 1. i < length Vs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < length Vs

goal (1 subgoal):
 1. i \<noteq> length Vs \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
hence Vsi: "Vs ! i = x"
[PROOF STATE]
proof (prove)
using this:
i < length Vs

goal (1 subgoal):
 1. Vs ! i = x
[PROOF STEP]
using snoc.prems(2) append_Cons_nth_left
[PROOF STATE]
proof (prove)
using this:
i < length Vs
(Vs @ [v]) ! i = x
?i < length ?xs \<Longrightarrow> (?xs @ ?u # ?ys) ! ?i = ?xs ! ?i

goal (1 subgoal):
 1. Vs ! i = x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Vs ! i = x

goal (1 subgoal):
 1. i \<noteq> length Vs \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
hence "x \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
Vs ! i = x

goal (1 subgoal):
 1. x \<noteq> v
[PROOF STEP]
using snoc.prems(3) i
[PROOF STATE]
proof (prove)
using this:
Vs ! i = x
distinct (Vs @ [v])
i < length Vs

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

goal (1 subgoal):
 1. i \<noteq> length Vs \<Longrightarrow> find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> v

goal (1 subgoal):
 1. find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
using snoc.IH[OF i Vsi dist]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> v
find_indices x Vs = [i]

goal (1 subgoal):
 1. find_indices x (Vs @ [v]) = [i]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_indices x (Vs @ [v]) = [i]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
find_indices x (Vs @ [v]) = [i]

goal (1 subgoal):
 1. \<lbrakk>i < length []; [] ! i = x; distinct []\<rbrakk> \<Longrightarrow> find_indices x [] = [i]
[PROOF STEP]
qed auto