Theory Refinement

(*<*)
theory Refinement
imports
  Constructions
  Next_Imp
  Stability
begin

(*>*)
section‹ Refinement\label{sec:refinement} ›

text‹

We develop a refinement story for the \<^typ>‹('a, 's, 'v) spec› lattice.

References:
 ▪ \<^citet>‹"Vafeiadis:2008"› (RGsep, program logic) and \<^citet>‹"LiangFenFu:2014"› (RGsim, refinement)
 ▪ \<^citet>‹"ArmstrongGomesStruth:2014"›
 ▪ \<^citet>‹"vanStaden:2015"›

›

definition refinement :: "'s pred ⇒ ('a, 's, 'v) spec ⇒ ('a, 's, 'v) spec ⇒ ('v ⇒ 's pred) ⇒ ('a, 's, 'v) spec" (‹⦃_⦄, _ ⊩ _, ⦃_⦄› [0,0,0,0] 100) where
  "⦃P⦄, A ⊩ G, ⦃Q⦄ = spec.pre P ⊓ A ❙⟶⇩+ G ⊓ spec.post Q"

text‹

An intuitive gloss on the proposition ‹c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄› is: assuming the precondition ‹P› holds
and all steps conform to the process ‹A›, then ‹c› is a refinement of ‹G› and satisfies
the postcondition ‹Q›.

Observations:
 ▪ We use \<^const>‹next_imp› here;\<^const>‹heyting› is (only) enough for an assume/guarantee program logic (see \S\ref{sec:refinement-ag})
 ▪ ‹A› is arbitrary but is intended to constrain only \<^const>‹env› steps
  ▪ similarly termination can depend on ‹A›: a parallel composition can only terminate if all of its constituent processes terminate
 ▪ As ‹P ❙⟶⇩+ Q› implies ‹idle ≤ Q›, in practice ‹idle ≤ G›
 ▪ see \S\ref{sec:programs-refinement-intros} for some introduction rules

›

setup ‹Sign.mandatory_path "refinement"›

lemma E:
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
  obtains "c ≤ spec.pre P ⊓ A ❙⟶⇩+ G"
      and "c ≤ spec.pre P ⊓ A ❙⟶⇩+ spec.post Q"
using assms by (simp add: refinement_def spec.next_imp.infR)

lemma pre_post_cong:
  assumes "P = P'"
  assumes "Q = Q'"
  shows "⦃P⦄, A ⊩ G, ⦃Q⦄ = ⦃P'⦄, A ⊩ G, ⦃Q'⦄"
using assms by simp

lemma top:
  shows "⦃P⦄, A ⊩ ⊤, ⦃⊤⦄ = ⊤"
    and "⦃P⦄, A ⊩ ⊤, ⦃⟨⊤⟩⦄ = ⊤"
    and "⦃P⦄, A ⊩ ⊤, ⦃λ_ _. True⦄ = ⊤"
by (simp_all add: refinement_def)

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) G"
  shows "mcont luba orda Sup (≤) (λx. ⦃P⦄, A ⊩ G x, ⦃Q⦄)"
by (simp add: assms refinement_def)

lemma mono:
  assumes "P' ≤ P"
  assumes "A' ≤ A"
  assumes "G ≤ G'"
  assumes "Q ≤ Q'"
  shows "⦃P⦄, A ⊩ G, ⦃Q⦄ ≤ ⦃P'⦄, A' ⊩ G', ⦃Q'⦄"
unfolding refinement_def
apply (strengthen ord_to_strengthen(1)[OF assms(1)])
apply (strengthen ord_to_strengthen(1)[OF assms(2)])
apply (strengthen ord_to_strengthen(1)[OF assms(3)])
apply (strengthen ord_to_strengthen(1)[OF assms(4)])
apply simp
done

lemma strengthen[strg]:
  assumes "st_ord (¬ F) P P'"
  assumes "st_ord (¬ F) A A'"
  assumes "st_ord F G G'"
  assumes "st_ord F Q Q'"
  shows "st_ord F (⦃P⦄, A ⊩ G, ⦃Q⦄) (⦃P'⦄, A' ⊩ G', ⦃Q'⦄)"
using assms by (cases F; simp add: refinement.mono)

lemma mono_stronger:
  assumes "P' ≤ P"
  assumes "spec.pre P' ⊓ A' ≤ A"
  assumes "spec.pre P' ⊓ G ≤ A' ❙⟶⇩+ G'"
  assumes "Q ≤ Q'"
  assumes "spec.idle ≤ G'"
  shows "⦃P⦄, A ⊩ G, ⦃Q⦄ ≤ ⦃P'⦄, A' ⊩ G', ⦃Q'⦄"
unfolding refinement_def
apply (strengthen ord_to_strengthen(2)[OF assms(1)])
apply (strengthen ord_to_strengthen(2)[OF assms(2)])
apply (strengthen ord_to_strengthen(2)[OF assms(4)])
apply (simp add: spec.next_imp.infR)
apply (metis assms(3) heyting.commute le_infI1
             spec.next_imp.closure.cl spec.pre.next_imp_eq_heyting(2)[OF assms(5)])
done

lemmas pre_ag = order.trans[OF _ refinement.mono[OF order.refl _ _ order.refl], of c] for c
lemmas pre_a = refinement.pre_ag[OF _ _ order.refl]
lemmas pre_g = refinement.pre_ag[OF _ order.refl]

lemma pre:
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
  assumes "⋀s. P' s ⟹ P s"
  assumes "A' ≤ A"
  assumes "G ≤ G'"
  assumes "⋀s v. Q s v ⟹ Q' s v"
  shows "c ≤ ⦃P'⦄, A' ⊩ G', ⦃Q'⦄"
using assms(2-) by (blast intro: order.trans[OF assms(1) refinement.mono])

lemmas pre_pre_post = refinement.pre[OF _ _ order.refl order.refl, of c] for c

lemma pre_imp:
  assumes "⋀s. P s ⟹ P' s"
  assumes "c ≤ ⦃P'⦄, A ⊩ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
using assms refinement.pre by blast

lemmas pre_pre = refinement.pre_imp[rotated]

lemma post_imp:
  assumes "⋀v s. Q v s ⟹ R v s"
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊩ G, ⦃R⦄"
using assms refinement.pre by blast

lemmas pre_post = refinement.post_imp[rotated]
lemmas strengthen_post = refinement.pre_post

lemma pre_inf_assume:
  shows "⦃P⦄, A ⊩ G, ⦃Q⦄ = ⦃P⦄, A ⊓ spec.pre P ⊩ G, ⦃Q⦄"
by (simp add: refinement_def ac_simps)

lemma pre_assume_absorb:
  assumes "A ≤ spec.pre P"
  shows "⦃P⦄, A ⊩ G, ⦃Q⦄ = ⦃⊤⦄, A ⊩ G, ⦃Q⦄"
by (simp add: assms refinement_def inf_absorb2)

lemmas sup = sup_least[where x="⦃P⦄, A ⊩ G, ⦃Q⦄"] for A G P Q

lemma
  shows supRL: "c ≤ ⦃P⦄, A ⊩ G⇩1, ⦃Q⦄ ⟹ c ≤ ⦃P⦄, A ⊩ G⇩1 ⊔ G⇩2, ⦃Q⦄"
    and supRR: "c ≤ ⦃P⦄, A ⊩ G⇩2, ⦃Q⦄ ⟹ c ≤ ⦃P⦄, A ⊩ G⇩1 ⊔ G⇩2, ⦃Q⦄"
by (simp_all add: refinement.pre_g)

lemma infR_conv:
  shows "⦃P⦄, A ⊩ G⇩1 ⊓ G⇩2, ⦃Q⇩1 ⊓ Q⇩2⦄ = ⦃P⦄, A ⊩ G⇩1, ⦃Q⇩1⦄ ⊓ ⦃P⦄, A ⊩ G⇩2, ⦃Q⇩2⦄"
by (simp add: refinement_def ac_simps spec.next_imp.infR spec.post.inf)

lemma inf_le:
  shows "X ⊓ ⦃P⦄, A ⊩ G, ⦃Q⦄ ≤ ⦃P⦄, X ⊓ A ⊩ X ⊓ G, ⦃Q⦄"
by (simp add: refinement_def le_infI1 le_infI2
              spec.next_imp.infR spec.next_imp.mono spec.next_imp.contains)

lemma heyting_le:
  shows "⦃P⦄, A ⊓ B ⊩ B ❙⟶⇩H G, ⦃Q⦄ ≤ B ❙⟶⇩H ⦃P⦄, A ⊩ G, ⦃Q⦄"
by (simp add: refinement_def ac_simps heyting.infR heyting.commute
              spec.next_imp.heytingL_distrib spec.next_imp.mono)

lemma heyting_pre:
  assumes "spec.idle ≤ G"
  shows "spec.pre P ❙⟶⇩H ⦃P'⦄, A ⊩ G, ⦃Q⦄ = ⦃P ❙∧ P'⦄, A ⊩ G, ⦃Q⦄"
by (simp add: ac_simps refinement_def spec.pre.conj assms spec.idle.post_le
        flip: spec.pre.next_imp_eq_heyting)

lemma sort_of_refl:
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊩ c, ⦃Q⦄"
using assms by (simp add: refinement_def spec.next_imp.infR spec.next_imp.closure.expansive)

lemma gen_asm_base:
  assumes "P ⟹ c ≤ ⦃P' ❙∧ P''⦄, A ⊩ G, ⦃Q⦄"
  assumes "spec.idle ≤ G"
  shows "c ≤ ⦃P' ❙∧ ⟨P⟩ ❙∧ P''⦄, A ⊩ G, ⦃Q⦄"
using assms by (simp add: refinement_def spec.pre.conj spec.pre.K spec.next_imp.botL spec.idle.post_le)

lemmas gen_asm =
  refinement.gen_asm_base[where P'="⟨True⟩" and P''="⟨True⟩", simplified]
  refinement.gen_asm_base[where P'="⟨True⟩", simplified]
  refinement.gen_asm_base[where P''="⟨True⟩", simplified]
  refinement.gen_asm_base

lemma post_conj:
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q'⦄"
  shows "c ≤ ⦃P⦄, A ⊩ G, ⦃λrv. Q rv ❙∧ Q' rv⦄"
using assms unfolding refinement_def by (simp add: spec.post.conj spec.next_imp.infR)

lemma conj_lift:
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
  assumes "c ≤ ⦃P'⦄, A ⊩ G, ⦃Q'⦄"
  shows "c ≤ ⦃P ❙∧ P'⦄, A ⊩ G, ⦃λrv. Q rv ❙∧ Q' rv⦄"
using assms by (blast intro: refinement.post_conj refinement.pre)

lemma drop_imp:
  assumes "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊩ G, ⦃λrv. Q' rv ❙⟶ Q rv⦄"
using assms refinement.strengthen_post by fastforce

lemma "prop":
  shows "c ≤ ⦃⟨P⟩⦄, A ⊩ c, ⦃λv. ⟨P⟩⦄"
by (simp add: refinement.sort_of_refl[where G=⊤] refinement.gen_asm refinement.top)

lemma name_pre_state:
  assumes "⋀s. P s ⟹ c ≤ ⦃(=) s⦄, A ⊩ G, ⦃Q⦄"
  assumes "spec.idle ≤ G"
  shows "c ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄" (is "?lhs ≤ ?rhs")
proof -
  have "⦉σ⦊ ≤ G ∧ ⦉σ⦊ ≤ spec.post Q"
    if "⦉σ⦊ ≤ c"
   and "∀σ''<σ. ⦉σ''⦊ ≤ spec.pre P ∧ ⦉σ''⦊ ≤ A"
   for σ
  proof(cases "trace.rest σ = [] ∧ trace.term σ = None")
    case True with ‹spec.idle ≤ G› show ?thesis
      by (cases σ) (simp add: spec.singleton.le_conv order.trans[OF spec.idle.minimal_le])
  next
    case False with order.trans[OF ‹⦉σ⦊ ≤ c› assms(1)[where s="trace.init σ"]] that(2)
    show ?thesis
      by (cases σ)
         (clarsimp simp: refinement_def spec.singleton.next_imp_le_conv spec.singleton.le_conv;
          fastforce simp: trace.less dest: spec[where x="trace.T (trace.init σ) [] None"])
  qed
  then show ?thesis
    by - (rule spec.singleton_le_extI;
          auto simp: refinement_def spec.singleton.next_imp_le_conv
              intro: order.trans[OF spec.singleton.mono])
qed

setup ‹Sign.parent_path›


subsection‹ Geenral rules for the ∗‹('a, 's, 'v) spec› lattice\label{sec:refinement-spec} ›

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "all"›

lemma refinement:
  shows "spec.term.all (⦃P⦄, A ⊩ G, ⦃Q⦄) = ⦃P⦄, spec.term.all A ⊩ spec.term.all G, ⦃⊤⦄"
by (simp add: refinement_def spec.term.all.next_imp spec.term.all.inf spec.term.all.pre spec.term.all.post)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "none"›

lemma refinement_le:
  shows "spec.term.none (⦃P⦄, A ⊩ G, ⦃Q⦄) ≤ ⦃P⦄, spec.term.all A ⊩ spec.term.all G, ⦃⊥⦄"
by (simp add: spec.term.galois spec.term.all.refinement order.trans[OF spec.term.all.expansive])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap"›

lemma refinement:
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  fixes A :: "('b, 't, 'w) spec"
  fixes G :: "('b, 't, 'w) spec"
  fixes P :: "'t pred"
  fixes Q :: "'w ⇒ 't pred"
  shows "spec.invmap af sf vf (⦃P⦄, A ⊩ G, ⦃Q⦄)
      = (⦃λs. P (sf s)⦄, spec.invmap af sf vf A ⊩ spec.invmap af sf vf G, ⦃λv s. Q (vf v) (sf s)⦄)"
unfolding refinement_def
by (simp only: spec.next_imp.invmap spec.invmap.inf spec.invmap.pre spec.invmap.post)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsubsection‹ Actions\label{sec:refinement-action} ›

text‹

Actions are anchored at the start of a trace, and therefore must be an initial step of the
assume ‹A›. However by the semantics of \<^const>‹spec.next_imp› we may only know
that that initial state of the trace is acceptable to ‹A›
when showing that ‹F›-steps are ‹F'›-steps
(the second assumption). This hypothesis is vacuous when ‹idle ≤ A›.

›

setup ‹Sign.mandatory_path "refinement.spec"›

lemma action:
  fixes F :: "('v × 'a × 's × 's) set"
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F; (a, s, s') ∈ spec.initial_steps A⟧ ⟹ Q v s'"
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F; (a, s, s) ∈ spec.initial_steps A⟧ ⟹ (v, a, s, s') ∈ F'"
  shows "spec.action F ≤ ⦃P⦄, A ⊩ spec.action F', ⦃Q⦄"
proof -
  have "spec.action (F ∩ UNIV × UNIV × Pre P) ≤ A ❙⟶⇩+ spec.action F' ⊓ spec.post Q"
  proof(induct rule: spec.action_le)
    case idle show ?case
      by (simp add: spec.next_imp.contains spec.idle.action_le spec.idle.post_le)
  next
    case (step v a s s') then show ?case
      by (fastforce simp: spec.singleton.next_imp_le_conv trace.split_all spec.initial_steps_def
                          trace.less Cons_eq_append_conv spec.singleton.post_le_conv
                          order.trans[OF spec.idle.minimal_le spec.idle.action_le]
                    elim: assms trace.less_eqE prefixE
                   intro: spec.action.stepI)
  qed
  then show ?thesis
    by (simp add: refinement_def spec.pre.next_imp_eq_heyting spec.idle.post_le spec.idle.action_le
                  heyting order.trans[OF spec.pre.inf_action_le(2)])
qed

lemma return:
  shows "spec.return v ≤ ⦃Q v⦄, A ⊩ spec.return v, ⦃Q⦄"
by (auto simp: spec.return_def intro: refinement.spec.action)

lemma action_rel:
  fixes F :: "('v × 'a × 's × 's) set"
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F; (a, s, s') ∈ spec.initial_steps A⟧ ⟹ Q v s'"
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F; (a, s, s) ∈ spec.initial_steps A; s ≠ s'⟧ ⟹ (a, s, s') ∈ r"
  shows "spec.action F ≤ ⦃P⦄, A ⊩ spec.rel r, ⦃Q⦄"
by (force simp: spec.rel_def spec.rel.act_def spec.term.all.action
         intro: assms refinement.supRL refinement.spec.action
                refinement.pre_g[OF _ spec.term.all.mono[OF spec.kleene.expansive_star]])

setup ‹Sign.parent_path›


subsubsection‹ Bind\label{sec:refinement-bind} ›

text‹

Consider showing ‹f ⤜ g ≤ f' ⤜ g'› under the assume ‹A› and pre/post conditions ‹P›/‹Q›.

The tricky part is to residuate the assume ‹A› wrt the process ‹f› for use in the refinement proof of ‹g›.
 ▪ we want to preserve as much of the structure of ‹A› as possible
 ▪ intuition: we want all the ways a trace can continue in ‹A› having started with a terminating trace in ‹f›
 ▪ intuitively a right residual for \<^const>‹spec.bind› should do the job
  ▪ however unlike \<^citet>‹"HoareHe:1987"› we have no chance of a right residual for \<^const>‹spec.bind› as we use traces (they use relations)
   ▪ i.e., if it is not the case that ‹f ⤜ ⊥ ≤ A› then there is no continuation ‹h› such that ‹f ⤜ h ≤ A›.
   ▪ also such a residual ‹h› has arbitrary behavior starting from states that ‹f› cannot reach
    ▪ i.e., for traces ‹¬σ ≤ f› ‹⦉σ⦊ ⪢ h ≤ A› need not hold
    ▪ and the user-provided assertions may be too weak to correct for this
 ▪ in practice the termination information in the assume ‹A› is not useful

We therefore define an ad hoc residual that does the trick.

See \<^citet>‹‹\S4› in "Emerson:1983"› for some related concerns.

›

setup ‹Sign.mandatory_path "refinement.spec.bind"›

definition res :: "('a, 's, 'v) spec ⇒ ('a, 's, 'w) spec ⇒ 'v ⇒ ('a, 's, 'w) spec" where
  "res f A v = ⨆{⦉trace.final' s xs, ys, w⦊ |s xs ys w. ⦉s, xs, Some v⦊ ≤ f ∧ ⦉s, xs @ ys, None⦊ ≤ A}"

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.singleton.refinement.bind"›

lemma res_le_conv[spec.singleton.le_conv]:
  shows "⦉σ⦊ ≤ refinement.spec.bind.res f A v
    ⟷ (∃s xs. ⦉s, xs, Some v⦊ ≤ f
              ∧ trace.init σ = trace.final' s xs
              ∧ ⦉s, xs @ trace.rest σ, None⦊ ≤ A)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
    by (fastforce simp: refinement.spec.bind.res_def trace.split_Ex spec.singleton_le_conv
                        trace.less_eq_None trace.natural'.append trace.natural_def
                  elim: trace.less_eqE order.trans[rotated])
  show "?rhs ⟹ ?lhs"
    by (cases σ) (clarsimp simp: refinement.spec.bind.res_def; blast)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.term.none.refinement.bind"›

lemma resL:
  shows "refinement.spec.bind.res (spec.term.none f) A v = ⊥"
by (simp add: refinement.spec.bind.res_def spec.singleton.le_conv)

lemma resR:
  shows "refinement.spec.bind.res f (spec.term.none A) v = refinement.spec.bind.res f A v"
by (simp add: refinement.spec.bind.res_def spec.singleton.le_conv)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.term.all.refinement.bind"›

lemma resR_mono:
  shows "refinement.spec.bind.res f (spec.term.all A) v = refinement.spec.bind.res f A v"
by (simp add: refinement.spec.bind.res_def spec.singleton.le_conv)
   (meson dual_order.trans spec.singleton.less_eq_None)

lemma res:
  shows "spec.term.all (refinement.spec.bind.res f A v) = refinement.spec.bind.res f A v"
by (rule spec.singleton.antisym) (auto simp: spec.singleton.le_conv)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.term.closed.refinement.bind"›

lemma res:
  shows "refinement.spec.bind.res f A v ∈ spec.term.closed _"
by (subst spec.term.all.refinement.bind.res[symmetric]) (rule spec.term.all.closed)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "refinement.spec.bind.res"›

lemma bot:
  shows botL: "refinement.spec.bind.res ⊥ = ⊥"
    and botR: "refinement.spec.bind.res f ⊥ = ⊥"
by (simp_all add: refinement.spec.bind.res_def fun_eq_iff spec.singleton.not_bot)

lemma mono:
  assumes "f ≤ f'"
  assumes "A ≤ A'"
  shows "refinement.spec.bind.res f A v ≤ refinement.spec.bind.res f' A' v"
using assms unfolding refinement.spec.bind.res_def by (fastforce intro!: Sup_subset_mono)

lemma strengthen[strg]:
  assumes "st_ord F f f'"
  assumes "st_ord F A A'"
  shows "st_ord F (refinement.spec.bind.res f A v) (refinement.spec.bind.res f' A' v)"
using assms by (cases F; simp add: refinement.spec.bind.res.mono)

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≤) f"
  assumes "monotone orda (≤) A"
  shows "monotone orda (≤) (λx. refinement.spec.bind.res (f x) (A x) v)"
using assms by (simp add: monotone_def refinement.spec.bind.res.mono)

lemma SupL:
  shows "refinement.spec.bind.res (⨆X) A v = (⨆x∈X. refinement.spec.bind.res x A v)"
by (rule antisym; simp add: refinement.spec.bind.res_def; blast)

lemma SupR:
  shows "refinement.spec.bind.res f (⨆X) v = (⨆x∈X. refinement.spec.bind.res f x v)"
by (rule antisym; simp add: refinement.spec.bind.res_def; blast)

lemma InfL_le:
  shows "refinement.spec.bind.res (⨅X) A v ≤ (⨅x∈X. refinement.spec.bind.res x A v)"
by (simp add: refinement.spec.bind.res_def le_Inf_iff) fast

lemma InfR_le:
  shows "refinement.spec.bind.res f (⨅X) v ≤ (⨅x∈X. refinement.spec.bind.res f x v)"
by (simp add: refinement.spec.bind.res_def le_Inf_iff) fast

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) f"
  assumes "mcont luba orda Sup (≤) A"
  shows "mcont luba orda Sup (≤) (λx. refinement.spec.bind.res (f x) (A x) v)"
proof(rule ccpo.mcont2mcont'[OF complete_lattice_ccpo _ _ assms(1)])
  show "mcont Sup (≤) Sup (≤) (λf. refinement.spec.bind.res f (A x) v)" for x
    by (intro mcontI contI monotoneI)
       (simp_all add: refinement.spec.bind.res.mono refinement.spec.bind.res.SupL)
  show "mcont luba orda Sup (≤) (λx. refinement.spec.bind.res f (A x) v)" for f
    by (intro mcontI monotoneI contI)
       (simp_all add: mcont_monoD[OF assms(2)] refinement.spec.bind.res.mono contD[OF mcont_cont[OF assms(2)]]
                      refinement.spec.bind.res.SupR image_image)
qed

lemma returnL:
  assumes "spec.idle ≤ A"
  shows "refinement.spec.bind.res (spec.return v) A v = spec.term.all A" (is "?lhs = ?rhs")
proof(rule antisym[OF _ spec.singleton_le_extI])
  show "?lhs ≤ ?rhs"
    by (auto simp: refinement.spec.bind.res_def trace.split_all spec.singleton.le_conv)
  show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
    using that
    by (auto simp: spec.singleton.le_conv
           intro!: exI[where x="trace.init σ"] exI[where x="[]"]
             elim: order.trans[rotated])
qed

lemma rel_le:
  assumes "r ⊆ r'"
  shows "refinement.spec.bind.res f (spec.rel r) v ≤ spec.rel r'"
using assms by (force intro: spec.singleton_le_extI simp: spec.singleton.le_conv trace.steps'.append)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.steps.refinement.spec.bind"›

lemma res_le: ―‹ we can always discard the extra structure ›
  shows "spec.steps (refinement.spec.bind.res f A v) ⊆ spec.steps A"
by (meson order_trans refinement.spec.bind.res.mono refinement.spec.bind.res.rel_le
          spec.rel.galois spec.rel.upper_lower_expansive)

setup ‹Sign.parent_path›


text‹

A refinement rule for \<^const>‹spec.bind›.
The function ‹vf› abstracts interstitial monadic return values.

›

setup ‹Sign.mandatory_path "refinement.spec"›

lemma bind_abstract:
  fixes f :: "('a, 's, 'v) spec"
  fixes f' :: "('a, 's, 'v') spec"
  fixes g :: "'v ⇒ ('a, 's, 'w) spec"
  fixes g' :: "'v' ⇒ ('a, 's, 'w) spec"
  fixes vf :: "'v ⇒ 'v'"
  assumes g: "⋀v. g v ≤ ⦃Q' (vf v)⦄, refinement.spec.bind.res (spec.pre P ⊓ spec.term.all A ⊓ f') A (vf v) ⊩ g' (vf v), ⦃Q⦄"
  assumes f: "f ≤ ⦃P⦄, spec.term.all A ⊩ spec.vinvmap vf f', ⦃λv. Q' (vf v)⦄"
  shows "f ⤜ g ≤ ⦃P⦄, A ⊩ f' ⤜ g', ⦃Q⦄"
proof (rule order.trans[OF spec.bind.mono[OF f g]],
       unfold refinement_def spec.bind.inf_post,
       induct rule: spec.bind_le)
  case incomplete show ?case
    apply (simp add: spec.term.galois spec.term.all.next_imp spec.term.all.bind spec.term.all.inf
                     spec.term.all.post spec.term.all.pre)
    apply (simp add: spec.next_imp.mono[OF order.refl] le_supI1 le_infI1 spec.term.none.invmap
                     spec.invmap.id
               flip: spec.term.galois)
    done
next
  case (continue σ⇩f σ⇩g v)
  have "⦉s, xs, w⦊ ≤ f' ⤜ (λv. g' v ⊓ spec.post Q)"
    if le: "trace.T s xs w ≤ trace.T (trace.init σ⇩f) (trace.rest σ⇩f @ trace.rest σ⇩g) (trace.term σ⇩g)"
   and pre: "∀σ''<trace.T s xs w. ⦉σ''⦊ ≤ spec.pre P ⊓ A"
   for s xs w
    using le
  proof(induct rule: trace.less_eq_extE)
    case prefix
    from prefix(3) show ?case
    proof(induct rule: prefix_append_not_NilE[case_names incomplete1 continue1])
      case incomplete1 with pre continue(1) prefix(1,2) show ?case
        apply (clarsimp simp: spec.singleton.next_imp_le_conv)
        apply (drule spec[where x="trace.T s xs None"],
               drule mp[where P="trace.T s xs None ≤ σ⇩f"])
         apply (force simp: spec.singleton.le_conv spec.map.singleton
                            le_inf_iff trace.less trace.split_All trace.less_eq_None
                 simp flip: spec.map_invmap.galois
                    intro!: spec.bind.incompleteI)+
        done
    next
      case (continue1 us)
      from continue(1,3) prefix(2) continue1(1,2)
           spec[OF pre, where x="trace.T (trace.init σ⇩f) (trace.rest σ⇩f) None"]
      have "⦉trace.init σ⇩f, trace.rest σ⇩f, Some (vf v)⦊ ≤ spec.pre P ⊓ spec.term.all A ⊓ f' ⊓ spec.post Q'"
        apply (cases σ⇩f)
        apply (clarsimp simp: spec.singleton.le_conv spec.singleton.next_imp_le_conv
                              trace.less le_inf_iff exI[where x=None]
                       split: option.split_asm
                       dest!: spec[where x=σ⇩f])
        apply (metis append_is_Nil_conv le_inf_iff pre trace.less_same_append_conv)
        done
      with pre continue(1,2,5) prefix(1,2) continue1
           spec[OF continue(4)[unfolded spec.singleton.next_imp_le_conv],
                where x="trace.T (trace.init σ⇩g) us None"]
      show ?case
        apply clarsimp
        apply (rule spec.bind.continueI[where v="vf v"], assumption)
        apply (clarsimp simp: spec.singleton.le_conv trace.split_All trace.less_eq_None trace.less)
        apply (metis append.assoc)
        done
    qed
  next
    case (maximal w')
    from maximal(1-3) continue(1,3)
         spec[OF pre, where x="trace.T (trace.init σ⇩f) (trace.rest σ⇩f) None"]
    have "⦉trace.init σ⇩f, trace.rest σ⇩f, Some (vf v)⦊ ≤ spec.pre P ⊓ spec.term.all A ⊓ f' ⊓ spec.post Q'"
      apply (cases σ⇩f)
      apply (clarsimp simp: spec.singleton.le_conv spec.singleton.next_imp_le_conv le_inf_iff
                     split: option.split_asm)
      apply (force simp: trace.less spec.singleton.mono trace.less_eq_same_append_conv
                   elim: notE order.trans[rotated]
                  dest!: spec[where x=σ⇩f] spec[where x=None])
      done
  with maximal(2-4) pre continue(2)
       spec[OF continue(4)[unfolded spec.singleton.next_imp_le_conv], where x="σ⇩g"]
  show ?case
    by (cases σ⇩g)
       (auto 0 2 intro!: spec.bind.continueI[where v="vf v"] exI[where x=s]
                  simp: spec.singleton.le_conv trace.split_All trace.less)
  qed
  then show ?case
    by (clarsimp simp: spec.singleton.next_imp_le_conv trace.split_all)
qed

lemmas bind = refinement.spec.bind_abstract[where vf=id, simplified spec.invmap.id, simplified]


subsubsection‹ Interference\label{sec:refinement-interference} ›

lemma rel_mono:
  assumes "r ⊆ r'"
  assumes "stable (snd ` (spec.steps A ∩ r)) P"
  shows "spec.rel r ≤ ⦃P⦄, A ⊩ spec.rel r', ⦃λ_::unit. P⦄"
apply (subst (1) spec.rel.monomorphic_conv)
using assms(2)
proof(induct arbitrary: A rule: spec.kleene.star.fixp_induct[case_names adm bot step])
  case (step R A)
  have *: "spec.rel.act r ≤ ⦃P⦄, spec.term.all A ⊩ spec.rel r', ⦃⟨P⟩⦄"
    unfolding spec.rel.act_def
  proof(rule refinement.spec.action_rel)
    show "P s'"
      if "P s"
     and "(v, a, s, s') ∈ {()} × (r ∪ UNIV × Id)"
     and "(a, s, s') ∈ spec.initial_steps (spec.term.all A)"
     for v a s s'
      using that monotoneD[OF stable.antimono_rel, unfolded le_bool_def, rule_format, OF _ step.prems,
                           where x="{(s, s')}"]
      by (cases "s = s'";
          force simp: spec.initial_steps.term.all stable.singleton_conv
                dest: subsetD[OF spec.initial_steps.steps_le])
    show "(a, s, s') ∈ r'" if "(v, a, s, s') ∈ {()} × (r ∪ UNIV × Id)" and "s ≠ s'" for v a s s'
      using that assms(1) by fast
  qed
  show ?case
    apply (rule refinement.sup[OF _ refinement.pre_g[OF refinement.spec.return spec.return.rel_le]])
    apply (subst spec.rel.unwind_bind)
    apply (rule refinement.spec.bind[OF step.hyps *])
    apply (force intro: monotoneD[OF stable.antimono_rel, unfolded le_bool_def, rule_format, OF _ step.prems]
                  dest: subsetD[OF spec.steps.refinement.spec.bind.res_le])
    done
qed simp_all

setup ‹Sign.parent_path›


subsubsection‹ Parallel\label{sec:refinement-parallel} ›

text‹

Our refinement rule for \<^const>‹spec.Parallel› does not constrain the constituent processes in
any way, unlike Abadi and Plotkin's proposed rule (see \S\ref{sec:abadi_plotkin}).

›

setup ‹Sign.mandatory_path "refinement.spec"›

definition ―‹ roughly the \<^const>‹spec.Parallel› construction with roles reversed ›
  env_hyp :: "('a ⇒ 's pred) ⇒ (sequential, 's, unit) spec ⇒ 'a set ⇒  ('a ⇒ (sequential, 's, unit) spec) ⇒ 'a ⇒ (sequential, 's, unit) spec"
where
  "env_hyp P A as Ps a =
    spec.pre (⨅ (P ` as))
      ⊓ spec.amap (toConcurrent_fn (proc a))
          (spec.rel (({env} ∪ proc ` as) × UNIV)
            ⊓ (⨅i∈as. spec.toConcurrent i (Ps i))
            ⊓ spec.ainvmap toSequential_fn A)"

setup ‹Sign.mandatory_path "env_hyp"›

lemma mono:
  assumes "⋀a. a ∈ as ⟹ P a ≤ P' a"
  assumes "A ≤ A'"
  assumes "⋀a. a ∈ as ⟹ Ps a ≤ Ps' a"
  shows "refinement.spec.env_hyp P A as Ps a ≤ refinement.spec.env_hyp P' A' as Ps' a"
unfolding refinement.spec.env_hyp_def
apply (strengthen ord_to_strengthen(2)[OF assms(1)], assumption)
apply (strengthen ord_to_strengthen(1)[OF assms(2)])
apply (strengthen ord_to_strengthen(1)[OF assms(3)], assumption)
apply simp
done

lemma strengthen[strg]:
  assumes "⋀a. a ∈ as ⟹ st_ord F (P a) (P' a)"
  assumes "st_ord F A A'"
  assumes "⋀a. a ∈ as ⟹ st_ord F (Ps a) (Ps' a)"
  shows "st_ord F (refinement.spec.env_hyp P A as Ps a) (refinement.spec.env_hyp P' A' as Ps' a)"
using assms by (cases F; simp add: refinement.spec.env_hyp.mono)

setup ‹Sign.parent_path›

lemma Parallel:
  fixes A :: "(sequential, 's, unit) spec"
  fixes Q :: "'a ⇒ 's ⇒ bool"
  fixes Ps :: "'a ⇒ (sequential, 's, unit) spec"
  fixes Ps' :: "'a ⇒ (sequential, 's, unit) spec"
  assumes "⋀a. a ∈ as ⟹ Ps a ≤ ⦃P a⦄, refinement.spec.env_hyp P A as Ps' a ⊩ Ps' a, ⦃λv. Q a⦄"
  shows "spec.Parallel as Ps ≤ ⦃⨅a∈as. P a⦄, A ⊩ spec.Parallel as Ps', ⦃λv. ⨅a∈as. Q a⦄"
proof(cases "as = {}")
  case True then show ?thesis
    by (simp add: spec.Parallel.no_agents refinement.sort_of_refl[where G=⊤] refinement.top)
next
  case False then show ?thesis
    unfolding refinement_def
    apply (subst (1) spec.Parallel_def)
    apply (simp only: spec.map_invmap.galois spec.invmap.inf
                      spec.next_imp.invmap spec.invmap.post spec.invmap.pre)
    apply (subst (1) spec.Parallel_def)
    apply (strengthen ord_to_strengthen(2)[OF spec.map_invmap.upper_lower_expansive])
    apply (subst inf.assoc)
    apply (subst spec.next_imp.infR)
    apply (simp only: spec.next_imp.contains inf.bounded_iff inf_le1)
    apply (strengthen ord_to_strengthen[OF assms], assumption)
    apply (simp only: spec.invmap.refinement id_apply simp_thms)
    apply (rule order.trans[rotated, OF spec.Abadi_Merz_Theorem4[where
               I=as
           and As="λa. spec.pre (P a) ⊓ spec.toConcurrent a (refinement.spec.env_hyp P A as Ps' a)"
           and Cs="λa. spec.toConcurrent a (Ps' a) ⊓ spec.post ⟨Q a⟩"]])
    apply (simp only: inf.bounded_iff)
    apply (intro conjI)
      ―‹ the meat of \<^const>‹refinement.spec.env_hyp› ›
      apply (simp only: heyting)
      apply (rule INFI)
      apply (simp only: inf.bounded_iff
                  flip: INF_inf_distrib)
      apply (intro conjI)
       apply (force simp: ac_simps spec.pre.INF
                   intro: le_infI1 le_infI2)
      apply (simp add: refinement.spec.env_hyp_def ac_simps
                 flip: spec.map_invmap.galois)
      apply (rule conjI)
       apply (simp add: spec.map_invmap.galois spec.invmap.pre le_infI2
                   del: Inf_apply INF_apply; fail)
      apply (simp add: spec.map.mono le_infI2; fail)
     apply (simp add: spec.next_imp.contains heyting spec.post.INF flip: INF_inf_distrib; fail)
    apply (force simp: refinement_def)
    done
qed

setup ‹Sign.parent_path›


subsection‹ A relational assume/guarantee program logic for the ∗‹(sequential, 's, 'v) spec› lattice\label{sec:refinement-ag} ›

text‹

Here we develop an assume/guarantee story based on abstracting processes
(represented as safety properties) to binary relations.

Observations:
 ▪ this can be seen as a reconstruction of the algebraic account given by \<^citet>‹"vanStaden:2015"› in our setting
 ▪ we show Heyting implication suffices for relations (see ‹ag.refinement›)
   ▪ the processes' agent type is required to be \<^typ>‹sequential›
 ▪ we use predicates and not relations for pre/post assertions
   ▪ we can use the metalanguage to do some relational reasoning; see, for example, ‹ag.name_pre_state›
 ▪ \<^const>‹Id› is the smallest significant assume and guarantee relation here; processes can always stutter any state

›

setup ‹Sign.mandatory_path "ag"›

abbreviation (input) assm :: "'s rel ⇒ (sequential, 's, 'v) spec" where
  "assm A ≡ spec.rel ({env} × A ∪ {self} × UNIV)"

abbreviation (input) guar :: "'s rel ⇒ (sequential, 's, 'v) spec" where
  "guar G ≡ spec.rel ({env} × UNIV ∪ {self} × G)"

setup ‹Sign.parent_path›

definition ag :: "'s pred ⇒ 's rel ⇒ 's rel ⇒ ('v ⇒ 's pred) ⇒ (sequential, 's, 'v) spec" (‹⦃_⦄, _/ ⊢ _, ⦃_⦄› [0,0,0,0] 100) where
  "⦃P⦄, A ⊢ G, ⦃Q⦄ = spec.pre P ⊓ ag.assm A ❙⟶⇩H ag.guar G ⊓ spec.post Q"

setup ‹Sign.mandatory_path "spec.invmap"›

lemma ag: ―‹ Note ‹af = id› ›
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  fixes A :: "'t rel"
  fixes G :: "'t rel"
  fixes P :: "'t pred"
  fixes Q :: "'w ⇒ 't pred"
  shows "spec.invmap id sf vf (⦃P⦄, A ⊢ G, ⦃Q⦄) = ⦃λs. P (sf s)⦄, inv_image (A⇧=) sf ⊢ inv_image (G⇧=) sf, ⦃λv s. Q (vf v) (sf s)⦄"
proof -
  have "{self} × UNIV ∪ ({env} × inv_image A sf ∪ UNIV × inv_image Id sf) = {self} × UNIV ∪ {env} × inv_image (A⇧=) sf"
   and "{env} × UNIV ∪ ({self} × inv_image G sf ∪ UNIV × inv_image Id sf) = {env} × UNIV ∪ {self} × inv_image (G⇧=) sf"
    by auto
  then show ?thesis
    by (simp add: ag_def spec.invmap.heyting spec.invmap.inf spec.invmap.rel spec.invmap.pre spec.invmap.post
                  ac_simps map_prod_vimage_Times Sigma_Un_distrib2
            flip:  inv_image_alt_def)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag"›

lemma refinement:
  shows "⦃P⦄, A ⊢ G, ⦃Q⦄ = ⦃P⦄, ag.assm A ⊩ ag.guar G, ⦃Q⦄"
proof -
  have constrains_heyting_ag: "ag.assm A ❙⟶⇩+ ag.guar G = ag.assm A ❙⟶⇩H ag.guar G"
    apply (rule antisym[OF spec.next_imp.heyting_le])
    apply (simp add: spec.next_imp.heyting heyting)
    apply (subst inf.commute)
    apply (rule spec.composition_principle_half[where a⇩1="{self}" and a⇩2="{env}"];
           force simp: spec.idle_le spec.term.closed.rel)
    done
  have constrains_heyting_post: "P ❙⟶⇩+ spec.post Q = P ❙⟶⇩H spec.post Q"
    if "P ∈ spec.term.closed _"
   for P :: "(sequential, _, _) spec"
    apply (rule antisym[OF spec.next_imp.heyting_le])
    apply (clarsimp simp: spec.next_imp.heyting)
    apply (metis spec.term.all.closed_conv[OF that] heyting.topL order_refl spec.term.all.post
                 spec.term.all_none spec.term.heyting_noneL_allR_mono spec.term.lower_upper_lower(2))
    done
  show ?thesis
    by (simp add: ag_def refinement_def
                  spec.pre.next_imp_eq_heyting spec.idle_le
                  constrains_heyting_ag spec.next_imp.infR spec.term.closed.rel
                  constrains_heyting_post[OF spec.term.closed.rel] heyting.infR heyting.curry_conv)
qed

lemma E:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  obtains "c ≤ spec.pre P ⊓ ag.assm A ❙⟶⇩H ag.guar G"
      and "c ≤ spec.pre P ⊓ ag.assm A ❙⟶⇩H spec.post Q"
using assms by (simp add: ag_def heyting.infR)

lemma pre_post_cong:
  assumes "P = P'"
  assumes "Q = Q'"
  shows "⦃P⦄, A ⊢ G, ⦃Q⦄ = ⦃P'⦄, A ⊢ G, ⦃Q'⦄"
using assms by simp

lemma pre_bot:
  shows "⦃⊥⦄, A ⊢ G, ⦃Q⦄ = ⊤"
    and "⦃⟨⊥⟩⦄, A ⊢ G, ⦃Q⦄ = ⊤"
    and "⦃⟨False⟩⦄, A ⊢ G, ⦃Q⦄ = ⊤"
by (simp_all add: ag_def heyting.botL)

lemma post_top:
  shows "⦃P⦄, A ⊢ UNIV, ⦃⊤⦄ = ⊤"
    and "⦃P⦄, A ⊢ UNIV, ⦃⟨⊤⟩⦄ = ⊤"
    and "⦃P⦄, A ⊢ UNIV, ⦃λ_ _. True⦄ = ⊤"
by (simp_all add: ag_def spec.rel.upper_top flip: Sigma_Un_distrib1)

lemma mono:
  assumes "P' ≤ P"
  assumes "A' ≤ A"
  assumes "G ≤ G'"
  assumes "Q ≤ Q'"
  shows "⦃P⦄, A ⊢ G, ⦃Q⦄ ≤ ⦃P'⦄, A' ⊢ G', ⦃Q'⦄"
unfolding ag_def
apply (strengthen ord_to_strengthen(1)[OF assms(1)])
apply (strengthen ord_to_strengthen(1)[OF assms(2)])
apply (strengthen ord_to_strengthen(1)[OF assms(3)])
apply (strengthen ord_to_strengthen(1)[OF assms(4)])
apply simp
done

lemma strengthen[strg]:
  assumes "st_ord (¬ F) P P'"
  assumes "st_ord (¬ F) A A'"
  assumes "st_ord F G G'"
  assumes "st_ord F Q Q'"
  shows "st_ord F (⦃P⦄, A ⊢ G, ⦃Q⦄) (⦃P'⦄, A' ⊢ G', ⦃Q'⦄)"
using assms by (cases F; simp add: ag.mono)

lemma strengthen_pre:
  assumes "st_ord (¬ F) P P'"
  shows "st_ord F (⦃P⦄, A ⊢ G, ⦃Q⦄) (⦃P'⦄, A ⊢ G, ⦃Q⦄)"
using assms by (cases F; simp add: ag.mono)

lemmas pre_ag = order.trans[OF _ ag.mono[OF order.refl _ _ order.refl], of c] for c
lemmas pre_a = ag.pre_ag[OF _ _ order.refl]
lemmas pre_g = ag.pre_ag[OF _ order.refl]

lemma pre:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  assumes "⋀s. P' s ⟹ P s"
  assumes "A' ⊆ A"
  assumes "G ⊆ G'"
  assumes "⋀v s. Q v s ⟹ Q' v s"
  shows "c ≤ ⦃P'⦄, A' ⊢ G', ⦃Q'⦄"
using assms(2-) by (blast intro: order.trans[OF assms(1) ag.mono])

lemmas pre_pre_post = ag.pre[OF _ _ order.refl order.refl, of c] for c

lemma pre_imp:
  assumes "⋀s. P s ⟹ P' s"
  assumes "c ≤ ⦃P'⦄, A ⊢ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
using assms ag.pre by blast

lemmas pre_pre = ag.pre_imp[rotated]

lemma post_imp:
  assumes "⋀v s . Q v s ⟹ Q' v s"
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊢ G, ⦃Q'⦄"
using assms ag.pre by blast

lemmas pre_post = ag.post_imp[rotated]
lemmas strengthen_post = ag.pre_post

lemmas reflcl_ag = spec.invmap.ag[where sf=id and vf=id, simplified spec.invmap.id, simplified]

lemma
  shows reflcl_a: "⦃P⦄, A ⊢ G, ⦃Q⦄ = ⦃P⦄, A⇧= ⊢ G, ⦃Q⦄"
    and reflcl_g: "⦃P⦄, A ⊢ G, ⦃Q⦄ = ⦃P⦄, A ⊢ G⇧=, ⦃Q⦄"
by (metis ag.reflcl_ag sup.left_idem sup_commute)+

lemma gen_asm_base:
  assumes "P ⟹ c ≤ ⦃P' ❙∧ P''⦄, A ⊢ G, ⦃Q⦄"
  shows "c ≤ ⦃P' ❙∧ ⟨P⟩ ❙∧ P''⦄, A ⊢ G, ⦃Q⦄"
using assms by (simp add: ag_def spec.pre.conj spec.pre.K heyting.botL)

lemmas gen_asm =
  ag.gen_asm_base[where P'="⟨True⟩" and P''="⟨True⟩", simplified]
  ag.gen_asm_base[where P'="⟨True⟩", simplified]
  ag.gen_asm_base[where P''="⟨True⟩", simplified]
  ag.gen_asm_base

lemma post_conj:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q'⦄"
  shows "c ≤ ⦃P⦄, A ⊢ G, ⦃λv. Q v ❙∧ Q' v⦄"
using assms by (simp add: ag_def spec.post.conj heyting)

lemma pre_disj:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  assumes "c ≤ ⦃P'⦄, A ⊢ G, ⦃Q⦄"
  shows "c ≤ ⦃P ❙∨ P'⦄, A ⊢ G, ⦃Q⦄"
using assms by (simp add: ag_def spec.pre.disj inf_sup_distrib heyting)

lemma drop_imp:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊢ G, ⦃λv. Q' v ❙⟶ Q v⦄"
using assms ag.strengthen_post by fastforce

lemma "prop":
  shows "c ≤ ⦃⟨P⟩⦄, A ⊢ UNIV, ⦃λv. ⟨P⟩⦄"
by (simp add: ag.gen_asm(1) ag.post_top(3))

lemma name_pre_state:
  assumes "⋀s. P s ⟹ c ≤ ⦃(=) s⦄, A ⊢ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
by (metis assms ag.refinement refinement.name_pre_state spec.idle.rel_le)

lemma conj_lift:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  assumes "c ≤ ⦃P'⦄, A ⊢ G, ⦃Q'⦄"
  shows "c ≤ ⦃P ❙∧ P'⦄, A ⊢ G, ⦃λv. Q v ❙∧ Q' v⦄"
using assms by (blast intro: ag.post_conj ag.pre)

lemma disj_lift:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  assumes "c ≤ ⦃P'⦄, A ⊢ G, ⦃Q'⦄"
  shows "c ≤ ⦃P ❙∨ P'⦄, A ⊢ G, ⦃λv. Q v ❙∨ Q' v⦄"
using assms by (simp add: ag_def spec.post.disj spec.pre.disj heyting inf_sup_distrib le_supI1 le_supI2)

lemma all_lift:
  assumes "⋀x. c ≤ ⦃P x⦄, A ⊢ G, ⦃Q x⦄"
  shows "c ≤ ⦃❙∀x. P x⦄, A ⊢ G, ⦃λv. ❙∀x. Q x v⦄"
using assms
by (auto simp: ag_def spec.pre.All spec.post.All le_Inf_iff heyting
    simp flip: INF_inf_const1 INF_inf_const2)

lemma interference_le:
  shows "spec.rel ({env} × UNIV) ≤ ⦃P⦄, A ⊢ G, ⦃⊤⦄"
    and "spec.rel ({env} × UNIV) ≤ ⦃P⦄, A ⊢ G, ⦃λ_. ⊤⦄"
    and "spec.rel ({env} × UNIV) ≤ ⦃P⦄, A ⊢ G, ⦃λ_ _. True⦄"
by (auto simp: ag_def heyting spec.term.all.rel intro: spec.rel.mono inf.coboundedI1)

lemma assm_heyting:
  fixes Q :: "'v ⇒ 's pred"
  shows "ag.assm r ❙⟶⇩H ⦃P⦄, A ⊢ G, ⦃Q⦄ = ⦃P⦄, A ∩ r ⊢ G, ⦃Q⦄"
by (simp add: ag_def ac_simps Int_Un_distrib Times_Int_Times flip: heyting.curry_conv spec.rel.inf)

lemma augment_a: ―‹ instantiate ‹A'› ›
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  shows "c ≤ ⦃P⦄, A ∩ A' ⊢ G, ⦃Q⦄"
by (blast intro: ag.pre_a[OF assms])

lemma augment_post: ―‹ instantiate ‹Q› ›
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃λv. Q' v ❙∧ Q v⦄"
  shows "c ≤ ⦃P⦄, A ⊢ G, ⦃Q'⦄"
by (blast intro: ag.pre_post[OF assms])

lemma augment_post_imp: ―‹ instantiate ‹Q› ›
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃λv. (Q v ❙⟶ Q' v) ❙∧ Q v⦄"
  shows "c ≤ ⦃P⦄, A ⊢ G, ⦃Q'⦄"
by (blast intro: ag.pre_post[OF assms])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.term.none"›

lemma ag_le:
  shows "spec.term.none (⦃P⦄, A ⊢ G, ⦃Q⦄) ≤ ⦃P⦄, A ⊢ G, ⦃⊥⦄"
by (simp add: ag.refinement spec.term.all.rel order.trans[OF spec.term.none.refinement_le])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag.spec.term"›

lemmas none_inteference =
  order.trans[OF spec.term.none.mono,
              OF ag.interference_le(1) ag.pre_post[where Q'=Q for Q, OF spec.term.none.ag_le, simplified]]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag.spec"›

lemma bind:
  assumes g: "⋀v. g v ≤ ⦃Q' v⦄, A ⊢ G, ⦃Q⦄"
  assumes f: "f ≤ ⦃P⦄, A ⊢ G, ⦃Q'⦄"
  shows "f ⤜ g ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
apply (subst ag.refinement)
apply (rule refinement.spec.bind[where f'="ag.guar G" and g'="⟨ag.guar G⟩", simplified spec.rel.wind_bind])
 apply (rule refinement.pre_a[OF g[unfolded ag.refinement]])
 apply (simp_all add: refinement.spec.bind.res.rel_le spec.term.all.rel f[unfolded ag.refinement])
done

lemma action:
  fixes F :: "('v × sequential × 's × 's) set"
  assumes Q: "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F⟧ ⟹ Q v s'"
  assumes G: "⋀v s s'. ⟦P s; (v, self, s, s') ∈ F; s ≠ s'⟧ ⟹ (s, s') ∈ G"
  shows "spec.action F ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
proof -
  from G have *: "spec.pre P ⊓ spec.action F ≤ spec.rel ({env} × UNIV ∪ {self} × G)"
    by - (rule order.trans[OF spec.pre.inf_action_le(1) spec.action.rel_le]; auto)
  show ?thesis
    by (fastforce intro: order.trans[OF _ refinement.mono_stronger[OF order.refl _ _ order.refl]]
                         refinement.spec.action Q
                   simp: ag.refinement order.trans[OF *] spec.next_imp.closure.expansive spec.idle.rel_le)
qed

lemma return:
  shows "spec.return v ≤ ⦃Q v⦄, A ⊢ G, ⦃Q⦄"
by (auto simp: spec.return_def intro: ag.spec.action)

lemma Parallel_assm:
  shows "refinement.spec.env_hyp P (ag.assm A) as (ag.guar ∘ G) a ≤ ag.assm (A ∪ ⋃ (G ` (as - {a})))"
by (simp add: refinement.spec.env_hyp_def spec.invmap.rel flip: spec.rel.upper_INF spec.rel.inf)
   (force intro!: le_infI2 order.trans[OF spec.map.rel_le] spec.rel.mono_reflcl)

lemma Parallel_guar:
  shows "spec.Parallel as (ag.guar ∘ G) = ag.guar (⋃a∈as. G a)"
proof -
  have *: "{self} × Id ∪ (insert env ((λx. self) ` as) × Id ∪ map_prod toSequential_fn id ` (insert env (proc ` as) × UNIV ∩ (⋂x∈as. {proc x} × G x ∪ (- {proc x}) × UNIV)))
         = {env} × UNIV ∪ ({self} × Id ∪ {self} × ⋃ (G ` as))"
    by (rule antisym, force simp: toSequential_fn_def, (safe; force simp: map_prod_conv))
  show ?thesis
    apply (simp add: spec.Parallel_def spec.invmap.rel
               flip: spec.rel.INF spec.rel.inf)
    apply (subst spec.map.rel)
     apply (clarsimp; blast)
    apply (subst (1 2) spec.rel.reflcl[where A="{self}", symmetric])
    apply (clarsimp simp: ac_simps inf_sup_distrib image_Un image_image *
                          map_prod_image_Times map_prod_vimage_Times Times_Int_Times)
    done
qed

lemma Parallel:
  fixes A :: "'s rel"
  fixes G :: "'a ⇒ 's rel"
  fixes Q :: "'a ⇒ 's ⇒ bool"
  fixes Ps :: "'a ⇒ (sequential, 's, unit) spec"
  assumes proc_ag: "⋀a. a ∈ as ⟹ Ps a ≤ ⦃P a⦄, A ∪ (⋃a'∈as-{a}. G a') ⊢ G a, ⦃λv. Q a⦄"
  shows "spec.Parallel as Ps ≤ ⦃⨅a∈as. P a⦄, A ⊢ ⋃a∈as. G a, ⦃λrv. ⨅a∈as. Q a⦄"
unfolding ag.refinement
apply (rule order.trans[OF _ refinement.mono[OF order.refl _ _ order.refl]])
  apply (rule refinement.spec.Parallel[where A="ag.assm A" and Ps'="ag.guar ∘ G"])
  apply (rule order.trans[OF proc_ag, unfolded ag.refinement], assumption)
  apply (rule refinement.mono[OF order.refl _ _ order.refl])
   apply (force intro: ag.spec.Parallel_assm simp: ag.spec.Parallel_guar)+
done

setup ‹Sign.parent_path›


subsubsection‹ Stability rules ›

setup ‹Sign.mandatory_path "spec"›

lemma stable_pre_post:
  fixes S :: "('a, 's, 'v) spec"
  assumes "stable (snd ` r) P"
  assumes "spec.steps S ⊆ r"
  shows "S ≤ spec.pre P ❙⟶⇩H spec.post ⟨P⟩"
proof -
  have "P (trace.final' s xs)"
    if "P s"
   and "trace.steps (trace.T s xs v) ⊆ r"
   for s :: 's and xs :: "('a × 's) list" and v :: "'v option"
    using that
  proof(induct xs arbitrary: s)
    case (Cons x xs) with ‹stable (snd ` r) P› show ?case
      by (cases x; cases "snd x = s";
          force simp: stable_def monotone_def dest: le_boolD)
  qed simp
  from this ‹spec.steps S ⊆ r› show ?thesis
    by - (rule spec.singleton_le_extI;
          auto dest: order.trans[where b=S]
               simp: spec.singleton.le_conv spec.singleton.heyting_le_conv trace.split_all spec.rel.galois
              split: option.split)
qed

lemma pre_post_stable:
  fixes P :: "'s ⇒ bool"
  assumes "stable (snd ` r) P"
  shows "spec.rel r ≤ spec.pre P ❙⟶⇩H spec.post ⟨P⟩"
by (rule spec.stable_pre_post[OF assms spec.rel.lower_upper_contractive])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag"›

lemma stable_lift:
  assumes "stable (A ∪ G) P'" ―‹ anything stable over ‹A ∪ G› is invariant ›
  shows "⦃P ❙∧ P'⦄, A ⊢ G, ⦃λv. P' ❙⟶ Q v⦄ ≤ ⦃P ❙∧ P'⦄, A ⊢ G, ⦃λv. Q v ❙∧ P'⦄"
apply (simp add: ag_def spec.pre.conj heyting heyting.detachment le_infI2 flip: spec.heyting.post)
apply (simp add: ac_simps Sigma_Un_distrib2 Int_Un_distrib Times_Int_Times flip: spec.rel.inf)
apply (rule order.subgoal)
 apply (rule order.trans[OF _ spec.pre_post_stable[where r="{env} × A ∪ {self} × G", simplified image_Un, simplified, OF assms]])
 apply (simp add: le_infI2; fail)
apply (simp add: ac_simps spec.post.conj)
apply (simp add: heyting.discharge le_infI1 flip: inf.assoc)
done

lemma stable_augment_base:
  assumes "c ≤ ⦃P ❙∧ P'⦄, A ⊢ G, ⦃λv. P' ❙⟶ Q v⦄"
  assumes "stable (A ∪ G) P'" ―‹ anything stable over ‹A ∪ G› is invariant ›
  shows "c ≤ ⦃P ❙∧ P'⦄, A ⊢ G, ⦃λv. Q v ❙∧ P'⦄"
using order.trans[OF _ ag.stable_lift] assms by blast

lemma stable_augment:
  assumes "c ≤ ⦃P'⦄, A ⊢ G, ⦃Q'⦄"
  assumes "⋀v s. ⟦P s; Q' v s⟧ ⟹ Q v s"
  assumes "stable (A ∪ G) P"
  shows "c ≤ ⦃P' ❙∧ P⦄, A ⊢ G, ⦃Q⦄"
apply (rule ag.strengthen_post)
 apply (rule ag.stable_augment_base[where Q=Q, OF _ assms(3)])
 apply (auto intro: assms(2) ag.pre[OF assms(1)])
done

lemma stable_augment_post:
  assumes "c ≤ ⦃P'⦄, A ⊢ G, ⦃Q'⦄" ―‹ resolve before application›
  assumes "⋀v. stable (A ∪ G) (Q' v ❙⟶ Q v)"
  shows "c ≤ ⦃(❙∀v. Q' v ❙⟶ Q v) ❙∧ P'⦄, A ⊢ G, ⦃Q⦄"
apply (rule ag.pre_pre_post)
 apply (rule ag.stable_augment_base[where P=P' and Q=Q' and P'="(❙∀v. Q' v ❙⟶ Q v)"])
   apply (rule ag.pre_pre_post[OF assms(1)])
    using assms(2) apply (fast intro: stable.allI)+
done

lemma stable_augment_frame: ―‹ anything stable over ‹A ∪ G› is invariant\label{sec:refinement-frame} ›
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  assumes "stable (A ∪ G) P'"
  shows "c ≤ ⦃P ❙∧ P'⦄, A ⊢ G, ⦃λv. Q v ❙∧ P'⦄"
using assms by (blast intro: ag.stable_augment[OF assms(1)])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag.spec"›

lemma stable_interference:
  assumes "stable (A ∩ r) P"
  shows "spec.rel ({env} × r) ≤ ⦃P⦄, A ⊢ G, ⦃⟨P⟩⦄"
using assms
by (auto simp: ag_def ac_simps heyting Int_Un_distrib Times_Int_Times
    simp flip: spec.rel.inf
        intro: le_infI2 spec.rel.mono spec.pre_post_stable[simplified heyting ac_simps])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "cam"›

lemma closed_ag:
  shows "⦃P⦄, A ⊢ G, ⦃Q⦄ ∈ spec.cam.closed ({env} × r)"
unfolding ag_def heyting.infR
by (blast intro: subsetD[OF spec.cam.closed.antimono, rotated])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference"›

lemma cl_ag_le:
  assumes P: "stable (A ∩ r) P"
  assumes Q: "⋀v. stable (A ∩ r) (Q v)"
  shows "spec.interference.cl ({env} × r) (⦃P⦄, A ⊢ G, ⦃Q⦄) ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
unfolding spec.interference.cl_def
by (rule ag.spec.bind ag.spec.return ag.spec.stable_interference spec.cam.least[OF _ spec.cam.closed_ag] assms order.refl)+

lemma closed_ag:
  assumes P: "stable (A ∩ r) P"
  assumes Q: "⋀v. stable (A ∩ r) (Q v)"
  shows "⦃P⦄, A ⊢ G, ⦃Q⦄ ∈ spec.interference.closed ({env} × r)"
by (rule spec.interference.closed_clI[OF spec.interference.cl_ag_le[OF assms]])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›
(*<*)

end
(*>*)