[STATEMENT]
lemma pseudo_mod_monic:
  fixes f g :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
  defines "r \<equiv> pseudo_mod f g"
  assumes monic_g: "monic g"
  shows "\<exists>q.  f = g * q + r" "r = 0 \<or> degree r < degree g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. f = g * q + r &&& r = 0 \<or> degree r < degree g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
let ?cg = "coeff g (degree g)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
let ?cge = "?cg ^ (Suc (degree f) - degree g)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
define a where "a = ?cge"
[PROOF STATE]
proof (state)
this:
a = lead_coeff g ^ (Suc (degree f) - degree g)

goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
from r_def[unfolded pseudo_mod_def]
[PROOF STATE]
proof (chain)
picking this:
r \<equiv> snd (pseudo_divmod f g)
[PROOF STEP]
obtain q where pdm: "pseudo_divmod f g = (q, r)"
[PROOF STATE]
proof (prove)
using this:
r \<equiv> snd (pseudo_divmod f g)

goal (1 subgoal):
 1. (\<And>q. pseudo_divmod f g = (q, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "pseudo_divmod f g") auto
[PROOF STATE]
proof (state)
this:
pseudo_divmod f g = (q, r)

goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
have g: "g \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<noteq> 0
[PROOF STEP]
using monic_g
[PROOF STATE]
proof (prove)
using this:
monic g

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

goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
from pseudo_divmod[OF g pdm]
[PROOF STATE]
proof (chain)
picking this:
smult (lead_coeff g ^ (Suc (degree f) - degree g)) f = g * q + r
r = 0 \<or> degree r < degree g
[PROOF STEP]
have id: "smult a f = g * q + r" and "r = 0 \<or> degree r < degree g"
[PROOF STATE]
proof (prove)
using this:
smult (lead_coeff g ^ (Suc (degree f) - degree g)) f = g * q + r
r = 0 \<or> degree r < degree g

goal (1 subgoal):
 1. smult a f = g * q + r &&& r = 0 \<or> degree r < degree g
[PROOF STEP]
by (auto simp: a_def)
[PROOF STATE]
proof (state)
this:
smult a f = g * q + r
r = 0 \<or> degree r < degree g

goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
have a1: "a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = (1::'a)
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff g ^ (Suc (degree f) - degree g) = (1::'a)
[PROOF STEP]
using monic_g
[PROOF STATE]
proof (prove)
using this:
monic g

goal (1 subgoal):
 1. lead_coeff g ^ (Suc (degree f) - degree g) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = (1::'a)

goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
hence id2: "f = g * q + r"
[PROOF STATE]
proof (prove)
using this:
a = (1::'a)

goal (1 subgoal):
 1. f = g * q + r
[PROOF STEP]
using id
[PROOF STATE]
proof (prove)
using this:
a = (1::'a)
smult a f = g * q + r

goal (1 subgoal):
 1. f = g * q + r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = g * q + r

goal (2 subgoals):
 1. \<exists>q. f = g * q + r
 2. r = 0 \<or> degree r < degree g
[PROOF STEP]
show "r = 0 \<or> degree r < degree g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = 0 \<or> degree r < degree g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
r = 0 \<or> degree r < degree g

goal (1 subgoal):
 1. \<exists>q. f = g * q + r
[PROOF STEP]
from g
[PROOF STATE]
proof (chain)
picking this:
g \<noteq> 0
[PROOF STEP]
have "a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
g \<noteq> 0

goal (1 subgoal):
 1. a \<noteq> (0::'a)
[PROOF STEP]
by (auto simp: a_def)
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>q. f = g * q + r
[PROOF STEP]
with id2
[PROOF STATE]
proof (chain)
picking this:
f = g * q + r
a \<noteq> (0::'a)
[PROOF STEP]
show "\<exists>q. f = g * q + r"
[PROOF STATE]
proof (prove)
using this:
f = g * q + r
a \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>q. f = g * q + r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q. f = g * q + r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma monic_imp_div_mod_int_poly_degree:
  fixes p :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
  assumes m: "monic u"
  shows "\<exists>q r. p = q*u + r \<and> (r = 0 \<or> degree r < degree u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q r. p = q * u + r \<and> (r = 0 \<or> degree r < degree u)
[PROOF STEP]
using pseudo_mod_monic[OF m]
[PROOF STATE]
proof (prove)
using this:
\<exists>q. ?f = u * q + pseudo_mod ?f u
pseudo_mod ?f u = 0 \<or> degree (pseudo_mod ?f u) < degree u

goal (1 subgoal):
 1. \<exists>q r. p = q * u + r \<and> (r = 0 \<or> degree r < degree u)
[PROOF STEP]
using mult.commute
[PROOF STATE]
proof (prove)
using this:
\<exists>q. ?f = u * q + pseudo_mod ?f u
pseudo_mod ?f u = 0 \<or> degree (pseudo_mod ?f u) < degree u
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. \<exists>q r. p = q * u + r \<and> (r = 0 \<or> degree r < degree u)
[PROOF STEP]
by metis


[STATEMENT]
lemma (in zero_hom) hom_upper_triangular:
  "A \<in> carrier_mat n n \<Longrightarrow> upper_triangular A \<Longrightarrow> upper_triangular (map_mat hom A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> carrier_mat n n; upper_triangular A\<rbrakk> \<Longrightarrow> upper_triangular (map_mat hom A)
[PROOF STEP]
by (auto simp: upper_triangular_def)


[STATEMENT]
lemma a_translate_functions:
  assumes "c \<in> carrier R"
  shows "a_translate c \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_translate c \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
apply(rule function_ring_car_memI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> a_translate c a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> a_translate c a = undefined
[PROOF STEP]
using assms a_translate_def
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier R
a_translate = (\<lambda>r\<in>carrier R. restrict ((\<oplus>) r) (carrier R))

goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> a_translate c a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> a_translate c a = undefined
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<notin> carrier R \<Longrightarrow> a_translate c a = undefined
[PROOF STEP]
using assms a_translate_def
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier R
a_translate = (\<lambda>r\<in>carrier R. restrict ((\<oplus>) r) (carrier R))

goal (1 subgoal):
 1. \<And>a. a \<notin> carrier R \<Longrightarrow> a_translate c a = undefined
[PROOF STEP]
by simp


[STATEMENT]
lemma m_translate_functions:
  assumes "c \<in> carrier R"
  shows "m_translate c \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_translate c \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
apply(rule function_ring_car_memI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> m_translate c a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> m_translate c a = undefined
[PROOF STEP]
using assms m_translate_def
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier R
m_translate = (\<lambda>r\<in>carrier R. restrict ((\<otimes>) r) (carrier R))

goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> m_translate c a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> m_translate c a = undefined
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<notin> carrier R \<Longrightarrow> m_translate c a = undefined
[PROOF STEP]
using assms m_translate_def
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier R
m_translate = (\<lambda>r\<in>carrier R. restrict ((\<otimes>) r) (carrier R))

goal (1 subgoal):
 1. \<And>a. a \<notin> carrier R \<Longrightarrow> m_translate c a = undefined
[PROOF STEP]
by simp


[STATEMENT]
lemma nat_power_functions:
  shows "nat_power n \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_power n \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
apply(rule function_ring_car_memI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> nat_power n a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> nat_power n a = undefined
[PROOF STEP]
using  nat_power_def
[PROOF STATE]
proof (prove)
using this:
nat_power = (\<lambda>n. \<lambda>a\<in>carrier R. a [^] n)

goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> nat_power n a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> nat_power n a = undefined
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<notin> carrier R \<Longrightarrow> nat_power n a = undefined
[PROOF STEP]
by (simp add: nat_power_def)


[STATEMENT]
lemma a_translate_eq:
  assumes "c \<in> carrier R"
  assumes "a \<in> carrier R"
  shows "a_translate c a = c \<oplus> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_translate c a = c \<oplus> a
[PROOF STEP]
by (simp add: a_translate_def assms(1) assms(2))


[STATEMENT]
lemma a_translate_eq':
  assumes "c \<in> carrier R"
  assumes "a \<notin> carrier R"
  shows "a_translate c a = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_translate c a = undefined
[PROOF STEP]
by (meson a_translate_functions assms(1) assms(2) function_ring_not_car)


[STATEMENT]
lemma a_translate_eq'':
  assumes "c \<notin> carrier R"
  shows "a_translate c = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_translate c = undefined
[PROOF STEP]
by (simp add: a_translate_def assms)


[STATEMENT]
lemma m_translate_eq:
  assumes "c \<in> carrier R"
  assumes "a \<in> carrier R"
  shows "m_translate c a = c \<otimes> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_translate c a = c \<otimes> a
[PROOF STEP]
by (simp add: m_translate_def assms(1) assms(2))


[STATEMENT]
lemma m_translate_eq':
  assumes "c \<in> carrier R"
  assumes "a \<notin> carrier R"
  shows "m_translate c a = undefined "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_translate c a = undefined
[PROOF STEP]
by (meson m_translate_functions assms(1) assms(2) function_ring_not_car)


[STATEMENT]
lemma m_translate_eq'':
  assumes "c \<notin> carrier R"
  shows "m_translate c = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_translate c = undefined
[PROOF STEP]
by (simp add: m_translate_def assms)


[STATEMENT]
lemma nat_power_eq:
  assumes "a \<in> carrier R"
  shows "nat_power n a = a[^]\<^bsub>R\<^esub> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_power n a = a [^] n
[PROOF STEP]
by (simp add: assms nat_power_def)


[STATEMENT]
lemma nat_power_eq':
  assumes "a \<notin> carrier R"
  shows "nat_power n a = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_power n a = undefined
[PROOF STEP]
by (simp add: assms nat_power_def)


[STATEMENT]
lemma constant_function_eq:
  assumes "a \<in> carrier R"
  assumes "b \<in> carrier R"
  shows "\<cc>\<^bsub>a\<^esub> b = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_function (carrier R) a b = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
b \<in> carrier R

goal (1 subgoal):
 1. constant_function (carrier R) a b = a
[PROOF STEP]
by (simp add: constant_functionE)


[STATEMENT]
lemma constant_function_eq':
  assumes "a \<in> carrier R"
  assumes "b \<notin> carrier R"
  shows "\<cc>\<^bsub>a\<^esub> b = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_function (carrier R) a b = undefined
[PROOF STEP]
by (simp add: constant_function_closed assms(1) assms(2) function_ring_not_car)


[STATEMENT]
lemma monomial_functions:
  assumes "c \<in> carrier R"
  shows "monomial c n \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomial c n \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
apply(rule function_ring_car_memI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> monomial c n a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> monomial c n a = undefined
[PROOF STEP]
unfolding monomial_function_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. c \<otimes> x [^] n) a \<in> carrier R
 2. \<And>a. a \<notin> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. c \<otimes> x [^] n) a = undefined
[PROOF STEP]
apply (simp add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<notin> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. c \<otimes> x [^] n) a = undefined
[PROOF STEP]
by simp


[STATEMENT]
lemma ring_id_closed[simp]:
"ring_id \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_id \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
by (simp add: function_ring_car_memI ring_id_def)


[STATEMENT]
lemma ring_id_eval:
  assumes "a \<in> carrier R"
  shows "ring_id a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_id a = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R

goal (1 subgoal):
 1. ring_id a = a
[PROOF STEP]
unfolding ring_id_def
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R

goal (1 subgoal):
 1. (\<lambda>x\<in>carrier R. x) a = a
[PROOF STEP]
by simp


[STATEMENT]
lemma constant_a_trans:
  assumes "a \<in>carrier R"
  shows "m_translate a  = \<cc>\<^bsub>a\<^esub> \<otimes>\<^bsub>Fun R\<^esub> ring_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_translate a = constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id
[PROOF STEP]
proof(rule function_ring_car_eqI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. m_translate a \<in> carrier (function_ring (carrier R) R)
 2. constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id \<in> carrier (function_ring (carrier R) R)
 3. \<And>aa. aa \<in> carrier R \<Longrightarrow> m_translate a aa = (constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id) aa
[PROOF STEP]
show "m_translate a \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_translate a \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R

goal (1 subgoal):
 1. m_translate a \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
using m_translate_functions
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
?c \<in> carrier R \<Longrightarrow> m_translate ?c \<in> carrier (function_ring (carrier R) R)

goal (1 subgoal):
 1. m_translate a \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m_translate a \<in> carrier (function_ring (carrier R) R)

goal (2 subgoals):
 1. constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id \<in> carrier (function_ring (carrier R) R)
 2. \<And>aa. aa \<in> carrier R \<Longrightarrow> m_translate a aa = (constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id) aa
[PROOF STEP]
show "\<cc>\<^bsub>a\<^esub> \<otimes>\<^bsub>Fun R\<^esub> ring_id \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
unfolding ring_id_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> (\<lambda>x\<in>carrier R. x) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
using assms ring_id_closed ring_id_def
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
ring_id \<in> carrier (function_ring (carrier R) R)
ring_id \<equiv> \<lambda>x\<in>carrier R. x

goal (1 subgoal):
 1. constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> (\<lambda>x\<in>carrier R. x) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
by (simp add: constant_function_closed fun_mult_closed)
[PROOF STATE]
proof (state)
this:
constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id \<in> carrier (function_ring (carrier R) R)

goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> m_translate a aa = (constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id) aa
[PROOF STEP]
show "\<And>x. x \<in> carrier R \<Longrightarrow> m_translate a x = (\<cc>\<^bsub>a\<^esub> \<otimes>\<^bsub>Fun R\<^esub> ring_id) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier R \<Longrightarrow> m_translate a x = (constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id) x
[PROOF STEP]
by (simp add: constant_function_closed assms constant_function_eq function_mult_eval_car m_translate_eq ring_id_eval)
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier R \<Longrightarrow> m_translate a ?x2 = (constant_function (carrier R) a \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> ring_id) ?x2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma polynomial_induct_lemma:
  assumes "f \<in> carrier (Fun R)"
  assumes "a \<in> carrier R"
  shows "(\<lambda>x \<in> carrier R. a \<oplus> x \<otimes> (f x)) \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
proof(rule function_ring_car_memI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa \<in> carrier R
 2. \<And>aa. aa \<notin> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa = undefined
[PROOF STEP]
show "\<And>aa. aa \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa \<in> carrier R
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa \<in> carrier R
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa \<in> carrier R
[PROOF STEP]
assume A: "y \<in> carrier R"
[PROOF STATE]
proof (state)
this:
y \<in> carrier R

goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa \<in> carrier R
[PROOF STEP]
have "a \<oplus> y \<otimes> f y \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<oplus> y \<otimes> f y \<in> carrier R
[PROOF STEP]
using A assms(1) assms(2) function_ring_car_closed
[PROOF STATE]
proof (prove)
using this:
y \<in> carrier R
f \<in> carrier (function_ring (carrier R) R)
a \<in> carrier R
\<lbrakk>?a \<in> carrier R; ?f \<in> carrier (function_ring (carrier R) R)\<rbrakk> \<Longrightarrow> ?f ?a \<in> carrier R

goal (1 subgoal):
 1. a \<oplus> y \<otimes> f y \<in> carrier R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<oplus> y \<otimes> f y \<in> carrier R

goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa \<in> carrier R
[PROOF STEP]
thus "(\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) y \<in> carrier R"
[PROOF STATE]
proof (prove)
using this:
a \<oplus> y \<otimes> f y \<in> carrier R

goal (1 subgoal):
 1. (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) y \<in> carrier R
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
a \<oplus> y \<otimes> f y \<in> carrier R
y \<in> carrier R

goal (1 subgoal):
 1. (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) y \<in> carrier R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) y \<in> carrier R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?aa2 \<in> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) ?aa2 \<in> carrier R

goal (1 subgoal):
 1. \<And>aa. aa \<notin> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa = undefined
[PROOF STEP]
show "\<And>aa. aa \<notin> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. aa \<notin> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) aa = undefined
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?aa2 \<notin> carrier R \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> f x) ?aa2 = undefined

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma polynomial_function:
  shows "set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (Fun R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
proof(induction as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> carrier R \<Longrightarrow> polynomial [] \<in> carrier (function_ring (carrier R) R)
 2. \<And>a as. \<lbrakk>set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R); set (a # as) \<subseteq> carrier R\<rbrakk> \<Longrightarrow> polynomial (a # as) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> carrier R

goal (2 subgoals):
 1. set [] \<subseteq> carrier R \<Longrightarrow> polynomial [] \<in> carrier (function_ring (carrier R) R)
 2. \<And>a as. \<lbrakk>set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R); set (a # as) \<subseteq> carrier R\<rbrakk> \<Longrightarrow> polynomial (a # as) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set [] \<subseteq> carrier R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set [] \<subseteq> carrier R

goal (1 subgoal):
 1. polynomial [] \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
by (simp add: function_zero_closed)
[PROOF STATE]
proof (state)
this:
polynomial [] \<in> carrier (function_ring (carrier R) R)

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R); set (a # as) \<subseteq> carrier R\<rbrakk> \<Longrightarrow> polynomial (a # as) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a as. \<lbrakk>set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R); set (a # as) \<subseteq> carrier R\<rbrakk> \<Longrightarrow> polynomial (a # as) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R)
set (a # as) \<subseteq> carrier R

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R); set (a # as) \<subseteq> carrier R\<rbrakk> \<Longrightarrow> polynomial (a # as) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R)
set (a # as) \<subseteq> carrier R
[PROOF STEP]
show "polynomial (a # as) \<in> carrier (function_ring (carrier R) R)"
[PROOF STATE]
proof (prove)
using this:
set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R)
set (a # as) \<subseteq> carrier R

goal (1 subgoal):
 1. polynomial (a # as) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
using polynomial.simps(2)[of a as] polynomial_induct_lemma[of "polynomial as" a]
[PROOF STATE]
proof (prove)
using this:
set as \<subseteq> carrier R \<Longrightarrow> polynomial as \<in> carrier (function_ring (carrier R) R)
set (a # as) \<subseteq> carrier R
polynomial (a # as) = (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> polynomial as x)
\<lbrakk>polynomial as \<in> carrier (function_ring (carrier R) R); a \<in> carrier R\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> polynomial as x) \<in> carrier (function_ring (carrier R) R)

goal (1 subgoal):
 1. polynomial (a # as) \<in> carrier (function_ring (carrier R) R)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
polynomial (a # as) \<in> carrier (function_ring (carrier R) R)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma polynomial_constant:
  assumes "a \<in> carrier R"
  shows "polynomial [a] = \<cc>\<^bsub>a\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. polynomial [a] = constant_function (carrier R) a
[PROOF STEP]
apply(rule function_ring_car_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. polynomial [a] \<in> carrier (function_ring (carrier R) R)
 2. constant_function (carrier R) a \<in> carrier (function_ring (carrier R) R)
 3. \<And>aa. aa \<in> carrier R \<Longrightarrow> polynomial [a] aa = constant_function (carrier R) a aa
[PROOF STEP]
using assms polynomial_function
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
set ?as \<subseteq> carrier R \<Longrightarrow> polynomial ?as \<in> carrier (function_ring (carrier R) R)

goal (3 subgoals):
 1. polynomial [a] \<in> carrier (function_ring (carrier R) R)
 2. constant_function (carrier R) a \<in> carrier (function_ring (carrier R) R)
 3. \<And>aa. aa \<in> carrier R \<Longrightarrow> polynomial [a] aa = constant_function (carrier R) a aa
[PROOF STEP]
apply (metis (full_types) list.distinct(1) list.set_cases set_ConsD subset_code(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. constant_function (carrier R) a \<in> carrier (function_ring (carrier R) R)
 2. \<And>aa. aa \<in> carrier R \<Longrightarrow> polynomial [a] aa = constant_function (carrier R) a aa
[PROOF STEP]
apply (simp add: constant_function_closed assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> polynomial [a] aa = constant_function (carrier R) a aa
[PROOF STEP]
using polynomial.simps(2)[of a "[]"] polynomial.simps(1) assms
[PROOF STATE]
proof (prove)
using this:
polynomial [a] = (\<lambda>x\<in>carrier R. a \<oplus> x \<otimes> polynomial [] x)
polynomial [] = \<zero>\<^bsub>function_ring (carrier R) R\<^esub>
a \<in> carrier R

goal (1 subgoal):
 1. \<And>aa. aa \<in> carrier R \<Longrightarrow> polynomial [a] aa = constant_function (carrier R) a aa
[PROOF STEP]
by (simp add: constant_function_eq function_zero_eval)


[STATEMENT]
lemma closed_seqs_memI:
  assumes "\<And>k. s k \<in> carrier R"
  shows "s \<in> closed_seqs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> carrier R\<^bsup>\<omega>\<^esup>
[PROOF STEP]
unfolding nat_seqs_def function_ring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> carrier \<lparr>carrier = UNIV \<rightarrow>\<^sub>E carrier R, mult = function_mult UNIV R, one = function_one UNIV R, zero = function_zero UNIV R, add = function_add UNIV R, smult = function_scalar_mult UNIV R\<rparr>
[PROOF STEP]
by (simp add: PiE_UNIV_domain assms)


[STATEMENT]
lemma closed_seqs_memE:
  assumes "s \<in> closed_seqs R"
  shows "s k \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s k \<in> carrier R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier R\<^bsup>\<omega>\<^esup>

goal (1 subgoal):
 1. s k \<in> carrier R
[PROOF STEP]
unfolding nat_seqs_def function_ring_def
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier \<lparr>carrier = UNIV \<rightarrow>\<^sub>E carrier R, mult = function_mult UNIV R, one = function_one UNIV R, zero = function_zero UNIV R, add = function_add UNIV R, smult = function_scalar_mult UNIV R\<rparr>

goal (1 subgoal):
 1. s k \<in> carrier R
[PROOF STEP]
by (simp add: PiE_iff)


[STATEMENT]
lemma is_constant_seqI:
  fixes a
  assumes "s \<in> closed_seqs R"
  assumes "\<And>k. s k = a"
  shows "is_constant_seq R s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_constant_seq R s
[PROOF STEP]
unfolding is_constant_seq_def constant_function_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>carrier R. s = (\<lambda>xa\<in>UNIV. x)
[PROOF STEP]
by (metis assms(1) assms(2) closed_seqs_memE restrict_UNIV restrict_ext)


[STATEMENT]
lemma is_constant_seqE:
  assumes "is_constant_seq R s"
  assumes "s k = a"
  shows "s n = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s n = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_constant_seq R s
s k = a

goal (1 subgoal):
 1. s n = a
[PROOF STEP]
unfolding is_constant_seq_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>carrier R. s = constant_function UNIV x
s k = a

goal (1 subgoal):
 1. s n = a
[PROOF STEP]
by (metis constant_function_def restrict_UNIV)


[STATEMENT]
lemma is_constant_seq_imp_closed:
  assumes "is_constant_seq R s"
  shows "s \<in> closed_seqs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> carrier R\<^bsup>\<omega>\<^esup>
[PROOF STEP]
apply(rule closed_seqs_memI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. s k \<in> carrier R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_constant_seq R s

goal (1 subgoal):
 1. \<And>k. s k \<in> carrier R
[PROOF STEP]
unfolding is_constant_seq_def constant_function_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>carrier R. s = (\<lambda>xa\<in>UNIV. x)

goal (1 subgoal):
 1. \<And>k. s k \<in> carrier R
[PROOF STEP]
by auto


[STATEMENT]
lemma seq_plus_closed:
  assumes "s \<in> closed_seqs R"
  assumes "s' \<in> closed_seqs R"
  shows "s \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> s' \<in> closed_seqs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> s' \<in> carrier R\<^bsup>\<omega>\<^esup>
[PROOF STEP]
by (metis assms(1) assms(2) nat_seqs_def ring_functions.fun_add_closed ring_functions_axioms)


[STATEMENT]
lemma seq_mult_closed:
  assumes "s \<in> closed_seqs R"
  assumes "s' \<in> closed_seqs R"
  shows "s \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> s' \<in> closed_seqs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> s' \<in> carrier R\<^bsup>\<omega>\<^esup>
[PROOF STEP]
apply(rule closed_seqs_memI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. (s \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> s') k \<in> carrier R
[PROOF STEP]
by (metis assms(1) assms(2) closed_seqs_memE nat_seqs_def ring_functions.fun_mult_closed ring_functions_axioms)


[STATEMENT]
lemma constant_function_comp_is_closed_seq:
  assumes "a \<in> carrier R"
  assumes "s \<in> closed_seqs R"
  shows "(const a \<circ> s) \<in> closed_seqs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_function (carrier R) a \<circ> s \<in> carrier R\<^bsup>\<omega>\<^esup>
[PROOF STEP]
by (simp add: constant_functionE assms(1) assms(2) closed_seqs_memE closed_seqs_memI)


[STATEMENT]
lemma constant_function_comp_is_constant_seq:
  assumes "a \<in> carrier R"
  assumes "s \<in> closed_seqs R"
  shows "is_constant_seq R ((const a) \<circ> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_constant_seq R (constant_function (carrier R) a \<circ> s)
[PROOF STEP]
apply(rule is_constant_seqI[of _ _ a] )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. constant_function (carrier R) a \<circ> s \<in> carrier R\<^bsup>\<omega>\<^esup>
 2. \<And>k. (constant_function (carrier R) a \<circ> s) k = a
[PROOF STEP]
apply (simp add: assms(1) assms(2) constant_function_comp_is_closed_seq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. (constant_function (carrier R) a \<circ> s) k = a
[PROOF STEP]
using assms(1) assms(2) closed_seqs_memE
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
s \<in> carrier R\<^bsup>\<omega>\<^esup>
?s \<in> carrier ?R\<^bsup>\<omega>\<^esup> \<Longrightarrow> ?s ?k \<in> carrier ?R

goal (1 subgoal):
 1. \<And>k. (constant_function (carrier R) a \<circ> s) k = a
[PROOF STEP]
by (simp add: closed_seqs_memE constant_functionE)


[STATEMENT]
lemma function_comp_is_closed_seq:
  assumes "s \<in> closed_seqs R"
  assumes "f \<in> carrier (Fun R)"
  shows "f \<circ> s \<in> closed_seqs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> s \<in> carrier R\<^bsup>\<omega>\<^esup>
[PROOF STEP]
apply(rule closed_seqs_memI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. (f \<circ> s) k \<in> carrier R
[PROOF STEP]
using assms(1) assms(2) closed_seqs_memE
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier R\<^bsup>\<omega>\<^esup>
f \<in> carrier (function_ring (carrier R) R)
?s \<in> carrier ?R\<^bsup>\<omega>\<^esup> \<Longrightarrow> ?s ?k \<in> carrier ?R

goal (1 subgoal):
 1. \<And>k. (f \<circ> s) k \<in> carrier R
[PROOF STEP]
by (metis comp_apply fun_add_eval_closed fun_add_zeroR function_zero_closed)


[STATEMENT]
lemma function_sum_comp_is_seq_sum:
  assumes "s \<in> closed_seqs R"
  assumes "f \<in> carrier (Fun R)"
  assumes "g \<in> carrier (Fun R)"
  shows "(f \<oplus>\<^bsub>Fun R\<^esub> g) \<circ> s = (f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s = (f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)
[PROOF STEP]
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV :: nat set"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. ring_functions R
 2. f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s \<in> carrier (function_ring UNIV R)
 3. (f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 4. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
apply (simp add: ring_functions_axioms)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s \<in> carrier (function_ring UNIV R)
 2. (f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 3. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
using function_comp_is_closed_seq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<in> carrier R\<^bsup>\<omega>\<^esup>; ?f \<in> carrier (function_ring (carrier R) R)\<rbrakk> \<Longrightarrow> ?f \<circ> ?s \<in> carrier R\<^bsup>\<omega>\<^esup>

goal (3 subgoals):
 1. f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s \<in> carrier (function_ring UNIV R)
 2. (f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 3. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
apply (metis assms(1) assms(2) assms(3) fun_add_closed nat_seqs_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 2. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
apply (metis assms(1) assms(2) assms(3) function_comp_is_closed_seq nat_seqs_def seq_plus_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<oplus>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
by (smt UNIV_eq_I assms(1) assms(2) assms(3) closed_seqs_memE comp_apply function_comp_is_closed_seq nat_seqs_def ring_functions.fun_add_eval_car ring_functions_axioms)


[STATEMENT]
lemma function_mult_comp_is_seq_mult:
  assumes "s \<in> closed_seqs R"
  assumes "f \<in> carrier (Fun R)"
  assumes "g \<in> carrier (Fun R)"
  shows "(f \<otimes>\<^bsub>Fun R\<^esub> g) \<circ> s = (f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s = (f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)
[PROOF STEP]
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV :: nat set"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. ring_functions R
 2. f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s \<in> carrier (function_ring UNIV R)
 3. (f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 4. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
apply (simp add: ring_functions_axioms)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s \<in> carrier (function_ring UNIV R)
 2. (f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 3. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
using function_comp_is_closed_seq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<in> carrier R\<^bsup>\<omega>\<^esup>; ?f \<in> carrier (function_ring (carrier R) R)\<rbrakk> \<Longrightarrow> ?f \<circ> ?s \<in> carrier R\<^bsup>\<omega>\<^esup>

goal (3 subgoals):
 1. f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s \<in> carrier (function_ring UNIV R)
 2. (f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 3. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
apply (metis assms(1) assms(2) assms(3) fun_mult_closed nat_seqs_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s) \<in> carrier (function_ring UNIV R)
 2. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
apply (metis assms(1) assms(2) assms(3) function_comp_is_closed_seq nat_seqs_def seq_mult_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> UNIV \<Longrightarrow> (f \<otimes>\<^bsub>function_ring (carrier R) R\<^esub> g \<circ> s) a = ((f \<circ> s) \<otimes>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> (g \<circ> s)) a
[PROOF STEP]
by (metis (no_types, lifting) assms(1) assms(2) assms(3) comp_apply function_comp_is_closed_seq nat_seqs_def ring_functions.function_mult_eval_car ring_functions.function_ring_car_closed ring_functions_axioms)


[STATEMENT]
lemma seq_plus_simp:
  assumes "s \<in> closed_seqs R"
  assumes "t \<in> closed_seqs R"
  shows "(s \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> t) k = s k \<oplus> t k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> t) k = s k \<oplus> t k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier R\<^bsup>\<omega>\<^esup>
t \<in> carrier R\<^bsup>\<omega>\<^esup>

goal (1 subgoal):
 1. (s \<oplus>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> t) k = s k \<oplus> t k
[PROOF STEP]
unfolding nat_seqs_def
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier (function_ring UNIV R)
t \<in> carrier (function_ring UNIV R)

goal (1 subgoal):
 1. (s \<oplus>\<^bsub>function_ring UNIV R\<^esub> t) k = s k \<oplus> t k
[PROOF STEP]
by (simp add: ring_functions.fun_add_eval_car ring_functions_axioms)


[STATEMENT]
lemma seq_one_simp:
"\<one>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> k = \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> k = \<one>
[PROOF STEP]
by (simp add: nat_seqs_def ring_functions.function_one_eval ring_functions_axioms)


[STATEMENT]
lemma seq_zero_simp:
"\<zero>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> k = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero>\<^bsub>R\<^bsup>\<omega>\<^esup>\<^esub> k = \<zero>
[PROOF STEP]
by (simp add: nat_seqs_def ring_functions.function_zero_eval ring_functions_axioms)


[STATEMENT]
lemma to_struct_map_closed:
  assumes "f \<in> (carrier T) \<rightarrow> (carrier S)"
  shows "to_struct_map T f \<in> (struct_maps T S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_struct_map T f \<in> struct_maps T S
[PROOF STEP]
by (smt PiE_restrict Pi_iff assms mem_Collect_eq restrict_PiE struct_maps_def to_struct_map_def)


[STATEMENT]
lemma struct_maps_memI:
  assumes "\<And> x. x \<in> carrier T \<Longrightarrow> f x \<in> carrier S"
  assumes "\<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined"
  shows "f \<in> struct_maps T S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> struct_maps T S
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> struct_maps T S
[PROOF STEP]
have 0: " (f \<in> (carrier T) \<rightarrow> (carrier S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> carrier T \<rightarrow> carrier S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier T \<Longrightarrow> f ?x \<in> carrier S
?x \<notin> carrier T \<Longrightarrow> f ?x = undefined

goal (1 subgoal):
 1. f \<in> carrier T \<rightarrow> carrier S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> carrier T \<rightarrow> carrier S

goal (1 subgoal):
 1. f \<in> struct_maps T S
[PROOF STEP]
have 1: "f  = restrict f (carrier T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = restrict f (carrier T)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier T \<Longrightarrow> f ?x \<in> carrier S
?x \<notin> carrier T \<Longrightarrow> f ?x = undefined

goal (1 subgoal):
 1. f = restrict f (carrier T)
[PROOF STEP]
by (simp add: extensional_def extensional_restrict)
[PROOF STATE]
proof (state)
this:
f = restrict f (carrier T)

goal (1 subgoal):
 1. f \<in> struct_maps T S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> struct_maps T S
[PROOF STEP]
using 0 1
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier T \<rightarrow> carrier S
f = restrict f (carrier T)

goal (1 subgoal):
 1. f \<in> struct_maps T S
[PROOF STEP]
unfolding struct_maps_def
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier T \<rightarrow> carrier S
f = restrict f (carrier T)

goal (1 subgoal):
 1. f \<in> {f \<in> carrier T \<rightarrow> carrier S. f = restrict f (carrier T)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> struct_maps T S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma struct_maps_memE:
  assumes "f \<in> struct_maps T S"
  shows  "\<And> x. x \<in> carrier T \<Longrightarrow> f x \<in> carrier S"
         "\<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> carrier T \<Longrightarrow> f x \<in> carrier S) &&& (\<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> struct_maps T S

goal (1 subgoal):
 1. (\<And>x. x \<in> carrier T \<Longrightarrow> f x \<in> carrier S) &&& (\<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined)
[PROOF STEP]
unfolding struct_maps_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> carrier T \<rightarrow> carrier S. f = restrict f (carrier T)}

goal (1 subgoal):
 1. (\<And>x. x \<in> carrier T \<Longrightarrow> f x \<in> carrier S) &&& (\<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> struct_maps T S

goal (1 subgoal):
 1. \<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined
[PROOF STEP]
unfolding struct_maps_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> carrier T \<rightarrow> carrier S. f = restrict f (carrier T)}

goal (1 subgoal):
 1. \<And>x. x \<notin> carrier T \<Longrightarrow> f x = undefined
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq restrict_apply)


[STATEMENT]
lemma struct_map_comp:
  assumes "g \<in> (struct_maps T S)"
  assumes "f \<in> (struct_maps S U)"
  shows "rcomp (carrier T) f g \<in> (struct_maps T U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compose (carrier T) f g \<in> struct_maps T U
[PROOF STEP]
proof(rule struct_maps_memI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> carrier T \<Longrightarrow> compose (carrier T) f g x \<in> carrier U
 2. \<And>x. x \<notin> carrier T \<Longrightarrow> compose (carrier T) f g x = undefined
[PROOF STEP]
show "\<And>x. x \<in> carrier T \<Longrightarrow> rcomp (carrier T) f g x \<in> carrier U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier T \<Longrightarrow> compose (carrier T) f g x \<in> carrier U
[PROOF STEP]
using assms struct_maps_memE(1)
[PROOF STATE]
proof (prove)
using this:
g \<in> struct_maps T S
f \<in> struct_maps S U
\<lbrakk>?f \<in> struct_maps ?T ?S; ?x \<in> carrier ?T\<rbrakk> \<Longrightarrow> ?f ?x \<in> carrier ?S

goal (1 subgoal):
 1. \<And>x. x \<in> carrier T \<Longrightarrow> compose (carrier T) f g x \<in> carrier U
[PROOF STEP]
by (metis compose_eq)
[PROOF STATE]
proof (state)
this:
?x \<in> carrier T \<Longrightarrow> compose (carrier T) f g ?x \<in> carrier U

goal (1 subgoal):
 1. \<And>x. x \<notin> carrier T \<Longrightarrow> compose (carrier T) f g x = undefined
[PROOF STEP]
show " \<And>x. x \<notin> carrier T \<Longrightarrow> rcomp (carrier T) f g x = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> carrier T \<Longrightarrow> compose (carrier T) f g x = undefined
[PROOF STEP]
by (meson compose_extensional extensional_arb)
[PROOF STATE]
proof (state)
this:
?x \<notin> carrier T \<Longrightarrow> compose (carrier T) f g ?x = undefined

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_comp_is_compose:
  assumes "g \<in> (struct_maps T S)"
  assumes "f \<in> (struct_maps S U)"
  assumes "a \<in> (carrier T)"
  shows "(rcomp (carrier T) f g) a = (f \<circ> g) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compose (carrier T) f g a = (f \<circ> g) a
[PROOF STEP]
by (simp add: FuncSet.compose_def assms(3))


[STATEMENT]
lemma r_comp_not_in_car:
  assumes "g \<in> (struct_maps T S)"
  assumes "f \<in> (struct_maps S U)"
  assumes "a \<notin> (carrier T)"
  shows "(rcomp (carrier T) f g) a = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compose (carrier T) f g a = undefined
[PROOF STEP]
by (simp add: FuncSet.compose_def assms(3))


[STATEMENT]
lemma pullback_closed:
  assumes "f \<in> (struct_maps T S)"
  assumes "g \<in> (struct_maps S U)"
  shows "pullback T f g \<in> (struct_maps T U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pullback T f g \<in> struct_maps T U
[PROOF STEP]
by (metis assms(1) assms(2) pullback_def struct_map_comp)


[STATEMENT]
lemma pushforward_closed:
  assumes "g \<in> (struct_maps T S)"
  assumes "f \<in> (struct_maps S U)"
  shows "pushforward T f g \<in> (struct_maps T U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pushforward T f g \<in> struct_maps T U
[PROOF STEP]
using assms(1) assms(2) struct_map_comp
[PROOF STATE]
proof (prove)
using this:
g \<in> struct_maps T S
f \<in> struct_maps S U
\<lbrakk>?g \<in> struct_maps ?T ?S; ?f \<in> struct_maps ?S ?U\<rbrakk> \<Longrightarrow> compose (carrier ?T) ?f ?g \<in> struct_maps ?T ?U

goal (1 subgoal):
 1. pushforward T f g \<in> struct_maps T U
[PROOF STEP]
by (metis pushforward_def)


[STATEMENT]
lemma JVM_states_unfold:
  "states P mxs mxl \<equiv> err(opt((Union {nlists n (types P) |n. n <= mxs}) \<times>
                                 nlists mxl (err(types P))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. states P mxs mxl \<equiv> err (opt (\<Union> {nlists n (types P) |n. n \<le> mxs} \<times> nlists mxl (err (types P))))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. states P mxs mxl \<equiv> err (opt (\<Union> {nlists n (types P) |n. n \<le> mxs} \<times> nlists mxl (err (types P))))
[PROOF STEP]
apply (unfold states_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (case case (case case (types P, subtype P, SemiType.sup P) of (A, r, f) \<Rightarrow> (\<Union> {nlists n A |n. n \<le> mxs}, Listn.le r, Listn.sup f) of (A, r\<^sub>A, f\<^sub>A) \<Rightarrow> \<lambda>(B, r\<^sub>B, f\<^sub>B). (A \<times> B, Product.le r\<^sub>A r\<^sub>B, Product.sup f\<^sub>A f\<^sub>B)) (case case case (types P, subtype P, SemiType.sup P) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f) of (A, r, f) \<Rightarrow> (nlists mxl A, Listn.le r, map2 f) of (A, r, f) \<Rightarrow> (A, r, \<lambda>x y. OK (f x y))) of (A, r, f) \<Rightarrow> (opt A, Opt.le r, Opt.sup f) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f)) \<equiv> err (opt (\<Union> {nlists n (types P) |n. n \<le> mxs} \<times> nlists mxl (err (types P))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma JVM_le_unfold:
 "le P m n \<equiv>
  Err.le(Opt.le(Product.le(Listn.le(subtype P))(Listn.le(Err.le(subtype P)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n \<equiv> Err.le (Opt.le (Product.le (Listn.le (subtype P)) (Listn.le (Err.le (subtype P)))))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n \<equiv> Err.le (Opt.le (Product.le (Listn.le (subtype P)) (Listn.le (Err.le (subtype P)))))
[PROOF STEP]
apply (unfold le_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (case case (case case (types P, subtype P, SemiType.sup P) of (A, r, f) \<Rightarrow> (\<Union> {nlists n A |n. n \<le> m}, Listn.le r, Listn.sup f) of (A, r\<^sub>A, f\<^sub>A) \<Rightarrow> \<lambda>(B, r\<^sub>B, f\<^sub>B). (A \<times> B, Product.le r\<^sub>A r\<^sub>B, Product.sup f\<^sub>A f\<^sub>B)) (case case case (types P, subtype P, SemiType.sup P) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f) of (A, r, f) \<Rightarrow> (nlists n A, Listn.le r, map2 f) of (A, r, f) \<Rightarrow> (A, r, \<lambda>x y. OK (f x y))) of (A, r, f) \<Rightarrow> (opt A, Opt.le r, Opt.sup f) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))) \<equiv> Err.le (Opt.le (Product.le (Listn.le (subtype P)) (Listn.le (Err.le (subtype P)))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sl_def2:
  "JVM_SemiType.sl P mxs mxl \<equiv>
  (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.sl P mxs mxl \<equiv> (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.sl P mxs mxl \<equiv> (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)
[PROOF STEP]
by (unfold JVM_SemiType.sup_def states_def JVM_SemiType.le_def) simp


[STATEMENT]
lemma JVM_le_conv:
  "le P m n (OK t1) (OK t2) = P \<turnstile> t1 \<le>' t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n (OK t1) (OK t2) = P \<turnstile> t1 \<le>' t2
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n (OK t1) (OK t2) = P \<turnstile> t1 \<le>' t2
[PROOF STEP]
by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def
                sup_state_def sup_ty_opt_def)


[STATEMENT]
lemma JVM_le_Err_conv:
  "le P m n = Err.le (sup_state_opt P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n = Err.le (sup_state_opt P)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n = Err.le (sup_state_opt P)
[PROOF STEP]
by (unfold sup_state_opt_def sup_state_def
             sup_ty_opt_def JVM_le_unfold) simp


[STATEMENT]
lemma err_le_unfold [iff]:
  "Err.le r (OK a) (OK b) = r a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le r (OK a) (OK b) = r a b
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le r (OK a) (OK b) = r a b
[PROOF STEP]
by (simp add: Err.le_def lesub_def)


[STATEMENT]
lemma order_sup_state_opt' [intro, simp]:
  "wf_prog wf_mb P \<Longrightarrow>
      order (sup_state_opt P) (opt ((\<Union> {nlists n (types P) |n. n \<le> mxs} ) \<times> nlists (Suc (length Ts + mxl\<^sub>0)) (err (types P))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> order (sup_state_opt P) (opt (\<Union> {nlists n (types P) |n. n \<le> mxs} \<times> nlists (Suc (length Ts + mxl\<^sub>0)) (err (types P))))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> order (sup_state_opt P) (opt (\<Union> {nlists n (types P) |n. n \<le> mxs} \<times> nlists (Suc (length Ts + mxl\<^sub>0)) (err (types P))))
[PROOF STEP]
apply (unfold sup_state_opt_def sup_state_def sup_ty_opt_def  )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> order (Opt.le (Product.le (Listn.le (subtype P)) (Listn.le (Err.le (subtype P))))) (opt (\<Union> {nlists n (types P) |n. n \<le> mxs} \<times> nlists (Suc (length Ts + mxl\<^sub>0)) (err (types P))))
[PROOF STEP]
apply (blast intro:order_le_prodI) \<comment>\<open> use Listn.thy.order_listI2  \<close>
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma semilat_JVM [intro?]:
  "wf_prog wf_mb P \<Longrightarrow> semilat (JVM_SemiType.sl P mxs mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> semilat (JVM_SemiType.sl P mxs mxl)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> semilat (JVM_SemiType.sl P mxs mxl)
[PROOF STEP]
apply (unfold JVM_SemiType.sl_def stk_esl_def loc_sl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> err_semilat (Opt.esl (Product.esl (upto_esl mxs (SemiType.esl P)) (Err.esl (Listn.sl mxl (Err.sl (SemiType.esl P))))))
[PROOF STEP]
apply (blast intro: err_semilat_Product_esl err_semilat_upto_esl
                      Listn_sl err_semilat_JType_esl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subtype_refl: "subtype P t t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtype P t t
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtype P t t
[PROOF STEP]
by (simp add: fun_of_def)


[STATEMENT]
lemma sup_ty_opt_refl [iff]: "P \<turnstile> T \<le>\<^sub>\<top> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> T \<le>\<^sub>\<top> T
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> T \<le>\<^sub>\<top> T
[PROOF STEP]
apply (unfold sup_ty_opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le (subtype P) T T
[PROOF STEP]
apply (fold lesub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> T
[PROOF STEP]
apply (rule le_err_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<sqsubseteq>\<^bsub>subtype P\<^esub> x
[PROOF STEP]
apply (simp add: lesub_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Err_any_conv [iff]: "P \<turnstile> Err \<le>\<^sub>\<top> T = (T = Err)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> Err \<le>\<^sub>\<top> T = (T = Err)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> Err \<le>\<^sub>\<top> T = (T = Err)
[PROOF STEP]
by (unfold sup_ty_opt_def) (rule Err_le_conv [simplified lesub_def])


[STATEMENT]
lemma any_Err [iff]: "P \<turnstile> T \<le>\<^sub>\<top> Err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> T \<le>\<^sub>\<top> Err
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> T \<le>\<^sub>\<top> Err
[PROOF STEP]
by (unfold sup_ty_opt_def) (rule le_Err [simplified lesub_def])


[STATEMENT]
lemma OK_OK_conv [iff]:
  "P \<turnstile> OK T \<le>\<^sub>\<top> OK T' = P \<turnstile> T \<le> T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> OK T \<le>\<^sub>\<top> OK T' = subtype P T T'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> OK T \<le>\<^sub>\<top> OK T' = subtype P T T'
[PROOF STEP]
by (simp add: sup_ty_opt_def fun_of_def)


[STATEMENT]
lemma any_OK_conv [iff]:
  "P \<turnstile> X \<le>\<^sub>\<top> OK T' = (\<exists>T. X = OK T \<and> P \<turnstile> T \<le> T')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> X \<le>\<^sub>\<top> OK T' = (\<exists>T. X = OK T \<and> subtype P T T')
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> X \<le>\<^sub>\<top> OK T' = (\<exists>T. X = OK T \<and> subtype P T T')
[PROOF STEP]
apply (unfold sup_ty_opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le (subtype P) X (OK T') = (\<exists>T. X = OK T \<and> subtype P T T')
[PROOF STEP]
apply (rule le_OK_conv [simplified lesub_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OK_any_conv:
 "P \<turnstile> OK T \<le>\<^sub>\<top> X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> P \<turnstile> T \<le> T'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> OK T \<le>\<^sub>\<top> X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> subtype P T T'))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> OK T \<le>\<^sub>\<top> X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> subtype P T T'))
[PROOF STEP]
apply (unfold sup_ty_opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le (subtype P) (OK T) X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> subtype P T T'))
[PROOF STEP]
apply (rule OK_le_conv [simplified lesub_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sup_ty_opt_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a \<le>\<^sub>\<top> b; P \<turnstile> b \<le>\<^sub>\<top> c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>\<top> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>\<^sub>\<top> b; P \<turnstile> b \<le>\<^sub>\<top> c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>\<top> c
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>\<^sub>\<top> b; P \<turnstile> b \<le>\<^sub>\<top> c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>\<top> c
[PROOF STEP]
by (auto intro: widen_trans
           simp add: sup_ty_opt_def Err.le_def lesub_def fun_of_def
           split: err.splits)


[STATEMENT]
lemma stk_convert:
  "P \<turnstile> ST [\<le>] ST' = Listn.le (subtype P) ST ST'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ST [\<le>] ST' = Listn.le (subtype P) ST ST'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ST [\<le>] ST' = Listn.le (subtype P) ST ST'
[PROOF STEP]
by (simp add: Listn.le_def lesub_def)


[STATEMENT]
lemma sup_loc_refl [iff]: "P \<turnstile> LT [\<le>\<^sub>\<top>] LT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> LT [\<le>\<^sub>\<top>] LT
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> LT [\<le>\<^sub>\<top>] LT
[PROOF STEP]
by (rule list_all2_refl) simp


[STATEMENT]
lemma sup_loc_def:
  "P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<equiv> Listn.le (sup_ty_opt P) LT LT'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<equiv> Listn.le (sup_ty_opt P) LT LT'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<equiv> Listn.le (sup_ty_opt P) LT LT'
[PROOF STEP]
by (simp add: Listn.le_def lesub_def)


[STATEMENT]
lemma sup_loc_widens_conv [iff]:
  "P \<turnstile> map OK Ts [\<le>\<^sub>\<top>] map OK Ts' = P \<turnstile> Ts [\<le>] Ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> map OK Ts [\<le>\<^sub>\<top>] map OK Ts' = P \<turnstile> Ts [\<le>] Ts'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> map OK Ts [\<le>\<^sub>\<top>] map OK Ts' = P \<turnstile> Ts [\<le>] Ts'
[PROOF STEP]
by (simp add: list_all2_map1 list_all2_map2)


[STATEMENT]
lemma sup_loc_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a [\<le>\<^sub>\<top>] b; P \<turnstile> b [\<le>\<^sub>\<top>] c\<rbrakk> \<Longrightarrow> P \<turnstile> a [\<le>\<^sub>\<top>] c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a [\<le>\<^sub>\<top>] b; P \<turnstile> b [\<le>\<^sub>\<top>] c\<rbrakk> \<Longrightarrow> P \<turnstile> a [\<le>\<^sub>\<top>] c
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a [\<le>\<^sub>\<top>] b; P \<turnstile> b [\<le>\<^sub>\<top>] c\<rbrakk> \<Longrightarrow> P \<turnstile> a [\<le>\<^sub>\<top>] c
[PROOF STEP]
by (rule list_all2_trans, rule sup_ty_opt_trans)


[STATEMENT]
lemma sup_state_conv [iff]:
  "P \<turnstile> (ST,LT) \<le>\<^sub>i (ST',LT') = (P \<turnstile> ST [\<le>] ST' \<and> P \<turnstile> LT [\<le>\<^sub>\<top>] LT')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> (ST, LT) \<le>\<^sub>i (ST', LT') = (P \<turnstile> ST [\<le>] ST' \<and> P \<turnstile> LT [\<le>\<^sub>\<top>] LT')
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> (ST, LT) \<le>\<^sub>i (ST', LT') = (P \<turnstile> ST [\<le>] ST' \<and> P \<turnstile> LT [\<le>\<^sub>\<top>] LT')
[PROOF STEP]
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_def)


[STATEMENT]
lemma sup_state_conv2:
  "P \<turnstile> s1 \<le>\<^sub>i s2 = (P \<turnstile> fst s1 [\<le>] fst s2 \<and> P \<turnstile> snd s1 [\<le>\<^sub>\<top>] snd s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s1 \<le>\<^sub>i s2 = (P \<turnstile> fst s1 [\<le>] fst s2 \<and> P \<turnstile> snd s1 [\<le>\<^sub>\<top>] snd s2)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s1 \<le>\<^sub>i s2 = (P \<turnstile> fst s1 [\<le>] fst s2 \<and> P \<turnstile> snd s1 [\<le>\<^sub>\<top>] snd s2)
[PROOF STEP]
by (cases s1, cases s2) simp


[STATEMENT]
lemma sup_state_refl [iff]: "P \<turnstile> s \<le>\<^sub>i s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>\<^sub>i s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>\<^sub>i s
[PROOF STEP]
by (auto simp add: sup_state_conv2)


[STATEMENT]
lemma sup_state_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a \<le>\<^sub>i b; P \<turnstile> b \<le>\<^sub>i c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>i c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>\<^sub>i b; P \<turnstile> b \<le>\<^sub>i c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>i c
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>\<^sub>i b; P \<turnstile> b \<le>\<^sub>i c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>i c
[PROOF STEP]
by (auto intro: sup_loc_trans widens_trans simp add: sup_state_conv2)


[STATEMENT]
lemma sup_state_opt_None_any [iff]:
  "P \<turnstile> None \<le>' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> None \<le>' s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> None \<le>' s
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def)


[STATEMENT]
lemma sup_state_opt_any_None [iff]:
  "P \<turnstile> s \<le>' None = (s = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>' None = (s = None)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>' None = (s = None)
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def)


[STATEMENT]
lemma sup_state_opt_Some_Some [iff]:
  "P \<turnstile> Some a \<le>' Some b = P \<turnstile> a \<le>\<^sub>i b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>a\<rfloor> \<le>' \<lfloor>b\<rfloor> = P \<turnstile> a \<le>\<^sub>i b
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>a\<rfloor> \<le>' \<lfloor>b\<rfloor> = P \<turnstile> a \<le>\<^sub>i b
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def lesub_def)


[STATEMENT]
lemma sup_state_opt_any_Some:
  "P \<turnstile> (Some s) \<le>' X = (\<exists>s'. X = Some s' \<and> P \<turnstile> s \<le>\<^sub>i s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>s\<rfloor> \<le>' X = (\<exists>s'. X = \<lfloor>s'\<rfloor> \<and> P \<turnstile> s \<le>\<^sub>i s')
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>s\<rfloor> \<le>' X = (\<exists>s'. X = \<lfloor>s'\<rfloor> \<and> P \<turnstile> s \<le>\<^sub>i s')
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def lesub_def)


[STATEMENT]
lemma sup_state_opt_refl [iff]: "P \<turnstile> s \<le>' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>' s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>' s
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def lesub_def)


[STATEMENT]
lemma sup_state_opt_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a \<le>' b; P \<turnstile> b \<le>' c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>' c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>' b; P \<turnstile> b \<le>' c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>' c
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>' b; P \<turnstile> b \<le>' c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>' c
[PROOF STEP]
apply (unfold sup_state_opt_def Opt.le_def lesub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case b of None \<Rightarrow> a = None | \<lfloor>y\<rfloor> \<Rightarrow> case a of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> P \<turnstile> x \<le>\<^sub>i y; case c of None \<Rightarrow> b = None | \<lfloor>y\<rfloor> \<Rightarrow> case b of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> P \<turnstile> x \<le>\<^sub>i y\<rbrakk> \<Longrightarrow> case c of None \<Rightarrow> a = None | \<lfloor>y\<rfloor> \<Rightarrow> case a of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> P \<turnstile> x \<le>\<^sub>i y
[PROOF STEP]
apply (simp del: split_paired_All)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a x2b. \<lbrakk>c = \<lfloor>x2a\<rfloor>; P \<turnstile> x2 \<le>\<^sub>i x2a; b = \<lfloor>x2\<rfloor>; a = \<lfloor>x2b\<rfloor>; P \<turnstile> x2b \<le>\<^sub>i x2\<rbrakk> \<Longrightarrow> P \<turnstile> x2b \<le>\<^sub>i x2a
[PROOF STEP]
apply (rule sup_state_trans, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sup_state_opt_err  : "(Err.le (sup_state_opt P)) s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le (sup_state_opt P) s s
[PROOF STEP]
apply (unfold JVM_le_unfold Product.le_def Opt.le_def Err.le_def lesssub_def lesub_def Listn.le_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case s of Err \<Rightarrow> True | OK y \<Rightarrow> case s of Err \<Rightarrow> False | OK x \<Rightarrow> P \<turnstile> x \<le>' y
[PROOF STEP]
apply (auto split: err.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Cons_less_Conss1 [simp]:
  "x#xs [\<sqsubset>\<^bsub>subtype P\<^esub>] y#ys = (x \<sqsubset>\<^bsub>subtype P\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>subtype P\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubset>\<^bsub>subtype P\<^esub>] y # ys) = (x \<sqsubset>\<^bsub>subtype P\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>subtype P\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys)
[PROOF STEP]
apply (unfold lesssub_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubseteq>\<^bsub>subtype P\<^esub>] y # ys \<and> x # xs \<noteq> y # ys) = ((x \<sqsubseteq>\<^bsub>subtype P\<^esub> y \<and> x \<noteq> y) \<and> xs [\<sqsubseteq>\<^bsub>subtype P\<^esub>] ys \<or> x = y \<and> xs [\<sqsubseteq>\<^bsub>subtype P\<^esub>] ys \<and> xs \<noteq> ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; xs [\<sqsubseteq>\<^bsub>subtype P\<^esub>] ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^bsub>subtype P\<^esub> y
[PROOF STEP]
apply (simp add:lesssub_def lesub_def) \<comment>\<open>widen_refl, subtype_refl \<close>
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Cons_less_Conss2 [simp]:
  "x#xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y#ys = (x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y # ys) = (x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys)
[PROOF STEP]
apply (unfold lesssub_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] y # ys \<and> x # xs \<noteq> y # ys) = ((x \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> y \<and> x \<noteq> y) \<and> xs [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] ys \<or> x = y \<and> xs [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] ys \<and> xs \<noteq> ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; xs [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> y
[PROOF STEP]
apply (simp add:lesssub_def lesub_def Err.le_def split: err.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done