[STATEMENT]
lemma refines_determ:
  fixes a::"'s prog"
  assumes da: "determ (wp a)"
      and wa: "well_def a"
      and wb: "well_def b"
      and dr: "a \<sqsubseteq> b"
  shows "a \<simeq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<simeq> b
[PROOF STEP]
txt \<open>Proof by contradiction.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<simeq> b
[PROOF STEP]
proof(rule pequivI, rule contrapos_pp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
from wb
[PROOF STATE]
proof (chain)
picking this:
well_def b
[PROOF STEP]
have "feasible (wp b)"
[PROOF STATE]
proof (prove)
using this:
well_def b

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

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
with wb
[PROOF STATE]
proof (chain)
picking this:
well_def b
feasible (wp b)
[PROOF STEP]
have sab: "sub_add (wp b)"
[PROOF STATE]
proof (prove)
using this:
well_def b
feasible (wp b)

goal (1 subgoal):
 1. sub_add (wp b)
[PROOF STEP]
by(auto dest: sublinear_subadd[OF well_def_wp_sublinear])
[PROOF STATE]
proof (state)
this:
sub_add (wp b)

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
fix P::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
txt \<open>Assume that @{term a} and @{term b} are not equivalent:\<close>
[PROOF STATE]
proof (state)
this:
sound P

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
assume ne: "wp a P \<noteq> wp b P"
[PROOF STATE]
proof (state)
this:
wp a P \<noteq> wp b P

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
txt \<open>Find a point at which they differ.  As @{term "a \<sqsubseteq> b"},
    @{term "wp b P s"} must by strictly greater than @{term "wp a P s"}
    here:\<close>
[PROOF STATE]
proof (state)
this:
wp a P \<noteq> wp b P

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
hence "\<exists>s. wp a P s < wp b P s"
[PROOF STATE]
proof (prove)
using this:
wp a P \<noteq> wp b P

goal (1 subgoal):
 1. \<exists>s. wp a P s < wp b P s
[PROOF STEP]
proof(rule contrapos_np)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>s. wp a P s < wp b P s \<Longrightarrow> wp a P = wp b P
[PROOF STEP]
assume "\<not>(\<exists>s. wp a P s < wp b P s)"
[PROOF STATE]
proof (state)
this:
\<nexists>s. wp a P s < wp b P s

goal (1 subgoal):
 1. \<nexists>s. wp a P s < wp b P s \<Longrightarrow> wp a P = wp b P
[PROOF STEP]
hence "\<forall>s. wp b P s \<le> wp a P s"
[PROOF STATE]
proof (prove)
using this:
\<nexists>s. wp a P s < wp b P s

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

goal (1 subgoal):
 1. \<nexists>s. wp a P s < wp b P s \<Longrightarrow> wp a P = wp b P
[PROOF STEP]
hence "wp b P \<tturnstile> wp a P"
[PROOF STATE]
proof (prove)
using this:
\<forall>s. wp b P s \<le> wp a P s

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

goal (1 subgoal):
 1. \<nexists>s. wp a P s < wp b P s \<Longrightarrow> wp a P = wp b P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wp b P \<tturnstile> wp a P

goal (1 subgoal):
 1. \<nexists>s. wp a P s < wp b P s \<Longrightarrow> wp a P = wp b P
[PROOF STEP]
from sP dr
[PROOF STATE]
proof (chain)
picking this:
sound P
a \<sqsubseteq> b
[PROOF STEP]
have "wp a P \<tturnstile> wp b P"
[PROOF STATE]
proof (prove)
using this:
sound P
a \<sqsubseteq> b

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

goal (1 subgoal):
 1. \<nexists>s. wp a P s < wp b P s \<Longrightarrow> wp a P = wp b P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wp b P \<tturnstile> wp a P
wp a P \<tturnstile> wp b P
[PROOF STEP]
show "wp a P = wp b P"
[PROOF STATE]
proof (prove)
using this:
wp b P \<tturnstile> wp a P
wp a P \<tturnstile> wp b P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s. wp a P s < wp b P s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s. wp a P s < wp b P s
[PROOF STEP]
obtain s where less: "wp a P s < wp b P s"
[PROOF STATE]
proof (prove)
using this:
\<exists>s. wp a P s < wp b P s

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

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
txt \<open>Take a carefully constructed expectation:\<close>
[PROOF STATE]
proof (state)
this:
wp a P s < wp b P s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
let ?Pc = "\<lambda>s. bound_of P - P s"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
have sPc: "sound ?Pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. bound_of P - P s)
[PROOF STEP]
proof(rule soundI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. bound_of P - P s)
 2. nneg (\<lambda>s. bound_of P - P s)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "\<And>s. 0 \<le> P s"
[PROOF STATE]
proof (prove)
using this:
sound P

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

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. bound_of P - P s)
 2. nneg (\<lambda>s. bound_of P - P s)
[PROOF STEP]
hence "\<And>s. ?Pc s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P ?s

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

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. bound_of P - P s)
 2. nneg (\<lambda>s. bound_of P - P s)
[PROOF STEP]
thus "bounded ?Pc"
[PROOF STATE]
proof (prove)
using this:
bound_of P - P ?s \<le> bound_of P

goal (1 subgoal):
 1. Expectations.bounded (\<lambda>s. bound_of P - P s)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
Expectations.bounded (\<lambda>s. bound_of P - P s)

goal (1 subgoal):
 1. nneg (\<lambda>s. bound_of P - P s)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "\<And>s. P s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P

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

goal (1 subgoal):
 1. nneg (\<lambda>s. bound_of P - P s)
[PROOF STEP]
hence "\<And>s. 0 \<le> ?Pc s"
[PROOF STATE]
proof (prove)
using this:
P ?s \<le> bound_of P

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

goal (1 subgoal):
 1. nneg (\<lambda>s. bound_of P - P s)
[PROOF STEP]
thus "nneg ?Pc"
[PROOF STATE]
proof (prove)
using this:
0 \<le> bound_of P - P ?s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sound (\<lambda>s. bound_of P - P s)

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
txt \<open>We then show that @{term "wp b"} violates feasibility, and
    thus healthiness.\<close>
[PROOF STATE]
proof (state)
this:
sound (\<lambda>s. bound_of P - P s)

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "0 \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P

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

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
with da
[PROOF STATE]
proof (chain)
picking this:
determ (wp a)
0 \<le> bound_of P
[PROOF STEP]
have "bound_of P = wp a (\<lambda>s. bound_of P) s"
[PROOF STATE]
proof (prove)
using this:
determ (wp a)
0 \<le> bound_of P

goal (1 subgoal):
 1. bound_of P = wp a (\<lambda>s. bound_of P) s
[PROOF STEP]
by(simp add:maximalD determ_maximalD)
[PROOF STATE]
proof (state)
this:
bound_of P = wp a (\<lambda>s. bound_of P) s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bound_of P = wp a (\<lambda>s. bound_of P) s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
have "... = wp a (\<lambda>s. ?Pc s + P s) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp a (\<lambda>s. bound_of P) s = wp a (\<lambda>s. bound_of P - P s + P s) s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of P) s = wp a (\<lambda>s. bound_of P - P s + P s) s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of P) s = wp a (\<lambda>s. bound_of P - P s + P s) s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
from da sP sPc
[PROOF STATE]
proof (chain)
picking this:
determ (wp a)
sound P
sound (\<lambda>s. bound_of P - P s)
[PROOF STEP]
have "... = wp a ?Pc s + wp a P s"
[PROOF STATE]
proof (prove)
using this:
determ (wp a)
sound P
sound (\<lambda>s. bound_of P - P s)

goal (1 subgoal):
 1. wp a (\<lambda>s. bound_of P - P s + P s) s = wp a (\<lambda>s. bound_of P - P s) s + wp a P s
[PROOF STEP]
by(subst additiveD[OF determ_additiveD], simp_all add:sP sPc)
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of P - P s + P s) s = wp a (\<lambda>s. bound_of P - P s) s + wp a P s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of P - P s + P s) s = wp a (\<lambda>s. bound_of P - P s) s + wp a P s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
from sPc dr
[PROOF STATE]
proof (chain)
picking this:
sound (\<lambda>s. bound_of P - P s)
a \<sqsubseteq> b
[PROOF STEP]
have "... \<le> wp b ?Pc s + wp a P s"
[PROOF STATE]
proof (prove)
using this:
sound (\<lambda>s. bound_of P - P s)
a \<sqsubseteq> b

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

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of P - P s) s + wp a P s \<le> wp b (\<lambda>s. bound_of P - P s) s + wp a P s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
from less
[PROOF STATE]
proof (chain)
picking this:
wp a P s < wp b P s
[PROOF STEP]
have "... < wp b ?Pc s + wp b P s"
[PROOF STATE]
proof (prove)
using this:
wp a P s < wp b P s

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

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp b (\<lambda>s. bound_of P - P s) s + wp a P s < wp b (\<lambda>s. bound_of P - P s) s + wp b P s

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
from sab sP sPc
[PROOF STATE]
proof (chain)
picking this:
sub_add (wp b)
sound P
sound (\<lambda>s. bound_of P - P s)
[PROOF STEP]
have "... \<le> wp b (\<lambda>s. ?Pc s + P s) s"
[PROOF STATE]
proof (prove)
using this:
sub_add (wp b)
sound P
sound (\<lambda>s. bound_of P - P s)

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

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bound_of P < wp b (\<lambda>s. bound_of P - P s + P s) s
[PROOF STEP]
have "\<not>wp b (\<lambda>s. bound_of P) s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
bound_of P < wp b (\<lambda>s. bound_of P - P s + P s) s

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

goal (2 subgoals):
 1. \<And>P. sound P \<Longrightarrow> ?Q2 P
 2. \<And>P. \<lbrakk>sound P; wp a P \<noteq> wp b P\<rbrakk> \<Longrightarrow> \<not> ?Q2 P
[PROOF STEP]
thus "\<not>bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))"
[PROOF STATE]
proof (prove)
using this:
\<not> wp b (\<lambda>s. bound_of P) s \<le> bound_of P

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

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
txt \<open>However,\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
fix P::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

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

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

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nneg (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
have "bounded_by (bound_of P) (\<lambda>s. bound_of P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by (bound_of P) (\<lambda>s. bound_of P)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of P) (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nneg (\<lambda>s. bound_of P)
bounded_by (bound_of P) (\<lambda>s. bound_of P)
[PROOF STEP]
show "bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))"
[PROOF STATE]
proof (prove)
using this:
nneg (\<lambda>s. bound_of P)
bounded_by (bound_of P) (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. bounded_by (bound_of P) (wp b (\<lambda>s. bound_of P))
[PROOF STEP]
using wb
[PROOF STATE]
proof (prove)
using this:
nneg (\<lambda>s. bound_of P)
bounded_by (bound_of P) (\<lambda>s. bound_of P)
well_def b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_det: "\<And>a b::'s prog. \<lbrakk> a \<simeq> b; determ (wp a) \<rbrakk> \<Longrightarrow> determ (wp b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<simeq> b; determ (wp a)\<rbrakk> \<Longrightarrow> determ (wp b)
[PROOF STEP]
proof(intro determI additiveI maximalI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
fix a b::"'s prog" and P::"'s \<Rightarrow> real"
    and Q::"'s \<Rightarrow> real" and s::"'s"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
assume da: "determ (wp a)"
[PROOF STATE]
proof (state)
this:
determ (wp a)

goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
assume sP: "sound P" and sQ: "sound Q"
    and eq: "a \<simeq> b"
[PROOF STATE]
proof (state)
this:
sound P
sound Q
a \<simeq> b

goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
hence "wp b (\<lambda>s. P s + Q s) s =
         wp a (\<lambda>s. P s + Q s) s"
[PROOF STATE]
proof (prove)
using this:
sound P
sound Q
a \<simeq> b

goal (1 subgoal):
 1. wp b (\<lambda>s. P s + Q s) s = wp a (\<lambda>s. P s + Q s) s
[PROOF STEP]
by(simp add:sound_intros)
[PROOF STATE]
proof (state)
this:
wp b (\<lambda>s. P s + Q s) s = wp a (\<lambda>s. P s + Q s) s

goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp b (\<lambda>s. P s + Q s) s = wp a (\<lambda>s. P s + Q s) s

goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
from da sP sQ
[PROOF STATE]
proof (chain)
picking this:
determ (wp a)
sound P
sound Q
[PROOF STEP]
have "... = wp a P s + wp a Q s"
[PROOF STATE]
proof (prove)
using this:
determ (wp a)
sound P
sound Q

goal (1 subgoal):
 1. wp a (\<lambda>s. P s + Q s) s = wp a P s + wp a Q s
[PROOF STEP]
by(simp add:additiveD determ_additiveD)
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. P s + Q s) s = wp a P s + wp a Q s

goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. P s + Q s) s = wp a P s + wp a Q s

goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
from eq sP sQ
[PROOF STATE]
proof (chain)
picking this:
a \<simeq> b
sound P
sound Q
[PROOF STEP]
have "... = wp b P s + wp b Q s"
[PROOF STATE]
proof (prove)
using this:
a \<simeq> b
sound P
sound Q

goal (1 subgoal):
 1. wp a P s + wp a Q s = wp b P s + wp b Q s
[PROOF STEP]
by(simp add:pequivD)
[PROOF STATE]
proof (state)
this:
wp a P s + wp a Q s = wp b P s + wp b Q s

goal (2 subgoals):
 1. \<And>a b P Q s. \<lbrakk>a \<simeq> b; determ (wp a); sound P; sound Q\<rbrakk> \<Longrightarrow> wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
 2. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s
[PROOF STEP]
show "wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s"
[PROOF STATE]
proof (prove)
using this:
wp b (\<lambda>s. P s + Q s) s = wp b P s + wp b Q s

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

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
fix a b::"'s prog" and c::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
assume da: "determ (wp a)"
[PROOF STATE]
proof (state)
this:
determ (wp a)

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
assume "a \<simeq> b"
[PROOF STATE]
proof (state)
this:
a \<simeq> b

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
hence "b \<simeq> a"
[PROOF STATE]
proof (prove)
using this:
a \<simeq> b

goal (1 subgoal):
 1. b \<simeq> a
[PROOF STEP]
by(simp add:ac_simps)
[PROOF STATE]
proof (state)
this:
b \<simeq> a

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b \<simeq> a

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
assume nn: "0 \<le> c"
[PROOF STATE]
proof (state)
this:
0 \<le> c

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b \<simeq> a
0 \<le> c
[PROOF STEP]
have "wp b (\<lambda>_. c) = wp a (\<lambda>_. c)"
[PROOF STATE]
proof (prove)
using this:
b \<simeq> a
0 \<le> c

goal (1 subgoal):
 1. wp b (\<lambda>_. c) = wp a (\<lambda>_. c)
[PROOF STEP]
by(simp add:pequivD const_sound)
[PROOF STATE]
proof (state)
this:
wp b (\<lambda>_. c) = wp a (\<lambda>_. c)

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp b (\<lambda>_. c) = wp a (\<lambda>_. c)

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
from da nn
[PROOF STATE]
proof (chain)
picking this:
determ (wp a)
0 \<le> c
[PROOF STEP]
have "... = (\<lambda>_. c)"
[PROOF STATE]
proof (prove)
using this:
determ (wp a)
0 \<le> c

goal (1 subgoal):
 1. wp a (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
by(simp add:determ_maximalD maximalD)
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>_. c) = (\<lambda>_. c)

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<simeq> b; determ (wp a); 0 \<le> c\<rbrakk> \<Longrightarrow> wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
show "wp b (\<lambda>_. c) = (\<lambda>_. c)"
[PROOF STATE]
proof (prove)
using this:
wp b (\<lambda>_. c) = (\<lambda>_. c)

goal (1 subgoal):
 1. wp b (\<lambda>_. c) = (\<lambda>_. c)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wp b (\<lambda>_. c) = (\<lambda>_. c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma determ_maximal:
  "\<lbrakk> pdeterm a; a \<le> x \<rbrakk> \<Longrightarrow> a = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pdeterm a; a \<le> x\<rbrakk> \<Longrightarrow> a = x
[PROOF STEP]
by(transfer, auto intro:refines_determ)


[STATEMENT]
lemma drefinesD[dest]:
  "\<lbrakk> drefines \<phi> G A B; unitary P; unitary Q; P \<tturnstile> wp A Q \<rbrakk> \<Longrightarrow>
   \<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> wp B (Q o \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drefines \<phi> G A B; unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
unfolding drefines_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P Q. unitary P \<and> unitary Q \<and> P \<tturnstile> wp A Q \<longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>); unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
by(blast)


[STATEMENT]
lemma drefinesD2:
  assumes dr:  "drefines \<phi> G A B"
      and uP:  "unitary P"
      and uQ:  "unitary Q"
      and wpA: "P \<tturnstile> wp A Q"
      and G:   "G s"
  shows "(P o \<phi>) s \<le> wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
from uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
[PROOF STEP]
have "0 \<le> (P o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
unitary P

goal (1 subgoal):
 1. 0 \<le> (P \<circ> \<phi>) s
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
unitary P

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

goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
with G
[PROOF STATE]
proof (chain)
picking this:
G s
0 \<le> (P \<circ> \<phi>) s
[PROOF STEP]
have "(P o \<phi>) s = (\<guillemotleft>G\<guillemotright> && (P o \<phi>)) s"
[PROOF STATE]
proof (prove)
using this:
G s
0 \<le> (P \<circ> \<phi>) s

goal (1 subgoal):
 1. (P \<circ> \<phi>) s = (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)) s
[PROOF STEP]
by(simp add:exp_conj_def)
[PROOF STATE]
proof (state)
this:
(P \<circ> \<phi>) s = (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)) s

goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(P \<circ> \<phi>) s = (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)) s

goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
drefines \<phi> G A B
unitary P
unitary Q
P \<tturnstile> wp A Q
G s
[PROOF STEP]
have "... \<le> wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
drefines \<phi> G A B
unitary P
unitary Q
P \<tturnstile> wp A Q
G s

goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)) s \<le> wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
show "(P o \<phi>) s \<le> ..."
[PROOF STATE]
proof (prove)
using this:
(P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drefinesD3:
  assumes dr: "drefines \<phi> G a b"
      and G:  "G s"
      and uQ: "unitary Q"
      and wa: "well_def a"
  shows "wp a Q (\<phi> s) \<le> wp b (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
let "?L s'" = "wp a Q s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
from uQ wa
[PROOF STATE]
proof (chain)
picking this:
unitary Q
well_def a
[PROOF STEP]
have sL: "sound ?L"
[PROOF STATE]
proof (prove)
using this:
unitary Q
well_def a

goal (1 subgoal):
 1. sound (wp a Q)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
sound (wp a Q)

goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
from uQ wa
[PROOF STATE]
proof (chain)
picking this:
unitary Q
well_def a
[PROOF STEP]
have bL: "bounded_by 1 ?L"
[PROOF STATE]
proof (prove)
using this:
unitary Q
well_def a

goal (1 subgoal):
 1. bounded_by 1 (wp a Q)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bounded_by 1 (wp a Q)

goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
have "?L \<tturnstile> ?L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp a Q \<tturnstile> wp a Q
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp a Q \<tturnstile> wp a Q

goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
with sL and bL and assms
[PROOF STATE]
proof (chain)
picking this:
sound (wp a Q)
bounded_by 1 (wp a Q)
drefines \<phi> G a b
G s
unitary Q
well_def a
wp a Q \<tturnstile> wp a Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sound (wp a Q)
bounded_by 1 (wp a Q)
drefines \<phi> G a b
G s
unitary Q
well_def a
wp a Q \<tturnstile> wp a Q

goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
by(blast intro:drefinesD2[OF dr, where P="?L", simplified])
[PROOF STATE]
proof (state)
this:
wp a Q (\<phi> s) \<le> wp b (Q \<circ> \<phi>) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drefinesI[intro]:
  "\<lbrakk> \<And>P Q. \<lbrakk> unitary P; unitary Q; P \<tturnstile> wp A Q \<rbrakk> \<Longrightarrow>
           \<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> wp B (Q o \<phi>) \<rbrakk> \<Longrightarrow>
   drefines \<phi> G A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)) \<Longrightarrow> drefines \<phi> G A B
[PROOF STEP]
unfolding drefines_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)) \<Longrightarrow> \<forall>P Q. unitary P \<and> unitary Q \<and> P \<tturnstile> wp A Q \<longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
by(blast)


[STATEMENT]
lemma drefinesI2:
  fixes   A::"'a prog"
    and   B::"'b prog"
    and   \<phi>::"'b \<Rightarrow> 'a"
    and   G::"'b \<Rightarrow> bool"
  assumes wB: "well_def B"
      and withAs:
        "\<And>P Q s. \<lbrakk> unitary P; unitary Q;
                 G s; P \<tturnstile> wp A Q \<rbrakk> \<Longrightarrow> (P o \<phi>) s \<le> wp B (Q o \<phi>) s"
  shows "drefines \<phi> G A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G A B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
fix P and Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
assume uP:  "unitary P"
     and uQ:  "unitary Q"
     and wpA: "P \<tturnstile> wp A Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
hence "\<And>s. G s \<Longrightarrow> (P o \<phi>) s \<le> wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>s. G s \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
using withAs
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
P \<tturnstile> wp A Q
\<lbrakk>unitary ?P; unitary ?Q; G ?s; ?P \<tturnstile> wp A ?Q\<rbrakk> \<Longrightarrow> (?P \<circ> \<phi>) ?s \<le> wp B (?Q \<circ> \<phi>) ?s

goal (1 subgoal):
 1. \<And>s. G s \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
G ?s \<Longrightarrow> (P \<circ> \<phi>) ?s \<le> wp B (Q \<circ> \<phi>) ?s

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
G ?s \<Longrightarrow> (P \<circ> \<phi>) ?s \<le> wp B (Q \<circ> \<phi>) ?s

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "unitary (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q

goal (1 subgoal):
 1. unitary (Q \<circ> \<phi>)
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
unitary Q

goal (1 subgoal):
 1. unitary (\<lambda>x. Q (\<phi> x))
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
from uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
[PROOF STEP]
have "unitary (P o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary P

goal (1 subgoal):
 1. unitary (P \<circ> \<phi>)
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
unitary P

goal (1 subgoal):
 1. unitary (\<lambda>x. P (\<phi> x))
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
unitary (P \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
G ?s \<Longrightarrow> (P \<circ> \<phi>) ?s \<le> wp B (Q \<circ> \<phi>) ?s
unitary (Q \<circ> \<phi>)
unitary (P \<circ> \<phi>)
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> wp B (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
G ?s \<Longrightarrow> (P \<circ> \<phi>) ?s \<le> wp B (Q \<circ> \<phi>) ?s
unitary (Q \<circ> \<phi>)
unitary (P \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
using wB
[PROOF STATE]
proof (prove)
using this:
G ?s \<Longrightarrow> (P \<circ> \<phi>) ?s \<le> wp B (Q \<circ> \<phi>) ?s
unitary (Q \<circ> \<phi>)
unitary (P \<circ> \<phi>)
well_def B

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
by(blast intro:entails_pconj_assumption)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_strengthen_guard:
  fixes a::"'s prog" and b::"'t prog"
  assumes fg: "\<And>s. F s \<Longrightarrow> G s"
      and drab: "drefines \<phi> G a b"
  shows "drefines \<phi> F a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> F a b
[PROOF STEP]
proof(intro drefinesI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
fix P Q::"'s expect"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
assume uP: "unitary P" and uQ: "unitary Q"
     and wp: "P \<tturnstile> wp a Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> wp a Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
from fg
[PROOF STATE]
proof (chain)
picking this:
F ?s \<Longrightarrow> G ?s
[PROOF STEP]
have "\<And>s. \<guillemotleft>F\<guillemotright> s \<le> \<guillemotleft>G\<guillemotright> s"
[PROOF STATE]
proof (prove)
using this:
F ?s \<Longrightarrow> G ?s

goal (1 subgoal):
 1. \<And>s. \<guillemotleft> F \<guillemotright> s \<le> \<guillemotleft> G \<guillemotright> s
[PROOF STEP]
by(simp add:embed_bool_def)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> F \<guillemotright> ?s \<le> \<guillemotleft> G \<guillemotright> ?s

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
hence "(\<guillemotleft>F\<guillemotright> && (P o \<phi>)) \<tturnstile> (\<guillemotleft>G\<guillemotright> && (P o \<phi>))"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> F \<guillemotright> ?s \<le> \<guillemotleft> G \<guillemotright> ?s

goal (1 subgoal):
 1. \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)
[PROOF STEP]
by(auto intro:pconj_mono le_funI simp:exp_conj_def)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
from drab uP uQ wp
[PROOF STATE]
proof (chain)
picking this:
drefines \<phi> G a b
unitary P
unitary Q
P \<tturnstile> wp a Q
[PROOF STEP]
have "... \<tturnstile> wp b (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
drefines \<phi> G a b
unitary P
unitary Q
P \<tturnstile> wp a Q

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
show "\<guillemotleft>F\<guillemotright> && (P o \<phi>) \<tturnstile> wp b (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<guillemotleft> F \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pcorresI:
  "\<lbrakk> \<And>Q. unitary Q \<Longrightarrow> \<guillemotleft>G\<guillemotright> && (wp A Q o \<phi>) = \<guillemotleft>G\<guillemotright> && wp B (Q o \<phi>) \<rbrakk> \<Longrightarrow>
   pcorres \<phi> G A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q. unitary Q \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) \<Longrightarrow> pcorres \<phi> G A B
[PROOF STEP]
by(simp add:pcorres_def)


[STATEMENT]
lemma pcorresD:
  "\<lbrakk> pcorres \<phi> G A B; unitary Q \<rbrakk> \<Longrightarrow> \<guillemotleft>G\<guillemotright> && (wp A Q o \<phi>) = \<guillemotleft>G\<guillemotright> && wp B (Q o \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pcorres \<phi> G A B; unitary Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)
[PROOF STEP]
unfolding pcorres_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>Q. unitary Q \<longrightarrow> \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>); unitary Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pcorresD2:
  assumes pc: "pcorres \<phi> G A B"
      and uQ: "unitary Q"
      and wA: "well_def A" and wB: "well_def B"
      and G: "G s"
  shows "wp A Q (\<phi> s) = wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
from uQ well_def_wp_healthy[OF wA]
[PROOF STATE]
proof (chain)
picking this:
unitary Q
healthy (wp A)
[PROOF STEP]
have "0 \<le> wp A Q (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
unitary Q
healthy (wp A)

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

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
with G
[PROOF STATE]
proof (chain)
picking this:
G s
0 \<le> wp A Q (\<phi> s)
[PROOF STEP]
have "wp A Q (\<phi> s) = \<guillemotleft>G\<guillemotright> s .& wp A Q (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
G s
0 \<le> wp A Q (\<phi> s)

goal (1 subgoal):
 1. wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s)

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s)

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s)

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
from pc uQ
[PROOF STATE]
proof (chain)
picking this:
pcorres \<phi> G A B
unitary Q
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> && (wp A Q o \<phi>) = \<guillemotleft>G\<guillemotright> && wp B (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
pcorres \<phi> G A B
unitary Q

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)
[PROOF STEP]
by(rule pcorresD)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
hence "\<guillemotleft>G\<guillemotright> s .& wp A Q (\<phi> s) = \<guillemotleft>G\<guillemotright> s .& wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s
[PROOF STEP]
unfolding exp_conj_def o_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>s. \<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s)) = (\<lambda>s. \<guillemotleft> G \<guillemotright> s .& wp B (\<lambda>x. Q (\<phi> x)) s)

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp B (\<lambda>x. Q (\<phi> x)) s
[PROOF STEP]
by(rule fun_cong)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s .& wp A Q (\<phi> s) = \<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "sound Q"
[PROOF STATE]
proof (prove)
using this:
unitary Q

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

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
hence "sound (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
sound Q

goal (1 subgoal):
 1. sound (Q \<circ> \<phi>)
[PROOF STEP]
by(auto intro:sound_intros)
[PROOF STATE]
proof (state)
this:
sound (Q \<circ> \<phi>)

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
with well_def_wp_healthy[OF wB]
[PROOF STATE]
proof (chain)
picking this:
healthy (wp B)
sound (Q \<circ> \<phi>)
[PROOF STEP]
have "0 \<le> wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp B)
sound (Q \<circ> \<phi>)

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

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
with G
[PROOF STATE]
proof (chain)
picking this:
G s
0 \<le> wp B (Q \<circ> \<phi>) s
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> s .& wp B (Q o \<phi>) s = wp B (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
G s
0 \<le> wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s = wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> s .& wp B (Q \<circ> \<phi>) s = wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wp A Q (\<phi> s) = wp B (Q \<circ> \<phi>) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma refines_drefines:
  fixes a::"'s prog"
  assumes rab: "a \<sqsubseteq> b" and wb: "well_def b"
  shows "drefines (\<lambda>s. s) G a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines (\<lambda>s. s) G a b
[PROOF STEP]
proof(intro drefinesI2 wb, simp add:o_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> P s \<le> wp b Q s
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and Q::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> P s \<le> wp b Q s
[PROOF STEP]
assume sQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> P s \<le> wp b Q s
[PROOF STEP]
assume "P \<tturnstile> wp a Q"
[PROOF STATE]
proof (state)
this:
P \<tturnstile> wp a Q

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> P s \<le> wp b Q s
[PROOF STEP]
hence "P s \<le> wp a Q s"
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> wp a Q

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

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> P s \<le> wp b Q s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P s \<le> wp a Q s

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> P s \<le> wp b Q s
[PROOF STEP]
from rab sQ
[PROOF STATE]
proof (chain)
picking this:
a \<sqsubseteq> b
unitary Q
[PROOF STEP]
have "... \<le> wp b Q s"
[PROOF STATE]
proof (prove)
using this:
a \<sqsubseteq> b
unitary Q

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

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> P s \<le> wp b Q s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
P s \<le> wp b Q s
[PROOF STEP]
show "P s \<le> wp b Q s"
[PROOF STATE]
proof (prove)
using this:
P s \<le> wp b Q s

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_trans[trans]:
  fixes A::"'a prog" and B::"'b prog" and C::"'c prog"
  assumes drAB: "drefines \<phi> G A B"
      and drBC: "drefines \<phi>' G' B C"
      and Gimp: "\<And>s. G' s \<Longrightarrow> G (\<phi>' s)"
  shows "drefines (\<phi> o \<phi>') G' A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines (\<phi> \<circ> \<phi>') G' A C
[PROOF STEP]
proof(rule drefinesI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
fix P::"'a \<Rightarrow> real" and Q::"'a \<Rightarrow> real" and s::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
assume uP: "unitary P" and uQ: "unitary Q"
     and wpA: "P \<tturnstile> wp A Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
have "\<guillemotleft>G'\<guillemotright> && \<guillemotleft>G o \<phi>'\<guillemotright> = \<guillemotleft>G'\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G' \<guillemotright> && \<guillemotleft> G \<circ> \<phi>' \<guillemotright> = \<guillemotleft> G' \<guillemotright>
[PROOF STEP]
proof(rule ext, unfold exp_conj_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
show "\<guillemotleft>G'\<guillemotright> x .& \<guillemotleft>G o \<phi>'\<guillemotright> x = \<guillemotleft>G'\<guillemotright> x" (is ?X)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
proof(cases "G' x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
 2. \<not> G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> G' x

goal (2 subgoals):
 1. G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
 2. \<not> G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> G' x
[PROOF STEP]
show ?X
[PROOF STATE]
proof (prove)
using this:
\<not> G' x

goal (1 subgoal):
 1. \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x

goal (1 subgoal):
 1. G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
G' x

goal (1 subgoal):
 1. G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
G' x

goal (1 subgoal):
 1. G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
with Gimp
[PROOF STATE]
proof (chain)
picking this:
G' ?s \<Longrightarrow> G (\<phi>' ?s)
G' x
[PROOF STEP]
have "(G o \<phi>') x"
[PROOF STATE]
proof (prove)
using this:
G' ?s \<Longrightarrow> G (\<phi>' ?s)
G' x

goal (1 subgoal):
 1. (G \<circ> \<phi>') x
[PROOF STEP]
by(simp add:o_def)
[PROOF STATE]
proof (state)
this:
(G \<circ> \<phi>') x

goal (1 subgoal):
 1. G' x \<Longrightarrow> \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
G' x
(G \<circ> \<phi>') x
[PROOF STEP]
show ?X
[PROOF STATE]
proof (prove)
using this:
G' x
(G \<circ> \<phi>') x

goal (1 subgoal):
 1. \<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> x .& \<guillemotleft> G \<circ> \<phi>' \<guillemotright> x = \<guillemotleft> G' \<guillemotright> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> && \<guillemotleft> G \<circ> \<phi>' \<guillemotright> = \<guillemotleft> G' \<guillemotright>

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
with uP
[PROOF STATE]
proof (chain)
picking this:
unitary P
\<guillemotleft> G' \<guillemotright> && \<guillemotleft> G \<circ> \<phi>' \<guillemotright> = \<guillemotleft> G' \<guillemotright>
[PROOF STEP]
have "\<guillemotleft>G'\<guillemotright> && (P o (\<phi> o \<phi>')) = \<guillemotleft>G'\<guillemotright> && ((\<guillemotleft>G\<guillemotright> && (P o \<phi>)) o \<phi>')"
[PROOF STATE]
proof (prove)
using this:
unitary P
\<guillemotleft> G' \<guillemotright> && \<guillemotleft> G \<circ> \<phi>' \<guillemotright> = \<guillemotleft> G' \<guillemotright>

goal (1 subgoal):
 1. \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) = \<guillemotleft> G' \<guillemotright> && (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<circ> \<phi>')
[PROOF STEP]
by(simp add:exp_conj_assoc o_assoc)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) = \<guillemotleft> G' \<guillemotright> && (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<circ> \<phi>')

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) = \<guillemotleft> G' \<guillemotright> && (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<circ> \<phi>')

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) = \<guillemotleft> G' \<guillemotright> && (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<circ> \<phi>')

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
from uP uQ wpA and drAB
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
P \<tturnstile> wp A Q
drefines \<phi> G A B
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> wp B (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
P \<tturnstile> wp A Q
drefines \<phi> G A B

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
by(blast intro:drefinesD)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
with drBC and uP uQ
[PROOF STATE]
proof (chain)
picking this:
drefines \<phi>' G' B C
unitary P
unitary Q
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
have "\<guillemotleft>G'\<guillemotright> && ((\<guillemotleft>G\<guillemotright> && (P o \<phi>)) o \<phi>') \<tturnstile> wp C ((Q o \<phi>) o \<phi>')"
[PROOF STATE]
proof (prove)
using this:
drefines \<phi>' G' B C
unitary P
unitary Q
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> G' \<guillemotright> && (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<circ> \<phi>') \<tturnstile> wp C (Q \<circ> \<phi> \<circ> \<phi>')
[PROOF STEP]
by(blast intro:unitary_intros drefinesD)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> && (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<circ> \<phi>') \<tturnstile> wp C (Q \<circ> \<phi> \<circ> \<phi>')

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> && (\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<circ> \<phi>') \<tturnstile> wp C (Q \<circ> \<phi> \<circ> \<phi>')

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> \<phi> \<circ> \<phi>')
[PROOF STEP]
show "\<guillemotleft>G'\<guillemotright> && (P o (\<phi> o \<phi>')) \<tturnstile> wp C (Q o (\<phi> o \<phi>'))"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> \<phi> \<circ> \<phi>')

goal (1 subgoal):
 1. \<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))
[PROOF STEP]
by(simp add:o_assoc)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G' \<guillemotright> && (P \<circ> (\<phi> \<circ> \<phi>')) \<tturnstile> wp C (Q \<circ> (\<phi> \<circ> \<phi>'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pr_dr_trans[trans]:
  assumes prAB: "A \<sqsubseteq> B"
      and drBC: "drefines \<phi> G B C"
  shows "drefines \<phi> G A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G A C
[PROOF STEP]
proof(rule drefinesI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
fix P and Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
assume uP:  "unitary P"
     and uQ:  "unitary Q"
     and wpA: "P \<tturnstile> wp A Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
note wpA
[PROOF STATE]
proof (state)
this:
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
from uQ and prAB
[PROOF STATE]
proof (chain)
picking this:
unitary Q
A \<sqsubseteq> B
[PROOF STEP]
have "wp A Q \<tturnstile> wp B Q"
[PROOF STATE]
proof (prove)
using this:
unitary Q
A \<sqsubseteq> B

goal (1 subgoal):
 1. wp A Q \<tturnstile> wp B Q
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wp A Q \<tturnstile> wp B Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
P \<tturnstile> wp B Q
[PROOF STEP]
have "P \<tturnstile> wp B Q"
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> wp B Q

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

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
with uP uQ drBC
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
drefines \<phi> G B C
P \<tturnstile> wp B Q
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> wp C (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
drefines \<phi> G B C
P \<tturnstile> wp B Q

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
by(blast intro:drefinesD)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_pr_trans[trans]:
  assumes drAB: "drefines \<phi> G A B"
  assumes prBC: "B \<sqsubseteq> C"
  shows "drefines \<phi> G A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G A C
[PROOF STEP]
proof(rule drefinesI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
fix P and Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
assume uP:  "unitary P"
     and uQ:  "unitary Q"
     and wpA: "P \<tturnstile> wp A Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
with drAB
[PROOF STATE]
proof (chain)
picking this:
drefines \<phi> G A B
unitary P
unitary Q
P \<tturnstile> wp A Q
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> wp B (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
drefines \<phi> G A B
unitary P
unitary Q
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)
[PROOF STEP]
by(blast intro:drefinesD)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp B (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
from uQ prBC
[PROOF STATE]
proof (chain)
picking this:
unitary Q
B \<sqsubseteq> C
[PROOF STEP]
have "... \<tturnstile> wp C (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q
B \<sqsubseteq> C

goal (1 subgoal):
 1. wp B (Q \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wp B (Q \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> ..."
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_refl:
  assumes wa: "well_def a"
      and comm: "\<And>Q. unitary Q \<Longrightarrow> wp a Q o \<phi> \<tturnstile> wp a (Q o \<phi>)"
  shows "drefines \<phi> G a a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G a a
[PROOF STEP]
proof(intro drefinesI2 wa)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
fix P and Q and s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
assume wp: "P \<tturnstile> wp a Q"
[PROOF STATE]
proof (state)
this:
P \<tturnstile> wp a Q

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
assume uQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
have "(P o \<phi>) s = P (\<phi> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<circ> \<phi>) s = P (\<phi> s)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
(P \<circ> \<phi>) s = P (\<phi> s)

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(P \<circ> \<phi>) s = P (\<phi> s)

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
from wp
[PROOF STATE]
proof (chain)
picking this:
P \<tturnstile> wp a Q
[PROOF STEP]
have "... \<le> wp a Q (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> wp a Q

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

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P (\<phi> s) \<le> wp a Q (\<phi> s)

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P (\<phi> s) \<le> wp a Q (\<phi> s)

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
from comm uQ
[PROOF STATE]
proof (chain)
picking this:
unitary ?Q \<Longrightarrow> wp a ?Q \<circ> \<phi> \<tturnstile> wp a (?Q \<circ> \<phi>)
unitary Q
[PROOF STEP]
have "wp a Q o \<phi> \<tturnstile> wp a (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary ?Q \<Longrightarrow> wp a ?Q \<circ> \<phi> \<tturnstile> wp a (?Q \<circ> \<phi>)
unitary Q

goal (1 subgoal):
 1. wp a Q \<circ> \<phi> \<tturnstile> wp a (Q \<circ> \<phi>)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wp a Q \<circ> \<phi> \<tturnstile> wp a (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
hence "(wp a Q o \<phi>) s \<le> wp a (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
wp a Q \<circ> \<phi> \<tturnstile> wp a (Q \<circ> \<phi>)

goal (1 subgoal):
 1. (wp a Q \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
(wp a Q \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
hence "wp a Q (\<phi> s) \<le> ..."
[PROOF STATE]
proof (prove)
using this:
(wp a Q \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. wp a Q (\<phi> s) \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp a Q (\<phi> s) \<le> wp a (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wp a Q (\<phi> s) \<le> wp a (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp a Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
show  "(P o \<phi>) s \<le> wp a (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
(P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. (P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(P \<circ> \<phi>) s \<le> wp a (Q \<circ> \<phi>) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pcorres_drefine:
  assumes corres: "pcorres \<phi> G A C"
      and wC: "well_def C"
  shows "drefines \<phi> G A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G A C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
fix P and Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
assume uP: "unitary P" and uQ: "unitary Q"
     and wpA: "P \<tturnstile> wp A Q"
[PROOF STATE]
proof (state)
this:
unitary P
unitary Q
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
from wpA
[PROOF STATE]
proof (chain)
picking this:
P \<tturnstile> wp A Q
[PROOF STEP]
have "P o \<phi> \<tturnstile> wp A Q o \<phi>"
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> wp A Q

goal (1 subgoal):
 1. P \<circ> \<phi> \<tturnstile> wp A Q \<circ> \<phi>
[PROOF STEP]
by(simp add:o_def le_fun_def)
[PROOF STATE]
proof (state)
this:
P \<circ> \<phi> \<tturnstile> wp A Q \<circ> \<phi>

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
hence "\<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> \<guillemotleft>G\<guillemotright> && (wp A Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
P \<circ> \<phi> \<tturnstile> wp A Q \<circ> \<phi>

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)
[PROOF STEP]
by(rule exp_conj_mono_right)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
from corres uQ
[PROOF STATE]
proof (chain)
picking this:
pcorres \<phi> G A C
unitary Q
[PROOF STEP]
have "... = \<guillemotleft>G\<guillemotright> && (wp C (Q o \<phi>))"
[PROOF STATE]
proof (prove)
using this:
pcorres \<phi> G A C
unitary Q

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)
[PROOF STEP]
by(rule pcorresD)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
have "... \<tturnstile> wp C (Q o \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
proof(rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) x \<le> wp C (Q \<circ> \<phi>) x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) x \<le> wp C (Q \<circ> \<phi>) x
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "unitary (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q

goal (1 subgoal):
 1. unitary (Q \<circ> \<phi>)
[PROOF STEP]
by(rule unitary_intros)
[PROOF STATE]
proof (state)
this:
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>x. (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) x \<le> wp C (Q \<circ> \<phi>) x
[PROOF STEP]
with well_def_wp_healthy[OF wC]
[PROOF STATE]
proof (chain)
picking this:
healthy (wp C)
unitary (Q \<circ> \<phi>)
[PROOF STEP]
have nn_wpC: "0 \<le> wp C (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp C)
unitary (Q \<circ> \<phi>)

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

goal (1 subgoal):
 1. \<And>x. (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) x \<le> wp C (Q \<circ> \<phi>) x
[PROOF STEP]
show "(\<guillemotleft>G\<guillemotright> && wp C (Q o \<phi>)) s \<le> wp C (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
proof(cases "G s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
G s

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
with nn_wpC
[PROOF STATE]
proof (chain)
picking this:
0 \<le> wp C (Q \<circ> \<phi>) s
G s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> wp C (Q \<circ> \<phi>) s
G s

goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
by(simp add:exp_conj_def)
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
note this
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "unitary (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q

goal (1 subgoal):
 1. unitary (Q \<circ> \<phi>)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
with well_def_wp_healthy[OF wC]
[PROOF STATE]
proof (chain)
picking this:
healthy (wp C)
unitary (Q \<circ> \<phi>)
[PROOF STEP]
have "wp C (Q o \<phi>) s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
healthy (wp C)
unitary (Q \<circ> \<phi>)

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

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wp C (Q \<circ> \<phi>) s \<le> 1

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wp C (Q \<circ> \<phi>) s \<le> 1

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
note nn_wpC
[PROOF STATE]
proof (state)
this:
0 \<le> wp C (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> G s
wp C (Q \<circ> \<phi>) s \<le> 1
0 \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> G s
wp C (Q \<circ> \<phi>) s \<le> 1
0 \<le> wp C (Q \<circ> \<phi>) s

goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s
[PROOF STEP]
by(simp add:exp_conj_def)
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>)) s \<le> wp C (Q \<circ> \<phi>) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && wp C (Q \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>unitary P; unitary Q; P \<tturnstile> wp A Q\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> && (P o \<phi>) \<tturnstile> wp C (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (P \<circ> \<phi>) \<tturnstile> wp C (Q \<circ> \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed