[STATEMENT]
lemma convex_hull_sum: assumes A: "A \<subseteq> carrier_vec n" and B: "B \<subseteq> carrier_vec n"
  shows "convex_hull (A + B) = convex_hull A + convex_hull B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull (A + B) = convex_hull A + convex_hull B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B
 2. convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)
[PROOF STEP]
note cA = convex_hull_carrier[OF A]
[PROOF STATE]
proof (state)
this:
convex_hull A \<subseteq> carrier_vec n

goal (2 subgoals):
 1. convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B
 2. convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)
[PROOF STEP]
note cB = convex_hull_carrier[OF B]
[PROOF STATE]
proof (state)
this:
convex_hull B \<subseteq> carrier_vec n

goal (2 subgoals):
 1. convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B
 2. convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)
[PROOF STEP]
have "convex (convex_hull A + convex_hull B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex (convex_hull A + convex_hull B)
[PROOF STEP]
proof (intro convexI sum_carrier_vec convex_hull_carrier A B)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
fix a :: 'a and x1 x2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
assume "x1 \<in> convex_hull A + convex_hull B" "x2 \<in> convex_hull A + convex_hull B"
[PROOF STATE]
proof (state)
this:
x1 \<in> convex_hull A + convex_hull B
x2 \<in> convex_hull A + convex_hull B

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> convex_hull A + convex_hull B
x2 \<in> convex_hull A + convex_hull B
[PROOF STEP]
obtain y1 y2 z1 z2 where
      x12: "x1 = y1 + z1" "x2 = y2 + z2" and
      y12: "y1 \<in> convex_hull A" "y2 \<in> convex_hull A" and
      z12: "z1 \<in> convex_hull B" "z2 \<in> convex_hull B"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> convex_hull A + convex_hull B
x2 \<in> convex_hull A + convex_hull B

goal (1 subgoal):
 1. (\<And>y1 z1 y2 z2. \<lbrakk>x1 = y1 + z1; x2 = y2 + z2; y1 \<in> convex_hull A; y2 \<in> convex_hull A; z1 \<in> convex_hull B; z2 \<in> convex_hull B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_plus_def
[PROOF STATE]
proof (prove)
using this:
x1 \<in> {c. \<exists>a\<in>convex_hull A. \<exists>b\<in>convex_hull B. c = a + b}
x2 \<in> {c. \<exists>a\<in>convex_hull A. \<exists>b\<in>convex_hull B. c = a + b}

goal (1 subgoal):
 1. (\<And>y1 z1 y2 z2. \<lbrakk>x1 = y1 + z1; x2 = y2 + z2; y1 \<in> convex_hull A; y2 \<in> convex_hull A; z1 \<in> convex_hull B; z2 \<in> convex_hull B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 = y1 + z1
x2 = y2 + z2
y1 \<in> convex_hull A
y2 \<in> convex_hull A
z1 \<in> convex_hull B
z2 \<in> convex_hull B

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
from y12 z12 cA cB
[PROOF STATE]
proof (chain)
picking this:
y1 \<in> convex_hull A
y2 \<in> convex_hull A
z1 \<in> convex_hull B
z2 \<in> convex_hull B
convex_hull A \<subseteq> carrier_vec n
convex_hull B \<subseteq> carrier_vec n
[PROOF STEP]
have carr:
      "y1 \<in> carrier_vec n" "y2 \<in> carrier_vec n"
      "z1 \<in> carrier_vec n" "z2 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
y1 \<in> convex_hull A
y2 \<in> convex_hull A
z1 \<in> convex_hull B
z2 \<in> convex_hull B
convex_hull A \<subseteq> carrier_vec n
convex_hull B \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (y1 \<in> carrier_vec n &&& y2 \<in> carrier_vec n) &&& z1 \<in> carrier_vec n &&& z2 \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
z1 \<in> carrier_vec n
z2 \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
assume a: "0 \<le> a" "a \<le> 1"
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a
a \<le> (1::'a)

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
have A: "a \<cdot>\<^sub>v y1 + (1 - a) \<cdot>\<^sub>v y2 \<in> convex_hull A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 \<in> convex_hull A
[PROOF STEP]
using y12 a A
[PROOF STATE]
proof (prove)
using this:
y1 \<in> convex_hull A
y2 \<in> convex_hull A
(0::'a) \<le> a
a \<le> (1::'a)
A \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
have B: "a \<cdot>\<^sub>v z1 + (1 - a) \<cdot>\<^sub>v z2 \<in> convex_hull B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2 \<in> convex_hull B
[PROOF STEP]
using z12 a B
[PROOF STATE]
proof (prove)
using this:
z1 \<in> convex_hull B
z2 \<in> convex_hull B
(0::'a) \<le> a
a \<le> (1::'a)
B \<subseteq> carrier_vec n

goal (1 subgoal):
 1. a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2 \<in> convex_hull B
[PROOF STEP]
by (metis convex_hull_convex_sum)
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2 \<in> convex_hull B

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
have "a \<cdot>\<^sub>v x1 + (1 - a) \<cdot>\<^sub>v x2 = (a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1) + ((1 - a) \<cdot>\<^sub>v y2 + (1 - a) \<cdot>\<^sub>v z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v x1 + ((1::'a) - a) \<cdot>\<^sub>v x2 = a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2)
[PROOF STEP]
unfolding x12
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v (y1 + z1) + ((1::'a) - a) \<cdot>\<^sub>v (y2 + z2) = a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2)
[PROOF STEP]
using carr
[PROOF STATE]
proof (prove)
using this:
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
z1 \<in> carrier_vec n
z2 \<in> carrier_vec n

goal (1 subgoal):
 1. a \<cdot>\<^sub>v (y1 + z1) + ((1::'a) - a) \<cdot>\<^sub>v (y2 + z2) = a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2)
[PROOF STEP]
by (auto simp: smult_add_distrib_vec)
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v x1 + ((1::'a) - a) \<cdot>\<^sub>v x2 = a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2)

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v x1 + ((1::'a) - a) \<cdot>\<^sub>v x2 = a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2)

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
have "\<dots> = (a \<cdot>\<^sub>v y1 + (1 - a) \<cdot>\<^sub>v y2) + (a \<cdot>\<^sub>v z1 + (1 - a) \<cdot>\<^sub>v z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2) = a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 + (a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2)
[PROOF STEP]
using carr
[PROOF STATE]
proof (prove)
using this:
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
z1 \<in> carrier_vec n
z2 \<in> carrier_vec n

goal (1 subgoal):
 1. a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2) = a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 + (a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2)
[PROOF STEP]
by (intro eq_vecI, auto)
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v y1 + a \<cdot>\<^sub>v z1 + (((1::'a) - a) \<cdot>\<^sub>v y2 + ((1::'a) - a) \<cdot>\<^sub>v z2) = a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 + (a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2)

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>x \<in> convex_hull A + convex_hull B; y \<in> convex_hull A + convex_hull B; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x + ((1::'a) - a) \<cdot>\<^sub>v y \<in> convex_hull A + convex_hull B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a \<cdot>\<^sub>v x1 + ((1::'a) - a) \<cdot>\<^sub>v x2 = a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 + (a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2)
[PROOF STEP]
show "a \<cdot>\<^sub>v x1 + (1 - a) \<cdot>\<^sub>v x2 \<in> convex_hull A + convex_hull B"
[PROOF STATE]
proof (prove)
using this:
a \<cdot>\<^sub>v x1 + ((1::'a) - a) \<cdot>\<^sub>v x2 = a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 + (a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2)

goal (1 subgoal):
 1. a \<cdot>\<^sub>v x1 + ((1::'a) - a) \<cdot>\<^sub>v x2 \<in> convex_hull A + convex_hull B
[PROOF STEP]
using A B
[PROOF STATE]
proof (prove)
using this:
a \<cdot>\<^sub>v x1 + ((1::'a) - a) \<cdot>\<^sub>v x2 = a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 + (a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2)
a \<cdot>\<^sub>v y1 + ((1::'a) - a) \<cdot>\<^sub>v y2 \<in> convex_hull A
a \<cdot>\<^sub>v z1 + ((1::'a) - a) \<cdot>\<^sub>v z2 \<in> convex_hull B

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
convex (convex_hull A + convex_hull B)

goal (2 subgoals):
 1. convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B
 2. convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)
[PROOF STEP]
from convex_convex_hull[OF this]
[PROOF STATE]
proof (chain)
picking this:
convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B
[PROOF STEP]
have id: "convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B"
[PROOF STATE]
proof (prove)
using this:
convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B

goal (1 subgoal):
 1. convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B

goal (2 subgoals):
 1. convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B
 2. convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)
[PROOF STEP]
show "convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B
[PROOF STEP]
by (subst id[symmetric], rule convex_hull_mono[OF set_plus_mono2]; intro set_in_convex_hull A B)
[PROOF STATE]
proof (state)
this:
convex_hull (A + B) \<subseteq> convex_hull A + convex_hull B

goal (1 subgoal):
 1. convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)
[PROOF STEP]
show "convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
assume "x \<in> convex_hull A + convex_hull B"
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull A + convex_hull B

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> convex_hull A + convex_hull B
[PROOF STEP]
obtain y z where x: "x = y + z" and y: "y \<in> convex_hull A" and z: "z \<in> convex_hull B"
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull A + convex_hull B

goal (1 subgoal):
 1. (\<And>y z. \<lbrakk>x = y + z; y \<in> convex_hull A; z \<in> convex_hull B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: set_plus_def)
[PROOF STATE]
proof (state)
this:
x = y + z
y \<in> convex_hull A
z \<in> convex_hull B

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from convex_hull_convex_hull_listD[OF A y]
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. set as \<subseteq> A \<and> y \<in> convex_hull_list as
[PROOF STEP]
obtain ys where ysA: "set ys \<subseteq> A" and
      y: "y \<in> convex_hull_list ys"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. set as \<subseteq> A \<and> y \<in> convex_hull_list as

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from convex_hull_convex_hull_listD[OF B z]
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. set as \<subseteq> B \<and> z \<in> convex_hull_list as
[PROOF STEP]
obtain zs where zsB: "set zs \<subseteq> B" and
      z: "z \<in> convex_hull_list zs"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. set as \<subseteq> B \<and> z \<in> convex_hull_list as

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from y[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def]
[PROOF STATE]
proof (chain)
picking this:
y \<in> {x. \<exists>c. (lincomb_list c ys = x \<and> (\<forall>i<length ys. (0::'a) \<le> c i)) \<and> sum c {0..<length ys} = (1::'a)}
[PROOF STEP]
obtain c where yid: "y = lincomb_list c ys"
      and conv_c: "(\<forall>i<length ys. 0 \<le> c i) \<and> sum c {0..<length ys} = 1"
[PROOF STATE]
proof (prove)
using this:
y \<in> {x. \<exists>c. (lincomb_list c ys = x \<and> (\<forall>i<length ys. (0::'a) \<le> c i)) \<and> sum c {0..<length ys} = (1::'a)}

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from z[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def]
[PROOF STATE]
proof (chain)
picking this:
z \<in> {x. \<exists>c. (lincomb_list c zs = x \<and> (\<forall>i<length zs. (0::'a) \<le> c i)) \<and> sum c {0..<length zs} = (1::'a)}
[PROOF STEP]
obtain d where zid: "z = lincomb_list d zs"
      and conv_d: "(\<forall>i<length zs. 0 \<le> d i) \<and> sum d {0..<length zs} = 1"
[PROOF STATE]
proof (prove)
using this:
z \<in> {x. \<exists>c. (lincomb_list c zs = x \<and> (\<forall>i<length zs. (0::'a) \<le> c i)) \<and> sum c {0..<length zs} = (1::'a)}

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from ysA A
[PROOF STATE]
proof (chain)
picking this:
set ys \<subseteq> A
A \<subseteq> carrier_vec n
[PROOF STEP]
have ys: "set ys \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> A
A \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from zsB B
[PROOF STATE]
proof (chain)
picking this:
set zs \<subseteq> B
B \<subseteq> carrier_vec n
[PROOF STEP]
have zs: "set zs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set zs \<subseteq> B
B \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have [intro, simp]: "lincomb_list x ys \<in> carrier_vec n" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list x ys \<in> carrier_vec n
[PROOF STEP]
using lincomb_list_carrier[OF ys]
[PROOF STATE]
proof (prove)
using this:
lincomb_list ?c ys \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb_list x ys \<in> carrier_vec n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb_list ?x3 ys \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have [intro, simp]: "lincomb_list x zs \<in> carrier_vec n" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list x zs \<in> carrier_vec n
[PROOF STEP]
using lincomb_list_carrier[OF zs]
[PROOF STATE]
proof (prove)
using this:
lincomb_list ?c zs \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb_list x zs \<in> carrier_vec n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb_list ?x3 zs \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have dim[simp]: "dim_vec (lincomb_list d zs) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (lincomb_list d zs) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (lincomb_list d zs) = n

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from yid
[PROOF STATE]
proof (chain)
picking this:
y = lincomb_list c ys
[PROOF STEP]
have y: "y \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
y = lincomb_list c ys

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
from zid
[PROOF STATE]
proof (chain)
picking this:
z = lincomb_list d zs
[PROOF STEP]
have z: "z \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
z = lincomb_list d zs

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
z \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
assume "x \<in> set (map ((+) y) zs)"
[PROOF STATE]
proof (state)
this:
x \<in> set (map ((+) y) zs)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (map ((+) y) zs)
[PROOF STEP]
obtain z where "x = y + z" and "z \<in> set zs"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (map ((+) y) zs)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>x = y + z; z \<in> set zs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y + z
z \<in> set zs

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y + z
z \<in> set zs
[PROOF STEP]
obtain j where j: "j < length zs" and x: "x = y + zs ! j"
[PROOF STATE]
proof (prove)
using this:
x = y + z
z \<in> set zs

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j < length zs; x = y + zs ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
x = y + z
z \<in> {zs ! i |i. i < length zs}

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
hence mem: "zs ! j \<in> set zs"
[PROOF STATE]
proof (prove)
using this:
j < length zs
x = y + zs ! j

goal (1 subgoal):
 1. zs ! j \<in> set zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zs ! j \<in> set zs

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
hence zsj: "zs ! j \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
zs ! j \<in> set zs

goal (1 subgoal):
 1. zs ! j \<in> carrier_vec n
[PROOF STEP]
using zs
[PROOF STATE]
proof (prove)
using this:
zs ! j \<in> set zs
set zs \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
let ?list = "(map (\<lambda> y. y + zs ! j) ys)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
let ?set = "set ?list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have set: "?set \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>y. y + zs ! j) ys) \<subseteq> carrier_vec n
[PROOF STEP]
using ys A zsj
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> carrier_vec n
A \<subseteq> carrier_vec n
zs ! j \<in> carrier_vec n

goal (1 subgoal):
 1. set (map (\<lambda>y. y + zs ! j) ys) \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map (\<lambda>y. y + zs ! j) ys) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have lin_map: "lincomb_list c ?list \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list c (map (\<lambda>y. y + zs ! j) ys) \<in> carrier_vec n
[PROOF STEP]
by (intro lincomb_list_carrier[OF set])
[PROOF STATE]
proof (state)
this:
lincomb_list c (map (\<lambda>y. y + zs ! j) ys) \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have "y + (zs ! j) = lincomb_list c ?list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + zs ! j = lincomb_list c (map (\<lambda>y. y + zs ! j) ys)
[PROOF STEP]
unfolding yid
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list c ys + zs ! j = lincomb_list c (map (\<lambda>y. y + zs ! j) ys)
[PROOF STEP]
using zsj lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ ys]
[PROOF STATE]
proof (prove)
using this:
zs ! j \<in> carrier_vec n
lincomb_list c (map (\<lambda>y. y + zs ! j) ys) \<in> carrier_vec n
?i < n \<Longrightarrow> lincomb_list ?c (map (\<lambda>y. y + zs ! j) ys) $ ?i = (\<Sum>ja = 0..<length (map (\<lambda>y. y + zs ! j) ys). ?c ja * map (\<lambda>y. y + zs ! j) ys ! ja $ ?i)
?i < n \<Longrightarrow> lincomb_list ?c ys $ ?i = (\<Sum>j = 0..<length ys. ?c j * ys ! j $ ?i)

goal (1 subgoal):
 1. lincomb_list c ys + zs ! j = lincomb_list c (map (\<lambda>y. y + zs ! j) ys)
[PROOF STEP]
by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_c)
[PROOF STATE]
proof (state)
this:
y + zs ! j = lincomb_list c (map (\<lambda>y. y + zs ! j) ys)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
hence "convex_lincomb_list c ?list (y + (zs ! j))"
[PROOF STATE]
proof (prove)
using this:
y + zs ! j = lincomb_list c (map (\<lambda>y. y + zs ! j) ys)

goal (1 subgoal):
 1. convex_lincomb_list c (map (\<lambda>y. y + zs ! j) ys) (y + zs ! j)
[PROOF STEP]
unfolding convex_lincomb_list_def nonneg_lincomb_list_def
[PROOF STATE]
proof (prove)
using this:
y + zs ! j = lincomb_list c (map (\<lambda>y. y + zs ! j) ys)

goal (1 subgoal):
 1. (lincomb_list c (map (\<lambda>y. y + zs ! j) ys) = y + zs ! j \<and> (\<forall>i<length (map (\<lambda>y. y + zs ! j) ys). (0::'a) \<le> c i)) \<and> sum c {0..<length (map (\<lambda>y. y + zs ! j) ys)} = (1::'a)
[PROOF STEP]
using conv_c
[PROOF STATE]
proof (prove)
using this:
y + zs ! j = lincomb_list c (map (\<lambda>y. y + zs ! j) ys)
(\<forall>i<length ys. (0::'a) \<le> c i) \<and> sum c {0..<length ys} = (1::'a)

goal (1 subgoal):
 1. (lincomb_list c (map (\<lambda>y. y + zs ! j) ys) = y + zs ! j \<and> (\<forall>i<length (map (\<lambda>y. y + zs ! j) ys). (0::'a) \<le> c i)) \<and> sum c {0..<length (map (\<lambda>y. y + zs ! j) ys)} = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
convex_lincomb_list c (map (\<lambda>y. y + zs ! j) ys) (y + zs ! j)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
hence "y + (zs ! j) \<in> convex_hull_list ?list"
[PROOF STATE]
proof (prove)
using this:
convex_lincomb_list c (map (\<lambda>y. y + zs ! j) ys) (y + zs ! j)

goal (1 subgoal):
 1. y + zs ! j \<in> convex_hull_list (map (\<lambda>y. y + zs ! j) ys)
[PROOF STEP]
unfolding convex_hull_list_def
[PROOF STATE]
proof (prove)
using this:
convex_lincomb_list c (map (\<lambda>y. y + zs ! j) ys) (y + zs ! j)

goal (1 subgoal):
 1. y + zs ! j \<in> {x. \<exists>c. convex_lincomb_list c (map (\<lambda>y. y + zs ! j) ys) x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + zs ! j \<in> convex_hull_list (map (\<lambda>y. y + zs ! j) ys)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
with finite_convex_hull_iff_convex_hull_list[OF set refl]
[PROOF STATE]
proof (chain)
picking this:
convex_hull (set (map (\<lambda>y. y + zs ! j) ys)) = convex_hull_list (map (\<lambda>y. y + zs ! j) ys)
y + zs ! j \<in> convex_hull_list (map (\<lambda>y. y + zs ! j) ys)
[PROOF STEP]
have "(y + zs ! j) \<in> convex_hull ?set"
[PROOF STATE]
proof (prove)
using this:
convex_hull (set (map (\<lambda>y. y + zs ! j) ys)) = convex_hull_list (map (\<lambda>y. y + zs ! j) ys)
y + zs ! j \<in> convex_hull_list (map (\<lambda>y. y + zs ! j) ys)

goal (1 subgoal):
 1. y + zs ! j \<in> convex_hull (set (map (\<lambda>y. y + zs ! j) ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + zs ! j \<in> convex_hull (set (map (\<lambda>y. y + zs ! j) ys))

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y + zs ! j \<in> convex_hull (set (map (\<lambda>y. y + zs ! j) ys))

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have "\<dots> \<subseteq> convex_hull (A + B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull (set (map (\<lambda>y. y + zs ! j) ys)) \<subseteq> convex_hull (A + B)
[PROOF STEP]
by (rule convex_hull_mono, insert mem ys ysA zsB, force simp: set_plus_def)
[PROOF STATE]
proof (state)
this:
convex_hull (set (map (\<lambda>y. y + zs ! j) ys)) \<subseteq> convex_hull (A + B)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y + zs ! j \<in> convex_hull (A + B)
[PROOF STEP]
have "x \<in> convex_hull (A + B)"
[PROOF STATE]
proof (prove)
using this:
y + zs ! j \<in> convex_hull (A + B)

goal (1 subgoal):
 1. x \<in> convex_hull (A + B)
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
y + zs ! j \<in> convex_hull (A + B)

goal (1 subgoal):
 1. y + zs ! j \<in> convex_hull (A + B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull (A + B)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?xa5 \<in> set (map ((+) y) zs) \<Longrightarrow> ?xa5 \<in> convex_hull (A + B)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
note step1 = this
[PROOF STATE]
proof (state)
this:
?xa5 \<in> set (map ((+) y) zs) \<Longrightarrow> ?xa5 \<in> convex_hull (A + B)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?xa5 \<in> set (map ((+) y) zs) \<Longrightarrow> ?xa5 \<in> convex_hull (A + B)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
let ?list = "map ((+) y) zs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
let ?set = "set ?list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have set: "?set \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map ((+) y) zs) \<subseteq> carrier_vec n
[PROOF STEP]
using zs B y
[PROOF STATE]
proof (prove)
using this:
set zs \<subseteq> carrier_vec n
B \<subseteq> carrier_vec n
y \<in> carrier_vec n

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have lin_map: "lincomb_list d ?list \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list d (map ((+) y) zs) \<in> carrier_vec n
[PROOF STEP]
by (intro lincomb_list_carrier[OF set])
[PROOF STATE]
proof (state)
this:
lincomb_list d (map ((+) y) zs) \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have [simp]: "i < n \<Longrightarrow> (\<Sum>j = 0..<length zs. d j * (y + zs ! j) $ i) =
        (\<Sum>j = 0..<length zs. d j * (y $ i + zs ! j $ i))" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> (\<Sum>j = 0..<length zs. d j * (y + zs ! j) $ i) = (\<Sum>j = 0..<length zs. d j * (y $ i + zs ! j $ i))
[PROOF STEP]
by (rule sum.cong, insert zs[unfolded set_conv_nth] y, auto)
[PROOF STATE]
proof (state)
this:
?i3 < n \<Longrightarrow> (\<Sum>j = 0..<length zs. d j * (y + zs ! j) $ ?i3) = (\<Sum>j = 0..<length zs. d j * (y $ ?i3 + zs ! j $ ?i3))

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have "y + z = lincomb_list d ?list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + z = lincomb_list d (map ((+) y) zs)
[PROOF STEP]
unfolding zid
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + lincomb_list d zs = lincomb_list d (map ((+) y) zs)
[PROOF STEP]
using y zs lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ zs]
          set lincomb_list_carrier[OF zs, of d] zs[unfolded set_conv_nth]
[PROOF STATE]
proof (prove)
using this:
y \<in> carrier_vec n
set zs \<subseteq> carrier_vec n
lincomb_list d (map ((+) y) zs) \<in> carrier_vec n
?i < n \<Longrightarrow> lincomb_list ?c (map ((+) y) zs) $ ?i = (\<Sum>j = 0..<length (map ((+) y) zs). ?c j * map ((+) y) zs ! j $ ?i)
?i < n \<Longrightarrow> lincomb_list ?c zs $ ?i = (\<Sum>j = 0..<length zs. ?c j * zs ! j $ ?i)
set (map ((+) y) zs) \<subseteq> carrier_vec n
lincomb_list d zs \<in> carrier_vec n
{zs ! i |i. i < length zs} \<subseteq> carrier_vec n

goal (1 subgoal):
 1. y + lincomb_list d zs = lincomb_list d (map ((+) y) zs)
[PROOF STEP]
by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_d)
[PROOF STATE]
proof (state)
this:
y + z = lincomb_list d (map ((+) y) zs)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
hence "convex_lincomb_list d ?list x"
[PROOF STATE]
proof (prove)
using this:
y + z = lincomb_list d (map ((+) y) zs)

goal (1 subgoal):
 1. convex_lincomb_list d (map ((+) y) zs) x
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
y + z = lincomb_list d (map ((+) y) zs)

goal (1 subgoal):
 1. convex_lincomb_list d (map ((+) y) zs) (y + z)
[PROOF STEP]
unfolding convex_lincomb_list_def nonneg_lincomb_list_def
[PROOF STATE]
proof (prove)
using this:
y + z = lincomb_list d (map ((+) y) zs)

goal (1 subgoal):
 1. (lincomb_list d (map ((+) y) zs) = y + z \<and> (\<forall>i<length (map ((+) y) zs). (0::'a) \<le> d i)) \<and> sum d {0..<length (map ((+) y) zs)} = (1::'a)
[PROOF STEP]
using conv_d
[PROOF STATE]
proof (prove)
using this:
y + z = lincomb_list d (map ((+) y) zs)
(\<forall>i<length zs. (0::'a) \<le> d i) \<and> sum d {0..<length zs} = (1::'a)

goal (1 subgoal):
 1. (lincomb_list d (map ((+) y) zs) = y + z \<and> (\<forall>i<length (map ((+) y) zs). (0::'a) \<le> d i)) \<and> sum d {0..<length (map ((+) y) zs)} = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
convex_lincomb_list d (map ((+) y) zs) x

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
hence "x \<in> convex_hull_list ?list"
[PROOF STATE]
proof (prove)
using this:
convex_lincomb_list d (map ((+) y) zs) x

goal (1 subgoal):
 1. x \<in> convex_hull_list (map ((+) y) zs)
[PROOF STEP]
unfolding convex_hull_list_def
[PROOF STATE]
proof (prove)
using this:
convex_lincomb_list d (map ((+) y) zs) x

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

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
with finite_convex_hull_iff_convex_hull_list[OF set refl]
[PROOF STATE]
proof (chain)
picking this:
convex_hull (set (map ((+) y) zs)) = convex_hull_list (map ((+) y) zs)
x \<in> convex_hull_list (map ((+) y) zs)
[PROOF STEP]
have "x \<in> convex_hull ?set"
[PROOF STATE]
proof (prove)
using this:
convex_hull (set (map ((+) y) zs)) = convex_hull_list (map ((+) y) zs)
x \<in> convex_hull_list (map ((+) y) zs)

goal (1 subgoal):
 1. x \<in> convex_hull (set (map ((+) y) zs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull (set (map ((+) y) zs))

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull (set (map ((+) y) zs))

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have "\<dots> \<subseteq> convex_hull (convex_hull (A + B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull (set (map ((+) y) zs)) \<subseteq> convex_hull (convex_hull (A + B))
[PROOF STEP]
by (rule convex_hull_mono, insert step1, auto)
[PROOF STATE]
proof (state)
this:
convex_hull (set (map ((+) y) zs)) \<subseteq> convex_hull (convex_hull (A + B))

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
convex_hull (set (map ((+) y) zs)) \<subseteq> convex_hull (convex_hull (A + B))

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
have "\<dots> = convex_hull (A + B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull (convex_hull (A + B)) = convex_hull (A + B)
[PROOF STEP]
by (rule convex_convex_hull[OF convex_hulls_are_convex], intro sum_carrier_vec A B)
[PROOF STATE]
proof (state)
this:
convex_hull (convex_hull (A + B)) = convex_hull (A + B)

goal (1 subgoal):
 1. \<And>x. x \<in> convex_hull A + convex_hull B \<Longrightarrow> x \<in> convex_hull (A + B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> convex_hull (A + B)
[PROOF STEP]
show "x \<in> convex_hull (A + B)"
[PROOF STATE]
proof (prove)
using this:
x \<in> convex_hull (A + B)

goal (1 subgoal):
 1. x \<in> convex_hull (A + B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull (A + B)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull (A + B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
convex_hull A + convex_hull B \<subseteq> convex_hull (A + B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_hull_in_cone:
  "convex_hull C \<subseteq> cone C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull C \<subseteq> cone C
[PROOF STEP]
unfolding convex_hull_def cone_def convex_lincomb_def finite_cone_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>Ws c. finite Ws \<and> Ws \<subseteq> C \<and> nonneg_lincomb c Ws x \<and> sum c Ws = (1::'a)} \<subseteq> {x. \<exists>Ws. finite Ws \<and> Ws \<subseteq> C \<and> x \<in> {b. \<exists>c. nonneg_lincomb c (if finite Ws then Ws else {}) b}}
[PROOF STEP]
by auto


[STATEMENT]
lemma convex_cone:
  assumes C: "C \<subseteq> carrier_vec n"
  shows "convex (cone C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex (cone C)
[PROOF STEP]
unfolding convex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex_hull (cone C) = cone C
[PROOF STEP]
using convex_hull_in_cone set_in_convex_hull[OF cone_carrier[OF C]] cone_cone[OF C]
[PROOF STATE]
proof (prove)
using this:
convex_hull ?C \<subseteq> cone ?C
cone C \<subseteq> convex_hull (cone C)
cone (cone C) = cone C

goal (1 subgoal):
 1. convex_hull (cone C) = cone C
[PROOF STEP]
by blast


[STATEMENT]
lemma free_tv_subst:
  "free_tv S = (dom S) Un (cod S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv S = Type.dom S \<union> cod S
[PROOF STEP]
by (simp add: free_tv_fun_def of_nat_nat_def typ_of_typ_def )

\<comment> \<open>unification algorithm mgu\<close>


[STATEMENT]
lemma mk_scheme_Fun:
  "mk_scheme t = sch1 =-> sch2 \<Longrightarrow> (\<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_scheme t = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. mk_scheme (TVar x) = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
 2. \<And>t1 t2. \<lbrakk>mk_scheme t1 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme t2 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme (t1 -> t2) = sch1 =-> sch2\<rbrakk> \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
case TVar
[PROOF STATE]
proof (state)
this:
mk_scheme (TVar x_) = sch1 =-> sch2

goal (2 subgoals):
 1. \<And>x. mk_scheme (TVar x) = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
 2. \<And>t1 t2. \<lbrakk>mk_scheme t1 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme t2 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme (t1 -> t2) = sch1 =-> sch2\<rbrakk> \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
mk_scheme (TVar x_) = sch1 =-> sch2

goal (1 subgoal):
 1. \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>mk_scheme t1 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme t2 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme (t1 -> t2) = sch1 =-> sch2\<rbrakk> \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>mk_scheme t1 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme t2 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme (t1 -> t2) = sch1 =-> sch2\<rbrakk> \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
case Fun
[PROOF STATE]
proof (state)
this:
mk_scheme t1_ = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
mk_scheme t2_ = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
mk_scheme (t1_ -> t2_) = sch1 =-> sch2

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>mk_scheme t1 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme t2 = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2; mk_scheme (t1 -> t2) = sch1 =-> sch2\<rbrakk> \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
mk_scheme t1_ = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
mk_scheme t2_ = sch1 =-> sch2 \<Longrightarrow> \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
mk_scheme (t1_ -> t2_) = sch1 =-> sch2

goal (1 subgoal):
 1. \<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t1 t2. sch1 = mk_scheme t1 \<and> sch2 = mk_scheme t2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mk_scheme_injective: "(mk_scheme t = mk_scheme t') \<Longrightarrow> t = t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_scheme t = mk_scheme t' \<Longrightarrow> t = t'
[PROOF STEP]
proof (induction t arbitrary: t')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x t'. mk_scheme (TVar x) = mk_scheme t' \<Longrightarrow> TVar x = t'
 2. \<And>t1 t2 t'. \<lbrakk>\<And>t'. mk_scheme t1 = mk_scheme t' \<Longrightarrow> t1 = t'; \<And>t'. mk_scheme t2 = mk_scheme t' \<Longrightarrow> t2 = t'; mk_scheme (t1 -> t2) = mk_scheme t'\<rbrakk> \<Longrightarrow> t1 -> t2 = t'
[PROOF STEP]
case TVar
[PROOF STATE]
proof (state)
this:
mk_scheme (TVar x_) = mk_scheme t'

goal (2 subgoals):
 1. \<And>x t'. mk_scheme (TVar x) = mk_scheme t' \<Longrightarrow> TVar x = t'
 2. \<And>t1 t2 t'. \<lbrakk>\<And>t'. mk_scheme t1 = mk_scheme t' \<Longrightarrow> t1 = t'; \<And>t'. mk_scheme t2 = mk_scheme t' \<Longrightarrow> t2 = t'; mk_scheme (t1 -> t2) = mk_scheme t'\<rbrakk> \<Longrightarrow> t1 -> t2 = t'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
mk_scheme (TVar x_) = mk_scheme t'

goal (1 subgoal):
 1. TVar x_ = t'
[PROOF STEP]
by(cases t') auto
[PROOF STATE]
proof (state)
this:
TVar x_ = t'

goal (1 subgoal):
 1. \<And>t1 t2 t'. \<lbrakk>\<And>t'. mk_scheme t1 = mk_scheme t' \<Longrightarrow> t1 = t'; \<And>t'. mk_scheme t2 = mk_scheme t' \<Longrightarrow> t2 = t'; mk_scheme (t1 -> t2) = mk_scheme t'\<rbrakk> \<Longrightarrow> t1 -> t2 = t'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2 t'. \<lbrakk>\<And>t'. mk_scheme t1 = mk_scheme t' \<Longrightarrow> t1 = t'; \<And>t'. mk_scheme t2 = mk_scheme t' \<Longrightarrow> t2 = t'; mk_scheme (t1 -> t2) = mk_scheme t'\<rbrakk> \<Longrightarrow> t1 -> t2 = t'
[PROOF STEP]
case Fun
[PROOF STATE]
proof (state)
this:
mk_scheme t1_ = mk_scheme ?t' \<Longrightarrow> t1_ = ?t'
mk_scheme t2_ = mk_scheme ?t' \<Longrightarrow> t2_ = ?t'
mk_scheme (t1_ -> t2_) = mk_scheme t'

goal (1 subgoal):
 1. \<And>t1 t2 t'. \<lbrakk>\<And>t'. mk_scheme t1 = mk_scheme t' \<Longrightarrow> t1 = t'; \<And>t'. mk_scheme t2 = mk_scheme t' \<Longrightarrow> t2 = t'; mk_scheme (t1 -> t2) = mk_scheme t'\<rbrakk> \<Longrightarrow> t1 -> t2 = t'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
mk_scheme t1_ = mk_scheme ?t' \<Longrightarrow> t1_ = ?t'
mk_scheme t2_ = mk_scheme ?t' \<Longrightarrow> t2_ = ?t'
mk_scheme (t1_ -> t2_) = mk_scheme t'

goal (1 subgoal):
 1. t1_ -> t2_ = t'
[PROOF STEP]
by(cases t') auto
[PROOF STATE]
proof (state)
this:
t1_ -> t2_ = t'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma free_tv_mk_scheme[simp]: "free_tv (mk_scheme t) = free_tv t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv (mk_scheme t) = free_tv t
[PROOF STEP]
by (induction t) auto


[STATEMENT]
lemma subst_mk_scheme[simp]: "$ S (mk_scheme t) = mk_scheme ($ S t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ S (mk_scheme t) = mk_scheme ($ S t)
[PROOF STEP]
by (induction t) auto

\<comment> \<open>constructor laws for @{text app_subst}\<close>


[STATEMENT]
lemma app_subst_Nil[simp]:
  "$ S [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ S [] = []
[PROOF STEP]
by (simp add: app_subst_list)


[STATEMENT]
lemma app_subst_Cons[simp]:
  "$ S (x#l) = ($ S x)#($ S l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ S (x # l) = $ S x # $ S l
[PROOF STEP]
by (simp add: app_subst_list)

\<comment> \<open>constructor laws for @{text new_tv}\<close>


[STATEMENT]
lemma new_tv_TVar[simp]:
  "new_tv n (TVar m) = (m<n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n (TVar m) = (m < n)
[PROOF STEP]
by (simp add: new_tv_def)


[STATEMENT]
lemma new_tv_FVar[simp]:
  "new_tv n (FVar m) = (m<n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n (FVar m) = (m < n)
[PROOF STEP]
by (simp add: new_tv_def)


[STATEMENT]
lemma new_tv_BVar[simp]:
  "new_tv n (BVar m) = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n (BVar m) = True
[PROOF STEP]
by (simp add: new_tv_def)


[STATEMENT]
lemma new_tv_Fun[simp]:
  "new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)
[PROOF STEP]
by (auto simp: new_tv_def)


[STATEMENT]
lemma new_tv_Fun2[simp]:
  "new_tv n (t1 =-> t2) = (new_tv n t1 \<and> new_tv n t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n (t1 =-> t2) = (new_tv n t1 \<and> new_tv n t2)
[PROOF STEP]
by (auto simp: new_tv_def)


[STATEMENT]
lemma new_tv_Nil[simp]:
  "new_tv n []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n []
[PROOF STEP]
by (simp add: new_tv_def)


[STATEMENT]
lemma new_tv_Cons[simp]:
  "new_tv n (x#l) = (new_tv n x \<and> new_tv n l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n (x # l) = (new_tv n x \<and> new_tv n l)
[PROOF STEP]
by (auto simp: new_tv_def)


[STATEMENT]
lemma new_tv_TVar_subst[simp]: "new_tv n TVar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n TVar
[PROOF STEP]
by (simp add: new_tv_def free_tv_subst dom_def cod_def)


[STATEMENT]
lemma new_tv_id_subst [simp]: "new_tv n id_subst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n id_subst
[PROOF STEP]
by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)


[STATEMENT]
lemma new_if_subst_type_scheme: "new_tv n (sch::type_scheme) \<Longrightarrow>
    $(\<lambda>k. if k<n then S k else S' k) sch = $S sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n sch \<Longrightarrow> $ (\<lambda>k. if k < n then S k else S' k) sch = $ S sch
[PROOF STEP]
by (induction sch) simp_all


[STATEMENT]
lemma new_if_subst_type_scheme_list: "new_tv n (A::type_scheme list) \<Longrightarrow>
    $(\<lambda>k. if k<n then S k else S' k) A = $S A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n A \<Longrightarrow> $ (\<lambda>k. if k < n then S k else S' k) A = $ S A
[PROOF STEP]
by (induction A) (simp_all add: new_if_subst_type_scheme)

\<comment> \<open>constructor laws for @{text dom} and @{text cod}\<close>


[STATEMENT]
lemma dom_id_subst [simp]: "dom id_subst = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Type.dom id_subst = {}
[PROOF STEP]
unfolding dom_def id_subst_def empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {n. TVar n \<noteq> TVar n} = {x. False}
[PROOF STEP]
by simp


[STATEMENT]
lemma cod_id_subst [simp]: "cod id_subst = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod id_subst = {}
[PROOF STEP]
unfolding cod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>m\<in>Type.dom id_subst. free_tv (id_subst m)) = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv id_subst = {}
[PROOF STEP]
unfolding free_tv_subst
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Type.dom id_subst \<union> cod id_subst = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma free_tv_nth_A_impl_free_tv_A:
  "\<lbrakk> n < length A;  x : free_tv (A!n) \<rbrakk> \<Longrightarrow> x : free_tv A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length A; x \<in> free_tv (A ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A
[PROOF STEP]
proof (induction A arbitrary: n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < length []; x \<in> free_tv ([] ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv []
 2. \<And>a A n. \<lbrakk>\<And>n. \<lbrakk>n < length A; x \<in> free_tv (A ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A; n < length (a # A); x \<in> free_tv ((a # A) ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv (a # A)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n < length []
x \<in> free_tv ([] ! n)

goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < length []; x \<in> free_tv ([] ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv []
 2. \<And>a A n. \<lbrakk>\<And>n. \<lbrakk>n < length A; x \<in> free_tv (A ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A; n < length (a # A); x \<in> free_tv ((a # A) ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv (a # A)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n < length []
x \<in> free_tv ([] ! n)

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

goal (1 subgoal):
 1. \<And>a A n. \<lbrakk>\<And>n. \<lbrakk>n < length A; x \<in> free_tv (A ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A; n < length (a # A); x \<in> free_tv ((a # A) ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv (a # A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A n. \<lbrakk>\<And>n. \<lbrakk>n < length A; x \<in> free_tv (A ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A; n < length (a # A); x \<in> free_tv ((a # A) ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv (a # A)
[PROOF STEP]
case (Cons a A)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n < length A; x \<in> free_tv (A ! ?n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A
n < length (a # A)
x \<in> free_tv ((a # A) ! n)

goal (1 subgoal):
 1. \<And>a A n. \<lbrakk>\<And>n. \<lbrakk>n < length A; x \<in> free_tv (A ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A; n < length (a # A); x \<in> free_tv ((a # A) ! n)\<rbrakk> \<Longrightarrow> x \<in> free_tv (a # A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?n < length A; x \<in> free_tv (A ! ?n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A
n < length (a # A)
x \<in> free_tv ((a # A) ! n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n < length A; x \<in> free_tv (A ! ?n)\<rbrakk> \<Longrightarrow> x \<in> free_tv A
n < length (a # A)
x \<in> free_tv ((a # A) ! n)

goal (1 subgoal):
 1. x \<in> free_tv (a # A)
[PROOF STEP]
by (fastforce simp add:nth_Cons' split: if_splits)
[PROOF STATE]
proof (state)
this:
x \<in> free_tv (a # A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma typ_substitutions_only_on_free_variables:
  "(\<forall>x\<in>free_tv t. (S x) = (S' x)) \<Longrightarrow> $ S (t::typ) = $ S' t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>free_tv t. S x = S' x \<Longrightarrow> $ S t = $ S' t
[PROOF STEP]
by (induct t) simp_all


[STATEMENT]
lemma eq_free_eq_subst_te: "(\<forall>n. n\<in>(free_tv t) \<longrightarrow> S1 n = S2 n) \<Longrightarrow> $ S1 (t::typ) = $ S2 t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> free_tv t \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 t = $ S2 t
[PROOF STEP]
apply (rule typ_substitutions_only_on_free_variables)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> free_tv t \<longrightarrow> S1 n = S2 n \<Longrightarrow> \<forall>x\<in>free_tv t. S1 x = S2 x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma scheme_substitutions_only_on_free_variables:
  "(\<forall>x\<in>free_tv sch. (S x) = (S' x)) \<Longrightarrow> $ S (sch::type_scheme) = $ S' sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>free_tv sch. S x = S' x \<Longrightarrow> $ S sch = $ S' sch
[PROOF STEP]
by (induct sch) simp_all


[STATEMENT]
lemma eq_free_eq_subst_type_scheme:
  "(\<forall>n. n\<in>(free_tv sch) \<longrightarrow> S1 n = S2 n) \<Longrightarrow> $ S1 (sch::type_scheme) = $ S2 sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> free_tv sch \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 sch = $ S2 sch
[PROOF STEP]
apply (rule scheme_substitutions_only_on_free_variables)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> free_tv sch \<longrightarrow> S1 n = S2 n \<Longrightarrow> \<forall>x\<in>free_tv sch. S1 x = S2 x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eq_free_eq_subst_scheme_list:
  "(\<forall>n. n\<in>(free_tv A) \<longrightarrow> S1 n = S2 n) \<Longrightarrow> $S1 (A::type_scheme list) = $S2 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> free_tv A \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A = $ S2 A
[PROOF STEP]
proof (induct A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>n. n \<in> free_tv [] \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 [] = $ S2 []
 2. \<And>a A. \<lbrakk>\<forall>n. n \<in> free_tv A \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A = $ S2 A; \<forall>n. n \<in> free_tv (a # A) \<longrightarrow> S1 n = S2 n\<rbrakk> \<Longrightarrow> $ S1 (a # A) = $ S2 (a # A)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> free_tv [] \<longrightarrow> S1 n = S2 n

goal (2 subgoals):
 1. \<forall>n. n \<in> free_tv [] \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 [] = $ S2 []
 2. \<And>a A. \<lbrakk>\<forall>n. n \<in> free_tv A \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A = $ S2 A; \<forall>n. n \<in> free_tv (a # A) \<longrightarrow> S1 n = S2 n\<rbrakk> \<Longrightarrow> $ S1 (a # A) = $ S2 (a # A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. n \<in> free_tv [] \<longrightarrow> S1 n = S2 n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>n. n \<in> free_tv [] \<longrightarrow> S1 n = S2 n

goal (1 subgoal):
 1. $ S1 [] = $ S2 []
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
$ S1 [] = $ S2 []

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<forall>n. n \<in> free_tv A \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A = $ S2 A; \<forall>n. n \<in> free_tv (a # A) \<longrightarrow> S1 n = S2 n\<rbrakk> \<Longrightarrow> $ S1 (a # A) = $ S2 (a # A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<forall>n. n \<in> free_tv A \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A = $ S2 A; \<forall>n. n \<in> free_tv (a # A) \<longrightarrow> S1 n = S2 n\<rbrakk> \<Longrightarrow> $ S1 (a # A) = $ S2 (a # A)
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> free_tv A_ \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A_ = $ S2 A_
\<forall>n. n \<in> free_tv (a_ # A_) \<longrightarrow> S1 n = S2 n

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<forall>n. n \<in> free_tv A \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A = $ S2 A; \<forall>n. n \<in> free_tv (a # A) \<longrightarrow> S1 n = S2 n\<rbrakk> \<Longrightarrow> $ S1 (a # A) = $ S2 (a # A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. n \<in> free_tv A_ \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A_ = $ S2 A_
\<forall>n. n \<in> free_tv (a_ # A_) \<longrightarrow> S1 n = S2 n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>n. n \<in> free_tv A_ \<longrightarrow> S1 n = S2 n \<Longrightarrow> $ S1 A_ = $ S2 A_
\<forall>n. n \<in> free_tv (a_ # A_) \<longrightarrow> S1 n = S2 n

goal (1 subgoal):
 1. $ S1 (a_ # A_) = $ S2 (a_ # A_)
[PROOF STEP]
by (fastforce intro: eq_free_eq_subst_type_scheme)
[PROOF STATE]
proof (state)
this:
$ S1 (a_ # A_) = $ S2 (a_ # A_)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weaken_asm_Un: "((\<forall>x\<in>A. (P x)) \<longrightarrow> Q) \<Longrightarrow> ((\<forall>x\<in>A \<union> B. (P x)) \<longrightarrow> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A. P x) \<longrightarrow> Q \<Longrightarrow> (\<forall>x\<in>A \<union> B. P x) \<longrightarrow> Q
[PROOF STEP]
by fast


[STATEMENT]
lemma scheme_list_substitutions_only_on_free_variables:
  "(\<forall>x\<in>free_tv A. (S x) = (S' x)) \<Longrightarrow> $ S (A::type_scheme list) = $ S' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>free_tv A. S x = S' x \<Longrightarrow> $ S A = $ S' A
[PROOF STEP]
by (induction A) (auto simp add: eq_free_eq_subst_type_scheme)


[STATEMENT]
lemma eq_subst_te_eq_free:
  "$ S1 (t::typ) = $ S2 t \<Longrightarrow> n:(free_tv t) \<Longrightarrow> S1 n = S2 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>$ S1 t = $ S2 t; n \<in> free_tv t\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma eq_subst_type_scheme_eq_free:
  "\<lbrakk> $ S1 (sch::type_scheme) = $ S2 sch; n:(free_tv sch) \<rbrakk> \<Longrightarrow> S1 n = S2 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>$ S1 sch = $ S2 sch; n \<in> free_tv sch\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
by (induction "sch") (auto dest: mk_scheme_injective)


[STATEMENT]
lemma codD: "v : cod S \<Longrightarrow> v : free_tv S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> cod S \<Longrightarrow> v \<in> free_tv S
[PROOF STEP]
unfolding free_tv_subst
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> cod S \<Longrightarrow> v \<in> Type.dom S \<union> cod S
[PROOF STEP]
by blast


[STATEMENT]
lemma not_free_impl_id: "x \<notin> free_tv S \<Longrightarrow> S x = TVar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> free_tv S \<Longrightarrow> S x = TVar x
[PROOF STEP]
unfolding free_tv_subst dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> {n. S n \<noteq> TVar n} \<union> cod S \<Longrightarrow> S x = TVar x
[PROOF STEP]
by blast


[STATEMENT]
lemma free_tv_le_new_tv: "[| new_tv n t; m:free_tv t |] ==> m<n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new_tv n t; m \<in> free_tv t\<rbrakk> \<Longrightarrow> m < n
[PROOF STEP]
unfolding new_tv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>m. m \<in> free_tv t \<longrightarrow> m < n; m \<in> free_tv t\<rbrakk> \<Longrightarrow> m < n
[PROOF STEP]
by blast


[STATEMENT]
lemma cod_app_subst:
  "[| v : free_tv(S n); v\<noteq>n |] ==> v : cod S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> free_tv (S n); v \<noteq> n\<rbrakk> \<Longrightarrow> v \<in> cod S
[PROOF STEP]
by (force simp add: dom_def cod_def UNION_eq Bex_def)


[STATEMENT]
lemma free_tv_subst_var: "free_tv (S (v::nat)) \<subseteq> insert v (cod S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv (S v) \<subseteq> insert v (cod S)
[PROOF STEP]
apply (cases "v:dom S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. v \<in> Type.dom S \<Longrightarrow> free_tv (S v) \<subseteq> insert v (cod S)
 2. v \<notin> Type.dom S \<Longrightarrow> free_tv (S v) \<subseteq> insert v (cod S)
[PROOF STEP]
apply (fastforce simp add: cod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> Type.dom S \<Longrightarrow> free_tv (S v) \<subseteq> insert v (cod S)
[PROOF STEP]
apply (fastforce simp add: dom_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma free_tv_app_subst_te: "free_tv ($ S (t::typ)) \<subseteq> cod S \<union> free_tv t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S t) \<subseteq> cod S \<union> free_tv t
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. free_tv ($ S (TVar x)) \<subseteq> cod S \<union> free_tv (TVar x)
 2. \<And>t1 t2. \<lbrakk>free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1; free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2\<rbrakk> \<Longrightarrow> free_tv ($ S (t1 -> t2)) \<subseteq> cod S \<union> free_tv (t1 -> t2)
[PROOF STEP]
case (TVar n)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. free_tv ($ S (TVar x)) \<subseteq> cod S \<union> free_tv (TVar x)
 2. \<And>t1 t2. \<lbrakk>free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1; free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2\<rbrakk> \<Longrightarrow> free_tv ($ S (t1 -> t2)) \<subseteq> cod S \<union> free_tv (t1 -> t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S (TVar n)) \<subseteq> cod S \<union> free_tv (TVar n)
[PROOF STEP]
by (simp add: free_tv_subst_var)
[PROOF STATE]
proof (state)
this:
free_tv ($ S (TVar n)) \<subseteq> cod S \<union> free_tv (TVar n)

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1; free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2\<rbrakk> \<Longrightarrow> free_tv ($ S (t1 -> t2)) \<subseteq> cod S \<union> free_tv (t1 -> t2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1; free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2\<rbrakk> \<Longrightarrow> free_tv ($ S (t1 -> t2)) \<subseteq> cod S \<union> free_tv (t1 -> t2)
[PROOF STEP]
case (Fun t1 t2)
[PROOF STATE]
proof (state)
this:
free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1
free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1; free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2\<rbrakk> \<Longrightarrow> free_tv ($ S (t1 -> t2)) \<subseteq> cod S \<union> free_tv (t1 -> t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1
free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1
free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2

goal (1 subgoal):
 1. free_tv ($ S (t1 -> t2)) \<subseteq> cod S \<union> free_tv (t1 -> t2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
free_tv ($ S (t1 -> t2)) \<subseteq> cod S \<union> free_tv (t1 -> t2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma free_tv_app_subst_type_scheme:
    "free_tv ($ S (sch::type_scheme)) \<subseteq> cod S \<union> free_tv sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S sch) \<subseteq> cod S \<union> free_tv sch
[PROOF STEP]
proof (induct sch)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. free_tv ($ S (FVar x)) \<subseteq> cod S \<union> free_tv (FVar x)
 2. \<And>x. free_tv ($ S (BVar x)) \<subseteq> cod S \<union> free_tv (BVar x)
 3. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
case (FVar n)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. free_tv ($ S (FVar x)) \<subseteq> cod S \<union> free_tv (FVar x)
 2. \<And>x. free_tv ($ S (BVar x)) \<subseteq> cod S \<union> free_tv (BVar x)
 3. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S (FVar n)) \<subseteq> cod S \<union> free_tv (FVar n)
[PROOF STEP]
by (simp add: free_tv_subst_var)
[PROOF STATE]
proof (state)
this:
free_tv ($ S (FVar n)) \<subseteq> cod S \<union> free_tv (FVar n)

goal (2 subgoals):
 1. \<And>x. free_tv ($ S (BVar x)) \<subseteq> cod S \<union> free_tv (BVar x)
 2. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. free_tv ($ S (BVar x)) \<subseteq> cod S \<union> free_tv (BVar x)
 2. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
case (BVar n)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. free_tv ($ S (BVar x)) \<subseteq> cod S \<union> free_tv (BVar x)
 2. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S (BVar n)) \<subseteq> cod S \<union> free_tv (BVar n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
free_tv ($ S (BVar n)) \<subseteq> cod S \<union> free_tv (BVar n)

goal (1 subgoal):
 1. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
case (SFun t1 t2)
[PROOF STATE]
proof (state)
this:
free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1
free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2

goal (1 subgoal):
 1. \<And>sch1 sch2. \<lbrakk>free_tv ($ S sch1) \<subseteq> cod S \<union> free_tv sch1; free_tv ($ S sch2) \<subseteq> cod S \<union> free_tv sch2\<rbrakk> \<Longrightarrow> free_tv ($ S (sch1 =-> sch2)) \<subseteq> cod S \<union> free_tv (sch1 =-> sch2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1
free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
free_tv ($ S t1) \<subseteq> cod S \<union> free_tv t1
free_tv ($ S t2) \<subseteq> cod S \<union> free_tv t2

goal (1 subgoal):
 1. free_tv ($ S (t1 =-> t2)) \<subseteq> cod S \<union> free_tv (t1 =-> t2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
free_tv ($ S (t1 =-> t2)) \<subseteq> cod S \<union> free_tv (t1 =-> t2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma free_tv_app_subst_scheme_list: "free_tv ($ S (A::type_scheme list)) \<subseteq> cod S \<union> free_tv A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S A) \<subseteq> cod S \<union> free_tv A
[PROOF STEP]
proof (induct A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. free_tv ($ S []) \<subseteq> cod S \<union> free_tv []
 2. \<And>a A. free_tv ($ S A) \<subseteq> cod S \<union> free_tv A \<Longrightarrow> free_tv ($ S (a # A)) \<subseteq> cod S \<union> free_tv (a # A)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. free_tv ($ S []) \<subseteq> cod S \<union> free_tv []
 2. \<And>a A. free_tv ($ S A) \<subseteq> cod S \<union> free_tv A \<Longrightarrow> free_tv ($ S (a # A)) \<subseteq> cod S \<union> free_tv (a # A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S []) \<subseteq> cod S \<union> free_tv []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
free_tv ($ S []) \<subseteq> cod S \<union> free_tv []

goal (1 subgoal):
 1. \<And>a A. free_tv ($ S A) \<subseteq> cod S \<union> free_tv A \<Longrightarrow> free_tv ($ S (a # A)) \<subseteq> cod S \<union> free_tv (a # A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. free_tv ($ S A) \<subseteq> cod S \<union> free_tv A \<Longrightarrow> free_tv ($ S (a # A)) \<subseteq> cod S \<union> free_tv (a # A)
[PROOF STEP]
case (Cons a al)
[PROOF STATE]
proof (state)
this:
free_tv ($ S al) \<subseteq> cod S \<union> free_tv al

goal (1 subgoal):
 1. \<And>a A. free_tv ($ S A) \<subseteq> cod S \<union> free_tv A \<Longrightarrow> free_tv ($ S (a # A)) \<subseteq> cod S \<union> free_tv (a # A)
[PROOF STEP]
with free_tv_app_subst_type_scheme
[PROOF STATE]
proof (chain)
picking this:
free_tv ($ ?S ?sch) \<subseteq> cod ?S \<union> free_tv ?sch
free_tv ($ S al) \<subseteq> cod S \<union> free_tv al
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
free_tv ($ ?S ?sch) \<subseteq> cod ?S \<union> free_tv ?sch
free_tv ($ S al) \<subseteq> cod S \<union> free_tv al

goal (1 subgoal):
 1. free_tv ($ S (a # al)) \<subseteq> cod S \<union> free_tv (a # al)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
free_tv ($ S (a # al)) \<subseteq> cod S \<union> free_tv (a # al)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma free_tv_comp_subst:
  "free_tv (\<lambda>u::nat. $ s1 (s2 u) :: typ) \<subseteq>
    free_tv s1 Un free_tv s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv (\<lambda>u. $ s1 (s2 u)) \<subseteq> free_tv s1 \<union> free_tv s2
[PROOF STEP]
unfolding free_tv_subst dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {n. $ s1 (s2 n) \<noteq> TVar n} \<union> cod (\<lambda>u. $ s1 (s2 u)) \<subseteq> {n. s1 n \<noteq> TVar n} \<union> cod s1 \<union> ({n. s2 n \<noteq> TVar n} \<union> cod s2)
[PROOF STEP]
by (force simp add: cod_def dom_def dest!:free_tv_app_subst_te [THEN subsetD])


[STATEMENT]
lemma free_tv_o_subst:
  "free_tv ($ S1 \<circ> S2) \<subseteq> free_tv S1 \<union> free_tv (S2 :: nat => typ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv ($ S1 \<circ> S2) \<subseteq> free_tv S1 \<union> free_tv S2
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. free_tv (\<lambda>x. $ S1 (S2 x)) \<subseteq> free_tv S1 \<union> free_tv S2
[PROOF STEP]
by (rule free_tv_comp_subst)


[STATEMENT]
lemma free_tv_of_substitutions_extend_to_types:
  "n : free_tv t \<Longrightarrow> free_tv (S n) \<subseteq> free_tv ($ S t::typ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> free_tv t \<Longrightarrow> free_tv (S n) \<subseteq> free_tv ($ S t)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma free_tv_of_substitutions_extend_to_schemes:
  "n : free_tv sch \<Longrightarrow> free_tv (S n) \<subseteq> free_tv ($ S sch::type_scheme)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> free_tv sch \<Longrightarrow> free_tv (S n) \<subseteq> free_tv ($ S sch)
[PROOF STEP]
by (induct sch) auto


[STATEMENT]
lemma free_tv_of_substitutions_extend_to_scheme_lists [simp]:
  "n : free_tv A \<Longrightarrow> free_tv (S n) \<subseteq> free_tv ($ S A::type_scheme list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> free_tv A \<Longrightarrow> free_tv (S n) \<subseteq> free_tv ($ S A)
[PROOF STEP]
by (induct A) (auto dest: free_tv_of_substitutions_extend_to_schemes)


[STATEMENT]
lemma free_tv_ML_scheme:
  fixes sch :: type_scheme
  shows "(n : free_tv sch) = (n: set (free_tv_ML sch))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<in> free_tv sch) = (n \<in> set (free_tv_ML sch))
[PROOF STEP]
by (induct sch) simp_all


[STATEMENT]
lemma free_tv_ML_scheme_list:
  fixes A :: "type_scheme list"
  shows "(n : free_tv A) = (n: set (free_tv_ML A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<in> free_tv A) = (n \<in> set (free_tv_ML A))
[PROOF STEP]
by (induct_tac A) (simp_all add: free_tv_ML_scheme)

\<comment> \<open>lemmata for @{text bound_tv}\<close>


[STATEMENT]
lemma bound_tv_mk_scheme [simp]: "bound_tv (mk_scheme t) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bound_tv (mk_scheme t) = {}
[PROOF STEP]
by (induct t) simp_all


[STATEMENT]
lemma bound_tv_subst_scheme [simp]:
  fixes sch :: type_scheme
  shows "bound_tv ($ S sch) = bound_tv sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bound_tv ($ S sch) = bound_tv sch
[PROOF STEP]
by (induct sch) simp_all


[STATEMENT]
lemma bound_tv_subst_scheme_list [simp]:
  fixes A :: "type_scheme list"
  shows "bound_tv ($ S A) = bound_tv A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bound_tv ($ S A) = bound_tv A
[PROOF STEP]
by (induct A) simp_all

\<comment> \<open>Lemmata for @{text new_tv}\<close>


[STATEMENT]
lemma new_tv_subst:
  "new_tv n S = ((\<forall>m. n \<le> m \<longrightarrow> (S m = TVar m)) \<and>
                 (\<forall>l. l < n \<longrightarrow> new_tv n (S l) ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n S = ((\<forall>m\<ge>n. S m = TVar m) \<and> (\<forall>l<n. new_tv n (S l)))
[PROOF STEP]
unfolding new_tv_def  free_tv_subst cod_def dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m. m \<in> {n. S n \<noteq> TVar n} \<union> (\<Union>m\<in>{n. S n \<noteq> TVar n}. free_tv (S m)) \<longrightarrow> m < n) = ((\<forall>m\<ge>n. S m = TVar m) \<and> (\<forall>l<n. \<forall>m. m \<in> free_tv (S l) \<longrightarrow> m < n))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>m. m \<in> {n. S n \<noteq> TVar n} \<union> (\<Union>m\<in>{n. S n \<noteq> TVar n}. free_tv (S m)) \<longrightarrow> m < n \<Longrightarrow> (\<forall>m\<ge>n. S m = TVar m) \<and> (\<forall>l<n. \<forall>m. m \<in> free_tv (S l) \<longrightarrow> m < n)
 2. (\<forall>m\<ge>n. S m = TVar m) \<and> (\<forall>l<n. \<forall>m. m \<in> free_tv (S l) \<longrightarrow> m < n) \<Longrightarrow> \<forall>m. m \<in> {n. S n \<noteq> TVar n} \<union> (\<Union>m\<in>{n. S n \<noteq> TVar n}. free_tv (S m)) \<longrightarrow> m < n
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m\<ge>n. S m = TVar m) \<and> (\<forall>l<n. \<forall>m. m \<in> free_tv (S l) \<longrightarrow> m < n) \<Longrightarrow> \<forall>m. m \<in> {n. S n \<noteq> TVar n} \<union> (\<Union>m\<in>{n. S n \<noteq> TVar n}. free_tv (S m)) \<longrightarrow> m < n
[PROOF STEP]
by simp (meson not_le)


[STATEMENT]
lemma new_tv_list: "new_tv n x = (\<forall>y\<in>set x. new_tv n y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n x = (\<forall>y\<in>set x. new_tv n y)
[PROOF STEP]
by (induction x) simp_all

\<comment> \<open>substitution affects only variables occurring freely\<close>


[STATEMENT]
lemma subst_te_new_tv:
  "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>x. if x=n then t' else S x) t = $S t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n t \<Longrightarrow> $ (\<lambda>x. if x = n then t' else S x) t = $ S t
[PROOF STEP]
by (induct t) simp_all


[STATEMENT]
lemma subst_te_new_type_scheme:
  "new_tv n (sch::type_scheme) \<Longrightarrow> $(\<lambda>x. if x=n then sch' else S x) sch = $S sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n sch \<Longrightarrow> $ (\<lambda>x. if x = n then sch' else S x) sch = $ S sch
[PROOF STEP]
by (induct sch) simp_all


[STATEMENT]
lemma subst_tel_new_scheme_list [simp]:
  "new_tv n (A::type_scheme list) \<Longrightarrow> $(\<lambda>x. if x=n then t else S x) A = $S A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n A \<Longrightarrow> $ (\<lambda>x. if x = n then t else S x) A = $ S A
[PROOF STEP]
by (induct A) (simp_all add: subst_te_new_type_scheme)

\<comment> \<open>all greater variables are also new\<close>


[STATEMENT]
lemma new_tv_le:
  "n\<le>m \<Longrightarrow> new_tv n t \<Longrightarrow> new_tv m t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> m; new_tv n t\<rbrakk> \<Longrightarrow> new_tv m t
[PROOF STEP]
by (meson less_le_trans new_tv_def)


[STATEMENT]
lemma new_tv_Suc[simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n t \<Longrightarrow> new_tv (Suc n) t
[PROOF STEP]
by (rule lessI [THEN less_imp_le [THEN new_tv_le]])

\<comment> \<open>@{text new_tv} property remains if a substitution is applied\<close>


[STATEMENT]
lemma new_tv_subst_var:
  "[| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < m; new_tv m S\<rbrakk> \<Longrightarrow> new_tv m (S n)
[PROOF STEP]
by (simp add: new_tv_subst)


[STATEMENT]
lemma new_tv_subst_te [simp]:
  "new_tv n S \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($ S t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new_tv n S; new_tv n t\<rbrakk> \<Longrightarrow> new_tv n ($ S t)
[PROOF STEP]
by (induction t) (auto simp add: new_tv_subst)


[STATEMENT]
lemma new_tv_subst_scheme_list:
  "new_tv n S \<Longrightarrow> new_tv n (A::type_scheme list) \<Longrightarrow> new_tv n ($ S A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new_tv n S; new_tv n A\<rbrakk> \<Longrightarrow> new_tv n ($ S A)
[PROOF STEP]
by (meson UnE codD free_tv_app_subst_scheme_list in_mono new_tv_def)


[STATEMENT]
lemma new_tv_only_depends_on_free_tv_type_scheme:
  fixes sch :: type_scheme
  shows "free_tv sch = free_tv sch' \<Longrightarrow> new_tv n sch \<Longrightarrow> new_tv n sch'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>free_tv sch = free_tv sch'; new_tv n sch\<rbrakk> \<Longrightarrow> new_tv n sch'
[PROOF STEP]
unfolding new_tv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>free_tv sch = free_tv sch'; \<forall>m. m \<in> free_tv sch \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<forall>m. m \<in> free_tv sch' \<longrightarrow> m < n
[PROOF STEP]
by simp


[STATEMENT]
lemma new_tv_only_depends_on_free_tv_scheme_list:
  fixes A :: "type_scheme list"
  shows "free_tv A = free_tv A' \<Longrightarrow> new_tv n A \<Longrightarrow> new_tv n A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>free_tv A = free_tv A'; new_tv n A\<rbrakk> \<Longrightarrow> new_tv n A'
[PROOF STEP]
unfolding new_tv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>free_tv A = free_tv A'; \<forall>m. m \<in> free_tv A \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<forall>m. m \<in> free_tv A' \<longrightarrow> m < n
[PROOF STEP]
by simp


[STATEMENT]
lemma new_tv_nth_nat_A:
  "m < length A \<Longrightarrow> new_tv n A \<Longrightarrow> new_tv n (A!m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length A; new_tv n A\<rbrakk> \<Longrightarrow> new_tv n (A ! m)
[PROOF STEP]
unfolding new_tv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length A; \<forall>m. m \<in> free_tv A \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<forall>ma. ma \<in> free_tv (A ! m) \<longrightarrow> ma < n
[PROOF STEP]
using free_tv_nth_A_impl_free_tv_A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n < length ?A; ?x \<in> free_tv (?A ! ?n)\<rbrakk> \<Longrightarrow> ?x \<in> free_tv ?A

goal (1 subgoal):
 1. \<lbrakk>m < length A; \<forall>m. m \<in> free_tv A \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<forall>ma. ma \<in> free_tv (A ! m) \<longrightarrow> ma < n
[PROOF STEP]
by blast

\<comment> \<open>composition of substitutions preserves @{text new_tv} proposition\<close>


[STATEMENT]
lemma new_tv_subst_comp_1:
  "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) \<circ> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new_tv n S; new_tv n R\<rbrakk> \<Longrightarrow> new_tv n ($ R \<circ> S)
[PROOF STEP]
by (simp add: new_tv_subst)


[STATEMENT]
lemma new_tv_subst_comp_2 :
  "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (\<lambda>v.$ R (S v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new_tv n S; new_tv n R\<rbrakk> \<Longrightarrow> new_tv n (\<lambda>v. $ R (S v))
[PROOF STEP]
by (simp add: new_tv_subst)

\<comment> \<open>new type variables do not occur freely in a type structure\<close>


[STATEMENT]
lemma new_tv_not_free_tv:
  "new_tv n A \<Longrightarrow> n \<notin> free_tv A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_tv n A \<Longrightarrow> n \<notin> free_tv A
[PROOF STEP]
by (auto simp add: new_tv_def)


[STATEMENT]
lemma fresh_variable_types: "\<exists>n. new_tv n (t::typ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. new_tv n t
[PROOF STEP]
apply (unfold new_tv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m. m \<in> free_tv t \<longrightarrow> m < n
[PROOF STEP]
apply (induction t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>n. \<forall>m. m \<in> free_tv (TVar x) \<longrightarrow> m < n
 2. \<And>t1 t2. \<lbrakk>\<exists>n. \<forall>m. m \<in> free_tv t1 \<longrightarrow> m < n; \<exists>n. \<forall>m. m \<in> free_tv t2 \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<exists>n. \<forall>m. m \<in> free_tv (t1 -> t2) \<longrightarrow> m < n
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>\<exists>n. \<forall>m. m \<in> free_tv t1 \<longrightarrow> m < n; \<exists>n. \<forall>m. m \<in> free_tv t2 \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<exists>n. \<forall>m. m \<in> free_tv (t1 -> t2) \<longrightarrow> m < n
[PROOF STEP]
by (metis less_trans linorder_cases new_tv_Fun new_tv_def)


[STATEMENT]
lemma fresh_variable_type_schemes:
  "\<exists>n. new_tv n (sch::type_scheme)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. new_tv n sch
[PROOF STEP]
apply (unfold new_tv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m. m \<in> free_tv sch \<longrightarrow> m < n
[PROOF STEP]
apply (induct_tac sch)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<exists>n. \<forall>m. m \<in> free_tv (FVar x) \<longrightarrow> m < n
 2. \<And>x. \<exists>n. \<forall>m. m \<in> free_tv (BVar x) \<longrightarrow> m < n
 3. \<And>x1a x2a. \<lbrakk>\<exists>n. \<forall>m. m \<in> free_tv x1a \<longrightarrow> m < n; \<exists>n. \<forall>m. m \<in> free_tv x2a \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<exists>n. \<forall>m. m \<in> free_tv (x1a =-> x2a) \<longrightarrow> m < n
[PROOF STEP]
apply (auto)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>n. \<forall>m. m \<in> free_tv (BVar x) \<longrightarrow> m < n
 2. \<And>x1a x2a. \<lbrakk>\<exists>n. \<forall>m. m \<in> free_tv x1a \<longrightarrow> m < n; \<exists>n. \<forall>m. m \<in> free_tv x2a \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<exists>n. \<forall>m. m \<in> free_tv (x1a =-> x2a) \<longrightarrow> m < n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2a. \<lbrakk>\<exists>n. \<forall>m. m \<in> free_tv x1a \<longrightarrow> m < n; \<exists>n. \<forall>m. m \<in> free_tv x2a \<longrightarrow> m < n\<rbrakk> \<Longrightarrow> \<exists>n. \<forall>m. m \<in> free_tv (x1a =-> x2a) \<longrightarrow> m < n
[PROOF STEP]
by (metis less_trans linorder_cases new_tv_Fun2 new_tv_def)


[STATEMENT]
lemma fresh_variable_type_scheme_lists:
  "\<exists>n. new_tv n (A::type_scheme list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. new_tv n A
[PROOF STEP]
apply (induction A)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>n. new_tv n []
 2. \<And>a A. \<exists>n. new_tv n A \<Longrightarrow> \<exists>n. new_tv n (a # A)
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a A. \<exists>n. new_tv n A \<Longrightarrow> \<exists>n. new_tv n (a # A)
[PROOF STEP]
by (metis fresh_variable_type_schemes le_cases new_tv_Cons new_tv_le)


[STATEMENT]
lemma make_one_new_out_of_two:
  "[| \<exists>n1. (new_tv n1 x); \<exists>n2. (new_tv n2 y)|] ==> \<exists>n. (new_tv n x) \<and> (new_tv n y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>n1. new_tv n1 x; \<exists>n2. new_tv n2 y\<rbrakk> \<Longrightarrow> \<exists>n. new_tv n x \<and> new_tv n y
[PROOF STEP]
by (meson new_tv_le nle_le)


[STATEMENT]
lemma ex_fresh_variable:
  "\<And>(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ).
          \<exists>n. (new_tv n A) \<and> (new_tv n A') \<and> (new_tv n t) \<and> (new_tv n t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A A' t t'. \<exists>n. new_tv n A \<and> new_tv n A' \<and> new_tv n t \<and> new_tv n t'
[PROOF STEP]
by (meson fresh_variable_type_scheme_lists fresh_variable_types max.cobounded1 max.cobounded2 new_tv_le)

\<comment> \<open>mgu does not introduce new type variables\<close>


[STATEMENT]
lemma length_app_subst_list [simp]:
  "\<And>A:: ('a::type_struct) list. length ($ S A) = length A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. length ($ S A) = length A
[PROOF STEP]
unfolding app_subst_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. length (map ($ S) A) = length A
[PROOF STEP]
by simp


[STATEMENT]
lemma subst_TVar_scheme [simp]:
  fixes sch :: type_scheme
  shows "$ TVar sch = sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ TVar sch = sch
[PROOF STEP]
by (induct sch) simp_all


[STATEMENT]
lemma subst_TVar_scheme_list [simp]:
  fixes A :: "type_scheme list"
  shows "$ TVar A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ TVar A = A
[PROOF STEP]
by (induct A) (simp_all add: app_subst_list)

\<comment> \<open>application of @{text id_subst} does not change type expression\<close>


[STATEMENT]
lemma app_subst_id_te [simp]: "$ id_subst = (\<lambda>t::typ. t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ id_subst = (\<lambda>t. t)
[PROOF STEP]
by (metis id_subst_def mk_scheme_injective subst_TVar_scheme subst_mk_scheme)


[STATEMENT]
lemma app_subst_id_tel [simp]:
  "$ id_subst = (\<lambda>A::type_scheme list. A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ id_subst = (\<lambda>A. A)
[PROOF STEP]
using id_subst_def subst_TVar_scheme_list
[PROOF STATE]
proof (prove)
using this:
id_subst = TVar
$ TVar ?A = ?A

goal (1 subgoal):
 1. $ id_subst = (\<lambda>A. A)
[PROOF STEP]
by auto

\<comment> \<open>composition of substitutions\<close>


[STATEMENT]
lemma o_id_subst [simp]: "$S \<circ> id_subst = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ S \<circ> id_subst = S
[PROOF STEP]
unfolding id_subst_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. $ S (TVar x)) = S
[PROOF STEP]
by simp


[STATEMENT]
lemma subst_comp_te: "$ R ($ S t::typ) = $ (\<lambda>x. $ R (S x) ) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ R ($ S t) = $ (\<lambda>x. $ R (S x)) t
[PROOF STEP]
by (induct t) simp_all


[STATEMENT]
lemma subst_comp_type_scheme:
  "$ R ($ S sch::type_scheme) = $ (\<lambda>x. $ R (S x) ) sch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ R ($ S sch) = $ (\<lambda>x. $ R (S x)) sch
[PROOF STEP]
by (induct sch) simp_all


[STATEMENT]
lemma subst_comp_scheme_list:
  "$ R ($ S A::type_scheme list) = $ (\<lambda>x. $ R (S x)) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ R ($ S A) = $ (\<lambda>x. $ R (S x)) A
[PROOF STEP]
unfolding app_subst_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ($ R) (map ($ S) A) = map ($ (\<lambda>x. $ R (S x))) A
[PROOF STEP]
proof (induct A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map ($ R) (map ($ S) []) = map ($ (\<lambda>x. $ R (S x))) []
 2. \<And>a A. map ($ R) (map ($ S) A) = map ($ (\<lambda>x. $ R (S x))) A \<Longrightarrow> map ($ R) (map ($ S) (a # A)) = map ($ (\<lambda>x. $ R (S x))) (a # A)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. map ($ R) (map ($ S) []) = map ($ (\<lambda>x. $ R (S x))) []
 2. \<And>a A. map ($ R) (map ($ S) A) = map ($ (\<lambda>x. $ R (S x))) A \<Longrightarrow> map ($ R) (map ($ S) (a # A)) = map ($ (\<lambda>x. $ R (S x))) (a # A)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ($ R) (map ($ S) []) = map ($ (\<lambda>x. $ R (S x))) []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map ($ R) (map ($ S) []) = map ($ (\<lambda>x. $ R (S x))) []

goal (1 subgoal):
 1. \<And>a A. map ($ R) (map ($ S) A) = map ($ (\<lambda>x. $ R (S x))) A \<Longrightarrow> map ($ R) (map ($ S) (a # A)) = map ($ (\<lambda>x. $ R (S x))) (a # A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. map ($ R) (map ($ S) A) = map ($ (\<lambda>x. $ R (S x))) A \<Longrightarrow> map ($ R) (map ($ S) (a # A)) = map ($ (\<lambda>x. $ R (S x))) (a # A)
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
map ($ R) (map ($ S) A_) = map ($ (\<lambda>x. $ R (S x))) A_

goal (1 subgoal):
 1. \<And>a A. map ($ R) (map ($ S) A) = map ($ (\<lambda>x. $ R (S x))) A \<Longrightarrow> map ($ R) (map ($ S) (a # A)) = map ($ (\<lambda>x. $ R (S x))) (a # A)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
map ($ R) (map ($ S) A_) = map ($ (\<lambda>x. $ R (S x))) A_

goal (1 subgoal):
 1. map ($ R) (map ($ S) (a_ # A_)) = map ($ (\<lambda>x. $ R (S x))) (a_ # A_)
[PROOF STEP]
by (simp add: subst_comp_type_scheme)
[PROOF STATE]
proof (state)
this:
map ($ R) (map ($ S) (a_ # A_)) = map ($ (\<lambda>x. $ R (S x))) (a_ # A_)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_subst:
  "n < length A \<Longrightarrow> ($ S A)!n = $S (A!n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length A \<Longrightarrow> $ S A ! n = $ S (A ! n)
[PROOF STEP]
by (simp add: app_subst_list)


[STATEMENT]
lemma nbae_param[param, autoref_rules]:
    "(nbae, nbae) \<in> \<langle>L\<rangle> set_rel \<rightarrow> \<langle>S\<rangle> set_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle> set_rel \<rightarrow>
      \<langle>S\<rangle> set_rel \<rightarrow> \<langle>L, S\<rangle> nbae_rel"
    "(alphabete, alphabete) \<in> \<langle>L, S\<rangle> nbae_rel \<rightarrow> \<langle>L\<rangle> set_rel"
    "(initiale, initiale) \<in> \<langle>L, S\<rangle> nbae_rel \<rightarrow> \<langle>S\<rangle> set_rel"
    "(transitione, transitione) \<in> \<langle>L, S\<rangle> nbae_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle> set_rel"
    "(acceptinge, acceptinge) \<in> \<langle>L, S\<rangle> nbae_rel \<rightarrow> \<langle>S\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nbae, nbae) \<in> \<langle>L\<rangle>set_rel \<rightarrow> \<langle>S\<rangle>set_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel \<rightarrow> \<langle>S\<rangle>set_rel \<rightarrow> \<langle>L, S\<rangle>nbae_rel &&& (alphabete, alphabete) \<in> \<langle>L, S\<rangle>nbae_rel \<rightarrow> \<langle>L\<rangle>set_rel) &&& (initiale, initiale) \<in> \<langle>L, S\<rangle>nbae_rel \<rightarrow> \<langle>S\<rangle>set_rel &&& (transitione, transitione) \<in> \<langle>L, S\<rangle>nbae_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel &&& (acceptinge, acceptinge) \<in> \<langle>L, S\<rangle>nbae_rel \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
unfolding nbae_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nbae, nbae) \<in> \<langle>L\<rangle>set_rel \<rightarrow> \<langle>S\<rangle>set_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel \<rightarrow> \<langle>S\<rangle>set_rel \<rightarrow> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>set_rel} &&& (alphabete, alphabete) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>set_rel} \<rightarrow> \<langle>L\<rangle>set_rel) &&& (initiale, initiale) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>set_rel} \<rightarrow> \<langle>S\<rangle>set_rel &&& (transitione, transitione) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>set_rel} \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel &&& (acceptinge, acceptinge) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>set_rel} \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
by auto