[STATEMENT]
lemma (in MC_syntax) is_THDTMC:
  fixes I :: "'s pmf"
  defines "U \<equiv> (SIGMA s:UNIV. K s)\<^sup>* `` I"
  shows "Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
have [measurable]: "U \<in> sets (count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<in> sets (count_space UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U \<in> sets (count_space UNIV)

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
interpret prob_space "T' I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (T' I)
[PROOF STEP]
by (rule prob_space_T')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
fix s t I
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
have "\<And>t s. \<P>(\<omega> in T s. s = t) = indicator {t} s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t s. T.prob s {\<omega> \<in> space (T s). s = t} = indicat_real {t} s
[PROOF STEP]
using T.prob_space
[PROOF STATE]
proof (prove)
using this:
T.prob ?s (space (T ?s)) = 1

goal (1 subgoal):
 1. \<And>t s. T.prob s {\<omega> \<in> space (T s). s = t} = indicat_real {t} s
[PROOF STEP]
by (auto split: split_indicator)
[PROOF STATE]
proof (state)
this:
T.prob ?s1 {\<omega> \<in> space (T ?s1). ?s1 = ?t1} = indicat_real {?t1} ?s1

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T.prob ?s1 {\<omega> \<in> space (T ?s1). ?s1 = ?t1} = indicat_real {?t1} ?s1

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T.prob ?s1 {\<omega> \<in> space (T ?s1). ?s1 = ?t1} = indicat_real {?t1} ?s1
[PROOF STEP]
have "\<And>t t' s. \<P>(\<omega> in T s. shd \<omega> = t' \<and> s = t) = pmf (K t) t' * indicator {t} s"
[PROOF STATE]
proof (prove)
using this:
T.prob ?s1 {\<omega> \<in> space (T ?s1). ?s1 = ?t1} = indicat_real {?t1} ?s1

goal (1 subgoal):
 1. \<And>t t' s. T.prob s {\<omega> \<in> space (T s). shd \<omega> = t' \<and> s = t} = pmf (K t) t' * indicat_real {t} s
[PROOF STEP]
by (subst prob_T) (auto split: split_indicator simp: pmf.rep_eq)
[PROOF STATE]
proof (state)
this:
T.prob ?s1 {\<omega> \<in> space (T ?s1). shd \<omega> = ?t'1 \<and> ?s1 = ?t1} = pmf (K ?t1) ?t'1 * indicat_real {?t1} ?s1

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
T.prob ?s1 {\<omega> \<in> space (T ?s1). ?s1 = ?t1} = indicat_real {?t1} ?s1
T.prob ?s1 {\<omega> \<in> space (T ?s1). shd \<omega> = ?t'1 \<and> ?s1 = ?t1} = pmf (K ?t1) ?t'1 * indicat_real {?t1} ?s1
[PROOF STEP]
have "\<P>(\<omega> in T' I. shd (stl \<omega>) = t \<and> shd \<omega> = s) = \<P>(\<omega> in T' I. shd \<omega> = s) * pmf (K s) t"
[PROOF STATE]
proof (prove)
using this:
T.prob ?s1 {\<omega> \<in> space (T ?s1). ?s1 = ?t1} = indicat_real {?t1} ?s1
T.prob ?s1 {\<omega> \<in> space (T ?s1). shd \<omega> = ?t'1 \<and> ?s1 = ?t1} = pmf (K ?t1) ?t'1 * indicat_real {?t1} ?s1

goal (1 subgoal):
 1. \<P>(\<omega> in T' I. shd (stl \<omega>) = t \<and> shd \<omega> = s) = \<P>(\<omega> in T' I. shd \<omega> = s) * pmf (K s) t
[PROOF STEP]
by (simp add: prob_T' pmf.rep_eq)
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' I. shd (stl \<omega>) = t \<and> shd \<omega> = s) = \<P>(\<omega> in T' I. shd \<omega> = s) * pmf (K s) t

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' ?Ia3. shd (stl \<omega>) = ?t3 \<and> shd \<omega> = ?s3) = \<P>(\<omega> in T' ?Ia3. shd \<omega> = ?s3) * pmf (K ?s3) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
note start_eq = this
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' ?Ia3. shd (stl \<omega>) = ?t3 \<and> shd \<omega> = ?s3) = \<P>(\<omega> in T' ?Ia3. shd \<omega> = ?s3) * pmf (K ?s3) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' ?Ia3. shd (stl \<omega>) = ?t3 \<and> shd \<omega> = ?s3) = \<P>(\<omega> in T' ?Ia3. shd \<omega> = ?s3) * pmf (K ?s3) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
fix n s t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
assume "\<P>(\<omega> in T' I. \<omega> !! n = s) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! n = s} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! n = s} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
have "\<P>(\<omega> in T' I. \<omega> !! (Suc n) = t \<and> \<omega> !! n = s) = \<P>(\<omega> in T' I. \<omega> !! n = s) * pmf (K s) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> \<omega> !! n = s} = prob {\<omega> \<in> space (T' I). \<omega> !! n = s} * pmf (K s) t
[PROOF STEP]
proof (induction n arbitrary: I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I. \<P>(\<omega> in T' I. \<omega> !! Suc 0 = t \<and> \<omega> !! 0 = s) = \<P>(\<omega> in T' I. \<omega> !! 0 = s) * pmf (K s) t
 2. \<And>n I. (\<And>I. \<P>(\<omega> in T' I. \<omega> !! Suc n = t \<and> \<omega> !! n = s) = \<P>(\<omega> in T' I. \<omega> !! n = s) * pmf (K s) t) \<Longrightarrow> \<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> \<omega> !! Suc n = s) = \<P>(\<omega> in T' I. \<omega> !! Suc n = s) * pmf (K s) t
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' ?I1. \<omega> !! Suc n = t \<and> \<omega> !! n = s) = \<P>(\<omega> in T' ?I1. \<omega> !! n = s) * pmf (K s) t

goal (2 subgoals):
 1. \<And>I. \<P>(\<omega> in T' I. \<omega> !! Suc 0 = t \<and> \<omega> !! 0 = s) = \<P>(\<omega> in T' I. \<omega> !! 0 = s) * pmf (K s) t
 2. \<And>n I. (\<And>I. \<P>(\<omega> in T' I. \<omega> !! Suc n = t \<and> \<omega> !! n = s) = \<P>(\<omega> in T' I. \<omega> !! n = s) * pmf (K s) t) \<Longrightarrow> \<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> \<omega> !! Suc n = s) = \<P>(\<omega> in T' I. \<omega> !! Suc n = s) * pmf (K s) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<P>(\<omega> in T' ?I1. \<omega> !! Suc n = t \<and> \<omega> !! n = s) = \<P>(\<omega> in T' ?I1. \<omega> !! n = s) * pmf (K s) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<P>(\<omega> in T' ?I1. \<omega> !! Suc n = t \<and> \<omega> !! n = s) = \<P>(\<omega> in T' ?I1. \<omega> !! n = s) * pmf (K s) t

goal (1 subgoal):
 1. \<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> \<omega> !! Suc n = s) = \<P>(\<omega> in T' I. \<omega> !! Suc n = s) * pmf (K s) t
[PROOF STEP]
by (subst (1 2) prob_T') (simp_all del: space_T add: T_eq_T')
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> \<omega> !! Suc n = s) = \<P>(\<omega> in T' I. \<omega> !! Suc n = s) * pmf (K s) t

goal (1 subgoal):
 1. \<And>I. \<P>(\<omega> in T' I. \<omega> !! Suc 0 = t \<and> \<omega> !! 0 = s) = \<P>(\<omega> in T' I. \<omega> !! 0 = s) * pmf (K s) t
[PROOF STEP]
qed (simp add: start_eq)
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> \<omega> !! n = s} = prob {\<omega> \<in> space (T' I). \<omega> !! n = s} * pmf (K s) t

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space (T' I). \<omega> !! n = s} \<noteq> 0
prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> \<omega> !! n = s} = prob {\<omega> \<in> space (T' I). \<omega> !! n = s} * pmf (K s) t
[PROOF STEP]
have "\<P>(\<omega> in T' I. stl \<omega> !! n = t \<bar> \<omega> !! n = s) = pmf (K s) t"
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space (T' I). \<omega> !! n = s} \<noteq> 0
prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> \<omega> !! n = s} = prob {\<omega> \<in> space (T' I). \<omega> !! n = s} * pmf (K s) t

goal (1 subgoal):
 1. cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! n = t) (\<lambda>\<omega>. \<omega> !! n = s) = pmf (K s) t
[PROOF STEP]
by (simp add: cond_prob_def field_simps)
[PROOF STATE]
proof (state)
this:
cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! n = t) (\<lambda>\<omega>. \<omega> !! n = s) = pmf (K s) t

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! ?n3 = ?s3} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! ?n3 = ?t3) (\<lambda>\<omega>. \<omega> !! ?n3 = ?s3) = pmf (K ?s3) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
note TH = this
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! ?n3 = ?s3} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! ?n3 = ?t3) (\<lambda>\<omega>. \<omega> !! ?n3 = ?s3) = pmf (K ?s3) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! ?n3 = ?s3} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! ?n3 = ?t3) (\<lambda>\<omega>. \<omega> !! ?n3 = ?s3) = pmf (K ?s3) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
fix n \<omega>' t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
assume "\<P>(\<omega> in T' I. \<forall>i\<le>n. \<omega> !! i = \<omega>' i) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
have "\<P>(\<omega> in T' I. \<omega> !! (Suc n) = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)) =
      \<P>(\<omega> in T' I. \<forall>i\<le>n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' n)) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)} = prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} * pmf (K (\<omega>' n)) t
[PROOF STEP]
proof (induction n arbitrary: I \<omega>')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I \<omega>'. \<P>(\<omega> in T' I. \<omega> !! Suc 0 = t \<and> (\<forall>i\<le>0. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>0. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' 0)) t
 2. \<And>n I \<omega>'. (\<And>I \<omega>'. \<P>(\<omega> in T' I. \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' n)) t) \<Longrightarrow> \<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> (\<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' (Suc n))) t
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' ?I1. \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = ?\<omega>'1 i)) = \<P>(\<omega> in T' ?I1. \<forall>i\<le>n. \<omega> !! i = ?\<omega>'1 i) * pmf (K (?\<omega>'1 n)) t

goal (2 subgoals):
 1. \<And>I \<omega>'. \<P>(\<omega> in T' I. \<omega> !! Suc 0 = t \<and> (\<forall>i\<le>0. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>0. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' 0)) t
 2. \<And>n I \<omega>'. (\<And>I \<omega>'. \<P>(\<omega> in T' I. \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' n)) t) \<Longrightarrow> \<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> (\<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' (Suc n))) t
[PROOF STEP]
have *[simp]: "\<And>s P. measure (T' (K s)) {x. s = \<omega>' 0 \<and> P x} =
        measure (T' (K (\<omega>' 0))) {x. P x} * indicator {\<omega>' 0} s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s P. Sigma_Algebra.measure (T' (K s)) {x. s = \<omega>' 0 \<and> P x} = Sigma_Algebra.measure (T' (K (\<omega>' 0))) {x. P x} * indicat_real {\<omega>' 0} s
[PROOF STEP]
by (auto split: split_indicator)
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure (T' (K ?s1)) {x. ?s1 = \<omega>' 0 \<and> ?P1 x} = Sigma_Algebra.measure (T' (K (\<omega>' 0))) {x. ?P1 x} * indicat_real {\<omega>' 0} ?s1

goal (2 subgoals):
 1. \<And>I \<omega>'. \<P>(\<omega> in T' I. \<omega> !! Suc 0 = t \<and> (\<forall>i\<le>0. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>0. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' 0)) t
 2. \<And>n I \<omega>'. (\<And>I \<omega>'. \<P>(\<omega> in T' I. \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' n)) t) \<Longrightarrow> \<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> (\<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' (Suc n))) t
[PROOF STEP]
from Suc[of _ "\<lambda>i. \<omega>' (Suc i)"]
[PROOF STATE]
proof (chain)
picking this:
\<P>(\<omega> in T' ?I1. \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' (Suc i))) = \<P>(\<omega> in T' ?I1. \<forall>i\<le>n. \<omega> !! i = \<omega>' (Suc i)) * pmf (K (\<omega>' (Suc n))) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<P>(\<omega> in T' ?I1. \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' (Suc i))) = \<P>(\<omega> in T' ?I1. \<forall>i\<le>n. \<omega> !! i = \<omega>' (Suc i)) * pmf (K (\<omega>' (Suc n))) t

goal (1 subgoal):
 1. \<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> (\<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' (Suc n))) t
[PROOF STEP]
by (subst (1 2) prob_T')
           (simp_all add: T_eq_T' all_Suc_split[where P="\<lambda>i. i \<le> Suc n \<longrightarrow> Q i" for n Q] conj_commute conj_left_commute sets_eq_imp_space_eq[OF sets_T'])
[PROOF STATE]
proof (state)
this:
\<P>(\<omega> in T' I. \<omega> !! Suc (Suc n) = t \<and> (\<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>Suc n. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' (Suc n))) t

goal (1 subgoal):
 1. \<And>I \<omega>'. \<P>(\<omega> in T' I. \<omega> !! Suc 0 = t \<and> (\<forall>i\<le>0. \<omega> !! i = \<omega>' i)) = \<P>(\<omega> in T' I. \<forall>i\<le>0. \<omega> !! i = \<omega>' i) * pmf (K (\<omega>' 0)) t
[PROOF STEP]
qed (simp add: start_eq)
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)} = prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} * pmf (K (\<omega>' n)) t

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} \<noteq> 0
prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)} = prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} * pmf (K (\<omega>' n)) t
[PROOF STEP]
have "\<P>(\<omega> in T' I. stl \<omega> !! n = t \<bar> \<forall>i\<le>n. \<omega> !! i = \<omega>' i) = pmf (K (\<omega>' n)) t"
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} \<noteq> 0
prob {\<omega> \<in> space (T' I). \<omega> !! Suc n = t \<and> (\<forall>i\<le>n. \<omega> !! i = \<omega>' i)} = prob {\<omega> \<in> space (T' I). \<forall>i\<le>n. \<omega> !! i = \<omega>' i} * pmf (K (\<omega>' n)) t

goal (1 subgoal):
 1. cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! n = t) (\<lambda>\<omega>. \<forall>i\<le>n. \<omega> !! i = \<omega>' i) = pmf (K (\<omega>' n)) t
[PROOF STEP]
by (simp add: cond_prob_def field_simps)
[PROOF STATE]
proof (state)
this:
cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! n = t) (\<lambda>\<omega>. \<forall>i\<le>n. \<omega> !! i = \<omega>' i) = pmf (K (\<omega>' n)) t

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>i\<le>?n3. \<omega> !! i = ?\<omega>'3 i} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! ?n3 = ?t3) (\<lambda>\<omega>. \<forall>i\<le>?n3. \<omega> !! i = ?\<omega>'3 i) = pmf (K (?\<omega>'3 ?n3)) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
note MC = this
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>i\<le>?n3. \<omega> !! i = ?\<omega>'3 i} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! ?n3 = ?t3) (\<lambda>\<omega>. \<forall>i\<le>?n3. \<omega> !! i = ?\<omega>'3 i) = pmf (K (?\<omega>'3 ?n3)) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>i\<le>?n3. \<omega> !! i = ?\<omega>'3 i} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. stl \<omega> !! ?n3 = ?t3) (\<lambda>\<omega>. \<forall>i\<le>?n3. \<omega> !! i = ?\<omega>'3 i) = pmf (K (?\<omega>'3 ?n3)) ?t3

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
fix n \<omega>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
assume "\<P>(\<omega> in T' I. \<forall>t\<le>n. \<omega> !! t = \<omega>' t) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
have "\<P>(\<omega> in T' I. \<forall>t\<le>n. \<omega> !! t = \<omega>' t) \<le> \<P>(\<omega> in T' I. \<omega> !! n = \<omega>' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<le> prob {\<omega> \<in> space (T' I). \<omega> !! n = \<omega>' n}
[PROOF STEP]
by (auto intro!: finite_measure_mono_AE simp: sets_T' sets_eq_imp_space_eq[OF sets_T'])
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<le> prob {\<omega> \<in> space (T' I). \<omega> !! n = \<omega>' n}

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<noteq> 0
prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<le> prob {\<omega> \<in> space (T' I). \<omega> !! n = \<omega>' n}
[PROOF STEP]
have "\<P>(\<omega> in T' I. \<omega> !! n = \<omega>' n) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<noteq> 0
prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = \<omega>' t} \<le> prob {\<omega> \<in> space (T' I). \<omega> !! n = \<omega>' n}

goal (1 subgoal):
 1. prob {\<omega> \<in> space (T' I). \<omega> !! n = \<omega>' n} \<noteq> 0
[PROOF STEP]
by (auto simp: neq_iff not_less measure_le_0_iff)
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<omega> !! n = \<omega>' n} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>t\<le>?n3. \<omega> !! t = ?\<omega>'3 t} \<noteq> 0 \<Longrightarrow> prob {\<omega> \<in> space (T' I). \<omega> !! ?n3 = ?\<omega>'3 ?n3} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
note MC' = this
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space (T' I). \<forall>t\<le>?n3. \<omega> !! t = ?\<omega>'3 t} \<noteq> 0 \<Longrightarrow> prob {\<omega> \<in> space (T' I). \<omega> !! ?n3 = ?\<omega>'3 ?n3} \<noteq> 0

goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t. random_variable (count_space UNIV) (\<lambda>\<omega>. \<omega> !! t)
 2. countable U
 3. \<And>n. AE x in T' I. x !! n \<in> U
 4. \<And>n s s'. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = s t} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<forall>t\<le>n. \<omega> !! t = s t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<omega> !! n = s n)
 5. \<And>n m s t. \<lbrakk>prob {\<omega> \<in> space (T' I). \<omega> !! n = t} \<noteq> 0; prob {\<omega> \<in> space (T' I). \<omega> !! m = t} \<noteq> 0\<rbrakk> \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s) (\<lambda>\<omega>. \<omega> !! n = t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc m = s) (\<lambda>\<omega>. \<omega> !! m = t)
[PROOF STEP]
show "countable U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable U
[PROOF STEP]
unfolding U_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (acc `` set_pmf I)
[PROOF STEP]
by (rule countable_reachable countable_Image countable_set_pmf)+
[PROOF STATE]
proof (state)
this:
countable U

goal (4 subgoals):
 1. \<And>t. random_variable (count_space UNIV) (\<lambda>\<omega>. \<omega> !! t)
 2. \<And>n. AE x in T' I. x !! n \<in> U
 3. \<And>n s s'. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = s t} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<forall>t\<le>n. \<omega> !! t = s t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<omega> !! n = s n)
 4. \<And>n m s t. \<lbrakk>prob {\<omega> \<in> space (T' I). \<omega> !! n = t} \<noteq> 0; prob {\<omega> \<in> space (T' I). \<omega> !! m = t} \<noteq> 0\<rbrakk> \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s) (\<lambda>\<omega>. \<omega> !! n = t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc m = s) (\<lambda>\<omega>. \<omega> !! m = t)
[PROOF STEP]
show "\<And>t. (\<lambda>\<omega>. \<omega> !! t) \<in> measurable (T' I) (count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. random_variable (count_space UNIV) (\<lambda>\<omega>. \<omega> !! t)
[PROOF STEP]
by (subst measurable_cong_sets[OF sets_T' refl]) simp
[PROOF STATE]
proof (state)
this:
random_variable (count_space UNIV) (\<lambda>\<omega>. \<omega> !! ?t1)

goal (3 subgoals):
 1. \<And>n. AE x in T' I. x !! n \<in> U
 2. \<And>n s s'. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = s t} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<forall>t\<le>n. \<omega> !! t = s t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<omega> !! n = s n)
 3. \<And>n m s t. \<lbrakk>prob {\<omega> \<in> space (T' I). \<omega> !! n = t} \<noteq> 0; prob {\<omega> \<in> space (T' I). \<omega> !! m = t} \<noteq> 0\<rbrakk> \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s) (\<lambda>\<omega>. \<omega> !! n = t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc m = s) (\<lambda>\<omega>. \<omega> !! m = t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. AE x in T' I. x !! n \<in> U
 2. \<And>n s s'. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = s t} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<forall>t\<le>n. \<omega> !! t = s t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<omega> !! n = s n)
 3. \<And>n m s t. \<lbrakk>prob {\<omega> \<in> space (T' I). \<omega> !! n = t} \<noteq> 0; prob {\<omega> \<in> space (T' I). \<omega> !! m = t} \<noteq> 0\<rbrakk> \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s) (\<lambda>\<omega>. \<omega> !! n = t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc m = s) (\<lambda>\<omega>. \<omega> !! m = t)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. AE x in T' I. x !! n \<in> U
 2. \<And>n s s'. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = s t} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<forall>t\<le>n. \<omega> !! t = s t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<omega> !! n = s n)
 3. \<And>n m s t. \<lbrakk>prob {\<omega> \<in> space (T' I). \<omega> !! n = t} \<noteq> 0; prob {\<omega> \<in> space (T' I). \<omega> !! m = t} \<noteq> 0\<rbrakk> \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s) (\<lambda>\<omega>. \<omega> !! n = t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc m = s) (\<lambda>\<omega>. \<omega> !! m = t)
[PROOF STEP]
have "\<forall>x\<in>I. AE y in T x. (x ## y) !! n \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> U
[PROOF STEP]
unfolding U_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I
[PROOF STEP]
proof (induction n arbitrary: I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! 0 \<in> acc `` set_pmf I
 2. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! 0 \<in> acc `` set_pmf I
 2. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! 0 \<in> acc `` set_pmf I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! 0 \<in> acc `` set_pmf I

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf ?I1. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf ?I1

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf ?I1. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf ?I1

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
assume "x \<in> I"
[PROOF STATE]
proof (state)
this:
x \<in> set_pmf I

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
have "AE y in T x. y !! n \<in> (SIGMA x:UNIV. K x)\<^sup>* `` K x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE y in T x. y !! n \<in> acc `` set_pmf (K x)
[PROOF STEP]
apply (subst AE_T_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Measurable.pred (stream_space (count_space UNIV)) (\<lambda>y. y !! n \<in> acc `` set_pmf (K x))
 2. \<forall>y\<in>set_pmf (K x). AE \<omega> in T y. (y ## \<omega>) !! n \<in> acc `` set_pmf (K x)
[PROOF STEP]
apply (rule measurable_compose[OF measurable_snth], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>set_pmf (K x). AE \<omega> in T y. (y ## \<omega>) !! n \<in> acc `` set_pmf (K x)
[PROOF STEP]
apply (rule Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AE y in T x. y !! n \<in> acc `` set_pmf (K x)

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE y in T x. y !! n \<in> acc `` set_pmf (K x)

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
have "(SIGMA x:UNIV. K x)\<^sup>* `` K x \<subseteq> (SIGMA x:UNIV. K x)\<^sup>* `` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc `` set_pmf (K x) \<subseteq> acc `` set_pmf I
[PROOF STEP]
using \<open>x \<in> I\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf I

goal (1 subgoal):
 1. acc `` set_pmf (K x) \<subseteq> acc `` set_pmf I
[PROOF STEP]
by (auto intro: converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
acc `` set_pmf (K x) \<subseteq> acc `` set_pmf I

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE y in T x. y !! n \<in> acc `` set_pmf (K x)
acc `` set_pmf (K x) \<subseteq> acc `` set_pmf I
[PROOF STEP]
have "AE y in T x. y !! n \<in> (SIGMA x:UNIV. K x)\<^sup>* `` I"
[PROOF STATE]
proof (prove)
using this:
AE y in T x. y !! n \<in> acc `` set_pmf (K x)
acc `` set_pmf (K x) \<subseteq> acc `` set_pmf I

goal (1 subgoal):
 1. AE y in T x. y !! n \<in> acc `` set_pmf I
[PROOF STEP]
by (auto simp: subset_eq)
[PROOF STATE]
proof (state)
this:
AE y in T x. y !! n \<in> acc `` set_pmf I

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x3 \<in> set_pmf I \<Longrightarrow> AE y in T ?x3. y !! n \<in> acc `` set_pmf I

goal (1 subgoal):
 1. \<And>n I. (\<And>I. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> acc `` set_pmf I) \<Longrightarrow> \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x3 \<in> set_pmf I \<Longrightarrow> AE y in T ?x3. y !! n \<in> acc `` set_pmf I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> set_pmf I \<Longrightarrow> AE y in T ?x3. y !! n \<in> acc `` set_pmf I

goal (1 subgoal):
 1. \<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! Suc n \<in> acc `` set_pmf I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> U

goal (3 subgoals):
 1. \<And>n. AE x in T' I. x !! n \<in> U
 2. \<And>n s s'. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = s t} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<forall>t\<le>n. \<omega> !! t = s t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<omega> !! n = s n)
 3. \<And>n m s t. \<lbrakk>prob {\<omega> \<in> space (T' I). \<omega> !! n = t} \<noteq> 0; prob {\<omega> \<in> space (T' I). \<omega> !! m = t} \<noteq> 0\<rbrakk> \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s) (\<lambda>\<omega>. \<omega> !! n = t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc m = s) (\<lambda>\<omega>. \<omega> !! m = t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> U
[PROOF STEP]
show "AE x in T' I. x !! n \<in> U"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set_pmf I. AE y in T x. (x ## y) !! n \<in> U

goal (1 subgoal):
 1. AE x in T' I. x !! n \<in> U
[PROOF STEP]
by (simp add: AE_T')
[PROOF STATE]
proof (state)
this:
AE x in T' I. x !! n \<in> U

goal (2 subgoals):
 1. \<And>n s s'. prob {\<omega> \<in> space (T' I). \<forall>t\<le>n. \<omega> !! t = s t} \<noteq> 0 \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<forall>t\<le>n. \<omega> !! t = s t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s') (\<lambda>\<omega>. \<omega> !! n = s n)
 2. \<And>n m s t. \<lbrakk>prob {\<omega> \<in> space (T' I). \<omega> !! n = t} \<noteq> 0; prob {\<omega> \<in> space (T' I). \<omega> !! m = t} \<noteq> 0\<rbrakk> \<Longrightarrow> cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc n = s) (\<lambda>\<omega>. \<omega> !! n = t) = cond_prob (T' I) (\<lambda>\<omega>. \<omega> !! Suc m = s) (\<lambda>\<omega>. \<omega> !! m = t)
[PROOF STEP]
qed (simp_all add: TH MC MC')
[PROOF STATE]
proof (state)
this:
Time_Homogeneous_Discrete_Markov_Process (T' I) U (\<lambda>n \<omega>. \<omega> !! n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_submatrix_UNIV:
assumes "i < card {i. i < dim_row A \<and> i \<in> I}"
shows "row (submatrix A I UNIV) i = row A (pick I i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (submatrix A I UNIV) i = row A (pick I i)
[PROOF STEP]
proof (rule eq_vecI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < dim_vec (row A (pick I i)) \<Longrightarrow> row (submatrix A I UNIV) i $ ia = row A (pick I i) $ ia
 2. dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))
[PROOF STEP]
show dim_eq:"dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))
[PROOF STEP]
unfolding carrier_vecD[OF row_carrier] dim_submatrix
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {j. j < dim_col A \<and> j \<in> UNIV} = dim_col A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (row A (pick I i)) \<Longrightarrow> row (submatrix A I UNIV) i $ ia = row A (pick I i) $ ia
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (row A (pick I i)) \<Longrightarrow> row (submatrix A I UNIV) i $ ia = row A (pick I i) $ ia
[PROOF STEP]
assume "j < dim_vec (row A (pick I i))"
[PROOF STATE]
proof (state)
this:
j < dim_vec (row A (pick I i))

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (row A (pick I i)) \<Longrightarrow> row (submatrix A I UNIV) i $ ia = row A (pick I i) $ ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < dim_vec (row A (pick I i))
[PROOF STEP]
have "j < dim_col (submatrix A I UNIV)" "j < dim_col A" "j < card {j. j < dim_col A \<and> j \<in> UNIV}"
[PROOF STATE]
proof (prove)
using this:
j < dim_vec (row A (pick I i))

goal (1 subgoal):
 1. j < dim_col (submatrix A I UNIV) &&& j < dim_col A &&& j < card {j. j < dim_col A \<and> j \<in> UNIV}
[PROOF STEP]
using dim_eq
[PROOF STATE]
proof (prove)
using this:
j < dim_vec (row A (pick I i))
dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))

goal (1 subgoal):
 1. j < dim_col (submatrix A I UNIV) &&& j < dim_col A &&& j < card {j. j < dim_col A \<and> j \<in> UNIV}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < dim_col (submatrix A I UNIV)
j < dim_col A
j < card {j. j < dim_col A \<and> j \<in> UNIV}

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (row A (pick I i)) \<Longrightarrow> row (submatrix A I UNIV) i $ ia = row A (pick I i) $ ia
[PROOF STEP]
show "row (submatrix A I UNIV) i $ j = row A (pick I i) $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (submatrix A I UNIV) i $ j = row A (pick I i) $ j
[PROOF STEP]
unfolding row_def index_vec[OF \<open>j < dim_col (submatrix A I UNIV)\<close>] index_vec[OF \<open>j < dim_col A\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A I UNIV $$ (i, j) = A $$ (pick I i, j)
[PROOF STEP]
using submatrix_index[OF assms \<open>j < card {j. j < dim_col A \<and> j \<in> UNIV}\<close>]
[PROOF STATE]
proof (prove)
using this:
submatrix A I UNIV $$ (i, j) = A $$ (pick I i, pick UNIV j)

goal (1 subgoal):
 1. submatrix A I UNIV $$ (i, j) = A $$ (pick I i, j)
[PROOF STEP]
using pick_UNIV
[PROOF STATE]
proof (prove)
using this:
submatrix A I UNIV $$ (i, j) = A $$ (pick I i, pick UNIV j)
pick UNIV ?j = ?j

goal (1 subgoal):
 1. submatrix A I UNIV $$ (i, j) = A $$ (pick I i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (submatrix A I UNIV) i $ j = row A (pick I i) $ j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_cols_submatrix_UNIV:
assumes "distinct (cols (submatrix A I UNIV))"
shows "distinct (cols A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (cols A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (cols (submatrix A I UNIV))

goal (1 subgoal):
 1. distinct (cols A)
[PROOF STEP]
proof (rule contrapos_pp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (cols A) \<Longrightarrow> \<not> distinct (cols (submatrix A I UNIV))
[PROOF STEP]
assume "\<not> distinct (cols A)"
[PROOF STATE]
proof (state)
this:
\<not> distinct (cols A)

goal (1 subgoal):
 1. \<not> distinct (cols A) \<Longrightarrow> \<not> distinct (cols (submatrix A I UNIV))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> distinct (cols A)
[PROOF STEP]
obtain i j where "i < dim_col A" "j < dim_col A" "(cols A)!i = (cols A)!j" "i\<noteq>j"
[PROOF STATE]
proof (prove)
using this:
\<not> distinct (cols A)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < dim_col A; j < dim_col A; cols A ! i = cols A ! j; i \<noteq> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using distinct_conv_nth cols_length
[PROOF STATE]
proof (prove)
using this:
\<not> distinct (cols A)
distinct ?xs = (\<forall>i<length ?xs. \<forall>j<length ?xs. i \<noteq> j \<longrightarrow> ?xs ! i \<noteq> ?xs ! j)
length (cols ?A) = dim_col ?A

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < dim_col A; j < dim_col A; cols A ! i = cols A ! j; i \<noteq> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i < dim_col A
j < dim_col A
cols A ! i = cols A ! j
i \<noteq> j

goal (1 subgoal):
 1. \<not> distinct (cols A) \<Longrightarrow> \<not> distinct (cols (submatrix A I UNIV))
[PROOF STEP]
have "i < dim_col (submatrix A I UNIV)" "j < dim_col (submatrix A I UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_col (submatrix A I UNIV) &&& j < dim_col (submatrix A I UNIV)
[PROOF STEP]
unfolding dim_submatrix
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < card {j. j < dim_col A \<and> j \<in> UNIV} &&& j < card {j. j < dim_col A \<and> j \<in> UNIV}
[PROOF STEP]
using \<open>i < dim_col A\<close> \<open>j < dim_col A\<close>
[PROOF STATE]
proof (prove)
using this:
i < dim_col A
j < dim_col A

goal (1 subgoal):
 1. i < card {j. j < dim_col A \<and> j \<in> UNIV} &&& j < card {j. j < dim_col A \<and> j \<in> UNIV}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
i < dim_col (submatrix A I UNIV)
j < dim_col (submatrix A I UNIV)

goal (1 subgoal):
 1. \<not> distinct (cols A) \<Longrightarrow> \<not> distinct (cols (submatrix A I UNIV))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_col (submatrix A I UNIV)
j < dim_col (submatrix A I UNIV)
[PROOF STEP]
have "i < length (cols (submatrix A I UNIV))" "j < length (cols (submatrix A I UNIV))"
[PROOF STATE]
proof (prove)
using this:
i < dim_col (submatrix A I UNIV)
j < dim_col (submatrix A I UNIV)

goal (1 subgoal):
 1. i < length (cols (submatrix A I UNIV)) &&& j < length (cols (submatrix A I UNIV))
[PROOF STEP]
unfolding cols_length
[PROOF STATE]
proof (prove)
using this:
i < dim_col (submatrix A I UNIV)
j < dim_col (submatrix A I UNIV)

goal (1 subgoal):
 1. i < dim_col (submatrix A I UNIV) &&& j < dim_col (submatrix A I UNIV)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
i < length (cols (submatrix A I UNIV))
j < length (cols (submatrix A I UNIV))

goal (1 subgoal):
 1. \<not> distinct (cols A) \<Longrightarrow> \<not> distinct (cols (submatrix A I UNIV))
[PROOF STEP]
have "(cols (submatrix A I UNIV))!i = (cols (submatrix A I UNIV))!j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cols (submatrix A I UNIV) ! i = cols (submatrix A I UNIV) ! j
[PROOF STEP]
proof (rule eq_vecI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
 2. dim_vec (cols (submatrix A I UNIV) ! i) = dim_vec (cols (submatrix A I UNIV) ! j)
[PROOF STEP]
show "dim_vec (cols (submatrix A I UNIV) ! i) = dim_vec (cols (submatrix A I UNIV) ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (cols (submatrix A I UNIV) ! i) = dim_vec (cols (submatrix A I UNIV) ! j)
[PROOF STEP]
by (simp add: \<open>i < dim_col (submatrix A I UNIV)\<close> \<open>j < dim_col (submatrix A I UNIV)\<close>)
[PROOF STATE]
proof (state)
this:
dim_vec (cols (submatrix A I UNIV) ! i) = dim_vec (cols (submatrix A I UNIV) ! j)

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
[PROOF STEP]
assume "k < dim_vec (cols (submatrix A I UNIV) ! j)"
[PROOF STATE]
proof (state)
this:
k < dim_vec (cols (submatrix A I UNIV) ! j)

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < dim_vec (cols (submatrix A I UNIV) ! j)
[PROOF STEP]
have "k < dim_row (submatrix A I UNIV)"
[PROOF STATE]
proof (prove)
using this:
k < dim_vec (cols (submatrix A I UNIV) ! j)

goal (1 subgoal):
 1. k < dim_row (submatrix A I UNIV)
[PROOF STEP]
using \<open>j < length (cols (submatrix A I UNIV))\<close>
[PROOF STATE]
proof (prove)
using this:
k < dim_vec (cols (submatrix A I UNIV) ! j)
j < length (cols (submatrix A I UNIV))

goal (1 subgoal):
 1. k < dim_row (submatrix A I UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < dim_row (submatrix A I UNIV)

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < dim_row (submatrix A I UNIV)
[PROOF STEP]
have  "k < card {j. j < dim_row A \<and> j \<in> I}"
[PROOF STATE]
proof (prove)
using this:
k < dim_row (submatrix A I UNIV)

goal (1 subgoal):
 1. k < card {j. j < dim_row A \<and> j \<in> I}
[PROOF STEP]
using dim_submatrix(1)
[PROOF STATE]
proof (prove)
using this:
k < dim_row (submatrix A I UNIV)
dim_row (submatrix ?A ?I ?J) = card {i. i < dim_row ?A \<and> i \<in> ?I}

goal (1 subgoal):
 1. k < card {j. j < dim_row A \<and> j \<in> I}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
k < card {j. j < dim_row A \<and> j \<in> I}

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
[PROOF STEP]
have i_transfer:"cols (submatrix A I UNIV) ! i $ k = (cols A) ! i $ (pick I k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cols (submatrix A I UNIV) ! i $ k = cols A ! i $ pick I k
[PROOF STEP]
unfolding cols_nth[OF \<open>i < dim_col (submatrix A I UNIV)\<close>] col_def index_vec[OF \<open>k < dim_row (submatrix A I UNIV)\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A I UNIV $$ (k, i) = cols A ! i $ pick I k
[PROOF STEP]
unfolding submatrix_index[OF \<open>k < card {j. j < dim_row A \<and> j \<in> I}\<close> \<open>i < dim_col (submatrix A I UNIV)\<close>[unfolded dim_submatrix]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (pick I k, pick UNIV i) = cols A ! i $ pick I k
[PROOF STEP]
unfolding pick_UNIV cols_nth[OF \<open>i < dim_col A\<close>] col_def index_vec[OF pick_le[OF \<open>k < card {j. j < dim_row A \<and> j \<in> I}\<close>]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (pick I k, i) = A $$ (pick I k, i)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cols (submatrix A I UNIV) ! i $ k = cols A ! i $ pick I k

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
[PROOF STEP]
have j_transfer:"cols (submatrix A I UNIV) ! j $ k = (cols A) ! j $ (pick I k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cols (submatrix A I UNIV) ! j $ k = cols A ! j $ pick I k
[PROOF STEP]
unfolding cols_nth[OF \<open>j < dim_col (submatrix A I UNIV)\<close>] col_def index_vec[OF \<open>k < dim_row (submatrix A I UNIV)\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A I UNIV $$ (k, j) = cols A ! j $ pick I k
[PROOF STEP]
unfolding submatrix_index[OF \<open>k < card {j. j < dim_row A \<and> j \<in> I}\<close> \<open>j < dim_col (submatrix A I UNIV)\<close>[unfolded dim_submatrix]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (pick I k, pick UNIV j) = cols A ! j $ pick I k
[PROOF STEP]
unfolding pick_UNIV cols_nth[OF \<open>j < dim_col A\<close>] col_def index_vec[OF pick_le[OF \<open>k < card {j. j < dim_row A \<and> j \<in> I}\<close>]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (pick I k, j) = A $$ (pick I k, j)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cols (submatrix A I UNIV) ! j $ k = cols A ! j $ pick I k

goal (1 subgoal):
 1. \<And>ia. ia < dim_vec (cols (submatrix A I UNIV) ! j) \<Longrightarrow> cols (submatrix A I UNIV) ! i $ ia = cols (submatrix A I UNIV) ! j $ ia
[PROOF STEP]
show "cols (submatrix A I UNIV) ! i $ k = cols (submatrix A I UNIV) ! j $ k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cols (submatrix A I UNIV) ! i $ k = cols (submatrix A I UNIV) ! j $ k
[PROOF STEP]
using \<open>cols A ! i = cols A ! j\<close> i_transfer j_transfer
[PROOF STATE]
proof (prove)
using this:
cols A ! i = cols A ! j
cols (submatrix A I UNIV) ! i $ k = cols A ! i $ pick I k
cols (submatrix A I UNIV) ! j $ k = cols A ! j $ pick I k

goal (1 subgoal):
 1. cols (submatrix A I UNIV) ! i $ k = cols (submatrix A I UNIV) ! j $ k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cols (submatrix A I UNIV) ! i $ k = cols (submatrix A I UNIV) ! j $ k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cols (submatrix A I UNIV) ! i = cols (submatrix A I UNIV) ! j

goal (1 subgoal):
 1. \<not> distinct (cols A) \<Longrightarrow> \<not> distinct (cols (submatrix A I UNIV))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cols (submatrix A I UNIV) ! i = cols (submatrix A I UNIV) ! j
[PROOF STEP]
show "\<not> distinct (cols (submatrix A I UNIV))"
[PROOF STATE]
proof (prove)
using this:
cols (submatrix A I UNIV) ! i = cols (submatrix A I UNIV) ! j

goal (1 subgoal):
 1. \<not> distinct (cols (submatrix A I UNIV))
[PROOF STEP]
unfolding distinct_conv_nth
[PROOF STATE]
proof (prove)
using this:
cols (submatrix A I UNIV) ! i = cols (submatrix A I UNIV) ! j

goal (1 subgoal):
 1. \<not> (\<forall>i<length (cols (submatrix A I UNIV)). \<forall>j<length (cols (submatrix A I UNIV)). i \<noteq> j \<longrightarrow> cols (submatrix A I UNIV) ! i \<noteq> cols (submatrix A I UNIV) ! j)
[PROOF STEP]
using \<open>i < length (cols (submatrix A I UNIV))\<close> \<open>j < length (cols (submatrix A I UNIV))\<close> \<open>i \<noteq> j\<close>
[PROOF STATE]
proof (prove)
using this:
cols (submatrix A I UNIV) ! i = cols (submatrix A I UNIV) ! j
i < length (cols (submatrix A I UNIV))
j < length (cols (submatrix A I UNIV))
i \<noteq> j

goal (1 subgoal):
 1. \<not> (\<forall>i<length (cols (submatrix A I UNIV)). \<forall>j<length (cols (submatrix A I UNIV)). i \<noteq> j \<longrightarrow> cols (submatrix A I UNIV) ! i \<noteq> cols (submatrix A I UNIV) ! j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> distinct (cols (submatrix A I UNIV))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cols_submatrix_subset: "set (cols (submatrix A UNIV J)) \<subseteq> set (cols A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (cols (submatrix A UNIV J)) \<subseteq> set (cols A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (cols (submatrix A UNIV J)) \<Longrightarrow> x \<in> set (cols A)
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (cols (submatrix A UNIV J)) \<Longrightarrow> x \<in> set (cols A)
[PROOF STEP]
assume "c \<in> set (cols (submatrix A UNIV J))"
[PROOF STATE]
proof (state)
this:
c \<in> set (cols (submatrix A UNIV J))

goal (1 subgoal):
 1. \<And>x. x \<in> set (cols (submatrix A UNIV J)) \<Longrightarrow> x \<in> set (cols A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> set (cols (submatrix A UNIV J))
[PROOF STEP]
obtain j where "j < length (cols (submatrix A UNIV J))" "cols (submatrix A UNIV J) ! j = c"
[PROOF STATE]
proof (prove)
using this:
c \<in> set (cols (submatrix A UNIV J))

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j < length (cols (submatrix A UNIV J)); cols (submatrix A UNIV J) ! j = c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson in_set_conv_nth)
[PROOF STATE]
proof (state)
this:
j < length (cols (submatrix A UNIV J))
cols (submatrix A UNIV J) ! j = c

goal (1 subgoal):
 1. \<And>x. x \<in> set (cols (submatrix A UNIV J)) \<Longrightarrow> x \<in> set (cols A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < length (cols (submatrix A UNIV J))
cols (submatrix A UNIV J) ! j = c
[PROOF STEP]
have "j < dim_col (submatrix A UNIV J)"
[PROOF STATE]
proof (prove)
using this:
j < length (cols (submatrix A UNIV J))
cols (submatrix A UNIV J) ! j = c

goal (1 subgoal):
 1. j < dim_col (submatrix A UNIV J)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j < dim_col (submatrix A UNIV J)

goal (1 subgoal):
 1. \<And>x. x \<in> set (cols (submatrix A UNIV J)) \<Longrightarrow> x \<in> set (cols A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < dim_col (submatrix A UNIV J)
[PROOF STEP]
have "j < card {j. j < dim_col A \<and> j \<in> J}"
[PROOF STATE]
proof (prove)
using this:
j < dim_col (submatrix A UNIV J)

goal (1 subgoal):
 1. j < card {j. j < dim_col A \<and> j \<in> J}
[PROOF STEP]
by (simp add: dim_submatrix(2))
[PROOF STATE]
proof (state)
this:
j < card {j. j < dim_col A \<and> j \<in> J}

goal (1 subgoal):
 1. \<And>x. x \<in> set (cols (submatrix A UNIV J)) \<Longrightarrow> x \<in> set (cols A)
[PROOF STEP]
have "cols (submatrix A UNIV J) ! j = cols A ! (pick J j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cols (submatrix A UNIV J) ! j = cols A ! pick J j
[PROOF STEP]
unfolding cols_nth[OF \<open>j < dim_col (submatrix A UNIV J)\<close>] cols_nth[OF pick_le[OF \<open>j < card {j. j < dim_col A \<and> j \<in> J}\<close>]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (submatrix A UNIV J) j = col A (pick J j)
[PROOF STEP]
proof (rule eq_vecI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (col A (pick J j)) \<Longrightarrow> col (submatrix A UNIV J) j $ i = col A (pick J j) $ i
 2. dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))
[PROOF STEP]
show "dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))
[PROOF STEP]
unfolding dim_col dim_submatrix
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i < dim_row A \<and> i \<in> UNIV} = dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (col A (pick J j)) \<Longrightarrow> col (submatrix A UNIV J) j $ i = col A (pick J j) $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (col A (pick J j)) \<Longrightarrow> col (submatrix A UNIV J) j $ i = col A (pick J j) $ i
[PROOF STEP]
assume "i < dim_vec (col A (pick J j))"
[PROOF STATE]
proof (state)
this:
i < dim_vec (col A (pick J j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (col A (pick J j)) \<Longrightarrow> col (submatrix A UNIV J) j $ i = col A (pick J j) $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_vec (col A (pick J j))
[PROOF STEP]
have "i < dim_row A"
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (col A (pick J j))

goal (1 subgoal):
 1. i < dim_row A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < dim_row A

goal (1 subgoal):
 1. \<And>i. i < dim_vec (col A (pick J j)) \<Longrightarrow> col (submatrix A UNIV J) j $ i = col A (pick J j) $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_row A
[PROOF STEP]
have "i < dim_row (submatrix A UNIV J)"
[PROOF STATE]
proof (prove)
using this:
i < dim_row A

goal (1 subgoal):
 1. i < dim_row (submatrix A UNIV J)
[PROOF STEP]
using \<open>dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))\<close>
[PROOF STATE]
proof (prove)
using this:
i < dim_row A
dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))

goal (1 subgoal):
 1. i < dim_row (submatrix A UNIV J)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < dim_row (submatrix A UNIV J)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (col A (pick J j)) \<Longrightarrow> col (submatrix A UNIV J) j $ i = col A (pick J j) $ i
[PROOF STEP]
show "col (submatrix A UNIV J) j $ i = col A (pick J j) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (submatrix A UNIV J) j $ i = col A (pick J j) $ i
[PROOF STEP]
unfolding col_def index_vec[OF \<open>i < dim_row (submatrix A UNIV J)\<close>] index_vec[OF \<open>i < dim_row A\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A UNIV J $$ (i, j) = A $$ (i, pick J j)
[PROOF STEP]
using submatrix_index
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < card {i. i < dim_row ?A \<and> i \<in> ?I}; ?j < card {j. j < dim_col ?A \<and> j \<in> ?J}\<rbrakk> \<Longrightarrow> submatrix ?A ?I ?J $$ (?i, ?j) = ?A $$ (pick ?I ?i, pick ?J ?j)

goal (1 subgoal):
 1. submatrix A UNIV J $$ (i, j) = A $$ (i, pick J j)
[PROOF STEP]
by (metis (no_types, lifting) \<open>dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))\<close>
      \<open>i < dim_vec (col A (pick J j))\<close> \<open>j < dim_col (submatrix A UNIV J)\<close> dim_col dim_submatrix(1) dim_submatrix(2) pick_UNIV)
[PROOF STATE]
proof (state)
this:
col (submatrix A UNIV J) j $ i = col A (pick J j) $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cols (submatrix A UNIV J) ! j = cols A ! pick J j

goal (1 subgoal):
 1. \<And>x. x \<in> set (cols (submatrix A UNIV J)) \<Longrightarrow> x \<in> set (cols A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cols (submatrix A UNIV J) ! j = cols A ! pick J j
[PROOF STEP]
show "c \<in> set (cols A)"
[PROOF STATE]
proof (prove)
using this:
cols (submatrix A UNIV J) ! j = cols A ! pick J j

goal (1 subgoal):
 1. c \<in> set (cols A)
[PROOF STEP]
using \<open>cols (submatrix A UNIV J) ! j = c\<close>
[PROOF STATE]
proof (prove)
using this:
cols (submatrix A UNIV J) ! j = cols A ! pick J j
cols (submatrix A UNIV J) ! j = c

goal (1 subgoal):
 1. c \<in> set (cols A)
[PROOF STEP]
using pick_le[OF \<open>j < card {j. j < dim_col A \<and> j \<in> J}\<close>]
[PROOF STATE]
proof (prove)
using this:
cols (submatrix A UNIV J) ! j = cols A ! pick J j
cols (submatrix A UNIV J) ! j = c
pick J j < dim_col A

goal (1 subgoal):
 1. c \<in> set (cols A)
[PROOF STEP]
by (metis cols_length nth_mem)
[PROOF STATE]
proof (state)
this:
c \<in> set (cols A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vec_space) lin_dep_submatrix_UNIV:
assumes "A \<in> carrier_mat n nc"
assumes "lin_dep (set (cols A))"
assumes "distinct (cols (submatrix A I UNIV))"
shows "LinearCombinations.module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))"
  (is "LinearCombinations.module.lin_dep class_ring ?M (set ?S')")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
obtain v where 2:"v \<in> carrier_vec nc" and 3:"v \<noteq> 0\<^sub>v nc" and "A *\<^sub>v v = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> carrier_vec nc; v \<noteq> 0\<^sub>v nc; A *\<^sub>v v = 0\<^sub>v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vec_space.lin_depE[OF assms(1) assms(2) distinct_cols_submatrix_UNIV[OF assms(3)]]
[PROOF STATE]
proof (prove)
using this:
(\<And>v. \<lbrakk>v \<in> carrier_vec nc; v \<noteq> 0\<^sub>v nc; A *\<^sub>v v = 0\<^sub>v n\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> carrier_vec nc; v \<noteq> 0\<^sub>v nc; A *\<^sub>v v = 0\<^sub>v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec nc
v \<noteq> 0\<^sub>v nc
A *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
have 1: "submatrix A I UNIV \<in> carrier_mat (card {i. i < n \<and> i \<in> I}) nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A I UNIV \<in> carrier_mat (card {i. i < n \<and> i \<in> I}) nc
[PROOF STEP]
apply (rule carrier_matI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dim_row (submatrix A I UNIV) = card {i. i < n \<and> i \<in> I}
 2. dim_col (submatrix A I UNIV) = nc
[PROOF STEP]
unfolding dim_submatrix
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card {i. i < dim_row A \<and> i \<in> I} = card {i. i < n \<and> i \<in> I}
 2. card {j. j < dim_col A \<and> j \<in> UNIV} = nc
[PROOF STEP]
using \<open>A \<in> carrier_mat n nc\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n nc

goal (2 subgoals):
 1. card {i. i < dim_row A \<and> i \<in> I} = card {i. i < n \<and> i \<in> I}
 2. card {j. j < dim_col A \<and> j \<in> UNIV} = nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
submatrix A I UNIV \<in> carrier_mat (card {i. i < n \<and> i \<in> I}) nc

goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
have 4:"submatrix A I UNIV *\<^sub>v v = 0\<^sub>v (card {i. i < n \<and> i \<in> I})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A I UNIV *\<^sub>v v = 0\<^sub>v (card {i. i < n \<and> i \<in> I})
[PROOF STEP]
proof (rule eq_vecI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
 2. dim_vec (submatrix A I UNIV *\<^sub>v v) = dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))
[PROOF STEP]
show dim_eq:"dim_vec (submatrix A I UNIV *\<^sub>v v) = dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (submatrix A I UNIV *\<^sub>v v) = dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))
[PROOF STEP]
using "1"
[PROOF STATE]
proof (prove)
using this:
submatrix A I UNIV \<in> carrier_mat (card {i. i < n \<and> i \<in> I}) nc

goal (1 subgoal):
 1. dim_vec (submatrix A I UNIV *\<^sub>v v) = dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (submatrix A I UNIV *\<^sub>v v) = dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
assume "i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))"
[PROOF STATE]
proof (state)
this:
i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))
[PROOF STEP]
have i_le:"i < card {i. i < n \<and> i \<in> I}"
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))

goal (1 subgoal):
 1. i < card {i. i < n \<and> i \<in> I}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < card {i. i < n \<and> i \<in> I}

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
have "(submatrix A I UNIV *\<^sub>v v) $ i = row (submatrix A I UNIV) i \<bullet> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (submatrix A I UNIV *\<^sub>v v) $ i = row (submatrix A I UNIV) i \<bullet> v
[PROOF STEP]
using dim_eq i_le
[PROOF STATE]
proof (prove)
using this:
dim_vec (submatrix A I UNIV *\<^sub>v v) = dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))
i < card {i. i < n \<and> i \<in> I}

goal (1 subgoal):
 1. (submatrix A I UNIV *\<^sub>v v) $ i = row (submatrix A I UNIV) i \<bullet> v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(submatrix A I UNIV *\<^sub>v v) $ i = row (submatrix A I UNIV) i \<bullet> v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(submatrix A I UNIV *\<^sub>v v) $ i = row (submatrix A I UNIV) i \<bullet> v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
have "... = row A (pick I i) \<bullet> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (submatrix A I UNIV) i \<bullet> v = row A (pick I i) \<bullet> v
[PROOF STEP]
using row_submatrix_UNIV
[PROOF STATE]
proof (prove)
using this:
?i < card {i. i < dim_row ?A \<and> i \<in> ?I} \<Longrightarrow> row (submatrix ?A ?I UNIV) ?i = row ?A (pick ?I ?i)

goal (1 subgoal):
 1. row (submatrix A I UNIV) i \<bullet> v = row A (pick I i) \<bullet> v
[PROOF STEP]
by (metis (no_types, lifting)  dim_eq dim_mult_mat_vec dim_submatrix(1) \<open>i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I}))\<close>)
[PROOF STATE]
proof (state)
this:
row (submatrix A I UNIV) i \<bullet> v = row A (pick I i) \<bullet> v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row (submatrix A I UNIV) i \<bullet> v = row A (pick I i) \<bullet> v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A (pick I i) \<bullet> v = (0::'a)
[PROOF STEP]
using \<open>A *\<^sub>v v = 0\<^sub>v n\<close> i_le[THEN pick_le]
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v v = 0\<^sub>v n
pick I i < n

goal (1 subgoal):
 1. row A (pick I i) \<bullet> v = (0::'a)
[PROOF STEP]
by (metis assms(1) index_mult_mat_vec carrier_matD(1) index_zero_vec(1))
[PROOF STATE]
proof (state)
this:
row A (pick I i) \<bullet> v = (0::'a)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row A (pick I i) \<bullet> v = (0::'a)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
have "... = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
by (simp add: i_le)
[PROOF STATE]
proof (state)
this:
(0::'a) = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i

goal (1 subgoal):
 1. \<And>i. i < dim_vec (0\<^sub>v (card {i. i < n \<and> i \<in> I})) \<Longrightarrow> (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
show "(submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i"
[PROOF STATE]
proof (prove)
using this:
(submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i

goal (1 subgoal):
 1. (submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(submatrix A I UNIV *\<^sub>v v) $ i = 0\<^sub>v (card {i. i < n \<and> i \<in> I}) $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
submatrix A I UNIV *\<^sub>v v = 0\<^sub>v (card {i. i < n \<and> i \<in> I})

goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
using vec_space.lin_depI[OF 1 2 3 4]
[PROOF STATE]
proof (prove)
using this:
distinct (cols (submatrix A I UNIV)) \<Longrightarrow> module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))

goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
distinct (cols (submatrix A I UNIV)) \<Longrightarrow> module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
distinct (cols (submatrix A I UNIV))

goal (1 subgoal):
 1. module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix A I UNIV)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vec_space) rank_gt_minor:
assumes "A \<in> carrier_mat n nc"
assumes "det (submatrix A I J) \<noteq> 0"
shows "card {j. j < nc \<and> j \<in> J} \<le> rank A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
have square:"dim_row (submatrix A I J) = dim_col (submatrix A I J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (submatrix A I J) = dim_col (submatrix A I J)
[PROOF STEP]
using det_def \<open>det (submatrix A I J) \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
det ?A = (if dim_row ?A = dim_col ?A then \<Sum>p | p permutes {0..<dim_row ?A}. of_int (sign p) * (\<Prod>i = 0..<dim_row ?A. ?A $$ (i, p i)) else (0::?'a))
det (submatrix A I J) \<noteq> (0::'a)

goal (1 subgoal):
 1. dim_row (submatrix A I J) = dim_col (submatrix A I J)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dim_row (submatrix A I J) = dim_col (submatrix A I J)

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dim_row (submatrix A I J) = dim_col (submatrix A I J)
[PROOF STEP]
have full_rank:"vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)"
[PROOF STATE]
proof (prove)
using this:
dim_row (submatrix A I J) = dim_col (submatrix A I J)

goal (1 subgoal):
 1. vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)
[PROOF STEP]
using vec_space.low_rank_det_zero assms(2) carrier_matI
[PROOF STATE]
proof (prove)
using this:
dim_row (submatrix A I J) = dim_col (submatrix A I J)
\<lbrakk>?A \<in> carrier_mat ?n ?n; det ?A \<noteq> (0::?'a)\<rbrakk> \<Longrightarrow> vec_space.rank ?n ?A = ?n
det (submatrix A I J) \<noteq> (0::'a)
\<lbrakk>dim_row ?A = ?nr; dim_col ?A = ?nc\<rbrakk> \<Longrightarrow> ?A \<in> carrier_mat ?nr ?nc

goal (1 subgoal):
 1. vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)
[PROOF STEP]
have distinct:"distinct (cols (submatrix A I J))"
[PROOF STATE]
proof (prove)
using this:
vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)

goal (1 subgoal):
 1. distinct (cols (submatrix A I J))
[PROOF STEP]
using vec_space.non_distinct_low_rank square less_irrefl carrier_matI
[PROOF STATE]
proof (prove)
using this:
vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)
\<lbrakk>?A \<in> carrier_mat ?n ?n; \<not> distinct (cols ?A)\<rbrakk> \<Longrightarrow> vec_space.rank ?n ?A < ?n
dim_row (submatrix A I J) = dim_col (submatrix A I J)
\<not> ?x < ?x
\<lbrakk>dim_row ?A = ?nr; dim_col ?A = ?nc\<rbrakk> \<Longrightarrow> ?A \<in> carrier_mat ?nr ?nc

goal (1 subgoal):
 1. distinct (cols (submatrix A I J))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distinct (cols (submatrix A I J))

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (cols (submatrix A I J))
[PROOF STEP]
have indpt:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))"
[PROOF STATE]
proof (prove)
using this:
distinct (cols (submatrix A I J))

goal (1 subgoal):
 1. \<not> module.lin_dep class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))
[PROOF STEP]
using vec_space.full_rank_lin_indpt[OF _ full_rank distinct] square
[PROOF STATE]
proof (prove)
using this:
distinct (cols (submatrix A I J))
submatrix A I J \<in> carrier_mat (dim_row (submatrix A I J)) (dim_row (submatrix A I J)) \<Longrightarrow> \<not> module.lin_dep class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))
dim_row (submatrix A I J) = dim_col (submatrix A I J)

goal (1 subgoal):
 1. \<not> module.lin_dep class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> module.lin_dep class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
have distinct2: "distinct (cols (submatrix (submatrix A UNIV J) I UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (cols (submatrix (submatrix A UNIV J) I UNIV))
[PROOF STEP]
using submatrix_split distinct
[PROOF STATE]
proof (prove)
using this:
submatrix ?A ?I ?J = submatrix (submatrix ?A UNIV ?J) ?I UNIV
distinct (cols (submatrix A I J))

goal (1 subgoal):
 1. distinct (cols (submatrix (submatrix A UNIV J) I UNIV))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distinct (cols (submatrix (submatrix A UNIV J) I UNIV))

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
have indpt2:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))
[PROOF STEP]
using submatrix_split dim_submatrix(1) indpt
[PROOF STATE]
proof (prove)
using this:
submatrix ?A ?I ?J = submatrix (submatrix ?A UNIV ?J) ?I UNIV
dim_row (submatrix ?A ?I ?J) = card {i. i < dim_row ?A \<and> i \<in> ?I}
\<not> module.lin_dep class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))

goal (1 subgoal):
 1. \<not> module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))
[PROOF STEP]
by (metis (full_types) assms(1) carrier_matD(1))
[PROOF STATE]
proof (state)
this:
\<not> module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
have "submatrix A UNIV J \<in> carrier_mat n (dim_col (submatrix A UNIV J))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A UNIV J \<in> carrier_mat n (dim_col (submatrix A UNIV J))
[PROOF STEP]
apply (rule carrier_matI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dim_row (submatrix A UNIV J) = n
 2. dim_col (submatrix A UNIV J) = dim_col (submatrix A UNIV J)
[PROOF STEP]
unfolding dim_submatrix(1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card {i. i < dim_row A \<and> i \<in> UNIV} = n
 2. dim_col (submatrix A UNIV J) = dim_col (submatrix A UNIV J)
[PROOF STEP]
using \<open>A \<in> carrier_mat n nc\<close> carrier_matD
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n nc
?A \<in> carrier_mat ?nr ?nc \<Longrightarrow> dim_row ?A = ?nr
?A \<in> carrier_mat ?nr ?nc \<Longrightarrow> dim_col ?A = ?nc

goal (2 subgoals):
 1. card {i. i < dim_row A \<and> i \<in> UNIV} = n
 2. dim_col (submatrix A UNIV J) = dim_col (submatrix A UNIV J)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
submatrix A UNIV J \<in> carrier_mat n (dim_col (submatrix A UNIV J))

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
have "lin_indpt (set (cols (submatrix A UNIV J)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (set (cols (submatrix A UNIV J)))
[PROOF STEP]
using indpt2 vec_space.lin_dep_submatrix_UNIV[OF \<open>submatrix A UNIV J \<in> carrier_mat n (dim_col (submatrix A UNIV J))\<close> _ distinct2]
[PROOF STATE]
proof (prove)
using this:
\<not> module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))
lin_dep (set (cols (submatrix A UNIV J))) \<Longrightarrow> module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n \<and> i \<in> I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))

goal (1 subgoal):
 1. lin_indpt (set (cols (submatrix A UNIV J)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lin_indpt (set (cols (submatrix A UNIV J)))

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
have distinct3:"distinct (cols (submatrix A UNIV J))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (cols (submatrix A UNIV J))
[PROOF STEP]
by (metis distinct distinct_cols_submatrix_UNIV submatrix_split)
[PROOF STATE]
proof (state)
this:
distinct (cols (submatrix A UNIV J))

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
using
    rank_ge_card_indpt[OF \<open>A \<in> carrier_mat n nc\<close> cols_submatrix_subset \<open>lin_indpt (set (cols (submatrix A UNIV J)))\<close>,
    unfolded distinct_card[OF distinct3, unfolded cols_length dim_submatrix], unfolded carrier_matD(2)[OF \<open>A \<in> carrier_mat n nc\<close>]]
[PROOF STATE]
proof (prove)
using this:
card {j. j < nc \<and> j \<in> J} \<le> rank A

goal (1 subgoal):
 1. card {j. j < nc \<and> j \<in> J} \<le> rank A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card {j. j < nc \<and> j \<in> J} \<le> rank A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ProcUniv: "(UNIV :: proc set) = {p0, p1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = {p0, p1}
[PROOF STEP]
by (metis UNIV_eq_I insert_iff proc.exhaust)


[STATEMENT]
lemma tensor_prod_2 [simp]:
"mult.vec_vec_Tensor (*) [x1::complex,x2] [x3, x4] = [x1 * x3, x1 * x4, x2 * x3, x2 * x4]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult.vec_vec_Tensor (*) [x1, x2] [x3, x4] = [x1 * x3, x1 * x4, x2 * x3, x2 * x4]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult.vec_vec_Tensor (*) [x1, x2] [x3, x4] = [x1 * x3, x1 * x4, x2 * x3, x2 * x4]
[PROOF STEP]
have "Matrix_Tensor.mult (1::complex) (*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Tensor.mult 1 (*)
[PROOF STEP]
by (simp add: Matrix_Tensor.mult_def)
[PROOF STATE]
proof (state)
this:
Matrix_Tensor.mult 1 (*)

goal (1 subgoal):
 1. mult.vec_vec_Tensor (*) [x1, x2] [x3, x4] = [x1 * x3, x1 * x4, x2 * x3, x2 * x4]
[PROOF STEP]
thus "mult.vec_vec_Tensor (*) [x1::complex,x2] [x3,x4] = [x1*x3,x1*x4,x2*x3,x2*x4]"
[PROOF STATE]
proof (prove)
using this:
Matrix_Tensor.mult 1 (*)

goal (1 subgoal):
 1. mult.vec_vec_Tensor (*) [x1, x2] [x3, x4] = [x1 * x3, x1 * x4, x2 * x3, x2 * x4]
[PROOF STEP]
using mult.vec_vec_Tensor_def[of "(1::complex)" "(*)"] mult.times_def[of "(1::complex)" "(*)"]
[PROOF STATE]
proof (prove)
using this:
Matrix_Tensor.mult 1 (*)
Matrix_Tensor.mult 1 (*) \<Longrightarrow> mult.vec_vec_Tensor (*) \<equiv> rec_list (\<lambda>ys. []) (\<lambda>x xs xsa ys. mult.times (*) x ys @ xsa ys)
Matrix_Tensor.mult 1 (*) \<Longrightarrow> mult.times (*) \<equiv> \<lambda>uu uua. rec_list (\<lambda>n. []) (\<lambda>y ys ysa n. n * y # ysa n) uua uu

goal (1 subgoal):
 1. mult.vec_vec_Tensor (*) [x1, x2] [x3, x4] = [x1 * x3, x1 * x4, x2 * x3, x2 * x4]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mult.vec_vec_Tensor (*) [x1, x2] [x3, x4] = [x1 * x3, x1 * x4, x2 * x3, x2 * x4]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_vec [simp]:
  assumes "v \<in> state_qbit 1"
  shows "list_of_vec v = [v $ 0, v $ 1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
have "Rep_vec v = (fst(Rep_vec v), snd(Rep_vec v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_vec v = (fst (Rep_vec v), snd (Rep_vec v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rep_vec v = (fst (Rep_vec v), snd (Rep_vec v))

goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_vec v = (fst (Rep_vec v), snd (Rep_vec v))

goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
have "\<dots> = (2, vec_index v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (Rep_vec v), snd (Rep_vec v)) = (2, ($) v)
[PROOF STEP]
by (metis (mono_tags, lifting) assms dim_vec.rep_eq mem_Collect_eq power_one_right state_qbit_def vec_index.rep_eq)
[PROOF STATE]
proof (state)
this:
(fst (Rep_vec v), snd (Rep_vec v)) = (2, ($) v)

goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(fst (Rep_vec v), snd (Rep_vec v)) = (2, ($) v)

goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
have "[0..<2::nat] = [0,1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<2] = [0, 1]
[PROOF STEP]
by(simp add: upt_rec)
[PROOF STATE]
proof (state)
this:
[0..<2] = [0, 1]

goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Rep_vec v = (fst (Rep_vec v), snd (Rep_vec v))
(fst (Rep_vec v), snd (Rep_vec v)) = (2, ($) v)
[0..<2] = [0, 1]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_vec v = (fst (Rep_vec v), snd (Rep_vec v))
(fst (Rep_vec v), snd (Rep_vec v)) = (2, ($) v)
[0..<2] = [0, 1]

goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
by(simp add: list_of_vec_def)
[PROOF STATE]
proof (state)
this:
list_of_vec v = [v $ 0, v $ 1]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_tensor_prod_2 [simp]:
  assumes "v \<in> state_qbit 1" and "w \<in> state_qbit 1"
  shows "v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]
[PROOF STEP]
have "list_of_vec v = [v $ 0, v $ 1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> state_qbit 1
w \<in> state_qbit 1

goal (1 subgoal):
 1. list_of_vec v = [v $ 0, v $ 1]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_of_vec v = [v $ 0, v $ 1]

goal (1 subgoal):
 1. v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_of_vec v = [v $ 0, v $ 1]

goal (1 subgoal):
 1. v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]
[PROOF STEP]
have "list_of_vec w = [w $ 0, w $ 1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_vec w = [w $ 0, w $ 1]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> state_qbit 1
w \<in> state_qbit 1

goal (1 subgoal):
 1. list_of_vec w = [w $ 0, w $ 1]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_of_vec w = [w $ 0, w $ 1]

goal (1 subgoal):
 1. v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list_of_vec v = [v $ 0, v $ 1]
list_of_vec w = [w $ 0, w $ 1]
[PROOF STEP]
show "v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]"
[PROOF STATE]
proof (prove)
using this:
list_of_vec v = [v $ 0, v $ 1]
list_of_vec w = [w $ 0, w $ 1]

goal (1 subgoal):
 1. v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]
[PROOF STEP]
by(simp add: tensor_vec_def)
[PROOF STATE]
proof (state)
this:
v \<otimes> w = vec_of_list [v $ 0 * w $ 0, v $ 0 * w $ 1, v $ 1 * w $ 0, v $ 1 * w $ 1]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_dim_of_vec_of_list [simp]:
  assumes "length l = n"
  shows "dim_vec (vec_of_list l) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_list l) = n
[PROOF STEP]
using assms vec_of_list_def
[PROOF STATE]
proof (prove)
using this:
length l = n
vec_of_list \<equiv> map_fun id Abs_vec (\<lambda>v. (length v, mk_vec (length v) ((!) v)))

goal (1 subgoal):
 1. dim_vec (vec_of_list l) = n
[PROOF STEP]
by simp


[STATEMENT]
lemma index_col_mat_of_cols_list [simp]:
  assumes "i < n" and "j < length l"
  shows "Matrix.col (mat_of_cols_list n l) j $ i = l ! j ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.col (Tensor.mat_of_cols_list n l) j $ i = l ! j ! i
[PROOF STEP]
apply (auto simp: Matrix.col_def mat_of_cols_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.vec n (\<lambda>i. Matrix.mat n (length l) (\<lambda>(i, j). l ! j ! i) $$ (i, j)) $ i = l ! j ! i
[PROOF STEP]
using assms less_le_trans
[PROOF STATE]
proof (prove)
using this:
i < n
j < length l
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. Matrix.vec n (\<lambda>i. Matrix.mat n (length l) (\<lambda>(i, j). l ! j ! i) $$ (i, j)) $ i = l ! j ! i
[PROOF STEP]
by fastforce


[STATEMENT]
lemma multTensor2 [simp]:
  assumes a1:"A = Matrix.mat 2 1 (\<lambda>(i,j). if i = 0 then a0 else a1)" and
          a2:"B = Matrix.mat 2 1 (\<lambda>(i,j). if i = 0 then b0 else b1)"
  shows "mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0*b0, a0*b1, a1*b0, a1*b1]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
have "mat_to_cols_list A = [[a0, a1]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list A = [[a0, a1]]
[PROOF STEP]
by (auto simp: a1 mat_to_cols_list_def) (simp add: numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list A = [[a0, a1]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat_to_cols_list A = [[a0, a1]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
have f2:"mat_to_cols_list B = [[b0, b1]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list B = [[b0, b1]]
[PROOF STEP]
by (auto simp: a2 mat_to_cols_list_def) (simp add: numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list B = [[b0, b1]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat_to_cols_list A = [[a0, a1]]
mat_to_cols_list B = [[b0, b1]]
[PROOF STEP]
have "mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) =
                   mult.Tensor (*) [[a0,a1]] [[b0,b1]]"
[PROOF STATE]
proof (prove)
using this:
mat_to_cols_list A = [[a0, a1]]
mat_to_cols_list B = [[b0, b1]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[a0, a1]] [[b0, b1]]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[a0, a1]] [[b0, b1]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[a0, a1]] [[b0, b1]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
using mult.Tensor_def[of "(1::complex)" "(*)"] mult.times_def[of "(1::complex)" "(*)"]
[PROOF STATE]
proof (prove)
using this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[a0, a1]] [[b0, b1]]
Matrix_Tensor.mult 1 (*) \<Longrightarrow> mult.Tensor (*) \<equiv> rec_list (\<lambda>xs. []) (\<lambda>x xs xsa ys. mult.vec_mat_Tensor (*) x ys @ xsa ys)
Matrix_Tensor.mult 1 (*) \<Longrightarrow> mult.times (*) \<equiv> \<lambda>uu uua. rec_list (\<lambda>n. []) (\<lambda>y ys ysa n. n * y # ysa n) uua uu

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]
[PROOF STEP]
by (metis (mono_tags, lifting) append_self_conv list.simps(6) mult.Tensor.simps(2) mult.vec_mat_Tensor.simps(1)
mult.vec_mat_Tensor.simps(2) plus_mult_cpx plus_mult_def tensor_prod_2)
[PROOF STATE]
proof (state)
this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[a0 * b0, a0 * b1, a1 * b0, a1 * b1]]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multTensor2_bis [simp]:
  assumes a1:"dim_row A = 2" and a2:"dim_col A = 1" and a3:"dim_row B = 2" and a4:"dim_col B = 1"
  shows "mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) =
[[A $$ (0,0) * B $$ (0,0), A $$ (0,0) *  B $$ (1,0), A $$ (1,0) * B $$ (0,0), A $$ (1,0) * B $$ (1,0)]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
have "mat_to_cols_list A = [[A $$ (0,0), A $$ (1,0)]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list A = [[A $$ (0, 0), A $$ (1, 0)]]
[PROOF STEP]
by (auto simp: a1 a2 mat_to_cols_list_def) (simp add: numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list A = [[A $$ (0, 0), A $$ (1, 0)]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat_to_cols_list A = [[A $$ (0, 0), A $$ (1, 0)]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
have f2:"mat_to_cols_list B = [[B $$ (0,0), B $$ (1,0)]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list B = [[B $$ (0, 0), B $$ (1, 0)]]
[PROOF STEP]
by (auto simp: a3 a4 mat_to_cols_list_def) (simp add: numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list B = [[B $$ (0, 0), B $$ (1, 0)]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat_to_cols_list A = [[A $$ (0, 0), A $$ (1, 0)]]
mat_to_cols_list B = [[B $$ (0, 0), B $$ (1, 0)]]
[PROOF STEP]
have "mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) =
                   mult.Tensor (*) [[A $$ (0,0), A $$ (1,0)]] [[B $$ (0,0), B $$ (1,0)]]"
[PROOF STATE]
proof (prove)
using this:
mat_to_cols_list A = [[A $$ (0, 0), A $$ (1, 0)]]
mat_to_cols_list B = [[B $$ (0, 0), B $$ (1, 0)]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[A $$ (0, 0), A $$ (1, 0)]] [[B $$ (0, 0), B $$ (1, 0)]]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[A $$ (0, 0), A $$ (1, 0)]] [[B $$ (0, 0), B $$ (1, 0)]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[A $$ (0, 0), A $$ (1, 0)]] [[B $$ (0, 0), B $$ (1, 0)]]

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
using mult.Tensor_def[of "(1::complex)" "(*)"] mult.times_def[of "(1::complex)" "(*)"]
[PROOF STATE]
proof (prove)
using this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = mult.Tensor (*) [[A $$ (0, 0), A $$ (1, 0)]] [[B $$ (0, 0), B $$ (1, 0)]]
Matrix_Tensor.mult 1 (*) \<Longrightarrow> mult.Tensor (*) \<equiv> rec_list (\<lambda>xs. []) (\<lambda>x xs xsa ys. mult.vec_mat_Tensor (*) x ys @ xsa ys)
Matrix_Tensor.mult 1 (*) \<Longrightarrow> mult.times (*) \<equiv> \<lambda>uu uua. rec_list (\<lambda>n. []) (\<lambda>y ys ysa n. n * y # ysa n) uua uu

goal (1 subgoal):
 1. mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]
[PROOF STEP]
by (smt append_self_conv list.simps(6) mult.Tensor.simps(2) mult.vec_mat_Tensor.simps(1)
mult.vec_mat_Tensor.simps(2) plus_mult_cpx plus_mult_def tensor_prod_2)
[PROOF STATE]
proof (state)
this:
mult.Tensor (*) (mat_to_cols_list A) (mat_to_cols_list B) = [[A $$ (0, 0) * B $$ (0, 0), A $$ (0, 0) * B $$ (1, 0), A $$ (1, 0) * B $$ (0, 0), A $$ (1, 0) * B $$ (1, 0)]]

goal:
No subgoals!
[PROOF STEP]
qed