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

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

section "The Algebra of pGCL"

theory Algebra imports WellDefined begin

text_raw ‹\label{s:Algebra}›

text ‹Programs in pGCL have a rich algebraic structure, largely mirroring that for GCL. We show
  programs form a lattice under refinement, with @{term "a ⊓ b"} and @{term "a ⊔ b"} as the meet
  join operators, respectively. We also take advantage of the algebraic structure to establish a
  for the modular decomposition of proofs.›

subsection ‹Program Refinement›

text_raw ‹\label{s:progref}›

text ‹Refinement in pGCL relates to refinement in GCL exactly as probabilistic entailment relates
  implication. It turns out to have a very similar algebra, the rules of which we establish
 .›

definition
  refines :: "'s prog → 's prog → bool" (infix ‹⊑› 70)
where
  "prog ⊑ prog' ≡ ∀P. sound P ⟶ wp prog P ⊨!!! wp prog' P"

lemma refinesI[intro]:
  "[ ∧P. sound P ==> wp prog P ⊨!!! wp prog' P ] ==> prog ⊑ prog'"
  unfolding refines_def by(simp)

lemma refinesD[dest]:
  "[ prog ⊑ prog'; sound P ] ==> wp prog P ⊨!!! wp prog' P"
  unfolding refines_def by(simp)

text ‹The equivalence relation below will turn out to be that induced by refinement. It is also
  application of @{term equiv_trans} to the weakest precondition.›

definition
  pequiv :: "'s prog → 's prog → bool" (infix ‹≃› 70)
where
  "prog ≃ prog' ≡ ∀P. sound P ⟶ wp prog P = wp prog' P"

lemma pequivI[intro]:
  "[ ∧P. sound P ==> wp prog P = wp prog' P ] ==> prog ≃ prog'"
  unfolding pequiv_def by(simp)

lemma pequivD[dest,simp]:
  "[ prog ≃ prog'; sound P ] ==> wp prog P = wp prog' P"
  unfolding pequiv_def by(simp)

lemma pequiv_equiv_trans:
  "a ≃ b ⟷ equiv_trans (wp a) (wp b)"
  by(auto)

subsection ‹Simple Identities›

text ‹The following identities involve only the primitive operations as defined in
 autoref{s:syntax}, and refinement as defined above.›

subsubsection ‹Laws following from the basic arithmetic of the operators seperately›

lemma DC_comm[ac_simps]:
  "a ⊓ b = b ⊓ a"
  unfolding DC_def by(simp add:ac_simps)

lemma DC_assoc[ac_simps]:
  "a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c"
  unfolding DC_def by(simp add:ac_simps)

lemma DC_idem:
  "a ⊓ a = a"
  unfolding DC_def by(simp)

lemma AC_comm[ac_simps]:
  "a ⊔ b = b ⊔ a"
  unfolding AC_def by(simp add:ac_simps)

lemma AC_assoc[ac_simps]:
  "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c"
  unfolding AC_def by(simp add:ac_simps)

lemma AC_idem:
  "a ⊔ a = a"
  unfolding AC_def by(simp)

lemma PC_quasi_comm:
  "a ⊕ b = b _{λs. 1 - p s)}⊕ a"
  unfolding PC_def by(simp add:algebra_simps)

lemma PC_idem:
  "a ⊕ a = a"
  unfolding PC_def by(simp add:algebra_simps)

lemma Seq_assoc[ac_simps]:
  "A ;; (B ;; C) = A ;; B ;; C"
  by(simp add:Seq_def o_def)

lemma Abort_refines[intro]:
  "well_def a ==> Abort ⊑ a"
  by(rule refinesI, unfold wp_eval, auto dest!:well_def_wp_healthy)

subsubsection ‹Laws relating demonic choice and refinement›

lemma left_refines_DC:
  "(a ⊓ b) ⊑ a"
  by(auto intro!:refinesI simp:wp_eval)

lemma right_refines_DC:
  "(a ⊓ b) ⊑ b"
  by(auto intro!:refinesI simp:wp_eval)

lemma DC_refines:
  fixes a::"'s prog" and b and c
  assumes rab: "a ⊑ b" and rac: "a ⊑ c"
  shows "a ⊑ (b ⊓ c)"
proof
  fix P::"'s → real" assume sP: "sound P"
  with assms have "wp a P ⊨!!! wp b P" and "wp a P ⊨!!! wp c P"
    by(auto dest:refinesD)
  thus "wp a P ⊨!!! wp (b ⊓ c) P"
    by(auto simp:wp_eval intro:min.boundedI)
qed

lemma DC_mono:
  fixes a::"'s prog"
  assumes rab: "a ⊑ b" and rcd: "c ⊑ d"
  shows "(a ⊓ c) ⊑ (b ⊓ d)"
proof(rule refinesI, unfold wp_eval, rule le_funI)
  fix P::"'s → real" and s::'s
  assume sP: "sound P"
  with assms have "wp a P s ≤ wp b P s" and "wp c P s ≤ wp d P s"
    by(auto)
  thus "min (wp a P s) (wp c P s) ≤ min (wp b P s) (wp d P s)"
    by(auto)
qed

subsubsection ‹Laws relating angelic choice and refinement›

lemma left_refines_AC:
  "a ⊑ (a ⊔ b)"
  by(auto intro!:refinesI simp:wp_eval)

lemma right_refines_AC:
  "b ⊑ (a ⊔ b)"
  by(auto intro!:refinesI simp:wp_eval)

lemma AC_refines:
  fixes a::"'s prog" and b and c
  assumes rac: "a ⊑ c" and rbc: "b ⊑ c"
  shows "(a ⊔ b) ⊑ c"
proof
  fix P::"'s → real" assume sP: "sound P"
  with assms have "∧s. wp a P s ≤ wp c P s"
              and "∧s. wp b P s ≤ wp c P s"
    by(auto dest:refinesD)
  thus "wp (a ⊔ b) P ⊨!!! wp c P"
    unfolding wp_eval by(auto)
qed

lemma AC_mono:
  fixes a::"'s prog"
  assumes rab: "a ⊑ b" and rcd: "c ⊑ d"
  shows "(a ⊔ c) ⊑ (b ⊔ d)"
proof(rule refinesI, unfold wp_eval, rule le_funI)
  fix P::"'s → real" and s::'s
  assume sP: "sound P"
  with assms have "wp a P s ≤ wp b P s" and "wp c P s ≤ wp d P s"
    by(auto)
  thus "max (wp a P s) (wp c P s) ≤ max (wp b P s) (wp d P s)"
    by(auto)
qed

subsubsection ‹Laws depending on the arithmetic of @{term "a ⊕ b"} and @{term "a ⊓ b"}
 ›

lemma DC_refines_PC:
  assumes unit: "unitary p"
  shows "(a ⊓ b) ⊑ (a ⊕ b)"
proof(rule refinesI, unfold wp_eval, rule le_funI)
  fix s and P::"'a → real" assume sound: "sound P"
  from unit have nn_p: "0 ≤ p s" by(blast)
  from unit have "p s ≤ 1" by(blast)
  hence nn_np: "0 ≤ 1 - p s" by(simp)
  show "min (wp a P s) (wp b P s) ≤ p s * wp a P s + (1 - p s) * wp b P s"
  proof(cases "wp a P s ≤ wp b P s",
      simp_all add:min.absorb1 min.absorb2)
    case True note le = this
    have "wp a P s = (p s + (1 - p s)) * wp a P s" by(simp)
    also have "... = p s * wp a P s + (1 - p s) * wp a P s"
      by(simp only: distrib_right)
    also {
      from le and nn_np have "(1 - p s) * wp a P s ≤ (1 - p s) * wp b P s"
        by(rule mult_left_mono)
      hence "p s * wp a P s + (1 - p s) * wp a P s ≤
        p s * wp a P s + (1 - p s) * wp b P s"
        by(rule add_left_mono)
    }
    finally show "wp a P s ≤ p s * wp a P s + (1 - p s) * wp b P s" .
  next
    case False
    then have le: "wp b P s ≤ wp a P s" by(simp)
    have "wp b P s = (p s + (1 - p s)) * wp b P s" by(simp)
    also have "... = p s * wp b P s + (1 - p s) * wp b P s"
      by(simp only:distrib_right)
    also {
      from le and nn_p have "p s * wp b P s ≤ p s * wp a P s"
        by(rule mult_left_mono)
      hence "p s * wp b P s + (1 - p s) * wp b P s ≤
        p s * wp a P s + (1 - p s) * wp b P s"
        by(rule add_right_mono)
    }
    finally show "wp b P s ≤ p s * wp a P s + (1 - p s) * wp b P s" .
  qed
qed

subsubsection ‹Laws depending on the arithmetic of @{term "a ⊕ b"} and @{term "a ⊔ b"}
 ›

lemma PC_refines_AC:
  assumes unit: "unitary p"
  shows "(a ⊕ b) ⊑ (a ⊔ b)"
proof(rule refinesI, unfold wp_eval, rule le_funI)
  fix s and P::"'a → real" assume sound: "sound P"

  from unit have "p s ≤ 1" by(blast)
  hence nn_np: "0 ≤ 1 - p s" by(simp)

  show "p s * wp a P s + (1 - p s) * wp b P s ≤
        max (wp a P s) (wp b P s)"
  proof(cases "wp a P s ≤ wp b P s")
    case True note leab = this
    with unit nn_np
    have "p s * wp a P s + (1 - p s) * wp b P s ≤
          p s * wp b P s + (1 - p s) * wp b P s"
      by(auto intro:add_mono mult_left_mono)
    also have "... = wp b P s"
      by(auto simp:field_simps)
    also from leab
    have "... = max (wp a P s) (wp b P s)"
      by(auto)
    finally show ?thesis .
  next
    case False note leba = this
    with unit nn_np
    have "p s * wp a P s + (1 - p s) * wp b P s ≤
          p s * wp a P s + (1 - p s) * wp a P s"
      by(auto intro:add_mono mult_left_mono)
    also have "... = wp a P s"
      by(auto simp:field_simps)
    also from leba
    have "... = max (wp a P s) (wp b P s)"
      by(auto)
    finally show ?thesis .
  qed
qed

subsubsection ‹Laws depending on the arithmetic of @{term "a ⊔ b"} and @{term "a ⊓ b"} together
 ›

lemma DC_refines_AC:
  "(a ⊓ b) ⊑ (a ⊔ b)"
  by(auto intro!:refinesI simp:wp_eval)

subsubsection ‹Laws Involving Refinement and Equivalence›

lemma pr_trans[trans]:
  fixes A::"'a prog"
  assumes prAB: "A ⊑ B"
      and prBC: "B ⊑ C"
  shows "A ⊑ C"
proof
  fix P::"'a → real" assume sP: "sound P"
  with prAB have "wp A P ⊨!!! wp B P" by(blast)
  also from sP and prBC have "... ⊨!!! wp C P" by(blast)
  finally show "wp A P ⊨!!! ..." .
qed

lemma pequiv_refl[intro!,simp]:
  "a ≃ a"
  by(auto)

lemma pequiv_comm[ac_simps]:
  "a ≃ b ⟷ b ≃ a"
  unfolding pequiv_def
  by(rule iffI, safe, simp_all)

lemma pequiv_pr[dest]:
  "a ≃ b ==> a ⊑ b"
  by(auto)

lemma pequiv_trans[intro,trans]:
  "[ a ≃ b; b ≃ c ] ==> a ≃ c"
  unfolding pequiv_def by(auto intro!:order_trans)

lemma pequiv_pr_trans[intro,trans]:
  "[ a ≃ b; b ⊑ c ] ==> a ⊑ c"
  unfolding pequiv_def refines_def by(simp)

lemma pr_pequiv_trans[intro,trans]:
  "[ a ⊑ b; b ≃ c ] ==> a ⊑ c"
  unfolding pequiv_def refines_def by(simp)

text ‹Refinement induces equivalence by antisymmetry:›
lemma pequiv_antisym:
  "[ a ⊑ b; b ⊑ a ] ==> a ≃ b"
  by(auto intro:antisym)

lemma pequiv_DC:
  "[ a ≃ c; b ≃ d ] ==> (a ⊓ b) ≃ (c ⊓ d)"
  by(auto intro!:DC_mono pequiv_antisym simp:ac_simps)

lemma pequiv_AC:
  "[ a ≃ c; b ≃ d ] ==> (a ⊔ b) ≃ (c ⊔ d)"
  by(auto intro!:AC_mono pequiv_antisym simp:ac_simps)

subsection ‹Deterministic Programs are Maximal›

text ‹Any sub-additive refinement of a deterministic program is in fact an equivalence.
  programs are thus maximal (under the refinement order) among sub-additive programs.
 ›
lemma refines_determ:
  fixes a::"'s prog"
  assumes da: "determ (wp a)"
      and wa: "well_def a"
      and wb: "well_def b"
      and dr: "a ⊑ b"
  shows "a ≃ b"
  txt ‹Proof by contradiction.›
proof(rule pequivI, rule contrapos_pp)
  from wb have "feasible (wp b)" by(auto)
  with wb have sab: "sub_add (wp b)"
    by(auto dest: sublinear_subadd[OF well_def_wp_sublinear])
  fix P::"'s → real" assume sP: "sound P"
  txt ‹Assume that @{term a} and @{term b} are not equivalent:›
  assume ne: "wp a P ≠ wp b P"
  txt ‹Find a point at which they differ. As @{term "a ⊑ b"},
 @{term "wp b P s"} must by strictly greater than @{term "wp a P s"}
 here:›
  hence "∃s. wp a P s < wp b P s"
  proof(rule contrapos_np)
    assume "¬(∃s. wp a P s < wp b P s)"
    hence "∀s. wp b P s ≤ wp a P s" by(auto simp:not_less)
    hence "wp b P ⊨!!! wp a P" by(auto)
    moreover from sP dr have "wp a P ⊨!!! wp b P" by(auto)
    ultimately show "wp a P = wp b P" by(auto)
  qed
  then obtain s where less: "wp a P s < wp b P s" by(blast)
  txt ‹Take a carefully constructed expectation:›
  let ?Pc = "λs. bound_of P - P s"
  have sPc: "sound ?Pc"
  proof(rule soundI)
    from sP have "∧s. 0 ≤ P s" by(auto)
    hence "∧s. ?Pc s ≤ bound_of P" by(auto)
    thus "bounded ?Pc" by(blast)
    from sP have "∧s. P s ≤ bound_of P" by(auto)
    hence "∧s. 0 ≤ ?Pc s"
      by auto
    thus "nneg ?Pc" by(auto)
  qed
  txt ‹We then show that @{term "wp b"} violates feasibility, and
 thus healthiness.›
  from sP have "0 ≤ bound_of P" by(auto)
  with da have "bound_of P = wp a (λs. bound_of P) s"
    by(simp add:maximalD determ_maximalD)
  also have "... = wp a (λs. ?Pc s + P s) s"
    by(simp)
  also from da sP sPc have "... = wp a ?Pc s + wp a P s"
    by(subst additiveD[OF determ_additiveD], simp_all add:sP sPc)
  also from sPc dr have "... ≤ wp b ?Pc s + wp a P s"
    by(auto)
  also from less have "... < wp b ?Pc s + wp b P s"
    by(auto)
  also from sab sP sPc have "... ≤ wp b (λs. ?Pc s + P s) s"
    by(blast)
  finally have "¬wp b (λs. bound_of P) s ≤ bound_of P"
    by(simp)
  thus "¬bounded_by (bound_of P) (wp b (λs. bound_of P))"
    by(auto)
next  
  txt ‹However,›
  fix P::"'s → real" assume sP: "sound P"
  hence "nneg (λs. bound_of P)" by(auto)
  moreover have "bounded_by (bound_of P) (λs. bound_of P)" by(auto)
  ultimately
  show "bounded_by (bound_of P) (wp b (λs. bound_of P))"
    using wb by(auto dest!:well_def_wp_healthy)
qed

subsection ‹The Algebraic Structure of Refinement›

text ‹Well-defined programs form a half-bounded semilattice under refinement, where @{term Abort}
  bottom, and @{term "a ⊓ b"} is @{term inf}. There is no unique top element, but all
 -deterministic programs are maximal.

  type that we construct here is not especially useful, but serves as a convenient way to express
  result.›

quotient_type 's program =
  "'s prog" / partial : "λa b. a ≃ b ∧ well_def a ∧ well_def b"
proof(rule part_equivpI)
  have "Skip ≃ Skip" and "well_def Skip" by(auto intro:wd_intros)
  thus "∃x. x ≃ x ∧ well_def x ∧ well_def x" by(blast)
  show "symp (λa b. a ≃ b ∧ well_def a ∧ well_def b)"
  proof(rule sympI, safe)
    fix a::"'a prog" and b
    assume "a ≃ b"
    hence "equiv_trans (wp a) (wp b)"
      by(simp add:pequiv_equiv_trans)
    thus "b ≃ a" by(simp add:ac_simps pequiv_equiv_trans)
  qed
  show "transp (λa b. a ≃ b ∧ well_def a ∧ well_def b)"
    by(rule transpI, safe, rule pequiv_trans)
qed

instantiation program :: (type) semilattice_inf begin
lift_definition
  less_eq_program :: "'a program → 'a program → bool" is refines
proof(safe)
  fix a::"'a prog" and b c d
  assume "a ≃ b" hence "b ≃ a" by(simp add:ac_simps)
  also assume "a ⊑ c"
  also assume "c ≃ d"
  finally show "b ⊑ d" .
next
  fix a::"'a prog" and b c d
  assume "a ≃ b"
  also assume "b ⊑ d"
  also assume "c ≃ d" hence "d ≃ c" by(simp add:ac_simps)
  finally show "a ⊑ c" .
qed (* XXX - what's up here? *)

lift_definition
  less_program :: "'a program → 'a program → bool"
  is "λa b. a ⊑ b ∧ ¬ b ⊑ a"
proof(safe)
  fix a::"'a prog" and b c d
  assume "a ≃ b" hence "b ≃ a" by(simp add:ac_simps)
  also assume "a ⊑ c"
  also assume "c ≃ d"
  finally show "b ⊑ d" .
next
  fix a::"'a prog" and b c d
  assume "a ≃ b"
  also assume "b ⊑ d"
  also assume "c ≃ d" hence "d ≃ c" by(simp add:ac_simps)
  finally show "a ⊑ c" .
next
  fix a b and c::"'a prog" and d
  assume "c ≃ d"
  also assume "d ⊑ b"
  also assume "a ≃ b" hence "b ≃ a" by(simp add:ac_simps)
  finally have "c ⊑ a" .
  moreover assume "¬ c ⊑ a"
  ultimately show False by(auto)
next
  fix a b and c::"'a prog" and d
  assume "c ≃ d" hence "d ≃ c" by(simp add:ac_simps)
  also assume "c ⊑ a"
  also assume "a ≃ b"
  finally have "d ⊑ b" .
  moreover assume "¬ d ⊑ b"
  ultimately show False by(auto)
qed

lift_definition
  inf_program :: "'a program → 'a program → 'a program" is DC
proof(safe)
  fix a b c d::"'s prog"
  assume "a ≃ b" and "c ≃ d"
  thus "(a ⊓ c) ≃ (b ⊓ d)" by(rule pequiv_DC)
next
  fix a c::"'s prog"
  assume "well_def a" "well_def c"
  thus "well_def (a ⊓ c)" by(rule wd_intros)
next
  fix a c::"'s prog"
  assume "well_def a" "well_def c"
  thus "well_def (a ⊓ c)" by(rule wd_intros)
qed

instance
proof
  fix x y::"'a program"
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by(transfer, simp)
  show "x ≤ x"
    by(transfer, auto)
  show "inf x y ≤ x"
    by(transfer, rule left_refines_DC)
  show "inf x y ≤ y"
    by(transfer, rule right_refines_DC)
  assume "x ≤ y" and "y ≤ x" thus "x = y"
    by(transfer, iprover intro:pequiv_antisym)
next
  fix x y z::"'a program"
  assume "x ≤ y" and "y ≤ z"
  thus "x ≤ z"
    by(transfer, iprover intro:pr_trans)
next
  fix x y z::"'a program"
  assume "x ≤ y" and "x ≤ z"
  thus "x ≤ inf y z"
    by(transfer, iprover intro:DC_refines)
qed
end

instantiation program :: (type) bot begin
lift_definition
  bot_program :: "'a program" is Abort
  by(auto intro:wd_intros)

instance ..
end

lemma eq_det: "∧a b::'s prog. [ a ≃ b; determ (wp a) ] ==> determ (wp b)"
proof(intro determI additiveI maximalI)
  fix a b::"'s prog" and P::"'s → real"
    and Q::"'s → real" and s::"'s"
  assume da: "determ (wp a)"
  assume sP: "sound P" and sQ: "sound Q"
    and eq: "a ≃ b"
  hence "wp b (λs. P s + Q s) s =
         wp a (λs. P s + Q s) s"
    by(simp add:sound_intros)
  also from da sP sQ
  have "... = wp a P s + wp a Q s"
    by(simp add:additiveD determ_additiveD)
  also from eq sP sQ
  have "... = wp b P s + wp b Q s"
    by(simp add:pequivD)
  finally show "wp b (λs. P s + Q s) s = wp b P s + wp b Q s" .
next
  fix a b::"'s prog" and c::real
  assume da: "determ (wp a)"
  assume "a ≃ b" hence "b ≃ a" by(simp add:ac_simps)
  moreover assume nn: "0 ≤ c"
  ultimately have "wp b (λ_. c) = wp a (λ_. c)"
    by(simp add:pequivD const_sound)
  also from da nn have "... = (λ_. c)"
    by(simp add:determ_maximalD maximalD)
  finally show "wp b (λ_. c) = (λ_. c)" .
qed

lift_definition
  pdeterm :: "'s program → bool"
  is "λa. determ (wp a)"
proof(safe)
  fix a b::"'s prog"
  assume "a ≃ b" and "determ (wp a)"
  thus "determ (wp b)" by(rule eq_det)
next
  fix a b::"'s prog"
  assume "a ≃ b" hence "b ≃ a" by(simp add:ac_simps)
  moreover assume "determ (wp b)"
  ultimately show "determ (wp a)" by(rule eq_det)
qed

lemma determ_maximal:
  "[ pdeterm a; a ≤ x ] ==> a = x"
  by(transfer, auto intro:refines_determ)

subsection ‹Data Refinement›

text ‹A projective data refinement construction for pGCL. By projective, we mean that the abstract
  is always a function (@{term φ}) of the concrete state. Refinement may be predicated (@{term
 }) on the state.›

definition
  drefines :: "('b → 'a) → ('b → bool) → 'a prog → 'b prog → bool"
where
  "drefines φ G A B ≡ ∀P Q. (unitary P ∧ unitary Q ∧ (P ⊨!!! wp A Q)) ⟶
                            («G¬ && (P o φ) ⊨!!! wp B (Q o φ))"

lemma drefinesD[dest]:
  "[ drefines φ G A B; unitary P; unitary Q; P ⊨!!! wp A Q ] ==>
   «G¬ && (P o φ) ⊨!!! wp B (Q o φ)"
  unfolding drefines_def by(blast)

text ‹We can alternatively use G as an assumption:›
lemma drefinesD2:
  assumes dr:  "drefines φ G A B"
      and uP:  "unitary P"
      and uQ:  "unitary Q"
      and wpA: "P ⊨!!! wp A Q"
      and G:   "G s"
  shows "(P o φ) s ≤ wp B (Q o φ) s"
proof -
  from uP have "0 ≤ (P o φ) s" unfolding o_def by(blast)
  with G have "(P o φ) s = («G¬ && (P o φ)) s"
    by(simp add:exp_conj_def)
  also from assms have "... ≤ wp B (Q o φ) s" by(blast)
  finally show "(P o φ) s ≤ ..." .
qed

text ‹This additional form is sometimes useful:›
lemma drefinesD3:
  assumes dr: "drefines φ G a b"
      and G:  "G s"
      and uQ: "unitary Q"
      and wa: "well_def a"
  shows "wp a Q (φ s) ≤ wp b (Q o φ) s"
proof -
  let "?L s'" = "wp a Q s'"
  from uQ wa have sL: "sound ?L" by(blast)
  from uQ wa have bL: "bounded_by 1 ?L" by(blast)

  have "?L ⊨!!! ?L" by(simp)
  with sL and bL and assms
  show ?thesis
    by(blast intro:drefinesD2[OF dr, where P="?L", simplified])
qed

lemma drefinesI[intro]:
  "[ ∧P Q. [ unitary P; unitary Q; P ⊨!!! wp A Q ] ==>
           «G¬ && (P o φ) ⊨!!! wp B (Q o φ) ] ==>
   drefines φ G A B"
  unfolding drefines_def by(blast)

text ‹Use G as an assumption, when showing refinement:›
lemma drefinesI2:
  fixes   A::"'a prog"
    and   B::"'b prog"
    and   φ::"'b → 'a"
    and   G::"'b → bool"
  assumes wB: "well_def B"
      and withAs:
        "∧P Q s. [ unitary P; unitary Q;
                 G s; P ⊨!!! wp A Q ] ==> (P o φ) s ≤ wp B (Q o φ) s"
  shows "drefines φ G A B"
proof
  fix P and Q
  assume uP:  "unitary P"
     and uQ:  "unitary Q"
     and wpA: "P ⊨!!! wp A Q"

  hence "∧s. G s ==> (P o φ) s ≤ wp B (Q o φ) s"
    using withAs by(blast)
  moreover
  from uQ have "unitary (Q o φ)"
    unfolding o_def by(blast)
  moreover
  from uP have "unitary (P o φ)"
    unfolding o_def by(blast)
  ultimately
  show "«G¬ && (P o φ) ⊨!!! wp B (Q o φ)"
    using wB by(blast intro:entails_pconj_assumption)
qed

lemma dr_strengthen_guard:
  fixes a::"'s prog" and b::"'t prog"
  assumes fg: "∧s. F s ==> G s"
      and drab: "drefines φ G a b"
  shows "drefines φ F a b"
proof(intro drefinesI)
  fix P Q::"'s expect"
  assume uP: "unitary P" and uQ: "unitary Q"
     and wp: "P ⊨!!! wp a Q"
  from fg have "∧s. «F¬ s ≤ «G¬ s" by(simp add:embed_bool_def)
  hence "(«F¬ && (P o φ)) ⊨!!! («G¬ && (P o φ))" by(auto intro:pconj_mono le_funI simp:exp_conj_def)
  also from drab uP uQ wp have "... ⊨!!! wp b (Q o φ)" by(auto)
  finally show "«F¬ && (P o φ) ⊨!!! wp b (Q o φ)" .
qed

text ‹Probabilistic correspondence, @{term pcorres}, is equality on distribution transformers,
  a guard. It is the analogue, for data refinement, of program equivalence for program
 .›
definition
  pcorres :: "('b → 'a) → ('b → bool) → 'a prog → 'b prog → bool"
where
  "pcorres φ G A B ⟷
   (∀Q. unitary Q ⟶ «G¬ && (wp A Q o φ) = «G¬ && wp B (Q o φ))"

lemma pcorresI:
  "[ ∧Q. unitary Q ==> «G¬ && (wp A Q o φ) = «G¬ && wp B (Q o φ) ] ==>
   pcorres φ G A B"
  by(simp add:pcorres_def)

text ‹Often easier to use, as it allows one to assume the precondition.›
lemma pcorresI2[intro]:
  fixes A::"'a prog" and B::"'b prog"
  assumes withG: "∧Q s. [ unitary Q; G s ] ==> wp A Q (φ s)= wp B (Q o φ) s"
      and wA: "well_def A"
      and wB: "well_def B"
  shows "pcorres φ G A B"
proof(rule pcorresI, rule ext)
  fix Q::"'a → real" and s::'b
  assume uQ: "unitary Q"
  hence uQφ: "unitary (Q o φ)" by(auto)
  show "(«G¬ && (wp A Q ∘ φ)) s = («G¬ && wp B (Q ∘ φ)) s"
  proof(cases "G s")
    case True note this
    moreover
    from well_def_wp_healthy[OF wA] uQ have "0 ≤ wp A Q (φ s)" by(blast)
    moreover
    from well_def_wp_healthy[OF wB] uQφ have "0 ≤ wp B (Q o φ) s" by(blast)
    ultimately show ?thesis
      using uQ by(simp add:exp_conj_def withG)
  next
    case False note this
    moreover
    from well_def_wp_healthy[OF wA] uQ have "wp A Q (φ s) ≤ 1" by(blast)
    moreover
    from well_def_wp_healthy[OF wB] uQφ have "wp B (Q o φ) s ≤ 1"
      by(blast dest!:healthy_bounded_byD intro:sound_nneg)
    ultimately show ?thesis by(simp add:exp_conj_def)
  qed
qed

lemma pcorresD:
  "[ pcorres φ G A B; unitary Q ] ==> «G¬ && (wp A Q o φ) = «G¬ && wp B (Q o φ)"
  unfolding pcorres_def by(simp)

text ‹Again, easier to use if the precondition is known to hold.›
lemma pcorresD2:
  assumes pc: "pcorres φ G A B"
      and uQ: "unitary Q"
      and wA: "well_def A" and wB: "well_def B"
      and G: "G s"
  shows "wp A Q (φ s) = wp B (Q o φ) s"
proof -
  from uQ well_def_wp_healthy[OF wA] have "0 ≤ wp A Q (φ s)" by(auto)
  with G have "wp A Q (φ s) = «G¬ s .& wp A Q (φ s)" by(simp)
  also {
    from pc uQ have "«G¬ && (wp A Q o φ) = «G¬ && wp B (Q o φ)"
      by(rule pcorresD)
    hence "«G¬ s .& wp A Q (φ s) = «G¬ s .& wp B (Q o φ) s"
      unfolding exp_conj_def o_def by(rule fun_cong)
  }
  also {
    from uQ have "sound Q" by(auto)
    hence "sound (Q o φ)" by(auto intro:sound_intros)
    with well_def_wp_healthy[OF wB] have "0 ≤ wp B (Q o φ) s" by(auto)
    with G have "«G¬ s .& wp B (Q o φ) s = wp B (Q o φ) s" by(simp)
  }
  finally show ?thesis .
qed

subsection ‹The Algebra of Data Refinement›

text ‹Program refinement implies a trivial data refinement:›
lemma refines_drefines:
  fixes a::"'s prog"
  assumes rab: "a ⊑ b" and wb: "well_def b"
  shows "drefines (λs. s) G a b"
proof(intro drefinesI2 wb, simp add:o_def)
  fix P::"'s → real" and Q::"'s → real" and s::'s
  assume sQ: "unitary Q"
  assume "P ⊨!!! wp a Q" hence "P s ≤ wp a Q s" by(auto)
  also from rab sQ have "... ≤ wp b Q s" by(auto)
  finally show "P s ≤ wp b Q s" .
qed

text ‹Data refinement is transitive:›
lemma dr_trans[trans]:
  fixes A::"'a prog" and B::"'b prog" and C::"'c prog"
  assumes drAB: "drefines φ G A B"
      and drBC: "drefines φ' G' B C"
      and Gimp: "∧s. G' s ==> G (φ' s)"
  shows "drefines (φ o φ') G' A C"
proof(rule drefinesI)
  fix P::"'a → real" and Q::"'a → real" and s::'a
  assume uP: "unitary P" and uQ: "unitary Q"
     and wpA: "P ⊨!!! wp A Q"

  have "«G'¬ && «G o φ'¬ = «G'¬"
  proof(rule ext, unfold exp_conj_def)
    fix x
    show "«G'¬ x .& «G o φ'¬ x = «G'¬ x" (is ?X)
    proof(cases "G' x")
      case False then show ?X by(simp)
    next
      case True
      moreover
      with Gimp have "(G o φ') x" by(simp add:o_def)
      ultimately
      show ?X by(simp)
    qed
  qed

  with uP
  have "«G'¬ && (P o (φ o φ')) = «G'¬ && ((«G¬ && (P o φ)) o φ')"
    by(simp add:exp_conj_assoc o_assoc)

  also {
    from uP uQ wpA and drAB
    have "«G¬ && (P o φ) ⊨!!! wp B (Q o φ)"
      by(blast intro:drefinesD)

    with drBC and uP uQ
    have "«G'¬ && ((«G¬ && (P o φ)) o φ') ⊨!!! wp C ((Q o φ) o φ')"
      by(blast intro:unitary_intros drefinesD)
  }

  finally
  show "«G'¬ && (P o (φ o φ')) ⊨!!! wp C (Q o (φ o φ'))"
    by(simp add:o_assoc)
qed

text ‹Data refinement composes with program refinement:›
lemma pr_dr_trans[trans]:
  assumes prAB: "A ⊑ B"
      and drBC: "drefines φ G B C"
  shows "drefines φ G A C"
proof(rule drefinesI)
  fix P and Q
  assume uP:  "unitary P"
     and uQ:  "unitary Q"
     and wpA: "P ⊨!!! wp A Q"

  note wpA
  also from uQ and prAB have "wp A Q ⊨!!! wp B Q" by(blast)
  finally have "P ⊨!!! wp B Q" .
  with uP uQ drBC
  show "«G¬ && (P o φ) ⊨!!! wp C (Q o φ)" by(blast intro:drefinesD)
qed

lemma dr_pr_trans[trans]:
  assumes drAB: "drefines φ G A B"
  assumes prBC: "B ⊑ C"
  shows "drefines φ G A C"
proof(rule drefinesI)
  fix P and Q
  assume uP:  "unitary P"
     and uQ:  "unitary Q"
     and wpA: "P ⊨!!! wp A Q"

  with drAB have "«G¬ && (P o φ) ⊨!!! wp B (Q o φ)" by(blast intro:drefinesD)
  also from uQ prBC have "... ⊨!!! wp C (Q o φ)" by(blast)
  finally show "«G¬ && (P o φ) ⊨!!! ..." .
qed

text ‹If the projection @{term φ} commutes with the transformer, then data refinement is
 :›
lemma dr_refl:
  assumes wa: "well_def a"
      and comm: "∧Q. unitary Q ==> wp a Q o φ ⊨!!! wp a (Q o φ)"
  shows "drefines φ G a a"
proof(intro drefinesI2 wa)
  fix P and Q and s
  assume wp: "P ⊨!!! wp a Q"
  assume uQ: "unitary Q"

  have "(P o φ) s = P (φ s)" by(simp)
  also from wp have "... ≤ wp a Q (φ s)" by(blast)
  also {
    from comm uQ have "wp a Q o φ ⊨!!! wp a (Q o φ)" by(blast)
    hence "(wp a Q o φ) s ≤ wp a (Q o φ) s" by(blast)
    hence "wp a Q (φ s) ≤ ..." by(simp)
  }
  finally show  "(P o φ) s ≤ wp a (Q o φ) s" .
qed

text ‹Correspondence implies data refinement›
lemma pcorres_drefine:
  assumes corres: "pcorres φ G A C"
      and wC: "well_def C"
  shows "drefines φ G A C"
proof
  fix P and Q
  assume uP: "unitary P" and uQ: "unitary Q"
     and wpA: "P ⊨!!! wp A Q"
  from wpA have "P o φ ⊨!!! wp A Q o φ" by(simp add:o_def le_fun_def)
  hence "«G¬ && (P o φ) ⊨!!! «G¬ && (wp A Q o φ)"
    by(rule exp_conj_mono_right)
  also from corres uQ
  have "... = «G¬ && (wp C (Q o φ))" by(rule pcorresD)
  also
  have "... ⊨!!! wp C (Q o φ)"
  proof(rule le_funI)
    fix s
    from uQ have "unitary (Q o φ)" by(rule unitary_intros)
    with well_def_wp_healthy[OF wC] have nn_wpC: "0 ≤ wp C (Q o φ) s" by(blast)
    show "(«G¬ && wp C (Q o φ)) s ≤ wp C (Q o φ) s"
    proof(cases "G s")
      case True
      with nn_wpC show ?thesis by(simp add:exp_conj_def)
    next
      case False note this
      moreover {
        from uQ have "unitary (Q o φ)" by(simp)
        with well_def_wp_healthy[OF wC] have "wp C (Q o φ) s ≤ 1" by(auto)
      }
      moreover note nn_wpC
      ultimately show ?thesis by(simp add:exp_conj_def)
    qed
  qed
  finally show "«G¬ && (P o φ) ⊨!!! wp C (Q o φ)" .
qed

text ‹Any \emph{data} refinement of a deterministic program is correspondence. This is the
  result to that relating program refinement and equivalence.›
lemma drefines_determ:
  fixes a::"'a prog" and b::"'b prog"
  assumes da: "determ (wp a)"
      and wa: "well_def a"
      and wb: "well_def b"
      and dr: "drefines φ G a b"
  shows "pcorres φ G a b"
  txt ‹The proof follows exactly the same form
 as that for program refinement: Assuming that correspondence
 \emph{doesn't} hold, we show that @{term "wp b"} is not feasible,
 and thus not healthy, contradicting the assumption.›
proof(rule pcorresI, rule contrapos_pp)
  from wb show "feasible (wp b)" by(auto)

  note ha = well_def_wp_healthy[OF wa]
  note hb = well_def_wp_healthy[OF wb]

  from wb have "sublinear (wp b)" by(auto)
  moreover from hb have "feasible (wp b)" by(auto)
  ultimately have sab: "sub_add (wp b)" by(rule sublinear_subadd)

  fix Q::"'a → real"
  assume uQ: "unitary Q"
  hence uQφ: "unitary (Q o φ)" by(auto)
  assume ne: "«G¬ && (wp a Q o φ) ≠ «G¬ && wp b (Q o φ)"
  hence ne': "wp a Q o φ ≠ wp b (Q o φ)" by(auto)

  txt ‹From refinement, @{term "«G¬ && (wp a Q o φ)"}
 lies below @{term "«G¬ && wp b (Q o φ)"}.›
  from ha uQ
  have gle: "«G¬ && (wp a Q o φ) ⊨!!! wp b (Q o φ)" by(blast intro!:drefinesD[OF dr])
  have le: "«G¬ && (wp a Q o φ) ⊨!!! «G¬ && wp b (Q o φ)"
    unfolding exp_conj_def
  proof(rule le_funI)
    fix s
    from gle have "«G¬ s .& (wp a Q o φ) s ≤ wp b (Q o φ) s"
      unfolding exp_conj_def by(auto)
    hence "«G¬ s .& («G¬ s .& (wp a Q o φ) s) ≤ «G¬ s .& wp b (Q o φ) s"
      by(auto intro:pconj_mono)
    moreover from uQ ha have "wp a Q (φ s) ≤ 1"
      by(auto dest:healthy_bounded_byD)
    moreover from uQ ha have "0 ≤ wp a Q (φ s)"
      by(auto)
    ultimately
    show "« G ¬ s .& (wp a Q ∘ φ) s ≤ « G ¬ s .& wp b (Q ∘ φ) s"
      by(simp add:pconj_assoc)
  qed

  txt ‹If the programs do not correspond, the terms must differ somewhere, and given the previous
 result, the second must be somewhere strictly larger than the first:›
  have nle: "∃s. («G¬ && (wp a Q o φ)) s < («G¬ && wp b (Q o φ)) s"
  proof(rule contrapos_np[OF ne], rule ext, rule antisym)
    fix s
    from le show "(«G¬ && (wp a Q o φ)) s ≤ («G¬ && wp b (Q o φ)) s"
      by(blast)
  next
    fix s
    assume "¬ (∃s. («G¬ && (wp a Q ∘ φ)) s < («G¬ && wp b (Q ∘ φ)) s)"
    thus " («G¬ && (wp b (Q ∘ φ))) s ≤ («G¬ && (wp a Q ∘ φ)) s"
      by(simp add:not_less)
  qed
  from this obtain s where less_s:
    "(«G¬ && (wp a Q ∘ φ)) s < («G¬ && wp b (Q ∘ φ)) s"
    by(blast)
  txt ‹The transformers themselves must differ at this point:›
  hence larger: "wp a Q (φ s) < wp b (Q ∘ φ) s"
  proof(cases "G s")
    case True
    moreover from ha uQ have "0 ≤ wp a Q (φ s)"
      by(blast)
    moreover from hb uQφ have "0 ≤ wp b (Q o φ) s"
      by(blast)
    moreover note less_s
    ultimately show ?thesis by(simp add:exp_conj_def)
  next
    case False
    moreover from ha uQ have "wp a Q (φ s) ≤ 1"
      by(blast)
    moreover {
      from uQ have "bounded_by 1 (Q o φ)"
        by(blast)
      moreover from unitary_sound[OF uQ]
      have "sound (Q o φ)" by(auto)
      ultimately have "wp b (Q o φ) s ≤ 1"
        using hb by(auto)
    }
    moreover note less_s
    ultimately show ?thesis by(simp add:exp_conj_def)
  qed
  from less_s have "(«G¬ && (wp a Q ∘ φ)) s ≠ («G¬ && wp b (Q ∘ φ)) s"
    by(force)
  txt ‹@{term G} must also hold, as otherwise both would be zero.›
  hence G_s: "G s"
  proof(rule contrapos_np)
    assume nG: "¬ G s"
    moreover from ha uQ have "wp a Q (φ s) ≤ 1"
      by(blast)
    moreover {
      from uQ have "bounded_by 1 (Q o φ)"
        by(blast)
      moreover from unitary_sound[OF uQ]
      have "sound (Q o φ)" by(auto)
      ultimately have "wp b (Q o φ) s ≤ 1"
        using hb by(auto)
    }
    ultimately
    show "(«G¬ && (wp a Q ∘ φ)) s = («G¬ && wp b (Q ∘ φ)) s"
      by(simp add:exp_conj_def)
  qed

  txt ‹Take a carefully constructed expectation:›
  let ?Qc = "λs. bound_of Q - Q s"
  have bQc: "bounded_by 1 ?Qc"
  proof(rule bounded_byI)
    fix s
    from uQ have "bound_of Q ≤ 1" and "0 ≤ Q s" by(auto)
    thus "bound_of Q - Q s ≤ 1" by(auto)
  qed
  have sQc: "sound ?Qc"
  proof(rule soundI)
    from bQc show "bounded ?Qc" by(auto)

    show "nneg ?Qc"
    proof(rule nnegI)
      fix s
      from uQ have "Q s ≤ bound_of Q" by(auto)
      thus "0 ≤ bound_of Q - Q s" by(auto)
    qed
  qed

  txt ‹By the maximality of @{term "wp a"}, @{term "wp b"} must violate feasibility, by mapping
 @{term s} to something strictly greater than @{term "bound_of Q"}.›
  from uQ have "0 ≤ bound_of Q" by(auto)
  with da have "bound_of Q = wp a (λs. bound_of Q) (φ s)"
    by(simp add:maximalD determ_maximalD)
  also have "wp a (λs. bound_of Q) (φ s) = wp a (λs. Q s + ?Qc s) (φ s)"
    by(simp)
  also {
    from da have "additive (wp a)" by(blast)
    with uQ sQc
    have "wp a (λs. Q s + ?Qc s) (φ s) =
          wp a Q (φ s) + wp a ?Qc (φ s)" by(subst additiveD, blast+)
  }
  also {
    from ha and sQc and bQc
    have "«G¬ && (wp a ?Qc o φ) ⊨!!! wp b (?Qc o φ)"
      by(blast intro!:drefinesD[OF dr])
    hence "(«G¬ && (wp a ?Qc o φ)) s ≤ wp b (?Qc o φ) s"
      by(blast)
    moreover from sQc and ha
    have "0 ≤ wp a (λs. bound_of Q - Q s) (φ s)"
      by(blast)
    ultimately
    have "wp a ?Qc (φ s) ≤ wp b (?Qc o φ) s"
      using G_s by(simp add:exp_conj_def)
    hence "wp a Q (φ s) + wp a ?Qc (φ s) ≤ wp a Q (φ s) + wp b (?Qc o φ) s"
      by(rule add_left_mono)
    also with larger
    have "wp a Q (φ s) + wp b (?Qc o φ) s <
          wp b (Q o φ) s + wp b (?Qc o φ) s"
      by(auto)
    finally
    have "wp a Q (φ s) + wp a ?Qc (φ s) <
          wp b (Q o φ) s + wp b (?Qc o φ) s" .
  }
  also from sab and unitary_sound[OF uQ] and sQc
  have "wp b (Q o φ) s + wp b (?Qc o φ) s ≤
        wp b (λs. (Q o φ) s + (?Qc o φ) s) s"
    by(blast)
  also have "... = wp b (λs. bound_of Q) s"
    by(simp)
  finally
  show "¬ feasible (wp b)"
  proof(rule contrapos_pn)
    assume fb: "feasible (wp b)"
    have "bounded_by (bound_of Q) (λs. bound_of Q)" by(blast)
    hence "bounded_by (bound_of Q) (wp b (λs. bound_of Q))"
      using uQ by(blast intro:feasible_boundedD[OF fb])
    hence "wp b (λs. bound_of Q) s ≤ bound_of Q" by(blast)
    thus "¬ bound_of Q < wp b (λs. bound_of Q) s" by(simp)
  qed
qed

subsection ‹Structural Rules for Correspondence›

lemma pcorres_Skip:
  "pcorres φ G Skip Skip"
  by(simp add:pcorres_def wp_eval)

text ‹Correspondence composes over sequential composition.›
lemma pcorres_Seq:
  fixes A::"'b prog" and B::"'c prog"
    and C::"'b prog" and D::"'c prog"
    and φ::"'c → 'b"
  assumes pcAB: "pcorres φ G A B"
      and pcCD: "pcorres φ H C D"
      and wA: "well_def A" and wB: "well_def B"
      and wC: "well_def C" and wD: "well_def D"
      and p3p2: "∧Q. unitary Q ==> «I¬ && wp B Q = wp B («H¬ && Q)"
      and p1p3: "∧s. G s ==> I s"
  shows "pcorres φ G (A;;C) (B;;D)"
proof(rule pcorresI)
  fix Q::"'b → real"
  assume uQ: "unitary Q"
  with well_def_wp_healthy[OF wC] have uCQ: "unitary (wp C Q)" by(auto)
  from uQ well_def_wp_healthy[OF wD] have uDQ: "unitary (wp D (Q o φ))"
    by(auto dest:unitary_comp)

  have p3p1: "∧R S. [ unitary R; unitary S; «I¬ && R = «I¬ && S ] ==>
                    «G¬ && R = «G¬ && S"
  proof(rule ext)
    fix R::"'c → real" and S::"'c → real" and s::'c
    assume a3: "«I¬ && R = «I¬ && S"
       and uR: "unitary R" and uS: "unitary S"
    show "(«G¬ && R) s = («G¬ && S) s"
    proof(simp add:exp_conj_def, cases "G s")
      case False note this
      moreover from uR have "R s ≤ 1" by(blast)
      moreover from uS have "S s ≤ 1" by(blast)
      ultimately show "«G¬ s .& R s = «G¬ s .& S s"
        by(simp)
    next
      case True note p1 = this
      with p1p3 have "I s" by(blast)
      with fun_cong[OF a3, where x=s] have "1 .& R s = 1 .& S s"
        by(simp add:exp_conj_def)
      with p1 show "«G¬ s .& R s = «G¬ s .& S s"
        by(simp)
    qed
  qed

  show "«G¬ && (wp (A;;C) Q o φ) = «G¬ && wp (B;;D) (Q o φ)"
  proof(simp add:wp_eval)
    from uCQ pcAB have "«G¬ && (wp A (wp C Q) ∘ φ) =
                        «G¬ && wp B ((wp C Q) ∘ φ)"
      by(auto dest:pcorresD)
    also have "«G¬ && wp B ((wp C Q) ∘ φ) =
               «G¬ && wp B (wp D (Q ∘ φ))"
    proof(rule p3p1)
      from uCQ well_def_wp_healthy[OF wB] show "unitary (wp B (wp C Q ∘ φ))"
        by(auto intro:unitary_comp)
      from uDQ well_def_wp_healthy[OF wB] show "unitary (wp B (wp D (Q ∘ φ)))"
        by(auto)

      from uQ have "« H ¬ && (wp C Q ∘ φ) = « H ¬ && wp D (Q ∘ φ)"
        by(blast intro:pcorresD[OF pcCD])
      thus "« I ¬ && wp B (wp C Q ∘ φ) = « I ¬ && wp B (wp D (Q ∘ φ))"
        by(simp add:p3p2 uCQ uDQ)
    qed
    finally show "«G¬ && (wp A (wp C Q) ∘ φ) = «G¬ && wp B (wp D (Q ∘ φ))" .
  qed
qed

subsection ‹Structural Rules for Data Refinement›

lemma dr_Skip:
  fixes φ::"'c → 'b"
  shows "drefines φ G Skip Skip"
proof(intro drefinesI2 wd_intros)
  fix P::"'b → real" and Q::"'b → real" and s::'c
  assume "P ⊨!!! wp Skip Q"
  hence "(P o φ) s ≤ wp Skip Q (φ s)" by(simp, blast)
  thus "(P o φ) s ≤ wp Skip (Q o φ) s" by(simp add:wp_eval)
qed

lemma dr_Abort:
  fixes φ::"'c → 'b"
  shows "drefines φ G Abort Abort"
proof(intro drefinesI2 wd_intros)
  fix P::"'b → real" and Q::"'b → real" and s::'c
  assume "P ⊨!!! wp Abort Q"
  hence "(P o φ) s ≤ wp Abort Q (φ s)" by(auto)
  thus "(P o φ) s ≤ wp Abort (Q o φ) s" by(simp add:wp_eval)
qed

lemma dr_Apply:
  fixes φ::"'c → 'b"
  assumes commutes: "f o φ = φ o g"
  shows "drefines φ G (Apply f) (Apply g)"
proof(intro drefinesI2 wd_intros)
  fix P::"'b → real" and Q::"'b → real" and s::'c

  assume wp: "P ⊨!!! wp (Apply f) Q"
  hence "P ⊨!!! (Q o f)" by(simp add:wp_eval)
  hence "P (φ s) ≤ (Q o f) (φ s)" by(blast)
  also have "... = Q ((f o φ) s)" by(simp)
  also with commutes
  have "... = ((Q o φ) o g) s" by(simp)
  also have "... = wp (Apply g) (Q o φ) s"
    by(simp add:wp_eval)
  finally show "(P o φ) s ≤ wp (Apply g) (Q o φ) s" by(simp)
qed

lemma dr_Seq:
  assumes drAB: "drefines φ P A B"
      and drBC: "drefines φ Q C D"
      and wpB:  "«P¬ ⊨!!! wp B «Q¬"
      and wB:   "well_def B"
      and wC:   "well_def C"
      and wD:   "well_def D"
  shows "drefines φ P (A;;C) (B;;D)"
proof
  fix R and S
  assume uR: "unitary R" and uS: "unitary S"
     and wpAC: "R ⊨!!! wp (A;;C) S"

  from uR
  have "«P¬ && (R o φ) = «P¬ && («P¬ && (R o φ))"
    by(simp add:exp_conj_assoc)

  also {
    from well_def_wp_healthy[OF wC] uR uS
     and wpAC[unfolded eval_wp_Seq o_def]
    have "«P¬ && (R o φ) ⊨!!! wp B (wp C S o φ)"
      by(auto intro:drefinesD[OF drAB])
    with wpB well_def_wp_healthy[OF wC] uS
         sublinear_sub_conj[OF well_def_wp_sublinear, OF wB]
    have "«P¬ && («P¬ && (R o φ)) ⊨!!! wp B («Q¬ && (wp C S o φ))"
      by(auto intro!:entails_combine dest!:unitary_sound)
  }

  also {
    from uS well_def_wp_healthy[OF wC]
    have "«Q¬ && (wp C S o φ) ⊨!!! wp D (S o φ)"
      by(auto intro!:drefinesD[OF drBC])
    with well_def_wp_healthy[OF wB] well_def_wp_healthy[OF wC]
         well_def_wp_healthy[OF wD] and unitary_sound[OF uS]
    have "wp B («Q¬ && (wp C S o φ)) ⊨!!! wp B (wp D (S o φ))"
      by(blast intro!:mono_transD)
  }

  finally
  show "«P¬ && (R o φ) ⊨!!! wp (B;;D) (S o φ)"
    unfolding wp_eval o_def .
qed

lemma dr_repeat:
  fixes φ :: "'a → 'b"
  assumes dr_ab: "drefines φ G a b"
      and Gpr:  "«G¬ ⊨!!! wp b «G¬"
      and wa:    "well_def a"
      and wb:    "well_def b"
  shows "drefines φ G (repeat n a) (repeat n b)" (is "?X n")
proof(induct n)
  show "?X 0" by(simp add:dr_Skip)

  fix n
  assume IH: "?X n"
  thus "?X (Suc n)" by(auto intro!:dr_Seq Gpr assms wd_intros)
qed

end