[STATEMENT]
lemma convex_improper:
  fixes f :: "'a::euclidean_space \<Rightarrow> ereal"
  assumes "convex_on UNIV f"
  assumes "~(proper f)"
  shows "\<forall>x\<in>rel_interior(domain f). f x = -\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
assume "domain f = {}"
[PROOF STATE]
proof (state)
this:
domain f = {}

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
domain f = {}

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
using rel_interior_empty
[PROOF STATE]
proof (prove)
using this:
domain f = {}
rel_interior {} = {}

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
domain f = {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domain f = {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
domain f = {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
assume nemp: "domain f \<noteq> {}"
[PROOF STATE]
proof (state)
this:
domain f \<noteq> {}

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
domain f \<noteq> {}
[PROOF STEP]
obtain u where u_def: "f u = -\<infinity>"
[PROOF STATE]
proof (prove)
using this:
domain f \<noteq> {}

goal (1 subgoal):
 1. (\<And>u. f u = - \<infinity> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms improper_iff[of f]
[PROOF STATE]
proof (prove)
using this:
domain f \<noteq> {}
Lower_Semicontinuous.convex_on UNIV f
\<not> proper f
(\<not> proper f) = ((\<exists>x. f x = - \<infinity>) \<or> (\<forall>x. f x = \<infinity>))

goal (1 subgoal):
 1. (\<And>u. f u = - \<infinity> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_def
[PROOF STATE]
proof (prove)
using this:
{x. f x < \<infinity>} \<noteq> {}
Lower_Semicontinuous.convex_on UNIV f
\<not> proper f
(\<not> proper f) = ((\<exists>x. f x = - \<infinity>) \<or> (\<forall>x. f x = \<infinity>))

goal (1 subgoal):
 1. (\<And>u. f u = - \<infinity> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f u = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
hence udom: "u:domain f"
[PROOF STATE]
proof (prove)
using this:
f u = - \<infinity>

goal (1 subgoal):
 1. u \<in> domain f
[PROOF STEP]
unfolding domain_def
[PROOF STATE]
proof (prove)
using this:
f u = - \<infinity>

goal (1 subgoal):
 1. u \<in> {x. f x < \<infinity>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> domain f

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
u \<in> domain f

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
assume "x:rel_interior(domain f)"
[PROOF STATE]
proof (state)
this:
x \<in> rel_interior (domain f)

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> rel_interior (domain f)
[PROOF STEP]
obtain m where m_def: "m>1 \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x : domain f"
[PROOF STATE]
proof (prove)
using this:
x \<in> rel_interior (domain f)

goal (1 subgoal):
 1. (\<And>m. 1 < m \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x \<in> domain f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using convex_rel_interior_iff[of "domain f" x] nemp convex_domain[of f] assms udom
[PROOF STATE]
proof (prove)
using this:
x \<in> rel_interior (domain f)
\<lbrakk>convex (domain f); domain f \<noteq> {}\<rbrakk> \<Longrightarrow> (x \<in> rel_interior (domain f)) = (\<forall>xa\<in>domain f. \<exists>e>1. (1 - e) *\<^sub>R xa + e *\<^sub>R x \<in> domain f)
domain f \<noteq> {}
Lower_Semicontinuous.convex_on UNIV f \<Longrightarrow> convex (domain f)
Lower_Semicontinuous.convex_on UNIV f
\<not> proper f
u \<in> domain f

goal (1 subgoal):
 1. (\<And>m. 1 < m \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x \<in> domain f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < m \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x \<in> domain f

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
define v where "v = 1/m"
[PROOF STATE]
proof (state)
this:
v = 1 / m

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
hence v01: "0<v \<and> v<1"
[PROOF STATE]
proof (prove)
using this:
v = 1 / m

goal (1 subgoal):
 1. 0 < v \<and> v < 1
[PROOF STEP]
using m_def
[PROOF STATE]
proof (prove)
using this:
v = 1 / m
1 < m \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x \<in> domain f

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

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
define y where "y = (1 - m) *\<^sub>R u + m *\<^sub>R x"
[PROOF STATE]
proof (state)
this:
y = (1 - m) *\<^sub>R u + m *\<^sub>R x

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
have "x = (1-v) *\<^sub>R u+v *\<^sub>R y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (1 - v) *\<^sub>R u + v *\<^sub>R y
[PROOF STEP]
unfolding v_def y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (1 - 1 / m) *\<^sub>R u + (1 / m) *\<^sub>R ((1 - m) *\<^sub>R u + m *\<^sub>R x)
[PROOF STEP]
using m_def
[PROOF STATE]
proof (prove)
using this:
1 < m \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x \<in> domain f

goal (1 subgoal):
 1. x = (1 - 1 / m) *\<^sub>R u + (1 / m) *\<^sub>R ((1 - m) *\<^sub>R u + m *\<^sub>R x)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
x = (1 - v) *\<^sub>R u + v *\<^sub>R y

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
hence "f x \<le> (1-ereal v) * f u+ereal v * f y"
[PROOF STATE]
proof (prove)
using this:
x = (1 - v) *\<^sub>R u + v *\<^sub>R y

goal (1 subgoal):
 1. f x \<le> (1 - ereal v) * f u + ereal v * f y
[PROOF STEP]
using convex_on_ereal_alt_mem[of "UNIV" f y u v] assms convex_UNIV v01
[PROOF STATE]
proof (prove)
using this:
x = (1 - v) *\<^sub>R u + v *\<^sub>R y
\<lbrakk>convex UNIV; Lower_Semicontinuous.convex_on UNIV f; y \<in> UNIV; u \<in> UNIV; 0 \<le> v; v \<le> 1\<rbrakk> \<Longrightarrow> f (v *\<^sub>R y + (1 - v) *\<^sub>R u) \<le> ereal v * f y + (1 - ereal v) * f u
Lower_Semicontinuous.convex_on UNIV f
\<not> proper f
convex UNIV
0 < v \<and> v < 1

goal (1 subgoal):
 1. f x \<le> (1 - ereal v) * f u + ereal v * f y
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
f x \<le> (1 - ereal v) * f u + ereal v * f y

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f x \<le> (1 - ereal v) * f u + ereal v * f y

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
have "f y < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f y < \<infinity>
[PROOF STEP]
using m_def y_def
[PROOF STATE]
proof (prove)
using this:
1 < m \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x \<in> domain f
y = (1 - m) *\<^sub>R u + m *\<^sub>R x

goal (1 subgoal):
 1. f y < \<infinity>
[PROOF STEP]
unfolding domain_def
[PROOF STATE]
proof (prove)
using this:
1 < m \<and> (1 - m) *\<^sub>R u + m *\<^sub>R x \<in> {x. f x < \<infinity>}
y = (1 - m) *\<^sub>R u + m *\<^sub>R x

goal (1 subgoal):
 1. f y < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f y < \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f y < \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
have *: "0 < 1 - ereal v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - ereal v
[PROOF STEP]
using v01
[PROOF STATE]
proof (prove)
using this:
0 < v \<and> v < 1

goal (1 subgoal):
 1. 0 < 1 - ereal v
[PROOF STEP]
by (metis diff_gt_0_iff_gt ereal_less(2) ereal_minus(1) one_ereal_def)
[PROOF STATE]
proof (state)
this:
0 < 1 - ereal v

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < 1 - ereal v

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
0 < 1 - ereal v
[PROOF STEP]
have "(1-ereal v) * f u = -\<infinity>"
[PROOF STATE]
proof (prove)
using this:
0 < 1 - ereal v

goal (1 subgoal):
 1. (1 - ereal v) * f u = - \<infinity>
[PROOF STEP]
using u_def
[PROOF STATE]
proof (prove)
using this:
0 < 1 - ereal v
f u = - \<infinity>

goal (1 subgoal):
 1. (1 - ereal v) * f u = - \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 - ereal v) * f u = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f x \<le> (1 - ereal v) * f u + ereal v * f y
f y < \<infinity>
0 < 1 - ereal v
(1 - ereal v) * f u = - \<infinity>
[PROOF STEP]
have "f x = -\<infinity>"
[PROOF STATE]
proof (prove)
using this:
f x \<le> (1 - ereal v) * f u + ereal v * f y
f y < \<infinity>
0 < 1 - ereal v
(1 - ereal v) * f u = - \<infinity>

goal (1 subgoal):
 1. f x = - \<infinity>
[PROOF STEP]
using v01
[PROOF STATE]
proof (prove)
using this:
f x \<le> (1 - ereal v) * f u + ereal v * f y
f y < \<infinity>
0 < 1 - ereal v
(1 - ereal v) * f u = - \<infinity>
0 < v \<and> v < 1

goal (1 subgoal):
 1. f x = - \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> rel_interior (domain f) \<Longrightarrow> f ?x2 = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> rel_interior (domain f) \<Longrightarrow> f ?x2 = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
domain f \<noteq> {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domain f = {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
domain f \<noteq> {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domain f = {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
domain f \<noteq> {} \<Longrightarrow> \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal (1 subgoal):
 1. \<forall>x\<in>rel_interior (domain f). f x = - \<infinity>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>rel_interior (domain f). f x = - \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_summaries: "finite {xs. distinct xs \<and> (\<forall>(l1, s, l2) \<in> set xs. s \<in>\<^sub>A weights l1 l2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {xs. distinct xs \<and> (\<forall>(l1, s, l2)\<in>set xs. s \<in>\<^sub>A weights l1 l2)}
[PROOF STEP]
apply (rule finite_subset[OF _ finite_distinct_bounded[of "((\<lambda>((l1,l2),s). (l1,s,l2)) ` (Sigma UNIV (\<lambda>(l1,l2). set_antichain (weights l1 l2))))"]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {xs. distinct xs \<and> (\<forall>(l1, s, l2)\<in>set xs. s \<in>\<^sub>A weights l1 l2)} \<subseteq> {xs. distinct xs \<and> set xs \<subseteq> (\<lambda>((l1, l2), s). (l1, s, l2)) ` (SIGMA (l1, l2):UNIV. set_antichain (weights l1 l2))}
 2. finite ((\<lambda>((l1, l2), s). (l1, s, l2)) ` (SIGMA (l1, l2):UNIV. set_antichain (weights l1 l2)))
[PROOF STEP]
apply (force simp: finite_set_summaries)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma discr0_coind[consumes 1, case_names Cont Term, induct pred: discr0]:
assumes *: "phi c" and
**: "\<And> c s c' s'.
       \<lbrakk>mustT c s; phi c; (c,s) \<rightarrow>c (c',s')\<rbrakk> \<Longrightarrow>
       s \<approx> s' \<and> (phi c' \<or> discr0 c')" and
***: "\<And> c s s'. \<lbrakk>mustT c s; phi c; (c,s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> s \<approx> s'"
shows "discr0 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. discr0 c
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
phi c

goal (1 subgoal):
 1. discr0 c
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi c \<Longrightarrow> discr0 c
[PROOF STEP]
apply(erule discr0.coinduct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. phi x \<Longrightarrow> \<exists>c. x = c \<and> (\<forall>x xa xb. mustT c x \<longrightarrow> (c, x) \<rightarrow>c (xa, xb) \<longrightarrow> x \<approx> xb \<and> (phi xa \<or> discr0 xa)) \<and> (\<forall>x xa. mustT c x \<longrightarrow> (c, x) \<rightarrow>t xa \<longrightarrow> x \<approx> xa)
[PROOF STEP]
using ** ***
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mustT ?c1 ?s1; phi ?c1; (?c1, ?s1) \<rightarrow>c (?c'1, ?s'1)\<rbrakk> \<Longrightarrow> ?s1 \<approx> ?s'1 \<and> (phi ?c'1 \<or> discr0 ?c'1)
\<lbrakk>mustT ?c1 ?s1; phi ?c1; (?c1, ?s1) \<rightarrow>t ?s'1\<rbrakk> \<Longrightarrow> ?s1 \<approx> ?s'1

goal (1 subgoal):
 1. \<And>x. phi x \<Longrightarrow> \<exists>c. x = c \<and> (\<forall>x xa xb. mustT c x \<longrightarrow> (c, x) \<rightarrow>c (xa, xb) \<longrightarrow> x \<approx> xb \<and> (phi xa \<or> discr0 xa)) \<and> (\<forall>x xa. mustT c x \<longrightarrow> (c, x) \<rightarrow>t xa \<longrightarrow> x \<approx> xa)
[PROOF STEP]
by auto