[STATEMENT]
lemma col_convergence:
  assumes "\<forall>i. (\<lambda>n. \<c>\<o>\<l> i (X n)) \<longlonglongrightarrow> L $ i"
  shows "X \<longlonglongrightarrow> to_mtx (transpose L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<longlonglongrightarrow> to_mtx (Finite_Cartesian_Product.transpose L)
[PROOF STEP]
proof(unfold LIMSEQ_def dist_norm, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
let ?L = "to_mtx (transpose L)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
let ?a = "CARD('a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
fix \<epsilon>::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
assume "\<epsilon> > 0"
[PROOF STATE]
proof (state)
this:
0 < \<epsilon>

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
hence "\<epsilon> / ?a > 0"
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon>

goal (1 subgoal):
 1. 0 < \<epsilon> / real CARD('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
hence "\<forall>i. \<exists> N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon>/?a"
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon> / real CARD('a)
\<forall>i. (\<lambda>n. \<c>\<o>\<l> i (X n)) \<longlonglongrightarrow> L $ i

goal (1 subgoal):
 1. \<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)
[PROOF STEP]
unfolding LIMSEQ_def dist_norm convergent_def
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon> / real CARD('a)
\<forall>i r. 0 < r \<longrightarrow> (\<exists>no. \<forall>n\<ge>no. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < r)

goal (1 subgoal):
 1. \<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)
[PROOF STEP]
obtain N where "\<forall>i. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon>/?a"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. (\<And>N. \<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_nat_minimal_witness[of "\<lambda> i n. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon>/?a"]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)
\<forall>i. \<exists>N. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a) \<Longrightarrow> \<exists>N. \<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. (\<And>N. \<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
have "\<And>i n. (\<c>\<o>\<l> i (X n) - L $ i) = (\<c>\<o>\<l> i (X n - ?L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<c>\<o>\<l> i (X n) - L $ i = \<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))
[PROOF STEP]
unfolding minus_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<c>\<o>\<l> i (X n) - L $ i = \<c>\<o>\<l> i (map_fun to_vec (map_fun to_vec to_mtx) (-) (X n) (to_mtx (Finite_Cartesian_Product.transpose L)))
[PROOF STEP]
by(transfer, simp add: transpose_def vec_eq_iff column_def)
[PROOF STATE]
proof (state)
this:
\<c>\<o>\<l> ?i (X ?n) - L $ ?i = \<c>\<o>\<l> ?i (X ?n - to_mtx (Finite_Cartesian_Product.transpose L))

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)
\<c>\<o>\<l> ?i (X ?n) - L $ ?i = \<c>\<o>\<l> ?i (X ?n - to_mtx (Finite_Cartesian_Product.transpose L))
[PROOF STEP]
have N_def:"\<forall>i. \<forall>n\<ge>N. \<parallel>\<c>\<o>\<l> i (X n - ?L)\<parallel> < \<epsilon>/?a"
[PROOF STATE]
proof (prove)
using this:
\<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n) - L $ i\<parallel> < \<epsilon> / real CARD('a)
\<c>\<o>\<l> ?i (X ?n) - L $ ?i = \<c>\<o>\<l> ?i (X ?n - to_mtx (Finite_Cartesian_Product.transpose L))

goal (1 subgoal):
 1. \<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
have "\<forall>n\<ge>N. \<parallel>X n - ?L\<parallel> < \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<ge>N. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
proof(rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
fix n::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
assume "N \<le> n"
[PROOF STATE]
proof (state)
this:
N \<le> n

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
hence "\<forall> i. \<parallel>\<c>\<o>\<l> i (X n - ?L)\<parallel> < \<epsilon>/?a"
[PROOF STATE]
proof (prove)
using this:
N \<le> n

goal (1 subgoal):
 1. \<forall>i. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)
[PROOF STEP]
using N_def
[PROOF STATE]
proof (prove)
using this:
N \<le> n
\<forall>i n. N \<le> n \<longrightarrow> \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<forall>i. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
hence "(\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - ?L)\<parallel>) < (\<Sum>(i::'a)\<in>UNIV. \<epsilon>/?a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)

goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>) < (\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a))
[PROOF STEP]
using sum_strict_mono[of _ "\<lambda>i. \<parallel>\<c>\<o>\<l> i (X n - ?L)\<parallel>"]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < \<epsilon> / real CARD('a)
\<lbrakk>finite ?A; ?A \<noteq> {}; \<And>x. x \<in> ?A \<Longrightarrow> \<parallel>\<c>\<o>\<l> x (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel> < ?g x\<rbrakk> \<Longrightarrow> (\<Sum>i\<in>?A. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>) < sum ?g ?A

goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>) < (\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>) < (\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a))

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>) < (\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a))

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
have "\<parallel>X n - ?L\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - ?L)\<parallel>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>)
[PROOF STEP]
using sq_mtx_norm_le_sum_col
[PROOF STATE]
proof (prove)
using this:
\<parallel>?A\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i ?A\<parallel>)

goal (1 subgoal):
 1. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>)

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>)

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
have "(\<Sum>(i::'a)\<in>UNIV. \<epsilon>/?a) = \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a)) = \<epsilon>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a)) = \<epsilon>

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>) < (\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a))
\<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>)
(\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a)) = \<epsilon>
[PROOF STEP]
show "\<parallel>X n - ?L\<parallel> < \<epsilon>"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>) < (\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a))
\<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i (X n - to_mtx (Finite_Cartesian_Product.transpose L))\<parallel>)
(\<Sum>i\<in>UNIV. \<epsilon> / real CARD('a)) = \<epsilon>

goal (1 subgoal):
 1. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < r
[PROOF STEP]
thus "\<exists>no. \<forall>n\<ge>no. \<parallel>X n - ?L\<parallel> < \<epsilon>"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>N. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>no. \<forall>n\<ge>no. \<parallel>X n - to_mtx (Finite_Cartesian_Product.transpose L)\<parallel> < \<epsilon>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_similiar_sq_mtx_diag_eq:
  assumes "mtx_invertible P"
      and "A = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i) * P"
    shows "exp A = P\<^sup>-\<^sup>1 * exp (\<d>\<i>\<a>\<g> i. f i) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp A = P\<^sup>-\<^sup>1 * exp (\<d>\<i>\<a>\<g> i. f i) * P
[PROOF STEP]
proof(unfold exp_def power_similiar_sq_mtx_diag_eq[OF assms])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P
[PROOF STEP]
have "(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) =
  (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P)

goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P)

goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P
[PROOF STEP]
have "... = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P) = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P
[PROOF STEP]
apply(subst suminf_multr[OF bounded_linear.summable[OF bounded_linear_mult_right]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable (\<lambda>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)
 2. (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P
[PROOF STEP]
unfolding power_sq_mtx_diag[symmetric]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable (\<lambda>n. (\<d>\<i>\<a>\<g> i. f i) ^ n /\<^sub>R fact n)
 2. (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i) ^ n /\<^sub>R fact n)) * P = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i) ^ n /\<^sub>R fact n)) * P
[PROOF STEP]
by (simp_all add: summable_exp_generic)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P) = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P

goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P) = (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P

goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P
[PROOF STEP]
have "... = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P
[PROOF STEP]
apply(subst suminf_mult[of _ "P\<^sup>-\<^sup>1"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable (\<lambda>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)
 2. P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P
[PROOF STEP]
unfolding power_sq_mtx_diag[symmetric]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable (\<lambda>n. (\<d>\<i>\<a>\<g> i. f i) ^ n /\<^sub>R fact n)
 2. P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i) ^ n /\<^sub>R fact n) * P = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i) ^ n /\<^sub>R fact n) * P
[PROOF STEP]
by (simp_all add: summable_exp_generic)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. P\<^sup>-\<^sup>1 * ((\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n)) * P = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P

goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P
[PROOF STEP]
show "(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) =
  P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P

goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P
[PROOF STEP]
unfolding power_sq_mtx_diag
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P

goal (1 subgoal):
 1. (\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. (\<d>\<i>\<a>\<g> i. f i ^ n) /\<^sub>R fact n) * P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>n. P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P /\<^sub>R fact n) = P\<^sup>-\<^sup>1 * (\<Sum>n. sq_mtx_diag f ^ n /\<^sub>R fact n) * P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_similiar_sq_mtx_diag:
  assumes "A \<sim> sq_mtx_diag f"
  shows "exp A \<sim> exp (sq_mtx_diag f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp A \<sim> exp (sq_mtx_diag f)
[PROOF STEP]
using assms exp_similiar_sq_mtx_diag_eq
[PROOF STATE]
proof (prove)
using this:
A \<sim> sq_mtx_diag f
\<lbrakk>mtx_invertible ?P; ?A = ?P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. ?f i) * ?P\<rbrakk> \<Longrightarrow> exp ?A = ?P\<^sup>-\<^sup>1 * exp (\<d>\<i>\<a>\<g> i. ?f i) * ?P

goal (1 subgoal):
 1. exp A \<sim> exp (sq_mtx_diag f)
[PROOF STEP]
unfolding similar_sq_mtx_def
[PROOF STATE]
proof (prove)
using this:
\<exists>P. mtx_invertible P \<and> A = P\<^sup>-\<^sup>1 * sq_mtx_diag f * P
\<lbrakk>mtx_invertible ?P; ?A = ?P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. ?f i) * ?P\<rbrakk> \<Longrightarrow> exp ?A = ?P\<^sup>-\<^sup>1 * exp (\<d>\<i>\<a>\<g> i. ?f i) * ?P

goal (1 subgoal):
 1. \<exists>P. mtx_invertible P \<and> exp A = P\<^sup>-\<^sup>1 * exp (sq_mtx_diag f) * P
[PROOF STEP]
by blast


[STATEMENT]
lemma suminf_sq_mtx_diag:
  assumes "\<forall>i. (\<lambda>n. f n i) sums (suminf (\<lambda>n. f n i))"
  shows "(\<Sum>n. (\<d>\<i>\<a>\<g> i. f n i)) = (\<d>\<i>\<a>\<g> i. \<Sum>n. f n i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. \<d>\<i>\<a>\<g> i. f n i) = (\<d>\<i>\<a>\<g> i. \<Sum>n. f n i)
[PROOF STEP]
proof(rule suminfI, unfold sums_def LIMSEQ_iff, clarsimp simp: norm_sq_mtx_diag)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
let ?g = "\<lambda>n i. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
fix r::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
assume "r > 0"
[PROOF STATE]
proof (state)
this:
0 < r

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
have "\<forall>i. \<exists>no. \<forall>n\<ge>no. ?g n i < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
[PROOF STEP]
using assms \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (\<lambda>n. f n i) sums (\<Sum>n. f n i)
0 < r

goal (1 subgoal):
 1. \<forall>i. \<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
[PROOF STEP]
unfolding sums_def LIMSEQ_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>i r. 0 < r \<longrightarrow> (\<exists>no. \<forall>n\<ge>no. \<parallel>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<parallel> < r)
0 < r

goal (1 subgoal):
 1. \<forall>i. \<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
[PROOF STEP]
obtain N where key: "\<forall>i. \<forall>n\<ge>N. ?g n i < r"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r

goal (1 subgoal):
 1. (\<And>N. \<forall>i n. N \<le> n \<longrightarrow> \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_nat_minimal_witness[of "\<lambda>i n. ?g n i < r"]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
\<forall>i. \<exists>N. \<forall>n\<ge>N. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r \<Longrightarrow> \<exists>N. \<forall>i n. N \<le> n \<longrightarrow> \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r

goal (1 subgoal):
 1. (\<And>N. \<forall>i n. N \<le> n \<longrightarrow> \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i n. N \<le> n \<longrightarrow> \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>i n. N \<le> n \<longrightarrow> \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
fix n::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
assume "n \<ge> N"
[PROOF STATE]
proof (state)
this:
N \<le> n

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
obtain i where i_def: "Max {x. \<exists>i. x = ?g n i} = ?g n i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cMax_finite_ex[of "{x. \<exists>i. x = ?g n i}"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>}; {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>{x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>}. Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} = x

goal (1 subgoal):
 1. (\<And>i. Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
hence "?g n i < r"
[PROOF STATE]
proof (prove)
using this:
Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>

goal (1 subgoal):
 1. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
[PROOF STEP]
using key \<open>n \<ge> N\<close>
[PROOF STATE]
proof (prove)
using this:
Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>
\<forall>i n. N \<le> n \<longrightarrow> \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
N \<le> n

goal (1 subgoal):
 1. \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
hence "Max {x. \<exists>i. x = ?g n i} < r"
[PROOF STATE]
proof (prove)
using this:
\<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar> < r

goal (1 subgoal):
 1. Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
unfolding i_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r

goal (1 subgoal):
 1. Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
N \<le> ?n2 \<Longrightarrow> Max {x. \<exists>i. x = \<bar>(\<Sum>n<?n2. f n i) - (\<Sum>n. f n i)\<bar>} < r

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. Max {uu_. \<exists>i. uu_ = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
thus "\<exists>N. \<forall>n\<ge>N. Max {x. \<exists>i. x = ?g n i} < r"
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n2 \<Longrightarrow> Max {x. \<exists>i. x = \<bar>(\<Sum>n<?n2. f n i) - (\<Sum>n. f n i)\<bar>} < r

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n\<ge>N. Max {x. \<exists>i. x = \<bar>(\<Sum>n<n. f n i) - (\<Sum>n. f n i)\<bar>} < r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_sq_mtx_diag: "exp (sq_mtx_diag f) = (\<d>\<i>\<a>\<g> i. exp (f i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (sq_mtx_diag f) = (\<d>\<i>\<a>\<g> i. exp (f i))
[PROOF STEP]
apply(unfold exp_def, simp add: power_sq_mtx_diag scaleR_sq_mtx_diag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. \<d>\<i>\<a>\<g> i. inverse (fact n) * f i ^ n) = (\<d>\<i>\<a>\<g> i. \<Sum>n. inverse (fact n) * f i ^ n)
[PROOF STEP]
apply(rule suminf_sq_mtx_diag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (\<lambda>n. inverse (fact n) * f i ^ n) sums (\<Sum>n. inverse (fact n) * f i ^ n)
[PROOF STEP]
using exp_converges[of "f _"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f ?uu3 ^ n /\<^sub>R fact n) sums exp (f ?uu3)

goal (1 subgoal):
 1. \<forall>i. (\<lambda>n. inverse (fact n) * f i ^ n) sums (\<Sum>n. inverse (fact n) * f i ^ n)
[PROOF STEP]
unfolding sums_def LIMSEQ_iff exp_def
[PROOF STATE]
proof (prove)
using this:
\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<parallel>(\<Sum>n<n. f ?uu3 ^ n /\<^sub>R fact n) - (\<Sum>n. f ?uu3 ^ n /\<^sub>R fact n)\<parallel> < r

goal (1 subgoal):
 1. \<forall>i r. 0 < r \<longrightarrow> (\<exists>no. \<forall>n\<ge>no. \<parallel>(\<Sum>n<n. inverse (fact n) * f i ^ n) - (\<Sum>n. inverse (fact n) * f i ^ n)\<parallel> < r)
[PROOF STEP]
by force


[STATEMENT]
lemma exp_scaleR_diagonal1:
  assumes "mtx_invertible P" and "A = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i) * P"
    shows "exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
have "exp (t *\<^sub>R A) = exp (P\<^sup>-\<^sup>1 * (t *\<^sub>R sq_mtx_diag f) * P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (t *\<^sub>R A) = exp (P\<^sup>-\<^sup>1 * t *\<^sub>R sq_mtx_diag f * P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mtx_invertible P
A = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i) * P

goal (1 subgoal):
 1. exp (t *\<^sub>R A) = exp (P\<^sup>-\<^sup>1 * t *\<^sub>R sq_mtx_diag f * P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exp (t *\<^sub>R A) = exp (P\<^sup>-\<^sup>1 * t *\<^sub>R sq_mtx_diag f * P)

goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp (t *\<^sub>R A) = exp (P\<^sup>-\<^sup>1 * t *\<^sub>R sq_mtx_diag f * P)

goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
have "... = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (P\<^sup>-\<^sup>1 * t *\<^sub>R sq_mtx_diag f * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
by (metis assms(1) exp_similiar_sq_mtx_diag_eq exp_sq_mtx_diag scaleR_sq_mtx_diag)
[PROOF STATE]
proof (state)
this:
exp (P\<^sup>-\<^sup>1 * t *\<^sub>R sq_mtx_diag f * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P

goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
show "exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P"
[PROOF STATE]
proof (prove)
using this:
exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P

goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_scaleR_diagonal2:
  assumes "mtx_invertible P" and "A = P * (\<d>\<i>\<a>\<g> i. f i) * P\<^sup>-\<^sup>1"
    shows "exp (t *\<^sub>R A) = P * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P\<^sup>-\<^sup>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P\<^sup>-\<^sup>1
[PROOF STEP]
apply(subst sq_mtx_inv_idempotent[OF assms(1), symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (t *\<^sub>R A) = P\<^sup>-\<^sup>1\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. exp (t * f i)) * P\<^sup>-\<^sup>1
[PROOF STEP]
apply(rule exp_scaleR_diagonal1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mtx_invertible P\<^sup>-\<^sup>1
 2. A = P\<^sup>-\<^sup>1\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i) * P\<^sup>-\<^sup>1
[PROOF STEP]
by (simp_all add: assms)


[STATEMENT]
lemma vector_nth_eq: "(vector A) $ i = foldr (\<lambda>x f n. (f (n + 1))(n := x)) A (\<lambda>n x. 0) 1 i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector A $ i = foldr (\<lambda>x f n. (f (n + (1::'b)))(n := x)) A (\<lambda>n x. 0::'a) (1::'b) i
[PROOF STEP]
unfolding vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_lambda (foldr (\<lambda>x f n. (f (n + (1::'b)))(n := x)) A (\<lambda>n x. 0::'a) (1::'b)) $ i = foldr (\<lambda>x f n. (f (n + (1::'b)))(n := x)) A (\<lambda>n x. 0::'a) (1::'b) i
[PROOF STEP]
by simp


[STATEMENT]
lemma mtx_ith_eq[simp]: "mtx A $$ i $ j = foldr (\<lambda>x f n. (f (n + 1))(n := x))
  (map (\<lambda>l. vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) l (\<lambda>n x. 0) 1)) A) (\<lambda>n x. 0) 1 i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx A $$ i $ j = foldr (\<lambda>x f n. (f (n + (1::'a)))(n := x)) (map (\<lambda>l. vec_lambda (foldr (\<lambda>x f n. (f (n + (1::'a)))(n := x)) l (\<lambda>n x. 0) (1::'a))) A) (\<lambda>n x. 0) (1::'a) i $ j
[PROOF STEP]
unfolding mtx_def vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (vec_lambda (foldr (\<lambda>x f n. (f (n + (1::'a)))(n := x)) (map (\<lambda>l. vec_lambda (foldr (\<lambda>x f n. (f (n + (1::'a)))(n := x)) l (\<lambda>n x. 0) (1::'a))) A) (\<lambda>n x. 0) (1::'a))) $$ i $ j = foldr (\<lambda>x f n. (f (n + (1::'a)))(n := x)) (map (\<lambda>l. vec_lambda (foldr (\<lambda>x f n. (f (n + (1::'a)))(n := x)) l (\<lambda>n x. 0) (1::'a))) A) (\<lambda>n x. 0) (1::'a) i $ j
[PROOF STEP]
by (simp add: vector_nth_eq)


[STATEMENT]
lemma mtx2_eq_iff: "(mtx
  ([a1, b1] #
   [c1, d1] # []) :: 2 sq_mtx) = mtx
  ([a2, b2] #
   [c2, d2] # []) \<longleftrightarrow> a1 = a2 \<and> b1 = b2 \<and> c1 = c2 \<and> d1 = d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mtx [[a1, b1], [c1, d1]] = mtx [[a2, b2], [c2, d2]]) = (a1 = a2 \<and> b1 = b2 \<and> c1 = c2 \<and> d1 = d2)
[PROOF STEP]
apply(simp add: sq_mtx_eq_iff, safe)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> a1 = a2
 2. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> b1 = b2
 3. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> c1 = c2
 4. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> d1 = d2
[PROOF STEP]
using exhaust_2
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2

goal (4 subgoals):
 1. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> a1 = a2
 2. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> b1 = b2
 3. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> c1 = c2
 4. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> d1 = d2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> c1 = c2))) \<and> (i \<noteq> 2 \<longrightarrow> i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> b1 = b2) \<and> (j \<noteq> 2 \<longrightarrow> j = 1 \<longrightarrow> a1 = a2))) \<Longrightarrow> d1 = d2
[PROOF STEP]
by force+


[STATEMENT]
lemma mtx2_to_mtx: "mtx
  ([a, b] #
   [c, d] # []) =
  to_mtx (\<chi> i j::2. if i=1 \<and> j=1 then a
  else (if i=1 \<and> j=2 then b
  else (if i=2 \<and> j=1 then c
  else d)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a, b], [c, d]] = to_mtx (\<chi>i j. if i = 1 \<and> j = 1 then a else if i = 1 \<and> j = 2 then b else if i = 2 \<and> j = 1 then c else d)
[PROOF STEP]
apply(subst sq_mtx_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. mtx [[a, b], [c, d]] $$ i $ j = to_mtx (\<chi>i j. if i = 1 \<and> j = 1 then a else if i = 1 \<and> j = 2 then b else if i = 2 \<and> j = 1 then c else d) $$ i $ j
[PROOF STEP]
using exhaust_2
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2

goal (1 subgoal):
 1. \<forall>i j. mtx [[a, b], [c, d]] $$ i $ j = to_mtx (\<chi>i j. if i = 1 \<and> j = 1 then a else if i = 1 \<and> j = 2 then b else if i = 2 \<and> j = 1 then c else d) $$ i $ j
[PROOF STEP]
by force


[STATEMENT]
lemma diag2_eq: "diag2 (\<iota> 1) (\<iota> 2) = (\<d>\<i>\<a>\<g> i. \<iota> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diag2 (\<iota> 1) (\<iota> 2) = (\<d>\<i>\<a>\<g> i. \<iota> i)
[PROOF STEP]
apply(simp add: sq_mtx_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. j \<noteq> 2 \<longrightarrow> (j = 1 \<longrightarrow> axis 2 (\<iota> 2) $ 1 = 0) \<and> (j \<noteq> 1 \<longrightarrow> axis 2 (\<iota> 2) $ j = 0))) \<and> (i \<noteq> 2 \<longrightarrow> (i = 1 \<longrightarrow> (\<forall>j. j \<noteq> 1 \<longrightarrow> axis 1 (\<iota> 1) $ j = 0)) \<and> (i \<noteq> 1 \<longrightarrow> (\<forall>j. axis i (\<iota> i) $ j = 0)))
[PROOF STEP]
using exhaust_2
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2

goal (1 subgoal):
 1. \<forall>i. (i = 2 \<longrightarrow> (\<forall>j. j \<noteq> 2 \<longrightarrow> (j = 1 \<longrightarrow> axis 2 (\<iota> 2) $ 1 = 0) \<and> (j \<noteq> 1 \<longrightarrow> axis 2 (\<iota> 2) $ j = 0))) \<and> (i \<noteq> 2 \<longrightarrow> (i = 1 \<longrightarrow> (\<forall>j. j \<noteq> 1 \<longrightarrow> axis 1 (\<iota> 1) $ j = 0)) \<and> (i \<noteq> 1 \<longrightarrow> (\<forall>j. axis i (\<iota> i) $ j = 0)))
[PROOF STEP]
by (force simp: axis_def)


[STATEMENT]
lemma one_mtx2: "(1::2 sq_mtx) = diag2 1 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = diag2 1 1
[PROOF STEP]
apply(subst sq_mtx_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. 1 $$ i $ j = diag2 1 1 $$ i $ j
[PROOF STEP]
using exhaust_2
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2

goal (1 subgoal):
 1. \<forall>i j. 1 $$ i $ j = diag2 1 1 $$ i $ j
[PROOF STEP]
by force


[STATEMENT]
lemma zero_mtx2: "(0::2 sq_mtx) = diag2 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = diag2 0 0
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma scaleR_mtx2: "k *\<^sub>R mtx
  ([a, b] #
   [c, d] # []) = mtx
  ([k*a, k*b] #
   [k*c, k*d] # [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k *\<^sub>R mtx [[a, b], [c, d]] = mtx [[k * a, k * b], [k * c, k * d]]
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma uminus_mtx2: "-mtx
  ([a, b] #
   [c, d] # []) = (mtx
  ([-a, -b] #
   [-c, -d] # [])::2 sq_mtx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - mtx [[a, b], [c, d]] = mtx [[- a, - b], [- c, - d]]
[PROOF STEP]
by (simp add: sq_mtx_uminus_eq sq_mtx_eq_iff)


[STATEMENT]
lemma plus_mtx2: "mtx
  ([a1, b1] #
   [c1, d1] # []) + mtx
  ([a2, b2] #
   [c2, d2] # []) = ((mtx
  ([a1+a2, b1+b2] #
   [c1+c2, d1+d2] # []))::2 sq_mtx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a1, b1], [c1, d1]] + mtx [[a2, b2], [c2, d2]] = mtx [[a1 + a2, b1 + b2], [c1 + c2, d1 + d2]]
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma minus_mtx2: "mtx
  ([a1, b1] #
   [c1, d1] # []) - mtx
  ([a2, b2] #
   [c2, d2] # []) = ((mtx
  ([a1-a2, b1-b2] #
   [c1-c2, d1-d2] # []))::2 sq_mtx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a1, b1], [c1, d1]] - mtx [[a2, b2], [c2, d2]] = mtx [[a1 - a2, b1 - b2], [c1 - c2, d1 - d2]]
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma times_mtx2: "mtx
  ([a1, b1] #
   [c1, d1] # []) * mtx
  ([a2, b2] #
   [c2, d2] # []) = ((mtx
  ([a1*a2+b1*c2, a1*b2+b1*d2] #
   [c1*a2+d1*c2, c1*b2+d1*d2] # []))::2 sq_mtx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a1, b1], [c1, d1]] * mtx [[a2, b2], [c2, d2]] = mtx [[a1 * a2 + b1 * c2, a1 * b2 + b1 * d2], [c1 * a2 + d1 * c2, c1 * b2 + d1 * d2]]
[PROOF STEP]
unfolding sq_mtx_times_eq UNIV_2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (\<chi>i j. \<Sum>k\<in>{1, 2}. mtx [[a1, b1], [c1, d1]] $$ i $ k * mtx [[a2, b2], [c2, d2]] $$ k $ j) = mtx [[a1 * a2 + b1 * c2, a1 * b2 + b1 * d2], [c1 * a2 + d1 * c2, c1 * b2 + d1 * d2]]
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma mtx3_to_mtx: "mtx
  ([a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3] #
   [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3] #
   [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3] # []) =
  to_mtx (\<chi> i j::3. if i=1 \<and> j=1 then a\<^sub>1\<^sub>1
  else (if i=1 \<and> j=2 then a\<^sub>1\<^sub>2
  else (if i=1 \<and> j=3 then a\<^sub>1\<^sub>3
  else (if i=2 \<and> j=1 then a\<^sub>2\<^sub>1
  else (if i=2 \<and> j=2 then a\<^sub>2\<^sub>2
  else (if i=2 \<and> j=3 then a\<^sub>2\<^sub>3
  else (if i=3 \<and> j=1 then a\<^sub>3\<^sub>1
  else (if i=3 \<and> j=2 then a\<^sub>3\<^sub>2
  else a\<^sub>3\<^sub>3))))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3]] = to_mtx (\<chi>i j. if i = 1 \<and> j = 1 then a\<^sub>1\<^sub>1 else if i = 1 \<and> j = 2 then a\<^sub>1\<^sub>2 else if i = 1 \<and> j = 3 then a\<^sub>1\<^sub>3 else if i = 2 \<and> j = 1 then a\<^sub>2\<^sub>1 else if i = 2 \<and> j = 2 then a\<^sub>2\<^sub>2 else if i = 2 \<and> j = 3 then a\<^sub>2\<^sub>3 else if i = 3 \<and> j = 1 then a\<^sub>3\<^sub>1 else if i = 3 \<and> j = 2 then a\<^sub>3\<^sub>2 else a\<^sub>3\<^sub>3)
[PROOF STEP]
apply(simp add: sq_mtx_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (i = 3 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)) \<and> (i \<noteq> 3 \<longrightarrow> (i = 2 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)) \<and> (i \<noteq> 2 \<longrightarrow> (i = 1 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)) \<and> (i \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)))
[PROOF STEP]
using exhaust_3
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3

goal (1 subgoal):
 1. \<forall>i. (i = 3 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)) \<and> (i \<noteq> 3 \<longrightarrow> (i = 2 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)) \<and> (i \<noteq> 2 \<longrightarrow> (i = 1 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)) \<and> (i \<noteq> 1 \<longrightarrow> a\<^sub>3\<^sub>3 = 0)))
[PROOF STEP]
by force


[STATEMENT]
lemma diag3_eq: "diag3 (\<iota> 1) (\<iota> 2) (\<iota> 3) = (\<d>\<i>\<a>\<g> i. \<iota> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diag3 (\<iota> 1) (\<iota> 2) (\<iota> 3) = (\<d>\<i>\<a>\<g> i. \<iota> i)
[PROOF STEP]
apply(simp add: sq_mtx_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (i = 3 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> (j = 2 \<longrightarrow> axis 3 (\<iota> 3) $ 2 = 0) \<and> (j \<noteq> 2 \<longrightarrow> (j = 1 \<longrightarrow> axis 3 (\<iota> 3) $ 1 = 0) \<and> (j \<noteq> 1 \<longrightarrow> axis 3 (\<iota> 3) $ j = 0)))) \<and> (i \<noteq> 3 \<longrightarrow> (i = 2 \<longrightarrow> (\<forall>j. j \<noteq> 2 \<longrightarrow> (j = 1 \<longrightarrow> axis 2 (\<iota> 2) $ 1 = 0) \<and> (j \<noteq> 1 \<longrightarrow> axis 2 (\<iota> 2) $ j = 0))) \<and> (i \<noteq> 2 \<longrightarrow> (i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> axis 1 (\<iota> 1) $ 2 = 0) \<and> (j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> axis 1 (\<iota> 1) $ j = 0))) \<and> (i \<noteq> 1 \<longrightarrow> (\<forall>j. axis i (\<iota> i) $ j = 0))))
[PROOF STEP]
using exhaust_3
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3

goal (1 subgoal):
 1. \<forall>i. (i = 3 \<longrightarrow> (\<forall>j. j \<noteq> 3 \<longrightarrow> (j = 2 \<longrightarrow> axis 3 (\<iota> 3) $ 2 = 0) \<and> (j \<noteq> 2 \<longrightarrow> (j = 1 \<longrightarrow> axis 3 (\<iota> 3) $ 1 = 0) \<and> (j \<noteq> 1 \<longrightarrow> axis 3 (\<iota> 3) $ j = 0)))) \<and> (i \<noteq> 3 \<longrightarrow> (i = 2 \<longrightarrow> (\<forall>j. j \<noteq> 2 \<longrightarrow> (j = 1 \<longrightarrow> axis 2 (\<iota> 2) $ 1 = 0) \<and> (j \<noteq> 1 \<longrightarrow> axis 2 (\<iota> 2) $ j = 0))) \<and> (i \<noteq> 2 \<longrightarrow> (i = 1 \<longrightarrow> (\<forall>j. (j = 2 \<longrightarrow> axis 1 (\<iota> 1) $ 2 = 0) \<and> (j \<noteq> 2 \<longrightarrow> j \<noteq> 1 \<longrightarrow> axis 1 (\<iota> 1) $ j = 0))) \<and> (i \<noteq> 1 \<longrightarrow> (\<forall>j. axis i (\<iota> i) $ j = 0))))
[PROOF STEP]
by (force simp: axis_def)


[STATEMENT]
lemma one_mtx3: "(1::3 sq_mtx) = diag3 1 1 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = diag3 1 1 1
[PROOF STEP]
apply(subst sq_mtx_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. 1 $$ i $ j = diag3 1 1 1 $$ i $ j
[PROOF STEP]
using exhaust_3
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3

goal (1 subgoal):
 1. \<forall>i j. 1 $$ i $ j = diag3 1 1 1 $$ i $ j
[PROOF STEP]
by force


[STATEMENT]
lemma zero_mtx3: "(0::3 sq_mtx) = diag3 0 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = diag3 0 0 0
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma scaleR_mtx3: "k *\<^sub>R mtx
  ([a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3] #
   [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3] #
   [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3] # []) = mtx
  ([k*a\<^sub>1\<^sub>1, k*a\<^sub>1\<^sub>2, k*a\<^sub>1\<^sub>3] #
   [k*a\<^sub>2\<^sub>1, k*a\<^sub>2\<^sub>2, k*a\<^sub>2\<^sub>3] #
   [k*a\<^sub>3\<^sub>1, k*a\<^sub>3\<^sub>2, k*a\<^sub>3\<^sub>3] # [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k *\<^sub>R mtx [[a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3]] = mtx [[k * a\<^sub>1\<^sub>1, k * a\<^sub>1\<^sub>2, k * a\<^sub>1\<^sub>3], [k * a\<^sub>2\<^sub>1, k * a\<^sub>2\<^sub>2, k * a\<^sub>2\<^sub>3], [k * a\<^sub>3\<^sub>1, k * a\<^sub>3\<^sub>2, k * a\<^sub>3\<^sub>3]]
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma plus_mtx3: "mtx
  ([a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3] #
   [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3] #
   [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3] # []) + mtx
  ([b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3] #
   [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3] #
   [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3] # []) = (mtx
  ([a\<^sub>1\<^sub>1+b\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2+b\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3+b\<^sub>1\<^sub>3] #
   [a\<^sub>2\<^sub>1+b\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2+b\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3+b\<^sub>2\<^sub>3] #
   [a\<^sub>3\<^sub>1+b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2+b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3+b\<^sub>3\<^sub>3] # [])::3 sq_mtx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3]] + mtx [[b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3], [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3], [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3]] = mtx [[a\<^sub>1\<^sub>1 + b\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2 + b\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3 + b\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1 + b\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2 + b\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3 + b\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1 + b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2 + b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3 + b\<^sub>3\<^sub>3]]
[PROOF STEP]
by (subst sq_mtx_eq_iff) simp


[STATEMENT]
lemma minus_mtx3: "mtx
  ([a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3] #
   [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3] #
   [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3] # []) - mtx
  ([b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3] #
   [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3] #
   [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3] # []) = (mtx
  ([a\<^sub>1\<^sub>1-b\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2-b\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3-b\<^sub>1\<^sub>3] #
   [a\<^sub>2\<^sub>1-b\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2-b\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3-b\<^sub>2\<^sub>3] #
   [a\<^sub>3\<^sub>1-b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2-b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3-b\<^sub>3\<^sub>3] # [])::3 sq_mtx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3]] - mtx [[b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3], [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3], [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3]] = mtx [[a\<^sub>1\<^sub>1 - b\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2 - b\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3 - b\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1 - b\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2 - b\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3 - b\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1 - b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2 - b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3 - b\<^sub>3\<^sub>3]]
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma times_mtx3: "mtx
  ([a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3] #
   [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3] #
   [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3] # []) * mtx
  ([b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3] #
   [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3] #
   [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3] # []) = (mtx
  ([a\<^sub>1\<^sub>1*b\<^sub>1\<^sub>1+a\<^sub>1\<^sub>2*b\<^sub>2\<^sub>1+a\<^sub>1\<^sub>3*b\<^sub>3\<^sub>1, a\<^sub>1\<^sub>1*b\<^sub>1\<^sub>2+a\<^sub>1\<^sub>2*b\<^sub>2\<^sub>2+a\<^sub>1\<^sub>3*b\<^sub>3\<^sub>2, a\<^sub>1\<^sub>1*b\<^sub>1\<^sub>3+a\<^sub>1\<^sub>2*b\<^sub>2\<^sub>3+a\<^sub>1\<^sub>3*b\<^sub>3\<^sub>3] #
   [a\<^sub>2\<^sub>1*b\<^sub>1\<^sub>1+a\<^sub>2\<^sub>2*b\<^sub>2\<^sub>1+a\<^sub>2\<^sub>3*b\<^sub>3\<^sub>1, a\<^sub>2\<^sub>1*b\<^sub>1\<^sub>2+a\<^sub>2\<^sub>2*b\<^sub>2\<^sub>2+a\<^sub>2\<^sub>3*b\<^sub>3\<^sub>2, a\<^sub>2\<^sub>1*b\<^sub>1\<^sub>3+a\<^sub>2\<^sub>2*b\<^sub>2\<^sub>3+a\<^sub>2\<^sub>3*b\<^sub>3\<^sub>3] #
   [a\<^sub>3\<^sub>1*b\<^sub>1\<^sub>1+a\<^sub>3\<^sub>2*b\<^sub>2\<^sub>1+a\<^sub>3\<^sub>3*b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>1*b\<^sub>1\<^sub>2+a\<^sub>3\<^sub>2*b\<^sub>2\<^sub>2+a\<^sub>3\<^sub>3*b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>1*b\<^sub>1\<^sub>3+a\<^sub>3\<^sub>2*b\<^sub>2\<^sub>3+a\<^sub>3\<^sub>3*b\<^sub>3\<^sub>3] # [])::3 sq_mtx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx [[a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3]] * mtx [[b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3], [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3], [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3]] = mtx [[a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>3], [a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>3], [a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>3]]
[PROOF STEP]
unfolding sq_mtx_times_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (\<chi>i j. \<Sum>k\<in>UNIV. mtx [[a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3]] $$ i $ k * mtx [[b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3], [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3], [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3]] $$ k $ j) = mtx [[a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>3], [a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>3], [a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>3]]
[PROOF STEP]
unfolding UNIV_3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (\<chi>i j. \<Sum>k\<in>{1, 2, 3}. mtx [[a\<^sub>1\<^sub>1, a\<^sub>1\<^sub>2, a\<^sub>1\<^sub>3], [a\<^sub>2\<^sub>1, a\<^sub>2\<^sub>2, a\<^sub>2\<^sub>3], [a\<^sub>3\<^sub>1, a\<^sub>3\<^sub>2, a\<^sub>3\<^sub>3]] $$ i $ k * mtx [[b\<^sub>1\<^sub>1, b\<^sub>1\<^sub>2, b\<^sub>1\<^sub>3], [b\<^sub>2\<^sub>1, b\<^sub>2\<^sub>2, b\<^sub>2\<^sub>3], [b\<^sub>3\<^sub>1, b\<^sub>3\<^sub>2, b\<^sub>3\<^sub>3]] $$ k $ j) = mtx [[a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>1\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>1\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>1\<^sub>3 * b\<^sub>3\<^sub>3], [a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>2\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>2\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>2\<^sub>3 * b\<^sub>3\<^sub>3], [a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>1 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>1 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>1, a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>2 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>2 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>2, a\<^sub>3\<^sub>1 * b\<^sub>1\<^sub>3 + a\<^sub>3\<^sub>2 * b\<^sub>2\<^sub>3 + a\<^sub>3\<^sub>3 * b\<^sub>3\<^sub>3]]
[PROOF STEP]
by (simp add: sq_mtx_eq_iff)


[STATEMENT]
lemma "wf_list_graph tainting_example"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_list_graph tainting_example
[PROOF STEP]
by eval


[STATEMENT]
lemma "sinvar tainting_example tainting_example_props"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sinvar tainting_example tainting_example_props
[PROOF STEP]
by eval


[STATEMENT]
lemma ex_rb_Q_susp_user: "the_res (RB Q_susp_user) = Q_susp_user_rb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_res (RB Q_susp_user) = Q_susp_user_rb
[PROOF STEP]
by code_simp


[STATEMENT]
lemma ex_split_Q_disj: "the_res (SPLIT Q_disj) = (Q_disj_split_fin, Q_disj_split_inf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_res (SPLIT Q_disj) = (Q_disj_split_fin, Q_disj_split_inf)
[PROOF STEP]
by code_simp


[STATEMENT]
lemma ex_split_Q_eq: "the_res (SPLIT Q_eq) = (Q_eq_split_fin, Q_eq_split_inf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_res (SPLIT Q_eq) = (Q_eq_split_fin, Q_eq_split_inf)
[PROOF STEP]
by code_simp


[STATEMENT]
lemma ex_split_Q_susp_user: "the_res (SPLIT Q_susp_user) = (Q_susp_user_split_fin, Q_susp_user_split_inf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_res (SPLIT Q_susp_user) = (Q_susp_user_split_fin, Q_susp_user_split_inf)
[PROOF STEP]
by code_simp


[STATEMENT]
lemma Abs_run_inverse_rewrite:
  \<open>\<forall>c. mono (\<lambda>n. time (\<rho> n c)) \<Longrightarrow> Rep_run (Abs_run \<rho>) = \<rho>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. mono (\<lambda>n. time (\<rho> n c)) \<Longrightarrow> Rep_run (Abs_run \<rho>) = \<rho>
[PROOF STEP]
by (simp add: Abs_run_inverse)


[STATEMENT]
lemma before_first_time:
  assumes \<open>first_time \<rho> K n \<tau>\<close>
      and \<open>m < n\<close>
    shows \<open>time ((Rep_run \<rho>) m K) < \<tau>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
have \<open>mono (\<lambda>n. time (Rep_run \<rho> n K))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>n. time (Rep_run \<rho> n K))
[PROOF STEP]
using Rep_run
[PROOF STATE]
proof (prove)
using this:
Rep_run ?x \<in> {\<rho>. \<forall>c. mono (\<lambda>n. time (\<rho> n c))}

goal (1 subgoal):
 1. mono (\<lambda>n. time (Rep_run \<rho> n K))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mono (\<lambda>n. time (Rep_run \<rho> n K))

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mono (\<lambda>n. time (Rep_run \<rho> n K))

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
m < n
[PROOF STEP]
have \<open>m \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. m \<le> n
[PROOF STEP]
using less_imp_le
[PROOF STATE]
proof (prove)
using this:
m < n
?x < ?y \<Longrightarrow> ?x \<le> ?y

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

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m \<le> n

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
have \<open>mono (\<lambda>n. time (Rep_run \<rho> n K))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>n. time (Rep_run \<rho> n K))
[PROOF STEP]
using Rep_run
[PROOF STATE]
proof (prove)
using this:
Rep_run ?x \<in> {\<rho>. \<forall>c. mono (\<lambda>n. time (\<rho> n c))}

goal (1 subgoal):
 1. mono (\<lambda>n. time (Rep_run \<rho> n K))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mono (\<lambda>n. time (Rep_run \<rho> n K))

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mono (\<lambda>n. time (Rep_run \<rho> n K))
m \<le> n
mono (\<lambda>n. time (Rep_run \<rho> n K))
[PROOF STEP]
have  \<open>time ((Rep_run \<rho>) m K) \<le> time ((Rep_run \<rho>) n K)\<close>
[PROOF STATE]
proof (prove)
using this:
mono (\<lambda>n. time (Rep_run \<rho> n K))
m \<le> n
mono (\<lambda>n. time (Rep_run \<rho> n K))

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) \<le> time (Rep_run \<rho> n K)
[PROOF STEP]
by (simp add:mono_def)
[PROOF STATE]
proof (state)
this:
time (Rep_run \<rho> m K) \<le> time (Rep_run \<rho> n K)

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
time (Rep_run \<rho> m K) \<le> time (Rep_run \<rho> n K)

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
first_time \<rho> K n \<tau>
[PROOF STEP]
have \<open>time ((Rep_run \<rho>) n K) = \<tau>\<close>
[PROOF STATE]
proof (prove)
using this:
first_time \<rho> K n \<tau>

goal (1 subgoal):
 1. time (Rep_run \<rho> n K) = \<tau>
[PROOF STEP]
using first_time_def
[PROOF STATE]
proof (prove)
using this:
first_time \<rho> K n \<tau>
first_time ?\<rho> ?K ?n ?\<tau> \<equiv> time (Rep_run ?\<rho> ?n ?K) = ?\<tau> \<and> \<not> (\<exists>n'<?n. time (Rep_run ?\<rho> n' ?K) = ?\<tau>)

goal (1 subgoal):
 1. time (Rep_run \<rho> n K) = \<tau>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
time (Rep_run \<rho> n K) = \<tau>

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
time (Rep_run \<rho> n K) = \<tau>

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
first_time \<rho> K n \<tau>
m < n
[PROOF STEP]
have \<open>time ((Rep_run \<rho>) m K) \<noteq> \<tau>\<close>
[PROOF STATE]
proof (prove)
using this:
first_time \<rho> K n \<tau>
m < n

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) \<noteq> \<tau>
[PROOF STEP]
using first_time_def
[PROOF STATE]
proof (prove)
using this:
first_time \<rho> K n \<tau>
m < n
first_time ?\<rho> ?K ?n ?\<tau> \<equiv> time (Rep_run ?\<rho> ?n ?K) = ?\<tau> \<and> \<not> (\<exists>n'<?n. time (Rep_run ?\<rho> n' ?K) = ?\<tau>)

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) \<noteq> \<tau>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
time (Rep_run \<rho> m K) \<noteq> \<tau>

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
time (Rep_run \<rho> m K) \<le> time (Rep_run \<rho> n K)
time (Rep_run \<rho> n K) = \<tau>
time (Rep_run \<rho> m K) \<noteq> \<tau>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
time (Rep_run \<rho> m K) \<le> time (Rep_run \<rho> n K)
time (Rep_run \<rho> n K) = \<tau>
time (Rep_run \<rho> m K) \<noteq> \<tau>

goal (1 subgoal):
 1. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
time (Rep_run \<rho> m K) < \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alt_first_time_def:
  assumes \<open>\<forall>m < n. time ((Rep_run \<rho>) m K) < \<tau>\<close>
      and \<open>time ((Rep_run \<rho>) n K) = \<tau>\<close>
    shows \<open>first_time \<rho> K n \<tau>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. first_time \<rho> K n \<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. first_time \<rho> K n \<tau>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. time (Rep_run \<rho> m K) < \<tau>
[PROOF STEP]
have \<open>\<forall>m < n. time ((Rep_run \<rho>) m K) \<noteq> \<tau>\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. time (Rep_run \<rho> m K) < \<tau>

goal (1 subgoal):
 1. \<forall>m<n. time (Rep_run \<rho> m K) \<noteq> \<tau>
[PROOF STEP]
by (simp add: less_le)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. time (Rep_run \<rho> m K) \<noteq> \<tau>

goal (1 subgoal):
 1. first_time \<rho> K n \<tau>
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
time (Rep_run \<rho> n K) = \<tau>
\<forall>m<n. time (Rep_run \<rho> m K) \<noteq> \<tau>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
time (Rep_run \<rho> n K) = \<tau>
\<forall>m<n. time (Rep_run \<rho> m K) \<noteq> \<tau>

goal (1 subgoal):
 1. first_time \<rho> K n \<tau>
[PROOF STEP]
by (simp add: first_time_def)
[PROOF STATE]
proof (state)
this:
first_time \<rho> K n \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_inductl: "z + x \<cdot> y \<le> y \<Longrightarrow> (x ^ n) \<cdot> z \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + x \<cdot> y \<le> y \<Longrightarrow> x ^ n \<cdot> z \<le> y
[PROOF STEP]
by(induct n, auto, metis mult.assoc mult_isol order_trans)


[STATEMENT]
lemma power_inductr: "z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> (x ^ n) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ 0 \<le> y
 2. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
z + y \<cdot> x \<le> y

goal (2 subgoals):
 1. z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ 0 \<le> y
 2. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<cdot> x ^ 0 \<le> y
[PROOF STEP]
using "0.prems"
[PROOF STATE]
proof (prove)
using this:
z + y \<cdot> x \<le> y

goal (1 subgoal):
 1. z \<cdot> x ^ 0 \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ 0 \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
case Suc
[PROOF STATE]
proof (state)
this:
z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n_ \<le> y
z + y \<cdot> x \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n_ \<le> y
z + y \<cdot> x \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
assume "z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y"
      and "z + y \<cdot> x \<le> y"
[PROOF STATE]
proof (state)
this:
z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y
z + y \<cdot> x \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
hence "z \<cdot> x ^ n \<le> y"
[PROOF STATE]
proof (prove)
using this:
z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y
z + y \<cdot> x \<le> y

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

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ n \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
have "z \<cdot> x ^ Suc n = z \<cdot> x \<cdot> x ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<cdot> x ^ Suc n = z \<cdot> x \<cdot> x ^ n
[PROOF STEP]
by (metis mult.assoc power_Suc)
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ Suc n = z \<cdot> x \<cdot> x ^ n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ Suc n = z \<cdot> x \<cdot> x ^ n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
have "... = (z \<cdot> x ^ n) \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<cdot> x \<cdot> x ^ n = z \<cdot> x ^ n \<cdot> x
[PROOF STEP]
by (metis mult.assoc power_commutes)
[PROOF STATE]
proof (state)
this:
z \<cdot> x \<cdot> x ^ n = z \<cdot> x ^ n \<cdot> x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z \<cdot> x \<cdot> x ^ n = z \<cdot> x ^ n \<cdot> x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
have "... \<le> y \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<cdot> x ^ n \<cdot> x \<le> y \<cdot> x
[PROOF STEP]
by (metis calculation(1) mult_isor)
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ n \<cdot> x \<le> y \<cdot> x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ n \<cdot> x \<le> y \<cdot> x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
have "... \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<cdot> x \<le> y
[PROOF STEP]
using \<open>z + y \<cdot> x \<le> y\<close>
[PROOF STATE]
proof (prove)
using this:
z + y \<cdot> x \<le> y

goal (1 subgoal):
 1. y \<cdot> x \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<cdot> x \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
z \<cdot> x ^ n \<le> y
z \<cdot> x ^ Suc n = z \<cdot> x \<cdot> x ^ n
z \<cdot> x \<cdot> x ^ n = z \<cdot> x ^ n \<cdot> x
z \<cdot> x ^ n \<cdot> x \<le> y \<cdot> x
y \<cdot> x \<le> y
[PROOF STEP]
have "z \<cdot> x ^ Suc n \<le> y"
[PROOF STATE]
proof (prove)
using this:
z \<cdot> x ^ n \<le> y
z \<cdot> x ^ Suc n = z \<cdot> x \<cdot> x ^ n
z \<cdot> x \<cdot> x ^ n = z \<cdot> x ^ n \<cdot> x
z \<cdot> x ^ n \<cdot> x \<le> y \<cdot> x
y \<cdot> x \<le> y

goal (1 subgoal):
 1. z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ Suc n \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ ?nb3 \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc ?nb3 \<le> y

goal (1 subgoal):
 1. \<And>n. \<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ n \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc n \<le> y
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z + y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ ?nb3 \<le> y; z + y \<cdot> x \<le> y\<rbrakk> \<Longrightarrow> z \<cdot> x ^ Suc ?nb3 \<le> y

goal (1 subgoal):
 1. z \<cdot> x ^ Suc n_ \<le> y
[PROOF STEP]
by (metis Suc)
[PROOF STATE]
proof (state)
this:
z \<cdot> x ^ Suc n_ \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_is_relpow: "rel_dioid.power X n = X ^^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_dioid.power X n = X ^^ n
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rel_dioid.power X 0 = X ^^ 0
 2. \<And>n. rel_dioid.power X n = X ^^ n \<Longrightarrow> rel_dioid.power X (Suc n) = X ^^ Suc n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. rel_dioid.power X 0 = X ^^ 0
 2. \<And>n. rel_dioid.power X n = X ^^ n \<Longrightarrow> rel_dioid.power X (Suc n) = X ^^ Suc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_dioid.power X 0 = X ^^ 0
[PROOF STEP]
by (metis rel_dioid.power_0 relpow.simps(1))
[PROOF STATE]
proof (state)
this:
rel_dioid.power X 0 = X ^^ 0

goal (1 subgoal):
 1. \<And>n. rel_dioid.power X n = X ^^ n \<Longrightarrow> rel_dioid.power X (Suc n) = X ^^ Suc n
[PROOF STEP]
case Suc
[PROOF STATE]
proof (state)
this:
rel_dioid.power X n_ = X ^^ n_

goal (1 subgoal):
 1. \<And>n. rel_dioid.power X n = X ^^ n \<Longrightarrow> rel_dioid.power X (Suc n) = X ^^ Suc n
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rel_dioid.power X n_ = X ^^ n_

goal (1 subgoal):
 1. rel_dioid.power X (Suc n_) = X ^^ Suc n_
[PROOF STEP]
by (metis rel_dioid.power_Suc2 relpow.simps(2))
[PROOF STATE]
proof (state)
this:
rel_dioid.power X (Suc n_) = X ^^ Suc n_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_star_def: "X^* = (\<Union>n. rel_dioid.power X n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X\<^sup>* = \<Union> (range (rel_dioid.power X))
[PROOF STEP]
by (simp add: power_is_relpow rtrancl_is_UN_relpow)


[STATEMENT]
lemma rel_star_contl: "X O Y^* = (\<Union>n. X O rel_dioid.power Y n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X O Y\<^sup>* = (\<Union>n. X O rel_dioid.power Y n)
[PROOF STEP]
by (metis rel_star_def relcomp_UNION_distrib)


[STATEMENT]
lemma rel_star_contr: "X^* O Y = (\<Union>n. (rel_dioid.power X n) O Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X\<^sup>* O Y = (\<Union>n. rel_dioid.power X n O Y)
[PROOF STEP]
by (metis rel_star_def relcomp_UNION_distrib2)


[STATEMENT]
lemma reach_PublicV_imples_FriendV[simp]:
assumes "reach s"
and "vis s pID \<noteq> PublicV"
shows "vis s pID = FriendV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vis s pID = FriendV
[PROOF STEP]
using assms reach_vis
[PROOF STATE]
proof (prove)
using this:
reach s
vis s pID \<noteq> PublicV
reach ?s \<Longrightarrow> vis ?s ?pID \<in> {FriendV, PublicV}

goal (1 subgoal):
 1. vis s pID = FriendV
[PROOF STEP]
by auto


[STATEMENT]
lemma reachNT_state:
assumes "reachNT s"
shows
"\<not> (\<exists> uid \<in> UIDs.
   uid \<in>\<in> userIDs s \<and> PID \<in>\<in> outerPostIDs s AID \<and>
   (uid = admin s \<or>
    (AID,outerOwner s AID PID) \<in>\<in> recvOuterFriendIDs s uid \<or>
     outerVis s AID PID = PublicV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> outerPostIDs s AID \<and> (uid = admin s \<or> (AID, outerOwner s AID PID) \<in>\<in> recvOuterFriendIDs s uid \<or> outerVis s AID PID = PublicV))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachNT s

goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> outerPostIDs s AID \<and> (uid = admin s \<or> (AID, outerOwner s AID PID) \<in>\<in> recvOuterFriendIDs s uid \<or> outerVis s AID PID = PublicV))
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs istate \<and> PID \<in>\<in> outerPostIDs istate AID \<and> (uid = admin istate \<or> (AID, outerOwner istate AID PID) \<in>\<in> recvOuterFriendIDs istate uid \<or> outerVis istate AID PID = PublicV))
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> outerPostIDs (srcOf trn) AID \<and> (uid = admin (srcOf trn) \<or> (AID, outerOwner (srcOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (srcOf trn) uid \<or> outerVis (srcOf trn) AID PID = PublicV)); validTrans trn; \<not> T trn\<rbrakk> \<Longrightarrow> \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> outerPostIDs (tgtOf trn) AID \<and> (uid = admin (tgtOf trn) \<or> (AID, outerOwner (tgtOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (tgtOf trn) uid \<or> outerVis (tgtOf trn) AID PID = PublicV))
[PROOF STEP]
case (Step trn)
[PROOF STATE]
proof (state)
this:
reachNT (srcOf trn)
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> outerPostIDs (srcOf trn) AID \<and> (uid = admin (srcOf trn) \<or> (AID, outerOwner (srcOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (srcOf trn) uid \<or> outerVis (srcOf trn) AID PID = PublicV))
validTrans trn
\<not> T trn

goal (2 subgoals):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs istate \<and> PID \<in>\<in> outerPostIDs istate AID \<and> (uid = admin istate \<or> (AID, outerOwner istate AID PID) \<in>\<in> recvOuterFriendIDs istate uid \<or> outerVis istate AID PID = PublicV))
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> outerPostIDs (srcOf trn) AID \<and> (uid = admin (srcOf trn) \<or> (AID, outerOwner (srcOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (srcOf trn) uid \<or> outerVis (srcOf trn) AID PID = PublicV)); validTrans trn; \<not> T trn\<rbrakk> \<Longrightarrow> \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> outerPostIDs (tgtOf trn) AID \<and> (uid = admin (tgtOf trn) \<or> (AID, outerOwner (tgtOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (tgtOf trn) uid \<or> outerVis (tgtOf trn) AID PID = PublicV))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
reachNT (srcOf trn)
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> outerPostIDs (srcOf trn) AID \<and> (uid = admin (srcOf trn) \<or> (AID, outerOwner (srcOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (srcOf trn) uid \<or> outerVis (srcOf trn) AID PID = PublicV))
validTrans trn
\<not> T trn

goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> outerPostIDs (tgtOf trn) AID \<and> (uid = admin (tgtOf trn) \<or> (AID, outerOwner (tgtOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (tgtOf trn) uid \<or> outerVis (tgtOf trn) AID PID = PublicV))
[PROOF STEP]
by (cases trn) auto
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> outerPostIDs (tgtOf trn) AID \<and> (uid = admin (tgtOf trn) \<or> (AID, outerOwner (tgtOf trn) AID PID) \<in>\<in> recvOuterFriendIDs (tgtOf trn) uid \<or> outerVis (tgtOf trn) AID PID = PublicV))

goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs istate \<and> PID \<in>\<in> outerPostIDs istate AID \<and> (uid = admin istate \<or> (AID, outerOwner istate AID PID) \<in>\<in> recvOuterFriendIDs istate uid \<or> outerVis istate AID PID = PublicV))
[PROOF STEP]
qed (simp add: istate_def)