Theory Continuity
section ‹Continuity›
theory Continuity imports Healthiness begin
text ‹We rely on one additional healthiness property, continuity, which is shown here seperately,
as its proof relies, in general, on healthiness. It is only relevant when a program appears
in an inductive context i.e.~inside a loop.›
text ‹A continuous transformer preserves limits (or the suprema of ascending chains).›
definition bd_cts :: "'s trans ⇒ bool"
where "bd_cts t = (∀M. (∀i. (M i ⊩ M (Suc i)) ∧ sound (M i)) ⟶
(∃b. ∀i. bounded_by b (M i)) ⟶
t (Sup_exp (range M)) = Sup_exp (range (t o M)))"
lemma bd_ctsD:
"⟦ bd_cts t; ⋀i. M i ⊩ M (Suc i); ⋀i. sound (M i); ⋀i. bounded_by b (M i) ⟧ ⟹
t (Sup_exp (range M)) = Sup_exp (range (t o M))"
unfolding bd_cts_def by(auto)
lemma bd_ctsI:
"(⋀b M. (⋀i. M i ⊩ M (Suc i)) ⟹ (⋀i. sound (M i)) ⟹ (⋀i. bounded_by b (M i)) ⟹
t (Sup_exp (range M)) = Sup_exp (range (t o M))) ⟹ bd_cts t"
unfolding bd_cts_def by(auto)
text ‹A generalised property for transformers of transformers.›
definition bd_cts_tr :: "('s trans ⇒ 's trans) ⇒ bool"
where "bd_cts_tr T = (∀M. (∀i. le_trans (M i) (M (Suc i)) ∧ feasible (M i)) ⟶
equiv_trans (T (Sup_trans (M ` UNIV))) (Sup_trans ((T o M) ` UNIV)))"
lemma bd_cts_trD:
"⟦ bd_cts_tr T; ⋀i. le_trans (M i) (M (Suc i)); ⋀i. feasible (M i) ⟧ ⟹
equiv_trans (T (Sup_trans (M ` UNIV))) (Sup_trans ((T o M) ` UNIV))"
by(simp add:bd_cts_tr_def)
lemma bd_cts_trI:
"(⋀M. (⋀i. le_trans (M i) (M (Suc i))) ⟹ (⋀i. feasible (M i)) ⟹
equiv_trans (T (Sup_trans (M ` UNIV))) (Sup_trans ((T o M) ` UNIV))) ⟹ bd_cts_tr T"
by(simp add:bd_cts_tr_def)
subsection ‹Continuity of Primitives›
lemma cts_wp_Abort:
"bd_cts (wp (Abort::'s prog))"
proof -
have X: "range (λ(i::nat) (s::'s). 0) = {λs. 0}" by(auto)
show ?thesis by(intro bd_ctsI, simp add:wp_eval o_def Sup_exp_def X)
qed
lemma cts_wp_Skip:
"bd_cts (wp Skip)"
by(rule bd_ctsI, simp add:wp_def Skip_def o_def)
lemma cts_wp_Apply:
"bd_cts (wp (Apply f))"
proof -
have X: "⋀M s. {P (f s) |P. P ∈ range M} = {P s |P. P ∈ range (λi s. M i (f s))}" by(auto)
show ?thesis by(intro bd_ctsI ext, simp add:wp_eval o_def Sup_exp_def X)
qed
lemma cts_wp_Bind:
fixes a::"'a ⇒ 's prog"
assumes ca: "⋀s. bd_cts (wp (a (f s)))"
shows "bd_cts (wp (Bind f a))"
proof(rule bd_ctsI)
fix M::"nat ⇒ 's expect" and c::real
assume chain: "⋀i. M i ⊩ M (Suc i)" and sM: "⋀i. sound (M i)"
and bM: "⋀i. bounded_by c (M i)"
with bd_ctsD[OF ca]
have "⋀s. wp (a (f s)) (Sup_exp (range M)) =
Sup_exp (range (wp (a (f s)) o M))"
by(auto)
moreover have "⋀s. {fa s |fa. fa ∈ range (λx. wp (a (f s)) (M x))} =
{fa s |fa. fa ∈ range (λx s. wp (a (f s)) (M x) s)}"
by(auto)
ultimately show "wp (Bind f a) (Sup_exp (range M)) =
Sup_exp (range (wp (Bind f a) ∘ M))"
by(simp add:wp_eval o_def Sup_exp_def)
qed
text ‹The first nontrivial proof. We transform the suprema into limits, and appeal to the
continuity of the underlying operation (here infimum). This is typical of the remainder of the
nonrecursive elements.›
lemma cts_wp_DC:
fixes a b::"'s prog"
assumes ca: "bd_cts (wp a)"
and cb: "bd_cts (wp b)"
and ha: "healthy (wp a)"
and hb: "healthy (wp b)"
shows "bd_cts (wp (a ⨅ b))"
proof(rule bd_ctsI, rule antisym)
fix M::"nat ⇒ 's expect" and c::real
assume chain: "⋀i. M i ⊩ M (Suc i)" and sM: "⋀i. sound (M i)"
and bM: "⋀i. bounded_by c (M i)"
from ha hb have hab: "healthy (wp (a ⨅ b))" by(rule healthy_intros)
from bM have leSup: "⋀i. M i ⊩ Sup_exp (range M)" by(auto intro:Sup_exp_upper)
from sM bM have sSup: "sound (Sup_exp (range M))" by(auto intro:Sup_exp_sound)
show "Sup_exp (range (wp (a ⨅ b) ∘ M)) ⊩ wp (a ⨅ b) (Sup_exp (range M))"
proof(rule Sup_exp_least, clarsimp, rule le_funI)
fix i s
from mono_transD[OF healthy_monoD[OF hab]] leSup sM sSup
have "wp (a ⨅ b) (M i) ⊩ wp (a ⨅ b) (Sup_exp (range M))" by(auto)
thus "wp (a ⨅ b) (M i) s ≤ wp (a ⨅ b) (Sup_exp (range M)) s" by(auto)
from hab sSup have "sound (wp (a ⨅ b) (Sup_exp (range M)))" by(auto)
thus "nneg (wp (a ⨅ b) (Sup_exp (range M)))" by(auto)
qed
from sM bM ha have "⋀i. bounded_by c (wp a (M i))" by(auto)
hence baM: "⋀i s. wp a (M i) s ≤ c" by(auto)
from sM bM hb have "⋀i. bounded_by c (wp b (M i))" by(auto)
hence bbM: "⋀i s. wp b (M i) s ≤ c" by(auto)
show "wp (a ⨅ b) (Sup_exp (range M)) ⊩ Sup_exp (range (wp (a ⨅ b) ∘ M))"
proof(simp add:wp_eval o_def, rule le_funI)
fix s::'s
from bd_ctsD[OF ca, of M, OF chain sM bM] bd_ctsD[OF cb, of M, OF chain sM bM]
have "min (wp a (Sup_exp (range M)) s) (wp b (Sup_exp (range M)) s) =
min (Sup_exp (range (wp a o M)) s) (Sup_exp (range (wp b o M)) s)" by(simp)
also {
have "{f s |f. f ∈ range (λx. wp a (M x))} = range (λi. wp a (M i) s)"
"{f s |f. f ∈ range (λx. wp b (M x))} = range (λi. wp b (M i) s)"
by(auto)
hence "min (Sup_exp (range (wp a o M)) s) (Sup_exp (range (wp b o M)) s) =
min (Sup (range (λi. wp a (M i) s))) (Sup (range (λi. wp b (M i) s)))"
by(simp add:Sup_exp_def o_def)
}
also {
have "(λi. wp a (M i) s) ⇢ Sup (range (λi. wp a (M i) s))"
proof(rule increasing_LIMSEQ)
fix n
from mono_transD[OF healthy_monoD, OF ha] sM chain
show "wp a (M n) s ≤ wp a (M (Suc n)) s" by(auto intro:le_funD)
from baM show "wp a (M n) s ≤ Sup (range (λi. wp a (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
fix e::real assume pe: "0 < e"
from baM have cSup: "Sup (range (λi. wp a (M i) s)) ∈ closure (range (λi. wp a (M i) s))"
by(blast intro:closure_contains_Sup)
with pe obtain y where yin: "y ∈ (range (λi. wp a (M i) s))"
and dy: "dist y (Sup (range (λi. wp a (M i) s))) < e"
by(blast dest:iffD1[OF closure_approachable])
from yin obtain i where "y = wp a (M i) s" by(auto)
with dy have "dist (wp a (M i) s) (Sup (range (λi. wp a (M i) s))) < e"
by(simp)
moreover from baM have "wp a (M i) s ≤ Sup (range (λi. wp a (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
ultimately have "Sup (range (λi. wp a (M i) s)) ≤ wp a (M i) s + e"
by(simp add:dist_real_def)
thus "∃i. Sup (range (λi. wp a (M i) s)) ≤ wp a (M i) s + e" by(auto)
qed
moreover
have "(λi. wp b (M i) s) ⇢ Sup (range (λi. wp b (M i) s))"
proof(rule increasing_LIMSEQ)
fix n
from mono_transD[OF healthy_monoD, OF hb] sM chain
show "wp b (M n) s ≤ wp b (M (Suc n)) s" by(auto intro:le_funD)
from bbM show "wp b (M n) s ≤ Sup (range (λi. wp b (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
fix e::real assume pe: "0 < e"
from bbM have cSup: "Sup (range (λi. wp b (M i) s)) ∈ closure (range (λi. wp b (M i) s))"
by(blast intro:closure_contains_Sup)
with pe obtain y where yin: "y ∈ (range (λi. wp b (M i) s))"
and dy: "dist y (Sup (range (λi. wp b (M i) s))) < e"
by(blast dest:iffD1[OF closure_approachable])
from yin obtain i where "y = wp b (M i) s" by(auto)
with dy have "dist (wp b (M i) s) (Sup (range (λi. wp b (M i) s))) < e"
by(simp)
moreover from bbM have "wp b (M i) s ≤ Sup (range (λi. wp b (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
ultimately have "Sup (range (λi. wp b (M i) s)) ≤ wp b (M i) s + e"
by(simp add:dist_real_def)
thus "∃i. Sup (range (λi. wp b (M i) s)) ≤ wp b (M i) s + e" by(auto)
qed
ultimately have "(λi. min (wp a (M i) s) (wp b (M i) s)) ⇢
min (Sup (range (λi. wp a (M i) s))) (Sup (range (λi. wp b (M i) s)))"
by(rule tendsto_min)
moreover have "bdd_above (range (λi. min (wp a (M i) s) (wp b (M i) s)))"
proof(intro bdd_aboveI, clarsimp)
fix i
have "min (wp a (M i) s) (wp b (M i) s) ≤ wp a (M i) s" by(auto)
also {
from ha sM bM have "bounded_by c (wp a (M i))" by(auto)
hence "wp a (M i) s ≤ c" by(auto)
}
finally show "min (wp a (M i) s) (wp b (M i) s) ≤ c" .
qed
ultimately
have "min (Sup (range (λi. wp a (M i) s))) (Sup (range (λi. wp b (M i) s))) ≤
Sup (range (λi. min (wp a (M i) s) (wp b (M i) s)))"
by(blast intro:LIMSEQ_le_const2 cSup_upper min.mono[OF baM bbM])
}
also {
have "range (λi. min (wp a (M i) s) (wp b (M i) s)) =
{f s |f. f ∈ range (λi s. min (wp a (M i) s) (wp b (M i) s))}"
by(auto)
hence "Sup (range (λi. min (wp a (M i) s) (wp b (M i) s))) =
Sup_exp (range (λi s. min (wp a (M i) s) (wp b (M i) s))) s"
by (simp add: Sup_exp_def cong del: SUP_cong_simp)
}
finally show "min (wp a (Sup_exp (range M)) s) (wp b (Sup_exp (range M)) s) ≤
Sup_exp (range (λi s. min (wp a (M i) s) (wp b (M i) s))) s" .
qed
qed
lemma cts_wp_Seq:
fixes a b::"'s prog"
assumes ca: "bd_cts (wp a)"
and cb: "bd_cts (wp b)"
and hb: "healthy (wp b)"
shows "bd_cts (wp (a ;; b))"
proof(rule bd_ctsI, simp add:o_def wp_eval)
fix M::"nat ⇒ 's expect" and c::real
assume chain: "⋀i. M i ⊩ M (Suc i)" and sM: "⋀i. sound (M i)"
and bM: "⋀i. bounded_by c (M i)"
hence "wp a (wp b (Sup_exp (range M))) = wp a (Sup_exp (range (wp b o M)))"
by(subst bd_ctsD[OF cb], auto)
also {
from sM hb have "⋀i. sound ((wp b o M) i)" by(auto)
moreover from chain sM
have "⋀i. (wp b o M) i ⊩ (wp b o M) (Suc i)"
by(auto intro:mono_transD[OF healthy_monoD, OF hb])
moreover from sM bM hb have "⋀i. bounded_by c ((wp b o M) i)" by(auto)
ultimately have "wp a (Sup_exp (range (wp b o M))) =
Sup_exp (range (wp a o (wp b o M)))"
by(subst bd_ctsD[OF ca], auto)
}
also have "Sup_exp (range (wp a o (wp b o M))) =
Sup_exp (range (λi. wp a (wp b (M i))))"
by(simp add:o_def)
finally show "wp a (wp b (Sup_exp (range M))) =
Sup_exp (range (λi. wp a (wp b (M i))))" .
qed
lemma cts_wp_PC:
fixes a b::"'s prog"
assumes ca: "bd_cts (wp a)"
and cb: "bd_cts (wp b)"
and ha: "healthy (wp a)"
and hb: "healthy (wp b)"
and up: "unitary p"
shows "bd_cts (wp (PC a p b))"
proof(rule bd_ctsI, rule ext, simp add:o_def wp_eval)
fix M::"nat ⇒ 's expect" and c::real and s::'s
assume chain: "⋀i. M i ⊩ M (Suc i)" and sM: "⋀i. sound (M i)"
and bM: "⋀i. bounded_by c (M i)"
from sM have "⋀i. nneg (M i)" by(auto)
with bM have nc: "0 ≤ c" by(auto)
from chain sM bM have "wp a (Sup_exp (range M)) = Sup_exp (range (wp a o M))"
by(rule bd_ctsD[OF ca])
hence "wp a (Sup_exp (range M)) s = Sup_exp (range (wp a o M)) s"
by(simp)
also {
have "{f s |f. f ∈ range (λx. wp a (M x))} = range (λi. wp a (M i) s)"
by(auto)
hence "Sup_exp (range (wp a o M)) s = Sup (range (λi. wp a (M i) s))"
by(simp add:Sup_exp_def o_def)
}
finally have "p s * wp a (Sup_exp (range M)) s =
p s * Sup (range (λi. wp a (M i) s))" by(simp)
also have "... = Sup {p s * x |x. x ∈ range (λi. wp a (M i) s)}"
proof(rule cSup_mult, blast, clarsimp)
from up show "0 ≤ p s" by(auto)
fix i
from sM bM ha have "bounded_by c (wp a (M i))" by(auto)
thus "wp a (M i) s ≤ c" by(auto)
qed
also {
have "{p s * x |x. x ∈ range (λi. wp a (M i) s)} = range (λi. p s * wp a (M i) s)"
by(auto)
hence "Sup {p s * x |x. x ∈ range (λi. wp a (M i) s)} =
Sup (range (λi. p s * wp a (M i) s))" by(simp)
}
finally have "p s * wp a (Sup_exp (range M)) s = Sup (range (λi. p s * wp a (M i) s))" .
moreover {
from chain sM bM have "wp b (Sup_exp (range M)) = Sup_exp (range (wp b o M))"
by(rule bd_ctsD[OF cb])
hence "wp b (Sup_exp (range M)) s = Sup_exp (range (wp b o M)) s"
by(simp)
also {
have "{f s |f. f ∈ range (λx. wp b (M x))} = range (λi. wp b (M i) s)"
by(auto)
hence "Sup_exp (range (wp b o M)) s = Sup (range (λi. wp b (M i) s))"
by(simp add:Sup_exp_def o_def)
}
finally have "(1 - p s) * wp b (Sup_exp (range M)) s =
(1 - p s) * Sup (range (λi. wp b (M i) s))" by(simp)
also have "... = Sup {(1 - p s) * x |x. x ∈ range (λi. wp b (M i) s)}"
proof(rule cSup_mult, blast, clarsimp)
from up show "0 ≤ 1 - p s"
by auto
fix i
from sM bM hb have "bounded_by c (wp b (M i))" by(auto)
thus "wp b (M i) s ≤ c" by(auto)
qed
also {
have "{(1 - p s) * x |x. x ∈ range (λi. wp b (M i) s)} =
range (λi. (1 - p s) * wp b (M i) s)"
by(auto)
hence "Sup {(1 - p s) * x |x. x ∈ range (λi. wp b (M i) s)} =
Sup (range (λi. (1 - p s) * wp b (M i) s))" by(simp)
}
finally have "(1 - p s) * wp b (Sup_exp (range M)) s =
Sup (range (λi. (1 - p s) * wp b (M i) s))" .
}
ultimately
have "p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s =
Sup (range (λi. p s * wp a (M i) s)) + Sup (range (λi. (1 - p s) * wp b (M i) s))"
by(simp)
also {
from bM sM ha have "⋀i. bounded_by c (wp a (M i))" by(auto)
hence "⋀i. wp a (M i) s ≤ c" by(auto)
moreover from up have "0 ≤ p s" by(auto)
ultimately have "⋀i. p s * wp a (M i) s ≤ p s * c" by(auto intro:mult_left_mono)
also from up nc have "p s * c ≤ 1 * c" by(blast intro:mult_right_mono)
also have "... = c" by(simp)
finally have baM: "⋀i. p s * wp a (M i) s ≤ c" .
have lima: "(λi. p s * wp a (M i) s) ⇢ Sup (range (λi. p s * wp a (M i) s))"
proof(rule increasing_LIMSEQ)
fix n
from sM chain healthy_monoD[OF ha] have "wp a (M n) ⊩ wp a (M (Suc n))"
by(auto)
with up show "p s * wp a (M n) s ≤ p s * wp a (M (Suc n)) s"
by(blast intro:mult_left_mono)
from baM show "p s * wp a (M n) s ≤ Sup (range (λi. p s * wp a (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
next
fix e::real
assume pe: "0 < e"
from baM have "Sup (range (λi. p s * wp a (M i) s)) ∈
closure (range (λi. p s * wp a (M i) s))"
by(blast intro:closure_contains_Sup)
thm closure_approachable
with pe obtain y where yin: "y ∈ range (λi. p s * wp a (M i) s)"
and dy: "dist y (Sup (range (λi. p s * wp a (M i) s))) < e"
by(blast dest:iffD1[OF closure_approachable])
from yin obtain i where "y = p s * wp a (M i) s" by(auto)
with dy have "dist (p s * wp a (M i) s) (Sup (range (λi. p s * wp a (M i) s))) < e"
by(simp)
moreover from baM have "p s * wp a (M i) s ≤ Sup (range (λi. p s * wp a (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
ultimately have "Sup (range (λi. p s * wp a (M i) s)) ≤ p s * wp a (M i) s + e"
by(simp add:dist_real_def)
thus "∃i. Sup (range (λi. p s * wp a (M i) s)) ≤ p s * wp a (M i) s + e" by(auto)
qed
from bM sM hb have "⋀i. bounded_by c (wp b (M i))" by(auto)
hence "⋀i. wp b (M i) s ≤ c" by(auto)
moreover from up have "0 ≤ (1 - p s)"
by auto
ultimately have "⋀i. (1 - p s) * wp b (M i) s ≤ (1 - p s) * c" by(auto intro:mult_left_mono)
also {
from up have "1 - p s ≤ 1" by(auto)
with nc have "(1 - p s) * c ≤ 1 * c" by(blast intro:mult_right_mono)
}
also have "1 * c = c" by(simp)
finally have bbM: "⋀i. (1 - p s) * wp b (M i) s ≤ c" .
have limb: "(λi. (1 - p s) * wp b (M i) s) ⇢ Sup (range (λi. (1 - p s) * wp b (M i) s))"
proof(rule increasing_LIMSEQ)
fix n
from sM chain healthy_monoD[OF hb] have "wp b (M n) ⊩ wp b (M (Suc n))"
by(auto)
moreover from up have "0 ≤ 1 - p s"
by auto
ultimately show "(1 - p s) * wp b (M n) s ≤ (1 - p s) * wp b (M (Suc n)) s"
by(blast intro:mult_left_mono)
from bbM show "(1 - p s) * wp b (M n) s ≤ Sup (range (λi. (1 - p s) * wp b (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
next
fix e::real
assume pe: "0 < e"
from bbM have "Sup (range (λi. (1 - p s) * wp b (M i) s)) ∈
closure (range (λi. (1 - p s) * wp b (M i) s))"
by(blast intro:closure_contains_Sup)
with pe obtain y where yin: "y ∈ range (λi. (1 - p s) * wp b (M i) s)"
and dy: "dist y (Sup (range (λi. (1 - p s) * wp b (M i) s))) < e"
by(blast dest:iffD1[OF closure_approachable])
from yin obtain i where "y = (1 - p s) * wp b (M i) s" by(auto)
with dy have "dist ((1 - p s) * wp b (M i) s)
(Sup (range (λi. (1 - p s) * wp b (M i) s))) < e"
by(simp)
moreover from bbM
have "(1 - p s) * wp b (M i) s ≤ Sup (range (λi. (1 - p s) * wp b (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
ultimately have "Sup (range (λi. (1 - p s) * wp b (M i) s)) ≤ (1 - p s) * wp b (M i) s + e"
by(simp add:dist_real_def)
thus "∃i. Sup (range (λi. (1 - p s) * wp b (M i) s)) ≤ (1 - p s) * wp b (M i) s + e" by(auto)
qed
from lima limb have "(λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s) ⇢
Sup (range (λi. p s * wp a (M i) s)) + Sup (range (λi. (1 - p s) * wp b (M i) s))"
by(rule tendsto_add)
moreover from add_mono[OF baM bbM]
have "⋀i. p s * wp a (M i) s + (1 - p s) * wp b (M i) s ≤
Sup (range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s))"
by(intro cSup_upper bdd_aboveI, auto)
ultimately have "Sup (range (λi. p s * wp a (M i) s)) +
Sup (range (λi. (1 - p s) * wp b (M i) s)) ≤
Sup (range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s))"
by(blast intro: LIMSEQ_le_const2)
}
also {
have "range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s) =
{f s |f. f ∈ range (λx s. p s * wp a (M x) s + (1 - p s) * wp b (M x) s)}"
by(auto)
hence "Sup (range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s)) =
Sup_exp (range (λx s. p s * wp a (M x) s + (1 - p s) * wp b (M x) s)) s"
by (simp add: Sup_exp_def cong del: SUP_cong_simp)
}
finally
have "p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s ≤
Sup_exp (range (λi s. p s * wp a (M i) s + (1 - p s) * wp b (M i) s)) s" .
moreover
have "Sup_exp (range (λi s. p s * wp a (M i) s + (1 - p s) * wp b (M i) s)) s ≤
p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s"
proof(rule le_funD[OF Sup_exp_least], clarsimp, rule le_funI)
fix i::nat and s::'s
from bM have leSup: "M i ⊩ Sup_exp (range M)"
by(blast intro: Sup_exp_upper)
moreover from sM bM have sSup: "sound (Sup_exp (range M))"
by(auto intro:Sup_exp_sound)
moreover note healthy_monoD[OF ha] sM
ultimately have "wp a (M i) ⊩ wp a (Sup_exp (range M))" by(auto)
hence "wp a (M i) s ≤ wp a (Sup_exp (range M)) s" by(auto)
moreover {
from leSup sSup healthy_monoD[OF hb] sM
have "wp b (M i) ⊩ wp b (Sup_exp (range M))" by(auto)
hence "wp b (M i) s ≤ wp b (Sup_exp (range M)) s" by(auto)
}
moreover from up have "0 ≤ p s" "0 ≤ 1 - p s"
by auto
ultimately
show "p s * wp a (M i) s + (1 - p s) * wp b (M i) s ≤
p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s"
by(blast intro:add_mono mult_left_mono)
from sSup ha hb have "sound (wp a (Sup_exp (range M)))"
"sound (wp b (Sup_exp (range M)))"
by(auto)
hence "⋀s. 0 ≤ wp a (Sup_exp (range M)) s" "⋀s. 0 ≤ wp b (Sup_exp (range M)) s"
by(auto)
moreover from up have "⋀s. 0 ≤ p s" "⋀s. 0 ≤ 1 - p s"
by auto
ultimately show "nneg (λc. p c * wp a (Sup_exp (range M)) c +
(1 - p c) * wp b (Sup_exp (range M)) c)"
by(blast intro:add_nonneg_nonneg mult_nonneg_nonneg)
qed
ultimately show "p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s =
Sup_exp (range (λx s. p s * wp a (M x) s + (1 - p s) * wp b (M x) s)) s"
by(auto)
qed
text ‹Both set-based choice operators are only continuous for finite sets (probabilistic choice
\emph{can} be extended infinitely, but we have not done so). The proofs for both are inductive,
and rely on the above results on binary operators.›
lemma SetPC_Bind:
"SetPC a p = Bind p (λp. SetPC a (λ_. p))"
by(intro ext, simp add:SetPC_def Bind_def Let_def)
lemma SetPC_remove:
assumes nz: "p x ≠ 0" and n1: "p x ≠ 1"
and fsupp: "finite (supp p)"
shows "SetPC a (λ_. p) = PC (a x) (λ_. p x) (SetPC a (λ_. dist_remove p x))"
proof(intro ext, simp add:SetPC_def PC_def)
fix ab P s
from nz have "x ∈ supp p" by(simp add:supp_def)
hence "supp p = insert x (supp p - {x})" by(auto)
hence "(∑x∈supp p. p x * a x ab P s) =
(∑x∈insert x (supp p - {x}). p x * a x ab P s)"
by(simp)
also from fsupp
have "... = p x * a x ab P s + (∑x∈supp p - {x}. p x * a x ab P s)"
by(blast intro:sum.insert)
also from n1
have "... = p x * a x ab P s + (1 - p x) * ((∑x∈supp p - {x}. p x * a x ab P s) / (1 - p x))"
by(simp add:field_simps)
also have "... = p x * a x ab P s +
(1 - p x) * ((∑y∈supp p - {x}. (p y / (1 - p x)) * a y ab P s))"
by(simp add:sum_divide_distrib)
also have "... = p x * a x ab P s +
(1 - p x) * ((∑y∈supp p - {x}. dist_remove p x y * a y ab P s))"
by(simp add:dist_remove_def)
also from nz n1
have "... = p x * a x ab P s +
(1 - p x) * ((∑y∈supp (dist_remove p x). dist_remove p x y * a y ab P s))"
by(simp add:supp_dist_remove)
finally show "(∑x∈supp p. p x * a x ab P s) =
p x * a x ab P s +
(1 - p x) * (∑y∈supp (dist_remove p x). dist_remove p x y * a y ab P s)" .
qed
lemma cts_bot:
"bd_cts (λ(P::'s expect) (s::'s). 0::real)"
proof -
have X: "⋀s::'s. {(P::'s expect) s |P. P ∈ range (λP s. 0)} = {0}" by(auto)
show ?thesis by(intro bd_ctsI, simp add:Sup_exp_def o_def X)
qed
lemma wp_SetPC_nil:
"wp (SetPC a (λs a. 0)) = (λP s. 0)"
by(intro ext, simp add:wp_eval)
lemma SetPC_sgl:
"supp p = {x} ⟹ SetPC a (λ_. p) = (λab P s. p x * a x ab P s)"
by(simp add:SetPC_def)
lemma bd_cts_scale:
fixes a::"'s trans"
assumes ca: "bd_cts a"
and ha: "healthy a"
and nnc: "0 ≤ c"
shows "bd_cts (λP s. c * a P s)"
proof(intro bd_ctsI ext, simp add:o_def)
fix M::"nat ⇒ 's expect" and d::real and s::'s
assume chain: "⋀i. M i ⊩ M (Suc i)" and sM: "⋀i. sound (M i)"
and bM: "⋀i. bounded_by d (M i)"
from sM have "⋀i. nneg (M i)" by(auto)
with bM have nnd: "0 ≤ d" by(auto)
from sM bM have sSup: "sound (Sup_exp (range M))" by(auto intro:Sup_exp_sound)
with healthy_scalingD[OF ha] nnc
have "c * a (Sup_exp (range M)) s = a (λs. c * Sup_exp (range M) s) s"
by(auto intro:scalingD)
also {
have "⋀s. {f s |f. f ∈ range M} = range (λi. M i s)" by(auto)
hence "a (λs. c * Sup_exp (range M) s) s =
a (λs. c * Sup (range (λi. M i s))) s"
by(simp add:Sup_exp_def)
}
also {
from bM have "⋀x s. x ∈ range (λi. M i s) ⟹ x ≤ d" by(auto)
with nnc have "a (λs. c * Sup (range (λi. M i s))) s =
a (λs. Sup {c*x |x. x ∈ range (λi. M i s)}) s"
by(subst cSup_mult, blast+)
}
also {
have X: "⋀s. {c * x |x. x ∈ range (λi. M i s)} = range (λi. c * M i s)" by(auto)
have "a (λs. Sup {c * x |x. x ∈ range (λi. M i s)}) s =
a (λs. Sup (range (λi. c * M i s))) s" by(simp add:X)
}
also {
have "⋀s. range (λi. c * M i s) = {f s |f. f ∈ range (λi s. c * M i s)}"
by(auto)
hence "(λs. Sup (range (λi. c * M i s))) = Sup_exp (range (λi s. c * M i s))"
by (simp add: Sup_exp_def cong del: SUP_cong_simp)
hence "a (λs. Sup (range (λi. c * M i s))) s =
a (Sup_exp (range (λi s. c * M i s))) s" by(simp)
}
also {
from le_funD[OF chain] nnc
have "⋀i. (λs. c * M i s) ⊩ (λs. c * M (Suc i) s)"
by(auto intro:le_funI[OF mult_left_mono])
moreover from sM nnc
have "⋀i. sound (λs. c * M i s)"
by(auto intro:sound_intros)
moreover from bM nnc
have "⋀i. bounded_by (c * d) (λs. c * M i s)"
by(auto intro:mult_left_mono)
ultimately
have "a (Sup_exp (range (λi s. c * M i s))) =
Sup_exp (range (a o (λi s. c * M i s)))"
by(rule bd_ctsD[OF ca])
hence "a (Sup_exp (range (λi s. c * M i s))) s =
Sup_exp (range (a o (λi s. c * M i s))) s"
by(auto)
}
also have "Sup_exp (range (a o (λi s. c * M i s))) s =
Sup_exp (range (λx. a (λs. c * M x s))) s"
by(simp add:o_def)
also {
from nnc sM
have "⋀x. a (λs. c * M x s) = (λs. c * a (M x) s)"
by(auto intro:scalingD[OF healthy_scalingD, OF ha, symmetric])
hence "Sup_exp (range (λx. a (λs. c * M x s))) s =
Sup_exp (range (λx s. c * a (M x) s)) s"
by(simp)
}
finally show "c * a (Sup_exp (range M)) s = Sup_exp (range (λx s. c * a (M x) s)) s" .
qed
lemma cts_wp_SetPC_const:
fixes a::"'a ⇒ 's prog"
assumes ca: "⋀x. x ∈ (supp p) ⟹ bd_cts (wp (a x))"
and ha: "⋀x. x ∈ (supp p) ⟹ healthy (wp (a x))"
and up: "unitary p"
and sump: "sum p (supp p) ≤ 1"
and fsupp: "finite (supp p)"
shows "bd_cts (wp (SetPC a (λ_. p)))"
proof(cases "supp p = {}", simp add:supp_empty SetPC_def wp_def cts_bot)
assume nesupp: "supp p ≠ {}"
from fsupp have "unitary p ⟶ sum p (supp p) ≤ 1 ⟶
(∀x∈supp p. bd_cts (wp (a x))) ⟶
(∀x∈supp p. healthy (wp (a x))) ⟶
bd_cts (wp (SetPC a (λ_. p)))"
proof(induct "supp p" arbitrary:p, simp add:supp_empty wp_SetPC_nil cts_bot, clarify)
fix x::'a and F::"'a set" and p::"'a ⇒ real"
assume fF: "finite F"
assume "insert x F = supp p"
hence pstep: "supp p = insert x F" by(simp)
hence xin: "x ∈ supp p" by(auto)
assume up: "unitary p" and ca: "∀x∈supp p. bd_cts (wp (a x))"
and ha: "∀x∈supp p. healthy (wp (a x))"
and sump: "sum p (supp p) ≤ 1"
and xni: "x ∉ F"
assume IH: "⋀p. F = supp p ⟹
unitary p ⟶ sum p (supp p) ≤ 1 ⟶
(∀x∈supp p. bd_cts (wp (a x))) ⟶
(∀x∈supp p. healthy (wp (a x))) ⟶
bd_cts (wp (SetPC a (λ_. p)))"
from fF pstep have fsupp: "finite (supp p)" by(auto)
from xin have nzp: "p x ≠ 0" by(simp add:supp_def)
have xy_le_sum:
"⋀y. y ∈ supp p ⟹ y ≠ x ⟹ p x + p y ≤ sum p (supp p)"
proof -
fix y assume yin: "y ∈ supp p" and yne: "y ≠ x"
from up have "0 ≤ sum p (supp p - {x,y})"
by(auto intro:sum_nonneg)
hence "p x + p y ≤ p x + p y + sum p (supp p - {x,y})"
by(auto)
also {
from yin yne fsupp
have "p y + sum p (supp p - {x,y}) = sum p (supp p - {x})"
by(subst sum.insert[symmetric], (blast intro!:sum.cong)+)
moreover
from xin fsupp
have "p x + sum p (supp p - {x}) = sum p (supp p)"
by(subst sum.insert[symmetric], (blast intro!:sum.cong)+)
ultimately
have "p x + p y + sum p (supp p - {x, y}) = sum p (supp p)" by(simp)
}
finally show "p x + p y ≤ sum p (supp p)" .
qed
have n1p: "⋀y. y ∈ supp p ⟹ y ≠ x ⟹ p x ≠ 1"
proof(rule ccontr, simp)
assume px1: "p x = 1"
fix y assume yin: "y ∈ supp p" and yne: "y ≠ x"
from up have "0 ≤ p y" by(auto)
with yin have "0 < p y" by(auto simp:supp_def)
hence "0 + p x < p y + p x" by(rule add_strict_right_mono)
with px1 have "1 < p x + p y" by(simp)
also from yin yne have "p x + p y ≤ sum p (supp p)"
by(rule xy_le_sum)
finally show False using sump by(simp)
qed
show "bd_cts (wp (SetPC a (λ_. p)))"
proof(cases "F = {}")
case True with pstep have "supp p = {x}" by(simp)
hence "wp (SetPC a (λ_. p)) = (λP s. p x * wp (a x) P s)"
by(simp add:SetPC_sgl wp_def)
moreover {
from up ca ha xin have "bd_cts (wp (a x))" "healthy (wp (a x))" "0 ≤ p x"
by(auto)
hence "bd_cts (λP s. p x * wp (a x) P s)"
by(rule bd_cts_scale)
}
ultimately show ?thesis by(simp)
next
assume neF: "F ≠ {}"
then obtain y where yinF: "y ∈ F" by(auto)
with xni have yne: "y ≠ x" by(auto)
from yinF pstep have yin: "y ∈ supp p" by(auto)
from supp_dist_remove[of p x, OF nzp n1p, OF yin yne]
have supp_sub: "supp (dist_remove p x) ⊆ supp p" by(auto)
from xin ca have cax: "bd_cts (wp (a x))" by(auto)
from xin ha have hax: "healthy (wp (a x))" by(auto)
from supp_sub ha have hra: "∀x∈supp (dist_remove p x). healthy (wp (a x))"
by(auto)
from supp_sub ca have cra: "∀x∈supp (dist_remove p x). bd_cts (wp (a x))"
by(auto)
from supp_dist_remove[of p x, OF nzp n1p, OF yin yne] pstep xni
have Fsupp: "F = supp (dist_remove p x)"
by(simp)
have udp: "unitary (dist_remove p x)"
proof(intro unitaryI2 nnegI bounded_byI)
fix y
show "0 ≤ dist_remove p x y"
proof(cases "y=x", simp_all add:dist_remove_def)
from up have "0 ≤ p y" "0 ≤ 1 - p x"
by auto
thus "0 ≤ p y / (1 - p x)"
by(rule divide_nonneg_nonneg)
qed
show "dist_remove p x y ≤ 1"
proof(cases "y=x", simp_all add:dist_remove_def,
cases "y∈supp p", simp_all add:nsupp_zero)
assume yne: "y ≠ x" and yin: "y ∈ supp p"
hence "p x + p y ≤ sum p (supp p)"
by(auto intro:xy_le_sum)
also note sump
finally have "p y ≤ 1 - p x" by(auto)
moreover from up have "p x ≤ 1" by(auto)
moreover from yin yne have "p x ≠ 1" by(rule n1p)
ultimately show "p y / (1 - p x) ≤ 1" by(auto)
qed
qed
from xin have pxn0: "p x ≠ 0" by(auto simp:supp_def)
from yin yne have pxn1: "p x ≠ 1" by(rule n1p)
from pxn0 pxn1 have "sum (dist_remove p x) (supp (dist_remove p x)) =
sum (dist_remove p x) (supp p - {x})"
by(simp add:supp_dist_remove)
also have "... = (∑y∈supp p - {x}. p y / (1 - p x))"
by(simp add:dist_remove_def)
also have "... = (∑y∈supp p - {x}. p y) / (1 - p x)"
by(simp add:sum_divide_distrib)
also {
from xin have "insert x (supp p) = supp p" by(auto)
with fsupp have "p x + (∑y∈supp p - {x}. p y) = sum p (supp p)"
by(simp add:sum.insert[symmetric])
also note sump
finally have "sum p (supp p - {x}) ≤ 1 - p x" by(auto)
moreover {
from up have "p x ≤ 1" by(auto)
with pxn1 have "p x < 1" by(auto)
hence "0 < 1 - p x" by(auto)
}
ultimately have "sum p (supp p - {x}) / (1 - p x) ≤ 1"
by(auto)
}
finally have sdp: "sum (dist_remove p x) (supp (dist_remove p x)) ≤ 1" .
from Fsupp udp sdp hra cra IH
have cts_dr: "bd_cts (wp (SetPC a (λ_. dist_remove p x)))"
by(auto)
from up have upx: "unitary (λ_. p x)" by(auto)
from pxn0 pxn1 fsupp hra show ?thesis
by(simp add:SetPC_remove,
blast intro:cts_wp_PC cax cts_dr hax healthy_intros
unitary_sound[OF udp] sdp upx)
qed
qed
with assms show ?thesis by(auto)
qed
lemma cts_wp_SetPC:
fixes a::"'a ⇒ 's prog"
assumes ca: "⋀x s. x ∈ (supp (p s)) ⟹ bd_cts (wp (a x))"
and ha: "⋀x s. x ∈ (supp (p s)) ⟹ healthy (wp (a x))"
and up: "⋀s. unitary (p s)"
and sump: "⋀s. sum (p s) (supp (p s)) ≤ 1"
and fsupp: "⋀s. finite (supp (p s))"
shows "bd_cts (wp (SetPC a p))"
proof -
from assms have "bd_cts (wp (Bind p (λp. SetPC a (λ_. p))))"
by(iprover intro!:cts_wp_Bind cts_wp_SetPC_const)
thus ?thesis by(simp add:SetPC_Bind[symmetric])
qed
lemma wp_SetDC_Bind:
"SetDC a S = Bind S (λS. SetDC a (λ_. S))"
by(intro ext, simp add:SetDC_def Bind_def)
lemma SetDC_finite_insert:
assumes fS: "finite S"
and neS: "S ≠ {}"
shows "SetDC a (λ_. insert x S) = a x ⨅ SetDC a (λ_. S)"
proof (intro ext, simp add: SetDC_def DC_def cong del: image_cong_simp cong add: INF_cong_simp)
fix ab P s
from fS have A: "finite (insert (a x ab P s) ((λx. a x ab P s) ` S))"
and B: "finite (((λx. a x ab P s) ` S))" by(auto)
from neS have C: "insert (a x ab P s) ((λx. a x ab P s) ` S) ≠ {}"
and D: "(λx. a x ab P s) ` S ≠ {}" by(auto)
from A C have "Inf (insert (a x ab P s) ((λx. a x ab P s) ` S)) =
Min (insert (a x ab P s) ((λx. a x ab P s) ` S))"
by(auto intro:cInf_eq_Min)
also from B D have "... = min (a x ab P s) (Min ((λx. a x ab P s) ` S))"
by(auto intro:Min_insert)
also from B D have "... = min (a x ab P s) (Inf ((λx. a x ab P s) ` S))"
by(simp add:cInf_eq_Min)
finally show "(INF x∈insert x S. a x ab P s) =
min (a x ab P s) (INF x∈S. a x ab P s)"
by (simp cong del: INF_cong_simp)
qed
lemma SetDC_singleton:
"SetDC a (λ_. {x}) = a x"
by (simp add: SetDC_def cong del: INF_cong_simp)
lemma cts_wp_SetDC_const:
fixes a::"'a ⇒ 's prog"
assumes ca: "⋀x. x ∈ S ⟹ bd_cts (wp (a x))"
and ha: "⋀x. x ∈ S ⟹ healthy (wp (a x))"
and fS: "finite S"
and neS: "S ≠ {}"
shows "bd_cts (wp (SetDC a (λ_. S)))"
proof -
have "finite S ⟹ S ≠ {} ⟹
(∀x∈S. bd_cts (wp (a x))) ⟶
(∀x∈S. healthy (wp (a x))) ⟶
bd_cts (wp (SetDC a (λ_. S)))"
proof(induct S rule:finite_induct, simp, clarsimp)
fix x::'a and F::"'a set"
assume fF: "finite F"
and IH: "F ≠ {} ⟹ bd_cts (wp (SetDC a (λ_. F)))"
and cax: "bd_cts (wp (a x))"
and hax: "healthy (wp (a x))"
and haF: "∀x∈F. healthy (wp (a x))"
show "bd_cts (wp (SetDC a (λ_. insert x F)))"
proof(cases "F = {}", simp add:SetDC_singleton cax)
assume "F ≠ {}"
with fF cax hax haF IH show "bd_cts (wp (SetDC a (λ_. insert x F)))"
by(auto intro!:cts_wp_DC healthy_intros simp:SetDC_finite_insert)
qed
qed
with assms show ?thesis by(auto)
qed
lemma cts_wp_SetDC:
fixes a::"'a ⇒ 's prog"
assumes ca: "⋀x s. x ∈ S s ⟹ bd_cts (wp (a x))"
and ha: "⋀x s. x ∈ S s ⟹ healthy (wp (a x))"
and fS: "⋀s. finite (S s)"
and neS: "⋀s. S s ≠ {}"
shows "bd_cts (wp (SetDC a S))"
proof -
from assms have "bd_cts (wp (Bind S (λS. SetDC a (λ_. S))))"
by(iprover intro!:cts_wp_Bind cts_wp_SetDC_const)
thus ?thesis by(simp add:wp_SetDC_Bind[symmetric])
qed
lemma cts_wp_repeat:
"bd_cts (wp a) ⟹ healthy (wp a) ⟹ bd_cts (wp (repeat n a))"
by(induct n, auto intro:cts_wp_Skip cts_wp_Seq healthy_intros)
lemma cts_wp_Embed:
"bd_cts t ⟹ bd_cts (wp (Embed t))"
by(simp add:wp_eval)
subsection ‹Continuity of a Single Loop Step›
text ‹A single loop iteration is continuous, in the more general sense defined above for
transformer transformers.›
lemma cts_wp_loopstep:
fixes body::"'s prog"
assumes hb: "healthy (wp body)"
and cb: "bd_cts (wp body)"
shows "bd_cts_tr (λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip))" (is "bd_cts_tr ?F")
proof(rule bd_cts_trI, rule le_trans_antisym)
fix M::"nat ⇒ 's trans" and b::real
assume chain: "⋀i. le_trans (M i) (M (Suc i))"
and fM: "⋀i. feasible (M i)"
show fw: "le_trans (Sup_trans (range (?F o M))) (?F (Sup_trans (range M)))"
proof(rule le_transI[OF Sup_trans_least2], clarsimp)
fix P Q::"'s expect" and t
assume sP: "sound P"
assume nQ: "nneg Q" and bP: "bounded_by (bound_of P) Q"
hence sQ: "sound Q" by(auto)
from fM have fSup: "feasible (Sup_trans (range M))"
by(auto intro:feasible_Sup_trans)
from sQ fM have "M t Q ⊩ Sup_trans (range M) Q"
by(auto intro:Sup_trans_upper2)
moreover from sQ fM fSup
have sMtP: "sound (M t Q)" "sound (Sup_trans (range M) Q)" by(auto)
ultimately have "wp body (M t Q) ⊩ wp body (Sup_trans (range M) Q)"
using healthy_monoD[OF hb] by(auto)
hence "⋀s. wp body (M t Q) s ≤ wp body (Sup_trans (range M) Q) s"
by(rule le_funD)
thus "?F (M t) Q ⊩ ?F (Sup_trans (range M)) Q"
by(intro le_funI, simp add:wp_eval mult_left_mono)
show "nneg (wp (body ;; Embed (Sup_trans (range M)) ⇘« G »⇙⊕ Skip) Q)"
proof(rule nnegI, simp add:wp_eval)
fix s::'s
from fSup sQ have "sound (Sup_trans (range M) Q)" by(auto)
with hb have "sound (wp body (Sup_trans (range M) Q))" by(auto)
hence "0 ≤ wp body (Sup_trans (range M) Q) s" by(auto)
moreover from sQ have "0 ≤ Q s" by(auto)
ultimately show "0 ≤ «G» s * wp body (Sup_trans (range M) Q) s + (1 - «G» s) * Q s"
by(auto intro:add_nonneg_nonneg mult_nonneg_nonneg)
qed
next
fix P::"'s expect" assume sP: "sound P"
thus "nneg P" "bounded_by (bound_of P) P" by(auto)
show "∀u∈range ((λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip)) ∘ M).
∀R. nneg R ∧ bounded_by (bound_of P) R ⟶
nneg (u R) ∧ bounded_by (bound_of P) (u R)"
proof(clarsimp, intro conjI nnegI bounded_byI, simp_all add:wp_eval)
fix u::nat and R::"'s expect" and s::'s
assume nR: "nneg R" and bR: "bounded_by (bound_of P) R"
hence sR: "sound R" by(auto)
with fM have sMuR: "sound (M u R)" by(auto)
with hb have "sound (wp body (M u R))" by(auto)
hence "0 ≤ wp body (M u R) s" by(auto)
moreover from nR have "0 ≤ R s" by(auto)
ultimately show "0 ≤ «G» s * wp body (M u R) s + (1 - «G» s) * R s"
by(auto intro:add_nonneg_nonneg mult_nonneg_nonneg)
from sR bR fM have "bounded_by (bound_of P) (M u R)" by(auto)
with sMuR hb have "bounded_by (bound_of P) (wp body (M u R))" by(auto)
hence "wp body (M u R) s ≤ bound_of P" by(auto)
moreover from bR have "R s ≤ bound_of P" by(auto)
ultimately have "«G» s * wp body (M u R) s + (1 - «G» s) * R s ≤
«G» s * bound_of P + (1 - «G» s) * bound_of P"
by(auto intro:add_mono mult_left_mono)
also have "... = bound_of P" by(simp add:algebra_simps)
finally show "«G» s * wp body (M u R) s + (1 - «G» s) * R s ≤ bound_of P" .
qed
qed
show "le_trans (?F (Sup_trans (range M))) (Sup_trans (range (?F o M)))"
proof(rule le_transI, rule le_funI, simp add: wp_eval cong del: image_cong_simp)
fix P::"'s expect" and s::'s
assume sP: "sound P"
have "{t P |t. t ∈ range M} = range (λi. M i P)"
by(blast)
hence "wp body (Sup_trans (range M) P) s = wp body (Sup_exp (range (λi. M i P))) s"
by(simp add:Sup_trans_def)
also {
from sP fM have "⋀i. sound (M i P)" by(auto)
moreover from sP chain have "⋀i. M i P ⊩ M (Suc i) P" by(auto)
moreover {
from sP have "bounded_by (bound_of P) P" by(auto)
with sP fM have "⋀i. bounded_by (bound_of P) (M i P)" by(auto)
}
ultimately have "wp body (Sup_exp (range (λi. M i P))) s =
Sup_exp (range (λi. wp body (M i P))) s"
by(subst bd_ctsD[OF cb], auto simp:o_def)
}
also have "Sup_exp (range (λi. wp body (M i P))) s =
Sup {f s |f. f ∈ range (λi. wp body (M i P))}"
by(simp add:Sup_exp_def)
finally have "«G» s * wp body (Sup_trans (range M) P) s + (1 - «G» s) * P s =
«G» s * Sup {f s |f. f ∈ range (λi. wp body (M i P))} + (1 - «G» s) * P s"
by(simp)
also {
from sP fM have "⋀i. sound (M i P)" by(auto)
moreover from sP fM have "⋀i. bounded_by (bound_of P) (M i P)" by(auto)
ultimately have "⋀i. bounded_by (bound_of P) (wp body (M i P))" using hb by(auto)
hence bound: "⋀i. wp body (M i P) s ≤ bound_of P" by(auto)
moreover
have "{« G » s * x |x. x ∈ {f s |f. f ∈ range (λi. wp body (M i P))}} =
{« G » s * f s |f. f ∈ range (λi. wp body (M i P))}"
by(blast)
ultimately
have "«G» s * Sup {f s |f. f ∈ range (λi. wp body (M i P))} =
Sup {«G» s * f s |f. f ∈ range (λi. wp body (M i P))}"
by(subst cSup_mult, auto)
moreover {
have "{x + (1-«G» s) * P s |x.
x ∈ {«G» s * f s |f. f ∈ range (λi. wp body (M i P))}} =
{«G» s * f s + (1-«G» s) * P s |f. f ∈ range (λi. wp body (M i P))}"
by(blast)
moreover from bound sP have "⋀i. «G» s * wp body (M i P) s ≤ bound_of P"
by(cases "G s", auto)
ultimately
have "Sup {«G» s * f s |f. f ∈ range (λi. wp body (M i P))} + (1-«G» s) * P s =
Sup {«G» s * f s + (1-«G» s) * P s |f. f ∈ range (λi. wp body (M i P))}"
by(subst cSup_add, auto)
}
ultimately
have "«G» s * Sup {f s |f. f ∈ range (λi. wp body (M i P))} + (1-«G» s) * P s =
Sup {«G» s * f s + (1-«G» s) * P s |f. f ∈ range (λi. wp body (M i P))}"
by(simp)
}
also {
have "⋀i. «G» s * wp body (M i P) s + (1-«G» s) * P s =
((λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip)) ∘ M) i P s"
by(simp add:wp_eval)
also have "⋀i. ... i ≤
Sup {f s |f. f ∈ {t P |t. t ∈ range ((λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip)) ∘ M)}}"
proof(intro cSup_upper bdd_aboveI, blast, clarsimp simp:wp_eval)
fix i
from sP have bP: "bounded_by (bound_of P) P" by(auto)
with sP fM have "sound (M i P)" "bounded_by (bound_of P) (M i P)" by(auto)
with hb have "bounded_by (bound_of P) (wp body (M i P))" by(auto)
with bP have "wp body (M i P) s ≤ bound_of P" "P s ≤ bound_of P" by(auto)
hence "«G» s * wp body (M i P) s + (1-«G» s) * P s ≤
«G» s * (bound_of P) + (1-«G» s) * (bound_of P)"
by(auto intro:add_mono mult_left_mono)
also have "... = bound_of P" by(simp add:algebra_simps)
finally show "«G» s * wp body (M i P) s + (1-«G» s) * P s ≤ bound_of P" .
qed
finally
have "Sup {«G» s * f s + (1-«G» s) * P s |f. f ∈ range (λi. wp body (M i P))} ≤
Sup {f s |f. f ∈ {t P |t. t ∈ range ((λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip)) ∘ M)}}"
by(blast intro:cSup_least)
}
also have "Sup {f s |f. f ∈ {t P |t. t ∈ range ((λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip)) ∘ M)}} =
Sup_trans (range ((λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip)) ∘ M)) P s"
by(simp add:Sup_trans_def Sup_exp_def)
finally show "«G» s * wp body (Sup_trans (range M) P) s + (1-«G» s) * P s ≤
Sup_trans (range ((λx. wp (body ;; Embed x ⇘« G »⇙⊕ Skip)) ∘ M)) P s" .
qed
qed
end