[STATEMENT]
lemma fmember_is_indexed_fmember:
  assumes "x |\<in>| s"
  shows "\<exists>i. x |\<in>|\<^bsub>i\<^esub> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. x |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. x |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x |\<in>| s
[PROOF STEP]
have "x \<in> set (list_of_fset s)"
[PROOF STATE]
proof (prove)
using this:
x |\<in>| s

goal (1 subgoal):
 1. x \<in> set (list_of_fset s)
[PROOF STEP]
using mem_fset_from_list
[PROOF STATE]
proof (prove)
using this:
x |\<in>| s
(?x |\<in>| fset_from_list ?l) = (?x \<in> set ?l)

goal (1 subgoal):
 1. x \<in> set (list_of_fset s)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> set (list_of_fset s)

goal (1 subgoal):
 1. \<exists>i. x |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (list_of_fset s)
[PROOF STEP]
obtain i where "i < length (list_of_fset s)" and "x = list_of_fset s ! i"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (list_of_fset s)

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

goal (1 subgoal):
 1. \<exists>i. x |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
hence "x |\<in>|\<^bsub>i\<^esub> s"
[PROOF STATE]
proof (prove)
using this:
i < length (list_of_fset s)
x = list_of_fset s ! i

goal (1 subgoal):
 1. x |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
by (simp add: indexed_fmember.simps)
[PROOF STATE]
proof (state)
this:
x |\<in>|\<^bsub>i\<^esub> s

goal (1 subgoal):
 1. \<exists>i. x |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x |\<in>|\<^bsub>i\<^esub> s

goal (1 subgoal):
 1. \<exists>i. x |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>i. x |\<in>|\<^bsub>i\<^esub> s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma indexed_fmember_unique: "x |\<in>|\<^bsub>i\<^esub> s \<Longrightarrow> y |\<in>|\<^bsub>j\<^esub> s \<Longrightarrow> x = y \<longleftrightarrow> i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x |\<in>|\<^bsub>i\<^esub> s; y |\<in>|\<^bsub>j\<^esub> s\<rbrakk> \<Longrightarrow> (x = y) = (i = j)
[PROOF STEP]
by (metis distinct_list_of_fset indexed_fmember.cases length_list_of_fset nth_eq_iff_index_eq)


[STATEMENT]
lemma mem_set_indexed_members:
  "(i,x) \<in> set (indexed_members s) \<longleftrightarrow> x |\<in>|\<^bsub>i\<^esub> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i, x) \<in> set (indexed_members s)) = (x |\<in>|\<^bsub>i\<^esub> s)
[PROOF STEP]
unfolding indexed_members_def indexed_fmember.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i, x) \<in> set (zip [0..<size s] (list_of_fset s))) = (\<exists>ia sa. x = list_of_fset sa ! ia \<and> i = ia \<and> s = sa \<and> ia < size sa)
[PROOF STEP]
by (force simp add: set_zip)


[STATEMENT]
lemma mem_set_indexed_members'[simp]:
  "t \<in> set (indexed_members s) \<longleftrightarrow> snd t |\<in>|\<^bsub>fst t\<^esub> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<in> set (indexed_members s)) = (snd t |\<in>|\<^bsub>fst t\<^esub> s)
[PROOF STEP]
by (cases t, simp add: mem_set_indexed_members)


[STATEMENT]
lemma fnth_indexed_fmember: "i < size s \<Longrightarrow> s |!| i |\<in>|\<^bsub>i\<^esub> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < size s \<Longrightarrow> s |!| i |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
unfolding fnth_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < size s \<Longrightarrow> list_of_fset s ! i |\<in>|\<^bsub>i\<^esub> s
[PROOF STEP]
by (rule indexed_fmember.intros)


[STATEMENT]
lemma indexed_fmember_fnth: "x |\<in>|\<^bsub>i\<^esub> s \<longleftrightarrow> (s |!| i = x \<and> i < size s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x |\<in>|\<^bsub>i\<^esub> s) = (s |!| i = x \<and> i < size s)
[PROOF STEP]
unfolding fnth_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x |\<in>|\<^bsub>i\<^esub> s) = (list_of_fset s ! i = x \<and> i < size s)
[PROOF STEP]
by (metis indexed_fmember.simps)


[STATEMENT]
lemma fidx_eq[simp]: "x |\<in>|\<^bsub>i\<^esub> s \<Longrightarrow> fidx s x = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x |\<in>|\<^bsub>i\<^esub> s \<Longrightarrow> fidx s x = i
[PROOF STEP]
unfolding fidx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x |\<in>|\<^bsub>i\<^esub> s \<Longrightarrow> (SOME i. x |\<in>|\<^bsub>i\<^esub> s) = i
[PROOF STEP]
by (rule someI2)(auto simp add: indexed_fmember_fnth fnth_def nth_eq_iff_index_eq)


[STATEMENT]
lemma fidx_inj[simp]: "x |\<in>| s \<Longrightarrow> y |\<in>| s \<Longrightarrow> fidx s x = fidx s y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x |\<in>| s; y |\<in>| s\<rbrakk> \<Longrightarrow> (fidx s x = fidx s y) = (x = y)
[PROOF STEP]
by (auto dest!: fmember_is_indexed_fmember simp add: indexed_fmember_unique)


[STATEMENT]
lemma inj_on_fidx: "inj_on (fidx vertices) (fset vertices)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (fidx vertices) (fset vertices)
[PROOF STEP]
by (rule inj_onI) (auto simp: fmember.rep_eq [symmetric])


[STATEMENT]
lemma less_oSuc[iff]: "x < oSuc x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < oSuc x
[PROOF STEP]
by (unfold oSuc_def, rule oStrictLimit_ub)


[STATEMENT]
lemma oSuc_leI: "x < y \<Longrightarrow> oSuc x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> oSuc x \<le> y
[PROOF STEP]
by (unfold oSuc_def, rule oStrictLimit_lub, simp)


[STATEMENT]
lemma less_oSuc_eq_le: "(x < oSuc y) = (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < oSuc y) = (x \<le> y)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x < oSuc y \<Longrightarrow> x \<le> y
 2. x \<le> y \<Longrightarrow> x < oSuc y
[PROOF STEP]
apply (erule contrapos_pp, simp add: linorder_not_less linorder_not_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y < x \<Longrightarrow> oSuc y \<le> x
 2. x \<le> y \<Longrightarrow> x < oSuc y
[PROOF STEP]
apply (erule oSuc_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x < oSuc y
[PROOF STEP]
apply (erule order_le_less_trans[OF _ less_oSuc])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ordinal_0_le [iff]: "0 \<le> (x::ordinal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
by (unfold ordinal_zero_def, rule oZero_least)


[STATEMENT]
lemma ordinal_not_less_0 [iff]: "\<not> (x::ordinal) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x < 0
[PROOF STEP]
by (simp add: linorder_not_less)


[STATEMENT]
lemma ordinal_le_0 [iff]: "(x \<le> 0) = (x = (0::ordinal))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> 0) = (x = 0)
[PROOF STEP]
by (simp add: order_le_less)


[STATEMENT]
lemma ordinal_neq_0 [iff]: "(x \<noteq> 0) = (0 < (x::ordinal))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> 0) = (0 < x)
[PROOF STEP]
by (simp add: order_less_le)


[STATEMENT]
lemma ordinal_not_0_less [iff]: "(\<not> 0 < x) = (x = (0::ordinal))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> 0 < x) = (x = 0)
[PROOF STEP]
by (simp add: linorder_not_less)


[STATEMENT]
lemma zero_less_oSuc [iff]: "0 < oSuc x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < oSuc x
[PROOF STEP]
by (rule order_le_less_trans, rule ordinal_0_le, rule less_oSuc)


[STATEMENT]
lemma oSuc_not_0 [iff]: "oSuc x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oSuc x \<noteq> 0
[PROOF STEP]
by simp


[STATEMENT]
lemma less_oSuc0 [iff]: "(x < oSuc 0) = (x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < oSuc 0) = (x = 0)
[PROOF STEP]
by (simp add: less_oSuc_eq_le)


[STATEMENT]
lemma oSuc_less_oSuc [iff]: "(oSuc x < oSuc y) = (x < y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (oSuc x < oSuc y) = (x < y)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. oSuc x < oSuc y \<Longrightarrow> x < y
 2. x < y \<Longrightarrow> oSuc x < oSuc y
[PROOF STEP]
apply (simp add: less_oSuc_eq_le order_less_le_trans[OF less_oSuc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> oSuc x < oSuc y
[PROOF STEP]
apply (erule order_le_less_trans[OF oSuc_leI less_oSuc])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oSuc_eq_oSuc [iff]: "(oSuc x = oSuc y) = (x = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (oSuc x = oSuc y) = (x = y)
[PROOF STEP]
by (safe, erule contrapos_pp, simp add: linorder_neq_iff)


[STATEMENT]
lemma oSuc_le_oSuc [iff]: "(oSuc x \<le> oSuc y) = (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (oSuc x \<le> oSuc y) = (x \<le> y)
[PROOF STEP]
by (simp add: order_le_less)


[STATEMENT]
lemma le_oSucE:
"\<lbrakk>x \<le> oSuc y; x \<le> y \<Longrightarrow> R; x = oSuc y \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> oSuc y; x \<le> y \<Longrightarrow> R; x = oSuc y \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (auto simp add: order_le_less less_oSuc_eq_le)


[STATEMENT]
lemma less_oSucE:
"\<lbrakk>x < oSuc y; x < y \<Longrightarrow> P; x = y \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < oSuc y; x < y \<Longrightarrow> P; x = y \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto simp add: less_oSuc_eq_le order_le_less)


[STATEMENT]
lemma strict_mono_natI:
fixes f :: "nat \<Rightarrow> 'a::order"
shows "(\<And>n. f n < f (Suc n)) \<Longrightarrow> strict_mono f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. f n < f (Suc n)) \<Longrightarrow> OrdinalInduct.strict_mono f
[PROOF STEP]
apply (rule strict_monoI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>\<And>n. f n < f (Suc n); A < B\<rbrakk> \<Longrightarrow> f A < f B
[PROOF STEP]
apply (drule Suc_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>\<And>n. f n < f (Suc n); Suc A \<le> B\<rbrakk> \<Longrightarrow> f A < f B
[PROOF STEP]
apply (drule le_add_diff_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>\<And>n. f n < f (Suc n); Suc A + (B - Suc A) = B\<rbrakk> \<Longrightarrow> f A < f B
[PROOF STEP]
apply (subgoal_tac "\<forall>k. f A < f (Suc A + k)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A B. \<lbrakk>\<And>n. f n < f (Suc n); Suc A + (B - Suc A) = B; \<forall>k. f A < f (Suc A + k)\<rbrakk> \<Longrightarrow> f A < f B
 2. \<And>A B. \<lbrakk>\<And>n. f n < f (Suc n); Suc A + (B - Suc A) = B\<rbrakk> \<Longrightarrow> \<forall>k. f A < f (Suc A + k)
[PROOF STEP]
apply (erule subst, erule spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>\<And>n. f n < f (Suc n); Suc A + (B - Suc A) = B\<rbrakk> \<Longrightarrow> \<forall>k. f A < f (Suc A + k)
[PROOF STEP]
apply (rule allI, induct_tac k, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B k n. \<lbrakk>\<And>n. f n < f (Suc n); Suc A + (B - Suc A) = B; f A < f (Suc A + n)\<rbrakk> \<Longrightarrow> f A < f (Suc A + Suc n)
[PROOF STEP]
apply (erule order_less_trans, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mono_natI:
fixes f :: "nat \<Rightarrow> 'a::order"
shows "(\<And>n. f n \<le> f (Suc n)) \<Longrightarrow> mono f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. f n \<le> f (Suc n)) \<Longrightarrow> mono f
[PROOF STEP]
apply (rule monoI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>n. f n \<le> f (Suc n); x \<le> y\<rbrakk> \<Longrightarrow> f x \<le> f y
[PROOF STEP]
apply (drule le_add_diff_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>n. f n \<le> f (Suc n); x + (y - x) = y\<rbrakk> \<Longrightarrow> f x \<le> f y
[PROOF STEP]
apply (subgoal_tac "\<forall>k. f x \<le> f (x + k)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<And>n. f n \<le> f (Suc n); x + (y - x) = y; \<forall>k. f x \<le> f (x + k)\<rbrakk> \<Longrightarrow> f x \<le> f y
 2. \<And>x y. \<lbrakk>\<And>n. f n \<le> f (Suc n); x + (y - x) = y\<rbrakk> \<Longrightarrow> \<forall>k. f x \<le> f (x + k)
[PROOF STEP]
apply (erule subst, erule spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>n. f n \<le> f (Suc n); x + (y - x) = y\<rbrakk> \<Longrightarrow> \<forall>k. f x \<le> f (x + k)
[PROOF STEP]
apply (rule allI, induct_tac k, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y k n. \<lbrakk>\<And>n. f n \<le> f (Suc n); x + (y - x) = y; f x \<le> f (x + n)\<rbrakk> \<Longrightarrow> f x \<le> f (x + Suc n)
[PROOF STEP]
apply (erule order_trans, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strict_mono_mono:
fixes f :: "'a::order \<Rightarrow> 'b::order"
shows "strict_mono f \<Longrightarrow> mono f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> mono f
[PROOF STEP]
by (auto intro!: monoI simp add: order_le_less strict_monoD)


[STATEMENT]
lemma strict_mono_monoD:
fixes f :: "'a::order \<Rightarrow> 'b::order"
shows "\<lbrakk>strict_mono f; A \<le> B\<rbrakk> \<Longrightarrow> f A \<le> f B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdinalInduct.strict_mono f; A \<le> B\<rbrakk> \<Longrightarrow> f A \<le> f B
[PROOF STEP]
by (rule monoD[OF strict_mono_mono])


[STATEMENT]
lemma strict_mono_cancel_eq:
fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
shows "strict_mono f \<Longrightarrow> (f x = f y) = (x = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> (f x = f y) = (x = y)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule_tac x=x and y=y in linorder_cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x = f y; x < y\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>OrdinalInduct.strict_mono f; f x = f y; x = y\<rbrakk> \<Longrightarrow> x = y
 3. \<lbrakk>OrdinalInduct.strict_mono f; f x = f y; y < x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (drule strict_monoD, assumption, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x = f y; x = y\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>OrdinalInduct.strict_mono f; f x = f y; y < x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x = f y; y < x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (drule strict_monoD, assumption, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strict_mono_cancel_less:
fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
shows "strict_mono f \<Longrightarrow> (f x < f y) = (x < y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> (f x < f y) = (x < y)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x < f y\<rbrakk> \<Longrightarrow> x < y
 2. \<lbrakk>OrdinalInduct.strict_mono f; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply (rule_tac x=x and y=y in linorder_cases)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x < f y; x < y\<rbrakk> \<Longrightarrow> x < y
 2. \<lbrakk>OrdinalInduct.strict_mono f; f x < f y; x = y\<rbrakk> \<Longrightarrow> x < y
 3. \<lbrakk>OrdinalInduct.strict_mono f; f x < f y; y < x\<rbrakk> \<Longrightarrow> x < y
 4. \<lbrakk>OrdinalInduct.strict_mono f; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x < f y; x = y\<rbrakk> \<Longrightarrow> x < y
 2. \<lbrakk>OrdinalInduct.strict_mono f; f x < f y; y < x\<rbrakk> \<Longrightarrow> x < y
 3. \<lbrakk>OrdinalInduct.strict_mono f; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x < f y; y < x\<rbrakk> \<Longrightarrow> x < y
 2. \<lbrakk>OrdinalInduct.strict_mono f; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply (drule strict_monoD, assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdinalInduct.strict_mono f; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply (simp add: strict_monoD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strict_mono_cancel_le:
fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
shows "strict_mono f \<Longrightarrow> (f x \<le> f y) = (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> (f x \<le> f y) = (x \<le> y)
[PROOF STEP]
apply (auto simp add: order_le_less)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; x \<noteq> y; f x < f y\<rbrakk> \<Longrightarrow> x < y
 2. \<lbrakk>OrdinalInduct.strict_mono f; x \<noteq> y; f x = f y\<rbrakk> \<Longrightarrow> x < y
 3. \<lbrakk>OrdinalInduct.strict_mono f; f x \<noteq> f y; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply (simp add: strict_mono_cancel_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>OrdinalInduct.strict_mono f; x \<noteq> y; f x = f y\<rbrakk> \<Longrightarrow> x < y
 2. \<lbrakk>OrdinalInduct.strict_mono f; f x \<noteq> f y; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply (simp add: strict_mono_cancel_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdinalInduct.strict_mono f; f x \<noteq> f y; x < y\<rbrakk> \<Longrightarrow> f x < f y
[PROOF STEP]
apply (simp add: strict_monoD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_leI: "\<forall>n. f n \<le> x \<Longrightarrow> oLimit f \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n \<le> x \<Longrightarrow> oLimit f \<le> x
[PROOF STEP]
apply (unfold oLimit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n \<le> x \<Longrightarrow> (LEAST k. \<forall>n. f n \<le> k) \<le> x
[PROOF STEP]
apply (erule Least_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_oLimit [iff]: "f n \<le> oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<le> oLimit f
[PROOF STEP]
apply (unfold oLimit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<le> (LEAST k. \<forall>n. f n \<le> k)
[PROOF STEP]
apply (rule_tac x=n in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. f x \<le> (LEAST k. \<forall>n. f n \<le> k)
[PROOF STEP]
apply (rule_tac k="oStrictLimit f" in LeastI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. f x \<le> oStrictLimit f
[PROOF STEP]
apply (clarify, rule order_less_imp_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f x < oStrictLimit f
[PROOF STEP]
apply (rule oStrictLimit_ub)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_oLimitI: "x \<le> f n \<Longrightarrow> x \<le> oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> f n \<Longrightarrow> x \<le> oLimit f
[PROOF STEP]
by (erule order_trans, rule le_oLimit)


[STATEMENT]
lemma less_oLimitI: "x < f n \<Longrightarrow> x < oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < f n \<Longrightarrow> x < oLimit f
[PROOF STEP]
by (erule order_less_le_trans, rule le_oLimit)


[STATEMENT]
lemma less_oLimitD: "x < oLimit f \<Longrightarrow> \<exists>n. x < f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < oLimit f \<Longrightarrow> \<exists>n. x < f n
[PROOF STEP]
apply (unfold oLimit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < (LEAST k. \<forall>n. f n \<le> k) \<Longrightarrow> \<exists>n. x < f n
[PROOF STEP]
apply (drule not_less_Least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>n. f n \<le> x) \<Longrightarrow> \<exists>n. x < f n
[PROOF STEP]
apply (simp add: linorder_not_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma less_oLimitE:
"\<lbrakk>x < oLimit f; \<And>n. x < f n \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < oLimit f; \<And>n. x < f n \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto dest: less_oLimitD)


[STATEMENT]
lemma le_oLimitE:
"\<lbrakk>x \<le> oLimit f; \<And>n. x \<le> f n \<Longrightarrow> R; x = oLimit f \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> oLimit f; \<And>n. x \<le> f n \<Longrightarrow> R; x = oLimit f \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (auto simp add: order_le_less dest: less_oLimitD)


[STATEMENT]
lemma oLimit_const [simp]: "oLimit (\<lambda>n. x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oLimit (\<lambda>n. x) = x
[PROOF STEP]
apply (rule order_antisym[OF _ le_oLimit])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oLimit (\<lambda>n. x) \<le> x
[PROOF STEP]
apply (rule oLimit_leI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strict_mono_less_oLimit:
"strict_mono f \<Longrightarrow> f n < oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> f n < oLimit f
[PROOF STEP]
apply (rule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> f n < ?y
 2. OrdinalInduct.strict_mono f \<Longrightarrow> ?y \<le> oLimit f
[PROOF STEP]
apply (erule strict_monoD, rule lessI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> f (Suc n) \<le> oLimit f
[PROOF STEP]
apply (rule le_oLimit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_eqI:
"\<lbrakk>\<And>n. \<exists>m. f n \<le> g m; \<And>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> oLimit f = oLimit g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<exists>m. f n \<le> g m; \<And>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> oLimit f = oLimit g
[PROOF STEP]
apply atomize
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. \<exists>m. f n \<le> g m; \<forall>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> oLimit f = oLimit g
[PROOF STEP]
apply (rule order_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n. \<exists>m. f n \<le> g m; \<forall>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> oLimit f \<le> oLimit g
 2. \<lbrakk>\<forall>n. \<exists>m. f n \<le> g m; \<forall>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> oLimit g \<le> oLimit f
[PROOF STEP]
apply (rule oLimit_leI, clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. \<exists>m. f n \<le> g m; \<forall>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> f n \<le> oLimit g
 2. \<lbrakk>\<forall>n. \<exists>m. f n \<le> g m; \<forall>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> oLimit g \<le> oLimit f
[PROOF STEP]
apply (drule spec, erule exE, erule le_oLimitI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. \<exists>m. f n \<le> g m; \<forall>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> oLimit g \<le> oLimit f
[PROOF STEP]
apply (rule oLimit_leI, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n. \<exists>m. f n \<le> g m; \<forall>n. \<exists>m. g n \<le> f m\<rbrakk> \<Longrightarrow> g n \<le> oLimit f
[PROOF STEP]
apply (drule spec, erule exE, erule le_oLimitI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_Suc:
"f 0 < oLimit f \<Longrightarrow> oLimit (\<lambda>n. f (Suc n)) = oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 < oLimit f \<Longrightarrow> oLimit (\<lambda>n. f (Suc n)) = oLimit f
[PROOF STEP]
apply (rule oLimit_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. f 0 < oLimit f \<Longrightarrow> \<exists>m. f (Suc n) \<le> f m
 2. \<And>n. f 0 < oLimit f \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
[PROOF STEP]
apply (rule exI, rule order_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. f 0 < oLimit f \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
[PROOF STEP]
apply (case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>f 0 < oLimit f; n = 0\<rbrakk> \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
 2. \<And>n nat. \<lbrakk>f 0 < oLimit f; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
[PROOF STEP]
apply (drule less_oLimitD, clarify, rename_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m. f 0 < f m \<Longrightarrow> \<exists>m. f 0 \<le> f (Suc m)
 2. \<And>n nat. \<lbrakk>f 0 < oLimit f; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
[PROOF STEP]
apply (case_tac m, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m nat. \<lbrakk>f 0 < f m; m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>m. f 0 \<le> f (Suc m)
 2. \<And>n nat. \<lbrakk>f 0 < oLimit f; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
[PROOF STEP]
apply (rule_tac x=nat in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m nat. \<lbrakk>f 0 < f m; m = Suc nat\<rbrakk> \<Longrightarrow> f 0 \<le> f (Suc nat)
 2. \<And>n nat. \<lbrakk>f 0 < oLimit f; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
[PROOF STEP]
apply (simp add: order_less_imp_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n nat. \<lbrakk>f 0 < oLimit f; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>m. f n \<le> f (Suc m)
[PROOF STEP]
apply (rule_tac x=nat in exI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_shift:
"\<forall>n. f n < oLimit f \<Longrightarrow> oLimit (\<lambda>n. f (n + k)) = oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> oLimit (\<lambda>n. f (n + k)) = oLimit f
[PROOF STEP]
apply (induct_tac k, simp, rename_tac k)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>n. f n < oLimit f; oLimit (\<lambda>n. f (n + k)) = oLimit f\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. f (n + Suc k)) = oLimit f
[PROOF STEP]
apply (simp only: add_Suc_right add_Suc[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>n. f n < oLimit f; oLimit (\<lambda>n. f (n + k)) = oLimit f\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. f (Suc n + k)) = oLimit f
[PROOF STEP]
apply (rule trans[OF oLimit_Suc], simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_shift_mono:
"mono f \<Longrightarrow> oLimit (\<lambda>n. f (n + k)) = oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono f \<Longrightarrow> oLimit (\<lambda>n. f (n + k)) = oLimit f
[PROOF STEP]
apply (rule oLimit_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. mono f \<Longrightarrow> \<exists>m. f (n + k) \<le> f m
 2. \<And>n. mono f \<Longrightarrow> \<exists>m. f n \<le> f (m + k)
[PROOF STEP]
apply (rule exI, rule order_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. mono f \<Longrightarrow> \<exists>m. f n \<le> f (m + k)
[PROOF STEP]
apply (rule_tac x=n in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. mono f \<Longrightarrow> f n \<le> f (n + k)
[PROOF STEP]
apply (erule monoD, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma limit_ordinal_not_0 [simp]: "\<not> limit_ordinal 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> limit_ordinal 0
[PROOF STEP]
by (simp add: limit_ordinal_def)


[STATEMENT]
lemma zero_less_limit_ordinal [simp]: "limit_ordinal x \<Longrightarrow> 0 < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_ordinal x \<Longrightarrow> 0 < x
[PROOF STEP]
by (simp add: limit_ordinal_def)


[STATEMENT]
lemma limit_ordinal_not_oSuc [simp]: "\<not> limit_ordinal (oSuc p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> limit_ordinal (oSuc p)
[PROOF STEP]
by (simp add: limit_ordinal_def)


[STATEMENT]
lemma oSuc_less_limit_ordinal:
"limit_ordinal x \<Longrightarrow> (oSuc w < x) = (w < x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_ordinal x \<Longrightarrow> (oSuc w < x) = (w < x)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>limit_ordinal x; oSuc w < x\<rbrakk> \<Longrightarrow> w < x
 2. \<lbrakk>limit_ordinal x; w < x\<rbrakk> \<Longrightarrow> oSuc w < x
[PROOF STEP]
apply (erule order_less_trans[OF less_oSuc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>limit_ordinal x; w < x\<rbrakk> \<Longrightarrow> oSuc w < x
[PROOF STEP]
apply (simp add: linorder_not_le[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>limit_ordinal x; \<not> x \<le> w\<rbrakk> \<Longrightarrow> \<not> x \<le> oSuc w
[PROOF STEP]
apply (erule contrapos_nn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>limit_ordinal x; x \<le> oSuc w\<rbrakk> \<Longrightarrow> x \<le> w
[PROOF STEP]
apply (auto simp add: order_le_less less_oSuc_eq_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma limit_ordinal_oLimitI:
"\<forall>n. f n < oLimit f \<Longrightarrow> limit_ordinal (oLimit f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> limit_ordinal (oLimit f)
[PROOF STEP]
apply (unfold limit_ordinal_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> 0 < oLimit f \<and> (\<forall>y. oLimit f \<noteq> oSuc y)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> 0 < oLimit f
 2. \<forall>n. f n < oLimit f \<Longrightarrow> \<forall>y. oLimit f \<noteq> oSuc y
[PROOF STEP]
apply (rule order_le_less_trans[OF ordinal_0_le])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> ?y3 < oLimit f
 2. \<forall>n. f n < oLimit f \<Longrightarrow> \<forall>y. oLimit f \<noteq> oSuc y
[PROOF STEP]
apply (erule spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> \<forall>y. oLimit f \<noteq> oSuc y
[PROOF STEP]
apply (clarsimp simp add: less_oSuc_eq_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<forall>n. f n \<le> y; oLimit f = oSuc y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule oLimit_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>oLimit f = oSuc y; oLimit f \<le> y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: linorder_not_less[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strict_mono_limit_ordinal:
"strict_mono f \<Longrightarrow> limit_ordinal (oLimit f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> limit_ordinal (oLimit f)
[PROOF STEP]
apply (rule limit_ordinal_oLimitI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalInduct.strict_mono f \<Longrightarrow> \<forall>n. f n < oLimit f
[PROOF STEP]
apply (simp add: strict_mono_less_oLimit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma limit_ordinalI:
"\<lbrakk>0 < z; \<forall>x<z. oSuc x < z\<rbrakk> \<Longrightarrow> limit_ordinal z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < z; \<forall>x<z. oSuc x < z\<rbrakk> \<Longrightarrow> limit_ordinal z
[PROOF STEP]
apply (erule contrapos_pp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x<z. oSuc x < z; \<not> limit_ordinal z\<rbrakk> \<Longrightarrow> \<not> 0 < z
[PROOF STEP]
apply (unfold limit_ordinal_def, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<forall>x<oSuc y. x < y; z = oSuc y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac x=y in spec, clarsimp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_make_mono_less:
"\<forall>n. f n < oLimit f \<Longrightarrow> f (make_mono f n) < f (make_mono f (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> f (make_mono f n) < f (make_mono f (Suc n))
[PROOF STEP]
apply (drule_tac x="make_mono f n" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (make_mono f n) < oLimit f \<Longrightarrow> f (make_mono f n) < f (make_mono f (Suc n))
[PROOF STEP]
apply (drule less_oLimitD, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. f (make_mono f n) < f na \<Longrightarrow> f (make_mono f n) < f (LEAST x. f (make_mono f n) < f x)
[PROOF STEP]
apply (erule LeastI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strict_mono_f_make_mono:
"\<forall>n. f n < oLimit f \<Longrightarrow> strict_mono (\<lambda>n. f (make_mono f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> OrdinalInduct.strict_mono (\<lambda>n. f (make_mono f n))
[PROOF STEP]
by (rule strict_mono_natI, erule f_make_mono_less)


[STATEMENT]
lemma le_f_make_mono:
"\<lbrakk>\<forall>n. f n < oLimit f; m \<le> make_mono f n\<rbrakk> \<Longrightarrow> f m \<le> f (make_mono f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; m \<le> make_mono f n\<rbrakk> \<Longrightarrow> f m \<le> f (make_mono f n)
[PROOF STEP]
apply (auto simp add: order_le_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; f m \<noteq> f (make_mono f n); m < make_mono f n\<rbrakk> \<Longrightarrow> f m < f (make_mono f n)
[PROOF STEP]
apply (case_tac n, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<forall>n. f n < oLimit f; f m \<noteq> f (LEAST x. f (make_mono f nat) < f x); m < (LEAST x. f (make_mono f nat) < f x); n = Suc nat\<rbrakk> \<Longrightarrow> f m < f (LEAST x. f (make_mono f nat) < f x)
[PROOF STEP]
apply (drule not_less_Least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<forall>n. f n < oLimit f; f m \<noteq> f (LEAST x. f (make_mono f nat) < f x); n = Suc nat; \<not> f (make_mono f nat) < f m\<rbrakk> \<Longrightarrow> f m < f (LEAST x. f (make_mono f nat) < f x)
[PROOF STEP]
apply (simp add: linorder_not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<forall>n. f n < oLimit f; f m \<noteq> f (LEAST x. f (make_mono f nat) < f x); n = Suc nat; f m \<le> f (make_mono f nat)\<rbrakk> \<Longrightarrow> f m < f (LEAST x. f (make_mono f nat) < f x)
[PROOF STEP]
apply (erule order_le_less_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<forall>n. f n < oLimit f; f m \<noteq> f (LEAST x. f (make_mono f nat) < f x); n = Suc nat\<rbrakk> \<Longrightarrow> f (make_mono f nat) < f (LEAST x. f (make_mono f nat) < f x)
[PROOF STEP]
apply (rule LeastI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<forall>n. f n < oLimit f; f m \<noteq> f (LEAST x. f (make_mono f nat) < f x); n = Suc nat\<rbrakk> \<Longrightarrow> f (make_mono f nat) < f (?k11 nat)
[PROOF STEP]
apply (erule f_make_mono_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma make_mono_less:
"\<forall>n. f n < oLimit f \<Longrightarrow> make_mono f n < make_mono f (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> make_mono f n < make_mono f (Suc n)
[PROOF STEP]
apply (frule_tac n=n in f_make_mono_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; f (make_mono f n) < f (make_mono f (Suc n))\<rbrakk> \<Longrightarrow> make_mono f n < make_mono f (Suc n)
[PROOF STEP]
apply (rule ccontr, simp only: linorder_not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; f (make_mono f n) < f (make_mono f (Suc n)); make_mono f (Suc n) \<le> make_mono f n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule le_f_make_mono, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f (make_mono f n) < f (make_mono f (Suc n)); make_mono f (Suc n) \<le> make_mono f n; f (make_mono f (Suc n)) \<le> f (make_mono f n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: linorder_not_less[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_make_mono_eq:
"\<forall>n. f n < oLimit f \<Longrightarrow> oLimit (\<lambda>n. f (make_mono f n)) = oLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> oLimit (\<lambda>n. f (make_mono f n)) = oLimit f
[PROOF STEP]
apply (rule oLimit_eqI, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n. f n < oLimit f \<Longrightarrow> \<exists>m. f n \<le> f (make_mono f m)
[PROOF STEP]
apply (rule_tac x=n in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n. f n < oLimit f \<Longrightarrow> f n \<le> f (make_mono f n)
[PROOF STEP]
apply (rule le_f_make_mono, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n. f n < oLimit f \<Longrightarrow> n \<le> make_mono f n
[PROOF STEP]
apply (induct_tac n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>\<forall>n. f n < oLimit f; na \<le> make_mono f na\<rbrakk> \<Longrightarrow> Suc na \<le> make_mono f (Suc na)
[PROOF STEP]
apply (rule Suc_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>\<forall>n. f n < oLimit f; na \<le> make_mono f na\<rbrakk> \<Longrightarrow> na < make_mono f (Suc na)
[PROOF STEP]
apply (erule order_le_less_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<forall>n. f n < oLimit f \<Longrightarrow> make_mono f na < make_mono f (Suc na)
[PROOF STEP]
apply (erule make_mono_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_le_oStrictLimit: "oLimit f \<le> oStrictLimit f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oLimit f \<le> oStrictLimit f
[PROOF STEP]
apply (rule oLimit_leI, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. f n \<le> oStrictLimit f
[PROOF STEP]
apply (rule order_less_imp_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. f n < oStrictLimit f
[PROOF STEP]
apply (rule oStrictLimit_ub)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_induct:
assumes zero: "P 0"
    and suc:  "\<And>x. P x \<Longrightarrow> P (oSuc x)"
    and lim:  "\<And>f. \<lbrakk>strict_mono f; \<forall>n. P (f n)\<rbrakk> \<Longrightarrow> P (oLimit f)"
shows "P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P a
[PROOF STEP]
apply (rule oStrictLimit_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. P oZero
 2. \<And>f. \<forall>n. P (f n) \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (rule zero[unfolded ordinal_zero_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<forall>n. P (f n) \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (cut_tac f=f in oLimit_le_oStrictLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (simp add: order_le_less, erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f < oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (drule less_oStrictLimitD, clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f n. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (subgoal_tac "oStrictLimit f = oSuc (f n)", simp add: suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f n. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> oStrictLimit f = oSuc (f n)
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (rule order_antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f n. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> oStrictLimit f \<le> oSuc (f n)
 2. \<And>f n. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> oSuc (f n) \<le> oStrictLimit f
 3. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (rule oStrictLimit_lub, clarify)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f n na. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> f na < oSuc (f n)
 2. \<And>f n. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> oSuc (f n) \<le> oStrictLimit f
 3. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (simp add: less_oSuc_eq_le)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f n na. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> f na \<le> f n
 2. \<And>f n. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> oSuc (f n) \<le> oStrictLimit f
 3. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (erule order_trans[OF le_oLimit])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f n. \<lbrakk>\<forall>n. P (f n); oLimit f \<le> f n\<rbrakk> \<Longrightarrow> oSuc (f n) \<le> oStrictLimit f
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (rule oSuc_leI, rule oStrictLimit_ub)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
[PROOF STEP]
apply (subgoal_tac "\<forall>n. f n < oLimit f")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f; \<forall>n. f n < oLimit f\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> \<forall>n. f n < oLimit f
[PROOF STEP]
apply (subgoal_tac "P (oLimit (\<lambda>n. f (make_mono f n)))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f; \<forall>n. f n < oLimit f; P (oLimit (\<lambda>n. f (make_mono f n)))\<rbrakk> \<Longrightarrow> P (oStrictLimit f)
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f; \<forall>n. f n < oLimit f\<rbrakk> \<Longrightarrow> P (oLimit (\<lambda>n. f (make_mono f n)))
 3. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> \<forall>n. f n < oLimit f
[PROOF STEP]
apply (simp add: oLimit_make_mono_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f; \<forall>n. f n < oLimit f\<rbrakk> \<Longrightarrow> P (oLimit (\<lambda>n. f (make_mono f n)))
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> \<forall>n. f n < oLimit f
[PROOF STEP]
apply (rule lim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f; \<forall>n. f n < oLimit f\<rbrakk> \<Longrightarrow> OrdinalInduct.strict_mono (\<lambda>n. f (make_mono f n))
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f; \<forall>n. f n < oLimit f\<rbrakk> \<Longrightarrow> \<forall>n. P (f (make_mono f n))
 3. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> \<forall>n. f n < oLimit f
[PROOF STEP]
apply (erule strict_mono_f_make_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f; \<forall>n. f n < oLimit f\<rbrakk> \<Longrightarrow> \<forall>n. P (f (make_mono f n))
 2. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> \<forall>n. f n < oLimit f
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. P (f n); oLimit f = oStrictLimit f\<rbrakk> \<Longrightarrow> \<forall>n. f n < oLimit f
[PROOF STEP]
apply (simp add: oStrictLimit_ub)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma convex_hull_carrier[intro]: "Vs \<subseteq> carrier_vec n \<Longrightarrow> convex_hull Vs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vs \<subseteq> carrier_vec n \<Longrightarrow> convex_hull Vs \<subseteq> carrier_vec n
[PROOF STEP]
unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vs \<subseteq> carrier_vec n \<Longrightarrow> {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)} \<subseteq> carrier_vec n
[PROOF STEP]
by auto


[STATEMENT]
lemma convex_hull_mono: "Vs \<subseteq> Ws \<Longrightarrow> convex_hull Vs \<subseteq> convex_hull Ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vs \<subseteq> Ws \<Longrightarrow> convex_hull Vs \<subseteq> convex_hull Ws
[PROOF STEP]
unfolding convex_hull_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vs \<subseteq> Ws \<Longrightarrow> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> Vs \<and> convex_lincomb c Ws x} \<subseteq> {x. \<exists>Wsa c. finite Wsa \<and> Wsa \<subseteq> Ws \<and> convex_lincomb c Wsa x}
[PROOF STEP]
by auto


[STATEMENT]
lemma convex_lincomb_empty[simp]: "\<not> (convex_lincomb c {} x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> convex_lincomb c {} x
[PROOF STEP]
unfolding convex_lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (nonneg_lincomb c {} x \<and> sum c {} = (1::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma set_in_convex_hull:
  assumes "A \<subseteq> carrier_vec n"
  shows "A \<subseteq> convex_hull A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> convex_hull A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> convex_hull A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> convex_hull A
[PROOF STEP]
assume "a \<in> A"
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> convex_hull A
[PROOF STEP]
hence acarr: "a \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
a \<in> A

goal (1 subgoal):
 1. a \<in> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> A
A \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> convex_hull A
[PROOF STEP]
hence "convex_lincomb (\<lambda> x. 1) {a} a "
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier_vec n

goal (1 subgoal):
 1. convex_lincomb (\<lambda>x. 1::'a) {a} a
[PROOF STEP]
unfolding convex_lincomb_def
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier_vec n

goal (1 subgoal):
 1. nonneg_lincomb (\<lambda>x. 1::'a) {a} a \<and> (\<Sum>x\<in>{a}. (1::'a)) = (1::'a)
[PROOF STEP]
by (auto simp: nonneg_lincomb_def lincomb_def)
[PROOF STATE]
proof (state)
this:
convex_lincomb (\<lambda>x. 1::'a) {a} a

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> convex_hull A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convex_lincomb (\<lambda>x. 1::'a) {a} a
[PROOF STEP]
show "a \<in> convex_hull A"
[PROOF STATE]
proof (prove)
using this:
convex_lincomb (\<lambda>x. 1::'a) {a} a

goal (1 subgoal):
 1. a \<in> convex_hull A
[PROOF STEP]
using \<open>a \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
convex_lincomb (\<lambda>x. 1::'a) {a} a
a \<in> A

goal (1 subgoal):
 1. a \<in> convex_hull A
[PROOF STEP]
unfolding convex_hull_def
[PROOF STATE]
proof (prove)
using this:
convex_lincomb (\<lambda>x. 1::'a) {a} a
a \<in> A

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_hull_empty[simp]:
  "convex_hull {} = {}"
  "A \<subseteq> carrier_vec n \<Longrightarrow> convex_hull A = {} \<longleftrightarrow> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull {} = {} &&& (A \<subseteq> carrier_vec n \<Longrightarrow> (convex_hull A = {}) = (A = {}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. convex_hull {} = {}
 2. A \<subseteq> carrier_vec n \<Longrightarrow> (convex_hull A = {}) = (A = {})
[PROOF STEP]
show "convex_hull {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull {} = {}
[PROOF STEP]
unfolding convex_hull_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> {} \<and> convex_lincomb c Ws x} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
convex_hull {} = {}

goal (1 subgoal):
 1. A \<subseteq> carrier_vec n \<Longrightarrow> (convex_hull A = {}) = (A = {})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convex_hull {} = {}
[PROOF STEP]
show "A \<subseteq> carrier_vec n \<Longrightarrow> convex_hull A = {} \<longleftrightarrow> A = {}"
[PROOF STATE]
proof (prove)
using this:
convex_hull {} = {}

goal (1 subgoal):
 1. A \<subseteq> carrier_vec n \<Longrightarrow> (convex_hull A = {}) = (A = {})
[PROOF STEP]
using set_in_convex_hull[of A]
[PROOF STATE]
proof (prove)
using this:
convex_hull {} = {}
A \<subseteq> carrier_vec n \<Longrightarrow> A \<subseteq> convex_hull A

goal (1 subgoal):
 1. A \<subseteq> carrier_vec n \<Longrightarrow> (convex_hull A = {}) = (A = {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<subseteq> carrier_vec n \<Longrightarrow> (convex_hull A = {}) = (A = {})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_hull_bound: assumes XBnd: "X \<subseteq> Bounded_vec Bnd"
  and X: "X \<subseteq> carrier_vec n"
shows "convex_hull X \<subseteq> Bounded_vec Bnd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull X \<subseteq> Bounded_vec Bnd
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull X \<Longrightarrow> x \<in> Bounded_vec Bnd
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull X \<Longrightarrow> x \<in> Bounded_vec Bnd
[PROOF STEP]
assume "x \<in> convex_hull X"
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull X

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull X \<Longrightarrow> x \<in> Bounded_vec Bnd
[PROOF STEP]
from this[unfolded convex_hull_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> X \<and> convex_lincomb c Ws x}
[PROOF STEP]
obtain Y c where fin: "finite Y" and YX: "Y \<subseteq> X" and cx: "convex_lincomb c Y x"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> X \<and> convex_lincomb c Ws x}

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull X \<Longrightarrow> x \<in> Bounded_vec Bnd
[PROOF STEP]
from cx[unfolded convex_lincomb_def nonneg_lincomb_def]
[PROOF STATE]
proof (chain)
picking this:
(lincomb c Y = x \<and> c ` Y \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum c Y = (1::'a)
[PROOF STEP]
have x: "x = lincomb c Y" and sum: "sum c Y = 1" and c0: "\<And> y. y \<in> Y \<Longrightarrow> c y \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
(lincomb c Y = x \<and> c ` Y \<subseteq> Collect ((\<le>) (0::'a))) \<and> sum c Y = (1::'a)

goal (1 subgoal):
 1. x = lincomb c Y &&& sum c Y = (1::'a) &&& (\<And>y. y \<in> Y \<Longrightarrow> (0::'a) \<le> c y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = lincomb c Y
sum c Y = (1::'a)
?y3 \<in> Y \<Longrightarrow> (0::'a) \<le> c ?y3

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull X \<Longrightarrow> x \<in> Bounded_vec Bnd
[PROOF STEP]
from YX X XBnd
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> X
X \<subseteq> carrier_vec n
X \<subseteq> Bounded_vec Bnd
[PROOF STEP]
have Y: "Y \<subseteq> carrier_vec n" and YBnd: "Y \<subseteq> Bounded_vec Bnd"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> X
X \<subseteq> carrier_vec n
X \<subseteq> Bounded_vec Bnd

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull X \<Longrightarrow> x \<in> Bounded_vec Bnd
[PROOF STEP]
from x Y
[PROOF STATE]
proof (chain)
picking this:
x = lincomb c Y
Y \<subseteq> carrier_vec n
[PROOF STEP]
have dim: "dim_vec x = n"
[PROOF STATE]
proof (prove)
using this:
x = lincomb c Y
Y \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull X \<Longrightarrow> x \<in> Bounded_vec Bnd
[PROOF STEP]
show "x \<in> Bounded_vec Bnd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Bounded_vec Bnd
[PROOF STEP]
unfolding Bounded_vec_def mem_Collect_eq dim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
assume i: "i < n"
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
have "abs (x $ i) = abs (\<Sum>x\<in>Y. c x * x $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x $ i\<bar> = \<bar>\<Sum>x\<in>Y. c x * x $ i\<bar>
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>lincomb c Y $ i\<bar> = \<bar>\<Sum>x\<in>Y. c x * x $ i\<bar>
[PROOF STEP]
by (subst lincomb_index[OF i Y], auto)
[PROOF STATE]
proof (state)
this:
\<bar>x $ i\<bar> = \<bar>\<Sum>x\<in>Y. c x * x $ i\<bar>

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x $ i\<bar> = \<bar>\<Sum>x\<in>Y. c x * x $ i\<bar>

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
have "\<dots> \<le> (\<Sum>x\<in>Y. abs (c x * x $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<Sum>x\<in>Y. c x * x $ i\<bar> \<le> (\<Sum>x\<in>Y. \<bar>c x * x $ i\<bar>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>x\<in>Y. c x * x $ i\<bar> \<le> (\<Sum>x\<in>Y. \<bar>c x * x $ i\<bar>)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>x\<in>Y. c x * x $ i\<bar> \<le> (\<Sum>x\<in>Y. \<bar>c x * x $ i\<bar>)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>Y. abs (c x) * abs (x $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>Y. \<bar>c x * x $ i\<bar>) = (\<Sum>x\<in>Y. \<bar>c x\<bar> * \<bar>x $ i\<bar>)
[PROOF STEP]
by (simp add: abs_mult)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x * x $ i\<bar>) = (\<Sum>x\<in>Y. \<bar>c x\<bar> * \<bar>x $ i\<bar>)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x * x $ i\<bar>) = (\<Sum>x\<in>Y. \<bar>c x\<bar> * \<bar>x $ i\<bar>)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
have "\<dots> \<le> (\<Sum>x\<in>Y. abs (c x) * Bnd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>Y. \<bar>c x\<bar> * \<bar>x $ i\<bar>) \<le> (\<Sum>x\<in>Y. \<bar>c x\<bar> * Bnd)
[PROOF STEP]
by (intro sum_mono mult_left_mono, insert YBnd[unfolded Bounded_vec_def] i Y, force+)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x\<bar> * \<bar>x $ i\<bar>) \<le> (\<Sum>x\<in>Y. \<bar>c x\<bar> * Bnd)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x\<bar> * \<bar>x $ i\<bar>) \<le> (\<Sum>x\<in>Y. \<bar>c x\<bar> * Bnd)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>Y. abs (c x)) * Bnd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>Y. \<bar>c x\<bar> * Bnd) = (\<Sum>x\<in>Y. \<bar>c x\<bar>) * Bnd
[PROOF STEP]
by (simp add: sum_distrib_right)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x\<bar> * Bnd) = (\<Sum>x\<in>Y. \<bar>c x\<bar>) * Bnd

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x\<bar> * Bnd) = (\<Sum>x\<in>Y. \<bar>c x\<bar>) * Bnd

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
have "(\<Sum>x\<in>Y. abs (c x)) = (\<Sum>x\<in>Y. c x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>Y. \<bar>c x\<bar>) = sum c Y
[PROOF STEP]
by (rule sum.cong, insert c0, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x\<bar>) = sum c Y

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>Y. \<bar>c x\<bar>) = sum c Y

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum c Y = (1::'a)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
sum c Y = (1::'a)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>x $ i\<bar> \<le> (1::'a) * Bnd
[PROOF STEP]
show "\<bar>x $ i\<bar> \<le> Bnd"
[PROOF STATE]
proof (prove)
using this:
\<bar>x $ i\<bar> \<le> (1::'a) * Bnd

goal (1 subgoal):
 1. \<bar>x $ i\<bar> \<le> Bnd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>x $ i\<bar> \<le> Bnd

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lincomb_list_elem:
  "set Vs \<subseteq> carrier_vec n \<Longrightarrow>
   lincomb_list (\<lambda> j. if i=j then 1 else 0) Vs = (if i < length Vs then Vs ! i else 0\<^sub>v n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = (if i < length Vs then Vs ! i else 0\<^sub>v n)
[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>j. if i = j then 1::'a else (0::'a)) [] = (if i < length [] then [] ! i else 0\<^sub>v n)
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) xs = (if i < length xs then xs ! i else 0\<^sub>v n); set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (xs @ [x]) = (if i < length (xs @ [x]) then (xs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
case (snoc x Vs)
[PROOF STATE]
proof (state)
this:
set Vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = (if i < length Vs then Vs ! i else 0\<^sub>v n)
set (Vs @ [x]) \<subseteq> carrier_vec n

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) [] = (if i < length [] then [] ! i else 0\<^sub>v n)
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) xs = (if i < length xs then xs ! i else 0\<^sub>v n); set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (xs @ [x]) = (if i < length (xs @ [x]) then (xs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have x: "x \<in> carrier_vec n" and Vs: "set Vs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier_vec n &&& set Vs \<subseteq> carrier_vec n
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
set (Vs @ [x]) \<subseteq> carrier_vec n

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

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) [] = (if i < length [] then [] ! i else 0\<^sub>v n)
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) xs = (if i < length xs then xs ! i else 0\<^sub>v n); set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (xs @ [x]) = (if i < length (xs @ [x]) then (xs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
let ?f = "\<lambda> j. if i = j then 1 else 0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) [] = (if i < length [] then [] ! i else 0\<^sub>v n)
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) xs = (if i < length xs then xs ! i else 0\<^sub>v n); set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (xs @ [x]) = (if i < length (xs @ [x]) then (xs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "lincomb_list ?f (Vs @ [x]) = lincomb_list ?f Vs + ?f (length Vs) \<cdot>\<^sub>v x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (Vs @ [x]) = lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x
[PROOF STEP]
using x Vs
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec n
set Vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (Vs @ [x]) = lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (Vs @ [x]) = lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x

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

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) [] = (if i < length [] then [] ! i else 0\<^sub>v n)
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) xs = (if i < length xs then xs ! i else 0\<^sub>v n); set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (xs @ [x]) = (if i < length (xs @ [x]) then (xs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "\<dots> = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)" (is ?goal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
using less_linear[of i "length Vs"]
[PROOF STATE]
proof (prove)
using this:
i < length Vs \<or> i = length Vs \<or> length Vs < i

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i < length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 3. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
assume i: "i < length Vs"
[PROOF STATE]
proof (state)
this:
i < length Vs

goal (3 subgoals):
 1. i < length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 3. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "lincomb_list (\<lambda>j. if i = j then 1 else 0) Vs = Vs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = Vs ! i
[PROOF STEP]
using snoc.IH[OF Vs] i
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = (if i < length Vs then Vs ! i else 0\<^sub>v n)
i < length Vs

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = Vs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = Vs ! i

goal (3 subgoals):
 1. i < length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 3. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = Vs ! i

goal (3 subgoals):
 1. i < length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 3. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "(if i = length Vs then 1 else 0) \<cdot>\<^sub>v x = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
[PROOF STEP]
using i x
[PROOF STATE]
proof (prove)
using this:
i < length Vs
x \<in> carrier_vec n

goal (1 subgoal):
 1. (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n

goal (3 subgoals):
 1. i < length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 3. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n

goal (3 subgoals):
 1. i < length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 3. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = Vs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = Vs ! i
[PROOF STEP]
using i append_Cons_nth_left
[PROOF STATE]
proof (prove)
using this:
i < length Vs
?i < length ?xs \<Longrightarrow> (?xs @ ?u # ?ys) ! ?i = ?xs ! ?i

goal (1 subgoal):
 1. (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = Vs ! i
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = Vs ! i

goal (3 subgoals):
 1. i < length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 3. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = Vs ! i
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = Vs ! i
[PROOF STEP]
show ?goal
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = Vs ! i
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = Vs ! i

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
using Vs i lincomb_list_carrier M.r_zero
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = Vs ! i
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = Vs ! i
set Vs \<subseteq> carrier_vec n
i < length Vs
set ?vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list ?c ?vs \<in> carrier_vec n
?x \<in> carrier_vec n \<Longrightarrow> ?x + 0\<^sub>v n = ?x

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)

goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
assume i: "i = length Vs"
[PROOF STATE]
proof (state)
this:
i = length Vs

goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "lincomb_list (\<lambda>j. if i = j then 1 else 0) Vs = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
[PROOF STEP]
using snoc.IH[OF Vs] i
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = (if i < length Vs then Vs ! i else 0\<^sub>v n)
i = length Vs

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n

goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n

goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "(if i = length Vs then 1 else 0) \<cdot>\<^sub>v x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = x
[PROOF STEP]
using i x
[PROOF STATE]
proof (prove)
using this:
i = length Vs
x \<in> carrier_vec n

goal (1 subgoal):
 1. (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = x

goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = x

goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = x
[PROOF STEP]
using i append_Cons_nth_left
[PROOF STATE]
proof (prove)
using this:
i = length Vs
?i < length ?xs \<Longrightarrow> (?xs @ ?u # ?ys) ! ?i = ?xs ! ?i

goal (1 subgoal):
 1. (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = x

goal (2 subgoals):
 1. i = length Vs \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
 2. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = x
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = x
[PROOF STEP]
show ?goal
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = x
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = x

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = x
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = x
x \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)

goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
assume i: "i > length Vs"
[PROOF STATE]
proof (state)
this:
length Vs < i

goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "lincomb_list (\<lambda>j. if i = j then 1 else 0) Vs = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
[PROOF STEP]
using snoc.IH[OF Vs] i
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = (if i < length Vs then Vs ! i else 0\<^sub>v n)
length Vs < i

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n

goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n

goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "(if i = length Vs then 1 else 0) \<cdot>\<^sub>v x = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
[PROOF STEP]
using i x
[PROOF STATE]
proof (prove)
using this:
length Vs < i
x \<in> carrier_vec n

goal (1 subgoal):
 1. (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n

goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n

goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = 0\<^sub>v n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
length Vs < i

goal (1 subgoal):
 1. (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = 0\<^sub>v n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = 0\<^sub>v n

goal (1 subgoal):
 1. length Vs < i \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = 0\<^sub>v n
[PROOF STEP]
show ?goal
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = 0\<^sub>v n
(if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = 0\<^sub>v n
(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n) = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs + (if i = length Vs then 1::'a else (0::'a)) \<cdot>\<^sub>v x = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) [] = (if i < length [] then [] ! i else 0\<^sub>v n)
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) xs = (if i < length xs then xs ! i else 0\<^sub>v n); set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (xs @ [x]) = (if i < length (xs @ [x]) then (xs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (Vs @ [x]) = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (Vs @ [x]) = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (Vs @ [x]) = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) (Vs @ [x]) = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0\<^sub>v n)

goal (1 subgoal):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) [] = (if i < length [] then [] ! i else 0\<^sub>v n)
[PROOF STEP]
qed simp


[STATEMENT]
lemma set_in_convex_hull_list: fixes Vs :: "'a vec list"
  assumes "set Vs \<subseteq> carrier_vec n"
  shows "set Vs \<subseteq> convex_hull_list Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Vs \<subseteq> convex_hull_list Vs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
assume "x \<in> set Vs"
[PROOF STATE]
proof (state)
this:
x \<in> set Vs

goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set Vs
[PROOF STEP]
obtain i where i: "i < length Vs"
    and x: "x = Vs ! i"
[PROOF STATE]
proof (prove)
using this:
x \<in> set Vs

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
let ?f = "\<lambda> j. if i = j then 1 else 0 :: 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
have "lincomb_list ?f Vs = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = x
[PROOF STEP]
using i x lincomb_list_elem[OF assms]
[PROOF STATE]
proof (prove)
using this:
i < length Vs
x = Vs ! i
lincomb_list (\<lambda>j. if ?i = j then 1::'a else (0::'a)) Vs = (if ?i < length Vs then Vs ! ?i else 0\<^sub>v n)

goal (1 subgoal):
 1. lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = x

goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = x

goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
have "\<forall> j < length Vs. ?f j \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<length Vs. (0::'a) \<le> (if i = j then 1::'a else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j<length Vs. (0::'a) \<le> (if i = j then 1::'a else (0::'a))

goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j<length Vs. (0::'a) \<le> (if i = j then 1::'a else (0::'a))

goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
have "sum ?f {0..<length Vs} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<length Vs. if i = j then 1::'a else (0::'a)) = (1::'a)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length Vs

goal (1 subgoal):
 1. (\<Sum>j = 0..<length Vs. if i = j then 1::'a else (0::'a)) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<length Vs. if i = j then 1::'a else (0::'a)) = (1::'a)

goal (1 subgoal):
 1. \<And>x. x \<in> set Vs \<Longrightarrow> x \<in> convex_hull_list Vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = x
\<forall>j<length Vs. (0::'a) \<le> (if i = j then 1::'a else (0::'a))
(\<Sum>j = 0..<length Vs. if i = j then 1::'a else (0::'a)) = (1::'a)
[PROOF STEP]
show "x \<in> convex_hull_list Vs"
[PROOF STATE]
proof (prove)
using this:
lincomb_list (\<lambda>j. if i = j then 1::'a else (0::'a)) Vs = x
\<forall>j<length Vs. (0::'a) \<le> (if i = j then 1::'a else (0::'a))
(\<Sum>j = 0..<length Vs. if i = j then 1::'a else (0::'a)) = (1::'a)

goal (1 subgoal):
 1. x \<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>j. if i = j then 1::'a else (0::'a)) Vs = x
\<forall>j<length Vs. (0::'a) \<le> (if i = j then 1::'a else (0::'a))
(\<Sum>j = 0..<length Vs. if i = j then 1::'a else (0::'a)) = (1::'a)

goal (1 subgoal):
 1. 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)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull_list Vs

goal:
No subgoals!
[PROOF STEP]
qed