Theory Constructions

(*<*)
theory Constructions
imports
  Safety_Logic
begin

(*>*)
section‹ Constructions in the ∗‹('a, 's, 'v) spec› lattice\label{sec:constructions} ›


subsection‹ Constrains-at-most \label{sec:cam} ›

text‹

\<^citet>‹‹\S3.1› in "AbadiPlotkin:1993"›
require that processes to be composed in parallel
∗‹constrain at most› (CAM) distinct sets of agents:
intuitively each process cannot block other processes from taking
steps after any of its transitions. We model this as a closure.

See \S\ref{sec:abadi_plotkin} for a discussion of their composition rules.

Observations:
 ▪ the sense of the relation ‹r› here is inverted wrt Abadi/Plotkin
 ▪ this is a key ingredient in interference closure (\S\ref{sec:interference_closure})
 ▪ this closure is antimatroidal

›

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "cam"›

definition cl :: "('a, 's) steps ⇒ ('a, 's, 'v) spec ⇒ ('a, 's, 'v) spec" where
  "cl r P = P ⊔ spec.term.none (spec.term.all P ⤜ (λ_::unit. spec.rel r :: (_, _, unit) spec))"

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "none.cam"›

lemma cl:
  shows "spec.term.none (spec.cam.cl r P) = spec.cam.cl r (spec.term.none P)"
by (simp add: spec.cam.cl_def spec.bind.supL spec.bind.bind spec.term.all.bind ac_simps
        flip: spec.bind.botR bot_fun_def)

lemma cl_rel_wind:
  fixes P :: "('a, 's, 'v) spec"
  shows "spec.cam.cl r P ⪢ spec.term.none (spec.rel r :: ('a, 's, 'w) spec)
       = spec.term.none (spec.cam.cl r P)"
by (simp add: spec.cam.cl_def spec.term.none.sup spec.term.none.bind spec.bind.supL spec.bind.bind
              bot_fun_def sup.absorb2
              spec.vmap.unitL[where f=P] spec.vmap.unitL[where f="spec.term.all P"]
              spec.vmap.unitL[where f="spec.rel r :: ('a, 's, 'w) spec"]
              spec.term.all.vmap_unit  spec.vmap.unit_rel spec.bind.mono spec.term.all.expansive
        flip: spec.bind.botR)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "all.cam"›

lemma cl_le: ―‹ Converse does not hold ›
  shows "spec.cam.cl r (spec.term.all P) ≤ spec.term.all (spec.cam.cl r P)"
by (simp add: spec.term.none.cam.cl flip: spec.term.galois) (simp flip: spec.term.none.cam.cl)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

interpretation cam: closure_complete_distrib_lattice_distributive_class "spec.cam.cl r" for r :: "('a, 's) steps"
proof standard
  show "P ≤ spec.cam.cl r Q ⟷ spec.cam.cl r P ≤ spec.cam.cl r Q" (is "?lhs ⟷ ?rhs") for P Q :: "('a, 's, 'v) spec"
  proof(rule iffI)
    assume ?lhs show ?rhs
      apply (subst spec.cam.cl_def)
      apply (strengthen ord_to_strengthen(1)[OF ‹?lhs›])
      apply (simp add: spec.cam.cl_def spec.term.galois spec.term.all.sup spec.term.all.bind
                       spec.bind.supL spec.term.all.rel spec.bind.bind spec.rel.wind_bind)
      done
next
    show "?rhs ⟹ ?lhs"
      by (simp add: spec.cam.cl_def)
  qed
  show "spec.cam.cl r (⨆P) ≤ ⨆(spec.cam.cl r ` P) ⊔ spec.cam.cl r ⊥" for P :: "('a, 's, 'v) spec set"
    by (simp add: spec.cam.cl_def spec.term.none.bind spec.term.all.Sup spec.bind.SupL
                  spec.term.none.Sup SUP_upper2)
qed

setup ‹Sign.mandatory_path "cam"›

setup ‹Sign.mandatory_path "cl"›

lemma bot[simp]:
  shows "spec.cam.cl r ⊥ = ⊥"
by (simp add: spec.cam.cl_def)

lemma mono:
  fixes r :: "('a, 's) steps"
  assumes "r ⊆ r'"
  assumes "P ≤ P'"
  shows "spec.cam.cl r P ≤ spec.cam.cl r' P'"
unfolding spec.cam.cl_def
apply (strengthen ord_to_strengthen(1)[OF ‹r ≤ r'›])
apply (strengthen ord_to_strengthen(1)[OF ‹P ≤ P'›])
apply blast
done

declare spec.cam.strengthen_cl[strg del]

lemma strengthen[strg]:
  assumes "st_ord F r r'"
  assumes "st_ord F P P'"
  shows "st_ord F (spec.cam.cl r P) (spec.cam.cl r' P')"
using assms by (cases F; simp add: spec.cam.cl.mono)

lemma Sup:
  shows "spec.cam.cl r (⨆X) = (⨆P∈X. spec.cam.cl r P)"
by (simp add: spec.cam.cl_Sup)

lemmas sup = spec.cam.cl.Sup[where X="{P, Q}" for P Q, simplified]

lemma rel_empty:
  shows "spec.cam.cl {} P = P"
by (simp add: spec.cam.cl_def spec.rel.empty sup.absorb1 UNIV_unit)

lemma rel_reflcl:
  shows "spec.cam.cl (r ∪ A × Id) P = spec.cam.cl r P"
    and "spec.cam.cl (A × Id ∪ r) P = spec.cam.cl r P"
by (simp_all add: spec.cam.cl_def spec.rel.reflcl)

lemma rel_minus_Id:
  shows "spec.cam.cl (r - UNIV × Id) P = spec.cam.cl r P"
by (metis Un_Diff_cancel2 spec.cam.cl.rel_reflcl(1))

lemma Inf:
  shows "spec.cam.cl r (⨅X) = ⨅(spec.cam.cl r ` X)" (is "?lhs = ?rhs")
proof(rule antisym[OF spec.cam.cl_Inf_le spec.singleton_le_extI])
  show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
  proof (cases "trace.term σ")
    case None
    have "⦉σ⦊ ≤ ⨅ (spec.term.all ` X) ⤜ (λv. spec.term.none (spec.rel r))"
      if "x ∈ X" and "¬ ⦉σ⦊ ≤ x"
     for x
    proof -
      from ‹⦉σ⦊ ≤ ?rhs› that
      have "⦉σ⦊ ≤ spec.term.all x ⤜ (λ_::unit. spec.term.none (spec.rel r :: (_, _, unit) spec))"
        by (auto simp: spec.cam.cl_def le_Inf_iff spec.term.none.bind)
      then show ?thesis
      proof(induct rule: spec.singleton.bind_le)
        case incomplete with ‹¬ ⦉σ⦊ ≤ x› show ?case
          using order_trans by auto
      next
        case (continue σ⇩f σ⇩g v⇩f)
        from None obtain xs ys
          where *: "∀xs' zs. trace.rest σ = xs' @ zs ∧ trace.steps' (trace.final' (trace.init σ) xs') zs ⊆ r
                         ⟶ length xs ≤ length xs'"
                   "xs @ ys = trace.rest σ"
                   "trace.steps' (trace.final' (trace.init σ) xs) ys ⊆ r"
          using ex_has_least_nat[where P="λxs. ∃ys. trace.rest σ = xs @ ys
                                             ∧ trace.steps' (trace.final' (trace.init σ) xs) ys ⊆ r"
                                   and k="trace.rest σ"
                                   and m=length]
          by clarsimp
        show ?case
        proof(induct rule: spec.bind.continueI[where s="trace.init σ" and xs=xs and ys=ys
                                                 and v=undefined and w="trace.term σ",
                                               simplified ‹xs @ ys = trace.rest σ› trace.t.collapse,
                                               case_names f g])
          case f
          have "⦉trace.init σ, xs, None⦊ ≤ x"
            if "x ∈ X"
           and "⦉σ⦊ ≤ spec.cam.cl r x"
           for x
            using that(2)[unfolded spec.cam.cl_def, simplified]
          proof(induct rule: disjE[consumes 1, case_names expansive cam])
            case expansive with ‹xs @ ys = trace.rest σ› show ?case
              by (cases σ)
                 (fastforce elim: order.trans[rotated]
                            simp: spec.singleton.mono trace.less_eq_same_append_conv)

          next
            case cam from cam[unfolded spec.term.none.bind] show ?case
            proof(induct rule: spec.singleton.bind_le)
              case incomplete with ‹xs @ ys = trace.rest σ› show ?case
                by clarsimp
                   (metis prefixI spec.singleton.mono spec.singleton_le_ext_conv
                          spec.term.none.contractive trace.less_eq_None(2))
            next
              case (continue σ⇩f σ⇩g v⇩f) with *(1,2) show ?case
                by (clarsimp simp: spec.singleton.le_conv trace.less_eq_None
                            elim!: order.trans[rotated]
                           intro!: spec.singleton.mono)
                   (metis prefixI prefix_length_prefix)
            qed
          qed
          with ‹⦉σ⦊ ≤ ?rhs› show ?case
            by (simp add: le_Inf_iff spec.singleton.le_conv exI[where x=None])
        next
          case g with None *(3) show ?case
            by (simp add: spec.singleton.le_conv)
        qed
    qed
  qed
  then show "⦉σ⦊ ≤ ?lhs"
    by (auto simp: spec.cam.cl_def spec.term.none.bind spec.term.all.Inf le_Inf_iff)
  next
    case Some with ‹⦉σ⦊ ≤ ?rhs› show ?thesis
      by (simp add: le_Inf_iff spec.cam.cl_def spec.singleton.term.none_le_conv)
  qed
qed

lemmas inf = spec.cam.cl.Inf[where X="{P, Q}" for P Q, simplified]

lemma idle:
  shows "spec.cam.cl r spec.idle = spec.term.none (spec.rel r :: (_, _, unit) spec)"
by (simp add: spec.cam.cl_def spec.term.all.idle UNIV_unit spec.bind.returnL
              spec.idle_le sup_absorb2)

lemma bind:
  shows "spec.cam.cl r (f ⤜ g) = spec.cam.cl r f ⤜ (λv. spec.cam.cl r (g v))"
by (simp add: spec.cam.cl_def spec.bind.supL spec.bind.supR spec.bind.bind ac_simps spec.term.all.bind
        flip: spec.bind.botR bot_fun_def)

lemma action:
  fixes r :: "('a, 's) steps"
  fixes F :: "('v × 'a × 's × 's) set"
  shows "spec.cam.cl r (spec.action F)
       = spec.action F
      ⊔ spec.term.none (spec.action F ⪢ (spec.rel r :: (_, _, unit) spec))
      ⊔ spec.term.none (spec.rel r :: (_, _, unit) spec)"
by (simp add: spec.cam.cl_def spec.term.all.action spec.term.none.bind spec.term.none.sup
              spec.bind.botR spec.bind.supL spec.bind.returnL spec.idle_le
              spec.vmap.unitL[where f="spec.action F"] spec.map.surj_sf_action
              UNIV_unit map_prod_const_image ac_simps
        flip: spec.return_def)

lemma return:
  shows "spec.cam.cl r (spec.return v) = spec.return v ⊔ spec.term.none (spec.rel r :: (_, _, unit) spec)"
unfolding spec.return_def spec.cam.cl.action
by (simp add: spec.bind.returnL spec.idle_le bot_fun_def
        flip: spec.return_def bot_fun_def)

lemma rel_le:
  assumes "r ⊆ r' ∨ r' ⊆ r"
  shows "spec.cam.cl r (spec.rel r') ≤ spec.rel (r ∪ r')"
using assms
by (auto simp: spec.cam.cl_def spec.rel.mono spec.term.all.rel
               spec.rel.wind_bind_leading spec.rel.wind_bind_trailing spec.term.galois)

lemma rel:
  assumes "r ⊆ r'"
  shows "spec.cam.cl r (spec.rel r') = spec.rel r'"
by (simp add: assms spec.eq_iff spec.cam.expansive
              order.trans[OF spec.cam.cl.rel_le[OF disjI1] spec.rel.mono])

lemma inf_rel:
  fixes r :: "('a, 's) steps"
  fixes s :: "('a, 's) steps"
  fixes P :: "('a, 's, 'v) spec"
  shows "spec.rel r ⊓ spec.cam.cl r' P = spec.cam.cl (r ∩ r') (spec.rel r ⊓ P)" (is ?thesis1)
    and "spec.cam.cl r' P ⊓ spec.rel r = spec.cam.cl (r ∩ r') (spec.rel r ⊓ P)" (is ?thesis2)
proof -
  show ?thesis1
    by (simp add: spec.cam.cl_def ac_simps inf_sup_distrib
                  spec.term.none.bind spec.term.all.inf spec.term.all.rel
                  spec.bind.inf_rel spec.rel.inf spec.term.none.inf spec.term.none.inf_none_rel(1))
  then show ?thesis2
    by (rule inf_commute_conv)
qed

lemma bind_return:
  shows "spec.cam.cl r (f ⪢ spec.return v) = spec.cam.cl r f ⪢ spec.return v"
by (simp add: spec.cam.cl.bind spec.cam.cl.return spec.bind.supR sup.absorb1 spec.term.none.cam.cl_rel_wind)

lemma heyting_le:
  shows "spec.cam.cl r (P ❙⟶⇩H Q) ≤ P ❙⟶⇩H spec.cam.cl r Q"
by (force intro!: SupI
            dest: spec.cam.mono_cl[where r=r]
            elim: order.trans[rotated]
            simp: heyting_def spec.cam.cl.Sup spec.cam.cl.inf le_infI1 spec.cam.expansive)

lemma pre:
  shows "spec.cam.cl r (spec.pre P) = spec.pre P"
by (simp add: spec.cam.cl_def spec.term.none.bind spec.term.all.pre sup_iff_le spec.bind.inf_pre
        flip: inf_iff_le)

lemma post:
  shows "spec.cam.cl r (spec.post Q) = spec.post Q"
by (simp add: spec.cam.cl_def spec.term.none.post_le sup_iff_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "closed"›

lemma empty:
  shows "spec.cam.closed {} = UNIV"
by (simp add: order.eq_iff spec.cam.cl.rel_empty spec.cam.closed_clI subsetI)

lemma antimonotone:
  shows "antimono spec.cam.closed"
by (rule monotoneI) (auto intro: spec.cam.closed_clI elim: spec.cam.le_closedE[OF spec.cam.cl.mono])

lemmas strengthen[strg] = st_ord_antimono[OF spec.cam.closed.antimonotone]
lemmas antimono = antimonoD[OF spec.cam.closed.antimonotone, of r r' for r r']

lemma reflcl:
  shows "spec.cam.closed (r ∪ A × Id) = spec.cam.closed r"
by (simp add: spec.cam.cl.rel_reflcl(1) spec.cam.closed_def)

setup ‹Sign.mandatory_path "term"›

lemma none:
  assumes "P ∈ spec.cam.closed r"
  shows "spec.term.none P ∈ spec.cam.closed r"
by (simp add: assms spec.cam.closed_clI flip: spec.term.none.cam.cl spec.cam.closed_conv[OF assms])

setup ‹Sign.parent_path›

lemma bind:
  fixes f :: "('a, 's, 'v) spec"
  fixes g :: "'v ⇒ ('a, 's, 'w) spec"
  assumes "f ∈ spec.cam.closed r"
  assumes "⋀x. g x ∈ spec.cam.closed r"
  shows "f ⤜ g ∈ spec.cam.closed r"
by (simp add: assms spec.cam.closed_clI spec.cam.least spec.cam.cl.bind spec.bind.mono)

lemma rel[intro]:
  assumes "r ⊆ r'"
  shows "spec.rel r' ∈ spec.cam.closed r"
by (simp add: assms spec.cam.closed_clI spec.cam.cl.rel)

lemma pre[intro]:
  shows "spec.pre P ∈ spec.cam.closed r"
by (simp add: spec.cam.closed_clI spec.cam.cl.pre)

lemma post[intro]:
  shows "spec.post Q ∈ spec.cam.closed r"
by (simp add: spec.cam.closed_clI spec.cam.cl.post)

lemma heyting[intro]:
  assumes "Q ∈ spec.cam.closed r"
  shows "P ❙⟶⇩H Q ∈ spec.cam.closed r"
by (rule spec.cam.closed_clI)
   (simp add: assms order.trans[OF spec.cam.cl.heyting_le] flip: spec.cam.closed_conv)

lemma snoc_conv:
  fixes P :: "('a, 's, 'v) spec"
  assumes "P ∈ spec.cam.closed r"
  assumes "(fst x, trace.final' s xs, snd x) ∈ r ∪ UNIV × Id"
  shows "⦉s, xs @ [x], None⦊ ≤ P ⟷ ⦉s, xs, None⦊ ≤ P" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
    by (erule order.trans[rotated]) (simp add: spec.singleton.mono trace.less_eq_same_append_conv)
  from assms(2) show "?rhs ⟹ ?lhs"
    by (subst spec.cam.closed_conv[OF ‹P ∈ spec.cam.closed r›])
       (auto simp: spec.cam.cl_def spec.singleton.term.none_le_conv
                   spec.term.none.singleton spec.steps.singleton
        simp flip: spec.rel.galois spec.term.galois
            intro: spec.bind.continueI)
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap.cam"›

lemma cl:
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  fixes r :: "('b, 't) steps"
  fixes P :: "('b, 't, 'w) spec"
  shows "spec.invmap af sf vf (spec.cam.cl r P)
       = spec.cam.cl (map_prod af (map_prod sf sf) -` (r ∪ UNIV × Id)) (spec.invmap af sf vf P)"
by (simp add: spec.cam.cl_def spec.invmap.sup spec.invmap.bind spec.invmap.rel spec.term.all.invmap
        flip: spec.term.none.invmap_gen[where vf=id])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "map.cam"›

lemma cl_le:
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  fixes r :: "('a, 's) steps"
  fixes P :: "('a, 's, 'v) spec"
  shows "spec.map af sf vf (spec.cam.cl r P)
      ≤ spec.cam.cl (map_prod af (map_prod sf sf) ` r) (spec.map af sf vf P)"
by (simp add: spec.map_invmap.galois spec.map_invmap.upper_lower_expansive
              spec.invmap.cam.cl spec.cam.cl.mono subset_vimage_iff le_supI1)

lemma cl_inj_sf:
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  fixes r :: "('a, 's) steps"
  fixes P :: "('a, 's, 'v) spec"
  assumes "inj sf"
  shows "spec.map af sf vf (spec.cam.cl r P)
       = spec.cam.cl (map_prod af (map_prod sf sf) ` r) (spec.map af sf vf P)"
apply (simp add: spec.cam.cl_def spec.map.sup spec.map.bind_inj_sf[OF ‹inj sf›] spec.term.all.map
           flip: spec.term.none.map_gen[where vf=id])
apply (subst spec.map.rel, blast dest: injD[OF ‹inj sf›])
apply (simp add: inf.absorb1 spec.map_invmap.galois spec.invmap.post flip: spec.bind_post_pre)
done

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Abadi and Plotkin's composition principle\label{sec:abadi_plotkin} ›

text‹

\<^citet>‹"AbadiPlotkin:1991" and "AbadiPlotkin:1993"›
develop a theory of circular reasoning about Heyting implication for
safety properties under the mild condition that each is CAM-closed with respect to the other.

›

setup ‹Sign.mandatory_path "spec"›

abbreviation ap_cam_cl :: "'a set ⇒ ('a, 's, 'v) spec ⇒ ('a, 's, 'v) spec" where
  "ap_cam_cl as ≡ spec.cam.cl ((-as) × UNIV)"

abbreviation (input) ap_cam_closed :: "'a set ⇒ ('a, 's, 'v) spec set" where
  "ap_cam_closed as ≡ spec.cam.closed ((-as) × UNIV)"

lemma composition_principle_1:
  fixes P :: "('a, 's, 'v) spec"
  assumes "P ∈ spec.ap_cam_closed as"
  assumes "P ∈ spec.term.closed _"
  assumes "spec.idle ≤ P"
  shows "spec.ap_cam_cl (-as) P ❙⟶⇩H P ≤ P" (is "?lhs ≤ ?rhs")
proof(rule spec.term.closed.singleton_le_extI)
  show "⦉s, xs, None⦊ ≤ ?rhs" if "⦉s, xs, None⦊ ≤ ?lhs" for s xs
    using that
  proof(induct xs rule: rev_induct)
    case Nil
    from ‹spec.idle ≤ P› show ?case
      by (simp add: order.trans[OF spec.idle.minimal_le])
  next
    case (snoc x xs)
    from snoc.prems have "⦉s, xs, None⦊ ≤ spec.ap_cam_cl (- as) P ❙⟶⇩H P"
      by (simp add: order.trans[OF spec.singleton.mono, rotated] trace.less_eq_None)
    with snoc.hyps have "⦉s, xs, None⦊ ≤ P" by blast
    show ?case
    proof(cases "fst x ∈ as")
      case True
      with ‹⦉s, xs, None⦊ ≤ P› have "⦉s, xs @ [x], None⦊ ≤ spec.ap_cam_cl (-as) P"
        by (subst spec.cam.closed.snoc_conv) (auto simp: order.trans[OF _ spec.cam.expansive])
      with snoc.prems show ?thesis by (blast intro: heyting.mp)
    next
      case False with ‹P ∈ spec.ap_cam_closed as› ‹⦉s, xs, None⦊ ≤ P› show ?thesis
        by (simp add: spec.cam.closed.snoc_conv)
    qed
  qed
qed fact

lemma composition_principle_half: ―‹ \<^citet>‹‹\S3.1(4)› in "AbadiPlotkin:1993"› -- cleaner than in \<^citet>‹‹\S3.1› in "AbadiPlotkin:1991"› ›
  assumes "M⇩1 ∈ spec.ap_cam_closed a⇩1"
  assumes "M⇩2 ∈ spec.ap_cam_closed a⇩2"
  assumes "M⇩1 ∈ spec.term.closed _"
  assumes "spec.idle ≤ M⇩1"
  assumes "a⇩1 ∩ a⇩2 = {}"
  shows "(M⇩1 ❙⟶⇩H M⇩2) ⊓ (M⇩2 ❙⟶⇩H M⇩1) ≤ M⇩1"
proof -
  have "(M⇩1 ❙⟶⇩H M⇩2) ⊓ (M⇩2 ❙⟶⇩H M⇩1) ≤ (spec.ap_cam_cl (-a⇩1) M⇩1 ❙⟶⇩H spec.ap_cam_cl (-a⇩1) M⇩2) ⊓ (M⇩2 ❙⟶⇩H M⇩1)"
    by (rule inf_mono[OF heyting.closure_imp_distrib_le[OF closure.axioms(2)[OF spec.cam.closure_axioms]] order.refl])
       (simp add: spec.cam.cl.inf)
  also have "… ≤ spec.ap_cam_cl (-a⇩1) M⇩1 ❙⟶⇩H M⇩1"
  proof -
    from ‹M⇩2 ∈ spec.ap_cam_closed a⇩2› ‹a⇩1 ∩ a⇩2 = {}› have "spec.ap_cam_cl (-a⇩1) M⇩2 ≤ M⇩2"
      by (fastforce intro: spec.cam.least elim: subsetD[OF spec.cam.closed.antimono, rotated])
    then show ?thesis
      by (simp add: heyting.trans order_antisym_conv spec.cam.expansive)
  qed
  also have "… ≤ M⇩1"
    by (rule spec.composition_principle_1[OF ‹M⇩1 ∈ spec.ap_cam_closed a⇩1› ‹M⇩1 ∈ spec.term.closed _› ‹spec.idle ≤ M⇩1›])
  finally show ?thesis .
qed

theorem composition_principle: ― ‹ \<^citet>‹‹\S3.1(3)› in "AbadiPlotkin:1993"› ›
  assumes "M⇩1 ∈ spec.ap_cam_closed a⇩1"
  assumes "M⇩2 ∈ spec.ap_cam_closed a⇩2"
  assumes "M⇩1 ∈ spec.term.closed _"
  assumes "M⇩2 ∈ spec.term.closed _"
  assumes "spec.idle ≤ M⇩1"
  assumes "spec.idle ≤ M⇩2"
  assumes "a⇩1 ∩ a⇩2 = {}"
  shows "(M⇩1 ❙⟶⇩H M⇩2) ⊓ (M⇩2 ❙⟶⇩H M⇩1) ≤ M⇩1 ⊓ M⇩2"
using assms by (metis spec.composition_principle_half inf.bounded_iff inf.commute)

text‹

An infinitary variant can be established in essentially the same way
as @{thm [source] "spec.composition_principle_1"}.

›

lemma ag_circular:
  fixes Ps :: "'a ⇒ ('a, 's, 'v) spec"
  assumes cam_closed: "⋀a. a ∈ as ⟹ Ps a ∈ spec.ap_cam_closed {a}"
  assumes term_closed: "⋀a. a ∈ as ⟹ Ps a ∈ spec.term.closed _"
  assumes idle: "⋀a. a ∈ as ⟹ spec.idle ≤ Ps a"
  shows "(⨅a∈as. (⨅a'∈as-{a}. Ps a') ❙⟶⇩H Ps a) ≤ (⨅a∈as. Ps a)" (is "?lhs ≤ ?rhs")
proof(rule spec.term.closed.singleton_le_extI)
  show "⦉s, xs, None⦊ ≤ ?rhs" if "⦉s, xs, None⦊ ≤ ?lhs" for s xs
    using that
  proof(induct xs rule: rev_induct)
    case Nil from idle show ?case
      by (simp add: le_INF_iff order.trans[OF spec.idle.minimal_le])
  next
    case (snoc x xs)
    have *: "⦉s, xs, None⦊ ≤ ?rhs"
      by (simp add: snoc(1) order.trans[OF spec.singleton.mono snoc(2)] trace.less_eq_same_append_conv)
    have "⦉s, xs @ [x], None⦊ ≤ Ps a" if "a ∈ as" for a
    proof(cases "fst x = a")
      case True
      with cam_closed * have "⦉s, xs @ [x], None⦊ ≤ ⨅(Ps ` (as - {a}))"
        by (subst spec.cam.closed.snoc_conv[where r="⨅a'∈as-{a}. (- {a'}) × UNIV"])
           (auto simp: le_INF_iff intro: subsetD[OF spec.cam.closed.antimono, rotated])
      with snoc.prems(1) ‹a ∈ as› show ?thesis
        by (meson heyting.mp le_INF_iff)
    next
      case False with cam_closed * ‹a ∈ as› show ?thesis
        by (fastforce simp: spec.cam.closed.snoc_conv le_INF_iff)
    qed
    then show ?case by (blast intro: INFI)
  qed
  from term_closed show "?rhs ∈ spec.term.closed _"
    by (fastforce simp: spec.term.all.monomorphic)
qed

setup ‹Sign.parent_path›


subsection‹ Interference closure\label{sec:interference_closure} ›

text‹

We add environment interference to the beginnings and ends of behaviors for two reasons:
 ▪ it ensures the wellformedness of parallel composition as conjunction (see \S\ref{sec:constructions-parallel_composition})
 ▪ it guarantees the monad laws hold (see \S\ref{sec:programs-laws})
  ▪ \<^const>‹spec.cam.cl› by itself is too weak to justify these

We use this closure to build the program sublattice of the \<^typ>‹('a, 's, 'v) spec› lattice (see \S\ref{sec:programs}).

Observations:
 ▪ if processes are made out of actions then it is not necessary to apply \<^const>‹spec.cam.cl›

›

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "interference"›

definition cl :: "('a, 's) steps ⇒ ('a, 's, 'v) spec ⇒ ('a, 's, 'v) spec" where
  "cl r P = spec.rel r ⤜ (λ_::unit. spec.cam.cl r P) ⤜ (λv. spec.rel r ⤜ (λ_::unit. spec.return v))"

setup ‹Sign.parent_path›

interpretation interference: closure_complete_distrib_lattice_distributive_class "spec.interference.cl r"
           for r :: "('a, 's) steps"
proof
  show "P ≤ spec.interference.cl r Q ⟷ spec.interference.cl r P ≤ spec.interference.cl r Q" (is "?lhs ⟷ ?rhs")
   for P Q :: "('a, 's, 'v) spec"
  proof(rule iffI)
    assume ?lhs show ?rhs
      apply (subst spec.interference.cl_def)
      apply (strengthen ord_to_strengthen(1)[OF ‹?lhs›])
      apply (simp add: spec.interference.cl_def spec.cam.cl.bind spec.cam.cl.return spec.cam.cl.rel
                       spec.bind.bind spec.bind.supL spec.bind.supR
                       spec.bind.returnL spec.idle_le
                 flip: bot_fun_def spec.bind.botR)
      apply (simp add: spec.rel.wind_bind flip: spec.bind.bind)
      apply (simp add: spec.bind.bind spec.bind.mono)
      done
  next
    assume ?rhs show ?lhs
      apply (strengthen ord_to_strengthen(2)[OF ‹?rhs›])
      apply (simp add: spec.interference.cl_def spec.bind.bind)
      apply (strengthen ord_to_strengthen(2)[OF spec.cam.expansive])
      apply (strengthen ord_to_strengthen(2)[OF spec.return.rel_le])
      apply (auto simp: spec.bind.return intro: spec.bind.returnL_le)
      done
  qed
  show "spec.interference.cl r (⨆P) ≤ ⨆(spec.interference.cl r ` P) ⊔ spec.interference.cl r ⊥"
   for P :: "('a, 's, 'v) spec set"
    by (simp add: spec.interference.cl_def spec.cam.cl.Sup image_image
                  spec.bind.SupL spec.bind.supL spec.bind.SUPR
            flip: bot_fun_def)
qed

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "none"›

setup ‹Sign.mandatory_path "interference"›

lemma cl:
  shows "spec.term.none (spec.interference.cl r P) = spec.interference.cl r (spec.term.none P)"
by (simp add: spec.interference.cl_def spec.term.none.bind spec.term.none.return
              spec.bind.bind spec.bind.idleR spec.bind.botR spec.term.none.cam.cl_rel_wind
        flip: spec.term.none.cam.cl)

setup ‹Sign.mandatory_path "closed"›

lemma rel_le:
  assumes "P ∈ spec.interference.closed r"
  shows "spec.term.none (spec.rel r) ≤ P"
by (subst spec.interference.closed_conv[OF assms])
   (simp add: spec.interference.cl_def spec.term.galois spec.term.all.bind spec.term.all.rel ac_simps)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "all"›

lemma cl_le: ―‹ Converse does not hold ›
  shows "spec.interference.cl r (spec.term.all P) ≤ spec.term.all (spec.interference.cl r P)"
by (simp add: spec.interference.cl_def spec.bind.bind spec.bind.idleR spec.bind.botR
              spec.term.none.bind spec.term.none.return
              spec.term.none.cam.cl_rel_wind spec.term.none.cam.cl
        flip: spec.term.galois)
   (simp add: spec.bind.mono flip: spec.term.none.cam.cl)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "cam.closed.interference"›

lemma cl:
  shows "spec.interference.cl r P ∈ spec.cam.closed r"
by (metis spec.cam.closed_clI spec.interference.cl_def spec.interference.expansive
          spec.interference.idempotent(1) spec.cam.idempotent(1))

lemma closed_subseteq:
  shows "spec.interference.closed r ⊆ spec.cam.closed r"
by (metis spec.cam.closed.interference.cl spec.interference.closed_conv subsetI)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference"›

setup ‹Sign.mandatory_path "cl"›

lemma mono:
  assumes "r ⊆ r'"
  assumes "P ≤ P'"
  shows "spec.interference.cl r P ≤ spec.interference.cl r' P'"
unfolding spec.interference.cl_def
apply (strengthen ord_to_strengthen(1)[OF ‹r ⊆ r'›])
apply (strengthen ord_to_strengthen(1)[OF ‹P ≤ P'›])
apply simp
done

declare spec.interference.strengthen_cl[strg del]

lemma strengthen[strg]:
  assumes "st_ord F r r'"
  assumes "st_ord F P P'"
  shows "st_ord F (spec.interference.cl r P) (spec.interference.cl r' P')"
using assms by (cases F; simp add: spec.interference.cl.mono)

lemma bot:
  shows "spec.interference.cl r ⊥ = spec.term.none (spec.rel r :: (_, _, unit) spec)"
by (simp add: spec.interference.cl_def spec.bind.bind flip: bot_fun_def spec.bind.botR)

lemmas Sup = spec.interference.cl_Sup
lemmas sup = spec.interference.cl_sup

lemma idle:
  shows "spec.interference.cl r spec.idle = spec.term.none (spec.rel r :: (_, _, unit) spec)"
by (simp add: spec.interference.cl_def spec.cam.cl.idle spec.bind.bind spec.rel.wind_bind
        flip: spec.term.none.bind)

lemma rel_empty:
  assumes "spec.idle ≤ P"
  shows "spec.interference.cl {} P = P"
by (simp add: spec.interference.cl_def spec.rel.empty spec.cam.cl.rel_empty spec.bind.return
              spec.bind.returnL assms UNIV_unit)

lemma rel_reflcl:
  shows "spec.interference.cl (r ∪ A × Id) P = spec.interference.cl r P"
    and "spec.interference.cl (A × Id ∪ r) P = spec.interference.cl r P"
by (simp_all add: spec.interference.cl_def spec.cam.cl.rel_reflcl spec.rel.reflcl)

lemma rel_minus_Id:
  shows "spec.interference.cl (r - UNIV × Id) P = spec.interference.cl r P"
by (metis Un_Diff_cancel2 spec.interference.cl.rel_reflcl(1))

(* Inf *)

lemma inf_rel:
  shows "spec.interference.cl s P ⊓ spec.rel r = spec.interference.cl (r ∩ s) (spec.rel r ⊓ P)"
    and "spec.rel r ⊓ spec.interference.cl s P = spec.interference.cl (r ∩ s) (spec.rel r ⊓ P)"
by (simp_all add: spec.interference.cl_def spec.bind.inf_rel spec.return.inf_rel spec.cam.cl.inf_rel
            flip: spec.rel.inf)

lemma bindL:
  assumes "f ∈ spec.interference.closed r"
  shows "spec.interference.cl r (f ⤜ g) = f ⤜ (λv. spec.interference.cl r (g v))"
apply (subst (1 2) spec.interference.closed_conv[OF assms])
apply (simp add: spec.interference.cl_def spec.bind.bind spec.cam.cl.bind spec.cam.cl.rel
                 spec.cam.cl.return spec.bind.supL spec.bind.return)
apply (simp add: spec.rel.wind_bind flip: spec.bind.bind)
done

lemma bindR:
  assumes "⋀v. g v ∈ spec.interference.closed r"
  shows "spec.interference.cl r (f ⤜ g) = spec.interference.cl r f ⤜ g" (is "?lhs = ?rhs")
proof -
  from assms have "?lhs = spec.interference.cl r (f ⤜ (λv. spec.interference.cl r (g v)))"
    by (meson spec.interference.closed_conv)
  also have "… = spec.interference.cl r f ⤜ (λv. spec.interference.cl r (g v))"
    apply (simp add: spec.interference.cl_def spec.bind.bind spec.cam.cl.bind spec.cam.cl.rel
                     spec.cam.cl.return spec.bind.supL spec.bind.supR spec.bind.return
                     sup.absorb1 spec.bind.mono
               flip: spec.bind.botR)
    apply (simp add: spec.rel.wind_bind flip: spec.bind.bind)
    done
  also from assms have "… = ?rhs"
    by (simp flip: spec.interference.closed_conv)
  finally show ?thesis .
qed

lemma bind_conv:
  assumes "f ∈ spec.interference.closed r"
  assumes "∀x. g x ∈ spec.interference.closed r"
  shows "spec.interference.cl r (f ⤜ g) = f ⤜ g"
using assms by (simp add: spec.interference.cl.bindR flip: spec.interference.closed_conv)

lemma action:
  shows "spec.interference.cl r (spec.action F)
       = spec.rel r ⤜ (λ_::unit. spec.action F ⤜ (λv. spec.rel r ⤜ (λ_::unit. spec.return v)))"
by (simp add: spec.interference.cl_def spec.cam.cl.action spec.bind.supL spec.bind.supR
        flip: spec.bind.botR spec.bind.bind spec.rel.unwind_bind)
   (simp add: spec.bind.bind sup.absorb1 spec.bind.mono)

lemma return:
  shows "spec.interference.cl r (spec.return v) = spec.rel r ⤜ (λ_::unit. spec.return v)"
by (simp add: spec.return_def spec.interference.cl.action spec.bind.bind)
   (simp add: spec.bind.return spec.rel.wind_bind flip: spec.return_def spec.bind.bind)

lemma bind_return:
  shows "spec.interference.cl r (f ⪢ spec.return v) = spec.interference.cl r f ⪢ spec.return v"
by (simp add: spec.interference.cl_def spec.bind.bind spec.bind.return spec.cam.cl.bind_return)

lemma rel: ―‹ complicated by polymorphic \<^const>‹spec.rel› ›
  assumes "r ⊆ r' ∨ r' ⊆ r"
  shows "spec.interference.cl r (spec.rel r') = spec.rel (r ∪ r')" (is "?lhs = ?rhs")
using assms
proof
  show ?thesis if "r ⊆ r'"
    apply (simp add: ‹r ⊆ r'› sup.absorb2 spec.eq_iff spec.interference.expansive)
    apply (strengthen ord_to_strengthen(1)[OF ‹r ⊆ r'›])
    apply (metis spec.interference.cl.bot spec.interference.idempotent(1) spec.term.all.rel
                 spec.term.all_none spec.term.none.interference.all.cl_le)
    done
  show ?thesis if "r' ⊆ r"
  proof(rule antisym)
    from ‹r' ⊆ r› show "?lhs ≤ ?rhs"
      by (simp add: inf.absorb_iff1 spec.interference.cl.inf_rel flip: spec.rel.inf)
    from ‹r' ⊆ r› show "?rhs ≤ ?lhs"
      by (simp add: sup.absorb1 spec.interference.cl_def spec.cam.cl_def
            spec.rel.wind_bind_trailing le_supI1  spec.bind.supR spec.bind.return
            order.trans[OF _ spec.bind.mono[OF order.refl spec.bind.mono[OF spec.return.rel_le order.refl]]])
  qed
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "idle.interference"›

lemma cl_le[spec.idle_le]:
  shows "spec.idle ≤ spec.interference.cl r P"
by (simp add: spec.interference.cl_def spec.idle_le)

lemma closed_le[spec.idle_le]:
  assumes "P ∈ spec.interference.closed r"
  shows "spec.idle ≤ P"
by (subst spec.interference.closed_conv[OF assms]) (simp add: spec.idle.interference.cl_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "map.interference"›

lemma cl_sf_id:
  shows "spec.map af id vf (spec.interference.cl r P)
       = spec.interference.cl (map_prod af id ` r) (spec.map af id vf P)"
apply (simp add: spec.interference.cl_def spec.map.return
                 spec.map.bind_inj_sf[OF inj_on_id] spec.map.cam.cl_inj_sf[OF inj_on_id])
apply (subst (1 2) spec.map.rel, force, force)
apply (simp add: spec.vmap.eq_return(2) spec.bind.bind
                 spec.bind.returnL spec.idle_le
           flip: spec.map.cam.cl_inj_sf[where af=id and sf=id and vf=vf and P="spec.amap af P",
                                        simplified spec.map.comp, simplified, folded id_def])
done

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap.interference"›

lemma cl:
  fixes as :: "'b set"
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  fixes r :: "('b, 't) steps"
  fixes P :: "('b, 't, 'w) spec"
  shows "spec.invmap af sf vf (spec.interference.cl r P)
       = spec.interference.cl (map_prod af (map_prod sf sf) -` (r ∪ UNIV × Id)) (spec.invmap af sf vf P)"
apply (simp add: spec.interference.cl_def map_prod_vimage_Times spec.rel.wind_bind_trailing
                 spec.invmap.bind spec.invmap.cam.cl spec.invmap.rel spec.invmap.return
           flip: spec.bind.bind)
apply (subst (2) spec.invmap.split_vinvmap)
apply (simp add: spec.cam.cl.bind spec.cam.cl.return spec.cam.cl.Sup spec.term.none.cam.cl_rel_wind
                 spec.bind.mono spec.bind.bind spec.bind.SupL spec.bind.supL
                 spec.bind.SUPR spec.bind.supR spec.bind.returnL spec.idle_le spec.bind.botR
                 image_image sup.absorb1)
done

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference.closed"›

lemma antimonotone:
  shows "antimono spec.interference.closed"
proof(rule antimonoI)
  show "spec.interference.closed r' ⊆ spec.interference.closed r" if "r ⊆ r'" for r r' :: "('a, 's) steps"
    unfolding spec.interference.closed_def by (strengthen ord_to_strengthen(2)[OF ‹r ⊆ r'›]) simp
qed

lemmas strengthen[strg] = st_ord_antimono[OF spec.interference.closed.antimonotone]
lemmas antimono = antimonoD[OF spec.interference.closed.antimonotone]

lemma Sup':
  assumes "X ⊆ spec.interference.closed r"
  shows "⨆X ⊔ spec.term.none (spec.rel r :: (_, _, unit) spec) ∈ spec.interference.closed r"
by (metis assms spec.interference.cl.bot spec.interference.closed_Sup)

lemma Sup_not_empty:
  assumes "X ⊆ spec.interference.closed r"
  assumes "X ≠ {}"
  shows "⨆X ∈ spec.interference.closed r"
using spec.interference.closed_Sup[OF assms(1)] assms
by (simp add: assms spec.interference.closed_Sup[OF assms(1)] less_eq_Sup spec.interference.least
              subsetD sup.absorb1)

lemma rel:
  assumes "r' ⊆ r"
  shows "spec.rel r ∈ spec.interference.closed r'"
by (metis assms spec.eq_iff inf.absorb_iff2 spec.interference.cl.inf_rel(2) spec.interference.closed_clI)

lemma bind_relL:
  fixes P :: "('a, 's, 'v) spec"
  assumes "P ∈ spec.interference.closed r"
  shows "spec.rel r ⤜ (λ_::unit. P) = P"
by (subst (1 2) spec.interference.closed_conv[OF assms])
   (simp add: spec.interference.cl_def spec.rel.wind_bind flip: spec.bind.bind)

lemma bind_relR:
  assumes "P ∈ spec.interference.closed r"
  shows "P ⤜ (λv. spec.rel r ⤜ (λ_::unit. Q v)) = P ⤜ Q"
by (subst (1 2) spec.interference.closed_conv[OF assms])
   (simp add: spec.interference.cl_def spec.bind.bind spec.bind.return;
    simp add: spec.rel.wind_bind flip: spec.bind.bind)

lemma bind_rel_unitR:
  assumes "P ∈ spec.interference.closed r"
  shows "P ⪢ (spec.rel r :: (_, _, unit) spec) = P"
by (subst (1 2) spec.interference.closed_conv[OF assms])
   (simp add: spec.interference.cl_def spec.bind.bind spec.rel.wind_bind)

lemma bind_rel_botR:
  assumes "P ∈ spec.interference.closed r"
  shows "P ⤜ (λv. spec.rel r ⤜ (λ_::unit. ⊥)) = P ⤜ ⊥"
by (subst (1 2) spec.interference.closed_conv[OF assms])
   (simp add: spec.interference.cl_def spec.bind.bind spec.bind.return;
    simp add: spec.rel.wind_bind flip: spec.bind.bind)

lemma bind[intro]:
  fixes f :: "('a, 's, 'v) spec"
  fixes g :: "'v ⇒ ('a, 's, 'w) spec"
  assumes "f ∈ spec.interference.closed r"
  assumes "⋀x. g x ∈ spec.interference.closed r"
  shows "(f ⤜ g) ∈ spec.interference.closed r"
using assms by (simp add: spec.interference.closed_clI spec.interference.cl.bindL
                    flip: spec.interference.closed_conv)

lemma kleene_star:
  assumes "P ∈ spec.interference.closed r"
  assumes "spec.return () ≤ P"
  shows "spec.kleene.star P ∈ spec.interference.closed r"
proof(rule spec.interference.closed_clI,
      induct rule: spec.kleene.star.fixp_induct[where P="λR. spec.interference.cl r (R P) ≤ spec.kleene.star P ", case_names adm bot step])
  case bot from ‹P ∈ spec.interference.closed r› show ?case
    by (simp add: order.trans[OF _ spec.kleene.expansive_star] spec.interference.cl.bot
                  spec.term.none.interference.closed.rel_le)
next
  case (step R) show ?case
    apply (simp add: spec.interference.cl_sup spec.interference.cl.bindL[OF assms(1)])
    apply (strengthen ord_to_strengthen(1)[OF step])
    apply (strengthen ord_to_strengthen(1)[OF ‹spec.return () ≤ P›])
    apply (simp add: spec.kleene.fold_starL spec.kleene.expansive_star
               flip: spec.interference.closed_conv[OF assms(1)])
    done
qed simp_all

lemma map_sf_id:
  fixes af :: "'a ⇒ 'b"
  fixes vf :: "'v ⇒ 'w"
  assumes "P ∈ spec.interference.closed r"
  shows "spec.map af id vf P ∈ spec.interference.closed (map_prod af id ` r)"
by (rule spec.interference.closed_clI)
   (subst (2) spec.interference.closed_conv[OF assms];
    simp add: spec.map.interference.cl_sf_id map_prod_image_Times)

lemma invmap:
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  assumes "P ∈ spec.interference.closed r"
  shows "spec.invmap af sf vf P ∈ spec.interference.closed (map_prod af (map_prod sf sf) -` r)"
by (rule spec.interference.closed_clI)
   (subst (2) spec.interference.closed_conv[OF assms];
    fastforce simp: spec.invmap.interference.cl intro: spec.interference.cl.mono)

setup ‹Sign.mandatory_path "term"›

lemma none:
  assumes "P ∈ spec.interference.closed r"
  shows "spec.term.none P ∈ spec.interference.closed r"
by (rule spec.interference.closed_clI)
   (subst (2) spec.interference.closed_conv[OF assms];
    simp add: spec.term.none.interference.cl)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ The ∗‹'a agent› datatype ›

text‹

For compositionality we often wish to designate a specific agent as the environment.

›

datatype 'a agent = proc (the_agent: 'a) | env
type_synonym sequential = "unit agent" ―‹ Sequential programs (\S\ref{sec:programs}) ›
abbreviation self :: sequential where "self ≡ proc ()"

declare agent.map_id[simp]
declare agent.map_id0[simp]
declare agent.map_id0[unfolded id_def, simp]
declare agent.map_comp[unfolded comp_def, simp]

lemma env_not_in_range_proc[iff]:
  shows "env ∉ range proc"
by fastforce

lemma range_proc_conv[simp]:
  shows "x ∈ range proc ⟷ x ≠ env"
by (cases x) simp_all

lemma inj_proc[iff]:
  shows "inj proc"
by (simp add: inj_def)

lemma surj_the_inv_proc[iff]:
  shows "surj (the_inv proc)"
by (meson inj_proc surjI the_inv_f_f)

lemma the_inv_proc[simp]:
  shows "the_inv proc (proc a) = a"
by (simp add: the_inv_f_f)

lemma uminus_env_range_proc[simp]:
  shows "-{env} = range proc"
by (auto intro: agent.exhaust)

lemma env_range_proc_UNIV[simp]:
  shows "insert env (range proc) = UNIV"
by (auto intro: agent.exhaust)

setup ‹Sign.mandatory_path "sequential"›

lemma not_conv[simp]:
  shows "a ≠ env ⟷ a = self"
    and "a ≠ self ⟷ a = env"
by (cases a; simp)+

lemma range_proc_self[simp]:
  shows "range proc = {self}"
by fastforce

lemma UNIV:
  shows "UNIV = {env, self}"
by fastforce

lemma rev_UNIV[simp]:
  shows "{env, self} = UNIV"
    and "{self, env} = UNIV"
by fastforce+

lemma uminus_self_env[simp]:
  shows "-{self} = {env}"
by fastforce

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "map_agent"›

lemma eq_conv:
  shows "map_agent f x = env ⟷ x = env"
    and "env = map_agent f x ⟷ x = env"
    and "map_agent f x = proc a ⟷ (∃a'. x = proc a' ∧ a = f a')"
    and "proc a = map_agent f x ⟷ (∃a'. x = proc a' ∧ a = f a')"
by (cases x; auto)+

lemma surj:
  fixes π :: "'a ⇒ 'b"
  assumes "surj π"
  shows "surj (map_agent π)"
  by (metis assms surj_def agent.exhaust agent.map(1,2))

lemma bij:
  fixes π :: "'a ⇒ 'b"
  assumes "bij π"
  shows "bij (map_agent π)"
by (rule bijI[OF agent.inj_map[OF bij_is_inj[OF assms]] map_agent.surj[OF bij_is_surj[OF assms]]])

setup ‹Sign.parent_path›

definition swap_env_self_fn :: "sequential ⇒ sequential" where
  "swap_env_self_fn a = (case a of proc () ⇒ env | env ⇒ self)"

lemma swap_env_self_fn_simps:
  shows "swap_env_self_fn self = env"
        "swap_env_self_fn env = self"
unfolding swap_env_self_fn_def by simp_all

lemma bij_swap_env_self_fn:
  shows "bij swap_env_self_fn"
unfolding swap_env_self_fn_def bij_def inj_def surj_def by (auto split: agent.split)

lemma swap_env_self_fn_vimage_singleton:
  shows "swap_env_self_fn -` {env} = {self}"
    and "swap_env_self_fn -` {self} = {env}"
unfolding swap_env_self_fn_def by (auto split: agent.splits)

setup ‹Sign.mandatory_path "spec"›

abbreviation swap_env_self :: "(sequential, 's, 'v) spec ⇒ (sequential, 's, 'v) spec" where
  "swap_env_self ≡ spec.amap swap_env_self_fn"

setup ‹Sign.parent_path›


subsection‹ Parallel composition\label{sec:constructions-parallel_composition} ›

text‹

We compose a collection of programs \<^typ>‹(sequential, 's, 'v) spec› in parallel by mapping
these into the \<^typ>‹('a agent, 's, 'v) spec› lattice, taking the infimum, and mapping back.

›

definition toConcurrent_fn :: "'a ⇒ 'a ⇒ sequential" where
  "toConcurrent_fn = (λa a'. if a' = a then self else env)"

definition toSequential_fn :: "'a agent ⇒ sequential" where
  "toSequential_fn = map_agent ⟨()⟩"

lemma toSequential_fn_alt_def:
  shows "toSequential_fn = (λx. case x of proc x ⇒ self | env ⇒ env)"
by (simp add: toSequential_fn_def fun_eq_iff split: agent.split)

setup ‹Sign.mandatory_path "spec"›

abbreviation toConcurrent :: "'a ⇒ (sequential, 's, 'v) spec ⇒ ('a agent, 's, 'v) spec" where
  "toConcurrent a ≡ spec.ainvmap (toConcurrent_fn (proc a))"

abbreviation toSequential :: "('a agent, 's, 'v) spec ⇒ (sequential, 's, 'v) spec" where
  "toSequential ≡ spec.amap toSequential_fn"

definition Parallel :: "'a set ⇒ ('a ⇒ (sequential, 's, unit) spec) ⇒ (sequential, 's, unit) spec" where
  "Parallel as Ps = spec.toSequential (spec.rel (insert env (proc ` as) × UNIV) ⊓ (⨅a∈as. spec.toConcurrent a (Ps a)))"

definition parallel :: "(sequential, 's, unit) spec ⇒ (sequential, 's, unit) spec ⇒ (sequential, 's, unit) spec" where
  "parallel P Q = spec.Parallel UNIV (λa::bool. if a then P else Q)"

adhoc_overloading
  Parallel spec.Parallel
adhoc_overloading
  parallel spec.parallel

lemma parallel_alt_def:
  shows "spec.parallel P Q = spec.toSequential (spec.toConcurrent True P ⊓ spec.toConcurrent False Q)"
by (simp add: spec.parallel_def spec.Parallel_def INF_UNIV_bool_expand spec.rel.UNIV)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "toConcurrent_fn"›

lemma simps[simp]:
  shows "toConcurrent_fn (proc a) (proc a) = self"
    and "toConcurrent_fn (proc a) env = env"
    and "toConcurrent_fn a' a'' = self ⟷ a'' = a'"
    and "self = toConcurrent_fn a' a'' ⟷ a'' = a'"
    and "toConcurrent_fn a' a'' = env ⟷ a'' ≠ a'"
    and "env = toConcurrent_fn a' a'' ⟷ a'' ≠ a'"
    and "toConcurrent_fn (proc a) (map_agent ⟨a⟩ x) = map_agent ⟨()⟩ x"
by (auto simp: toConcurrent_fn_def map_agent.eq_conv intro: agent.exhaust)

lemma inj_map_agent:
  assumes "inj_on f (insert x (set_agent a))"
  shows "toConcurrent_fn (proc (f x)) (map_agent f a) = toConcurrent_fn (proc x) a"
by (cases a) (auto simp: toConcurrent_fn_def intro: inj_onD[OF assms])

lemma inv_into_map_agent:
  fixes f :: "'a ⇒ 'b"
  fixes a :: "'b agent"
  fixes x :: "'a"
  assumes "inj_on f as"
  assumes "x ∈ as"
  assumes "a ∈ insert env ((λx. proc (f x)) ` as)"
  shows "toConcurrent_fn (proc x) (map_agent (inv_into as f) a) = toConcurrent_fn (proc (f x)) a"
using assms by (auto simp: toConcurrent_fn_def)

lemma vimage_sequential[simp]:
  shows "toConcurrent_fn (proc a) -` {self} = {proc a}"
    and "toConcurrent_fn (proc a) -` {env} = -{proc a}"
by (auto simp: toConcurrent_fn_def split: if_splits)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "toSequential_fn"›

lemma simps[simp]:
  shows "toSequential_fn env = env"
    and "toSequential_fn (proc x) = self"
    and "toSequential_fn (map_agent f a) = toSequential_fn a"
    and "trace.map toSequential_fn id id σ = σ"
    and "trace.map toSequential_fn (λx. x) (λx. x) σ = σ"
    and "(λx. if x = self then self else env) = id"
by (simp_all add: toSequential_fn_def fun_unit_id[where f="λx. ()"] fun_eq_iff flip: id_def)

lemma eq_conv:
  shows "toSequential_fn x = env ⟷ x = env"
    and "toSequential_fn x = self ⟷ (∃a. x = proc a)"
by (simp_all add: toSequential_fn_def map_agent.eq_conv)

lemma surj:
  shows "surj toSequential_fn"
proof -
  have "x ∈ range toSequential_fn" for x
    by (cases x)
       (simp_all add: toSequential_fn_def range_eqI[where x="proc undefined"] range_eqI[where x="env"])
  then show ?thesis by blast
qed

lemma image[simp]:
  assumes "as ≠ {}"
  shows "toSequential_fn ` proc ` as = {self}"
using assms by (auto simp: toSequential_fn_def image_image)

lemma vimage_sequential[simp]:
  shows "toSequential_fn -` {env} = {env}"
    and "toSequential_fn -` {self} = range proc"
by (auto simp: toSequential_fn_def map_agent.eq_conv)

setup ‹Sign.parent_path›

lemma toSequential_fn_eq_toConcurrent_fn_conv:
  shows "toSequential_fn a = toConcurrent_fn a' a'' ⟷ (case a of env ⇒ a'' ≠ a' | proc _ ⇒ a'' = a')"
    and "toConcurrent_fn a' a'' = toSequential_fn a ⟷ (case a of env ⇒ a'' ≠ a' | proc _ ⇒ a'' = a')"
by (simp_all split: agent.split)

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "toSequential"›

lemma interference:
  shows "spec.toSequential (spec.rel ({env} × r)) = spec.rel ({env} × r)"
by (simp add: spec.map.rel map_prod_image_Times)

lemma interference_inf_toConcurrent:
  fixes a :: "'a"
  fixes P :: "(sequential, 's, 'v) spec"
  shows "spec.toSequential (spec.rel ({env, proc a} × UNIV) ⊓ spec.toConcurrent a P) = P" (is "?lhs = ?rhs")
    and "spec.toSequential (spec.toConcurrent a P ⊓ spec.rel ({env, proc a} × UNIV)) = P" (is ?thesis1)
proof -
  show "?lhs = ?rhs"
  proof(rule spec.singleton.antisym)
    have *: "trace.natural' s (map (map_prod toSequential_fn id) xs)
           = trace.natural' s (map (map_prod (toConcurrent_fn (proc a)) id) xs)"
         if "trace.steps' s xs ⊆ {env, proc a} × UNIV"
        for s and xs :: "('a agent × 's) list"
      using that by (induct xs arbitrary: s) auto
    show "⦉σ⦊ ≤ ?rhs" if "⦉σ⦊ ≤ ?lhs" for σ
      using that
      by (force simp: spec.singleton.le_conv spec.singleton_le_conv trace.natural_def *
                elim: order.trans[rotated])
    show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
      using that
      by (clarsimp intro!: exI[where x="trace.map (map_agent ⟨a⟩) id id σ"]
                     simp: spec.singleton.le_conv trace.steps'.map map_agent.eq_conv
                           fun_unit_id[where f="λ_::unit. ()"]
                simp flip: id_def)
  qed
  then show ?thesis1
    by (simp add: ac_simps)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "toConcurrent"›

lemma interference:
  shows "spec.toConcurrent a (spec.rel ({env} × UNIV)) = spec.rel ((- {proc a}) × UNIV)"
by (simp add: spec.invmap.rel map_prod_vimage_Times spec.rel.reflcl)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "idle"›

lemma Parallel_le[spec.idle_le]:
  assumes "⋀a. a ∈ as ⟹ spec.idle ≤ Ps a"
  shows "spec.idle ≤ spec.Parallel as Ps"
apply (simp add: spec.Parallel_def)
apply (strengthen ord_to_strengthen(2)[OF assms], assumption)
apply (strengthen ord_to_strengthen(2)[OF spec.idle.invmap_le[OF order.refl]])
apply (simp add: le_INF_iff spec.idle_le)
done

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "Parallel"›

lemma cong:
  assumes "as = as'"
  assumes "⋀a. a ∈ as' ⟹ Ps a = Ps' a"
  shows "spec.Parallel as Ps = spec.Parallel as' Ps'"
unfolding spec.Parallel_def using assms by simp

lemma no_agents:
  shows "spec.Parallel {} Ps = spec.rel ({env} × UNIV)"
by (simp add: spec.Parallel_def spec.toSequential.interference)

lemma singleton_agents:
  shows "spec.Parallel {a} Ps = Ps a"
by (simp add: spec.Parallel_def spec.toSequential.interference_inf_toConcurrent)

lemma bot:
  assumes "Ps a = ⊥"
  assumes "a ∈ as"
  shows "spec.Parallel as Ps = ⊥"
by (simp add: spec.Parallel_def assms INF_unwind_index[of a] spec.invmap.bot spec.map.bot)

lemma top:
  shows "spec.Parallel as ⊤ = (if as = {} then spec.rel ({env} × UNIV) else ⊤)"
proof -
  have "spec.toSequential (spec.rel (insert env (proc ` as) × UNIV)) = ⊤" if "as ≠ {}"
    using that by (subst spec.map.rel, force, simp add: map_prod_image_Times flip: spec.rel.UNIV)
  then show ?thesis
    by (simp add: spec.Parallel.no_agents) (auto simp: spec.Parallel_def spec.invmap.top)
qed

lemma mono:
  assumes "⋀a. a ∈ as ⟹ Ps a ≤ Ps' a"
  shows "spec.Parallel as Ps ≤ spec.Parallel as Ps'"
unfolding spec.Parallel_def by (strengthen ord_to_strengthen(1)[OF assms(1)]; simp)

lemma strengthen[strg]:
  assumes "⋀a. a ∈ as ⟹ st_ord F (Ps a) (Ps' a)"
  shows "st_ord F (spec.Parallel as Ps) (spec.Parallel as Ps')"
using assms by (cases F) (auto simp: spec.Parallel.mono)

lemma mono2mono[cont_intro, partial_function_mono]:
  fixes Ps :: "'a ⇒ 'b ⇒ (sequential, 's, unit) spec"
  assumes "⋀a. a ∈ as ⟹ monotone orda (≤) (Ps a)"
  shows "monotone orda (≤) (λx::'b. spec.Parallel as (λa. Ps a x))"
using spec.Parallel.mono assms unfolding monotone_def by meson

(* Sup, mcont *)

lemma invmap: ―‹ ‹af = id› in ‹spec.invmap› ›
  shows "spec.invmap id sf vf (spec.Parallel UNIV Ps) = spec.Parallel UNIV (spec.invmap id sf vf ∘ Ps)"
by (simp add: spec.Parallel_def image_image spec.invmap.inf spec.invmap.Inf spec.invmap.comp spec.rel.UNIV
        flip: spec.amap.surj_invmap[OF toSequential_fn.surj])

lemma discard_interference:
  assumes "⋀a. a ∈ bs ⟹ Ps a = spec.rel ({env} × UNIV)"
  shows "spec.Parallel as Ps = spec.Parallel (as - bs) Ps"
proof -
  have *: "as = (as - bs) ∪ (as ∩ bs)" by blast
  have **: "(insert env (proc ` as) ∩ - proc ` (as ∩ bs)) = insert env (proc ` (as - bs))" by blast
  from assms have ***: "(⨅a∈as ∩ bs. spec.toConcurrent a (Ps a))
                      = spec.rel ((- proc ` (as ∩ bs)) × UNIV)"
    by (force simp: assms spec.toConcurrent.interference le_Inf_iff
         simp flip: spec.rel.INF
             intro: spec.rel.mono antisym)
  show ?thesis
    apply (simp add: spec.Parallel_def)
    apply (subst (2) *)
    apply (simp add: image_Un Inf_union_distrib ac_simps ** *** Times_Int_Times
               flip: spec.rel.inf inf.assoc)
    done
qed

lemma rename_UNIV_aux:
  fixes f :: "'a ⇒ 'b"
  assumes "inj_on f as"
  shows "spec.toSequential (spec.rel (insert env (proc ` as) × UNIV)
           ⊓ (⨅a∈as. spec.toConcurrent a (Ps a)))
       = spec.toSequential (spec.rel (insert env (proc ` f ` as) × UNIV)
           ⊓ (⨅a∈as. spec.toConcurrent (f a) (Ps a)))" (is "?lhs = ?rhs")
proof(rule spec.singleton.antisym)
  show "⦉σ⦊ ≤ ?rhs" if "⦉σ⦊ ≤ ?lhs" for σ
    using that assms
    apply (clarsimp simp: spec.singleton.le_conv le_Inf_iff)
    apply (rule exI[where x="trace.map (map_agent f) id id σ" for σ])
    apply (intro conjI)
      apply (fastforce simp: trace.steps'.map)
     apply (fastforce intro: ord_eq_le_trans[OF spec.singleton.map_cong[OF toConcurrent_fn.inj_map_agent refl refl refl]]
                       dest: inj_onD trace.steps'.asetD
                  simp flip: id_def)
    apply (fastforce simp flip: id_def)
    done
  show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
    using that assms
    apply (clarsimp simp: spec.singleton.le_conv le_Inf_iff image_image)
    apply (rule exI[where x="trace.map (map_agent (inv_into as f)) id id σ" for σ])
    apply (auto 4 2 dest: trace.steps'.asetD
                simp: spec.singleton.map_cong[OF toConcurrent_fn.inv_into_map_agent refl refl refl]
                      comp_def trace.steps'.map
           simp flip: id_def)
    done
qed

lemma rename_UNIV: ―‹ expand the set of agents to ‹UNIV› ›
  fixes f :: "'a ⇒ 'b"
  assumes "inj_on f as"
  shows "spec.Parallel as Ps
       = spec.Parallel (UNIV :: 'b set)
                       (λb. if b ∈ f ` as then Ps (inv_into as f b) else spec.rel ({env} × UNIV))"
(is "?lhs = spec.Parallel _ ?f")
proof -
  have *: "(⨅x. spec.toConcurrent x (?f x))
         = spec.rel (insert env (proc ` f ` as) × UNIV)
            ⊓ (⨅x∈f ` as. spec.toConcurrent x (Ps (inv_into as f x)))"
  proof -
    have *: "(⋂x∈- f ` as. (- {proc x}) × UNIV) = insert env (proc ` f ` as) × UNIV"
      by (auto intro: agent.exhaust)
    have "(⨅x. spec.toConcurrent x (?f x))
        = (⨅x∈f ` as. spec.toConcurrent x (?f x)) ⊓ (⨅x∈-f ` as. spec.toConcurrent x (?f x))"
      by (subst INF_union[symmetric]) simp
    also have "… = spec.rel (insert env (proc ` f ` as) × UNIV)
                    ⊓ (⨅x∈f ` as. spec.toConcurrent x (Ps (inv_into as f x)))"
      by (simp add: ac_simps spec.invmap.rel map_prod_vimage_Times spec.rel.reflcl *
              flip: spec.rel.upper_INF)
    finally show ?thesis .
  qed
  show ?thesis
    by (simp add: spec.Parallel_def * inv_into_f_f[OF assms] spec.rel.UNIV
                  INF_rename_bij[OF inj_on_imp_bij_betw[OF assms],
                             where F="λ_ x. spec.toConcurrent x (Ps (inv_into as f x))"]
                  spec.Parallel.rename_UNIV_aux[OF assms])
qed

lemma rename:
  fixes π :: "'a ⇒ 'b"
  fixes Ps :: "'b ⇒ (sequential, 's, unit) spec"
  assumes "bij_betw π as bs"
  shows "spec.Parallel as (Ps ∘ π) = spec.Parallel bs Ps"
proof -
  define π' where "π' = (λx::'a+'b. case x of
                  Inl a ⇒ if a ∈ as then Inr (π a) else Inl a
                | Inr b ⇒ if b ∈ bs then Inl (inv_into as π b) else Inr b)"
  from assms have "inj π'"
    by (force intro: injI
               simp: π'_def bij_betw_apply bij_betw_imp_surj_on inv_into_into
              split: sum.split_asm if_split_asm
               dest: bij_betw_inv_into_left[rotated] bij_betw_inv_into_right[rotated])
  have simps: "⋀a. π' (Inl a) = (if a ∈ as then Inr (π a) else Inl a)"
              "⋀b. π' (Inr b) = (if b ∈ bs then Inl (inv_into as π b) else Inr b)"
    by (simp_all add: π'_def)
  have inv_simps: "⋀a. a ∈ as ⟹ inv π' (Inl a) = Inr (π a)"
    by (simp add: inv_f_eq[OF ‹inj π'›] bij_betw_inv_into_left[OF assms] bij_betw_apply[OF assms] simps(2))
  show ?thesis
    apply (simp add: spec.Parallel.rename_UNIV[where as=as and f="Inl :: 'a ⇒ 'a + 'b"]
                     spec.Parallel.rename_UNIV[where as=bs and f="Inr :: 'b ⇒ 'a + 'b"] comp_def)
    apply (subst (2) spec.Parallel.rename_UNIV[where as=UNIV, OF ‹inj π'›])
    apply (fastforce intro: arg_cong[where f="spec.Parallel UNIV"]
                      simp: fun_eq_iff split_sum_all image_iff simps inv_simps
                      inv_f_f[OF ‹inj π'›]  bij_betw_apply[OF bij_betw_inv_into[OF assms]]
                      bij_betw_apply[OF assms] bij_betw_inv_into_left[OF assms])
    done
qed

lemma rename_cong:
  fixes π :: "'a ⇒ 'b"
  fixes Ps :: "'a ⇒ (_, _, _) spec"
  fixes Ps' :: "'b ⇒ (_, _, _) spec"
  assumes "bij_betw π as bs"
  assumes "⋀a. a ∈ as ⟹ Ps a = Ps' (π a)"
  shows "spec.Parallel as Ps = spec.Parallel bs Ps'"
by (simp add: assms(2) flip: spec.Parallel.rename[OF assms(1)] cong: spec.Parallel.cong)

lemma inf_pre:
  assumes "as ≠ {}"
  shows "spec.Parallel as Ps ⊓ spec.pre P = (‖i∈as. Ps i ⊓ spec.pre P)" (is ?thesis1)
    and "spec.pre P ⊓ spec.Parallel as Ps = (‖i∈as. spec.pre P ⊓ Ps i)" (is ?thesis2)
proof -
  show ?thesis1
    by (simp add: spec.Parallel_def assms spec.invmap.inf spec.invmap.pre spec.map.inf_distr
                  inf.assoc INF_inf_const2)
  then show ?thesis2
    by (simp add: ac_simps)
qed

lemma inf_post:
  assumes "as ≠ {}"
  shows "spec.Parallel as Ps ⊓ spec.post Q = spec.Parallel as (λi. Ps i ⊓ spec.post Q)" (is ?thesis1)
    and "spec.post Q ⊓ spec.Parallel as Ps = spec.Parallel as (λi. spec.post Q ⊓ Ps i)" (is ?thesis2)
proof -
  show ?thesis1
    by (simp add: spec.Parallel_def assms spec.invmap.inf spec.invmap.post spec.map.inf_distr
                  inf.assoc INF_inf_const2)
  then show ?thesis2
    by (simp add: ac_simps)
qed

lemma unwind:
    ―‹ All other processes begin with interference ›
  assumes b: "⋀b. b ∈ as - {a} ⟹ spec.rel ({env} × UNIV) ⤜ (λ_::unit. Ps b) ≤ Ps b"
  assumes a: "f ⤜ g ≤ Ps a" ―‹ The selected process starts with ‹f› ›
  assumes "a ∈ as"
  shows "f ⤜ (λv. spec.Parallel as (Ps(a := g v))) ≤ spec.Parallel as Ps"
proof -
  have *: "spec.toConcurrent a f ⊓ spec.rel (⋂x∈as - {a}. (- {proc x}) × UNIV)
            ⤜ (λv. ⨅b∈as. spec.toConcurrent b ((Ps(a:=g v)) b))
        ≤ (⨅a∈as. spec.toConcurrent a (Ps a))" (is "?lhs ≤ ?rhs")
  proof -
    from ‹a ∈ as›
    have "?lhs = spec.toConcurrent a f ⊓ spec.rel (⋂x∈as - {a}. (- {proc x}) × UNIV)
                    ⤜ (λv. spec.toConcurrent a (g v) ⊓ (⨅b∈as - {a}. spec.toConcurrent b (Ps b)))"
      by (simp add: INF_unwind_index)
    also have "… ≤ (spec.toConcurrent a f ⤜ (λx. spec.toConcurrent a (g x)))
                        ⊓ (spec.rel (⋂x∈as - {a}. (- {proc x}) × UNIV)
                             ⤜ (λ_::unit. ⨅b∈as - {a}. spec.toConcurrent b (Ps b)))"
      by (strengthen ord_to_strengthen(2)[OF spec.bind.inf_rel_distr_le]) simp
    also have "… = (spec.toConcurrent a f ⤜ (λx. spec.toConcurrent a (g x)))
                        ⊓ ((⨅b∈as - {a}. spec.toConcurrent b (spec.rel ({env} × UNIV)))
                             ⤜ (λ_::unit. ⨅b∈as - {a}. spec.toConcurrent b (Ps b)))"
      by (simp add: spec.invmap.rel map_prod_vimage_Times spec.rel.reflcl flip: spec.rel.INF)
    also have "… ≤ (spec.toConcurrent a f ⤜ (λx. spec.toConcurrent a (g x)))
                        ⊓ (⨅b∈as - {a}. spec.toConcurrent b (spec.rel ({env} × UNIV))
                             ⤜ (λ_::unit. spec.toConcurrent b (Ps b)))"
      by (strengthen ord_to_strengthen(2)[OF spec.bind.Inf_le]) simp
    also have "… = spec.toConcurrent a (f ⤜ g)
                        ⊓ (⨅b∈as - {a}. spec.toConcurrent b (spec.rel ({env} × UNIV) ⤜ (λ_::unit. Ps b)))"
      by (simp add: spec.invmap.bind)
    also have "… ≤ spec.toConcurrent a (Ps a) ⊓ (⨅b∈as - {a}. spec.toConcurrent b (Ps b))"
      by (strengthen ord_to_strengthen(2)[OF a], strengthen ord_to_strengthen(2)[OF b], assumption, rule order.refl)
    also from ‹a ∈ as› have "… = ?rhs" by (simp add: INF_unwind_index)
    finally show ?thesis .
  qed
  from ‹a ∈ as›
  have **: "(insert env (proc ` as) × UNIV ∩ (⋂x∈as - {a}. (- {proc x}) × UNIV)) = {env, proc a} × UNIV"
    by blast
  show ?thesis
    unfolding spec.Parallel_def
    by (strengthen ord_to_strengthen(2)[OF *])
       (simp add: ac_simps spec.bind.inf_rel spec.map.bind_inj_sf **
                  spec.toSequential.interference_inf_toConcurrent
            flip: spec.rel.inf)
qed

lemma inf_rel:
  fixes as :: "'a set"
  fixes r :: "'s rel"
  shows "spec.rel ({env} × UNIV ∪ {self} × r) ⊓ spec.Parallel as Ps
       = spec.Parallel as (λa. spec.rel ({env} × UNIV ∪ {self} × r) ⊓ Ps a)" (is "?lhs = ?rhs")
    and "spec.Parallel as Ps ⊓ spec.rel ({env} × UNIV ∪ {self} × r)
       = spec.Parallel as (λa. Ps a ⊓ spec.rel ({env} × UNIV ∪ {self} × r))" (is ?thesis1)
proof -
  show "?lhs = ?rhs"
  proof(cases "as = {}")
    case True then show ?thesis
      by (simp add: spec.Parallel.no_agents flip: spec.rel.inf)
  next
    case False show ?thesis
  proof(rule antisym)
    have *: "insert env (proc ` as) × UNIV ∩ map_prod toSequential_fn id -` (UNIV × Id ∪ ({env} × UNIV ∪ {self} × r))
          ⊆ insert env (proc ` as) × UNIV ∩ map_prod (toConcurrent_fn (proc a)) id -` (UNIV × Id ∪ (({env} × UNIV) ∪ {self} × r))" for a
      by auto
    from False
    show "?lhs ≤ ?rhs"
      apply (simp add: spec.Parallel_def ac_simps spec.map.inf_rel
                 flip: spec.rel.inf spec.invmap.inf_rel INF_inf_const1 INF_inf_const2
                  del: vimage_Un)
      apply (strengthen ord_to_strengthen(1)[OF *])
      apply (rule order.refl)
      done
    have "spec.toSequential (⨅x∈as. spec.toConcurrent x (Ps x) ⊓ spec.rel (insert env (proc ` as) × UNIV ∩ map_prod (toConcurrent_fn (proc x)) id -` (UNIV × Id ∪ ({env} × UNIV ∪ {self} × r))))
       ≤ spec.toSequential (⨅x∈as. spec.toConcurrent x (Ps x) ⊓ spec.rel (insert env (proc ` as) × UNIV ∩ map_prod toSequential_fn id -` (UNIV × Id ∪ ({env} × UNIV ∪ {self} × r))))"
      apply (rule spec.singleton_le_extI)
      apply (clarsimp simp: spec.singleton.le_conv le_INF_iff)
      apply (rename_tac σ σ')
      apply (rule_tac x=σ' in exI)
      apply (clarsimp simp: toConcurrent_fn_def toSequential_fn_def trace.split_all)
      apply (rename_tac σ σ' a s s' a')
      apply (case_tac a)
       apply (case_tac "the_agent a ∈ as"; force)
      apply simp
      done
    with False
    show "?rhs ≤ ?lhs"
      by (simp add: spec.Parallel_def ac_simps spec.map.inf_rel
           flip: INF_inf_const1 INF_inf_const2 spec.invmap.inf_rel spec.rel.inf)
    qed
  qed
  then show ?thesis1
    by (simp add: ac_simps)
qed

lemma flatten:
  fixes as :: "'a set"
  fixes a :: "'a"
  fixes bs :: "'b set"
  fixes Ps :: "'a ⇒ (sequential, 's, unit) spec"
  fixes Ps' :: "'b ⇒ (sequential, 's, unit) spec"
  assumes "Ps a = spec.Parallel bs Ps'"
  assumes "a ∈ as"
  shows "spec.Parallel as Ps = spec.Parallel ((as - {a}) <+> bs) (case_sum Ps Ps')" (is "?lhs = ?rhs")
proof(rule spec.singleton.antisym)
  have simps:
    "⋀a'. a' ≠ a ⟹ (λx::('a + 'b) agent. toConcurrent_fn (proc a') (case x of proc (Inl a) ⇒ proc a | proc (Inr _) ⇒ proc a | env ⇒ env)) = toConcurrent_fn (proc (Inl a'))"
    "⋀a'.            (λx::('a + 'b) agent. toConcurrent_fn (proc a') (case x of proc (Inl _) ⇒ env | proc (Inr a) ⇒ proc a | env ⇒ env)) = toConcurrent_fn (proc (Inr a'))"
    by (auto simp: fun_eq_iff toConcurrent_fn_def split: agent.split sum.split)
  have *:
    "∃σ''' :: (('a + 'b) agent, 's, unit) trace.t.
          ⦉σ'⦊ = ⦉trace.map (case_agent (case_sum proc ⟨proc a⟩) env) id id σ'''⦊
        ∧ ⦉trace.map (case_agent (case_sum ⟨env⟩ proc) env) id id σ'''⦊ ≤ ⦉σ''⦊
        ∧ proc (Inl a) ∉ trace.aset (♮σ''')"
      if "⦉trace.map (toConcurrent_fn (proc a)) id id σ'⦊ ≤ ⦉trace.map toSequential_fn id id σ''⦊"
     for σ'  :: "('a agent, 's, unit) trace.t"
     and σ'' :: "('b agent, 's, unit) trace.t"
  proof(cases "trace.term σ'")
    case None
    have "∃zs :: (('a + 'b) agent × 's) list.
               xs = map (map_prod (case_agent (case_sum proc (λs. proc a)) env) id) zs
             ∧ prefix (map (map_prod (case_agent (case_sum (λs. env) proc) env) id) zs) ys
             ∧ (proc (Inl a) ∉ fst ` set zs)" (is "∃zs. ?goal xs zs")
      if "prefix (map (map_prod (toConcurrent_fn (proc a)) id) xs) (map (map_prod toSequential_fn id) ys)"
     for xs :: "('a agent × 's) list" and ys :: "('b agent × 's) list"
      using that
    proof(induct xs rule: rev_induct)
      case (snoc x xs)
      then obtain zs where "?goal xs zs" by (auto dest: append_prefixD)
      with snoc.prems show ?case
        apply (clarsimp simp: map_prod.comp map_prod_conv simp flip: id_def elim!: prefixE)
        subgoal for a⇩y
          by (rule exI[where x="zs @ [(if fst x = proc a then map_agent Inr a⇩y else map_agent Inl (fst x), (snd x))]"])
             (auto simp: toSequential_fn.eq_conv map_agent.eq_conv simp flip: all_simps split: agent.split)
        done
    qed simp
    from this[of "(trace.natural' (trace.init σ') (trace.rest σ'))"
                 "trace.natural' (trace.init σ') (trace.rest σ'')"] that None
    show ?thesis
      apply (simp add: spec.singleton_le_conv trace.natural.map_inj_on_sf)
      apply (clarsimp simp: trace.natural_def trace.aset.simps trace.split_Ex image_iff trace.less_eq_None)
      subgoal for zs
        by (clarsimp dest!: trace.natural'.amap_noop intro!: exI[where x=zs])
      done
  next
    case (Some v)
    have *: "∃zs :: (('a + 'b) agent × 's) list.
               xs = map (map_prod (case_agent (case_sum proc (λs. proc a)) env) id) zs
             ∧ ys = map (map_prod (case_agent (case_sum (λs. env) proc) env) id) zs
             ∧ (proc (Inl a) ∉ fst ` set zs)"
      if "map (map_prod (toConcurrent_fn (proc a)) id) xs = map (map_prod toSequential_fn id) ys"
     for xs :: "('a agent × 's) list" and ys :: "('b agent × 's) list"
    proof -
      from that have "length xs = length ys"
        using map_eq_imp_length_eq by blast
      from this that show ?thesis
      proof(induct rule: list_induct2)
        case (Cons x xs y ys) then show ?case
          by (cases x, cases y, cases "fst x")
             (auto 8 0 simp: Cons_eq_map_conv comp_def toSequential_fn_eq_toConcurrent_fn_conv
                  simp flip: id_def ex_simps
                      split: if_splits agent.splits sum.split)
      qed simp
    qed
    from that Some
         *[where xs="trace.natural' (trace.init σ') (trace.rest σ')"
             and ys="trace.natural' (trace.init σ') (trace.rest σ'')"]
    show ?thesis
      apply (simp add: spec.singleton_le_conv trace.natural.map_inj_on_sf)
      apply (clarsimp simp: trace.natural_def)
      subgoal for zs
        by (clarsimp simp: trace.split_Ex trace.aset.simps
                    dest!: trace.natural'.amap_noop
                   intro!: exI[where x=zs])
      done
  qed
  {
    fix σ
    assume "⦉σ⦊ ≤ ?lhs"
    then obtain σ⇩a σ⇩b σ⇩c
      where 1: "trace.steps' (trace.init σ⇩a) (trace.rest σ⇩a) ⊆ insert env (proc ` as) × UNIV"
        and 2: "∀x∈as. ⦉trace.map (toConcurrent_fn (proc x)) id id σ⇩a⦊ ≤ Ps x"
        and 3: "⦉σ⦊ ≤ ⦉trace.map toSequential_fn id id σ⇩a⦊"
        and 4: "trace.steps' (trace.init σ⇩b) (trace.rest σ⇩b) ⊆ insert env (proc ` bs) × UNIV"
        and 5: "∀x∈bs. ⦉trace.map (toConcurrent_fn (proc x)) id id σ⇩b⦊ ≤ Ps' x"
        and 6: "σ⇩a ≃⇩S trace.map (case_agent (case_sum proc ⟨proc a⟩) env) id id σ⇩c"
        and 7: "⦉trace.map (case_agent (case_sum ⟨env⟩ proc) env) id id σ⇩c⦊ ≤ ⦉σ⇩b⦊"
        and 8: "proc (Inl a) ∉ trace.aset (♮σ⇩c)"
      apply (clarsimp simp: spec.Parallel_def spec.singleton.le_conv le_Inf_iff)
      apply (frule bspec[OF _ ‹a ∈ as›])
      apply (clarsimp simp: assms(1) spec.Parallel_def spec.singleton.le_conv le_Inf_iff dest!: *)
      done
    show "⦉σ⦊ ≤ ?rhs"
      unfolding spec.Parallel_def spec.singleton.le_conv inf.bounded_iff le_Inf_iff ball_simps
    proof(intro exI[where x=σ⇩c] conjI ballI)
      show "trace.steps' (trace.init σ⇩c) (trace.rest σ⇩c)
         ⊆ insert env (proc ` ((as - {a}) <+> bs)) × UNIV" (is "?lhs ⊆ ?rhs")
      proof(rule subsetI, unfold split_paired_all)
        show "(x, s, s') ∈ ?rhs" if "(x, s, s') ∈ ?lhs" for x s s'
        proof(cases x)
          case (proc y) then show ?thesis
          proof(cases y)
            case (Inl a)
            with that proc 1 arg_cong[OF 6, where f=trace.steps] 8
            show ?thesis
              by (fastforce simp: trace.steps'.natural' trace.steps'.map trace.aset.natural_conv)
          next
            case (Inr b)
            with that proc 4 spec.steps.mono[OF 7]
            show ?thesis
              by (fastforce simp: trace.steps'.natural' trace.steps'.map spec.steps.singleton)
          qed
        qed simp
      qed
      show "⦉trace.map (toConcurrent_fn (proc x)) id id σ⇩c⦊ ≤ (case x of Inl x ⇒ Ps x | Inr x ⇒ Ps' x)"
        if "x ∈ (as - {a}) <+> bs"
       for x
      proof(cases x)
        case (Inl l) with 2 6 that show ?thesis
          by (force dest: trace.stuttering.equiv.map[where af="toConcurrent_fn (proc l)" and sf=id and vf=id]
                    simp: sum_In_conv simps fun_unit_id[where f="λ_::unit. ()"]
               simp flip: id_def
                    cong: spec.singleton_cong)
      next
        case (Inr r) with 2 5 6 7 that show ?thesis
          by (fastforce dest: spec.singleton.map_le[where af="toConcurrent_fn (proc r)" and sf=id and vf=id]
                        simp: simps fun_unit_id[where f="λ_::unit. ()"]
                   simp flip: id_def
                        cong: spec.singleton_cong)
      qed
      from 3 6
      show "⦉σ⦊ ≤ ⦉trace.map toSequential_fn id id σ⇩c⦊"
        by (fastforce dest: trace.stuttering.equiv.map[where af="toSequential_fn" and sf=id and vf=id]
                      simp: spec.singleton_le_conv id_def agent.case_distrib sum.case_distrib
                 simp flip: toSequential_fn_alt_def
                      cong: agent.case_cong sum.case_cong)
    qed
  }
  {
    fix σ
    assume "⦉σ⦊ ≤ ?rhs"
    then obtain σ'
      where 1: "trace.steps' (trace.init σ') (trace.rest σ') ⊆ insert env (proc ` ((as - {a}) <+> bs)) × UNIV"
        and 2: "∀x∈(as - {a}) <+> bs. ⦉trace.map (toConcurrent_fn (proc x)) id id σ'⦊ ≤ (case x of Inl x ⇒ Ps x | Inr x ⇒ Ps' x)"
        and 3: "⦉σ⦊ ≤ ⦉trace.map toSequential_fn id id σ'⦊"
      by (clarsimp simp: spec.Parallel_def spec.singleton.le_conv le_Inf_iff)
    show "⦉σ⦊ ≤ ?lhs"
    proof -
      from ‹a ∈ as› 1
      have "trace.steps' (trace.init σ') (map (map_prod (case_agent (case_sum proc ⟨proc a⟩) env) id) (trace.rest σ'))
         ⊆ insert env (proc ` as) × UNIV"
        by (auto simp: trace.steps'.map)
      moreover
      have "⦉trace.map (λy. toConcurrent_fn (proc x) (case y of proc (Inl a) ⇒ proc a | proc (Inr b) ⇒ proc a | env ⇒ env)) id id σ'⦊ ≤ Ps x"
        if "x ∈ as"
       for x
      proof(cases "x = a")
        case True show ?thesis
        proof -
          from ‹a ∈ as› 1
          have "trace.steps' (trace.init σ') (map (map_prod (case_agent (case_sum ⟨env⟩ proc) env) id) (trace.rest σ'))
             ⊆ insert env (proc ` bs) × UNIV"
            by (auto simp: trace.steps'.map)
          moreover
          from 2
          have "⦉trace.map (λy. toConcurrent_fn (proc b) (case y of proc (Inl a) ⇒ env | proc (Inr b) ⇒ proc b | env ⇒ env)) id id σ'⦊ ≤ Ps' b"
            if "b ∈ bs"
           for b
            using that by (fastforce simp: simps dest: bspec[where x="Inr b"])
          moreover
          from 1
          have "⦉trace.map (λy. toConcurrent_fn (proc a) (case y of proc (Inl a) ⇒ proc a | proc (Inr b) ⇒ proc a | env ⇒ env)) id id σ'⦊
             ≤ ⦉trace.map (λy. toSequential_fn (case y of proc (Inl a) ⇒ env | proc (Inr b) ⇒ proc b | env ⇒ env)) id id σ'⦊"
            by (subst spec.singleton.map_cong[where af'="λy. toSequential_fn (case y of proc (Inl s) ⇒ env | proc (Inr b) ⇒ proc b | env ⇒ env)", OF _ refl refl refl];
                fastforce simp: trace.aset.natural_conv split: agent.split sum.split)
          ultimately show ?thesis
            apply (simp add: ‹x = a› assms(1) spec.Parallel_def spec.singleton.le_conv le_Inf_iff)
            apply (rule exI[where x="trace.map (case_agent (case_sum ⟨env⟩ proc) env) id id σ'"])
            apply (intro conjI ballI)
            apply (simp_all add: fun_unit_id[where f="λ_::unit. ()"] flip: id_def)
            done
        qed
      next
        case False with 2 that show ?thesis
          by (fastforce simp: simps dest: bspec[where x="Inl x"])
      qed
      moreover
      from 3
      have "⦉σ⦊ ≤ ⦉trace.map (λx. toSequential_fn (case x of proc (Inl a) ⇒ proc a | proc (Inr b) ⇒ proc a | env ⇒ env)) id id σ'⦊"
        by (simp add: agent.case_distrib sum.case_distrib
                flip: toSequential_fn_alt_def
                cong: agent.case_cong sum.case_cong)
      ultimately show ?thesis
        apply (simp add: spec.Parallel_def spec.singleton.le_conv le_Inf_iff)
        apply (rule exI[where x="trace.map (case_agent (case_sum proc ⟨proc a⟩) env) id id σ'"] conjI ballI)
        apply (simp add: fun_unit_id[where f="λ_::unit. ()"] flip: id_def)
        done
    qed
  }
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "none"›

lemma Parallel_some_agents:
  assumes "⋀a. a ∈ bs ⟹ Ps a = spec.term.none (Ps' a)"
  assumes "as ∩ bs ≠ {}"
  shows "spec.Parallel as Ps = spec.term.none (‖a∈as. if a ∈ as ∩ bs then Ps' a else Ps a)"
using assms(1)[symmetric] assms(2)
      INF_union[where A="as - bs" and B="as ∩ bs"
                  and M="λa. spec.toConcurrent a (if a ∈ bs then Ps' a else Ps a)"]
by (simp add: spec.Parallel_def Un_Diff_Int inf_assoc image_image
              spec.term.none.map spec.term.none.invmap spec.term.none.inf_unit(2) spec.term.none.Inf_not_empty
        flip: INF_union)

lemma Parallel_not_empty:
  assumes "as ≠ {}"
  shows "spec.term.none (Parallel as Ps) = Parallel as (spec.term.none ∘ Ps)"
using assms spec.term.none.Parallel_some_agents[where as=as and bs=as and Ps="spec.term.none ∘ Ps" and Ps'=Ps]
by (simp cong: spec.Parallel.cong)

lemma parallel:
  shows "spec.term.none (P ∥ Q) = spec.term.none P ∥ spec.term.none Q"
by (simp add: spec.parallel_def spec.term.none.Parallel_not_empty comp_def if_distrib)

lemma
  shows parallelL: "spec.term.none P ∥ Q = spec.term.none (P ∥ Q)"
    and parallelR: "P ∥ spec.term.none Q = spec.term.none (P ∥ Q)"
using
  spec.term.none.Parallel_some_agents[where
    as=UNIV and bs="{True}"
            and Ps="λa. if a then spec.term.none P else Q" and Ps'="λa. if a then P else Q"]
  spec.term.none.Parallel_some_agents[where
    as=UNIV and bs="{False}"
            and Ps="λa. if a then P else spec.term.none Q" and Ps'="λa. if a then P else Q"]
by (simp_all add: spec.parallel_def cong: if_cong)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "all"›

lemma Parallel:
  shows "spec.term.all (spec.Parallel as Ps) = spec.Parallel as (spec.term.all ∘ Ps)"
by (simp add: spec.Parallel_def image_image
              spec.term.all.Inf spec.term.all.inf spec.term.all.invmap spec.term.all.map spec.term.all.rel)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "idle"›

lemma parallel_le:
  assumes "spec.idle ≤ P"
  assumes "spec.idle ≤ Q"
  shows "spec.idle ≤ P ∥ Q"
by (simp add: assms spec.parallel_def spec.idle_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap"›

lemma parallel: ―‹ ‹af = id› in ‹spec.invmap› ›
  shows "spec.invmap id sf vf (spec.parallel P Q)
       = spec.parallel (spec.invmap id sf vf P) (spec.invmap id sf vf Q)"
by (simp add: spec.parallel_def spec.Parallel.invmap comp_def if_distrib)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "parallel"›

lemma bot:
  shows botL: "spec.parallel ⊥ P = ⊥"
    and botR: "spec.parallel P ⊥ = ⊥"
by (simp_all add: spec.parallel_def spec.Parallel.bot[where a="False"] spec.Parallel.bot[where a="True"])

lemma commute:
  shows "spec.parallel P Q = spec.parallel Q P"
unfolding spec.parallel_def by (subst spec.Parallel.rename[symmetric, OF bij_Not]) (simp add: comp_def)

lemma mono:
  assumes "P ≤ P'"
  assumes "Q ≤ Q'"
  shows "spec.parallel P Q ≤ spec.parallel P' Q'"
by (simp add: assms spec.parallel_def spec.Parallel.mono)

lemma strengthen[strg]:
  assumes "st_ord F P P'"
  assumes "st_ord F Q Q'"
  shows "st_ord F (spec.parallel P Q) (spec.parallel P' Q')"
using assms by (cases F; simp add: spec.parallel.mono)

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≤) F"
  assumes "monotone orda (≤) G"
  shows "monotone orda (≤) (λf. spec.parallel (F f) (G f))"
using assms by (simp add: spec.parallel_def spec.Parallel.mono2mono)

lemma Sup:
  fixes Ps :: "(sequential, 's, unit) spec set"
  shows SupL: "⨆Ps ∥ Q = (⨆P∈Ps. P ∥ Q)"
    and SupR: "Q ∥ ⨆Ps = (⨆P∈Ps. Q ∥ P)"
by (simp_all add: spec.parallel_alt_def spec.invmap.Sup spec.map.Sup heyting.inf_SUP_distrib image_image)

lemma sup:
  fixes P :: "(sequential, 's, unit) spec"
  shows supL: "(P ⊔ Q) ∥ R = (P ∥ R) ⊔ (Q ∥ R)"
    and supR: "P ∥ (Q ⊔ R) = (P ∥ Q) ⊔ (P ∥ R)"
using spec.parallel.Sup[where Ps="{P, Q}" for P Q, simplified] by fast+

text‹

We can residuate \<^const>‹spec.parallel› but not ‹prog.parallel› (see \S\ref{sec:programs-language})
as the latter is not strict. Intuitively any realistic modelling of parallel composition will be
non-strict as the divergence of one process should not block the progress of others, and
incorporating such interference may preclude the implementation of a specification via this residuation.

References:
 ▪ \<^citet>‹‹Law 23› in "Hayes:2016"›: residuate parallel
 ▪ \<^citet>‹‹Lemma~6› in "vanStaden:2015"› who cites \<^citet>‹"ArmstrongGomesStruth:2014"›

›

definition res :: "(sequential, 's, unit) spec ⇒ (sequential, 's, unit) spec ⇒ (sequential, 's, unit) spec" where
  "res S i = ⨆{P. P ∥ i ≤ S}"

interpretation res: galois.complete_lattice_class "λS. spec.parallel S i" "λS. spec.parallel.res S i" for i  ―‹ \<^citet>‹‹Law 23 (rely refinement)› in "Hayes:2016"› ›
proof
  have *: "spec.parallel.res S i ∥ i ≤ S" for S ―‹ \<^citet>‹‹Law 22 (rely quotient)› in "Hayes:2016"› ›
    by (simp add: spec.parallel.res_def spec.parallel.SupL)
  show "x ∥ i ≤ S ⟷ x ≤ spec.parallel.res S i" for x S
    by (fastforce simp: spec.parallel.res_def Sup_upper spec.parallel.mono intro: order.trans[OF _ *])
qed

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) P"
  assumes "mcont luba orda Sup (≤) Q"
  shows "mcont luba orda Sup (≤) (λx. spec.parallel (P x) (Q x))"
proof(rule ccpo.mcont2mcont'[OF complete_lattice_ccpo _ _ assms(1)])
  show "mcont Sup (≤) Sup (≤) (λy. spec.parallel y (Q x))" for x
    by (intro mcontI contI monotoneI) (simp_all add: spec.parallel.mono spec.parallel.SupL)
  show "mcont luba orda Sup (≤) (λx. spec.parallel y (Q x))" for y
    by (simp add: mcontI monotoneI contI mcont_monoD[OF assms(2)] spec.parallel.mono mcont_contD[OF assms(2)] spec.parallel.SupR image_image)
qed

lemma inf_rel:
  shows "spec.rel ({env} × UNIV ∪ {self} × r) ⊓ (P ∥ Q)
      = (spec.rel ({env} × UNIV ∪ {self} × r) ⊓ P) ∥ (spec.rel ({env} × UNIV ∪ {self} × r) ⊓ Q)"
    and "(P ∥ Q) ⊓ spec.rel ({env} × UNIV ∪ {self} × r)
      = (spec.rel ({env} × UNIV ∪ {self} × r) ⊓ P) ∥ (spec.rel ({env} × UNIV ∪ {self} × r) ⊓ Q)"
by (simp_all add: ac_simps spec.parallel_def spec.Parallel.inf_rel if_distrib[where f="λx. x ⊓ y" for y])

lemma assoc:
  shows "spec.parallel P (spec.parallel Q R) = spec.parallel (spec.parallel P Q) R" (is "?lhs = ?rhs")
by (auto simp: spec.parallel_def bij_betw_def Plus_def UNIV_bool
               spec.Parallel.flatten[where a=False] spec.Parallel.flatten[where a=True]
       intro!: spec.Parallel.rename_cong[where π="case_sum (λa. if a then Inr True else undefined)
                                                           (λa. if a then Inr False else Inl False)"])

lemma bind_botR:
  shows "spec.parallel (P ⤜ ⊥) Q  = spec.parallel P Q ⤜ ⊥"
    and "spec.parallel P (Q ⤜ ⊥)  = spec.parallel P Q ⤜ ⊥"
by (simp_all add: spec.bind.botR spec.term.none.parallelL spec.term.none.parallelR)

lemma interference:
  shows interferenceL: "spec.rel ({env} × UNIV) ∥ c = c"
    and interferenceR: "c ∥ spec.rel ({env} × UNIV) = c"
by (simp_all add: spec.parallel_def spec.Parallel.singleton_agents
  flip: spec.Parallel.rename_UNIV[where as="{False}" and f="id" and Ps="⟨c⟩", simplified]
        spec.Parallel.rename_UNIV[where as="{True}" and f="id" and Ps="⟨c⟩", simplified])

lemma unwindL:
  assumes "spec.rel ({env} × UNIV) ⤜ (λ_::unit. Q) ≤ Q" ―‹ All other processes begin with interference ›
  assumes "f ⤜ g ≤ P" ―‹ The selected process starts with action ‹f› ›
  shows "f ⤜ (λv. g v ∥ Q) ≤ P ∥ Q"
unfolding spec.parallel_def
by (strengthen ord_to_strengthen[OF spec.Parallel.unwind[where a=True]])
   (auto simp: spec.Parallel.mono spec.bind.mono intro: assms)

lemma unwindR:
  assumes "spec.rel ({env} × UNIV) ⤜ (λ_::unit. P) ≤ P" ―‹ All other processes begin with interference ›
  assumes "f ⤜ g ≤ Q" ―‹ The selected process starts with action ‹f› ›
  shows "f ⤜ (λv. P ∥ g v) ≤ P ∥ Q"
by (subst (1 2) spec.parallel.commute) (rule spec.parallel.unwindL[OF assms])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference.closed"›

lemma toConcurrent_gen:
  fixes P :: "(sequential, 's, 'v) spec"
  fixes a :: "'a"
  assumes P: "P ∈ spec.interference.closed ({env} × r)"
  shows "spec.toConcurrent a P ∈ spec.interference.closed ((-{proc a}) × r)"
proof -
  have *: "map_prod (toConcurrent_fn (proc a)) id -` ({env} × r) = (-{proc a}) × r"
    by (force simp: toConcurrent_fn_def)
  show ?thesis
    apply (rule spec.interference.closed_clI)
    apply (subst (2) spec.interference.closed_conv[OF P])
    apply (force intro: spec.interference.cl.mono simp: * spec.invmap.interference.cl)
    done
qed

lemma toConcurrent:
  fixes P :: "(sequential, 's, 'v) spec"
  fixes a :: "'a"
  assumes P: "P ∈ spec.interference.closed ({env} × r)"
  shows "spec.toConcurrent a P ∈ spec.interference.closed ({env} × r)"
by (blast intro: subsetD[OF spec.interference.closed.antimono
                            spec.interference.closed.toConcurrent_gen[OF assms]])

lemma toSequential:
  fixes P :: "('a agent, 's, 'v) spec"
  assumes "P ∈ spec.interference.closed ({env} × r)"
  shows "spec.toSequential P ∈ spec.interference.closed ({env} × r)"
proof -
  have *: "map_prod toSequential_fn id ` ({env} × r) = {env} × r"
    by (force simp: toSequential_fn_def)
  show ?thesis
    apply (rule spec.interference.closed_clI)
    apply (subst (2) spec.interference.closed_conv[OF assms])
    apply (simp add: * spec.map.interference.cl_sf_id)
    done
qed

lemma Parallel:
  assumes "⋀a. Ps a ∈ spec.interference.closed ({env} × UNIV)"
  shows "spec.Parallel as Ps ∈ spec.interference.closed ({env} × UNIV)"
unfolding spec.Parallel_def
by (fastforce intro: spec.interference.closed.rel spec.interference.closed_Inf spec.interference.closed.toSequential
               simp: assms image_subset_iff spec.interference.closed.toConcurrent)

lemma parallel:
  assumes "P ∈ spec.interference.closed ({env} × UNIV)"
  assumes "Q ∈ spec.interference.closed ({env} × UNIV)"
  shows "P ∥ Q ∈ spec.interference.closed ({env} × UNIV)"
by (simp add: assms spec.parallel_def spec.interference.closed.Parallel)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Specification Inhabitation\label{sec:inhabitation} ›

text‹

Given that ‹⊥› satisfies any specification \<^term>‹S::('a, 's, 'v) spec›, we may wish to show that
a specific trace ‹σ› is allowed by ‹S›.

The strategy is to compute the allowed transitions from a given
initial state and possibly a return value. We almost always discard the
closures we've added for various kinds of compositionality.

References:
 ▪ Similar to how \<^citet>‹‹\S3.3› in "vanStaden:2014"› models a small-step operational semantics.
  ▪ i.e., we can (semantically) define something like an LTS, which is compositional wrt parallel
  ▪ a bit like a resumption or a residual
 ▪ Similar to \<^citet>‹"HoareHeSampaio:2000"›

TODO:
 ▪ often want transitive variants of these rules
 ▪ automate: only stop when there's a scheduling decision to be made

›

definition inhabits :: "('a, 's, 'w) spec ⇒ 's ⇒ ('a × 's) list ⇒ ('a, 's, 'w) spec ⇒ bool" (‹_/ -_, _→/ _› [50, 0, 0, 50] 50) where
  "S -s, xs→ T ⟷ ⦉s, xs, Some ()⦊ ⪢ T ≤ S"

setup ‹Sign.mandatory_path "inhabits"›

lemma incomplete:
  assumes "S -s, xs→ S'"
  shows "⦉s, xs, None⦊ ≤ S"
by (strengthen ord_to_strengthen[OF assms[unfolded inhabits_def]])
   (simp add: spec.bind.incompleteI)

lemma complete:
  assumes "S -s, xs→ spec.return v"
  shows "⦉s, xs, Some v⦊ ≤ S"
by (strengthen ord_to_strengthen[OF assms[unfolded inhabits_def]])
   (simp add: spec.bind.continueI[where ys="[]", simplified] spec.singleton.le_conv)

lemmas I = inhabits.complete inhabits.incomplete

lemma mono:
  assumes "S ≤ S'"
  assumes "T' ≤ T"
  assumes "S -s, xs→ T"
  shows "S' -s, xs→ T'"
unfolding inhabits_def
apply (strengthen ord_to_strengthen[OF assms(1)])
apply (strengthen ord_to_strengthen[OF assms(2)])
apply (rule assms(3)[unfolded inhabits_def])
done

lemma strengthen[strg]:
  assumes "st_ord F S S'"
  assumes "st_ord (¬F) T T'"
  shows "st F (⟶) (S -s, xs→ T) (S' -s, xs→ T')"
using assms by (cases F; simp add: inhabits.mono)

lemma pre:
  assumes "S -s, xs'→ T"
  assumes "T' ≤ T"
  assumes "xs = xs'"
  shows "S -s, xs→ T'"
using assms by (blast intro: inhabits.mono[OF order.refl assms(2)])

lemma tau:
  assumes "spec.idle ≤ S"
  shows "S -s, []→ S"
unfolding inhabits_def
by (strengthen ord_to_strengthen[OF spec.action.stutterI[where F="{()} × UNIV × Id"]])
   (simp_all add: assms spec.bind.returnL flip: spec.return_def)

lemma trans:
  assumes "R -s, xs→ S"
  assumes "S -trace.final' s xs, ys→ T"
  shows "R -s, xs @ ys→ T"
unfolding inhabits_def
apply (strengthen ord_to_strengthen(2)[OF assms(1)[unfolded inhabits_def]])
apply (strengthen ord_to_strengthen(2)[OF assms(2)[unfolded inhabits_def]])
apply (simp add: spec.bind.continueI spec.bind.mono flip: spec.bind.bind)
done

lemma Sup:
  assumes "P -s, xs→ P'"
  assumes "P ∈ X"
  shows "⨆X -s, xs→ P'"
using assms by (simp add: inhabits_def Sup_upper2)

lemma supL:
  assumes "P -s, xs→ P'"
  shows "P ⊔ Q -s, xs→ P'"
using assms by (simp add: inhabits_def le_supI1)

lemma supR:
  assumes "Q -s, xs→ Q'"
  shows "P ⊔ Q -s, xs→ Q'"
using assms by (simp add: inhabits_def le_supI2)

lemma inf:
  assumes "P -s, xs→ P'"
  assumes "Q -s, xs→ Q'"
  shows "P ⊓ Q -s, xs→ P' ⊓ Q'"
using assms by (meson inf.cobounded1 inf.cobounded2 le_inf_iff inhabits.pre inhabits_def)

lemma infL:
  assumes "P -s, xs→ R"
  assumes "Q -s, xs→ R"
  shows "P ⊓ Q -s, xs→ R"
using assms by (meson le_inf_iff inhabits_def)

setup ‹Sign.mandatory_path "spec"›

lemma bind:
  assumes "f -s, xs→ f'"
  shows "f ⤜ g -s, xs→ f' ⤜ g"
using assms by (simp add: inhabits_def spec.bind.mono flip: spec.bind.bind)

lemmas bind' = inhabits.trans[OF inhabits.spec.bind]

lemma parallelL:
  assumes "P -s, xs→ P'"
  assumes "spec.rel ({env} × UNIV) ⤜ (λ_::unit. Q) ≤ Q"
  shows "P ∥ Q -s, xs→ P' ∥ Q"
by (rule inhabits.mono[OF spec.parallel.unwindL[OF assms(2) assms(1)[unfolded inhabits_def]]
                          order.refl])
   (simp add: inhabits_def)

lemma parallelR:
  assumes "Q -s, xs→ Q'"
  assumes "spec.rel ({env} × UNIV) ⤜ (λ_::unit. P) ≤ P"
  shows "P ∥ Q -s, xs→ P ∥ Q'"
by (subst (1 2) spec.parallel.commute) (rule inhabits.spec.parallelL assms)+

lemmas parallelL' = inhabits.trans[OF inhabits.spec.parallelL]
lemmas parallelR' = inhabits.trans[OF inhabits.spec.parallelR]

setup ‹Sign.mandatory_path "action"›

lemma step:
  assumes "(v, a, s, s') ∈ F"
  shows "spec.action F -s, [(a, s')]→ spec.return v"
by (clarsimp simp: inhabits_def trace.split_all spec.bind.singletonL spec.term.none.singleton
                   spec.singleton.le_conv spec.action.stepI[OF assms]
           intro!: ord_eq_le_trans[OF spec.singleton.Cons spec.action.stepI[OF assms]])

lemma stutter:
  assumes "(v, a, s, s) ∈ F"
  shows "spec.action F -s, []→ spec.return v"
using inhabits.spec.action.step[OF assms] by (simp add: inhabits_def)

setup ‹Sign.parent_path›

lemma map:
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  assumes "P -s, xs → spec.return v"
  shows "spec.map af sf vf P -sf s, map (map_prod af sf) xs→ spec.return (vf v)"
proof -
  have "⦉sf s, map (map_prod af sf) xs, Some ()⦊ ⪢ spec.return (vf v)
     ≤ spec.map af sf vf (⦉s, xs, Some ()⦊ ⪢ spec.return v)"
    by (subst (1) spec.bind.singletonL)
       (fastforce intro: spec.bind.incompleteI
                         spec.bind.continueI[where ys="[]" and w="Some v", simplified]
                   simp: spec.singleton.le_conv spec.term.none.singleton
                  split: option.split_asm)
  then show ?thesis
    using assms by (auto simp: inhabits_def dest: spec.map.mono[where af=af and sf=sf and vf=vf])
qed

lemma invmap:
  fixes af :: "'a ⇒ 'b"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  assumes "P -sf s, map (map_prod af sf) xs → P'"
  shows "spec.invmap af sf vf P -s, xs→ spec.invmap af sf vf P'"
by (strengthen ord_to_strengthen(2)[OF assms(1)[unfolded inhabits_def]])
   (simp add: inhabits_def spec.invmap.bind spec.map.singleton spec.bind.mono
        flip: spec.map_invmap.galois)

setup ‹Sign.mandatory_path "term.none"›

lemma step:
  assumes "P -s, xs→ P'"
  shows "spec.term.none P -s, xs→ spec.term.none P'"
by (simp add: inhabits.spec.bind[OF assms] flip: spec.bind.botR)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term.all"›

lemma step:
  assumes "P -s, xs→ P'"
  shows "spec.term.all P -s, xs→ spec.term.all P'"
by (strengthen ord_to_strengthen(2)[OF assms(1)[unfolded inhabits_def]])
   (simp add: inhabits_def spec.term.all.bind)

lemma "term":
  assumes "spec.idle ≤ P"
  shows "spec.term.all P -s, []→ spec.return v"
by (strengthen ord_to_strengthen(2)[OF assms(1)])
   (auto simp: spec.term.all.idle intro: spec.idle_le inhabits.tau inhabits.Sup)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "kleene.star"›

lemma step:
  assumes "P -s, xs→ P'"
  shows "spec.kleene.star P -s, xs→ P' ⪢ spec.kleene.star P"
by (subst spec.kleene.star.simps) (simp add: assms inhabits.supL inhabits.spec.bind)

lemma "term":
  shows "spec.kleene.star P -s, []→ spec.return ()"
by (metis inhabits.tau inhabits.supR spec.kleene.star.simps spec.idle.return_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "rel"›

lemma rel:
  assumes "trace.steps' s xs ⊆ r"
  shows "spec.rel r -s, xs→ spec.rel r"
proof -
  from assms
  have "⦉s, xs, Some ()⦊ ⪢ spec.rel r ≤ spec.rel r ⤜ (λ_::unit. spec.rel r)"
    by (simp add: spec.bind.mono spec.singleton.le_conv)
  then show ?thesis
    by (simp add: inhabits_def spec.rel.wind_bind)
qed

lemma rel_term:
  assumes "trace.steps' s xs ⊆ r"
  shows "spec.rel r -s, xs→ spec.return v"
by (rule inhabits.pre[OF inhabits.spec.rel.rel[OF assms] spec.return.rel_le refl])

lemma step:
  assumes "(a, s, s') ∈ r"
  shows "spec.rel r -s, [(a, s')]→ spec.rel r"
by (rule inhabits.pre)
   (auto intro: assms inhabits.spec.action.step[where s'=s'] inhabits.spec.kleene.star.step
                      inhabits.spec.term.all.step
          simp: spec.rel_def spec.rel.act_def spec.bind.returnL spec.idle_le)

lemma "term":
  shows "spec.rel r -s, []→ spec.return v"
by (simp add: inhabits.pre[OF inhabits.tau[OF spec.idle.rel_le] spec.return.rel_le])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›
(*<*)

end
(*>*)