Theory WellDefined

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

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

section ‹Well-Defined Programs.›

theory WellDefined imports
  Healthiness
  Sublinearity
  LoopInduction
begin

text ‹The definition of a well-defined program collects the various notions of healthiness and
well-behavedness that we have so far established: healthiness of the strict and liberal
transformers, continuity and sublinearity of the strict transformers, and two new properties.
These are that the strict transformer always lies below the liberal one (i.e. that it is at least
as \emph{strict}, recalling the standard embedding of a predicate), and that expectation
conjunction is distributed between then in a particular manner, which will be crucial in
establishing the loop rules.›

subsection ‹Strict Implies Liberal›

text ‹This establishes the first connection between the strict and
  liberal interpretations (@{term wp} and @{term wlp}).›

definition
  wp_under_wlp :: "'s prog ⇒ bool"
where
  "wp_under_wlp prog ≡ ∀P. unitary P ⟶ wp prog P ⊩ wlp prog P"

lemma wp_under_wlpI[intro]:
  "⟦ ⋀P. unitary P ⟹ wp prog P ⊩ wlp prog P ⟧ ⟹ wp_under_wlp prog"
  unfolding wp_under_wlp_def by(simp)

lemma wp_under_wlpD[dest]:
  "⟦ wp_under_wlp prog; unitary P ⟧ ⟹ wp prog P ⊩ wlp prog P"
  unfolding wp_under_wlp_def by(simp)

lemma wp_under_le_trans:
  "wp_under_wlp a ⟹ le_utrans (wp a) (wlp a)"
  by(blast)

lemma wp_under_wlp_Abort:
  "wp_under_wlp Abort"
  by(rule wp_under_wlpI, unfold wp_eval, auto)

lemma wp_under_wlp_Skip:
  "wp_under_wlp Skip"
  by(rule wp_under_wlpI, unfold wp_eval, blast)

lemma wp_under_wlp_Apply:
  "wp_under_wlp (Apply f)"
  by(auto simp:wp_eval)

lemma wp_under_wlp_Seq:
  assumes h_wlp_a: "nearly_healthy (wlp a)"
      and h_wp_b:  "healthy (wp b)"
      and h_wlp_b: "nearly_healthy (wlp b)"
      and wp_u_a:  "wp_under_wlp a"
      and wp_u_b:  "wp_under_wlp b"
  shows "wp_under_wlp (a ;; b)"
proof(rule wp_under_wlpI, unfold wp_eval o_def)
  fix P::"'a ⇒ real" assume uP: "unitary P"
  with h_wp_b have "unitary (wp b P)" by(blast)
  with wp_u_a have "wp a (wp b P) ⊩ wlp a (wp b P)" by(auto)
  also {
    from wp_u_b and uP have "wp b P ⊩ wlp b P" by(blast)
    with h_wlp_a and h_wlp_b and h_wp_b and uP
    have "wlp a (wp b P) ⊩ wlp a (wlp b P)"
      by(blast intro:nearly_healthy_monoD[OF h_wlp_a])
  }
  finally show "wp a (wp b P) ⊩ wlp a (wlp b P)" .
qed

lemma wp_under_wlp_PC:
  assumes h_wp_a:  "healthy (wp a)"
      and h_wlp_a: "nearly_healthy (wlp a)"
      and h_wp_b:  "healthy (wp b)"
      and h_wlp_b: "nearly_healthy (wlp b)"
      and wp_u_a:  "wp_under_wlp a"
      and wp_u_b:  "wp_under_wlp b"
      and uP:      "unitary P"
  shows "wp_under_wlp (a ⇘P⇙⊕ b)"
proof(rule wp_under_wlpI, unfold wp_eval, rule le_funI)
  fix Q::"'a ⇒ real" and s
  assume uQ: "unitary Q"
  from uP have "P s ≤ 1" by(blast)
  hence "0 ≤ 1 - P s" by(simp)
  moreover
  from uQ and wp_u_b have "wp b Q s ≤ wlp b Q s" by(blast)
  ultimately
  have "(1 - P s) * wp b Q s ≤ (1 - P s) * wlp b Q s"
    by(blast intro:mult_left_mono)

  moreover {
    from uQ and wp_u_a have "wp a Q s ≤ wlp a Q s" by(blast)
    with uP have "P s * wp a Q s ≤ P s * wlp a Q s"
      by(blast intro:mult_left_mono)
  }

  ultimately
  show "P s * wp  a Q s + (1 - P s) * wp  b Q s ≤
        P s * wlp a Q s + (1 - P s) * wlp b Q s"
    by(blast intro: add_mono)
qed

lemma wp_under_wlp_DC:
  assumes wp_u_a:  "wp_under_wlp a"
      and wp_u_b:  "wp_under_wlp b"
  shows "wp_under_wlp (a ⨅ b)"
proof(rule wp_under_wlpI, unfold wp_eval, rule le_funI)
  fix Q::"'a ⇒ real" and s
  assume uQ: "unitary Q"

  from wp_u_a uQ have "wp a Q s ≤ wlp a Q s" by(blast)
  moreover
  from wp_u_b uQ have "wp b Q s ≤ wlp b Q s" by(blast)
  ultimately
  show "min (wp a Q s) (wp b Q s) ≤ min (wlp a Q s) (wlp b Q s)"
    by(auto)
qed

lemma wp_under_wlp_SetPC:
  assumes wp_u_f:  "⋀s a. a ∈ supp (P s) ⟹ wp_under_wlp (f a)"
      and nP:      "⋀s a. a ∈ supp (P s) ⟹ 0 ≤ P s a"
  shows "wp_under_wlp (SetPC f P)"
proof(rule wp_under_wlpI, unfold wp_eval, rule le_funI)
  fix Q::"'a ⇒ real" and s
  assume uQ: "unitary Q"

  from wp_u_f uQ nP
  show "(∑a∈supp (P s). P s a * wp (f a) Q s) ≤ (∑a∈supp (P s). P s a * wlp (f a) Q s)"
    by(auto intro!:sum_mono mult_left_mono)
qed

lemma wp_under_wlp_SetDC:
  assumes wp_u_f:  "⋀s a. a ∈ S s ⟹ wp_under_wlp (f a)"
      and hf:      "⋀s a. a ∈ S s ⟹ healthy (wp (f a))"
      and nS:      "⋀s. S s ≠ {}"
  shows "wp_under_wlp (SetDC f S)"
proof(rule wp_under_wlpI, rule le_funI, unfold wp_eval)
  fix Q::"'a ⇒ real" and s
  assume uQ: "unitary Q"

  show "Inf ((λa. wp (f a) Q s) ` S s) ≤ Inf ((λa. wlp (f a) Q s) ` S s)"
  proof(rule cInf_mono)
    from nS show "(λa. wlp (f a) Q s) ` S s ≠ {}" by(blast)

    fix x assume xin: "x ∈ (λa. wlp (f a) Q s) ` S s"
    then obtain a where ain: "a ∈ S s" and xrw: "x = wlp (f a) Q s"
      by(blast)
    with wp_u_f uQ
    have "wp (f a) Q s ≤ wlp (f a) Q s" by(blast)
    moreover from ain have "wp (f a) Q s ∈ (λa. wp (f a) Q s) ` S s"
      by(blast)
    ultimately show "∃y∈ (λa. wp (f a) Q s) ` S s. y ≤ x"
      by(auto simp:xrw)

  next
    fix y assume yin: "y ∈ (λa. wp (f a) Q s) ` S s"
    then obtain a where ain: "a ∈ S s" and yrw: "y = wp (f a) Q s"
      by(blast)
    with hf uQ have "unitary (wp (f a) Q)" by(auto)
    with yrw show "0 ≤ y" by(auto)
  qed
qed

lemma wp_under_wlp_Embed:
  "wp_under_wlp (Embed t)"
  by(rule wp_under_wlpI, unfold wp_eval, blast)

lemma wp_under_wlp_loop:
  fixes body::"'s prog"
  assumes hwp: "healthy (wp body)"
      and hwlp: "nearly_healthy (wlp body)"
      and wp_under: "wp_under_wlp body"
  shows "wp_under_wlp (do G ⟶ body od)"
proof(rule wp_under_wlpI)
  fix P::"'s expect"
  assume uP: "unitary P" hence sP: "sound P" by(auto)

  let "?X Q s" = "«G» s * wp body Q s + «𝒩 G» s * P s"
  let "?Y Q s" = "«G» s * wlp body Q s + «𝒩 G» s * P s"

  show "wp (do G ⟶ body od) P ⊩ wlp (do G ⟶ body od) P"
  proof(simp add:hwp hwlp sP uP wp_Loop1 wlp_Loop1, rule gfp_exp_upperbound)
    thm lfp_loop_fp
    from hwp sP have "lfp_exp ?X = ?X (lfp_exp ?X)"
      by(rule lfp_wp_loop_unfold)
    hence "lfp_exp ?X ⊩ ?X (lfp_exp ?X)" by(simp)
    also {
      from hwp uP have "wp body (lfp_exp ?X) ⊩ wlp body (lfp_exp ?X)"
        by(auto intro:wp_under_wlpD[OF wp_under] lfp_loop_unitary)
      hence "?X (lfp_exp ?X) ⊩ ?Y (lfp_exp ?X)"
        by(auto intro:add_mono mult_left_mono)
    }
    finally show "lfp_exp ?X ⊩ ?Y (lfp_exp ?X)" .
    from hwp uP show "unitary (lfp_exp ?X)"
      by(auto intro:lfp_loop_unitary)
  qed
qed

lemma wp_under_wlp_repeat:
  "⟦ healthy (wp a); nearly_healthy (wlp a); wp_under_wlp a ⟧ ⟹
   wp_under_wlp (repeat n a)"
  by(induct n, auto intro!:wp_under_wlp_Skip wp_under_wlp_Seq healthy_intros)

lemma wp_under_wlp_Bind:
  "⟦ ⋀s. wp_under_wlp (a (f s)) ⟧ ⟹ wp_under_wlp (Bind f a)"
  unfolding wp_under_wlp_def by(auto simp:wp_eval)

lemmas wp_under_wlp_intros =
  wp_under_wlp_Abort wp_under_wlp_Skip
  wp_under_wlp_Apply wp_under_wlp_Seq
  wp_under_wlp_PC    wp_under_wlp_DC
  wp_under_wlp_SetPC wp_under_wlp_SetDC
  wp_under_wlp_Embed wp_under_wlp_loop
  wp_under_wlp_repeat wp_under_wlp_Bind

subsection ‹Sub-Distributivity of Conjunction›

definition
  sub_distrib_pconj :: "'s prog ⇒ bool"
where
  "sub_distrib_pconj prog ≡
   ∀P Q. unitary P ⟶ unitary Q ⟶
         wlp prog P && wp prog Q ⊩ wp prog (P && Q)"

lemma sub_distrib_pconjI[intro]:
  "⟦⋀P Q. ⟦ unitary P; unitary Q ⟧ ⟹  wlp prog P && wp prog Q ⊩ wp prog (P && Q) ⟧ ⟹
    sub_distrib_pconj prog"
  unfolding sub_distrib_pconj_def by(simp)

lemma sub_distrib_pconjD[dest]:
  "⋀P Q. ⟦ sub_distrib_pconj prog; unitary P; unitary Q ⟧ ⟹
   wlp prog P && wp prog Q ⊩ wp prog (P && Q)"
  unfolding sub_distrib_pconj_def by(simp)

lemma sdp_Abort:
  "sub_distrib_pconj Abort"
  by(rule sub_distrib_pconjI, unfold wp_eval, auto intro:exp_conj_rzero)

lemma sdp_Skip:
  "sub_distrib_pconj Skip"
  by(rule sub_distrib_pconjI, simp add:wp_eval)

lemma sdp_Seq:
  fixes a and b
  assumes sdp_a:   "sub_distrib_pconj a"
      and sdp_b:   "sub_distrib_pconj b"
      and h_wp_a:  "healthy (wp a)"
      and h_wp_b:  "healthy (wp b)"
      and h_wlp_b: "nearly_healthy (wlp b)"
  shows "sub_distrib_pconj (a ;; b)"
proof(rule sub_distrib_pconjI, unfold wp_eval o_def)
  fix P::"'a ⇒ real" and Q::"'a ⇒ real"
  assume uP: "unitary P" and uQ: "unitary Q"

  with h_wp_b and h_wlp_b
  have "wlp a (wlp b P) && wp a (wp b Q) ⊩ wp a (wlp b P && wp b Q)"
    by(blast intro!:sub_distrib_pconjD[OF sdp_a])
  also {
    from sdp_b and uP and uQ
    have "wlp b P && wp b Q ⊩ wp b (P && Q)" by(blast)
    with h_wp_a h_wp_b h_wlp_b uP uQ
    have "wp a (wlp b P && wp b Q) ⊩ wp a (wp b (P && Q))"
      by(blast intro!:mono_transD[OF healthy_monoD, OF h_wp_a] unitary_sound
                      unitary_intros sound_intros)
  }
  finally show "wlp a (wlp b P) && wp a (wp b Q) ⊩ wp a (wp b (P && Q))" .
qed

lemma sdp_Apply:
  "sub_distrib_pconj (Apply f)"
  by(rule sub_distrib_pconjI, simp add:wp_eval)

lemma sdp_DC:
  fixes a::"'s prog" and b
  assumes sdp_a:   "sub_distrib_pconj a"
      and sdp_b:   "sub_distrib_pconj b"
      and h_wp_a:  "healthy (wp a)"
      and h_wp_b:  "healthy (wp b)"
      and h_wlp_b: "nearly_healthy (wlp b)"
  shows "sub_distrib_pconj (a ⨅ b)"
proof(rule sub_distrib_pconjI, unfold wp_eval, rule le_funI)
  fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
  assume uP: "unitary P" and uQ: "unitary Q"

  have "((λs. min (wlp a P s) (wlp b P s)) &&
         (λs. min (wp a Q s) (wp b Q s))) s ≤
        min (wlp a P s .& wp a Q s) (wlp b P s .& wp b Q s)"
    unfolding exp_conj_def by(rule min_pconj)
  also {
    have "(λs. wlp a P s .& wp a Q s) = wlp a P && wp a Q"
      by(simp add:exp_conj_def)
    also from sdp_a uP uQ have "... ⊩ wp a (P && Q)"
      by(blast dest:sub_distrib_pconjD)
    finally have "wlp a P s .& wp a Q s ≤ wp a (P && Q) s"
      by(rule le_funD)
    moreover {
      have "(λs. wlp b P s .& wp b Q s) = wlp b P && wp b Q"
        by(simp add:exp_conj_def)
    also from sdp_b uP uQ have "... ⊩ wp b (P && Q)"
      by(blast)
    finally have "wlp b P s .& wp b Q s ≤ wp b (P && Q) s"
      by(rule le_funD)
    }
    ultimately
    have "min (wlp a P s .& wp a Q s) (wlp b P s .& wp b Q s) ≤
          min (wp a (P && Q) s) (wp b (P && Q) s)" by(auto)
  }
  finally
  show "((λs. min (wlp a P s) (wlp b P s)) &&
         (λs. min (wp a Q s) (wp b Q s))) s ≤
        min (wp a (P && Q) s) (wp b (P && Q) s)" .
qed

lemma sdp_PC:
  fixes a::"'s prog" and b
  assumes sdp_a:   "sub_distrib_pconj a"
      and sdp_b:   "sub_distrib_pconj b"
      and h_wp_a:  "healthy (wp a)"
      and h_wp_b:  "healthy (wp b)"
      and h_wlp_b: "nearly_healthy (wlp b)"
      and uP:      "unitary P"
  shows "sub_distrib_pconj (a ⇘P⇙⊕ b)"
proof(rule sub_distrib_pconjI, unfold wp_eval, rule le_funI)
  fix Q::"'s ⇒ real" and R::"'s ⇒ real" and s::'s
  assume uQ: "unitary Q" and uR: "unitary R"

  have nnA: "0 ≤ P s" and nnB: "P s ≤ 1"
    using uP by auto
  note nn = nnA nnB

  have "((λs. P s * wlp a Q s + (1 - P s) * wlp b Q s) &&
         (λs. P s *  wp a R s + (1 - P s) *  wp b R s)) s =
        ((P s * wlp a Q s + (1 - P s) * wlp b Q s) +
         (P s *  wp a R s + (1 - P s) *  wp b R s)) ⊖ 1"
    by(simp add:exp_conj_def pconj_def)
  also have "... = P s *       (wlp a Q s + wp a R s) +
                   (1 - P s) * (wlp b Q s + wp b R s) ⊖ 1"
    by(simp add:field_simps)
  also have "... = P s *       (wlp a Q s + wp a R s) +
                   (1 - P s) * (wlp b Q s + wp b R s) ⊖
                   (P s + (1 - P s))"
    by(simp)
  also have "... ≤ (P s *       (wlp a Q s + wp a R s) ⊖ P s) +
                   ((1 - P s) * (wlp b Q s + wp b R s) ⊖ (1 - P s))"
    by(rule tminus_add_mono)
  also have "... = (P s       * (wlp a Q s + wp a R s ⊖ 1)) +
                   ((1 - P s) * (wlp b Q s + wp b R s ⊖ 1))"
    by(simp add:nn tminus_left_distrib)
  also have "... = P s *       ((wlp a Q && wp a R) s) +
                   (1 - P s) * ((wlp b Q && wp b R) s)"
    by(simp add:exp_conj_def pconj_def)
  also {
    from sdp_a sdp_b uQ uR
    have "P s * (wlp a Q && wp a R) s ≤ P s * wp a (Q && R) s"
     and "(1 - P s) * (wlp b Q && wp b R) s ≤ (1 - P s) * wp b (Q && R) s"
       by (simp_all add: entailsD mult_left_mono nn sub_distrib_pconjD)
    hence "P s *       ((wlp a Q && wp a R) s) +
           (1 - P s) * ((wlp b Q && wp b R) s) ≤
           P s * wp a (Q && R) s + (1 - P s) * wp b (Q && R) s"
      by(auto)
  }
  finally show "((λs. P s * wlp a Q s + (1 - P s) * wlp b Q s) &&
                 (λs. P s *  wp a R s + (1 - P s) *  wp b R s)) s ≤
                P s * wp a (Q && R) s + (1 - P s) * wp b (Q && R) s" .
qed

lemma sdp_Embed:
  "⟦ ⋀P Q. ⟦ unitary P; unitary Q ⟧ ⟹ t P && t Q ⊩ t (P && Q) ⟧ ⟹
   sub_distrib_pconj (Embed t)"
  by(auto simp:wp_eval)

lemma sdp_repeat:
  fixes a::"'s prog"
  assumes sdpa: "sub_distrib_pconj a"
      and hwp: "healthy (wp a)" and hwlp: "nearly_healthy (wlp a)"
  shows "sub_distrib_pconj (repeat n a)" (is "?X n")
proof(induct n)
  show "?X 0" by(simp add:sdp_Skip)
  fix n assume IH: "?X n"
  show "?X (Suc n)"
  proof(rule sub_distrib_pconjI, simp add:wp_eval)
    fix P::"'s ⇒ real" and Q::"'s ⇒ real"
    assume uP: "unitary P" and uQ: "unitary Q"
    from assms have hwlpa: "nearly_healthy (wlp (repeat n a))"
                and hwpa:  "healthy (wp (repeat n a))"
      by(auto intro:healthy_intros)
    from uP and hwlpa have "unitary (wlp (repeat n a) P)" by(blast)
    moreover from uQ and hwpa have "unitary (wp (repeat n a) Q)" by(blast)
    ultimately
    have "wlp a (wlp (repeat n a) P) && wp a (wp (repeat n a) Q) ⊩
          wp a (wlp (repeat n a) P && wp (repeat n a) Q)"
      using sdpa by(blast)
    also {
      from hwlp have "nearly_healthy (wlp (repeat n a))" by(rule healthy_intros)
      with uP have "sound (wlp (repeat n a) P)" by(auto)
      moreover from hwp uQ have "sound (wp (repeat n a) Q)"
        by(auto intro:healthy_intros)
      ultimately have "sound (wlp (repeat n a) P && wp (repeat n a) Q)"
        by(rule exp_conj_sound)
      moreover {
        from uP uQ have "sound (P && Q)" by(auto intro:exp_conj_sound)
        with hwp have "sound (wp (repeat n a) (P && Q))"
          by(auto intro:healthy_intros)
      }
      moreover from uP uQ IH
      have "wlp (repeat n a) P && wp (repeat n a) Q ⊩ wp (repeat n a) (P && Q)"
        by(blast)
      ultimately
      have "wp a (wlp (repeat n a) P && wp (repeat n a) Q) ⊩
            wp a (wp (repeat n a) (P && Q))"
        by(rule mono_transD[OF healthy_monoD, OF hwp])
    }
    finally show "wlp a (wlp (repeat n a) P) && wp a (wp (repeat n a) Q) ⊩
                  wp a (wp (repeat n a) (P && Q))" .
  qed
qed

lemma sdp_SetPC:
  fixes p::"'a ⇒ 's prog"
  assumes sdp: "⋀s a. a ∈ supp (P s) ⟹ sub_distrib_pconj (p a)"
      and fin: "⋀s. finite (supp (P s))"
      and nnp: "⋀s a. 0 ≤ P s a"
      and sub: "⋀s. sum (P s) (supp (P s)) ≤ 1"
  shows "sub_distrib_pconj (SetPC p P)"
proof(rule sub_distrib_pconjI, simp add:wp_eval, rule le_funI)
  fix Q::"'s ⇒ real" and R::"'s ⇒ real" and s::'s
  assume uQ: "unitary Q" and uR: "unitary R"
  have "((λs. ∑a∈supp (P s). P s a * wlp (p a) Q s) &&
         (λs. ∑a∈supp (P s). P s a *  wp (p a) R s)) s =
        (∑a∈supp (P s). P s a * wlp (p a) Q s) + (∑a∈supp (P s). P s a * wp (p a) R s) ⊖ 1"
    by(simp add:exp_conj_def pconj_def)
  also have "... = (∑a∈supp (P s). P s a * (wlp (p a) Q s + wp (p a) R s)) ⊖ 1"
    by(simp add: sum.distrib field_simps)
  also from sub
  have "... ≤ (∑a∈supp (P s). P s a * (wlp (p a) Q s + wp (p a) R s)) ⊖
              (∑a∈supp (P s). P s a)"
    by(rule tminus_right_antimono)
  also from fin
  have "... ≤ (∑a∈supp (P s). P s a * (wlp (p a) Q s + wp (p a) R s) ⊖ P s a)"
    by(rule tminus_sum_mono)
  also from nnp
  have "... = (∑a∈supp (P s). P s a * (wlp (p a) Q s + wp (p a) R s ⊖ 1))"
    by(simp add:tminus_left_distrib)
  also have "... = (∑a∈supp (P s). P s a * (wlp (p a) Q && wp (p a) R) s)"
    by(simp add:pconj_def exp_conj_def)
  also {
    from sdp uQ uR
    have "⋀a. a ∈ supp (P s) ⟹ wlp (p a) Q && wp (p a) R ⊩ wp (p a) (Q && R)"
      by(blast intro:sub_distrib_pconjD)
    with nnp
    have "(∑a∈supp (P s). P s a * (wlp (p a) Q && wp (p a) R) s) ≤
          (∑a∈supp (P s). P s a * (wp (p a) (Q && R)) s)"
      by(blast intro:sum_mono mult_left_mono)
  }
  finally show "((λs. ∑a∈supp (P s). P s a * wlp (p a) Q s) &&
                 (λs. ∑a∈supp (P s). P s a * wp (p a) R s)) s ≤
                (∑a∈supp (P s). P s a * wp (p a) (Q && R) s)" .
qed

lemma sdp_SetDC:
  fixes p::"'a ⇒ 's prog"
  assumes sdp: "⋀s a. a ∈ S s ⟹ sub_distrib_pconj (p a)"
      and hwp: "⋀s a. a ∈ S s ⟹ healthy (wp (p a))"
      and hwlp: "⋀s a. a ∈ S s ⟹ nearly_healthy (wlp (p a))"
      and ne:  "⋀s. S s ≠ {}"
  shows "sub_distrib_pconj (SetDC p S)"
proof(rule sub_distrib_pconjI, rule le_funI)
  fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
  assume uP: "unitary P" and uQ: "unitary Q"

  from uP hwlp
  have "⋀x. x ∈ (λa. wlp (p a) P) ` S s ⟹ unitary x" by(auto)
  hence "⋀y. y ∈ (λa. wlp (p a) P s) ` S s ⟹ 0 ≤ y" by(auto)
  hence "⋀a. a ∈ S s ⟹ wlp (SetDC p S) P s ≤ wlp (p a) P s"
    unfolding wp_eval by(intro cInf_lower bdd_belowI, auto)
  moreover {
    from uQ hwp have "⋀a. a ∈ S s ⟹  0 ≤ wp (p a) Q s" by(blast)
    hence "⋀a. a ∈ S s ⟹ wp (SetDC p S) Q s ≤ wp (p a) Q s"
    unfolding wp_eval by(intro cInf_lower bdd_belowI, auto)
  }
  ultimately
  have "⋀a. a ∈ S s ⟹ wlp (SetDC p S) P s + wp (SetDC p S) Q s ⊖ 1 ≤
                      wlp (p a) P s + wp (p a) Q s ⊖ 1"
    by(auto intro:tminus_left_mono add_mono)
  also have "⋀a. wlp (p a) P s + wp (p a) Q s ⊖ 1 = (wlp (p a) P && wp (p a) Q) s"
    by(simp add:exp_conj_def pconj_def)
  also from sdp uP uQ
  have "⋀a. a ∈ S s ⟹ ... a ≤ wp (p a) (P && Q) s"
    by(blast)
  also have "⋀a. ... a = wp (p a) (λs. P s + Q s ⊖ 1) s"
    by(simp add:exp_conj_def pconj_def)
  finally
  show "(wlp (SetDC p S) P && wp (SetDC p S) Q) s ≤ wp (SetDC p S) (P && Q) s"
    unfolding exp_conj_def pconj_def wp_eval
    using ne by(blast intro!:cInf_greatest)
qed

lemma sdp_Bind:
  "⟦ ⋀s. sub_distrib_pconj (p (f s)) ⟧ ⟹ sub_distrib_pconj (Bind f p)"
  unfolding sub_distrib_pconj_def wp_eval exp_conj_def pconj_def
  by(blast)

text ‹For loops, we again appeal to our transfinite induction principle, this time taking
advantage of the simultaneous treatment of both strict and liberal transformers.›
lemma sdp_loop:
  fixes body::"'s prog"
  assumes sdp_body: "sub_distrib_pconj body"
      and hwlp: "nearly_healthy (wlp body)"
      and hwp:  "healthy (wp body)"
  shows "sub_distrib_pconj (do G ⟶ body od)"
proof(rule sub_distrib_pconjI, rule loop_induct[OF hwp hwlp])
  fix P Q::"'s expect" and S::"('s trans × 's trans) set"
  assume uP: "unitary P" and uQ: "unitary Q"
     and ffst: "∀x∈S. feasible (fst x)"
     and usnd: "∀x∈S. ∀Q. unitary Q ⟶ unitary (snd x Q)"
     and IH: "∀x∈S. snd x P && fst x Q ⊩ fst x (P && Q)"

  show "Inf_utrans (snd ` S) P && Sup_trans (fst ` S) Q ⊩
                  Sup_trans (fst ` S) (P && Q)"
  proof(cases)
    assume "S = {}"
    thus ?thesis
      by(simp add:Inf_trans_def Sup_trans_def Inf_utrans_def
                  Inf_exp_def Sup_exp_def exp_conj_def)
  next
    assume ne: "S ≠ {}"

    let "?f s" = "1 + Sup_trans (fst ` S) (P && Q) s - Inf_utrans (snd ` S) P s"

    from ne obtain t where tin: "t ∈ fst ` S" by(auto)
    from ne obtain u where uin: "u ∈ snd ` S" by(auto)

    from tin ffst uP uQ have utPQ: "unitary (t (P && Q))"
      by(auto intro:exp_conj_unitary)
    hence "⋀s. 0 ≤ t (P && Q) s" by(auto)
    also {
      from ffst tin have le: "le_utrans t (Sup_trans (fst ` S))"
        by(auto intro:Sup_trans_upper)
      with uP uQ have "⋀s. t (P && Q) s ≤ Sup_trans (fst ` S) (P && Q) s"
        by(auto intro:exp_conj_unitary)
    }
    finally have nn_rhs: "⋀s. 0 ≤ Sup_trans (fst ` S) (P && Q) s" .

    have "⋀R. Inf_utrans (snd ` S) P && R ⊩ Sup_trans (fst ` S) (P && Q) ⟹ R ≤ ?f"
    proof(rule contrapos_pp, assumption)
      fix R
      assume "¬ R ≤ ?f"
      then obtain s where "¬ R s ≤ ?f s" by(auto)
      hence gt: "?f s < R s" by(simp)

      from nn_rhs have g1: "1 ≤ 1 + Sup_trans (fst ` S) (P && Q) s" by(auto)
      hence "Sup_trans (fst ` S) (P && Q) s = Inf_utrans (snd ` S) P s .& ?f s"
        by(simp add:pconj_def)
      also from g1 have "... = Inf_utrans (snd ` S) P s + ?f s - 1"
        by(simp)
      also from gt have "... < Inf_utrans (snd ` S) P s + R s - 1"
        by(simp)
      also {
        with g1 have "1 ≤ Inf_utrans (snd ` S) P s + R s"
          by(simp)
        hence "Inf_utrans (snd ` S) P s + R s - 1 = Inf_utrans (snd ` S) P s .& R s"
          by(simp add:pconj_def)
      }
      finally
      have "¬ (Inf_utrans (snd ` S) P && R) s ≤ Sup_trans (fst ` S) (P && Q) s"
        by(simp add:exp_conj_def)
      thus "¬ Inf_utrans (snd ` S) P && R ⊩ Sup_trans (fst ` S) (P && Q)"
        by(auto)
    qed

    moreover have "∀t∈fst ` S. Inf_utrans (snd ` S) P && t Q  ⊩ Sup_trans (fst ` S) (P && Q)"
    proof
      fix t assume tin: "t ∈ fst ` S"
      then obtain x where xin: "x ∈ S" and fx: "t = fst x" by(auto)

      from xin have "snd x ∈ snd ` S" by(auto)
      with uP usnd have "Inf_utrans (snd ` S) P ⊩ snd x P"
        by(auto intro:le_utransD[OF Inf_utrans_lower])
      hence "Inf_utrans (snd ` S) P && fst x Q ⊩ snd x P && fst x Q"
        by(auto intro:entails_frame)
      also from xin IH have "... ⊩ fst x (P && Q)"
        by(auto)
      also from xin ffst exp_conj_unitary[OF uP uQ]
      have "... ⊩ Sup_trans (fst ` S) (P && Q)"
        by(auto intro:le_utransD[OF Sup_trans_upper])
      finally show "Inf_utrans (snd ` S) P && t Q ⊩ Sup_trans (fst ` S) (P && Q)"
        by(simp add:fx)
    qed
    ultimately have bt: "∀t∈fst ` S. t Q ⊩ ?f" by(blast)

    have "Sup_trans (fst ` S) Q = Sup_exp {t Q |t. t ∈ fst ` S}"
      by(simp add:Sup_trans_def)
    also have "... ⊩ ?f"
    proof(rule Sup_exp_least)
      from bt show " ∀R∈{t Q |t. t ∈ fst ` S}. R ⊩ ?f" by(blast)
      from ne obtain t where tin: "t ∈ fst ` S" by(auto)
      with ffst uQ have "unitary (t Q)" by(auto)
      hence "λs. 0 ⊩ t Q" by(auto)
      also from tin bt have "... ⊩ ?f" by(auto)
      finally show "nneg (λs. 1 + Sup_trans (fst ` S) (P && Q) s -
                          Inf_utrans (snd ` S) P s)"
        by(auto)
    qed
    finally have "Inf_utrans (snd ` S) P && Sup_trans (fst ` S) Q ⊩
                  Inf_utrans (snd ` S) P && ?f"
      by(auto intro:entails_frame)
    also from nn_rhs have "... ⊩ Sup_trans (fst ` S) (P && Q)"
      by(simp add:exp_conj_def pconj_def)
    finally show ?thesis .
  qed

next
  fix P Q::"'s expect" and t u::"'s trans"
  assume uP: "unitary P" and uQ: "unitary Q"
     and ft: "feasible t"
     and uu: "⋀Q. unitary Q ⟹ unitary (u Q)"
     and IH: "u P && t Q ⊩ t (P && Q)"
  show "wlp (body ;; Embed u ⇘« G »⇙⊕ Skip) P &&
        wp  (body ;; Embed t ⇘« G »⇙⊕ Skip) Q ⊩
        wp  (body ;; Embed t ⇘« G »⇙⊕ Skip) (P && Q)"
  proof(rule le_funI, simp add:wp_eval exp_conj_def pconj_def)
    fix s::'s
    have "« G » s * wlp body (u P) s + (1 - « G » s) * P s +
          (« G » s * wp body (t Q) s + (1 - « G » s) * Q s) ⊖ 1 =
          (« G » s * wlp body (u P) s + « G » s * wp body (t Q) s) +
           ((1 - « G » s) * P s + (1 - « G » s) * Q s) ⊖ («G» s + (1 - «G» s))"
      by(simp add:ac_simps)
    also have "... ≤
          (« G » s * wlp body (u P) s + « G » s * wp body (t Q) s ⊖ «G» s) +
           ((1 - « G » s) * P s + (1 - « G » s) * Q s ⊖ (1 - «G» s))"
      by(rule tminus_add_mono)
    also have "... =
          « G » s * (wlp body (u P) s + wp body (t Q) s ⊖ 1) +
           (1 - « G » s) * (P s + Q s ⊖ 1)"
       by(simp add:tminus_left_distrib distrib_left)
    also {
      from uP uQ ft uu
      have "wlp body (u P) && wp body (t Q) ⊩ wp body (u P && t Q)"
        by(auto intro:sub_distrib_pconjD[OF sdp_body])
      also from IH unitary_sound[OF uP] unitary_sound[OF uQ] ft
                   unitary_sound[OF uu[OF uP]]
      have "… ≤ wp body (t (P && Q))"
        by(blast intro!:mono_transD[OF healthy_monoD, OF hwp] exp_conj_sound)
      finally have "wlp body (u P) s + wp body (t Q) s ⊖ 1 ≤
                    wp body (t (λs. P s + Q s ⊖ 1)) s"
        by(auto simp:exp_conj_def pconj_def)
      hence "« G » s * (wlp body (u P) s + wp body (t Q) s ⊖ 1) +
             (1 - « G » s) * (P s + Q s ⊖ 1) ≤
             « G » s * wp body (t (λs. P s + Q s ⊖ 1)) s +
             (1 - « G » s) * (P s + Q s ⊖ 1)"
        by(auto intro:add_right_mono mult_left_mono)
    }
    finally
    show "« G » s * wlp body (u P) s + (1 - « G » s) * P s +
          (« G » s * wp body (t Q) s + (1 - « G » s) * Q s) ⊖ 1 ≤
          « G » s * wp body (t (λs. P s + Q s ⊖ 1)) s +
          (1 - « G » s) * (P s + Q s ⊖ 1)" .
  qed
next
  fix P Q::"'s expect" and t t' u u'::"'s trans"
  assume "unitary P" "unitary Q"
         "equiv_trans t t'" "equiv_utrans u u'"
         "u P && t Q ⊩ t (P && Q)"
  thus "u' P && t' Q ⊩ t' (P && Q)"
    by(simp add:equiv_transD unitary_sound equiv_utransD exp_conj_unitary)
qed

lemmas sdp_intros =
  sdp_Abort  sdp_Skip  sdp_Apply
  sdp_Seq    sdp_DC    sdp_PC
  sdp_SetPC  sdp_SetDC sdp_Embed
  sdp_repeat sdp_Bind  sdp_loop

subsection ‹The Well-Defined Predicate.›

definition
  well_def :: "'s prog ⇒ bool"
where
  "well_def prog ≡ healthy (wp prog) ∧ nearly_healthy (wlp prog)
                 ∧ wp_under_wlp prog ∧ sub_distrib_pconj prog
                 ∧ sublinear (wp prog) ∧ bd_cts (wp prog)"

lemma well_defI[intro]:
  "⟦ healthy (wp prog); nearly_healthy (wlp prog);
     wp_under_wlp prog; sub_distrib_pconj prog; sublinear (wp prog);
     bd_cts (wp prog) ⟧ ⟹
   well_def prog"
  unfolding well_def_def by(simp)

lemma well_def_wp_healthy[dest]:
  "well_def prog ⟹ healthy (wp prog)"
  unfolding well_def_def by(simp)

lemma well_def_wlp_nearly_healthy[dest]:
  "well_def prog ⟹ nearly_healthy (wlp prog)"
  unfolding well_def_def by(simp)

lemma well_def_wp_under[dest]:
  "well_def prog ⟹ wp_under_wlp prog"
  unfolding well_def_def by(simp)

lemma well_def_sdp[dest]:
  "well_def prog ⟹ sub_distrib_pconj prog"
  unfolding well_def_def by(simp)

lemma well_def_wp_sublinear[dest]:
  "well_def prog ⟹ sublinear (wp prog)"
  unfolding well_def_def by(simp)

lemma well_def_wp_cts[dest]:
  "well_def prog ⟹ bd_cts (wp prog)"
  unfolding well_def_def by(simp)

lemmas wd_dests =
  well_def_wp_healthy well_def_wlp_nearly_healthy
  well_def_wp_under well_def_sdp
  well_def_wp_sublinear well_def_wp_cts

lemma wd_Abort:
  "well_def Abort"
  by(blast intro:healthy_wp_Abort nearly_healthy_wlp_Abort
                 wp_under_wlp_Abort sdp_Abort sublinear_wp_Abort
                 cts_wp_Abort)

lemma wd_Skip:
  "well_def Skip"
  by(blast intro:healthy_wp_Skip nearly_healthy_wlp_Skip
                 wp_under_wlp_Skip sdp_Skip sublinear_wp_Skip
                 cts_wp_Skip)

lemma wd_Apply:
  "well_def (Apply f)"
  by(blast intro:healthy_wp_Apply nearly_healthy_wlp_Apply
                 wp_under_wlp_Apply sdp_Apply sublinear_wp_Apply
                 cts_wp_Apply)

lemma wd_Seq:
  "⟦ well_def a; well_def b ⟧ ⟹ well_def (a ;; b)"
  by(blast intro:healthy_wp_Seq nearly_healthy_wlp_Seq
                 wp_under_wlp_Seq sdp_Seq sublinear_wp_Seq
                 cts_wp_Seq)

lemma wd_PC:
  "⟦ well_def a; well_def b; unitary P ⟧ ⟹ well_def (a ⇘P⇙⊕ b)"
  by(blast intro:healthy_wp_PC nearly_healthy_wlp_PC
                 wp_under_wlp_PC sdp_PC sublinear_wp_PC
                 cts_wp_PC)

lemma wd_DC:
  "⟦ well_def a; well_def b ⟧ ⟹ well_def (a ⨅ b)"
  by(blast intro:healthy_wp_DC nearly_healthy_wlp_DC
                 wp_under_wlp_DC sdp_DC sublinear_wp_DC
                 cts_wp_DC)

lemma wd_SetDC:
  "⟦ ⋀x s. x ∈ S s ⟹ well_def (a x); ⋀s. S s ≠ {};
     ⋀s. finite (S s) ⟧ ⟹ well_def (SetDC a S)"
by (simp add: cts_wp_SetDC ex_in_conv healthy_intros(17) healthy_intros(18) sdp_intros(8) sublinear_intros(8) well_def_def wp_under_wlp_intros(8))


lemma wd_SetPC:
  "⟦ ⋀x s. x ∈ (supp (p s)) ⟹ well_def (a x); ⋀s. unitary (p s); ⋀s. finite (supp (p s));
     ⋀s. sum (p s) (supp (p s)) ≤ 1 ⟧ ⟹ well_def (SetPC a p)"
  by(iprover intro!:well_defI healthy_wp_SetPC nearly_healthy_wlp_SetPC
                    wp_under_wlp_SetPC sdp_SetPC sublinear_wp_SetPC cts_wp_SetPC
             dest:wd_dests unitary_sound sound_nneg[OF unitary_sound] nnegD)

lemma wd_Embed:
  fixes t::"'s trans"
  assumes ht: "healthy t" and st: "sublinear t" and ct: "bd_cts t"
  shows "well_def (Embed t)"
proof(intro well_defI)
  from ht show "healthy (wp (Embed t))" "nearly_healthy (wlp (Embed t))"
    by(simp add:wp_def wlp_def Embed_def healthy_nearly_healthy)+
  from st show "sublinear (wp (Embed t))" by(simp add:wp_def Embed_def)
  show "wp_under_wlp (Embed t)" by(simp add:wp_under_wlp_def wp_eval)
  show "sub_distrib_pconj (Embed t)"
    by(rule sub_distrib_pconjI,
       auto intro:le_funI[OF sublinearD[OF st, where a=1 and b=1 and c=1, simplified]]
            simp:exp_conj_def pconj_def wp_def wlp_def Embed_def)
  from ct show "bd_cts (wp (Embed t))"
    by(simp add:wp_def Embed_def)
qed

lemma wd_repeat:
  "well_def a ⟹ well_def (repeat n a)"
  by(blast intro:healthy_wp_repeat nearly_healthy_wlp_repeat
                 wp_under_wlp_repeat sdp_repeat sublinear_wp_repeat cts_wp_repeat)

lemma wd_Bind:
  "⟦ ⋀s. well_def (a (f s)) ⟧ ⟹ well_def (Bind f a)"
  by(blast intro:healthy_wp_Bind nearly_healthy_wlp_Bind
                 wp_under_wlp_Bind sdp_Bind sublinear_wp_Bind cts_wp_Bind)

lemma wd_loop:
  "well_def body ⟹ well_def (do G ⟶ body od)"
  by(blast intro:healthy_wp_loop nearly_healthy_wlp_loop
                 wp_under_wlp_loop sdp_loop sublinear_wp_loop cts_wp_loop)

lemmas wd_intros =
  wd_Abort wd_Skip   wd_Apply
  wd_Embed wd_Seq    wd_PC
  wd_DC    wd_SetPC  wd_SetDC
  wd_Bind  wd_repeat wd_loop

end