[STATEMENT]
lemma healthy_wp_loop:
  fixes body::"'s prog"
  assumes hb: "healthy (wp body)"
  shows "healthy (wp (do G \<longrightarrow> body od))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. healthy (wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
let "?X P" = "(\<lambda>Q s. \<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. healthy (wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. healthy (wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))
[PROOF STEP]
proof(intro healthy_parts bounded_byI2 nnegI2, simp_all add:wp_Loop1 hb soundI2 sound_intros)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) x = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * (c * P s)) x
[PROOF STEP]
fix P::"'s expect" and c::real and s::'s
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) x = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * (c * P s)) x
[PROOF STEP]
assume sP: "sound P" and nnc: "0 \<le> c"
[PROOF STATE]
proof (state)
this:
sound P
0 \<le> c

goal (4 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
 4. \<And>P c x. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> c * lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) x = lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * (c * P s)) x
[PROOF STEP]
show "c * (lfp_exp (?X P)) s = lfp_exp (?X (\<lambda>s. c * P s)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
 2. \<not> ?P \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
assume "c = 0"
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
 2. \<not> ?P \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
proof(simp, intro antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s \<le> 0
 2. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> 0 \<le> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s
[PROOF STEP]
from hb
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
[PROOF STEP]
have fp: "\<lambda>s. \<guillemotleft>G\<guillemotright> s * wp body (\<lambda>_. 0) s \<tturnstile> \<lambda>s. 0"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)

goal (1 subgoal):
 1. \<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>_. 0) s \<tturnstile> \<lambda>s. 0
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>_. 0) s \<tturnstile> \<lambda>s. 0

goal (2 subgoals):
 1. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s \<le> 0
 2. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> 0 \<le> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s
[PROOF STEP]
hence "lfp_exp (\<lambda>P s. \<guillemotleft>G\<guillemotright> s * wp body P s) \<tturnstile> \<lambda>s. 0"
[PROOF STATE]
proof (prove)
using this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>_. 0) s \<tturnstile> \<lambda>s. 0

goal (1 subgoal):
 1. lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s) \<tturnstile> \<lambda>s. 0
[PROOF STEP]
by(auto intro:lfp_exp_lowerbound)
[PROOF STATE]
proof (state)
this:
lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s) \<tturnstile> \<lambda>s. 0

goal (2 subgoals):
 1. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s \<le> 0
 2. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> 0 \<le> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s
[PROOF STEP]
thus "lfp_exp (\<lambda>P s. \<guillemotleft>G\<guillemotright> s * wp body P s) s \<le> 0"
[PROOF STATE]
proof (prove)
using this:
lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s) \<tturnstile> \<lambda>s. 0

goal (1 subgoal):
 1. lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s) s \<le> 0
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s) s \<le> 0

goal (1 subgoal):
 1. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> 0 \<le> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s
[PROOF STEP]
have "\<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>P s. \<guillemotleft>G\<guillemotright> s * wp body P s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s)
[PROOF STEP]
by(auto intro:lfp_exp_greatest fp)
[PROOF STATE]
proof (state)
this:
\<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s)

goal (1 subgoal):
 1. \<lbrakk>c = 0; c = 0\<rbrakk> \<Longrightarrow> 0 \<le> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b) s
[PROOF STEP]
thus "0 \<le> lfp_exp (\<lambda>P s. \<guillemotleft>G\<guillemotright> s * wp body P s) s"
[PROOF STATE]
proof (prove)
using this:
\<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s)

goal (1 subgoal):
 1. 0 \<le> lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s) s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> lfp_exp (\<lambda>P s. \<guillemotleft> G \<guillemotright> s * wp body P s) s

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

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
have onesided: "\<And>P c. c \<noteq> 0 \<Longrightarrow> 0 \<le> c \<Longrightarrow> sound P \<Longrightarrow>
            \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * P b) a \<tturnstile>
                    lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * (c * P b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P c. \<lbrakk>c \<noteq> 0; 0 \<le> c; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c. \<lbrakk>c \<noteq> 0; 0 \<le> c; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
fix P::"'s expect" and c::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P c. \<lbrakk>c \<noteq> 0; 0 \<le> c; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
assume cnz: "c \<noteq> 0" and nnc: "0 \<le> c" and sP: "sound P"
[PROOF STATE]
proof (state)
this:
c \<noteq> 0
0 \<le> c
sound P

goal (1 subgoal):
 1. \<And>P c. \<lbrakk>c \<noteq> 0; 0 \<le> c; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
with nnc
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
c \<noteq> 0
0 \<le> c
sound P
[PROOF STEP]
have cpos: "0 < c"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
c \<noteq> 0
0 \<le> c
sound P

goal (1 subgoal):
 1. 0 < c
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. \<And>P c. \<lbrakk>c \<noteq> 0; 0 \<le> c; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
hence nnic: "0 \<le> inverse c"
[PROOF STATE]
proof (prove)
using this:
0 < c

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

goal (1 subgoal):
 1. \<And>P c. \<lbrakk>c \<noteq> 0; 0 \<le> c; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
show "\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * P b) a \<tturnstile>
              lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * (c * P b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
proof(rule lfp_exp_greatest)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
fix Q::"'s expect"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
assume sQ: "sound Q"
             and fp: "\<lambda>b. \<guillemotleft>G\<guillemotright> b * wp body Q b + \<guillemotleft>\<N> G\<guillemotright> b * (c * P b) \<tturnstile> Q"
[PROOF STATE]
proof (state)
this:
sound Q
\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body Q b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> Q

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
hence "\<And>s. \<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * (c * P s) \<le> Q s"
[PROOF STATE]
proof (prove)
using this:
sound Q
\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body Q b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> Q

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

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
with nnic
[PROOF STATE]
proof (chain)
picking this:
0 \<le> inverse c
\<guillemotleft> G \<guillemotright> ?s * wp body Q ?s + \<guillemotleft> \<N> G \<guillemotright> ?s * (c * P ?s) \<le> Q ?s
[PROOF STEP]
have "\<And>s. inverse c * (\<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * (c * P s)) \<le>
                     inverse c * Q s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> inverse c
\<guillemotleft> G \<guillemotright> ?s * wp body Q ?s + \<guillemotleft> \<N> G \<guillemotright> ?s * (c * P ?s) \<le> Q ?s

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

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
hence "\<And>s. \<guillemotleft>G\<guillemotright> s * (inverse c * wp body Q s) + (inverse c * c) * \<guillemotleft>\<N> G\<guillemotright> s * P s \<le>
                     inverse c * Q s"
[PROOF STATE]
proof (prove)
using this:
inverse c * (\<guillemotleft> G \<guillemotright> ?s * wp body Q ?s + \<guillemotleft> \<N> G \<guillemotright> ?s * (c * P ?s)) \<le> inverse c * Q ?s

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

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
hence "\<And>s. \<guillemotleft>G\<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft>\<N> G\<guillemotright> s * P s \<le>
                     inverse c * Q s"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> ?s * (inverse c * wp body Q ?s) + inverse c * c * \<guillemotleft> \<N> G \<guillemotright> ?s * P ?s \<le> inverse c * Q ?s

goal (1 subgoal):
 1. \<And>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<le> inverse c * Q s
[PROOF STEP]
by(simp add:cnz scalingD[OF healthy_scalingD, OF hb sQ nnic])
[PROOF STATE]
proof (state)
this:
\<guillemotleft> G \<guillemotright> ?s * wp body (\<lambda>s. inverse c * Q s) ?s + \<guillemotleft> \<N> G \<guillemotright> ?s * P ?s \<le> inverse c * Q ?s

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
hence "\<lambda>s. \<guillemotleft>G\<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft>\<N> G\<guillemotright> s * P s \<tturnstile>
                 \<lambda>s. inverse c * Q s"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> G \<guillemotright> ?s * wp body (\<lambda>s. inverse c * Q s) ?s + \<guillemotleft> \<N> G \<guillemotright> ?s * P ?s \<le> inverse c * Q ?s

goal (1 subgoal):
 1. \<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<tturnstile> \<lambda>s. inverse c * Q s
[PROOF STEP]
by(rule le_funI)
[PROOF STATE]
proof (state)
this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<tturnstile> \<lambda>s. inverse c * Q s

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<tturnstile> \<lambda>s. inverse c * Q s

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
from nnic sQ
[PROOF STATE]
proof (chain)
picking this:
0 \<le> inverse c
sound Q
[PROOF STEP]
have "sound (\<lambda>s. inverse c * Q s)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> inverse c
sound Q

goal (1 subgoal):
 1. sound (\<lambda>s. inverse c * Q s)
[PROOF STEP]
by(iprover intro:sound_intros)
[PROOF STATE]
proof (state)
this:
sound (\<lambda>s. inverse c * Q s)

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<tturnstile> \<lambda>s. inverse c * Q s
sound (\<lambda>s. inverse c * Q s)
[PROOF STEP]
have "lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * P b) \<tturnstile>
                           \<lambda>s. inverse c * Q s"
[PROOF STATE]
proof (prove)
using this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. inverse c * Q s) s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<tturnstile> \<lambda>s. inverse c * Q s
sound (\<lambda>s. inverse c * Q s)

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> \<lambda>s. inverse c * Q s
[PROOF STEP]
by(rule lfp_exp_lowerbound)
[PROOF STATE]
proof (state)
this:
lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> \<lambda>s. inverse c * Q s

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
hence "\<And>s. lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * P b) s \<le> inverse c * Q s"
[PROOF STATE]
proof (prove)
using this:
lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> \<lambda>s. inverse c * Q s

goal (1 subgoal):
 1. \<And>s. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s \<le> inverse c * Q s
[PROOF STEP]
by(rule le_funD)
[PROOF STATE]
proof (state)
this:
lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) ?s \<le> inverse c * Q ?s

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
with nnc
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) ?s \<le> inverse c * Q ?s
[PROOF STEP]
have "\<And>s. c * lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * P b) s \<le>
                     c * (inverse c * Q s)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) ?s \<le> inverse c * Q ?s

goal (1 subgoal):
 1. \<And>s. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s \<le> c * (inverse c * Q s)
[PROOF STEP]
by(auto intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) ?s \<le> c * (inverse c * Q ?s)

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) ?s \<le> c * (inverse c * Q ?s)

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
from cnz
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
[PROOF STEP]
have "\<And>s. ... s = Q s"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. \<And>s. c * (inverse c * Q s) = Q s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
c * (inverse c * Q ?s) = Q ?s

goal (4 subgoals):
 1. \<And>P. \<lbrakk>\<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body P b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> P; sound P\<rbrakk> \<Longrightarrow> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> P
 2. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 3. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) ?s1 \<le> Q ?s1
[PROOF STEP]
show "\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft>G\<guillemotright> b * wp body a b + \<guillemotleft>\<N> G\<guillemotright> b * P b) a \<tturnstile> Q"
[PROOF STATE]
proof (prove)
using this:
c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) ?s1 \<le> Q ?s1

goal (1 subgoal):
 1. \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> Q
[PROOF STEP]
by(rule le_funI)
[PROOF STATE]
proof (state)
this:
\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> Q

goal (3 subgoals):
 1. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 2. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 3. sound ?R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 2. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 3. sound ?R
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "sound (\<lambda>s. bound_of P)"
[PROOF STATE]
proof (prove)
using this:
sound P

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

goal (3 subgoals):
 1. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 2. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 3. sound ?R
[PROOF STEP]
with hb sP
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
sound P
sound (\<lambda>s. bound_of P)
[PROOF STEP]
have "sound (lfp_exp (?X P))"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
sound P
sound (\<lambda>s. bound_of P)

goal (1 subgoal):
 1. sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))
[PROOF STEP]
by(blast intro:lfp_exp_sound lfp_loop_fp)
[PROOF STATE]
proof (state)
this:
sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))

goal (3 subgoals):
 1. sound (\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a)
 2. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 3. sound ?R
[PROOF STEP]
with nnc
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))
[PROOF STEP]
show "sound (\<lambda>s. c * lfp_exp (?X P) s)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))

goal (1 subgoal):
 1. sound (\<lambda>s. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s)
[PROOF STEP]
by(auto intro!:sound_intros)
[PROOF STATE]
proof (state)
this:
sound (\<lambda>s. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s)

goal (2 subgoals):
 1. \<lambda>b. \<guillemotleft> G \<guillemotright> b * wp body ?R b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b) \<tturnstile> ?R
 2. sound ?R
[PROOF STEP]
from hb sP nnc
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
sound P
0 \<le> c
[PROOF STEP]
show "\<lambda>s. \<guillemotleft>G\<guillemotright> s * wp body (\<lambda>s. bound_of (\<lambda>s. c * P s)) s +
                    \<guillemotleft>\<N> G\<guillemotright> s * (c * P s) \<tturnstile> \<lambda>s. bound_of (\<lambda>s. c * P s)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
sound P
0 \<le> c

goal (1 subgoal):
 1. \<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. bound_of (\<lambda>s. c * P s)) s + \<guillemotleft> \<N> G \<guillemotright> s * (c * P s) \<tturnstile> \<lambda>s. bound_of (\<lambda>s. c * P s)
[PROOF STEP]
by(iprover intro:lfp_loop_fp sound_intros)
[PROOF STATE]
proof (state)
this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. bound_of (\<lambda>s. c * P s)) s + \<guillemotleft> \<N> G \<guillemotright> s * (c * P s) \<tturnstile> \<lambda>s. bound_of (\<lambda>s. c * P s)

goal (1 subgoal):
 1. sound (\<lambda>s. bound_of (\<lambda>s. c * P s))
[PROOF STEP]
from sP nnc
[PROOF STATE]
proof (chain)
picking this:
sound P
0 \<le> c
[PROOF STEP]
show "sound (\<lambda>s. bound_of (\<lambda>s. c * P s))"
[PROOF STATE]
proof (prove)
using this:
sound P
0 \<le> c

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<noteq> 0; 0 \<le> ?c; sound ?P\<rbrakk> \<Longrightarrow> \<lambda>a. ?c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * ?P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (?c * ?P b))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
assume nzc: "c \<noteq> 0"
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
show ?thesis (is "?X P c s = ?Y P c s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) s = lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s
[PROOF STEP]
proof(rule fun_cong[where x=s], rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
 2. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
from nzc nnc sP
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
0 \<le> c
sound P
[PROOF STEP]
show "?X P c \<tturnstile> ?Y P c"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
0 \<le> c
sound P

goal (1 subgoal):
 1. \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))
[PROOF STEP]
by(rule onesided)
[PROOF STATE]
proof (state)
this:
\<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b))

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
from nzc
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
[PROOF STEP]
have nzic: "inverse c \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. inverse c \<noteq> 0
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
inverse c \<noteq> 0

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inverse c \<noteq> 0

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
with nnc
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
inverse c \<noteq> 0
[PROOF STEP]
have nnic: "0 \<le> inverse c"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
inverse c \<noteq> 0

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

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> inverse c

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
from nnc sP
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
sound P
[PROOF STEP]
have scP: "sound (\<lambda>s. c * P s)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
sound P

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

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inverse c \<noteq> 0
0 \<le> inverse c
sound (\<lambda>s. c * P s)
[PROOF STEP]
have "?X (\<lambda>s. c * P s) (inverse c) \<tturnstile> ?Y (\<lambda>s. c * P s) (inverse c)"
[PROOF STATE]
proof (prove)
using this:
inverse c \<noteq> 0
0 \<le> inverse c
sound (\<lambda>s. c * P s)

goal (1 subgoal):
 1. \<lambda>a. inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b)))
[PROOF STEP]
by(rule onesided)
[PROOF STATE]
proof (state)
this:
\<lambda>a. inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b)))

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
with nnc
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
\<lambda>a. inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b)))
[PROOF STEP]
have "\<lambda>s. c * ?X (\<lambda>s. c * P s) (inverse c) s \<tturnstile>
                       \<lambda>s. c * ?Y (\<lambda>s. c * P s) (inverse c) s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
\<lambda>a. inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) a \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b)))

goal (1 subgoal):
 1. \<lambda>s. c * (inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s) \<tturnstile> \<lambda>s. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b))) s
[PROOF STEP]
by(blast intro:mult_left_mono)
[PROOF STATE]
proof (state)
this:
\<lambda>s. c * (inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s) \<tturnstile> \<lambda>s. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b))) s

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
with nzc
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
\<lambda>s. c * (inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s) \<tturnstile> \<lambda>s. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b))) s
[PROOF STEP]
show "?Y P c \<tturnstile> ?X P c"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
\<lambda>s. c * (inverse c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) s) \<tturnstile> \<lambda>s. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (inverse c * (c * P b))) s

goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a
[PROOF STEP]
by(simp add:mult.assoc[symmetric])
[PROOF STATE]
proof (state)
this:
lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * (c * P b)) \<tturnstile> \<lambda>a. c * lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) a

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

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

goal (3 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
fix P::"'s expect" and b::real
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
assume bP: "bounded_by b P" and nP: "nneg P"
[PROOF STATE]
proof (state)
this:
bounded_by b P
nneg P

goal (3 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
 2. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 3. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
show "lfp_exp (\<lambda>Q s. \<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s) \<tturnstile> \<lambda>s. b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> \<lambda>s. b
[PROOF STEP]
proof(intro lfp_exp_lowerbound le_funI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. b) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> b
 2. sound (\<lambda>s. b)
[PROOF STEP]
fix s::'s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<guillemotleft> G \<guillemotright> x * wp body (\<lambda>s. b) x + \<guillemotleft> \<N> G \<guillemotright> x * P x \<le> b
 2. sound (\<lambda>s. b)
[PROOF STEP]
from bP nP hb
[PROOF STATE]
proof (chain)
picking this:
bounded_by b P
nneg P
healthy (wp body)
[PROOF STEP]
have "bounded_by b (wp body (\<lambda>s. b))"
[PROOF STATE]
proof (prove)
using this:
bounded_by b P
nneg P
healthy (wp body)

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. sound (\<lambda>s. b)
[PROOF STEP]
from bP nP
[PROOF STATE]
proof (chain)
picking this:
bounded_by b P
nneg P
[PROOF STEP]
have "0 \<le> b"
[PROOF STATE]
proof (prove)
using this:
bounded_by b P
nneg P

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

goal (1 subgoal):
 1. sound (\<lambda>s. b)
[PROOF STEP]
thus "sound (\<lambda>s. b)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b

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

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

goal (2 subgoals):
 1. \<And>b P. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
 2. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
from hb bP nP
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
bounded_by b P
nneg P
[PROOF STEP]
show "\<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft>G\<guillemotright> s * wp body Q s + \<guillemotleft>\<N> G\<guillemotright> s * P s)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
bounded_by b P
nneg P

goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)
[PROOF STEP]
by(auto dest!:sound_nneg intro!:lfp_loop_greatest)
[PROOF STATE]
proof (state)
this:
\<lambda>s. 0 \<tturnstile> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s)

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

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>sound P; sound Q; P \<tturnstile> Q\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>Q s. \<guillemotleft> G \<guillemotright> s * wp body Q s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> lfp_exp (\<lambda>Qa s. \<guillemotleft> G \<guillemotright> s * wp body Qa s + \<guillemotleft> \<N> G \<guillemotright> s * Q s)
[PROOF STEP]
show "lfp_exp (?X P) \<tturnstile> lfp_exp (?X Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * Q b)
[PROOF STEP]
proof(rule lfp_exp_greatest)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> Pa; sound Pa\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> Pa
 2. sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))
 3. \<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body ?R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
fix R::"'s expect"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> Pa; sound Pa\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> Pa
 2. sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))
 3. \<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body ?R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
assume sR: "sound R"
         and fp: "\<lambda>s. \<guillemotleft>G\<guillemotright> s * wp body R s + \<guillemotleft>\<N> G\<guillemotright> s * Q s \<tturnstile> R"
[PROOF STATE]
proof (state)
this:
sound R
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body R s + \<guillemotleft> \<N> G \<guillemotright> s * Q s \<tturnstile> R

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

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

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

goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>\<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body Pa a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> Pa; sound Pa\<rbrakk> \<Longrightarrow> lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b) \<tturnstile> Pa
 2. sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))
 3. \<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body ?R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> ?R
 4. sound ?R
[PROOF STEP]
note fp
[PROOF STATE]
proof (state)
this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body R s + \<guillemotleft> \<N> G \<guillemotright> s * Q s \<tturnstile> R

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

goal (1 subgoal):
 1. lfp_exp (\<lambda>R s. \<guillemotleft> G \<guillemotright> s * wp body R s + \<guillemotleft> \<N> G \<guillemotright> s * P s) \<tturnstile> R
[PROOF STEP]
using sR
[PROOF STATE]
proof (prove)
using this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body R s + \<guillemotleft> \<N> G \<guillemotright> s * P s \<tturnstile> R
sound R

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

goal (3 subgoals):
 1. sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))
 2. \<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body ?R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> ?R
 3. sound ?R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sound (lfp_exp (\<lambda>a b. \<guillemotleft> G \<guillemotright> b * wp body a b + \<guillemotleft> \<N> G \<guillemotright> b * P b))
 2. \<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body ?R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> ?R
 3. sound ?R
[PROOF STEP]
from hb sP
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
sound P
[PROOF STEP]
show "sound (lfp_exp (\<lambda>R s. \<guillemotleft>G\<guillemotright> s * wp body R s + \<guillemotleft>\<N> G\<guillemotright> s * P s))"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
sound P

goal (1 subgoal):
 1. sound (lfp_exp (\<lambda>R s. \<guillemotleft> G \<guillemotright> s * wp body R s + \<guillemotleft> \<N> G \<guillemotright> s * P s))
[PROOF STEP]
by(rule lfp_loop_sound)
[PROOF STATE]
proof (state)
this:
sound (lfp_exp (\<lambda>R s. \<guillemotleft> G \<guillemotright> s * wp body R s + \<guillemotleft> \<N> G \<guillemotright> s * P s))

goal (2 subgoals):
 1. \<lambda>a. \<guillemotleft> G \<guillemotright> a * wp body ?R a + \<guillemotleft> \<N> G \<guillemotright> a * Q a \<tturnstile> ?R
 2. sound ?R
[PROOF STEP]
from hb sQ
[PROOF STATE]
proof (chain)
picking this:
healthy (wp body)
sound Q
[PROOF STEP]
show "\<lambda>s. \<guillemotleft>G\<guillemotright> s * wp body (\<lambda>s. bound_of Q) s +  \<guillemotleft>\<N> G\<guillemotright> s * Q s \<tturnstile> \<lambda>s. bound_of Q"
[PROOF STATE]
proof (prove)
using this:
healthy (wp body)
sound Q

goal (1 subgoal):
 1. \<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. bound_of Q) s + \<guillemotleft> \<N> G \<guillemotright> s * Q s \<tturnstile> \<lambda>s. bound_of Q
[PROOF STEP]
by(rule lfp_loop_fp)
[PROOF STATE]
proof (state)
this:
\<lambda>s. \<guillemotleft> G \<guillemotright> s * wp body (\<lambda>s. bound_of Q) s + \<guillemotleft> \<N> G \<guillemotright> s * Q s \<tturnstile> \<lambda>s. bound_of Q

goal (1 subgoal):
 1. sound (\<lambda>s. bound_of Q)
[PROOF STEP]
from sQ
[PROOF STATE]
proof (chain)
picking this:
sound Q
[PROOF STEP]
show "sound (\<lambda>s. bound_of Q)"
[PROOF STATE]
proof (prove)
using this:
sound Q

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
healthy (wp (\<mu>x. body ;; x \<^bsub>\<guillemotleft> G \<guillemotright>\<^esub>\<oplus> Skip))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pure_fun_refine[sepref_fr_rules]: "hn_refine
    (hn_val (A\<rightarrow>B) f fi * hn_val A x xi)
    (return (pho_apply$fi$xi))
    (hn_val (A\<rightarrow>B) f fi * hn_val A x xi)
    (pure B)
    (RETURN$(pho_apply$f$x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_val (A \<rightarrow> B) f fi * hn_val A x xi) (return (pho_apply $ fi $ xi)) (hn_val (A \<rightarrow> B) f fi * hn_val A x xi) (pure B) (RETURN $ (pho_apply $ f $ x))
[PROOF STEP]
by (sep_auto intro!: hn_refineI simp: pure_def hn_ctxt_def dest: fun_relD)


[STATEMENT]
lemma key_gen_alt:
  "key_gen = map_spmf (\<lambda>x. (\<^bold>g [^] x, x)) (sample_uniform (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. key_gen = map_spmf (\<lambda>x. (\<^bold>g [^] x, x)) (sample_uniform (order \<G>))
[PROOF STEP]
by(simp add: map_spmf_conv_bind_spmf key_gen_def)


[STATEMENT]
lemma aencrypt_alt:
  "aencrypt \<alpha> msg = map_spmf (\<lambda>y. (\<^bold>g [^] y, (\<alpha> [^] y) \<otimes> msg)) (sample_uniform (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aencrypt \<alpha> msg = map_spmf (\<lambda>y. (\<^bold>g [^] y, \<alpha> [^] y \<otimes> msg)) (sample_uniform (order \<G>))
[PROOF STEP]
by(simp add: map_spmf_conv_bind_spmf aencrypt_def)


[STATEMENT]
theorem advantage_elgamal: "ind_cpa.advantage \ = ddh.advantage (elgamal_adversary \)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
obtain \1 and \2 where "\ = (\1, \2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\1 \2. \ = (\1, \2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases \)
[PROOF STATE]
proof (state)
this:
\ = (\1, \2)

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
note [simp] = this order_gt_0_iff_finite finite_carrier try_spmf_bind_out split_def o_def spmf_of_set bind_map_spmf weight_spmf_le_1 scale_bind_spmf bind_spmf_const
    and [cong] = bind_spmf_cong_simp
[PROOF STATE]
proof (state)
this:
\ = (\1, \2)
(0 < order \<G>) = finite (carrier \<G>)
finite (carrier \<G>)
lossless_spmf ?p \<Longrightarrow> ?p \<bind> (\<lambda>x. TRY ?f x ELSE ?q) = TRY ?p \<bind> ?f ELSE ?q
case_prod = (\<lambda>c p. c (fst p) (snd p))
?f \<circ> ?g = (\<lambda>x. ?f (?g x))
spmf (spmf_of_set ?A) ?x = indicat_real ?A ?x / real (card ?A)
map_spmf ?f ?p \<bind> ?g = ?p \<bind> ?g \<circ> ?f
weight_spmf ?p \<le> 1
?r \<le> 1 \<Longrightarrow> scale_spmf ?r (?p \<bind> ?f) = ?p \<bind> (\<lambda>x. scale_spmf ?r (?f x))
?p \<bind> (\<lambda>x. ?q) = scale_spmf (weight_spmf ?p) ?q
\<lbrakk>?p = ?q; \<And>x. x \<in> set_spmf ?q =simp=> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?p \<bind> ?f = ?q \<bind> ?g

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
have "ddh.ddh_1 (elgamal_adversary \) = TRY do {
       x \<leftarrow> sample_uniform (order \<G>);
       y \<leftarrow> sample_uniform (order \<G>);
       ((msg1, msg2), \<sigma>) \<leftarrow> \1 (\<^bold>g [^] x);
       _ :: unit \<leftarrow> assert_spmf (valid_plains msg1 msg2);
       b \<leftarrow> coin_spmf;
       z \<leftarrow> map_spmf (\<lambda>z. \<^bold>g [^] z \<otimes> (if b then msg1 else msg2)) (sample_uniform (order \<G>));
       guess \<leftarrow> \2 (\<^bold>g [^] y, z) \<sigma>;
       return_spmf (guess \<longleftrightarrow> b)
     } ELSE coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.ddh.ddh_1 (elgamal_adversary \) = TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. map_spmf (\<lambda>z. \<^bold>g [^] z \<otimes> (if b then msg1 else msg2)) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b)))))))) ELSE coin_spmf
[PROOF STEP]
by(simp add: ddh.ddh_1_def)
[PROOF STATE]
proof (state)
this:
local.ddh.ddh_1 (elgamal_adversary \) = TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. map_spmf (\<lambda>z. \<^bold>g [^] z \<otimes> (if b then msg1 else msg2)) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.ddh.ddh_1 (elgamal_adversary \) = TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. map_spmf (\<lambda>z. \<^bold>g [^] z \<otimes> (if b then msg1 else msg2)) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
have "\<dots> = TRY do {
       x \<leftarrow> sample_uniform (order \<G>);
       y \<leftarrow> sample_uniform (order \<G>);
       ((msg1, msg2), \<sigma>) \<leftarrow> \1 (\<^bold>g [^] x);
       _ :: unit \<leftarrow> assert_spmf (valid_plains msg1 msg2);
       z \<leftarrow> map_spmf (\<lambda>z. \<^bold>g [^] z) (sample_uniform (order \<G>));
       guess \<leftarrow> \2 (\<^bold>g [^] y, z) \<sigma>;
       map_spmf ((=) guess) coin_spmf
     } ELSE coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. map_spmf (\<lambda>z. \<^bold>g [^] z \<otimes> (if b then msg1 else msg2)) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b)))))))) ELSE coin_spmf = TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. map_spmf (([^]) \<^bold>g) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf
[PROOF STEP]
by(simp add: sample_uniform_one_time_pad map_spmf_conv_bind_spmf[where p=coin_spmf])
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. map_spmf (\<lambda>z. \<^bold>g [^] z \<otimes> (if b then msg1 else msg2)) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b)))))))) ELSE coin_spmf = TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. map_spmf (([^]) \<^bold>g) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. map_spmf (\<lambda>z. \<^bold>g [^] z \<otimes> (if b then msg1 else msg2)) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b)))))))) ELSE coin_spmf = TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. map_spmf (([^]) \<^bold>g) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
have "\<dots> = coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. map_spmf (([^]) \<^bold>g) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf = coin_spmf
[PROOF STEP]
by(simp add: map_eq_const_coin_spmf try_bind_spmf_lossless2')
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. map_spmf (([^]) \<^bold>g) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf = coin_spmf

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (\<^bold>g [^] x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plains msg1 msg2) \<bind> (\<lambda>_. map_spmf (([^]) \<^bold>g) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. \2 (\<^bold>g [^] y, z) \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf = coin_spmf

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
have "ddh.ddh_0 (elgamal_adversary \) = ind_cpa.ind_cpa \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.ddh.ddh_0 (elgamal_adversary \) = local.ind_cpa.ind_cpa \
[PROOF STEP]
by(simp add: ddh.ddh_0_def IND_CPA_PK_Single.ind_cpa.ind_cpa_def key_gen_def aencrypt_def nat_pow_pow eq_commute)
[PROOF STATE]
proof (state)
this:
local.ddh.ddh_0 (elgamal_adversary \) = local.ind_cpa.ind_cpa \

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.ddh.ddh_1 (elgamal_adversary \) = coin_spmf
local.ddh.ddh_0 (elgamal_adversary \) = local.ind_cpa.ind_cpa \
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.ddh.ddh_1 (elgamal_adversary \) = coin_spmf
local.ddh.ddh_0 (elgamal_adversary \) = local.ind_cpa.ind_cpa \

goal (1 subgoal):
 1. local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)
[PROOF STEP]
by(simp add: ddh.advantage_def ind_cpa.advantage_def)
[PROOF STATE]
proof (state)
this:
local.ind_cpa.advantage \ = local.ddh.advantage (elgamal_adversary \)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem elgamal_secure:
  "negligible (\<lambda>\<eta>. ind_cpa.advantage \<eta> (\<A> \<eta>))" if "negligible (\<lambda>\<eta>. ddh.advantage \<eta> (elgamal_adversary \<eta> (\<A> \<eta>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>\<eta>. local.ind_cpa.advantage \<eta> (\<A> \<eta>))
[PROOF STEP]
by(simp add: advantage_elgamal that)


[STATEMENT]
lemma lossless_key_gen [simp]: "lossless_spmf (key_gen) \<longleftrightarrow> 0 < order \<G>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf key_gen = (0 < order \<G>)
[PROOF STEP]
by(simp add: key_gen_def Let_def)


[STATEMENT]
lemma lossless_aencrypt [simp]:
  "lossless_spmf (aencrypt key plain) \<longleftrightarrow> 0 < order \<G>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (aencrypt key plain) = (0 < order \<G>)
[PROOF STEP]
by(simp add: aencrypt_def Let_def)


[STATEMENT]
lemma lossless_elgamal_adversary:
  "\<lbrakk> ind_cpa.lossless \<A>; 0 < order \<G> \<rbrakk>
  \<Longrightarrow> ddh.lossless (elgamal_adversary \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.ind_cpa.lossless \<A>; 0 < order \<G>\<rbrakk> \<Longrightarrow> local.ddh.lossless (elgamal_adversary \<A>)
[PROOF STEP]
by(cases \<A>)(simp add: ddh.lossless_def ind_cpa.lossless_def Let_def split_def)


[STATEMENT]
lemma chain_then_restrict:
  assumes "chain S" shows "S i = restrict (S i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (S i)
[PROOF STEP]
using assms[unfolded chain_def graph_homomorphism_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. vertices (S i) = Domain (Id_on (vertices (S i))) \<and> graph (S i) \<and> graph (S (i + 1)) \<and> Id_on (vertices (S i)) `` vertices (S i) \<subseteq> vertices (S (i + 1)) \<and> univalent (Id_on (vertices (S i))) \<and> edge_preserving (Id_on (vertices (S i))) (edges (S i)) (edges (S (i + 1)))

goal (1 subgoal):
 1. graph (S i)
[PROOF STEP]
by auto


[STATEMENT]
lemma chain:
  assumes "chain S"
  shows "j \<ge> i \<Longrightarrow> subgraph (S i) (S j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
proof(induct "j-i" arbitrary:i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>0 = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
 2. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j); Suc x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = j - i
i \<le> j

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>0 = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
 2. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j); Suc x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = j - i
i \<le> j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 = j - i
i \<le> j

goal (1 subgoal):
 1. subgraph (S i) (S j)
[PROOF STEP]
using chain_then_restrict[OF assms] assms[unfolded chain_def]
[PROOF STATE]
proof (prove)
using this:
0 = j - i
i \<le> j
graph (S ?i)
\<forall>i. subgraph (S i) (S (i + 1))

goal (1 subgoal):
 1. subgraph (S i) (S j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgraph (S i) (S j)

goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j); Suc x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j); Suc x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = ?j - ?i; ?i \<le> ?j\<rbrakk> \<Longrightarrow> subgraph (S ?i) (S ?j)
Suc x = j - i
i \<le> j

goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j); Suc x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
hence j:"i + x + 1 = j"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = ?j - ?i; ?i \<le> ?j\<rbrakk> \<Longrightarrow> subgraph (S ?i) (S ?j)
Suc x = j - i
i \<le> j

goal (1 subgoal):
 1. i + x + 1 = j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i + x + 1 = j

goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j); Suc x = j - i; i \<le> j\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i + x + 1 = j

goal (1 subgoal):
 1. subgraph (S i) (S j)
[PROOF STEP]
using subgraph_trans[OF Suc(1) assms[unfolded chain_def,rule_format,of "i+x"],of i,unfolded j]
[PROOF STATE]
proof (prove)
using this:
i + x + 1 = j
\<lbrakk>x = i + x - i; i \<le> i + x\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)

goal (1 subgoal):
 1. subgraph (S i) (S j)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
i + x + 1 = j
\<lbrakk>x = i + x - i; i \<le> i + x\<rbrakk> \<Longrightarrow> subgraph (S i) (S j)
\<lbrakk>x = ?j - ?i; ?i \<le> ?j\<rbrakk> \<Longrightarrow> subgraph (S ?i) (S ?j)
Suc x = j - i
i \<le> j

goal (1 subgoal):
 1. subgraph (S i) (S j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgraph (S i) (S j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_def2:
  "chain S = (\<forall> i j. j \<ge> i \<longrightarrow> subgraph (S i) (S j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain S = (\<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. chain S \<Longrightarrow> \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j)
 2. \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j) \<Longrightarrow> chain S
[PROOF STEP]
show "chain S \<Longrightarrow> \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain S \<Longrightarrow> \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>chain ?S; ?i \<le> ?j\<rbrakk> \<Longrightarrow> subgraph (?S ?i) (?S ?j)

goal (1 subgoal):
 1. chain S \<Longrightarrow> \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
chain S \<Longrightarrow> \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j)

goal (1 subgoal):
 1. \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j) \<Longrightarrow> chain S
[PROOF STEP]
show "\<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j) \<Longrightarrow> chain S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j) \<Longrightarrow> chain S
[PROOF STEP]
unfolding chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j) \<Longrightarrow> \<forall>i. subgraph (S i) (S (i + 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i j. i \<le> j \<longrightarrow> subgraph (S i) (S j) \<Longrightarrow> chain S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_sup_const[simp]:
  "chain_sup (\<lambda> x. S) = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_sup (\<lambda>x. S) = S
[PROOF STEP]
unfolding chain_sup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LG (\<Union>i. edges S) (\<Union>i. vertices S) = S
[PROOF STEP]
by auto