[STATEMENT]
lemma wlp_Loop1:
  fixes body :: "'s prog"
  assumes unitary: "unitary P"
      and healthy: "nearly_healthy (wlp body)"
  shows "wlp (do G \<longrightarrow> body od) P =
   gfp_exp (\<lambda>Q s. \<guillemotleft>G\<guillemotright> s * wlp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s)"
  (is "?X = gfp_exp (?Y P)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wlp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
let "?Z u" = "(body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wlp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
proof(simp only: wp_eval, intro gfp_pulldown assms le_funI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>u P. unitary P \<Longrightarrow> wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>t P. \<lbrakk>\<And>Q. unitary Q \<Longrightarrow> unitary (t Q); unitary P\<rbrakk> \<Longrightarrow> unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 3. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 4. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 5. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
fix u P
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>u P. unitary P \<Longrightarrow> wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>t P. \<lbrakk>\<And>Q. unitary Q \<Longrightarrow> unitary (t Q); unitary P\<rbrakk> \<Longrightarrow> unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 3. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 4. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 5. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
show "wlp (?Z u) P = ?Y P (u P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
[PROOF STEP]
by(simp add:wp_eval negate_embed)
[PROOF STATE]
proof (state)
this:
wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)

goal (4 subgoals):
 1. \<And>t P. \<lbrakk>\<And>Q. unitary Q \<Longrightarrow> unitary (t Q); unitary P\<rbrakk> \<Longrightarrow> unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 3. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 4. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>t P. \<lbrakk>\<And>Q. unitary Q \<Longrightarrow> unitary (t Q); unitary P\<rbrakk> \<Longrightarrow> unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 3. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 4. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
fix t::"'s trans" and P::"'s expect"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>t P. \<lbrakk>\<And>Q. unitary Q \<Longrightarrow> unitary (t Q); unitary P\<rbrakk> \<Longrightarrow> unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 3. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 4. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
assume ut: "\<And>Q. unitary Q \<Longrightarrow> unitary (t Q)" and uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary ?Q \<Longrightarrow> unitary (t ?Q)
unitary P

goal (4 subgoals):
 1. \<And>t P. \<lbrakk>\<And>Q. unitary Q \<Longrightarrow> unitary (t Q); unitary P\<rbrakk> \<Longrightarrow> unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 3. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 4. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
thus "unitary (wlp (?Z t) P)"
[PROOF STATE]
proof (prove)
using this:
unitary ?Q \<Longrightarrow> unitary (t ?Q)
unitary P

goal (1 subgoal):
 1. unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
[PROOF STEP]
by(rule wlp_loop_step_unitary[OF healthy])
[PROOF STATE]
proof (state)
this:
unitary (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)

goal (3 subgoals):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
fix P Q::"'s expect"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
assume uP: "unitary P" and uQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q

goal (3 subgoals):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
show "unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
[PROOF STEP]
proof(intro unitaryI2 nnegI bounded_byI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> 1
[PROOF STEP]
fix s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> 1
[PROOF STEP]
from healthy uQ
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp body)
unitary Q
[PROOF STEP]
have "unitary (wlp body Q)"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp body)
unitary Q

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> 1
[PROOF STEP]
from healthy uQ
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp body)
unitary Q
[PROOF STEP]
have "bounded_by 1 (wlp body Q)"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp body)
unitary Q

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unitary (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)

goal (2 subgoals):
 1. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
fix P Q R::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
assume uP: "unitary P" and uQ: "unitary Q" and uR: "unitary R"
       and le: "Q \<tturnstile> R"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
unitary R
Q \<tturnstile> R

goal (2 subgoals):
 1. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
hence "wlp body Q s \<le> wlp body R s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
unitary R
Q \<tturnstile> R

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

goal (2 subgoals):
 1. \<And>P Q R x. \<lbrakk>unitary P; unitary Q; unitary R; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wlp body R x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
thus "\<guillemotleft>G\<guillemotright> s * wlp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s \<le>
          \<guillemotleft>G\<guillemotright> s * wlp body R s + \<guillemotleft>\<N> G\<guillemotright> s * P s"
[PROOF STATE]
proof (prove)
using this:
wlp body Q s \<le> wlp body R s

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

goal (1 subgoal):
 1. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
fix t u::"'s trans"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
assume "le_utrans t u"
           "\<And>P. unitary P \<Longrightarrow> unitary (t P)"
           "\<And>P. unitary P \<Longrightarrow> unitary (u P)"
[PROOF STATE]
proof (state)
this:
le_utrans t u
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary ?P \<Longrightarrow> unitary (u ?P)

goal (1 subgoal):
 1. \<And>t u. \<lbrakk>le_utrans t u; \<And>P. unitary P \<Longrightarrow> unitary (t P); \<And>P. unitary P \<Longrightarrow> unitary (u P)\<rbrakk> \<Longrightarrow> le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
thus "le_utrans (wlp (?Z t)) (wlp (?Z u))"
[PROOF STATE]
proof (prove)
using this:
le_utrans t u
unitary ?P \<Longrightarrow> unitary (t ?P)
unitary ?P \<Longrightarrow> unitary (u ?P)

goal (1 subgoal):
 1. le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
by(blast intro!:wlp_loop_step_mono[OF healthy])
[PROOF STATE]
proof (state)
this:
le_utrans (wlp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wlp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wlp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wp_loop_sound:
  assumes sP: "sound P"
      and hb: "healthy (wp body)"
  shows "sound (wp do G \<longrightarrow> body od P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
[PROOF STEP]
proof(simp only: wp_eval, intro lfp_trans_sound sP)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 2. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
let ?v = "\<lambda>P s. bound_of P"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 2. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
show "le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_trans (wp (body ;; Embed (\<lambda>P s. bound_of P) \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (\<lambda>P s. bound_of P)
[PROOF STEP]
by(intro le_transI, simp add:wp_eval lfp_loop_fp[unfolded negate_embed] hb)
[PROOF STATE]
proof (state)
this:
le_trans (wp (body ;; Embed (\<lambda>P s. bound_of P) \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (\<lambda>P s. bound_of P)

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> sound (\<lambda>s. bound_of P)
[PROOF STEP]
show "\<And>P. sound P \<Longrightarrow> sound (?v P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> sound (\<lambda>s. bound_of P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sound ?P1 \<Longrightarrow> sound (\<lambda>s. bound_of ?P1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wp_Loop1:
  fixes body :: "'s prog"
  assumes sP: "sound P"
      and healthy: "healthy (wp body)"
  shows "wp (do G \<longrightarrow> body od) P =
   lfp_exp (\<lambda>Q s. \<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s)"
  (is "?X = lfp_exp (?Y P)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
let "?Z u" = "(body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
proof(simp only: wp_eval, intro lfp_pulldown assms le_funI sP mono_transI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>u P. sound P \<Longrightarrow> wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 3. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 4. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 5. \<And>t P. \<lbrakk>\<And>Q. sound Q \<Longrightarrow> sound (t Q); sound P\<rbrakk> \<Longrightarrow> sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 6. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 7. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
fix u P
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>u P. sound P \<Longrightarrow> wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 3. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 4. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 5. \<And>t P. \<lbrakk>\<And>Q. sound Q \<Longrightarrow> sound (t Q); sound P\<rbrakk> \<Longrightarrow> sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 6. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 7. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
show "wp (?Z u) P = ?Y P (u P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
[PROOF STEP]
by(simp add:wp_eval negate_embed)
[PROOF STATE]
proof (state)
this:
wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body (u P) a + \<guillemotleft> \<N> G \<guillemotright> a * P a)

goal (6 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. \<And>t P. \<lbrakk>\<And>Q. sound Q \<Longrightarrow> sound (t Q); sound P\<rbrakk> \<Longrightarrow> sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 5. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 6. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. \<And>t P. \<lbrakk>\<And>Q. sound Q \<Longrightarrow> sound (t Q); sound P\<rbrakk> \<Longrightarrow> sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 5. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 6. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
fix t::"'s trans" and P::"'s expect"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. \<And>t P. \<lbrakk>\<And>Q. sound Q \<Longrightarrow> sound (t Q); sound P\<rbrakk> \<Longrightarrow> sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 5. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 6. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
assume ut: "\<And>Q. sound Q \<Longrightarrow> sound (t Q)" and uP: "sound P"
[PROOF STATE]
proof (state)
this:
sound ?Q \<Longrightarrow> sound (t ?Q)
sound P

goal (6 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. \<And>t P. \<lbrakk>\<And>Q. sound Q \<Longrightarrow> sound (t Q); sound P\<rbrakk> \<Longrightarrow> sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
 5. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 6. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
with healthy
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
sound ?Q \<Longrightarrow> sound (t ?Q)
sound P
[PROOF STEP]
show "sound (wp (?Z t) P)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
sound ?Q \<Longrightarrow> sound (t ?Q)
sound P

goal (1 subgoal):
 1. sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)
[PROOF STEP]
by(rule wp_loop_step_sound)
[PROOF STATE]
proof (state)
this:
sound (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P)

goal (5 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 5. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 5. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
fix P Q::"'s expect"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 5. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
assume sP: "sound P" and sQ: "sound Q"
[PROOF STATE]
proof (state)
this:
sound P
sound Q

goal (5 subgoals):
 1. \<And>P Q. \<lbrakk>sound P; sound Q\<rbrakk> \<Longrightarrow> sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
 2. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 3. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 4. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 5. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
show "sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)
[PROOF STEP]
proof(intro soundI2 nnegI bounded_byI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> ?b
 2. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
[PROOF STEP]
fix s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> ?b
 2. \<And>x. 0 \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
[PROOF STEP]
from sQ
[PROOF STATE]
proof (chain)
picking this:
sound Q
[PROOF STEP]
have "nneg Q" "bounded_by (bound_of Q) Q"
[PROOF STATE]
proof (prove)
using this:
sound Q

goal (1 subgoal):
 1. nneg Q &&& bounded_by (bound_of Q) Q
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
nneg Q
bounded_by (bound_of Q) Q

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

goal (1 subgoal):
 1. bounded_by (bound_of Q) (wp body Q)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of Q) (wp body Q)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sound (\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Q a + \<guillemotleft> \<N> G \<guillemotright> a * P a)

goal (4 subgoals):
 1. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 3. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 4. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 3. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 4. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
fix P Q R::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 3. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 4. \<And>P. sound P \<Longrightarrow> sound (?v P)
[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 (4 subgoals):
 1. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 3. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 4. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
hence "wp body Q s \<le> wp body R s"
[PROOF STATE]
proof (prove)
using this:
sound Q
sound R
Q \<tturnstile> R

goal (1 subgoal):
 1. wp body Q s \<le> wp body R s
[PROOF STEP]
by(blast intro:le_funD[OF mono_transD, OF healthy_monoD, OF healthy])
[PROOF STATE]
proof (state)
this:
wp body Q s \<le> wp body R s

goal (4 subgoals):
 1. \<And>P Pa Q x. \<lbrakk>sound P; sound Pa; sound Q; Pa \<tturnstile> Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wp body Pa x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> \<guillemotleft> G \<guillemotright> x * wp body Q x + \<guillemotleft> \<N> G \<guillemotright> x * P x
 2. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 3. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 4. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
thus "\<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s \<le>
          \<guillemotleft>G\<guillemotright> s * wp body R s + \<guillemotleft>\<N> G\<guillemotright> s * P s"
[PROOF STATE]
proof (prove)
using this:
wp body Q s \<le> wp body R s

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

goal (3 subgoals):
 1. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 2. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 3. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 2. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 3. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
fix t u::"'s trans"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 2. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 3. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
assume le: "le_trans t u"
       and st: "\<And>P. sound P \<Longrightarrow> sound (t P)"
       and su: "\<And>P. sound P \<Longrightarrow> sound (u P)"
[PROOF STATE]
proof (state)
this:
le_trans t u
sound ?P \<Longrightarrow> sound (t ?P)
sound ?P \<Longrightarrow> sound (u ?P)

goal (3 subgoals):
 1. \<And>t u. \<lbrakk>le_trans t u; \<And>P. sound P \<Longrightarrow> sound (t P); \<And>P. sound P \<Longrightarrow> sound (u P)\<rbrakk> \<Longrightarrow> le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
 2. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 3. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
with healthy
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
le_trans t u
sound ?P \<Longrightarrow> sound (t ?P)
sound ?P \<Longrightarrow> sound (u ?P)
[PROOF STEP]
show "le_trans (wp (?Z t)) (wp (?Z u))"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
le_trans t u
sound ?P \<Longrightarrow> sound (t ?P)
sound ?P \<Longrightarrow> sound (u ?P)

goal (1 subgoal):
 1. le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
by(rule wp_loop_step_mono)
[PROOF STATE]
proof (state)
this:
le_trans (wp (body ;; Embed t \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (wp (body ;; Embed u \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))

goal (2 subgoals):
 1. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 2. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. le_trans (wp (body ;; Embed ?v \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) ?v
 2. \<And>P. sound P \<Longrightarrow> sound (?v P)
[PROOF STEP]
from healthy
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
[PROOF STEP]
show "le_trans (wp (?Z (\<lambda>P s. bound_of P))) (\<lambda>P s. bound_of P)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)

goal (1 subgoal):
 1. le_trans (wp (body ;; Embed (\<lambda>a b. bound_of a) \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (\<lambda>P s. bound_of P)
[PROOF STEP]
by(intro le_transI, simp add:wp_eval lfp_loop_fp[unfolded negate_embed])
[PROOF STATE]
proof (state)
this:
le_trans (wp (body ;; Embed (\<lambda>a b. bound_of a) \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip)) (\<lambda>P s. bound_of P)

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> sound (\<lambda>s. bound_of P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> sound (\<lambda>s. bound_of P)
[PROOF STEP]
fix P::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> sound (\<lambda>s. bound_of P)
[PROOF STEP]
assume "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> sound (\<lambda>s. bound_of P)
[PROOF STEP]
thus "sound (\<lambda>s. bound_of P)"
[PROOF STATE]
proof (prove)
using this:
sound P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip) P = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nearly_healthy_wlp_loop:
  fixes body::"'s prog"
  assumes hb: "nearly_healthy (wlp body)"
  shows "nearly_healthy (wlp (do G \<longrightarrow> body od))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nearly_healthy (wlp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
proof(intro nearly_healthyI unitaryI2 nnegI2 bounded_byI2, simp_all add:wlp_Loop1 hb)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> \<lambda>s. 0 \<tturnstile> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 2. \<And>P. unitary P \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. 1
 3. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
fix P::"'s expect"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> \<lambda>s. 0 \<tturnstile> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 2. \<And>P. unitary P \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. 1
 3. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
assume uP: "unitary P"
[PROOF STATE]
proof (state)
this:
unitary P

goal (3 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> \<lambda>s. 0 \<tturnstile> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 2. \<And>P. unitary P \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. 1
 3. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
let "?X R" = "\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * R s"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> \<lambda>s. 0 \<tturnstile> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 2. \<And>P. unitary P \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. 1
 3. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
show "\<lambda>s. 0 \<tturnstile> gfp_exp (?X P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b)
[PROOF STEP]
proof(rule gfp_exp_upperbound)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lambda>s. 0 \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (\<lambda>a. 0) a + \<guillemotleft> \<N> G \<guillemotright> a * P a
 2. unitary (\<lambda>s. 0)
[PROOF STEP]
show "unitary (\<lambda>s. 0::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (\<lambda>s. 0)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (\<lambda>s. 0)

goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (\<lambda>a. 0) a + \<guillemotleft> \<N> G \<guillemotright> a * P a
[PROOF STEP]
with hb
[PROOF STATE]
proof (chain)
picking this:
nearly_healthy (wlp body)
unitary (\<lambda>s. 0)
[PROOF STEP]
have "unitary (wlp body (\<lambda>s. 0))"
[PROOF STATE]
proof (prove)
using this:
nearly_healthy (wlp body)
unitary (\<lambda>s. 0)

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

goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (\<lambda>a. 0) a + \<guillemotleft> \<N> G \<guillemotright> a * P a
[PROOF STEP]
with uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary (wlp body (\<lambda>s. 0))
[PROOF STEP]
show "\<lambda>s. 0 \<tturnstile> (?X P (\<lambda>s. 0))"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary (wlp body (\<lambda>s. 0))

goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (\<lambda>a. 0) a + \<guillemotleft> \<N> G \<guillemotright> a * P a
[PROOF STEP]
by(blast intro!:le_funI add_nonneg_nonneg mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
\<lambda>s. 0 \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body (\<lambda>a. 0) a + \<guillemotleft> \<N> G \<guillemotright> a * P a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lambda>s. 0 \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b)

goal (2 subgoals):
 1. \<And>P. unitary P \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. 1
 2. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
show "gfp_exp (?X P) \<tturnstile> \<lambda>s. 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> \<lambda>s. 1
[PROOF STEP]
proof(rule gfp_exp_least)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> \<lambda>s. 1
 2. unitary (\<lambda>s. 1)
[PROOF STEP]
show "unitary (\<lambda>s. 1::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (\<lambda>s. 1)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
unitary (\<lambda>s. 1)

goal (1 subgoal):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> \<lambda>s. 1
[PROOF STEP]
fix Q::"'s expect"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> \<lambda>s. 1
[PROOF STEP]
assume "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (1 subgoal):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> \<lambda>s. 1
[PROOF STEP]
thus "Q \<tturnstile> \<lambda>s. 1"
[PROOF STATE]
proof (prove)
using this:
unitary Q

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> \<lambda>s. 1

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
fix Q::"'s expect"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
assume uQ: "unitary Q" and le: "P \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
unitary Q
P \<tturnstile> Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> gfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wlp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> gfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wlp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
show "gfp_exp (?X P) \<tturnstile> gfp_exp (?X Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
[PROOF STEP]
proof(rule gfp_exp_least)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
 2. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
fix R::"'s expect"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
 2. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
assume uR: "unitary R"
[PROOF STATE]
proof (state)
this:
unitary R

goal (2 subgoals):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
 2. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
assume fp: "R \<tturnstile> ?X P R"
[PROOF STATE]
proof (state)
this:
R \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * P a

goal (2 subgoals):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
 2. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * P a

goal (2 subgoals):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
 2. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
from le
[PROOF STATE]
proof (chain)
picking this:
P \<tturnstile> Q
[PROOF STEP]
have "... \<tturnstile> ?X Q R"
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> Q

goal (1 subgoal):
 1. \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * P a \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a
[PROOF STEP]
by(blast intro:add_mono mult_left_mono le_funI)
[PROOF STATE]
proof (state)
this:
\<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * P a \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a

goal (2 subgoals):
 1. \<And>Pa. \<lbrakk>Pa \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * P a; unitary Pa\<rbrakk> \<Longrightarrow> Pa \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
 2. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
R \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a
[PROOF STEP]
show "R \<tturnstile> gfp_exp (?X Q)"
[PROOF STATE]
proof (prove)
using this:
R \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a

goal (1 subgoal):
 1. R \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
[PROOF STEP]
using uR
[PROOF STATE]
proof (prove)
using this:
R \<tturnstile> \<lambda>a. \<guillemotleft> G \<guillemotright> a * wlp body R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a
unitary R

goal (1 subgoal):
 1. R \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
[PROOF STEP]
by(auto intro:gfp_exp_upperbound)
[PROOF STATE]
proof (state)
this:
R \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)

goal (1 subgoal):
 1. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
show "unitary (gfp_exp (?X Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))
[PROOF STEP]
proof(rule gfp_exp_unitary, intro unitaryI2 nnegI bounded_byI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body P x + \<guillemotleft> \<N> G \<guillemotright> x * Q x
 2. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body P x + \<guillemotleft> \<N> G \<guillemotright> x * Q x \<le> 1
[PROOF STEP]
fix R::"'s expect" and s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P x. unitary P \<Longrightarrow> 0 \<le> \<guillemotleft> G \<guillemotright> x * wlp body P x + \<guillemotleft> \<N> G \<guillemotright> x * Q x
 2. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body P x + \<guillemotleft> \<N> G \<guillemotright> x * Q x \<le> 1
[PROOF STEP]
assume uR: "unitary R"
[PROOF STATE]
proof (state)
this:
unitary R

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

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

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

goal (1 subgoal):
 1. 0 \<le> \<guillemotleft> G \<guillemotright> s * wlp body R s + \<guillemotleft> \<N> G \<guillemotright> s * Q s
[PROOF STEP]
by(blast intro:add_nonneg_nonneg mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> \<guillemotleft> G \<guillemotright> s * wlp body R s + \<guillemotleft> \<N> G \<guillemotright> s * Q s

goal (1 subgoal):
 1. \<And>P x. unitary P \<Longrightarrow> \<guillemotleft> G \<guillemotright> x * wlp body P x + \<guillemotleft> \<N> G \<guillemotright> x * Q x \<le> 1
[PROOF STEP]
from ubP uQ
[PROOF STATE]
proof (chain)
picking this:
unitary (wlp body R)
unitary Q
[PROOF STEP]
have "wlp body R s \<le> 1" "Q s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary (wlp body R)
unitary Q

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

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

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

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

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * wlp body R s + \<guillemotleft> \<N> G \<guillemotright> s * Q s \<le> 1
[PROOF STEP]
by(simp add:negate_embed)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s * wlp body R s + \<guillemotleft> \<N> G \<guillemotright> s * Q s \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unitary (gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> gfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wlp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)

goal:
No subgoals!
[PROOF STEP]
qed