# Theory Misc

(*
*)

(* Author: David Cock - David.Cock@nicta.com.au *)

section ‹Miscellaneous Mathematics›

theory Misc
imports
"HOL-Analysis.Multivariate_Analysis"
begin

text_raw ‹\label{s:misc}›

lemma sum_UNIV:
fixes S::"'a::finite set"
assumes complete: "⋀x. x∉S ⟹ f x = 0"
shows "sum f S = sum f UNIV"
proof -
from complete have "sum f S = sum f (UNIV - S) + sum f S" by(simp)
also have "... = sum f UNIV"
by(auto intro: sum.subset_diff[symmetric])
finally show ?thesis .
qed

lemma cInf_mono:
fixes A::"'a::conditionally_complete_lattice set"
assumes lower: "⋀b. b ∈ B ⟹ ∃a∈A. a ≤ b"
and bounded: "⋀a. a ∈ A ⟹ c ≤ a"
and ne: "B ≠ {}"
shows "Inf A ≤ Inf B"
proof(rule cInf_greatest[OF ne])
fix b assume bin: "b ∈ B"
with lower obtain a where ain: "a ∈ A" and le: "a ≤ b" by(auto)
from ain bounded have "Inf A ≤ a" by(intro cInf_lower bdd_belowI, auto)
also note le
finally show "Inf A ≤ b" .
qed

lemma max_distrib:
fixes c::real
assumes nn: "0 ≤ c"
shows "c * max a b = max (c * a) (c * b)"
proof(cases "a ≤ b")
case True
moreover with nn have "c * a ≤ c * b" by(auto intro:mult_left_mono)
next
case False then have "b ≤ a" by(auto)
moreover with nn have "c * b ≤ c * a" by(auto intro:mult_left_mono)
qed

lemma mult_div_mono_left:
fixes c::real
assumes nnc: "0 ≤ c" and nzc: "c ≠ 0"
and inv: "a ≤ inverse c * b"
shows "c * a ≤ b"
proof -
from nnc inv have "c * a ≤ (c * inverse c) * b"
by(auto simp:mult.assoc intro:mult_left_mono)
also from nzc have "... = b" by(simp)
finally show "c * a ≤ b" .
qed

lemma mult_div_mono_right:
fixes c::real
assumes nnc: "0 ≤ c" and nzc: "c ≠ 0"
and inv: "inverse c * a ≤ b"
shows "a ≤ c * b"
proof -
from nzc have "a = (c * inverse c) * a " by(simp)
also from nnc inv have "(c * inverse c) * a ≤ c * b"
by(auto simp:mult.assoc intro:mult_left_mono)
finally show "a ≤ c * b" .
qed

lemma min_distrib:
fixes c::real
assumes nnc: "0 ≤ c"
shows "c * min a b = min (c * a) (c * b)"
proof(cases "a ≤ b")
case True moreover with nnc have "c * a ≤ c * b"
by(blast intro:mult_left_mono)
ultimately show ?thesis by(auto)
next
case False hence "b ≤ a" by(auto)
moreover with nnc have "c * b ≤ c * a"
by(blast intro:mult_left_mono)
qed

lemma finite_set_least:
fixes S::"'a::linorder set"
assumes finite: "finite S"
and ne: "S ≠ {}"
shows "∃x∈S. ∀y∈S. x ≤ y"
proof -
have "S = {} ∨ (∃x∈S. ∀y∈S. x ≤ y)"
fix x::'a and S::"'a set"
assume IH: "S = {} ∨ (∃x∈S. ∀y∈S. x ≤ y)"
show "(∀y∈S. x ≤ y) ∨ (∃x'∈S. x' ≤ x ∧ (∀y∈S. x' ≤ y))"
proof(cases "S={}")
case True then show ?thesis by(auto)
next
case False with IH have "∃x∈S. ∀y∈S. x ≤ y" by(auto)
then obtain z where zin: "z ∈ S" and zmin: "∀y∈S. z ≤ y" by(auto)
thus ?thesis by(cases "z ≤ x", auto)
qed
qed
with ne show ?thesis by(auto)
qed

fixes c::real
assumes ne: "S ≠ {}"
and bS: "⋀x. x∈S ⟹ x ≤ b"
shows "Sup S + c = Sup {x + c |x. x ∈ S}"
proof(rule antisym)
from ne bS show "Sup {x + c |x. x ∈ S} ≤ Sup S + c"

have "Sup S ≤ Sup {x + c |x. x ∈ S} - c"
proof(intro cSup_least ne)
fix x assume xin: "x ∈ S"
from bS have "⋀x. x∈S ⟹ x + c ≤ b + c" by(auto intro:add_right_mono)
hence "bdd_above {x + c |x. x ∈ S}" by(intro bdd_aboveI, blast)
with xin have "x + c ≤ Sup {x + c |x. x ∈ S}" by(auto intro:cSup_upper)
thus "x ≤ Sup {x + c |x. x ∈ S} - c" by(auto)
qed
thus "Sup S + c ≤ Sup {x + c |x. x ∈ S}" by(auto)
qed

lemma cSup_mult:
fixes c::real
assumes ne: "S ≠ {}"
and bS: "⋀x. x∈S ⟹ x ≤ b"
and nnc: "0 ≤ c"
shows "c * Sup S = Sup {c * x |x. x ∈ S}"
proof(cases)
assume "c = 0"
moreover from ne have "∃x. x ∈ S" by(auto)
ultimately show ?thesis by(simp)
next
assume cnz: "c ≠ 0"
show ?thesis
proof(rule antisym)
from bS have baS: "bdd_above S" by(intro bdd_aboveI, auto)
with ne nnc show "Sup {c * x |x. x ∈ S} ≤ c * Sup S"
by(blast intro!:cSup_least mult_left_mono[OF cSup_upper])
have "Sup S ≤ inverse c * Sup {c * x |x. x ∈ S}"
proof(intro cSup_least ne)
fix x assume xin: "x∈S"
moreover from bS nnc have "⋀x. x∈S ⟹ c * x ≤ c * b" by(auto intro:mult_left_mono)
ultimately have "c * x ≤ Sup {c * x |x. x ∈ S}"
by(auto intro!:cSup_upper bdd_aboveI)
moreover from nnc have "0 ≤ inverse c" by(auto)
ultimately have "inverse c * (c * x) ≤ inverse c * Sup {c * x |x. x ∈ S}"
by(auto intro:mult_left_mono)
with cnz show "x ≤ inverse c * Sup {c * x |x. x ∈ S}"
qed
with nnc have "c * Sup S ≤ c * (inverse c * Sup {c * x |x. x ∈ S})"
by(auto intro:mult_left_mono)
with cnz show "c * Sup S ≤ Sup {c * x |x. x ∈ S}"
qed
qed

lemma closure_contains_Sup:
fixes S :: "real set"
assumes neS: "S ≠ {}" and bS: "∀x∈S. x ≤ B"
shows "Sup S ∈ closure S"
proof -
let ?T = "uminus  S"
from neS have neT: "?T ≠ {}" by(auto)
from bS have bT: "∀x∈?T. -B ≤ x" by(auto)
hence bbT: "bdd_below ?T" by(intro bdd_belowI, blast)

have "Sup S = - Inf ?T"
proof(rule antisym)
from neT bbT
have "⋀x. x∈S ⟹ Inf (uminus  S) ≤ -x"
by(blast intro:cInf_lower)
hence "⋀x. x∈S ⟹ -1 * -x ≤ -1 * Inf (uminus  S)"
by(rule mult_left_mono_neg, auto)
hence lenInf: "⋀x. x∈S ⟹ x ≤ - Inf (uminus  S)"
by(simp)
with neS bS show "Sup S ≤ - Inf ?T"
by(blast intro:cSup_least)

have "- Sup S ≤ Inf ?T"
proof(rule cInf_greatest[OF neT])
fix x assume "x ∈ uminus  S"
then obtain y where yin: "y ∈ S" and rwx: "x = -y" by(auto)
from yin bS have "y ≤ Sup S"
by(intro cSup_upper bdd_belowI, auto)
hence "-1 * Sup S ≤ -1 * y"
with rwx show "- Sup S ≤ x" by(simp)
qed
hence "-1 * Inf ?T ≤ -1 * (- Sup S)"
thus "- Inf ?T ≤ Sup S" by(simp)
qed
also {
from neT bbT have "Inf ?T ∈ closure ?T" by(rule closure_contains_Inf)
hence "- Inf ?T ∈ uminus  closure ?T" by(auto)
}
also {
have "linear uminus" by(auto intro:linearI)
hence "uminus  closure ?T ⊆ closure (uminus  ?T)"
by(rule closure_linear_image_subset)
}
also {
have "uminus  ?T ⊆ S" by(auto)
hence "closure (uminus  ?T) ⊆ closure S" by(rule closure_mono)
}
finally show "Sup S ∈ closure S" .
qed

lemma tendsto_min:
fixes x y::real
assumes ta: "a ⇢ x"
and tb: "b ⇢ y"
shows "(λi. min (a i) (b i)) ⇢ min x y"
proof(rule LIMSEQ_I, simp)
fix e::real assume pe: "0 < e"

from ta pe obtain noa where balla: "∀n≥noa. abs (a n - x) < e"
by(auto dest:LIMSEQ_D)
from tb pe obtain nob where ballb: "∀n≥nob. abs (b n - y) < e"
by(auto dest:LIMSEQ_D)

{
fix n
assume ge: "max noa nob ≤ n"
hence gea: "noa ≤ n" and geb: "nob ≤ n" by(auto)
have "abs (min (a n) (b n) - min x y) < e"
proof cases
assume le: "min (a n) (b n) ≤ min x y"
show ?thesis
proof cases
assume "a n ≤ b n"
hence rwmin: "min (a n) (b n) = a n" by(auto)
with le have "a n ≤ min x y" by(simp)
moreover from gea balla have "abs (a n - x) < e" by(simp)
moreover have "min x y ≤ x" by(auto)
ultimately have "abs (a n - min x y) < e" by(auto)
with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
next
assume "¬ a n ≤ b n"
hence "b n ≤ a n" by(auto)
hence rwmin: "min (a n) (b n) = b n" by(auto)
with le have "b n ≤ min x y" by(simp)
moreover from geb ballb have "abs (b n - y) < e" by(simp)
moreover have "min x y ≤ y" by(auto)
ultimately have "abs (b n - min x y) < e" by(auto)
with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
qed
next
assume "¬ min (a n) (b n) ≤ min x y"
hence le: "min x y ≤ min (a n) (b n)" by(auto)
show ?thesis
proof cases
assume "x ≤ y"
hence rwmin: "min x y = x" by(auto)
with le have "x ≤ min (a n) (b n)" by(simp)
moreover from gea balla have "abs (a n - x) < e" by(simp)
moreover have "min (a n) (b n) ≤ a n" by(auto)
ultimately have "abs (min (a n) (b n) - x) < e" by(auto)
with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
next
assume "¬ x ≤ y"
hence "y ≤ x" by(auto)
hence rwmin: "min x y = y" by(auto)
with le have "y ≤ min (a n) (b n)" by(simp)
moreover from geb ballb have "abs (b n - y) < e" by(simp)
moreover have "min (a n) (b n) ≤ b n" by(auto)
ultimately have "abs (min (a n) (b n) - y) < e" by(auto)
with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
qed
qed
}
thus "∃no. ∀n≥no. ¦min (a n) (b n) - min x y¦ < e" by(blast)
qed

definition supp :: "('s ⇒ real) ⇒ 's set"
where "supp f = {x. f x ≠ 0}"

definition dist_remove :: "('s ⇒ real) ⇒ 's ⇒ 's ⇒ real"
where "dist_remove p x = (λy. if y=x then 0 else p y / (1 - p x))"

lemma supp_dist_remove:
"p x ≠ 0 ⟹ p x ≠ 1 ⟹ supp (dist_remove p x) = supp p - {x}"
by(auto simp:dist_remove_def supp_def)

lemma supp_empty:
"supp f = {} ⟹ f x = 0"

lemma nsupp_zero:
"x ∉ supp f ⟹ f x = 0"

lemma sum_supp:
fixes f::"'a::finite ⇒ real"
shows "sum f (supp f) = sum f UNIV"
proof -
have "sum f (UNIV - supp f) = 0"
hence "sum f (supp f) = sum f (UNIV - supp f) + sum f (supp f)"
by(simp)
also have "... = sum f UNIV"
finally show ?thesis .
qed

subsection ‹Truncated Subtraction›
text_raw ‹\label{s:trunc_sub}›

definition
tminus :: "real ⇒ real ⇒ real" (infixl "⊖" 60)
where
"x ⊖ y = max (x - y) 0"

lemma minus_le_tminus[intro!,simp]:
"a - b ≤ a ⊖ b"
unfolding tminus_def by(auto)

lemma tminus_cancel_1:
"0 ≤ a ⟹ a + 1 ⊖ 1 = a"
unfolding tminus_def by(simp)

lemma tminus_zero_imp_le:
"x ⊖ y ≤ 0 ⟹ x ≤ y"

lemma tminus_zero[simp]:
"0 ≤ x ⟹ x ⊖ 0 = x"

lemma tminus_left_mono:
"a ≤ b ⟹ a ⊖ c ≤ b ⊖ c"
unfolding tminus_def
by(case_tac "a ≤ c", simp_all)

lemma tminus_less:
"⟦ 0 ≤ a; 0 ≤ b ⟧ ⟹ a ⊖ b ≤ a"
unfolding tminus_def by(force)

lemma tminus_left_distrib:
assumes nna: "0 ≤ a"
shows "a * (b ⊖ c) = a * b ⊖ a * c"
proof(cases "b ≤ c")
case True note le = this
hence "a * max (b - c) 0 = 0" by(simp add:max.absorb2)
also {
from nna le have "a * b ≤ a * c" by(blast intro:mult_left_mono)
hence "0 = max (a * b - a * c) 0" by(simp add:max.absorb1)
}
next
case False hence le: "c ≤ b" by(auto)
hence "a * max (b - c) 0 = a * (b - c)" by(simp only:max.absorb1)
also {
from nna le have "a * c ≤ a * b" by(blast intro:mult_left_mono)
hence "a * (b - c) = max (a * b - a * c) 0" by(simp add:max.absorb1 field_simps)
}
qed

lemma tminus_le[simp]:
"b ≤ a ⟹ a ⊖ b = a - b"
unfolding tminus_def by(simp)

lemma tminus_le_alt[simp]:
"a ≤ b ⟹ a ⊖ b = 0"

lemma tminus_nle[simp]:
"¬b ≤ a ⟹ a ⊖ b = 0"
unfolding tminus_def by(simp)

"(a+b) ⊖ (c+d) ≤ (a⊖c) + (b⊖d)"
proof(cases "0 ≤ a - c")
case True note pac = this
show ?thesis
proof(cases "0 ≤ b - d")
case True note pbd = this
from pac and pbd have "(c + d) ≤ (a + b)" by(simp)
with pac and pbd show ?thesis by(simp)
next
case False with pac show ?thesis
by(cases "c + d ≤ a + b", auto)
qed
next
case False note nac = this
show ?thesis
proof(cases "0 ≤ b - d")
case True with nac show ?thesis
by(cases "c + d ≤ a + b", auto)
next
case False note nbd = this
with nac have "¬(c + d) ≤ (a + b)" by(simp)
with nac and nbd show ?thesis by(simp)
qed
qed

lemma tminus_sum_mono:
assumes fS: "finite S"
shows "sum f S ⊖ sum g S ≤ sum (λx. f x ⊖ g x) S"
(is "?X S")
proof(rule finite_induct)
from fS show "finite S" .

show "?X {}" by(simp)

fix x and F
assume fF: "finite F" and xniF: "x ∉ F"
and IH: "?X F"
have "f x + sum f F ⊖ g x + sum g F ≤
(f x ⊖ g x) + (sum f F ⊖ sum g F)"
also from IH have "... ≤ (f x ⊖ g x) + (∑x∈F. f x ⊖ g x)"
finally show "?X (insert x F)"
qed

lemma tminus_nneg[simp,intro]:
"0 ≤ a ⊖ b"
by(cases "b ≤ a", auto)

lemma tminus_right_antimono:
assumes clb: "c ≤ b"
shows "a ⊖ b ≤ a ⊖ c"
proof(cases "b ≤ a")
case True
moreover with clb have "c ≤ a" by(auto)
moreover note clb
ultimately show ?thesis by(simp)
next
case False then show ?thesis by(simp)
qed

lemma min_tminus_distrib:
"min a b ⊖ c = min (a ⊖ c) (b ⊖ c)"
unfolding tminus_def by(auto)

end


# Theory Expectations

(*
*)

(* Author: David Cock - David.Cock@nicta.com.au *)

section "Expectations"

theory Expectations imports Misc begin

text_raw ‹\label{s:expectations}›

type_synonym 's expect = "'s ⇒ real"

text ‹Expectations are a real-valued generalisation of boolean predicates: An expectation on state
@{typ 's} is a function @{typ "'s ⇒ real"}. A predicate @{term P} on @{typ 's} is embedded as an
expectation by mapping @{term True} to 1 and @{term False} to 0.  Under this embedding, implication
becomes comparison, as the truth tables demonstrate:
\begin{center}
\begin{tabular}{ccc|ccc}
$a$ & $b$ & $a \rightarrow b$ & $x$ & $y$ & $x \le y$ \\
F  &  F  &  T                &  0  &  0  &  T \\
F  &  T  &  T                &  0  &  1  &  T \\
T  &  F  &  F                &  1  &  0  &  F \\
T  &  T  &  T                &  1  &  1  &  T
\end{tabular}
\end{center}

\begin{figure}
\begin{center}
\mbox{
\xymatrix{
*++[o][F=]{b} & & *++[o][F=]{c} \\
& *++[o][F-]{a} \ar[ul]^{0.7} \ar[ur]_{0.3} \\
& \ar[u]
}
}
\end{center}
\caption{\label{f:automaton_1}A probabilistic automaton}
\end{figure}

For probabilistic automata, an expectation gives the current expected value of some expression, if
it were to be evaluated in the final state. For example, consider the automaton of
\autoref{f:automaton_1}, with transition probabilities affixed to edges. Let $P\ b = 2.0$ and $P\ c = 3.0$. Both states $b$ and $c$ are final (accepting) states, and thus the final expected value' of
$P$ in state $b$ is $2.0$ and in state $c$ is $3.0$. The expected value from state $a$ is the
weighted sum of these, or $0.7 \times 2.0 + 0.3 \times 3.0 = 2.3$.

All expectations must be non-negative and bounded i.e. $\forall s.~0 \le P\ s$ and $\exists b. \forall s. P\ s \le b$. Note that although every expectation must have a bound, there is no bound on
all expectations; In particular, the following series has no global bound, although each element is
clearly bounded:
\begin{displaymath}
P_i = \lambda s.\ i\quad\text{where}\ i \in \mathbb{N}
\end{displaymath}
›

subsection ‹Bounded Functions›

definition bounded_by :: "real ⇒ ('a ⇒ real) ⇒ bool"
where     "bounded_by b P ≡ ∀x. P x ≤ b"

text ‹By instantiating the classical reasoner, both establishing and appealing to boundedness
is largely automatic.›

lemma bounded_byI[intro]:
"⟦ ⋀x. P x ≤ b ⟧ ⟹ bounded_by b P"

lemma bounded_byI2[intro]:
"P ≤ (λs. b) ⟹ bounded_by b P"
by (blast dest:le_funD)

lemma bounded_byD[dest]:
"bounded_by b P ⟹ P x ≤ b"

lemma bounded_byD2[dest]:
"bounded_by b P ⟹ P ≤ (λs. b)"
by (blast intro:le_funI)

text ‹A function is bounded if there exists at least one upper bound on it.›

definition bounded :: "('a ⇒ real) ⇒ bool"
where     "bounded P ≡ (∃b. bounded_by b P)"

text ‹In the reals, if there exists any upper bound, then there must exist a least upper bound.›

definition bound_of :: "('a ⇒ real) ⇒ real"
where     "bound_of P ≡ Sup (P  UNIV)"

lemma bounded_bdd_above[intro]:
assumes bP: "bounded P"
shows "bdd_above (range P)"
proof
fix x assume "x ∈ range P"
with bP show "x ≤ Inf {b. bounded_by b P}"
unfolding bounded_def by(auto intro:cInf_greatest)
qed

text ‹The least upper bound has the usual properties:›
lemma bound_of_least[intro]:
assumes bP: "bounded_by b P"
shows "bound_of P ≤ b"
unfolding bound_of_def
using bP by(intro cSup_least, auto)

lemma bounded_by_bound_of[intro!]:
fixes P::"'a ⇒ real"
assumes bP: "bounded P"
shows "bounded_by (bound_of P) P"
unfolding bound_of_def
using bP by(intro bounded_byI cSup_upper bounded_bdd_above, auto)

lemma bound_of_greater[intro]:
"bounded P ⟹ P x ≤ bound_of P"
by (blast intro:bounded_byD)

lemma bounded_by_mono:
"⟦ bounded_by a P; a ≤ b ⟧ ⟹ bounded_by b P"
unfolding bounded_by_def by(blast intro:order_trans)

lemma bounded_by_imp_bounded[intro]:
"bounded_by b P ⟹ bounded P"
unfolding bounded_def by(blast)

text ‹This is occasionally easier to apply:›

lemma bounded_by_bound_of_alt:
"⟦ bounded P; bound_of P = a ⟧ ⟹ bounded_by a P"
by (blast)

lemma bounded_const[simp]:
"bounded (λx. c)"
by (blast)

lemma bounded_by_const[intro]:
"c ≤ b ⟹ bounded_by b (λx. c)"
by (blast)

lemma bounded_by_mono_alt[intro]:
"⟦ bounded_by b Q; P ≤ Q ⟧ ⟹ bounded_by b P"
by (blast intro:order_trans dest:le_funD)

lemma bound_of_const[simp, intro]:
"bound_of (λx. c) = (c::real)"
unfolding bound_of_def
by(intro antisym cSup_least cSup_upper bounded_bdd_above bounded_const, auto)

lemma bound_of_leI:
assumes "⋀x. P x ≤ (c::real)"
shows "bound_of P ≤ c"
unfolding bound_of_def
using assms by(intro cSup_least, auto)

lemma bound_of_mono[intro]:
"⟦ P ≤ Q; bounded P; bounded Q ⟧ ⟹ bound_of P ≤ bound_of Q"
by (blast intro:order_trans dest:le_funD)

lemma bounded_by_o[intro,simp]:
"⋀b. bounded_by b P ⟹ bounded_by b (P o f)"
unfolding o_def by(blast)

lemma le_bound_of[intro]:
"⋀x. bounded f ⟹ f x ≤ bound_of f"
by(blast)

subsection ‹Non-Negative Functions.›

text ‹The definitions for non-negative functions are analogous to those for bounded functions.›

definition
nneg :: "('a ⇒ 'b::{zero,order}) ⇒ bool"
where
"nneg P ⟷ (∀x. 0 ≤ P x)"

lemma nnegI[intro]:
"⟦ ⋀x. 0 ≤ P x ⟧ ⟹ nneg P"

lemma nnegI2[intro]:
"(λs. 0) ≤ P ⟹ nneg P"
by (blast dest:le_funD)

lemma nnegD[dest]:
"nneg P ⟹ 0 ≤ P x"

lemma nnegD2[dest]:
"nneg P ⟹ (λs. 0) ≤ P"
by (blast intro:le_funI)

lemma nneg_bdd_below[intro]:
"nneg P ⟹ bdd_below (range P)"
by(auto)

lemma nneg_const[iff]:
"nneg (λx. c) ⟷ 0 ≤ c"

lemma nneg_o[intro,simp]:
"nneg P ⟹ nneg (P o f)"
by (force)

lemma nneg_bound_nneg[intro]:
"⟦ bounded P; nneg P ⟧ ⟹ 0 ≤ bound_of P"
by (blast intro:order_trans)

lemma nneg_bounded_by_nneg[dest]:
"⟦ bounded_by b P; nneg P ⟧ ⟹ 0 ≤ (b::real)"
by (blast intro:order_trans)

lemma bounded_by_nneg[dest]:
fixes P::"'s ⇒ real"
shows "⟦ bounded_by b P; nneg P ⟧ ⟹ 0 ≤ b"
by (blast intro:order_trans)

subsection ‹Sound Expectations›

definition sound :: "('s ⇒ real) ⇒ bool"
where "sound P ≡ bounded P ∧ nneg P"

text ‹Combining @{term nneg} and @{term bounded}, we have @{term sound} expectations. We set up
the classical reasoner and the simplifier, such that showing soundess, or deriving a simple
consequence (e.g. @{term "sound P ⟹ 0 ≤ P s"}) will usually follow by blast, force or simp.›

lemma soundI:
"⟦ bounded P; nneg P ⟧ ⟹ sound P"

lemma soundI2[intro]:
"⟦ bounded_by b P; nneg P ⟧ ⟹ sound P"
by(blast intro:soundI)

lemma sound_bounded[dest]:
"sound P ⟹ bounded P"

lemma sound_nneg[dest]:
"sound P ⟹ nneg P"

lemma bound_of_sound[intro]:
assumes sP: "sound P"
shows "0 ≤ bound_of P"
using assms by(auto)

text ‹This proof demonstrates the use of the classical reasoner (specifically blast), to both
introduce and eliminate soundness terms.›

lemma sound_sum[simp,intro]:
assumes sP: "sound P" and sQ: "sound Q"
shows "sound (λs. P s + Q s)"
proof
from sP have "⋀s. P s ≤ bound_of P" by(blast)
moreover from sQ have "⋀s. Q s ≤ bound_of Q" by(blast)
ultimately have "⋀s. P s + Q s ≤ bound_of P + bound_of Q"
thus "bounded_by (bound_of P + bound_of Q) (λs. P s + Q s)"
by(blast)

from sP have "⋀s. 0 ≤ P s" by(blast)
moreover from sQ have "⋀s. 0 ≤ Q s" by(blast)
ultimately have "⋀s. 0 ≤ P s + Q s" by(simp add:add_mono)
thus "nneg (λs. P s + Q s)" by(blast)
qed

lemma mult_sound:
assumes sP: "sound P" and sQ: "sound Q"
shows "sound (λs. P s * Q s)"
proof
from sP have "⋀s. P s ≤ bound_of P" by(blast)
moreover from sQ have "⋀s. Q s ≤ bound_of Q" by(blast)
ultimately have "⋀s. P s * Q s ≤ bound_of P * bound_of Q"
using sP and sQ by(blast intro:mult_mono)
thus "bounded_by (bound_of P * bound_of Q) (λs. P s * Q s)" by(blast)

from sP and sQ show "nneg (λs. P s * Q s)"
by(blast intro:mult_nonneg_nonneg)
qed

lemma div_sound:
assumes sP: "sound P" and cpos: "0 < c"
shows "sound (λs. P s / c)"
proof
from sP and cpos have "⋀s. P s / c ≤ bound_of P / c"
by(blast intro:divide_right_mono less_imp_le)
thus "bounded_by (bound_of P / c) (λs. P s / c)" by(blast)
from assms show "nneg (λs. P s / c)"
by(blast intro:divide_nonneg_pos)
qed

lemma tminus_sound:
assumes sP: "sound P" and nnc: "0 ≤ c"
shows "sound (λs. P s ⊖ c)"
proof(rule soundI)
from sP have "⋀s. P s ≤ bound_of P" by(blast)
with nnc have "⋀s. P s ⊖ c ≤ bound_of P ⊖ c"
by(blast intro:tminus_left_mono)
thus "bounded (λs. P s ⊖ c)" by(blast)
show "nneg (λs. P s ⊖ c)" by(blast)
qed

lemma const_sound:
"0 ≤ c ⟹ sound (λs. c)"
by (blast)

lemma sound_o[intro,simp]:
"sound P ⟹ sound (P o f)"
unfolding o_def by(blast)

lemma sc_bounded_by[intro,simp]:
"⟦ sound P; 0 ≤ c ⟧ ⟹ bounded_by (c * bound_of P) (λx. c * P x)"
by(blast intro!:mult_left_mono)

lemma sc_bounded[intro,simp]:
assumes sP:  "sound P" and pos: "0 ≤ c"
shows "bounded (λx. c * P x)"
using assms by(blast)

lemma sc_bound[simp]:
assumes sP: "sound P"
and cnn: "0 ≤ c"
shows "c * bound_of P = bound_of (λx. c * P x)"
proof(cases "c = 0")
case True then show ?thesis by(simp)
next
case False with cnn have cpos: "0 < c" by(auto)
show ?thesis
proof (rule antisym)
from sP and cnn have "bounded (λx. c * P x)" by(simp)
hence "⋀x. c * P x ≤ bound_of (λx. c * P x)"
by(rule le_bound_of)
with cpos have "⋀x. P x ≤ inverse c * bound_of (λx. c * P x)"
by(force intro:mult_div_mono_right)
hence "bound_of P ≤ inverse c * bound_of (λx. c * P x)"
by(blast)
with cpos show "c * bound_of P ≤ bound_of (λx. c * P x)"
by(force intro:mult_div_mono_left)
next
from sP and cpos have "⋀x. c * P x ≤ c * bound_of P"
by(blast intro:mult_left_mono less_imp_le)
thus "bound_of (λx. c * P x) ≤ c * bound_of P"
by(blast)
qed
qed

lemma sc_sound:
"⟦ sound P; 0 ≤ c ⟧ ⟹ sound (λs. c * P s)"
by (blast intro:mult_nonneg_nonneg)

lemma bounded_by_mult:
assumes sP: "sound P" and bP: "bounded_by a P"
and sQ: "sound Q" and bQ: "bounded_by b Q"
shows "bounded_by (a * b) (λs. P s * Q s)"
using assms by(intro bounded_byI, auto intro:mult_mono)

fixes P::"'s ⇒ real" and Q
assumes bP: "bounded_by a P"
and bQ: "bounded_by b Q"
shows "bounded_by (a + b) (λs. P s + Q s)"
using assms by(intro bounded_byI, auto intro:add_mono)

lemma sound_unit[intro!,simp]:
"sound (λs. 1)"
by(auto)

lemma unit_mult[intro]:
assumes sP: "sound P" and bP: "bounded_by 1 P"
and sQ: "sound Q" and bQ: "bounded_by 1 Q"
shows "bounded_by 1 (λs. P s * Q s)"
proof(rule bounded_byI)
fix s
have "P s * Q s ≤ 1 * 1"
using assms by(blast dest:bounded_by_mult)
thus "P s * Q s ≤ 1" by(simp)
qed

lemma sum_sound:
assumes sP: "∀x∈S. sound (P x)"
shows "sound (λs. ∑x∈S. P x s)"
proof(rule soundI2)
from sP show "bounded_by (∑x∈S. bound_of (P x)) (λs. ∑x∈S. P x s)"
by(auto intro!:sum_mono)
from sP show "nneg (λs. ∑x∈S. P x s)"
by(auto intro!:sum_nonneg)
qed

subsection ‹Unitary expectations›

text ‹A unitary expectation is a sound expectation that is additionally bounded by one.  This
is the domain on which the \emph{liberal} (partial correctness) semantics operates.›

definition unitary :: "'s expect ⇒ bool"
where "unitary P ⟷ sound P ∧ bounded_by 1 P"

lemma unitaryI[intro]:
"⟦ sound P; bounded_by 1 P ⟧ ⟹ unitary P"

lemma unitaryI2:
"⟦ nneg P; bounded_by 1 P ⟧ ⟹ unitary P"
by(auto)

lemma unitary_sound[dest]:
"unitary P ⟹ sound P"

lemma unitary_bound[dest]:
"unitary P ⟹ bounded_by 1 P"

subsection ‹Standard Expectations›
text_raw ‹\label{s:standard}›

definition
embed_bool :: "('s ⇒ bool) ⇒ 's ⇒ real" ("« _ »" 1000)
where
"«P» ≡ (λs. if P s then 1 else 0)"

text ‹Standard expectations are the embeddings of boolean predicates, mapping @{term False} to 0
and @{term True} to 1. We write @{term "«P»"} rather than @{term "[P]"} (the syntax employed by
\citet{McIver_M_04}) for boolean embedding to avoid clashing with the HOL syntax for lists.›

lemma embed_bool_nneg[simp,intro]:
"nneg «P»"
unfolding embed_bool_def by(force)

lemma embed_bool_bounded_by_1[simp,intro]:
"bounded_by 1 «P»"
unfolding embed_bool_def by(force)

lemma embed_bool_bounded[simp,intro]:
"bounded «P»"
by (blast)

text ‹Standard expectations have a number of convenient properties, which mostly follow from
boolean algebra.›

lemma embed_bool_idem:
"«P» s * «P» s = «P» s"

lemma eval_embed_true[simp]:
"P s ⟹ «P» s = 1"

lemma eval_embed_false[simp]:
"¬P s ⟹ «P» s = 0"

lemma embed_ge_0[simp,intro]:
"0 ≤ «G» s"

lemma embed_le_1[simp,intro]:
"«G» s ≤ 1"

lemma embed_le_1_alt[simp,intro]:
"0 ≤ 1 - «G» s"
by(subst add_le_cancel_right[where c="«G» s", symmetric], simp)

lemma expect_1_I:
"P x ⟹ 1 ≤ «P» x"
by(simp)

lemma standard_sound[intro,simp]:
"sound «P»"
by(blast)

lemma embed_o[simp]:
"«P» o f = «P o f»"
unfolding embed_bool_def o_def by(simp)

text ‹Negating a predicate has the expected effect in its
embedding as an expectation:›

definition negate :: "('s ⇒ bool) ⇒ 's ⇒ bool" ("𝒩")
where     "negate P = (λs. ¬ P s)"

lemma negateI:
"¬ P s ⟹ 𝒩 P s"

lemma embed_split:
"f s = «P» s * f s + «𝒩 P» s * f s"

lemma negate_embed:
"«𝒩 P» s = 1 - «P» s"

lemma eval_nembed_true[simp]:
"P s ⟹ «𝒩 P» s = 0"

lemma eval_nembed_false[simp]:
"¬P s ⟹ «𝒩 P» s = 1"

lemma negate_Not[simp]:
"𝒩 Not = (λx. x)"

lemma negate_negate[simp]:
"𝒩 (𝒩 P) = P"

lemma embed_bool_cancel:
"«G» s * «𝒩 G» s = 0"
by(cases "G s", simp_all)

subsection ‹Entailment›
text_raw ‹\label{s:entailment}›

text ‹Entailment on expectations is a generalisation of that on predicates, and is defined by
pointwise comparison:›

abbreviation entails :: "('s ⇒ real) ⇒ ('s ⇒ real) ⇒ bool" ("_ ⊩ _" 50)
where "P ⊩ Q ≡ P ≤ Q"

lemma entailsI[intro]:
"⟦⋀s. P s ≤ Q s⟧ ⟹ P ⊩ Q"

lemma entailsD[dest]:
"P ⊩ Q ⟹ P s ≤ Q s"

lemma eq_entails[intro]:
"P = Q ⟹ P ⊩ Q"
by(blast)

lemma entails_trans[trans]:
"⟦ P ⊩ Q; Q ⊩ R ⟧ ⟹ P ⊩ R"
by(blast intro:order_trans)

text ‹For standard expectations, both notions of entailment coincide. This result justifies the
above claim that our definition generalises predicate entailment:›

lemma implies_entails:
"⟦ ⋀s. P s ⟹ Q s ⟧ ⟹ «P» ⊩ «Q»"
by(rule entailsI, case_tac "P s", simp_all)

lemma entails_implies:
"⋀s. ⟦ «P» ⊩ «Q»; P s ⟧ ⟹ Q s"
by(rule ccontr, drule_tac s=s in entailsD, simp)

subsection ‹Expectation Conjunction›

definition
pconj :: "real ⇒ real ⇒  real" (infixl ".&" 71)
where
"p .& q ≡ p + q ⊖ 1"

definition
exp_conj :: "('s ⇒ real) ⇒ ('s ⇒ real) ⇒ ('s ⇒ real)" (infixl "&&" 71)
where "a && b ≡ λs. (a s .& b s)"

text ‹Expectation conjunction likewise generalises (boolean) predicate conjunction. We show that
the expected properties are preserved, and instantiate both the classical reasoner, and the
simplifier (in the case of associativity and commutativity).›

lemma pconj_lzero[intro,simp]:
"b ≤ 1 ⟹ 0 .& b = 0"

lemma pconj_rzero[intro,simp]:
"b ≤ 1 ⟹ b .& 0 = 0"

lemma pconj_lone[intro,simp]:
"0 ≤ b ⟹ 1 .& b = b"

lemma pconj_rone[intro,simp]:
"0 ≤ b ⟹ b .& 1 = b"

lemma pconj_bconj:
"«a» s .& «b» s = «λs. a s ∧ b s» s"
unfolding embed_bool_def pconj_def tminus_def by(force)

lemma pconj_comm[ac_simps]:
"a .& b = b .& a"

lemma pconj_assoc:
"⟦ 0 ≤ a; a ≤ 1; 0 ≤ b; b ≤ 1; 0 ≤ c; c ≤ 1 ⟧ ⟹
a .& (b .& c) = (a .& b) .& c"
unfolding pconj_def tminus_def by(simp)

lemma pconj_mono:
"⟦ a ≤ b; c ≤ d ⟧ ⟹ a .& c ≤ b .& d"
unfolding pconj_def tminus_def by(simp)

lemma pconj_nneg[intro,simp]:
"0 ≤ a .& b"
unfolding pconj_def tminus_def by(auto)

lemma min_pconj:
"(min a b) .& (min c d) ≤ min (a .& c) (b .& d)"
by(cases "a ≤ b",
(cases "c ≤ d",
(cases "c ≤ d",

lemma pconj_less_one[simp]:
"a + b < 1 ⟹ a .& b = 0"
unfolding pconj_def by(simp)

lemma pconj_ge_one[simp]:
"1 ≤ a + b ⟹ a .& b = a + b - 1"
unfolding pconj_def by(simp)

lemma pconj_idem[simp]:
"«P» s .& «P» s = «P» s"
unfolding pconj_def by(cases "P s", simp_all)

subsection ‹Rules Involving Conjunction.›

lemma exp_conj_mono_left:
"P ⊩ Q ⟹ P && R ⊩ Q && R"
unfolding exp_conj_def pconj_def

lemma exp_conj_mono_right:
"Q ⊩ R ⟹ P && Q ⊩ P && R"
unfolding exp_conj_def pconj_def

lemma exp_conj_comm[ac_simps]:
"a && b = b && a"

lemma exp_conj_bounded_by[intro,simp]:
assumes bP: "bounded_by 1 P"
and bQ: "bounded_by 1 Q"
shows "bounded_by 1 (P && Q)"
proof(rule bounded_byI, unfold exp_conj_def pconj_def)
fix x
from bP have "P x ≤ 1" by(blast)
moreover from bQ have "Q x ≤ 1" by(blast)
ultimately have "P x + Q x ≤ 2" by(auto)
thus "P x + Q x ⊖ 1 ≤ 1"
unfolding tminus_def by(simp)
qed

lemma exp_conj_o_distrib[simp]:
"(P && Q) o f = (P o f) && (Q o f)"
unfolding exp_conj_def o_def by(simp)

lemma exp_conj_assoc:
assumes "unitary P" and "unitary Q" and "unitary R"
shows "P && (Q && R) = (P && Q) && R"
unfolding exp_conj_def
proof(rule ext)
fix s
from assms have "0 ≤ P s" by(blast)
moreover from assms have "0 ≤ Q s" by(blast)
moreover from assms have "0 ≤ R s" by(blast)
moreover from assms have "P s ≤ 1" by(blast)
moreover from assms have "Q s ≤ 1" by(blast)
moreover from assms have "R s ≤ 1" by(blast)
ultimately
show "P s .& (Q s .& R s) = (P s .& Q s) .& R s"
qed

lemma exp_conj_top_left[simp]:
"sound P ⟹ «λ_. True» && P = P"
unfolding exp_conj_def by(force)

lemma exp_conj_top_right[simp]:
"sound P ⟹ P && «λ_. True» = P"
unfolding exp_conj_def by(force)

lemma exp_conj_idem[simp]:
"«P» && «P» = «P»"
unfolding exp_conj_def
by(rule ext, cases "P s", simp_all)

lemma exp_conj_nneg[intro,simp]:
"(λs. 0) ≤ P && Q"
unfolding exp_conj_def
by(blast intro:le_funI)

lemma exp_conj_sound[intro,simp]:
assumes s_P: "sound P"
and s_Q: "sound Q"
shows "sound (P && Q)"
unfolding exp_conj_def
proof(rule soundI)
from s_P and s_Q have "⋀s. 0 ≤ P s + Q s" by(blast intro:add_nonneg_nonneg)
hence "⋀s. P s .& Q s ≤ P s + Q s"
unfolding pconj_def by(force intro:tminus_less)
also from assms have "⋀s. ... s ≤ bound_of P + bound_of Q"
finally have "bounded_by (bound_of P + bound_of Q) (λs. P s .& Q s)"
by(blast)
thus "bounded (λs. P s .& Q s)" by(blast)

show "nneg (λs. P s .& Q s)"
unfolding pconj_def tminus_def by(force)
qed

lemma exp_conj_rzero[simp]:
"bounded_by 1 P ⟹ P && (λs. 0) = (λs. 0)"
unfolding exp_conj_def by(force)

lemma exp_conj_1_right[simp]:
assumes nn: "nneg A"
shows "A && (λ_. 1) = A"
unfolding exp_conj_def pconj_def tminus_def
proof(rule ext, simp)
fix s
from nn have "0 ≤ A s" by(blast)
thus "max (A s) 0 = A s" by(force)
qed

lemma exp_conj_std_split:
"«λs. P s ∧ Q s» = «P» && «Q»"
unfolding exp_conj_def embed_bool_def pconj_def
by(auto)

subsection ‹Rules Involving Entailment and Conjunction Together›

text ‹Meta-conjunction distributes over expectaton entailment,
becoming expectation conjunction:›
lemma entails_frame:
assumes ePR: "P ⊩ R"
and eQS: "Q ⊩ S"
shows "P && Q ⊩ R && S"
proof(rule le_funI)
fix s
from ePR have "P s ≤ R s" by(blast)
moreover from eQS have "Q s ≤ S s" by(blast)
ultimately have "P s + Q s ≤ R s + S s" by(rule add_mono)
hence "P s + Q s ⊖ 1 ≤ R s + S s ⊖ 1" by(rule tminus_left_mono)
thus "(P && Q) s ≤ (R && S) s"
unfolding exp_conj_def pconj_def .
qed

text ‹This rule allows something very much akin to a case distinction
on the pre-expectation.›
lemma pentails_cases:
assumes PQe: "⋀x. P x ⊩ Q x"
and exhaust: "⋀s. ∃x. P (x s) s = 1"
and framed: "⋀x. P x && R ⊩ Q x && S"
and sR: "sound R" and sS: "sound S"
and bQ: "⋀x. bounded_by 1 (Q x)"
shows "R ⊩ S"
proof(rule le_funI)
fix s
from exhaust obtain x where P_xs: "P x s = 1" by(blast)
moreover {
hence "1 = P x s" by(simp)
also from PQe have "P x s ≤ Q x s" by(blast dest:le_funD)
finally have "Q x s = 1"
using bQ by(blast intro:antisym)
}
moreover note le_funD[OF framed[where x=x], where x=s]
moreover from sR have "0 ≤ R s" by(blast)
moreover from sS have "0 ≤ S s" by(blast)
ultimately show "R s ≤ S s" by(simp add:exp_conj_def)
qed

lemma unitary_bot[iff]:
"unitary (λs. 0::real)"
by(auto)

lemma unitary_top[iff]:
"unitary (λs. 1::real)"
by(auto)

lemma unitary_embed[iff]:
"unitary «P»"
by(auto)

lemma unitary_const[iff]:
"⟦ 0 ≤ c; c ≤ 1 ⟧ ⟹ unitary (λs. c)"
by(auto)

lemma unitary_mult:
assumes uA: "unitary A" and uB: "unitary B"
shows "unitary (λs. A s * B s)"
proof(intro unitaryI2 nnegI bounded_byI)
fix s
from assms have nnA: "0 ≤ A s" and nnB: "0 ≤ B s" by(auto)
thus "0 ≤ A s * B s" by(rule mult_nonneg_nonneg)
from assms have "A s ≤ 1" and "B s ≤ 1" by(auto)
with nnB have "A s * B s ≤ 1 * 1" by(intro mult_mono, auto)
also have "... = 1" by(simp)
finally show "A s * B s ≤ 1" .
qed

lemma exp_conj_unitary:
"⟦ unitary P; unitary Q ⟧ ⟹ unitary (P && Q)"
by(intro unitaryI2 nnegI2, auto)

lemma unitary_comp[simp]:
"unitary P ⟹ unitary (P o f)"
by(intro unitaryI2 nnegI bounded_byI, auto simp:o_def)

lemmas unitary_intros =
unitary_bot unitary_top unitary_embed unitary_mult exp_conj_unitary
unitary_comp unitary_const

lemmas sound_intros =
mult_sound div_sound const_sound sound_o sound_sum
tminus_sound sc_sound exp_conj_sound sum_sound

end


# Theory Transformers

(*
*)

(* Author: David Cock - David.Cock@nicta.com.au *)

section "Expectation Transformers"

theory Transformers imports Expectations begin

text_raw ‹\label{s:transformers}›

type_synonym 's trans = "'s expect ⇒ 's expect"

text ‹Transformers are functions from expectations to expectations i.e. @{typ "('s ⇒ real) ⇒ 's ⇒
real"}.

The set of \emph{healthy} transformers is the universe into which we place our semantic
interpretation of pGCL programs. In its standard presentation, the healthiness condition for pGCL
programs is \emph{sublinearity}, for demonic programs, and \emph{superlinearity} for angelic
programs. We extract a minimal core property, consisting of monotonicity, feasibility and scaling to
form our healthiness property, which holds across all programs. The additional components of
sublinearity are broken out separately, and shown later. The two reasons for this are firstly to
avoid the effort of establishing sub-(super-)linearity globally, and to allow us to define
primitives whose sublinearity, and indeed healthiness, depend on context.

Consider again the automaton of \autoref{f:automaton_1}. Here, the effect of executing the automaton
from its initial state ($a$) until it reaches some final state ($b$ or $c$) is to \emph{transform}
the expectation on final states ($P$), into one on initial states, giving the \emph{expected} value
of the function on termination. Here, the transformation is linear: $P_\text{prior}(a) = 0.7 * P_\text{post}(b) + 0.3 * P_\text{post}(c)$, but this need not be the case.

\begin{figure}
\begin{center}
\mbox{
\xymatrix{
*++[o][F=]{b} & & *++[o][F=]{c} \\
*++[o][F-]{a} \ar[u]^{0.7} \ar[urr]_(0.25){0.3}  & & *++[o][F-]{d} \ar[ull]^(0.25){0.5} \ar[u]_{0.5}\\
& *++[o][F-]{e}\ar[ul] \ar[ur] \\
& \ar[u]
}
}
\end{center}
\caption{\label{f:automaton_2}A nondeterministic-probabilistic automaton.}
\end{figure}

Consider the automaton of \autoref{f:automaton_2}. Here, we have extended that of
\autoref{f:automaton_1} with two additional states, $d$ and $e$, and a pair of silent (unlabelled)
transitions. From the initial state, $e$, this automaton is free to transition either to the
original starting state ($a$), and thence behave exactly as the previous automaton did, or to $d$,
which has the same set of available transitions, now with different probabilities. Where previously
we could state that the automaton would terminate in state $b$ with probability 0.7 (and in $c$ with
probability 0.3), this now depends on the outcome of the \emph{nondeterministic} transition from $e$
to either $a$ or $d$. The most we can now say is that we must reach $b$ with probability \emph{at
least} 0.5 (the minimum from either $a$ or $d$) and $c$ with at least probability 0.3. Note that
these probabilities do not sum to one (although the sum will still always be less than one). The
associated expectation transformer is now \emph{sub-}linear: $P_\text{prior}(e) = 0.5 * P_\text{post}(b) + 0.3 * P_\text{post}(c)$.›

text_raw ‹
\begin{figure}
\begin{center}
\mbox{
\xymatrix{
*++[o][F=]{b} & & *++[o][F=]{c} \\
*++[o][F-]{a} \ar@(dl,ul)[] \ar[u]^{0.5} \ar[urr]_{0.3}
& & *++[o][F-]{d} \ar@(dr,ur)[] \\
& *++[o][F-]{e}\ar[ul]^{0.5} \ar[ur]_{0.5} \\
& \ar[u]
}
}
\end{center}
\caption{\label{f:automaton_3}A diverging automaton.}
\end{figure}
›

text ‹
Finally, \autoref{f:automaton_3} shows the other way in which strict sublinearity arises:
divergence.  This automaton transitions with probability 0.5 to state $d$, from which it never
escapes.  Once there, the probability of reaching any terminating state is zero, and thus the
probabilty of terminating from the initial state ($e$) is no higher than 0.5.  If it instead
takes the edge to state $a$, we again see a self loop, and thus in theory an infinite trace.  In
this case, however, every time the automaton reaches state $a$, with probability $0.5 + 0.3 = 0.8$,
it transitions to a terminating state.  An infinite trace of transitions $a \rightarrow a \rightarrow \ldots$ thus has probability 0, and the automaton terminates with probability 1.  We
formalise such probabilistic termination arguments in \autoref{s:termination}.

Having reached $a$, the automaton will proceed to $b$ with probability $0.5 * (1 / (0.5 + 0.3)) = 0.625$, and to $c$ with probability $0.375$.  As $a$ is in turn reached half the time, the final
probability of ending in $b$ is $0.3125$, and in $c$, $0.1875$, which sum to only $0.5$.  The
remaining probability is that the automaton diverges via $d$.  We view nondeterminism and
divergence demonically: we take the \emph{least} probability of reaching a given final state, and
use it to calculate the expectation.  Thus for this automaton, $P_\text{prior}(e) = 0.3125 * P_\text{post}(b) + 0.1875 * P_\text{post}(c)$.  The end result is the same as for nondeterminism:
a sublinear transformation (the weights sum to less than one).  The two outcomes are thus unified
in the semantic interpretation, although as we will establish in \autoref{s:prog_determ}, the two
have slightly different algebraic properties.

This pattern holds for all pGCL programs: probabilistic choices are always linear, while struct
sublinearity is introduced both nondeterminism and divergence.

Healthiness, again, is the combination of three properties: feasibility, monotonicity and
scaling. Feasibility requires that a transformer take non-negative expectations to non-negative
expectations, and preserve bounds. Thus, starting with an expectation bounded between 0 and some
bound, $b$, after applying any number of feasible transformers, the result will still be bounded
between 0 and $b$. This closure property allows us to treat expectations almost as a complete
lattice. Specifically, for any $b$, the set of expectations bounded by $b$ is a complete lattice
($\bot = (\lambda s. 0)$, $\top = (\lambda s. b)$), and is closed under the action of feasible
transformers, including $\sqcap$ and $\sqcup$, which are themselves feasible. We are thus able to
define both least and greatest fixed points on this set, and thus give semantics to recursive
programs built from feasible components.›

subsection ‹Comparing Transformers›

text ‹Transformers are compared pointwise, but only on @{term sound} expectations. From the
preorder so generated, we define equivalence by antisymmetry, giving a partial order.›

definition
le_trans :: "'s trans ⇒ 's trans ⇒ bool"
where
"le_trans t u ≡ ∀P. sound P ⟶ t P ≤ u P"

text ‹We also need to define relations restricted to @{term unitary} transformers, for the
liberal (wlp) semantics.›

definition
le_utrans :: "'s trans ⇒ 's trans ⇒ bool"
where
"le_utrans t u ⟷ (∀P. unitary P ⟶ t P ≤ u P)"

lemma le_transI[intro]:
"⟦ ⋀P. sound P ⟹ t P ≤ u P ⟧ ⟹ le_trans t u"

lemma le_utransI[intro]:
"⟦ ⋀P. unitary P ⟹ t P ≤ u P ⟧ ⟹ le_utrans t u"

lemma  le_transD[dest]:
"⟦ le_trans t u; sound P ⟧ ⟹ t P ≤ u P"

lemma le_utransD[dest]:
"⟦ le_utrans t u; unitary P ⟧ ⟹ t P ≤ u P"

lemma le_trans_trans[trans]:
"⟦ le_trans x y; le_trans y z ⟧ ⟹ le_trans x z"
unfolding le_trans_def by(blast dest:order_trans)

lemma le_utrans_trans[trans]:
"⟦ le_utrans x y; le_utrans y z ⟧ ⟹ le_utrans x z"
unfolding le_utrans_def by(blast dest:order_trans)

lemma le_trans_refl[iff]:
"le_trans x x"

lemma le_utrans_refl[iff]:
"le_utrans x x"

lemma le_trans_le_utrans[dest]:
"le_trans t u ⟹ le_utrans t u"
unfolding le_trans_def le_utrans_def by(auto)

definition
l_trans :: "'s trans ⇒ 's trans ⇒ bool"
where
"l_trans t u ⟷ le_trans t u ∧ ¬ le_trans u t"

text ‹Transformer equivalence is induced by comparison:›

definition
equiv_trans :: "'s trans ⇒ 's trans ⇒ bool"
where
"equiv_trans t u ⟷ le_trans t u ∧ le_trans u t"

definition
equiv_utrans :: "'s trans ⇒ 's trans ⇒ bool"
where
"equiv_utrans t u ⟷ le_utrans t u ∧ le_utrans u t"

lemma equiv_transI[intro]:
"⟦ ⋀P. sound P ⟹ t P = u P ⟧ ⟹ equiv_trans t u"
unfolding equiv_trans_def by(force)

lemma equiv_utransI[intro]:
"⟦ ⋀P. sound P ⟹ t P = u P ⟧ ⟹ equiv_utrans t u"
unfolding equiv_utrans_def by(force)

lemma equiv_transD[dest]:
"⟦ equiv_trans t u; sound P ⟧ ⟹ t P = u P"
unfolding equiv_trans_def by(blast intro:antisym)

lemma equiv_utransD[dest]:
"⟦ equiv_utrans t u; unitary P ⟧ ⟹ t P = u P"
unfolding equiv_utrans_def by(blast intro:antisym)

lemma equiv_trans_refl[iff]:
"equiv_trans t t"
by(blast)

lemma equiv_utrans_refl[iff]:
"equiv_utrans t t"
by(blast)

lemma le_trans_antisym:
"⟦ le_trans x y; le_trans y x ⟧ ⟹ equiv_trans x y"
unfolding equiv_trans_def by(simp)

lemma le_utrans_antisym:
"⟦ le_utrans x y; le_utrans y x ⟧ ⟹ equiv_utrans x y"
unfolding equiv_utrans_def by(simp)

lemma equiv_trans_comm[ac_simps]:
"equiv_trans t u ⟷ equiv_trans u t"
unfolding equiv_trans_def by(blast)

lemma equiv_utrans_comm[ac_simps]:
"equiv_utrans t u ⟷ equiv_utrans u t"
unfolding equiv_utrans_def by(blast)

lemma equiv_imp_le[intro]:
"equiv_trans t u ⟹ le_trans t u"
unfolding equiv_trans_def by(clarify)

lemma equivu_imp_le[intro]:
"equiv_utrans t u ⟹ le_utrans t u"
unfolding equiv_utrans_def by(clarify)

lemma equiv_imp_le_alt:
"equiv_trans t u ⟹ le_trans u t"
by(force simp:ac_simps)

lemma equiv_uimp_le_alt:
"equiv_utrans t u ⟹ le_utrans u t"
by(force simp:ac_simps)

lemma le_trans_equiv_rsp[simp]:
"equiv_trans t u ⟹ le_trans t v ⟷ le_trans u v"
unfolding equiv_trans_def by(blast intro:le_trans_trans)

lemma le_utrans_equiv_rsp[simp]:
"equiv_utrans t u ⟹ le_utrans t v ⟷ le_utrans u v"
unfolding equiv_utrans_def by(blast intro:le_utrans_trans)

lemma equiv_trans_le_trans[trans]:
"⟦ equiv_trans t u; le_trans u v ⟧ ⟹ le_trans t v"
by(simp)

lemma equiv_utrans_le_utrans[trans]:
"⟦ equiv_utrans t u; le_utrans u v ⟧ ⟹ le_utrans t v"
by(simp)

lemma le_trans_equiv_rsp_right[simp]:
"equiv_trans t u ⟹ le_trans v t ⟷ le_trans v u"
unfolding equiv_trans_def by(blast intro:le_trans_trans)

lemma le_utrans_equiv_rsp_right[simp]:
"equiv_utrans t u ⟹ le_utrans v t ⟷ le_utrans v u"
unfolding equiv_utrans_def by(blast intro:le_utrans_trans)

lemma le_trans_equiv_trans[trans]:
"⟦ le_trans t u; equiv_trans u v ⟧ ⟹ le_trans t v"
by(simp)

lemma le_utrans_equiv_utrans[trans]:
"⟦ le_utrans t u; equiv_utrans u v ⟧ ⟹ le_utrans t v"
by(simp)

lemma equiv_trans_trans[trans]:
assumes xy: "equiv_trans x y"
and yz: "equiv_trans y z"
shows "equiv_trans x z"
proof(rule le_trans_antisym)
from xy have "le_trans x y" by(blast)
also from yz have "le_trans y z" by(blast)
finally show "le_trans x z" .
from yz have "le_trans z y" by(force simp:ac_simps)
also from xy have "le_trans y x" by(force simp:ac_simps)
finally show "le_trans z x" .
qed

lemma equiv_utrans_trans[trans]:
assumes xy: "equiv_utrans x y"
and yz: "equiv_utrans y z"
shows "equiv_utrans x z"
proof(rule le_utrans_antisym)
from xy have "le_utrans x y" by(blast)
also from yz have "le_utrans y z" by(blast)
finally show "le_utrans x z" .
from yz have "le_utrans z y" by(force simp:ac_simps)
also from xy have "le_utrans y x" by(force simp:ac_simps)
finally show "le_utrans z x" .
qed

lemma equiv_trans_equiv_utrans[dest]:
"equiv_trans t u ⟹ equiv_utrans t u"
by(auto)

subsection ‹Healthy Transformers›

subsubsection ‹Feasibility›

definition feasible :: "(('a ⇒ real) ⇒ ('a ⇒ real)) ⇒ bool"
where     "feasible t ⟷ (∀P b. bounded_by b P ∧ nneg P ⟶
bounded_by b (t P) ∧ nneg (t P))"

text ‹A @{term feasible} transformer preserves non-negativity, and bounds. A @{term feasible}
transformer always takes its argument closer to 0' (or leaves it where it is). Note that any
particular value of the expectation may increase, but no element of the new expectation may exceed
any bound on the old. This is thus a relatively weak condition.›

lemma feasibleI[intro]:
"⟦ ⋀b P. ⟦ bounded_by b P; nneg P ⟧ ⟹ bounded_by b (t P);
⋀b P. ⟦ bounded_by b P; nneg P ⟧ ⟹ nneg (t P) ⟧ ⟹ feasible t"
by(force simp:feasible_def)

lemma feasible_boundedD[dest]:
"⟦ feasible t; bounded_by b P; nneg P ⟧ ⟹ bounded_by b (t P)"

lemma feasible_nnegD[dest]:
"⟦ feasible t; bounded_by b P; nneg P ⟧ ⟹ nneg (t P)"

lemma feasible_sound[dest]:
"⟦ feasible t; sound P ⟧ ⟹ sound (t P)"
by(rule soundI, unfold sound_def, (blast)+)

lemma feasible_pr_0[simp]:
fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes ft: "feasible t"
shows "t (λx. 0) = (λx. 0)"
proof(rule ext, rule antisym)
fix s

have "bounded_by 0 (λ_::'s. 0::real)" by(blast)
with ft have "bounded_by 0 (t (λ_. 0))" by(blast)
thus "t (λ_. 0) s ≤ 0" by(blast)

have "nneg (λ_::'s. 0::real)" by(blast)
with ft have "nneg (t (λ_. 0))" by(blast)
thus "0 ≤ t (λ_. 0) s" by(blast)
qed

lemma feasible_id:
"feasible (λx. x)"
unfolding feasible_def by(blast)

lemma feasible_bounded_by[dest]:
"⟦ feasible t; sound P; bounded_by b P ⟧ ⟹ bounded_by b (t P)"
by(auto)

lemma feasible_fixes_top:
"feasible t ⟹ t (λs. 1) ≤ (λs. (1::real))"
by(drule bounded_byD2[OF feasible_bounded_by], auto)

lemma feasible_fixes_bot:
assumes ft: "feasible t"
shows "t (λs. 0) = (λs. 0)"
proof(rule antisym)
have sb: "sound (λs. 0)" by(auto)
with ft show "(λs. 0) ≤ t (λs. 0)" by(auto)
thm bound_of_const
from sb have "bounded_by (bound_of (λs. 0::real)) (λs. 0)" by(auto)
hence "bounded_by 0 (λs. 0::real)" by(simp add:bound_of_const)
with ft have "bounded_by 0 (t (λs. 0))" by(auto)
thus "t (λs. 0) ≤ (λs. 0)" by(auto)
qed

lemma feasible_unitaryD[dest]:
assumes ft: "feasible t" and uP: "unitary P"
shows "unitary (t P)"
proof(rule unitaryI)
from uP have "sound P" by(auto)
with ft show "sound (t P)" by(auto)
from assms show "bounded_by 1 (t P)" by(auto)
qed

subsubsection ‹Monotonicity›

definition
mono_trans :: "(('s ⇒ real) ⇒ ('s ⇒ real)) ⇒ bool"
where
"mono_trans t ≡ ∀P Q. (sound P ∧ sound Q ∧ P ≤ Q) ⟶ t P ≤ t Q"

text ‹Monotonicity allows us to compose transformers, and thus model sequential computation.
Recall the definition of predicate entailment (\autoref{s:entailment}) as less-than-or-equal. The
statement @{term "Q ⊩ t R"} means that @{term Q} is everywhere below @{term "t R"}. For standard
expectations (\autoref{s:standard}), this simply means that @{term Q} \emph{implies} @{term "t R"},
the \emph{weakest precondition} of @{term R} under @{term t}.

Given another, monotonic, transformer @{term u}, we have that @{term "u Q ⊩ u (t R)"}, or that the
weakest precondition of @{term Q} under @{term u} entails that of @{term R} under the composition
@{term "u o t"}.  If we additionally know that @{term "P ⊩ u Q"}, then by transitivity we have
@{term "P ⊩ u (t R)"}.  We thus derive a probabilistic form of the standard rule for sequential
composition: @{term "⟦ mono_trans t; P ⊩ u Q; Q ⊩ t R ⟧ ⟹ P ⊩ u (t R)"}.
›

lemma mono_transI[intro]:
"⟦ ⋀P Q. ⟦ sound P; sound Q; P ≤ Q ⟧ ⟹  t P ≤ t Q ⟧ ⟹ mono_trans t"

lemma mono_transD[dest]:
"⟦ mono_trans t; sound P; sound Q; P ≤ Q ⟧ ⟹ t P ≤ t Q"

subsubsection ‹Scaling›
text_raw ‹\label{s:scaling}›

text ‹A healthy transformer commutes with scaling by a non-negative constant.›

definition
scaling :: "(('s ⇒ real) ⇒ ('s ⇒ real)) ⇒ bool"
where
"scaling t ≡ ∀P c x. sound P ∧ 0 ≤ c ⟶ c * t P x = t (λx. c * P x) x"

text ‹The @{term scaling} and feasibility properties together allow us to treat transformers as a
complete lattice, when operating on bounded expectations. The action of a transformer on such a
bounded expectation is completely determined by its action on \emph{unitary} expectations (those
bounded by 1): @{term "t P s = bound_of P * t (λs. P s / bound_of P) s"}. Feasibility in turn
ensures that the lattice of unitary expectations is closed under the action of a healthy
transformer. We take advantage of this fact in \autoref{s:induction}, in order to define the fixed
points of healthy transformers.›

lemma scalingI[intro]:
"⟦ ⋀P c x. ⟦ sound P; 0 ≤ c ⟧ ⟹ c * t P x = t (λx. c * P x) x ⟧ ⟹ scaling t"

lemma scalingD[dest]:
"⟦ scaling t; sound P; 0 ≤ c ⟧  ⟹ c * t P x = t (λx. c * P x) x"

lemma right_scalingD:
assumes st: "scaling t"
and sP: "sound P"
and nnc: "0 ≤ c"
shows "t P s * c = t (λs. P s * c) s"
proof -
have "t P s * c = c * t P s" by(simp add:algebra_simps)
also from assms have "... = t (λs. c * P s) s" by(rule scalingD)
also have "... = t (λs. P s * c) s" by(simp add:algebra_simps)
finally show ?thesis .
qed

subsubsection ‹Healthiness›

text ‹Healthy transformers are feasible and monotonic, and respect scaling›

definition
healthy :: "(('s ⇒ real) ⇒ ('s ⇒ real)) ⇒ bool"
where
"healthy t ⟷ feasible t ∧ mono_trans t ∧ scaling t"

lemma healthyI[intro]:
"⟦ feasible t; mono_trans t; scaling t ⟧ ⟹ healthy t"

lemmas healthy_parts = healthyI[OF feasibleI mono_transI scalingI]

lemma healthy_monoD[dest]:
"healthy t ⟹ mono_trans t"

lemmas healthy_monoD2 = mono_transD[OF healthy_monoD]

lemma healthy_feasibleD[dest]:
"healthy t ⟹ feasible t"

lemma healthy_scalingD[dest]:
"healthy t ⟹ scaling t"

lemma healthy_bounded_byD[intro]:
"⟦ healthy t; bounded_by b P; nneg P ⟧ ⟹ bounded_by b (t P)"
by(blast)

lemma healthy_bounded_byD2:
"⟦ healthy t; bounded_by b P; sound P ⟧ ⟹ bounded_by b (t P)"
by(blast)

lemma healthy_boundedD[dest,simp]:
"⟦ healthy t; sound P ⟧ ⟹ bounded (t P)"
by(blast)

lemma healthy_nnegD[dest,simp]:
"⟦ healthy t; sound P ⟧ ⟹ nneg (t P)"
by(blast intro!:feasible_nnegD)

lemma healthy_nnegD2[dest,simp]:
"⟦ healthy t; bounded_by b P; nneg P ⟧ ⟹ nneg (t P)"
by(blast)

lemma healthy_sound[intro]:
"⟦ healthy t; sound P ⟧ ⟹ sound (t P)"
by(rule soundI, blast, blast intro:feasible_nnegD)

lemma healthy_unitary[intro]:
"⟦ healthy t; unitary P ⟧ ⟹ unitary (t P)"
by(blast intro!:unitaryI dest:unitary_bound healthy_bounded_byD)

lemma healthy_id[simp,intro!]:
"healthy id"

lemmas healthy_fixes_bot = feasible_fixes_bot[OF healthy_feasibleD]

text ‹Some additional results on @{term le_trans}, specific to
@{term healthy} transformers.›

lemma le_trans_bot[intro,simp]:
"healthy t ⟹ le_trans (λP s. 0) t"
by(blast intro:le_funI)

lemma le_trans_top[intro,simp]:
"healthy t ⟹ le_trans t (λP s. bound_of P)"
by(blast intro!:le_transI[OF le_funI])

lemma healthy_pr_bot[simp]:
"healthy t ⟹ t (λs. 0) = (λs. 0)"
by(blast intro:feasible_pr_0)

text ‹The first significant result is that healthiness is preserved by equivalence:›

lemma healthy_equivI:
fixes t::"('s ⇒ real) ⇒ 's ⇒ real" and u
assumes equiv:   "equiv_trans t u"
and healthy: "healthy t"
shows "healthy u"
proof
have le_t_u: "le_trans t u" by(blast intro:equiv)
have le_u_t: "le_trans u t" by(simp add:equiv_imp_le ac_simps equiv)
from equiv have eq_u_t: "equiv_trans u t" by(simp add:ac_simps)

show "feasible u"
proof
fix b and P::"'s ⇒ real"
assume bP: "bounded_by b P" and nP: "nneg P"
hence sP: "sound P" by(blast)
with healthy have "⋀s. 0 ≤ t P s" by(blast)
also from sP and le_t_u have "⋀s. ... s ≤ u P s" by(blast)
finally show "nneg (u P)" by(blast)

from sP and le_u_t have "⋀s. u P s ≤ t P s" by(blast)
also from healthy and sP and bP have "⋀s. t P s ≤ b" by(blast)
finally show "bounded_by b (u P)" by(blast)
qed

show "mono_trans u"
proof
fix P::"'s ⇒ real" and Q::"'s ⇒ real"
assume sP: "sound P" and sQ: "sound Q"
and le: "P ⊩ Q"
from sP and le_u_t have "u P ⊩ t P" by(blast)
also from sP and sQ and le and healthy have "t P ⊩ t Q" by(blast)
also from sQ and le_t_u have "t Q ⊩ u Q" by(blast)
finally show "u P ⊩ u Q" .
qed

show "scaling u"
proof
fix P::"'s ⇒ real" and c::real and x::'s
assume sound: "sound P"
and pos:   "0 ≤ c"

hence "bounded_by (c * bound_of P) (λx. c * P x)"
by(blast intro!:mult_left_mono dest!:less_imp_le)
hence sc_bounded: "bounded (λx. c * P x)"
by(blast)
moreover from sound and pos have sc_nneg: "nneg (λx. c * P x)"
by(blast intro:mult_nonneg_nonneg less_imp_le)
ultimately have sc_sound: "sound (λx. c * P x)" by(blast)

show "c * u P x = u (λx. c * P x) x"
proof -
from sound have "c * u P x = c * t P x"

also have "... = t (λx. c * P x) x"
using healthy and sound and pos
by(blast intro: scalingD)

also from sc_sound and equiv have "... = u (λx. c * P x) x"
by(blast intro:fun_cong)

finally show ?thesis .
qed
qed
qed

lemma healthy_equiv:
"equiv_trans t u ⟹ healthy t ⟷ healthy u"
by(rule iffI, rule healthy_equivI, assumption+,

lemma healthy_scale:
fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes ht: "healthy t" and nc: "0 ≤ c" and bc: "c ≤ 1"
shows "healthy (λP s. c * t P s)"
proof
show "feasible (λP s. c * t P s)"
proof
fix b and P::"'s ⇒ real"
assume nnP: "nneg P" and bP: "bounded_by b P"

from ht nnP bP have "⋀s. t P s ≤ b" by(blast)
with nc have "⋀s. c * t P s ≤ c * b" by(blast intro:mult_left_mono)
also {
from nnP and bP have "0 ≤ b" by(auto)
with bc have "c * b ≤ 1 * b" by(blast intro:mult_right_mono)
hence "c * b ≤ b" by(simp)
}
finally show "bounded_by b (λs. c * t P s)" by(blast)

from ht nnP bP have "⋀s. 0 ≤ t P s" by(blast)
with nc have "⋀s. 0 ≤ c * t P s" by(rule mult_nonneg_nonneg)
thus "nneg (λs. c * t P s)" by(blast)
qed
show "mono_trans (λP s. c * t P s)"
proof
fix P::"'s ⇒ real" and Q
assume sP: "sound P" and sQ: "sound Q" and le: "P ⊩ Q"
with ht have "⋀s. t P s ≤ t Q s" by(auto intro:le_funD)
with nc have "⋀s. c * t P s ≤ c * t Q s"
by(blast intro:mult_left_mono)
thus "λs. c * t P s ⊩ λs. c * t Q s" by(blast)
qed
from ht show "scaling (λP s. c * t P s)"
by(auto simp:scalingD healthy_scalingD ht)
qed

lemma healthy_top[iff]:
"healthy (λP s. bound_of P)"
by(auto intro!:healthy_parts)

lemma healthy_bot[iff]:
"healthy (λP s. 0)"
by(auto intro!:healthy_parts)

text ‹This weaker healthiness condition is for the liberal (wlp) semantics. We only insist that
the transformer preserves \emph{unitarity} (bounded by 1), and drop scaling (it is unnecessary in
establishing the lattice structure here, unlike for the strict semantics).›

definition
nearly_healthy :: "(('s ⇒ real) ⇒ ('s ⇒ real)) ⇒ bool"
where
"nearly_healthy t ⟷ (∀P. unitary P ⟶ unitary (t P)) ∧
(∀P Q. unitary P ⟶ unitary Q ⟶ P ⊩ Q ⟶ t P ⊩ t Q)"

lemma nearly_healthyI[intro]:
"⟦ ⋀P. unitary P ⟹ unitary (t P);
⋀P Q. ⟦ unitary P; unitary Q; P ⊩ Q ⟧ ⟹ t P ⊩ t Q ⟧ ⟹ nearly_healthy t"

lemma nearly_healthy_monoD[dest]:
"⟦ nearly_healthy t; P ⊩ Q; unitary P; unitary Q ⟧ ⟹ t P ⊩ t Q"

lemma nearly_healthy_unitaryD[dest]:
"⟦ nearly_healthy t; unitary P ⟧ ⟹ unitary (t P)"

lemma healthy_nearly_healthy[dest]:
assumes ht: "healthy t"
shows "nearly_healthy t"
by(intro nearly_healthyI, auto intro:mono_transD[OF healthy_monoD, OF ht] ht)

lemmas nearly_healthy_id[iff] =
healthy_nearly_healthy[OF healthy_id, unfolded id_def]

subsection ‹Sublinearity›

text ‹As already mentioned, the core healthiness property (aside from feasibility and continuity)
for transformers is \emph{sublinearity}: The transformation of a quasi-linear combination of sound
expectations is greater than the same combination applied to the transformation of the expectations
themselves. The term @{term "x ⊖ y"} represents \emph{truncated subtraction} i.e. @{term "max (x-y)
0"} (see \autoref{s:trunc_sub}).›

definition sublinear ::
"(('s ⇒ real) ⇒ ('s ⇒ real)) ⇒ bool"
where
"sublinear t ⟷ (∀a b c P Q s. (sound P ∧ sound Q ∧ 0 ≤ a ∧ 0 ≤ b ∧ 0 ≤ c) ⟶
a * t P s + b * t Q s ⊖ c
≤ t (λs'. a * P s' + b * Q s' ⊖ c) s)"

lemma sublinearI[intro]:
"⟦ ⋀a b c P Q s. ⟦ sound P; sound Q; 0 ≤ a; 0 ≤ b; 0 ≤ c ⟧ ⟹
a * t P s + b * t Q s ⊖ c ≤
t (λs'. a * P s' + b * Q s' ⊖ c) s ⟧ ⟹ sublinear t"

lemma sublinearD[dest]:
"⟦ sublinear t; sound P; sound Q; 0 ≤ a; 0 ≤ b; 0 ≤ c ⟧ ⟹
a * t P s + b * t Q s ⊖ c ≤
t (λs'. a * P s' + b * Q s' ⊖ c) s"

text ‹It is easier to see the relevance of sublinearity by breaking it into several component
properties, as in the following sections.›

"(('s ⇒ real) ⇒ ('s ⇒ real)) ⇒ bool"
where
"sub_add t ⟷ (∀P Q s. (sound P ∧ sound Q) ⟶
t P s + t Q s ≤ t (λs'. P s' + Q s') s)"

text ‹
\begin{figure}
\begin{center}
\begin{displaymath}
\begin{xy}
0;<1cm,0cm>:
(-0.25,0); (10,0) **\dir{-} *\dir{>},
(0,-0.25); (0,6) **\dir{-} *\dir{>},
(0.1,5.5)="Ps";  (9.9,1.5)="Pe"  **\dir{-} ?(0.1)+<0em,1em> *{P},
(0.1,4.0)="tPs"; (9.9,1.0)="tPe" **\dir{} ?(0.1)+<0em,1em> *{tP},
(0.1,0.5)="uPs"; (9.9,5.0)="uPe" **\dir{} ?(0.9)+<0em,1em> *{uP}
?!{"tPs";"tPe"}="inter";
"tPs" **\dir{--}, "uPe" **\dir{--},
"tPe" **\dir{-}, "uPs" **\dir{-} ?(0.5)+<0em,1.5em> *{Q=tP \sqcap uP},
(1,0)="x"; "x"-<0em,1em>*{x};
"x"; (1,6) **{}, ?!{"uPs";"uPe"}="uPx" *{\bullet} -<0em,1em>*{Q(x)},
(9,0)="y"; "y"-<0em,1em>*{y};
"y"; (9,6) **{}, ?!{"tPs";"tPe"}="tPy" *{\bullet} -<0em,1em>*{Q(y)},
"uPx"; "tPy" **\dir{.},
(5,0)="xy"; (5,6) **{},
?!{"tPs";"tPe"}="tPxy" *{\bullet} -<0em,1.5em>*{Q(\frac{x+y}{2})},
?!{"uPx";"tPy"}="tPuP" *{\bullet} -<0em,1em>*{\frac{Q(x)+Q(y)}{2}},
\end{xy}
\end{displaymath}
\end{center}
\end{figure}
›

text ‹Sub-additivity, together with scaling (\autoref{s:scaling}) gives the \emph{linear} portion
of sublinearity. Together, these two properties are equivalent to \emph{convexity}, as

Here $P$ is an affine function (expectation) @{typ "real ⇒ real"}, restricted to some finite
interval. In practice the state space (the left-hand type) is typically discrete and
multi-dimensional, but on the reals we have a convenient geometrical intuition. The lines $tP$ and
$uP$ represent the effect of two healthy transformers (again affine). Neither monotonicity nor
scaling are represented, but both are feasible: Both lines are bounded above by the greatest value
of $P$.

The curve $Q$ is the pointwise minimum of $tP$ and $tQ$, written $tP \sqcap tQ$.  This is, not
coincidentally, the syntax for a binary nondeterministic choice in pGCL: The probability that some
property is established by the choice between programs $a$ and $b$ cannot be guaranteed to be any
higher than either the probability under $a$, or that under $b$.

The original curve, $P$, is trivially convex---it is linear.  Also, both $t$ and $u$, and the
operator $\sqcap$ preserve convexity.  A probabilistic choice will also preserve it.  The
preservation of convexity is a property of sub-additive transformers that respect scaling.  Note
the form of the definition of convexity:
\begin{displaymath}
\forall x,y. \frac{Q(x) + Q(y)}{2} \le Q(\frac{x+y}{2})
\end{displaymath}
Were we to replace $Q$ by some sub-additive transformer $v$, and $x$ and $y$ by expectations $R$
and $S$, the equivalent expression:
\begin{displaymath}
\frac{vR + vS}{2} \le v(\frac{R+S}{2})
\end{displaymath}
Can be rewritten, using scaling, to:
\begin{displaymath}
\frac{1}{2}(vR + vS) \le \frac{1}{2}v(R+S)
\end{displaymath}
Which holds everywhere exactly when $v$ is sub-additive i.e.:
\begin{displaymath}
vR + vS \le v(R+S)
\end{displaymath}
›

"⟦ ⋀P Q s. ⟦ sound P; sound Q ⟧ ⟹
t P s + t Q s ≤ t (λs'. P s' + Q s') s ⟧ ⟹ sub_add t"

"⟦⋀P Q. ⟦ sound P; sound Q ⟧ ⟹
λs. t P s + t Q s ⊩ t (λs. P s + Q s)⟧ ⟹
by(auto)

"⟦ sub_add t; sound P; sound Q ⟧ ⟹ t P s + t Q s ≤ t (λs'. P s' + Q s') s"

fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes eq: "equiv_trans t u"
proof
fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::"'s"
assume sP: "sound P" and sQ: "sound Q"

with eq have "u P s + u Q s = t P s + t Q s"
also from sP sQ sa have "t P s + t Q s ≤ t (λs. P s + Q s) s"
by(auto)
also {
from sP sQ have "sound (λs. P s + Q s)" by(auto)
with eq have "t (λs. P s + Q s) s = u (λs. P s + Q s) s"
}
finally show "u P s + u Q s ≤ u (λs. P s + Q s) s" .
qed

text ‹Sublinearity and feasibility imply sub-additivity.›
fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes slt: "sublinear t"
and ft:  "feasible t"
proof
fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
assume sP: "sound P" and sQ: "sound Q"

with ft have "sound (t P)" "sound (t Q)" by(auto)
hence "0 ≤ t P s" and "0 ≤ t Q s" by(auto)
hence "0 ≤ t P s + t Q s" by(auto)
hence "... = ...⊖ 0" by(simp)

also from sP sQ
have "... ≤ t (λs. P s + Q s ⊖ 0) s"
by(rule sublinearD[OF slt, where a=1 and b=1 and c=0, simplified])

also {
from sP sQ have "⋀s. 0 ≤ P s" and "⋀s. 0 ≤ Q s" by(auto)
hence "⋀s. 0 ≤ P s + Q s" by(auto)
hence "t (λs. P s + Q s ⊖ 0) s = t (λs. P s + Q s) s"
by(simp)
}

finally show "t P s + t Q s ≤ t (λs. P s + Q s) s" .
qed

text ‹A few properties following from sub-additivity:›
lemma standard_negate:
assumes ht: "healthy t"
shows "t «P» s + t «𝒩 P» s ≤ 1"
proof -
from sat have "t «P» s + t «𝒩 P» s ≤ t (λs. «P» s + «𝒩 P» s) s" by(auto)
also have "... = t (λs. 1) s" by(simp add:negate_embed)
also {
from ht have "bounded_by 1 (t (λs. 1))" by(auto)
hence "t (λs. 1) s ≤ 1" by(auto)
}
finally show ?thesis .
qed

fixes t::"'s trans" and S::"'a set"
and ht: "healthy t"
and sP: "⋀x. sound (P x)"
shows "(λx. ∑y∈S. t (P y) x) ≤ t (λx. ∑y∈S. P y x)"
assume fS: "finite S"
show ?thesis
proof(rule finite_induct[OF fS le_funI le_funI], simp_all)
fix s::'s
from ht have "sound (t (λs. 0))" by(auto)
thus "0 ≤ t (λs. 0) s" by(auto)

fix F::"'a set" and x::'a
assume IH: "λa. ∑y∈F. t (P y) a ⊩ t (λx. ∑y∈F. P y x)"
hence "t (P x) s + (∑y∈F. t (P y) s) ≤
t (P x) s + t (λx. ∑y∈F. P y x) s"
also from sat sP
have "... ≤ t (λxa. P x xa + (∑y∈F. P y xa)) s"
finally
show "t (P x) s + (∑y∈F. t (P y) s) ≤
t (λxa. P x xa + (∑y∈F. P y xa)) s" .
qed
qed

fixes t::"'s::finite trans" and P::"'s expect" and s::'s
and ht: "healthy t"
and sP: "sound P"
shows "(∑y∈{s. G s}.  P y * t « λz. z = y » s) +
(∑y∈{s. ¬G s}. P y * t « λz. z = y » s) ≤ t P s"
proof -
have "{s. G s} ∩ {s. ¬G s} = {}" by(blast)
hence "(∑y∈{s. G s}.  P y * t « λz. z = y » s) +
(∑y∈{s. ¬G s}. P y * t « λz. z = y » s) =
(∑y∈({s. G s} ∪ {s. ¬G s}). P y * t « λz. z = y » s)"
by(auto intro: sum.union_disjoint[symmetric])
also {
have "{s. G s} ∪ {s. ¬G s} = UNIV" by (blast)
hence "(∑y∈({s. G s} ∪ {s. ¬G s}). P y * t « λz. z = y » s) =
(λx. ∑y∈UNIV. P y * t (λx. «λz. z = y» x) x) s"
by(simp)
}
also {
from sP have "⋀y. 0 ≤ P y" by(auto)
with healthy_scalingD[OF ht]
have "(λx. ∑y∈UNIV. P y * t (λx. «λz. z = y» x) x) s =
(λx. ∑y∈UNIV. t (λx. P y * «λz. z = y» x) x) s"
}
also {
from sat ht sP
have "(λx. ∑y∈UNIV. t (λx. P y * «λz. z = y» x) x) ≤
t (λx. ∑y∈UNIV. P y * «λz. z = y» x)"
hence "(λx. ∑y∈UNIV. t (λx. P y * «λz. z = y» x) x) s ≤
t (λx. ∑y∈UNIV. P y * «λz. z = y» x) s" by(auto)
}
also {
have rw1: "(λx. ∑y∈UNIV. P y * «λz. z = y» x) =
(λx. ∑y∈UNIV. if y = x then P y else 0)"
by (rule ext [OF sum.cong]) auto
also from sP have "... ⊩ P"
by(cases "finite (UNIV::'s set)", auto simp:sum.delta)
finally have leP: "λx. ∑y∈UNIV. P y * « λz. z = y » x ⊩ P" .
moreover have "sound (λx. ∑y∈UNIV. P y * «λz. z = y» x)"
proof(intro soundI2 bounded_byI nnegI sum_nonneg ballI)
fix x
from leP have "(∑y∈UNIV. P y * « λz. z = y » x) ≤ P x" by(auto)
also from sP have "... ≤ bound_of P" by(auto)
finally show "(∑y∈UNIV. P y * « λz. z = y » x) ≤ bound_of P" .
fix y
from sP show "0 ≤ P y * « λz. z = y » x"
by(auto intro:mult_nonneg_nonneg)
qed
ultimately have "t (λx. ∑y∈UNIV. P y * «λz. z = y» x) s ≤ t P s"
using sP by(auto intro:le_funD[OF mono_transD, OF healthy_monoD, OF ht])
}
finally show ?thesis .
qed

subsubsection ‹Sub-distributivity›

definition sub_distrib ::
"(('s ⇒ real) ⇒ ('s ⇒ real)) ⇒ bool"
where
"sub_distrib t ⟷ (∀P s. sound P ⟶ t P s ⊖ 1 ≤ t (λs'. P s' ⊖ 1) s)"

lemma sub_distribI[intro]:
"⟦ ⋀P s. sound P ⟹ t P s ⊖ 1 ≤ t (λs'. P s' ⊖ 1) s ⟧ ⟹ sub_distrib t"

lemma sub_distribI2:
"⟦ ⋀P. sound P ⟹ λs. t P s ⊖ 1 ⊩ t (λs. P s ⊖ 1) ⟧ ⟹ sub_distrib t"
by(auto)

lemma sub_distribD[dest]:
"⟦ sub_distrib t; sound P ⟧ ⟹ t P s ⊖ 1 ≤ t (λs'. P s' ⊖ 1) s"

lemma equiv_sub_distrib:
fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes eq: "equiv_trans t u"
and sd: "sub_distrib t"
shows "sub_distrib u"
proof
fix P::"'s ⇒ real" and s::"'s"
assume sP: "sound P"

with eq have "u P s ⊖ 1 = t P s ⊖ 1" by(simp add:equiv_transD)
also from sP sd have "... ≤ t (λs. P s ⊖ 1) s" by(auto)
also from sP eq have "... = u (λs. P s ⊖ 1) s"
finally show "u P s ⊖ 1 ≤ u (λs. P s ⊖ 1) s" .
qed

text ‹Sublinearity implies sub-distributivity:›
lemma sublinear_sub_distrib:
fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes slt: "sublinear t"
shows "sub_distrib t"
proof
fix P::"'s ⇒ real" and s::'s
assume sP: "sound P"
moreover have "sound (λ_. 0)" by(auto)
ultimately show "t P s ⊖ 1 ≤ t (λs. P s ⊖ 1) s"
by(rule sublinearD[OF slt, where a=1 and b=0 and c=1, simplified])
qed

text ‹Healthiness, sub-additivity and sub-distributivity imply
sublinearity.  This is how we usually show sublinearity.›
lemma sd_sa_sublinear:
fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes sdt: "sub_distrib t" and sat: "sub_add t" and ht: "healthy t"
shows "sublinear t"
proof
fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
and a::real and b::real and c::real
assume sP: "sound P" and sQ: "sound Q"
and nna: "0 ≤ a" and nnb: "0 ≤ b" and nnc: "0 ≤ c"

from ht sP sQ nna nnb
have saP: "sound (λs. a * P s)" and staP: "sound (λs. a * t P s)"
and sbQ: "sound (λs. b * Q s)" and stbQ: "sound (λs. b * t Q s)"
by(auto intro:sc_sound)
hence sabPQ:  "sound (λs. a * P s + b * Q s)"
and stabPQ: "sound (λs. a * t P s + b * t Q s)"
by(auto intro:sound_sum)

from ht sP sQ nna nnb
have "a * t P s + b * t Q s = t (λs. a * P s) s + t (λs. b * Q s) s"
also from saP sbQ sat
have "t (λs. a * P s) s + t (λs. b * Q s) s ≤
t (λs. a * P s + b * Q s) s" by(blast)
finally
have notm: "a * t P s + b * t Q s ≤ t (λs. a * P s + b * Q s) s" .

show "a * t P s + b * t Q s ⊖ c ≤ t (λs'. a * P s' + b * Q s' ⊖ c) s"
proof(cases "c = 0")
case True note z = this
from stabPQ have "⋀s. 0 ≤ a * t P s + b * t Q s" by(auto)
moreover from sabPQ
have "⋀s. 0 ≤ a * P s + b * Q s" by(auto)
ultimately show ?thesis by(simp add:z notm)
next
case False note nz = this
from nz and nnc have nni: "0 ≤ inverse c" by(auto)

have "⋀s. (inverse c * a) * P s + (inverse c * b) * Q s =
inverse c * (a * P s + b * Q s)"
with sabPQ and nni
have si: "sound (λs. (inverse c * a) * P s + (inverse c * b) * Q s)"
by(auto intro:sc_sound)
hence sim: "sound (λs. (inverse c * a) * P s + (inverse c * b) * Q s ⊖ 1)"
by(auto intro!:tminus_sound)

from nz
have "a * t P s + b * t Q s ⊖ c =
(c * inverse c) * a * t P s +
(c * inverse c) * b * t Q s ⊖ c"
by(simp)
also
have "... = c * (inverse c * a * t P s) +
c * (inverse c * b * t Q s) ⊖ c"
also from nnc
have "... = c * (inverse c * a * t P s + inverse c * b * t Q s ⊖ 1)"
also {
have X: "⋀s. (inverse c * a) * t P s + (inverse c * b) * t Q s =
inverse c * (a * t P s + b * t Q s)" by(simp add: divide_simps)
also from nni and notm
have "inverse c * (a * t P s + b * t Q s) ≤
inverse c * (t (λs. a * P s + b * Q s) s)"
by(blast intro:mult_left_mono)
also from nni ht sabPQ
have "... = t (λs. (inverse c * a) * P s + (inverse c * b) * Q s) s"
by(simp add:scalingD[OF healthy_scalingD, OF ht] algebra_simps)
finally
have "(inverse c * a) * t P s + (inverse c * b) * t Q s ⊖ 1 ≤
t (λs. (inverse c * a) * P s + (inverse c * b) * Q s) s ⊖ 1"
by(rule tminus_left_mono)
also {
from sdt si
have "t (λs. (inverse c * a) * P s + (inverse c * b) * Q s) s ⊖ 1 ≤
t (λs. (inverse c * a) * P s + (inverse c * b) * Q s ⊖ 1) s"
by(blast)
}
finally
have "c * (inverse c * a * t P s + inverse c * b * t Q s ⊖ 1) ≤
c * t (λs. inverse c * a * P s + inverse c * b * Q s ⊖ 1) s"
using nnc by(blast intro:mult_left_mono)
}
also from nnc ht sim
have "c * t (λs. inverse c * a * P s + inverse c * b * Q s ⊖ 1) s
= t (λs. c * (inverse c * a * P s + inverse c * b * Q s ⊖ 1)) s"
also from nnc
have "... = t (λs. c * (inverse c * a * P s) +
c * (inverse c * b * Q s) ⊖ c) s"
also have "... = t (λs. (c * inverse c) * a * P s +
(c * inverse c) * b * Q s ⊖ c) s"
finally
show "a * t P s + b * t Q s ⊖ c ≤ t (λs'. a * P s' + b * Q s' ⊖ c) s"
using nz by(simp)
qed
qed

subsubsection ‹Sub-conjunctivity›
definition
sub_conj :: "(('s ⇒ real) ⇒ 's ⇒ real) ⇒ bool"
where
"sub_conj t ≡ ∀P Q. (sound P ∧ sound Q) ⟶
t P && t Q ⊩ t (P && Q)"

lemma sub_conjI[intro]:
"⟦ ⋀P Q. ⟦ sound P; sound Q ⟧ ⟹
t P && t Q ⊩ t (P && Q) ⟧ ⟹ sub_conj t"
unfolding sub_conj_def by(simp)

lemma sub_conjD[dest]:
"⟦ sub_conj t; sound P; sound Q ⟧ ⟹ t P && t Q ⊩ t (P && Q)"
unfolding sub_conj_def by(simp)

lemma sub_conj_wp_twice:
fixes f::"'s ⇒ (('s ⇒ real) ⇒ 's ⇒ real)"
assumes all: "∀s. sub_conj (f s)"
shows "sub_conj (λP s. f s P s)"
proof(rule sub_conjI, rule le_funI)
fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s
assume sP: "sound P" and sQ: "sound Q"

have "((λs. f s P s) && (λs. f s Q s)) s = (f s P && f s Q) s"
also {
from all have "sub_conj (f s)" by(blast)
with sP and sQ have "(f s P && f s Q) s ≤ f s (P && Q) s"
by(blast)
}
finally show "((λs. f s P s) && (λs. f s Q s)) s ≤ f s (P && Q) s" .
qed

text ‹Sublinearity implies sub-conjunctivity:›
lemma sublinear_sub_conj:
fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
assumes slt: "sublinear t"
shows "sub_conj t"
proof(rule sub_conjI, rule le_funI, unfold exp_conj_def pconj_def)
fix P::"'s ⇒ real" and Q::"'s ⇒ real"and s::'s
assume sP: "sound P" and sQ: "sound Q"
thus "t P s + t Q s ⊖ 1 ≤ t (λs. P s + Q s ⊖ 1) s"
by(rule sublinearD[OF slt, where a=1 and b=1 and c=1, simplified])
qed

subsubsection ‹Sublinearity under equivalence›

text ‹Sublinearity is preserved by equivalence.›
lemma equiv_sublinear:
"⟦ equiv_trans t u; sublinear t; healthy t ⟧ ⟹ sublinear u"
by(iprover intro:sd_sa_sublinear healthy_equivI
healthy_feasibleD)

subsection ‹Determinism›

text ‹Transformers which are both additive, and maximal among those that
satisfy feasibility are \emph{deterministic}, and will turn out to be maximal
in the refinement order.›

text ‹Full additivity is not generally satisfied.  It holds for
(sub-)probabilistic transformers however.›
definition
additive :: "(('a ⇒ real) ⇒ 'a ⇒ real) ⇒ bool"
where
"additive t ≡ ∀P Q. (sound P ∧ sound Q) ⟶
t (λs. P s + Q s) = (λs. t P s + t Q s)"

"⟦ additive t; sound P; sound Q ⟧ ⟹ t (λs. P s + Q s) = (λs. t P s + t Q s)"

"⟦ ⋀P Q s. ⟦ sound P; sound Q ⟧ ⟹ t (λs. P s + Q s) s = t P s + t Q s ⟧ ⟹

text ‹The additivity property extends to finite summation.›
fixes S::"'s set"
and healthy:  "healthy t"
and finite:   "finite S"
and sPz:      "⋀z. sound (P z)"
shows "t (λx. ∑y∈S. P y x) = (λx. ∑y∈S. t (P y) x)"
fix z::'s and T::"'s set"
assume finT: "finite T"
and IH: "t (λx. ∑y∈T. P y x) = (λx. ∑y∈T. t (P y) x)"

have "t (λx. P z x + (∑y∈T. P y x)) =
(λx. t (P z) x +  t (λx. ∑y∈T. P y x) x)"
also from IH
have "... = (λx. t (P z) x + (∑y∈T. t (P y) x))"
by(simp)
finally show "t (λx. P z x + (∑y∈T. P y x)) =
(λx. t (P z) x + (∑y∈T. t (P y) x))" .
qed

text ‹An additive transformer (over a finite state space) is linear: it is
simply the weighted sum of final expectation values, the weights being the
probability of reaching a given final state.  This is useful for reasoning
using the forward, or gambling game'' interpretation.›
fixes t::"('s::finite ⇒ real) ⇒ 's ⇒ real"
and ht: "healthy t"
and sP: "sound P"
shows "t P x = (∑y∈UNIV. P y * t «λz. z = y» x)"
proof -
have "⋀x. (∑y∈UNIV. P y * «λz. z = y» x) =
(∑y∈UNIV. if y = x then P y else 0)"
by (rule sum.cong) auto
also have "⋀x. ... x = P x"
finally
have "t P x = t (λx. ∑y∈UNIV. P y * «λz. z = y» x) x"
by(simp)
also {
from sP have "⋀z. sound (λa. P z * « λza. za = z » a)"
by(auto intro!:mult_sound)
hence "t (λx. ∑y∈UNIV. P y * «λz. z = y» x) x =
(∑y∈UNIV. t (λx. P y * «λz. z = y» x) x)"
}
also from sP
have "(∑y∈UNIV. t (λx. P y * «λz. z = y» x) x) =
(∑y∈UNIV. P y * t «λz. z = y» x)"
by(subst scalingD[OF healthy_scalingD, OF ht], auto)
finally show "t P x = (∑y∈UNIV. P y * t « λz. z = y » x)" .
qed

text ‹We can group the states in the linear form, to split on the value
of a predicate (guard).›
fixes t::"('s::finite ⇒ real) ⇒ 's ⇒ real"
and ht: "healthy t"
and sP: "sound P"
shows "t P x = (∑y∈{s.   G s}. P y * t «λz. z = y» x) +
(∑y∈{s. ¬ G s}. P y * t «λz. z = y» x)"
proof -
from assms
have "t P x = (∑y∈UNIV. P y * t «λz. z = y» x)"
also {
have "UNIV = {s. G s} ∪ {s. ¬ G s}"
by(auto)
hence "(∑y∈UNIV. P y * t «λz. z = y» x) =
(∑y∈{s. G s} ∪ {s. ¬ G s}. P y * t «λz. z = y» x)"
by(simp)
}
also
have "(∑y∈{s. G s} ∪ {s. ¬ G s}. P y * t «λz. z = y» x) =
(∑y∈{s.   G s}. P y * t «λz. z = y» x) +
(∑y∈{s. ¬ G s}. P y * t «λz. z = y» x)"
by(auto intro:sum.union_disjoint)
finally show ?thesis .
qed

subsubsection ‹Maximality›
definition
maximal :: "(('a ⇒ real) ⇒ 'a ⇒ real) ⇒ bool"
where
"maximal t ≡ ∀c. 0 ≤ c ⟶ t (λ_. c) = (λ_. c)"

lemma maximalI[intro]:
"⟦ ⋀c. 0 ≤ c ⟹ t (λ_. c) = (λ_. c) ⟧ ⟹ maximal t"

lemma maximalD[dest]:
"⟦ maximal t; 0 ≤ c ⟧  ⟹ t (λ_. c) = (λ_. c)"

text ‹A transformer that is both additive and maximal is deterministic:›
definition determ :: "(('a ⇒ real) ⇒ 'a ⇒ real) ⇒ bool"
where
"determ t ≡ additive t ∧ maximal t"

lemma determI[intro]:
"⟦ additive t; maximal t ⟧ ⟹ determ t"

lemma determ_maximalD[intro]:
"determ t ⟹ maximal t"

text ‹For a fully-deterministic transformer, a transformed standard
expectation, and its transformed negation are complementary.›
lemma determ_negate:
assumes determ:  "determ t"
shows "t «P» s + t «𝒩 P» s = 1"
proof -
have "t «P» s + t «𝒩 P» s = t (λs. «P» s + «𝒩 P» s) s"
also {
have "⋀s. «P» s + «𝒩 P» s = 1"
by(case_tac "P s", simp_all)
hence "t (λs. «P» s + «𝒩 P» s) = t (λs. 1)"
by(simp)
}
also have "t (λs. 1) = (λs. 1)"
finally show ?thesis .
qed

subsection ‹Modular Reasoning›

text ‹The emphasis of a mechanised logic is on automation, and letting
the computer tackle the large, uninteresting problems.  However, as
terms generally grow exponentially in the size of a program, it is
still essential to break up a proof and reason in a modular fashion.

The following rules allow proof decomposition, and later will be
incorporated into a verification condition generator.›

lemma entails_combine:
assumes wp1: "P ⊩ t R"
and wp2: "Q ⊩ t S"
and sc:  "sub_conj t"
and sR:  "sound R"
and sS:  "sound S"
shows "P && Q ⊩ t (R && S)"
proof -
from wp1 and wp2 have "P && Q ⊩ t R && t S"
by(blast intro:entails_frame)
also from sc and sR and sS have "... ≤ t (R && S)"
by(rule sub_conjD)
finally show ?thesis .
qed

text ‹These allow mismatched results to be composed›

lemma entails_strengthen_post:
"⟦ P ⊩ t Q; healthy t; sound R; Q ⊩ R; sound Q ⟧ ⟹ P ⊩ t R"
by(blast intro:entails_trans)

lemma entails_weaken_pre:
"⟦ Q ⊩ t R; P ⊩ Q ⟧ ⟹ P ⊩ t R"
by(blast intro:entails_trans)

text ‹This rule is unique to pGCL.  Use it to scale the post-expectation
of a rule to 'fit under' the precondition you need to satisfy.›
lemma entails_scale:
assumes wp: "P ⊩ t Q" and h: "healthy t"
and sQ: "sound Q" and pos: "0 ≤ c"
shows "(λs. c * P s) ⊩ t (λs. c * Q s)"
proof(rule le_funI)
fix s
from pos and wp have "c * P s ≤ c * t Q s"
by(auto intro:mult_left_mono)
with sQ pos h show "c * P s ≤ t (λs. c * Q s) s"
qed

subsection ‹Transforming Standard Expectations›

text ‹Reasoning with \emph{standard} expectations, those obtained
by embedding a predicate, is often easier, as the analogues of
many familiar boolean rules hold in modified form.›

text ‹One may use a standard pre-expectation as an assumption:›
lemma use_premise:
assumes h: "healthy t" and wP: "⋀s. P s ⟹ 1 ≤ t «Q» s"
shows "«P» ⊩ t «Q»"
proof(rule entailsI)
fix s show "«P» s ≤ t «Q» s"
proof(cases "P s")
case True with wP show ?thesis by(auto)
next
case False with h show ?thesis by(auto)
qed
qed

text ‹The other direction works too.›
lemma fold_premise:
assumes ht: "healthy t"
and wp: "«P» ⊩ t «Q»"
shows "∀s. P s ⟶ 1 ≤ t «Q» s"
proof(clarify)
fix s assume "P s"
hence "1 = «P» s" by(simp)
also from wp have "... ≤ t «Q» s" by(auto)
finally show "1 ≤ t «Q» s" .
qed

text ‹Predicate conjunction behaves as expected:›
lemma conj_post:
"⟦ P ⊩ t «λs. Q s ∧ R s»; healthy t ⟧ ⟹ P ⊩ t «Q»"
by(blast intro:entails_strengthen_post implies_entails)

text ‹Similar to @{thm use_premise}, but more general.›
lemma entails_pconj_assumption:
assumes f: "feasible t" and wP: "⋀s. P s ⟹ Q s ≤ t R s"
and uQ: "unitary Q" and uR: "unitary R"
shows "«P» && Q ⊩ t R"
unfolding exp_conj_def
proof(rule entailsI)
fix s show "«P» s .& Q s ≤ t R s"
proof(cases "P s")
case True
moreover from uQ have "0 ≤ Q s" by(auto)
ultimately show ?thesis by(simp add:pconj_lone wP)
next
case False
moreover from uQ have "Q s ≤ 1" by(auto)
ultimately show ?thesis using assms by auto
qed
qed

end


# Theory Induction

(*
*)

(* Author: David Cock - David.Cock@nicta.com.au *)

section "Induction"

theory Induction
imports Expectations Transformers
begin

text_raw ‹\label{s:induction}›

subsection ‹The Lattice of Expectations›

text_raw ‹\label{s:exp_induct}›

text ‹Defining recursive (or iterative) programs requires us to reason about
fixed points on the semantic objects, in this case expectations.  The
complication here, compared to the standard Knaster-Tarski theorem (for example,
as shown in @{theory HOL.Inductive}), is that we do not have a complete lattice.

Finding a lower bound is easy (it's @{term "λ_. 0"}), but as we do not insist
on any global bound on expectations (and work directly in HOL's real type, rather
than extending it with a point at infinity), there is no top element.  We solve
the problem by defining the least (greatest) fixed point, restricted to an
internally-bounded set, allowing us to substitute this bound for the top element.
This works as long as the set contains at least one fixed point, which appears
as an extra assumption in all the theorems.

This also works semantically, thanks to the definition of healthiness.  Given a
healthy transformer parameterised by some sound expectation:
@{term "t::('s ⇒ real) ⇒ ('s ⇒ real) ⇒ 's ⇒ real"}.  Imagine that we wish to find
the least fixed point of @{term "t P"}.  In practice, @{term t} is generally
doubly healthy, that is @{term "∀P. sound P ⟶ healthy (t P)"} and
@{term "∀Q. sound Q ⟶ healthy (λP. t P Q)"}.  Thus by feasibility, @{term "t P Q"}
must be bounded by @{term "bound_of P"}.  Thus, as by definition @{term "x ≤ t P x"}
for any fixed point, all must lie in the
set of sound expectations bounded above by @{term "λ_. bound_of P"}.›

definition Inf_exp :: "'s expect set ⇒ 's expect"
where "Inf_exp S = (λs. Inf {f s |f. f ∈ S})"

lemma Inf_exp_lower:
"⟦ P ∈ S; ∀P∈S. nneg P ⟧ ⟹ Inf_exp S ≤ P"
unfolding Inf_exp_def
by(intro le_funI cInf_lower bdd_belowI[where m=0], auto)

lemma Inf_exp_greatest:
"⟦ S ≠ {}; ∀P∈S. Q ≤ P ⟧ ⟹ Q ≤ Inf_exp S"
unfolding Inf_exp_def by(auto intro!:le_funI[OF cInf_greatest])

definition Sup_exp :: "'s expect set ⇒ 's expect"
where "Sup_exp S = (if S = {} then λs. 0 else (λs. Sup {f s |f. f ∈ S}))"

lemma Sup_exp_upper:
"⟦ P ∈ S; ∀P∈S. bounded_by b P ⟧ ⟹ P ≤ Sup_exp S"
unfolding Sup_exp_def
by(cases "S={}", simp_all, intro le_funI cSup_upper bdd_aboveI[where M=b], auto)

lemma Sup_exp_least:
"⟦ ∀P∈S. P ≤ Q; nneg Q ⟧ ⟹ Sup_exp S ≤ Q"
unfolding Sup_exp_def
by(cases "S={}", auto intro!:le_funI[OF cSup_least])

lemma Sup_exp_sound:
assumes sS: "⋀P. P∈S ⟹ sound P"
and bS: "⋀P. P∈S ⟹ bounded_by b P"
shows "sound (Sup_exp S)"
intro soundI2 bounded_byI2 nnegI2)
assume neS: "S ≠ {}"
then obtain P where Pin: "P ∈ S" by(auto)
with sS bS have nP: "nneg P" "bounded_by b P" by(auto)
hence nb: "0 ≤ b" by(auto)

from bS nb show "Sup_exp S ⊩ λs. b"
by(auto intro:Sup_exp_least)

from nP have "λs. 0 ⊩ P" by(auto)
also from Pin bS have "P ⊩ Sup_exp S"
by(auto intro:Sup_exp_upper)
finally show "λs. 0 ⊩ Sup_exp S" .
qed

definition lfp_exp :: "'s trans ⇒ 's expect"
where "lfp_exp t = Inf_exp {P. sound P ∧ t P ≤ P}"

lemma lfp_exp_lowerbound:
"⟦ t P ≤ P; sound P ⟧ ⟹ lfp_exp t ≤ P"
unfolding lfp_exp_def by(auto intro:Inf_exp_lower)

lemma lfp_exp_greatest:
"⟦ ⋀P. ⟦ t P ≤ P; sound P ⟧ ⟹ Q ≤ P; sound Q; t R ⊩ R; sound R ⟧ ⟹ Q ≤ lfp_exp t"
unfolding lfp_exp_def by(auto intro:Inf_exp_greatest)

lemma feasible_lfp_exp_sound:
"feasible t ⟹ sound (lfp_exp t)"
by(intro soundI2 bounded_byI2 nnegI2, auto intro!:lfp_exp_lowerbound lfp_exp_greatest)

lemma lfp_exp_sound:
assumes fR: "t R ⊩ R" and sR: "sound R"
shows "sound (lfp_exp t)"
proof(intro soundI2)
from fR sR have "lfp_exp t ⊩ R"
by(auto intro:lfp_exp_lowerbound)
also from sR have "R ⊩ λs. bound_of R" by(auto)
finally show "bounded_by (bound_of R) (lfp_exp t)" by(auto)
from fR sR show "nneg (lfp_exp t)" by(auto intro:lfp_exp_greatest)
qed

lemma lfp_exp_bound:
"(⋀P. unitary P ⟹ unitary (t P)) ⟹ bounded_by 1 (lfp_exp t)"
by(auto intro!:lfp_exp_lowerbound)

lemma lfp_exp_unitary:
"(⋀P. unitary P ⟹ unitary (t P)) ⟹ unitary (lfp_exp t)"
proof(intro unitaryI[OF lfp_exp_sound lfp_exp_bound], simp_all)
assume IH: "⋀P. unitary P ⟹ unitary (t P)"
have "unitary (λs. 1)" by(auto)
with IH have "unitary (t (λs. 1))" by(auto)
thus "t (λs. 1) ⊩ λs. 1" by(auto)
show "sound (λs. 1)" by(auto)
qed

lemma lfp_exp_lemma2:
fixes t::"'s trans"
assumes st: "⋀P. sound P ⟹ sound (t P)"
and mt: "mono_trans t"
and fR: "t R ⊩ R" and sR: "sound R"
shows "t (lfp_exp t) ≤ lfp_exp t"
proof(rule lfp_exp_greatest[of t, OF _ _ fR sR])
from fR sR show "sound (t (lfp_exp t))" by(auto intro:lfp_exp_sound st)

fix P::"'s expect"
assume fP: "t P ⊩ P" and sP: "sound P"
hence "lfp_exp t ⊩ P" by(rule lfp_exp_lowerbound)
with fP sP have "t (lfp_exp t) ⊩ t P" by(auto intro:mono_transD[OF mt] lfp_exp_sound)
also note fP
finally show "t (lfp_exp t) ⊩ P" .
qed

lemma lfp_exp_lemma3:
assumes st: "⋀P. sound P ⟹ sound (t P)"
and mt: "mono_trans t"
and fR: "t R ⊩ R" and sR: "sound R"
shows "lfp_exp t ≤ t (lfp_exp t)"
by(iprover intro:lfp_exp_lowerbound lfp_exp_sound lfp_exp_lemma2 assms
mono_transD[OF mt])

lemma lfp_exp_unfold:
assumes nt: "⋀P. sound P ⟹ sound (t P)"
and mt: "mono_trans t"
and fR: "t R ⊩ R" and sR: "sound R"
shows "lfp_exp t = t (lfp_exp t)"
by(iprover intro:antisym lfp_exp_lemma2 lfp_exp_lemma3 assms)

definition gfp_exp :: "'s trans ⇒ 's expect"
where "gfp_exp t = Sup_exp {P. unitary P ∧ P ≤ t P}"

lemma gfp_exp_upperbound:
"⟦ P ≤ t P; unitary P ⟧ ⟹ P ≤ gfp_exp t"
by(auto simp:gfp_exp_def intro:Sup_exp_upper)

lemma gfp_exp_least:
"⟦ ⋀P. ⟦ P ≤ t P; unitary P ⟧ ⟹ P ≤ Q; unitary Q ⟧ ⟹ gfp_exp t ≤ Q"
unfolding gfp_exp_def by(auto intro:Sup_exp_least)

lemma gfp_exp_bound:
"(⋀P. unitary P ⟹ unitary (t P)) ⟹ bounded_by 1 (gfp_exp t)"
unfolding gfp_exp_def
by(rule bounded_byI2[OF Sup_exp_least], auto)

lemma gfp_exp_nneg[iff]:
"nneg (gfp_exp t)"
assume empty: "{P. unitary P ∧ P ⊩ t P} = {}"
show "λs. 0 ⊩ Sup_exp {P. unitary P ∧ P ⊩ t P}"
by(simp only:empty Sup_exp_def, auto)
next
assume "{P. unitary P ∧ P ⊩ t P} ≠ {}"
then obtain Q where Qin: "Q ∈ {P. unitary P ∧ P ⊩ t P}" by(auto)
hence "λs. 0 ⊩ Q" by(auto)
also from Qin have "Q ⊩ Sup_exp {P. unitary P ∧ P ⊩ t P}"
by(auto intro:Sup_exp_upper)
finally show "λs. 0 ⊩ Sup_exp {P. unitary P ∧ P ⊩ t P}" .
qed

lemma gfp_exp_unitary:
"(⋀P. unitary P ⟹ unitary (t P)) ⟹ unitary (gfp_exp t)"
by(iprover intro:gfp_exp_nneg gfp_exp_bound unitaryI2)

lemma gfp_exp_lemma2:
assumes ft: "⋀P. unitary P ⟹ unitary (t P)"
and mt: "⋀P Q. ⟦ unitary P; unitary Q; P ⊩ Q ⟧ ⟹ t P ⊩ t Q"
shows "gfp_exp t ≤ t (gfp_exp t)"
proof(rule gfp_exp_least)
show "unitary (t (gfp_exp t))" by(auto intro:gfp_exp_unitary ft)
fix P
assume fp: "P ≤ t P" and uP: "unitary P"
with ft have "P ≤ gfp_exp t" by(auto intro:gfp_exp_upperbound)
with uP gfp_exp_unitary ft
have "t P ≤ t (gfp_exp t)" by(blast intro: mt)
with fp show "P ≤ t (gfp_exp t)" by(auto)
qed

lemma gfp_exp_lemma3:
assumes ft: "⋀P. unitary P ⟹ unitary (t P)"
and mt: "⋀P Q. ⟦ unitary P; unitary Q; P ⊩ Q ⟧ ⟹ t P ⊩ t Q"
shows "t (gfp_exp t) ≤ gfp_exp t"
by(iprover intro:gfp_exp_upperbound unitary_sound
gfp_exp_unitary gfp_exp_lemma2 assms)

lemma gfp_exp_unfold:
"(⋀P. unitary P ⟹ unitary (t P)) ⟹ (⋀P Q. ⟦ unitary P; unitary Q; P ⊩ Q ⟧ ⟹ t P ⊩ t Q) ⟹
gfp_exp t = t (gfp_exp t)"
by(iprover intro:antisym gfp_exp_lemma2 gfp_exp_lemma3)

subsection ‹The Lattice of Transformers›

text_raw ‹\label{s:trans_induct}›

text ‹In addition to fixed points on expectations, we also need
to reason about fixed points on expectation transformers.  The
interpretation of a recursive program in pGCL is as a fixed
point of a function from transformers to transformers.  In contrast
to the case of expectations, \emph{healthy} transformers do form
a complete lattice, where the bottom element is @{term "λ_. (λ_. 0)"},
and the top element is the greatest allowed by feasibility:
@{term "λP. (λ_. bound_of P)"}.›

definition Inf_trans :: "'s trans set ⇒ 's trans"
where "Inf_trans S = (λP. Inf_exp {t P |t. t ∈ S})"

lemma Inf_trans_lower:
"⟦ t ∈ S; ∀u∈S. ∀P. sound P ⟶ sound (u P) ⟧ ⟹ le_trans (Inf_trans S) t"
unfolding Inf_trans_def
by(rule le_transI[OF Inf_exp_lower], blast+)

lemma Inf_trans_greatest:
"⟦ S ≠ {}; ∀t∈S. ∀P. le_trans u t ⟧ ⟹ le_trans u (Inf_trans S)"
unfolding Inf_trans_def by(auto intro!:le_transI[OF Inf_exp_greatest])

definition Sup_trans :: "'s trans set ⇒ 's trans"
where "Sup_trans S = (λP. Sup_exp {t P |t. t ∈ S})"

lemma Sup_trans_upper:
"⟦ t ∈ S; ∀u∈S. ∀P. unitary P ⟶ unitary (u P) ⟧ ⟹ le_utrans t (Sup_trans S)"
unfolding Sup_trans_def
by(intro le_utransI[OF Sup_exp_upper], auto intro:unitary_bound)

lemma Sup_trans_upper2:
"⟦ t ∈ S; ∀u∈S. ∀P. (nneg P ∧ bounded_by b P) ⟶ (nneg (u P) ∧ bounded_by b (u P));
nneg P; bounded_by b P ⟧ ⟹ t P ⊩ Sup_trans S P"
unfolding Sup_trans_def by(blast intro:Sup_exp_upper)

lemma Sup_trans_least:
"⟦ ∀t∈S. le_utrans t u; ⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (Sup_trans S) u"
unfolding Sup_trans_def
by(auto intro!:sound_nneg[OF unitary_sound] le_utransI[OF Sup_exp_least])

lemma Sup_trans_least2:
"⟦ ∀t∈S. ∀P. nneg P ⟶ bounded_by b P ⟶ t P ⊩ u P;
∀u∈S. ∀P. (nneg P ∧ bounded_by b P) ⟶ (nneg (u P) ∧ bounded_by b (u P));
nneg P; bounded_by b P; ⋀P. ⟦ nneg P; bounded_by b P ⟧ ⟹ nneg (u P) ⟧ ⟹ Sup_trans S P ⊩ u P"
unfolding Sup_trans_def by(blast intro!:Sup_exp_least)

lemma feasible_Sup_trans:
fixes S::"'s trans set"
assumes fS: "∀t∈S. feasible t"
shows "feasible (Sup_trans S)"
proof(cases "S={}", simp add:Sup_trans_def Sup_exp_def, blast, intro feasibleI)
fix b::real and P::"'s expect"
assume bP: "bounded_by b P" and nP: "nneg P"
and neS: "S ≠ {}"

from neS obtain t where tin: "t ∈ S" by(auto)
with fS have ft: "feasible t" by(auto)
with bP nP have "λs. 0 ⊩ t P" by(auto)
also {
from bP nP have "sound P" by(auto)
with tin fS have "t P ⊩ Sup_trans S P"
by(auto intro!:Sup_trans_upper2)
}
finally show "nneg (Sup_trans S P)" by(auto)

from fS bP nP
show "bounded_by b (Sup_trans S P)"
by(auto intro!:bounded_byI2[OF Sup_trans_least2])
qed

definition lfp_trans :: "('s trans ⇒ 's trans) ⇒ 's trans"
where "lfp_trans T = Inf_trans {t. (∀P. sound P ⟶ sound (t P)) ∧ le_trans (T t) t}"

lemma lfp_trans_lowerbound:
"⟦ le_trans (T t) t; ⋀P. sound P ⟹ sound (t P) ⟧ ⟹ le_trans (lfp_trans T) t"
unfolding lfp_trans_def
by(auto intro:Inf_trans_lower)

lemma lfp_trans_greatest:
"⟦ ⋀t P. ⟦ le_trans (T t) t; ⋀P. sound P ⟹ sound (t P) ⟧ ⟹ le_trans u t;
⋀P. sound P ⟹ sound (v P); le_trans (T v) v ⟧ ⟹
le_trans u (lfp_trans T)"
unfolding lfp_trans_def by(rule Inf_trans_greatest, auto)

lemma lfp_trans_sound:
fixes P Q::"'s expect"
assumes sP: "sound P"
and fv: "le_trans (T v) v"
and sv: "⋀P. sound P ⟹ sound (v P)"
shows  "sound (lfp_trans T P)"
proof(intro soundI2 bounded_byI2 nnegI2)
from fv sv have "le_trans (lfp_trans T) v"
by(iprover intro:lfp_trans_lowerbound)
with sP have "lfp_trans T P ⊩ v P" by(auto)
also {
from sv sP have "sound (v P)" by(iprover)
hence "v P ⊩ λs. bound_of (v P)" by(auto)
}
finally show "lfp_trans T P ⊩ λs. bound_of (v P)" .

have "le_trans (λP s. 0) (lfp_trans T)"
proof(intro lfp_trans_greatest)
fix t::"'s trans"
assume "⋀P. sound P ⟹ sound (t P)"
hence "⋀P. sound P ⟹ λs. 0 ⊩ t P" by(auto)
thus "le_trans (λP s. 0) t" by(auto)
next
fix P::"'s expect"
assume "sound P" thus "sound (v P)" by(rule sv)
next
show "le_trans (T v) v" by(rule fv)
qed
with sP show "λs. 0 ⊩ lfp_trans T P" by(auto)
qed

lemma lfp_trans_unitary:
fixes P Q::"'s expect"
assumes uP: "unitary P"
and fv: "le_trans (T v) v"
and sv: "⋀P. sound P ⟹ sound (v P)"
and fT: "le_trans (T (λP s. bound_of P)) (λP s. bound_of P)"
shows  "unitary (lfp_trans T P)"
proof(rule unitaryI)
from unitary_sound[OF uP] fv sv show "sound (lfp_trans T P)"
by(rule lfp_trans_sound)

show "bounded_by 1 (lfp_trans T P)"
proof(rule bounded_byI2)
from fT have "le_trans (lfp_trans T) (λP s. bound_of P)"
by(auto intro: lfp_trans_lowerbound)
with uP have "lfp_trans T P ⊩ λs. bound_of P" by(auto)
also from uP have "... ⊩ λs. 1" by(auto)
finally show "lfp_trans T P ⊩ λs. 1" .
qed
qed

lemma lfp_trans_lemma2:
fixes v::"'s trans"
assumes mono: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
and nT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
and fv:   "le_trans (T v) v"
and sv:   "⋀P. sound P ⟹ sound (v P)"
shows "le_trans (T (lfp_trans T)) (lfp_trans T)"
proof(rule lfp_trans_greatest[where T=T and v=v], simp_all add:assms)
fix t::"'s trans" and P::"'s expect"
assume ft: "le_trans (T t) t" and st: "⋀P. sound P ⟹ sound (t P)"
hence "le_trans (lfp_trans T) t" by(auto intro!:lfp_trans_lowerbound)
with ft st have "le_trans (T (lfp_trans T)) (T t)"
by(iprover intro:mono lfp_trans_sound fv sv)
also note ft
finally show "le_trans (T (lfp_trans T)) t" .
qed

lemma lfp_trans_lemma3:
fixes v::"'s trans"
assumes mono: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
and sT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
and fv:   "le_trans (T v) v"
and sv:   "⋀P. sound P ⟹ sound (v P)"
shows "le_trans (lfp_trans T) (T (lfp_trans T))"
proof(rule lfp_trans_lowerbound)
fix P::"'s expect"
assume sP: "sound P"
have n1: "⋀P. sound P ⟹ sound (lfp_trans T P)"
by(iprover intro:lfp_trans_sound fv sv)
with sP have n2: "sound (lfp_trans T P)"
by(iprover intro:lfp_trans_sound fv sv sT)
with n1 sP show n3: "sound (T (lfp_trans T) P)"
by(iprover intro: sT)
next
show "le_trans (T (T (lfp_trans T))) (T (lfp_trans T))"
by(rule mono[OF lfp_trans_lemma2, OF mono],
(iprover intro:assms lfp_trans_sound)+)
qed

lemma lfp_trans_unfold:
fixes P::"'s expect"
assumes mono: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
and sT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
and fv:   "le_trans (T v) v"
and sv:   "⋀P. sound P ⟹ sound (v P)"
shows "equiv_trans (lfp_trans T) (T (lfp_trans T))"
by(rule le_trans_antisym,
rule lfp_trans_lemma3[OF mono], (iprover intro:assms)+,
rule lfp_trans_lemma2[OF mono], (iprover intro:assms)+)

definition gfp_trans :: "('s trans ⇒ 's trans) ⇒ 's trans"
where "gfp_trans T = Sup_trans {t. (∀P. unitary P ⟶ unitary (t P)) ∧ le_utrans t (T t)}"

lemma gfp_trans_upperbound:
"⟦ le_utrans t (T t); ⋀P. unitary P ⟹ unitary (t P) ⟧ ⟹ le_utrans t (gfp_trans T)"
unfolding gfp_trans_def by(auto intro:Sup_trans_upper)

lemma gfp_trans_least:
"⟦ ⋀t. ⟦ le_utrans t (T t); ⋀P. unitary P ⟹ unitary (t P) ⟧ ⟹ le_utrans t u;
⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹
le_utrans (gfp_trans T) u"
unfolding gfp_trans_def by(auto intro:Sup_trans_least)

lemma gfp_trans_unitary:
fixes P::"'s expect"
assumes uP: "unitary P"
shows "unitary (gfp_trans T P)"
proof(intro unitaryI2 nnegI2 bounded_byI2)
show "gfp_trans T P ⊩ λs. 1"
unfolding gfp_trans_def Sup_trans_def
proof(rule Sup_exp_least, clarify)
fix t::"'s trans"
assume "∀P. unitary P ⟶ unitary (t P)"
with uP have "unitary (t P)" by(auto)
thus "t P ⊩ λs. 1" by(auto)
next
show "nneg (λs. 1::real)" by(auto)
qed
let ?S = "{t P |t. t ∈ {t. (∀P. unitary P ⟶ unitary (t P)) ∧ le_utrans t (T t)}}"
show "λs. 0 ⊩ gfp_trans T P"
unfolding gfp_trans_def Sup_trans_def
proof(cases)
assume empty: "?S = {}"
show "λs. 0 ⊩ Sup_exp ?S"
by(simp only:empty Sup_exp_def, auto)
next
assume "?S ≠ {}"
then obtain Q where Qin: "Q ∈ ?S" by(auto)
with uP have "unitary Q" by(auto)
hence "λs. 0 ⊩ Q" by(auto)
also with uP Qin have "Q ⊩ Sup_exp ?S"
proof(intro Sup_exp_upper, blast, clarify)
fix t::"'s trans"
assume "∀Q. unitary Q ⟶ unitary (t Q)"
with uP show "bounded_by 1 (t P)" by(auto)
qed
finally show "λs. 0 ⊩ Sup_exp ?S" .
qed
qed

lemma gfp_trans_lemma2:
assumes mono: "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
and hT:   "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
shows "le_utrans (gfp_trans T) (T (gfp_trans T))"
fix t
assume fp: "le_utrans t (T t)" and ht: "⋀P. unitary P ⟹ unitary (t P)"

note fp
also {
from fp ht have "le_utrans t (gfp_trans T)"by(rule gfp_trans_upperbound)
moreover note ht gfp_trans_unitary
ultimately have "le_utrans (T t) (T (gfp_trans T))" by(rule mono)
}
finally show "le_utrans t (T (gfp_trans T))" .
qed

lemma gfp_trans_lemma3:
assumes mono: "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
and hT:   "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
shows "le_utrans (T (gfp_trans T)) (gfp_trans T)"
by(blast intro!:mono gfp_trans_unitary gfp_trans_upperbound gfp_trans_lemma2 mono hT)

lemma gfp_trans_unfold:
assumes mono: "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
and hT:   "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
shows "equiv_utrans (gfp_trans T) (T (gfp_trans T))"
using assms by(auto intro!: le_utrans_antisym gfp_trans_lemma2 gfp_trans_lemma3)

subsection ‹Tail Recursion›

text_raw ‹\label{s:tail}›

text ‹The least (greatest) fixed point of a tail-recursive expression on transformers is
equivalent (given appropriate side conditions) to the least (greatest) fixed point on
expectations.›

lemma gfp_pulldown:
fixes P::"'s expect"
assumes tailcall:  "⋀u P. unitary P ⟹ T u P = t P (u P)"
and fT:        "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
and ft:        "⋀P Q. unitary P ⟹ unitary Q ⟹ unitary (t P Q)"
and mt:        "⋀P Q R. ⟦ unitary P; unitary Q; unitary R; Q ⊩ R ⟧ ⟹ t P Q ⊩ t P R"
and uP:        "unitary P"
and monoT:     "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
shows "gfp_trans T P = gfp_exp (t P)" (is "?X P = ?Y P")
proof(rule antisym)
show "?X P ≤ ?Y P"
proof(rule gfp_exp_upperbound)
from monoT fT uP have "(gfp_trans T) P ≤ (T (gfp_trans T)) P"
by(auto intro!: le_utransD[OF gfp_trans_lemma2])
also from uP have "(T (gfp_trans T)) P = t P (gfp_trans T P)" by(rule tailcall)
finally show "gfp_trans T P ⊩ t P (gfp_trans T P)" .
from uP gfp_trans_unitary show "unitary (gfp_trans T P)" by(auto)
qed
show "?Y P ≤ ?X P"
show "le_utrans (λa. gfp_exp (t a)) (T (λa. gfp_exp (t a)))"
proof(rule le_utransI)
fix Q::"'s expect" assume uQ: "unitary Q"
with ft have "⋀R. unitary R ⟹ unitary (t Q R)" by(auto)
with mt[OF uQ] have "gfp_exp (t Q) = t Q (gfp_exp (t Q))" by(blast intro:gfp_exp_unfold)
also from uQ have "... = T (λa. gfp_exp (t a)) Q" by(rule tailcall[symmetric])
finally show "gfp_exp (t Q) ≤ T (λa. gfp_exp (t a)) Q" by(simp)
qed
fix Q::"'s expect" assume "unitary Q"
with ft have "⋀R. unitary R ⟹ unitary (t Q R)" by(auto)
thus "unitary (gfp_exp (t Q))" by(rule gfp_exp_unitary)
qed
qed

lemma lfp_pulldown:
fixes P::"'s expect" and t::"'s expect ⇒ 's trans"
and T::"'s trans ⇒ 's trans"
assumes tailcall:  "⋀u P. sound P ⟹ T u P = t P (u P)"
and st:        "⋀P Q. sound P ⟹ sound Q ⟹ sound (t P Q)"
and mt:        "⋀P. sound P ⟹ mono_trans (t P)"
and monoT: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
and nT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
and fv:   "le_trans (T v) v"
and sv:   "⋀P. sound P ⟹ sound (v P)"
and sP:   "sound P"
shows "lfp_trans T P = lfp_exp (t P)" (is "?X P = ?Y P")
proof(rule antisym)
show "?Y P ≤ ?X P"
proof(rule lfp_exp_lowerbound)
from sP have "t P (lfp_trans T P) = (T (lfp_trans T)) P" by(rule tailcall[symmetric])
also have "(T (lfp_trans T)) P ≤ (lfp_trans T) P"
by(rule le_transD[OF lfp_trans_lemma2[OF monoT]], (iprover intro:assms)+)
finally show "t P (lfp_trans T P) ≤ lfp_trans T P" .
from sP show "sound (lfp_trans T P)"
by(iprover intro:lfp_trans_sound assms)
qed

have "⋀P. sound P ⟹ t P (v P) = T v P" by(simp add:tailcall)
also have "⋀P. sound P ⟹ ... P ⊩ v P" by(auto intro:le_transD[OF fv])
finally have fvP: "⋀P. sound P ⟹ t P (v P) ⊩ v P" .
have svP: "⋀P. sound P ⟹ sound (v P)" by(rule sv)

show "?X P ≤ ?Y P"
proof(rule le_transD[OF lfp_trans_lowerbound, OF _ _ sP])
show "le_trans (T (λa. lfp_exp (t a))) (λa. lfp_exp (t a))"
proof(rule le_transI)
fix P::"'s expect"
assume sP: "sound P"

from sP have "T (λa. lfp_exp (t a)) P = t P (lfp_exp (t P))" by(rule tailcall)
also have "t P (lfp_exp (t P)) = lfp_exp (t P)"
by(iprover intro: lfp_exp_unfold[symmetric] sP st mt fvP svP)
finally show "T (λa. lfp_exp (t a)) P ⊩ lfp_exp (t P)" by(simp)
qed
fix P::"'s expect"
assume "sound P"
with fvP svP show "sound (lfp_exp (t P))"
by(blast intro:lfp_exp_sound)
qed
qed

definition Inf_utrans :: "'s trans set ⇒ 's trans"
where "Inf_utrans S = (if S = {} then λP s. 1 else Inf_trans S)"

lemma Inf_utrans_lower:
"⟦ t ∈ S; ∀t∈S. ∀P. unitary P ⟶ unitary (t P) ⟧ ⟹ le_utrans (Inf_utrans S) t"
unfolding Inf_utrans_def
by(cases "S={}",
auto intro!:le_utransI Inf_exp_lower sound_nneg unitary_sound
simp:Inf_trans_def)

lemma Inf_utrans_greatest:
"⟦ ⋀P. unitary P ⟹ unitary (t P); ∀u∈S. le_utrans t u ⟧ ⟹ le_utrans t (Inf_utrans S)"
unfolding Inf_utrans_def Inf_trans_def
by(cases "S={}", simp_all, (blast intro!:le_utransI Inf_exp_greatest)+)

end


# Theory Embedding

(*
*)

(* Author: David Cock - David.Cock@nicta.com.au *)

section "A Shallow Embedding of pGCL in HOL"

theory Embedding imports Misc Induction begin

subsection ‹Core Primitives and Syntax›

text_raw ‹\label{s:syntax}›

text ‹A pGCL program is embedded directly as its strict or liberal transformer.  This is
achieved with an additional parameter, specifying which semantics should be obeyed.›

type_synonym 's prog = "bool ⇒ ('s ⇒ real) ⇒ ('s ⇒ real)"

text ‹@{term Abort} either always fails, @{term "λP s. 0"}, or always succeeds,
@{term "λP s. 1"}.›
definition Abort :: "'s prog"
where     "Abort ≡ λab P s. if ab then 0 else 1"

text ‹@{term Skip} does nothing at all.›
definition Skip :: "'s prog"
where     "Skip ≡ λab P. P"

text ‹@{term Apply} lifts a state transformer into the space of programs.›
definition Apply :: "('s ⇒ 's) ⇒ 's prog"
where     "Apply f ≡ λab P s. P (f s)"

text ‹@{term Seq} is sequential composition.›
definition Seq :: "'s prog ⇒ 's prog ⇒ 's prog"
(infixl ";;" 59)
where     "Seq a b ≡ (λab. a ab o b ab)"

text ‹@{term PC} is \emph{probabilistic} choice between programs.›
definition PC :: "'s prog ⇒ ('s ⇒ real) ⇒ 's prog ⇒ 's prog"
("_ ⇘_⇙⊕ _" [58,57,57] 57)
where     "PC a P b ≡ λab Q s. P s * a ab Q s + (1 - P s) * b ab Q s"

text ‹@{term DC} is \emph{demonic} choice between programs.›
definition DC :: "'s prog ⇒ 's prog ⇒ 's prog" ("_ ⨅ _" [58,57] 57)
where     "DC a b ≡ λab Q s. min (a ab Q s) (b ab Q s)"

text ‹@{term AC} is \emph{angelic} choice between programs.›
definition AC :: "'s prog ⇒ 's prog ⇒ 's prog" ("_ ⨆ _" [58,57] 57)
where     "AC a b ≡ λab Q s. max (a ab Q s) (b ab Q s)"

text ‹@{term Embed} allows any expectation transformer to be treated
syntactically as a program, by ignoring the failure flag.›
definition Embed :: "'s trans ⇒ 's prog"
where     "Embed t = (λab. t)"

text ‹@{term Mu} is the recursive primitive, and is either then
least or greatest fixed point.›
definition Mu :: "('s prog ⇒ 's prog) ⇒ 's prog" (binder "μ" 50)
where     "Mu(T) ≡ (λab. if ab then lfp_trans (λt. T (Embed t) ab)
else gfp_trans (λt. T (Embed t) ab))"

text ‹@{term repeat} expresses finite repetition›
primrec
repeat :: "nat ⇒ 'a prog ⇒ 'a prog"
where
"repeat 0 p = Skip" |
"repeat (Suc n) p = p ;; repeat n p"

text ‹@{term SetDC} is demonic choice between a set of alternatives,
which may depend on the state.›
definition SetDC :: "('a ⇒ 's prog) ⇒ ('s ⇒ 'a set) ⇒ 's prog"
where "SetDC f S ≡ λab P s. Inf ((λa. f a ab P s)  S s)"

syntax "_SetDC" :: "pttrn => ('s => 'a set) => 's prog => 's prog"
("⨅_∈_./ _" 100)
translations "⨅x∈S. p" == "CONST SetDC (%x. p) S"

text ‹The above syntax allows us to write @{term "⨅x∈S. Apply f"}›

text ‹@{term SetPC} is \emph{probabilistic} choice from a set.  Note that this is only
meaningful for distributions of finite support.›
definition
SetPC :: "('a ⇒ 's prog) ⇒ ('s ⇒ 'a ⇒ real) ⇒ 's prog"
where
"SetPC f p ≡ λab P s. ∑a∈supp (p s). p s a * f a ab P s"

text ‹@{term Bind} allows us to name an expression in the current state, and re-use it later.›
definition
Bind :: "('s ⇒ 'a) ⇒ ('a ⇒ 's prog) ⇒ 's prog"
where
"Bind g f ab ≡ λP s. let a = g s in f a ab P s"

text ‹This gives us something like let syntax›
syntax "_Bind" :: "pttrn => ('s => 'a) => 's prog => 's prog"
("_ is _ in _" [55,55,55]55)
translations "x is f in a" => "CONST Bind f (%x. a)"

definition flip :: "('a ⇒ 'b ⇒ 'c) ⇒ 'b ⇒ 'a ⇒ 'c"
where [simp]: "flip f = (λb a. f a b)"

text ‹The following pair of translations introduce let-style syntax
for @{term SetPC} and @{term SetDC}, respectively.›
syntax "_PBind" :: "pttrn => ('s => real) => 's prog => 's prog"
("bind _ at _ in _" [55,55,55]55)
translations "bind x at p in a" => "CONST SetPC (%x. a) (CONST flip (%x. p))"

syntax "_DBind" :: "pttrn => ('s => 'a set) ⇒ 's prog => 's prog"
("bind _ from _ in _" [55,55,55]55)
translations "bind x from S in a" => "CONST SetDC (%x. a) S"

text ‹The following syntax translations are for convenience when
using a record as the state type.›
syntax
"_assign" :: "ident => 'a => 's prog" ("_ := _" [1000,900]900)
ML ‹
fun assign_tr _ [Const (name,_), arg] =
Const ("Embedding.Apply", dummyT) $Abs ("s", dummyT, Syntax.const (suffix Record.updateN name)$
Abs (Name.uu_, dummyT, arg $Bound 1)$ Bound 0)
| assign_tr _ ts = raise TERM ("assign_tr", ts)
›
parse_translation ‹[(@{syntax_const "_assign"}, assign_tr)]›

syntax
"_SetPC" :: "ident => ('s => 'a => real) => 's prog"
("choose _ at _" [66,66]66)
ML ‹
fun set_pc_tr _ [Const (f,_), P] =
Const ("SetPC", dummyT) $Abs ("v", dummyT, (Const ("Embedding.Apply", dummyT)$
Abs ("s", dummyT,
Syntax.const (suffix Record.updateN f) $Abs (Name.uu_, dummyT, Bound 2)$ Bound 0))) $P | set_pc_tr _ ts = raise TERM ("set_pc_tr", ts) › parse_translation ‹[(@{syntax_const "_SetPC"}, set_pc_tr)]› syntax "_set_dc" :: "ident => ('s => 'a set) => 's prog" ("_ :∈ _" [66,66]66) ML ‹ fun set_dc_tr _ [Const (f,_), S] = Const ("SetDC", dummyT)$
Abs ("v", dummyT,
(Const ("Embedding.Apply", dummyT) $Abs ("s", dummyT, Syntax.const (suffix Record.updateN f)$
Abs (Name.uu_, dummyT, Bound 2) $Bound 0)))$
S
| set_dc_tr _ ts = raise TERM ("set_dc_tr", ts)
›
parse_translation ‹[(@{syntax_const "_set_dc"}, set_dc_tr)]›

text ‹These definitions instantiate the embedding as either
weakest precondition (True) or weakest liberal precondition
(False).›

syntax
"_set_dc_UNIV" :: "ident => 's prog" ("any _" [66]66)

translations
"_set_dc_UNIV x" => "_set_dc x (%_. CONST UNIV)"

definition
wp :: "'s prog ⇒ 's trans"
where
"wp pr ≡ pr True"

definition
wlp :: "'s prog ⇒ 's trans"
where
"wlp pr ≡ pr False"

text ‹If-Then-Else as a degenerate probabilistic choice.›
abbreviation(input)
if_then_else :: "['s ⇒ bool, 's prog, 's prog] ⇒ 's prog"
("If _ Then _ Else _" 58)
where
"If P Then a Else b == a ⇘«P»⇙⊕ b"

text ‹Syntax for loops›
abbreviation
do_while :: "['s ⇒ bool, 's prog] ⇒ 's prog"
("do _ ⟶// (4 _) //od")
where
"do_while P a ≡ μ x. If P Then a ;; x Else Skip"

subsection ‹Unfolding rules for non-recursive primitives›

lemma eval_wp_Abort:
"wp Abort P = (λs. 0)"
unfolding wp_def Abort_def by(simp)

lemma eval_wlp_Abort:
"wlp Abort P = (λs. 1)"
unfolding wlp_def Abort_def by(simp)

lemma eval_wp_Skip:
"wp Skip P = P"
unfolding wp_def Skip_def by(simp)

lemma eval_wlp_Skip:
"wlp Skip P = P"
unfolding wlp_def Skip_def by(simp)

lemma eval_wp_Apply:
"wp (Apply f) P = P o f"

lemma eval_wlp_Apply:
"wlp (Apply f) P = P o f"

lemma eval_wp_Seq:
"wp (a ;; b) P = (wp a o wp b) P"
unfolding wp_def Seq_def by(simp)

lemma eval_wlp_Seq:
"wlp (a ;; b) P = (wlp a o wlp b) P"
unfolding wlp_def Seq_def by(simp)

lemma eval_wp_PC:
"wp (a ⇘Q⇙⊕ b) P = (λs. Q s * wp a P s + (1 - Q s) * wp b P s)"
unfolding wp_def PC_def by(simp)

lemma eval_wlp_PC:
"wlp (a ⇘Q⇙⊕ b) P = (λs. Q s * wlp a P s + (1 - Q s) * wlp b P s)"
unfolding wlp_def PC_def by(simp)

lemma eval_wp_DC:
"wp (a ⨅ b) P = (λs. min (wp a P s) (wp b P s))"
unfolding wp_def DC_def by(simp)

lemma eval_wlp_DC:
"wlp (a ⨅ b) P = (λs. min (wlp a P s) (wlp b P s))"
unfolding wlp_def DC_def by(simp)

lemma eval_wp_AC:
"wp (a ⨆ b) P = (λs. max (wp a P s) (wp b P s))"
unfolding wp_def AC_def by(simp)

lemma eval_wlp_AC:
"wlp (a ⨆ b) P = (λs. max (wlp a P s) (wlp b P s))"
unfolding wlp_def AC_def by(simp)

lemma eval_wp_Embed:
"wp (Embed t) = t"
unfolding wp_def Embed_def by(simp)

lemma eval_wlp_Embed:
"wlp (Embed t) = t"
unfolding wlp_def Embed_def by(simp)

lemma eval_wp_SetDC:
"wp (SetDC p S) R s = Inf ((λa. wp (p a) R s)  S s)"
unfolding wp_def SetDC_def by(simp)

lemma eval_wlp_SetDC:
"wlp (SetDC p S) R s = Inf ((λa. wlp (p a) R s)  S s)"
unfolding wlp_def SetDC_def by(simp)

lemma eval_wp_SetPC:
"wp (SetPC f p) P = (λs. ∑a∈supp (p s). p s a * wp (f a) P s)"
unfolding wp_def SetPC_def by(simp)

lemma eval_wlp_SetPC:
"wlp (SetPC f p) P = (λs. ∑a∈supp (p s). p s a * wlp (f a) P s)"
unfolding wlp_def SetPC_def by(simp)

lemma eval_wp_Mu:
"wp (μ t. T t) = lfp_trans (λt. wp (T (Embed t)))"
unfolding wp_def Mu_def by(simp)

lemma eval_wlp_Mu:
"wlp (μ t. T t) = gfp_trans (λt. wlp (T (Embed t)))"
unfolding wlp_def Mu_def by(simp)

lemma eval_wp_Bind:
"wp (Bind g f) = (λP s. wp (f (g s)) P s)"
unfolding Bind_def wp_def Let_def by(simp)

lemma eval_wlp_Bind:
"wlp (Bind g f) = (λP s. wlp (f (g s)) P s)"
unfolding Bind_def wlp_def Let_def by(simp)

text ‹Use simp add:wp\_eval to fully unfold a program fragment›
lemmas wp_eval = eval_wp_Abort eval_wlp_Abort eval_wp_Skip eval_wlp_Skip
eval_wp_Apply eval_wlp_Apply eval_wp_Seq eval_wlp_Seq
eval_wp_PC eval_wlp_PC eval_wp_DC eval_wlp_DC
eval_wp_AC eval_wlp_AC
eval_wp_Embed eval_wlp_Embed eval_wp_SetDC eval_wlp_SetDC
eval_wp_SetPC eval_wlp_SetPC eval_wp_Mu eval_wlp_Mu
eval_wp_Bind eval_wlp_Bind

lemma Skip_Seq:
"Skip ;; A = A"
unfolding Skip_def Seq_def o_def by(rule refl)

lemma Seq_Skip:
"A ;; Skip = A"
unfolding Skip_def Seq_def o_def by(rule refl)

text ‹Use these as simp rules to clear out Skips›
lemmas skip_simps = Skip_Seq Seq_Skip

end


# Theory Healthiness

(*
*)

(* Author: David Cock - David.Cock@nicta.com.au *)

section ‹Healthiness›

theory Healthiness imports Embedding begin

subsection ‹The Healthiness of the Embedding›

text ‹Healthiness is mostly derived by structural induction using
the simplifier.  @{term Abort}, @{term Skip} and @{term Apply}
form base cases.›

lemma healthy_wp_Abort:
"healthy (wp Abort)"
proof(rule healthy_parts)
fix b and P::"'a ⇒ real"
assume nP: "nneg P" and bP: "bounded_by b P"
thus "bounded_by b (wp Abort P)"
unfolding wp_eval by(blast)
show "nneg (wp Abort P)"
unfolding wp_eval by(blast)
next
fix P Q::"'a expect"
show "wp Abort P ⊩ wp Abort Q"
unfolding wp_eval by(blast)
next
fix P and c and s::'a
show "c * wp Abort P s = wp Abort (λs. c * P s) s"
unfolding wp_eval by(auto)
qed

lemma nearly_healthy_wlp_Abort:
"nearly_healthy (wlp Abort)"
proof(rule nearly_healthyI)
fix P::"'s ⇒ real"
show "unitary (wlp Abort P)"
next
fix P Q :: "'s expect"
assume "P ⊩ Q" and "unitary P" and "unitary Q"
thus "wlp Abort P ⊩ wlp Abort Q"
unfolding wp_eval by(blast)
qed

lemma healthy_wp_Skip:
"healthy (wp Skip)"
by(force intro!:healthy_parts simp:wp_eval)

lemma nearly_healthy_wlp_Skip:
"nearly_healthy (wlp Skip)"
by(auto simp:wp_eval)

lemma healthy_wp_Seq:
fixes t::"'s prog" and u
assumes ht: "healthy (wp t)" and hu: "healthy (wp u)"
shows "healthy (wp (t ;; u))"
fix b and P::"'s ⇒ real"
assume "bounded_by b P" and "nneg P"
with hu have "bounded_by b (wp u P)" and "nneg (wp u P)" by(auto)
with ht show "bounded_by b (wp t (wp u P))"
and "nneg (wp t (wp u P))" by(auto)
next
fix P::"'s ⇒ real" and Q
assume "sound P" and "sound Q" and "P ⊩ Q"
with hu have "sound (wp u P)" and "sound (wp u Q)"
and "wp u P ⊩ wp u Q" by(auto)
with ht show "wp t (wp u P) ⊩ wp t (wp u Q)" by(auto)
next
fix P::"'s ⇒ real" and c::real and s
assume pos: "0 ≤ c" and sP: "sound P"
with ht and hu have "c * wp t (wp u P) s = wp t (λs. c * wp u P s) s"
by(auto intro!:scalingD)
also with hu and pos and sP have "... = wp t (wp u (λs. c * P s)) s"
finally show "c * wp t (wp u P) s = wp t (wp u (λs. c * P s)) s" .
qed

lemma nearly_healthy_wlp_Seq:
fixes t::"'s prog" and u
assumes ht: "nearly_healthy (wlp t)" and hu: "nearly_healthy (wlp u)"
shows "nearly_healthy (wlp (t ;; u))"
fix b and P::"'s ⇒ real"
assume "unitary P"
with hu have "unitary (wlp u P)" by(auto)
with ht show "unitary (wlp t (wlp u P))" by(auto)
next
fix P Q::"'s ⇒ real"
assume "unitary P" and "unitary Q" and "P ⊩ Q"
with hu have "unitary (wlp u P)" and "unitary (wlp u Q)"
and "wlp u P ⊩ wlp u Q" by(auto)
with ht show "wlp t (wlp u P) ⊩ wlp t (wlp u Q)" by(auto)
qed

lemma healthy_wp_PC:
fixes f::"'s prog"
assumes hf: "healthy (wp f)" and hg: "healthy (wp g)"
and uP: "unitary P"
shows "healthy (wp (f ⇘P⇙⊕ g))"
proof(intro healthy_parts bounded_byI nnegI le_funI, simp_all add:wp_eval)
fix b and Q::"'s ⇒ real" and s::'s
assume nQ: "nneg Q" and bQ: "bounded_by b Q"

txt ‹Non-negative:›
from nQ and bQ and hf have "0 ≤ wp f Q s" by(auto)
with uP have "0 ≤ P s * ..." by(auto intro:mult_nonneg_nonneg)
moreover {
from uP have "0 ≤ 1 - P s"
by auto
with nQ and bQ and hg have "0 ≤ ... * wp g Q s"
by (metis healthy_nnegD2 mult_nonneg_nonneg nneg_def)
}
ultimately show "0 ≤ P s * wp f Q s + (1 - P s) * wp g Q s"
by(auto intro:mult_nonneg_nonneg)

txt ‹Bounded:›
from nQ bQ hf have "wp f Q s ≤ b" by(auto)
with uP nQ bQ hf have "P s * wp f Q s ≤ P s * b"
by(blast intro!:mult_mono)
moreover {
from nQ bQ hg uP
have "wp g Q s ≤ b" and "0 ≤ 1 - P s"
by auto
with nQ bQ hg have "(1 - P s) * wp g Q s ≤ (1 - P s) * b"
by(blast intro!:mult_mono)
}
ultimately have "P s * wp f Q s + (1 - P s) * wp g Q s ≤
P s * b + (1 - P s) * b"
also have "... = b" by(auto simp:algebra_simps)
finally show "P s * wp f Q s + (1 - P s) * wp g Q s ≤ b" .
next
txt ‹Monotonic:›
fix Q R::"'s ⇒ real" and s
assume sQ: "sound Q" and sR: "sound R" and le: "Q ⊩ R"

with hf have "wp f Q s ≤ wp f R s" by(blast dest:mono_transD)
with uP have "P s * wp f Q s ≤ P s * wp f R s"
by(auto intro:mult_left_mono)
moreover {
from sQ sR le hg
have "wp g Q s ≤ wp g R s" by(blast dest:mono_transD)
moreover from uP have "0 ≤ 1 - P s"
by auto
ultimately have "(1 - P s) * wp g Q s ≤ (1 - P s) * wp g R s"
by(auto intro:mult_left_mono)
}
ultimately show "P s * wp f Q s + (1 - P s) * wp g Q s ≤
P s * wp f R s + (1 - P s) * wp g R s" by(auto)
next
txt ‹Scaling:›
fix Q::"'s ⇒ real" and c::real and s::'s
assume sQ: "sound Q" and pos: "0 ≤ c"
have "c * (P s * wp f Q s + (1 - P s) * wp g Q s) =
P s * (c * wp f Q s) + (1 - P s) * (c * wp g Q s)"
also have "... = P s * wp f (λs.  c * Q s) s +
(1 - P s) * wp g (λs. c * Q s) s"
using hf hg sQ pos
finally show "c * (P s * wp f Q s + (1 - P s) * wp g Q s) =
P s * wp f (λs. c * Q s) s + (1 - P s) * wp g (λs. c * Q s) s" .
qed

lemma nearly_healthy_wlp_PC:
fixes f::"'s prog"
assumes hf: "nearly_healthy (wlp f)"
and hg: "nearly_healthy (wlp g)"
and uP: "unitary P"
shows "nearly_healthy (wlp (f ⇘P⇙⊕ g))"
proof(intro nearly_healthyI unitaryI2 nnegI bounded_byI le_funI,
fix Q::"'s expect" and s::'s
assume uQ: "unitary Q"
from uQ hf hg have utQ: "unitary (wlp f Q)" "unitary (wlp g Q)" by(auto)
from uP have nnP: "0 ≤ P s" "0 ≤ 1 - P s"
by auto
moreover from utQ have "0 ≤ wlp f Q s" "0 ≤ wlp g Q s" by(auto)
ultimately show "0 ≤ P s * wlp f Q s + (1 - P s) * wlp g Q s"

from utQ have "wlp f Q s ≤ 1" "wlp g Q s ≤ 1" by(auto)
with nnP have "P s * wlp f Q s + (1 - P s) * wlp g Q s ≤ P s * 1 + (1 - P s) * 1"
thus "P s * wlp f Q s + (1 - P s) * wlp g Q s ≤ 1" by(simp)

fix R::"'s expect"
assume uR: "unitary R" and le: "Q ⊩ R"
with uQ have "wlp f Q s ≤ wlp f R s"
by(auto intro:le_funD[OF nearly_healthy_monoD, OF hf])
with nnP have "P s * wlp f Q s ≤ P s * wlp f R s"
by(auto intro:mult_left_mono)
moreover {
from uQ uR le have "wlp g Q s ≤ wlp g R s"
by(auto intro:le_funD[OF nearly_healthy_monoD, OF hg])
with nnP have "(1 - P s) * wlp g Q s ≤ (1 - P s) * wlp g R s"
by(auto intro:mult_left_mono)
}
ultimately show "P s * wlp f Q s + (1 - P s) * wlp g Q s ≤
P s * wlp f R s + (1 - P s) * wlp g R s"
by(auto)
qed

lemma healthy_wp_DC:
fixes f::"'s prog"
assumes hf: "healthy (wp f)" and hg: "healthy (wp g)"
shows "healthy (wp (f ⨅ g))"
proof(intro healthy_parts bounded_byI nnegI le_funI, simp_all only:wp_eval)
fix b and P::"'s ⇒ real" and s::'s
assume nP: "nneg P" and bP: "bounded_by b P"

with hf have "bounded_by b (wp f P)" by(auto)
hence "wp f P s ≤ b" by(blast)
thus "min (wp f P s) (wp g P s) ≤ b" by(auto)

from nP bP assms show "0 ≤ min (wp f P s) (wp g P s)" by(auto)
next
fix P::"'s ⇒ real" and Q and s::'s
from assms have mf: "mono_trans (wp f)" and mg: "mono_trans (wp g)" by(auto)
assume sP: "sound P" and sQ: "sound Q" and le: "P ⊩ Q"
hence "wp f P s ≤ wp f Q s" and "wp g P s ≤ wp g Q s"
by(auto intro:le_funD[OF mono_transD[OF mf]] le_funD[OF mono_transD[OF mg]])
thus "min (wp f P s) (wp g P s) ≤ min (wp f Q s) (wp g Q s)" by(auto)
next
fix P::"'s ⇒ real" and c::real and s::'s
assume sP: "sound P" and pos: "0 ≤ c"
from assms have sf: "scaling (wp f)" and sg: "scaling (wp g)" by(auto)
from pos have "c * min (wp f P s) (wp g P s) =
min (c * wp f P s) (c * wp g P s)"
also from sP and pos
have "... = min (wp f (λs. c * P s) s) (wp g (λs. c * P s) s)"
finally show "c * min (wp f P s) (wp g P s) =
min (wp f (λs. c * P s) s) (wp g (λs. c * P s) s)" .
qed

lemma nearly_healthy_wlp_DC:
fixes f::"'s prog"
assumes hf: "nearly_healthy (wlp f)"
and hg: "nearly_healthy (wlp g)"
shows "nearly_healthy (wlp (f ⨅ g))"
proof(intro nearly_healthyI bounded_byI nnegI le_funI unitaryI2,
fix P::"'s ⇒ real" and s::'s
assume uP: "unitary P"
with hf hg have utP: "unitary (wlp f P)" "unitary (wlp g P)" by(auto)
thus "0 ≤ wlp f P s" "0 ≤ wlp g P s" by(auto)

have "min (wlp f P s) (wlp g P s) ≤ wlp f P s" by(auto)
also from utP have "... ≤ 1" by(auto)
finally show "min (wlp f P s) (wlp g P s) ≤ 1" .

fix Q::"'s ⇒ real"
assume uQ: "unitary Q" and le: "P ⊩ Q"
have "min (wlp f P s) (wlp g P s) ≤ wlp f P s" by(auto)
also from uP uQ le have "... ≤ wlp f Q s"
by(auto intro:le_funD[OF nearly_healthy_monoD, OF hf])
finally show "min (wlp f P s) (wlp g P s) ≤ wlp f Q s" .

have "min (wlp f P s) (wlp g P s) ≤ wlp g P s" by(auto)
also from uP uQ le have "... ≤ wlp g Q s"
by(auto intro:le_funD[OF nearly_healthy_monoD, OF hg])
finally show "min (wlp f P s) (wlp g P s) ≤ wlp g Q s" .
qed

lemma healthy_wp_AC:
fixes f::"'s prog"
assumes hf: "healthy (wp f)" and hg: "healthy (wp g)"
shows "healthy (wp (f ⨆ g))"
proof(intro healthy_parts bounded_byI nnegI le_funI, simp_all only:wp_eval)
fix b and P::"'s ⇒ real" and s::'s
assume nP: "nneg P" and bP: "bounded_by b P"

with hf