[STATEMENT]
lemma "doE x \<leftarrow> returnOk 1;
           returnOk (2::nat);
           returnOk x
       odE =
       returnOk 1 >>=E
       (\<lambda>x. returnOk (2::nat) >>=E
            K_bind (returnOk x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doE x \<leftarrow> returnOk (1::'c);
returnOk 2;
returnOk x
odE = doE x \<leftarrow> returnOk (1::'c);
returnOk 2;
returnOk x
odE
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma "doE x \<leftarrow> returnOk 1;
           returnOk 2;
           returnOk x
       odE = returnOk 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doE x \<leftarrow> returnOk (1::'c);
returnOk (2::'d);
returnOk x
odE = returnOk (1::'c)
[PROOF STEP]
by simp


[STATEMENT]
lemma validE_NF_alt_def:
  "\<lbrace> P \<rbrace> B \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! = \<lbrace> P \<rbrace> B \<lbrace> \<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s \<rbrace>!"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> B \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! = \<lbrace>P\<rbrace> B \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>!
[PROOF STEP]
by (clarsimp simp: validE_NF_def validE_def validNF_def)


[STATEMENT]
lemma ereal_Inf_finite_Min:
  fixes S :: "ereal set"
  assumes "finite S" and "S \<noteq> {}"
  shows "Inf S = Min S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf S = Min S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
S \<noteq> {}

goal (1 subgoal):
 1. Inf S = Min S
[PROOF STEP]
by (induct S rule: finite_ne_induct) (auto simp: min_absorb1)


[STATEMENT]
lemma finite_INF_in:
  fixes f :: "'a \<Rightarrow> ereal"
  assumes "finite S"
  assumes "S \<noteq> {}"
  shows "(INF s\<in> S. f s) \<in> f ` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf (f ` S) \<in> f ` S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Inf (f ` S) \<in> f ` S
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite S
S \<noteq> {}
[PROOF STEP]
have "finite (f ` S)" "f ` S \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
finite S
S \<noteq> {}

goal (1 subgoal):
 1. finite (f ` S) &&& f ` S \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (f ` S)
f ` S \<noteq> {}

goal (1 subgoal):
 1. Inf (f ` S) \<in> f ` S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (f ` S)
f ` S \<noteq> {}
[PROOF STEP]
show "Inf (f ` S) \<in> f ` S"
[PROOF STATE]
proof (prove)
using this:
finite (f ` S)
f ` S \<noteq> {}

goal (1 subgoal):
 1. Inf (f ` S) \<in> f ` S
[PROOF STEP]
using ereal_Inf_finite_Min [of "f ` S"]
[PROOF STATE]
proof (prove)
using this:
finite (f ` S)
f ` S \<noteq> {}
\<lbrakk>finite (f ` S); f ` S \<noteq> {}\<rbrakk> \<Longrightarrow> Inf (f ` S) = Min (f ` S)

goal (1 subgoal):
 1. Inf (f ` S) \<in> f ` S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Inf (f ` S) \<in> f ` S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_mem_less_INF:
  fixes f :: "'a \<Rightarrow> 'b :: complete_lattice"
  assumes "f x < (INF s\<in> S. f s)"
  assumes "x \<in> S"
  shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f x < Inf (f ` S)
x \<in> S

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis INF_lower less_le_not_le)


[STATEMENT]
lemma sym_diff:
  assumes "sym A" "sym B" shows "sym (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (A - B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sym A
sym B

goal (1 subgoal):
 1. sym (A - B)
[PROOF STEP]
by (auto simp: sym_def)


[STATEMENT]
lemma list_exhaust_NSC:
  obtains (Nil) "xs = []" | (Single) x where "xs = [x]" | (Cons_Cons) x y ys where "xs = x # y # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x. xs = [x] \<Longrightarrow> thesis; \<And>x y ys. xs = x # y # ys \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis list.exhaust)


[STATEMENT]
lemma tl_rev:
  "tl (rev p) = rev (butlast p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (rev p) = rev (butlast p)
[PROOF STEP]
by (induct p) auto


[STATEMENT]
lemma butlast_rev:
  "butlast (rev p) = rev (tl p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast (rev p) = rev (tl p)
[PROOF STEP]
by (induct p) auto


[STATEMENT]
lemma take_drop_take:
   "take n xs @ drop n (take m xs) = take (max n m) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
 2. \<not> ?P \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
assume "m < n"
[PROOF STATE]
proof (state)
this:
m < n

goal (2 subgoals):
 1. ?P \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
 2. \<not> ?P \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
by (auto simp: max_def)
[PROOF STATE]
proof (state)
this:
take n xs @ drop n (take m xs) = take (max n m) xs

goal (1 subgoal):
 1. \<not> m < n \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> m < n \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
assume "\<not>m < n"
[PROOF STATE]
proof (state)
this:
\<not> m < n

goal (1 subgoal):
 1. \<not> m < n \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> m < n
[PROOF STEP]
have "take n xs = take n (take m xs)"
[PROOF STATE]
proof (prove)
using this:
\<not> m < n

goal (1 subgoal):
 1. take n xs = take n (take m xs)
[PROOF STEP]
by (auto simp: min_def)
[PROOF STATE]
proof (state)
this:
take n xs = take n (take m xs)

goal (1 subgoal):
 1. \<not> m < n \<Longrightarrow> take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take n xs = take n (take m xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take n xs = take n (take m xs)

goal (1 subgoal):
 1. take n xs @ drop n (take m xs) = take (max n m) xs
[PROOF STEP]
by (simp del: take_take add: max_def)
[PROOF STATE]
proof (state)
this:
take n xs @ drop n (take m xs) = take (max n m) xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drop_take_drop:
  "drop n (take m xs) @ drop m xs = drop (min n m) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop n (take m xs) @ drop m xs = drop (min n m) xs
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> drop n (take m xs) @ drop m xs = drop (min n m) xs
 2. \<not> ?P \<Longrightarrow> drop n (take m xs) @ drop m xs = drop (min n m) xs
[PROOF STEP]
assume A: "\<not>m < n"
[PROOF STATE]
proof (state)
this:
\<not> m < n

goal (2 subgoals):
 1. ?P \<Longrightarrow> drop n (take m xs) @ drop m xs = drop (min n m) xs
 2. \<not> ?P \<Longrightarrow> drop n (take m xs) @ drop m xs = drop (min n m) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> m < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> m < n

goal (1 subgoal):
 1. drop n (take m xs) @ drop m xs = drop (min n m) xs
[PROOF STEP]
using drop_append[of n "take m xs" "drop m xs"]
[PROOF STATE]
proof (prove)
using this:
\<not> m < n
drop n (take m xs @ drop m xs) = drop n (take m xs) @ drop (n - length (take m xs)) (drop m xs)

goal (1 subgoal):
 1. drop n (take m xs) @ drop m xs = drop (min n m) xs
[PROOF STEP]
by (cases "length xs < n") (auto simp: not_less min_def)
[PROOF STATE]
proof (state)
this:
drop n (take m xs) @ drop m xs = drop (min n m) xs

goal (1 subgoal):
 1. \<not> \<not> m < n \<Longrightarrow> drop n (take m xs) @ drop m xs = drop (min n m) xs
[PROOF STEP]
qed (auto simp: min_def)


[STATEMENT]
lemma not_distinct_decomp_min_prefix:
  assumes "\<not> distinct ws"
  shows "\<exists> xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys
[PROOF STEP]
obtain xs y ys where "y \<in> set xs" "distinct xs" "ws = xs @ y # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y xs ys. \<lbrakk>y \<in> set xs; distinct xs; ws = xs @ y # ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ws

goal (1 subgoal):
 1. (\<And>y xs ys. \<lbrakk>y \<in> set xs; distinct xs; ws = xs @ y # ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: not_distinct_conv_prefix)
[PROOF STATE]
proof (state)
this:
y \<in> set xs
distinct xs
ws = xs @ y # ys

goal (1 subgoal):
 1. \<exists>xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> set xs
distinct xs
ws = xs @ y # ys

goal (1 subgoal):
 1. \<exists>xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set xs
distinct xs
ws = xs @ y # ys
[PROOF STEP]
obtain xs' ys' where "xs = xs' @ y # ys'"
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
distinct xs
ws = xs @ y # ys

goal (1 subgoal):
 1. (\<And>xs' ys'. xs = xs' @ y # ys' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: in_set_conv_decomp)
[PROOF STATE]
proof (state)
this:
xs = xs' @ y # ys'

goal (1 subgoal):
 1. \<exists>xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> set xs
distinct xs
ws = xs @ y # ys
xs = xs' @ y # ys'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
distinct xs
ws = xs @ y # ys
xs = xs' @ y # ys'

goal (1 subgoal):
 1. \<exists>xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs y. ws = xs @ y # ys @ y # zs \<and> distinct xs \<and> y \<notin> set xs \<and> y \<notin> set ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_distinct_decomp_min_not_distinct:
  assumes "\<not> distinct ws"
  shows "\<exists>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ws

goal (1 subgoal):
 1. \<exists>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
proof (induct ws)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> distinct [] \<Longrightarrow> \<exists>xs y ys zs. [] = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
 2. \<And>a ws. \<lbrakk>\<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y]); \<not> distinct (a # ws)\<rbrakk> \<Longrightarrow> \<exists>xs y ys zs. a # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
case (Cons w ws)
[PROOF STATE]
proof (state)
this:
\<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
\<not> distinct (w # ws)

goal (2 subgoals):
 1. \<not> distinct [] \<Longrightarrow> \<exists>xs y ys zs. [] = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
 2. \<And>a ws. \<lbrakk>\<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y]); \<not> distinct (a # ws)\<rbrakk> \<Longrightarrow> \<exists>xs y ys zs. a # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
proof (cases "distinct ws")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
 2. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
distinct ws

goal (2 subgoals):
 1. distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
 2. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct ws
[PROOF STEP]
obtain xs ys where "ws = xs @ w # ys" "w \<notin> set xs"
[PROOF STATE]
proof (prove)
using this:
distinct ws

goal (1 subgoal):
 1. (\<And>xs ys. \<lbrakk>ws = xs @ w # ys; w \<notin> set xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
distinct ws
\<not> distinct (w # ws)

goal (1 subgoal):
 1. (\<And>xs ys. \<lbrakk>ws = xs @ w # ys; w \<notin> set xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce dest: split_list_first)
[PROOF STATE]
proof (state)
this:
ws = xs @ w # ys
w \<notin> set xs

goal (2 subgoals):
 1. distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
 2. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ws = xs @ w # ys
w \<notin> set xs
[PROOF STEP]
have "distinct (xs @ [w])" "w # ws = [] @ w # xs @ w # ys"
[PROOF STATE]
proof (prove)
using this:
ws = xs @ w # ys
w \<notin> set xs

goal (1 subgoal):
 1. distinct (xs @ [w]) &&& w # ws = [] @ w # xs @ w # ys
[PROOF STEP]
using \<open>distinct ws\<close>
[PROOF STATE]
proof (prove)
using this:
ws = xs @ w # ys
w \<notin> set xs
distinct ws

goal (1 subgoal):
 1. distinct (xs @ [w]) &&& w # ws = [] @ w # xs @ w # ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (xs @ [w])
w # ws = [] @ w # xs @ w # ys

goal (2 subgoals):
 1. distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
 2. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (xs @ [w])
w # ws = [] @ w # xs @ w # ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ [w])
w # ws = [] @ w # xs @ w # ys

goal (1 subgoal):
 1. \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])

goal (1 subgoal):
 1. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> distinct ws

goal (1 subgoal):
 1. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> distinct ws
[PROOF STEP]
obtain xs y ys zs where "ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])"
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ws

goal (1 subgoal):
 1. (\<And>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ws
\<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
\<not> distinct (w # ws)

goal (1 subgoal):
 1. (\<And>xs y ys zs. ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])

goal (1 subgoal):
 1. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
have "w # ws = (w # xs) @ y # ys @ y # zs \<and> distinct (ys @ [y])"
[PROOF STATE]
proof (prove)
using this:
ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])

goal (1 subgoal):
 1. w # ws = (w # xs) @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w # ws = (w # xs) @ y # ys @ y # zs \<and> distinct (ys @ [y])

goal (1 subgoal):
 1. \<not> distinct ws \<Longrightarrow> \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w # ws = (w # xs) @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w # ws = (w # xs) @ y # ys @ y # zs \<and> distinct (ys @ [y])

goal (1 subgoal):
 1. \<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs y ys zs. w # ws = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])

goal (1 subgoal):
 1. \<not> distinct [] \<Longrightarrow> \<exists>xs y ys zs. [] = xs @ y # ys @ y # zs \<and> distinct (ys @ [y])
[PROOF STEP]
qed simp


[STATEMENT]
lemma card_Ex_subset:
  "k \<le> card M \<Longrightarrow> \<exists>N. N \<subseteq> M \<and> card N = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> card M \<Longrightarrow> \<exists>N\<subseteq>M. card N = k
[PROOF STEP]
by (induct rule: inc_induct) (auto simp: card_Suc_eq)


[STATEMENT]
lemma list_set_tl: "x \<in> set (tl xs) \<Longrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (tl xs) \<Longrightarrow> x \<in> set xs
[PROOF STEP]
by (cases xs) auto


[STATEMENT]
lemma NOMATCH_cong[cong]: "NOMATCH val pat = NOMATCH val pat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NOMATCH val pat = NOMATCH val pat
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma denote_while_n_iter_assoc:
  "denote_while_n_iter M0 M1 DS (Suc n) \<rho> = DS (M1 * (denote_while_n_iter M0 M1 DS n \<rho>) * adjoint M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS (Suc n) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)
[PROOF STEP]
proof (induct n arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<rho>. denote_while_n_iter M0 M1 DS (Suc 0) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS 0 \<rho> * adjoint M1)
 2. \<And>n \<rho>. (\<And>\<rho>. denote_while_n_iter M0 M1 DS (Suc n) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)) \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc (Suc n)) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>\<rho>. denote_while_n_iter M0 M1 DS (Suc 0) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS 0 \<rho> * adjoint M1)
 2. \<And>n \<rho>. (\<And>\<rho>. denote_while_n_iter M0 M1 DS (Suc n) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)) \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc (Suc n)) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS (Suc 0) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS 0 \<rho> * adjoint M1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n_iter M0 M1 DS (Suc 0) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS 0 \<rho> * adjoint M1)

goal (1 subgoal):
 1. \<And>n \<rho>. (\<And>\<rho>. denote_while_n_iter M0 M1 DS (Suc n) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)) \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc (Suc n)) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<rho>. (\<And>\<rho>. denote_while_n_iter M0 M1 DS (Suc n) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)) \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc (Suc n)) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
denote_while_n_iter M0 M1 DS (Suc n) ?\<rho> = DS (M1 * denote_while_n_iter M0 M1 DS n ?\<rho> * adjoint M1)

goal (1 subgoal):
 1. \<And>n \<rho>. (\<And>\<rho>. denote_while_n_iter M0 M1 DS (Suc n) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS n \<rho> * adjoint M1)) \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc (Suc n)) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS (Suc (Suc n)) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)
[PROOF STEP]
apply (subst denote_while_n_iter.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS (Suc n) (DS (M1 * \<rho> * adjoint M1)) = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)
[PROOF STEP]
apply (subst Suc, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
denote_while_n_iter M0 M1 DS (Suc (Suc n)) \<rho> = DS (M1 * denote_while_n_iter M0 M1 DS (Suc n) \<rho> * adjoint M1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_n_iter_dim:
  "\<rho> \<in> carrier_mat m m \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> M1 \<in> carrier_mat m m \<Longrightarrow> adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
  \<Longrightarrow> (\<And>\<rho>. \<rho> \<in> carrier_mat m m \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>))
  \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>)
[PROOF STEP]
proof (induct n arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS 0 \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)

goal (2 subgoals):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS 0 \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)

goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS 0 \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)
[PROOF STEP]
unfolding denote_while_n_iter.simps
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)

goal (1 subgoal):
 1. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n_iter M0 M1 DS 0 \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)
[PROOF STEP]
have dr: "\<rho> \<in> carrier_mat m m" and dM1: "M1 \<in> carrier_mat m m"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)

goal (1 subgoal):
 1. \<rho> \<in> carrier_mat m m &&& M1 \<in> carrier_mat m m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<rho> \<in> carrier_mat m m
M1 \<in> carrier_mat m m

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
have dMr: "M1 * \<rho> * adjoint M1 \<in> carrier_mat m m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
[PROOF STEP]
using dr dM1
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat m m
M1 \<in> carrier_mat m m

goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
M1 * \<rho> * adjoint M1 \<in> carrier_mat m m

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
have pdoMr: "partial_density_operator (M1 * \<rho> * adjoint M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
using pdo_close_under_measurement Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?\<rho> \<in> carrier_mat ?n ?n; partial_density_operator ?\<rho>; adjoint ?M * ?M \<le>\<^sub>L 1\<^sub>m ?n\<rbrakk> \<Longrightarrow> partial_density_operator (?M * ?\<rho> * adjoint ?M)
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)

goal (1 subgoal):
 1. partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
from Suc dMr pdoMr
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)
M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
have d: "DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m" and "partial_density_operator (DS (M1 * \<rho> * adjoint M1))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)
M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m &&& partial_density_operator (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m
partial_density_operator (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m
partial_density_operator (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m
partial_density_operator (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
unfolding denote_while_n_iter.simps
[PROOF STATE]
proof (prove)
using this:
DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m
partial_density_operator (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m
partial_density_operator (DS (M1 * \<rho> * adjoint M1))
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS \<rho>)\<rbrakk> \<Longrightarrow> denote_while_n_iter M0 M1 DS n ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m \<and> partial_density_operator (DS ?\<rho>)

goal (1 subgoal):
 1. denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n_iter M0 M1 DS (Suc n) \<rho> \<in> carrier_mat m m \<and> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pdo_denote_while_n_iter:
  "\<rho> \<in> carrier_mat m m \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> M1 \<in> carrier_mat m m \<Longrightarrow> adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
  \<Longrightarrow> (\<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>))
  \<Longrightarrow> (\<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m)
  \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>)
[PROOF STEP]
proof (induct n arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m

goal (2 subgoals):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m

goal (1 subgoal):
 1. partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)
[PROOF STEP]
unfolding denote_while_n_iter.simps
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m

goal (1 subgoal):
 1. partial_density_operator \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (denote_while_n_iter M0 M1 DS 0 \<rho>)

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
have "partial_density_operator (M1 * \<rho> * adjoint M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
using Suc pdo_close_under_measurement
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?\<rho> \<in> carrier_mat ?n ?n; partial_density_operator ?\<rho>; adjoint ?M * ?M \<le>\<^sub>L 1\<^sub>m ?n\<rbrakk> \<Longrightarrow> partial_density_operator (?M * ?\<rho> * adjoint ?M)

goal (1 subgoal):
 1. partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
have "M1 * \<rho> * adjoint M1 \<in> carrier_mat m m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m

goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M1 * \<rho> * adjoint M1 \<in> carrier_mat m m

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partial_density_operator (M1 * \<rho> * adjoint M1)
M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
[PROOF STEP]
have p: "partial_density_operator (DS (M1 * \<rho> * adjoint M1))" and d: "DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m "
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (M1 * \<rho> * adjoint M1)
M1 * \<rho> * adjoint M1 \<in> carrier_mat m m

goal (1 subgoal):
 1. partial_density_operator (DS (M1 * \<rho> * adjoint M1)) &&& DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (M1 * \<rho> * adjoint M1)
M1 * \<rho> * adjoint M1 \<in> carrier_mat m m
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m

goal (1 subgoal):
 1. partial_density_operator (DS (M1 * \<rho> * adjoint M1)) &&& DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (DS (M1 * \<rho> * adjoint M1))
DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat m m

goal (1 subgoal):
 1. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<rho> \<in> carrier_mat m m; partial_density_operator \<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)
[PROOF STEP]
unfolding denote_while_n_iter.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
using Suc(1)[OF d p Suc(4) Suc(5)] Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)))
\<lbrakk>?\<rho> \<in> carrier_mat m m; partial_density_operator ?\<rho>; M1 \<in> carrier_mat m m; adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m; \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat m m \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat m m\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n ?\<rho>)
\<rho> \<in> carrier_mat m m
partial_density_operator \<rho>
M1 \<in> carrier_mat m m
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m m
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> partial_density_operator (DS ?\<rho>)
?\<rho> \<in> carrier_mat m m \<and> partial_density_operator ?\<rho> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat m m

goal (1 subgoal):
 1. partial_density_operator (denote_while_n_iter M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (denote_while_n_iter M0 M1 DS (Suc n) \<rho>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_n_dim:
  assumes "\<rho> \<in> carrier_mat d d"
    "M0 \<in> carrier_mat d d"
    "M1 \<in> carrier_mat d d"
    "partial_density_operator \<rho>"
    "\<And>\<rho>'. \<rho>' \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>'  \<Longrightarrow> positive (DS \<rho>') \<and> trace (DS \<rho>') \<le> trace \<rho>' \<and> DS \<rho>' \<in> carrier_mat d d"
   shows "denote_while_n M0 M1 DS n \<rho>  \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof (induction n arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<rho>. denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d
 2. \<And>n \<rho>. (\<And>\<rho>. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d) \<Longrightarrow> denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>\<rho>. denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d
 2. \<And>n \<rho>. (\<And>\<rho>. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d) \<Longrightarrow> denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "M0 * \<rho> * adjoint M0 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M0 * \<rho> * adjoint M0 \<in> carrier_mat d d
[PROOF STEP]
using assms assoc_mult_mat
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
partial_density_operator \<rho>
\<lbrakk>?\<rho>' \<in> carrier_mat d d; partial_density_operator ?\<rho>'\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>') \<and> trace (DS ?\<rho>') \<le> trace ?\<rho>' \<and> DS ?\<rho>' \<in> carrier_mat d d
\<lbrakk>?A \<in> carrier_mat ?n\<^sub>1 ?n\<^sub>2; ?B \<in> carrier_mat ?n\<^sub>2 ?n\<^sub>3; ?C \<in> carrier_mat ?n\<^sub>3 ?n\<^sub>4\<rbrakk> \<Longrightarrow> ?A * ?B * ?C = ?A * (?B * ?C)

goal (1 subgoal):
 1. M0 * \<rho> * adjoint M0 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M0 * \<rho> * adjoint M0 \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M0 * \<rho> * adjoint M0 \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M0 * \<rho> * adjoint M0 \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS 0 \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n \<rho>. (\<And>\<rho>. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d) \<Longrightarrow> denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<rho>. (\<And>\<rho>. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d) \<Longrightarrow> denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n \<rho>. (\<And>\<rho>. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d) \<Longrightarrow> denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote_while_n M0 M1 DS n ?\<rho> \<in> carrier_mat d d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS n ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<rho>. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d) \<Longrightarrow> denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "denote_while_n M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d
[PROOF STEP]
using Suc assms
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS n ?\<rho> \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
partial_density_operator \<rho>
\<lbrakk>?\<rho>' \<in> carrier_mat d d; partial_density_operator ?\<rho>'\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>') \<and> trace (DS ?\<rho>') \<le> trace ?\<rho>' \<and> DS ?\<rho>' \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d

goal (1 subgoal):
 1. (\<And>\<rho>. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d) \<Longrightarrow> denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote_while_n M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS n (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS (Suc n) \<rho> \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_while_n_sum_dim:
  assumes "\<rho> \<in> carrier_mat d d"
    "M0 \<in> carrier_mat d d"
    "M1 \<in> carrier_mat d d"
    "partial_density_operator \<rho>"
    "\<And>\<rho>'. \<rho>' \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>'  \<Longrightarrow> positive (DS \<rho>') \<and> trace (DS \<rho>') \<le> trace \<rho>' \<and> DS \<rho>' \<in> carrier_mat d d"
  shows "matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0 \<in> carrier_mat d d
 2. \<And>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0 \<in> carrier_mat d d
 2. \<And>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) 0 \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
have " denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_dim assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; partial_density_operator ?\<rho>; \<And>\<rho>'. \<lbrakk>\<rho>' \<in> carrier_mat d d; partial_density_operator \<rho>'\<rbrakk> \<Longrightarrow> positive (?DS \<rho>') \<and> trace (?DS \<rho>') \<le> trace \<rho>' \<and> ?DS \<rho>' \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho> \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
partial_density_operator \<rho>
\<lbrakk>?\<rho>' \<in> carrier_mat d d; partial_density_operator ?\<rho>'\<rbrakk> \<Longrightarrow> positive (DS ?\<rho>') \<and> trace (DS ?\<rho>') \<le> trace ?\<rho>' \<and> DS ?\<rho>' \<in> carrier_mat d d

goal (1 subgoal):
 1. denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
denote_while_n M0 M1 DS n \<rho> \<in> carrier_mat d d
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) n \<in> carrier_mat d d \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. denote_while_n M0 M1 DS n \<rho>) (Suc n) \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trace_decrease_mul_adj:
  assumes pdo: "partial_density_operator \<rho>" and dimr: "\<rho> \<in> carrier_mat d d"
    and dimx: "x \<in> carrier_mat d d" and un: "adjoint x * x \<le>\<^sub>L   1\<^sub>m d "
  shows "trace (x * \<rho> * adjoint x) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
have ad: "adjoint x * x \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint x * x \<in> carrier_mat d d
[PROOF STEP]
using adjoint_dim index_mult_mat dimx
[PROOF STATE]
proof (prove)
using this:
?A \<in> carrier_mat ?n ?n \<Longrightarrow> adjoint ?A \<in> carrier_mat ?n ?n
\<lbrakk>?i < dim_row ?A; ?j < dim_col ?B\<rbrakk> \<Longrightarrow> (?A * ?B) $$ (?i, ?j) = row ?A ?i \<bullet> col ?B ?j
dim_row (?A * ?B) = dim_row ?A
dim_col (?A * ?B) = dim_col ?B
x \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint x * x \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint x * x \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
have "trace (x * \<rho> * adjoint x) = trace ((adjoint x * x) * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)
[PROOF STEP]
using dimx dimr
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)
[PROOF STEP]
by (mat_assoc d)
[PROOF STATE]
proof (state)
this:
trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
have "\<dots> \<le> trace (1\<^sub>m d * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (adjoint x * x * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)
[PROOF STEP]
using lowner_le_trace un ad dimr pdo
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> (?A \<le>\<^sub>L ?B) = (\<forall>\<rho>\<in>carrier_mat ?n ?n. partial_density_operator \<rho> \<longrightarrow> trace (?A * \<rho>) \<le> trace (?B * \<rho>))
adjoint x * x \<le>\<^sub>L 1\<^sub>m d
adjoint x * x \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. trace (adjoint x * x * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (adjoint x * x * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (adjoint x * x * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
have "\<dots> = trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (1\<^sub>m d * \<rho>) = trace \<rho>
[PROOF STEP]
using dimr
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (1\<^sub>m d * \<rho>) = trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (1\<^sub>m d * \<rho>) = trace \<rho>

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (x * \<rho> * adjoint x) \<le> trace (1\<^sub>m d * \<rho>)
trace (1\<^sub>m d * \<rho>) = trace \<rho>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (x * \<rho> * adjoint x) \<le> trace (1\<^sub>m d * \<rho>)
trace (1\<^sub>m d * \<rho>) = trace \<rho>

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (x * \<rho> * adjoint x) \<le> trace \<rho>

goal:
No subgoals!
[PROOF STEP]
qed