[STATEMENT]
lemma healthy_wp_SetPC:
  fixes p::"'s \<Rightarrow> 'a \<Rightarrow> real"
  and   f::"'a \<Rightarrow> 's prog"
  assumes healthy: "\<And>a s. a \<in> supp (p s) \<Longrightarrow> healthy (wp (f a))"
      and sound: "\<And>s. sound (p s)"
      and sub_dist: "\<And>s. (\<Sum>a\<in>supp (p s). p s a) \<le> 1"
  shows "healthy (wp (SetPC f p))" (is "healthy ?X")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (SetPC f p))
[PROOF STEP]
proof(intro healthy_parts bounded_byI nnegI le_funI, simp_all add:wp_eval)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
fix b and P::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
assume bP: "bounded_by b P" and nP: "nneg P"
[PROOF STATE]
proof (state)
this:
bounded_by b P
nneg P

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
hence sP: "sound P"
[PROOF STATE]
proof (prove)
using this:
bounded_by b P
nneg P

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

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from sP and bP and healthy
[PROOF STATE]
proof (chain)
picking this:
sound P
bounded_by b P
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))
[PROOF STEP]
have "\<And>a s. a \<in> supp (p s) \<Longrightarrow> wp (f a) P s \<le> b"
[PROOF STATE]
proof (prove)
using this:
sound P
bounded_by b P
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))

goal (1 subgoal):
 1. \<And>a s. a \<in> supp (p s) \<Longrightarrow> wp (f a) P s \<le> b
[PROOF STEP]
by(blast dest:healthy_bounded_byD)
[PROOF STATE]
proof (state)
this:
?a \<in> supp (p ?s) \<Longrightarrow> wp (f ?a) P ?s \<le> b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
with sound
[PROOF STATE]
proof (chain)
picking this:
sound (p ?s)
?a \<in> supp (p ?s) \<Longrightarrow> wp (f ?a) P ?s \<le> b
[PROOF STEP]
have "(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * b)"
[PROOF STATE]
proof (prove)
using this:
sound (p ?s)
?a \<in> supp (p ?s) \<Longrightarrow> wp (f ?a) P ?s \<le> b

goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * b)
[PROOF STEP]
by(blast intro:sum_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * b)

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * b)

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
have "... = (\<Sum>a\<in>supp (p s). p s a) * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * b) = sum (p s) (supp (p s)) * b
[PROOF STEP]
by(simp add:sum_distrib_right)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * b) = sum (p s) (supp (p s)) * b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * b) = sum (p s) (supp (p s)) * b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * b) = sum (p s) (supp (p s)) * b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from bP and nP
[PROOF STATE]
proof (chain)
picking this:
bounded_by b P
nneg P
[PROOF STEP]
have "0 \<le> b"
[PROOF STATE]
proof (prove)
using this:
bounded_by b P
nneg P

goal (1 subgoal):
 1. 0 \<le> b
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
with sub_dist
[PROOF STATE]
proof (chain)
picking this:
sum (p ?s) (supp (p ?s)) \<le> 1
0 \<le> b
[PROOF STEP]
have "(\<Sum>a\<in>supp (p s). p s a) * b \<le> 1 * b"
[PROOF STATE]
proof (prove)
using this:
sum (p ?s) (supp (p ?s)) \<le> 1
0 \<le> b

goal (1 subgoal):
 1. sum (p s) (supp (p s)) * b \<le> 1 * b
[PROOF STEP]
by(rule mult_right_mono)
[PROOF STATE]
proof (state)
this:
sum (p s) (supp (p s)) * b \<le> 1 * b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
sum (p s) (supp (p s)) * b \<le> 1 * b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (p s) (supp (p s)) * b \<le> 1 * b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
have "1 * b = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * b = b
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
1 * b = b

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> b
[PROOF STEP]
show "(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> b"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> b

goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> b

goal (3 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x)
 2. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 3. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
show "0 \<le> (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s)
[PROOF STEP]
proof(rule sum_nonneg [OF mult_nonneg_nonneg])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> p s a
 2. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wp (f a) P s
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> p s a
 2. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wp (f a) P s
[PROOF STEP]
from sound
[PROOF STATE]
proof (chain)
picking this:
sound (p ?s)
[PROOF STEP]
show "0 \<le> p s x"
[PROOF STATE]
proof (prove)
using this:
sound (p ?s)

goal (1 subgoal):
 1. 0 \<le> p s x
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> p s x

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wp (f a) P s
[PROOF STEP]
assume "x \<in> supp (p s)"
[PROOF STATE]
proof (state)
this:
x \<in> supp (p s)

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wp (f a) P s
[PROOF STEP]
with sP and healthy
[PROOF STATE]
proof (chain)
picking this:
sound P
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))
x \<in> supp (p s)
[PROOF STEP]
show "0 \<le> wp (f x) P s"
[PROOF STATE]
proof (prove)
using this:
sound P
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))
x \<in> supp (p s)

goal (1 subgoal):
 1. 0 \<le> wp (f x) P s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> wp (f x) P s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s)

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and Q::"'s \<Rightarrow> real" and s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
assume s_P: "sound P" and s_Q: "sound Q" and ent: "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
sound P
sound Q
P \<tturnstile> Q

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
with healthy
[PROOF STATE]
proof (chain)
picking this:
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))
sound P
sound Q
P \<tturnstile> Q
[PROOF STEP]
have "\<And>a. a \<in> supp (p s) \<Longrightarrow> wp (f a) P s \<le> wp (f a) Q s"
[PROOF STATE]
proof (prove)
using this:
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))
sound P
sound Q
P \<tturnstile> Q

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> wp (f a) P s \<le> wp (f a) Q s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
?a \<in> supp (p s) \<Longrightarrow> wp (f ?a) P s \<le> wp (f ?a) Q s

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wp (f a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
with sound
[PROOF STATE]
proof (chain)
picking this:
sound (p ?s)
?a \<in> supp (p s) \<Longrightarrow> wp (f ?a) P s \<le> wp (f ?a) Q s
[PROOF STEP]
show "(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le>
                   (\<Sum>a\<in>supp (p s). p s a * wp (f a) Q s)"
[PROOF STATE]
proof (prove)
using this:
sound (p ?s)
?a \<in> supp (p s) \<Longrightarrow> wp (f ?a) P s \<le> wp (f ?a) Q s

goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * wp (f a) Q s)
[PROOF STEP]
by(blast intro:sum_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * wp (f a) Q s)

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and c::real and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
assume sound: "sound P" and pos: "0 \<le> c"
[PROOF STATE]
proof (state)
this:
sound P
0 \<le> c

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
have "c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) =
        (\<Sum>a\<in>supp (p s). p s a * (c * wp (f a) P s))"
       (is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) = (\<Sum>a\<in>supp (p s). p s a * (c * wp (f a) P s))
[PROOF STEP]
by(simp add:sum_distrib_left ac_simps)
[PROOF STATE]
proof (state)
this:
c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) = (\<Sum>a\<in>supp (p s). p s a * (c * wp (f a) P s))

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) = (\<Sum>a\<in>supp (p s). p s a * (c * wp (f a) P s))

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from sound and pos and healthy
[PROOF STATE]
proof (chain)
picking this:
sound P
0 \<le> c
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))
[PROOF STEP]
have "... = (\<Sum>a\<in>supp (p s). p s a * wp (f a) (\<lambda>s. c * P s) s)"
[PROOF STATE]
proof (prove)
using this:
sound P
0 \<le> c
?a \<in> supp (p ?s) \<Longrightarrow> healthy (wp (f ?a))

goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * (c * wp (f a) P s)) = (\<Sum>a\<in>supp (p s). p s a * wp (f a) (\<lambda>s. c * P s) s)
[PROOF STEP]
by(auto simp:scalingD[OF healthy_scalingD])
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * (c * wp (f a) P s)) = (\<Sum>a\<in>supp (p s). p s a * wp (f a) (\<lambda>s. c * P s) s)

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (\<Sum>a\<in>supp (p x). p x a * wp (f a) P x) = (\<Sum>a\<in>supp (p x). p x a * wp (f a) (\<lambda>x. c * P x) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) = (\<Sum>a\<in>supp (p s). p s a * wp (f a) (\<lambda>s. c * P s) s)
[PROOF STEP]
show "?A = ..."
[PROOF STATE]
proof (prove)
using this:
c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) = (\<Sum>a\<in>supp (p s). p s a * wp (f a) (\<lambda>s. c * P s) s)

goal (1 subgoal):
 1. c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) = (\<Sum>a\<in>supp (p s). p s a * wp (f a) (\<lambda>s. c * P s) s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c * (\<Sum>a\<in>supp (p s). p s a * wp (f a) P s) = (\<Sum>a\<in>supp (p s). p s a * wp (f a) (\<lambda>s. c * P s) s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_SetPC:
  fixes p::"'s \<Rightarrow> 'a \<Rightarrow> real"
  and   f::"'a \<Rightarrow> 's prog"
  assumes healthy: "\<And>a s. a \<in> supp (p s) \<Longrightarrow> nearly_healthy (wlp (f a))"
      and sound: "\<And>s. sound (p s)"
      and sub_dist: "\<And>s. (\<Sum>a\<in>supp (p s). p s a) \<le> 1"
  shows "nearly_healthy (wlp (SetPC f p))" (is "nearly_healthy ?X")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (SetPC f p))
[PROOF STEP]
proof(intro nearly_healthyI unitaryI2 bounded_byI nnegI le_funI, simp_all only:wp_eval)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
fix b and P::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
assume uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
from uP healthy
[PROOF STATE]
proof (chain)
picking this:
unitary P
?a \<in> supp (p ?s) \<Longrightarrow> nearly_healthy (wlp (f ?a))
[PROOF STEP]
have "\<And>a. a \<in> supp (p s) \<Longrightarrow> unitary (wlp (f a) P)"
[PROOF STATE]
proof (prove)
using this:
unitary P
?a \<in> supp (p ?s) \<Longrightarrow> nearly_healthy (wlp (f ?a))

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> unitary (wlp (f a) P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
?a \<in> supp (p s) \<Longrightarrow> unitary (wlp (f ?a) P)

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
hence "\<And>a. a \<in> supp (p s) \<Longrightarrow> wlp (f a) P s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
?a \<in> supp (p s) \<Longrightarrow> unitary (wlp (f ?a) P)

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> wlp (f a) P s \<le> 1
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
?a \<in> supp (p s) \<Longrightarrow> wlp (f ?a) P s \<le> 1

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
with sound
[PROOF STATE]
proof (chain)
picking this:
sound (p ?s)
?a \<in> supp (p s) \<Longrightarrow> wlp (f ?a) P s \<le> 1
[PROOF STEP]
have "(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * 1)"
[PROOF STATE]
proof (prove)
using this:
sound (p ?s)
?a \<in> supp (p s) \<Longrightarrow> wlp (f ?a) P s \<le> 1

goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * 1)
[PROOF STEP]
by(blast intro:sum_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * 1)

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * 1)

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
have "... = (\<Sum>a\<in>supp (p s). p s a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * 1) = sum (p s) (supp (p s))
[PROOF STEP]
by(simp add:sum_distrib_right)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * 1) = sum (p s) (supp (p s))

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * 1) = sum (p s) (supp (p s))

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
note sub_dist
[PROOF STATE]
proof (state)
this:
sum (p ?s) (supp (p ?s)) \<le> 1

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> 1
[PROOF STEP]
show "(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> 1

goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> 1

goal (2 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x)
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
show "0 \<le> (\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s)
[PROOF STEP]
proof(rule sum_nonneg [OF mult_nonneg_nonneg])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> p s a
 2. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wlp (f a) P s
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> p s a
 2. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wlp (f a) P s
[PROOF STEP]
from sound
[PROOF STATE]
proof (chain)
picking this:
sound (p ?s)
[PROOF STEP]
show "0 \<le> p s x"
[PROOF STATE]
proof (prove)
using this:
sound (p ?s)

goal (1 subgoal):
 1. 0 \<le> p s x
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> p s x

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wlp (f a) P s
[PROOF STEP]
assume "x \<in> supp (p s)"
[PROOF STATE]
proof (state)
this:
x \<in> supp (p s)

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> 0 \<le> wlp (f a) P s
[PROOF STEP]
with uP healthy
[PROOF STATE]
proof (chain)
picking this:
unitary P
?a \<in> supp (p ?s) \<Longrightarrow> nearly_healthy (wlp (f ?a))
x \<in> supp (p s)
[PROOF STEP]
show "0 \<le> wlp (f x) P s"
[PROOF STATE]
proof (prove)
using this:
unitary P
?a \<in> supp (p ?s) \<Longrightarrow> nearly_healthy (wlp (f ?a))
x \<in> supp (p s)

goal (1 subgoal):
 1. 0 \<le> wlp (f x) P s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> wlp (f x) P s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s)

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
fix P::"'s expect" and Q::"'s expect" and s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
assume uP: "unitary P" and uQ: "unitary Q" and le: "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> Q

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
hence "\<And>a. a \<in> supp (p s) \<Longrightarrow> wlp (f a) P s \<le> wlp (f a) Q s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
P \<tturnstile> Q

goal (1 subgoal):
 1. \<And>a. a \<in> supp (p s) \<Longrightarrow> wlp (f a) P s \<le> wlp (f a) Q s
[PROOF STEP]
by(blast intro:le_funD[OF nearly_healthy_monoD, OF healthy])
[PROOF STATE]
proof (state)
this:
?a \<in> supp (p s) \<Longrightarrow> wlp (f ?a) P s \<le> wlp (f ?a) Q s

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) P x) \<le> (\<Sum>a\<in>supp (p x). p x a * wlp (f a) Q x)
[PROOF STEP]
with sound
[PROOF STATE]
proof (chain)
picking this:
sound (p ?s)
?a \<in> supp (p s) \<Longrightarrow> wlp (f ?a) P s \<le> wlp (f ?a) Q s
[PROOF STEP]
show "(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le>
                   (\<Sum>a\<in>supp (p s). p s a * wlp (f a) Q s)"
[PROOF STATE]
proof (prove)
using this:
sound (p ?s)
?a \<in> supp (p s) \<Longrightarrow> wlp (f ?a) P s \<le> wlp (f ?a) Q s

goal (1 subgoal):
 1. (\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * wlp (f a) Q s)
[PROOF STEP]
by(blast intro:sum_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>supp (p s). p s a * wlp (f a) P s) \<le> (\<Sum>a\<in>supp (p s). p s a * wlp (f a) Q s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma healthy_wp_Apply:
  "healthy (wp (Apply f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (Apply f))
[PROOF STEP]
unfolding Apply_def wp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (\<lambda>P s. P (f s))
[PROOF STEP]
by(blast)


[STATEMENT]
lemma nearly_healthy_wlp_Apply:
  "nearly_healthy (wlp (Apply f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (Apply f))
[PROOF STEP]
by(intro nearly_healthyI unitaryI2 nnegI bounded_byI, auto simp:o_def wp_eval)


[STATEMENT]
lemma healthy_wp_Bind:
  fixes f::"'s \<Rightarrow> 'a"
  assumes hsub: "\<And>s. healthy (wp (p (f s)))"
  shows "healthy (wp (Bind f p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (Bind f p))
[PROOF STEP]
proof(intro healthy_parts nnegI bounded_byI le_funI, simp_all only:wp_eval)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> wp (p (f x)) P x
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
fix b and P::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> wp (p (f x)) P x
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
assume bP: "bounded_by b P" and nP: "nneg P"
[PROOF STATE]
proof (state)
this:
bounded_by b P
nneg P

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> wp (p (f x)) P x
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
with hsub
[PROOF STATE]
proof (chain)
picking this:
healthy (wp (p (f ?s)))
bounded_by b P
nneg P
[PROOF STEP]
have "bounded_by b (wp (p (f s)) P)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp (p (f ?s)))
bounded_by b P
nneg P

goal (1 subgoal):
 1. bounded_by b (wp (p (f s)) P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by b (wp (p (f s)) P)

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> wp (p (f x)) P x
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
thus "wp (p (f s)) P s \<le> b"
[PROOF STATE]
proof (prove)
using this:
bounded_by b (wp (p (f s)) P)

goal (1 subgoal):
 1. wp (p (f s)) P s \<le> b
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp (p (f s)) P s \<le> b

goal (3 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> wp (p (f x)) P x
 2. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 3. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
from bP nP hsub
[PROOF STATE]
proof (chain)
picking this:
bounded_by b P
nneg P
healthy (wp (p (f ?s)))
[PROOF STEP]
have "nneg (wp (p (f s)) P)"
[PROOF STATE]
proof (prove)
using this:
bounded_by b P
nneg P
healthy (wp (p (f ?s)))

goal (1 subgoal):
 1. nneg (wp (p (f s)) P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
nneg (wp (p (f s)) P)

goal (3 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> wp (p (f x)) P x
 2. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 3. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
thus "0 \<le> wp (p (f s)) P s"
[PROOF STATE]
proof (prove)
using this:
nneg (wp (p (f s)) P)

goal (1 subgoal):
 1. 0 \<le> wp (p (f s)) P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> wp (p (f s)) P s

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
fix P Q::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
assume "sound P" "sound Q" "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
sound P
sound Q
P \<tturnstile> Q

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp (p (f x)) P x \<le> wp (p (f x)) Q x
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
thus "wp (p (f s)) P s \<le> wp (p (f s)) Q s"
[PROOF STATE]
proof (prove)
using this:
sound P
sound Q
P \<tturnstile> Q

goal (1 subgoal):
 1. wp (p (f s)) P s \<le> wp (p (f s)) Q s
[PROOF STEP]
by(rule le_funD[OF mono_transD, OF healthy_monoD, OF hsub])
[PROOF STATE]
proof (state)
this:
wp (p (f s)) P s \<le> wp (p (f s)) Q s

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
fix P::"'s expect" and c::real and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
assume "sound P" and "0 \<le> c"
[PROOF STATE]
proof (state)
this:
sound P
0 \<le> c

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp (p (f x)) P x = wp (p (f x)) (\<lambda>x. c * P x) x
[PROOF STEP]
thus "c * wp (p (f s)) P s = wp (p (f s)) (\<lambda>s. c * P s) s"
[PROOF STATE]
proof (prove)
using this:
sound P
0 \<le> c

goal (1 subgoal):
 1. c * wp (p (f s)) P s = wp (p (f s)) (\<lambda>s. c * P s) s
[PROOF STEP]
by(simp add:scalingD[OF healthy_scalingD, OF hsub])
[PROOF STATE]
proof (state)
this:
c * wp (p (f s)) P s = wp (p (f s)) (\<lambda>s. c * P s) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_Bind:
  fixes f::"'s \<Rightarrow> 'a"
  assumes hsub: "\<And>s. nearly_healthy (wlp (p (f s)))"
  shows "nearly_healthy (wlp (Bind f p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (Bind f p))
[PROOF STEP]
proof(intro nearly_healthyI unitaryI2 nnegI bounded_byI le_funI, simp_all only:wp_eval)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp (p (f x)) P x
 2. \<And>P x. unitary P \<Longrightarrow> wlp (p (f x)) P x \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp (p (f x)) P x \<le> wlp (p (f x)) Q x
[PROOF STEP]
fix P::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp (p (f x)) P x
 2. \<And>P x. unitary P \<Longrightarrow> wlp (p (f x)) P x \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp (p (f x)) P x \<le> wlp (p (f x)) Q x
[PROOF STEP]
assume uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp (p (f x)) P x
 2. \<And>P x. unitary P \<Longrightarrow> wlp (p (f x)) P x \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp (p (f x)) P x \<le> wlp (p (f x)) Q x
[PROOF STEP]
with hsub
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp (p (f ?s)))
unitary P
[PROOF STEP]
have "unitary (wlp (p (f s)) P)"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp (p (f ?s)))
unitary P

goal (1 subgoal):
 1. unitary (wlp (p (f s)) P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (wlp (p (f s)) P)

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp (p (f x)) P x
 2. \<And>P x. unitary P \<Longrightarrow> wlp (p (f x)) P x \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp (p (f x)) P x \<le> wlp (p (f x)) Q x
[PROOF STEP]
thus "0 \<le> wlp (p (f s)) P s" "wlp (p (f s)) P s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary (wlp (p (f s)) P)

goal (1 subgoal):
 1. 0 \<le> wlp (p (f s)) P s &&& wlp (p (f s)) P s \<le> 1
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> wlp (p (f s)) P s
wlp (p (f s)) P s \<le> 1

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp (p (f x)) P x \<le> wlp (p (f x)) Q x
[PROOF STEP]
fix Q::"'s expect"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp (p (f x)) P x \<le> wlp (p (f x)) Q x
[PROOF STEP]
assume "unitary Q" "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
unitary Q
P \<tturnstile> Q

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp (p (f x)) P x \<le> wlp (p (f x)) Q x
[PROOF STEP]
with uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
P \<tturnstile> Q
[PROOF STEP]
show "wlp (p (f s)) P s \<le> wlp (p (f s)) Q s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
P \<tturnstile> Q

goal (1 subgoal):
 1. wlp (p (f s)) P s \<le> wlp (p (f s)) Q s
[PROOF STEP]
by(blast intro:le_funD[OF nearly_healthy_monoD, OF hsub])
[PROOF STATE]
proof (state)
this:
wlp (p (f s)) P s \<le> wlp (p (f s)) Q s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wp_loop_step_mono:
  fixes t u::"'s trans"
  assumes hb: "healthy (wp body)"
      and le: "le_trans t u"
      and ht: "\<And>P. sound P \<Longrightarrow> sound (t P)"
      and hu: "\<And>P. sound P \<Longrightarrow> sound (u P)"
  shows "le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
                  (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
proof(intro le_transI le_funI, simp add:wp_eval)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wp body (u P) x
[PROOF STEP]
fix P::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wp body (u P) x
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wp body (u P) x
[PROOF STEP]
with le
[PROOF STATE]
proof (chain)
picking this:
le_trans t u
sound P
[PROOF STEP]
have "t P \<tturnstile> u P"
[PROOF STATE]
proof (prove)
using this:
le_trans t u
sound P

goal (1 subgoal):
 1. t P \<tturnstile> u P
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
t P \<tturnstile> u P

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wp body (u P) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t P \<tturnstile> u P

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wp body (u P) x
[PROOF STEP]
from sP ht hu
[PROOF STATE]
proof (chain)
picking this:
sound P
sound ?P \<Longrightarrow> sound (t ?P)
sound ?P \<Longrightarrow> sound (u ?P)
[PROOF STEP]
have "sound (t P)" "sound (u P)"
[PROOF STATE]
proof (prove)
using this:
sound P
sound ?P \<Longrightarrow> sound (t ?P)
sound ?P \<Longrightarrow> sound (u ?P)

goal (1 subgoal):
 1. sound (t P) &&& sound (u P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sound (t P)
sound (u P)

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wp body (u P) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t P \<tturnstile> u P
sound (t P)
sound (u P)
[PROOF STEP]
have "wp body (t P) s \<le> wp body (u P) s"
[PROOF STATE]
proof (prove)
using this:
t P \<tturnstile> u P
sound (t P)
sound (u P)

goal (1 subgoal):
 1. wp body (t P) s \<le> wp body (u P) s
[PROOF STEP]
by(auto intro:le_funD[OF mono_transD, OF healthy_monoD, OF hb])
[PROOF STATE]
proof (state)
this:
wp body (t P) s \<le> wp body (u P) s

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wp body (u P) x
[PROOF STEP]
thus "\<guillemotleft>G\<guillemotright> s * wp body (t P) s \<le> \<guillemotleft>G\<guillemotright> s * wp body (u P) s "
[PROOF STATE]
proof (prove)
using this:
wp body (t P) s \<le> wp body (u P) s

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wp body (t P) s \<le> \<guillemotleft> G \<guillemotright> s * wp body (u P) s
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wp body (t P) s \<le> \<guillemotleft> G \<guillemotright> s * wp body (u P) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_loop_step_mono:
  fixes t u::"'s trans"
  assumes mb: "nearly_healthy (wlp body)"
      and le: "le_utrans t u"
      and ht: "\<And>P. unitary P \<Longrightarrow> unitary (t P)"
      and hu: "\<And>P. unitary P \<Longrightarrow> unitary (u P)"
  shows "le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
                   (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
proof(intro le_utransI le_funI, simp add:wp_eval)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wlp body (u P) x
[PROOF STEP]
fix P::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wlp body (u P) x
[PROOF STEP]
assume uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wlp body (u P) x
[PROOF STEP]
with le
[PROOF STATE]
proof (chain)
picking this:
le_utrans t u
unitary P
[PROOF STEP]
have "t P \<tturnstile> u P"
[PROOF STATE]
proof (prove)
using this:
le_utrans t u
unitary P

goal (1 subgoal):
 1. t P \<tturnstile> u P
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
t P \<tturnstile> u P

goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wlp body (u P) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t P \<tturnstile> u P

goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wlp body (u P) x
[PROOF STEP]
from uP ht hu
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary ?P \<Longrightarrow> unitary (u ?P)
[PROOF STEP]
have "unitary (t P)" "unitary (u P)"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary ?P \<Longrightarrow> unitary (u ?P)

goal (1 subgoal):
 1. unitary (t P) &&& unitary (u P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (t P)
unitary (u P)

goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wlp body (u P) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t P \<tturnstile> u P
unitary (t P)
unitary (u P)
[PROOF STEP]
have "wlp body (t P) s \<le> wlp body (u P) s"
[PROOF STATE]
proof (prove)
using this:
t P \<tturnstile> u P
unitary (t P)
unitary (u P)

goal (1 subgoal):
 1. wlp body (t P) s \<le> wlp body (u P) s
[PROOF STEP]
by(rule le_funD[OF nearly_healthy_monoD[OF mb]])
[PROOF STATE]
proof (state)
this:
wlp body (t P) s \<le> wlp body (u P) s

goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x \<le> \<guillemotleft> G \<guillemotright> x * wlp body (u P) x
[PROOF STEP]
thus "\<guillemotleft>G\<guillemotright> s * wlp body (t P) s \<le> \<guillemotleft>G\<guillemotright> s * wlp body (u P) s "
[PROOF STATE]
proof (prove)
using this:
wlp body (t P) s \<le> wlp body (u P) s

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wlp body (t P) s \<le> \<guillemotleft> G \<guillemotright> s * wlp body (u P) s
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wlp body (t P) s \<le> \<guillemotleft> G \<guillemotright> s * wlp body (u P) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lfp_loop_fp:
  assumes hb: "healthy (wp body)"
      and sP: "sound P"
  shows "\<lambda>s. \<guillemotleft>G\<guillemotright> s * wp body (\<lambda>s. bound_of P) s + \<guillemotleft>\<N> G\<guillemotright> s * P s \<tturnstile> \<lambda>s. bound_of P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. bound_of P) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<tturnstile> \<lambda>s. bound_of P
[PROOF STEP]
proof(rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "sound (\<lambda>s. bound_of P)"
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. sound (\<lambda>s. bound_of P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sound (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sound (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
hence "bounded_by (bound_of P) (\<lambda>s. bound_of P)"
[PROOF STATE]
proof (prove)
using this:
sound (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. bounded_by (bound_of P) (\<lambda>s. bound_of P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of P) (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sound (\<lambda>s. bound_of P)
bounded_by (bound_of P) (\<lambda>s. bound_of P)
[PROOF STEP]
have "bounded_by (bound_of P) (wp body (\<lambda>s. bound_of P))"
[PROOF STATE]
proof (prove)
using this:
sound (\<lambda>s. bound_of P)
bounded_by (bound_of P) (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. bounded_by (bound_of P) (wp body (\<lambda>s. bound_of P))
[PROOF STEP]
using hb
[PROOF STATE]
proof (prove)
using this:
sound (\<lambda>s. bound_of P)
bounded_by (bound_of P) (\<lambda>s. bound_of P)
healthy (wp body)

goal (1 subgoal):
 1. bounded_by (bound_of P) (wp body (\<lambda>s. bound_of P))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of P) (wp body (\<lambda>s. bound_of P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
hence "wp body (\<lambda>s. bound_of P) s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
bounded_by (bound_of P) (wp body (\<lambda>s. bound_of P))

goal (1 subgoal):
 1. wp body (\<lambda>s. bound_of P) s \<le> bound_of P
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp body (\<lambda>s. bound_of P) s \<le> bound_of P

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wp body (\<lambda>s. bound_of P) s \<le> bound_of P

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "P s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. P s \<le> bound_of P
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
P s \<le> bound_of P

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wp body (\<lambda>s. bound_of P) s \<le> bound_of P
P s \<le> bound_of P
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> s * wp body (\<lambda>a. bound_of P) s + (1 - \<guillemotleft>G\<guillemotright> s) * P s \<le>
                   \<guillemotleft>G\<guillemotright> s * bound_of P + (1 - \<guillemotleft>G\<guillemotright> s) * bound_of P"
[PROOF STATE]
proof (prove)
using this:
wp body (\<lambda>s. bound_of P) s \<le> bound_of P
P s \<le> bound_of P

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>a. bound_of P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * bound_of P + (1 - \<guillemotleft> G \<guillemotright> s) * bound_of P
[PROOF STEP]
by(blast intro:add_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wp body (\<lambda>a. bound_of P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * bound_of P + (1 - \<guillemotleft> G \<guillemotright> s) * bound_of P

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. bound_of P) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> bound_of P
[PROOF STEP]
thus "\<guillemotleft>G\<guillemotright> s * wp body (\<lambda>a. bound_of P) s + \<guillemotleft>\<N> G\<guillemotright> s * P s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> s * wp body (\<lambda>a. bound_of P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * bound_of P + (1 - \<guillemotleft> G \<guillemotright> s) * bound_of P

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>a. bound_of P) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<le> bound_of P
[PROOF STEP]
by(simp add:algebra_simps negate_embed)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wp body (\<lambda>a. bound_of P) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<le> bound_of P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lfp_loop_greatest:
  fixes P::"'s expect"
  assumes lb: "\<And>R. \<lambda>s. \<guillemotleft>G\<guillemotright> s * wp body R s + \<guillemotleft>\<N> G\<guillemotright> s * P s \<tturnstile> R \<Longrightarrow> sound R \<Longrightarrow> Q \<tturnstile> R"
      and hb: "healthy (wp body)"
      and sP: "sound P"
      and sQ: "sound Q"
  shows "Q \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
using sP
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. Q \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
by(auto intro!:lfp_exp_greatest[OF lb sQ] sP lfp_loop_fp hb)


[STATEMENT]
lemma lfp_loop_sound:
  fixes P::"'s expect"
  assumes hb: "healthy (wp body)"
      and sP: "sound P"
  shows "sound (lfp_exp (\<lambda>Q s. \<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
sound P

goal (1 subgoal):
 1. sound (lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s))
[PROOF STEP]
by(auto intro!:lfp_exp_sound lfp_loop_fp)


[STATEMENT]
lemma wlp_loop_step_unitary:
  fixes t u::"'s trans"
  assumes hb: "nearly_healthy (wlp body)"
      and ht: "\<And>P. unitary P \<Longrightarrow> unitary (t P)"
      and uP: "unitary P"
  shows "unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
[PROOF STEP]
proof(intro unitaryI2 nnegI bounded_byI, simp_all add:wp_eval)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
 2. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
fix s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
 2. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
from ht uP
[PROOF STATE]
proof (chain)
picking this:
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary P
[PROOF STEP]
have utP: "unitary (t P)"
[PROOF STATE]
proof (prove)
using this:
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary P

goal (1 subgoal):
 1. unitary (t P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (t P)

goal (2 subgoals):
 1. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
 2. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
with hb
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp body)
unitary (t P)
[PROOF STEP]
have "unitary (wlp body (t P))"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp body)
unitary (t P)

goal (1 subgoal):
 1. unitary (wlp body (t P))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (wlp body (t P))

goal (2 subgoals):
 1. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
 2. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
hence "0 \<le> wlp body (t P) s"
[PROOF STATE]
proof (prove)
using this:
unitary (wlp body (t P))

goal (1 subgoal):
 1. 0 \<le> wlp body (t P) s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> wlp body (t P) s

goal (2 subgoals):
 1. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
 2. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
with uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
0 \<le> wlp body (t P) s
[PROOF STEP]
show "0 \<le> \<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s"
[PROOF STATE]
proof (prove)
using this:
unitary P
0 \<le> wlp body (t P) s

goal (1 subgoal):
 1. 0 \<le> \<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s
[PROOF STEP]
by(auto intro!:add_nonneg_nonneg mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> \<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
from ht uP
[PROOF STATE]
proof (chain)
picking this:
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary P
[PROOF STEP]
have "bounded_by 1 (t P)"
[PROOF STATE]
proof (prove)
using this:
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary P

goal (1 subgoal):
 1. bounded_by 1 (t P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by 1 (t P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
with utP hb
[PROOF STATE]
proof (chain)
picking this:
unitary (t P)
nearly_healthy (wlp body)
bounded_by 1 (t P)
[PROOF STEP]
have "bounded_by 1 (wlp body (t P))"
[PROOF STATE]
proof (prove)
using this:
unitary (t P)
nearly_healthy (wlp body)
bounded_by 1 (t P)

goal (1 subgoal):
 1. bounded_by 1 (wlp body (t P))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by 1 (wlp body (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
hence "wlp body (t P) s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 (wlp body (t P))

goal (1 subgoal):
 1. wlp body (t P) s \<le> 1
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wlp body (t P) s \<le> 1

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
with uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
wlp body (t P) s \<le> 1
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft>G\<guillemotright> s) * P s \<le> \<guillemotleft>G\<guillemotright> s * 1 + (1 - \<guillemotleft>G\<guillemotright> s) * 1"
[PROOF STATE]
proof (prove)
using this:
unitary P
wlp body (t P) s \<le> 1

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * 1 + (1 - \<guillemotleft> G \<guillemotright> s) * 1
[PROOF STEP]
by(blast intro:add_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * 1 + (1 - \<guillemotleft> G \<guillemotright> s) * 1

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * 1 + (1 - \<guillemotleft> G \<guillemotright> s) * 1

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
have "... = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * 1 + (1 - \<guillemotleft> G \<guillemotright> s) * 1 = 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * 1 + (1 - \<guillemotleft> G \<guillemotright> s) * 1 = 1

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> 1
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft>G\<guillemotright> s) * P s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> 1

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wlp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wp_loop_step_sound:
  fixes t u::"'s trans"
  assumes hb: "healthy (wp body)"
      and ht: "\<And>P. sound P \<Longrightarrow> sound (t P)"
      and sP: "sound P"
  shows "sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
[PROOF STEP]
proof(intro soundI2 nnegI bounded_byI, simp_all add:wp_eval)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
 2. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
[PROOF STEP]
fix s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
 2. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
[PROOF STEP]
from ht sP
[PROOF STATE]
proof (chain)
picking this:
sound ?P \<Longrightarrow> sound (t ?P)
sound P
[PROOF STEP]
have stP: "sound (t P)"
[PROOF STATE]
proof (prove)
using this:
sound ?P \<Longrightarrow> sound (t ?P)
sound P

goal (1 subgoal):
 1. sound (t P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sound (t P)

goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
 2. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
[PROOF STEP]
with hb
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
sound (t P)
[PROOF STEP]
have "0 \<le> wp body (t P) s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
sound (t P)

goal (1 subgoal):
 1. 0 \<le> wp body (t P) s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> wp body (t P) s

goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
 2. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x
[PROOF STEP]
with sP
[PROOF STATE]
proof (chain)
picking this:
sound P
0 \<le> wp body (t P) s
[PROOF STEP]
show "0 \<le> \<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s"
[PROOF STATE]
proof (prove)
using this:
sound P
0 \<le> wp body (t P) s

goal (1 subgoal):
 1. 0 \<le> \<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s
[PROOF STEP]
by(auto intro!:add_nonneg_nonneg mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> \<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
from ht sP
[PROOF STATE]
proof (chain)
picking this:
sound ?P \<Longrightarrow> sound (t ?P)
sound P
[PROOF STEP]
have "sound (t P)"
[PROOF STATE]
proof (prove)
using this:
sound ?P \<Longrightarrow> sound (t ?P)
sound P

goal (1 subgoal):
 1. sound (t P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sound (t P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sound (t P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
hence "bounded_by (bound_of (t P)) (t P)"
[PROOF STATE]
proof (prove)
using this:
sound (t P)

goal (1 subgoal):
 1. bounded_by (bound_of (t P)) (t P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of (t P)) (t P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sound (t P)
bounded_by (bound_of (t P)) (t P)
[PROOF STEP]
have "wp body (t P) s \<le> bound_of (t P)"
[PROOF STATE]
proof (prove)
using this:
sound (t P)
bounded_by (bound_of (t P)) (t P)

goal (1 subgoal):
 1. wp body (t P) s \<le> bound_of (t P)
[PROOF STEP]
using hb
[PROOF STATE]
proof (prove)
using this:
sound (t P)
bounded_by (bound_of (t P)) (t P)
healthy (wp body)

goal (1 subgoal):
 1. wp body (t P) s \<le> bound_of (t P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp body (t P) s \<le> bound_of (t P)

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
hence "wp body (t P) s \<le> max (bound_of P) (bound_of (t P))"
[PROOF STATE]
proof (prove)
using this:
wp body (t P) s \<le> bound_of (t P)

goal (1 subgoal):
 1. wp body (t P) s \<le> max (bound_of P) (bound_of (t P))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp body (t P) s \<le> max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wp body (t P) s \<le> max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wp body (t P) s \<le> max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "P s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. P s \<le> bound_of P
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
P s \<le> bound_of P

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
hence "P s \<le> max (bound_of P) (bound_of (t P))"
[PROOF STATE]
proof (prove)
using this:
P s \<le> bound_of P

goal (1 subgoal):
 1. P s \<le> max (bound_of P) (bound_of (t P))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
P s \<le> max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
P s \<le> max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wp body (t P) s \<le> max (bound_of P) (bound_of (t P))
P s \<le> max (bound_of P) (bound_of (t P))
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft>G\<guillemotright> s) * P s \<le>
        \<guillemotleft>G\<guillemotright> s * max (bound_of P) (bound_of (t P)) +
        (1 - \<guillemotleft>G\<guillemotright> s) * max (bound_of P) (bound_of (t P))"
[PROOF STATE]
proof (prove)
using this:
wp body (t P) s \<le> max (bound_of P) (bound_of (t P))
P s \<le> max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * max (bound_of P) (bound_of (t P)) + (1 - \<guillemotleft> G \<guillemotright> s) * max (bound_of P) (bound_of (t P))
[PROOF STEP]
by(blast intro:add_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * max (bound_of P) (bound_of (t P)) + (1 - \<guillemotleft> G \<guillemotright> s) * max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> \<guillemotleft> G \<guillemotright> s * max (bound_of P) (bound_of (t P)) + (1 - \<guillemotleft> G \<guillemotright> s) * max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
have "... = max (bound_of P) (bound_of (t P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * max (bound_of P) (bound_of (t P)) + (1 - \<guillemotleft> G \<guillemotright> s) * max (bound_of P) (bound_of (t P)) = max (bound_of P) (bound_of (t P))
[PROOF STEP]
by(simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * max (bound_of P) (bound_of (t P)) + (1 - \<guillemotleft> G \<guillemotright> s) * max (bound_of P) (bound_of (t P)) = max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (t P) x + (1 - \<guillemotleft> G \<guillemotright> x) * P x \<le> ?b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> max (bound_of P) (bound_of (t P))
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft>G\<guillemotright> s) * P s \<le>
                max (bound_of P) (bound_of (t P))"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> max (bound_of P) (bound_of (t P))

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> max (bound_of P) (bound_of (t P))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wp body (t P) s + (1 - \<guillemotleft> G \<guillemotright> s) * P s \<le> max (bound_of P) (bound_of (t P))

goal:
No subgoals!
[PROOF STEP]
qed