[STATEMENT]
lemma healthy_wp_AC:
  fixes f::"'s prog"
  assumes hf: "healthy (wp f)" and hg: "healthy (wp g)"
  shows "healthy (wp (f \<Squnion> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (f \<Squnion> 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> max (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> max (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (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> max (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (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> max (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (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> max (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (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> max (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
moreover
[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> max (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> max (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
{
[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> max (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> max (wp f P x) (wp g P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
from bP nP hg
[PROOF STATE]
proof (chain)
picking this:
bounded_by b P
nneg P
healthy (wp g)
[PROOF STEP]
have "bounded_by b (wp g P)"
[PROOF STATE]
proof (prove)
using this:
bounded_by b P
nneg P
healthy (wp g)

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

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

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

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

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

goal (1 subgoal):
 1. max (wp f P s) (wp g P s) \<le> b
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
max (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> max (wp f P x) (wp g P x)
 2. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 3. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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]
have "0 \<le> wp f 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> wp f P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> wp f P s

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

goal (1 subgoal):
 1. 0 \<le> max (wp f P s) (wp g P s)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> max (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> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (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> max (wp f P x) (wp g P x) \<le> max (wp f Q x) (wp g Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * max (wp f P x) (wp g P x) = max (wp f (\<lambda>x. c * P x) x) (wp g (\<lambda>x. c * P x) x)
[PROOF STEP]
thus "max (wp f P s) (wp g P s) \<le> max (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. max (wp f P s) (wp g P s) \<le> max (wp f Q s) (wp g Q s)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
max (wp f P s) (wp g P s) \<le> max (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 * max (wp f P x) (wp g P x) = max (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 * max (wp f P x) (wp g P x) = max (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 * max (wp f P x) (wp g P x) = max (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 * max (wp f P x) (wp g P x) = max (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 * max (wp f P x) (wp g P x) = max (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 * max (wp f P s) (wp g P s) =
                 max (c * wp f P s) (c * wp g P s)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c

goal (1 subgoal):
 1. c * max (wp f P s) (wp g P s) = max (c * wp f P s) (c * wp g P s)
[PROOF STEP]
by(simp add:max_distrib)
[PROOF STATE]
proof (state)
this:
c * max (wp f P s) (wp g P s) = max (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 * max (wp f P x) (wp g P x) = max (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 * max (wp f P s) (wp g P s) = max (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 * max (wp f P x) (wp g P x) = max (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 "... = max (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. max (c * wp f P s) (c * wp g P s) = max (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:
max (c * wp f P s) (c * wp g P s) = max (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 * max (wp f P x) (wp g P x) = max (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 * max (wp f P s) (wp g P s) = max (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)
[PROOF STEP]
show "c * max (wp f P s) (wp g P s) =
                max (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)"
[PROOF STATE]
proof (prove)
using this:
c * max (wp f P s) (wp g P s) = max (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)

goal (1 subgoal):
 1. c * max (wp f P s) (wp g P s) = max (wp f (\<lambda>s. c * P s) s) (wp g (\<lambda>s. c * P s) s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c * max (wp f P s) (wp g P s) = max (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_AC:
  fixes f::"'s prog"
  assumes hf: "nearly_healthy (wlp f)"
      and hg: "nearly_healthy (wlp g)"
  shows "nearly_healthy (wlp (f \<Squnion> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (f \<Squnion> g))
[PROOF STEP]
proof(intro nearly_healthyI bounded_byI nnegI unitaryI2 le_funI, simp_all only:wp_eval)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> max (wlp f P x) (wlp g P x)
 2. \<And>P x. unitary P \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> max (wlp f Q x) (wlp g Q x)
[PROOF STEP]
fix b and P::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> max (wlp f P x) (wlp g P x)
 2. \<And>P x. unitary P \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> max (wlp f Q x) (wlp g Q x)
[PROOF STEP]
assume uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> max (wlp f P x) (wlp g P x)
 2. \<And>P x. unitary P \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> max (wlp f Q x) (wlp g Q x)
[PROOF STEP]
with hf
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp f)
unitary P
[PROOF STEP]
have "wlp f P s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp f)
unitary 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> 0 \<le> max (wlp f P x) (wlp g P x)
 2. \<And>P x. unitary P \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> max (wlp f Q x) (wlp g Q x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wlp f P s \<le> 1

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> max (wlp f P x) (wlp g P x) \<le> max (wlp f Q x) (wlp g Q x)
[PROOF STEP]
hence "wlp f P s \<le> wlp f Q s" and "wlp g P s \<le> wlp g 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 &&& wlp g P s \<le> wlp g Q s
[PROOF STEP]
by(auto intro:le_funD[OF nearly_healthy_monoD, OF hf]
                  le_funD[OF nearly_healthy_monoD, OF hg])
[PROOF STATE]
proof (state)
this:
wlp f P s \<le> wlp f Q s
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> max (wlp f P x) (wlp g P x) \<le> max (wlp f Q x) (wlp g Q x)
[PROOF STEP]
thus "max (wlp f P s) (wlp g P s) \<le> max (wlp f Q s) (wlp g Q s)"
[PROOF STATE]
proof (prove)
using this:
wlp f P s \<le> wlp f Q s
wlp g P s \<le> wlp g Q s

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma healthy_wp_Embed:
  "healthy t \<Longrightarrow> healthy (wp (Embed t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy t \<Longrightarrow> healthy (wp (Embed t))
[PROOF STEP]
unfolding wp_def Embed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy t \<Longrightarrow> healthy t
[PROOF STEP]
by(simp)


[STATEMENT]
lemma nearly_healthy_wlp_Embed:
  "nearly_healthy t \<Longrightarrow> nearly_healthy (wlp (Embed t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy t \<Longrightarrow> nearly_healthy (wlp (Embed t))
[PROOF STEP]
unfolding wlp_def Embed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy t \<Longrightarrow> nearly_healthy t
[PROOF STEP]
by(simp)


[STATEMENT]
lemma healthy_wp_repeat:
  assumes h_a: "healthy (wp a)"
  shows "healthy (wp (repeat n a))" (is "?X n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (repeat n a))
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. healthy (wp (repeat 0 a))
 2. \<And>n. healthy (wp (repeat n a)) \<Longrightarrow> healthy (wp (repeat (Suc n) a))
[PROOF STEP]
show "?X 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (repeat 0 a))
[PROOF STEP]
by(auto simp:wp_eval)
[PROOF STATE]
proof (state)
this:
healthy (wp (repeat 0 a))

goal (1 subgoal):
 1. \<And>n. healthy (wp (repeat n a)) \<Longrightarrow> healthy (wp (repeat (Suc n) a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. healthy (wp (repeat n a)) \<Longrightarrow> healthy (wp (repeat (Suc n) a))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. healthy (wp (repeat n a)) \<Longrightarrow> healthy (wp (repeat (Suc n) a))
[PROOF STEP]
assume IH: "?X n"
[PROOF STATE]
proof (state)
this:
healthy (wp (repeat n a))

goal (1 subgoal):
 1. \<And>n. healthy (wp (repeat n a)) \<Longrightarrow> healthy (wp (repeat (Suc n) a))
[PROOF STEP]
thus "?X (Suc n)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp (repeat n a))

goal (1 subgoal):
 1. healthy (wp (repeat (Suc n) a))
[PROOF STEP]
by(simp add:healthy_wp_Seq h_a)
[PROOF STATE]
proof (state)
this:
healthy (wp (repeat (Suc n) a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_repeat:
  assumes h_a: "nearly_healthy (wlp a)"
  shows "nearly_healthy (wlp (repeat n a))" (is "?X n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (repeat n a))
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nearly_healthy (wlp (repeat 0 a))
 2. \<And>n. nearly_healthy (wlp (repeat n a)) \<Longrightarrow> nearly_healthy (wlp (repeat (Suc n) a))
[PROOF STEP]
show "?X 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (repeat 0 a))
[PROOF STEP]
by(simp add:wp_eval)
[PROOF STATE]
proof (state)
this:
nearly_healthy (wlp (repeat 0 a))

goal (1 subgoal):
 1. \<And>n. nearly_healthy (wlp (repeat n a)) \<Longrightarrow> nearly_healthy (wlp (repeat (Suc n) a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. nearly_healthy (wlp (repeat n a)) \<Longrightarrow> nearly_healthy (wlp (repeat (Suc n) a))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. nearly_healthy (wlp (repeat n a)) \<Longrightarrow> nearly_healthy (wlp (repeat (Suc n) a))
[PROOF STEP]
assume IH: "?X n"
[PROOF STATE]
proof (state)
this:
nearly_healthy (wlp (repeat n a))

goal (1 subgoal):
 1. \<And>n. nearly_healthy (wlp (repeat n a)) \<Longrightarrow> nearly_healthy (wlp (repeat (Suc n) a))
[PROOF STEP]
thus "?X (Suc n)"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp (repeat n a))

goal (1 subgoal):
 1. nearly_healthy (wlp (repeat (Suc n) a))
[PROOF STEP]
by(simp add:nearly_healthy_wlp_Seq h_a)
[PROOF STATE]
proof (state)
this:
nearly_healthy (wlp (repeat (Suc n) a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma healthy_wp_SetDC:
  fixes prog::"'b \<Rightarrow> 'a prog" and S::"'a \<Rightarrow> 'b set"
  assumes healthy:  "\<And>x s. x \<in> S s \<Longrightarrow> healthy (wp (prog x))"
      and nonempty: "\<And>s. \<exists>x. x \<in> S s"
  shows "healthy (wp (SetDC prog S))" (is "healthy ?T")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (SetDC prog S))
[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> (INF a\<in>S x. wp (prog a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (INF a\<in>S x. wp (prog a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
fix b and P::"'a \<Rightarrow> real" and s::'a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (INF a\<in>S x. wp (prog a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
assume bP: "bounded_by b P" and nP: "nneg P"
[PROOF STATE]
proof (state)
this:
bounded_by b P
nneg P

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

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

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (INF a\<in>S x. wp (prog a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
obtain x where xin: "x \<in> (\<lambda>a. wp (prog a) P s) ` S s"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. (\<And>x. x \<in> (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s

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

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

goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x

goal (4 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> b
 2. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (INF a\<in>S x. wp (prog a) P x)
 3. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s
\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x
[PROOF STEP]
have "Inf ((\<lambda>a. wp (prog a) P s) ` S s) \<le> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s
\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x

goal (1 subgoal):
 1. (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
by(intro cInf_lower bdd_belowI, auto)
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. wp (prog a) P s) \<le> x

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

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

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

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

goal (1 subgoal):
 1. (INF a\<in>S s. wp (prog a) P s) \<le> b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. wp (prog a) P s) \<le> b

goal (3 subgoals):
 1. \<And>b P x. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> (INF a\<in>S x. wp (prog a) P x)
 2. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 3. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from xin and sP and healthy
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s
sound P
?x \<in> S ?s \<Longrightarrow> healthy (wp (prog ?x))
[PROOF STEP]
show "0 \<le> Inf ((\<lambda>a. wp (prog a) P s) ` S s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s
sound P
?x \<in> S ?s \<Longrightarrow> healthy (wp (prog ?x))

goal (1 subgoal):
 1. 0 \<le> (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
by(blast intro:cInf_greatest)
[PROOF STATE]
proof (state)
this:
0 \<le> (INF a\<in>S s. wp (prog a) P s)

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
fix P::"'a \<Rightarrow> real" and Q and s::'a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<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> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
obtain x where xin: "x \<in> (\<lambda>a. wp (prog a) P s) ` S s"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. (\<And>x. x \<in> (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from sP and healthy
[PROOF STATE]
proof (chain)
picking this:
sound P
?x \<in> S ?s \<Longrightarrow> healthy (wp (prog ?x))
[PROOF STEP]
have "\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x"
[PROOF STATE]
proof (prove)
using this:
sound P
?x \<in> S ?s \<Longrightarrow> healthy (wp (prog ?x))

goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
have "\<forall>x\<in>(\<lambda>a. wp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wp (prog a) P s) ` S s. y \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wp (prog a) P s) ` S s. y \<le> x
[PROOF STEP]
proof(rule ballI, clarify, rule bexI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<le> wp (prog a) Q s
 2. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<in> (\<lambda>a. wp (prog a) P s) ` S s
[PROOF STEP]
fix x and a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<le> wp (prog a) Q s
 2. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<in> (\<lambda>a. wp (prog a) P s) ` S s
[PROOF STEP]
assume ain: "a \<in> S s"
[PROOF STATE]
proof (state)
this:
a \<in> S s

goal (2 subgoals):
 1. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<le> wp (prog a) Q s
 2. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<in> (\<lambda>a. wp (prog a) P s) ` S s
[PROOF STEP]
with healthy and sP and sQ and le
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S ?s \<Longrightarrow> healthy (wp (prog ?x))
sound P
sound Q
P \<tturnstile> Q
a \<in> S s
[PROOF STEP]
show "wp (prog a) P s \<le> wp (prog a) Q s"
[PROOF STATE]
proof (prove)
using this:
?x \<in> S ?s \<Longrightarrow> healthy (wp (prog ?x))
sound P
sound Q
P \<tturnstile> Q
a \<in> S s

goal (1 subgoal):
 1. wp (prog a) P s \<le> wp (prog a) Q s
[PROOF STEP]
by(auto dest:mono_transD[OF healthy_monoD])
[PROOF STATE]
proof (state)
this:
wp (prog a) P s \<le> wp (prog a) Q s

goal (1 subgoal):
 1. \<And>x a. a \<in> S s \<Longrightarrow> wp (prog a) P s \<in> (\<lambda>a. wp (prog a) P s) ` S s
[PROOF STEP]
from ain
[PROOF STATE]
proof (chain)
picking this:
a \<in> S s
[PROOF STEP]
show "wp (prog a) P s \<in> (\<lambda>a. wp (prog a) P s) ` S s"
[PROOF STATE]
proof (prove)
using this:
a \<in> S s

goal (1 subgoal):
 1. wp (prog a) P s \<in> (\<lambda>a. wp (prog a) P s) ` S s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp (prog a) P s \<in> (\<lambda>a. wp (prog a) P s) ` S s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wp (prog a) P s) ` S s. y \<le> x

goal (2 subgoals):
 1. \<And>P Q x. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wp (prog a) P x) \<le> (INF a\<in>S x. wp (prog a) Q x)
 2. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s
\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x
\<forall>x\<in>(\<lambda>a. wp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wp (prog a) P s) ` S s. y \<le> x
[PROOF STEP]
show "Inf ((\<lambda>a. wp (prog a) P s) ` S s) \<le> Inf ((\<lambda>a. wp (prog a) Q s) ` S s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s
\<forall>x\<in>(\<lambda>a. wp (prog a) P s) ` S s. 0 \<le> x
\<forall>x\<in>(\<lambda>a. wp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wp (prog a) P s) ` S s. y \<le> x

goal (1 subgoal):
 1. (INF a\<in>S s. wp (prog a) P s) \<le> (INF a\<in>S s. wp (prog a) Q s)
[PROOF STEP]
by(intro cInf_mono, blast+)
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. wp (prog a) P s) \<le> (INF a\<in>S s. wp (prog a) Q s)

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
fix P::"'a \<Rightarrow> real" and c::real and s::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<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 * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
obtain x where xin: "x \<in> (\<lambda>a. wp (prog a) P s) ` S s"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. (\<And>x. x \<in> (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wp (prog a) P s) ` S s

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
have "c * Inf ((\<lambda>a. wp (prog a) P s) ` S s) =
        Inf ((*) c ` ((\<lambda>a. wp (prog a) P s) ` S s))" (is "?U = ?V")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * (INF a\<in>S s. wp (prog a) P s) = Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c * (INF a\<in>S s. wp (prog a) P s) \<le> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)
 2. Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
show "?U \<le> ?V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * (INF a\<in>S s. wp (prog a) P s) \<le> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)
[PROOF STEP]
proof(rule cInf_greatest)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<noteq> {}
 2. \<And>x. x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> c * (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
show "(*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<noteq> {}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<noteq> {}

goal (1 subgoal):
 1. \<And>x. x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> c * (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> c * (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
assume "x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s"
[PROOF STATE]
proof (state)
this:
x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s

goal (1 subgoal):
 1. \<And>x. x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> c * (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s
[PROOF STEP]
obtain y where yin: "y \<in> (\<lambda>a. wp (prog a) P s) ` S s" and rwx: "x = c * y"
[PROOF STATE]
proof (prove)
using this:
x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> (\<lambda>a. wp (prog a) P s) ` S s; x = c * y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
y \<in> (\<lambda>a. wp (prog a) P s) ` S s
x = c * y

goal (1 subgoal):
 1. \<And>x. x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> c * (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
have "Inf ((\<lambda>a. wp (prog a) P s) ` S s) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (INF a\<in>S s. wp (prog a) P s) \<le> y
[PROOF STEP]
proof(intro cInf_lower[OF yin] bdd_belowI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> ?m1 \<le> x
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> ?m1 \<le> x
[PROOF STEP]
assume zin: "z \<in> (\<lambda>a. wp (prog a) P s) ` S s"
[PROOF STATE]
proof (state)
this:
z \<in> (\<lambda>a. wp (prog a) P s) ` S s

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> ?m1 \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> (\<lambda>a. wp (prog a) P s) ` S s
[PROOF STEP]
obtain a where "a \<in> S s" and "z = wp (prog a) P s"
[PROOF STATE]
proof (prove)
using this:
z \<in> (\<lambda>a. wp (prog a) P s) ` S s

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> S s; z = wp (prog a) P s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
a \<in> S s
z = wp (prog a) P s

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> ?m1 \<le> x
[PROOF STEP]
with sP
[PROOF STATE]
proof (chain)
picking this:
sound P
a \<in> S s
z = wp (prog a) P s
[PROOF STEP]
show "0 \<le> z"
[PROOF STATE]
proof (prove)
using this:
sound P
a \<in> S s
z = wp (prog a) P s

goal (1 subgoal):
 1. 0 \<le> z
[PROOF STEP]
by(auto dest:healthy)
[PROOF STATE]
proof (state)
this:
0 \<le> z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. wp (prog a) P s) \<le> y

goal (1 subgoal):
 1. \<And>x. x \<in> (*) c ` (\<lambda>a. wp (prog a) P s) ` S s \<Longrightarrow> c * (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
with pos rwx
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
x = c * y
(INF a\<in>S s. wp (prog a) P s) \<le> y
[PROOF STEP]
show "c * Inf ((\<lambda>a. wp (prog a) P s) ` S s) \<le> x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
x = c * y
(INF a\<in>S s. wp (prog a) P s) \<le> y

goal (1 subgoal):
 1. c * (INF a\<in>S s. wp (prog a) P s) \<le> x
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
c * (INF a\<in>S s. wp (prog a) P s) \<le> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c * (INF a\<in>S s. wp (prog a) P s) \<le> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)

goal (1 subgoal):
 1. Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
show "?V \<le> ?U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
 2. \<not> ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
assume cz: "c = 0"
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
 2. \<not> ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
 2. \<not> ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
 2. \<not> ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
obtain c where "c \<in> S s"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. (\<And>c. c \<in> S s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
c \<in> S s

goal (2 subgoals):
 1. ?P \<Longrightarrow> Inf ((*) c__ ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c__ * (INF a\<in>S s. wp (prog a) P s)
 2. \<not> ?P \<Longrightarrow> Inf ((*) c__ ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c__ * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
hence "\<exists>x. \<exists>xa\<in>S s. x = wp (prog xa) P s"
[PROOF STATE]
proof (prove)
using this:
c \<in> S s

goal (1 subgoal):
 1. \<exists>x. \<exists>xa\<in>S s. x = wp (prog xa) P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<exists>x. \<exists>xa\<in>S s. x = wp (prog xa) P s

goal (2 subgoals):
 1. ?P \<Longrightarrow> Inf ((*) c__ ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c__ * (INF a\<in>S s. wp (prog a) P s)
 2. \<not> ?P \<Longrightarrow> Inf ((*) c__ ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c__ * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>x. \<exists>xa\<in>S s. x = wp (prog xa) P s

goal (2 subgoals):
 1. ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
 2. \<not> ?P \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = 0
\<exists>x. \<exists>xa\<in>S s. x = wp (prog xa) P s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0
\<exists>x. \<exists>xa\<in>S s. x = wp (prog xa) P s

goal (1 subgoal):
 1. Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
by(simp add:image_def)
[PROOF STATE]
proof (state)
this:
Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
assume "c \<noteq> 0"
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
have "S s \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. S s \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S s \<noteq> {}

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S s \<noteq> {}
[PROOF STEP]
have "inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> (INF a\<in>S s. wp (prog a) P s)"
[PROOF STATE]
proof (prove)
using this:
S s \<noteq> {}

goal (1 subgoal):
 1. inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
proof (rule cINF_greatest)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S s \<Longrightarrow> inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S s \<Longrightarrow> inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s
[PROOF STEP]
assume "x \<in> S s"
[PROOF STATE]
proof (state)
this:
x \<in> S s

goal (1 subgoal):
 1. \<And>x. x \<in> S s \<Longrightarrow> inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s
[PROOF STEP]
have "bdd_below ((\<lambda>x. c * wp (prog x) P s) ` S s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_below ((\<lambda>x. c * wp (prog x) P s) ` S s)
[PROOF STEP]
proof (rule bdd_belowI [of _ 0])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. c * wp (prog x) P s) ` S s \<Longrightarrow> 0 \<le> x
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. c * wp (prog x) P s) ` S s \<Longrightarrow> 0 \<le> x
[PROOF STEP]
assume "z \<in> (\<lambda>x. c * wp (prog x) P s) ` S s"
[PROOF STATE]
proof (state)
this:
z \<in> (\<lambda>x. c * wp (prog x) P s) ` S s

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. c * wp (prog x) P s) ` S s \<Longrightarrow> 0 \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> (\<lambda>x. c * wp (prog x) P s) ` S s
[PROOF STEP]
obtain b where "b \<in> S s" and rwz: "z = c * wp (prog b) P s"
[PROOF STATE]
proof (prove)
using this:
z \<in> (\<lambda>x. c * wp (prog x) P s) ` S s

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>b \<in> S s; z = c * wp (prog b) P s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> S s
z = c * wp (prog b) P s

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. c * wp (prog x) P s) ` S s \<Longrightarrow> 0 \<le> x
[PROOF STEP]
with sP
[PROOF STATE]
proof (chain)
picking this:
sound P
b \<in> S s
z = c * wp (prog b) P s
[PROOF STEP]
have "0 \<le> wp (prog b) P s"
[PROOF STATE]
proof (prove)
using this:
sound P
b \<in> S s
z = c * wp (prog b) P s

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

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. c * wp (prog x) P s) ` S s \<Longrightarrow> 0 \<le> x
[PROOF STEP]
with pos
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
0 \<le> wp (prog b) P s
[PROOF STEP]
show "0 \<le> z"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
0 \<le> wp (prog b) P s

goal (1 subgoal):
 1. 0 \<le> z
[PROOF STEP]
by (auto simp: rwz intro: mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bdd_below ((\<lambda>x. c * wp (prog x) P s) ` S s)

goal (1 subgoal):
 1. \<And>x. x \<in> S s \<Longrightarrow> inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bdd_below ((\<lambda>x. c * wp (prog x) P s) ` S s)
[PROOF STEP]
have "(INF x\<in>S s. c * wp (prog x) P s) \<le> c * wp (prog x) P s"
[PROOF STATE]
proof (prove)
using this:
bdd_below ((\<lambda>x. c * wp (prog x) P s) ` S s)

goal (1 subgoal):
 1. (INF x\<in>S s. c * wp (prog x) P s) \<le> c * wp (prog x) P s
[PROOF STEP]
using \<open>x \<in> S s\<close>
[PROOF STATE]
proof (prove)
using this:
bdd_below ((\<lambda>x. c * wp (prog x) P s) ` S s)
x \<in> S s

goal (1 subgoal):
 1. (INF x\<in>S s. c * wp (prog x) P s) \<le> c * wp (prog x) P s
[PROOF STEP]
by (rule cINF_lower)
[PROOF STATE]
proof (state)
this:
(INF x\<in>S s. c * wp (prog x) P s) \<le> c * wp (prog x) P s

goal (1 subgoal):
 1. \<And>x. x \<in> S s \<Longrightarrow> inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s
[PROOF STEP]
with \<open>c \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
(INF x\<in>S s. c * wp (prog x) P s) \<le> c * wp (prog x) P s
[PROOF STEP]
show "inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
(INF x\<in>S s. c * wp (prog x) P s) \<le> c * wp (prog x) P s

goal (1 subgoal):
 1. inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s
[PROOF STEP]
by (simp add: mult_div_mono_left pos)
[PROOF STATE]
proof (state)
this:
inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> wp (prog x) P s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> (INF a\<in>S s. wp (prog a) P s)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
with \<open>c \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
have "inverse c * ?V \<le> inverse c * ?U"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
inverse c * (INF x\<in>S s. c * wp (prog x) P s) \<le> (INF a\<in>S s. wp (prog a) P s)

goal (1 subgoal):
 1. inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> inverse c * (c * (INF a\<in>S s. wp (prog a) P s))
[PROOF STEP]
by (simp add: mult.assoc [symmetric] image_comp)
[PROOF STATE]
proof (state)
this:
inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> inverse c * (c * (INF a\<in>S s. wp (prog a) P s))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
with pos
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> inverse c * (c * (INF a\<in>S s. wp (prog a) P s))
[PROOF STEP]
have "c * (inverse c * ?V) \<le> c * (inverse c * ?U)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> inverse c * (c * (INF a\<in>S s. wp (prog a) P s))

goal (1 subgoal):
 1. c * (inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)) \<le> c * (inverse c * (c * (INF a\<in>S s. wp (prog a) P s)))
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
c * (inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)) \<le> c * (inverse c * (c * (INF a\<in>S s. wp (prog a) P s)))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
with \<open>c \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
c * (inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)) \<le> c * (inverse c * (c * (INF a\<in>S s. wp (prog a) P s)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
c * (inverse c * Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)) \<le> c * (inverse c * (c * (INF a\<in>S s. wp (prog a) P s)))

goal (1 subgoal):
 1. Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)
[PROOF STEP]
by (simp add:mult.assoc [symmetric])
[PROOF STATE]
proof (state)
this:
Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) \<le> c * (INF a\<in>S s. wp (prog a) P s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c * (INF a\<in>S s. wp (prog a) P s) = Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s)

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

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<lambda>x. c * P x) x)
[PROOF STEP]
have "... = Inf ((\<lambda>a. c * wp (prog a) P s) ` S s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) = (INF a\<in>S s. c * wp (prog a) P s)
[PROOF STEP]
by (simp add: image_comp)
[PROOF STATE]
proof (state)
this:
Inf ((*) c ` (\<lambda>a. wp (prog a) P s) ` S s) = (INF a\<in>S s. c * wp (prog a) P s)

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

goal (1 subgoal):
 1. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * (INF a\<in>S x. wp (prog a) P x) = (INF a\<in>S x. wp (prog a) (\<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 "... = Inf ((\<lambda>a. wp (prog a) (\<lambda>s. c * P s) s) ` S s)"
[PROOF STATE]
proof (prove)
using this:
sound P
0 \<le> c

goal (1 subgoal):
 1. (INF a\<in>S s. c * wp (prog a) P s) = (INF a\<in>S s. wp (prog a) (\<lambda>s. c * P s) s)
[PROOF STEP]
by(simp add:scalingD[OF healthy_scalingD, OF healthy] cong:image_cong)
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. c * wp (prog a) P s) = (INF a\<in>S s. wp (prog a) (\<lambda>s. c * P s) s)

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

goal (1 subgoal):
 1. c * (INF a\<in>S s. wp (prog a) P s) = (INF a\<in>S s. wp (prog a) (\<lambda>s. c * P s) s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c * (INF a\<in>S s. wp (prog a) P s) = (INF a\<in>S s. wp (prog a) (\<lambda>s. c * P s) s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_SetDC:
  fixes prog::"'b \<Rightarrow> 'a prog" and S::"'a \<Rightarrow> 'b set"
  assumes healthy:  "\<And>x s. x \<in> S s \<Longrightarrow> nearly_healthy (wlp (prog x))"
      and nonempty: "\<And>s. \<exists>x. x \<in> S s"
  shows "nearly_healthy (wlp (SetDC prog S))" (is "nearly_healthy ?T")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (SetDC prog S))
[PROOF STEP]
proof(intro nearly_healthyI unitaryI2 bounded_byI nnegI le_funI, simp_all only:wp_eval)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
fix b and P::"'a \<Rightarrow> real" and s::'a
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
assume uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
obtain x where xin: "x \<in> (\<lambda>a. wlp (prog a) P s) ` S s"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. (\<And>x. x \<in> (\<lambda>a. wlp (prog a) P s) ` S s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s

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

goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. unitary x
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. unitary x

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
hence "\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. unitary x

goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
hence "\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s

goal (1 subgoal):
 1. \<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y
[PROOF STEP]
have "Inf ((\<lambda>a. wlp (prog a) P s) ` S s) \<le> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y

goal (1 subgoal):
 1. (INF a\<in>S s. wlp (prog a) P s) \<le> x
[PROOF STEP]
by(intro cInf_lower bdd_belowI, auto)
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. wlp (prog a) P s) \<le> x

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

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

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

goal (3 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P x. unitary P \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> 1
 3. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(INF a\<in>S s. wlp (prog a) P s) \<le> 1
[PROOF STEP]
show "Inf ((\<lambda>a. wlp (prog a) P s) ` S s) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
(INF a\<in>S s. wlp (prog a) P s) \<le> 1

goal (1 subgoal):
 1. (INF a\<in>S s. wlp (prog a) P s) \<le> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. wlp (prog a) P s) \<le> 1

goal (2 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> (INF a\<in>S x. wlp (prog a) P x)
 2. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
from xin uP healthy
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s
unitary P
?x \<in> S ?s \<Longrightarrow> nearly_healthy (wlp (prog ?x))
[PROOF STEP]
show "0 \<le> Inf ((\<lambda>a. wlp (prog a) P s) ` S s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s
unitary P
?x \<in> S ?s \<Longrightarrow> nearly_healthy (wlp (prog ?x))

goal (1 subgoal):
 1. 0 \<le> (INF a\<in>S s. wlp (prog a) P s)
[PROOF STEP]
by(blast dest!:unitary_sound[OF nearly_healthy_unitaryD[OF _ uP]]
             intro:cInf_greatest)
[PROOF STATE]
proof (state)
this:
0 \<le> (INF a\<in>S s. wlp (prog a) P s)

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
fix P::"'a \<Rightarrow> real" and Q and s::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
assume uP: "unitary P" and uQ: "unitary Q" and le: "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> Q

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> S ?s
[PROOF STEP]
obtain x where xin: "x \<in> (\<lambda>a. wlp (prog a) P s) ` S s"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S ?s

goal (1 subgoal):
 1. (\<And>x. x \<in> (\<lambda>a. wlp (prog a) P s) ` S s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
from uP healthy
[PROOF STATE]
proof (chain)
picking this:
unitary P
?x \<in> S ?s \<Longrightarrow> nearly_healthy (wlp (prog ?x))
[PROOF STEP]
have "\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. unitary x"
[PROOF STATE]
proof (prove)
using this:
unitary P
?x \<in> S ?s \<Longrightarrow> nearly_healthy (wlp (prog ?x))

goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. unitary x
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. unitary x

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
hence "\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. unitary x

goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
hence "\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) P) ` S s. 0 \<le> x s

goal (1 subgoal):
 1. \<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
have "\<forall>x\<in>(\<lambda>a. wlp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. y \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>(\<lambda>a. wlp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. y \<le> x
[PROOF STEP]
proof(rule ballI, clarify, rule bexI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<le> wlp (prog a) Q s
 2. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<in> (\<lambda>a. wlp (prog a) P s) ` S s
[PROOF STEP]
fix x and a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<le> wlp (prog a) Q s
 2. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<in> (\<lambda>a. wlp (prog a) P s) ` S s
[PROOF STEP]
assume ain: "a \<in> S s"
[PROOF STATE]
proof (state)
this:
a \<in> S s

goal (2 subgoals):
 1. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<le> wlp (prog a) Q s
 2. \<And>x a. a \<in> S s \<Longrightarrow> ?y4 x a \<in> (\<lambda>a. wlp (prog a) P s) ` S s
[PROOF STEP]
from uP uQ le
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
P \<tturnstile> Q
[PROOF STEP]
show "wlp (prog a) P s \<le> wlp (prog a) Q s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
P \<tturnstile> Q

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

goal (1 subgoal):
 1. \<And>x a. a \<in> S s \<Longrightarrow> wlp (prog a) P s \<in> (\<lambda>a. wlp (prog a) P s) ` S s
[PROOF STEP]
from ain
[PROOF STATE]
proof (chain)
picking this:
a \<in> S s
[PROOF STEP]
show "wlp (prog a) P s \<in> (\<lambda>a. wlp (prog a) P s) ` S s"
[PROOF STATE]
proof (prove)
using this:
a \<in> S s

goal (1 subgoal):
 1. wlp (prog a) P s \<in> (\<lambda>a. wlp (prog a) P s) ` S s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wlp (prog a) P s \<in> (\<lambda>a. wlp (prog a) P s) ` S s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>(\<lambda>a. wlp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. y \<le> x

goal (1 subgoal):
 1. \<And>P Q x. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> (INF a\<in>S x. wlp (prog a) P x) \<le> (INF a\<in>S x. wlp (prog a) Q x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y
\<forall>x\<in>(\<lambda>a. wlp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. y \<le> x
[PROOF STEP]
show "Inf ((\<lambda>a. wlp (prog a) P s) ` S s) \<le> Inf ((\<lambda>a. wlp (prog a) Q s) ` S s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>a. wlp (prog a) P s) ` S s
\<forall>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. 0 \<le> y
\<forall>x\<in>(\<lambda>a. wlp (prog a) Q s) ` S s. \<exists>y\<in>(\<lambda>a. wlp (prog a) P s) ` S s. y \<le> x

goal (1 subgoal):
 1. (INF a\<in>S s. wlp (prog a) P s) \<le> (INF a\<in>S s. wlp (prog a) Q s)
[PROOF STEP]
by(intro cInf_mono, blast+)
[PROOF STATE]
proof (state)
this:
(INF a\<in>S s. wlp (prog a) P s) \<le> (INF a\<in>S s. wlp (prog a) Q s)

goal:
No subgoals!
[PROOF STEP]
qed