[STATEMENT]
theorem banach_steinhaus:
  fixes f::\<open>'c \<Rightarrow> ('a::banach \<Rightarrow>\<^sub>L 'b::real_normed_vector)\<close>
  assumes \<open>\<And>x. bounded (range (\<lambda>n. (f n) *\<^sub>v x))\<close>
  shows  \<open>bounded (range f)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded (range f)
[PROOF STEP]
text\<open>
  This is Banach-Steinhaus Theorem.

  Explanation: If a family of bounded operators on a Banach space
  is pointwise bounded, then it is uniformly bounded.
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded (range f)
[PROOF STEP]
proof(rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
assume \<open>\<not>(bounded (range f))\<close>
[PROOF STATE]
proof (state)
this:
\<not> bounded (range f)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have sum_1: \<open>\<exists>K. \<forall>n. sum (\<lambda>k. inverse (real_of_nat 3^k)) {0..n} \<le> K\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
have \<open>summable (\<lambda>n. inverse ((3::real) ^ n))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. inverse (3 ^ n))
[PROOF STEP]
by (simp flip: power_inverse)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. inverse (3 ^ n))

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
hence \<open>bounded (range (\<lambda>n. sum (\<lambda> k. inverse (real 3 ^ k)) {0..<n}))\<close>
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. inverse (3 ^ n))

goal (1 subgoal):
 1. bounded (range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)))
[PROOF STEP]
using summable_imp_sums_bounded[where f = "(\<lambda>n. inverse (real_of_nat 3^n))"]
        lessThan_atLeast0
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. inverse (3 ^ n))
summable (\<lambda>n. inverse (real 3 ^ n)) \<Longrightarrow> bounded (range (\<lambda>n. \<Sum>n<n. inverse (real 3 ^ n)))
{..<?n} = {0..<?n}

goal (1 subgoal):
 1. bounded (range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded (range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)))

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
hence \<open>\<exists>M. \<forall>h\<in>(range (\<lambda>n. sum (\<lambda> k. inverse (real 3 ^ k)) {0..<n})). norm h \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
bounded (range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)))

goal (1 subgoal):
 1. \<exists>M. \<forall>h\<in>range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)). norm h \<le> M
[PROOF STEP]
using bounded_iff
[PROOF STATE]
proof (prove)
using this:
bounded (range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)))
bounded ?S = (\<exists>a. \<forall>x\<in>?S. norm x \<le> a)

goal (1 subgoal):
 1. \<exists>M. \<forall>h\<in>range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)). norm h \<le> M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>M. \<forall>h\<in>range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)). norm h \<le> M

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>M. \<forall>h\<in>range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)). norm h \<le> M
[PROOF STEP]
obtain M where \<open>h\<in>range (\<lambda>n. sum (\<lambda> k. inverse (real 3 ^ k)) {0..<n}) \<Longrightarrow> norm h \<le> M\<close>
      for h
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>h\<in>range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)). norm h \<le> M

goal (1 subgoal):
 1. (\<And>M. (\<And>h. h \<in> range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)) \<Longrightarrow> norm h \<le> M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?h \<in> range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)) \<Longrightarrow> norm ?h \<le> M

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
have sum_2: \<open>sum (\<lambda>k. inverse (real_of_nat 3^k)) {0..n} \<le> M\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
have  \<open>norm (sum (\<lambda> k. inverse (real 3 ^ k)) {0..< Suc n}) \<le> M\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (\<Sum>k = 0..<Suc n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
using \<open>\<And>h. h\<in>(range (\<lambda>n. sum (\<lambda> k. inverse (real 3 ^ k)) {0..<n})) \<Longrightarrow> norm h \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
?h \<in> range (\<lambda>n. \<Sum>k = 0..<n. inverse (real 3 ^ k)) \<Longrightarrow> norm ?h \<le> M

goal (1 subgoal):
 1. norm (\<Sum>k = 0..<Suc n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (\<Sum>k = 0..<Suc n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
hence  \<open>norm (sum (\<lambda> k. inverse (real 3 ^ k)) {0..n}) \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
norm (\<Sum>k = 0..<Suc n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. norm (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
by (simp add: atLeastLessThanSuc_atLeastAtMost)
[PROOF STATE]
proof (state)
this:
norm (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
hence  \<open>(sum (\<lambda> k. inverse (real 3 ^ k)) {0..n}) \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
norm (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..?n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
have \<open>sum (\<lambda>k. inverse (real_of_nat 3^k)) {0..n} \<le> M\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
using sum_2
[PROOF STATE]
proof (prove)
using this:
(\<Sum>k = 0..?n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..?n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>k = 0..?n. inverse (real 3 ^ k)) \<le> M

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>of_rat 2/3 < (1::real)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat 2 / 3 < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat 2 / 3 < 1

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
hence \<open>\<forall>g::'a \<Rightarrow>\<^sub>L 'b. \<forall>x. \<forall>r. \<exists>\<xi>. g \<noteq> 0 \<and> r > 0
               \<longrightarrow> (\<xi>\<in>ball x r \<and> (of_rat 2/3) * r * norm g \<le> norm ((*\<^sub>v) g \<xi>))\<close>
[PROOF STATE]
proof (prove)
using this:
real_of_rat 2 / 3 < 1

goal (1 subgoal):
 1. \<forall>g x r. \<exists>\<xi>. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi>)
[PROOF STEP]
using onorm_Sup_on_ball'
[PROOF STATE]
proof (prove)
using this:
real_of_rat 2 / 3 < 1
\<lbrakk>0 < ?r; ?\<tau> < 1\<rbrakk> \<Longrightarrow> \<exists>\<xi>\<in>ball ?x ?r. ?\<tau> * ?r * norm ?f \<le> norm (?f *\<^sub>v \<xi>)

goal (1 subgoal):
 1. \<forall>g x r. \<exists>\<xi>. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>g x r. \<exists>\<xi>. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi>)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
hence \<open>\<exists>\<xi>. \<forall>g::'a \<Rightarrow>\<^sub>L 'b. \<forall>x. \<forall>r. g \<noteq> 0 \<and> r > 0
           \<longrightarrow> ((\<xi> g x r)\<in>ball x r \<and> (of_rat 2/3) * r * norm g \<le> norm ((*\<^sub>v) g (\<xi> g x r)))\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>g x r. \<exists>\<xi>. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi>)

goal (1 subgoal):
 1. \<exists>\<xi>. \<forall>g x r. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> g x r \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi> g x r)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>\<xi>. \<forall>g x r. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> g x r \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi> g x r)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<xi>. \<forall>g x r. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> g x r \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi> g x r)
[PROOF STEP]
obtain \<xi> where f1: \<open>\<lbrakk>g \<noteq> 0; r > 0\<rbrakk> \<Longrightarrow>
        \<xi> g x r \<in> ball x r \<and>  (of_rat 2/3) * r * norm g \<le> norm ((*\<^sub>v) g (\<xi> g x r))\<close>
    for g::\<open>'a \<Rightarrow>\<^sub>L 'b\<close> and x and r
[PROOF STATE]
proof (prove)
using this:
\<exists>\<xi>. \<forall>g x r. g \<noteq> 0 \<and> 0 < r \<longrightarrow> \<xi> g x r \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi> g x r)

goal (1 subgoal):
 1. (\<And>\<xi>. (\<And>g x r. \<lbrakk>g \<noteq> 0; 0 < r\<rbrakk> \<Longrightarrow> \<xi> g x r \<in> ball x r \<and> real_of_rat 2 / 3 * r * norm g \<le> norm (g *\<^sub>v \<xi> g x r)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?g \<noteq> 0; 0 < ?r\<rbrakk> \<Longrightarrow> \<xi> ?g ?x ?r \<in> ball ?x ?r \<and> real_of_rat 2 / 3 * ?r * norm ?g \<le> norm (?g *\<^sub>v \<xi> ?g ?x ?r)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>\<forall>n. \<exists>k. norm (f k) \<ge> 4^n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<exists>k. 4 ^ n \<le> norm (f k)
[PROOF STEP]
using \<open>\<not>(bounded (range f))\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> bounded (range f)

goal (1 subgoal):
 1. \<forall>n. \<exists>k. 4 ^ n \<le> norm (f k)
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) boundedI image_iff linear)
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>k. 4 ^ n \<le> norm (f k)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
hence  \<open>\<exists>k. \<forall>n. norm (f (k n)) \<ge> 4^n\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<exists>k. 4 ^ n \<le> norm (f k)

goal (1 subgoal):
 1. \<exists>k. \<forall>n. 4 ^ n \<le> norm (f (k n))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. 4 ^ n \<le> norm (f (k n))

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
hence  \<open>\<exists>k. \<forall>n. norm ((f \<circ> k) n) \<ge> 4^n\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>n. 4 ^ n \<le> norm (f (k n))

goal (1 subgoal):
 1. \<exists>k. \<forall>n. 4 ^ n \<le> norm ((f \<circ> k) n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. 4 ^ n \<le> norm ((f \<circ> k) n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. \<forall>n. 4 ^ n \<le> norm ((f \<circ> k) n)
[PROOF STEP]
obtain k where \<open>norm ((f \<circ> k) n) \<ge> 4^n\<close> for n
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>n. 4 ^ n \<le> norm ((f \<circ> k) n)

goal (1 subgoal):
 1. (\<And>k. (\<And>n. 4 ^ n \<le> norm ((f \<circ> k) n)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
4 ^ ?n \<le> norm ((f \<circ> k) ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
define T where \<open>T = f \<circ> k\<close>
[PROOF STATE]
proof (state)
this:
T = f \<circ> k

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>T n \<in> range f\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T n \<in> range f
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<circ> k) n \<in> range f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T ?n \<in> range f

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>norm (T n) \<ge> of_nat (4^n)\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (4 ^ n) \<le> norm (T n)
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (4 ^ n) \<le> norm ((f \<circ> k) n)
[PROOF STEP]
using \<open>\<And> n. norm ((f \<circ> k) n) \<ge> 4^n\<close>
[PROOF STATE]
proof (prove)
using this:
4 ^ ?n \<le> norm ((f \<circ> k) ?n)

goal (1 subgoal):
 1. real (4 ^ n) \<le> norm ((f \<circ> k) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (4 ^ ?n) \<le> norm (T ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
hence \<open>T n \<noteq> 0\<close> for n
[PROOF STATE]
proof (prove)
using this:
real (4 ^ ?n) \<le> norm (T ?n)

goal (1 subgoal):
 1. T n \<noteq> 0
[PROOF STEP]
by (smt T_def \<open>\<And>n. 4 ^ n \<le> norm ((f \<circ> k) n)\<close> norm_zero power_not_zero zero_le_power)
[PROOF STATE]
proof (state)
this:
T ?n \<noteq> 0

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>inverse (of_nat 3^n) > (0::real)\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < inverse (real 3 ^ n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
define y::\<open>nat \<Rightarrow> 'a\<close> where \<open>y = rec_nat 0 (\<lambda>n x. \<xi> (T n) x (inverse (of_nat 3^n)))\<close>
[PROOF STATE]
proof (state)
this:
y = rec_nat (0::'a) (\<lambda>n x. \<xi> (T n) x (inverse (real 3 ^ n)))

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>y (Suc n) \<in> ball (y n) (inverse (of_nat 3^n))\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y (Suc n) \<in> ball (y n) (inverse (real 3 ^ n))
[PROOF STEP]
using f1 \<open>\<And> n. T n \<noteq> 0\<close> \<open>\<And> n. inverse (of_nat 3^n) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?g \<noteq> 0; 0 < ?r\<rbrakk> \<Longrightarrow> \<xi> ?g ?x ?r \<in> ball ?x ?r \<and> real_of_rat 2 / 3 * ?r * norm ?g \<le> norm (?g *\<^sub>v \<xi> ?g ?x ?r)
T ?n \<noteq> 0
0 < inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. y (Suc n) \<in> ball (y n) (inverse (real 3 ^ n))
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?g \<noteq> 0; 0 < ?r\<rbrakk> \<Longrightarrow> \<xi> ?g ?x ?r \<in> ball ?x ?r \<and> real_of_rat 2 / 3 * ?r * norm ?g \<le> norm (?g *\<^sub>v \<xi> ?g ?x ?r)
T ?n \<noteq> 0
0 < inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. rec_nat (0::'a) (\<lambda>n x. \<xi> (T n) x (inverse (real 3 ^ n))) (Suc n) \<in> ball (rec_nat (0::'a) (\<lambda>n x. \<xi> (T n) x (inverse (real 3 ^ n))) n) (inverse (real 3 ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y (Suc ?n) \<in> ball (y ?n) (inverse (real 3 ^ ?n))

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
hence \<open>norm (y (Suc n) - y n) \<le> inverse (of_nat 3^n)\<close> for n
[PROOF STATE]
proof (prove)
using this:
y (Suc ?n) \<in> ball (y ?n) (inverse (real 3 ^ ?n))

goal (1 subgoal):
 1. norm (y (Suc n) - y n) \<le> inverse (real 3 ^ n)
[PROOF STEP]
unfolding ball_def
[PROOF STATE]
proof (prove)
using this:
y (Suc ?n) \<in> {ya. dist (y ?n) ya < inverse (real 3 ^ ?n)}

goal (1 subgoal):
 1. norm (y (Suc n) - y n) \<le> inverse (real 3 ^ n)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. dist (y n) (y (Suc n)) < inverse (3 ^ n)) \<Longrightarrow> norm (y (Suc n) - y n) \<le> inverse (3 ^ n)
[PROOF STEP]
using dist_norm
[PROOF STATE]
proof (prove)
using this:
dist ?x ?y = norm (?x - ?y)

goal (1 subgoal):
 1. (\<And>n. dist (y n) (y (Suc n)) < inverse (3 ^ n)) \<Longrightarrow> norm (y (Suc n) - y n) \<le> inverse (3 ^ n)
[PROOF STEP]
by (smt norm_minus_commute)
[PROOF STATE]
proof (state)
this:
norm (y (Suc ?n) - y ?n) \<le> inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
norm (y (Suc ?n) - y ?n) \<le> inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>\<exists>K. \<forall>n. sum (\<lambda>k. inverse (real_of_nat 3^k)) {0..n} \<le> K\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
using sum_1
[PROOF STATE]
proof (prove)
using this:
\<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K

goal (1 subgoal):
 1. \<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>Cauchy y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cauchy y
[PROOF STEP]
using convergent_series_Cauchy[where a = "\<lambda>n. inverse (of_nat 3^n)" and \<phi> = y] dist_norm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>M. \<forall>n. (\<Sum>n = 0..n. inverse (real 3 ^ n)) \<le> M; \<And>n. dist (y (Suc n)) (y n) \<le> inverse (real 3 ^ n)\<rbrakk> \<Longrightarrow> Cauchy y
dist ?x ?y = norm (?x - ?y)

goal (1 subgoal):
 1. Cauchy y
[PROOF STEP]
by (metis calculation(1) calculation(2))
[PROOF STATE]
proof (state)
this:
Cauchy y

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
hence \<open>\<exists> x. y \<longlonglongrightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
Cauchy y

goal (1 subgoal):
 1. \<exists>x. y \<longlonglongrightarrow> x
[PROOF STEP]
by (simp add: convergent_eq_Cauchy)
[PROOF STATE]
proof (state)
this:
\<exists>x. y \<longlonglongrightarrow> x

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. y \<longlonglongrightarrow> x
[PROOF STEP]
obtain x where \<open>y \<longlonglongrightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>x. y \<longlonglongrightarrow> x

goal (1 subgoal):
 1. (\<And>x. y \<longlonglongrightarrow> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<longlonglongrightarrow> x

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have norm_2: \<open>norm (x - y (Suc n)) \<le> (inverse (of_nat 2))*(inverse (of_nat 3^n))\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
have \<open>inverse (real_of_nat 3) < 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 3) < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverse (real 3) < 1

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inverse (real 3) < 1

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
have \<open>y 0 = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y 0 = (0::'a)
[PROOF STEP]
using y_def
[PROOF STATE]
proof (prove)
using this:
y = rec_nat (0::'a) (\<lambda>n x. \<xi> (T n) x (inverse (real 3 ^ n)))

goal (1 subgoal):
 1. y 0 = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y 0 = (0::'a)

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inverse (real 3) < 1
y 0 = (0::'a)
[PROOF STEP]
have \<open>norm (x - y (Suc n))
    \<le> (inverse (of_nat 3)) * inverse (1 - (inverse (of_nat 3))) * ((inverse (of_nat 3)) ^ n)\<close>
[PROOF STATE]
proof (prove)
using this:
inverse (real 3) < 1
y 0 = (0::'a)

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 3) * inverse (1 - inverse (real 3)) * inverse (real 3) ^ n
[PROOF STEP]
using bound_Cauchy_to_lim[where c = "inverse (of_nat 3)" and y = y and x = x]
        power_inverse semiring_norm(77)  \<open>y \<longlonglongrightarrow> x\<close>
        \<open>\<And> n. norm (y (Suc n) - y n) \<le> inverse (of_nat 3^n)\<close>
[PROOF STATE]
proof (prove)
using this:
inverse (real 3) < 1
y 0 = (0::'a)
\<lbrakk>y \<longlonglongrightarrow> x; \<And>n. norm (y (Suc n) - y n) \<le> inverse (real 3) ^ n; y 0 = (0::'a); inverse (real 3) < 1\<rbrakk> \<Longrightarrow> norm (x - y (Suc ?n)) \<le> inverse (real 3) / (1 - inverse (real 3)) * inverse (real 3) ^ ?n
inverse ?a ^ ?n = inverse (?a ^ ?n)
(num.One < num.Bit1 ?n) = True
y \<longlonglongrightarrow> x
norm (y (Suc ?n) - y ?n) \<le> inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 3) * inverse (1 - inverse (real 3)) * inverse (real 3) ^ n
[PROOF STEP]
by (metis divide_inverse)
[PROOF STATE]
proof (state)
this:
norm (x - y (Suc n)) \<le> inverse (real 3) * inverse (1 - inverse (real 3)) * inverse (real 3) ^ n

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
norm (x - y (Suc n)) \<le> inverse (real 3) * inverse (1 - inverse (real 3)) * inverse (real 3) ^ n

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
have \<open>inverse (real_of_nat 3) * inverse (1 - (inverse (of_nat 3)))
                   = inverse (of_nat 2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 3) * inverse (1 - inverse (real 3)) = inverse (real 2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inverse (real 3) * inverse (1 - inverse (real 3)) = inverse (real 2)

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
norm (x - y (Suc n)) \<le> inverse (real 3) * inverse (1 - inverse (real 3)) * inverse (real 3) ^ n
inverse (real 3) * inverse (1 - inverse (real 3)) = inverse (real 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (x - y (Suc n)) \<le> inverse (real 3) * inverse (1 - inverse (real 3)) * inverse (real 3) ^ n
inverse (real 3) * inverse (1 - inverse (real 3)) = inverse (real 2)

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
by (metis power_inverse)
[PROOF STATE]
proof (state)
this:
norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
norm (x - y (Suc ?n)) \<le> inverse (real 2) * inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>norm (x - y (Suc n)) \<le> (inverse (of_nat 2))*(inverse (of_nat 3^n))\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
using norm_2
[PROOF STATE]
proof (prove)
using this:
norm (x - y (Suc ?n)) \<le> inverse (real 2) * inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (x - y (Suc ?n)) \<le> inverse (real 2) * inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>\<exists> M. \<forall> n. norm ((*\<^sub>v) (T n) x) \<le> M\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. \<forall>n. norm (T n *\<^sub>v x) \<le> M
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. \<forall>n. norm ((f \<circ> k) n *\<^sub>v x) \<le> M
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. \<forall>n. norm (f (k n) *\<^sub>v x) \<le> M
[PROOF STEP]
by (metis \<open>\<And>x. bounded (range (\<lambda>n. (*\<^sub>v) (f n) x))\<close> bounded_iff rangeI)
[PROOF STATE]
proof (state)
this:
\<exists>M. \<forall>n. norm (T n *\<^sub>v x) \<le> M

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>M. \<forall>n. norm (T n *\<^sub>v x) \<le> M
[PROOF STEP]
obtain M where \<open>norm ((*\<^sub>v) (T n) x) \<le> M\<close> for n
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>n. norm (T n *\<^sub>v x) \<le> M

goal (1 subgoal):
 1. (\<And>M. (\<And>n. norm (T n *\<^sub>v x) \<le> M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (T ?n *\<^sub>v x) \<le> M

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have norm_1: \<open>norm (T n) * norm (y (Suc n) - x) + norm ((*\<^sub>v) (T n) x)
       \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm ((*\<^sub>v) (T n) x)\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>norm (y (Suc n) - x) \<le> (inverse (of_nat 2))*(inverse (of_nat 3^n))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
using \<open>norm (x - y (Suc n)) \<le> (inverse (of_nat 2))*(inverse (of_nat 3^n))\<close>
[PROOF STATE]
proof (prove)
using this:
norm (x - y (Suc n)) \<le> inverse (real 2) * inverse (real 3 ^ n)

goal (1 subgoal):
 1. norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n)
[PROOF STEP]
by (simp add: norm_minus_commute)
[PROOF STATE]
proof (state)
this:
norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n)

goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n)

goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>norm (T n) \<ge> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> norm (T n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> norm (T n)

goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n)
0 \<le> norm (T n)
[PROOF STEP]
have \<open>norm (T n) * norm (y (Suc n) - x)
                     \<le> (inverse (of_nat 2))*(inverse (of_nat 3^n))*norm (T n)\<close>
[PROOF STATE]
proof (prove)
using this:
norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n)
0 \<le> norm (T n)

goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
by (simp add: \<open>\<And>n. T n \<noteq> 0\<close>)
[PROOF STATE]
proof (state)
this:
norm (T n) * norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (T n) * norm (y (Suc n) - x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
norm (T ?n) * norm (y (Suc ?n) - x) + norm (T ?n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ ?n) * norm (T ?n) + norm (T ?n *\<^sub>v x)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have inverse_2: \<open>(inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)
                  \<le> norm ((*\<^sub>v) (T n) x)\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>(of_rat 2/3)*(inverse (of_nat 3^n))*norm (T n) \<le> norm ((*\<^sub>v) (T n) (y (Suc n)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v y (Suc n))
[PROOF STEP]
using f1 \<open>\<And> n. T n \<noteq> 0\<close> \<open>\<And> n. inverse (of_nat 3^n) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?g \<noteq> 0; 0 < ?r\<rbrakk> \<Longrightarrow> \<xi> ?g ?x ?r \<in> ball ?x ?r \<and> real_of_rat 2 / 3 * ?r * norm ?g \<le> norm (?g *\<^sub>v \<xi> ?g ?x ?r)
T ?n \<noteq> 0
0 < inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v y (Suc n))
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?g \<noteq> 0; 0 < ?r\<rbrakk> \<Longrightarrow> \<xi> ?g ?x ?r \<in> ball ?x ?r \<and> real_of_rat 2 / 3 * ?r * norm ?g \<le> norm (?g *\<^sub>v \<xi> ?g ?x ?r)
T ?n \<noteq> 0
0 < inverse (real 3 ^ ?n)

goal (1 subgoal):
 1. real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v rec_nat (0::'a) (\<lambda>n x. \<xi> (T n) x (inverse (real 3 ^ n))) (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v y (Suc n))

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v y (Suc n))

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>\<dots> = norm ((*\<^sub>v) (T n) ((y (Suc n) - x) + x))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (T n *\<^sub>v y (Suc n)) = norm (T n *\<^sub>v (y (Suc n) - x + x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v y (Suc n)) = norm (T n *\<^sub>v (y (Suc n) - x + x))

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v y (Suc n)) = norm (T n *\<^sub>v (y (Suc n) - x + x))

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>\<dots> = norm ((*\<^sub>v) (T n) (y (Suc n) - x) + (*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (T n *\<^sub>v (y (Suc n) - x + x)) = norm (T n *\<^sub>v (y (Suc n) - x) + T n *\<^sub>v x)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T n y x. pred_fun top bounded_linear T \<Longrightarrow> norm (T n (y (Suc n) - x + x)) = norm (T n (y (Suc n) - x) + T n x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T n y x. \<forall>x. bounded_linear (T x) \<Longrightarrow> norm (T n (y (Suc n))) = norm (T n (y (Suc n) - x) + T n x)
[PROOF STEP]
by (metis diff_add_cancel linear_simps(1))
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v (y (Suc n) - x + x)) = norm (T n *\<^sub>v (y (Suc n) - x) + T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v (y (Suc n) - x + x)) = norm (T n *\<^sub>v (y (Suc n) - x) + T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>\<dots> \<le> norm ((*\<^sub>v) (T n) (y (Suc n) - x)) + norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (T n *\<^sub>v (y (Suc n) - x) + T n *\<^sub>v x) \<le> norm (T n *\<^sub>v (y (Suc n) - x)) + norm (T n *\<^sub>v x)
[PROOF STEP]
by (simp add: norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v (y (Suc n) - x) + T n *\<^sub>v x) \<le> norm (T n *\<^sub>v (y (Suc n) - x)) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v (y (Suc n) - x) + T n *\<^sub>v x) \<le> norm (T n *\<^sub>v (y (Suc n) - x)) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>\<dots> \<le> norm (T n) * norm (y (Suc n) - x) + norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (T n *\<^sub>v (y (Suc n) - x)) + norm (T n *\<^sub>v x) \<le> norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T n y x. pred_fun top bounded_linear T \<Longrightarrow> norm (T n (y (Suc n) - x)) + norm (T n x) \<le> onorm (T n) * norm (y (Suc n) - x) + norm (T n x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T n y x. \<forall>x. bounded_linear (T x) \<Longrightarrow> norm (T n (y (Suc n) - x)) \<le> onorm (T n) * norm (y (Suc n) - x)
[PROOF STEP]
using onorm
[PROOF STATE]
proof (prove)
using this:
bounded_linear ?f \<Longrightarrow> norm (?f ?x) \<le> onorm ?f * norm ?x

goal (1 subgoal):
 1. \<And>T n y x. \<forall>x. bounded_linear (T x) \<Longrightarrow> norm (T n (y (Suc n) - x)) \<le> onorm (T n) * norm (y (Suc n) - x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v (y (Suc n) - x)) + norm (T n *\<^sub>v x) \<le> norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (T n *\<^sub>v (y (Suc n) - x)) + norm (T n *\<^sub>v x) \<le> norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>\<dots> \<le> (inverse (of_nat 2))*(inverse (of_nat 3^n))*norm (T n)
                + norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
using norm_1
[PROOF STATE]
proof (prove)
using this:
norm (T ?n) * norm (y (Suc ?n) - x) + norm (T ?n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ ?n) * norm (T ?n) + norm (T ?n *\<^sub>v x)

goal (1 subgoal):
 1. norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (T n) * norm (y (Suc n) - x) + norm (T n *\<^sub>v x) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>(of_rat 2/3) * inverse (real 3 ^ n) * norm (T n)
                \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n)
                + norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
hence \<open>(of_rat 2/3) * inverse (real 3 ^ n) * norm (T n)
             - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) \<le> norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) \<le> inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>(of_rat 2/3) * inverse (real 3 ^ n) * norm (T n)
             - inverse (real 2) * inverse (real 3 ^ n) * norm (T n)
             = (inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) = inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) = inverse (real 6) * inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) = inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
show \<open>(inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n) \<le> norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
real_of_rat 2 / 3 * inverse (real 3 ^ n) * norm (T n) - inverse (real 2) * inverse (real 3 ^ n) * norm (T n) = inverse (real 6) * inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverse (real 6) * inverse (real 3 ^ ?n) * norm (T ?n) \<le> norm (T ?n *\<^sub>v x)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have inverse_3: \<open>(inverse (of_nat 6)) * (of_rat (4/3)^n)
                    \<le> (inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
have \<open>of_rat (4/3)^n = inverse (real 3 ^ n) * (of_nat 4^n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat (4 / 3) ^ n = inverse (real 3 ^ n) * real 4 ^ n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat (4 / 3) ^ n = inverse (3 ^ n) * 4 ^ n
[PROOF STEP]
by (metis divide_inverse_commute of_rat_divide power_divide of_rat_numeral_eq)
[PROOF STATE]
proof (state)
this:
real_of_rat (4 / 3) ^ n = inverse (real 3 ^ n) * real 4 ^ n

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_rat (4 / 3) ^ n = inverse (real 3 ^ n) * real 4 ^ n

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
have \<open>\<dots> \<le>  inverse (real 3 ^ n) * norm (T n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 3 ^ n) * real 4 ^ n \<le> inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
using \<open>\<And>n. norm (T n) \<ge> of_nat (4^n)\<close>
[PROOF STATE]
proof (prove)
using this:
real (4 ^ ?n) \<le> norm (T ?n)

goal (1 subgoal):
 1. inverse (real 3 ^ n) * real 4 ^ n \<le> inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverse (real 3 ^ n) * real 4 ^ n \<le> inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_rat (4 / 3) ^ n \<le> inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
have \<open>of_rat (4/3)^n \<le> inverse (real 3 ^ n) * norm (T n)\<close>
[PROOF STATE]
proof (prove)
using this:
real_of_rat (4 / 3) ^ n \<le> inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. real_of_rat (4 / 3) ^ n \<le> inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
real_of_rat (4 / 3) ^ n \<le> inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_rat (4 / 3) ^ n \<le> inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
have \<open>inverse (of_nat 6) > (0::real)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < inverse (real 6)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < inverse (real 6)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_of_rat (4 / 3) ^ n \<le> inverse (real 3 ^ n) * norm (T n)
0 < inverse (real 6)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_rat (4 / 3) ^ n \<le> inverse (real 3 ^ n) * norm (T n)
0 < inverse (real 6)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ ?n \<le> inverse (real 6) * inverse (real 3 ^ ?n) * norm (T ?n)

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have inverse_1: \<open>(inverse (of_nat 6)) * (of_rat (4/3)^n) \<le> M\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
have \<open>(inverse (of_nat 6)) * (of_rat (4/3)^n)
          \<le> (inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
using inverse_3
[PROOF STATE]
proof (prove)
using this:
inverse (real 6) * real_of_rat (4 / 3) ^ ?n \<le> inverse (real 6) * inverse (real 3 ^ ?n) * norm (T ?n)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> inverse (real 6) * inverse (real 3 ^ n) * norm (T n)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
have \<open>\<dots> \<le> norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
using inverse_2
[PROOF STATE]
proof (prove)
using this:
inverse (real 6) * inverse (real 3 ^ ?n) * norm (T ?n) \<le> norm (T ?n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse (real 6) * inverse (real 3 ^ n) * norm (T n) \<le> norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
have \<open>(inverse (of_nat 6)) * (of_rat (4/3)^n) \<le> norm ((*\<^sub>v) (T n) x)\<close>
[PROOF STATE]
proof (prove)
using this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> norm (T n *\<^sub>v x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> norm (T n *\<^sub>v x)

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
using \<open>\<And> n. norm ((*\<^sub>v) (T n) x) \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> norm (T n *\<^sub>v x)
norm (T ?n *\<^sub>v x) \<le> M

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ ?n \<le> M

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>\<exists>n. M < (inverse (of_nat 6)) * (of_rat (4/3)^n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. M < inverse (real 6) * real_of_rat (4 / 3) ^ n
[PROOF STEP]
using Real.real_arch_pow
[PROOF STATE]
proof (prove)
using this:
1 < ?x \<Longrightarrow> \<exists>n. ?y < ?x ^ n

goal (1 subgoal):
 1. \<exists>n. M < inverse (real 6) * real_of_rat (4 / 3) ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. M < inverse (real 6) * real_of_rat (4 / 3) ^ n

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>n. M < inverse (real 6) * real_of_rat (4 / 3) ^ n

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
have \<open>(inverse (of_nat 6)) * (of_rat (4/3)^n) \<le> M\<close> for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
using inverse_1
[PROOF STATE]
proof (prove)
using this:
inverse (real 6) * real_of_rat (4 / 3) ^ ?n \<le> M

goal (1 subgoal):
 1. inverse (real 6) * real_of_rat (4 / 3) ^ n \<le> M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse (real 6) * real_of_rat (4 / 3) ^ ?n \<le> M

goal (1 subgoal):
 1. \<not> bounded (range f) \<Longrightarrow> bounded (range f)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
norm (y (Suc ?n) - y ?n) \<le> inverse (real 3 ^ ?n)
\<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
\<exists>n. M < inverse (real 6) * real_of_rat (4 / 3) ^ n
inverse (real 6) * real_of_rat (4 / 3) ^ ?n \<le> M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (y (Suc ?n) - y ?n) \<le> inverse (real 3 ^ ?n)
\<exists>K. \<forall>n. (\<Sum>k = 0..n. inverse (real 3 ^ k)) \<le> K
\<exists>n. M < inverse (real 6) * real_of_rat (4 / 3) ^ n
inverse (real 6) * real_of_rat (4 / 3) ^ ?n \<le> M

goal (1 subgoal):
 1. bounded (range f)
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
bounded (range f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "\<And>f x::'a af. f \<diamondop> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. f \<diamondop> x = x
[PROOF STEP]
apply applicative_nf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. pure (\<lambda>x. x) \<diamondop> f = pure (\<lambda>x. x)
[PROOF STEP]
oops


[STATEMENT]
lemma "(X :: _ :: semigroup_add set) + Y + Z = X + (Y + Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X + Y + Z = X + (Y + Z)
[PROOF STEP]
by (fact add.assoc[applicative_lifted set])


[STATEMENT]
lemma "Inl plus \<diamondop> (x :: nat + 'e list) \<diamondop> x = Inl (\<lambda>x. 2 * x) \<diamondop> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inl (+) \<diamondop> x \<diamondop> x = Inl ((*) 2) \<diamondop> x
[PROOF STEP]
by applicative_lifting simp


[STATEMENT]
lemma "rel_sum (\<le>) (\<le>) (x :: nat + nat) (Inl Suc \<diamondop> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_sum (\<le>) (\<le>) x (Inl Suc \<diamondop> x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_sum (\<le>) (\<le>) x (Inl Suc \<diamondop> x)
[PROOF STEP]
interpret either_af "(\<le>) :: nat \<Rightarrow> _"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. either_af (\<le>)
[PROOF STEP]
by unfold_locales (rule reflpI, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_sum (\<le>) (\<le>) x (Inl Suc \<diamondop> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_sum (\<le>) (\<le>) x (Inl Suc \<diamondop> x)
[PROOF STEP]
by applicative_lifting simp
[PROOF STATE]
proof (state)
this:
rel_sum (\<le>) (\<le>) x (Inl Suc \<diamondop> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "(x::int stream) * sconst 0 = sconst 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * pure 0 = pure 0
[PROOF STEP]
by applicative_lifting simp


[STATEMENT]
lemma "(x::int stream) * (y + z) = x * y + x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y + z) = x * y + x * z
[PROOF STEP]
by applicative_lifting algebra


[STATEMENT]
lemma lift_streams_Nil[applicative_unfold]: "lift_streams [] = sconst []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_streams [] = pure []
[PROOF STEP]
unfolding lift_streams_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (smap2 (#)) [] (pure []) = pure []
[PROOF STEP]
by simp


[STATEMENT]
lemma lift_streams_Cons[applicative_unfold]:
  "lift_streams (x # xs) = smap2 Cons x (lift_streams xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_streams (x # xs) = smap2 (#) x (lift_streams xs)
[PROOF STEP]
unfolding lift_streams_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (smap2 (#)) (x # xs) (pure []) = smap2 (#) x (foldr (smap2 (#)) xs (pure []))
[PROOF STEP]
by applicative_unfold


[STATEMENT]
lemma stream_append_Cons: "smap2 append (smap2 Cons x ys) zs = smap2 Cons x (smap2 append ys zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap2 (@) (smap2 (#) x ys) zs = smap2 (#) x (smap2 (@) ys zs)
[PROOF STEP]
by applicative_lifting simp


[STATEMENT]
lemma lift_streams_append[applicative_unfold]:
  "lift_streams (xs @ ys) = smap2 append (lift_streams xs) (lift_streams ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lift_streams ([] @ ys) = smap2 (@) (lift_streams []) (lift_streams ys)
 2. \<And>a xs. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys) \<Longrightarrow> lift_streams ((a # xs) @ ys) = smap2 (@) (lift_streams (a # xs)) (lift_streams ys)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. lift_streams ([] @ ys) = smap2 (@) (lift_streams []) (lift_streams ys)
 2. \<And>a xs. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys) \<Longrightarrow> lift_streams ((a # xs) @ ys) = smap2 (@) (lift_streams (a # xs)) (lift_streams ys)
[PROOF STEP]
(*
    case could be proved directly if "lift_streams ([] @ ys) = lift_streams ys" is solved
    in head_cong_tac (invoke simplifier?) -- but only with applicative_nf
  *)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. lift_streams ([] @ ys) = smap2 (@) (lift_streams []) (lift_streams ys)
 2. \<And>a xs. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys) \<Longrightarrow> lift_streams ((a # xs) @ ys) = smap2 (@) (lift_streams (a # xs)) (lift_streams ys)
[PROOF STEP]
have "lift_streams ys = sconst append \<diamondop> lift_streams [] \<diamondop> lift_streams ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_streams ys = pure (@) \<diamondop> lift_streams [] \<diamondop> lift_streams ys
[PROOF STEP]
by applicative_lifting simp
[PROOF STATE]
proof (state)
this:
lift_streams ys = pure (@) \<diamondop> lift_streams [] \<diamondop> lift_streams ys

goal (2 subgoals):
 1. lift_streams ([] @ ys) = smap2 (@) (lift_streams []) (lift_streams ys)
 2. \<And>a xs. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys) \<Longrightarrow> lift_streams ((a # xs) @ ys) = smap2 (@) (lift_streams (a # xs)) (lift_streams ys)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
lift_streams ys = pure (@) \<diamondop> lift_streams [] \<diamondop> lift_streams ys

goal (1 subgoal):
 1. lift_streams ([] @ ys) = smap2 (@) (lift_streams []) (lift_streams ys)
[PROOF STEP]
by applicative_unfold
[PROOF STATE]
proof (state)
this:
lift_streams ([] @ ys) = smap2 (@) (lift_streams []) (lift_streams ys)

goal (1 subgoal):
 1. \<And>a xs. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys) \<Longrightarrow> lift_streams ((a # xs) @ ys) = smap2 (@) (lift_streams (a # xs)) (lift_streams ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys) \<Longrightarrow> lift_streams ((a # xs) @ ys) = smap2 (@) (lift_streams (a # xs)) (lift_streams ys)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys)

goal (1 subgoal):
 1. \<And>a xs. lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys) \<Longrightarrow> lift_streams ((a # xs) @ ys) = smap2 (@) (lift_streams (a # xs)) (lift_streams ys)
[PROOF STEP]
with stream_append_Cons
[PROOF STATE]
proof (chain)
picking this:
smap2 (@) (smap2 (#) ?x ?ys) ?zs = smap2 (#) ?x (smap2 (@) ?ys ?zs)
lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys)
[PROOF STEP]
(* the actual lifted fact *)
[PROOF STATE]
proof (chain)
picking this:
smap2 (@) (smap2 (#) ?x ?ys) ?zs = smap2 (#) ?x (smap2 (@) ?ys ?zs)
lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
smap2 (@) (smap2 (#) ?x ?ys) ?zs = smap2 (#) ?x (smap2 (@) ?ys ?zs)
lift_streams (xs @ ys) = smap2 (@) (lift_streams xs) (lift_streams ys)

goal (1 subgoal):
 1. lift_streams ((x # xs) @ ys) = smap2 (@) (lift_streams (x # xs)) (lift_streams ys)
[PROOF STEP]
by applicative_unfold (rule sym)
[PROOF STATE]
proof (state)
this:
lift_streams ((x # xs) @ ys) = smap2 (@) (lift_streams (x # xs)) (lift_streams ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "lift_streams (rev x) = smap rev (lift_streams x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_streams (rev x) = smap rev (lift_streams x)
[PROOF STEP]
proof (induction x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lift_streams (rev []) = smap rev (lift_streams [])
 2. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. lift_streams (rev []) = smap rev (lift_streams [])
 2. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
have "lift_streams [] = smap rev (lift_streams [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_streams [] = smap rev (lift_streams [])
[PROOF STEP]
by applicative_lifting simp
[PROOF STATE]
proof (state)
this:
lift_streams [] = smap rev (lift_streams [])

goal (2 subgoals):
 1. lift_streams (rev []) = smap rev (lift_streams [])
 2. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
lift_streams [] = smap rev (lift_streams [])

goal (1 subgoal):
 1. lift_streams (rev []) = smap rev (lift_streams [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lift_streams (rev []) = smap rev (lift_streams [])

goal (1 subgoal):
 1. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
lift_streams (rev xs) = smap rev (lift_streams xs)

goal (1 subgoal):
 1. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
have "\<forall>y ys. rev ys @ [y] = rev (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y ys. rev ys @ [y] = rev (y # ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>y ys. rev ys @ [y] = rev (y # ys)

goal (1 subgoal):
 1. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
hence "\<forall>y ys. smap2 append (smap rev ys) (smap2 Cons y (sconst [])) = smap rev (smap2 Cons y ys)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y ys. rev ys @ [y] = rev (y # ys)

goal (1 subgoal):
 1. \<forall>y ys. smap2 (@) (smap rev ys) (smap2 (#) y (pure [])) = smap rev (smap2 (#) y ys)
[PROOF STEP]
by applicative_lifting simp
[PROOF STATE]
proof (state)
this:
\<forall>y ys. smap2 (@) (smap rev ys) (smap2 (#) y (pure [])) = smap rev (smap2 (#) y ys)

goal (1 subgoal):
 1. \<And>a x. lift_streams (rev x) = smap rev (lift_streams x) \<Longrightarrow> lift_streams (rev (a # x)) = smap rev (lift_streams (a # x))
[PROOF STEP]
with Cons.IH
[PROOF STATE]
proof (chain)
picking this:
lift_streams (rev xs) = smap rev (lift_streams xs)
\<forall>y ys. smap2 (@) (smap rev ys) (smap2 (#) y (pure [])) = smap rev (smap2 (#) y ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lift_streams (rev xs) = smap rev (lift_streams xs)
\<forall>y ys. smap2 (@) (smap rev ys) (smap2 (#) y (pure [])) = smap rev (smap2 (#) y ys)

goal (1 subgoal):
 1. lift_streams (rev (x # xs)) = smap rev (lift_streams (x # xs))
[PROOF STEP]
by applicative_unfold blast
[PROOF STATE]
proof (state)
this:
lift_streams (rev (x # xs)) = smap rev (lift_streams (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "sconcat (lift_streams [sconst ''Hello '', sconst ''world!'']) = sconst ''Hello world!''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcat (lift_streams [pure ''Hello '', pure ''world!'']) = pure ''Hello world!''
[PROOF STEP]
by applicative_lifting simp


[STATEMENT]
lemma "rel_fun (=) (\<le>) (const (0::nat)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (=) (\<le>) (pure 0) x
[PROOF STEP]
by applicative_lifting simp


[STATEMENT]
lemma "list_all2 (\<subseteq>) (map (\<lambda>_. {}) x) (map set x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<subseteq>) (map (\<lambda>_. {}) x) (map set x)
[PROOF STEP]
by applicative_nf simp


[STATEMENT]
lemma "x = Some a \<Longrightarrow> rel_option (\<le>) (map_option (\<lambda>_. a) x) (map_option Suc x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = Some a \<Longrightarrow> rel_option (\<le>) (map_option (\<lambda>_. a) x) (map_option Suc x)
[PROOF STEP]
by applicative_lifting simp


[STATEMENT]
lemma MMU_register_induct:
  "P CR \<Longrightarrow> P CTP \<Longrightarrow> P CNR \<Longrightarrow> P FTSR \<Longrightarrow> P FAR
   \<Longrightarrow> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P CR; P CTP; P CNR; P FTSR; P FAR\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
by (cases x) auto


[STATEMENT]
lemma UNIV_MMU_register [no_atp]: "UNIV = {CR, CTP, CNR, FTSR, FAR}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = {CR, CTP, CNR, FTSR, FAR}
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>x \<in> UNIV; x \<noteq> CR; x \<noteq> CTP; x \<noteq> CNR; x \<noteq> FTSR; x \<notin> {}\<rbrakk> \<Longrightarrow> x = FAR
 2. \<And>x. CR \<in> UNIV
 3. \<And>x. CTP \<in> UNIV
 4. \<And>x. CNR \<in> UNIV
 5. \<And>x. FTSR \<in> UNIV
 6. \<And>x. FAR \<in> UNIV
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>x. \<lbrakk>x \<in> UNIV; x \<noteq> CR; x \<noteq> CTP; x \<noteq> CNR; x \<noteq> FTSR; x \<notin> {}; x = CR\<rbrakk> \<Longrightarrow> x = FAR
 2. \<And>x. \<lbrakk>x \<in> UNIV; x \<noteq> CR; x \<noteq> CTP; x \<noteq> CNR; x \<noteq> FTSR; x \<notin> {}; x = CTP\<rbrakk> \<Longrightarrow> x = FAR
 3. \<And>x. \<lbrakk>x \<in> UNIV; x \<noteq> CR; x \<noteq> CTP; x \<noteq> CNR; x \<noteq> FTSR; x \<notin> {}; x = CNR\<rbrakk> \<Longrightarrow> x = FAR
 4. \<And>x. \<lbrakk>x \<in> UNIV; x \<noteq> CR; x \<noteq> CTP; x \<noteq> CNR; x \<noteq> FTSR; x \<notin> {}; x = FTSR\<rbrakk> \<Longrightarrow> x = FAR
 5. \<And>x. \<lbrakk>x \<in> UNIV; x \<noteq> CR; x \<noteq> CTP; x \<noteq> CNR; x \<noteq> FTSR; x \<notin> {}; x = FAR\<rbrakk> \<Longrightarrow> x = FAR
 6. \<And>x. CR \<in> UNIV
 7. \<And>x. CTP \<in> UNIV
 8. \<And>x. CNR \<in> UNIV
 9. \<And>x. FTSR \<in> UNIV
 10. \<And>x. FAR \<in> UNIV
[PROOF STEP]
apply (auto intro:MMU_register_induct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_list_of_set: "finite s \<Longrightarrow> set (list_of_set s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s \<Longrightarrow> set (list_of_set s) = s
[PROOF STEP]
unfolding list_of_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s \<Longrightarrow> set (SOME l. set l = s) = s
[PROOF STEP]
by (metis (mono_tags) finite_list some_eq_ex)


[STATEMENT]
lemma basevars: "basevars vs \<Longrightarrow> \<exists>u. vs u = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basevars vs \<Longrightarrow> \<exists>u. vs u = c
[PROOF STEP]
proof (unfold basevars_def surj_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>y. \<exists>x. y = vs x \<Longrightarrow> \<exists>u. vs u = c
[PROOF STEP]
assume "\<forall>y. \<exists>x. y = vs x"
[PROOF STATE]
proof (state)
this:
\<forall>y. \<exists>x. y = vs x

goal (1 subgoal):
 1. \<forall>y. \<exists>x. y = vs x \<Longrightarrow> \<exists>u. vs u = c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. \<exists>x. y = vs x
[PROOF STEP]
obtain x where "c = vs x"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>x. y = vs x

goal (1 subgoal):
 1. (\<And>x. c = vs x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c = vs x

goal (1 subgoal):
 1. \<forall>y. \<exists>x. y = vs x \<Longrightarrow> \<exists>u. vs u = c
[PROOF STEP]
thus "\<exists>u. vs u = c"
[PROOF STATE]
proof (prove)
using this:
c = vs x

goal (1 subgoal):
 1. \<exists>u. vs u = c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>u. vs u = c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma baseE:
  assumes H1: "basevars v" and H2:"\<And>x. v x = c \<Longrightarrow> Q"
  shows "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
using H1[THEN basevars] H2
[PROOF STATE]
proof (prove)
using this:
\<exists>u. v u = ?c
v ?x = c \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by auto


[STATEMENT]
lemma first_baseE:
  assumes H1: "basevars v" and H2: "\<And>x. v (first x) = c \<Longrightarrow> Q"
  shows "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
using H1[THEN basevars] H2
[PROOF STATE]
proof (prove)
using this:
\<exists>u. v u = ?c
v (first ?x) = c \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by (force simp: first_def)


[STATEMENT]
lemma base_pair1:
  assumes h: "basevars (x,y)"
  shows "basevars x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basevars x
[PROOF STEP]
proof (auto simp: basevars_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> range x
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> range x
[PROOF STEP]
from h[THEN basevars]
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. (x, y) u = ?c
[PROOF STEP]
obtain s where "(LIFT (x,y)) s = (c, arbitrary)"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. (x, y) u = ?c

goal (1 subgoal):
 1. (\<And>s. (x, y) s = (c, arbitrary) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) s = (c, arbitrary)

goal (1 subgoal):
 1. \<And>xa. xa \<in> range x
[PROOF STEP]
thus "c \<in> range x"
[PROOF STATE]
proof (prove)
using this:
(x, y) s = (c, arbitrary)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma base_pair2:
  assumes h: "basevars (x,y)"
  shows "basevars y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basevars y
[PROOF STEP]
proof (auto simp: basevars_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range y
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range y
[PROOF STEP]
from h[THEN basevars]
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. (x, y) u = ?c
[PROOF STEP]
obtain s where "(LIFT (x,y)) s = (arbitrary, d)"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. (x, y) u = ?c

goal (1 subgoal):
 1. (\<And>s. (x, y) s = (arbitrary, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) s = (arbitrary, d)

goal (1 subgoal):
 1. \<And>x. x \<in> range y
[PROOF STEP]
thus "d \<in> range y"
[PROOF STATE]
proof (prove)
using this:
(x, y) s = (arbitrary, d)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma base_pair: "basevars (x,y) \<Longrightarrow> basevars x \<and> basevars y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basevars (x, y) \<Longrightarrow> basevars x \<and> basevars y
[PROOF STEP]
by (auto elim: base_pair1 base_pair2)


[STATEMENT]
lemma unit_base: "basevars (v::state \<Rightarrow> unit)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basevars v
[PROOF STEP]
by (auto simp: basevars_def)


[STATEMENT]
lemma base_enabled:
  assumes h1: "basevars vs"
  and h2: "\<And>u. vs (first u) = c \<Longrightarrow> ((first s) ## u) \<Turnstile> F"
  shows "s \<Turnstile> Enabled F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Enabled F) s
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
basevars vs

goal (1 subgoal):
 1. (Enabled F) s
[PROOF STEP]
proof (rule first_baseE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. vs (first x) = ?c \<Longrightarrow> (Enabled F) s
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. vs (first x) = ?c \<Longrightarrow> (Enabled F) s
[PROOF STEP]
assume "vs (first t) = c"
[PROOF STATE]
proof (state)
this:
vs (first t) = c

goal (1 subgoal):
 1. \<And>x. vs (first x) = ?c \<Longrightarrow> (Enabled F) s
[PROOF STEP]
hence "((first s) ## t) \<Turnstile> F"
[PROOF STATE]
proof (prove)
using this:
vs (first t) = c

goal (1 subgoal):
 1. F (first s ## t)
[PROOF STEP]
by (rule h2)
[PROOF STATE]
proof (state)
this:
F (first s ## t)

goal (1 subgoal):
 1. \<And>x. vs (first x) = ?c \<Longrightarrow> (Enabled F) s
[PROOF STEP]
thus "s \<Turnstile> Enabled F"
[PROOF STATE]
proof (prove)
using this:
F (first s ## t)

goal (1 subgoal):
 1. (Enabled F) s
[PROOF STEP]
unfolding enabled_def
[PROOF STATE]
proof (prove)
using this:
F (first s ## t)

goal (1 subgoal):
 1. \<exists>t. F (first s ## t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Enabled F) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma COMB_init[simp]: "COMB_init h init =
                do {
                    (b::bool) \<leftarrow> (bernoulli_pmf 0.8);
                    (xs::bool list) \<leftarrow> Prob_Theory.bv (length init);
                    return_pmf (if b then Inl (xs, init) else Inr h)
                  }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COMB_init h init = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. bv (length init) \<bind> (\<lambda>xs. return_pmf (if b then Inl (xs, init) else Inr h)))
[PROOF STEP]
apply(simp add: bind_return_pmf COMB_init_def BIT_init_def rTS_def
              bind_assoc_pmf )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum_pmf (4 / 5) (map_pmf (\<lambda>l. (l, init)) (bv (length init))) (return_pmf h) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. bv (length init) \<bind> (\<lambda>xs. return_pmf (if b then Inl (xs, init) else Inr h)))
[PROOF STEP]
unfolding map_pmf_def Sum_pmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then bv (length init) \<bind> (\<lambda>x. return_pmf (x, init)) \<bind> (\<lambda>x. return_pmf (Inl x)) else return_pmf h \<bind> (\<lambda>x. return_pmf (Inr x))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. bv (length init) \<bind> (\<lambda>xs. return_pmf (if b then Inl (xs, init) else Inr h)))
[PROOF STEP]
apply(simp add: if_distrib bind_return_pmf bind_assoc_pmf )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then bv (length init) \<bind> (\<lambda>x. return_pmf (x, init)) \<bind> (\<lambda>x. return_pmf (Inl x)) else return_pmf h \<bind> (\<lambda>x. return_pmf (Inr x))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. bv (length init) \<bind> (\<lambda>xs. if b then return_pmf (Inl (xs, init)) else return_pmf (Inr h)))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bernoulli_pmf (4 / 5) = bernoulli_pmf (4 / 5)
 2. \<And>x. x \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> (if x then bv (length init) \<bind> (\<lambda>x. return_pmf (x, init)) \<bind> (\<lambda>x. return_pmf (Inl x)) else return_pmf h \<bind> (\<lambda>x. return_pmf (Inr x))) = bv (length init) \<bind> (\<lambda>xs. if x then return_pmf (Inl (xs, init)) else return_pmf (Inr h))
[PROOF STEP]
by(auto simp add: bind_return_pmf bind_assoc_pmf)


[STATEMENT]
lemma noccon: "noc o con = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. noc \<circ> con = id
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (noc \<circ> con) x = id x
[PROOF STEP]
apply(case_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a b. x = (a, b) \<Longrightarrow> (noc \<circ> con) x = id x
[PROOF STEP]
by(auto simp add: sum.case_eq_if)


[STATEMENT]
lemma connoc: "con o noc = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. con \<circ> noc = id
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (con \<circ> noc) x = id x
[PROOF STEP]
apply(case_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a. x = Inl a \<Longrightarrow> (con \<circ> noc) x = id x
 2. \<And>x b. x = Inr b \<Longrightarrow> (con \<circ> noc) x = id x
[PROOF STEP]
by(auto simp add: sum.case_eq_if)