[STATEMENT]
lemma submultiplicative_converges:
  fixes u::"nat\<Rightarrow>real"
  assumes "\<And>n. u n \<ge> 0"
          "\<And>m n. u (m+n) \<le> u m * u n"
  shows "(\<lambda>n. root n (u n))\<longlonglongrightarrow> Inf {root n (u n) | n. n>0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
define v where "v = (\<lambda> n. root n (u n))"
[PROOF STATE]
proof (state)
this:
v = (\<lambda>n. root n (u n))

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
define V where "V = {v n | n. n>0}"
[PROOF STATE]
proof (state)
this:
V = {v n |n. 0 < n}

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V = {v n |n. 0 < n}
[PROOF STEP]
have "V \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
V = {v n |n. 0 < n}

goal (1 subgoal):
 1. V \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V \<noteq> {}

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
have "t \<ge> 0" if "t \<in> V" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> t
[PROOF STEP]
using that V_def v_def assms(1)
[PROOF STATE]
proof (prove)
using this:
t \<in> V
V = {v n |n. 0 < n}
v = (\<lambda>n. root n (u n))
0 \<le> u ?n

goal (1 subgoal):
 1. 0 \<le> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?t \<in> V \<Longrightarrow> 0 \<le> ?t

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t \<in> V \<Longrightarrow> 0 \<le> ?t
[PROOF STEP]
have "Inf V \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
?t \<in> V \<Longrightarrow> 0 \<le> ?t

goal (1 subgoal):
 1. 0 \<le> Inf V
[PROOF STEP]
by (simp add: \<open>V \<noteq> {}\<close> cInf_greatest)
[PROOF STATE]
proof (state)
this:
0 \<le> Inf V

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
have "bdd_below V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_below V
[PROOF STEP]
by (meson \<open>\<And>t. t \<in> V \<Longrightarrow> 0 \<le> t\<close> bdd_below_def)
[PROOF STATE]
proof (state)
this:
bdd_below V

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
assume "\<exists>n. u n = 0"
[PROOF STATE]
proof (state)
this:
\<exists>n. u n = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. u n = 0
[PROOF STEP]
obtain n where "u n = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. u n = 0

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u n = 0
[PROOF STEP]
have "u m = 0" if "m \<ge> n" for m
[PROOF STATE]
proof (prove)
using this:
u n = 0

goal (1 subgoal):
 1. u m = 0
[PROOF STEP]
by (metis that antisym_conv assms(1) assms(2) le_Suc_ex mult_zero_left)
[PROOF STATE]
proof (state)
this:
n \<le> ?m \<Longrightarrow> u ?m = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> ?m \<Longrightarrow> u ?m = 0
[PROOF STEP]
have *: "v m = 0" if "m \<ge> n" for m
[PROOF STATE]
proof (prove)
using this:
n \<le> ?m \<Longrightarrow> u ?m = 0

goal (1 subgoal):
 1. v m = 0
[PROOF STEP]
using v_def that
[PROOF STATE]
proof (prove)
using this:
n \<le> ?m \<Longrightarrow> u ?m = 0
v = (\<lambda>n. root n (u n))
n \<le> m

goal (1 subgoal):
 1. v m = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<le> ?m \<Longrightarrow> v ?m = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> ?m \<Longrightarrow> v ?m = 0
[PROOF STEP]
have "v \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
n \<le> ?m \<Longrightarrow> v ?m = 0

goal (1 subgoal):
 1. v \<longlonglongrightarrow> 0
[PROOF STEP]
using lim_explicit
[PROOF STATE]
proof (prove)
using this:
n \<le> ?m \<Longrightarrow> v ?m = 0
?f \<longlonglongrightarrow> ?f0.0 = (\<forall>S. open S \<longrightarrow> ?f0.0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. ?f n \<in> S))

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
have "v (Suc n) \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v (Suc n) \<in> V
[PROOF STEP]
using V_def
[PROOF STATE]
proof (prove)
using this:
V = {v n |n. 0 < n}

goal (1 subgoal):
 1. v (Suc n) \<in> V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v (Suc n) \<in> V

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v (Suc n) \<in> V

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
have "v (Suc n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v (Suc n) = 0
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
n \<le> ?m \<Longrightarrow> v ?m = 0

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v (Suc n) \<in> V
v (Suc n) = 0
[PROOF STEP]
have "Inf V \<le> 0"
[PROOF STATE]
proof (prove)
using this:
v (Suc n) \<in> V
v (Suc n) = 0

goal (1 subgoal):
 1. Inf V \<le> 0
[PROOF STEP]
by (simp add: \<open>bdd_below V\<close> cInf_lower)
[PROOF STATE]
proof (state)
this:
Inf V \<le> 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf V \<le> 0
[PROOF STEP]
have "Inf V = 0"
[PROOF STATE]
proof (prove)
using this:
Inf V \<le> 0

goal (1 subgoal):
 1. Inf V = 0
[PROOF STEP]
using \<open>0 \<le> Inf V\<close>
[PROOF STATE]
proof (prove)
using this:
Inf V \<le> 0
0 \<le> Inf V

goal (1 subgoal):
 1. Inf V = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Inf V = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
 2. \<not> ?P \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf V = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Inf V = 0

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
using V_def v_def \<open>v \<longlonglongrightarrow> 0\<close>
[PROOF STATE]
proof (prove)
using this:
Inf V = 0
V = {v n |n. 0 < n}
v = (\<lambda>n. root n (u n))
v \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
assume "\<not> (\<exists>n. u n = 0)"
[PROOF STATE]
proof (state)
this:
\<nexists>n. u n = 0

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>n. u n = 0
[PROOF STEP]
have "u n > 0" for n
[PROOF STATE]
proof (prove)
using this:
\<nexists>n. u n = 0

goal (1 subgoal):
 1. 0 < u n
[PROOF STEP]
by (metis assms(1) less_eq_real_def)
[PROOF STATE]
proof (state)
this:
0 < u ?n

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
define w where "w n = ln (u n)" for n
[PROOF STATE]
proof (state)
this:
w ?n = ln (u ?n)

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
have express_vn: "v n = exp(w n/n)" if "n>0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
have "(exp(w n/n))^n = exp(n*(w n/n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (w n / real n) ^ n = exp (real n * (w n / real n))
[PROOF STEP]
by (metis exp_of_nat_mult)
[PROOF STATE]
proof (state)
this:
exp (w n / real n) ^ n = exp (real n * (w n / real n))

goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp (w n / real n) ^ n = exp (real n * (w n / real n))

goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
have "... = exp(w n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (real n * (w n / real n)) = exp (w n)
[PROOF STEP]
by (simp add: \<open>0 < n\<close>)
[PROOF STATE]
proof (state)
this:
exp (real n * (w n / real n)) = exp (w n)

goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp (real n * (w n / real n)) = exp (w n)

goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
have "... = u n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (w n) = u n
[PROOF STEP]
by (simp add: \<open>\<And>n. 0 < u n\<close> w_def)
[PROOF STATE]
proof (state)
this:
exp (w n) = u n

goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
exp (w n / real n) ^ n = u n
[PROOF STEP]
have "exp(w n/n) = root n (u n)"
[PROOF STATE]
proof (prove)
using this:
exp (w n / real n) ^ n = u n

goal (1 subgoal):
 1. exp (w n / real n) = root n (u n)
[PROOF STEP]
by (metis \<open>0 < n\<close> exp_ge_zero real_root_power_cancel)
[PROOF STATE]
proof (state)
this:
exp (w n / real n) = root n (u n)

goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
exp (w n / real n) = root n (u n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exp (w n / real n) = root n (u n)

goal (1 subgoal):
 1. v n = exp (w n / real n)
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
using this:
exp (w n / real n) = root n (u n)

goal (1 subgoal):
 1. root n (u n) = exp (w n / real n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v n = exp (w n / real n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> v ?n = exp (w ?n / real ?n)

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
have "eventually_subadditive w 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually_subadditive w 0
[PROOF STEP]
proof (rule eventually_subadditiveI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
fix m n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
have "w (m+n) = ln (u (m+n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w (m + n) = ln (u (m + n))
[PROOF STEP]
by (simp add: w_def)
[PROOF STATE]
proof (state)
this:
w (m + n) = ln (u (m + n))

goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w (m + n) = ln (u (m + n))

goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
have "... \<le> ln(u m * u n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (u (m + n)) \<le> ln (u m * u n)
[PROOF STEP]
by (meson \<open>\<And>n. 0 < u n\<close> assms(2) zero_less_mult_iff ln_le_cancel_iff)
[PROOF STATE]
proof (state)
this:
ln (u (m + n)) \<le> ln (u m * u n)

goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln (u (m + n)) \<le> ln (u m * u n)

goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
have "... = ln(u m) + ln(u n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (u m * u n) = ln (u m) + ln (u n)
[PROOF STEP]
by (simp add: \<open>\<And>n. 0 < u n\<close> ln_mult)
[PROOF STATE]
proof (state)
this:
ln (u m * u n) = ln (u m) + ln (u n)

goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln (u m * u n) = ln (u m) + ln (u n)

goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
have "... = w m + w n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (u m) + ln (u n) = w m + w n
[PROOF STEP]
by (simp add: w_def)
[PROOF STATE]
proof (state)
this:
ln (u m) + ln (u n) = w m + w n

goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> w (m + n) \<le> w m + w n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w (m + n) \<le> w m + w n
[PROOF STEP]
show "w (m+n) \<le> w m + w n"
[PROOF STATE]
proof (prove)
using this:
w (m + n) \<le> w m + w n

goal (1 subgoal):
 1. w (m + n) \<le> w m + w n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
w (m + n) \<le> w m + w n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eventually_subadditive w 0

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
define l where "l = Inf V"
[PROOF STATE]
proof (state)
this:
l = Inf V

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = Inf V
[PROOF STEP]
have "v n\<ge>l" if "n > 0" for n
[PROOF STATE]
proof (prove)
using this:
l = Inf V

goal (1 subgoal):
 1. l \<le> v n
[PROOF STEP]
using V_def that
[PROOF STATE]
proof (prove)
using this:
l = Inf V
V = {v n |n. 0 < n}
0 < n

goal (1 subgoal):
 1. l \<le> v n
[PROOF STEP]
by (metis (mono_tags, lifting) \<open>bdd_below V\<close> cInf_lower mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> l \<le> v ?n

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?n \<Longrightarrow> l \<le> v ?n
[PROOF STEP]
have lower: "eventually (\<lambda>n. a < v n) sequentially" if "a < l" for a
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> l \<le> v ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. a < v n
[PROOF STEP]
by (meson that dual_order.strict_trans1 eventually_at_top_dense)
[PROOF STATE]
proof (state)
this:
?a < l \<Longrightarrow> \<forall>\<^sub>F n in sequentially. ?a < v n

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
have upper: "eventually (\<lambda>n. a > v n) sequentially" if "a > l" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
obtain t where "t\<in>V" "t < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> V; t < a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>V \<noteq> {}\<close> cInf_lessD l_def \<open>a>l\<close>
[PROOF STATE]
proof (prove)
using this:
V \<noteq> {}
\<lbrakk>?X \<noteq> {}; Inf ?X < ?z\<rbrakk> \<Longrightarrow> \<exists>x\<in>?X. x < ?z
l = Inf V
l < a

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> V; t < a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> V
t < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> V
t < a
[PROOF STEP]
have "t > 0"
[PROOF STATE]
proof (prove)
using this:
t \<in> V
t < a

goal (1 subgoal):
 1. 0 < t
[PROOF STEP]
using V_def \<open>\<And>n. 0 < u n\<close> v_def
[PROOF STATE]
proof (prove)
using this:
t \<in> V
t < a
V = {v n |n. 0 < n}
0 < u ?n
v = (\<lambda>n. root n (u n))

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

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < t
[PROOF STEP]
have "a/t > 1"
[PROOF STATE]
proof (prove)
using this:
0 < t

goal (1 subgoal):
 1. 1 < a / t
[PROOF STEP]
using \<open>t<a\<close>
[PROOF STATE]
proof (prove)
using this:
0 < t
t < a

goal (1 subgoal):
 1. 1 < a / t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < a / t

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
define e where "e = ln(a/t)/2"
[PROOF STATE]
proof (state)
this:
e = ln (a / t) / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
have "e > 0" "e < ln(a/t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < e &&& e < ln (a / t)
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < ln (a / t) / 2 &&& ln (a / t) / 2 < ln (a / t)
[PROOF STEP]
by (simp_all add: \<open>1 < a / t\<close> ln_gt_zero)
[PROOF STATE]
proof (state)
this:
0 < e
e < ln (a / t)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < e
e < ln (a / t)
[PROOF STEP]
have "exp(e) < a/t"
[PROOF STATE]
proof (prove)
using this:
0 < e
e < ln (a / t)

goal (1 subgoal):
 1. exp e < a / t
[PROOF STEP]
by (metis \<open>1 < a / t\<close> exp_less_cancel_iff exp_ln less_trans zero_less_one)
[PROOF STATE]
proof (state)
this:
exp e < a / t

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
obtain n where "n>0" "t = v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>0 < n; t = v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using V_def v_def \<open>t \<in> V\<close>
[PROOF STATE]
proof (prove)
using this:
V = {v n |n. 0 < n}
v = (\<lambda>n. root n (u n))
t \<in> V

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>0 < n; t = v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < n
t = v n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
with \<open>0 < t\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < t
0 < n
t = v n
[PROOF STEP]
have "v n * exp(e) < a"
[PROOF STATE]
proof (prove)
using this:
0 < t
0 < n
t = v n

goal (1 subgoal):
 1. v n * exp e < a
[PROOF STEP]
using \<open>exp(e) < a/t\<close>
[PROOF STATE]
proof (prove)
using this:
0 < t
0 < n
t = v n
exp e < a / t

goal (1 subgoal):
 1. v n * exp e < a
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
v n * exp e < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
obtain N where *: "N>0" "\<And>m. m\<ge>N \<Longrightarrow> w m/m < w n/n + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<lbrakk>0 < N; \<And>m. N \<le> m \<Longrightarrow> w m / real m < w n / real n + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eventually_subadditive_ineq[OF \<open>eventually_subadditive w 0\<close>] \<open>0 < n\<close> \<open>e>0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?e; 0 < ?n\<rbrakk> \<Longrightarrow> \<exists>N>0. \<forall>m\<ge>N. w m / real m < w ?n / real ?n + ?e
0 < n
0 < e

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>0 < N; \<And>m. N \<le> m \<Longrightarrow> w m / real m < w n / real n + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < N
N \<le> ?m \<Longrightarrow> w ?m / real ?m < w n / real n + e

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
have "v m < a" if "m \<ge> N" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v m < a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v m < a
[PROOF STEP]
have "m>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < m
[PROOF STEP]
using that \<open>N>0\<close>
[PROOF STATE]
proof (prove)
using this:
N \<le> m
0 < N

goal (1 subgoal):
 1. 0 < m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < m

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
have "w m/m < w n/n + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w m / real m < w n / real n + e
[PROOF STEP]
by (simp add: \<open>N \<le> m\<close> *)
[PROOF STATE]
proof (state)
this:
w m / real m < w n / real n + e

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w m / real m < w n / real n + e
[PROOF STEP]
have "exp(w m/m) < exp(w n/n + e)"
[PROOF STATE]
proof (prove)
using this:
w m / real m < w n / real n + e

goal (1 subgoal):
 1. exp (w m / real m) < exp (w n / real n + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exp (w m / real m) < exp (w n / real n + e)

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp (w m / real m) < exp (w n / real n + e)

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
have "... = exp(w n/n) * exp(e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (w n / real n + e) = exp (w n / real n) * exp e
[PROOF STEP]
by (simp add: mult_exp_exp)
[PROOF STATE]
proof (state)
this:
exp (w n / real n + e) = exp (w n / real n) * exp e

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
exp (w m / real m) < exp (w n / real n) * exp e
[PROOF STEP]
have "v m < v n * exp(e)"
[PROOF STATE]
proof (prove)
using this:
exp (w m / real m) < exp (w n / real n) * exp e

goal (1 subgoal):
 1. v m < v n * exp e
[PROOF STEP]
using express_vn \<open>m>0\<close> \<open>n>0\<close>
[PROOF STATE]
proof (prove)
using this:
exp (w m / real m) < exp (w n / real n) * exp e
0 < ?n \<Longrightarrow> v ?n = exp (w ?n / real ?n)
0 < m
0 < n

goal (1 subgoal):
 1. v m < v n * exp e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v m < v n * exp e

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v m < v n * exp e
[PROOF STEP]
show "v m < a"
[PROOF STATE]
proof (prove)
using this:
v m < v n * exp e

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
using \<open>v n * exp(e) < a\<close>
[PROOF STATE]
proof (prove)
using this:
v m < v n * exp e
v n * exp e < a

goal (1 subgoal):
 1. v m < a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v m < a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N \<le> ?m \<Longrightarrow> v ?m < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?m \<Longrightarrow> v ?m < a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> v ?m < a

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
using eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
N \<le> ?m \<Longrightarrow> v ?m < a
eventually ?P at_top = (\<exists>N. \<forall>n\<ge>N. ?P n)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. v n < a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. v n < a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l < ?a \<Longrightarrow> \<forall>\<^sub>F n in sequentially. v n < ?a

goal (1 subgoal):
 1. \<nexists>n. u n = 0 \<Longrightarrow> (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
using lower upper
[PROOF STATE]
proof (prove)
using this:
?a < l \<Longrightarrow> \<forall>\<^sub>F n in sequentially. ?a < v n
l < ?a \<Longrightarrow> \<forall>\<^sub>F n in sequentially. v n < ?a

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
unfolding v_def l_def V_def
[PROOF STATE]
proof (prove)
using this:
?a < Inf {root n (u n) |n. 0 < n} \<Longrightarrow> \<forall>\<^sub>F n in sequentially. ?a < root n (u n)
Inf {root n (u n) |n. 0 < n} < ?a \<Longrightarrow> \<forall>\<^sub>F n in sequentially. root n (u n) < ?a

goal (1 subgoal):
 1. (\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}
[PROOF STEP]
by (simp add: order_tendsto_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. root n (u n)) \<longlonglongrightarrow> Inf {root n (u n) |n. 0 < n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spectral_radius_aux:
  fixes x::"'a::real_normed_algebra_1"
  defines "V \<equiv> {root n (norm(x^n))| n. n>0}"
  shows "\<And>t. t\<in>V \<Longrightarrow> t \<ge> spectral_radius x"
        "\<And>t. t\<in>V \<Longrightarrow> t \<ge> 0"
        "bdd_below V"
        "V \<noteq> {}"
        "Inf V \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>t. t \<in> V \<Longrightarrow> spectral_radius x \<le> t) &&& (\<And>t. t \<in> V \<Longrightarrow> 0 \<le> t)) &&& bdd_below V &&& V \<noteq> {} &&& 0 \<le> Inf V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t. t \<in> V \<Longrightarrow> spectral_radius x \<le> t
 2. \<And>t. t \<in> V \<Longrightarrow> 0 \<le> t
 3. bdd_below V
 4. V \<noteq> {}
 5. 0 \<le> Inf V
[PROOF STEP]
show "V\<noteq>{}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {}
[PROOF STEP]
using V_def
[PROOF STATE]
proof (prove)
using this:
V \<equiv> {root n (norm (x ^ n)) |n. 0 < n}

goal (1 subgoal):
 1. V \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V \<noteq> {}

goal (4 subgoals):
 1. \<And>t. t \<in> V \<Longrightarrow> spectral_radius x \<le> t
 2. \<And>t. t \<in> V \<Longrightarrow> 0 \<le> t
 3. bdd_below V
 4. 0 \<le> Inf V
[PROOF STEP]
show *: "t \<ge> 0" if "t \<in> V" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> t
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
t \<in> V

goal (1 subgoal):
 1. 0 \<le> t
[PROOF STEP]
unfolding V_def
[PROOF STATE]
proof (prove)
using this:
t \<in> {root n (norm (x ^ n)) |n. 0 < n}

goal (1 subgoal):
 1. 0 \<le> t
[PROOF STEP]
using real_root_pos_pos_le
[PROOF STATE]
proof (prove)
using this:
t \<in> {root n (norm (x ^ n)) |n. 0 < n}
0 \<le> ?x \<Longrightarrow> 0 \<le> root ?n ?x

goal (1 subgoal):
 1. 0 \<le> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?t \<in> V \<Longrightarrow> 0 \<le> ?t

goal (3 subgoals):
 1. \<And>t. t \<in> V \<Longrightarrow> spectral_radius x \<le> t
 2. bdd_below V
 3. 0 \<le> Inf V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t \<in> V \<Longrightarrow> 0 \<le> ?t
[PROOF STEP]
show "bdd_below V"
[PROOF STATE]
proof (prove)
using this:
?t \<in> V \<Longrightarrow> 0 \<le> ?t

goal (1 subgoal):
 1. bdd_below V
[PROOF STEP]
by (meson bdd_below_def)
[PROOF STATE]
proof (state)
this:
bdd_below V

goal (2 subgoals):
 1. \<And>t. t \<in> V \<Longrightarrow> spectral_radius x \<le> t
 2. 0 \<le> Inf V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bdd_below V
[PROOF STEP]
show "Inf V \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
bdd_below V

goal (1 subgoal):
 1. 0 \<le> Inf V
[PROOF STEP]
by (simp add: \<open>V \<noteq> {}\<close> * cInf_greatest)
[PROOF STATE]
proof (state)
this:
0 \<le> Inf V

goal (1 subgoal):
 1. \<And>t. t \<in> V \<Longrightarrow> spectral_radius x \<le> t
[PROOF STEP]
show "\<And>t. t\<in>V \<Longrightarrow> t \<ge> spectral_radius x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> V \<Longrightarrow> spectral_radius x \<le> t
[PROOF STEP]
by (metis (mono_tags, lifting) \<open>bdd_below V\<close> assms cInf_lower spectral_radius_def)
[PROOF STATE]
proof (state)
this:
?t \<in> V \<Longrightarrow> spectral_radius x \<le> ?t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spectral_radius_nonneg [simp]:
  "spectral_radius x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> spectral_radius x
[PROOF STEP]
by (simp add: spectral_radius_aux(5) spectral_radius_def)


[STATEMENT]
lemma spectral_radius_upper_bound [simp]:
  "(spectral_radius x)^n \<le> norm(x^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spectral_radius x ^ n \<le> norm (x ^ n)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> spectral_radius x ^ n \<le> norm (x ^ n)
 2. \<not> ?P \<Longrightarrow> spectral_radius x ^ n \<le> norm (x ^ n)
[PROOF STEP]
assume "\<not>(n = 0)"
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> spectral_radius x ^ n \<le> norm (x ^ n)
 2. \<not> ?P \<Longrightarrow> spectral_radius x ^ n \<le> norm (x ^ n)
[PROOF STEP]
have "root n (norm(x^n)) \<ge> spectral_radius x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spectral_radius x \<le> root n (norm (x ^ n))
[PROOF STEP]
using spectral_radius_aux \<open>n \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
?t \<in> {root n (norm (?x ^ n)) |n. 0 < n} \<Longrightarrow> spectral_radius ?x \<le> ?t
?t \<in> {root n (norm (?x ^ n)) |n. 0 < n} \<Longrightarrow> 0 \<le> ?t
bdd_below {root n (norm (?x ^ n)) |n. 0 < n}
{root n (norm (?x ^ n)) |n. 0 < n} \<noteq> {}
0 \<le> Inf {root n (norm (?x ^ n)) |n. 0 < n}
n \<noteq> 0

goal (1 subgoal):
 1. spectral_radius x \<le> root n (norm (x ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
spectral_radius x \<le> root n (norm (x ^ n))

goal (2 subgoals):
 1. ?P \<Longrightarrow> spectral_radius x ^ n \<le> norm (x ^ n)
 2. \<not> ?P \<Longrightarrow> spectral_radius x ^ n \<le> norm (x ^ n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
spectral_radius x \<le> root n (norm (x ^ n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
spectral_radius x \<le> root n (norm (x ^ n))

goal (1 subgoal):
 1. spectral_radius x ^ n \<le> norm (x ^ n)
[PROOF STEP]
by (metis \<open>n \<noteq> 0\<close> spectral_radius_nonneg norm_ge_zero not_gr0 power_mono real_root_pow_pos2)
[PROOF STATE]
proof (state)
this:
spectral_radius x ^ n \<le> norm (x ^ n)

goal (1 subgoal):
 1. \<not> n \<noteq> 0 \<Longrightarrow> spectral_radius x ^ n \<le> norm (x ^ n)
[PROOF STEP]
qed (simp)


[STATEMENT]
lemma spectral_radius_limit:
  "(\<lambda>n. root n (norm(x^n))) \<longlonglongrightarrow> spectral_radius x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. root n (norm (x ^ n))) \<longlonglongrightarrow> spectral_radius x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. root n (norm (x ^ n))) \<longlonglongrightarrow> spectral_radius x
[PROOF STEP]
have "norm(x^(m+n)) \<le> norm(x^m) * norm(x^n)" for m n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x ^ (m + n)) \<le> norm (x ^ m) * norm (x ^ n)
[PROOF STEP]
by (simp add: power_add norm_mult_ineq)
[PROOF STATE]
proof (state)
this:
norm (x ^ (?m + ?n)) \<le> norm (x ^ ?m) * norm (x ^ ?n)

goal (1 subgoal):
 1. (\<lambda>n. root n (norm (x ^ n))) \<longlonglongrightarrow> spectral_radius x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (x ^ (?m + ?n)) \<le> norm (x ^ ?m) * norm (x ^ ?n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (x ^ (?m + ?n)) \<le> norm (x ^ ?m) * norm (x ^ ?n)

goal (1 subgoal):
 1. (\<lambda>n. root n (norm (x ^ n))) \<longlonglongrightarrow> spectral_radius x
[PROOF STEP]
unfolding spectral_radius_def
[PROOF STATE]
proof (prove)
using this:
norm (x ^ (?m + ?n)) \<le> norm (x ^ ?m) * norm (x ^ ?n)

goal (1 subgoal):
 1. (\<lambda>n. root n (norm (x ^ n))) \<longlonglongrightarrow> Inf {root n (norm (x ^ n)) |n. 0 < n}
[PROOF STEP]
using submultiplicative_converges
[PROOF STATE]
proof (prove)
using this:
norm (x ^ (?m + ?n)) \<le> norm (x ^ ?m) * norm (x ^ ?n)
\<lbrakk>\<And>n. 0 \<le> ?u n; \<And>m n. ?u (m + n) \<le> ?u m * ?u n\<rbrakk> \<Longrightarrow> (\<lambda>n. root n (?u n)) \<longlonglongrightarrow> Inf {root n (?u n) |n. 0 < n}

goal (1 subgoal):
 1. (\<lambda>n. root n (norm (x ^ n))) \<longlonglongrightarrow> Inf {root n (norm (x ^ n)) |n. 0 < n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. root n (norm (x ^ n))) \<longlonglongrightarrow> spectral_radius x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_emptyI:
  "m \<subseteq>\<^sub>m Map.empty" if "\<And> x. m x = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
m ?x = None

goal (1 subgoal):
 1. m \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
unfolding map_le_def
[PROOF STATE]
proof (prove)
using this:
m ?x = None

goal (1 subgoal):
 1. \<forall>a\<in>dom m. m a = None
[PROOF STEP]
by auto


[STATEMENT]
lemma result_of_return[simp]:
  "result_of (Heap_Monad.return x) h = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. result_of (return x) h = x
[PROOF STEP]
by (simp add: execute_simps)


[STATEMENT]
lemma get_result_of_lookup:
  "result_of (!r) heap = x" if "Ref.get heap r = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. result_of (!r) heap = x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Ref.get heap r = x

goal (1 subgoal):
 1. result_of (!r) heap = x
[PROOF STEP]
by (auto simp: execute_simps)


[STATEMENT]
lemma success_empty[intro]:
  "success mem_empty heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success local.mem_empty heap
[PROOF STEP]
unfolding mem_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (Array.new size None) heap
[PROOF STEP]
by (auto intro: success_intros)


[STATEMENT]
lemma length_mem_empty:
  "Array.length
    (heap_of (mem_empty:: (('b :: heap) option array) Heap) h)
    (result_of (mem_empty :: ('b option array) Heap) h) = size"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length (heap_of local.mem_empty h) (result_of local.mem_empty h) = size
[PROOF STEP]
unfolding mem_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length (heap_of (Array.new size None) h) (result_of (Array.new size None) h) = size
[PROOF STEP]
by (auto simp: execute_simps Array.length_alloc)


[STATEMENT]
lemma nth_mem_empty:
  "result_of
    (Array.nth (result_of (mem_empty :: ('b option array) Heap) h) i)
    (heap_of (mem_empty :: (('b :: heap) option array) Heap) h) = None" if "i < size"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. result_of (Array.nth (result_of local.mem_empty h) i) (heap_of local.mem_empty h) = None
[PROOF STEP]
apply (subst execute_nth(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < Array.length (heap_of local.mem_empty h) (result_of local.mem_empty h)
 2. fst (the (Some (Array.get (heap_of local.mem_empty h) (result_of local.mem_empty h) ! i, heap_of local.mem_empty h))) = None
[PROOF STEP]
apply (simp add: length_mem_empty that)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (Some (Array.get (heap_of local.mem_empty h) (result_of local.mem_empty h) ! i, heap_of local.mem_empty h))) = None
[PROOF STEP]
apply (simp add: execute_simps mem_empty_def Array.get_alloc that)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma execute_bind_success':
  assumes "success f h" "execute (f \<bind> g) h = Some (y, h'')"
  obtains x h' where "execute f h = Some (x, h')" "execute (g x) h' = Some (y, h'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x h'. \<lbrakk>execute f h = Some (x, h'); execute (g x) h' = Some (y, h'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
success f h
execute (f \<bind> g) h = Some (y, h'')

goal (1 subgoal):
 1. (\<And>x h'. \<lbrakk>execute f h = Some (x, h'); execute (g x) h' = Some (y, h'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: execute_simps elim: successE)


[STATEMENT]
lemma success_bind_I:
  assumes "success f h"
    and "\<And> x h'. execute f h = Some (x, h') \<Longrightarrow> success (g x) h'"
  shows "success (f \<bind> g) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (f \<bind> g) h
[PROOF STEP]
by (rule successE[OF assms(1)]) (auto elim: assms(2) intro: success_bind_executeI)


[STATEMENT]
lemma alloc_pair_alloc:
  "Ref.get heap' r1 = a" "Ref.get heap' r2 = b"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ref.get heap' r1 = a &&& Ref.get heap' r2 = b
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair a b) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. Ref.get heap' r1 = a &&& Ref.get heap' r2 = b
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
using this:
execute (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. Ref.get heap' r1 = a &&& Ref.get heap' r2 = b
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF success_refI])
     (metis Ref.get_alloc fst_conv get_alloc_neq next_present present_alloc_neq snd_conv)+


[STATEMENT]
lemma alloc_pairD1:
  "r =!= r1 \<and> r =!= r2 \<and> Ref.present heap' r"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')" "Ref.present heap r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r =!= r1 \<and> r =!= r2 \<and> Ref.present heap' r
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair a b) heap = Some ((r1, r2), heap')
Ref.present heap r

goal (1 subgoal):
 1. r =!= r1 \<and> r =!= r2 \<and> Ref.present heap' r
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
using this:
execute (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap = Some ((r1, r2), heap')
Ref.present heap r

goal (1 subgoal):
 1. r =!= r1 \<and> r =!= r2 \<and> Ref.present heap' r
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF success_refI])
     (metis next_fresh noteq_I Ref.present_alloc snd_conv)+


[STATEMENT]
lemma alloc_pairD2:
  "r1 =!= r2 \<and> Ref.present heap' r2 \<and> Ref.present heap' r1"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r1 =!= r2 \<and> Ref.present heap' r2 \<and> Ref.present heap' r1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair a b) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. r1 =!= r2 \<and> Ref.present heap' r2 \<and> Ref.present heap' r1
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
using this:
execute (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. r1 =!= r2 \<and> Ref.present heap' r2 \<and> Ref.present heap' r1
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF success_refI])
     (metis next_fresh next_present noteq_I Ref.present_alloc snd_conv)+


[STATEMENT]
lemma alloc_pairD3:
  "Array.present heap' r"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')" "Array.present heap r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.present heap' r
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair a b) heap = Some ((r1, r2), heap')
Array.present heap r

goal (1 subgoal):
 1. Array.present heap' r
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
using this:
execute (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap = Some ((r1, r2), heap')
Array.present heap r

goal (1 subgoal):
 1. Array.present heap' r
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF success_refI])
     (metis array_present_alloc snd_conv)


[STATEMENT]
lemma alloc_pairD4:
  "Ref.get heap' r = x"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')"
     "Ref.get heap r = x" "Ref.present heap r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ref.get heap' r = x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair a b) heap = Some ((r1, r2), heap')
Ref.get heap r = x
Ref.present heap r

goal (1 subgoal):
 1. Ref.get heap' r = x
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
using this:
execute (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap = Some ((r1, r2), heap')
Ref.get heap r = x
Ref.present heap r

goal (1 subgoal):
 1. Ref.get heap' r = x
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF success_refI])
     (metis Ref.not_present_alloc Ref.present_alloc get_alloc_neq noteq_I snd_conv)


[STATEMENT]
lemma alloc_pair_array_get:
  "Array.get heap' r = x"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')" "Array.get heap r = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.get heap' r = x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair a b) heap = Some ((r1, r2), heap')
Array.get heap r = x

goal (1 subgoal):
 1. Array.get heap' r = x
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
using this:
execute (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap = Some ((r1, r2), heap')
Array.get heap r = x

goal (1 subgoal):
 1. Array.get heap' r = x
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF success_refI])
 (metis array_get_alloc snd_conv)


[STATEMENT]
lemma alloc_pair_array_length:
  "Array.length heap' r = Array.length heap r"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length heap' r = Array.length heap r
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair a b) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. Array.length heap' r = Array.length heap r
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
using this:
execute (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. Array.length heap' r = Array.length heap r
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF success_refI])
     (metis Ref.length_alloc snd_conv)


[STATEMENT]
lemma alloc_pair_nth:
  "result_of (Array.nth r i) heap' = result_of (Array.nth r i) heap"
  if "execute (alloc_pair a b) heap = Some ((r1, r2), heap')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. result_of (Array.nth r i) heap' = result_of (Array.nth r i) heap
[PROOF STEP]
using alloc_pair_array_get[OF that(1) HOL.refl, of r] alloc_pair_array_length[OF that(1), of r]
[PROOF STATE]
proof (prove)
using this:
Array.get heap' r = Array.get heap r
Array.length heap' r = Array.length heap r

goal (1 subgoal):
 1. result_of (Array.nth r i) heap' = result_of (Array.nth r i) heap
[PROOF STEP]
by (cases "(\<lambda>h. i < Array.length h r) heap"; simp add: execute_simps Array.nth_def)


[STATEMENT]
lemma succes_alloc_pair[intro]:
  "success (alloc_pair a b) heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (alloc_pair a b) heap
[PROOF STEP]
unfolding alloc_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (ref a \<bind> (\<lambda>r1. ref b \<bind> (\<lambda>r2. return (r1, r2)))) heap
[PROOF STEP]
by (auto intro: success_intros success_bind_I)


[STATEMENT]
lemma init_state_inner_alloc:
  assumes
    "execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "Ref.get heap' k_ref1 = k1" "Ref.get heap' k_ref2 = k2"
    "Ref.get heap' m_ref1 = m1" "Ref.get heap' m_ref2 = m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ref.get heap' k_ref1 = k1 &&& Ref.get heap' k_ref2 = k2) &&& Ref.get heap' m_ref1 = m1 &&& Ref.get heap' m_ref2 = m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. (Ref.get heap' k_ref1 = k1 &&& Ref.get heap' k_ref2 = k2) &&& Ref.get heap' m_ref1 = m1 &&& Ref.get heap' m_ref2 = m2
[PROOF STEP]
unfolding init_state_inner_def
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair k1 k2 \<bind> (\<lambda>(k_ref1, k_ref2). alloc_pair m1 m2 \<bind> (\<lambda>(m_ref1, m_ref2). return (k_ref1, k_ref2, m_ref1, m_ref2)))) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. (Ref.get heap' k_ref1 = k1 &&& Ref.get heap' k_ref2 = k2) &&& Ref.get heap' m_ref1 = m1 &&& Ref.get heap' m_ref2 = m2
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF succes_alloc_pair])
     (auto intro: alloc_pair_alloc dest: alloc_pairD2 elim: alloc_pairD4)


[STATEMENT]
lemma init_state_inner_distinct:
  assumes
    "execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "m_ref1 =!= m_ref2 \<and> m_ref1 =!= k_ref1 \<and> m_ref1 =!= k_ref2 \<and> m_ref2 =!= k_ref1
   \<and> m_ref2 =!= k_ref2 \<and> k_ref1 =!= k_ref2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_ref1 =!= m_ref2 \<and> m_ref1 =!= k_ref1 \<and> m_ref1 =!= k_ref2 \<and> m_ref2 =!= k_ref1 \<and> m_ref2 =!= k_ref2 \<and> k_ref1 =!= k_ref2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. m_ref1 =!= m_ref2 \<and> m_ref1 =!= k_ref1 \<and> m_ref1 =!= k_ref2 \<and> m_ref2 =!= k_ref1 \<and> m_ref2 =!= k_ref2 \<and> k_ref1 =!= k_ref2
[PROOF STEP]
unfolding init_state_inner_def
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair k1 k2 \<bind> (\<lambda>(k_ref1, k_ref2). alloc_pair m1 m2 \<bind> (\<lambda>(m_ref1, m_ref2). return (k_ref1, k_ref2, m_ref1, m_ref2)))) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. m_ref1 =!= m_ref2 \<and> m_ref1 =!= k_ref1 \<and> m_ref1 =!= k_ref2 \<and> m_ref2 =!= k_ref1 \<and> m_ref2 =!= k_ref2 \<and> k_ref1 =!= k_ref2
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF succes_alloc_pair])
     (blast dest: alloc_pairD1 alloc_pairD2 intro: noteq_sym)+


[STATEMENT]
lemma init_state_inner_present:
  assumes
    "execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "Ref.present heap' k_ref1" "Ref.present heap' k_ref2"
    "Ref.present heap' m_ref1" "Ref.present heap' m_ref2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ref.present heap' k_ref1 &&& Ref.present heap' k_ref2) &&& Ref.present heap' m_ref1 &&& Ref.present heap' m_ref2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. (Ref.present heap' k_ref1 &&& Ref.present heap' k_ref2) &&& Ref.present heap' m_ref1 &&& Ref.present heap' m_ref2
[PROOF STEP]
unfolding init_state_inner_def
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair k1 k2 \<bind> (\<lambda>(k_ref1, k_ref2). alloc_pair m1 m2 \<bind> (\<lambda>(m_ref1, m_ref2). return (k_ref1, k_ref2, m_ref1, m_ref2)))) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. (Ref.present heap' k_ref1 &&& Ref.present heap' k_ref2) &&& Ref.present heap' m_ref1 &&& Ref.present heap' m_ref2
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF succes_alloc_pair])
     (blast dest: alloc_pairD1 alloc_pairD2)+


[STATEMENT]
lemma inite_state_inner_present':
  assumes
    "execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
    "Array.present heap a"
  shows
    "Array.present heap' a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.present heap' a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (init_state_inner k1 k2 m1 m2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')
Array.present heap a

goal (1 subgoal):
 1. Array.present heap' a
[PROOF STEP]
unfolding init_state_inner_def
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair k1 k2 \<bind> (\<lambda>(k_ref1, k_ref2). alloc_pair m1 m2 \<bind> (\<lambda>(m_ref1, m_ref2). return (k_ref1, k_ref2, m_ref1, m_ref2)))) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')
Array.present heap a

goal (1 subgoal):
 1. Array.present heap' a
[PROOF STEP]
by (auto simp: execute_simps elim!: execute_bind_success'[OF succes_alloc_pair] alloc_pairD3)


[STATEMENT]
lemma succes_init_state_inner[intro]:
  "success (init_state_inner k1 k2 m1 m2) heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (init_state_inner k1 k2 m1 m2) heap
[PROOF STEP]
unfolding init_state_inner_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (alloc_pair k1 k2 \<bind> (\<lambda>(k_ref1, k_ref2). alloc_pair m1 m2 \<bind> (\<lambda>(m_ref1, m_ref2). return (k_ref1, k_ref2, m_ref1, m_ref2)))) heap
[PROOF STEP]
by (auto 4 3 intro: success_intros success_bind_I)


[STATEMENT]
lemma init_state_inner_nth:
  "result_of (Array.nth r i) heap' = result_of (Array.nth r i) heap"
  if "execute (init_state_inner k1 k2 m1 m2) heap = Some ((r1, r2), heap')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. result_of (Array.nth r i) heap' = result_of (Array.nth r i) heap
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute (init_state_inner k1 k2 m1 m2) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. result_of (Array.nth r i) heap' = result_of (Array.nth r i) heap
[PROOF STEP]
unfolding init_state_inner_def
[PROOF STATE]
proof (prove)
using this:
execute (alloc_pair k1 k2 \<bind> (\<lambda>(k_ref1, k_ref2). alloc_pair m1 m2 \<bind> (\<lambda>(m_ref1, m_ref2). return (k_ref1, k_ref2, m_ref1, m_ref2)))) heap = Some ((r1, r2), heap')

goal (1 subgoal):
 1. result_of (Array.nth r i) heap' = result_of (Array.nth r i) heap
[PROOF STEP]
by (auto simp: execute_simps alloc_pair_nth elim!: execute_bind_success'[OF succes_alloc_pair])


[STATEMENT]
lemma succes_init_state[intro]:
  "success (init_state k1 k2) heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (local.init_state k1 k2) heap
[PROOF STEP]
unfolding init_state_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap
[PROOF STEP]
by (auto intro: success_intros success_bind_I)


[STATEMENT]
lemma init_state_distinct:
  assumes
    "execute (init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "inv_distinct k_ref1 k_ref2 m_ref1 m_ref2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_distinct k_ref1 k_ref2 m_ref1 m_ref2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. inv_distinct k_ref1 k_ref2 m_ref1 m_ref2
[PROOF STEP]
unfolding init_state_def inv_distinct_def
[PROOF STATE]
proof (prove)
using this:
execute (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. m_ref1 =!= m_ref2 \<and> m_ref1 =!= k_ref1 \<and> m_ref1 =!= k_ref2 \<and> m_ref2 =!= k_ref1 \<and> m_ref2 =!= k_ref2 \<and> k_ref1 =!= k_ref2
[PROOF STEP]
by (elim execute_bind_success'[OF success_empty] init_state_inner_distinct)


[STATEMENT]
lemma init_state_present:
  assumes
    "execute (init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "Ref.present heap' k_ref1" "Ref.present heap' k_ref2"
    "Ref.present heap' m_ref1" "Ref.present heap' m_ref2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ref.present heap' k_ref1 &&& Ref.present heap' k_ref2) &&& Ref.present heap' m_ref1 &&& Ref.present heap' m_ref2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. (Ref.present heap' k_ref1 &&& Ref.present heap' k_ref2) &&& Ref.present heap' m_ref1 &&& Ref.present heap' m_ref2
[PROOF STEP]
unfolding init_state_def
[PROOF STATE]
proof (prove)
using this:
execute (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. (Ref.present heap' k_ref1 &&& Ref.present heap' k_ref2) &&& Ref.present heap' m_ref1 &&& Ref.present heap' m_ref2
[PROOF STEP]
by (auto
        simp: execute_simps elim!: execute_bind_success'[OF success_empty]
        dest: init_state_inner_present
     )


[STATEMENT]
lemma empty_present:
  "Array.present h' x" if "execute mem_empty heap = Some (x, h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.present h' x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute local.mem_empty heap = Some (x, h')

goal (1 subgoal):
 1. Array.present h' x
[PROOF STEP]
unfolding mem_empty_def
[PROOF STATE]
proof (prove)
using this:
execute (Array.new size None) heap = Some (x, h')

goal (1 subgoal):
 1. Array.present h' x
[PROOF STEP]
by (auto simp: execute_simps) (metis Array.present_alloc fst_conv snd_conv)


[STATEMENT]
lemma empty_present':
  "Array.present h' a" if "execute mem_empty heap = Some (x, h')" "Array.present heap a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.present h' a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
execute local.mem_empty heap = Some (x, h')
Array.present heap a

goal (1 subgoal):
 1. Array.present h' a
[PROOF STEP]
unfolding mem_empty_def
[PROOF STATE]
proof (prove)
using this:
execute (Array.new size None) heap = Some (x, h')
Array.present heap a

goal (1 subgoal):
 1. Array.present h' a
[PROOF STEP]
by (auto simp: execute_simps Array.present_def Array.alloc_def Array.set_def Let_def)


[STATEMENT]
lemma init_state_present2:
  assumes
    "execute (init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "Array.present heap' (Ref.get heap' m_ref1)" "Array.present heap' (Ref.get heap' m_ref2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.present heap' (Ref.get heap' m_ref1) &&& Array.present heap' (Ref.get heap' m_ref2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. Array.present heap' (Ref.get heap' m_ref1) &&& Array.present heap' (Ref.get heap' m_ref2)
[PROOF STEP]
unfolding init_state_def
[PROOF STATE]
proof (prove)
using this:
execute (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. Array.present heap' (Ref.get heap' m_ref1) &&& Array.present heap' (Ref.get heap' m_ref2)
[PROOF STEP]
by (auto 4 3
        simp: execute_simps init_state_inner_alloc elim!: execute_bind_success'[OF success_empty]
        dest: inite_state_inner_present' empty_present empty_present'
     )


[STATEMENT]
lemma init_state_neq:
  assumes
    "execute (init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "Ref.get heap' m_ref1 =!!= Ref.get heap' m_ref2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ref.get heap' m_ref1 =!!= Ref.get heap' m_ref2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. Ref.get heap' m_ref1 =!!= Ref.get heap' m_ref2
[PROOF STEP]
unfolding init_state_def
[PROOF STATE]
proof (prove)
using this:
execute (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. Ref.get heap' m_ref1 =!!= Ref.get heap' m_ref2
[PROOF STEP]
by (auto 4 3
        simp: execute_simps init_state_inner_alloc elim!: execute_bind_success'[OF success_empty]
        dest: inite_state_inner_present' empty_present empty_present'
     )
    (metis empty_present execute_new fst_conv mem_empty_def option.inject present_alloc_noteq)


[STATEMENT]
lemma present_alloc_get:
  "Array.get heap' a = Array.get heap a"
  if "Array.alloc xs heap = (a', heap')" "Array.present heap a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.get heap' a = Array.get heap a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Array.alloc xs heap = (a', heap')
Array.present heap a

goal (1 subgoal):
 1. Array.get heap' a = Array.get heap a
[PROOF STEP]
by (auto simp: Array.alloc_def Array.present_def Array.get_def Let_def Array.set_def)


[STATEMENT]
lemma init_state_length:
  assumes
    "execute (init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows
    "Array.length heap' (Ref.get heap' m_ref1) = size"
    "Array.length heap' (Ref.get heap' m_ref2) = size"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length heap' (Ref.get heap' m_ref1) = size &&& Array.length heap' (Ref.get heap' m_ref2) = size
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. Array.length heap' (Ref.get heap' m_ref1) = size &&& Array.length heap' (Ref.get heap' m_ref2) = size
[PROOF STEP]
unfolding init_state_def
[PROOF STATE]
proof (prove)
using this:
execute (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. Array.length heap' (Ref.get heap' m_ref1) = size &&& Array.length heap' (Ref.get heap' m_ref2) = size
[PROOF STEP]
apply (auto
        simp: execute_simps init_state_inner_alloc elim!: execute_bind_success'[OF success_empty]
        dest: inite_state_inner_present' empty_present empty_present'
     )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x h' xa h'a. \<lbrakk>execute local.mem_empty heap = Some (x, h'); execute local.mem_empty h' = Some (xa, h'a); execute (init_state_inner k1 k2 x xa) h'a = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')\<rbrakk> \<Longrightarrow> Array.length heap' x = size
 2. \<And>x h' xa h'a. \<lbrakk>execute local.mem_empty heap = Some (x, h'); execute local.mem_empty h' = Some (xa, h'a); execute (init_state_inner k1 k2 x xa) h'a = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')\<rbrakk> \<Longrightarrow> Array.length heap' xa = size
[PROOF STEP]
apply (auto
      simp: execute_simps init_state_inner_def alloc_pair_def mem_empty_def Array.length_def
      elim!: execute_bind_success'[OF success_refI]
     )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x h' xa h'a h'b h'c h'd. \<lbrakk>Array.alloc (replicate size None) heap = (x, h'); Array.alloc (replicate size None) h' = (xa, h'a); Ref.alloc k1 h'a = (k_ref1, h'b); Ref.alloc k2 h'b = (k_ref2, h'c); Ref.alloc x h'c = (m_ref1, h'd); Ref.alloc xa h'd = (m_ref2, heap')\<rbrakk> \<Longrightarrow> length (Array.get heap' x) = size
 2. \<And>x h' xa h'a h'b h'c h'd. \<lbrakk>Array.alloc (replicate size None) heap = (x, h'); Array.alloc (replicate size None) h' = (xa, h'a); Ref.alloc k1 h'a = (k_ref1, h'b); Ref.alloc k2 h'b = (k_ref2, h'c); Ref.alloc x h'c = (m_ref1, h'd); Ref.alloc xa h'd = (m_ref2, heap')\<rbrakk> \<Longrightarrow> length (Array.get heap' xa) = size
[PROOF STEP]
apply (metis
      Array.alloc_def Array.get_set_eq Array.present_alloc array_get_alloc fst_conv length_replicate
      present_alloc_get snd_conv
     )+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma init_state_inv:
  assumes
    "execute (init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')"
  shows "inv_pair_weak heap'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv_pair_weak heap'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. local.inv_pair_weak heap'
[PROOF STEP]
unfolding inv_pair_weak_def Let_def
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. Array.length heap' (Ref.get heap' m_ref1) = size \<and> Array.length heap' (Ref.get heap' m_ref2) = size \<and> Ref.present heap' k_ref1 \<and> Ref.present heap' k_ref2 \<and> Ref.present heap' m_ref1 \<and> Ref.present heap' m_ref2 \<and> Array.present heap' (Ref.get heap' m_ref1) \<and> Array.present heap' (Ref.get heap' m_ref2) \<and> Ref.get heap' m_ref1 =!!= Ref.get heap' m_ref2
[PROOF STEP]
by (auto intro:
      init_state_present init_state_present2 init_state_neq init_state_length
      init_state_distinct
     )


[STATEMENT]
lemma inv_pair_lengthD1:
  "Array.length heap (Ref.get heap m_ref1) = size" if "inv_pair_weak heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length heap (Ref.get heap m_ref1) = size
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
local.inv_pair_weak heap

goal (1 subgoal):
 1. Array.length heap (Ref.get heap m_ref1) = size
[PROOF STEP]
unfolding inv_pair_weak_def
[PROOF STATE]
proof (prove)
using this:
let m1 = Ref.get heap m_ref1; m2 = Ref.get heap m_ref2 in Array.length heap m1 = size \<and> Array.length heap m2 = size \<and> Ref.present heap k_ref1 \<and> Ref.present heap k_ref2 \<and> Ref.present heap m_ref1 \<and> Ref.present heap m_ref2 \<and> Array.present heap m1 \<and> Array.present heap m2 \<and> m1 =!!= m2

goal (1 subgoal):
 1. Array.length heap (Ref.get heap m_ref1) = size
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma inv_pair_lengthD2:
  "Array.length heap (Ref.get heap m_ref2) = size" if "inv_pair_weak heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length heap (Ref.get heap m_ref2) = size
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
local.inv_pair_weak heap

goal (1 subgoal):
 1. Array.length heap (Ref.get heap m_ref2) = size
[PROOF STEP]
unfolding inv_pair_weak_def
[PROOF STATE]
proof (prove)
using this:
let m1 = Ref.get heap m_ref1; m2 = Ref.get heap m_ref2 in Array.length heap m1 = size \<and> Array.length heap m2 = size \<and> Ref.present heap k_ref1 \<and> Ref.present heap k_ref2 \<and> Ref.present heap m_ref1 \<and> Ref.present heap m_ref2 \<and> Array.present heap m1 \<and> Array.present heap m2 \<and> m1 =!!= m2

goal (1 subgoal):
 1. Array.length heap (Ref.get heap m_ref2) = size
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma inv_pair_presentD:
  "Array.present heap (Ref.get heap m_ref1)" "Array.present heap (Ref.get heap m_ref2)"
  if "inv_pair_weak heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.present heap (Ref.get heap m_ref1) &&& Array.present heap (Ref.get heap m_ref2)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
local.inv_pair_weak heap

goal (1 subgoal):
 1. Array.present heap (Ref.get heap m_ref1) &&& Array.present heap (Ref.get heap m_ref2)
[PROOF STEP]
unfolding inv_pair_weak_def
[PROOF STATE]
proof (prove)
using this:
let m1 = Ref.get heap m_ref1; m2 = Ref.get heap m_ref2 in Array.length heap m1 = size \<and> Array.length heap m2 = size \<and> Ref.present heap k_ref1 \<and> Ref.present heap k_ref2 \<and> Ref.present heap m_ref1 \<and> Ref.present heap m_ref2 \<and> Array.present heap m1 \<and> Array.present heap m2 \<and> m1 =!!= m2

goal (1 subgoal):
 1. Array.present heap (Ref.get heap m_ref1) &&& Array.present heap (Ref.get heap m_ref2)
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma inv_pair_presentD2:
  "Ref.present heap m_ref1" "Ref.present heap m_ref2"
  "Ref.present heap k_ref1" "Ref.present heap k_ref2"
  if "inv_pair_weak heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ref.present heap m_ref1 &&& Ref.present heap m_ref2) &&& Ref.present heap k_ref1 &&& Ref.present heap k_ref2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
local.inv_pair_weak heap

goal (1 subgoal):
 1. (Ref.present heap m_ref1 &&& Ref.present heap m_ref2) &&& Ref.present heap k_ref1 &&& Ref.present heap k_ref2
[PROOF STEP]
unfolding inv_pair_weak_def
[PROOF STATE]
proof (prove)
using this:
let m1 = Ref.get heap m_ref1; m2 = Ref.get heap m_ref2 in Array.length heap m1 = size \<and> Array.length heap m2 = size \<and> Ref.present heap k_ref1 \<and> Ref.present heap k_ref2 \<and> Ref.present heap m_ref1 \<and> Ref.present heap m_ref2 \<and> Array.present heap m1 \<and> Array.present heap m2 \<and> m1 =!!= m2

goal (1 subgoal):
 1. (Ref.present heap m_ref1 &&& Ref.present heap m_ref2) &&& Ref.present heap k_ref1 &&& Ref.present heap k_ref2
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma inv_pair_not_eqD:
  "Ref.get heap m_ref1 =!!= Ref.get heap m_ref2" if "inv_pair_weak heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ref.get heap m_ref1 =!!= Ref.get heap m_ref2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
local.inv_pair_weak heap

goal (1 subgoal):
 1. Ref.get heap m_ref1 =!!= Ref.get heap m_ref2
[PROOF STEP]
unfolding inv_pair_weak_def
[PROOF STATE]
proof (prove)
using this:
let m1 = Ref.get heap m_ref1; m2 = Ref.get heap m_ref2 in Array.length heap m1 = size \<and> Array.length heap m2 = size \<and> Ref.present heap k_ref1 \<and> Ref.present heap k_ref2 \<and> Ref.present heap m_ref1 \<and> Ref.present heap m_ref2 \<and> Array.present heap m1 \<and> Array.present heap m2 \<and> m1 =!!= m2

goal (1 subgoal):
 1. Ref.get heap m_ref1 =!!= Ref.get heap m_ref2
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma run_state_state_of[simp]:
  "State_Monad.run_state (state_of p) m = the (execute p m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_state (state_of p) m = the (execute p m)
[PROOF STEP]
unfolding state_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_state (State (\<lambda>heap. the (execute p heap))) m = the (execute p m)
[PROOF STEP]
by simp


[STATEMENT]
lemma disjoint[simp]:
  "m_ref1 =!= m_ref2" "m_ref1 =!= k_ref1" "m_ref1 =!= k_ref2"
  "m_ref2 =!= k_ref1" "m_ref2 =!= k_ref2"
  "k_ref1 =!= k_ref2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m_ref1 =!= m_ref2 &&& m_ref1 =!= k_ref1 &&& m_ref1 =!= k_ref2) &&& m_ref2 =!= k_ref1 &&& m_ref2 =!= k_ref2 &&& k_ref1 =!= k_ref2
[PROOF STEP]
using inv_distinct
[PROOF STATE]
proof (prove)
using this:
inv_distinct k_ref1 k_ref2 m_ref1 m_ref2

goal (1 subgoal):
 1. (m_ref1 =!= m_ref2 &&& m_ref1 =!= k_ref1 &&& m_ref1 =!= k_ref2) &&& m_ref2 =!= k_ref1 &&& m_ref2 =!= k_ref2 &&& k_ref1 =!= k_ref2
[PROOF STEP]
unfolding inv_distinct_def
[PROOF STATE]
proof (prove)
using this:
m_ref1 =!= m_ref2 \<and> m_ref1 =!= k_ref1 \<and> m_ref1 =!= k_ref2 \<and> m_ref2 =!= k_ref1 \<and> m_ref2 =!= k_ref2 \<and> k_ref1 =!= k_ref2

goal (1 subgoal):
 1. (m_ref1 =!= m_ref2 &&& m_ref1 =!= k_ref1 &&& m_ref1 =!= k_ref2) &&& m_ref2 =!= k_ref1 &&& m_ref2 =!= k_ref2 &&& k_ref1 =!= k_ref2
[PROOF STEP]
by auto


[STATEMENT]
lemma [simp]:
  "Array.get (snd (Array.alloc xs heap)) a = Array.get heap a" if "Array.present heap a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.get (snd (Array.alloc xs heap)) a = Array.get heap a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Array.present heap a

goal (1 subgoal):
 1. Array.get (snd (Array.alloc xs heap)) a = Array.get heap a
[PROOF STEP]
unfolding Array.alloc_def Array.present_def
[PROOF STATE]
proof (prove)
using this:
addr_of_array a < lim heap

goal (1 subgoal):
 1. Array.get (snd (let l = lim heap; r = Array l in Let (Array.set r xs (heap\<lparr>lim := l + 1\<rparr>)) (Pair r))) a = Array.get heap a
[PROOF STEP]
apply (simp add: Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_array a < lim heap \<Longrightarrow> Array.get (Array.set (Array (lim heap)) xs (heap\<lparr>lim := Suc (lim heap)\<rparr>)) a = Array.get heap a
[PROOF STEP]
apply (subst Array.get_set_neq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. addr_of_array a < lim heap \<Longrightarrow> a =!!= Array (lim heap)
 2. addr_of_array a < lim heap \<Longrightarrow> Array.get (heap\<lparr>lim := Suc (lim heap)\<rparr>) a = Array.get heap a
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_array a < lim heap \<Longrightarrow> a =!!= Array (lim heap)
[PROOF STEP]
by (simp add: Array.noteq_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_array a < lim heap \<Longrightarrow> Array.get (heap\<lparr>lim := Suc (lim heap)\<rparr>) a = Array.get heap a
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_array a < lim heap \<Longrightarrow> Array.get (heap\<lparr>lim := Suc (lim heap)\<rparr>) a = Array.get heap a
[PROOF STEP]
unfolding Array.get_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_array a < lim heap \<Longrightarrow> map from_nat (arrays (heap\<lparr>lim := Suc (lim heap)\<rparr>) TYPEREP('a) (addr_of_array a)) = map from_nat (arrays heap TYPEREP('a) (addr_of_array a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]:
  "Ref.get (snd (Array.alloc xs heap)) r = Ref.get heap r" if "Ref.present heap r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ref.get (snd (Array.alloc xs heap)) r = Ref.get heap r
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Ref.present heap r

goal (1 subgoal):
 1. Ref.get (snd (Array.alloc xs heap)) r = Ref.get heap r
[PROOF STEP]
unfolding Array.alloc_def Ref.present_def
[PROOF STATE]
proof (prove)
using this:
addr_of_ref r < lim heap

goal (1 subgoal):
 1. Ref.get (snd (let l = lim heap; r = Array l in Let (Array.set r xs (heap\<lparr>lim := l + 1\<rparr>)) (Pair r))) r = Ref.get heap r
[PROOF STEP]
by (simp add: Let_def Ref.get_def Array.set_def)


[STATEMENT]
lemma alloc_present:
  "Array.present (snd (Array.alloc xs heap)) a" if "Array.present heap a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.present (snd (Array.alloc xs heap)) a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Array.present heap a

goal (1 subgoal):
 1. Array.present (snd (Array.alloc xs heap)) a
[PROOF STEP]
unfolding Array.present_def Array.alloc_def
[PROOF STATE]
proof (prove)
using this:
addr_of_array a < lim heap

goal (1 subgoal):
 1. addr_of_array a < lim (snd (let l = lim heap; r = Array l in Let (Array.set r xs (heap\<lparr>lim := l + 1\<rparr>)) (Pair r)))
[PROOF STEP]
by (simp add: Let_def Array.set_def)


[STATEMENT]
lemma alloc_present':
  "Ref.present (snd (Array.alloc xs heap)) r" if "Ref.present heap r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ref.present (snd (Array.alloc xs heap)) r
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Ref.present heap r

goal (1 subgoal):
 1. Ref.present (snd (Array.alloc xs heap)) r
[PROOF STEP]
unfolding Ref.present_def Array.alloc_def
[PROOF STATE]
proof (prove)
using this:
addr_of_ref r < lim heap

goal (1 subgoal):
 1. addr_of_ref r < lim (snd (let l = lim heap; r = Array l in Let (Array.set r xs (heap\<lparr>lim := l + 1\<rparr>)) (Pair r)))
[PROOF STEP]
by (simp add: Let_def Array.set_def)


[STATEMENT]
lemma length_get_upd[simp]:
  "length (Array.get (Array.update a i x heap) r) = length (Array.get heap r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Array.get (Array.update a i x heap) r) = length (Array.get heap r)
[PROOF STEP]
unfolding Array.get_def Array.update_def Array.set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map from_nat (arrays (arrays_update (\<lambda>h. h(TYPEREP('b) := (h TYPEREP('b))(addr_of_array a := map to_nat ((map from_nat (arrays heap TYPEREP('b) (addr_of_array a)))[i := x])))) heap) TYPEREP('a) (addr_of_array r))) = length (map from_nat (arrays heap TYPEREP('a) (addr_of_array r)))
[PROOF STEP]
by simp


[STATEMENT]
lemma rel_state_ofI:
  "rel_state (=) (state_of m) m" if
  "\<forall> heap. inv_pair_weak heap \<longrightarrow> success m heap"
  "lift_p inv_pair_weak m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.rel_state (=) (state_of m) m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. local.inv_pair_weak heap \<longrightarrow> success m heap
State_Heap.lift_p local.inv_pair_weak m

goal (1 subgoal):
 1. local.rel_state (=) (state_of m) m
[PROOF STEP]
unfolding rel_state_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. local.inv_pair_weak heap \<longrightarrow> success m heap
State_Heap.lift_p local.inv_pair_weak m

goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> (case run_state (state_of m) heap of (v1, heap1) \<Rightarrow> case execute m heap of None \<Rightarrow> False | Some (v2, heap2) \<Rightarrow> v1 = v2 \<and> heap1 = heap2 \<and> local.inv_pair_weak heap2)
[PROOF STEP]
by (auto split: option.split intro: lift_p_P'' simp: success_def)


[STATEMENT]
lemma inv_pair_iff:
  "inv_pair_weak = inv_pair"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv_pair_weak = local.inv_pair
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv_pair_weak = (\<lambda>heap. local.inv_pair_weak heap \<and> inv_distinct k_ref1 k_ref2 m_ref1 m_ref2)
[PROOF STEP]
using inv_distinct
[PROOF STATE]
proof (prove)
using this:
inv_distinct k_ref1 k_ref2 m_ref1 m_ref2

goal (1 subgoal):
 1. local.inv_pair_weak = (\<lambda>heap. local.inv_pair_weak heap \<and> inv_distinct k_ref1 k_ref2 m_ref1 m_ref2)
[PROOF STEP]
by simp


[STATEMENT]
lemma lift_p_inv_pairI:
  "State_Heap.lift_p inv_pair m" if "State_Heap.lift_p inv_pair_weak m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State_Heap.lift_p local.inv_pair m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
State_Heap.lift_p local.inv_pair_weak m

goal (1 subgoal):
 1. State_Heap.lift_p local.inv_pair m
[PROOF STEP]
unfolding inv_pair_iff
[PROOF STATE]
proof (prove)
using this:
State_Heap.lift_p local.inv_pair m

goal (1 subgoal):
 1. State_Heap.lift_p local.inv_pair m
[PROOF STEP]
by simp


[STATEMENT]
lemma lift_p_success:
  "State_Heap.lift_p inv_pair_weak m"
  if "DP_CRelVS.lift_p inv_pair_weak (state_of m)" "\<forall> heap. inv_pair_weak heap \<longrightarrow> success m heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State_Heap.lift_p local.inv_pair_weak m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (state_of m)
\<forall>heap. local.inv_pair_weak heap \<longrightarrow> success m heap

goal (1 subgoal):
 1. State_Heap.lift_p local.inv_pair_weak m
[PROOF STEP]
unfolding lift_p_def DP_CRelVS.lift_p_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. local.inv_pair_weak heap \<longrightarrow> (case run_state (state_of m) heap of (x, xa) \<Rightarrow> local.inv_pair_weak xa)
\<forall>heap. local.inv_pair_weak heap \<longrightarrow> success m heap

goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> (case execute m heap of None \<Rightarrow> False | Some (xa, xb) \<Rightarrow> local.inv_pair_weak xb)
[PROOF STEP]
by (auto simp: success_def split: option.split)


[STATEMENT]
lemma rel_state_ofI2:
  "rel_state (=) (state_of m) m" if
  "\<forall> heap. inv_pair_weak heap \<longrightarrow> success m heap"
  "DP_CRelVS.lift_p inv_pair_weak (state_of m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.rel_state (=) (state_of m) m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. local.inv_pair_weak heap \<longrightarrow> success m heap
DP_CRelVS.lift_p local.inv_pair_weak (state_of m)

goal (1 subgoal):
 1. local.rel_state (=) (state_of m) m
[PROOF STEP]
by (blast intro: rel_state_ofI lift_p_success)


[STATEMENT]
lemma [transfer_rule]:
  "((=) ===> rel_state (=)) move12 move12'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (=)) local.move12 local.move12'
[PROOF STEP]
unfolding move12_def move12'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (=)) (\<lambda>k. state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := k \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m)))))))) (\<lambda>k. !k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := k \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m)))))))
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = y \<Longrightarrow> local.rel_state (=) (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m)))))))) (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := y \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m)))))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. local.rel_state (=) (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m)))))))) (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m)))))))
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))) heap
 2. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x_ \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))) heap
[PROOF STEP]
by (auto
        simp: mem_empty_def inv_pair_lengthD1 execute_simps Let_def
        intro: success_intros intro!: success_bind_I
       )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x_ \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))))
[PROOF STEP]
using pair.move12_inv
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (local.move12 ?k1.0)

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x_ \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))))
[PROOF STEP]
unfolding move12_def
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := ?k1.0 \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))))

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := x_ \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m))))))))
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [transfer_rule]:
  "((=) ===> rel_state (rel_option (=))) lookup2 mem_lookup2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (rel_option (=))) local.lookup2 local.mem_lookup2
[PROOF STEP]
unfolding lookup2_def mem_lookup2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (rel_option (=))) (\<lambda>k. state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m k))) (\<lambda>k. !m_ref2 \<bind> (\<lambda>m. local.mem_lookup m k))
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = y \<Longrightarrow> local.rel_state (rel_option (=)) (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x))) (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m y))
[PROOF STEP]
apply (simp add: option.rel_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. local.rel_state (=) (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x))) (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x))
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x)) heap
 2. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x_)) heap
[PROOF STEP]
by (auto 4 3
        simp: mem_lookup_def inv_pair_lengthD2 execute_simps Let_def
        intro: success_intros intro!: success_bind_I
       )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
using pair.lookup_inv(2)
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (local.lookup2 ?k')

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
unfolding lookup2_def
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m ?k')))

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [transfer_rule]:
  "rel_state (=) get_k1 get_k1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.rel_state (=) local.get_k1 local.get_k1'
[PROOF STEP]
unfolding get_k1_def get_k1'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.rel_state (=) (state_of (!k_ref1)) (!k_ref1)
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!k_ref1) heap
 2. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!k_ref1) heap
[PROOF STEP]
by (auto intro: success_lookupI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref1))
[PROOF STEP]
unfolding get_k1_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak local.get_k1
[PROOF STEP]
by (auto dest: pair.get_state(1) intro: lift_pI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [transfer_rule]:
  "rel_state (=) get_k2 get_k2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.rel_state (=) local.get_k2 local.get_k2'
[PROOF STEP]
unfolding get_k2_def get_k2'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.rel_state (=) (state_of (!k_ref2)) (!k_ref2)
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!k_ref2) heap
 2. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref2))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!k_ref2) heap
[PROOF STEP]
by (auto intro: success_lookupI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref2))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!k_ref2))
[PROOF STEP]
unfolding get_k2_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak local.get_k2
[PROOF STEP]
by (auto dest: pair.get_state(2) intro: lift_pI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [transfer_rule]:
  "((=) ===> (=) ===> rel_state (=)) update1 update1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) local.update1 local.update1'
[PROOF STEP]
unfolding update1_def update1'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) (\<lambda>k v. state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m k v))) (\<lambda>k v. !m_ref1 \<bind> (\<lambda>m. local.mem_update m k v))
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> local.rel_state (=) (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m x xa))) (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y ya))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> local.rel_state (=) (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y ya))) (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y ya))
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y ya)) heap
 2. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y ya)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y_ ya_)) heap
[PROOF STEP]
by (auto 4 3
        simp: mem_update_def inv_pair_lengthD1 execute_simps Let_def
        intro: success_intros intro!: success_bind_I
       )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y ya)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y_ ya_)))
[PROOF STEP]
using pair.update_inv(1)
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (local.update1 ?k' ?v)

goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y_ ya_)))
[PROOF STEP]
unfolding update1_def
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m ?k' ?v)))

goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_update m y_ ya_)))
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [transfer_rule]:
  "((=) ===> (=) ===> rel_state (=)) update2 update2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) local.update2 local.update2'
[PROOF STEP]
unfolding update2_def update2'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) (\<lambda>k v. state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m k v))) (\<lambda>k v. !m_ref2 \<bind> (\<lambda>m. local.mem_update m k v))
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> local.rel_state (=) (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m x xa))) (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y ya))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> local.rel_state (=) (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y ya))) (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y ya))
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y ya)) heap
 2. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y ya)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y_ ya_)) heap
[PROOF STEP]
by (auto 4 3
        simp: mem_update_def inv_pair_lengthD2 execute_simps Let_def
        intro: success_intros intro!: success_bind_I
       )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y ya)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y_ ya_)))
[PROOF STEP]
using pair.update_inv(2)
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (local.update2 ?k' ?v)

goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y_ ya_)))
[PROOF STEP]
unfolding update2_def
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m ?k' ?v)))

goal (1 subgoal):
 1. \<lbrakk>x_ = y_; xa_ = ya_\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref2 \<bind> (\<lambda>m. local.mem_update m y_ ya_)))
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [transfer_rule]:
  "((=) ===> rel_state (rel_option (=))) lookup1 mem_lookup1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (rel_option (=))) local.lookup1 local.mem_lookup1
[PROOF STEP]
unfolding lookup1_def mem_lookup1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (rel_option (=))) (\<lambda>k. state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m k))) (\<lambda>k. !m_ref1 \<bind> (\<lambda>m. local.mem_lookup m k))
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = y \<Longrightarrow> local.rel_state (rel_option (=)) (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x))) (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m y))
[PROOF STEP]
apply (simp add: option.rel_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. local.rel_state (=) (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x))) (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x))
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x)) heap
 2. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)) heap
[PROOF STEP]
by (auto 4 3
        simp: mem_lookup_def inv_pair_lengthD1 execute_simps Let_def
        intro: success_intros intro!: success_bind_I
       )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
using pair.lookup_inv(1)
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (local.lookup1 ?k')

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
unfolding lookup1_def
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m ?k')))

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done