[STATEMENT]
lemma wlp_complete:
  "well_com S \<Longrightarrow> is_quantum_predicate P \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}
[PROOF STEP]
proof (induct S arbitrary: P)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P. \<lbrakk>well_com SKIP; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp SKIP P} SKIP {P}
 2. \<And>x P. \<lbrakk>well_com (Utrans x); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Utrans x) P} Utrans x {P}
 3. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 4. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 5. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
case SKIP
[PROOF STATE]
proof (state)
this:
well_com SKIP
is_quantum_predicate P

goal (5 subgoals):
 1. \<And>P. \<lbrakk>well_com SKIP; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp SKIP P} SKIP {P}
 2. \<And>x P. \<lbrakk>well_com (Utrans x); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Utrans x) P} Utrans x {P}
 3. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 4. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 5. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_com SKIP
is_quantum_predicate P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
well_com SKIP
is_quantum_predicate P

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp SKIP P} SKIP {P}
[PROOF STEP]
unfolding wlp.simps
[PROOF STATE]
proof (prove)
using this:
well_com SKIP
is_quantum_predicate P

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {P} SKIP {P}
[PROOF STEP]
using hoare_partial.intros
[PROOF STATE]
proof (prove)
using this:
well_com SKIP
is_quantum_predicate P
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {?P} SKIP {?P}
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {adjoint ?U * ?P * ?U} Utrans ?U {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?R; \<turnstile>\<^sub>p {?P} ?S1.0 {?Q}; \<turnstile>\<^sub>p {?Q} ?S2.0 {?R}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S1.0;; ?S2.0 {?R}
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> is_quantum_predicate (?P k); is_quantum_predicate ?Q; \<And>k. k < ?n \<Longrightarrow> \<turnstile>\<^sub>p {?P k} ?S ! k {?Q}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {matrix_sum d (\<lambda>k. adjoint (?M k) * ?P k * ?M k) ?n} Measure ?n ?M ?S {?Q}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; \<turnstile>\<^sub>p {?Q} ?S {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1} While ?M ?S {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?P'; is_quantum_predicate ?Q'; ?P \<le>\<^sub>L ?P'; \<turnstile>\<^sub>p {?P'} ?S {?Q'}; ?Q' \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S {?Q}

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

goal (4 subgoals):
 1. \<And>x P. \<lbrakk>well_com (Utrans x); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Utrans x) P} Utrans x {P}
 2. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 3. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 4. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x P. \<lbrakk>well_com (Utrans x); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Utrans x) P} Utrans x {P}
 2. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 3. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 4. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
case (Utrans U)
[PROOF STATE]
proof (state)
this:
well_com (Utrans U)
is_quantum_predicate P

goal (4 subgoals):
 1. \<And>x P. \<lbrakk>well_com (Utrans x); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Utrans x) P} Utrans x {P}
 2. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 3. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 4. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_com (Utrans U)
is_quantum_predicate P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans U)
is_quantum_predicate P

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp (Utrans U) P} Utrans U {P}
[PROOF STEP]
unfolding wlp.simps
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans U)
is_quantum_predicate P

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {adjoint U * P * U} Utrans U {P}
[PROOF STEP]
using hoare_partial.intros
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans U)
is_quantum_predicate P
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {?P} SKIP {?P}
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {adjoint ?U * ?P * ?U} Utrans ?U {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?R; \<turnstile>\<^sub>p {?P} ?S1.0 {?Q}; \<turnstile>\<^sub>p {?Q} ?S2.0 {?R}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S1.0;; ?S2.0 {?R}
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> is_quantum_predicate (?P k); is_quantum_predicate ?Q; \<And>k. k < ?n \<Longrightarrow> \<turnstile>\<^sub>p {?P k} ?S ! k {?Q}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {matrix_sum d (\<lambda>k. adjoint (?M k) * ?P k * ?M k) ?n} Measure ?n ?M ?S {?Q}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; \<turnstile>\<^sub>p {?Q} ?S {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1} While ?M ?S {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?P'; is_quantum_predicate ?Q'; ?P \<le>\<^sub>L ?P'; \<turnstile>\<^sub>p {?P'} ?S {?Q'}; ?Q' \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S {?Q}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {adjoint U * P * U} Utrans U {P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {wlp (Utrans U) P} Utrans U {P}

goal (3 subgoals):
 1. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 2. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 3. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 2. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 3. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
case (Seq S1 S2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_com S1; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 ?P} S1 {?P}
\<lbrakk>well_com S2; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 ?P} S2 {?P}
well_com (S1;; S2)
is_quantum_predicate P

goal (3 subgoals):
 1. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 2. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 3. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_com S1; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 ?P} S1 {?P}
\<lbrakk>well_com S2; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 ?P} S2 {?P}
well_com (S1;; S2)
is_quantum_predicate P
[PROOF STEP]
have wc1: "well_com S1" and wc2: "well_com S2" and qpP: "is_quantum_predicate P"
    and p2: "\<turnstile>\<^sub>p {wlp S2 P} S2 {P}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S1; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 ?P} S1 {?P}
\<lbrakk>well_com S2; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 ?P} S2 {?P}
well_com (S1;; S2)
is_quantum_predicate P

goal (1 subgoal):
 1. (well_com S1 &&& well_com S2) &&& is_quantum_predicate P &&& \<turnstile>\<^sub>p {wlp S2 P} S2 {P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_com S1
well_com S2
is_quantum_predicate P
\<turnstile>\<^sub>p {wlp S2 P} S2 {P}

goal (3 subgoals):
 1. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 2. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 3. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have qpW2P: "is_quantum_predicate (wlp S2 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S2 P)
[PROOF STEP]
using wlp_close[OF wc2 qpP]
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S2 P)

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

goal (3 subgoals):
 1. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 2. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 3. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp S2 P)
[PROOF STEP]
have p1: "\<turnstile>\<^sub>p {wlp S1 (wlp S2 P)} S1 {wlp S2 P}"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S2 P)

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp S1 (wlp S2 P)} S1 {wlp S2 P}
[PROOF STEP]
using Seq
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S2 P)
\<lbrakk>well_com S1; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 ?P} S1 {?P}
\<lbrakk>well_com S2; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 ?P} S2 {?P}
well_com (S1;; S2)
is_quantum_predicate P

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp S1 (wlp S2 P)} S1 {wlp S2 P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {wlp S1 (wlp S2 P)} S1 {wlp S2 P}

goal (3 subgoals):
 1. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 2. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 3. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have qpW1W2P: "is_quantum_predicate (wlp S1 (wlp S2 P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S1 (wlp S2 P))
[PROOF STEP]
using wlp_close[OF wc1 qpW2P]
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S1 (wlp S2 P))

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

goal (3 subgoals):
 1. \<And>S1 S2 P. \<lbrakk>\<And>P. \<lbrakk>well_com S1; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S1 P} S1 {P}; \<And>P. \<lbrakk>well_com S2; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S2 P} S2 {P}; well_com (S1;; S2); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
 2. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 3. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp S1 (wlp S2 P))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S1 (wlp S2 P))

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}
[PROOF STEP]
unfolding wlp.simps
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S1 (wlp S2 P))

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp S1 (wlp S2 P)} S1;; S2 {P}
[PROOF STEP]
using hoare_partial.intros qpW1W2P qpW2P qpP p1 p2
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S1 (wlp S2 P))
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {?P} SKIP {?P}
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {adjoint ?U * ?P * ?U} Utrans ?U {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?R; \<turnstile>\<^sub>p {?P} ?S1.0 {?Q}; \<turnstile>\<^sub>p {?Q} ?S2.0 {?R}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S1.0;; ?S2.0 {?R}
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> is_quantum_predicate (?P k); is_quantum_predicate ?Q; \<And>k. k < ?n \<Longrightarrow> \<turnstile>\<^sub>p {?P k} ?S ! k {?Q}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {matrix_sum d (\<lambda>k. adjoint (?M k) * ?P k * ?M k) ?n} Measure ?n ?M ?S {?Q}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; \<turnstile>\<^sub>p {?Q} ?S {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1} While ?M ?S {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?P'; is_quantum_predicate ?Q'; ?P \<le>\<^sub>L ?P'; \<turnstile>\<^sub>p {?P'} ?S {?Q'}; ?Q' \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S {?Q}
is_quantum_predicate (wlp S1 (wlp S2 P))
is_quantum_predicate (wlp S2 P)
is_quantum_predicate P
\<turnstile>\<^sub>p {wlp S1 (wlp S2 P)} S1 {wlp S2 P}
\<turnstile>\<^sub>p {wlp S2 P} S2 {P}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp S1 (wlp S2 P)} S1;; S2 {P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {wlp (S1;; S2) P} S1;; S2 {P}

goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
case (Measure n M S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp ?x3a ?P} ?x3a {?P}
well_com (Measure n M S)
is_quantum_predicate P

goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp ?x3a ?P} ?x3a {?P}
well_com (Measure n M S)
is_quantum_predicate P
[PROOF STEP]
have wc: "well_com (Measure n M S)" and qpP: "is_quantum_predicate P"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp ?x3a ?P} ?x3a {?P}
well_com (Measure n M S)
is_quantum_predicate P

goal (1 subgoal):
 1. well_com (Measure n M S) &&& is_quantum_predicate P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_com (Measure n M S)
is_quantum_predicate P

goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have set: "k < n \<Longrightarrow> (S!k) \<in> set S" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> S ! k \<in> set S
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (Measure n M S)

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

goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have wck: "k < n \<Longrightarrow> well_com (S!k)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> well_com (S ! k)
[PROOF STEP]
using wc measure_well_com
[PROOF STATE]
proof (prove)
using this:
well_com (Measure n M S)
\<lbrakk>well_com (Measure ?n ?M ?S); ?k < ?n\<rbrakk> \<Longrightarrow> well_com (?S ! ?k)

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

goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> well_com (S ! ?k)
[PROOF STEP]
have qpWkP: "k < n \<Longrightarrow> is_quantum_predicate (wlp (S!k) P)" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> well_com (S ! ?k)

goal (1 subgoal):
 1. k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! k) P)
[PROOF STEP]
using wlp_close qpP
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> well_com (S ! ?k)
\<lbrakk>well_com ?S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp ?S ?P)
is_quantum_predicate P

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

goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have pk: "k < n \<Longrightarrow> \<turnstile>\<^sub>p {(wlp (S!k) P)} (S!k) {P}" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S ! k) P} S ! k {P}
[PROOF STEP]
using Measure(1) set wck qpP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp ?x3a ?P} ?x3a {?P}
?k < n \<Longrightarrow> S ! ?k \<in> set S
?k < n \<Longrightarrow> well_com (S ! ?k)
is_quantum_predicate P

goal (1 subgoal):
 1. k < n \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S ! k) P} S ! k {P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S ! ?k) P} S ! ?k {P}

goal (2 subgoals):
 1. \<And>x1 x2a x3 P. \<lbrakk>\<And>x3a P. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp x3a P} x3a {P}; well_com (Measure x1 x2a x3); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (Measure x1 x2a x3) P} Measure x1 x2a x3 {P}
 2. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp (Measure n M S) P} Measure n M S {P}
[PROOF STEP]
unfolding wlp_measure_expand[OF wc]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<^sub>p {matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n} Measure n M S {P}
[PROOF STEP]
using hoare_partial.intros qpWkP qpP pk
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {?P} SKIP {?P}
is_quantum_predicate ?P \<Longrightarrow> \<turnstile>\<^sub>p {adjoint ?U * ?P * ?U} Utrans ?U {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?R; \<turnstile>\<^sub>p {?P} ?S1.0 {?Q}; \<turnstile>\<^sub>p {?Q} ?S2.0 {?R}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S1.0;; ?S2.0 {?R}
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> is_quantum_predicate (?P k); is_quantum_predicate ?Q; \<And>k. k < ?n \<Longrightarrow> \<turnstile>\<^sub>p {?P k} ?S ! k {?Q}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {matrix_sum d (\<lambda>k. adjoint (?M k) * ?P k * ?M k) ?n} Measure ?n ?M ?S {?Q}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; \<turnstile>\<^sub>p {?Q} ?S {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1}\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * ?Q * ?M 1} While ?M ?S {?P}
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; is_quantum_predicate ?P'; is_quantum_predicate ?Q'; ?P \<le>\<^sub>L ?P'; \<turnstile>\<^sub>p {?P'} ?S {?Q'}; ?Q' \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S {?Q}
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) P)
is_quantum_predicate P
?k < n \<Longrightarrow> \<turnstile>\<^sub>p {wlp (S ! ?k) P} S ! ?k {P}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n} Measure n M S {P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {wlp (Measure n M S) P} Measure n M S {P}

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
case (While M S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_com S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S ?P} S {?P}
well_com (While M S)
is_quantum_predicate P

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_com S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S ?P} S {?P}
well_com (While M S)
is_quantum_predicate P
[PROOF STEP]
have wc: "well_com (While M S)" and wcS: "well_com S" and qpP: "is_quantum_predicate P "
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S ?P} S {?P}
well_com (While M S)
is_quantum_predicate P

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

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have qpWP: "is_quantum_predicate (wlp (While M S) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp (While M S) P)
[PROOF STEP]
using wlp_close[OF wc qpP]
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp (While M S) P)

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

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp (While M S) P)
[PROOF STEP]
have qpWWP: "is_quantum_predicate (wlp S (wlp (While M S) P))"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp (While M S) P)

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

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

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have "\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {wlp (While M S) P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {wlp (While M S) P}
[PROOF STEP]
using While(1) wcS qpWP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S ?P} S {?P}
well_com S
is_quantum_predicate (wlp (While M S) P)

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

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {wlp (While M S) P}

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
have eq: "wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
using wlp_while_split wc qpP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com (While ?M ?S); is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> wlp (While ?M ?S) ?P = adjoint (?M 0) * ?P * ?M 0 + adjoint (?M 1) * wlp ?S (wlp (While ?M ?S) ?P) * ?M 1
well_com (While M S)
is_quantum_predicate P

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

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {wlp (While M S) P}
wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1
[PROOF STEP]
have p: "\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1}"
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {wlp (While M S) P}
wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1}

goal (1 subgoal):
 1. \<And>x1 S P. \<lbrakk>\<And>P. \<lbrakk>well_com S; is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp S P} S {P}; well_com (While x1 S); is_quantum_predicate P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp (While x1 S) P} While x1 S {P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp (While M S) P} While M S {P}
[PROOF STEP]
using hoare_partial.intros(5)[OF qpP qpWWP p] eq
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>p {wlp S (wlp (While M S) P)} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1}
\<turnstile>\<^sub>p {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1} While M S {P}
wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem hoare_partial_complete:
  "\<Turnstile>\<^sub>p {P} S {Q} \<Longrightarrow> well_com S \<Longrightarrow> is_quantum_predicate P \<Longrightarrow> is_quantum_predicate Q \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Turnstile>\<^sub>p {P} S {Q}; well_com S; is_quantum_predicate P; is_quantum_predicate Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<Turnstile>\<^sub>p {P} S {Q}; well_com S; is_quantum_predicate P; is_quantum_predicate Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
assume p: "\<Turnstile>\<^sub>p {P} S {Q}" and wc: "well_com S" and qpP: "is_quantum_predicate P" and qpQ: "is_quantum_predicate Q"
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {P} S {Q}
well_com S
is_quantum_predicate P
is_quantum_predicate Q

goal (1 subgoal):
 1. \<lbrakk>\<Turnstile>\<^sub>p {P} S {Q}; well_com S; is_quantum_predicate P; is_quantum_predicate Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Turnstile>\<^sub>p {P} S {Q}
well_com S
is_quantum_predicate P
is_quantum_predicate Q
[PROOF STEP]
have dQ: "Q \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {P} S {Q}
well_com S
is_quantum_predicate P
is_quantum_predicate Q

goal (1 subgoal):
 1. Q \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {P} S {Q}
well_com S
is_quantum_predicate P
is_quantum_predicate Q
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

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

goal (1 subgoal):
 1. \<lbrakk>\<Turnstile>\<^sub>p {P} S {Q}; well_com S; is_quantum_predicate P; is_quantum_predicate Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
have qpWP: "is_quantum_predicate (wlp S Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S Q)
[PROOF STEP]
using wlp_close wc qpQ
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp ?S ?P)
well_com S
is_quantum_predicate Q

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

goal (1 subgoal):
 1. \<lbrakk>\<Turnstile>\<^sub>p {P} S {Q}; well_com S; is_quantum_predicate P; is_quantum_predicate Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp S Q)
[PROOF STEP]
have dWP: "wlp S Q \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp S Q)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. P \<le>\<^sub>L wlp S Q
[PROOF STEP]
using lowner_le_trace density_states_def qpP qpWP is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
?\<rho>2 \<in> density_states \<Longrightarrow> trace (P * ?\<rho>2) \<le> trace (wlp S Q * ?\<rho>2)
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> (?A \<le>\<^sub>L ?B) = (\<forall>\<rho>\<in>carrier_mat ?n ?n. partial_density_operator \<rho> \<longrightarrow> trace (?A * \<rho>) \<le> trace (?B * \<rho>))
density_states = {\<rho> \<in> carrier_mat d d. partial_density_operator \<rho>}
is_quantum_predicate P
is_quantum_predicate (wlp S Q)
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

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

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

goal (1 subgoal):
 1. \<lbrakk>\<Turnstile>\<^sub>p {P} S {Q}; well_com S; is_quantum_predicate P; is_quantum_predicate Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
have wlp: "\<turnstile>\<^sub>p {wlp S Q} S {Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<^sub>p {wlp S Q} S {Q}
[PROOF STEP]
using wlp_complete wc qpQ
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {wlp ?S ?P} ?S {?P}
well_com S
is_quantum_predicate Q

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

goal (1 subgoal):
 1. \<lbrakk>\<Turnstile>\<^sub>p {P} S {Q}; well_com S; is_quantum_predicate P; is_quantum_predicate Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<le>\<^sub>L wlp S Q
\<turnstile>\<^sub>p {wlp S Q} S {Q}
[PROOF STEP]
show "\<turnstile>\<^sub>p {P} S {Q}"
[PROOF STATE]
proof (prove)
using this:
P \<le>\<^sub>L wlp S Q
\<turnstile>\<^sub>p {wlp S Q} S {Q}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {P} S {Q}
[PROOF STEP]
using hoare_partial.intros(6)[OF qpP qpQ qpWP qpQ] lowner_le_refl[OF dQ]
[PROOF STATE]
proof (prove)
using this:
P \<le>\<^sub>L wlp S Q
\<turnstile>\<^sub>p {wlp S Q} S {Q}
\<lbrakk>P \<le>\<^sub>L wlp S Q; \<turnstile>\<^sub>p {wlp S Q} ?S {Q}; Q \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {P} ?S {Q}
Q \<le>\<^sub>L Q

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hoare_patial_seq_assoc_sem:
  shows "\<Turnstile>\<^sub>p {A} (S1 ;; S2) ;; S3 {B} \<longleftrightarrow> \<Turnstile>\<^sub>p {A} S1 ;; (S2 ;; S3) {B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}) = (\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B})
[PROOF STEP]
unfolding hoare_partial_correct_def denote.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>\<rho>\<in>density_states. trace (A * \<rho>) \<le> trace (B * denote S3 (denote S2 (denote S1 \<rho>))) + (trace \<rho> - trace (denote S3 (denote S2 (denote S1 \<rho>))))) = (\<forall>\<rho>\<in>density_states. trace (A * \<rho>) \<le> trace (B * denote S3 (denote S2 (denote S1 \<rho>))) + (trace \<rho> - trace (denote S3 (denote S2 (denote S1 \<rho>)))))
[PROOF STEP]
by auto


[STATEMENT]
lemma hoare_patial_seq_assoc:
  assumes "well_com S1" and "well_com S2" and "well_com S3"
    and "is_quantum_predicate A" and "is_quantum_predicate B"
  shows "\<turnstile>\<^sub>p {A} (S1 ;; S2) ;; S3 {B} \<longleftrightarrow> \<turnstile>\<^sub>p {A} S1 ;; (S2 ;; S3) {B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}) = (\<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
 2. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
assume "\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}"
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}

goal (2 subgoals):
 1. \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
 2. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
have "\<Turnstile>\<^sub>p {A} (S1 ;; S2) ;; S3 {B}"
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
using hoare_partial_sound assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
\<lbrakk>\<turnstile>\<^sub>p {?P} ?S {?Q}; well_com ?S\<rbrakk> \<Longrightarrow> \<Turnstile>\<^sub>p {?P} ?S {?Q}
well_com S1
well_com S2
well_com S3
is_quantum_predicate A
is_quantum_predicate B

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}

goal (2 subgoals):
 1. \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
 2. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
have "\<Turnstile>\<^sub>p {A} S1 ;; (S2 ;; S3) {B}"
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
using hoare_patial_seq_assoc_sem
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
(\<Turnstile>\<^sub>p {?A} ?S1.0;; ?S2.0;; ?S3.0 {?B}) = (\<Turnstile>\<^sub>p {?A} ?S1.0;; (?S2.0;; ?S3.0) {?B})

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}

goal (2 subgoals):
 1. \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
 2. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
show "\<turnstile>\<^sub>p {A} S1 ;; (S2 ;; S3) {B}"
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
using hoare_partial_complete assms
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
\<lbrakk>\<Turnstile>\<^sub>p {?P} ?S {?Q}; well_com ?S; is_quantum_predicate ?P; is_quantum_predicate ?Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S {?Q}
well_com S1
well_com S2
well_com S3
is_quantum_predicate A
is_quantum_predicate B

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
assume "\<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}"
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
have "\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}"
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
using hoare_partial_sound assms
[PROOF STATE]
proof (prove)
using this:
\<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
\<lbrakk>\<turnstile>\<^sub>p {?P} ?S {?Q}; well_com ?S\<rbrakk> \<Longrightarrow> \<Turnstile>\<^sub>p {?P} ?S {?Q}
well_com S1
well_com S2
well_com S3
is_quantum_predicate A
is_quantum_predicate B

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
[PROOF STEP]
have "\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}"
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
using hoare_patial_seq_assoc_sem
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; (S2;; S3) {B}
(\<Turnstile>\<^sub>p {?A} ?S1.0;; ?S2.0;; ?S3.0 {?B}) = (\<Turnstile>\<^sub>p {?A} ?S1.0;; (?S2.0;; ?S3.0) {?B})

goal (1 subgoal):
 1. \<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; (S2;; S3) {B} \<Longrightarrow> \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
show "\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}"
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
using hoare_partial_complete assms
[PROOF STATE]
proof (prove)
using this:
\<Turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
\<lbrakk>\<Turnstile>\<^sub>p {?P} ?S {?Q}; well_com ?S; is_quantum_predicate ?P; is_quantum_predicate ?Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>p {?P} ?S {?Q}
well_com S1
well_com S2
well_com S3
is_quantum_predicate A
is_quantum_predicate B

goal (1 subgoal):
 1. \<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>p {A} S1;; S2;; S3 {B}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valuate_poly_of_vec: assumes "w \<in> carrier_vec n"
  and "v \<in> carrier_vec n"
shows "valuate (poly_of_vec v) (val_of_vec w) = v \<bullet> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec v \<lbrace> val_of_vec w \<rbrace> = v \<bullet> w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. poly_of_vec v \<lbrace> val_of_vec w \<rbrace> = v \<bullet> w
[PROOF STEP]
by (transfer, auto simp: val_of_vec_def scalar_prod_def intro: sum.mono_neutral_left)


[STATEMENT]
lemma constraints_of_mat_vec_solution_main: assumes A: "A \<in> carrier_mat nr nc"
  and x: "x \<in> carrier_vec nc"
  and b: "b \<in> carrier_vec nr"
  and sol: "A *\<^sub>v x \<le> b"
  and c: "c \<in> constraints_of_mat_vec A b"
shows "val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
from c[unfolded constraints_of_mat_vec_def] A
[PROOF STATE]
proof (chain)
picking this:
c \<in> (\<lambda>i. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)) ` {0..<dim_row A}
A \<in> carrier_mat nr nc
[PROOF STEP]
obtain i where
    i: "i < nr" and c: "c = Leqc (poly_of_vec (row A i)) (b $ i)"
[PROOF STATE]
proof (prove)
using this:
c \<in> (\<lambda>i. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)) ` {0..<dim_row A}
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < nr; c = Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < nr
c = Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)

goal (1 subgoal):
 1. val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
from i A
[PROOF STATE]
proof (chain)
picking this:
i < nr
A \<in> carrier_mat nr nc
[PROOF STEP]
have ri: "row A i \<in> carrier_vec nc"
[PROOF STATE]
proof (prove)
using this:
i < nr
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. row A i \<in> carrier_vec nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row A i \<in> carrier_vec nc

goal (1 subgoal):
 1. val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
from sol i A x b
[PROOF STATE]
proof (chain)
picking this:
A *\<^sub>v x \<le> b
i < nr
A \<in> carrier_mat nr nc
x \<in> carrier_vec nc
b \<in> carrier_vec nr
[PROOF STEP]
have sol: "(A *\<^sub>v x) $ i \<le> b $ i"
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v x \<le> b
i < nr
A \<in> carrier_mat nr nc
x \<in> carrier_vec nc
b \<in> carrier_vec nr

goal (1 subgoal):
 1. (A *\<^sub>v x) $ i \<le> b $ i
[PROOF STEP]
unfolding less_eq_vec_def
[PROOF STATE]
proof (prove)
using this:
dim_vec (A *\<^sub>v x) = dim_vec b \<and> (\<forall>i<dim_vec b. (A *\<^sub>v x) $ i \<le> b $ i)
i < nr
A \<in> carrier_mat nr nc
x \<in> carrier_vec nc
b \<in> carrier_vec nr

goal (1 subgoal):
 1. (A *\<^sub>v x) $ i \<le> b $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A *\<^sub>v x) $ i \<le> b $ i

goal (1 subgoal):
 1. val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
thus "val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c"
[PROOF STATE]
proof (prove)
using this:
(A *\<^sub>v x) $ i \<le> b $ i

goal (1 subgoal):
 1. val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
unfolding c satisfiable_le_constraint.simps rel_of.simps
      valuate_poly_of_vec[OF x ri]
[PROOF STATE]
proof (prove)
using this:
(A *\<^sub>v x) $ i \<le> b $ i

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
using A x i
[PROOF STATE]
proof (prove)
using this:
(A *\<^sub>v x) $ i \<le> b $ i
A \<in> carrier_mat nr nc
x \<in> carrier_vec nc
i < nr

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_of_vec x \<Turnstile>\<^sub>l\<^sub>e c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_poly_of_vec: "vars (poly_of_vec v) \<subseteq> { 0 ..< dim_vec v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (poly_of_vec v) \<subseteq> {0..<dim_vec v}
[PROOF STEP]
by (transfer', auto)


[STATEMENT]
lemma finite_constraints_of_mat_vec: "finite (constraints_of_mat_vec A b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (constraints_of_mat_vec A b)
[PROOF STEP]
unfolding constraints_of_mat_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>i. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)) ` {0..<dim_row A})
[PROOF STEP]
by auto


[STATEMENT]
lemma constraints_of_mat_vec_solution_1:
  assumes A: "A \<in> carrier_mat nr nc"
    and b: "b \<in> carrier_vec nr"
    and sol: "\<exists> x \<in> carrier_vec nc. A *\<^sub>v x \<le> b"
  shows "\<exists> v. \<forall> c \<in> constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
using constraints_of_mat_vec_solution_main[OF A _ b _] sol
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier_vec nc; A *\<^sub>v ?x \<le> b; ?c \<in> constraints_of_mat_vec A b\<rbrakk> \<Longrightarrow> val_of_vec ?x \<Turnstile>\<^sub>l\<^sub>e ?c
\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b

goal (1 subgoal):
 1. \<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
by blast


[STATEMENT]
lemma constraints_of_mat_vec_solution_2:
  assumes A: "A \<in> carrier_mat nr nc"
    and b: "b \<in> carrier_vec nr"
    and sol: "\<exists> v. \<forall> c \<in> constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c"
  shows "\<exists> x \<in> carrier_vec nc. A *\<^sub>v x \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b
[PROOF STEP]
from sol
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c
[PROOF STEP]
obtain v where sol: "v \<Turnstile>\<^sub>l\<^sub>e c" if "c \<in> constraints_of_mat_vec A b" for c
[PROOF STATE]
proof (prove)
using this:
\<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c

goal (1 subgoal):
 1. (\<And>v. (\<And>c. c \<in> constraints_of_mat_vec A b \<Longrightarrow> v \<Turnstile>\<^sub>l\<^sub>e c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?c \<in> constraints_of_mat_vec A b \<Longrightarrow> v \<Turnstile>\<^sub>l\<^sub>e ?c

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b
[PROOF STEP]
define x where "x = vec nc (\<lambda> i. v i)"
[PROOF STATE]
proof (state)
this:
x = vec nc v

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b
[PROOF STEP]
proof (intro bexI[of _ x])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A *\<^sub>v x \<le> b
 2. x \<in> carrier_vec nc
[PROOF STEP]
show x: "x \<in> carrier_vec nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier_vec nc
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec nc v \<in> carrier_vec nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec nc

goal (1 subgoal):
 1. A *\<^sub>v x \<le> b
[PROOF STEP]
have "row A i \<bullet> x \<le> b $ i" if "i < nr" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
i < nr
[PROOF STEP]
have "Leqc (poly_of_vec (row A i)) (b $ i) \<in> constraints_of_mat_vec A b"
[PROOF STATE]
proof (prove)
using this:
i < nr

goal (1 subgoal):
 1. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i) \<in> constraints_of_mat_vec A b
[PROOF STEP]
unfolding constraints_of_mat_vec_def
[PROOF STATE]
proof (prove)
using this:
i < nr

goal (1 subgoal):
 1. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i) \<in> (\<lambda>i. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)) ` {0..<dim_row A}
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
i < nr
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i) \<in> (\<lambda>i. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)) ` {0..<dim_row A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i) \<in> constraints_of_mat_vec A b

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
from sol[OF this, simplified]
[PROOF STATE]
proof (chain)
picking this:
poly_of_vec (row A i) \<lbrace> v \<rbrace> \<le> b $ i
[PROOF STEP]
have "valuate (poly_of_vec (row A i)) v \<le> b $ i"
[PROOF STATE]
proof (prove)
using this:
poly_of_vec (row A i) \<lbrace> v \<rbrace> \<le> b $ i

goal (1 subgoal):
 1. poly_of_vec (row A i) \<lbrace> v \<rbrace> \<le> b $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly_of_vec (row A i) \<lbrace> v \<rbrace> \<le> b $ i

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly_of_vec (row A i) \<lbrace> v \<rbrace> \<le> b $ i

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
have "valuate (poly_of_vec (row A i)) v = valuate (poly_of_vec (row A i)) (val_of_vec x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (row A i) \<lbrace> v \<rbrace> = poly_of_vec (row A i) \<lbrace> val_of_vec x \<rbrace>
[PROOF STEP]
by (rule valuate_depend, insert A that,
          auto simp: x_def val_of_vec_def dest!: set_mp[OF vars_poly_of_vec])
[PROOF STATE]
proof (state)
this:
poly_of_vec (row A i) \<lbrace> v \<rbrace> = poly_of_vec (row A i) \<lbrace> val_of_vec x \<rbrace>

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly_of_vec (row A i) \<lbrace> v \<rbrace> = poly_of_vec (row A i) \<lbrace> val_of_vec x \<rbrace>

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
have "\<dots> = row A i \<bullet> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (row A i) \<lbrace> val_of_vec x \<rbrace> = row A i \<bullet> x
[PROOF STEP]
by (subst valuate_poly_of_vec[OF x], insert that A x, auto)
[PROOF STATE]
proof (state)
this:
poly_of_vec (row A i) \<lbrace> val_of_vec x \<rbrace> = row A i \<bullet> x

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
row A i \<bullet> x \<le> b $ i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row A i \<bullet> x \<le> b $ i

goal (1 subgoal):
 1. row A i \<bullet> x \<le> b $ i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
row A i \<bullet> x \<le> b $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> row A ?i \<bullet> x \<le> b $ ?i

goal (1 subgoal):
 1. A *\<^sub>v x \<le> b
[PROOF STEP]
thus "A *\<^sub>v x \<le> b"
[PROOF STATE]
proof (prove)
using this:
?i < nr \<Longrightarrow> row A ?i \<bullet> x \<le> b $ ?i

goal (1 subgoal):
 1. A *\<^sub>v x \<le> b
[PROOF STEP]
unfolding less_eq_vec_def
[PROOF STATE]
proof (prove)
using this:
?i < nr \<Longrightarrow> row A ?i \<bullet> x \<le> b $ ?i

goal (1 subgoal):
 1. dim_vec (A *\<^sub>v x) = dim_vec b \<and> (\<forall>i<dim_vec b. (A *\<^sub>v x) $ i \<le> b $ i)
[PROOF STEP]
using x A b
[PROOF STATE]
proof (prove)
using this:
?i < nr \<Longrightarrow> row A ?i \<bullet> x \<le> b $ ?i
x \<in> carrier_vec nc
A \<in> carrier_mat nr nc
b \<in> carrier_vec nr

goal (1 subgoal):
 1. dim_vec (A *\<^sub>v x) = dim_vec b \<and> (\<forall>i<dim_vec b. (A *\<^sub>v x) $ i \<le> b $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x \<le> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma constraints_of_mat_vec_solution:
  assumes A: "A \<in> carrier_mat nr nc"
    and b: "b \<in> carrier_vec nr"
  shows "(\<exists> x \<in> carrier_vec nc. A *\<^sub>v x \<le> b) =
    (\<exists> v. \<forall> c \<in> constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c)
[PROOF STEP]
using constraints_of_mat_vec_solution_1[OF assms] constraints_of_mat_vec_solution_2[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b \<Longrightarrow> \<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c
\<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c \<Longrightarrow> \<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<exists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c)
[PROOF STEP]
by blast