Theory Expectations

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

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

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

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

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

lemma nnegD[dest]:
  "nneg P ⟹ 0 ≤ P x"
  by (simp add:nneg_def)

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

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

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

lemma sound_bounded[dest]:
  "sound P ⟹ bounded P"
  by (simp add:sound_def)

lemma sound_nneg[dest]:
  "sound P ⟹ nneg P"
  by (simp add:sound_def)

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"
    by(rule add_mono)
  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)

lemma bounded_by_add:
  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"
  by(simp add:unitary_def)

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

lemma unitary_sound[dest]:
  "unitary P ⟹ sound P"
  by(simp add:unitary_def)
  
lemma unitary_bound[dest]:
  "unitary P ⟹ bounded_by 1 P"
  by(simp add:unitary_def)

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

lemma eval_embed_true[simp]:
  "P s ⟹ «P» s = 1"
  by (simp add:embed_bool_def)

lemma eval_embed_false[simp]:
  "¬P s ⟹ «P» s = 0"
  by (simp add:embed_bool_def)

lemma embed_ge_0[simp,intro]:
  "0 ≤ «G» s"
  by (simp add:embed_bool_def)

lemma embed_le_1[simp,intro]:
  "«G» s ≤ 1"
  by(simp add:embed_bool_def)

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

lemma embed_split:
  "f s = «P» s * f s + «𝒩 P» s * f s"
  by (simp add:negate_def embed_bool_def)

lemma negate_embed:
  "«𝒩 P» s = 1 - «P» s"
  by (simp add:embed_bool_def negate_def)

lemma eval_nembed_true[simp]:
  "P s ⟹ «𝒩 P» s = 0"
  by (simp add:embed_bool_def negate_def)

lemma eval_nembed_false[simp]:
  "¬P s ⟹ «𝒩 P» s = 1"
  by (simp add:embed_bool_def negate_def)

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

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

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

lemma entailsD[dest]:
  "P ⊩ Q ⟹ P s ≤ Q s"
  by(simp add:le_funD)

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

lemma pconj_rzero[intro,simp]:
  "b ≤ 1 ⟹ b .& 0 = 0"
  by(simp add:pconj_def tminus_def)

lemma pconj_lone[intro,simp]:
  "0 ≤ b ⟹ 1 .& b = b"
  by(simp add:pconj_def tminus_def)

lemma pconj_rone[intro,simp]:
  "0 ≤ b ⟹ b .& 1 = b"
  by(simp add:pconj_def tminus_def)

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

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",
      simp_all add:min.absorb1 min.absorb2 pconj_mono)[],
     (cases "c ≤ d",
      simp_all add:min.absorb1 min.absorb2 pconj_mono))

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
  by(auto intro:tminus_left_mono add_right_mono)

lemma exp_conj_mono_right:
  "Q ⊩ R ⟹ P && Q ⊩ P && R"
  unfolding exp_conj_def pconj_def
  by(auto intro:tminus_left_mono add_left_mono)

lemma exp_conj_comm[ac_simps]:
  "a && b = b && a"
  by(simp add:exp_conj_def ac_simps)

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"
    by(simp add:pconj_assoc)
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"
    by(blast intro:add_mono)
  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