[STATEMENT]
lemma qps_after_measure_is_qp:
  assumes m: "measurement d n M " and qpk: "\<And>k. k < n \<Longrightarrow> is_quantum_predicate (P k)"
  shows "is_quantum_predicate (matrix_sum d (\<lambda>k. adjoint (M k) * P k  * M k) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
[PROOF STEP]
unfolding is_quantum_predicate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d \<and> positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n) \<and> matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d
 2. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 3. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have dMk: "k < n \<Longrightarrow> M k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> M k \<in> carrier_mat d d
[PROOF STEP]
using m measurement_def
[PROOF STATE]
proof (prove)
using this:
measurement d n 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)

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

goal (3 subgoals):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d
 2. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 3. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d

goal (3 subgoals):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d
 2. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 3. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have dPk: "k < n \<Longrightarrow> P k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> P k \<in> carrier_mat d d
[PROOF STEP]
using qpk is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> is_quantum_predicate (P ?k)
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. k < n \<Longrightarrow> P k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> P ?k \<in> carrier_mat d d

goal (3 subgoals):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d
 2. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 3. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> P ?k \<in> carrier_mat d d
[PROOF STEP]
have dk: "k < n \<Longrightarrow> adjoint (M k) * P k  * M k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> P ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * P k * M k \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> adjoint (M ?k) * P ?k * M ?k \<in> carrier_mat d d

goal (3 subgoals):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d
 2. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 3. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> adjoint (M ?k) * P ?k * M ?k \<in> carrier_mat d d
[PROOF STEP]
show d: "matrix_sum d (\<lambda>k. adjoint (M k) * P k  * M k) n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> adjoint (M ?k) * P ?k * M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d
[PROOF STEP]
using matrix_sum_dim[of n "\<lambda>k. adjoint (M k) * P k  * M k"]
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> adjoint (M ?k) * P ?k * M ?k \<in> carrier_mat d d
(\<And>k. k < n \<Longrightarrow> adjoint (M k) * P k * M k \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d

goal (2 subgoals):
 1. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 2. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "k < n \<Longrightarrow> positive (P k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (P k)
[PROOF STEP]
using qpk is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> is_quantum_predicate (P ?k)
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. k < n \<Longrightarrow> positive (P k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (P ?k)

goal (2 subgoals):
 1. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 2. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> positive (P ?k)
[PROOF STEP]
have "k < n \<Longrightarrow> positive (adjoint (M k) * P k * M k)" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (P ?k)

goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (adjoint (M k) * P k * M k)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dMk] dPk, simplified adjoint_adjoint]
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (P ?k)
\<lbrakk>?k3 < n; ?k1 < n; positive (P ?k1)\<rbrakk> \<Longrightarrow> positive (adjoint (M ?k3) * P ?k1 * M ?k3)

goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (adjoint (M k) * P k * M k)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * P ?k * M ?k)

goal (2 subgoals):
 1. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
 2. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * P ?k * M ?k)
[PROOF STEP]
show "positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)"
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * P ?k * M ?k)

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
[PROOF STEP]
using matrix_sum_positive dk
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * P ?k * M ?k)
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d; \<And>k. k < ?n \<Longrightarrow> positive (?f k)\<rbrakk> \<Longrightarrow> positive (matrix_sum ?d ?f ?n)
?k < n \<Longrightarrow> adjoint (M ?k) * P ?k * M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "k < n \<Longrightarrow> P k \<le>\<^sub>L 1\<^sub>m d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> P k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using qpk is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> is_quantum_predicate (P ?k)
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. k < n \<Longrightarrow> P k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> P ?k \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> P ?k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "k < n \<Longrightarrow> positive (1\<^sub>m d - P k)" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> P ?k \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (1\<^sub>m d - P k)
[PROOF STEP]
using lowner_le_def
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> P ?k \<le>\<^sub>L 1\<^sub>m d
(?A \<le>\<^sub>L ?B) = (dim_row ?A = dim_row ?B \<and> dim_col ?A = dim_col ?B \<and> positive (?B - ?A))

goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (1\<^sub>m d - P k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (1\<^sub>m d - P ?k)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> positive (1\<^sub>m d - P ?k)
[PROOF STEP]
have p: "k < n \<Longrightarrow> positive (adjoint (M k) * (1\<^sub>m d - P k) * M k)" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (1\<^sub>m d - P ?k)

goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (adjoint (M k) * (1\<^sub>m d - P k) * M k)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dMk], simplified adjoint_adjoint, of _ "1\<^sub>m d - P k"] dPk
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (1\<^sub>m d - P ?k)
\<lbrakk>?k2 < n; 1\<^sub>m d - P k \<in> carrier_mat d d; positive (1\<^sub>m d - P k)\<rbrakk> \<Longrightarrow> positive (adjoint (M ?k2) * (1\<^sub>m d - P k) * M ?k2)
?k < n \<Longrightarrow> P ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (adjoint (M k) * (1\<^sub>m d - P k) * M k)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * (1\<^sub>m d - P ?k) * M ?k)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * (1\<^sub>m d - P ?k) * M ?k)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
assume k: "k < n"
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "adjoint (M k) * (1\<^sub>m d - P k) * M k = adjoint (M k) * M k - adjoint (M k) * P k * M k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (M k) * (1\<^sub>m d - P k) * M k = adjoint (M k) * M k - adjoint (M k) * P k * M k
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. P k \<in> carrier_mat d d
 2. M k \<in> carrier_mat d d
 3. 1\<^sub>m d \<in> carrier_mat d d
[PROOF STEP]
using dMk dPk k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> P ?k \<in> carrier_mat d d
k < n

goal (3 subgoals):
 1. P k \<in> carrier_mat d d
 2. M k \<in> carrier_mat d d
 3. 1\<^sub>m d \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint (M k) * (1\<^sub>m d - P k) * M k = adjoint (M k) * M k - adjoint (M k) * P k * M k

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?k2 < n \<Longrightarrow> adjoint (M ?k2) * (1\<^sub>m d - P ?k2) * M ?k2 = adjoint (M ?k2) * M ?k2 - adjoint (M ?k2) * P ?k2 * M ?k2

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
note split = this
[PROOF STATE]
proof (state)
this:
?k2 < n \<Longrightarrow> adjoint (M ?k2) * (1\<^sub>m d - P ?k2) * M ?k2 = adjoint (M ?k2) * M ?k2 - adjoint (M ?k2) * P ?k2 * M ?k2

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have dk': "k < n \<Longrightarrow> adjoint (M k) * M k - adjoint (M k) * P k * M k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * M k - adjoint (M k) * P k * M k \<in> carrier_mat d d
[PROOF STEP]
using dMk dPk
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> P ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * M k - adjoint (M k) * P k * M k \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> adjoint (M ?k) * M ?k - adjoint (M ?k) * P ?k * M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "k < n \<Longrightarrow> positive (adjoint (M k) * M k - adjoint (M k) * P k * M k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (adjoint (M k) * M k - adjoint (M k) * P k * M k)
[PROOF STEP]
using p split
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * (1\<^sub>m d - P ?k) * M ?k)
?k2 < n \<Longrightarrow> adjoint (M ?k2) * (1\<^sub>m d - P ?k2) * M ?k2 = adjoint (M ?k2) * M ?k2 - adjoint (M ?k2) * P ?k2 * M ?k2

goal (1 subgoal):
 1. k < n \<Longrightarrow> positive (adjoint (M k) * M k - adjoint (M k) * P k * M k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * M ?k - adjoint (M ?k) * P ?k * M ?k)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * M ?k - adjoint (M ?k) * P ?k * M ?k)
[PROOF STEP]
have p': "positive (matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)"
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * M ?k - adjoint (M ?k) * P ?k * M ?k)

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)
[PROOF STEP]
using matrix_sum_positive[OF dk', of n id, simplified]
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> positive (adjoint (M ?k) * M ?k - adjoint (M ?k) * P ?k * M ?k)
(\<And>k. k < n \<Longrightarrow> positive (adjoint (M k) * M k - adjoint (M k) * P k * M k)) \<Longrightarrow> positive (matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)

goal (1 subgoal):
 1. positive (matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have daMMk: "k < n \<Longrightarrow> adjoint (M k) * M k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * M k \<in> carrier_mat d d
[PROOF STEP]
using dMk
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * M k \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> adjoint (M ?k) * M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have daMPMk: "k < n \<Longrightarrow> adjoint (M k) * P k * M k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * P k * M k \<in> carrier_mat d d
[PROOF STEP]
using dMk dPk
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> P ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * P k * M k \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> adjoint (M ?k) * P ?k * M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n
    = matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n = matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n
[PROOF STEP]
using matrix_sum_minus_distrib[OF daMMk daMPMk]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> ?k2 k < n; \<And>k. k < ?n \<Longrightarrow> ?k1 k < n\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. adjoint (M (?k2 k)) * M (?k2 k) - adjoint (M (?k1 k)) * P (?k1 k) * M (?k1 k)) ?n = matrix_sum d (\<lambda>k. adjoint (M (?k2 k)) * M (?k2 k)) ?n - matrix_sum d (\<lambda>k. adjoint (M (?k1 k)) * P (?k1 k) * M (?k1 k)) ?n

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n = matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n = matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n = matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "\<dots> = 1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k  * M k) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n = 1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n
[PROOF STEP]
using m measurement_def
[PROOF STATE]
proof (prove)
using this:
measurement d n 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)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n = 1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. adjoint (M k) * M k) n - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n = 1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n = 1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n
[PROOF STEP]
have "positive (1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n = 1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n

goal (1 subgoal):
 1. positive (1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
[PROOF STEP]
using p'
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n = 1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n
positive (matrix_sum d (\<lambda>k. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)

goal (1 subgoal):
 1. positive (1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
[PROOF STEP]
show "matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using lowner_le_def d
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d - matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n)
(?A \<le>\<^sub>L ?B) = (dim_row ?A = dim_row ?B \<and> dim_col ?A = dim_col ?B \<and> positive (?B - ?A))
matrix_sum d (\<lambda>k. adjoint (M k) * P k * M k) n \<in> carrier_mat d d

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma total_implies_partial:
  assumes S: "well_com S"
    and total: "\<Turnstile>\<^sub>t {P} S {Q}"
  shows "\<Turnstile>\<^sub>p {P} S {Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
have "trace (P * \<rho>) \<le> trace (Q * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))" if \<rho>: "\<rho> \<in> density_states" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (Q * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (Q * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
have "trace (P * \<rho>) \<le> trace (Q * denote S \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (Q * denote S \<rho>)
[PROOF STEP]
using total hoare_total_correct_def \<rho>
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>t {P} S {Q}
(\<Turnstile>\<^sub>t {?P} ?S {?Q}) = (\<forall>\<rho>\<in>density_states. trace (?P * \<rho>) \<le> trace (?Q * denote ?S \<rho>))
\<rho> \<in> density_states

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

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

goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (Q * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
have "trace (denote S \<rho>) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote S \<rho>) \<le> trace \<rho>
[PROOF STEP]
using denote_trace[OF S] \<rho> density_states_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> trace (denote S ?\<rho>) \<le> trace ?\<rho>
\<rho> \<in> density_states
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

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

goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (Q * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (P * \<rho>) \<le> trace (Q * denote S \<rho>)
trace (denote S \<rho>) \<le> trace \<rho>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (P * \<rho>) \<le> trace (Q * denote S \<rho>)
trace (denote S \<rho>) \<le> trace \<rho>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<rho> \<in> density_states \<Longrightarrow> trace (P * ?\<rho>) \<le> trace (Q * denote S ?\<rho>) + (trace ?\<rho> - trace (denote S ?\<rho>))

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

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

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {P} S {Q}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma predicate_prob_positive:
  assumes "0\<^sub>m d d \<le>\<^sub>L P"
    and "\<rho> \<in> density_states"
  shows "0 \<le> trace (P * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> trace (P * \<rho>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> trace (P * \<rho>)
[PROOF STEP]
have "trace (0\<^sub>m d d * \<rho>) \<le> trace (P * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (0\<^sub>m d d * \<rho>) \<le> trace (P * \<rho>)
[PROOF STEP]
apply (rule lowner_le_traceD)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. 0\<^sub>m d d \<in> carrier_mat ?n ?n
 2. P \<in> carrier_mat ?n ?n
 3. \<rho> \<in> carrier_mat ?n ?n
 4. 0\<^sub>m d d \<le>\<^sub>L P
 5. partial_density_operator \<rho>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0\<^sub>m d d \<le>\<^sub>L P
\<rho> \<in> density_states

goal (5 subgoals):
 1. 0\<^sub>m d d \<in> carrier_mat ?n ?n
 2. P \<in> carrier_mat ?n ?n
 3. \<rho> \<in> carrier_mat ?n ?n
 4. 0\<^sub>m d d \<le>\<^sub>L P
 5. partial_density_operator \<rho>
[PROOF STEP]
unfolding lowner_le_def density_states_def
[PROOF STATE]
proof (prove)
using this:
dim_row (0\<^sub>m d d) = dim_row P \<and> dim_col (0\<^sub>m d d) = dim_col P \<and> positive (P - 0\<^sub>m d d)
\<rho> \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

goal (5 subgoals):
 1. 0\<^sub>m d d \<in> carrier_mat ?n ?n
 2. P \<in> carrier_mat ?n ?n
 3. \<rho> \<in> carrier_mat ?n ?n
 4. dim_row (0\<^sub>m d d) = dim_row P \<and> dim_col (0\<^sub>m d d) = dim_col P \<and> positive (P - 0\<^sub>m d d)
 5. partial_density_operator \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (0\<^sub>m d d * \<rho>) \<le> trace (P * \<rho>)

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

goal (1 subgoal):
 1. 0 \<le> trace (P * \<rho>)
[PROOF STEP]
using assms(2) density_states_def
[PROOF STATE]
proof (prove)
using this:
trace (0\<^sub>m d d * \<rho>) \<le> trace (P * \<rho>)
\<rho> \<in> density_states
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma total_pre_zero:
  assumes S: "well_com S"
    and Q: "is_quantum_predicate Q"
  shows "\<Turnstile>\<^sub>t {0\<^sub>m d d} S {Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Turnstile>\<^sub>t {0\<^sub>m d d} S {Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Turnstile>\<^sub>t {0\<^sub>m d d} S {Q}
[PROOF STEP]
have "trace (0\<^sub>m d d * \<rho>) \<le> trace (Q * denote S \<rho>)" if \<rho>: "\<rho> \<in> density_states" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (0\<^sub>m d d * \<rho>) \<le> trace (Q * denote S \<rho>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (0\<^sub>m d d * \<rho>) \<le> trace (Q * denote S \<rho>)
[PROOF STEP]
have 1: "trace (0\<^sub>m d d * \<rho>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (0\<^sub>m d d * \<rho>) = 0
[PROOF STEP]
using \<rho>
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states

goal (1 subgoal):
 1. trace (0\<^sub>m d d * \<rho>) = 0
[PROOF STEP]
unfolding density_states_def
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

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

goal (1 subgoal):
 1. trace (0\<^sub>m d d * \<rho>) \<le> trace (Q * denote S \<rho>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (0\<^sub>m d d * \<rho>) \<le> trace (Q * denote S \<rho>)
[PROOF STEP]
apply (subst 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> trace (Q * denote S \<rho>)
[PROOF STEP]
apply (rule predicate_prob_positive)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0\<^sub>m d d \<le>\<^sub>L Q
 2. denote S \<rho> \<in> density_states
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>m d d \<le>\<^sub>L Q
[PROOF STEP]
apply (simp add: lowner_le_def, subgoal_tac "Q - 0\<^sub>m d d = Q")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Q - 0\<^sub>m d d = Q \<Longrightarrow> d = dim_row Q \<and> d = dim_col Q \<and> positive (Q - 0\<^sub>m d d)
 2. Q - 0\<^sub>m d d = Q
[PROOF STEP]
using Q is_quantum_predicate_def[of Q]
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate Q
is_quantum_predicate Q = (Q \<in> carrier_mat d d \<and> positive Q \<and> Q \<le>\<^sub>L 1\<^sub>m d)

goal (2 subgoals):
 1. Q - 0\<^sub>m d d = Q \<Longrightarrow> d = dim_row Q \<and> d = dim_col Q \<and> positive (Q - 0\<^sub>m d d)
 2. Q - 0\<^sub>m d d = Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote S \<rho> \<in> density_states
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote S \<rho> \<in> density_states
[PROOF STEP]
using denote_density_states \<rho> S
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> density_states; well_com ?S\<rbrakk> \<Longrightarrow> denote ?S ?\<rho> \<in> density_states
\<rho> \<in> density_states
well_com S

goal (1 subgoal):
 1. denote S \<rho> \<in> density_states
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
trace (0\<^sub>m d d * \<rho>) \<le> trace (Q * denote S \<rho>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<rho> \<in> density_states \<Longrightarrow> trace (0\<^sub>m d d * ?\<rho>) \<le> trace (Q * denote S ?\<rho>)

goal (1 subgoal):
 1. \<Turnstile>\<^sub>t {0\<^sub>m d d} S {Q}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?\<rho> \<in> density_states \<Longrightarrow> trace (0\<^sub>m d d * ?\<rho>) \<le> trace (Q * denote S ?\<rho>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<rho> \<in> density_states \<Longrightarrow> trace (0\<^sub>m d d * ?\<rho>) \<le> trace (Q * denote S ?\<rho>)

goal (1 subgoal):
 1. \<Turnstile>\<^sub>t {0\<^sub>m d d} S {Q}
[PROOF STEP]
using hoare_total_correct_def
[PROOF STATE]
proof (prove)
using this:
?\<rho> \<in> density_states \<Longrightarrow> trace (0\<^sub>m d d * ?\<rho>) \<le> trace (Q * denote S ?\<rho>)
(\<Turnstile>\<^sub>t {?P} ?S {?Q}) = (\<forall>\<rho>\<in>density_states. trace (?P * \<rho>) \<le> trace (?Q * denote ?S \<rho>))

goal (1 subgoal):
 1. \<Turnstile>\<^sub>t {0\<^sub>m d d} S {Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>t {0\<^sub>m d d} S {Q}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partial_post_identity:
  assumes S: "well_com S"
    and P: "is_quantum_predicate P"
  shows "\<Turnstile>\<^sub>p {P} S {1\<^sub>m d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {1\<^sub>m d}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {1\<^sub>m d}
[PROOF STEP]
have "trace (P * \<rho>) \<le> trace (1\<^sub>m d * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))" if \<rho>: "\<rho> \<in> density_states" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (1\<^sub>m d * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (1\<^sub>m d * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
have "denote S \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote S \<rho> \<in> carrier_mat d d
[PROOF STEP]
using S denote_dim \<rho> density_states_def
[PROOF STATE]
proof (prove)
using this:
well_com S
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> denote ?S ?\<rho> \<in> carrier_mat d d
\<rho> \<in> density_states
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

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

goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (1\<^sub>m d * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote S \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "trace (1\<^sub>m d * denote S \<rho>) = trace (denote S \<rho>)"
[PROOF STATE]
proof (prove)
using this:
denote S \<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (1\<^sub>m d * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trace (1\<^sub>m d * denote S \<rho>) = trace (denote S \<rho>)

goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (1\<^sub>m d * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
have "trace (P * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)
[PROOF STEP]
apply (rule lowner_le_traceD)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. P \<in> carrier_mat ?n ?n
 2. 1\<^sub>m d \<in> carrier_mat ?n ?n
 3. \<rho> \<in> carrier_mat ?n ?n
 4. P \<le>\<^sub>L 1\<^sub>m d
 5. partial_density_operator \<rho>
[PROOF STEP]
using \<rho>
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> density_states

goal (5 subgoals):
 1. P \<in> carrier_mat ?n ?n
 2. 1\<^sub>m d \<in> carrier_mat ?n ?n
 3. \<rho> \<in> carrier_mat ?n ?n
 4. P \<le>\<^sub>L 1\<^sub>m d
 5. partial_density_operator \<rho>
[PROOF STEP]
unfolding density_states_def
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}

goal (5 subgoals):
 1. P \<in> carrier_mat ?n ?n
 2. 1\<^sub>m d \<in> carrier_mat ?n ?n
 3. \<rho> \<in> carrier_mat ?n ?n
 4. P \<le>\<^sub>L 1\<^sub>m d
 5. partial_density_operator \<rho>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> P \<in> carrier_mat d d
 2. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> P \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using P 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 (2 subgoals):
 1. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> P \<in> carrier_mat d d
 2. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> P \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (P * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)

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

goal (1 subgoal):
 1. trace (P * \<rho>) \<le> trace (1\<^sub>m d * denote S \<rho>) + (trace \<rho> - trace (denote S \<rho>))
[PROOF STEP]
using density_states_def that
[PROOF STATE]
proof (prove)
using this:
trace (1\<^sub>m d * denote S \<rho>) = trace (denote S \<rho>)
trace (P * \<rho>) \<le> trace (1\<^sub>m d * \<rho>)
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
\<rho> \<in> density_states

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<rho> \<in> density_states \<Longrightarrow> trace (P * ?\<rho>) \<le> trace (1\<^sub>m d * denote S ?\<rho>) + (trace ?\<rho> - trace (denote S ?\<rho>))

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {1\<^sub>m d}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?\<rho> \<in> density_states \<Longrightarrow> trace (P * ?\<rho>) \<le> trace (1\<^sub>m d * denote S ?\<rho>) + (trace ?\<rho> - trace (denote S ?\<rho>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<rho> \<in> density_states \<Longrightarrow> trace (P * ?\<rho>) \<le> trace (1\<^sub>m d * denote S ?\<rho>) + (trace ?\<rho> - trace (denote S ?\<rho>))

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {1\<^sub>m d}
[PROOF STEP]
using hoare_partial_correct_def
[PROOF STATE]
proof (prove)
using this:
?\<rho> \<in> density_states \<Longrightarrow> trace (P * ?\<rho>) \<le> trace (1\<^sub>m d * denote S ?\<rho>) + (trace ?\<rho> - trace (denote S ?\<rho>))
(\<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>)))

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {P} S {1\<^sub>m d}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {P} S {1\<^sub>m d}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measurement2_leq_one_mat:
  assumes dP: "P \<in> carrier_mat d d" and dQ: "Q \<in> carrier_mat d d"
    and leP: "P \<le>\<^sub>L 1\<^sub>m d" and leQ: "Q \<le>\<^sub>L 1\<^sub>m d" and m: "measurement d 2 M"
  shows "(adjoint (M 0) * P * (M 0) + adjoint (M 1) * Q * (M 1)) \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
define M0 where "M0 = M 0"
[PROOF STATE]
proof (state)
this:
M0 = M 0

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
define M1 where "M1 = M 1"
[PROOF STATE]
proof (state)
this:
M1 = M 1

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[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 M0_def M1_def measurement_def
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M
M0 = M 0
M1 = M 1
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)

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. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * 1\<^sub>m d * M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * 1\<^sub>m d * M1
[PROOF STEP]
using lowner_le_keep_under_measurement[OF dM1 dQ _ leQ]
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d \<in> carrier_mat d d \<Longrightarrow> adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * 1\<^sub>m d * M1

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

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * 1\<^sub>m d * M1
[PROOF STEP]
have le1: "adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * M1"
[PROOF STATE]
proof (prove)
using this:
adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * 1\<^sub>m d * M1

goal (1 subgoal):
 1. adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * M1
[PROOF STEP]
using dM1 dQ
[PROOF STATE]
proof (prove)
using this:
adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * 1\<^sub>m d * M1
M1 \<in> carrier_mat d d
Q \<in> carrier_mat d d

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

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * 1\<^sub>m d * M0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * 1\<^sub>m d * M0
[PROOF STEP]
using lowner_le_keep_under_measurement[OF dM0 dP _ leP]
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d \<in> carrier_mat d d \<Longrightarrow> adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * 1\<^sub>m d * M0

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

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * 1\<^sub>m d * M0
[PROOF STEP]
have le0: "adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * M0"
[PROOF STATE]
proof (prove)
using this:
adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * 1\<^sub>m d * M0

goal (1 subgoal):
 1. adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * M0
[PROOF STEP]
using dM0 dP
[PROOF STATE]
proof (prove)
using this:
adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * 1\<^sub>m d * M0
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * M0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * M0

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "adjoint M0 * P * M0 + adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M0 * M0 + adjoint M1 * M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M0 * M0 + adjoint M1 * M1
[PROOF STEP]
apply (rule lowner_le_add[of "adjoint M0 * P * M0" d "adjoint M0 * M0" "adjoint M1 * Q * M1" "adjoint M1 * M1"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. adjoint M0 * P * M0 \<in> carrier_mat d d
 2. adjoint M0 * M0 \<in> carrier_mat d d
 3. adjoint M1 * Q * M1 \<in> carrier_mat d d
 4. adjoint M1 * M1 \<in> carrier_mat d d
 5. adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * M0
 6. adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * M1
[PROOF STEP]
using dM0 dP dM1 dQ le0 le1
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d
M1 \<in> carrier_mat d d
Q \<in> carrier_mat d d
adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * M0
adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * M1

goal (6 subgoals):
 1. adjoint M0 * P * M0 \<in> carrier_mat d d
 2. adjoint M0 * M0 \<in> carrier_mat d d
 3. adjoint M1 * Q * M1 \<in> carrier_mat d d
 4. adjoint M1 * M1 \<in> carrier_mat d d
 5. adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * M0
 6. adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M1 * M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint M0 * P * M0 + adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M0 * M0 + adjoint M1 * M1

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
adjoint M0 * P * M0 + adjoint M1 * Q * M1 \<le>\<^sub>L adjoint M0 * M0 + adjoint M1 * M1

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "\<dots> = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * M0 + adjoint M1 * M1 = 1\<^sub>m d
[PROOF STEP]
using m M0_def M1_def measurement_id2
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M
M0 = M 0
M1 = M 1
measurement ?d 2 ?M \<Longrightarrow> adjoint (?M 0) * ?M 0 + adjoint (?M 1) * ?M 1 = 1\<^sub>m ?d

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

goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
adjoint M0 * P * M0 + adjoint M1 * Q * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
show "adjoint M0 * P * M0 + adjoint M1 * Q * M1 \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
adjoint M0 * P * M0 + adjoint M1 * Q * M1 \<le>\<^sub>L 1\<^sub>m d

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_while_n_close:
  assumes close: "\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (WS P)"
    and m: "measurement d 2 M" and qpP: "is_quantum_predicate P"
  shows "is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS 0 P)
 2. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS 0 P)
 2. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS 0 P)
[PROOF STEP]
unfolding wlp_while_n.simps is_quantum_predicate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m d \<in> carrier_mat d d \<and> positive (1\<^sub>m d) \<and> 1\<^sub>m d \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using positive_one[of d] lowner_le_refl[of "1\<^sub>m d"]
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d)
1\<^sub>m d \<in> carrier_mat ?n ?n \<Longrightarrow> 1\<^sub>m d \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. 1\<^sub>m d \<in> carrier_mat d d \<and> positive (1\<^sub>m d) \<and> 1\<^sub>m d \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS 0 P)

goal (1 subgoal):
 1. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)

goal (1 subgoal):
 1. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
define M0 where "M0 = M 0"
[PROOF STATE]
proof (state)
this:
M0 = M 0

goal (1 subgoal):
 1. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
define M1 where "M1 = M 1"
[PROOF STATE]
proof (state)
this:
M1 = M 1

goal (1 subgoal):
 1. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
define W where "W k = wlp_while_n M0 M1 WS k P" for k
[PROOF STATE]
proof (state)
this:
W ?k = wlp_while_n M0 M1 WS ?k P

goal (1 subgoal):
 1. \<And>k. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P) \<Longrightarrow> is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)
[PROOF STEP]
unfolding wlp_while_n.simps is_quantum_predicate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (M 0) * P * M 0 + adjoint (M 1) * WS (wlp_while_n (M 0) (M 1) WS k P) * M 1 \<in> carrier_mat d d \<and> positive (adjoint (M 0) * P * M 0 + adjoint (M 1) * WS (wlp_while_n (M 0) (M 1) WS k P) * M 1) \<and> adjoint (M 0) * P * M 0 + adjoint (M 1) * WS (wlp_while_n (M 0) (M 1) WS k P) * M 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
proof (fold M0_def M1_def, fold W_def, auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
 2. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 3. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[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 M0_def M1_def measurement_def
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M
M0 = M 0
M1 = M 1
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)

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 (3 subgoals):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
 2. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 3. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[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 (3 subgoals):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
 2. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 3. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have qpWk: "is_quantum_predicate (W k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (W k)
[PROOF STEP]
using Suc M0_def M1_def W_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)
M0 = M 0
M1 = M 1
W ?k = wlp_while_n M0 M1 WS ?k P

goal (1 subgoal):
 1. is_quantum_predicate (W k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (W k)

goal (3 subgoals):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
 2. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 3. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (W k)
[PROOF STEP]
have qpWWk: "is_quantum_predicate (WS (W k))"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W k)

goal (1 subgoal):
 1. is_quantum_predicate (WS (W k))
[PROOF STEP]
using close
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W k)
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)

goal (1 subgoal):
 1. is_quantum_predicate (WS (W k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (WS (W k))

goal (3 subgoals):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
 2. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 3. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
from qpWk
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (W k)
[PROOF STEP]
have dWk: "W k \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W k)

goal (1 subgoal):
 1. W k \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W k)
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. W k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W k \<in> carrier_mat d d

goal (3 subgoals):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
 2. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 3. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
from qpWWk
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (WS (W k))
[PROOF STEP]
have dWWk: "WS (W k) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W k))

goal (1 subgoal):
 1. WS (W k) \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W k))
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. WS (W k) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
WS (W k) \<in> carrier_mat d d

goal (3 subgoals):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
 2. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 3. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
show "adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
[PROOF STEP]
using dM0 dP dM1 dWWk
[PROOF STATE]
proof (prove)
using this:
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d
M1 \<in> carrier_mat d d
WS (W k) \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d

goal (2 subgoals):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 2. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have pP: "positive P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive P
[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. positive P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive P

goal (2 subgoals):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 2. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive P
[PROOF STEP]
have pM0P: "positive (adjoint M0 * P * M0)"
[PROOF STATE]
proof (prove)
using this:
positive P

goal (1 subgoal):
 1. positive (adjoint M0 * P * M0)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM0]] dM0 dP adjoint_adjoint[of M0]
[PROOF STATE]
proof (prove)
using this:
positive P
\<lbrakk>?A \<in> carrier_mat d d; positive ?A\<rbrakk> \<Longrightarrow> positive (adjoint M0 * ?A * adjoint (adjoint M0))
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d
adjoint (adjoint M0) = M0

goal (1 subgoal):
 1. positive (adjoint M0 * P * M0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (adjoint M0 * P * M0)

goal (2 subgoals):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 2. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have pWWk: "positive (WS (W k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (WS (W k))
[PROOF STEP]
using qpWWk is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W k))
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. positive (WS (W k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (WS (W k))

goal (2 subgoals):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 2. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (WS (W k))
[PROOF STEP]
have pM1WWk: "positive (adjoint M1 * WS (W k) * M1)"
[PROOF STATE]
proof (prove)
using this:
positive (WS (W k))

goal (1 subgoal):
 1. positive (adjoint M1 * WS (W k) * M1)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM1]] dM1 dWWk adjoint_adjoint[of M1]
[PROOF STATE]
proof (prove)
using this:
positive (WS (W k))
\<lbrakk>?A \<in> carrier_mat d d; positive ?A\<rbrakk> \<Longrightarrow> positive (adjoint M1 * ?A * adjoint (adjoint M1))
M1 \<in> carrier_mat d d
WS (W k) \<in> carrier_mat d d
adjoint (adjoint M1) = M1

goal (1 subgoal):
 1. positive (adjoint M1 * WS (W k) * M1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (adjoint M1 * WS (W k) * M1)

goal (2 subgoals):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
 2. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (adjoint M1 * WS (W k) * M1)
[PROOF STEP]
show "positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)"
[PROOF STATE]
proof (prove)
using this:
positive (adjoint M1 * WS (W k) * M1)

goal (1 subgoal):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
[PROOF STEP]
using positive_add[OF pM0P pM1WWk] dM0 dP dM1 dWWk
[PROOF STATE]
proof (prove)
using this:
positive (adjoint M1 * WS (W k) * M1)
\<lbrakk>adjoint M0 * P * M0 \<in> carrier_mat ?n ?n; adjoint M1 * WS (W k) * M1 \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d
M1 \<in> carrier_mat d d
WS (W k) \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)

goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have leWWk: "WS (W k) \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WS (W k) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using qpWWk is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W k))
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. WS (W k) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
WS (W k) \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have leP: "P \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<le>\<^sub>L 1\<^sub>m 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 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
show "(adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1) \<le>\<^sub>L 1\<^sub>m d "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement2_leq_one_mat[OF dP dWWk leP leWWk m] M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
adjoint (M 0) * P * M 0 + adjoint (M 1) * WS (W k) * M 1 \<le>\<^sub>L 1\<^sub>m d
M0 = M 0
M1 = M 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS (Suc k) P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_while_n_mono:
  assumes "\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (WS P)"
    and "\<And>P Q. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate Q \<Longrightarrow> P \<le>\<^sub>L Q \<Longrightarrow> WS P \<le>\<^sub>L WS Q"
    and "measurement d 2 M"
    and "is_quantum_predicate P"
    and "is_quantum_predicate Q"
    and "P \<le>\<^sub>L Q"
  shows "(wlp_while_n (M 0) (M 1) WS k P) \<le>\<^sub>L (wlp_while_n (M 0) (M 1) WS k Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wlp_while_n (M 0) (M 1) WS 0 P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS 0 Q
 2. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. wlp_while_n (M 0) (M 1) WS 0 P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS 0 Q
 2. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp_while_n (M 0) (M 1) WS 0 P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS 0 Q
[PROOF STEP]
unfolding wlp_while_n.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m d \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using lowner_le_refl[of "1\<^sub>m d"]
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m d \<in> carrier_mat ?n ?n \<Longrightarrow> 1\<^sub>m d \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. 1\<^sub>m d \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
wlp_while_n (M 0) (M 1) WS 0 P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS 0 Q

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
define M0 where "M0 = M 0"
[PROOF STATE]
proof (state)
this:
M0 = M 0

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
define M1 where "M1 = M 1"
[PROOF STATE]
proof (state)
this:
M1 = M 1

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[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 assms M0_def M1_def measurement_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
M0 = M 0
M1 = M 1
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)

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. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
define W where "W P k = wlp_while_n M0 M1 WS k P" for k P
[PROOF STATE]
proof (state)
this:
W ?P ?k = wlp_while_n M0 M1 WS ?k ?P

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have dP: "P \<in> carrier_mat d d" and dQ: "Q \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat d d &&& Q \<in> carrier_mat d d
[PROOF STEP]
using assms is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
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 &&& Q \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat d d
Q \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have eq1: "W P (Suc k) = adjoint M0 * P * M0 + adjoint M1 * (WS (W P k)) * M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W P (Suc k) = adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1
[PROOF STEP]
unfolding W_def wlp_while_n.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (wlp_while_n M0 M1 WS k P) * M1 = adjoint M0 * P * M0 + adjoint M1 * WS (wlp_while_n M0 M1 WS k P) * M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W P (Suc k) = adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have eq2: "W Q (Suc k) = adjoint M0 * Q * M0 + adjoint M1 * (WS (W Q k)) * M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W Q (Suc k) = adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1
[PROOF STEP]
unfolding W_def wlp_while_n.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * Q * M0 + adjoint M1 * WS (wlp_while_n M0 M1 WS k Q) * M1 = adjoint M0 * Q * M0 + adjoint M1 * WS (wlp_while_n M0 M1 WS k Q) * M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W Q (Suc k) = adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have le1: "adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * Q * M0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * Q * M0
[PROOF STEP]
using lowner_le_keep_under_measurement dM0 dP dQ assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n; ?A \<le>\<^sub>L ?B\<rbrakk> \<Longrightarrow> adjoint ?M * ?A * ?M \<le>\<^sub>L adjoint ?M * ?B * ?M
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d
Q \<in> carrier_mat d d
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

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

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have leWk: "(W P k) \<le>\<^sub>L (W Q k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W P k \<le>\<^sub>L W Q k
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q

goal (1 subgoal):
 1. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W P k \<le>\<^sub>L W Q k

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have qpWPk: "is_quantum_predicate (W P k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (W P k)
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)
[PROOF STEP]
using wlp_while_n_close assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (?WS P); measurement d 2 ?M; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp_while_n (?M 0) (?M 1) ?WS ?k ?P)
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (W P k)

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (W P k)
[PROOF STEP]
have "is_quantum_predicate (WS (W P k))"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W P k)

goal (1 subgoal):
 1. is_quantum_predicate (WS (W P k))
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)

goal (1 subgoal):
 1. is_quantum_predicate (WS (wlp_while_n (M 0) (M 1) WS k P))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. is_quantum_predicate (WS (wlp_while_n (M 0) (M 1) WS k P))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (WS (W P k))

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (WS (W P k))
[PROOF STEP]
have dWWPk: "(WS (W P k)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W P k))

goal (1 subgoal):
 1. WS (W P k) \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W P k))
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. WS (W P k) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
WS (W P k) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have qpWQk: "is_quantum_predicate (W Q k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (W Q k)
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k Q)
[PROOF STEP]
using wlp_while_n_close assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (?WS P); measurement d 2 ?M; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp_while_n (?M 0) (?M 1) ?WS ?k ?P)
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (W Q k)

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (W Q k)
[PROOF STEP]
have "is_quantum_predicate (WS (W Q k))"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W Q k)

goal (1 subgoal):
 1. is_quantum_predicate (WS (W Q k))
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k Q)

goal (1 subgoal):
 1. is_quantum_predicate (WS (wlp_while_n (M 0) (M 1) WS k Q))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k Q)
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. is_quantum_predicate (WS (wlp_while_n (M 0) (M 1) WS k Q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (WS (W Q k))

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (WS (W Q k))
[PROOF STEP]
have dWWQk: "(WS (W Q k)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W Q k))

goal (1 subgoal):
 1. WS (W Q k) \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W Q k))
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. WS (W Q k) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
WS (W Q k) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have "(WS (W P k)) \<le>\<^sub>L (WS (W Q k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WS (W P k) \<le>\<^sub>L WS (W Q k)
[PROOF STEP]
using qpWPk qpWQk leWk assms
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W P k)
is_quantum_predicate (W Q k)
W P k \<le>\<^sub>L W Q k
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (WS ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> WS ?P \<le>\<^sub>L WS ?Q
measurement d 2 M
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

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

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
WS (W P k) \<le>\<^sub>L WS (W Q k)
[PROOF STEP]
have le2: "adjoint M1 * (WS (W P k)) * M1 \<le>\<^sub>L adjoint M1 * (WS (W Q k)) * M1"
[PROOF STATE]
proof (prove)
using this:
WS (W P k) \<le>\<^sub>L WS (W Q k)

goal (1 subgoal):
 1. adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M1 * WS (W Q k) * M1
[PROOF STEP]
using lowner_le_keep_under_measurement dM1 dWWPk dWWQk
[PROOF STATE]
proof (prove)
using this:
WS (W P k) \<le>\<^sub>L WS (W Q k)
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n; ?A \<le>\<^sub>L ?B\<rbrakk> \<Longrightarrow> adjoint ?M * ?A * ?M \<le>\<^sub>L adjoint ?M * ?B * ?M
M1 \<in> carrier_mat d d
WS (W P k) \<in> carrier_mat d d
WS (W Q k) \<in> carrier_mat d d

goal (1 subgoal):
 1. adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M1 * WS (W Q k) * M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M1 * WS (W Q k) * M1

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
have "(adjoint M0 * P * M0 + adjoint M1 * (WS (W P k)) * M1) \<le>\<^sub>L (adjoint M0 * Q * M0 + adjoint M1 * (WS (W Q k)) * M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1
[PROOF STEP]
using lowner_le_add[OF _ _ _ _ le1 le2] dM0 dP dM1 dQ dWWPk dWWQk le1 le2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>adjoint M0 * P * M0 \<in> carrier_mat ?n ?n; adjoint M0 * Q * M0 \<in> carrier_mat ?n ?n; adjoint M1 * WS (W P k) * M1 \<in> carrier_mat ?n ?n; adjoint M1 * WS (W Q k) * M1 \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1
M0 \<in> carrier_mat d d
P \<in> carrier_mat d d
M1 \<in> carrier_mat d d
Q \<in> carrier_mat d d
WS (W P k) \<in> carrier_mat d d
WS (W Q k) \<in> carrier_mat d d
adjoint M0 * P * M0 \<le>\<^sub>L adjoint M0 * Q * M0
adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M1 * WS (W Q k) * M1

goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1
[PROOF STEP]
have "W P (Suc k) \<le>\<^sub>L W Q (Suc k)"
[PROOF STATE]
proof (prove)
using this:
adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1

goal (1 subgoal):
 1. W P (Suc k) \<le>\<^sub>L W Q (Suc k)
[PROOF STEP]
using eq1 eq2
[PROOF STATE]
proof (prove)
using this:
adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1 \<le>\<^sub>L adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1
W P (Suc k) = adjoint M0 * P * M0 + adjoint M1 * WS (W P k) * M1
W Q (Suc k) = adjoint M0 * Q * M0 + adjoint M1 * WS (W Q k) * M1

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

goal (1 subgoal):
 1. \<And>k. wlp_while_n (M 0) (M 1) WS k P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q \<Longrightarrow> wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W P (Suc k) \<le>\<^sub>L W Q (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
W P (Suc k) \<le>\<^sub>L W Q (Suc k)

goal (1 subgoal):
 1. wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q

goal (1 subgoal):
 1. wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp_while_n (M 0) (M 1) WS (Suc k) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS (Suc k) Q

goal:
No subgoals!
[PROOF STEP]
qed