[STATEMENT]
lemma wlp_while_exists:
  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 m: "measurement d 2 M"
    and qpP: "is_quantum_predicate P"
  shows "is_quantum_predicate (wlp_while (M 0) (M 1) WS P)
    \<and> (\<forall>n. (wlp_while (M 0) (M 1) WS P) \<le>\<^sub>L (wlp_while_n (M 0) (M 1) WS n P))
    \<and> (\<forall>W'. (\<forall>n. W' \<le>\<^sub>L (wlp_while_n (M 0) (M 1) WS n P)) \<longrightarrow> W' \<le>\<^sub>L (wlp_while (M 0) (M 1) WS P))
    \<and> limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) (wlp_while (M 0) (M 1) WS P) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while (M 0) (M 1) WS P) \<and> (\<forall>n. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS n P) \<and> (\<forall>W'. (\<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS n P) \<longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M 1) WS P) \<and> limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) (wlp_while (M 0) (M 1) WS P) d
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
define M0 where "M0 = M 0"
[PROOF STATE]
proof (state)
this:
M0 = M 0

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
define M1 where "M1 = M 1"
[PROOF STATE]
proof (state)
this:
M1 = M 1

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) 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 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
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 (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[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 (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have leP: "P \<le>\<^sub>L 1\<^sub>m d" and dP: "P \<in> carrier_mat d d" and pP: "positive P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<le>\<^sub>L 1\<^sub>m d &&& P \<in> carrier_mat d d &&& 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. P \<le>\<^sub>L 1\<^sub>m d &&& P \<in> carrier_mat d d &&& positive P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<le>\<^sub>L 1\<^sub>m d
P \<in> carrier_mat d d
positive P

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have pM0P: "positive (adjoint M0 * P * M0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (adjoint M0 * P * M0)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM0]] adjoint_adjoint[of "M0"] dP pP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat d d; positive ?A\<rbrakk> \<Longrightarrow> positive (adjoint M0 * ?A * adjoint (adjoint M0))
adjoint (adjoint M0) = M0
P \<in> carrier_mat d d
positive P

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

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have le_qp: "W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
have "is_quantum_predicate (1\<^sub>m d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (1\<^sub>m d)
[PROOF STEP]
unfolding 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 lowner_le_refl[of "1\<^sub>m d"]
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m ?n)
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 (1\<^sub>m d)

goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (1\<^sub>m d)
[PROOF STEP]
have "is_quantum_predicate (WS (1\<^sub>m d))"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (1\<^sub>m d)

goal (1 subgoal):
 1. is_quantum_predicate (WS (1\<^sub>m d))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (1\<^sub>m 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

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

goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (WS (1\<^sub>m d))
[PROOF STEP]
have "(WS (1\<^sub>m d)) \<in> carrier_mat d d" and "(WS (1\<^sub>m d)) \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (1\<^sub>m d))

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

goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
WS (1\<^sub>m d) \<in> carrier_mat d d
WS (1\<^sub>m d) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "W 1 \<le>\<^sub>L W 0"
[PROOF STATE]
proof (prove)
using this:
WS (1\<^sub>m d) \<in> carrier_mat d d
WS (1\<^sub>m d) \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. W 1 \<le>\<^sub>L W 0
[PROOF STEP]
unfolding W_def wlp_while_n.simps M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
WS (1\<^sub>m d) \<in> carrier_mat d d
WS (1\<^sub>m d) \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. wlp_while_n (M 0) (M 1) WS 1 P \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement2_leq_one_mat[OF dP _ leP _ m]
[PROOF STATE]
proof (prove)
using this:
WS (1\<^sub>m d) \<in> carrier_mat d d
WS (1\<^sub>m d) \<le>\<^sub>L 1\<^sub>m d
\<lbrakk>?Q \<in> carrier_mat d d; ?Q \<le>\<^sub>L 1\<^sub>m d\<rbrakk> \<Longrightarrow> adjoint (M 0) * P * M 0 + adjoint (M 1) * ?Q * M 1 \<le>\<^sub>L 1\<^sub>m d

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

goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
W 1 \<le>\<^sub>L W 0

goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
have "is_quantum_predicate (W 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (W 0)
[PROOF STEP]
unfolding W_def 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 lowner_le_refl[of "1\<^sub>m d"]
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m ?n)
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 (W 0)

goal (2 subgoals):
 1. W (Suc 0) \<le>\<^sub>L W 0 \<and> is_quantum_predicate (W 0)
 2. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
W 1 \<le>\<^sub>L W 0
is_quantum_predicate (W 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
W 1 \<le>\<^sub>L W 0
is_quantum_predicate (W 0)

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

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k)

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k)
[PROOF STEP]
have leWSk: "W (Suc k) \<le>\<^sub>L W k" and qpWk: "is_quantum_predicate (W k)"
[PROOF STATE]
proof (prove)
using this:
W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k)

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

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

goal (1 subgoal):
 1. is_quantum_predicate (WS (W k))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
W (Suc k) \<le>\<^sub>L W k
is_quantum_predicate (W 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

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 (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (WS (W k))
[PROOF STEP]
have dWWk: "WS (W k) \<in> carrier_mat d d" and leWWk1: "(WS (W k)) \<le>\<^sub>L 1\<^sub>m d" and pWWk: "positive (WS (W k))"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (WS (W k))

goal (1 subgoal):
 1. WS (W k) \<in> carrier_mat d d &&& WS (W k) \<le>\<^sub>L 1\<^sub>m d &&& positive (WS (W k))
[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 &&& WS (W k) \<le>\<^sub>L 1\<^sub>m d &&& positive (WS (W k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
WS (W k) \<in> carrier_mat d d
WS (W k) \<le>\<^sub>L 1\<^sub>m d
positive (WS (W k))

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
WS (W k) \<in> carrier_mat d d
WS (W k) \<le>\<^sub>L 1\<^sub>m d
positive (WS (W k))
[PROOF STEP]
have leWSk1: "W (Suc k) \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
WS (W k) \<in> carrier_mat d d
WS (W k) \<le>\<^sub>L 1\<^sub>m d
positive (WS (W k))

goal (1 subgoal):
 1. W (Suc k) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement2_leq_one_mat[OF dP dWWk leP leWWk1 m]
[PROOF STATE]
proof (prove)
using this:
WS (W k) \<in> carrier_mat d d
WS (W k) \<le>\<^sub>L 1\<^sub>m d
positive (WS (W k))
adjoint (M 0) * P * M 0 + adjoint (M 1) * WS (W k) * M 1 \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. W (Suc k) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
unfolding W_def wlp_while_n.simps M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
WS (wlp_while_n (M 0) (M 1) WS k P) \<in> carrier_mat d d
WS (wlp_while_n (M 0) (M 1) WS k P) \<le>\<^sub>L 1\<^sub>m d
positive (WS (wlp_while_n (M 0) (M 1) WS k P))
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

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 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W (Suc k) \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W (Suc k) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have dWSk: "W (Suc k) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
W (Suc k) \<le>\<^sub>L 1\<^sub>m d

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

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
have pM1WWk: "positive (adjoint M1 * (WS (W k)) * M1)"
[PROOF STATE]
proof (prove)
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] dWWk pWWk] adjoint_adjoint[of "M1"]
[PROOF STATE]
proof (prove)
using this:
positive (adjoint M1 * WS (W k) * adjoint (adjoint M1))
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 (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
have pWSk: "positive (W (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (W (Suc k))
[PROOF STEP]
unfolding W_def wlp_while_n.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (adjoint M0 * P * M0 + adjoint M1 * WS (wlp_while_n M0 M1 WS k P) * M1)
[PROOF STEP]
apply (fold W_def)
[PROOF STATE]
proof (prove)
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
[PROOF STATE]
proof (prove)
using this:
\<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

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 (W (Suc k))

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
have qpWSk:"is_quantum_predicate (W (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (W (Suc k))
[PROOF STEP]
unfolding is_quantum_predicate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W (Suc k) \<in> carrier_mat d d \<and> positive (W (Suc k)) \<and> W (Suc k) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using dWSk pWSk leWSk1
[PROOF STATE]
proof (prove)
using this:
W (Suc k) \<in> carrier_mat d d
positive (W (Suc k))
W (Suc k) \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. W (Suc k) \<in> carrier_mat d d \<and> positive (W (Suc k)) \<and> W (Suc k) \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (W (Suc k))

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

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

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

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

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

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
have "WS (W (Suc k)) \<le>\<^sub>L WS (W k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WS (W (Suc k)) \<le>\<^sub>L WS (W k)
[PROOF STEP]
using assms(2)[OF qpWSk qpWk] leWSk
[PROOF STATE]
proof (prove)
using this:
W (Suc k) \<le>\<^sub>L W k \<Longrightarrow> WS (W (Suc k)) \<le>\<^sub>L WS (W k)
W (Suc k) \<le>\<^sub>L W k

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

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

goal (1 subgoal):
 1. adjoint M1 * WS (W (Suc k)) * M1 \<le>\<^sub>L adjoint M1 * WS (W k) * M1
[PROOF STEP]
using lowner_le_keep_under_measurement[OF dM1 dWWSk dWWk]
[PROOF STATE]
proof (prove)
using this:
WS (W (Suc k)) \<le>\<^sub>L WS (W k)
WS (W (Suc k)) \<le>\<^sub>L WS (W k) \<Longrightarrow> adjoint M1 * WS (W (Suc k)) * M1 \<le>\<^sub>L adjoint M1 * WS (W k) * M1

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

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

goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (W (Suc k)) * M1 \<le>\<^sub>L adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1
[PROOF STEP]
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
[PROOF STATE]
proof (prove)
using this:
adjoint M1 * WS (W (Suc k)) * M1 \<le>\<^sub>L adjoint M1 * WS (W k) * M1
\<lbrakk>adjoint M0 * P * M0 \<in> carrier_mat d d; adjoint M0 * P * M0 \<in> carrier_mat d d; adjoint M1 * WS (W (Suc k)) * M1 \<in> carrier_mat d d; adjoint M1 * WS (W k) * M1 \<in> carrier_mat d d; adjoint M0 * P * M0 \<in> carrier_mat ?n1 ?n1; adjoint M1 * WS (W (Suc k)) * M1 \<le>\<^sub>L adjoint M1 * WS (W k) * M1\<rbrakk> \<Longrightarrow> adjoint M0 * P * M0 + adjoint M1 * WS (W (Suc k)) * M1 \<le>\<^sub>L adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1
M0 \<in> carrier_mat d d
M1 \<in> carrier_mat d d
P \<in> carrier_mat d d
WS (W (Suc k)) \<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 (Suc k)) * M1 \<le>\<^sub>L adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
adjoint M0 * P * M0 + adjoint M1 * WS (W (Suc k)) * M1 \<le>\<^sub>L adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1

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

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

goal (1 subgoal):
 1. adjoint M0 * P * M0 + adjoint M1 * WS (adjoint M0 * P * M0 + adjoint M1 * WS (wlp_while_n M0 M1 WS k P) * M1) * M1 \<le>\<^sub>L 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 (Suc (Suc k)) \<le>\<^sub>L W (Suc k)

goal (1 subgoal):
 1. \<And>k. W (Suc k) \<le>\<^sub>L W k \<and> is_quantum_predicate (W k) \<Longrightarrow> W (Suc (Suc k)) \<le>\<^sub>L W (Suc k) \<and> is_quantum_predicate (W (Suc k))
[PROOF STEP]
with qpWSk
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (W (Suc k))
W (Suc (Suc k)) \<le>\<^sub>L W (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W (Suc k))
W (Suc (Suc k)) \<le>\<^sub>L W (Suc k)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
W (Suc ?k) \<le>\<^sub>L W ?k \<and> is_quantum_predicate (W ?k)

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W (Suc ?k) \<le>\<^sub>L W ?k \<and> is_quantum_predicate (W ?k)
[PROOF STEP]
have dWk: "W k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
W (Suc ?k) \<le>\<^sub>L W ?k \<and> 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:
W (Suc ?k) \<le>\<^sub>L W ?k \<and> 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 (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W ?k \<in> carrier_mat d d
[PROOF STEP]
have dmWk: "- W k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
W ?k \<in> carrier_mat d 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 (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have incmWk: "- (W k) \<le>\<^sub>L - (W (Suc k))" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - W k \<le>\<^sub>L - W (Suc k)
[PROOF STEP]
using lowner_le_swap[of "W (Suc k)" d "W k"] dWk le_qp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>W (Suc k) \<in> carrier_mat d d; W k \<in> carrier_mat d d; W (Suc k) \<le>\<^sub>L W k\<rbrakk> \<Longrightarrow> - W k \<le>\<^sub>L - W (Suc k)
W ?k \<in> carrier_mat d d
W (Suc ?k) \<le>\<^sub>L W ?k \<and> is_quantum_predicate (W ?k)

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

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have pWk: "positive (W k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (W k)
[PROOF STEP]
using le_qp is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
W (Suc ?k) \<le>\<^sub>L W ?k \<and> 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. positive (W k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (W ?k)

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have ubmWk: "- W k \<le>\<^sub>L 0\<^sub>m d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - W k \<le>\<^sub>L 0\<^sub>m d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - W k \<le>\<^sub>L 0\<^sub>m d d
[PROOF STEP]
have "0\<^sub>m d d \<le>\<^sub>L W k" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>m d d \<le>\<^sub>L W k
[PROOF STEP]
using zero_lowner_le_positiveI dWk pWk
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> 0\<^sub>m ?n ?n \<le>\<^sub>L ?A
W ?k \<in> carrier_mat d d
positive (W ?k)

goal (1 subgoal):
 1. 0\<^sub>m d d \<le>\<^sub>L W k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0\<^sub>m d d \<le>\<^sub>L W ?k

goal (1 subgoal):
 1. - W k \<le>\<^sub>L 0\<^sub>m d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0\<^sub>m d d \<le>\<^sub>L W ?k
[PROOF STEP]
have "- W k \<le>\<^sub>L - 0\<^sub>m d d" for k
[PROOF STATE]
proof (prove)
using this:
0\<^sub>m d d \<le>\<^sub>L W ?k

goal (1 subgoal):
 1. - W k \<le>\<^sub>L - 0\<^sub>m d d
[PROOF STEP]
using lowner_le_swap[of "0\<^sub>m d d" d "W k"] dWk
[PROOF STATE]
proof (prove)
using this:
0\<^sub>m d d \<le>\<^sub>L W ?k
\<lbrakk>0\<^sub>m d d \<in> carrier_mat d d; W k \<in> carrier_mat d d; 0\<^sub>m d d \<le>\<^sub>L W k\<rbrakk> \<Longrightarrow> - W k \<le>\<^sub>L - 0\<^sub>m d d
W ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. - W k \<le>\<^sub>L - 0\<^sub>m d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- W ?k \<le>\<^sub>L - 0\<^sub>m d d

goal (1 subgoal):
 1. - W k \<le>\<^sub>L 0\<^sub>m d d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- W ?k \<le>\<^sub>L - 0\<^sub>m d d

goal (1 subgoal):
 1. - W k \<le>\<^sub>L 0\<^sub>m d d
[PROOF STEP]
have "(- 0\<^sub>m d d :: complex mat) = (0\<^sub>m d d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 0\<^sub>m d d = 0\<^sub>m d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- 0\<^sub>m d d = 0\<^sub>m d d

goal (1 subgoal):
 1. - W k \<le>\<^sub>L 0\<^sub>m d d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- W ?k \<le>\<^sub>L - 0\<^sub>m d d
- 0\<^sub>m d d = 0\<^sub>m d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- W ?k \<le>\<^sub>L - 0\<^sub>m d d
- 0\<^sub>m d d = 0\<^sub>m d d

goal (1 subgoal):
 1. - W k \<le>\<^sub>L 0\<^sub>m d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- W k \<le>\<^sub>L 0\<^sub>m d d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
- W ?k \<le>\<^sub>L 0\<^sub>m d d

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have "\<exists>B. lowner_is_lub (\<lambda>k. - W k) B \<and> limit_mat (\<lambda>k. - W k) B d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B. lowner_is_lub (\<lambda>k. - W k) B \<and> limit_mat (\<lambda>k. - W k) B d
[PROOF STEP]
using mat_inc_seq_lub[of "\<lambda>k. - W k" d "0\<^sub>m d d"] dmWk incmWk ubmWk
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>n. - W n \<in> carrier_mat d d; \<And>n. - W n \<le>\<^sub>L - W (Suc n); \<And>n. - W n \<le>\<^sub>L 0\<^sub>m d d\<rbrakk> \<Longrightarrow> \<exists>B. lowner_is_lub (\<lambda>k. - W k) B \<and> limit_mat (\<lambda>k. - W k) B d
- W ?k \<in> carrier_mat d d
- W ?k \<le>\<^sub>L - W (Suc ?k)
- W ?k \<le>\<^sub>L 0\<^sub>m d d

goal (1 subgoal):
 1. \<exists>B. lowner_is_lub (\<lambda>k. - W k) B \<and> limit_mat (\<lambda>k. - W k) B d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>B. lowner_is_lub (\<lambda>k. - W k) B \<and> limit_mat (\<lambda>k. - W k) B d

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>B. lowner_is_lub (\<lambda>k. - W k) B \<and> limit_mat (\<lambda>k. - W k) B d
[PROOF STEP]
obtain B where lubB: "lowner_is_lub (\<lambda>k. - W k) B" and limB: "limit_mat (\<lambda>k. - W k) B d"
[PROOF STATE]
proof (prove)
using this:
\<exists>B. lowner_is_lub (\<lambda>k. - W k) B \<and> limit_mat (\<lambda>k. - W k) B d

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>lowner_is_lub (\<lambda>k. - W k) B; limit_mat (\<lambda>k. - W k) B d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lowner_is_lub (\<lambda>k. - W k) B
limit_mat (\<lambda>k. - W k) B d

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lowner_is_lub (\<lambda>k. - W k) B
limit_mat (\<lambda>k. - W k) B d
[PROOF STEP]
have dB: "B \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
lowner_is_lub (\<lambda>k. - W k) B
limit_mat (\<lambda>k. - W k) B d

goal (1 subgoal):
 1. B \<in> carrier_mat d d
[PROOF STEP]
using limit_mat_def
[PROOF STATE]
proof (prove)
using this:
lowner_is_lub (\<lambda>k. - W k) B
limit_mat (\<lambda>k. - W k) B d
limit_mat ?X ?A ?m = (\<forall>n. ?X n \<in> carrier_mat ?m ?m \<and> ?A \<in> carrier_mat ?m ?m \<and> (\<forall>i<?m. \<forall>j<?m. (\<lambda>n. ?X n $$ (i, j)) \<longlonglongrightarrow> ?A $$ (i, j)))

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

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
define A where "A = - B"
[PROOF STATE]
proof (state)
this:
A = - B

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = - B
[PROOF STEP]
have dA: "A \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
A = - B

goal (1 subgoal):
 1. A \<in> carrier_mat d d
[PROOF STEP]
using dB
[PROOF STATE]
proof (prove)
using this:
A = - B
B \<in> carrier_mat d d

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

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have "limit_mat (\<lambda>k. (-1) \<cdot>\<^sub>m (- W k)) (-1 \<cdot>\<^sub>m B) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (\<lambda>k. - 1 \<cdot>\<^sub>m - W k) (- 1 \<cdot>\<^sub>m B) d
[PROOF STEP]
using limit_mat_scale[OF limB]
[PROOF STATE]
proof (prove)
using this:
limit_mat (\<lambda>n. ?c \<cdot>\<^sub>m - W n) (?c \<cdot>\<^sub>m B) d

goal (1 subgoal):
 1. limit_mat (\<lambda>k. - 1 \<cdot>\<^sub>m - W k) (- 1 \<cdot>\<^sub>m B) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (\<lambda>k. - 1 \<cdot>\<^sub>m - W k) (- 1 \<cdot>\<^sub>m B) d

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
limit_mat (\<lambda>k. - 1 \<cdot>\<^sub>m - W k) (- 1 \<cdot>\<^sub>m B) d

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have "W k = -1 \<cdot>\<^sub>m (- W k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W k = - 1 \<cdot>\<^sub>m - W k
[PROOF STEP]
using dWk
[PROOF STATE]
proof (prove)
using this:
W ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. W k = - 1 \<cdot>\<^sub>m - W k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W ?k = - 1 \<cdot>\<^sub>m - W ?k

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
W ?k = - 1 \<cdot>\<^sub>m - W ?k

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have "-1 \<cdot>\<^sub>m B = - B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 \<cdot>\<^sub>m B = - B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- 1 \<cdot>\<^sub>m B = - B

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
limit_mat (\<lambda>k. - 1 \<cdot>\<^sub>m - W k) (- 1 \<cdot>\<^sub>m B) d
W ?k = - 1 \<cdot>\<^sub>m - W ?k
- 1 \<cdot>\<^sub>m B = - B
[PROOF STEP]
have limA: "limit_mat W A d"
[PROOF STATE]
proof (prove)
using this:
limit_mat (\<lambda>k. - 1 \<cdot>\<^sub>m - W k) (- 1 \<cdot>\<^sub>m B) d
W ?k = - 1 \<cdot>\<^sub>m - W ?k
- 1 \<cdot>\<^sub>m B = - B

goal (1 subgoal):
 1. limit_mat W A d
[PROOF STEP]
using A_def
[PROOF STATE]
proof (prove)
using this:
limit_mat (\<lambda>k. - 1 \<cdot>\<^sub>m - W k) (- 1 \<cdot>\<^sub>m B) d
W ?k = - 1 \<cdot>\<^sub>m - W ?k
- 1 \<cdot>\<^sub>m B = - B
A = - B

goal (1 subgoal):
 1. limit_mat W A d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat W A d

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
limit_mat W A d

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
have "(limit_mat W A' d \<Longrightarrow> A' = A)" for A'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat W A' d \<Longrightarrow> A' = A
[PROOF STEP]
using limit_mat_unique[of W A d] limA
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>limit_mat W A d; limit_mat W ?B d\<rbrakk> \<Longrightarrow> A = ?B
limit_mat W A d

goal (1 subgoal):
 1. limit_mat W A' d \<Longrightarrow> A' = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat W ?A' d \<Longrightarrow> ?A' = A

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
limit_mat W A d
limit_mat W ?A' d \<Longrightarrow> ?A' = A
[PROOF STEP]
have eqA: "(wlp_while (M 0) (M 1) WS P) = A"
[PROOF STATE]
proof (prove)
using this:
limit_mat W A d
limit_mat W ?A' d \<Longrightarrow> ?A' = A

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P = A
[PROOF STEP]
unfolding wlp_while_def W_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k P) A d
limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k P) ?A' d \<Longrightarrow> ?A' = A

goal (1 subgoal):
 1. (THE Q. limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) Q d) = A
[PROOF STEP]
using the_equality[of "\<lambda>X. limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) X d" A]
[PROOF STATE]
proof (prove)
using this:
limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k P) A d
limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k P) ?A' d \<Longrightarrow> ?A' = A
\<lbrakk>limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) A d; \<And>x. limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) x d \<Longrightarrow> x = A\<rbrakk> \<Longrightarrow> (THE x. limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) x d) = A

goal (1 subgoal):
 1. (THE Q. limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) WS n P) Q d) = A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
wlp_while (M 0) (M 1) WS P = A

goal (4 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
 4. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
show "limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
using limA eqA
[PROOF STATE]
proof (prove)
using this:
limit_mat W A d
wlp_while (M 0) (M 1) WS P = A

goal (1 subgoal):
 1. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k P) A d
wlp_while (M 0) (M 1) WS P = A

goal (1 subgoal):
 1. limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (\<lambda>n. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d

goal (3 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
have "- W k \<le>\<^sub>L B" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - W k \<le>\<^sub>L B
[PROOF STEP]
using lubB lowner_is_lub_def
[PROOF STATE]
proof (prove)
using this:
lowner_is_lub (\<lambda>k. - W k) B
lowner_is_lub ?f ?M = ((\<forall>n. ?f n \<le>\<^sub>L ?M) \<and> (\<forall>M'. (\<forall>n. ?f n \<le>\<^sub>L M') \<longrightarrow> ?M \<le>\<^sub>L M'))

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

goal (3 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- W ?k \<le>\<^sub>L B
[PROOF STEP]
have glbA: "A \<le>\<^sub>L W k" for k
[PROOF STATE]
proof (prove)
using this:
- W ?k \<le>\<^sub>L B

goal (1 subgoal):
 1. A \<le>\<^sub>L W k
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
- W ?k \<le>\<^sub>L B

goal (1 subgoal):
 1. - B \<le>\<^sub>L W k
[PROOF STEP]
using lowner_le_swap[of "- W k" d] dB dWk
[PROOF STATE]
proof (prove)
using this:
- W ?k \<le>\<^sub>L B
\<lbrakk>- W k \<in> carrier_mat d d; ?B \<in> carrier_mat d d; - W k \<le>\<^sub>L ?B\<rbrakk> \<Longrightarrow> - ?B \<le>\<^sub>L - (- W k)
B \<in> carrier_mat d d
W ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. - B \<le>\<^sub>L W k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A \<le>\<^sub>L W ?k

goal (3 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
 3. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<le>\<^sub>L W ?k
[PROOF STEP]
show "\<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P"
[PROOF STATE]
proof (prove)
using this:
A \<le>\<^sub>L W ?k

goal (1 subgoal):
 1. \<And>n. wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P
[PROOF STEP]
using eqA
[PROOF STATE]
proof (prove)
using this:
A \<le>\<^sub>L W ?k
wlp_while (M 0) (M 1) WS P = A

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

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

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
have "W k \<le>\<^sub>L 1\<^sub>m d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using le_qp
[PROOF STATE]
proof (prove)
using this:
W (Suc ?k) \<le>\<^sub>L W ?k \<and> is_quantum_predicate (W ?k)

goal (1 subgoal):
 1. W k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
unfolding is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
W (Suc ?k) \<le>\<^sub>L W ?k \<and> W ?k \<in> carrier_mat d d \<and> positive (W ?k) \<and> W ?k \<le>\<^sub>L 1\<^sub>m d

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

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W ?k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have "positive (1\<^sub>m d - W k)" for k
[PROOF STATE]
proof (prove)
using this:
W ?k \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. positive (1\<^sub>m d - W k)
[PROOF STEP]
using lowner_le_def
[PROOF STATE]
proof (prove)
using this:
W ?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. positive (1\<^sub>m d - W k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (1\<^sub>m d - W ?k)

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (1\<^sub>m d - W ?k)

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
have "limit_mat (\<lambda>k. 1\<^sub>m d - W k) (1\<^sub>m d - A) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (\<lambda>k. 1\<^sub>m d - W k) (1\<^sub>m d - A) d
[PROOF STEP]
using mat_minus_limit limA
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?B \<in> carrier_mat ?m ?m; limit_mat ?X ?A ?m\<rbrakk> \<Longrightarrow> limit_mat (\<lambda>n. ?B - ?X n) (?B - ?A) ?m
limit_mat W A d

goal (1 subgoal):
 1. limit_mat (\<lambda>k. 1\<^sub>m d - W k) (1\<^sub>m d - A) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (\<lambda>k. 1\<^sub>m d - W k) (1\<^sub>m d - A) d

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
positive (1\<^sub>m d - W ?k)
limit_mat (\<lambda>k. 1\<^sub>m d - W k) (1\<^sub>m d - A) d
[PROOF STEP]
have "positive (1\<^sub>m d - A)"
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d - W ?k)
limit_mat (\<lambda>k. 1\<^sub>m d - W k) (1\<^sub>m d - A) d

goal (1 subgoal):
 1. positive (1\<^sub>m d - A)
[PROOF STEP]
using pos_mat_lim_is_pos
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d - W ?k)
limit_mat (\<lambda>k. 1\<^sub>m d - W k) (1\<^sub>m d - A) d
\<lbrakk>limit_mat ?X ?A ?m; \<forall>n. positive (?X n)\<rbrakk> \<Longrightarrow> positive ?A

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

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (1\<^sub>m d - A)
[PROOF STEP]
have leA1: "A \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d - A)

goal (1 subgoal):
 1. A \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using dA lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (1\<^sub>m d - A)
A \<in> carrier_mat d 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. A \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<le>\<^sub>L 1\<^sub>m d

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
have pA: "positive A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive A
[PROOF STEP]
using pos_mat_lim_is_pos limA pWk
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>limit_mat ?X ?A ?m; \<forall>n. positive (?X n)\<rbrakk> \<Longrightarrow> positive ?A
limit_mat W A d
positive (W ?k)

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

goal (2 subgoals):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
 2. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
show "is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)
[PROOF STEP]
unfolding is_quantum_predicate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp_while (M 0) (M (Suc 0)) WS P \<in> carrier_mat d d \<and> positive (wlp_while (M 0) (M (Suc 0)) WS P) \<and> wlp_while (M 0) (M (Suc 0)) WS P \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using pA dA leA1 eqA
[PROOF STATE]
proof (prove)
using this:
positive A
A \<in> carrier_mat d d
A \<le>\<^sub>L 1\<^sub>m d
wlp_while (M 0) (M 1) WS P = A

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

goal (1 subgoal):
 1. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)

goal (1 subgoal):
 1. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
fix W'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
assume asmW': "\<forall>k. W' \<le>\<^sub>L W k"
[PROOF STATE]
proof (state)
this:
\<forall>k. W' \<le>\<^sub>L W k

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

goal (1 subgoal):
 1. W' \<in> carrier_mat d d
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
\<forall>k. dim_row W' = dim_row (W k) \<and> dim_col W' = dim_col (W k) \<and> positive (W k - W')

goal (1 subgoal):
 1. W' \<in> carrier_mat d d
[PROOF STEP]
using carrier_matD[OF dWk]
[PROOF STATE]
proof (prove)
using this:
\<forall>k. dim_row W' = dim_row (W k) \<and> dim_col W' = dim_col (W k) \<and> positive (W k - W')
dim_row (W ?k1) = d
dim_col (W ?k1) = d

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

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

goal (1 subgoal):
 1. - W k \<le>\<^sub>L - W'
[PROOF STEP]
using lowner_le_swap dWk asmW'
[PROOF STATE]
proof (prove)
using this:
W' \<in> carrier_mat d d
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n; ?A \<le>\<^sub>L ?B\<rbrakk> \<Longrightarrow> - ?B \<le>\<^sub>L - ?A
W ?k \<in> carrier_mat d d
\<forall>k. W' \<le>\<^sub>L W k

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

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

goal (1 subgoal):
 1. B \<le>\<^sub>L - W'
[PROOF STEP]
using lubB
[PROOF STATE]
proof (prove)
using this:
- W ?k \<le>\<^sub>L - W'
lowner_is_lub (\<lambda>k. - W k) B

goal (1 subgoal):
 1. B \<le>\<^sub>L - W'
[PROOF STEP]
unfolding lowner_is_lub_def
[PROOF STATE]
proof (prove)
using this:
- W ?k \<le>\<^sub>L - W'
(\<forall>n. - W n \<le>\<^sub>L B) \<and> (\<forall>M'. (\<forall>n. - W n \<le>\<^sub>L M') \<longrightarrow> B \<le>\<^sub>L M')

goal (1 subgoal):
 1. B \<le>\<^sub>L - W'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<le>\<^sub>L - W'

goal (1 subgoal):
 1. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<le>\<^sub>L - W'
[PROOF STEP]
have "W' \<le>\<^sub>L A"
[PROOF STATE]
proof (prove)
using this:
B \<le>\<^sub>L - W'

goal (1 subgoal):
 1. W' \<le>\<^sub>L A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
B \<le>\<^sub>L - W'

goal (1 subgoal):
 1. W' \<le>\<^sub>L - B
[PROOF STEP]
using lowner_le_swap[of "B" d "- W'"] dB dW'
[PROOF STATE]
proof (prove)
using this:
B \<le>\<^sub>L - W'
\<lbrakk>B \<in> carrier_mat d d; - W' \<in> carrier_mat d d; B \<le>\<^sub>L - W'\<rbrakk> \<Longrightarrow> - (- W') \<le>\<^sub>L - B
B \<in> carrier_mat d d
W' \<in> carrier_mat d d

goal (1 subgoal):
 1. W' \<le>\<^sub>L - B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W' \<le>\<^sub>L A

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

goal (1 subgoal):
 1. W' \<le>\<^sub>L wlp_while (M 0) (M 1) WS P
[PROOF STEP]
using eqA
[PROOF STATE]
proof (prove)
using this:
W' \<le>\<^sub>L A
wlp_while (M 0) (M 1) WS P = A

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

goal (1 subgoal):
 1. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>k. ?W'2 \<le>\<^sub>L W k \<Longrightarrow> ?W'2 \<le>\<^sub>L wlp_while (M 0) (M 1) WS P

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

goal (1 subgoal):
 1. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
unfolding W_def M0_def M1_def
[PROOF STATE]
proof (prove)
using this:
\<forall>k. ?W'2 \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k P \<Longrightarrow> ?W'2 \<le>\<^sub>L wlp_while (M 0) (M 1) WS P

goal (1 subgoal):
 1. \<And>W'. \<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. ?W' \<le>\<^sub>L wlp_while_n (M 0) (M (Suc 0)) WS n P \<Longrightarrow> ?W' \<le>\<^sub>L wlp_while (M 0) (M (Suc 0)) WS P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_while_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 (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
define M0 where "M0 = M 0"
[PROOF STATE]
proof (state)
this:
M0 = M 0

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

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

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
define W where "W P = wlp_while M0 M1 WS P" for P
[PROOF STATE]
proof (state)
this:
W ?P = wlp_while M0 M1 WS ?P

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
have lePQk: "Wn P k \<le>\<^sub>L Wn Q k" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wn P k \<le>\<^sub>L Wn Q k
[PROOF STEP]
unfolding Wn_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 wlp_while_n_mono assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (?WS P); \<And>P Q. \<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\<rbrakk> \<Longrightarrow> wlp_while_n (?M 0) (?M 1) ?WS ?k ?P \<le>\<^sub>L 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. 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:
Wn P ?k \<le>\<^sub>L Wn Q ?k

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
have "is_quantum_predicate (Wn P k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (Wn P k)
[PROOF STEP]
unfolding Wn_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 (Wn P ?k)

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (Wn P ?k)
[PROOF STEP]
have dWPk: "Wn P k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (Wn P ?k)

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

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
have "is_quantum_predicate (Wn Q k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (Wn Q k)
[PROOF STEP]
unfolding Wn_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 (Wn Q ?k)

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (Wn Q ?k)
[PROOF STEP]
have dWQk:"Wn Q k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (Wn Q ?k)

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

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
have "is_quantum_predicate (W P)" and lePk: "(W P) \<le>\<^sub>L (Wn P k)" and "limit_mat (Wn P) (W P) d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (W P) &&& W P \<le>\<^sub>L Wn P k &&& limit_mat (Wn P) (W P) d
[PROOF STEP]
unfolding W_def Wn_def M0_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp_while (M 0) (M 1) WS P) &&& wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k P &&& limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k P) (wlp_while (M 0) (M 1) WS P) d
[PROOF STEP]
using wlp_while_exists assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (?WS P); \<And>P Q. \<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\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp_while (?M 0) (?M 1) ?WS ?P) \<and> (\<forall>n. wlp_while (?M 0) (?M 1) ?WS ?P \<le>\<^sub>L wlp_while_n (?M 0) (?M 1) ?WS n ?P) \<and> (\<forall>W'. (\<forall>n. W' \<le>\<^sub>L wlp_while_n (?M 0) (?M 1) ?WS n ?P) \<longrightarrow> W' \<le>\<^sub>L wlp_while (?M 0) (?M 1) ?WS ?P) \<and> limit_mat (\<lambda>n. wlp_while_n (?M 0) (?M 1) ?WS n ?P) (wlp_while (?M 0) (?M 1) ?WS ?P) 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. is_quantum_predicate (wlp_while (M 0) (M 1) WS P) &&& wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k P &&& limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k P) (wlp_while (M 0) (M 1) WS P) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (W P)
W P \<le>\<^sub>L Wn P ?k
limit_mat (Wn P) (W P) d

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (W P)
W P \<le>\<^sub>L Wn P ?k
limit_mat (Wn P) (W P) d
[PROOF STEP]
have dWP: "W P \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (W P)
W P \<le>\<^sub>L Wn P ?k
limit_mat (Wn P) (W P) d

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

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
have "is_quantum_predicate (W Q)" and "(W Q) \<le>\<^sub>L (Wn Q k)"
    and glb:"(\<forall>k. W' \<le>\<^sub>L (Wn Q k)) \<longrightarrow> W' \<le>\<^sub>L (W Q)" and "limit_mat (Wn Q) (W Q) d" for k W'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_quantum_predicate (W Q) &&& W Q \<le>\<^sub>L Wn Q k) &&& (\<forall>k. W' \<le>\<^sub>L Wn Q k) \<longrightarrow> W' \<le>\<^sub>L W Q &&& limit_mat (Wn Q) (W Q) d
[PROOF STEP]
unfolding W_def Wn_def M0_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_quantum_predicate (wlp_while (M 0) (M 1) WS Q) &&& wlp_while (M 0) (M 1) WS Q \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q) &&& (\<forall>k. W' \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q) \<longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q &&& limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k Q) (wlp_while (M 0) (M 1) WS Q) d
[PROOF STEP]
using wlp_while_exists assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (?WS P); \<And>P Q. \<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\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp_while (?M 0) (?M 1) ?WS ?P) \<and> (\<forall>n. wlp_while (?M 0) (?M 1) ?WS ?P \<le>\<^sub>L wlp_while_n (?M 0) (?M 1) ?WS n ?P) \<and> (\<forall>W'. (\<forall>n. W' \<le>\<^sub>L wlp_while_n (?M 0) (?M 1) ?WS n ?P) \<longrightarrow> W' \<le>\<^sub>L wlp_while (?M 0) (?M 1) ?WS ?P) \<and> limit_mat (\<lambda>n. wlp_while_n (?M 0) (?M 1) ?WS n ?P) (wlp_while (?M 0) (?M 1) ?WS ?P) 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. (is_quantum_predicate (wlp_while (M 0) (M 1) WS Q) &&& wlp_while (M 0) (M 1) WS Q \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q) &&& (\<forall>k. W' \<le>\<^sub>L wlp_while_n (M 0) (M 1) WS k Q) \<longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q &&& limit_mat (\<lambda>k. wlp_while_n (M 0) (M 1) WS k Q) (wlp_while (M 0) (M 1) WS Q) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (W Q)
W Q \<le>\<^sub>L Wn Q ?k
(\<forall>k. ?W' \<le>\<^sub>L Wn Q k) \<longrightarrow> ?W' \<le>\<^sub>L W Q
limit_mat (Wn Q) (W Q) d

goal (1 subgoal):
 1. wlp_while (M 0) (M 1) WS P \<le>\<^sub>L wlp_while (M 0) (M 1) WS Q
[PROOF STEP]
have "W P \<le>\<^sub>L Wn Q k" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W P \<le>\<^sub>L Wn Q k
[PROOF STEP]
using lowner_le_trans[of "W P" d "Wn P k" "Wn Q k"] lePk lePQk dWPk dWQk dWP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>W P \<in> carrier_mat d d; Wn P k \<in> carrier_mat d d; Wn Q k \<in> carrier_mat d d; W P \<le>\<^sub>L Wn P k; Wn P k \<le>\<^sub>L Wn Q k\<rbrakk> \<Longrightarrow> W P \<le>\<^sub>L Wn Q k
W P \<le>\<^sub>L Wn P ?k
Wn P ?k \<le>\<^sub>L Wn Q ?k
Wn P ?k \<in> carrier_mat d d
Wn Q ?k \<in> carrier_mat d d
W P \<in> carrier_mat d d

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

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

goal (1 subgoal):
 1. W P \<le>\<^sub>L W Q
[PROOF STEP]
using glb
[PROOF STATE]
proof (prove)
using this:
W P \<le>\<^sub>L Wn Q ?k
(\<forall>k. ?W' \<le>\<^sub>L Wn Q k) \<longrightarrow> ?W' \<le>\<^sub>L W Q

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_measure_expand_m:
  assumes m: "m \<le> n" and wc: "well_com (Measure n M S)"
  shows "wlp (Measure m M S) P = matrix_sum d (\<lambda>k. adjoint (M k) * (wlp (S!k) P) * (M k)) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (Measure m M S) P = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) m
[PROOF STEP]
unfolding wlp.simps wlp_measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * (map wlp S ! k) P * M k) m = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * (map wlp S ! k) P * M k) m = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) m
[PROOF STEP]
have "k < m \<Longrightarrow> map wlp S ! k = wlp (S!k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < m \<Longrightarrow> map wlp S ! k = wlp (S ! k)
[PROOF STEP]
using wc m
[PROOF STATE]
proof (prove)
using this:
well_com (Measure n M S)
m \<le> n

goal (1 subgoal):
 1. k < m \<Longrightarrow> map wlp S ! k = wlp (S ! k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> map wlp S ! ?k = wlp (S ! ?k)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * (map wlp S ! k) P * M k) m = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < m \<Longrightarrow> map wlp S ! ?k = wlp (S ! ?k)
[PROOF STEP]
have "k < m \<Longrightarrow> (map wlp S ! k) P = wlp (S!k) P" for k
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> map wlp S ! ?k = wlp (S ! ?k)

goal (1 subgoal):
 1. k < m \<Longrightarrow> (map wlp S ! k) P = wlp (S ! k) P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> (map wlp S ! ?k) P = wlp (S ! ?k) P

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * (map wlp S ! k) P * M k) m = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < m \<Longrightarrow> (map wlp S ! ?k) P = wlp (S ! ?k) P
[PROOF STEP]
show "matrix_sum d (\<lambda>k. adjoint (M k) * ((map wlp S ! k) P) * (M k)) m
    = matrix_sum d (\<lambda>k. adjoint (M k) * (wlp (S!k) P) * (M k)) m"
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> (map wlp S ! ?k) P = wlp (S ! ?k) P

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * (map wlp S ! k) P * M k) m = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) m
[PROOF STEP]
using matrix_sum_cong[of m "\<lambda>k. adjoint (M k) * ((map wlp S ! k) P) * (M k)" "\<lambda>k. adjoint (M k) * (wlp (S!k) P) * (M k)"]
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> (map wlp S ! ?k) P = wlp (S ! ?k) P
(\<And>k. k < m \<Longrightarrow> adjoint (M k) * (map wlp S ! k) P * M k = adjoint (M k) * wlp (S ! k) P * M k) \<Longrightarrow> matrix_sum ?d (\<lambda>k. adjoint (M k) * (map wlp S ! k) P * M k) m = matrix_sum ?d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) m

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_measure_expand:
  assumes wc: "well_com (Measure n M S)"
  shows "wlp (Measure n M S) P = matrix_sum d (\<lambda>k. adjoint (M k) * (wlp (S!k) P) * (M k)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (Measure n M S) P = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n
[PROOF STEP]
using wlp_measure_expand_m[OF Nat.le_refl[of n]] wc
[PROOF STATE]
proof (prove)
using this:
well_com (Measure n ?M ?S) \<Longrightarrow> wlp (Measure n ?M ?S) ?P = matrix_sum d (\<lambda>k. adjoint (?M k) * wlp (?S ! k) ?P * ?M k) n
well_com (Measure n M S)

goal (1 subgoal):
 1. wlp (Measure n M S) P = matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n
[PROOF STEP]
by auto