[STATEMENT]
lemma denote_while_split:
  assumes wc: "well_com (While M S)" and dsr: "\<rho> \<in> density_states"
  shows "denote (While M S) \<rho> = (M 0) * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have m: "measurement d 2 M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measurement d 2 M
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (While M S)

goal (1 subgoal):
 1. measurement d 2 M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
measurement d 2 M

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have wcs: "well_com S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_com S
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (While M S)

goal (1 subgoal):
 1. well_com S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_com S

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
define M0 where "M0 = M 0"
[PROOF STATE]
proof (state)
this:
M0 = M 0

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
define M1 where "M1 = M 1"
[PROOF STATE]
proof (state)
this:
M1 = M 1

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have dM0: "M0 \<in> carrier_mat d d" and dM1: "M1 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M0 \<in> carrier_mat d d &&& M1 \<in> carrier_mat d d
[PROOF STEP]
using m measurement_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M
measurement ?d ?n ?M = ((\<forall>j<?n. ?M j \<in> carrier_mat ?d ?d) \<and> matrix_sum ?d (\<lambda>j. adjoint (?M j) * ?M j) ?n = 1\<^sub>m ?d)
M0 = M 0
M1 = M 1

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have M1leq: "adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement_le_one_mat m M1_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>measurement ?d ?n ?f; ?j < ?n\<rbrakk> \<Longrightarrow> adjoint (?f ?j) * ?f ?j \<le>\<^sub>L 1\<^sub>m ?d
measurement d 2 M
M1 = M 1

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
define DS where "DS = denote S"
[PROOF STATE]
proof (state)
this:
DS = denote S

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
define D0 where "D0 = denote_while_n M0 M1 DS"
[PROOF STATE]
proof (state)
this:
D0 = denote_while_n M0 M1 DS

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
[PROOF STATE]
proof (state)
this:
D1 = denote_while_n_comp M0 M1 DS

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
define D where "D = denote_while_n_iter M0 M1 DS"
[PROOF STATE]
proof (state)
this:
D = denote_while_n_iter M0 M1 DS

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
define DW where "DW \<rho> = denote (While M S) \<rho>" for \<rho>
[PROOF STATE]
proof (state)
this:
DW ?\<rho> = denote (While M S) ?\<rho>

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
DW ?\<rho> = denote (While M S) ?\<rho>

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
fix \<rho>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
assume dsr: "\<rho> \<in> density_states"
[PROOF STATE]
proof (state)
this:
\<rho> \<in> density_states

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> \<in> density_states
[PROOF STEP]
have dr: "\<rho> \<in> carrier_mat d d" and pdor: "partial_density_operator \<rho>"
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states

goal (1 subgoal):
 1. \<rho> \<in> carrier_mat d d &&& partial_density_operator \<rho>
[PROOF STEP]
using density_states_def
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have pdoDkr: "\<And>k. partial_density_operator (D k \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. partial_density_operator (D k \<rho>)
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. partial_density_operator (denote_while_n_iter M0 M1 DS k \<rho>)
[PROOF STEP]
using pdo_denote_while_n_iter[OF dr pdor dM1 M1leq]
      denote_partial_density_operator[OF wcs] denote_dim[OF wcs, folded DS_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<rho>. \<rho> \<in> carrier_mat d d \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (?DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat d d \<and> partial_density_operator \<rho> \<Longrightarrow> ?DS \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter ?M0.0 M1 ?DS ?n \<rho>)
\<lbrakk>partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (denote S ?\<rho>)
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> DS ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. partial_density_operator (denote_while_n_iter M0 M1 DS k \<rho>)
[PROOF STEP]
apply (fold DS_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>DS M0 n. \<lbrakk>\<And>\<rho>. \<rho> \<in> carrier_mat d d \<and> partial_density_operator \<rho> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<rho> \<in> carrier_mat d d \<and> partial_density_operator \<rho> \<Longrightarrow> DS \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS n \<rho>); \<And>\<rho>. \<lbrakk>partial_density_operator \<rho>; \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (DS \<rho>); \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> DS \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (denote_while_n_iter M0 M1 DS k \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (D ?k \<rho>)

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_density_operator (D ?k \<rho>)
[PROOF STEP]
have pDkr: "\<And>k. positive (D k \<rho>)"
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (D ?k \<rho>)

goal (1 subgoal):
 1. \<And>k. positive (D k \<rho>)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
positive (D ?k \<rho>) \<and> trace (D ?k \<rho>) \<le> 1

goal (1 subgoal):
 1. \<And>k. positive (D k \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (D ?k \<rho>)

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have dDkr: "\<And>k. D k \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. D k \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_iter_dim[OF dr pdor dM1 M1leq denote_dim_pdo[OF wcs, folded DS_def], of id M0, simplified, folded D_def]
[PROOF STATE]
proof (prove)
using this:
D ?n \<rho> \<in> carrier_mat d d \<and> partial_density_operator (D ?n \<rho>)

goal (1 subgoal):
 1. \<And>k. D k \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
D ?k \<rho> \<in> carrier_mat d d
[PROOF STEP]
have dD0kr: "\<And>k. D0 k \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
D ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. D0 k \<rho> \<in> carrier_mat d d
[PROOF STEP]
unfolding D0_def denote_while_n.simps
[PROOF STATE]
proof (prove)
using this:
D ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. M0 * denote_while_n_iter M0 M1 DS k \<rho> * adjoint M0 \<in> carrier_mat d d
[PROOF STEP]
apply (fold D_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. (\<And>k. D k \<rho> \<in> carrier_mat d d) \<Longrightarrow> M0 * D k \<rho> * adjoint M0 \<in> carrier_mat d d
[PROOF STEP]
using dM0
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?\<rho>'3 \<in> density_states \<Longrightarrow> D0 ?k ?\<rho>'3 \<in> carrier_mat d d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
note dD0k = this
[PROOF STATE]
proof (state)
this:
?\<rho>'3 \<in> density_states \<Longrightarrow> D0 ?k ?\<rho>'3 \<in> carrier_mat d d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have "matrix_sum d (\<lambda>k. D0 k \<rho>) k \<in> carrier_mat d d" if dsr: "\<rho> \<in> density_states" for \<rho> k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. D0 k \<rho>) k \<in> carrier_mat d d
[PROOF STEP]
using matrix_sum_dim[OF dD0k, of _ "\<lambda>k. \<rho>" id, OF dsr] dsr
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. D0 (id k) \<rho>) ?n \<in> carrier_mat d d
\<rho> \<in> density_states

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. D0 k \<rho>) k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?\<rho> \<in> density_states \<Longrightarrow> matrix_sum d (\<lambda>k. D0 k ?\<rho>) ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?\<rho> \<in> density_states \<Longrightarrow> matrix_sum d (\<lambda>k. D0 k ?\<rho>) ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have "matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = (D0 0 \<rho>) + matrix_sum d (\<lambda>k. D0 (Suc k) \<rho>) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = D0 0 \<rho> + matrix_sum d (\<lambda>k. D0 (Suc k) \<rho>) k
[PROOF STEP]
using matrix_sum_shift_Suc[of _ "\<lambda>k. D0 k \<rho>"] dD0k[OF dsr]
[PROOF STATE]
proof (prove)
using this:
(\<And>k. k < Suc ?n \<Longrightarrow> D0 k \<rho> \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d (\<lambda>k. D0 k \<rho>) (Suc ?n) = D0 0 \<rho> + matrix_sum ?d (\<lambda>k. D0 (Suc k) \<rho>) ?n
D0 ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = D0 0 \<rho> + matrix_sum d (\<lambda>k. D0 (Suc k) \<rho>) k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = D0 0 \<rho> + matrix_sum d (\<lambda>k. D0 (Suc k) \<rho>) k

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = D0 0 \<rho> + matrix_sum d (\<lambda>k. D0 (Suc k) \<rho>) k

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have "\<dots> = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D0 0 \<rho> + matrix_sum d (\<lambda>k. D0 (Suc k) \<rho>) k = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k
[PROOF STEP]
unfolding D0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while_n M0 M1 DS 0 \<rho> + matrix_sum d (\<lambda>k. denote_while_n M0 M1 DS (Suc k) \<rho>) k = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. denote_while_n M0 M1 DS k (DS (M1 * \<rho> * adjoint M1))) k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D0 0 \<rho> + matrix_sum d (\<lambda>k. D0 (Suc k) \<rho>) k = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k
[PROOF STEP]
have "matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) k

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc ?k2) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) ?k2

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
note eqk = this
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc ?k2) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) ?k2

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have dr: "\<rho> \<in> carrier_mat d d" and pdor: "partial_density_operator \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> \<in> carrier_mat d d &&& partial_density_operator \<rho>
[PROOF STEP]
using density_states_def dsr
[PROOF STATE]
proof (prove)
using this:
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
\<rho> \<in> density_states

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
[PROOF STEP]
have "M1 * \<rho> * adjoint M1 \<in> carrier_mat d d" and "partial_density_operator (M1 * \<rho> * adjoint M1)"
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> carrier_mat d d &&& partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
using dM1 dr pdo_close_under_measurement[OF dM1 dr pdor M1leq]
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
M1 \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
partial_density_operator (M1 * \<rho> * adjoint M1)

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M1 * \<rho> * adjoint M1 \<in> carrier_mat d d
partial_density_operator (M1 * \<rho> * adjoint M1)
[PROOF STEP]
have dSM1r: "(DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d" and pdoSM1r: "partial_density_operator (DS (M1 * \<rho> * adjoint M1))"
[PROOF STATE]
proof (prove)
using this:
M1 * \<rho> * adjoint M1 \<in> carrier_mat d d
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. DS (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d &&& partial_density_operator (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
unfolding DS_def
[PROOF STATE]
proof (prove)
using this:
M1 * \<rho> * adjoint M1 \<in> carrier_mat d d
partial_density_operator (M1 * \<rho> * adjoint M1)

goal (1 subgoal):
 1. denote S (M1 * \<rho> * adjoint M1) \<in> carrier_mat d d &&& partial_density_operator (denote S (M1 * \<rho> * adjoint M1))
[PROOF STEP]
using denote_dim_pdo[OF wcs]
[PROOF STATE]
proof (prove)
using this:
M1 * \<rho> * adjoint M1 \<in> carrier_mat d d
partial_density_operator (M1 * \<rho> * adjoint M1)
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> denote S ?\<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote S ?\<rho>)

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have "limit_mat (matrix_sum d (\<lambda>k. D0 k \<rho>)) (DW \<rho>) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. D0 k \<rho>)) (DW \<rho>) d
[PROOF STEP]
unfolding M0_def M1_def D0_def DS_def DW_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
using limit_mat_denote_while_n[OF wc dr pdor]
[PROOF STATE]
proof (prove)
using this:
limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (matrix_sum d (\<lambda>k. D0 k \<rho>)) (DW \<rho>) d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
limit_mat (matrix_sum d (\<lambda>k. D0 k \<rho>)) (DW \<rho>) d
[PROOF STEP]
have liml: "limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (DW \<rho>) d"
[PROOF STATE]
proof (prove)
using this:
limit_mat (matrix_sum d (\<lambda>k. D0 k \<rho>)) (DW \<rho>) d

goal (1 subgoal):
 1. limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (DW \<rho>) d
[PROOF STEP]
using limit_mat_ignore_initial_segment[of "matrix_sum d (\<lambda>k. D0 k \<rho>)" "DW \<rho>" d 1]
[PROOF STATE]
proof (prove)
using this:
limit_mat (matrix_sum d (\<lambda>k. D0 k \<rho>)) (DW \<rho>) d
limit_mat (matrix_sum d (\<lambda>k. D0 k \<rho>)) (DW \<rho>) d \<Longrightarrow> limit_mat (\<lambda>n. matrix_sum d (\<lambda>k. D0 k \<rho>) (n + 1)) (DW \<rho>) d

goal (1 subgoal):
 1. limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (DW \<rho>) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (DW \<rho>) d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have dM0r: "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 dM0 dr
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have "limit_mat (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))) (DW (DS (M1 * \<rho> * adjoint M1))) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))) (DW (DS (M1 * \<rho> * adjoint M1))) d
[PROOF STEP]
using limit_mat_denote_while_n[OF wc dSM1r pdoSM1r]
[PROOF STATE]
proof (prove)
using this:
limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k (DS (M1 * \<rho> * adjoint M1)))) (denote (While M S) (DS (M1 * \<rho> * adjoint M1))) d

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))) (DW (DS (M1 * \<rho> * adjoint M1))) d
[PROOF STEP]
unfolding M0_def M1_def D0_def DS_def DW_def
[PROOF STATE]
proof (prove)
using this:
limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k (denote S (M 1 * \<rho> * adjoint (M 1))))) (denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))) d

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k (denote S (M 1 * \<rho> * adjoint (M 1))))) (denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))) (DW (DS (M1 * \<rho> * adjoint M1))) d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
limit_mat (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))) (DW (DS (M1 * \<rho> * adjoint M1))) d
[PROOF STEP]
have
    limr: "limit_mat
      (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))))
      (M0 * \<rho> * adjoint M0 + (DW (DS (M1 * \<rho> * adjoint M1))))
      d"
[PROOF STATE]
proof (prove)
using this:
limit_mat (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))) (DW (DS (M1 * \<rho> * adjoint M1))) d

goal (1 subgoal):
 1. limit_mat (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d
[PROOF STEP]
using mat_add_limit[OF dM0r]
[PROOF STATE]
proof (prove)
using this:
limit_mat (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))) (DW (DS (M1 * \<rho> * adjoint M1))) d
limit_mat ?X ?A d \<Longrightarrow> limit_mat (mat_add_seq (M0 * \<rho> * adjoint M0) ?X) (M0 * \<rho> * adjoint M0 + ?A) d

goal (1 subgoal):
 1. limit_mat (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
limit_mat (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
have
    "(\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k))
     = (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) = mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
using eqk mat_add_seq_def
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc ?k2) = M0 * \<rho> * adjoint M0 + matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))) ?k2
mat_add_seq ?A ?X = (\<lambda>n. ?A + ?X n)

goal (1 subgoal):
 1. (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) = mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) = mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
limit_mat (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d
(\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) = mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
have
    "limit_mat
      (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k))
      (M0 * \<rho> * adjoint M0 + (DW (DS (M1 * \<rho> * adjoint M1))))
      d"
[PROOF STATE]
proof (prove)
using this:
limit_mat (mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d
(\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) = mat_add_seq (M0 * \<rho> * adjoint M0) (matrix_sum d (\<lambda>k. D0 k (DS (M1 * \<rho> * adjoint M1))))

goal (1 subgoal):
 1. limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
with liml limit_mat_unique
[PROOF STATE]
proof (chain)
picking this:
limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (DW \<rho>) d
\<lbrakk>limit_mat ?X ?A ?m; limit_mat ?X ?B ?m\<rbrakk> \<Longrightarrow> ?A = ?B
limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d
[PROOF STEP]
have
    "DW \<rho> = (M0 * \<rho> * adjoint M0 + (DW (DS (M1 * \<rho> * adjoint M1))))"
[PROOF STATE]
proof (prove)
using this:
limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (DW \<rho>) d
\<lbrakk>limit_mat ?X ?A ?m; limit_mat ?X ?B ?m\<rbrakk> \<Longrightarrow> ?A = ?B
limit_mat (\<lambda>k. matrix_sum d (\<lambda>k. D0 k \<rho>) (Suc k)) (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) d

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

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
DW \<rho> = M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
DW \<rho> = M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
unfolding DW_def M0_def M1_def DS_def
[PROOF STATE]
proof (prove)
using this:
denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))

goal (1 subgoal):
 1. denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_while_split:
  assumes wc: "well_com (While M S)" and qpP: "is_quantum_predicate P"
  shows "wlp (While M S) P = adjoint (M 0) * P * (M 0) + adjoint (M 1) * (wlp S (wlp (While M S) P)) * (M 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have m: "measurement d 2 M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measurement d 2 M
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (While M S)

goal (1 subgoal):
 1. measurement d 2 M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
measurement d 2 M

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have wcs: "well_com S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_com S
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (While M S)

goal (1 subgoal):
 1. well_com S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_com S

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
define M0 where "M0 = M 0"
[PROOF STATE]
proof (state)
this:
M0 = M 0

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
define M1 where "M1 = M 1"
[PROOF STATE]
proof (state)
this:
M1 = M 1

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have dM0: "M0 \<in> carrier_mat d d" and dM1: "M1 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M0 \<in> carrier_mat d d &&& M1 \<in> carrier_mat d d
[PROOF STEP]
using m measurement_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M
measurement ?d ?n ?M = ((\<forall>j<?n. ?M j \<in> carrier_mat ?d ?d) \<and> matrix_sum ?d (\<lambda>j. adjoint (?M j) * ?M j) ?n = 1\<^sub>m ?d)
M0 = M 0
M1 = M 1

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

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have M1leq: "adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement_le_one_mat m M1_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>measurement ?d ?n ?f; ?j < ?n\<rbrakk> \<Longrightarrow> adjoint (?f ?j) * ?f ?j \<le>\<^sub>L 1\<^sub>m ?d
measurement d 2 M
M1 = M 1

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

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
define DS where "DS = denote S"
[PROOF STATE]
proof (state)
this:
DS = denote S

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
define D0 where "D0 = denote_while_n M0 M1 DS"
[PROOF STATE]
proof (state)
this:
D0 = denote_while_n M0 M1 DS

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
[PROOF STATE]
proof (state)
this:
D1 = denote_while_n_comp M0 M1 DS

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
define D where "D = denote_while_n_iter M0 M1 DS"
[PROOF STATE]
proof (state)
this:
D = denote_while_n_iter M0 M1 DS

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
define DW where "DW \<rho> = denote (While M S) \<rho>" for \<rho>
[PROOF STATE]
proof (state)
this:
DW ?\<rho> = denote (While M S) ?\<rho>

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have dP: "P \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat d d
[PROOF STEP]
using qpP is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate P
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

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

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have qpWP: "is_quantum_predicate (wlp (While M S) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp (While M S) P)
[PROOF STEP]
using qpP wc wlp_close[OF wc qpP]
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate P
well_com (While M S)
is_quantum_predicate (wlp (While M S) P)

goal (1 subgoal):
 1. is_quantum_predicate (wlp (While M S) P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (While M S) P)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp (While M S) P)
[PROOF STEP]
have "is_quantum_predicate (wlp S (wlp (While M S) P))"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp (While M S) P)

goal (1 subgoal):
 1. is_quantum_predicate (wlp S (wlp (While M S) P))
[PROOF STEP]
using wc wlp_close[OF wcs]
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp (While M S) P)
well_com (While M S)
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (wlp S ?P)

goal (1 subgoal):
 1. is_quantum_predicate (wlp S (wlp (While M S) P))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp S (wlp (While M S) P))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp S (wlp (While M S) P))
[PROOF STEP]
have dWWP: "(wlp S (wlp (While M S) P)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S (wlp (While M S) P))

goal (1 subgoal):
 1. wlp S (wlp (While M S) P) \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S (wlp (While M S) P))
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. wlp S (wlp (While M S) P) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp S (wlp (While M S) P) \<in> carrier_mat d d

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have dWP: "(wlp (While M S) P) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (While M S) P \<in> carrier_mat d d
[PROOF STEP]
using qpWP is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp (While M S) P)
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. wlp (While M S) P \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp (While M S) P \<in> carrier_mat d d

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wlp (While M S) P \<in> carrier_mat d d

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
fix \<rho>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
assume dsr: "\<rho> \<in> density_states"
[PROOF STATE]
proof (state)
this:
\<rho> \<in> density_states

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> \<in> density_states
[PROOF STEP]
have dr: "\<rho> \<in> carrier_mat d d" and pdor: "partial_density_operator \<rho>"
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states

goal (1 subgoal):
 1. \<rho> \<in> carrier_mat d d &&& partial_density_operator \<rho>
[PROOF STEP]
using density_states_def
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

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

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have dsM1r: "M1 * \<rho> * adjoint M1 \<in> density_states"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> density_states
[PROOF STEP]
unfolding density_states_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 * \<rho> * adjoint M1 \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
[PROOF STEP]
using pdo_close_under_measurement[OF dM1 dr pdor] M1leq dM1 dr
[PROOF STATE]
proof (prove)
using this:
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d \<Longrightarrow> partial_density_operator (M1 * \<rho> * adjoint M1)
adjoint M1 * M1 \<le>\<^sub>L 1\<^sub>m d
M1 \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M1 * \<rho> * adjoint M1 \<in> density_states
[PROOF STEP]
have dsDSM1r: "DS (M1 * \<rho> * adjoint M1) \<in> density_states"
[PROOF STATE]
proof (prove)
using this:
M1 * \<rho> * adjoint M1 \<in> density_states

goal (1 subgoal):
 1. DS (M1 * \<rho> * adjoint M1) \<in> density_states
[PROOF STEP]
unfolding density_states_def DS_def
[PROOF STATE]
proof (prove)
using this:
M1 * \<rho> * adjoint M1 \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

goal (1 subgoal):
 1. denote S (M1 * \<rho> * adjoint M1) \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
[PROOF STEP]
using denote_dim_pdo[OF wcs]
[PROOF STATE]
proof (prove)
using this:
M1 * \<rho> * adjoint M1 \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> denote S ?\<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote S ?\<rho>)

goal (1 subgoal):
 1. denote S (M1 * \<rho> * adjoint M1) \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
DS (M1 * \<rho> * adjoint M1) \<in> density_states

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have dM0r: "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 dM0 dr
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have dDWDSM1r: "DW (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DW (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d
[PROOF STEP]
unfolding DW_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (While M S) (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d
[PROOF STEP]
using denote_dim[OF wc] dsDSM1r density_states_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> denote (While M S) ?\<rho> \<in> carrier_mat d d
DS (M1 * \<rho> * adjoint M1) \<in> density_states
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

goal (1 subgoal):
 1. denote (While M S) (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
DW (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have eq2: "trace ((wlp (While M S) P) * DS (M1 * \<rho> * adjoint M1))
          = trace (P * (DW (DS (M1 * \<rho> * adjoint M1)))) + trace (DS (M1 * \<rho> * adjoint M1)) - trace (DW (DS (M1 * \<rho> * adjoint M1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (DS (M1 * \<rho> * adjoint M1)) - trace (DW (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
unfolding DW_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) = trace (P * denote (While M S) (DS (M1 * \<rho> * adjoint M1))) + trace (DS (M1 * \<rho> * adjoint M1)) - trace (denote (While M S) (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
using wlp_soundness[OF wc qpP] dsDSM1r
[PROOF STATE]
proof (prove)
using this:
\<forall>\<rho>\<in>density_states. trace (wlp (While M S) P * \<rho>) = trace (P * denote (While M S) \<rho>) + trace \<rho> - trace (denote (While M S) \<rho>)
DS (M1 * \<rho> * adjoint M1) \<in> density_states

goal (1 subgoal):
 1. trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) = trace (P * denote (While M S) (DS (M1 * \<rho> * adjoint M1))) + trace (DS (M1 * \<rho> * adjoint M1)) - trace (denote (While M S) (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (DS (M1 * \<rho> * adjoint M1)) - trace (DW (DS (M1 * \<rho> * adjoint M1)))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have eq3: "trace (M1 * \<rho> * adjoint M1) = trace \<rho> - trace (M0 * \<rho> * adjoint M0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M1 * \<rho> * adjoint M1) = trace \<rho> - trace (M0 * \<rho> * adjoint M0)
[PROOF STEP]
unfolding M0_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M 1 * \<rho> * adjoint (M 1)) = trace \<rho> - trace (M 0 * \<rho> * adjoint (M 0))
[PROOF STEP]
using m trace_measurement2[OF m dr] dr
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M
trace (M 0 * \<rho> * adjoint (M 0)) + trace (M 1 * \<rho> * adjoint (M 1)) = trace \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (M 1 * \<rho> * adjoint (M 1)) = trace \<rho> - trace (M 0 * \<rho> * adjoint (M 0))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
trace (M1 * \<rho> * adjoint M1) = trace \<rho> - trace (M0 * \<rho> * adjoint M0)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "trace (adjoint M1 * (wlp S (wlp (While M S) P)) * M1 * \<rho>)
          = trace ((wlp S (wlp (While M S) P)) * (M1 * \<rho> * adjoint M1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1))
[PROOF STEP]
using dWWP dM1 dr
[PROOF STATE]
proof (prove)
using this:
wlp S (wlp (While M S) P) \<in> carrier_mat d d
M1 \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1))
[PROOF STEP]
by (mat_assoc d)
[PROOF STATE]
proof (state)
this:
trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "\<dots> = trace ((wlp (While M S) P) * DS (M1 * \<rho> * adjoint M1))
                  + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1)) = trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1))
[PROOF STEP]
unfolding DS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1)) = trace (wlp (While M S) P * denote S (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (denote S (M1 * \<rho> * adjoint M1))
[PROOF STEP]
using wlp_soundness[OF wcs qpWP] dsM1r
[PROOF STATE]
proof (prove)
using this:
\<forall>\<rho>\<in>density_states. trace (wlp S (wlp (While M S) P) * \<rho>) = trace (wlp (While M S) P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)
M1 * \<rho> * adjoint M1 \<in> density_states

goal (1 subgoal):
 1. trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1)) = trace (wlp (While M S) P * denote S (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (denote S (M1 * \<rho> * adjoint M1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1)) = trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (wlp S (wlp (While M S) P) * (M1 * \<rho> * adjoint M1)) = trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "\<dots> = trace (P * (DW (DS (M1 * \<rho> * adjoint M1))))
                  + trace (M1 * \<rho> * adjoint M1)  - trace (DW (DS (M1 * \<rho> * adjoint M1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1)) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (M1 * \<rho> * adjoint M1) - trace (DW (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
using eq2
[PROOF STATE]
proof (prove)
using this:
trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (DS (M1 * \<rho> * adjoint M1)) - trace (DW (DS (M1 * \<rho> * adjoint M1)))

goal (1 subgoal):
 1. trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1)) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (M1 * \<rho> * adjoint M1) - trace (DW (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1)) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (M1 * \<rho> * adjoint M1) - trace (DW (DS (M1 * \<rho> * adjoint M1)))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (wlp (While M S) P * DS (M1 * \<rho> * adjoint M1)) + trace (M1 * \<rho> * adjoint M1) - trace (DS (M1 * \<rho> * adjoint M1)) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (M1 * \<rho> * adjoint M1) - trace (DW (DS (M1 * \<rho> * adjoint M1)))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "\<dots> = trace (P * (DW (DS (M1 * \<rho> * adjoint M1)))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (M1 * \<rho> * adjoint M1) - trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
using eq3
[PROOF STATE]
proof (prove)
using this:
trace (M1 * \<rho> * adjoint M1) = trace \<rho> - trace (M0 * \<rho> * adjoint M0)

goal (1 subgoal):
 1. trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (M1 * \<rho> * adjoint M1) - trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace (M1 * \<rho> * adjoint M1) - trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
have eq4: "trace (adjoint M1 * (wlp S (wlp (While M S) P)) * M1 * \<rho>)
      = trace (P * (DW (DS (M1 * \<rho> * adjoint M1)))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))"
[PROOF STATE]
proof (prove)
using this:
trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))

goal (1 subgoal):
 1. trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "trace (adjoint M0 * P * M0 * \<rho>) + trace (P * (DW (DS (M1 * \<rho> * adjoint M1))))
      = trace (P * ((M0 * \<rho> * adjoint M0) + (DW (DS (M1 * \<rho> * adjoint M1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
using dP dr dM0 dDWDSM1r
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
M0 \<in> carrier_mat d d
DW (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))))
[PROOF STEP]
by (mat_assoc d)
[PROOF STATE]
proof (state)
this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "\<dots> = trace (P * (DW \<rho>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (P * (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1)))) = trace (P * DW \<rho>)
[PROOF STEP]
unfolding DW_def M0_def M1_def DS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (P * (M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1))))) = trace (P * denote (While M S) \<rho>)
[PROOF STEP]
using denote_while_split[OF wc dsr]
[PROOF STATE]
proof (prove)
using this:
denote (While M S) \<rho> = M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))

goal (1 subgoal):
 1. trace (P * (M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1))))) = trace (P * denote (While M S) \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (P * (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1)))) = trace (P * DW \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW \<rho>)
[PROOF STEP]
have eq5: "trace (adjoint M0 * P * M0 * \<rho>) + trace (P * (DW (DS (M1 * \<rho> * adjoint M1)))) = trace (P * (DW \<rho>))"
[PROOF STATE]
proof (prove)
using this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW \<rho>)

goal (1 subgoal):
 1. trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW \<rho>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1)))
      = trace (M0 * \<rho> * adjoint M0 + (DW (DS (M1 * \<rho> * adjoint M1))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1)))
[PROOF STEP]
using dr dM0 dDWDSM1r
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
M0 \<in> carrier_mat d d
DW (DS (M1 * \<rho> * adjoint M1)) \<in> carrier_mat d d

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

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1)))

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have "\<dots> = trace (DW \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)
[PROOF STEP]
unfolding DW_def DS_def M0_def M1_def denote_while_split[OF wc dsr]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1)))) = trace (M 0 * \<rho> * adjoint (M 0) + denote (While M S) (denote S (M 1 * \<rho> * adjoint (M 1))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (M0 * \<rho> * adjoint M0 + DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)
[PROOF STEP]
have eq6: "trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)"
[PROOF STATE]
proof (prove)
using this:
trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)

goal (1 subgoal):
 1. trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
from eq5 eq4 eq6
[PROOF STATE]
proof (chain)
picking this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW \<rho>)
trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))
trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)
[PROOF STEP]
have
      eq7: "trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>)
      = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)"
[PROOF STATE]
proof (prove)
using this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (P * DW (DS (M1 * \<rho> * adjoint M1))) = trace (P * DW \<rho>)
trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW (DS (M1 * \<rho> * adjoint M1))) + trace \<rho> - (trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))))
trace (M0 * \<rho> * adjoint M0) + trace (DW (DS (M1 * \<rho> * adjoint M1))) = trace (DW \<rho>)

goal (1 subgoal):
 1. trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have eq8: "trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>)
      = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)
[PROOF STEP]
using dM0 dM1 dr dP dWWP
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
P \<in> carrier_mat d d
wlp S (wlp (While M S) P) \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)
[PROOF STEP]
by (mat_assoc d)
[PROOF STATE]
proof (state)
this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
from eq7 eq8
[PROOF STATE]
proof (chain)
picking this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)
[PROOF STEP]
have
      eq9: "trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)"
[PROOF STATE]
proof (prove)
using this:
trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
trace (adjoint M0 * P * M0 * \<rho>) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)

goal (1 subgoal):
 1. trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have eq10: "trace ((wlp (While M S) P) * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp (While M S) P * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
[PROOF STEP]
unfolding DW_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp (While M S) P * \<rho>) = trace (P * denote (While M S) \<rho>) + trace \<rho> - trace (denote (While M S) \<rho>)
[PROOF STEP]
using wlp_soundness[OF wc qpP] dsr
[PROOF STATE]
proof (prove)
using this:
\<forall>\<rho>\<in>density_states. trace (wlp (While M S) P * \<rho>) = trace (P * denote (While M S) \<rho>) + trace \<rho> - trace (denote (While M S) \<rho>)
\<rho> \<in> density_states

goal (1 subgoal):
 1. trace (wlp (While M S) P * \<rho>) = trace (P * denote (While M S) \<rho>) + trace \<rho> - trace (denote (While M S) \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (wlp (While M S) P * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
with eq9
[PROOF STATE]
proof (chain)
picking this:
trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
trace (wlp (While M S) P * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
[PROOF STEP]
have "trace ((wlp (While M S) P) * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)"
[PROOF STATE]
proof (prove)
using this:
trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)
trace (wlp (While M S) P * \<rho>) = trace (P * DW \<rho>) + trace \<rho> - trace (DW \<rho>)

goal (1 subgoal):
 1. trace (wlp (While M S) P * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (wlp (While M S) P * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (wlp (While M S) P * ?\<rho>2) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * ?\<rho>2)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (wlp (While M S) P * ?\<rho>2) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * ?\<rho>2)
[PROOF STEP]
have "(wlp (While M S) P) = (adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1)"
[PROOF STATE]
proof (prove)
using this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (wlp (While M S) P * ?\<rho>2) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * ?\<rho>2)

goal (1 subgoal):
 1. wlp (While M S) P = adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1
[PROOF STEP]
using trace_pdo_eq_imp_eq[OF dWP, of "adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1"]
      dM0 dP dM1 dWWP density_states_def
[PROOF STATE]
proof (prove)
using this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (wlp (While M S) P * ?\<rho>2) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * ?\<rho>2)
\<lbrakk>adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1 \<in> carrier_mat d d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> trace (wlp (While M S) P * \<rho>) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * \<rho>)\<rbrakk> \<Longrightarrow> wlp (While M S) P = adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d
M1 \<in> carrier_mat d d
wlp S (wlp (While M S) P) \<in> carrier_mat d d
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

goal (1 subgoal):
 1. wlp (While M S) P = adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
wlp (While M S) P = adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wlp (While M S) P = adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wlp (While M S) P = adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
using M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
wlp (While M S) P = adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1
M0 = M 0
M1 = M 1

goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_is_weakest_liberal_precondition:
  assumes "well_com S" and "is_quantum_predicate P"
  shows "is_weakest_liberal_precondition (wlp S P) S P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_weakest_liberal_precondition (wlp S P) S P
[PROOF STEP]
unfolding is_weakest_liberal_precondition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S P) \<and> \<Turnstile>\<^sub>p {wlp S P} S {P} \<and> (\<forall>Q. is_quantum_predicate Q \<longrightarrow> \<Turnstile>\<^sub>p {Q} S {P} \<longrightarrow> Q \<le>\<^sub>L wlp S P)
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. is_quantum_predicate (wlp S P)
 2. \<Turnstile>\<^sub>p {wlp S P} S {P}
 3. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
show qpWP: "is_quantum_predicate (wlp S P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S P)
[PROOF STEP]
using wlp_close assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp ?S ?P)
well_com S
is_quantum_predicate P

goal (1 subgoal):
 1. is_quantum_predicate (wlp S P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp S P)

goal (2 subgoals):
 1. \<Turnstile>\<^sub>p {wlp S P} S {P}
 2. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
have eq: "trace (wlp S P * \<rho>) = trace (P * (denote S \<rho>)) + trace \<rho> - trace (denote S \<rho>)" if dsr: "\<rho> \<in> density_states" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (wlp S P * \<rho>) = trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)
[PROOF STEP]
using wlp_soundness assms dsr
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<forall>\<rho>\<in>density_states. trace (wlp ?S ?P * \<rho>) = trace (?P * denote ?S \<rho>) + trace \<rho> - trace (denote ?S \<rho>)
well_com S
is_quantum_predicate P
\<rho> \<in> density_states

goal (1 subgoal):
 1. trace (wlp S P * \<rho>) = trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?\<rho> \<in> density_states \<Longrightarrow> trace (wlp S P * ?\<rho>) = trace (P * denote S ?\<rho>) + trace ?\<rho> - trace (denote S ?\<rho>)

goal (2 subgoals):
 1. \<Turnstile>\<^sub>p {wlp S P} S {P}
 2. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?\<rho> \<in> density_states \<Longrightarrow> trace (wlp S P * ?\<rho>) = trace (P * denote S ?\<rho>) + trace ?\<rho> - trace (denote S ?\<rho>)
[PROOF STEP]
show "\<Turnstile>\<^sub>p {wlp S P} S {P}"
[PROOF STATE]
proof (prove)
using this:
?\<rho> \<in> density_states \<Longrightarrow> trace (wlp S P * ?\<rho>) = trace (P * denote S ?\<rho>) + trace ?\<rho> - trace (denote S ?\<rho>)

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {wlp S P} S {P}
[PROOF STEP]
unfolding hoare_partial_correct_def
[PROOF STATE]
proof (prove)
using this:
?\<rho> \<in> density_states \<Longrightarrow> trace (wlp S P * ?\<rho>) = trace (P * denote S ?\<rho>) + trace ?\<rho> - trace (denote S ?\<rho>)

goal (1 subgoal):
 1. \<forall>\<rho>\<in>density_states. trace (wlp S P * \<rho>) \<le> trace (P * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {wlp S P} S {P}

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
fix Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
assume qpQ: "is_quantum_predicate Q" and p: "\<Turnstile>\<^sub>p {Q} S {P}"
[PROOF STATE]
proof (state)
this:
is_quantum_predicate Q
\<Turnstile>\<^sub>p {Q} S {P}

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
is_quantum_predicate Q
\<Turnstile>\<^sub>p {Q} S {P}

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
fix \<rho>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
assume dsr: "\<rho> \<in> density_states"
[PROOF STATE]
proof (state)
this:
\<rho> \<in> density_states

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> \<in> density_states
[PROOF STEP]
have "trace (Q * \<rho>) \<le> trace (P * (denote S \<rho>)) + trace \<rho> - trace (denote S \<rho>)"
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states

goal (1 subgoal):
 1. trace (Q * \<rho>) \<le> trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)
[PROOF STEP]
using hoare_partial_correct_def p
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states
(\<Turnstile>\<^sub>p {?P} ?S {?Q}) = (\<forall>\<rho>\<in>density_states. trace (?P * \<rho>) \<le> trace (?Q * denote ?S \<rho>) + (trace \<rho> - trace (denote ?S \<rho>)))
\<Turnstile>\<^sub>p {Q} S {P}

goal (1 subgoal):
 1. trace (Q * \<rho>) \<le> trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)
[PROOF STEP]
by (auto simp: less_eq_complex_def)
[PROOF STATE]
proof (state)
this:
trace (Q * \<rho>) \<le> trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (Q * \<rho>) \<le> trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)
[PROOF STEP]
have "trace (Q * \<rho>) \<le> trace (wlp S P * \<rho>)"
[PROOF STATE]
proof (prove)
using this:
trace (Q * \<rho>) \<le> trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)

goal (1 subgoal):
 1. trace (Q * \<rho>) \<le> trace (wlp S P * \<rho>)
[PROOF STEP]
using eq[symmetric] dsr
[PROOF STATE]
proof (prove)
using this:
trace (Q * \<rho>) \<le> trace (P * denote S \<rho>) + trace \<rho> - trace (denote S \<rho>)
?\<rho> \<in> density_states \<Longrightarrow> trace (P * denote S ?\<rho>) + trace ?\<rho> - trace (denote S ?\<rho>) = trace (wlp S P * ?\<rho>)
\<rho> \<in> density_states

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (Q * ?\<rho>2) \<le> trace (wlp S P * ?\<rho>2)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>is_quantum_predicate Q; \<Turnstile>\<^sub>p {Q} S {P}\<rbrakk> \<Longrightarrow> Q \<le>\<^sub>L wlp S P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (Q * ?\<rho>2) \<le> trace (wlp S P * ?\<rho>2)
[PROOF STEP]
show "Q \<le>\<^sub>L wlp S P"
[PROOF STATE]
proof (prove)
using this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (Q * ?\<rho>2) \<le> trace (wlp S P * ?\<rho>2)

goal (1 subgoal):
 1. Q \<le>\<^sub>L wlp S P
[PROOF STEP]
using lowner_le_trace density_states_def qpQ qpWP is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (Q * ?\<rho>2) \<le> trace (wlp S P * ?\<rho>2)
\<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>))
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
is_quantum_predicate Q
is_quantum_predicate (wlp S P)
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. Q \<le>\<^sub>L wlp S P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<le>\<^sub>L wlp S P

goal:
No subgoals!
[PROOF STEP]
qed