[STATEMENT]
lemma (in category) compI [intro]:
  assumes f: "f \<in> Ar" and g: "g \<in> Ar" and "Cod f = Dom g"
  shows "g \<bullet> f \<in> Ar"
  and "Dom (g \<bullet> f) = Dom f"
  and "Cod (g \<bullet> f) = Cod g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<bullet> f \<in> Ar &&& Dom (g \<bullet> f) = Dom f &&& Cod (g \<bullet> f) = Cod g
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. g \<bullet> f \<in> Ar
 2. Dom (g \<bullet> f) = Dom f
 3. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
have "f \<in> Hom (Dom f) (Cod f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> Hom (Dom f) (Cod f)
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f \<in> Ar

goal (1 subgoal):
 1. f \<in> Hom (Dom f) (Cod f)
[PROOF STEP]
by (simp add: hom_def)
[PROOF STATE]
proof (state)
this:
f \<in> Hom (Dom f) (Cod f)

goal (3 subgoals):
 1. g \<bullet> f \<in> Ar
 2. Dom (g \<bullet> f) = Dom f
 3. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
with \<open>Cod f = Dom g\<close>
[PROOF STATE]
proof (chain)
picking this:
Cod f = Dom g
f \<in> Hom (Dom f) (Cod f)
[PROOF STEP]
have f_homset: "f \<in> Hom (Dom f) (Dom g)"
[PROOF STATE]
proof (prove)
using this:
Cod f = Dom g
f \<in> Hom (Dom f) (Cod f)

goal (1 subgoal):
 1. f \<in> Hom (Dom f) (Dom g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<in> Hom (Dom f) (Dom g)

goal (3 subgoals):
 1. g \<bullet> f \<in> Ar
 2. Dom (g \<bullet> f) = Dom f
 3. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
have g_homset: "g \<in> Hom (Dom g) (Cod g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> Hom (Dom g) (Cod g)
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
g \<in> Ar

goal (1 subgoal):
 1. g \<in> Hom (Dom g) (Cod g)
[PROOF STEP]
by (simp add: hom_def)
[PROOF STATE]
proof (state)
this:
g \<in> Hom (Dom g) (Cod g)

goal (3 subgoals):
 1. g \<bullet> f \<in> Ar
 2. Dom (g \<bullet> f) = Dom f
 3. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
have "(\<bullet>) : Hom (Dom g) (Cod g) \<rightarrow> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bullet>) \<in> Hom (Dom g) (Cod g) \<rightarrow> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<bullet>) \<in> Hom (Dom g) (Cod g) \<rightarrow> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)

goal (3 subgoals):
 1. g \<bullet> f \<in> Ar
 2. Dom (g \<bullet> f) = Dom f
 3. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
from this and g_homset
[PROOF STATE]
proof (chain)
picking this:
(\<bullet>) \<in> Hom (Dom g) (Cod g) \<rightarrow> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)
g \<in> Hom (Dom g) (Cod g)
[PROOF STEP]
have "(\<bullet>) g \<in> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)"
[PROOF STATE]
proof (prove)
using this:
(\<bullet>) \<in> Hom (Dom g) (Cod g) \<rightarrow> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)
g \<in> Hom (Dom g) (Cod g)

goal (1 subgoal):
 1. (\<bullet>) g \<in> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)
[PROOF STEP]
by (rule funcset_mem)
[PROOF STATE]
proof (state)
this:
(\<bullet>) g \<in> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)

goal (3 subgoals):
 1. g \<bullet> f \<in> Ar
 2. Dom (g \<bullet> f) = Dom f
 3. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
from this and f_homset
[PROOF STATE]
proof (chain)
picking this:
(\<bullet>) g \<in> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)
f \<in> Hom (Dom f) (Dom g)
[PROOF STEP]
have gf_homset: "g \<bullet> f \<in> Hom (Dom f) (Cod g)"
[PROOF STATE]
proof (prove)
using this:
(\<bullet>) g \<in> Hom (Dom f) (Dom g) \<rightarrow> Hom (Dom f) (Cod g)
f \<in> Hom (Dom f) (Dom g)

goal (1 subgoal):
 1. g \<bullet> f \<in> Hom (Dom f) (Cod g)
[PROOF STEP]
by (rule funcset_mem)
[PROOF STATE]
proof (state)
this:
g \<bullet> f \<in> Hom (Dom f) (Cod g)

goal (3 subgoals):
 1. g \<bullet> f \<in> Ar
 2. Dom (g \<bullet> f) = Dom f
 3. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
thus "g \<bullet> f \<in> Ar"
[PROOF STATE]
proof (prove)
using this:
g \<bullet> f \<in> Hom (Dom f) (Cod g)

goal (1 subgoal):
 1. g \<bullet> f \<in> Ar
[PROOF STEP]
by (simp add: hom_def)
[PROOF STATE]
proof (state)
this:
g \<bullet> f \<in> Ar

goal (2 subgoals):
 1. Dom (g \<bullet> f) = Dom f
 2. Cod (g \<bullet> f) = Cod g
[PROOF STEP]
from gf_homset
[PROOF STATE]
proof (chain)
picking this:
g \<bullet> f \<in> Hom (Dom f) (Cod g)
[PROOF STEP]
show "Dom (g \<bullet> f) = Dom f" and "Cod (g \<bullet> f) = Cod g"
[PROOF STATE]
proof (prove)
using this:
g \<bullet> f \<in> Hom (Dom f) (Cod g)

goal (1 subgoal):
 1. Dom (g \<bullet> f) = Dom f &&& Cod (g \<bullet> f) = Cod g
[PROOF STEP]
by (simp_all add: hom_def)
[PROOF STATE]
proof (state)
this:
Dom (g \<bullet> f) = Dom f
Cod (g \<bullet> f) = Cod g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma healthy_wp_Abort:
  "healthy (wp Abort)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp Abort)
[PROOF STEP]
proof(rule healthy_parts)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> bounded_by b (wp Abort P)
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> nneg (wp Abort P)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp Abort P \<tturnstile> wp Abort Q
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
fix b and P::"'a \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> bounded_by b (wp Abort P)
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> nneg (wp Abort P)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp Abort P \<tturnstile> wp Abort Q
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
assume nP: "nneg P" and bP: "bounded_by b P"
[PROOF STATE]
proof (state)
this:
nneg P
bounded_by b P

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

goal (1 subgoal):
 1. bounded_by b (wp Abort P)
[PROOF STEP]
unfolding wp_eval
[PROOF STATE]
proof (prove)
using this:
nneg P
bounded_by b P

goal (1 subgoal):
 1. bounded_by b (\<lambda>s. 0)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bounded_by b (wp Abort P)

goal (3 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> nneg (wp Abort P)
 2. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp Abort P \<tturnstile> wp Abort Q
 3. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
show "nneg (wp Abort P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (wp Abort P)
[PROOF STEP]
unfolding wp_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (\<lambda>s. 0)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
nneg (wp Abort P)

goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp Abort P \<tturnstile> wp Abort Q
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp Abort P \<tturnstile> wp Abort Q
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
fix P Q::"'a expect"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp Abort P \<tturnstile> wp Abort Q
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
show "wp Abort P \<tturnstile> wp Abort Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp Abort P \<tturnstile> wp Abort Q
[PROOF STEP]
unfolding wp_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> \<lambda>s. 0
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wp Abort P \<tturnstile> wp Abort Q

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<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 Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
fix P and c and s::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp Abort P x = wp Abort (\<lambda>x. c * P x) x
[PROOF STEP]
show "c * wp Abort P s = wp Abort (\<lambda>s. c * P s) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * wp Abort P s = wp Abort (\<lambda>s. c * P s) s
[PROOF STEP]
unfolding wp_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * 0 = 0
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
c * wp Abort P s = wp Abort (\<lambda>s. c * P s) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_Abort:
  "nearly_healthy (wlp Abort)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp Abort)
[PROOF STEP]
proof(rule nearly_healthyI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> unitary (wlp Abort P)
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp Abort P \<tturnstile> wlp Abort Q
[PROOF STEP]
fix P::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> unitary (wlp Abort P)
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp Abort P \<tturnstile> wlp Abort Q
[PROOF STEP]
show "unitary (wlp Abort P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (wlp Abort P)
[PROOF STEP]
by(simp add:wp_eval)
[PROOF STATE]
proof (state)
this:
unitary (wlp Abort P)

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

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp Abort P \<tturnstile> wlp Abort Q
[PROOF STEP]
thus "wlp Abort P \<tturnstile> wlp Abort Q"
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> Q
unitary P
unitary Q

goal (1 subgoal):
 1. wlp Abort P \<tturnstile> wlp Abort Q
[PROOF STEP]
unfolding wp_eval
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> Q
unitary P
unitary Q

goal (1 subgoal):
 1. \<lambda>s. 1 \<tturnstile> \<lambda>s. 1
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wlp Abort P \<tturnstile> wlp Abort Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma healthy_wp_Skip:
  "healthy (wp Skip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp Skip)
[PROOF STEP]
by(force intro!:healthy_parts simp:wp_eval)


[STATEMENT]
lemma nearly_healthy_wlp_Skip:
  "nearly_healthy (wlp Skip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp Skip)
[PROOF STEP]
by(auto simp:wp_eval)


[STATEMENT]
lemma healthy_wp_Seq:
  fixes t::"'s prog" and u
  assumes ht: "healthy (wp t)" and hu: "healthy (wp u)"
  shows "healthy (wp (t ;; u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (t ;; u))
[PROOF STEP]
proof(rule healthy_parts, simp_all add:wp_eval)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> bounded_by b (wp t (wp u P))
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> nneg (wp t (wp u P))
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp t (wp u P) \<tturnstile> wp t (wp u Q)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
fix b and P::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> bounded_by b (wp t (wp u P))
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> nneg (wp t (wp u P))
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp t (wp u P) \<tturnstile> wp t (wp u Q)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
assume "bounded_by b P" and "nneg P"
[PROOF STATE]
proof (state)
this:
bounded_by b P
nneg P

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

goal (1 subgoal):
 1. bounded_by b (wp u P) &&& nneg (wp u P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by b (wp u P)
nneg (wp u P)

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

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

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

goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp t (wp u P) \<tturnstile> wp t (wp u Q)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
with hu
[PROOF STATE]
proof (chain)
picking this:
healthy (wp u)
sound P
sound Q
P \<tturnstile> Q
[PROOF STEP]
have "sound (wp u P)" and "sound (wp u Q)"
    and "wp u P \<tturnstile> wp u Q"
[PROOF STATE]
proof (prove)
using this:
healthy (wp u)
sound P
sound Q
P \<tturnstile> Q

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

goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wp t (wp u P) \<tturnstile> wp t (wp u Q)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
with ht
[PROOF STATE]
proof (chain)
picking this:
healthy (wp t)
sound (wp u P)
sound (wp u Q)
wp u P \<tturnstile> wp u Q
[PROOF STEP]
show "wp t (wp u P) \<tturnstile> wp t (wp u Q)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp t)
sound (wp u P)
sound (wp u Q)
wp u P \<tturnstile> wp u Q

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

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<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 t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and c::real and s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
assume pos: "0 \<le> c" and sP: "sound P"
[PROOF STATE]
proof (state)
this:
0 \<le> c
sound P

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
with ht and hu
[PROOF STATE]
proof (chain)
picking this:
healthy (wp t)
healthy (wp u)
0 \<le> c
sound P
[PROOF STEP]
have "c * wp t (wp u P) s = wp t (\<lambda>s. c * wp u P s) s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp t)
healthy (wp u)
0 \<le> c
sound P

goal (1 subgoal):
 1. c * wp t (wp u P) s = wp t (\<lambda>s. c * wp u P s) s
[PROOF STEP]
by(auto intro!:scalingD)
[PROOF STATE]
proof (state)
this:
c * wp t (wp u P) s = wp t (\<lambda>s. c * wp u P s) s

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

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * wp t (wp u P) x = wp t (wp u (\<lambda>x. c * P x)) x
[PROOF STEP]
with hu and pos and sP
[PROOF STATE]
proof (chain)
picking this:
healthy (wp u)
0 \<le> c
sound P
c * wp t (wp u P) s = wp t (\<lambda>s. c * wp u P s) s
[PROOF STEP]
have "... = wp t (wp u (\<lambda>s. c * P s)) s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp u)
0 \<le> c
sound P
c * wp t (wp u P) s = wp t (\<lambda>s. c * wp u P s) s

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

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

goal (1 subgoal):
 1. c * wp t (wp u P) s = wp t (wp u (\<lambda>s. c * P s)) s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c * wp t (wp u P) s = wp t (wp u (\<lambda>s. c * P s)) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_Seq:
  fixes t::"'s prog" and u
  assumes ht: "nearly_healthy (wlp t)" and hu: "nearly_healthy (wlp u)"
  shows "nearly_healthy (wlp (t ;; u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (t ;; u))
[PROOF STEP]
proof(rule nearly_healthyI, simp_all add:wp_eval)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> unitary (wlp t (wlp u P))
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
fix b and P::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> unitary (wlp t (wlp u P))
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
assume "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (2 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> unitary (wlp t (wlp u P))
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
with hu
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp u)
unitary P
[PROOF STEP]
have "unitary (wlp u P)"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp u)
unitary P

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

goal (2 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> unitary (wlp t (wlp u P))
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
with ht
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp t)
unitary (wlp u P)
[PROOF STEP]
show "unitary (wlp t (wlp u P))"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp t)
unitary (wlp u P)

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

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
fix P Q::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
assume "unitary P" and "unitary Q" and "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
with hu
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp u)
unitary P
unitary Q
P \<tturnstile> Q
[PROOF STEP]
have "unitary (wlp u P)" and "unitary (wlp u Q)"
    and "wlp u P \<tturnstile> wlp u Q"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp u)
unitary P
unitary Q
P \<tturnstile> Q

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

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)
[PROOF STEP]
with ht
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp t)
unitary (wlp u P)
unitary (wlp u Q)
wlp u P \<tturnstile> wlp u Q
[PROOF STEP]
show "wlp t (wlp u P) \<tturnstile> wlp t (wlp u Q)"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp t)
unitary (wlp u P)
unitary (wlp u Q)
wlp u P \<tturnstile> wlp u Q

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma healthy_wp_PC:
  fixes f::"'s prog"
  assumes hf: "healthy (wp f)" and hg: "healthy (wp g)"
      and uP: "unitary P"
  shows "healthy (wp (f \<^bsub>P\<^esub>\<oplus> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (f \<^bsub>P\<^esub>\<oplus> g))
[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 Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> 0 \<le> P x * wp f Pa x + (1 - P x) * wp g Pa x
 3. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 4. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
fix b and Q::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> 0 \<le> P x * wp f Pa x + (1 - P x) * wp g Pa x
 3. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 4. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
assume nQ: "nneg Q" and bQ: "bounded_by b Q"
[PROOF STATE]
proof (state)
this:
nneg Q
bounded_by b Q

goal (4 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> 0 \<le> P x * wp f Pa x + (1 - P x) * wp g Pa x
 3. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 4. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
txt \<open>Non-negative:\<close>
[PROOF STATE]
proof (state)
this:
nneg Q
bounded_by b Q

goal (4 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> 0 \<le> P x * wp f Pa x + (1 - P x) * wp g Pa x
 3. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 4. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
from nQ and bQ and hf
[PROOF STATE]
proof (chain)
picking this:
nneg Q
bounded_by b Q
healthy (wp f)
[PROOF STEP]
have "0 \<le> wp f Q s"
[PROOF STATE]
proof (prove)
using this:
nneg Q
bounded_by b Q
healthy (wp f)

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

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

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

goal (4 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> 0 \<le> P x * wp f Pa x + (1 - P x) * wp g Pa x
 3. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 4. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> P s * wp f Q s

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

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

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

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

goal (1 subgoal):
 1. 0 \<le> (1 - P s) * wp g Q s
[PROOF STEP]
by (metis healthy_nnegD2 mult_nonneg_nonneg nneg_def)
[PROOF STATE]
proof (state)
this:
0 \<le> (1 - P s) * wp g Q s

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

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

goal (1 subgoal):
 1. 0 \<le> P s * wp f Q s + (1 - P s) * wp g Q s
[PROOF STEP]
by(auto intro:mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> P s * wp f Q s + (1 - P s) * wp g Q s

goal (3 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 3. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
txt \<open>Bounded:\<close>
[PROOF STATE]
proof (state)
this:
0 \<le> P s * wp f Q s + (1 - P s) * wp g Q s

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

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

goal (3 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 3. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
with uP nQ bQ hf
[PROOF STATE]
proof (chain)
picking this:
unitary P
nneg Q
bounded_by b Q
healthy (wp f)
wp f Q s \<le> b
[PROOF STEP]
have "P s * wp f Q s \<le> P s * b"
[PROOF STATE]
proof (prove)
using this:
unitary P
nneg Q
bounded_by b Q
healthy (wp f)
wp f Q s \<le> b

goal (1 subgoal):
 1. P s * wp f Q s \<le> P s * b
[PROOF STEP]
by(blast intro!:mult_mono)
[PROOF STATE]
proof (state)
this:
P s * wp f Q s \<le> P s * b

goal (3 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 3. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P s * wp f Q s \<le> P s * b

goal (3 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 3. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P s * wp f Q s \<le> P s * b

goal (3 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 3. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
from nQ bQ hg uP
[PROOF STATE]
proof (chain)
picking this:
nneg Q
bounded_by b Q
healthy (wp g)
unitary P
[PROOF STEP]
have "wp g Q s \<le> b" and "0 \<le> 1 - P s"
[PROOF STATE]
proof (prove)
using this:
nneg Q
bounded_by b Q
healthy (wp g)
unitary P

goal (1 subgoal):
 1. wp g Q s \<le> b &&& 0 \<le> 1 - P s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wp g Q s \<le> b
0 \<le> 1 - P s

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

goal (1 subgoal):
 1. (1 - P s) * wp g Q s \<le> (1 - P s) * b
[PROOF STEP]
by(blast intro!:mult_mono)
[PROOF STATE]
proof (state)
this:
(1 - P s) * wp g Q s \<le> (1 - P s) * b

goal (3 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 3. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(1 - P s) * wp g Q s \<le> (1 - P s) * b

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

goal (1 subgoal):
 1. P s * wp f Q s + (1 - P s) * wp g Q s \<le> P s * b + (1 - P s) * b
[PROOF STEP]
by(blast intro:add_mono)
[PROOF STATE]
proof (state)
this:
P s * wp f Q s + (1 - P s) * wp g Q s \<le> P s * b + (1 - P s) * b

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

goal (3 subgoals):
 1. \<And>b Pa x. \<lbrakk>bounded_by b Pa; nneg Pa\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> b
 2. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 3. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
have "... = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P s * b + (1 - P s) * b = b
[PROOF STEP]
by(auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
P s * b + (1 - P s) * b = b

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

goal (1 subgoal):
 1. P s * wp f Q s + (1 - P s) * wp g Q s \<le> b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P s * wp f Q s + (1 - P s) * wp g Q s \<le> b

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
txt \<open>Monotonic:\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
fix Q R::"'s \<Rightarrow> real" and s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
assume sQ: "sound Q" and sR: "sound R" and le: "Q \<tturnstile> R"
[PROOF STATE]
proof (state)
this:
sound Q
sound R
Q \<tturnstile> R

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
with hf
[PROOF STATE]
proof (chain)
picking this:
healthy (wp f)
sound Q
sound R
Q \<tturnstile> R
[PROOF STEP]
have "wp f Q s \<le> wp f R s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp f)
sound Q
sound R
Q \<tturnstile> R

goal (1 subgoal):
 1. wp f Q s \<le> wp f R s
[PROOF STEP]
by(blast dest:mono_transD)
[PROOF STATE]
proof (state)
this:
wp f Q s \<le> wp f R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
with uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
wp f Q s \<le> wp f R s
[PROOF STEP]
have "P s * wp f Q s \<le> P s * wp f R s"
[PROOF STATE]
proof (prove)
using this:
unitary P
wp f Q s \<le> wp f R s

goal (1 subgoal):
 1. P s * wp f Q s \<le> P s * wp f R s
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
P s * wp f Q s \<le> P s * wp f R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P s * wp f Q s \<le> P s * wp f R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P s * wp f Q s \<le> P s * wp f R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
from sQ sR le hg
[PROOF STATE]
proof (chain)
picking this:
sound Q
sound R
Q \<tturnstile> R
healthy (wp g)
[PROOF STEP]
have "wp g Q s \<le> wp g R s"
[PROOF STATE]
proof (prove)
using this:
sound Q
sound R
Q \<tturnstile> R
healthy (wp g)

goal (1 subgoal):
 1. wp g Q s \<le> wp g R s
[PROOF STEP]
by(blast dest:mono_transD)
[PROOF STATE]
proof (state)
this:
wp g Q s \<le> wp g R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wp g Q s \<le> wp g R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
from uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
[PROOF STEP]
have "0 \<le> 1 - P s"
[PROOF STATE]
proof (prove)
using this:
unitary P

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

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wp g Q s \<le> wp g R s
0 \<le> 1 - P s
[PROOF STEP]
have "(1 - P s) * wp g Q s \<le> (1 - P s) * wp g R s"
[PROOF STATE]
proof (prove)
using this:
wp g Q s \<le> wp g R s
0 \<le> 1 - P s

goal (1 subgoal):
 1. (1 - P s) * wp g Q s \<le> (1 - P s) * wp g R s
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
(1 - P s) * wp g Q s \<le> (1 - P s) * wp g R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(1 - P s) * wp g Q s \<le> (1 - P s) * wp g R s

goal (2 subgoals):
 1. \<And>Pa Q x. \<lbrakk>sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wp f Pa x + (1 - P x) * wp g Pa x \<le> P x * wp f Q x + (1 - P x) * wp g Q x
 2. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P s * wp f Q s \<le> P s * wp f R s
(1 - P s) * wp g Q s \<le> (1 - P s) * wp g R s
[PROOF STEP]
show "P s * wp f Q s + (1 - P s) * wp g Q s \<le>
                   P s * wp f R s + (1 - P s) * wp g R s"
[PROOF STATE]
proof (prove)
using this:
P s * wp f Q s \<le> P s * wp f R s
(1 - P s) * wp g Q s \<le> (1 - P s) * wp g R s

goal (1 subgoal):
 1. P s * wp f Q s + (1 - P s) * wp g Q s \<le> P s * wp f R s + (1 - P s) * wp g R s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
P s * wp f Q s + (1 - P s) * wp g Q s \<le> P s * wp f R s + (1 - P s) * wp g R s

goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
txt \<open>Scaling:\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
fix Q::"'s \<Rightarrow> real" and c::real and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
assume sQ: "sound Q" and pos: "0 \<le> c"
[PROOF STATE]
proof (state)
this:
sound Q
0 \<le> c

goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
have "c * (P s * wp f Q s + (1 - P s) * wp g Q s) =
        P s * (c * wp f Q s) + (1 - P s) * (c * wp g Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * (P s * wp f Q s + (1 - P s) * wp g Q s) = P s * (c * wp f Q s) + (1 - P s) * (c * wp g Q s)
[PROOF STEP]
by(simp add:distrib_left)
[PROOF STATE]
proof (state)
this:
c * (P s * wp f Q s + (1 - P s) * wp g Q s) = P s * (c * wp f Q s) + (1 - P s) * (c * wp g Q s)

goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c * (P s * wp f Q s + (1 - P s) * wp g Q s) = P s * (c * wp f Q s) + (1 - P s) * (c * wp g Q s)

goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
have "... = P s * wp f (\<lambda>s.  c * Q s) s +
                   (1 - P s) * wp g (\<lambda>s. c * Q s) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P s * (c * wp f Q s) + (1 - P s) * (c * wp g Q s) = P s * wp f (\<lambda>s. c * Q s) s + (1 - P s) * wp g (\<lambda>s. c * Q s) s
[PROOF STEP]
using hf hg sQ pos
[PROOF STATE]
proof (prove)
using this:
healthy (wp f)
healthy (wp g)
sound Q
0 \<le> c

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

goal (1 subgoal):
 1. \<And>Pa c x. \<lbrakk>sound Pa; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (P x * wp f Pa x + (1 - P x) * wp g Pa x) = P x * wp f (\<lambda>x. c * Pa x) x + (1 - P x) * wp g (\<lambda>x. c * Pa x) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c * (P s * wp f Q s + (1 - P s) * wp g Q s) = P s * wp f (\<lambda>s. c * Q s) s + (1 - P s) * wp g (\<lambda>s. c * Q s) s
[PROOF STEP]
show "c * (P s * wp f Q s + (1 - P s) * wp g Q s) =
                P s * wp f (\<lambda>s. c * Q s) s + (1 - P s) * wp g (\<lambda>s. c * Q s) s"
[PROOF STATE]
proof (prove)
using this:
c * (P s * wp f Q s + (1 - P s) * wp g Q s) = P s * wp f (\<lambda>s. c * Q s) s + (1 - P s) * wp g (\<lambda>s. c * Q s) s

goal (1 subgoal):
 1. c * (P s * wp f Q s + (1 - P s) * wp g Q s) = P s * wp f (\<lambda>s. c * Q s) s + (1 - P s) * wp g (\<lambda>s. c * Q s) s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c * (P s * wp f Q s + (1 - P s) * wp g Q s) = P s * wp f (\<lambda>s. c * Q s) s + (1 - P s) * wp g (\<lambda>s. c * Q s) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_PC:
  fixes f::"'s prog"
  assumes hf: "nearly_healthy (wlp f)"
      and hg: "nearly_healthy (wlp g)"
      and uP: "unitary P"
  shows "nearly_healthy (wlp (f \<^bsub>P\<^esub>\<oplus> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (f \<^bsub>P\<^esub>\<oplus> g))
[PROOF STEP]
proof(intro nearly_healthyI unitaryI2 nnegI bounded_byI le_funI,
      simp_all add:wp_eval)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> 0 \<le> P x * wlp f Pa x + (1 - P x) * wlp g Pa x
 2. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 3. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
fix Q::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> 0 \<le> P x * wlp f Pa x + (1 - P x) * wlp g Pa x
 2. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 3. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
assume uQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (3 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> 0 \<le> P x * wlp f Pa x + (1 - P x) * wlp g Pa x
 2. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 3. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
from uQ hf hg
[PROOF STATE]
proof (chain)
picking this:
unitary Q
nearly_healthy (wlp f)
nearly_healthy (wlp g)
[PROOF STEP]
have utQ: "unitary (wlp f Q)" "unitary (wlp g Q)"
[PROOF STATE]
proof (prove)
using this:
unitary Q
nearly_healthy (wlp f)
nearly_healthy (wlp g)

goal (1 subgoal):
 1. unitary (wlp f Q) &&& unitary (wlp g Q)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (wlp f Q)
unitary (wlp g Q)

goal (3 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> 0 \<le> P x * wlp f Pa x + (1 - P x) * wlp g Pa x
 2. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 3. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
from uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
[PROOF STEP]
have nnP: "0 \<le> P s" "0 \<le> 1 - P s"
[PROOF STATE]
proof (prove)
using this:
unitary P

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

goal (3 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> 0 \<le> P x * wlp f Pa x + (1 - P x) * wlp g Pa x
 2. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 3. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> P s
0 \<le> 1 - P s

goal (3 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> 0 \<le> P x * wlp f Pa x + (1 - P x) * wlp g Pa x
 2. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 3. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
from utQ
[PROOF STATE]
proof (chain)
picking this:
unitary (wlp f Q)
unitary (wlp g Q)
[PROOF STEP]
have "0 \<le> wlp f Q s" "0 \<le> wlp g Q s"
[PROOF STATE]
proof (prove)
using this:
unitary (wlp f Q)
unitary (wlp g Q)

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

goal (3 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> 0 \<le> P x * wlp f Pa x + (1 - P x) * wlp g Pa x
 2. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 3. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> P s
0 \<le> 1 - P s
0 \<le> wlp f Q s
0 \<le> wlp g Q s
[PROOF STEP]
show "0 \<le> P s * wlp f Q s + (1 - P s) * wlp g Q s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P s
0 \<le> 1 - P s
0 \<le> wlp f Q s
0 \<le> wlp g Q s

goal (1 subgoal):
 1. 0 \<le> P s * wlp f Q s + (1 - P s) * wlp g Q s
[PROOF STEP]
by(auto intro:add_nonneg_nonneg mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> P s * wlp f Q s + (1 - P s) * wlp g Q s

goal (2 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 2. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
from utQ
[PROOF STATE]
proof (chain)
picking this:
unitary (wlp f Q)
unitary (wlp g Q)
[PROOF STEP]
have "wlp f Q s \<le> 1" "wlp g Q s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary (wlp f Q)
unitary (wlp g Q)

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

goal (2 subgoals):
 1. \<And>Pa x. unitary Pa \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> 1
 2. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
with nnP
[PROOF STATE]
proof (chain)
picking this:
0 \<le> P s
0 \<le> 1 - P s
wlp f Q s \<le> 1
wlp g Q s \<le> 1
[PROOF STEP]
have "P s * wlp f Q s + (1 - P s) * wlp g Q s \<le> P s * 1 + (1 - P s) * 1"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P s
0 \<le> 1 - P s
wlp f Q s \<le> 1
wlp g Q s \<le> 1

goal (1 subgoal):
 1. P s * wlp f Q s + (1 - P s) * wlp g Q s \<le> P s * 1 + (1 - P s) * 1
[PROOF STEP]
by(blast intro:add_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
P s * wlp f Q s + (1 - P s) * wlp g Q s \<le> P s * 1 + (1 - P s) * 1

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

goal (1 subgoal):
 1. P s * wlp f Q s + (1 - P s) * wlp g Q s \<le> 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
P s * wlp f Q s + (1 - P s) * wlp g Q s \<le> 1

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

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
with uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
unitary R
Q \<tturnstile> R
[PROOF STEP]
have "wlp f Q s \<le> wlp f R s"
[PROOF STATE]
proof (prove)
using this:
unitary Q
unitary R
Q \<tturnstile> R

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

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
with nnP
[PROOF STATE]
proof (chain)
picking this:
0 \<le> P s
0 \<le> 1 - P s
wlp f Q s \<le> wlp f R s
[PROOF STEP]
have "P s * wlp f Q s \<le> P s * wlp f R s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P s
0 \<le> 1 - P s
wlp f Q s \<le> wlp f R s

goal (1 subgoal):
 1. P s * wlp f Q s \<le> P s * wlp f R s
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
P s * wlp f Q s \<le> P s * wlp f R s

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P s * wlp f Q s \<le> P s * wlp f R s

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P s * wlp f Q s \<le> P s * wlp f R s

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
from uQ uR le
[PROOF STATE]
proof (chain)
picking this:
unitary Q
unitary R
Q \<tturnstile> R
[PROOF STEP]
have "wlp g Q s \<le> wlp g R s"
[PROOF STATE]
proof (prove)
using this:
unitary Q
unitary R
Q \<tturnstile> R

goal (1 subgoal):
 1. wlp g Q s \<le> wlp g R s
[PROOF STEP]
by(auto intro:le_funD[OF nearly_healthy_monoD, OF hg])
[PROOF STATE]
proof (state)
this:
wlp g Q s \<le> wlp g R s

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
with nnP
[PROOF STATE]
proof (chain)
picking this:
0 \<le> P s
0 \<le> 1 - P s
wlp g Q s \<le> wlp g R s
[PROOF STEP]
have "(1 - P s) * wlp g Q s \<le> (1 - P s) * wlp g R s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P s
0 \<le> 1 - P s
wlp g Q s \<le> wlp g R s

goal (1 subgoal):
 1. (1 - P s) * wlp g Q s \<le> (1 - P s) * wlp g R s
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
(1 - P s) * wlp g Q s \<le> (1 - P s) * wlp g R s

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(1 - P s) * wlp g Q s \<le> (1 - P s) * wlp g R s

goal (1 subgoal):
 1. \<And>Pa Q x. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> P x * wlp f Pa x + (1 - P x) * wlp g Pa x \<le> P x * wlp f Q x + (1 - P x) * wlp g Q x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P s * wlp f Q s \<le> P s * wlp f R s
(1 - P s) * wlp g Q s \<le> (1 - P s) * wlp g R s
[PROOF STEP]
show "P s * wlp f Q s + (1 - P s) * wlp g Q s \<le>
                   P s * wlp f R s + (1 - P s) * wlp g R s"
[PROOF STATE]
proof (prove)
using this:
P s * wlp f Q s \<le> P s * wlp f R s
(1 - P s) * wlp g Q s \<le> (1 - P s) * wlp g R s

goal (1 subgoal):
 1. P s * wlp f Q s + (1 - P s) * wlp g Q s \<le> P s * wlp f R s + (1 - P s) * wlp g R s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
P s * wlp f Q s + (1 - P s) * wlp g Q s \<le> P s * wlp f R s + (1 - P s) * wlp g R s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma healthy_wp_DC:
  fixes f::"'s prog"
  assumes hf: "healthy (wp f)" and hg: "healthy (wp g)"
  shows "healthy (wp (f \<Sqinter> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (f \<Sqinter> g))
[PROOF STEP]
proof(intro healthy_parts bounded_byI nnegI 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> min (wp f P x) (wp g P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> min (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wp f P x) (wp g P x) \<le> min (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<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> min (wp f P x) (wp g P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> min (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wp f P x) (wp g P x) \<le> min (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
assume nP: "nneg P" and bP: "bounded_by b P"
[PROOF STATE]
proof (state)
this:
nneg P
bounded_by b P

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wp f P x) (wp g P x) \<le> min (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<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> min (wp f P x) (wp g P x) \<le> min (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and Q 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> min (wp f P x) (wp g P x) \<le> min (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
healthy (wp f)
healthy (wp g)
[PROOF STEP]
have mf: "mono_trans (wp f)" and mg: "mono_trans (wp g)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp f)
healthy (wp g)

goal (1 subgoal):
 1. mono_trans (wp f) &&& mono_trans (wp g)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
mono_trans (wp f)
mono_trans (wp g)

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wp f P x) (wp g P x) \<le> min (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
assume sP: "sound P" and sQ: "sound Q" and le: "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> min (wp f P x) (wp g P x) \<le> min (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
hence "wp f P s \<le> wp f Q s" and "wp g P s \<le> wp g Q s"
[PROOF STATE]
proof (prove)
using this:
sound P
sound Q
P \<tturnstile> Q

goal (1 subgoal):
 1. wp f P s \<le> wp f Q s &&& wp g P s \<le> wp g Q s
[PROOF STEP]
by(auto intro:le_funD[OF mono_transD[OF mf]] le_funD[OF mono_transD[OF mg]])
[PROOF STATE]
proof (state)
this:
wp f P s \<le> wp f Q s
wp g P s \<le> wp g Q s

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

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

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<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 * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<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 * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
assume sP: "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 * min (wp f P x) (wp g P x) = min (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
healthy (wp f)
healthy (wp g)
[PROOF STEP]
have sf: "scaling (wp f)" and sg: "scaling (wp g)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp f)
healthy (wp g)

goal (1 subgoal):
 1. scaling (wp f) &&& scaling (wp g)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
scaling (wp f)
scaling (wp g)

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

goal (1 subgoal):
 1. c * min (wp f P s) (wp g P s) = min (c * wp f P s) (c * wp g P s)
[PROOF STEP]
by(simp add:min_distrib)
[PROOF STATE]
proof (state)
this:
c * min (wp f P s) (wp g P s) = min (c * wp f P s) (c * wp g P s)

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

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

goal (1 subgoal):
 1. min (c * wp f P s) (c * wp g P s) = min (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)
[PROOF STEP]
by(simp add:scalingD[OF sf] scalingD[OF sg])
[PROOF STATE]
proof (state)
this:
min (c * wp f P s) (c * wp g P s) = min (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)

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

goal (1 subgoal):
 1. c * min (wp f P s) (wp g P s) = min (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c * min (wp f P s) (wp g P s) = min (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_DC:
  fixes f::"'s prog"
  assumes hf: "nearly_healthy (wlp f)"
      and hg: "nearly_healthy (wlp g)"
  shows "nearly_healthy (wlp (f \<Sqinter> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (f \<Sqinter> g))
[PROOF STEP]
proof(intro nearly_healthyI bounded_byI nnegI le_funI unitaryI2,
      simp_all add:wp_eval, safe)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp f P x
 2. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp g P x
 3. \<And>P x. unitary P \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> 1
 4. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 5. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp f P x
 2. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp g P x
 3. \<And>P x. unitary P \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> 1
 4. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 5. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
assume uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (5 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp f P x
 2. \<And>P x. unitary P \<Longrightarrow> 0 \<le> wlp g P x
 3. \<And>P x. unitary P \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> 1
 4. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 5. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
with hf hg
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp f)
nearly_healthy (wlp g)
unitary P
[PROOF STEP]
have utP: "unitary (wlp f P)" "unitary (wlp g P)"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp f)
nearly_healthy (wlp g)
unitary P

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

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

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

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> 1
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
have "min (wlp f P s) (wlp g P s) \<le> wlp f P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (wlp f P s) (wlp g P s) \<le> wlp f P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp f P s

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> 1
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp f P s

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> 1
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
from utP
[PROOF STATE]
proof (chain)
picking this:
unitary (wlp f P)
unitary (wlp g P)
[PROOF STEP]
have "... \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary (wlp f P)
unitary (wlp g P)

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

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

goal (1 subgoal):
 1. min (wlp f P s) (wlp g P s) \<le> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> 1

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
fix Q::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
assume uQ: "unitary Q" and le: "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
unitary Q
P \<tturnstile> Q

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
have "min (wlp f P s) (wlp g P s) \<le> wlp f P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (wlp f P s) (wlp g P s) \<le> wlp f P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp f P s

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp f P s

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp f Q x
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
from uP uQ le
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
P \<tturnstile> Q
[PROOF STEP]
have "... \<le> wlp f Q s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
P \<tturnstile> Q

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

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

goal (1 subgoal):
 1. min (wlp f P s) (wlp g P s) \<le> wlp f Q s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp f Q s

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
have "min (wlp f P s) (wlp g P s) \<le> wlp g P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (wlp f P s) (wlp g P s) \<le> wlp g P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp g P s

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> min (wlp f P x) (wlp g P x) \<le> wlp g Q x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp g P s

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

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

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

goal (1 subgoal):
 1. min (wlp f P s) (wlp g P s) \<le> wlp g Q s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
min (wlp f P s) (wlp g P s) \<le> wlp g Q s

goal:
No subgoals!
[PROOF STEP]
qed