Quelle  Continuity.thy

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

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

section ‹Continuity›

theory Continuity imports Healthiness begin

text ‹We rely on one additional healthiness property, continuity, which is shown here seperately,
  its proof relies, in general, on healthiness. It is only relevant when a program appears
  an inductive context i.e.~inside a loop.›

text ‹A continuous transformer preserves limits (or the suprema of ascending chains).›
definition bd_cts :: "'s trans ==> bool"
where "bd_cts t = (∀M. (∀i. (M i ⊨!!! M (Suc i)) ∧ sound (M i)) ⟶
                       (∃b. ∀i. bounded_by b (M i)) ⟶
                       t (Sup_exp (range M)) = Sup_exp (range (t o M)))"

lemma bd_ctsD:
  "[ bd_cts t; ∧i. M i ⊨!!! M (Suc i); ∧i. sound (M i); ∧i. bounded_by b (M i) ] ==>
   t (Sup_exp (range M)) = Sup_exp (range (t o M))"
  unfolding bd_cts_def by(auto)

lemma bd_ctsI:
  "(∧b M. (∧i. M i ⊨!!! M (Suc i)) ==> (∧i. sound (M i)) ==> (∧i. bounded_by b (M i)) ==>
         t (Sup_exp (range M)) = Sup_exp (range (t o M))) ==> bd_cts t"
  unfolding bd_cts_def by(auto)

text ‹A generalised property for transformers of transformers.›
definition bd_cts_tr :: "('s trans ==> 's trans) ==> bool"
where "bd_cts_tr T = (∀M. (∀i. le_trans (M i) (M (Suc i)) ∧ feasible (M i)) ⟶
                          equiv_trans (T (Sup_trans (M ` UNIV))) (Sup_trans ((T o M) ` UNIV)))"

lemma bd_cts_trD:
  "[ bd_cts_tr T; ∧i. le_trans (M i) (M (Suc i)); ∧i. feasible (M i) ] ==>
   equiv_trans (T (Sup_trans (M ` UNIV))) (Sup_trans ((T o M) ` UNIV))"
  by(simp add:bd_cts_tr_def)

lemma bd_cts_trI:
  "(∧M. (∧i. le_trans (M i) (M (Suc i))) ==> (∧i. feasible (M i)) ==>
         equiv_trans (T (Sup_trans (M ` UNIV))) (Sup_trans ((T o M) ` UNIV))) ==> bd_cts_tr T"
  by(simp add:bd_cts_tr_def)

subsection ‹Continuity of Primitives›

lemma cts_wp_Abort:
  "bd_cts (wp (Abort::'s prog))"
proof -
  have X: "range (λ(i::nat) (s::'s). 0) = {λs. 0}" by(auto)
  show ?thesis by(intro bd_ctsI, simp add:wp_eval o_def Sup_exp_def X)
qed

lemma cts_wp_Skip:
  "bd_cts (wp Skip)"
  by(rule bd_ctsI, simp add:wp_def Skip_def o_def)

lemma cts_wp_Apply:
  "bd_cts (wp (Apply f))"
proof -
  have X: "∧M s. {P (f s) |P. P ∈ range M} = {P s |P. P ∈ range (λi s. M i (f s))}" by(auto)
  show ?thesis by(intro bd_ctsI ext, simp add:wp_eval o_def Sup_exp_def X)
qed

lemma cts_wp_Bind:
  fixes a::"'a ==> 's prog"
  assumes ca: "∧s. bd_cts (wp (a (f s)))"
  shows "bd_cts (wp (Bind f a))"
proof(rule bd_ctsI)
  fix M::"nat ==> 's expect" and c::real
  assume chain: "∧i. M i ⊨!!! M (Suc i)" and sM: "∧i. sound (M i)"
     and bM: "∧i. bounded_by c (M i)"
  with bd_ctsD[OF ca]
  have "∧s. wp (a (f s)) (Sup_exp (range M)) =
            Sup_exp (range (wp (a (f s)) o M))"
    by(auto)
  moreover have "∧s. {fa s |fa. fa ∈ range (λx. wp (a (f s)) (M x))} =
                      {fa s |fa. fa ∈ range (λx s. wp (a (f s)) (M x) s)}"
    by(auto)
  ultimately show "wp (Bind f a) (Sup_exp (range M)) =
                   Sup_exp (range (wp (Bind f a) ∘ M))"
    by(simp add:wp_eval o_def Sup_exp_def)
qed

text ‹The first nontrivial proof. We transform the suprema into limits, and appeal to the
  of the underlying operation (here infimum). This is typical of the remainder of the
  elements.›
lemma cts_wp_DC:
  fixes a b::"'s prog"
  assumes ca: "bd_cts (wp a)"
      and cb: "bd_cts (wp b)"
      and ha: "healthy (wp a)"
      and hb: "healthy (wp b)"
  shows "bd_cts (wp (a ⊓ b))"
proof(rule bd_ctsI, rule antisym)
  fix M::"nat ==> 's expect" and c::real
  assume chain: "∧i. M i ⊨!!! M (Suc i)" and sM: "∧i. sound (M i)"
     and bM: "∧i. bounded_by c (M i)"

  from ha hb have hab: "healthy (wp (a ⊓ b))" by(rule healthy_intros)
  from bM have leSup: "∧i. M i ⊨!!! Sup_exp (range M)" by(auto intro:Sup_exp_upper)
  from sM bM have sSup: "sound (Sup_exp (range M))" by(auto intro:Sup_exp_sound)

  show "Sup_exp (range (wp (a ⊓ b) ∘ M)) ⊨!!! wp (a ⊓ b) (Sup_exp (range M))"
  proof(rule Sup_exp_least, clarsimp, rule le_funI)
    fix i s
    from mono_transD[OF healthy_monoD[OF hab]] leSup sM sSup
    have "wp (a ⊓ b) (M i) ⊨!!! wp (a ⊓ b) (Sup_exp (range M))" by(auto)
    thus "wp (a ⊓ b) (M i) s ≤ wp (a ⊓ b) (Sup_exp (range M)) s" by(auto)

    from hab sSup have "sound (wp (a ⊓ b) (Sup_exp (range M)))" by(auto)
    thus "nneg (wp (a ⊓ b) (Sup_exp (range M)))" by(auto)
  qed

  from sM bM ha have "∧i. bounded_by c (wp a (M i))" by(auto)
  hence baM: "∧i s. wp a (M i) s ≤ c" by(auto)
  from sM bM hb have "∧i. bounded_by c (wp b (M i))" by(auto)
  hence bbM: "∧i s. wp b (M i) s ≤ c" by(auto)

  show "wp (a ⊓ b) (Sup_exp (range M)) ⊨!!! Sup_exp (range (wp (a ⊓ b) ∘ M))"
  proof(simp add:wp_eval o_def, rule le_funI)
    fix s::'s
    from bd_ctsD[OF ca, of M, OF chain sM bM] bd_ctsD[OF cb, of M, OF chain sM bM]
    have "min (wp a (Sup_exp (range M)) s) (wp b (Sup_exp (range M)) s) =
          min (Sup_exp (range (wp a o M)) s) (Sup_exp (range (wp b o M)) s)" by(simp)
    also {
      have "{f s |f. f ∈ range (λx. wp a (M x))} = range (λi. wp a (M i) s)"
           "{f s |f. f ∈ range (λx. wp b (M x))} = range (λi. wp b (M i) s)"
        by(auto)
      hence "min (Sup_exp (range (wp a o M)) s) (Sup_exp (range (wp b o M)) s) =
            min (Sup (range (λi. wp a (M i) s))) (Sup (range (λi. wp b (M i) s)))"
        by(simp add:Sup_exp_def o_def)
    }
    also {
      have "(λi. wp a (M i) s) <---- Sup (range (λi. wp a (M i) s))"
      proof(rule increasing_LIMSEQ)
        fix n
        from mono_transD[OF healthy_monoD, OF ha] sM chain
        show "wp a (M n) s ≤ wp a (M (Suc n)) s" by(auto intro:le_funD)
        from baM show "wp a (M n) s ≤ Sup (range (λi. wp a (M i) s))"
          by(intro cSup_upper bdd_aboveI, auto)

        fix e::real assume pe: "0 < e"
        from baM have cSup: "Sup (range (λi. wp a (M i) s)) ∈ closure (range (λi. wp a (M i) s))"
          by(blast intro:closure_contains_Sup)
        with pe obtain y where yin: "y ∈ (range (λi. wp a (M i) s))"
                          and dy: "dist y (Sup (range (λi. wp a (M i) s))) < e"
          by(blast dest:iffD1[OF closure_approachable])
        from yin obtain i where "y = wp a (M i) s" by(auto)
        with dy have "dist (wp a (M i) s) (Sup (range (λi. wp a (M i) s))) < e"
          by(simp)
        moreover from baM have "wp a (M i) s ≤ Sup (range (λi. wp a (M i) s))"
          by(intro cSup_upper bdd_aboveI, auto)
        ultimately have "Sup (range (λi. wp a (M i) s)) ≤ wp a (M i) s + e"
          by(simp add:dist_real_def)
        thus "∃i. Sup (range (λi. wp a (M i) s)) ≤ wp a (M i) s + e" by(auto)
      qed
      moreover
      have "(λi. wp b (M i) s) <---- Sup (range (λi. wp b (M i) s))"
      proof(rule increasing_LIMSEQ)
        fix n
        from mono_transD[OF healthy_monoD, OF hb] sM chain
        show "wp b (M n) s ≤ wp b (M (Suc n)) s" by(auto intro:le_funD)
        from bbM show "wp b (M n) s ≤ Sup (range (λi. wp b (M i) s))"
          by(intro cSup_upper bdd_aboveI, auto)

        fix e::real assume pe: "0 < e"
        from bbM have cSup: "Sup (range (λi. wp b (M i) s)) ∈ closure (range (λi. wp b (M i) s))"
          by(blast intro:closure_contains_Sup)
        with pe obtain y where yin: "y ∈ (range (λi. wp b (M i) s))"
                          and dy: "dist y (Sup (range (λi. wp b (M i) s))) < e"
          by(blast dest:iffD1[OF closure_approachable])
        from yin obtain i where "y = wp b (M i) s" by(auto)
        with dy have "dist (wp b (M i) s) (Sup (range (λi. wp b (M i) s))) < e"
          by(simp)
        moreover from bbM have "wp b (M i) s ≤ Sup (range (λi. wp b (M i) s))"
          by(intro cSup_upper bdd_aboveI, auto)
        ultimately have "Sup (range (λi. wp b (M i) s)) ≤ wp b (M i) s + e"
          by(simp add:dist_real_def)
        thus "∃i. Sup (range (λi. wp b (M i) s)) ≤ wp b (M i) s + e" by(auto)
      qed
      ultimately have "(λi. min (wp a (M i) s) (wp b (M i) s)) <----
                       min (Sup (range (λi. wp a (M i) s))) (Sup (range (λi. wp b (M i) s)))"
        by(rule tendsto_min)
      moreover have "bdd_above (range (λi. min (wp a (M i) s) (wp b (M i) s)))"
      proof(intro bdd_aboveI, clarsimp)
        fix i
        have "min (wp a (M i) s) (wp b (M i) s) ≤ wp a (M i) s" by(auto)
        also {
          from ha sM bM have "bounded_by c (wp a (M i))" by(auto)
          hence "wp a (M i) s ≤ c" by(auto)
        }
        finally show "min (wp a (M i) s) (wp b (M i) s) ≤ c" .
      qed
      ultimately
      have "min (Sup (range (λi. wp a (M i) s))) (Sup (range (λi. wp b (M i) s))) ≤
            Sup (range (λi. min (wp a (M i) s) (wp b (M i) s)))"
        by(blast intro:LIMSEQ_le_const2 cSup_upper min.mono[OF baM bbM])
    }
    also {
      have "range (λi. min (wp a (M i) s) (wp b (M i) s)) =
            {f s |f. f ∈ range (λi s. min (wp a (M i) s) (wp b (M i) s))}"
        by(auto)
      hence "Sup (range (λi. min (wp a (M i) s) (wp b (M i) s))) =
           Sup_exp (range (λi s. min (wp a (M i) s) (wp b (M i) s))) s"
        by (simp add: Sup_exp_def cong del: SUP_cong_simp)
    }
    finally show "min (wp a (Sup_exp (range M)) s) (wp b (Sup_exp (range M)) s) ≤
                  Sup_exp (range (λi s. min (wp a (M i) s) (wp b (M i) s))) s" .
  qed
qed

lemma cts_wp_Seq:
  fixes a b::"'s prog"
  assumes ca: "bd_cts (wp a)"
      and cb: "bd_cts (wp b)"
      and hb: "healthy (wp b)"
  shows "bd_cts (wp (a ;; b))"
proof(rule bd_ctsI, simp add:o_def wp_eval)
  fix M::"nat ==> 's expect" and c::real
  assume chain: "∧i. M i ⊨!!! M (Suc i)" and sM: "∧i. sound (M i)"
     and bM: "∧i. bounded_by c (M i)"
  hence "wp a (wp b (Sup_exp (range M))) = wp a (Sup_exp (range (wp b o M)))"
    by(subst bd_ctsD[OF cb], auto)
  also {
    from sM hb have "∧i. sound ((wp b o M) i)" by(auto)
    moreover from chain sM
    have "∧i. (wp b o M) i ⊨!!! (wp b o M) (Suc i)"
      by(auto intro:mono_transD[OF healthy_monoD, OF hb])
    moreover from sM bM hb have "∧i. bounded_by c ((wp b o M) i)" by(auto)
    ultimately have "wp a (Sup_exp (range (wp b o M))) =
                     Sup_exp (range (wp a o (wp b o M)))"
      by(subst bd_ctsD[OF ca], auto)
  }
  also have "Sup_exp (range (wp a o (wp b o M))) =
             Sup_exp (range (λi. wp a (wp b (M i))))"
    by(simp add:o_def)
  finally show "wp a (wp b (Sup_exp (range M))) =
                Sup_exp (range (λi. wp a (wp b (M i))))" .
qed

lemma cts_wp_PC:
  fixes a b::"'s prog"
  assumes ca: "bd_cts (wp a)"
      and cb: "bd_cts (wp b)"
      and ha: "healthy (wp a)"
      and hb: "healthy (wp b)"
      and up: "unitary p"
  shows "bd_cts (wp (PC a p b))"
proof(rule bd_ctsI, rule ext, simp add:o_def wp_eval)
  fix M::"nat ==> 's expect" and c::real and s::'s
  assume chain: "∧i. M i ⊨!!! M (Suc i)" and sM: "∧i. sound (M i)"
     and bM: "∧i. bounded_by c (M i)"

  from sM have "∧i. nneg (M i)" by(auto)
  with bM have nc: "0 ≤ c" by(auto)

  from chain sM bM have "wp a (Sup_exp (range M)) = Sup_exp (range (wp a o M))"
    by(rule bd_ctsD[OF ca])
  hence "wp a (Sup_exp (range M)) s = Sup_exp (range (wp a o M)) s"
    by(simp)
  also {
    have "{f s |f. f ∈ range (λx. wp a (M x))} = range (λi. wp a (M i) s)"
      by(auto)
    hence "Sup_exp (range (wp a o M)) s = Sup (range (λi. wp a (M i) s))"
      by(simp add:Sup_exp_def o_def)
  }
  finally have "p s * wp a (Sup_exp (range M)) s =
                p s * Sup (range (λi. wp a (M i) s))" by(simp)
  also have "... = Sup {p s * x |x. x ∈ range (λi. wp a (M i) s)}"
  proof(rule cSup_mult, blast, clarsimp)
    from up show "0 ≤ p s" by(auto)
    fix i
    from sM bM ha have "bounded_by c (wp a (M i))" by(auto)
    thus "wp a (M i) s ≤ c" by(auto)
  qed
  also {
    have "{p s * x |x. x ∈ range (λi. wp a (M i) s)} = range (λi. p s * wp a (M i) s)"
      by(auto)
    hence "Sup {p s * x |x. x ∈ range (λi. wp a (M i) s)} =
           Sup (range (λi. p s * wp a (M i) s))" by(simp)
  }
  finally have "p s * wp a (Sup_exp (range M)) s = Sup (range (λi. p s * wp a (M i) s))" .
  moreover {
    from chain sM bM have "wp b (Sup_exp (range M)) = Sup_exp (range (wp b o M))"
      by(rule bd_ctsD[OF cb])
    hence "wp b (Sup_exp (range M)) s = Sup_exp (range (wp b o M)) s"
      by(simp)
    also {
      have "{f s |f. f ∈ range (λx. wp b (M x))} = range (λi. wp b (M i) s)"
        by(auto)
      hence "Sup_exp (range (wp b o M)) s = Sup (range (λi. wp b (M i) s))"
        by(simp add:Sup_exp_def o_def)
    }
    finally have "(1 - p s) * wp b (Sup_exp (range M)) s =
                  (1 - p s) * Sup (range (λi. wp b (M i) s))" by(simp)
    also have "... = Sup {(1 - p s) * x |x. x ∈ range (λi. wp b (M i) s)}"
    proof(rule cSup_mult, blast, clarsimp)
      from up show "0 ≤ 1 - p s"
        by auto
      fix i
      from sM bM hb have "bounded_by c (wp b (M i))" by(auto)
      thus "wp b (M i) s ≤ c" by(auto)
    qed
    also {
      have "{(1 - p s) * x |x. x ∈ range (λi. wp b (M i) s)} =
            range (λi. (1 - p s) * wp b (M i) s)"
        by(auto)
      hence "Sup {(1 - p s) * x |x. x ∈ range (λi. wp b (M i) s)} =
             Sup (range (λi. (1 - p s) * wp b (M i) s))" by(simp)
    }
    finally have "(1 - p s) * wp b (Sup_exp (range M)) s =
                  Sup (range (λi. (1 - p s) * wp b (M i) s))" .
  }
  ultimately
  have "p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s =
        Sup (range (λi. p s * wp a (M i) s)) + Sup (range (λi. (1 - p s) * wp b (M i) s))"
    by(simp)
  also {
    from bM sM ha have "∧i. bounded_by c (wp a (M i))" by(auto)
    hence "∧i. wp a (M i) s ≤ c" by(auto)
    moreover from up have "0 ≤ p s" by(auto)
    ultimately have "∧i. p s * wp a (M i) s ≤ p s * c" by(auto intro:mult_left_mono)
    also from up nc have "p s * c ≤ 1 * c" by(blast intro:mult_right_mono)
    also have "... = c" by(simp)
    finally have baM: "∧i. p s * wp a (M i) s ≤ c" .

    have lima: "(λi. p s * wp a (M i) s) <---- Sup (range (λi. p s * wp a (M i) s))"
    proof(rule increasing_LIMSEQ)
      fix n
      from sM chain healthy_monoD[OF ha] have "wp a (M n) ⊨!!! wp a (M (Suc n))"
        by(auto)
      with up show "p s * wp a (M n) s ≤ p s * wp a (M (Suc n)) s"
        by(blast intro:mult_left_mono)
      from baM show "p s * wp a (M n) s ≤ Sup (range (λi. p s * wp a (M i) s))"
        by(intro cSup_upper bdd_aboveI, auto)
    next
      fix e::real
      assume pe: "0 < e"
      from baM have "Sup (range (λi. p s * wp a (M i) s)) ∈
                     closure (range (λi. p s * wp a (M i) s))"
        by(blast intro:closure_contains_Sup)
      thm closure_approachable
      with pe obtain y where yin: "y ∈ range (λi. p s * wp a (M i) s)"
                         and dy: "dist y (Sup (range (λi. p s * wp a (M i) s))) < e"
        by(blast dest:iffD1[OF closure_approachable])
      from yin obtain i where "y = p s * wp a (M i) s" by(auto)
      with dy have "dist (p s * wp a (M i) s) (Sup (range (λi. p s * wp a (M i) s))) < e"
        by(simp)
      moreover from baM have "p s * wp a (M i) s ≤ Sup (range (λi. p s * wp a (M i) s))"
        by(intro cSup_upper bdd_aboveI, auto)
      ultimately have "Sup (range (λi. p s * wp a (M i) s)) ≤ p s * wp a (M i) s + e"
        by(simp add:dist_real_def)
      thus "∃i. Sup (range (λi. p s * wp a (M i) s)) ≤ p s * wp a (M i) s + e" by(auto)
    qed

    from bM sM hb have "∧i. bounded_by c (wp b (M i))" by(auto)
    hence "∧i. wp b (M i) s ≤ c" by(auto)
    moreover from up have "0 ≤ (1 - p s)"
      by auto
    ultimately have "∧i. (1 - p s) * wp b (M i) s ≤ (1 - p s) * c" by(auto intro:mult_left_mono)
    also {
      from up have "1 - p s ≤ 1" by(auto)
      with nc have "(1 - p s) * c ≤ 1 * c" by(blast intro:mult_right_mono)
    }
    also have "1 * c = c" by(simp)
    finally have bbM: "∧i. (1 - p s) * wp b (M i) s ≤ c" .

    have limb: "(λi. (1 - p s) * wp b (M i) s) <---- Sup (range (λi. (1 - p s) * wp b (M i) s))"
    proof(rule increasing_LIMSEQ)
      fix n
      from sM chain healthy_monoD[OF hb] have "wp b (M n) ⊨!!! wp b (M (Suc n))"
        by(auto)
      moreover from up have "0 ≤ 1 - p s"
        by auto
      ultimately show "(1 - p s) * wp b (M n) s ≤ (1 - p s) * wp b (M (Suc n)) s"
        by(blast intro:mult_left_mono)
      from bbM show "(1 - p s) * wp b (M n) s ≤ Sup (range (λi. (1 - p s) * wp b (M i) s))"
        by(intro cSup_upper bdd_aboveI, auto)
    next
      fix e::real
      assume pe: "0 < e"
      from bbM have "Sup (range (λi. (1 - p s) * wp b (M i) s)) ∈
                     closure (range (λi. (1 - p s) * wp b (M i) s))"
        by(blast intro:closure_contains_Sup)
      with pe obtain y where yin: "y ∈ range (λi. (1 - p s) * wp b (M i) s)"
                         and dy: "dist y (Sup (range (λi. (1 - p s) * wp b (M i) s))) < e"
        by(blast dest:iffD1[OF closure_approachable])
      from yin obtain i where "y = (1 - p s) * wp b (M i) s" by(auto)
      with dy have "dist ((1 - p s) * wp b (M i) s)
                         (Sup (range (λi. (1 - p s) * wp b (M i) s))) < e"
        by(simp)
      moreover from bbM
      have "(1 - p s) * wp b (M i) s ≤ Sup (range (λi. (1 - p s) * wp b (M i) s))"
        by(intro cSup_upper bdd_aboveI, auto)
      ultimately have "Sup (range (λi. (1 - p s) * wp b (M i) s)) ≤ (1 - p s) * wp b (M i) s + e"
        by(simp add:dist_real_def)
      thus "∃i. Sup (range (λi. (1 - p s) * wp b (M i) s)) ≤ (1 - p s) * wp b (M i) s + e" by(auto)
    qed

    from lima limb have "(λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s) <----
      Sup (range (λi. p s * wp a (M i) s)) + Sup (range (λi. (1 - p s) * wp b (M i) s))"
      by(rule tendsto_add)
    moreover from add_mono[OF baM bbM]
    have "∧i. p s * wp a (M i) s + (1 - p s) * wp b (M i) s ≤
                       Sup (range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s))"
      by(intro cSup_upper bdd_aboveI, auto)
    ultimately have "Sup (range (λi. p s * wp a (M i) s)) +
                     Sup (range (λi. (1 - p s) * wp b (M i) s)) ≤
                     Sup (range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s))"
      by(blast intro: LIMSEQ_le_const2)
  }
  also {
    have "range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s) =
          {f s |f. f ∈ range (λx s. p s * wp a (M x) s + (1 - p s) * wp b (M x) s)}"
      by(auto)
    hence "Sup (range (λi. p s * wp a (M i) s + (1 - p s) * wp b (M i) s)) =
           Sup_exp (range (λx s. p s * wp a (M x) s + (1 - p s) * wp b (M x) s)) s"
      by (simp add: Sup_exp_def cong del: SUP_cong_simp)
  }
  finally
  have "p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s ≤
        Sup_exp (range (λi s. p s * wp a (M i) s + (1 - p s) * wp b (M i) s)) s" .
  moreover
  have "Sup_exp (range (λi s. p s * wp a (M i) s + (1 - p s) * wp b (M i) s)) s ≤
        p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s"
  proof(rule le_funD[OF Sup_exp_least], clarsimp, rule le_funI)
    fix i::nat and s::'s
    from bM have leSup: "M i ⊨!!! Sup_exp (range M)"
      by(blast intro: Sup_exp_upper)
    moreover from sM bM have sSup: "sound (Sup_exp (range M))"
      by(auto intro:Sup_exp_sound)
    moreover note healthy_monoD[OF ha] sM
    ultimately have "wp a (M i) ⊨!!! wp a (Sup_exp (range M))" by(auto)
    hence "wp a (M i) s ≤ wp a (Sup_exp (range M)) s" by(auto)
    moreover {
      from leSup sSup healthy_monoD[OF hb] sM
      have "wp b (M i) ⊨!!! wp b (Sup_exp (range M))" by(auto)
      hence "wp b (M i) s ≤ wp b (Sup_exp (range M)) s" by(auto)
    }
    moreover from up have "0 ≤ p s" "0 ≤ 1 - p s"
      by auto
    ultimately
    show "p s * wp a (M i) s + (1 - p s) * wp b (M i) s ≤
          p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s"
      by(blast intro:add_mono mult_left_mono)

    from sSup ha hb have "sound (wp a (Sup_exp (range M)))"
                         "sound (wp b (Sup_exp (range M)))"
      by(auto)
    hence "∧s. 0 ≤ wp a (Sup_exp (range M)) s" "∧s. 0 ≤ wp b (Sup_exp (range M)) s"
      by(auto)
    moreover from up have "∧s. 0 ≤ p s" "∧s. 0 ≤ 1 - p s"
      by auto
    ultimately show "nneg (λc. p c * wp a (Sup_exp (range M)) c +
                          (1 - p c) * wp b (Sup_exp (range M)) c)"
      by(blast intro:add_nonneg_nonneg mult_nonneg_nonneg)
  qed
  ultimately show "p s * wp a (Sup_exp (range M)) s + (1 - p s) * wp b (Sup_exp (range M)) s =
                  Sup_exp (range (λx s. p s * wp a (M x) s + (1 - p s) * wp b (M x) s)) s"
    by(auto)
qed

text ‹Both set-based choice operators are only continuous for finite sets (probabilistic choice
 emph{can} be extended infinitely, but we have not done so). The proofs for both are inductive,
  rely on the above results on binary operators.›

lemma SetPC_Bind:
  "SetPC a p = Bind p (λp. SetPC a (λ_. p))"
  by(intro ext, simp add:SetPC_def Bind_def Let_def)

lemma SetPC_remove:
  assumes nz: "p x ≠ 0" and n1: "p x ≠ 1"
      and fsupp: "finite (supp p)"
  shows "SetPC a (λ_. p) = PC (a x) (λ_. p x) (SetPC a (λ_. dist_remove p x))"
proof(intro ext, simp add:SetPC_def PC_def)
  fix ab P s
  from nz have "x ∈ supp p" by(simp add:supp_def)
  hence "supp p = insert x (supp p - {x})" by(auto)
  hence "(∑x∈supp p. p x * a x ab P s) =
         (∑x∈insert x (supp p - {x}). p x * a x ab P s)"
    by(simp)
  also from fsupp
  have "... = p x * a x ab P s + (∑x∈supp p - {x}. p x * a x ab P s)"
    by(blast intro:sum.insert)
  also from n1
  have "... = p x * a x ab P s + (1 - p x) * ((∑x∈supp p - {x}. p x * a x ab P s) / (1 - p x))"
    by(simp add:field_simps)
  also have "... = p x * a x ab P s +
                   (1 - p x) * ((∑y∈supp p - {x}. (p y / (1 - p x)) * a y ab P s))"
    by(simp add:sum_divide_distrib)
  also have "... = p x * a x ab P s +
                   (1 - p x) * ((∑y∈supp p - {x}. dist_remove p x y * a y ab P s))"
    by(simp add:dist_remove_def)
  also from nz n1
  have "... = p x * a x ab P s +
              (1 - p x) * ((∑y∈supp (dist_remove p x). dist_remove p x y * a y ab P s))"
    by(simp add:supp_dist_remove)
  finally show "(∑x∈supp p. p x * a x ab P s) =
                 p x * a x ab P s +
                 (1 - p x) * (∑y∈supp (dist_remove p x). dist_remove p x y * a y ab P s)" .
qed

lemma cts_bot:
  "bd_cts (λ(P::'s expect) (s::'s). 0::real)"
proof -
  have X: "∧s::'s. {(P::'s expect) s |P. P ∈ range (λP s. 0)} = {0}" by(auto)
  show ?thesis by(intro bd_ctsI, simp add:Sup_exp_def o_def X)
qed

lemma wp_SetPC_nil:
  "wp (SetPC a (λs a. 0)) = (λP s. 0)"
  by(intro ext, simp add:wp_eval)

lemma SetPC_sgl:
  "supp p = {x} ==> SetPC a (λ_. p) = (λab P s. p x * a x ab P s)"
  by(simp add:SetPC_def)

lemma bd_cts_scale:
  fixes a::"'s trans"
  assumes ca: "bd_cts a"
      and ha: "healthy a"
      and nnc: "0 ≤ c"
  shows "bd_cts (λP s. c * a P s)"
proof(intro bd_ctsI ext, simp add:o_def)
  fix M::"nat ==> 's expect" and d::real and s::'s
  assume chain: "∧i. M i ⊨!!! M (Suc i)" and sM: "∧i. sound (M i)"
     and bM: "∧i. bounded_by d (M i)"

  from sM have "∧i. nneg (M i)" by(auto)
  with bM have nnd: "0 ≤ d" by(auto)

  from sM bM have sSup: "sound (Sup_exp (range M))" by(auto intro:Sup_exp_sound)
  with healthy_scalingD[OF ha] nnc
  have "c * a (Sup_exp (range M)) s = a (λs. c * Sup_exp (range M) s) s"
    by(auto intro:scalingD)
  also {
    have "∧s. {f s |f. f ∈ range M} = range (λi. M i s)" by(auto)
    hence "a (λs. c * Sup_exp (range M) s) s =
           a (λs. c * Sup (range (λi. M i s))) s"
      by(simp add:Sup_exp_def)
  }
  also {
    from bM have "∧x s. x ∈ range (λi. M i s) ==> x ≤ d" by(auto)
    with nnc have "a (λs. c * Sup (range (λi. M i s))) s =
                   a (λs. Sup {c*x |x. x ∈ range (λi. M i s)}) s"
      by(subst cSup_mult, blast+)
  }
  also {
    have X: "∧s. {c * x |x. x ∈ range (λi. M i s)} = range (λi. c * M i s)" by(auto)
    have "a (λs. Sup {c * x |x. x ∈ range (λi. M i s)}) s =
          a (λs. Sup (range (λi. c * M i s))) s" by(simp add:X)
  }
  also {
    have "∧s. range (λi. c * M i s) = {f s |f. f ∈ range (λi s. c * M i s)}"
      by(auto)
    hence "(λs. Sup (range (λi. c * M i s))) = Sup_exp (range (λi s. c * M i s))"
      by (simp add: Sup_exp_def cong del: SUP_cong_simp)
    hence "a (λs. Sup (range (λi. c * M i s))) s =
           a (Sup_exp (range (λi s. c * M i s))) s" by(simp)
  }
  also {
    from le_funD[OF chain] nnc
    have "∧i. (λs. c * M i s) ⊨!!! (λs. c * M (Suc i) s)"
      by(auto intro:le_funI[OF mult_left_mono])
    moreover from sM nnc
    have "∧i. sound (λs. c * M i s)"
      by(auto intro:sound_intros)
    moreover from bM nnc
    have "∧i. bounded_by (c * d) (λs. c * M i s)"
      by(auto intro:mult_left_mono)
    ultimately
    have "a (Sup_exp (range (λi s. c * M i s))) =
          Sup_exp (range (a o (λi s. c * M i s)))"
      by(rule bd_ctsD[OF ca])
    hence "a (Sup_exp (range (λi s. c * M i s))) s =
          Sup_exp (range (a o (λi s. c * M i s))) s"
      by(auto)
  }
  also have "Sup_exp (range (a o (λi s. c * M i s))) s =
             Sup_exp (range (λx. a (λs. c * M x s))) s"
    by(simp add:o_def)
  also {
    from nnc sM
    have "∧x. a (λs. c * M x s) = (λs. c * a (M x) s)"
      by(auto intro:scalingD[OF healthy_scalingD, OF ha, symmetric])
    hence "Sup_exp (range (λx. a (λs. c * M x s))) s =
           Sup_exp (range (λx s. c * a (M x) s)) s"
      by(simp)
  }
  finally show "c * a (Sup_exp (range M)) s = Sup_exp (range (λx s. c * a (M x) s)) s" .
qed

lemma cts_wp_SetPC_const:
  fixes a::"'a ==> 's prog"
  assumes ca: "∧x. x ∈ (supp p) ==> bd_cts (wp (a x))"
      and ha: "∧x. x ∈ (supp p) ==> healthy (wp (a x))"
      and up: "unitary p"
      and sump: "sum p (supp p) ≤ 1"
      and fsupp: "finite (supp p)"
  shows "bd_cts (wp (SetPC a (λ_. p)))"
proof(cases "supp p = {}", simp add:supp_empty SetPC_def wp_def cts_bot)
  assume nesupp: "supp p ≠ {}"
  from fsupp have "unitary p ⟶ sum p (supp p) ≤ 1 ⟶
                   (∀x∈supp p. bd_cts (wp (a x))) ⟶
                   (∀x∈supp p. healthy (wp (a x))) ⟶
                   bd_cts (wp (SetPC a (λ_. p)))"
  proof(induct "supp p" arbitrary:p, simp add:supp_empty wp_SetPC_nil cts_bot, clarify)
    fix x::'a and F::"'a set" and p::"'a ==> real"
    assume fF: "finite F"
    assume "insert x F = supp p"
    hence pstep: "supp p = insert x F" by(simp)
    hence xin: "x ∈ supp p" by(auto)
    assume up: "unitary p" and ca: "∀x∈supp p. bd_cts (wp (a x))"
       and ha: "∀x∈supp p. healthy (wp (a x))"
       and sump: "sum p (supp p) ≤ 1"
       and xni: "x ∉ F"
    assume IH: "∧p. F = supp p ==>
                     unitary p ⟶ sum p (supp p) ≤ 1 ⟶
                     (∀x∈supp p. bd_cts (wp (a x))) ⟶
                     (∀x∈supp p. healthy (wp (a x))) ⟶
                     bd_cts (wp (SetPC a (λ_. p)))"

    from fF pstep have fsupp: "finite (supp p)" by(auto)

    from xin have nzp: "p x ≠ 0" by(simp add:supp_def)

    have xy_le_sum:
      "∧y. y ∈ supp p ==> y ≠ x ==> p x + p y ≤ sum p (supp p)"
    proof -
      fix y assume yin: "y ∈ supp p" and yne: "y ≠ x"
      from up have "0 ≤ sum p (supp p - {x,y})"
        by(auto intro:sum_nonneg)
      hence "p x + p y ≤ p x + p y + sum p (supp p - {x,y})"
        by(auto)
    also {
      from yin yne fsupp
      have "p y + sum p (supp p - {x,y}) = sum p (supp p - {x})"
        by(subst sum.insert[symmetric], (blast intro!:sum.cong)+)
      moreover
      from xin fsupp
      have "p x + sum p (supp p - {x}) = sum p (supp p)"
        by(subst sum.insert[symmetric], (blast intro!:sum.cong)+)
      ultimately
      have "p x + p y + sum p (supp p - {x, y}) = sum p (supp p)" by(simp)
    }
    finally show "p x + p y ≤ sum p (supp p)" .
    qed

    have n1p: "∧y. y ∈ supp p ==> y ≠ x ==> p x ≠ 1"
    proof(rule ccontr, simp)
      assume px1: "p x = 1"
      fix y assume yin: "y ∈ supp p" and yne: "y ≠ x"
      from up have "0 ≤ p y" by(auto)
      with yin have "0 < p y" by(auto simp:supp_def)
      hence "0 + p x < p y + p x" by(rule add_strict_right_mono)
      with px1 have "1 < p x + p y" by(simp)
      also from yin yne have "p x + p y ≤ sum p (supp p)"
        by(rule xy_le_sum)
      finally show False using sump by(simp)
    qed

    show "bd_cts (wp (SetPC a (λ_. p)))"
    proof(cases "F = {}")
      case True with pstep have "supp p = {x}" by(simp)
      hence "wp (SetPC a (λ_. p)) = (λP s. p x * wp (a x) P s)"
        by(simp add:SetPC_sgl wp_def)
      moreover {
        from up ca ha xin have "bd_cts (wp (a x))" "healthy (wp (a x))" "0 ≤ p x"
          by(auto)
        hence "bd_cts (λP s. p x * wp (a x) P s)"
          by(rule bd_cts_scale)
      } 
      ultimately show ?thesis by(simp)
    next
      assume neF: "F ≠ {}"
      then obtain y where yinF: "y ∈ F" by(auto)
      with xni have yne: "y ≠ x" by(auto)
      from yinF pstep have yin: "y ∈ supp p" by(auto)

      from supp_dist_remove[of p x, OF nzp n1p, OF yin yne]
      have supp_sub: "supp (dist_remove p x) ⊆ supp p" by(auto)

      from xin ca have cax: "bd_cts (wp (a x))" by(auto)
      from xin ha have hax: "healthy (wp (a x))" by(auto)

      from supp_sub ha have hra: "∀x∈supp (dist_remove p x). healthy (wp (a x))"
        by(auto)
      from supp_sub ca have cra: "∀x∈supp (dist_remove p x). bd_cts (wp (a x))"
        by(auto)

      from supp_dist_remove[of p x, OF nzp n1p, OF yin yne] pstep xni
      have Fsupp: "F = supp (dist_remove p x)"
        by(simp)

      have udp: "unitary (dist_remove p x)"
      proof(intro unitaryI2 nnegI bounded_byI)
        fix y
        show "0 ≤ dist_remove p x y"
        proof(cases "y=x", simp_all add:dist_remove_def)
          from up have "0 ≤ p y" "0 ≤ 1 - p x"
            by auto
          thus "0 ≤ p y / (1 - p x)"
            by(rule divide_nonneg_nonneg)
        qed
        show "dist_remove p x y ≤ 1"
        proof(cases "y=x", simp_all add:dist_remove_def,
              cases "y∈supp p", simp_all add:nsupp_zero)
          assume yne: "y ≠ x" and yin: "y ∈ supp p"
          hence "p x + p y ≤ sum p (supp p)"
            by(auto intro:xy_le_sum)
          also note sump
          finally have "p y ≤ 1 - p x" by(auto)
          moreover from up have "p x ≤ 1" by(auto)
          moreover from yin yne have "p x ≠ 1" by(rule n1p)
          ultimately show "p y / (1 - p x) ≤ 1" by(auto)
        qed
      qed

      from xin have pxn0: "p x ≠ 0" by(auto simp:supp_def)
      from yin yne have pxn1: "p x ≠ 1" by(rule n1p)

      from pxn0 pxn1 have "sum (dist_remove p x) (supp (dist_remove p x)) =
                           sum (dist_remove p x) (supp p - {x})"
        by(simp add:supp_dist_remove)
      also have "... = (∑y∈supp p - {x}. p y / (1 - p x))"
        by(simp add:dist_remove_def)
      also have "... = (∑y∈supp p - {x}. p y) / (1 - p x)"
        by(simp add:sum_divide_distrib)
      also {
        from xin have "insert x (supp p) = supp p" by(auto)
        with fsupp have "p x + (∑y∈supp p - {x}. p y) = sum p (supp p)"
          by(simp add:sum.insert[symmetric])
        also note sump
        finally have "sum p (supp p - {x}) ≤ 1 - p x" by(auto)
        moreover {
          from up have "p x ≤ 1" by(auto)
          with pxn1 have "p x < 1" by(auto)
          hence "0 < 1 - p x" by(auto)
        }
        ultimately have "sum p (supp p - {x}) / (1 - p x) ≤ 1"
          by(auto)
      }
      finally have sdp: "sum (dist_remove p x) (supp (dist_remove p x)) ≤ 1" .

      from Fsupp udp sdp hra cra IH
      have cts_dr: "bd_cts (wp (SetPC a (λ_. dist_remove p x)))"
        by(auto)

      from up have upx: "unitary (λ_. p x)" by(auto)
      
      from pxn0 pxn1 fsupp hra show ?thesis
        by(simp add:SetPC_remove,
           blast intro:cts_wp_PC cax cts_dr hax healthy_intros
                       unitary_sound[OF udp] sdp upx)
    qed
  qed
  with assms show ?thesis by(auto)
qed

lemma cts_wp_SetPC:
  fixes a::"'a ==> 's prog"
  assumes ca: "∧x s. x ∈ (supp (p s)) ==> bd_cts (wp (a x))"
      and ha: "∧x s. x ∈ (supp (p s)) ==> healthy (wp (a x))"
      and up: "∧s. unitary (p s)"
      and sump: "∧s. sum (p s) (supp (p s)) ≤ 1"
      and fsupp: "∧s. finite (supp (p s))"
  shows "bd_cts (wp (SetPC a p))"
proof -
  from assms have "bd_cts (wp (Bind p (λp. SetPC a (λ_. p))))"
    by(iprover intro!:cts_wp_Bind cts_wp_SetPC_const)
  thus ?thesis by(simp add:SetPC_Bind[symmetric])
qed

lemma wp_SetDC_Bind:
  "SetDC a S = Bind S (λS. SetDC a (λ_. S))"
  by(intro ext, simp add:SetDC_def Bind_def)

lemma SetDC_finite_insert:
  assumes fS: "finite S"
      and neS: "S ≠ {}"
  shows "SetDC a (λ_. insert x S) = a x ⊓ SetDC a (λ_. S)"
proof (intro ext, simp add: SetDC_def DC_def cong del: image_cong_simp cong add: INF_cong_simp)
  fix ab P s
  from fS have A: "finite (insert (a x ab P s) ((λx. a x ab P s) ` S))" 
           and B: "finite (((λx. a x ab P s) ` S))" by(auto)
  from neS have C: "insert (a x ab P s) ((λx. a x ab P s) ` S) ≠ {}"
            and D: "(λx. a x ab P s) ` S ≠ {}" by(auto)
  from A C have "Inf (insert (a x ab P s) ((λx. a x ab P s) ` S)) =
                 Min (insert (a x ab P s) ((λx. a x ab P s) ` S))"
    by(auto intro:cInf_eq_Min)
  also from B D have "... = min (a x ab P s) (Min ((λx. a x ab P s) ` S))"
    by(auto intro:Min_insert)
  also from B D have "... = min (a x ab P s) (Inf ((λx. a x ab P s) ` S))"
    by(simp add:cInf_eq_Min)
  finally show "(INF x∈insert x S. a x ab P s) =
    min (a x ab P s) (INF x∈S. a x ab P s)"
    by (simp cong del: INF_cong_simp)
qed

lemma SetDC_singleton:
  "SetDC a (λ_. {x}) = a x"
  by (simp add: SetDC_def cong del: INF_cong_simp)

lemma cts_wp_SetDC_const:
  fixes a::"'a ==> 's prog"
  assumes ca: "∧x. x ∈ S ==> bd_cts (wp (a x))"
      and ha: "∧x. x ∈ S ==> healthy (wp (a x))"
      and fS: "finite S"
      and neS: "S ≠ {}"
  shows "bd_cts (wp (SetDC a (λ_. S)))"
proof -
  have "finite S ==> S ≠ {} ==>
        (∀x∈S. bd_cts (wp (a x))) ⟶
        (∀x∈S. healthy (wp (a x))) ⟶
        bd_cts (wp (SetDC a (λ_. S)))"
  proof(induct S rule:finite_induct, simp, clarsimp)
    fix x::'a and F::"'a set"
    assume fF: "finite F"
       and IH: "F ≠ {} ==> bd_cts (wp (SetDC a (λ_. F)))"
       and cax: "bd_cts (wp (a x))"
       and hax: "healthy (wp (a x))"
       and haF: "∀x∈F. healthy (wp (a x))"
    show "bd_cts (wp (SetDC a (λ_. insert x F)))"
    proof(cases "F = {}", simp add:SetDC_singleton cax)
      assume "F ≠ {}"
      with fF cax hax haF IH show "bd_cts (wp (SetDC a (λ_. insert x F)))"
       by(auto intro!:cts_wp_DC healthy_intros simp:SetDC_finite_insert)
    qed
  qed
  with assms show ?thesis by(auto)
qed

lemma cts_wp_SetDC:
  fixes a::"'a ==> 's prog"
  assumes ca: "∧x s. x ∈ S s ==> bd_cts (wp (a x))"
      and ha: "∧x s. x ∈ S s ==> healthy (wp (a x))"
      and fS: "∧s. finite (S s)"
      and neS: "∧s. S s ≠ {}"
  shows "bd_cts (wp (SetDC a S))"
proof -
  from assms have "bd_cts (wp (Bind S (λS. SetDC a (λ_. S))))"
    by(iprover intro!:cts_wp_Bind cts_wp_SetDC_const)
  thus ?thesis by(simp add:wp_SetDC_Bind[symmetric])
qed

lemma cts_wp_repeat:
  "bd_cts (wp a) ==> healthy (wp a) ==> bd_cts (wp (repeat n a))"
  by(induct n, auto intro:cts_wp_Skip cts_wp_Seq healthy_intros)

lemma cts_wp_Embed:
  "bd_cts t ==> bd_cts (wp (Embed t))"
  by(simp add:wp_eval)

subsection ‹Continuity of a Single Loop Step›

text ‹A single loop iteration is continuous, in the more general sense defined above for
  transformers.›
lemma cts_wp_loopstep:
  fixes body::"'s prog"
  assumes hb: "healthy (wp body)"
      and cb: "bd_cts (wp body)"
  shows "bd_cts_tr (λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip))" (is "bd_cts_tr ?F")
proof(rule bd_cts_trI, rule le_trans_antisym)
  fix M::"nat ==> 's trans" and b::real
  assume chain: "∧i. le_trans (M i) (M (Suc i))"
     and fM:    "∧i. feasible (M i)"
  show fw: "le_trans (Sup_trans (range (?F o M))) (?F (Sup_trans (range M)))"
  proof(rule le_transI[OF Sup_trans_least2], clarsimp)
    fix P Q::"'s expect" and t
    assume sP: "sound P"
    assume nQ: "nneg Q" and bP: "bounded_by (bound_of P) Q"
    hence sQ: "sound Q" by(auto)

    from fM have fSup: "feasible (Sup_trans (range M))"
      by(auto intro:feasible_Sup_trans)

    from sQ fM have "M t Q ⊨!!! Sup_trans (range M) Q"
      by(auto intro:Sup_trans_upper2)
    moreover from sQ fM fSup
      have sMtP: "sound (M t Q)" "sound (Sup_trans (range M) Q)" by(auto)
    ultimately have "wp body (M t Q) ⊨!!! wp body (Sup_trans (range M) Q)"
      using healthy_monoD[OF hb] by(auto)
    hence "∧s. wp body (M t Q) s ≤ wp body (Sup_trans (range M) Q) s"
      by(rule le_funD)
    thus "?F (M t) Q ⊨!!! ?F (Sup_trans (range M)) Q"
      by(intro le_funI, simp add:wp_eval mult_left_mono)

    show "nneg (wp (body ;; Embed (Sup_trans (range M)) _{<guillemotleft> G ¬}⊕ Skip) Q)"
    proof(rule nnegI, simp add:wp_eval)
      fix s::'s
        from fSup sQ have "sound (Sup_trans (range M) Q)" by(auto)
        with hb have "sound (wp body (Sup_trans (range M) Q))" by(auto)
        hence "0 ≤ wp body (Sup_trans (range M) Q) s" by(auto)
        moreover from sQ have "0 ≤ Q s" by(auto)
        ultimately show "0 ≤ «G¬ s * wp body (Sup_trans (range M) Q) s + (1 - «G¬ s) * Q s"
          by(auto intro:add_nonneg_nonneg mult_nonneg_nonneg)
    qed
  next
    fix P::"'s expect" assume sP: "sound P"
    thus "nneg P" "bounded_by (bound_of P) P" by(auto)
    show "∀u∈range ((λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip)) ∘ M).
            ∀R. nneg R ∧ bounded_by (bound_of P) R ⟶
                nneg (u R) ∧ bounded_by (bound_of P) (u R)"
    proof(clarsimp, intro conjI nnegI bounded_byI, simp_all add:wp_eval)
      fix u::nat and R::"'s expect" and s::'s
      assume nR: "nneg R" and bR: "bounded_by (bound_of P) R"
      hence sR: "sound R" by(auto)
      with fM have sMuR: "sound (M u R)" by(auto)
      with hb have "sound (wp body (M u R))" by(auto)
      hence "0 ≤ wp body (M u R) s" by(auto)
      moreover from nR have "0 ≤ R s" by(auto)
      ultimately show "0 ≤ «G¬ s * wp body (M u R) s + (1 - «G¬ s) * R s"
        by(auto intro:add_nonneg_nonneg mult_nonneg_nonneg)

      from sR bR fM have "bounded_by (bound_of P) (M u R)" by(auto)
      with sMuR hb have "bounded_by (bound_of P) (wp body (M u R))" by(auto)
      hence "wp body (M u R) s ≤ bound_of P" by(auto)
      moreover from bR have "R s ≤ bound_of P" by(auto)
      ultimately have "«G¬ s * wp body (M u R) s + (1 - «G¬ s) * R s ≤
                       «G¬ s * bound_of P + (1 - «G¬ s) * bound_of P"
        by(auto intro:add_mono mult_left_mono)
      also have "... = bound_of P" by(simp add:algebra_simps)
      finally show "«G¬ s * wp body (M u R) s + (1 - «G¬ s) * R s ≤ bound_of P" .
    qed
  qed

  show "le_trans (?F (Sup_trans (range M))) (Sup_trans (range (?F o M)))"
   proof(rule le_transI, rule le_funI, simp add: wp_eval cong del: image_cong_simp)
    fix P::"'s expect" and s::'s
    assume sP: "sound P"
    have "{t P |t. t ∈ range M} = range (λi. M i P)"
      by(blast)
    hence "wp body (Sup_trans (range M) P) s = wp body (Sup_exp (range (λi. M i P))) s"
      by(simp add:Sup_trans_def)
    also {
      from sP fM have "∧i. sound (M i P)" by(auto)
      moreover from sP chain have "∧i. M i P ⊨!!! M (Suc i) P" by(auto)
      moreover {
        from sP have "bounded_by (bound_of P) P" by(auto)
        with sP fM have "∧i. bounded_by (bound_of P) (M i P)" by(auto)
      }
      ultimately have "wp body (Sup_exp (range (λi. M i P))) s =
                       Sup_exp (range (λi. wp body (M i P))) s"
        by(subst bd_ctsD[OF cb], auto simp:o_def)
    }
    also have "Sup_exp (range (λi. wp body (M i P))) s =
               Sup {f s |f. f ∈ range (λi. wp body (M i P))}"
      by(simp add:Sup_exp_def)
    finally have "«G¬ s * wp body (Sup_trans (range M) P) s + (1 - «G¬ s) * P s =
                  «G¬ s * Sup {f s |f. f ∈ range (λi. wp body (M i P))} + (1 - «G¬ s) * P s"
      by(simp)
    also {
      from sP fM have "∧i. sound (M i P)" by(auto)
      moreover from sP fM have "∧i. bounded_by (bound_of P) (M i P)" by(auto)
      ultimately have "∧i. bounded_by (bound_of P) (wp body (M i P))" using hb by(auto)
      hence bound: "∧i. wp body (M i P) s ≤ bound_of P" by(auto)
      moreover
      have "{« G ¬ s * x |x. x ∈ {f s |f. f ∈ range (λi. wp body (M i P))}} =
            {« G ¬ s * f s |f. f ∈ range (λi. wp body (M i P))}"
        by(blast)
      ultimately
      have "«G¬ s * Sup {f s |f. f ∈ range (λi. wp body (M i P))} =
            Sup {«G¬ s * f s |f. f ∈ range (λi. wp body (M i P))}"
        by(subst cSup_mult, auto)
      moreover {
        have "{x + (1-«G¬ s) * P s |x.
               x ∈ {«G¬ s * f s |f. f ∈ range (λi. wp body (M i P))}} =
              {«G¬ s * f s + (1-«G¬ s) * P s |f. f ∈ range (λi. wp body (M i P))}"
          by(blast)
        moreover from bound sP have "∧i. «G¬ s * wp body (M i P) s ≤ bound_of P"
          by(cases "G s", auto)
        ultimately
        have "Sup {«G¬ s * f s |f. f ∈ range (λi. wp body (M i P))} + (1-«G¬ s) * P s =
              Sup {«G¬ s * f s + (1-«G¬ s) * P s |f. f ∈ range (λi. wp body (M i P))}"
          by(subst cSup_add, auto)
      }
      ultimately
      have "«G¬ s * Sup {f s |f. f ∈ range (λi. wp body (M i P))} + (1-«G¬ s) * P s =
            Sup {«G¬ s * f s + (1-«G¬ s) * P s |f. f ∈ range (λi. wp body (M i P))}"
        by(simp)
    }
    also {
      have "∧i. «G¬ s * wp body (M i P) s + (1-«G¬ s) * P s =
                 ((λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip)) ∘ M) i P s"
        by(simp add:wp_eval)
      also have "∧i. ... i ≤
                 Sup {f s |f. f ∈ {t P |t. t ∈ range ((λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip)) ∘ M)}}"
      proof(intro cSup_upper bdd_aboveI, blast, clarsimp simp:wp_eval)
        fix i
        from sP have bP: "bounded_by (bound_of P) P" by(auto)
        with sP fM have "sound (M i P)" "bounded_by (bound_of P) (M i P)" by(auto)
        with hb have "bounded_by (bound_of P) (wp body (M i P))" by(auto)
        with bP have "wp body (M i P) s ≤ bound_of P" "P s ≤ bound_of P" by(auto)
        hence "«G¬ s * wp body (M i P) s + (1-«G¬ s) * P s ≤
               «G¬ s * (bound_of P) + (1-«G¬ s) * (bound_of P)"
          by(auto intro:add_mono mult_left_mono)
        also have "... = bound_of P" by(simp add:algebra_simps)
        finally show "«G¬ s * wp body (M i P) s + (1-«G¬ s) * P s ≤ bound_of P" .
      qed
      finally
      have "Sup {«G¬ s * f s + (1-«G¬ s) * P s |f. f ∈ range (λi. wp body (M i P))} ≤
            Sup {f s |f. f ∈ {t P |t. t ∈ range ((λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip)) ∘ M)}}"
        by(blast intro:cSup_least)
    }
    also have "Sup {f s |f. f ∈ {t P |t. t ∈ range ((λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip)) ∘ M)}} =
               Sup_trans (range ((λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip)) ∘ M)) P s"
      by(simp add:Sup_trans_def Sup_exp_def)
    finally show "«G¬ s * wp body (Sup_trans (range M) P) s + (1-«G¬ s) * P s ≤
                  Sup_trans (range ((λx. wp (body ;; Embed x _{<guillemotleft> G ¬}⊕ Skip)) ∘ M)) P s" .
  qed
qed

end