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

(* 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)
  ultimately show ?thesis by(simp add:max.absorb2)
next
  case False then have "b ≤ a" by(auto)
  moreover with nn have "c * b ≤ c * a" by(auto intro:mult_left_mono)
  ultimately show ?thesis by(simp add:max.absorb1)
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)
  ultimately show ?thesis by(simp add:min.absorb2)
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)"
  proof(rule finite_induct, simp_all add:assms)
    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

lemma cSup_add:
  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"
    by(auto intro!:cSup_least add_right_mono cSup_upper bdd_aboveI)

  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}"
        by(simp add:mult.assoc[symmetric])
    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}"
      by(simp add:mult.assoc[symmetric])
  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"
        by(simp add:mult_left_mono_neg)
      with rwx show "- Sup S ≤ x" by(simp)
    qed
    hence "-1 * Inf ?T ≤ -1 * (- Sup S)"
      by(simp add:mult_left_mono_neg)
    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"
  by(simp add:supp_def)

lemma nsupp_zero:
  "x ∉ supp f ⟹ f x = 0"
  by(simp add:supp_def)

lemma sum_supp:
  fixes f::"'a::finite ⇒ real"
  shows "sum f (supp f) = sum f UNIV"
proof -
  have "sum f (UNIV - supp f) = 0"
    by(simp add:supp_def)
  hence "sum f (supp f) = sum f (UNIV - supp f) + sum f (supp f)"
    by(simp)
  also have "... = sum f UNIV"
    by(simp add:sum.subset_diff[symmetric])
  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"
  by(simp add:tminus_def)

lemma tminus_zero[simp]:
  "0 ≤ x ⟹ x ⊖ 0 = x"
  by(simp add:tminus_def)

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)
  }
  finally show ?thesis by(simp add:tminus_def)
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)
  }
  finally show ?thesis by(simp add:tminus_def)
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"
  by(simp add:tminus_def)

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

lemma tminus_add_mono:
  "(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)"
    by(rule tminus_add_mono)
  also from IH have "... ≤ (f x ⊖ g x) + (∑x∈F. f x ⊖ g x)"
    by(rule add_left_mono)
  finally show "?X (insert x F)"
    by(simp add:sum.insert[OF fF xniF])
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

(*
 * 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