Theory Transformers

(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* 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"
  by(simp add:le_trans_def)

lemma le_utransI[intro]:
  "⟦ ⋀P. unitary P ⟹ t P ≤ u P ⟧ ⟹ le_utrans t u"
  by(simp add:le_utrans_def)

lemma  le_transD[dest]:
  "⟦ le_trans t u; sound P ⟧ ⟹ t P ≤ u P"
  by(simp add:le_trans_def)
  
lemma le_utransD[dest]:
  "⟦ le_utrans t u; unitary P ⟧ ⟹ t P ≤ u P"
  by(simp add:le_utrans_def)

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"
  by(simp add:le_trans_def)
  
lemma le_utrans_refl[iff]:
  "le_utrans x x"
  by(simp add:le_utrans_def)
  
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)"
  by(simp add:feasible_def)

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

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"
  by(simp add:mono_trans_def)

lemma mono_transD[dest]:
  "⟦ mono_trans t; sound P; sound Q; P ≤ Q ⟧ ⟹ t P ≤ t Q"
  by(simp add:mono_trans_def)

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"
  by(simp add:scaling_def)

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

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"
  by(simp add:healthy_def)

lemmas healthy_parts = healthyI[OF feasibleI mono_transI scalingI]

lemma healthy_monoD[dest]:
  "healthy t ⟹ mono_trans t"
  by(simp add:healthy_def)

lemmas healthy_monoD2 = mono_transD[OF healthy_monoD]

lemma healthy_feasibleD[dest]:
  "healthy t ⟹ feasible t"
  by(simp add:healthy_def)

lemma healthy_scalingD[dest]:
  "healthy t ⟹ scaling t"
  by(simp add:healthy_def)

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"
  by(simp add:healthyI feasibleI mono_transI scalingI)

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"
        by(simp add:equiv_transD[OF eq_u_t])

      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+,
     simp add:healthy_equivI ac_simps)

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"
  by(simp add:nearly_healthy_def)

lemma nearly_healthy_monoD[dest]:
  "⟦ nearly_healthy t; P ⊩ Q; unitary P; unitary Q ⟧ ⟹ t P ⊩ t Q"
  by(simp add:nearly_healthy_def)

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

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"
  by(simp add:sublinear_def)

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"
  by(simp add:sublinear_def)

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

subsubsection ‹Sub-additivity›
text_raw ‹\label{s:subadd}›

definition sub_add ::
  "(('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}
\caption{\label{f:subadd_plot}A graphical depiction of sub-additivity as convexity.}
\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
\autoref{f:subadd_plot} illustrates by analogy.

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}
›

lemma sub_addI[intro]:
  "⟦ ⋀P Q s. ⟦ sound P; sound Q ⟧ ⟹
             t P s + t Q s ≤ t (λs'. P s' + Q s') s ⟧ ⟹ sub_add t"
  by(simp add:sub_add_def)

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

lemma sub_addD[dest]:
  "⟦ sub_add t; sound P; sound Q ⟧ ⟹ t P s + t Q s ≤ t (λs'. P s' + Q s') s"
  by(simp add:sub_add_def)

lemma equiv_sub_add:
  fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
  assumes eq: "equiv_trans t u"
      and sa: "sub_add t"
  shows "sub_add 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"
    by(simp add:equiv_transD)
  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"
      by(simp add:equiv_transD)
  }
  finally show "u P s + u Q s ≤ u (λs. P s + Q s) s" .
qed

text ‹Sublinearity and feasibility imply sub-additivity.›
lemma sublinear_subadd:
  fixes t::"('s ⇒ real) ⇒ 's ⇒ real"
  assumes slt: "sublinear t"
      and ft:  "feasible t"
  shows "sub_add 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"
      and sat: "sub_add 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

lemma sub_add_sum:
  fixes t::"'s trans" and S::"'a set"
  assumes sat: "sub_add t"
      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)"
proof(cases "infinite S", simp_all add:ht)
  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"
      by(auto intro:add_left_mono)
    also from sat sP
    have "... ≤ t (λxa. P x xa + (∑y∈F. P y xa)) s"
      by(auto intro!:sub_addD[OF sat] sum_sound)
    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

lemma sub_add_guard_split:
  fixes t::"'s::finite trans" and P::"'s expect" and s::'s
  assumes sat: "sub_add t"
      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"
      by(simp add:scalingD)
  }
  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)"
      by(intro sub_add_sum sound_intros, auto)
    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"
  by(simp add:sub_distrib_def)
  
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"
  by(simp add:sub_distrib_def)

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"
    by(simp add:equiv_transD tminus_sound)
  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"
    by(simp add:scalingD healthy_scalingD)
  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)"
      by(simp add: divide_simps)
    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"
      by(simp add:field_simps)
    also from nnc
    have "... = c * (inverse c * a * t P s + inverse c * b * t Q s ⊖ 1)"
      by(simp add:distrib_left tminus_left_distrib)
    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"
      by(simp add:scalingD healthy_scalingD)
    also from nnc
    have "... = t (λs. c * (inverse c * a * P s) +
                       c * (inverse c * b * Q s) ⊖ c) s"
      by(simp add:distrib_left tminus_left_distrib)
    also have "... = t (λs. (c * inverse c) * a * P s +
                            (c * inverse c) * b * Q s ⊖ c) s"
      by(simp add:field_simps)
    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"
    by(simp add:exp_conj_def)
  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
             dest:equiv_sub_distrib equiv_sub_add
                  sublinear_sub_distrib sublinear_subadd
                  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.›

subsubsection ‹Additivity›
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)"

lemma additiveD:
  "⟦ additive t; sound P; sound Q ⟧ ⟹ t (λs. P s + Q s) = (λs. t P s + t Q s)"
  by(simp add:additive_def)

lemma additiveI[intro]:
  "⟦ ⋀P Q s. ⟦ sound P; sound Q ⟧ ⟹ t (λs. P s + Q s) s = t P s + t Q s ⟧ ⟹
   additive t"
  unfolding additive_def by(blast)

text ‹Additivity is strictly stronger than sub-additivity.›
lemma additive_sub_add:
  "additive t ⟹ sub_add t"
  by(simp add:sub_addI additiveD)

text ‹The additivity property extends to finite summation.›
lemma additive_sum:
  fixes S::"'s set"
  assumes additive: "additive t"
      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)"
proof(rule finite_induct, simp_all add:assms)
  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)"

  from additive sPz
  have "t (λx. P z x + (∑y∈T. P y x)) =
        (λx. t (P z) x +  t (λx. ∑y∈T. P y x) x)"
    by(auto intro!:sum_sound additiveD)
  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.›
lemma additive_delta_split:
  fixes t::"('s::finite ⇒ real) ⇒ 's ⇒ real"
  assumes additive: "additive t"
      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"
    by(simp add:sum.delta)
  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)"
      by(subst additive_sum, simp_all add:assms)
  }
  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).›
lemma additive_guard_split:
  fixes t::"('s::finite ⇒ real) ⇒ 's ⇒ real"
  assumes additive: "additive t"
      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)"
    by(rule additive_delta_split)
  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"
  by(simp add:maximal_def)

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

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"
  by(simp add:determ_def)

lemma determ_additiveD[intro]:
  "determ t ⟹ additive t"
  by(simp add:determ_def)

lemma determ_maximalD[intro]:
  "determ t ⟹ maximal t"
  by(simp add:determ_def)

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"
    by(simp add:additiveD determ determ_additiveD)
  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)"
    by(simp add:maximalD determ determ_maximalD)
  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"
    by(simp add:scalingD healthy_scalingD)
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