[STATEMENT]
lemma bounded_clinear_compose:
  assumes "bounded_clinear f"
    and "bounded_clinear g"
  shows "bounded_clinear (\<lambda>x. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. f (g x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b1 b2. f (g (b1 + b2)) = f (g b1) + f (g b2)
 2. \<And>r b. f (g (r *\<^sub>C b)) = r *\<^sub>C f (g b)
 3. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
interpret f: bounded_clinear f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b1 b2. f (g (b1 + b2)) = f (g b1) + f (g b2)
 2. \<And>r b. f (g (r *\<^sub>C b)) = r *\<^sub>C f (g b)
 3. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
interpret g: bounded_clinear g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b1 b2. f (g (b1 + b2)) = f (g b1) + f (g b2)
 2. \<And>r b. f (g (r *\<^sub>C b)) = r *\<^sub>C f (g b)
 3. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
show "f (g (x + y)) = f (g x) + f (g y)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (g (x + y)) = f (g x) + f (g y)
[PROOF STEP]
by (simp only: f.add g.add)
[PROOF STATE]
proof (state)
this:
f (g (?x + ?y)) = f (g ?x) + f (g ?y)

goal (2 subgoals):
 1. \<And>r b. f (g (r *\<^sub>C b)) = r *\<^sub>C f (g b)
 2. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
show "f (g (scaleC r x)) = scaleC r (f (g x))" for r x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (g (r *\<^sub>C x)) = r *\<^sub>C f (g x)
[PROOF STEP]
by (simp only: f.scaleC g.scaleC)
[PROOF STATE]
proof (state)
this:
f (g (?r *\<^sub>C ?x)) = ?r *\<^sub>C f (g ?x)

goal (1 subgoal):
 1. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
from f.pos_bounded
[PROOF STATE]
proof (chain)
picking this:
\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K
[PROOF STEP]
obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf"
[PROOF STATE]
proof (prove)
using this:
\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K

goal (1 subgoal):
 1. (\<And>Kf. \<lbrakk>\<And>x. norm (f x) \<le> norm x * Kf; 0 < Kf\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (f ?x) \<le> norm ?x * Kf
0 < Kf

goal (1 subgoal):
 1. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
from g.pos_bounded
[PROOF STATE]
proof (chain)
picking this:
\<exists>K>0. \<forall>x. norm (g x) \<le> norm x * K
[PROOF STEP]
obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg"
[PROOF STATE]
proof (prove)
using this:
\<exists>K>0. \<forall>x. norm (g x) \<le> norm x * K

goal (1 subgoal):
 1. (\<And>Kg. (\<And>x. norm (g x) \<le> norm x * Kg) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (g ?x) \<le> norm ?x * Kg

goal (1 subgoal):
 1. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K
[PROOF STEP]
proof (intro exI allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. norm (f (g x)) \<le> norm x * ?K
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. norm (f (g x)) \<le> norm x * ?K
[PROOF STEP]
have "norm (f (g x)) \<le> norm (g x) * Kf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (f (g x)) \<le> norm (g x) * Kf
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
norm (f ?x) \<le> norm ?x * Kf

goal (1 subgoal):
 1. norm (f (g x)) \<le> norm (g x) * Kf
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
norm (f (g x)) \<le> norm (g x) * Kf

goal (1 subgoal):
 1. \<And>x. norm (f (g x)) \<le> norm x * ?K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (f (g x)) \<le> norm (g x) * Kf

goal (1 subgoal):
 1. \<And>x. norm (f (g x)) \<le> norm x * ?K
[PROOF STEP]
have "\<dots> \<le> (norm x * Kg) * Kf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (g x) * Kf \<le> norm x * Kg * Kf
[PROOF STEP]
using g Kf [THEN order_less_imp_le]
[PROOF STATE]
proof (prove)
using this:
norm (g ?x) \<le> norm ?x * Kg
0 \<le> Kf

goal (1 subgoal):
 1. norm (g x) * Kf \<le> norm x * Kg * Kf
[PROOF STEP]
by (rule mult_right_mono)
[PROOF STATE]
proof (state)
this:
norm (g x) * Kf \<le> norm x * Kg * Kf

goal (1 subgoal):
 1. \<And>x. norm (f (g x)) \<le> norm x * ?K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (g x) * Kf \<le> norm x * Kg * Kf

goal (1 subgoal):
 1. \<And>x. norm (f (g x)) \<le> norm x * ?K
[PROOF STEP]
have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x * Kg * Kf = norm x * (Kg * Kf)
[PROOF STEP]
by (rule mult.assoc)
[PROOF STATE]
proof (state)
this:
norm x * Kg * Kf = norm x * (Kg * Kf)

goal (1 subgoal):
 1. \<And>x. norm (f (g x)) \<le> norm x * ?K
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm (f (g x)) \<le> norm x * (Kg * Kf)
[PROOF STEP]
show "norm (f (g x)) \<le> norm x * (Kg * Kf)"
[PROOF STATE]
proof (prove)
using this:
norm (f (g x)) \<le> norm x * (Kg * Kf)

goal (1 subgoal):
 1. norm (f (g x)) \<le> norm x * (Kg * Kf)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
norm (f (g x)) \<le> norm x * (Kg * Kf)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_cbilinear_mult: "bounded_cbilinear ((*) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::complex_normed_algebra)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_cbilinear (*)
[PROOF STEP]
proof (rule bounded_cbilinear.intro)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a a' b. (a + a') * b = a * b + a' * b
 2. \<And>a b b'. a * (b + b') = a * b + a * b'
 3. \<And>r a b. r *\<^sub>C a * b = r *\<^sub>C (a * b)
 4. \<And>a r b. a * r *\<^sub>C b = r *\<^sub>C (a * b)
 5. \<exists>K. \<forall>a b. norm (a * b) \<le> norm a * norm b * K
[PROOF STEP]
show "\<exists>K. \<forall>a b::'a. norm (a * b) \<le> norm a * norm b * K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>a b. norm (a * b) \<le> norm a * norm b * K
[PROOF STEP]
by (rule_tac x=1 in exI) (simp add: norm_mult_ineq)
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>a b. norm (a * b) \<le> norm a * norm b * K

goal (4 subgoals):
 1. \<And>a a' b. (a + a') * b = a * b + a' * b
 2. \<And>a b b'. a * (b + b') = a * b + a * b'
 3. \<And>r a b. r *\<^sub>C a * b = r *\<^sub>C (a * b)
 4. \<And>a r b. a * r *\<^sub>C b = r *\<^sub>C (a * b)
[PROOF STEP]
qed (auto simp: algebra_simps)


[STATEMENT]
lemma bounded_clinear_mult_left: "bounded_clinear (\<lambda>x::'a::complex_normed_algebra. x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. x * y)
[PROOF STEP]
using bounded_cbilinear_mult
[PROOF STATE]
proof (prove)
using this:
bounded_cbilinear (*)

goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. x * y)
[PROOF STEP]
by (rule bounded_cbilinear.bounded_clinear_left)


[STATEMENT]
lemma bounded_clinear_mult_right: "bounded_clinear (\<lambda>y::'a::complex_normed_algebra. x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear ((*) x)
[PROOF STEP]
using bounded_cbilinear_mult
[PROOF STATE]
proof (prove)
using this:
bounded_cbilinear (*)

goal (1 subgoal):
 1. bounded_clinear ((*) x)
[PROOF STEP]
by (rule bounded_cbilinear.bounded_clinear_right)


[STATEMENT]
lemma bounded_clinear_divide: "bounded_clinear (\<lambda>x. x / y)"
  for y :: "'a::complex_normed_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. x / y)
[PROOF STEP]
unfolding divide_inverse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. x * inverse y)
[PROOF STEP]
by (rule bounded_clinear_mult_left)


[STATEMENT]
lemma bounded_cbilinear_scaleC: "bounded_cbilinear scaleC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_cbilinear (*\<^sub>C)
[PROOF STEP]
proof (rule bounded_cbilinear.intro)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a a' b. (a + a') *\<^sub>C b = a *\<^sub>C b + a' *\<^sub>C b
 2. \<And>a b b'. a *\<^sub>C (b + b') = a *\<^sub>C b + a *\<^sub>C b'
 3. \<And>r a b. (r *\<^sub>C a) *\<^sub>C b = r *\<^sub>C a *\<^sub>C b
 4. \<And>a r b. a *\<^sub>C r *\<^sub>C b = r *\<^sub>C a *\<^sub>C b
 5. \<exists>K. \<forall>a b. norm (a *\<^sub>C b) \<le> cmod a * norm b * K
[PROOF STEP]
obtain K where K: \<open>\<forall>a (b::'a). norm b \<le> norm b * K\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. \<forall>a b. norm b \<le> norm b * K \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. (\<And>K. \<forall>a b. norm b \<le> norm b * K \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a b. norm b \<le> norm b * K

goal (5 subgoals):
 1. \<And>a a' b. (a + a') *\<^sub>C b = a *\<^sub>C b + a' *\<^sub>C b
 2. \<And>a b b'. a *\<^sub>C (b + b') = a *\<^sub>C b + a *\<^sub>C b'
 3. \<And>r a b. (r *\<^sub>C a) *\<^sub>C b = r *\<^sub>C a *\<^sub>C b
 4. \<And>a r b. a *\<^sub>C r *\<^sub>C b = r *\<^sub>C a *\<^sub>C b
 5. \<exists>K. \<forall>a b. norm (a *\<^sub>C b) \<le> cmod a * norm b * K
[PROOF STEP]
show "\<exists>K. \<forall>a (b::'a). norm (a *\<^sub>C b) \<le> norm a * norm b * K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>a b. norm (a *\<^sub>C b) \<le> cmod a * norm b * K
[PROOF STEP]
apply (rule exI[where x=K])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. norm (a *\<^sub>C b) \<le> cmod a * norm b * K
[PROOF STEP]
using K
[PROOF STATE]
proof (prove)
using this:
\<forall>a b. norm b \<le> norm b * K

goal (1 subgoal):
 1. \<forall>a b. norm (a *\<^sub>C b) \<le> cmod a * norm b * K
[PROOF STEP]
by (metis norm_scaleC)
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>a b. norm (a *\<^sub>C b) \<le> cmod a * norm b * K

goal (4 subgoals):
 1. \<And>a a' b. (a + a') *\<^sub>C b = a *\<^sub>C b + a' *\<^sub>C b
 2. \<And>a b b'. a *\<^sub>C (b + b') = a *\<^sub>C b + a *\<^sub>C b'
 3. \<And>r a b. (r *\<^sub>C a) *\<^sub>C b = r *\<^sub>C a *\<^sub>C b
 4. \<And>a r b. a *\<^sub>C r *\<^sub>C b = r *\<^sub>C a *\<^sub>C b
[PROOF STEP]
qed (auto simp: algebra_simps)


[STATEMENT]
lemma bounded_clinear_scaleC_left: "bounded_clinear (\<lambda>c. scaleC c x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>c. c *\<^sub>C x)
[PROOF STEP]
using bounded_cbilinear_scaleC
[PROOF STATE]
proof (prove)
using this:
bounded_cbilinear (*\<^sub>C)

goal (1 subgoal):
 1. bounded_clinear (\<lambda>c. c *\<^sub>C x)
[PROOF STEP]
by (rule bounded_cbilinear.bounded_clinear_left)


[STATEMENT]
lemma bounded_clinear_scaleC_right: "bounded_clinear (\<lambda>x. scaleC c x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear ((*\<^sub>C) c)
[PROOF STEP]
using bounded_cbilinear_scaleC
[PROOF STATE]
proof (prove)
using this:
bounded_cbilinear (*\<^sub>C)

goal (1 subgoal):
 1. bounded_clinear ((*\<^sub>C) c)
[PROOF STEP]
by (rule bounded_cbilinear.bounded_clinear_right)


[STATEMENT]
lemma bounded_clinear_of_complex: "bounded_clinear (\<lambda>r. of_complex r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear of_complex
[PROOF STEP]
unfolding of_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>r. r *\<^sub>C (1::'a))
[PROOF STEP]
by (rule bounded_clinear_scaleC_left)


[STATEMENT]
lemma complex_bounded_clinear: "bounded_clinear f \<longleftrightarrow> (\<exists>c::complex. f = (\<lambda>x. x * c))"
  for f :: "complex \<Rightarrow> complex"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
assume "bounded_clinear f"
[PROOF STATE]
proof (state)
this:
bounded_clinear f

goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded_clinear f
[PROOF STEP]
interpret bounded_clinear f
[PROOF STATE]
proof (prove)
using this:
bounded_clinear f

goal (1 subgoal):
 1. bounded_clinear f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
from scaleC[of x 1]
[PROOF STATE]
proof (chain)
picking this:
f (x *\<^sub>C 1) = x *\<^sub>C f 1
[PROOF STEP]
have "f x = x * f 1"
[PROOF STATE]
proof (prove)
using this:
f (x *\<^sub>C 1) = x *\<^sub>C f 1

goal (1 subgoal):
 1. f x = x * f 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f x = x * f 1

goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
bounded_clinear f \<Longrightarrow> f ?x2 = ?x2 * f 1

goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded_clinear f \<Longrightarrow> f ?x2 = ?x2 * f 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bounded_clinear f \<Longrightarrow> f ?x2 = ?x2 * f 1

goal (1 subgoal):
 1. bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))
[PROOF STEP]
by (auto intro: exI[of _ "f 1"] bounded_clinear_mult_left)
[PROOF STATE]
proof (state)
this:
bounded_clinear f = (\<exists>c. f = (\<lambda>x. x * c))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cCauchy_iff2: "Cauchy X \<longleftrightarrow> (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. cmod (X m - X n) < inverse (real (Suc j))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cauchy X = (\<forall>j. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. cmod (X m - X n) < inverse (real (Suc j)))
[PROOF STEP]
by (simp only: metric_Cauchy_iff2 dist_complex_def)


[STATEMENT]
lemma complex_increasing_LIMSEQ:
  fixes f :: "nat \<Rightarrow> complex"
  assumes inc: "\<And>n. f n \<le> f (Suc n)"
    and bdd: "\<And>n. f n \<le> l"
    and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
  shows "f \<longlonglongrightarrow> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<longlonglongrightarrow> l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<longlonglongrightarrow> l
[PROOF STEP]
have \<open>(\<lambda>n. Re (f n)) \<longlonglongrightarrow> Re l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. Re (f n)) \<longlonglongrightarrow> Re l
[PROOF STEP]
apply (rule increasing_LIMSEQ)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. Re (f n) \<le> Re (f (Suc n))
 2. \<And>n. Re (f n) \<le> Re l
 3. \<And>e. 0 < e \<Longrightarrow> \<exists>n. Re l \<le> Re (f n) + e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f ?n \<le> f (Suc ?n)
f ?n \<le> l
0 < ?e \<Longrightarrow> \<exists>n. l \<le> f n + ?e

goal (3 subgoals):
 1. \<And>n. Re (f n) \<le> Re (f (Suc n))
 2. \<And>n. Re (f n) \<le> Re l
 3. \<And>e. 0 < e \<Longrightarrow> \<exists>n. Re l \<le> Re (f n) + e
[PROOF STEP]
apply (auto simp: less_eq_complex_def less_complex_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>0 < e; \<And>n. Re (f n) \<le> Re (f (Suc n)); \<And>n. Re (f n) \<le> Re l \<and> Im (f n) = Im l; \<And>e. 0 < Re e \<and> Im e = 0 \<Longrightarrow> \<exists>n. Re l \<le> Re (f n) + Re e\<rbrakk> \<Longrightarrow> \<exists>n. Re l \<le> Re (f n) + e
[PROOF STEP]
by (metis Im_complex_of_real Re_complex_of_real)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Re (f n)) \<longlonglongrightarrow> Re l

goal (1 subgoal):
 1. f \<longlonglongrightarrow> l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Re (f n)) \<longlonglongrightarrow> Re l

goal (1 subgoal):
 1. f \<longlonglongrightarrow> l
[PROOF STEP]
have \<open>Im (f n) = Im l\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im (f n) = Im l
[PROOF STEP]
using bdd
[PROOF STATE]
proof (prove)
using this:
f ?n \<le> l

goal (1 subgoal):
 1. Im (f n) = Im l
[PROOF STEP]
by (auto simp: less_eq_complex_def)
[PROOF STATE]
proof (state)
this:
Im (f ?n) = Im l

goal (1 subgoal):
 1. f \<longlonglongrightarrow> l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Im (f ?n) = Im l
[PROOF STEP]
have \<open>(\<lambda>n. Im (f n)) \<longlonglongrightarrow> Im l\<close>
[PROOF STATE]
proof (prove)
using this:
Im (f ?n) = Im l

goal (1 subgoal):
 1. (\<lambda>n. Im (f n)) \<longlonglongrightarrow> Im l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Im (f n)) \<longlonglongrightarrow> Im l

goal (1 subgoal):
 1. f \<longlonglongrightarrow> l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. Re (f n)) \<longlonglongrightarrow> Re l
(\<lambda>n. Im (f n)) \<longlonglongrightarrow> Im l
[PROOF STEP]
show \<open>f \<longlonglongrightarrow> l\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. Re (f n)) \<longlonglongrightarrow> Re l
(\<lambda>n. Im (f n)) \<longlonglongrightarrow> Im l

goal (1 subgoal):
 1. f \<longlonglongrightarrow> l
[PROOF STEP]
by (simp add: tendsto_complex_iff)
[PROOF STATE]
proof (state)
this:
f \<longlonglongrightarrow> l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_Cauchy_convergent:
  fixes X :: "nat \<Rightarrow> complex"
  assumes X: "Cauchy X"
  shows "convergent X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Cauchy X

goal (1 subgoal):
 1. convergent X
[PROOF STEP]
by (rule Cauchy_convergent)


[STATEMENT]
lemma PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> PP t \<in> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> PP t \<in> fmla
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> subst P t xx \<in> fmla
[PROOF STEP]
by auto


[STATEMENT]
lemma Fvars_PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> Fvars (PP t) = FvarsT t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> Fvars (PP t) = FvarsT t
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> Fvars (subst P t xx) = FvarsT t
[PROOF STEP]
by auto


[STATEMENT]
lemma [simp]:
"n \<in> num \<Longrightarrow> subst (PP (Var yy)) n yy = PP n"
"n \<in> num \<Longrightarrow> subst (PP (Var xx)) n xx = PP n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<in> num \<Longrightarrow> subst (PP (Var yy)) n yy = PP n) &&& (n \<in> num \<Longrightarrow> subst (PP (Var xx)) n xx = PP n)
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<in> num \<Longrightarrow> subst (subst P (Var yy) xx) n yy = subst P n xx) &&& (n \<in> num \<Longrightarrow> subst (subst P (Var xx) xx) n xx = subst P n xx)
[PROOF STEP]
by auto


[STATEMENT]
lemma HBL1_PP:
"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>\<rbrakk> \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)
[PROOF STEP]
using HBL1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prv ?\<phi>\<rbrakk> \<Longrightarrow> prv (subst P \<langle>?\<phi>\<rangle> xx)

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>\<rbrakk> \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prv ?\<phi>\<rbrakk> \<Longrightarrow> prv (subst P \<langle>?\<phi>\<rangle> xx)

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>\<rbrakk> \<Longrightarrow> prv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
by auto


[STATEMENT]
lemma inth_append [simp]:
 "0 \<le> i \<Longrightarrow>
    (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> i \<Longrightarrow> (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))
[PROOF STEP]
by (induction xs arbitrary: i, auto simp: algebra_simps)


[STATEMENT]
lemma iexec_simp:
 "(ins, cf) \<mapsto> cf' = (cf' = iexec ins cf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ins, cf) \<mapsto> cf' = (cf' = iexec ins cf)
[PROOF STEP]
by (auto elim: iexec_pred.cases)


[STATEMENT]
lemma exec1I [intro, code_pred_intro]:
 "\<lbrakk>c' = iexec (P !! i) (i, s, stk); 0 \<le> i; i < size P\<rbrakk> \<Longrightarrow>
    P \<turnstile> (i, s, stk) \<rightarrow> c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c' = iexec (P !! i) (i, s, stk); 0 \<le> i; i < size P\<rbrakk> \<Longrightarrow> P \<turnstile> (i, s, stk) \<rightarrow> c'
[PROOF STEP]
by (auto simp: exec1_def iexec_simp)


[STATEMENT]
lemma inth_map [simp]:
 "\<lbrakk>0 \<le> i; i < size xs\<rbrakk> \<Longrightarrow> (map f xs) !! i = f (xs !! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> i; i < size xs\<rbrakk> \<Longrightarrow> map f xs !! i = f (xs !! i)
[PROOF STEP]
by (induction xs arbitrary: i, simp_all)


[STATEMENT]
lemma inth_set [simp]:
 "\<lbrakk>0 \<le> i; i < size xs\<rbrakk> \<Longrightarrow> xs !! i \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> i; i < size xs\<rbrakk> \<Longrightarrow> xs !! i \<in> set xs
[PROOF STEP]
by (induction xs arbitrary: i, simp_all)


[STATEMENT]
lemma vars_dist:
 "distinct (vars P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (vars P)
[PROOF STEP]
by (induction P, simp_all split: instr.split)


[STATEMENT]
lemma vars_load:
 "\<lbrakk>0 \<le> i; i < size P; P !! i = LOAD x\<rbrakk> \<Longrightarrow> x \<in> set (vars P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> i; i < size P; P !! i = LOAD x\<rbrakk> \<Longrightarrow> x \<in> set (vars P)
[PROOF STEP]
by (induction P arbitrary: i, simp, fastforce split: if_split_asm)


[STATEMENT]
lemma vars_store:
 "\<lbrakk>0 \<le> i; i < size P; P !! i = STORE x\<rbrakk> \<Longrightarrow> x \<in> set (vars P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> i; i < size P; P !! i = STORE x\<rbrakk> \<Longrightarrow> x \<in> set (vars P)
[PROOF STEP]
by (induction P arbitrary: i, simp, fastforce split: if_split_asm)


[STATEMENT]
lemma addr_of_max:
 "addr_of xs x \<le> size xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of xs x \<le> size xs
[PROOF STEP]
by (induction xs, simp_all)


[STATEMENT]
lemma addr_of_neq:
 "1 + size xs \<noteq> addr_of xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + size xs \<noteq> addr_of xs x
[PROOF STEP]
by (insert addr_of_max [of xs x], simp)


[STATEMENT]
lemma addr_of_correct:
 "x \<in> set xs \<Longrightarrow> xs !! (size xs - addr_of xs x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> xs !! (size xs - addr_of xs x) = x
[PROOF STEP]
by (induction xs, simp, clarsimp, erule contrapos_pp, rule addr_of_neq)


[STATEMENT]
lemma addr_of_nneg:
 "0 \<le> addr_of xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> addr_of xs x
[PROOF STEP]
by (induction xs, simp_all)


[STATEMENT]
lemma addr_of_set:
 "x \<in> set xs \<Longrightarrow> 0 < addr_of xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> 0 < addr_of xs x
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma addr_of_unique:
 "\<lbrakk>distinct xs; 0 < a; a \<le> size xs\<rbrakk> \<Longrightarrow> addr_of xs (xs !! (size xs - a)) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; 0 < a; a \<le> size xs\<rbrakk> \<Longrightarrow> addr_of xs (xs !! (size xs - a)) = a
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma add_m_stack_nneg:
 "0 \<le> a \<Longrightarrow> add_m_stack n stk ms a = ms a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a \<Longrightarrow> add_m_stack n stk ms a = ms a
[PROOF STEP]
by (induction n arbitrary: stk, simp_all)


[STATEMENT]
lemma add_m_stack_hd:
 "0 < n \<Longrightarrow> add_m_stack n stk ms (-n) = hd stk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> add_m_stack n stk ms (- int n) = hd stk
[PROOF STEP]
by (cases n, simp_all)


[STATEMENT]
lemma add_m_stack_hd2:
 "1 < n \<Longrightarrow> add_m_stack n stk ms (1 - int n) = hd2 stk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> add_m_stack n stk ms (1 - int n) = hd2 stk
[PROOF STEP]
by (cases n, simp_all add: add_m_stack_hd)


[STATEMENT]
lemma add_m_stack_nth:
 "\<lbrakk>-n \<le> a; n \<le> length stk\<rbrakk> \<Longrightarrow>
    add_m_stack n stk ms a = (if 0 \<le> a then ms a else stk ! (nat (n + a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- int n \<le> a; n \<le> length stk\<rbrakk> \<Longrightarrow> add_m_stack n stk ms a = (if 0 \<le> a then ms a else stk ! nat (int n + a))
[PROOF STEP]
by (induction n arbitrary: stk, auto intro: hd_conv_nth simp: add_m_stack_nneg
 nth_tl Suc_nat_eq_nat_zadd1 ac_simps)


[STATEMENT]
lemma exec1_m_exec1 [simplified Let_def]:
 "\<lbrakk>P \<turnstile> (pc, s, stk) \<rightarrow> (pc', s', stk'); msp P pc \<le> sp; sp \<le> length stk\<rbrakk> \<Longrightarrow>
    let sp' = sp + length stk' - length stk in to_m_prog P \<^bold>\<turnstile>
      (pc, add_m_stack sp stk (to_m_state (vars P) s), sp) \<^bold>\<rightarrow>
      (pc', add_m_stack sp' stk' (to_m_state (vars P) s'), sp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> (pc, s, stk) \<rightarrow> (pc', s', stk'); msp P pc \<le> sp; sp \<le> length stk\<rbrakk> \<Longrightarrow> let sp' = sp + length stk' - length stk in to_m_prog P \<^bold>\<turnstile> (pc, add_m_stack sp stk (to_m_state (vars P) s), sp) \<^bold>\<rightarrow> (pc', add_m_stack sp' stk' (to_m_state (vars P) s'), sp')
[PROOF STEP]
proof (auto dest: vars_load vars_store addr_of_set intro: addr_of_max
 simp: msp_def exec1_def m_exec1_def vars_load addr_of_correct addr_of_nneg
 add_m_stack_nneg add_m_stack_hd add_m_stack_hd2 split: instr.split)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<lbrakk>2 \<le> sp; sp \<le> length stk; 0 \<le> pc; pc < size P; P !! pc = ADD; pc' = pc + 1; stk' = (hd2 stk + hd stk) # tl2 stk; s' = s\<rbrakk> \<Longrightarrow> let sp' = sp - Suc 0 in \<forall>a. (a = 1 - int sp \<longrightarrow> - int sp' \<le> 1 - int sp \<longrightarrow> add_m_stack sp' ((hd2 stk + hd stk) # tl2 stk) (to_m_state (vars P) s) (1 - int sp) = hd2 stk + hd stk) \<and> (a \<noteq> 1 - int sp \<longrightarrow> - int sp' \<le> a \<longrightarrow> add_m_stack sp' ((hd2 stk + hd stk) # tl2 stk) (to_m_state (vars P) s) a = add_m_stack sp stk (to_m_state (vars P) s) a)
 2. \<And>x4. \<lbrakk>Suc 0 \<le> sp; sp \<le> length stk; 0 \<le> pc; pc < size P; 0 < addr_of (vars P) x4; addr_of (vars P) x4 \<le> size (vars P); P !! pc = STORE x4; pc' = pc + 1; stk' = tl stk; s' = s(x4 := hd stk); vars P !! (size (vars P) - addr_of (vars P) x4) = x4\<rbrakk> \<Longrightarrow> let sp' = sp - Suc 0 in \<forall>a. a \<noteq> addr_of (vars P) x4 \<longrightarrow> - int sp' \<le> a \<longrightarrow> add_m_stack sp' (tl stk) (to_m_state (vars P) (s(x4 := hd stk))) a = add_m_stack sp stk (to_m_state (vars P) s) a
 3. \<And>x4. \<lbrakk>Suc 0 \<le> sp; sp \<le> length stk; 0 \<le> pc; pc < size P; 0 < addr_of (vars P) x4; addr_of (vars P) x4 \<le> size (vars P); P !! pc = STORE x4; pc' = pc + 1; stk' = tl stk; s' = s(x4 := hd stk); vars P !! (size (vars P) - addr_of (vars P) x4) \<noteq> x4\<rbrakk> \<Longrightarrow> let sp' = sp - Suc 0 in \<forall>a. (a = addr_of (vars P) x4 \<longrightarrow> s (vars P !! (size (vars P) - addr_of (vars P) x4)) = hd stk) \<and> (a \<noteq> addr_of (vars P) x4 \<longrightarrow> - int sp' \<le> a \<longrightarrow> add_m_stack sp' (tl stk) (to_m_state (vars P) (s(x4 := hd stk))) a = add_m_stack sp stk (to_m_state (vars P) s) a)
 4. \<And>x6. \<lbrakk>2 \<le> sp; sp \<le> length stk; 0 \<le> pc; pc < size P; hd2 stk < hd stk; P !! pc = JMPLESS x6; pc' = pc + 1 + x6; stk' = tl2 stk; s' = s\<rbrakk> \<Longrightarrow> let sp' = sp - 2 in \<forall>a\<ge>- int sp'. add_m_stack sp' (tl2 stk) (to_m_state (vars P) s) a = add_m_stack sp stk (to_m_state (vars P) s) a
 5. \<And>x6. \<lbrakk>2 \<le> sp; sp \<le> length stk; 0 \<le> pc; pc < size P; \<not> hd2 stk < hd stk; P !! pc = JMPLESS x6; pc' = pc + 1; stk' = tl2 stk; s' = s\<rbrakk> \<Longrightarrow> let sp' = sp - 2 in \<forall>a\<ge>- int sp'. add_m_stack sp' (tl2 stk) (to_m_state (vars P) s) a = add_m_stack sp stk (to_m_state (vars P) s) a
 6. \<And>x7. \<lbrakk>2 \<le> sp; sp \<le> length stk; 0 \<le> pc; pc < size P; hd stk \<le> hd2 stk; P !! pc = JMPGE x7; pc' = pc + 1 + x7; stk' = tl2 stk; s' = s\<rbrakk> \<Longrightarrow> let sp' = sp - 2 in \<forall>a\<ge>- int sp'. add_m_stack sp' (tl2 stk) (to_m_state (vars P) s) a = add_m_stack sp stk (to_m_state (vars P) s) a
 7. \<And>x7. \<lbrakk>2 \<le> sp; sp \<le> length stk; 0 \<le> pc; pc < size P; \<not> hd stk \<le> hd2 stk; P !! pc = JMPGE x7; pc' = pc + 1; stk' = tl2 stk; s' = s\<rbrakk> \<Longrightarrow> let sp' = sp - 2 in \<forall>a\<ge>- int sp'. add_m_stack sp' (tl2 stk) (to_m_state (vars P) s) a = add_m_stack sp stk (to_m_state (vars P) s) a
[PROOF STEP]
qed (auto dest: vars_store simp: add_m_stack_nth nth_tl Suc_nat_eq_nat_zadd1
 of_nat_diff vars_dist addr_of_correct addr_of_unique)


[STATEMENT]
lemma addr_of_nset:
 "x \<notin> set xs \<Longrightarrow> addr_of xs x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> addr_of xs x = 0
[PROOF STEP]
by (induction xs, auto split: if_split_asm)


[STATEMENT]
lemma addr_of_inj:
 "inj_on (addr_of xs) (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (addr_of xs) (set xs)
[PROOF STEP]
by (subst inj_on_def, clarify, induction xs, simp_all split: if_split_asm,
 drule sym, (subst (asm) add.commute, erule contrapos_pp, rule addr_of_neq)+)


[STATEMENT]
lemma addr_of_neq2:
 "\<lbrakk>x \<in> set xs; x' \<noteq> x\<rbrakk> \<Longrightarrow> addr_of xs x' \<noteq> addr_of xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; x' \<noteq> x\<rbrakk> \<Longrightarrow> addr_of xs x' \<noteq> addr_of xs x
[PROOF STEP]
by (cases "x' \<in> set xs", erule contrapos_nn, rule inj_onD [OF addr_of_inj],
 simp_all, drule addr_of_set, drule addr_of_nset, simp)


[STATEMENT]
lemma to_state_eq:
 "\<forall>a \<ge> 0. ms' a = ms a \<Longrightarrow> to_state xs ms' = to_state xs ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<ge>0. ms' a = ms a \<Longrightarrow> to_state xs ms' = to_state xs ms
[PROOF STEP]
by (rule ext, simp, induction xs, simp_all)


[STATEMENT]
lemma to_state_upd:
 "\<lbrakk>\<forall>a \<ge> 0. ms' a = (if a = addr_of xs x then i else ms a); x \<in> set xs\<rbrakk> \<Longrightarrow>
    to_state xs ms' = (to_state xs ms)(x := i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<ge>0. ms' a = (if a = addr_of xs x then i else ms a); x \<in> set xs\<rbrakk> \<Longrightarrow> to_state xs ms' = (to_state xs ms)(x := i)
[PROOF STEP]
by (rule ext, simp, rule conjI, rule_tac [!] impI, simp add: addr_of_nneg,
 drule addr_of_neq2, simp, simp add: addr_of_nneg)


[STATEMENT]
lemma add_stack_eq:
 "\<lbrakk>\<forall>a \<in> {-m..<0}. ms' a = ms a; m = n\<rbrakk> \<Longrightarrow> add_stack m ms' = add_stack n ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>{- int m..<0}. ms' a = ms a; m = n\<rbrakk> \<Longrightarrow> add_stack m ms' = add_stack n ms
[PROOF STEP]
by (induction m arbitrary: n, auto)


[STATEMENT]
lemma add_stack_eq2:
 "\<lbrakk>\<forall>a \<in> {-n..<0}. ms' a = (if a = -n then i else ms a); 0 < n\<rbrakk> \<Longrightarrow>
    add_stack n ms' = i # add_stack (n - 1) ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>{- int n..<0}. ms' a = (if a = - int n then i else ms a); 0 < n\<rbrakk> \<Longrightarrow> add_stack n ms' = i # add_stack (n - 1) ms
[PROOF STEP]
by (cases n, simp_all add: add_stack_eq)


[STATEMENT]
lemma add_stack_hd:
 "0 < n \<Longrightarrow> hd (add_stack n ms) = ms (-n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> hd (add_stack n ms) = ms (- int n)
[PROOF STEP]
by (cases n, simp_all)


[STATEMENT]
lemma add_stack_hd2:
 "1 < n \<Longrightarrow> hd2 (add_stack n ms) = ms (1 - int n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> hd2 (add_stack n ms) = ms (1 - int n)
[PROOF STEP]
by (induction n, simp_all add: add_stack_hd)


[STATEMENT]
lemma add_stack_nnil:
 "0 < n \<Longrightarrow> add_stack n ms \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> add_stack n ms \<noteq> []
[PROOF STEP]
by (cases n, simp_all)


[STATEMENT]
lemma add_stack_nnil2:
 "1 < n \<Longrightarrow> tl (add_stack n ms) \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> tl (add_stack n ms) \<noteq> []
[PROOF STEP]
by (induction n, simp_all add: add_stack_nnil)


[STATEMENT]
lemma add_stack_tl:
 "tl (add_stack n ms) = add_stack (n - 1) ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (add_stack n ms) = add_stack (n - 1) ms
[PROOF STEP]
by (cases n, simp_all)


[STATEMENT]
lemma m_exec1_exec1 [simplified]:
 "to_m_prog P \<^bold>\<turnstile> (pc, ms, sp) \<^bold>\<rightarrow> (pc', ms', sp') \<Longrightarrow>
    P \<turnstile> (pc, to_state (vars P) ms, add_stack sp ms @ stk) \<rightarrow>
      (pc', to_state (vars P) ms', add_stack sp' ms' @ stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_m_prog P \<^bold>\<turnstile> (pc, ms, sp) \<^bold>\<rightarrow> (pc', ms', sp') \<Longrightarrow> P \<turnstile> (pc, to_state (vars P) ms, add_stack sp ms @ stk) \<rightarrow> (pc', to_state (vars P) ms', add_stack sp' ms' @ stk)
[PROOF STEP]
proof (auto elim!: vars_store intro!: to_state_eq to_state_upd add_stack_eq
 simp: exec1_def m_exec1_def iexec_simp add_stack_hd add_stack_hd2
 add_stack_nnil add_stack_nnil2 split: instr.split_asm)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>0 \<le> pc; pc < size P; 2 \<le> sp; P !! pc = ADD; pc' = pc + 1; \<forall>a\<ge>- int (sp - Suc 0). ms' a = (if a = 1 - int sp then ms (1 - int sp) + ms (- int sp) else ms a); sp' = sp - Suc 0\<rbrakk> \<Longrightarrow> add_stack (sp - Suc 0) ms' = (ms (1 - int sp) + ms (- int sp)) # tl2 (add_stack sp ms)
 2. \<And>x4. \<lbrakk>0 \<le> pc; pc < size P; Suc 0 \<le> sp; P !! pc = STORE x4; pc' = pc + 1; \<forall>a\<ge>- int (sp - Suc 0). ms' a = (if a = addr_of (vars P) x4 then ms (- int sp) else ms a); sp' = sp - Suc 0\<rbrakk> \<Longrightarrow> add_stack (sp - Suc 0) ms' = tl (add_stack sp ms)
 3. \<And>x6. \<lbrakk>0 \<le> pc; pc < size P; 2 \<le> sp; P !! pc = JMPLESS x6; pc' = (if ms (1 - int sp) < ms (- int sp) then pc + 1 + x6 else pc + 1); \<forall>a\<ge>- int (sp - 2). ms' a = ms a; sp' = sp - 2\<rbrakk> \<Longrightarrow> add_stack (sp - 2) ms' = tl2 (add_stack sp ms)
 4. \<And>x7. \<lbrakk>0 \<le> pc; pc < size P; 2 \<le> sp; P !! pc = JMPGE x7; pc' = (if ms (- int sp) \<le> ms (1 - int sp) then pc + 1 + x7 else pc + 1); \<forall>a\<ge>- int (sp - 2). ms' a = ms a; sp' = sp - 2\<rbrakk> \<Longrightarrow> add_stack (sp - 2) ms' = tl2 (add_stack sp ms)
[PROOF STEP]
qed (subst add_stack_eq2, fastforce+, simp_all add: add_stack_tl, rule arg_cong,
 auto dest!: vars_store addr_of_set intro: add_stack_eq)


[STATEMENT]
lemma m_exec_exec:
 "to_m_prog P \<^bold>\<turnstile> (pc, ms, sp) \<^bold>\<rightarrow>\<^bold>* (pc', ms', sp') \<Longrightarrow>
    P \<turnstile> (pc, to_state (vars P) ms, add_stack sp ms @ stk) \<rightarrow>*
      (pc', to_state (vars P) ms', add_stack sp' ms' @ stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_m_prog P \<^bold>\<turnstile> (pc, ms, sp) \<^bold>\<rightarrow>\<^bold>* (pc', ms', sp') \<Longrightarrow> P \<turnstile> (pc, to_state (vars P) ms, add_stack sp ms @ stk) \<rightarrow>* (pc', to_state (vars P) ms', add_stack sp' ms' @ stk)
[PROOF STEP]
by (induction _ "(pc, ms, sp)" "(pc', ms', sp')" arbitrary: pc ms sp rule:
 star.induct, simp_all add: split_paired_all, drule m_exec1_exec1,
 auto intro: star_trans)


[STATEMENT]
lemma iexec_shift [simp]:
 "((n + i', s', stk') = iexec ins (n + i, s, stk)) =
    ((i', s', stk') = iexec ins (i, s, stk))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((n + i', s', stk') = iexec ins (n + i, s, stk)) = ((i', s', stk') = iexec ins (i, s, stk))
[PROOF STEP]
by (auto split: instr.split)


[STATEMENT]
lemma exec1_appendR:
 "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P @ P' \<turnstile> c \<rightarrow> c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P @ P' \<turnstile> c \<rightarrow> c'
[PROOF STEP]
by (auto simp: exec1_def)


[STATEMENT]
lemma exec_appendR:
 "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P @ P' \<turnstile> c \<rightarrow>* c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P @ P' \<turnstile> c \<rightarrow>* c'
[PROOF STEP]
by (induction rule: star.induct) (fastforce intro: star.step exec1_appendR)+


[STATEMENT]
lemma exec1_appendL:
  fixes i i' :: int
  shows "P \<turnstile> (i, s, stk) \<rightarrow> (i', s', stk') \<Longrightarrow>
    P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow> (size P' + i', s', stk')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> (i, s, stk) \<rightarrow> (i', s', stk') \<Longrightarrow> P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow> (size P' + i', s', stk')
[PROOF STEP]
by (auto simp: exec1_def iexec_simp simp del: iexec.simps)


[STATEMENT]
lemma exec_appendL:
  fixes i i' :: int
  shows "P \<turnstile> (i, s, stk) \<rightarrow>* (i', s', stk') \<Longrightarrow>
    P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow>* (size P' + i', s', stk')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> (i, s, stk) \<rightarrow>* (i', s', stk') \<Longrightarrow> P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow>* (size P' + i', s', stk')
[PROOF STEP]
by (induction rule: exec_induct) (blast intro: star.step exec1_appendL)+


[STATEMENT]
lemma exec_Cons_1 [intro]:
 "P \<turnstile> (0, s, stk) \<rightarrow>* (j, t, stk') \<Longrightarrow>
    ins # P \<turnstile> (1, s, stk) \<rightarrow>* (1 + j, t, stk')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> (0, s, stk) \<rightarrow>* (j, t, stk') \<Longrightarrow> ins # P \<turnstile> (1, s, stk) \<rightarrow>* (1 + j, t, stk')
[PROOF STEP]
by (drule exec_appendL [where P' = "[ins]"]) simp


[STATEMENT]
lemma exec_appendL_if [intro]:
  fixes i i' j :: int
  shows "\<lbrakk>size P' \<le> i; P \<turnstile> (i - size P', s, stk) \<rightarrow>* (j, s', stk');
    i' = size P' + j\<rbrakk> \<Longrightarrow>
      P' @ P \<turnstile> (i, s, stk) \<rightarrow>* (i', s', stk')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size P' \<le> i; P \<turnstile> (i - size P', s, stk) \<rightarrow>* (j, s', stk'); i' = size P' + j\<rbrakk> \<Longrightarrow> P' @ P \<turnstile> (i, s, stk) \<rightarrow>* (i', s', stk')
[PROOF STEP]
by (drule exec_appendL [where P' = P']) simp


[STATEMENT]
lemma exec_append_trans [intro]:
  fixes i' i'' j'' :: int
  shows "\<lbrakk>P \<turnstile> (0, s, stk) \<rightarrow>* (i', s', stk'); size P \<le> i';
    P' \<turnstile> (i' - size P, s', stk') \<rightarrow>* (i'', s'', stk''); j'' = size P + i''\<rbrakk> \<Longrightarrow>
      P @ P' \<turnstile> (0, s, stk) \<rightarrow>* (j'', s'', stk'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> (0, s, stk) \<rightarrow>* (i', s', stk'); size P \<le> i'; P' \<turnstile> (i' - size P, s', stk') \<rightarrow>* (i'', s'', stk''); j'' = size P + i''\<rbrakk> \<Longrightarrow> P @ P' \<turnstile> (0, s, stk) \<rightarrow>* (j'', s'', stk'')
[PROOF STEP]
by (metis star_trans [OF exec_appendR exec_appendL_if])


[STATEMENT]
lemma acomp_correct [intro]:
 "acomp a \<turnstile> (0, s, stk) \<rightarrow>* (size (acomp a), s, aval a s # stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acomp a \<turnstile> (0, s, stk) \<rightarrow>* (size (acomp a), s, aval a s # stk)
[PROOF STEP]
by (induction a arbitrary: stk) fastforce+


[STATEMENT]
lemma bcomp_correct [intro]:
  fixes i :: int
  shows "0 \<le> i \<Longrightarrow> bcomp (b, f, i) \<turnstile> (0, s, stk) \<rightarrow>*
    (size (bcomp (b, f, i)) + (if f = bval b s then i else 0), s, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> i \<Longrightarrow> bcomp (b, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b, f, i)) + (if f = bval b s then i else 0), s, stk)
[PROOF STEP]
proof (induction b arbitrary: f i)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x f i. 0 \<le> i \<Longrightarrow> bcomp (Bc x, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Bc x, f, i)) + (if f = bval (Bc x) s then i else 0), s, stk)
 2. \<And>b f i. \<lbrakk>\<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b, f, i)) + (if f = bval b s then i else 0), s, stk); 0 \<le> i\<rbrakk> \<Longrightarrow> bcomp (bexp.Not b, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (bexp.Not b, f, i)) + (if f = bval (bexp.Not b) s then i else 0), s, stk)
 3. \<And>b1 b2 f i. \<lbrakk>\<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b1, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b1, f, i)) + (if f = bval b1 s then i else 0), s, stk); \<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b2, f, i)) + (if f = bval b2 s then i else 0), s, stk); 0 \<le> i\<rbrakk> \<Longrightarrow> bcomp (And b1 b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (And b1 b2, f, i)) + (if f = bval (And b1 b2) s then i else 0), s, stk)
 4. \<And>x1a x2a f i. 0 \<le> i \<Longrightarrow> bcomp (Less x1a x2a, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Less x1a x2a, f, i)) + (if f = bval (Less x1a x2a) s then i else 0), s, stk)
[PROOF STEP]
case Not
[PROOF STATE]
proof (state)
this:
0 \<le> ?i \<Longrightarrow> bcomp (b_, ?f, ?i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b_, ?f, ?i)) + (if ?f = bval b_ s then ?i else 0), s, stk)
0 \<le> i

goal (4 subgoals):
 1. \<And>x f i. 0 \<le> i \<Longrightarrow> bcomp (Bc x, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Bc x, f, i)) + (if f = bval (Bc x) s then i else 0), s, stk)
 2. \<And>b f i. \<lbrakk>\<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b, f, i)) + (if f = bval b s then i else 0), s, stk); 0 \<le> i\<rbrakk> \<Longrightarrow> bcomp (bexp.Not b, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (bexp.Not b, f, i)) + (if f = bval (bexp.Not b) s then i else 0), s, stk)
 3. \<And>b1 b2 f i. \<lbrakk>\<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b1, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b1, f, i)) + (if f = bval b1 s then i else 0), s, stk); \<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b2, f, i)) + (if f = bval b2 s then i else 0), s, stk); 0 \<le> i\<rbrakk> \<Longrightarrow> bcomp (And b1 b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (And b1 b2, f, i)) + (if f = bval (And b1 b2) s then i else 0), s, stk)
 4. \<And>x1a x2a f i. 0 \<le> i \<Longrightarrow> bcomp (Less x1a x2a, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Less x1a x2a, f, i)) + (if f = bval (Less x1a x2a) s then i else 0), s, stk)
[PROOF STEP]
from Not(1) [where f = "\<not> f"] Not(2)
[PROOF STATE]
proof (chain)
picking this:
0 \<le> ?i \<Longrightarrow> bcomp (b_, \<not> f, ?i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b_, \<not> f, ?i)) + (if (\<not> f) = bval b_ s then ?i else 0), s, stk)
0 \<le> i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?i \<Longrightarrow> bcomp (b_, \<not> f, ?i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b_, \<not> f, ?i)) + (if (\<not> f) = bval b_ s then ?i else 0), s, stk)
0 \<le> i

goal (1 subgoal):
 1. bcomp (bexp.Not b_, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (bexp.Not b_, f, i)) + (if f = bval (bexp.Not b_) s then i else 0), s, stk)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bcomp (bexp.Not b_, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (bexp.Not b_, f, i)) + (if f = bval (bexp.Not b_) s then i else 0), s, stk)

goal (3 subgoals):
 1. \<And>x f i. 0 \<le> i \<Longrightarrow> bcomp (Bc x, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Bc x, f, i)) + (if f = bval (Bc x) s then i else 0), s, stk)
 2. \<And>b1 b2 f i. \<lbrakk>\<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b1, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b1, f, i)) + (if f = bval b1 s then i else 0), s, stk); \<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b2, f, i)) + (if f = bval b2 s then i else 0), s, stk); 0 \<le> i\<rbrakk> \<Longrightarrow> bcomp (And b1 b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (And b1 b2, f, i)) + (if f = bval (And b1 b2) s then i else 0), s, stk)
 3. \<And>x1a x2a f i. 0 \<le> i \<Longrightarrow> bcomp (Less x1a x2a, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Less x1a x2a, f, i)) + (if f = bval (Less x1a x2a) s then i else 0), s, stk)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x f i. 0 \<le> i \<Longrightarrow> bcomp (Bc x, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Bc x, f, i)) + (if f = bval (Bc x) s then i else 0), s, stk)
 2. \<And>b1 b2 f i. \<lbrakk>\<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b1, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b1, f, i)) + (if f = bval b1 s then i else 0), s, stk); \<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b2, f, i)) + (if f = bval b2 s then i else 0), s, stk); 0 \<le> i\<rbrakk> \<Longrightarrow> bcomp (And b1 b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (And b1 b2, f, i)) + (if f = bval (And b1 b2) s then i else 0), s, stk)
 3. \<And>x1a x2a f i. 0 \<le> i \<Longrightarrow> bcomp (Less x1a x2a, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Less x1a x2a, f, i)) + (if f = bval (Less x1a x2a) s then i else 0), s, stk)
[PROOF STEP]
case (And b\<^sub>1 b\<^sub>2)
[PROOF STATE]
proof (state)
this:
0 \<le> ?i \<Longrightarrow> bcomp (b\<^sub>1, ?f, ?i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b\<^sub>1, ?f, ?i)) + (if ?f = bval b\<^sub>1 s then ?i else 0), s, stk)
0 \<le> ?i \<Longrightarrow> bcomp (b\<^sub>2, ?f, ?i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b\<^sub>2, ?f, ?i)) + (if ?f = bval b\<^sub>2 s then ?i else 0), s, stk)
0 \<le> i

goal (3 subgoals):
 1. \<And>x f i. 0 \<le> i \<Longrightarrow> bcomp (Bc x, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Bc x, f, i)) + (if f = bval (Bc x) s then i else 0), s, stk)
 2. \<And>b1 b2 f i. \<lbrakk>\<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b1, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b1, f, i)) + (if f = bval b1 s then i else 0), s, stk); \<And>f i. 0 \<le> i \<Longrightarrow> bcomp (b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b2, f, i)) + (if f = bval b2 s then i else 0), s, stk); 0 \<le> i\<rbrakk> \<Longrightarrow> bcomp (And b1 b2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (And b1 b2, f, i)) + (if f = bval (And b1 b2) s then i else 0), s, stk)
 3. \<And>x1a x2a f i. 0 \<le> i \<Longrightarrow> bcomp (Less x1a x2a, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Less x1a x2a, f, i)) + (if f = bval (Less x1a x2a) s then i else 0), s, stk)
[PROOF STEP]
from And(1) [of "if f then size (bcomp (b\<^sub>2, f, i)) else
    size (bcomp (b\<^sub>2, f, i)) + i" False] And(2) [of i f] And(3)
[PROOF STATE]
proof (chain)
picking this:
0 \<le> (if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i) \<Longrightarrow> bcomp (b\<^sub>1, False, if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b\<^sub>1, False, if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i)) + (if False = bval b\<^sub>1 s then if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i else 0), s, stk)
0 \<le> i \<Longrightarrow> bcomp (b\<^sub>2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b\<^sub>2, f, i)) + (if f = bval b\<^sub>2 s then i else 0), s, stk)
0 \<le> i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> (if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i) \<Longrightarrow> bcomp (b\<^sub>1, False, if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b\<^sub>1, False, if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i)) + (if False = bval b\<^sub>1 s then if f then size (bcomp (b\<^sub>2, f, i)) else size (bcomp (b\<^sub>2, f, i)) + i else 0), s, stk)
0 \<le> i \<Longrightarrow> bcomp (b\<^sub>2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (b\<^sub>2, f, i)) + (if f = bval b\<^sub>2 s then i else 0), s, stk)
0 \<le> i

goal (1 subgoal):
 1. bcomp (And b\<^sub>1 b\<^sub>2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (And b\<^sub>1 b\<^sub>2, f, i)) + (if f = bval (And b\<^sub>1 b\<^sub>2) s then i else 0), s, stk)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bcomp (And b\<^sub>1 b\<^sub>2, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (And b\<^sub>1 b\<^sub>2, f, i)) + (if f = bval (And b\<^sub>1 b\<^sub>2) s then i else 0), s, stk)

goal (2 subgoals):
 1. \<And>x f i. 0 \<le> i \<Longrightarrow> bcomp (Bc x, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Bc x, f, i)) + (if f = bval (Bc x) s then i else 0), s, stk)
 2. \<And>x1a x2a f i. 0 \<le> i \<Longrightarrow> bcomp (Less x1a x2a, f, i) \<turnstile> (0, s, stk) \<rightarrow>* (size (bcomp (Less x1a x2a, f, i)) + (if f = bval (Less x1a x2a) s then i else 0), s, stk)
[PROOF STEP]
qed fastforce+