Theory Quantum_Hoare
section ‹Partial and total correctness›
theory Quantum_Hoare
imports Quantum_Program
begin
context state_sig
begin
definition density_states :: "state set" where
"density_states = {ρ ∈ carrier_mat d d. partial_density_operator ρ}"
lemma denote_density_states:
"ρ ∈ density_states ⟹ well_com S ⟹ denote S ρ ∈ density_states"
by (simp add: denote_dim_pdo density_states_def)
definition is_quantum_predicate :: "complex mat ⇒ bool" where
"is_quantum_predicate P ⟷ P ∈ carrier_mat d d ∧ positive P ∧ P ≤⇩L 1⇩m d"
lemma trace_measurement2:
assumes m: "measurement n 2 M" and dA: "A ∈ carrier_mat n n"
shows "trace ((M 0) * A * adjoint (M 0)) + trace ((M 1) * A * adjoint (M 1)) = trace A"
proof -
from m have dM0: "M 0 ∈ carrier_mat n n" and dM1: "M 1 ∈ carrier_mat n n" and id: "adjoint (M 0) * (M 0) + adjoint (M 1) * (M 1) = 1⇩m n"
using measurement_def measurement_id2 by auto
have "trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0))
= trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A)"
using dM0 dM1 dA by (mat_assoc n)
also have "… = trace (1⇩m n * A)" using id by auto
also have "… = trace A" using dA by auto
finally show ?thesis
using dA dM0 dM1 local.id state_sig.trace_measure2_id by blast
qed
lemma qp_close_under_unitary_operator:
fixes U P :: "complex mat"
assumes dU: "U ∈ carrier_mat d d"
and u: "unitary U"
and qp: "is_quantum_predicate P"
shows "is_quantum_predicate (adjoint U * P * U)"
unfolding is_quantum_predicate_def
proof (auto)
have dP: "P ∈ carrier_mat d d" using qp is_quantum_predicate_def by auto
show "adjoint U * P * U ∈ carrier_mat d d" using dU dP by fastforce
have "positive P" using qp is_quantum_predicate_def by auto
then show "positive (adjoint U * P * U)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dU] dP, simplified adjoint_adjoint] by fastforce
have "adjoint U * U = 1⇩m d" apply (subgoal_tac "inverts_mat (adjoint U) U")
subgoal unfolding inverts_mat_def using dU by auto
using u unfolding unitary_def using inverts_mat_symm[OF dU adjoint_dim[OF dU]] by auto
then have u': "adjoint U * 1⇩m d * U = 1⇩m d" using dU by auto
have le: "P ≤⇩L 1⇩m d" using qp is_quantum_predicate_def by auto
show "adjoint U * P * U ≤⇩L 1⇩m d"
using lowner_le_keep_under_measurement[OF dU dP one_carrier_mat le] u' by auto
qed
lemma qps_after_measure_is_qp:
assumes m: "measurement d n M " and qpk: "⋀k. k < n ⟹ is_quantum_predicate (P k)"
shows "is_quantum_predicate (matrix_sum d (λk. adjoint (M k) * P k * M k) n)"
unfolding is_quantum_predicate_def
proof (auto)
have dMk: "k < n ⟹ M k ∈ carrier_mat d d" for k using m measurement_def by auto
moreover have dPk: "k < n ⟹ P k ∈ carrier_mat d d" for k using qpk is_quantum_predicate_def by auto
ultimately have dk: "k < n ⟹ adjoint (M k) * P k * M k ∈ carrier_mat d d" for k by fastforce
then show d: "matrix_sum d (λk. adjoint (M k) * P k * M k) n ∈ carrier_mat d d"
using matrix_sum_dim[of n "λk. adjoint (M k) * P k * M k"] by auto
have "k < n ⟹ positive (P k)" for k using qpk is_quantum_predicate_def by auto
then have "k < n ⟹ positive (adjoint (M k) * P k * M k)" for k
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dMk] dPk, simplified adjoint_adjoint] by fastforce
then show "positive (matrix_sum d (λk. adjoint (M k) * P k * M k) n)" using matrix_sum_positive dk by auto
have "k < n ⟹ P k ≤⇩L 1⇩m d" for k using qpk is_quantum_predicate_def by auto
then have "k < n ⟹ positive (1⇩m d - P k)" for k using lowner_le_def by auto
then have p: "k < n ⟹ positive (adjoint (M k) * (1⇩m d - P k) * M k)" for k
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dMk], simplified adjoint_adjoint, of _ "1⇩m d - P k"] dPk by fastforce
{
fix k assume k: "k < n"
have "adjoint (M k) * (1⇩m d - P k) * M k = adjoint (M k) * M k - adjoint (M k) * P k * M k"
apply (mat_assoc d) using dMk dPk k by auto
}
note split = this
have dk': "k < n ⟹ adjoint (M k) * M k - adjoint (M k) * P k * M k ∈ carrier_mat d d" for k using dMk dPk by fastforce
have "k < n ⟹ positive (adjoint (M k) * M k - adjoint (M k) * P k * M k)" for k using p split by auto
then have p': "positive (matrix_sum d (λk. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)"
using matrix_sum_positive[OF dk', of n id, simplified] by auto
have daMMk: "k < n ⟹ adjoint (M k) * M k ∈ carrier_mat d d" for k using dMk by fastforce
have daMPMk: "k < n ⟹ adjoint (M k) * P k * M k ∈ carrier_mat d d" for k using dMk dPk by fastforce
have "matrix_sum d (λk. adjoint (M k) * M k - adjoint (M k) * P k * M k) n
= matrix_sum d (λk. adjoint (M k) * M k) n - matrix_sum d (λk. adjoint (M k) * P k * M k) n"
using matrix_sum_minus_distrib[OF daMMk daMPMk] by auto
also have "… = 1⇩m d - matrix_sum d (λk. adjoint (M k) * P k * M k) n" using m measurement_def by auto
finally have "positive (1⇩m d - matrix_sum d (λk. adjoint (M k) * P k * M k) n)" using p' by auto
then show "matrix_sum d (λk. adjoint (M k) * P k * M k) n ≤⇩L 1⇩m d" using lowner_le_def d by auto
qed
definition hoare_total_correct :: "complex mat ⇒ com ⇒ complex mat ⇒ bool" ("⊨⇩t {(1_)}/ (_)/ {(1_)}" 50) where
"⊨⇩t {P} S {Q} ⟷ (∀ρ∈density_states. trace (P * ρ) ≤ trace (Q * denote S ρ))"
definition hoare_partial_correct :: "complex mat ⇒ com ⇒ complex mat ⇒ bool" ("⊨⇩p {(1_)}/ (_)/ {(1_)}" 50) where
"⊨⇩p {P} S {Q} ⟷ (∀ρ∈density_states. trace (P * ρ) ≤ trace (Q * denote S ρ) + (trace ρ - trace (denote S ρ)))"
lemma total_implies_partial:
assumes S: "well_com S"
and total: "⊨⇩t {P} S {Q}"
shows "⊨⇩p {P} S {Q}"
proof -
have "trace (P * ρ) ≤ trace (Q * denote S ρ) + (trace ρ - trace (denote S ρ))" if ρ: "ρ ∈ density_states" for ρ
proof -
have "trace (P * ρ) ≤ trace (Q * denote S ρ)"
using total hoare_total_correct_def ρ by auto
moreover have "trace (denote S ρ) ≤ trace ρ"
using denote_trace[OF S] ρ density_states_def by auto
ultimately show ?thesis by (auto simp: less_eq_complex_def)
qed
then show ?thesis
using hoare_partial_correct_def by auto
qed
lemma predicate_prob_positive:
assumes "0⇩m d d ≤⇩L P"
and "ρ ∈ density_states"
shows "0 ≤ trace (P * ρ)"
proof -
have "trace (0⇩m d d * ρ) ≤ trace (P * ρ)"
apply (rule lowner_le_traceD)
using assms unfolding lowner_le_def density_states_def by auto
then show ?thesis
using assms(2) density_states_def by auto
qed
lemma total_pre_zero:
assumes S: "well_com S"
and Q: "is_quantum_predicate Q"
shows "⊨⇩t {0⇩m d d} S {Q}"
proof -
have "trace (0⇩m d d * ρ) ≤ trace (Q * denote S ρ)" if ρ: "ρ ∈ density_states" for ρ
proof -
have 1: "trace (0⇩m d d * ρ) = 0"
using ρ unfolding density_states_def by auto
show ?thesis
apply (subst 1)
apply (rule predicate_prob_positive)
subgoal apply (simp add: lowner_le_def, subgoal_tac "Q - 0⇩m d d = Q") using Q is_quantum_predicate_def[of Q] by auto
subgoal using denote_density_states ρ S by auto
done
qed
then show ?thesis
using hoare_total_correct_def by auto
qed
lemma partial_post_identity:
assumes S: "well_com S"
and P: "is_quantum_predicate P"
shows "⊨⇩p {P} S {1⇩m d}"
proof -
have "trace (P * ρ) ≤ trace (1⇩m d * denote S ρ) + (trace ρ - trace (denote S ρ))" if ρ: "ρ ∈ density_states" for ρ
proof -
have "denote S ρ ∈ carrier_mat d d"
using S denote_dim ρ density_states_def by auto
then have "trace (1⇩m d * denote S ρ) = trace (denote S ρ)"
by auto
moreover have "trace (P * ρ) ≤ trace (1⇩m d * ρ)"
apply (rule lowner_le_traceD)
using ρ unfolding density_states_def apply auto
using P is_quantum_predicate_def by auto
ultimately show ?thesis
using density_states_def that by auto
qed
then show ?thesis
using hoare_partial_correct_def by auto
qed
subsection ‹Weakest liberal preconditions›
definition is_weakest_liberal_precondition :: "complex mat ⇒ com ⇒ complex mat ⇒ bool" where
"is_weakest_liberal_precondition W S P ⟷
is_quantum_predicate W ∧ ⊨⇩p {W} S {P} ∧ (∀Q. is_quantum_predicate Q ⟶ ⊨⇩p {Q} S {P} ⟶ Q ≤⇩L W)"
definition wlp_measure :: "nat ⇒ (nat ⇒ complex mat) ⇒ ((complex mat ⇒ complex mat) list) ⇒ complex mat ⇒ complex mat" where
"wlp_measure n M WS P = matrix_sum d (λk. adjoint (M k) * ((WS!k) P) * (M k)) n"
fun wlp_while_n :: "complex mat ⇒ complex mat ⇒ (complex mat ⇒ complex mat) ⇒ nat ⇒ complex mat ⇒ complex mat" where
"wlp_while_n M0 M1 WS 0 P = 1⇩m d"
| "wlp_while_n M0 M1 WS (Suc n) P = adjoint M0 * P * M0 + adjoint M1 * (WS (wlp_while_n M0 M1 WS n P)) * M1"
lemma measurement2_leq_one_mat:
assumes dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d"
and leP: "P ≤⇩L 1⇩m d" and leQ: "Q ≤⇩L 1⇩m d" and m: "measurement d 2 M"
shows "(adjoint (M 0) * P * (M 0) + adjoint (M 1) * Q * (M 1)) ≤⇩L 1⇩m d"
proof -
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m M0_def M1_def measurement_def by auto
have "adjoint M1 * Q * M1 ≤⇩L adjoint M1 * 1⇩m d * M1"
using lowner_le_keep_under_measurement[OF dM1 dQ _ leQ] by auto
then have le1: "adjoint M1 * Q * M1 ≤⇩L adjoint M1 * M1" using dM1 dQ by fastforce
have "adjoint M0 * P * M0 ≤⇩L adjoint M0 * 1⇩m d * M0"
using lowner_le_keep_under_measurement[OF dM0 dP _ leP] by auto
then have le0: "adjoint M0 * P * M0 ≤⇩L adjoint M0 * M0"
using dM0 dP by fastforce
have "adjoint M0 * P * M0 + adjoint M1 * Q * M1 ≤⇩L adjoint M0 * M0 + adjoint M1 * M1"
apply (rule lowner_le_add[of "adjoint M0 * P * M0" d "adjoint M0 * M0" "adjoint M1 * Q * M1" "adjoint M1 * M1"])
using dM0 dP dM1 dQ le0 le1 by auto
also have "… = 1⇩m d" using m M0_def M1_def measurement_id2 by auto
finally show "adjoint M0 * P * M0 + adjoint M1 * Q * M1 ≤⇩L 1⇩m d".
qed
lemma wlp_while_n_close:
assumes close: "⋀P. is_quantum_predicate P ⟹ 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 (induct k)
case 0
then show ?case
unfolding wlp_while_n.simps is_quantum_predicate_def using positive_one[of d] lowner_le_refl[of "1⇩m d"] by fastforce
next
case (Suc k)
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
define W where "W k = wlp_while_n M0 M1 WS k P" for k
show ?case unfolding wlp_while_n.simps is_quantum_predicate_def
proof (fold M0_def M1_def, fold W_def, auto)
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m M0_def M1_def measurement_def by auto
have dP: "P ∈ carrier_mat d d" using qpP is_quantum_predicate_def by auto
have qpWk: "is_quantum_predicate (W k)" using Suc M0_def M1_def W_def by auto
then have qpWWk: "is_quantum_predicate (WS (W k))" using close by auto
from qpWk have dWk: "W k ∈ carrier_mat d d" using is_quantum_predicate_def by auto
from qpWWk have dWWk: "WS (W k) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
show "adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 ∈ carrier_mat d d" using dM0 dP dM1 dWWk by auto
have pP: "positive P" using qpP is_quantum_predicate_def by auto
then have pM0P: "positive (adjoint M0 * P * M0)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM0]] dM0 dP adjoint_adjoint[of M0] by auto
have pWWk: "positive (WS (W k))" using qpWWk is_quantum_predicate_def by auto
then have pM1WWk: "positive (adjoint M1 * WS (W k) * M1)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM1]] dM1 dWWk adjoint_adjoint[of M1] by auto
then show "positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)"
using positive_add[OF pM0P pM1WWk] dM0 dP dM1 dWWk by fastforce
have leWWk: "WS (W k) ≤⇩L 1⇩m d" using qpWWk is_quantum_predicate_def by auto
have leP: "P ≤⇩L 1⇩m d" using qpP is_quantum_predicate_def by auto
show "(adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1) ≤⇩L 1⇩m d "
using measurement2_leq_one_mat[OF dP dWWk leP leWWk m] M0_def M1_def by auto
qed
qed
lemma wlp_while_n_mono:
assumes "⋀P. is_quantum_predicate P ⟹ is_quantum_predicate (WS P)"
and "⋀P Q. is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ WS P ≤⇩L WS Q"
and "measurement d 2 M"
and "is_quantum_predicate P"
and "is_quantum_predicate Q"
and "P ≤⇩L Q"
shows "(wlp_while_n (M 0) (M 1) WS k P) ≤⇩L (wlp_while_n (M 0) (M 1) WS k Q)"
proof (induct k)
case 0
then show ?case unfolding wlp_while_n.simps using lowner_le_refl[of "1⇩m d"] by fastforce
next
case (Suc k)
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using assms M0_def M1_def measurement_def by auto
define W where "W P k = wlp_while_n M0 M1 WS k P" for k P
have dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d" using assms is_quantum_predicate_def by auto
have eq1: "W P (Suc k) = adjoint M0 * P * M0 + adjoint M1 * (WS (W P k)) * M1" unfolding W_def wlp_while_n.simps by auto
have eq2: "W Q (Suc k) = adjoint M0 * Q * M0 + adjoint M1 * (WS (W Q k)) * M1" unfolding W_def wlp_while_n.simps by auto
have le1: "adjoint M0 * P * M0 ≤⇩L adjoint M0 * Q * M0" using lowner_le_keep_under_measurement dM0 dP dQ assms by auto
have leWk: "(W P k) ≤⇩L (W Q k)" unfolding W_def M0_def M1_def using Suc by auto
have qpWPk: "is_quantum_predicate (W P k)" unfolding W_def M0_def M1_def using wlp_while_n_close assms by auto
then have "is_quantum_predicate (WS (W P k))" unfolding W_def M0_def M1_def using assms by auto
then have dWWPk: "(WS (W P k)) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have qpWQk: "is_quantum_predicate (W Q k)" unfolding W_def M0_def M1_def using wlp_while_n_close assms by auto
then have "is_quantum_predicate (WS (W Q k))" unfolding W_def M0_def M1_def using assms by auto
then have dWWQk: "(WS (W Q k)) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "(WS (W P k)) ≤⇩L (WS (W Q k))" using qpWPk qpWQk leWk assms by auto
then have le2: "adjoint M1 * (WS (W P k)) * M1 ≤⇩L adjoint M1 * (WS (W Q k)) * M1"
using lowner_le_keep_under_measurement dM1 dWWPk dWWQk by auto
have "(adjoint M0 * P * M0 + adjoint M1 * (WS (W P k)) * M1) ≤⇩L (adjoint M0 * Q * M0 + adjoint M1 * (WS (W Q k)) * M1)"
using lowner_le_add[OF _ _ _ _ le1 le2] dM0 dP dM1 dQ dWWPk dWWQk le1 le2 by fastforce
then have "W P (Suc k) ≤⇩L W Q (Suc k)" using eq1 eq2 by auto
then show ?case unfolding W_def M0_def M1_def by auto
qed
definition wlp_while :: "complex mat ⇒ complex mat ⇒ (complex mat ⇒ complex mat) ⇒ complex mat ⇒ complex mat" where
"wlp_while M0 M1 WS P = (THE Q. limit_mat (λn. wlp_while_n M0 M1 WS n P) Q d)"
lemma wlp_while_exists:
assumes "⋀P. is_quantum_predicate P ⟹ is_quantum_predicate (WS P)"
and "⋀P Q. is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ WS P ≤⇩L WS Q"
and m: "measurement d 2 M"
and qpP: "is_quantum_predicate P"
shows "is_quantum_predicate (wlp_while (M 0) (M 1) WS P)
∧ (∀n. (wlp_while (M 0) (M 1) WS P) ≤⇩L (wlp_while_n (M 0) (M 1) WS n P))
∧ (∀W'. (∀n. W' ≤⇩L (wlp_while_n (M 0) (M 1) WS n P)) ⟶ W' ≤⇩L (wlp_while (M 0) (M 1) WS P))
∧ limit_mat (λn. wlp_while_n (M 0) (M 1) WS n P) (wlp_while (M 0) (M 1) WS P) d"
proof (auto)
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using assms M0_def M1_def measurement_def by auto
define W where "W k = wlp_while_n M0 M1 WS k P" for k
have leP: "P ≤⇩L 1⇩m d" and dP: "P ∈ carrier_mat d d" and pP: "positive P" using qpP is_quantum_predicate_def by auto
have pM0P: "positive (adjoint M0 * P * M0)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM0]] adjoint_adjoint[of "M0"] dP pP by auto
have le_qp: "W (Suc k) ≤⇩L W k ∧ is_quantum_predicate (W k)" for k
proof (induct k)
case 0
have "is_quantum_predicate (1⇩m d)"
unfolding is_quantum_predicate_def using positive_one lowner_le_refl[of "1⇩m d"] by fastforce
then have "is_quantum_predicate (WS (1⇩m d))" using assms by auto
then have "(WS (1⇩m d)) ∈ carrier_mat d d" and "(WS (1⇩m d)) ≤⇩L 1⇩m d" using is_quantum_predicate_def by auto
then have "W 1 ≤⇩L W 0" unfolding W_def wlp_while_n.simps M0_def M1_def
using measurement2_leq_one_mat[OF dP _ leP _ m] by auto
moreover have "is_quantum_predicate (W 0)" unfolding W_def wlp_while_n.simps is_quantum_predicate_def
using positive_one lowner_le_refl[of "1⇩m d"] by fastforce
ultimately show ?case by auto
next
case (Suc k)
then have leWSk: "W (Suc k) ≤⇩L W k" and qpWk: "is_quantum_predicate (W k)" by auto
then have "is_quantum_predicate (WS (W k))" using assms by auto
then have dWWk: "WS (W k) ∈ carrier_mat d d" and leWWk1: "(WS (W k)) ≤⇩L 1⇩m d" and pWWk: "positive (WS (W k))"
using is_quantum_predicate_def by auto
then have leWSk1: "W (Suc k) ≤⇩L 1⇩m d" using measurement2_leq_one_mat[OF dP dWWk leP leWWk1 m]
unfolding W_def wlp_while_n.simps M0_def M1_def by auto
then have dWSk: "W (Suc k) ∈ carrier_mat d d" using lowner_le_def by fastforce
have pM1WWk: "positive (adjoint M1 * (WS (W k)) * M1)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM1] dWWk pWWk] adjoint_adjoint[of "M1"] by auto
have pWSk: "positive (W (Suc k))" unfolding W_def wlp_while_n.simps apply (fold W_def)
using positive_add[OF pM0P pM1WWk] dM0 dP dM1 by fastforce
have qpWSk:"is_quantum_predicate (W (Suc k))" unfolding is_quantum_predicate_def using dWSk pWSk leWSk1 by auto
then have qpWWSk: "is_quantum_predicate (WS (W (Suc k)))" using assms(1) by auto
then have dWWSk: "(WS (W (Suc k))) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "WS (W (Suc k)) ≤⇩L WS (W k)" using assms(2)[OF qpWSk qpWk] leWSk by auto
then have "adjoint M1 * WS (W (Suc k)) * M1 ≤⇩L adjoint M1 * WS (W k) * M1"
using lowner_le_keep_under_measurement[OF dM1 dWWSk dWWk] by auto
then have "(adjoint M0 * P * M0 + adjoint M1 * WS (W (Suc k)) * M1)
≤⇩L (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)"
using lowner_le_add[of _ d _ "adjoint M1 * WS (W (Suc k)) * M1" "adjoint M1 * WS (W k) * M1",
OF _ _ _ _ lowner_le_refl[of "adjoint M0 * P * M0"]] dM0 dM1 dP dWWSk dWWk by fastforce
then have "W (Suc (Suc k)) ≤⇩L W (Suc k)" unfolding W_def wlp_while_n.simps by auto
with qpWSk show ?case by auto
qed
then have dWk: "W k ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
then have dmWk: "- W k ∈ carrier_mat d d" for k by auto
have incmWk: "- (W k) ≤⇩L - (W (Suc k))" for k using lowner_le_swap[of "W (Suc k)" d "W k"] dWk le_qp by auto
have pWk: "positive (W k)" for k using le_qp is_quantum_predicate_def by auto
have ubmWk: "- W k ≤⇩L 0⇩m d d" for k
proof -
have "0⇩m d d ≤⇩L W k" for k using zero_lowner_le_positiveI dWk pWk by auto
then have "- W k ≤⇩L - 0⇩m d d" for k using lowner_le_swap[of "0⇩m d d" d "W k"] dWk by auto
moreover have "(- 0⇩m d d :: complex mat) = (0⇩m d d)" by auto
ultimately show ?thesis by auto
qed
have "∃B. lowner_is_lub (λk. - W k) B ∧ limit_mat (λk. - W k) B d"
using mat_inc_seq_lub[of "λk. - W k" d "0⇩m d d"] dmWk incmWk ubmWk by auto
then obtain B where lubB: "lowner_is_lub (λk. - W k) B" and limB: "limit_mat (λk. - W k) B d" by auto
then have dB: "B ∈ carrier_mat d d" using limit_mat_def by auto
define A where "A = - B"
then have dA: "A ∈ carrier_mat d d" using dB by auto
have "limit_mat (λk. (-1) ⋅⇩m (- W k)) (-1 ⋅⇩m B) d" using limit_mat_scale[OF limB] by auto
moreover have "W k = -1 ⋅⇩m (- W k)" for k using dWk by auto
moreover have "-1 ⋅⇩m B = - B" by auto
ultimately have limA: "limit_mat W A d" using A_def by auto
moreover have "(limit_mat W A' d ⟹ A' = A)" for A' using limit_mat_unique[of W A d] limA by auto
ultimately have eqA: "(wlp_while (M 0) (M 1) WS P) = A" unfolding wlp_while_def W_def M0_def M1_def
using the_equality[of "λX. limit_mat (λn. wlp_while_n (M 0) (M 1) WS n P) X d" A] by fastforce
show "limit_mat (λn. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d"
using limA eqA unfolding W_def M0_def M1_def by auto
have "- W k ≤⇩L B" for k using lubB lowner_is_lub_def by auto
then have glbA: "A ≤⇩L W k" for k unfolding A_def using lowner_le_swap[of "- W k" d] dB dWk by fastforce
then show "⋀n. wlp_while (M 0) (M (Suc 0)) WS P ≤⇩L wlp_while_n (M 0) (M (Suc 0)) WS n P" using eqA unfolding W_def M0_def M1_def by auto
have "W k ≤⇩L 1⇩m d" for k using le_qp unfolding is_quantum_predicate_def by auto
then have "positive (1⇩m d - W k)" for k using lowner_le_def by auto
moreover have "limit_mat (λk. 1⇩m d - W k) (1⇩m d - A) d" using mat_minus_limit limA by auto
ultimately have "positive (1⇩m d - A)" using pos_mat_lim_is_pos by auto
then have leA1: "A ≤⇩L 1⇩m d" using dA lowner_le_def by auto
have pA: "positive A" using pos_mat_lim_is_pos limA pWk by auto
show "is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)" unfolding is_quantum_predicate_def using pA dA leA1 eqA by auto
{
fix W' assume asmW': "∀k. W' ≤⇩L W k"
then have dW': "W' ∈ carrier_mat d d" unfolding lowner_le_def using carrier_matD[OF dWk] by auto
then have "- W k ≤⇩L - W'" for k using lowner_le_swap dWk asmW' by auto
then have "B ≤⇩L - W'" using lubB unfolding lowner_is_lub_def by auto
then have "W' ≤⇩L A" unfolding A_def
using lowner_le_swap[of "B" d "- W'"] dB dW' by auto
then have "W' ≤⇩L wlp_while (M 0) (M 1) WS P" using eqA by auto
}
then show "⋀W'. ∀n. W' ≤⇩L wlp_while_n (M 0) (M (Suc 0)) WS n P ⟹ W' ≤⇩L wlp_while (M 0) (M (Suc 0)) WS P"
unfolding W_def M0_def M1_def by auto
qed
lemma wlp_while_mono:
assumes "⋀P. is_quantum_predicate P ⟹ is_quantum_predicate (WS P)"
and "⋀P Q. is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ WS P ≤⇩L WS Q"
and "measurement d 2 M"
and "is_quantum_predicate P"
and "is_quantum_predicate Q"
and "P ≤⇩L Q"
shows "wlp_while (M 0) (M 1) WS P ≤⇩L wlp_while (M 0) (M 1) WS Q"
proof -
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using assms M0_def M1_def measurement_def by auto
define Wn where "Wn P k = wlp_while_n M0 M1 WS k P" for P k
define W where "W P = wlp_while M0 M1 WS P" for P
have lePQk: "Wn P k ≤⇩L Wn Q k" for k unfolding Wn_def M0_def M1_def
using wlp_while_n_mono assms by auto
have "is_quantum_predicate (Wn P k)" for k unfolding Wn_def M0_def M1_def using wlp_while_n_close assms by auto
then have dWPk: "Wn P k ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
have "is_quantum_predicate (Wn Q k)" for k unfolding Wn_def M0_def M1_def using wlp_while_n_close assms by auto
then have dWQk:"Wn Q k ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
have "is_quantum_predicate (W P)" and lePk: "(W P) ≤⇩L (Wn P k)" and "limit_mat (Wn P) (W P) d" for k
unfolding W_def Wn_def M0_def M1_def using wlp_while_exists assms by auto
then have dWP: "W P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "is_quantum_predicate (W Q)" and "(W Q) ≤⇩L (Wn Q k)"
and glb:"(∀k. W' ≤⇩L (Wn Q k)) ⟶ W' ≤⇩L (W Q)" and "limit_mat (Wn Q) (W Q) d" for k W'
unfolding W_def Wn_def M0_def M1_def using wlp_while_exists assms by auto
have "W P ≤⇩L Wn Q k" for k using lowner_le_trans[of "W P" d "Wn P k" "Wn Q k"] lePk lePQk dWPk dWQk dWP by auto
then show "W P ≤⇩L W Q" using glb by auto
qed
fun wlp :: "com ⇒ complex mat ⇒ complex mat" where
"wlp SKIP P = P"
| "wlp (Utrans U) P = adjoint U * P * U"
| "wlp (Seq S1 S2) P = wlp S1 (wlp S2 P)"
| "wlp (Measure n M S) P = wlp_measure n M (map wlp S) P"
| "wlp (While M S) P = wlp_while (M 0) (M 1) (wlp S) P"
lemma wlp_measure_expand_m:
assumes m: "m ≤ n" and wc: "well_com (Measure n M S)"
shows "wlp (Measure m M S) P = matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * (M k)) m"
unfolding wlp.simps wlp_measure_def
proof -
have "k < m ⟹ map wlp S ! k = wlp (S!k)" for k using wc m by auto
then have "k < m ⟹ (map wlp S ! k) P = wlp (S!k) P" for k by auto
then show "matrix_sum d (λk. adjoint (M k) * ((map wlp S ! k) P) * (M k)) m
= matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * (M k)) m"
using matrix_sum_cong[of m "λk. adjoint (M k) * ((map wlp S ! k) P) * (M k)" "λk. adjoint (M k) * (wlp (S!k) P) * (M k)"] by auto
qed
lemma wlp_measure_expand:
assumes wc: "well_com (Measure n M S)"
shows "wlp (Measure n M S) P = matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * (M k)) n"
using wlp_measure_expand_m[OF Nat.le_refl[of n]] wc by auto
lemma wlp_mono_and_close:
shows "well_com S ⟹ is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q
⟹ is_quantum_predicate (wlp S P) ∧ wlp S P ≤⇩L wlp S Q"
proof (induct S arbitrary: P Q)
case SKIP
then show ?case by auto
next
case (Utrans U)
then have dU: "U ∈ carrier_mat d d" and u: "unitary U" and qp: "is_quantum_predicate P" and le: "P ≤⇩L Q"
and dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d" using is_quantum_predicate_def by auto
then have qp': "is_quantum_predicate (wlp (Utrans U) P)" using qp_close_under_unitary_operator by auto
moreover have "adjoint U * P * U ≤⇩L adjoint U * Q * U" using lowner_le_keep_under_measurement[OF dU dP dQ le] by auto
ultimately show ?case by auto
next
case (Seq S1 S2)
then have qpP: "is_quantum_predicate P" and qpQ: "is_quantum_predicate Q" and wc1: "well_com S1" and wc2: "well_com S2"
and dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d" and le: "P ≤⇩L Q"using is_quantum_predicate_def by auto
have qpP2: "is_quantum_predicate (wlp S2 P)" using Seq qpP wc2 by auto
have qpQ2: "is_quantum_predicate (wlp S2 Q)" using Seq(2)[OF wc2 qpQ qpQ] lowner_le_refl dQ by blast
have qpP1: "is_quantum_predicate (wlp S1 (wlp S2 P))"
using Seq(1)[OF wc1 qpP2 qpP2] qpP2 is_quantum_predicate_def[of "wlp S2 P"] lowner_le_refl by auto
have "wlp S2 P ≤⇩L wlp S2 Q" using Seq(2) wc2 qpP qpQ le by auto
then have "wlp S1 (wlp S2 P) ≤⇩L wlp S1 (wlp S2 Q)" using Seq(1) wc1 qpP2 qpQ2 by auto
then show ?case using qpP1 by auto
next
case (Measure n M S)
then have wc: "well_com (Measure n M S)" and wck: "k < n ⟹ well_com (S!k)" and l: "length S = n"
and m: "measurement d n M" and le: "P ≤⇩L Q"
and qpP: "is_quantum_predicate P" and dP: "P ∈ carrier_mat d d"
and qpQ: "is_quantum_predicate Q" and dQ: "Q ∈ carrier_mat d d"
for k using measure_well_com is_quantum_predicate_def by auto
have dMk: "k < n ⟹ M k ∈ carrier_mat d d" for k using m measurement_def by auto
have set: "k < n ⟹ S!k ∈ set S" for k using l by auto
have qpk: "k < n ⟹ is_quantum_predicate (wlp (S!k) P)" for k
using Measure(1)[OF set wck qpP qpP] lowner_le_refl[of P] dP by auto
then have dWkP: "k < n ⟹ wlp (S!k) P ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
then have dMkP: "k < n ⟹ adjoint (M k) * (wlp (S!k) P) * (M k) ∈ carrier_mat d d" for k using dMk by fastforce
have "k < n ⟹ is_quantum_predicate (wlp (S!k) Q)" for k
using Measure(1)[OF set wck qpQ qpQ] lowner_le_refl[of Q] dQ by auto
then have dWkQ: "k < n ⟹ wlp (S!k) Q ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
then have dMkQ: "k < n ⟹ adjoint (M k) * (wlp (S!k) Q) * (M k) ∈ carrier_mat d d" for k using dMk by fastforce
have "k < n ⟹ wlp (S!k) P ≤⇩L wlp (S!k) Q" for k
using Measure(1)[OF set wck qpP qpQ le] by auto
then have "k < n ⟹ adjoint (M k) * (wlp (S!k) P) * (M k) ≤⇩L adjoint (M k) * (wlp (S!k) Q) * (M k)" for k
using lowner_le_keep_under_measurement[OF dMk dWkP dWkQ] by auto
then have le': "wlp (Measure n M S) P ≤⇩L wlp (Measure n M S) Q" unfolding wlp_measure_expand[OF wc]
using lowner_le_matrix_sum dMkP dMkQ by auto
have qp': "is_quantum_predicate (wlp (Measure n M S) P)" unfolding wlp_measure_expand[OF wc]
using qps_after_measure_is_qp[OF m] qpk by auto
show ?case using le' qp' by auto
next
case (While M S)
then have m: "measurement d 2 M" and wcs: "well_com S"
and qpP: "is_quantum_predicate P"
by auto
have closeWS: "is_quantum_predicate P ⟹ is_quantum_predicate (wlp S P)" for P
proof -
assume asm: "is_quantum_predicate P"
then have dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
then show "is_quantum_predicate (wlp S P)" using While(1)[OF wcs asm asm lowner_le_refl] dP by auto
qed
have monoWS: "is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ wlp S P ≤⇩L wlp S Q" for P Q
using While(1)[OF wcs] by auto
have "is_quantum_predicate (wlp (While M S) P)"
using wlp_while_exists[of "wlp S" M P] closeWS monoWS m qpP by auto
moreover have "wlp (While M S) P ≤⇩L wlp (While M S) Q"
using wlp_while_mono[of "wlp S" M P Q] closeWS monoWS m While by auto
ultimately show ?case by auto
qed
lemma wlp_close:
assumes wc: "well_com S" and qp: "is_quantum_predicate P"
shows "is_quantum_predicate (wlp S P)"
using wlp_mono_and_close[OF wc qp qp] is_quantum_predicate_def[of P] qp lowner_le_refl by auto
lemma wlp_soundness:
"well_com S ⟹
(⋀P. (is_quantum_predicate P ⟹
(∀ρ ∈ density_states. trace (wlp S P * ρ) = trace (P * (denote S ρ)) + trace ρ - trace (denote S ρ))))"
proof (induct S)
case SKIP
then show ?case by auto
next
case (Utrans U)
then have dU: "U ∈ carrier_mat d d" and u: "unitary U" and wc: "well_com (Utrans U)"
and qp: "is_quantum_predicate P" and dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have qp': "is_quantum_predicate (wlp (Utrans U) P)" using wlp_close[OF wc qp] by auto
have eq1: "trace (adjoint U * P * U * ρ) = trace (P * (U * ρ * adjoint U))" if dr: "ρ ∈ carrier_mat d d" for ρ
using dr dP apply (mat_assoc d) using wc by auto
have eq2: "trace (U * ρ * adjoint U) = trace ρ" if dr: "ρ ∈ carrier_mat d d" for ρ
using unitary_operator_keep_trace[OF adjoint_dim[OF dU] dr unitary_adjoint[OF dU u]] adjoint_adjoint[of U] by auto
show ?case using qp' eq1 eq2 density_states_def by auto
next
case (Seq S1 S2)
then have qp: "is_quantum_predicate P" and wc1: "well_com S1" and wc2: "well_com S2" by auto
then have qp2: "is_quantum_predicate (wlp S2 P)" using wlp_close by auto
then have qp1: "is_quantum_predicate (wlp S1 (wlp S2 P))" using wlp_close wc1 by auto
have eq1: "trace (wlp S2 P * ρ) = trace (P * denote S2 ρ) + trace ρ - trace (denote S2 ρ)"
if ds: "ρ ∈ density_states" for ρ using Seq(2) wc2 qp ds by auto
have eq2: "trace (wlp S1 (wlp S2 P) * ρ) = trace ((wlp S2 P) * denote S1 ρ) + trace ρ - trace (denote S1 ρ)"
if ds: "ρ ∈ density_states" for ρ using Seq(1) wc1 qp2 ds by auto
have eq3: "trace (wlp S1 (wlp S2 P) * ρ) = trace (P * (denote S2 (denote S1 ρ))) + trace ρ - trace (denote S2 (denote S1 ρ))"
if ds: "ρ ∈ density_states" for ρ
proof -
have "denote S1 ρ ∈ density_states"
using ds denote_density_states wc1 by auto
then have "trace ((wlp S2 P) * denote S1 ρ) = trace (P * denote S2 (denote S1 ρ)) + trace (denote S1 ρ) - trace (denote S2 (denote S1 ρ))"
using eq1 by auto
then show "trace (wlp S1 (wlp S2 P) * ρ) = trace (P * (denote S2 (denote S1 ρ))) + trace ρ - trace (denote S2 (denote S1 ρ))"
using eq2 ds by auto
qed
then show ?case using qp1 by auto
next
case (Measure n M S)
then have wc: "well_com (Measure n M S)"
and wck: "k < n ⟹ well_com (S!k)"
and qpP: "is_quantum_predicate P"
and dP: "P ∈ carrier_mat d d"
and qpWk: "k < n ⟹ is_quantum_predicate (wlp (S!k) P)"
and dWk: "k < n ⟹ (wlp (S!k) P) ∈ carrier_mat d d"
and c: "k < n ⟹ ρ ∈ density_states ⟹ trace (wlp (S!k) P * ρ) = trace (P * denote (S!k) ρ) + trace ρ - trace (denote (S!k) ρ)"
and m: "measurement d n M"
and aMMkleq: "k < n ⟹ adjoint (M k) * M k ≤⇩L 1⇩m d"
and dMk: "k < n ⟹ M k ∈ carrier_mat d d"
for k ρ using is_quantum_predicate_def measurement_def measure_well_com measurement_le_one_mat wlp_close by auto
{
fix ρ assume ρ: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have dsr: "k < n ⟹ (M k) * ρ * adjoint (M k) ∈ density_states" for k unfolding density_states_def
using dMk pdo_close_under_measurement[OF dMk dr pdor aMMkleq] dr by fastforce
then have leqk: "k < n ⟹ trace (wlp (S!k) P * ((M k) * ρ * adjoint (M k))) =
trace (P * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" for k
using c by auto
have "k < n ⟹ M k * ρ * adjoint (M k) ∈ carrier_mat d d" for k using dMk dr by fastforce
then have dsMrk: "k < n ⟹ matrix_sum d (λk. (M k * ρ * adjoint (M k))) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. (M k * ρ * adjoint (M k))" d] by fastforce
have "k < n ⟹ adjoint (M k) * (wlp (S!k) P) * M k ∈ carrier_mat d d" for k using dMk by fastforce
then have dsMW: "k < n ⟹ matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. adjoint (M k) * (wlp (S!k) P) * M k" d] by fastforce
have dSMrk: "k < n ⟹ denote (S ! k) (M k * ρ * adjoint (M k)) ∈ carrier_mat d d" for k
using denote_dim[OF wck, of k "M k * ρ * adjoint (M k)"] dsr density_states_def by fastforce
have dsSMrk: "k < n ⟹ matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. denote (S ! k) (M k * ρ * adjoint (M k))" d, OF dSMrk] by fastforce
have "k ≤ n ⟹
trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) k * ρ)
= trace (P * (denote (Measure k M S) ρ)) + (trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) k) - trace (denote (Measure k M S) ρ))" for k
unfolding denote_measure_expand[OF _ wc]
proof (induct k)
case 0
then show ?case unfolding matrix_sum.simps using dP dr by auto
next
case (Suc k)
then have k: "k < n" by auto
have eq1: "trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) (Suc k) * ρ)
= trace (adjoint (M k) * (wlp (S!k) P) * M k * ρ) + trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) k * ρ)"
unfolding matrix_sum.simps
using dMk[OF k] dWk[OF k] dr dsMW[OF k] by (mat_assoc d)
have "trace (adjoint (M k) * (wlp (S!k) P) * M k * ρ) = trace ((wlp (S!k) P) * (M k * ρ * adjoint (M k)))"
using dMk[OF k] dWk[OF k] dr by (mat_assoc d)
also have "… = trace (P * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" using leqk k by auto
finally have eq2: "trace (adjoint (M k) * (wlp (S!k) P) * M k * ρ) = trace (P * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" .
have eq3: "trace (P * matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) (Suc k))
= trace (P * (denote (S!k) (M k * ρ * adjoint (M k)))) + trace (P * matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)"
unfolding matrix_sum.simps
using dP dSMrk[OF k] dsSMrk[OF k] by (mat_assoc d)
have eq4: "trace (denote (S ! k) (M k * ρ * adjoint (M k)) + matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)
= trace (denote (S ! k) (M k * ρ * adjoint (M k))) + trace (matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)"
using dSMrk[OF k] dsSMrk[OF k] by (mat_assoc d)
show ?case
apply (subst eq1) apply (subst eq3)
apply (simp del: less_eq_complex_def)
apply (subst trace_add_linear[of "M k * ρ * adjoint (M k)" d "matrix_sum d (λk. M k * ρ * adjoint (M k)) k"])
apply (simp add: dMk adjoint_dim[OF dMk] dr mult_carrier_mat[of _ d d _ d] k)
apply (simp add: dsMrk k)
apply (subst eq4)
apply (insert eq2 Suc(1) k, fastforce)
done
qed
then have leq: "trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) n * ρ)
= trace (P * denote (Measure n M S) ρ) +
(trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) n) - trace (denote (Measure n M S) ρ))"
by auto
have "trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) n) = trace ρ" using trace_measurement m dr by auto
with leq have "trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) n * ρ)
= trace (P * denote (Measure n M S) ρ) + (trace ρ - trace (denote (Measure n M S) ρ))"
unfolding denote_measure_def by auto
}
then show ?case unfolding wlp_measure_expand[OF wc] by auto
next
case (While M S)
then have qpP: "is_quantum_predicate P" and dP: "P ∈ carrier_mat d d"
and wcS: "well_com S" and m: "measurement d 2 M" and wc: "well_com (While M S)"
using is_quantum_predicate_def by auto
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m measurement_def M0_def M1_def by auto
have leM1: "adjoint M1 * M1 ≤⇩L 1⇩m d" using measurement_le_one_mat m M1_def by auto
define W where "W k = wlp_while_n M0 M1 (wlp S) k P" for k
define DS where "DS = denote S"
define D0 where "D0 = denote_while_n M0 M1 DS"
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
define D where "D = denote_while_n_iter M0 M1 DS"
have eqk: "ρ ∈ density_states ⟹ trace ((W k) * ρ) = (∑k=0..<k. trace (P * (D0 k ρ))) + trace ρ - (∑k=0..<k. trace (D0 k ρ))" for k ρ
proof (induct k arbitrary: ρ)
case 0
then have dsr: "ρ ∈ density_states" by auto
show ?case unfolding W_def wlp_while_n.simps using dsr density_states_def by auto
next
case (Suc k)
then have dsr: "ρ ∈ density_states" and dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
then have dsM1r: "M1 * ρ * adjoint M1 ∈ density_states" unfolding density_states_def using pdo_close_under_measurement[OF dM1 dr pdor leM1] dr dM1 by auto
then have dsDSM1r: "(DS (M1 * ρ * adjoint M1)) ∈ density_states" unfolding density_states_def DS_def
using denote_dim[OF wcS] denote_partial_density_operator[OF wcS] dsM1r by auto
have qpWk: "is_quantum_predicate (W k)"
using wlp_while_n_close[OF _ m qpP, folded M0_def M1_def, of "wlp S", folded W_def] wlp_close[OF wcS] by auto
then have "is_quantum_predicate (wlp S (W k))" using wlp_close[OF wcS] by auto
then have dWWk: "wlp S (W k) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "trace (P * (M0 * ρ * adjoint M0)) + (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1)))))
= trace (P * (D0 0 ρ)) + (∑k=0..<k. trace (P * (D0 (Suc k) ρ)))"
unfolding D0_def by auto
also have "… = trace (P * (D0 0 ρ)) + (∑k=1..<(Suc k). trace (P * (D0 k ρ)))"
using sum.shift_bounds_Suc_ivl[symmetric, of "λk. trace (P * (D0 k ρ))"] by auto
also have "… = (∑k=0..<(Suc k). trace (P * (D0 k ρ)))" using sum.atLeast_Suc_lessThan[of 0 "Suc k" "λk. trace (P * (D0 k ρ))"] by auto
finally have eq1: "trace (P * (M0 * ρ * adjoint M0)) + (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1)))))
= (∑k=0..<(Suc k). trace (P * (D0 k ρ)))".
have eq2: "trace (M1 * ρ * adjoint M1) = trace ρ - trace (M0 * ρ * adjoint M0)"
unfolding M0_def M1_def using m trace_measurement2[OF m dr] dr by (simp add: algebra_simps)
have "trace (M0 * ρ * adjoint M0) + (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))
= trace (D0 0 ρ) + (∑k=0..<k. trace (D0 (Suc k) ρ))" unfolding D0_def by auto
also have "… = trace (D0 0 ρ) + (∑k=1..<(Suc k). trace (D0 k ρ))"
using sum.shift_bounds_Suc_ivl[symmetric, of "λk. trace (D0 k ρ)"] by auto
also have "… = (∑k=0..<(Suc k). trace (D0 k ρ))"
using sum.atLeast_Suc_lessThan[of 0 "Suc k" "λk. trace (D0 k ρ)"] by auto
finally have eq3: "trace (M0 * ρ * adjoint M0) + (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1)))) = (∑k=0..<(Suc k). trace (D0 k ρ))".
then have "trace (M1 * ρ * adjoint M1) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))
= trace ρ - (trace (M0 * ρ * adjoint M0) + (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1)))))"
by (simp add: algebra_simps eq2)
then have eq4: "trace (M1 * ρ * adjoint M1) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1)))) = trace ρ - (∑k=0..<(Suc k). trace (D0 k ρ))"
by (simp add: eq3)
have "trace ((W (Suc k)) * ρ) = trace (P * (M0 * ρ * adjoint M0)) + trace ((wlp S (W k)) * (M1 * ρ * adjoint M1))"
unfolding W_def wlp_while_n.simps
apply (fold W_def) using dM0 dP dM1 dWWk dr by (mat_assoc d)
also have "… = trace (P * (M0 * ρ * adjoint M0)) + trace ((W k) * (DS (M1 * ρ * adjoint M1))) + trace (M1 * ρ * adjoint M1) - trace (DS (M1 * ρ * adjoint M1))"
using While(1)[OF wcS, of "W k"] qpWk dsM1r DS_def by auto
also have "… = trace (P * (M0 * ρ * adjoint M0))
+ (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1))))) + trace (DS (M1 * ρ * adjoint M1)) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))
+ trace (M1 * ρ * adjoint M1) - trace (DS (M1 * ρ * adjoint M1))"
using Suc(1)[OF dsDSM1r] by auto
also have "… = trace (P * (M0 * ρ * adjoint M0)) + (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1)))))
+ trace (M1 * ρ * adjoint M1) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))"
by auto
also have "… = (∑k=0..<(Suc k). trace (P * (D0 k ρ))) + trace ρ - (∑k=0..<(Suc k). trace (D0 k ρ))"
by (simp add: eq1 eq4)
finally show ?case.
qed
{
fix ρ assume dsr: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have limDW: "limit_mat (λn. matrix_sum d (λk. D0 k ρ) (n)) (denote (While M S) ρ) d"
using limit_mat_denote_while_n[OF wc dr pdor] unfolding D0_def M0_def M1_def DS_def by auto
then have "limit_mat (λn. (P * (matrix_sum d (λk. D0 k ρ) (n)))) (P * (denote (While M S) ρ)) d"
using mat_mult_limit[OF dP] unfolding mat_mult_seq_def by auto
then have limtrPm: "(λn. trace (P * (matrix_sum d (λk. D0 k ρ) (n)))) ⇢ trace (P * (denote (While M S) ρ))"
using mat_trace_limit by auto
with limDW have limtrDW:"(λn. trace (matrix_sum d (λk. D0 k ρ) (n))) ⇢ trace (denote (While M S) ρ)"
using mat_trace_limit by auto
have limm: "(λn. trace (matrix_sum d (λk. D0 k ρ) (n))) ⇢ trace (denote (While M S) ρ)"
using mat_trace_limit limDW by auto
have closeWS: "is_quantum_predicate P ⟹ is_quantum_predicate (wlp S P)" for P
proof -
assume asm: "is_quantum_predicate P"
then have dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
then show "is_quantum_predicate (wlp S P)" using wlp_mono_and_close[OF wcS asm asm] lowner_le_refl by auto
qed
have monoWS: "is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ wlp S P ≤⇩L wlp S Q" for P Q
using wlp_mono_and_close[OF wcS] by auto
have "is_quantum_predicate (wlp (While M S) P)"
using wlp_while_exists[of "wlp S" M P] closeWS monoWS m qpP by auto
have "limit_mat W (wlp_while M0 M1 (wlp S) P) d" unfolding W_def M0_def M1_def
using wlp_while_exists[of "wlp S" M P] closeWS monoWS m qpP by auto
then have "limit_mat (λk. (W k) * ρ) ((wlp_while M0 M1 (wlp S) P) * ρ) d" using mult_mat_limit dr by auto
then have lim1: "(λk. trace ((W k) * ρ)) ⇢ trace ((wlp_while M0 M1 (wlp S) P) * ρ)"
using mat_trace_limit by auto
have dD0kr: "D0 k ρ ∈ carrier_mat d d" for k unfolding D0_def
using denote_while_n_dim[OF dr dM0 dM1 pdor] denote_positive_trace_dim[OF wcS, folded DS_def] by auto
then have "(P * (matrix_sum d (λk. D0 k ρ) (n))) = matrix_sum d (λk. P * (D0 k ρ)) n" for n
using matrix_sum_distrib_left[OF dP] by auto
moreover have "trace (matrix_sum d (λk. P * (D0 k ρ)) n) = (∑k=0..<n. trace (P * (D0 k ρ)))" for n
using trace_matrix_sum_linear dD0kr dP by auto
ultimately have eqPsD0kr: "trace (P * (matrix_sum d (λk. D0 k ρ) (n))) = (∑k=0..<n. trace (P * (D0 k ρ)))" for n by auto
with limtrPm have lim2: "(λk. (∑k=0..<k. trace (P * (D0 k ρ)))) ⇢ trace (P * (denote (While M S) ρ))" by auto
have "trace (matrix_sum d (λk. D0 k ρ) (n)) = (∑k=0..<n. trace (D0 k ρ))" for n
using trace_matrix_sum_linear dD0kr by auto
with limtrDW have lim3: "(λk. (∑k=0..<k. trace (D0 k ρ))) ⇢ trace (denote (While M S) ρ)" by auto
have "(λk. (∑k=0..<k. trace (P * (D0 k ρ))) + trace ρ) ⇢ trace (P * (denote (While M S) ρ)) + trace ρ"
using tendsto_add[of "λk. (∑k=0..<k. trace (P * (D0 k ρ)))"] lim2 by auto
then have "(λk. (∑k=0..<k. trace (P * (D0 k ρ))) + trace ρ - (∑k=0..<k. trace (D0 k ρ)))
⇢ trace (P * (denote (While M S) ρ)) + trace ρ - trace (denote (While M S) ρ)"
using tendsto_diff[of _ _ _ "λk. (∑k=0..<k. trace (D0 k ρ))"] lim3 by auto
then have lim4: "(λk. trace ((W k) * ρ)) ⇢ trace (P * (denote (While M S) ρ)) + trace ρ - trace (denote (While M S) ρ)"
using eqk[OF dsr] by auto
then have "trace ((wlp_while M0 M1 (wlp S) P) * ρ) = trace (P * (denote (While M S) ρ)) + trace ρ - trace (denote (While M S) ρ)"
using eqk[OF dsr] tendsto_unique[OF _ lim1 lim4] by auto
}
then show ?case unfolding M0_def M1_def DS_def wlp.simps by auto
qed
lemma denote_while_split:
assumes wc: "well_com (While M S)" and dsr: "ρ ∈ density_states"
shows "denote (While M S) ρ = (M 0) * ρ * adjoint (M 0) + denote (While M S) (denote S (M 1 * ρ * adjoint (M 1)))"
proof -
have m: "measurement d 2 M" using wc by auto
have wcs: "well_com S" using wc by auto
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m measurement_def M0_def M1_def by auto
have M1leq: "adjoint M1 * M1 ≤⇩L 1⇩m d" using measurement_le_one_mat m M1_def by auto
define DS where "DS = denote S"
define D0 where "D0 = denote_while_n M0 M1 DS"
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
define D where "D = denote_while_n_iter M0 M1 DS"
define DW where "DW ρ = denote (While M S) ρ" for ρ
{
fix ρ assume dsr: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have pdoDkr: "⋀k. partial_density_operator (D k ρ)" unfolding D_def
using pdo_denote_while_n_iter[OF dr pdor dM1 M1leq]
denote_partial_density_operator[OF wcs] denote_dim[OF wcs, folded DS_def]
apply (fold DS_def) by auto
then have pDkr: "⋀k. positive (D k ρ)" unfolding partial_density_operator_def by auto
have dDkr: "⋀k. D k ρ ∈ carrier_mat d d"
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] by auto
then have dD0kr: "⋀k. D0 k ρ ∈ carrier_mat d d" unfolding D0_def denote_while_n.simps apply (fold D_def) using dM0 by auto
}
note dD0k = this
have "matrix_sum d (λk. D0 k ρ) k ∈ carrier_mat d d" if dsr: "ρ ∈ density_states" for ρ k
using matrix_sum_dim[OF dD0k, of _ "λk. ρ" id, OF dsr] dsr by auto
{
fix k
have "matrix_sum d (λk. D0 k ρ) (Suc k) = (D0 0 ρ) + matrix_sum d (λk. D0 (Suc k) ρ) k"
using matrix_sum_shift_Suc[of _ "λk. D0 k ρ"] dD0k[OF dsr] by fastforce
also have "… = M0 * ρ * adjoint M0 + matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1))) k"
unfolding D0_def by auto
finally have "matrix_sum d (λk. D0 k ρ) (Suc k) = M0 * ρ * adjoint M0 + matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1))) k".
}
note eqk = this
have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def dsr by auto
then have "M1 * ρ * adjoint M1 ∈ carrier_mat d d" and "partial_density_operator (M1 * ρ * adjoint M1)"
using dM1 dr pdo_close_under_measurement[OF dM1 dr pdor M1leq] by auto
then have dSM1r: "(DS (M1 * ρ * adjoint M1)) ∈ carrier_mat d d" and pdoSM1r: "partial_density_operator (DS (M1 * ρ * adjoint M1))"
unfolding DS_def using denote_dim_pdo[OF wcs] by auto
have "limit_mat (matrix_sum d (λk. D0 k ρ)) (DW ρ) d" unfolding M0_def M1_def D0_def DS_def DW_def
using limit_mat_denote_while_n[OF wc dr pdor] by auto
then have liml: "limit_mat (λk. matrix_sum d (λk. D0 k ρ) (Suc k)) (DW ρ) d"
using limit_mat_ignore_initial_segment[of "matrix_sum d (λk. D0 k ρ)" "DW ρ" d 1] by auto
have dM0r: "M0 * ρ * adjoint M0 ∈ carrier_mat d d" using dM0 dr by fastforce
have "limit_mat (matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1)))) (DW (DS (M1 * ρ * adjoint M1))) d"
using limit_mat_denote_while_n[OF wc dSM1r pdoSM1r] unfolding M0_def M1_def D0_def DS_def DW_def by auto
then have
limr: "limit_mat
(mat_add_seq (M0 * ρ * adjoint M0) (matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1)))))
(M0 * ρ * adjoint M0 + (DW (DS (M1 * ρ * adjoint M1))))
d"
using mat_add_limit[OF dM0r] by auto
moreover have
"(λk. matrix_sum d (λk. D0 k ρ) (Suc k))