[STATEMENT]
lemma drefines_determ:
  fixes a::"'a prog" and b::"'b prog"
  assumes da: "determ (wp a)"
      and wa: "well_def a"
      and wb: "well_def b"
      and dr: "drefines \<phi> G a b"
  shows "pcorres \<phi> G a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcorres \<phi> G a b
[PROOF STEP]
txt \<open>The proof follows exactly the same form
    as that for program refinement: Assuming that correspondence
    \emph{doesn't} hold, we show that @{term "wp b"} is not feasible,
    and thus not healthy, contradicting the assumption.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcorres \<phi> G a b
[PROOF STEP]
proof(rule pcorresI, rule contrapos_pp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Q. unitary Q \<Longrightarrow> ?Q2 Q
 2. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> ?Q2 Q
[PROOF STEP]
from wb
[PROOF STATE]
proof (chain)
picking this:
well_def b
[PROOF STEP]
show "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 (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
note ha = well_def_wp_healthy[OF wa]
[PROOF STATE]
proof (state)
this:
healthy (wp a)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
note hb = well_def_wp_healthy[OF wb]
[PROOF STATE]
proof (state)
this:
healthy (wp b)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from wb
[PROOF STATE]
proof (chain)
picking this:
well_def b
[PROOF STEP]
have "sublinear (wp b)"
[PROOF STATE]
proof (prove)
using this:
well_def b

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sublinear (wp b)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from hb
[PROOF STATE]
proof (chain)
picking this:
healthy (wp b)
[PROOF STEP]
have "feasible (wp b)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp b)

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sublinear (wp b)
feasible (wp b)
[PROOF STEP]
have sab: "sub_add (wp b)"
[PROOF STATE]
proof (prove)
using this:
sublinear (wp b)
feasible (wp b)

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
fix Q::"'a \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
assume uQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
hence uQ\<phi>: "unitary (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
assume ne: "\<guillemotleft>G\<guillemotright> && (wp a Q o \<phi>) \<noteq> \<guillemotleft>G\<guillemotright> && wp b (Q o \<phi>)"
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
hence ne': "wp a Q o \<phi> \<noteq> wp b (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
txt \<open>From refinement, @{term "\<guillemotleft>G\<guillemotright> && (wp a Q o \<phi>)"}
    lies below @{term "\<guillemotleft>G\<guillemotright> && wp b (Q o \<phi>)"}.\<close>
[PROOF STATE]
proof (state)
this:
wp a Q \<circ> \<phi> \<noteq> wp b (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from ha uQ
[PROOF STATE]
proof (chain)
picking this:
healthy (wp a)
unitary Q
[PROOF STEP]
have gle: "\<guillemotleft>G\<guillemotright> && (wp a Q o \<phi>) \<tturnstile> wp b (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp a)
unitary Q

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
have le: "\<guillemotleft>G\<guillemotright> && (wp a Q o \<phi>) \<tturnstile> \<guillemotleft>G\<guillemotright> && wp b (Q o \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. \<guillemotleft> G \<guillemotright> s .& (wp a Q \<circ> \<phi>) s \<tturnstile> \<lambda>s. \<guillemotleft> G \<guillemotright> s .& wp b (Q \<circ> \<phi>) s
[PROOF STEP]
proof(rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x .& (wp a Q \<circ> \<phi>) x \<le> \<guillemotleft> G \<guillemotright> x .& wp b (Q \<circ> \<phi>) x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x .& (wp a Q \<circ> \<phi>) x \<le> \<guillemotleft> G \<guillemotright> x .& wp b (Q \<circ> \<phi>) x
[PROOF STEP]
from gle
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> s .& (wp a Q o \<phi>) s \<le> wp b (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<tturnstile> wp b (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s .& (wp a Q \<circ> \<phi>) s \<le> wp b (Q \<circ> \<phi>) s
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
using this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s .& (wp a Q \<circ> \<phi>) s \<tturnstile> wp b (Q \<circ> \<phi>)

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

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x .& (wp a Q \<circ> \<phi>) x \<le> \<guillemotleft> G \<guillemotright> x .& wp b (Q \<circ> \<phi>) x
[PROOF STEP]
hence "\<guillemotleft>G\<guillemotright> s .& (\<guillemotleft>G\<guillemotright> s .& (wp a Q o \<phi>) s) \<le> \<guillemotleft>G\<guillemotright> s .& wp b (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> s .& (wp a Q \<circ> \<phi>) s \<le> wp b (Q \<circ> \<phi>) s

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

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

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x .& (wp a Q \<circ> \<phi>) x \<le> \<guillemotleft> G \<guillemotright> x .& wp b (Q \<circ> \<phi>) x
[PROOF STEP]
from uQ ha
[PROOF STATE]
proof (chain)
picking this:
unitary Q
healthy (wp a)
[PROOF STEP]
have "wp a Q (\<phi> s) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary Q
healthy (wp a)

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

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

goal (1 subgoal):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x .& (wp a Q \<circ> \<phi>) x \<le> \<guillemotleft> G \<guillemotright> x .& wp b (Q \<circ> \<phi>) x
[PROOF STEP]
from uQ ha
[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. \<And>x. \<guillemotleft> G \<guillemotright> x .& (wp a Q \<circ> \<phi>) x \<le> \<guillemotleft> G \<guillemotright> x .& wp b (Q \<circ> \<phi>) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> s .& (\<guillemotleft> G \<guillemotright> s .& (wp a Q \<circ> \<phi>) s) \<le> \<guillemotleft> G \<guillemotright> s .& wp b (Q \<circ> \<phi>) s
wp a Q (\<phi> s) \<le> 1
0 \<le> wp a Q (\<phi> s)
[PROOF STEP]
show "\<guillemotleft> G \<guillemotright> s .& (wp a Q \<circ> \<phi>) s \<le> \<guillemotleft> G \<guillemotright> s .& wp b (Q \<circ> \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> s .& (\<guillemotleft> G \<guillemotright> s .& (wp a Q \<circ> \<phi>) s) \<le> \<guillemotleft> G \<guillemotright> s .& wp b (Q \<circ> \<phi>) s
wp a Q (\<phi> s) \<le> 1
0 \<le> wp a Q (\<phi> s)

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

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
txt \<open>If the programs do not correspond, the terms must differ somewhere, and given the previous
  result, the second must be somewhere strictly larger than the first:\<close>
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
have nle: "\<exists>s. (\<guillemotleft>G\<guillemotright> && (wp a Q o \<phi>)) s < (\<guillemotleft>G\<guillemotright> && wp b (Q o \<phi>)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s
[PROOF STEP]
proof(rule contrapos_np[OF ne], rule ext, rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x
 2. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x
 2. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x
[PROOF STEP]
from le
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)
[PROOF STEP]
show "(\<guillemotleft>G\<guillemotright> && (wp a Q o \<phi>)) s \<le> (\<guillemotleft>G\<guillemotright> && wp b (Q o \<phi>)) s"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<tturnstile> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)

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

goal (1 subgoal):
 1. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x
[PROOF STEP]
assume "\<not> (\<exists>s. (\<guillemotleft>G\<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft>G\<guillemotright> && wp b (Q \<circ> \<phi>)) s)"
[PROOF STATE]
proof (state)
this:
\<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. \<And>x. \<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) x \<le> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) x
[PROOF STEP]
thus " (\<guillemotleft>G\<guillemotright> && (wp b (Q \<circ> \<phi>))) s \<le> (\<guillemotleft>G\<guillemotright> && (wp a Q \<circ> \<phi>)) s"
[PROOF STATE]
proof (prove)
using this:
\<nexists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

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

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s
[PROOF STEP]
obtain s where less_s:
    "(\<guillemotleft>G\<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft>G\<guillemotright> && wp b (Q \<circ> \<phi>)) s"
[PROOF STATE]
proof (prove)
using this:
\<exists>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. (\<And>s. (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
txt \<open>The transformers themselves must differ at this point:\<close>
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
hence larger: "wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
proof(cases "G s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
 2. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
G s

goal (2 subgoals):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
 2. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
G s

goal (2 subgoals):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
 2. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
from ha uQ
[PROOF STATE]
proof (chain)
picking this:
healthy (wp a)
unitary Q
[PROOF STEP]
have "0 \<le> wp a Q (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp a)
unitary Q

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

goal (2 subgoals):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
 2. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> wp a Q (\<phi> s)

goal (2 subgoals):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
 2. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
from hb uQ\<phi>
[PROOF STATE]
proof (chain)
picking this:
healthy (wp b)
unitary (Q \<circ> \<phi>)
[PROOF STEP]
have "0 \<le> wp b (Q o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
healthy (wp b)
unitary (Q \<circ> \<phi>)

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

goal (2 subgoals):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
 2. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> wp b (Q \<circ> \<phi>) s

goal (2 subgoals):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
 2. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
note less_s
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> 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 "bounded_by 1 (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q

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

goal (1 subgoal):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bounded_by 1 (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
from unitary_sound[OF uQ]
[PROOF STATE]
proof (chain)
picking this:
sound Q
[PROOF STEP]
have "sound (Q o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
sound Q

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

goal (1 subgoal):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bounded_by 1 (Q \<circ> \<phi>)
sound (Q \<circ> \<phi>)
[PROOF STEP]
have "wp b (Q o \<phi>) s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 (Q \<circ> \<phi>)
sound (Q \<circ> \<phi>)

goal (1 subgoal):
 1. wp b (Q \<circ> \<phi>) s \<le> 1
[PROOF STEP]
using hb
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 (Q \<circ> \<phi>)
sound (Q \<circ> \<phi>)
healthy (wp b)

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

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

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

goal (1 subgoal):
 1. \<lbrakk>(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s; \<not> G s\<rbrakk> \<Longrightarrow> wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
[PROOF STEP]
note less_s
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s < (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s

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

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
txt \<open>@{term G} must also hold, as otherwise both would be zero.\<close>
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s \<noteq> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
hence G_s: "G s"
[PROOF STATE]
proof (prove)
using this:
(\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s \<noteq> (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s

goal (1 subgoal):
 1. G s
[PROOF STEP]
proof(rule contrapos_np)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s
[PROOF STEP]
assume nG: "\<not> G s"
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp b (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 a Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s
[PROOF STEP]
from ha uQ
[PROOF STATE]
proof (chain)
picking this:
healthy (wp a)
unitary Q
[PROOF STEP]
have "wp a Q (\<phi> s) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
healthy (wp a)
unitary Q

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bounded_by 1 (Q \<circ> \<phi>)
sound (Q \<circ> \<phi>)
[PROOF STEP]
have "wp b (Q o \<phi>) s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 (Q \<circ> \<phi>)
sound (Q \<circ> \<phi>)

goal (1 subgoal):
 1. wp b (Q \<circ> \<phi>) s \<le> 1
[PROOF STEP]
using hb
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 (Q \<circ> \<phi>)
sound (Q \<circ> \<phi>)
healthy (wp b)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
G s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
txt \<open>Take a carefully constructed expectation:\<close>
[PROOF STATE]
proof (state)
this:
G s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
let ?Qc = "\<lambda>s. bound_of Q - Q s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
have bQc: "bounded_by 1 ?Qc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by 1 (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
proof(rule bounded_byI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bound_of Q - Q x \<le> 1
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bound_of Q - Q x \<le> 1
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "bound_of Q \<le> 1" and "0 \<le> Q s"
[PROOF STATE]
proof (prove)
using this:
unitary Q

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

goal (1 subgoal):
 1. \<And>x. bound_of Q - Q x \<le> 1
[PROOF STEP]
thus "bound_of Q - Q s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
bound_of Q \<le> 1
0 \<le> Q s

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

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
have sQc: "sound ?Qc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
proof(rule soundI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. bound_of Q - Q s)
 2. nneg (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
from bQc
[PROOF STATE]
proof (chain)
picking this:
bounded_by 1 (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
show "bounded ?Qc"
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 (\<lambda>s. bound_of Q - Q s)

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

goal (1 subgoal):
 1. nneg (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
show "nneg ?Qc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
proof(rule nnegI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. 0 \<le> bound_of Q - Q x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. 0 \<le> bound_of Q - Q x
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "Q s \<le> bound_of Q"
[PROOF STATE]
proof (prove)
using this:
unitary Q

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

goal (1 subgoal):
 1. \<And>x. 0 \<le> bound_of Q - Q x
[PROOF STEP]
thus "0 \<le> bound_of Q - Q s"
[PROOF STATE]
proof (prove)
using this:
Q s \<le> bound_of Q

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

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

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
txt \<open>By the maximality of @{term "wp a"}, @{term "wp b"} must violate feasibility, by mapping
  @{term s} to something strictly greater than @{term "bound_of Q"}.\<close>
[PROOF STATE]
proof (state)
this:
sound (\<lambda>s. bound_of Q - Q s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "0 \<le> bound_of Q"
[PROOF STATE]
proof (prove)
using this:
unitary Q

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
with da
[PROOF STATE]
proof (chain)
picking this:
determ (wp a)
0 \<le> bound_of Q
[PROOF STEP]
have "bound_of Q = wp a (\<lambda>s. bound_of Q) (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
determ (wp a)
0 \<le> bound_of Q

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bound_of Q = wp a (\<lambda>s. bound_of Q) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
have "wp a (\<lambda>s. bound_of Q) (\<phi> s) = wp a (\<lambda>s. Q s + ?Qc s) (\<phi> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp a (\<lambda>s. bound_of Q) (\<phi> s) = wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of Q) (\<phi> s) = wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of Q) (\<phi> s) = wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. bound_of Q) (\<phi> s) = wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from da
[PROOF STATE]
proof (chain)
picking this:
determ (wp a)
[PROOF STEP]
have "additive (wp a)"
[PROOF STATE]
proof (prove)
using this:
determ (wp a)

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
with uQ sQc
[PROOF STATE]
proof (chain)
picking this:
unitary Q
sound (\<lambda>s. bound_of Q - Q s)
Transformers.additive (wp a)
[PROOF STEP]
have "wp a (\<lambda>s. Q s + ?Qc s) (\<phi> s) =
          wp a Q (\<phi> s) + wp a ?Qc (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
unitary Q
sound (\<lambda>s. bound_of Q - Q s)
Transformers.additive (wp a)

goal (1 subgoal):
 1. wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s) = wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)
[PROOF STEP]
by(subst additiveD, blast+)
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s) = wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s) = wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s) = wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wp a (\<lambda>s. Q s + (bound_of Q - Q s)) (\<phi> s) = wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from ha and sQc and bQc
[PROOF STATE]
proof (chain)
picking this:
healthy (wp a)
sound (\<lambda>s. bound_of Q - Q s)
bounded_by 1 (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> && (wp a ?Qc o \<phi>) \<tturnstile> wp b (?Qc o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp a)
sound (\<lambda>s. bound_of Q - Q s)
bounded_by 1 (\<lambda>s. bound_of Q - Q s)

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp a (\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) \<tturnstile> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>)
[PROOF STEP]
by(blast intro!:drefinesD[OF dr])
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> && (wp a (\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) \<tturnstile> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>)

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

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<guillemotleft> G \<guillemotright> && (wp a (\<lambda>s. bound_of Q - Q s) \<circ> \<phi>)) s \<le> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from sQc and ha
[PROOF STATE]
proof (chain)
picking this:
sound (\<lambda>s. bound_of Q - Q s)
healthy (wp a)
[PROOF STEP]
have "0 \<le> wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)"
[PROOF STATE]
proof (prove)
using this:
sound (\<lambda>s. bound_of Q - Q s)
healthy (wp a)

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<guillemotleft> G \<guillemotright> && (wp a (\<lambda>s. bound_of Q - Q s) \<circ> \<phi>)) s \<le> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s
0 \<le> wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)
[PROOF STEP]
have "wp a ?Qc (\<phi> s) \<le> wp b (?Qc o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
(\<guillemotleft> G \<guillemotright> && (wp a (\<lambda>s. bound_of Q - Q s) \<circ> \<phi>)) s \<le> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s
0 \<le> wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)

goal (1 subgoal):
 1. wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) \<le> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s
[PROOF STEP]
using G_s
[PROOF STATE]
proof (prove)
using this:
(\<guillemotleft> G \<guillemotright> && (wp a (\<lambda>s. bound_of Q - Q s) \<circ> \<phi>)) s \<le> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s
0 \<le> wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s)
G s

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
hence "wp a Q (\<phi> s) + wp a ?Qc (\<phi> s) \<le> wp a Q (\<phi> s) + wp b (?Qc o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) \<le> wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) \<le> wp a Q (\<phi> s) + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
with larger
[PROOF STATE]
proof (chain)
picking this:
wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) \<le> wp a Q (\<phi> s) + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s
[PROOF STEP]
have "wp a Q (\<phi> s) + wp b (?Qc o \<phi>) s <
          wp b (Q o \<phi>) s + wp b (?Qc o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
wp a Q (\<phi> s) < wp b (Q \<circ> \<phi>) s
wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) \<le> wp a Q (\<phi> s) + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) < wp b (Q \<circ> \<phi>) s + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s
[PROOF STEP]
have "wp a Q (\<phi> s) + wp a ?Qc (\<phi> s) <
          wp b (Q o \<phi>) s + wp b (?Qc o \<phi>) s"
[PROOF STATE]
proof (prove)
using this:
wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) < wp b (Q \<circ> \<phi>) s + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) < wp b (Q \<circ> \<phi>) s + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a Q (\<phi> s) + wp a (\<lambda>s. bound_of Q - Q s) (\<phi> s) < wp b (Q \<circ> \<phi>) s + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
from sab and unitary_sound[OF uQ] and sQc
[PROOF STATE]
proof (chain)
picking this:
sub_add (wp b)
sound Q
sound (\<lambda>s. bound_of Q - Q s)
[PROOF STEP]
have "wp b (Q o \<phi>) s + wp b (?Qc o \<phi>) s \<le>
        wp b (\<lambda>s. (Q o \<phi>) s + (?Qc o \<phi>) s) s"
[PROOF STATE]
proof (prove)
using this:
sub_add (wp b)
sound Q
sound (\<lambda>s. bound_of Q - Q s)

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

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp b (Q \<circ> \<phi>) s + wp b ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s \<le> wp b (\<lambda>s. (Q \<circ> \<phi>) s + ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
have "... = wp b (\<lambda>s. bound_of Q) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp b (\<lambda>s. (Q \<circ> \<phi>) s + ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s) s = wp b (\<lambda>s. bound_of Q) s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp b (\<lambda>s. (Q \<circ> \<phi>) s + ((\<lambda>s. bound_of Q - Q s) \<circ> \<phi>) s) s = wp b (\<lambda>s. bound_of Q) s

goal (1 subgoal):
 1. \<And>Q. \<lbrakk>unitary Q; \<guillemotleft> G \<guillemotright> && (wp a Q \<circ> \<phi>) \<noteq> \<guillemotleft> G \<guillemotright> && wp b (Q \<circ> \<phi>)\<rbrakk> \<Longrightarrow> \<not> feasible (wp b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bound_of Q < wp b (\<lambda>s. bound_of Q) s
[PROOF STEP]
show "\<not> feasible (wp b)"
[PROOF STATE]
proof (prove)
using this:
bound_of Q < wp b (\<lambda>s. bound_of Q) s

goal (1 subgoal):
 1. \<not> feasible (wp b)
[PROOF STEP]
proof(rule contrapos_pn)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. feasible (wp b) \<Longrightarrow> \<not> bound_of Q < wp b (\<lambda>s. bound_of Q) s
[PROOF STEP]
assume fb: "feasible (wp b)"
[PROOF STATE]
proof (state)
this:
feasible (wp b)

goal (1 subgoal):
 1. feasible (wp b) \<Longrightarrow> \<not> bound_of Q < wp b (\<lambda>s. bound_of Q) s
[PROOF STEP]
have "bounded_by (bound_of Q) (\<lambda>s. bound_of Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by (bound_of Q) (\<lambda>s. bound_of Q)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of Q) (\<lambda>s. bound_of Q)

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

goal (1 subgoal):
 1. bounded_by (bound_of Q) (wp b (\<lambda>s. bound_of Q))
[PROOF STEP]
using uQ
[PROOF STATE]
proof (prove)
using this:
bounded_by (bound_of Q) (\<lambda>s. bound_of Q)
unitary Q

goal (1 subgoal):
 1. bounded_by (bound_of Q) (wp b (\<lambda>s. bound_of Q))
[PROOF STEP]
by(blast intro:feasible_boundedD[OF fb])
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of Q) (wp b (\<lambda>s. bound_of Q))

goal (1 subgoal):
 1. feasible (wp b) \<Longrightarrow> \<not> bound_of Q < wp b (\<lambda>s. bound_of Q) s
[PROOF STEP]
hence "wp b (\<lambda>s. bound_of Q) s \<le> bound_of Q"
[PROOF STATE]
proof (prove)
using this:
bounded_by (bound_of Q) (wp b (\<lambda>s. bound_of Q))

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

goal (1 subgoal):
 1. feasible (wp b) \<Longrightarrow> \<not> bound_of Q < wp b (\<lambda>s. bound_of Q) s
[PROOF STEP]
thus "\<not> bound_of Q < wp b (\<lambda>s. bound_of Q) s"
[PROOF STATE]
proof (prove)
using this:
wp b (\<lambda>s. bound_of Q) s \<le> bound_of Q

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> feasible (wp b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pcorres_Skip:
  "pcorres \<phi> G Skip Skip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcorres \<phi> G Skip Skip
[PROOF STEP]
by(simp add:pcorres_def wp_eval)


[STATEMENT]
lemma pcorres_Seq:
  fixes A::"'b prog" and B::"'c prog"
    and C::"'b prog" and D::"'c prog"
    and \<phi>::"'c \<Rightarrow> 'b"
  assumes pcAB: "pcorres \<phi> G A B"
      and pcCD: "pcorres \<phi> H C D"
      and wA: "well_def A" and wB: "well_def B"
      and wC: "well_def C" and wD: "well_def D"
      and p3p2: "\<And>Q. unitary Q \<Longrightarrow> \<guillemotleft>I\<guillemotright> && wp B Q = wp B (\<guillemotleft>H\<guillemotright> && Q)"
      and p1p3: "\<And>s. G s \<Longrightarrow> I s"
  shows "pcorres \<phi> G (A;;C) (B;;D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcorres \<phi> G (A ;; C) (B ;; D)
[PROOF STEP]
proof(rule pcorresI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. unitary Q \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp (A ;; C) Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
fix Q::"'b \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q. unitary Q \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp (A ;; C) Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
assume uQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (1 subgoal):
 1. \<And>Q. unitary Q \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp (A ;; C) Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
with well_def_wp_healthy[OF wC]
[PROOF STATE]
proof (chain)
picking this:
healthy (wp C)
unitary Q
[PROOF STEP]
have uCQ: "unitary (wp C Q)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp C)
unitary Q

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

goal (1 subgoal):
 1. \<And>Q. unitary Q \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp (A ;; C) Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
from uQ well_def_wp_healthy[OF wD]
[PROOF STATE]
proof (chain)
picking this:
unitary Q
healthy (wp D)
[PROOF STEP]
have uDQ: "unitary (wp D (Q o \<phi>))"
[PROOF STATE]
proof (prove)
using this:
unitary Q
healthy (wp D)

goal (1 subgoal):
 1. unitary (wp D (Q \<circ> \<phi>))
[PROOF STEP]
by(auto dest:unitary_comp)
[PROOF STATE]
proof (state)
this:
unitary (wp D (Q \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Q. unitary Q \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp (A ;; C) Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
have p3p1: "\<And>R S. \<lbrakk> unitary R; unitary S; \<guillemotleft>I\<guillemotright> && R = \<guillemotleft>I\<guillemotright> && S \<rbrakk> \<Longrightarrow>
                    \<guillemotleft>G\<guillemotright> && R = \<guillemotleft>G\<guillemotright> && S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>R S. \<lbrakk>unitary R; unitary S; \<guillemotleft> I \<guillemotright> && R = \<guillemotleft> I \<guillemotright> && S\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && R = \<guillemotleft> G \<guillemotright> && S
[PROOF STEP]
proof(rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S x. \<lbrakk>unitary R; unitary S; \<guillemotleft> I \<guillemotright> && R = \<guillemotleft> I \<guillemotright> && S\<rbrakk> \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && R) x = (\<guillemotleft> G \<guillemotright> && S) x
[PROOF STEP]
fix R::"'c \<Rightarrow> real" and S::"'c \<Rightarrow> real" and s::'c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S x. \<lbrakk>unitary R; unitary S; \<guillemotleft> I \<guillemotright> && R = \<guillemotleft> I \<guillemotright> && S\<rbrakk> \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && R) x = (\<guillemotleft> G \<guillemotright> && S) x
[PROOF STEP]
assume a3: "\<guillemotleft>I\<guillemotright> && R = \<guillemotleft>I\<guillemotright> && S"
       and uR: "unitary R" and uS: "unitary S"
[PROOF STATE]
proof (state)
this:
\<guillemotleft> I \<guillemotright> && R = \<guillemotleft> I \<guillemotright> && S
unitary R
unitary S

goal (1 subgoal):
 1. \<And>R S x. \<lbrakk>unitary R; unitary S; \<guillemotleft> I \<guillemotright> && R = \<guillemotleft> I \<guillemotright> && S\<rbrakk> \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && R) x = (\<guillemotleft> G \<guillemotright> && S) x
[PROOF STEP]
show "(\<guillemotleft>G\<guillemotright> && R) s = (\<guillemotleft>G\<guillemotright> && S) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && R) s = (\<guillemotleft> G \<guillemotright> && S) s
[PROOF STEP]
proof(simp add:exp_conj_def, cases "G s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
 2. \<not> G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (2 subgoals):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
 2. \<not> G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
note this
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (2 subgoals):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
 2. \<not> G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> G s

goal (2 subgoals):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
 2. \<not> G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
from uR
[PROOF STATE]
proof (chain)
picking this:
unitary R
[PROOF STEP]
have "R s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary R

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

goal (2 subgoals):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
 2. \<not> G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R s \<le> 1

goal (2 subgoals):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
 2. \<not> G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
from uS
[PROOF STATE]
proof (chain)
picking this:
unitary S
[PROOF STEP]
have "S s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary S

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

goal (2 subgoals):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
 2. \<not> G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> G s
R s \<le> 1
S s \<le> 1
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> s .& R s = \<guillemotleft>G\<guillemotright> s .& S s"
[PROOF STATE]
proof (prove)
using this:
\<not> G s
R s \<le> 1
S s \<le> 1

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

goal (1 subgoal):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
G s

goal (1 subgoal):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
note p1 = this
[PROOF STATE]
proof (state)
this:
G s

goal (1 subgoal):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
with p1p3
[PROOF STATE]
proof (chain)
picking this:
G ?s \<Longrightarrow> I ?s
G s
[PROOF STEP]
have "I s"
[PROOF STATE]
proof (prove)
using this:
G ?s \<Longrightarrow> I ?s
G s

goal (1 subgoal):
 1. I s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
I s

goal (1 subgoal):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
with fun_cong[OF a3, where x=s]
[PROOF STATE]
proof (chain)
picking this:
(\<guillemotleft> I \<guillemotright> && R) s = (\<guillemotleft> I \<guillemotright> && S) s
I s
[PROOF STEP]
have "1 .& R s = 1 .& S s"
[PROOF STATE]
proof (prove)
using this:
(\<guillemotleft> I \<guillemotright> && R) s = (\<guillemotleft> I \<guillemotright> && S) s
I s

goal (1 subgoal):
 1. 1 .& R s = 1 .& S s
[PROOF STEP]
by(simp add:exp_conj_def)
[PROOF STATE]
proof (state)
this:
1 .& R s = 1 .& S s

goal (1 subgoal):
 1. G s \<Longrightarrow> \<guillemotleft> G \<guillemotright> s .& R s = \<guillemotleft> G \<guillemotright> s .& S s
[PROOF STEP]
with p1
[PROOF STATE]
proof (chain)
picking this:
G s
1 .& R s = 1 .& S s
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> s .& R s = \<guillemotleft>G\<guillemotright> s .& S s"
[PROOF STATE]
proof (prove)
using this:
G s
1 .& R s = 1 .& S s

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>unitary ?R; unitary ?S; \<guillemotleft> I \<guillemotright> && ?R = \<guillemotleft> I \<guillemotright> && ?S\<rbrakk> \<Longrightarrow> \<guillemotleft> G \<guillemotright> && ?R = \<guillemotleft> G \<guillemotright> && ?S

goal (1 subgoal):
 1. \<And>Q. unitary Q \<Longrightarrow> \<guillemotleft> G \<guillemotright> && (wp (A ;; C) Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> && (wp (A;;C) Q o \<phi>) = \<guillemotleft>G\<guillemotright> && wp (B;;D) (Q o \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp (A ;; C) Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
proof(simp add:wp_eval)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp A (wp C Q) \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
from uCQ pcAB
[PROOF STATE]
proof (chain)
picking this:
unitary (wp C Q)
pcorres \<phi> G A B
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> && (wp A (wp C Q) \<circ> \<phi>) =
                        \<guillemotleft>G\<guillemotright> && wp B ((wp C Q) \<circ> \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary (wp C Q)
pcorres \<phi> G A B

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

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

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp A (wp C Q) \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
have "\<guillemotleft>G\<guillemotright> && wp B ((wp C Q) \<circ> \<phi>) =
               \<guillemotleft>G\<guillemotright> && wp B (wp D (Q \<circ> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
proof(rule p3p1)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. unitary (wp B (wp C Q \<circ> \<phi>))
 2. unitary (wp B (wp D (Q \<circ> \<phi>)))
 3. \<guillemotleft> I \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> I \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
from uCQ well_def_wp_healthy[OF wB]
[PROOF STATE]
proof (chain)
picking this:
unitary (wp C Q)
healthy (wp B)
[PROOF STEP]
show "unitary (wp B (wp C Q \<circ> \<phi>))"
[PROOF STATE]
proof (prove)
using this:
unitary (wp C Q)
healthy (wp B)

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

goal (2 subgoals):
 1. unitary (wp B (wp D (Q \<circ> \<phi>)))
 2. \<guillemotleft> I \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> I \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
from uDQ well_def_wp_healthy[OF wB]
[PROOF STATE]
proof (chain)
picking this:
unitary (wp D (Q \<circ> \<phi>))
healthy (wp B)
[PROOF STEP]
show "unitary (wp B (wp D (Q \<circ> \<phi>)))"
[PROOF STATE]
proof (prove)
using this:
unitary (wp D (Q \<circ> \<phi>))
healthy (wp B)

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

goal (1 subgoal):
 1. \<guillemotleft> I \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> I \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
from uQ
[PROOF STATE]
proof (chain)
picking this:
unitary Q
[PROOF STEP]
have "\<guillemotleft> H \<guillemotright> && (wp C Q \<circ> \<phi>) = \<guillemotleft> H \<guillemotright> && wp D (Q \<circ> \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary Q

goal (1 subgoal):
 1. \<guillemotleft> H \<guillemotright> && (wp C Q \<circ> \<phi>) = \<guillemotleft> H \<guillemotright> && wp D (Q \<circ> \<phi>)
[PROOF STEP]
by(blast intro:pcorresD[OF pcCD])
[PROOF STATE]
proof (state)
this:
\<guillemotleft> H \<guillemotright> && (wp C Q \<circ> \<phi>) = \<guillemotleft> H \<guillemotright> && wp D (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> I \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> I \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
thus "\<guillemotleft> I \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> I \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> H \<guillemotright> && (wp C Q \<circ> \<phi>) = \<guillemotleft> H \<guillemotright> && wp D (Q \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> I \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> I \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
by(simp add:p3p2 uCQ uDQ)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> I \<guillemotright> && wp B (wp C Q \<circ> \<phi>) = \<guillemotleft> I \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))

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

goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> && (wp A (wp C Q) \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> G \<guillemotright> && (wp A (wp C Q) \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))
[PROOF STEP]
show "\<guillemotleft>G\<guillemotright> && (wp A (wp C Q) \<circ> \<phi>) = \<guillemotleft>G\<guillemotright> && wp B (wp D (Q \<circ> \<phi>))"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> && (wp A (wp C Q) \<circ> \<phi>) = \<guillemotleft> G \<guillemotright> && wp B (wp D (Q \<circ> \<phi>))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_Skip:
  fixes \<phi>::"'c \<Rightarrow> 'b"
  shows "drefines \<phi> G Skip Skip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G Skip Skip
[PROOF STEP]
proof(intro drefinesI2 wd_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp Skip Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp Skip (Q \<circ> \<phi>) s
[PROOF STEP]
fix P::"'b \<Rightarrow> real" and Q::"'b \<Rightarrow> real" and s::'c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp Skip Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp Skip (Q \<circ> \<phi>) s
[PROOF STEP]
assume "P \<tturnstile> wp Skip Q"
[PROOF STATE]
proof (state)
this:
P \<tturnstile> wp Skip Q

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_Abort:
  fixes \<phi>::"'c \<Rightarrow> 'b"
  shows "drefines \<phi> G Abort Abort"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G Abort Abort
[PROOF STEP]
proof(intro drefinesI2 wd_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp Abort Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp Abort (Q \<circ> \<phi>) s
[PROOF STEP]
fix P::"'b \<Rightarrow> real" and Q::"'b \<Rightarrow> real" and s::'c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp Abort Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp Abort (Q \<circ> \<phi>) s
[PROOF STEP]
assume "P \<tturnstile> wp Abort Q"
[PROOF STATE]
proof (state)
this:
P \<tturnstile> wp Abort Q

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_Apply:
  fixes \<phi>::"'c \<Rightarrow> 'b"
  assumes commutes: "f o \<phi> = \<phi> o g"
  shows "drefines \<phi> G (Apply f) (Apply g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G (Apply f) (Apply g)
[PROOF STEP]
proof(intro drefinesI2 wd_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp (Apply f) Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp (Apply g) (Q \<circ> \<phi>) s
[PROOF STEP]
fix P::"'b \<Rightarrow> real" and Q::"'b \<Rightarrow> real" and s::'c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q s. \<lbrakk>unitary P; unitary Q; G s; P \<tturnstile> wp (Apply f) Q\<rbrakk> \<Longrightarrow> (P \<circ> \<phi>) s \<le> wp (Apply g) (Q \<circ> \<phi>) s
[PROOF STEP]
assume wp: "P \<tturnstile> wp (Apply f) Q"
[PROOF STATE]
proof (state)
this:
P \<tturnstile> wp (Apply f) Q

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

goal (1 subgoal):
 1. P \<tturnstile> Q \<circ> f
[PROOF STEP]
by(simp add:wp_eval)
[PROOF STATE]
proof (state)
this:
P \<tturnstile> Q \<circ> f

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed