[STATEMENT]
lemma pcorresI2[intro]:
  fixes A::"'a prog" and B::"'b prog"
  assumes withG: "\<And>Q s. \<lbrakk> unitary Q; G s \<rbrakk> \<Longrightarrow> wp A Q (\<phi> s)= wp B (Q o \<phi>) s"
      and wA: "well_def A"
      and wB: "well_def B"
  shows "pcorres \<phi> G A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcorres \<phi> G A B
[PROOF STEP]
proof(rule pcorresI, rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[PROOF STEP]
fix Q::"'a \<Rightarrow> real" and s::'b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[PROOF STEP]
assume uQ: "unitary Q"
[PROOF STATE]
proof (state)
this:
unitary Q

goal (1 subgoal):
 1. \<And>Q x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[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 x. unitary Q \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) x = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) x
[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)
goal (1 subgoal):
 1. (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
proof(cases "G s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
G s

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

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<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:
G s

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<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 well_def_wp_healthy[OF wA] 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. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<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:
0 \<le> wp A Q (\<phi> s)

goal (2 subgoals):
 1. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<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 well_def_wp_healthy[OF wB] 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. G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
 2. \<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:
G s
0 \<le> wp A Q (\<phi> s)
0 \<le> 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

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

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 withG)
[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. \<not> G s \<Longrightarrow> (\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s
[PROOF STEP]
next
[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]
case False
[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]
note this
[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 well_def_wp_healthy[OF wA] 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]
from well_def_wp_healthy[OF wB] uQ\<phi>
[PROOF STATE]
proof (chain)
picking this:
healthy (wp B)
unitary (Q \<circ> \<phi>)
[PROOF STEP]
have "wp B (Q o \<phi>) s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
healthy (wp B)
unitary (Q \<circ> \<phi>)

goal (1 subgoal):
 1. wp B (Q \<circ> \<phi>) s \<le> 1
[PROOF STEP]
by(blast dest!:healthy_bounded_byD intro:sound_nneg)
[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 ?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

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:
(\<guillemotleft> G \<guillemotright> && (wp A Q \<circ> \<phi>)) s = (\<guillemotleft> G \<guillemotright> && wp B (Q \<circ> \<phi>)) s

goal:
No subgoals!
[PROOF STEP]
qed