Theory Local_State

(*<*)
theory Local_State
imports
  Programs
begin

lemmas trace_steps'_map =
  trace.steps'.map(1)[where af=id and sf="Pair (fst (trace.final' (ls, s) xs))" and s="snd (trace.final' (ls, s) xs)", simplified]
  trace.steps'.map(1)[where af=id and sf="Pair x"]
    for ls s xs x

lemma trace_steps'_snd_le_const:
  assumes "trace.steps' (ls, s) xs ⊆ {(a, (ls', s'), (ls'', s'))}"
  shows "(λx. snd (snd x)) ` set xs ⊆ {s}"
using subset_singletonD[OF assms] by (force simp: trace.steps'.step_conv image_subset_iff)

lemma trace_natural'_took_step_shared_changes:
  assumes "trace.steps' (ls, s) xs ⊆ {(a, (ls'', s''), (ls''', s'''))}"
  assumes "trace.final' (ls, s) xs = (ls', s')"
  assumes "s ≠ s'"
  shows "trace.natural' s (map (map_prod id snd) xs) = [(a, s')]"
using subset_singletonD[OF assms(1)] assms(2-)
by (auto simp: trace.steps'.step_conv trace.natural'.append trace.natural'.eq_Nil_conv
               image_subset_iff append_eq_Cons_conv)

lemma trace_natural'_took_step_shared_same:
  assumes "trace.steps' (ls, s) xs ⊆ {(a, (ls'', s'), (ls''', s'))}"
  assumes "alss ∈ set xs"
  shows "snd (snd alss) = s"
using subset_singletonD[OF assms(1)] assms(2)
by (fastforce simp: trace.steps'.step_conv image_subset_iff)

(*>*)
section‹ Structural local state\label{sec:local_state} ›

subsection‹ ∗‹spec.local›\label{sec:local_state-spec_local} ›

text‹

We develop a few combinators for structural local state. The goal is to encapsulate a local state
of type \<^typ>‹'ls› in a process \<^typ>‹('a agent, 'ls × 's, 'v) spec›. Applying \<^term>‹spec.smap snd›
yields a process of type \<^typ>‹('a agent, 's, 'v) spec›. We also constrain environment steps
to not affect \<^typ>‹'ls›, yielding a plausible data refinement rule
(see \S\ref{sec:local_state-data_refinement}).

›

―‹ Lift a predicate on the shared state ›
abbreviation (input) localize1 :: "('b ⇒ 's ⇒ 'a) ⇒ 'b ⇒ 'ls × 's ⇒ 'a" where
  "localize1 f b s ≡ f b (snd s)"

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "local"›

definition qrm :: "('a agent, 'ls × 's) steps" where ―‹ cf \<^const>‹ag.assm› ›
  "qrm = range proc × UNIV ∪ {env} × (Id ×⇩R UNIV)"

abbreviation (input) "interference ≡ spec.rel spec.local.qrm"

setup ‹Sign.parent_path›

definition local :: "('a agent, 'ls × 's, 'v) spec ⇒ ('a agent, 's, 'v) spec" where
  "local P = spec.smap snd (spec.local.interference ⊓ P)"

setup ‹Sign.mandatory_path "singleton"›

lemma local_le_conv:
  shows "⦉σ⦊ ≤ spec.local P
         ⟷ (∃σ'. ⦉σ'⦊ ≤ P
                 ∧ trace.steps σ' ⊆ spec.local.qrm
                 ∧ ⦉σ⦊ ≤ ⦉trace.map id snd id σ'⦊)"
by (simp add: spec.local_def spec.singleton.le_conv ac_simps)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "idle"›

lemma local_le[spec.idle_le]: ―‹ Converse does not hold ›
  assumes "spec.idle ≤ P"
  shows "spec.idle ≤ spec.local P"
by (simp add: spec.local_def assms spec.idle_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "local"›

setup ‹Sign.mandatory_path "qrm"›

lemma refl:
  shows "refl (spec.local.qrm `` {a})"
by (simp add: spec.local.qrm_def refl_onI)

lemma member:
  shows "(proc a, s, s') ∈ spec.local.qrm"
    and "(env, s, s') ∈ spec.local.qrm ⟷ fst s = fst s'"
by (auto simp: spec.local.qrm_def)

lemma inter:
  shows "UNIV × Id ∩ spec.local.qrm = UNIV × Id"
    and "spec.local.qrm ∩ UNIV × Id = UNIV × Id"
    and "spec.local.qrm ∩ {self} × Id = {self} × Id"
    and "spec.local.qrm ∩ {env} × UNIV = {env} × (Id ×⇩R UNIV)"
    and "spec.local.qrm ∩ {env} × (UNIV ×⇩R Id) = {env} × Id"
    and "spec.local.qrm ∩ A × (Id ×⇩R r) = A × (Id ×⇩R r)"
by (auto simp: spec.local.qrm_def)

lemmas simps[simp] =
  spec.local.qrm.refl
  spec.local.qrm.member
  spec.local.qrm.inter

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference"›

lemma smap_snd:
  shows "spec.smap snd spec.local.interference = ⊤"
by (subst spec.map.rel)
   (auto simp: spec.local.qrm_def spec.rel.UNIV
               image_Un map_prod_image_Times map_prod_image_relprod map_prod_surj
    simp flip: Sigma_Un_distrib1)

setup ‹Sign.parent_path›

lemma inf_interference:
  shows "spec.local P = spec.local (P ⊓ spec.local.interference)"
by (simp add: spec.local_def ac_simps)

lemma bot:
  shows "spec.local ⊥ = ⊥"
by (simp add: spec.local_def spec.map.bot)

lemma top:
  shows "spec.local ⊤ = ⊤"
by (simp add: spec.local_def spec.local.interference.smap_snd)

lemma monotone:
  shows "mono spec.local"
proof(rule monotoneI)
  show "spec.local P ≤ spec.local P'" if "P ≤ P'" for P P' :: "('a agent, 's × 'ls, 'v) spec"
    unfolding spec.local_def by (strengthen ord_to_strengthen(1)[OF ‹P ≤ P'›]) simp
qed

lemmas strengthen[strg] = st_monotone[OF spec.local.monotone]
lemmas mono = monotoneD[OF spec.local.monotone]
lemmas mono2mono[cont_intro, partial_function_mono]
  = monotone2monotone[OF spec.local.monotone, simplified, of orda P for orda P]

lemma Sup:
  shows "spec.local (⨆X) = (⨆x∈X. spec.local x)"
by (simp add: spec.local_def inf_Sup spec.map.Sup image_image)

lemmas sup = spec.local.Sup[where X="{X, Y}" for X Y, simplified]

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) P"
  shows "mcont luba orda Sup (≤) (λx. spec.local (P x))"
by (simp add: spec.local_def assms)

lemma idle:
  shows "spec.local spec.idle = spec.idle"
by (simp add: spec.local_def inf.absorb2[OF spec.idle.rel_le] spec.map.idle)

lemma action:
  fixes F :: "('v × 'a agent × ('ls × 's) × ('ls × 's)) set"
  shows "spec.local (spec.action F)
       = spec.action (map_prod id (map_prod id (map_prod snd snd)) `
                                  (F ∩ UNIV × spec.local.qrm))"
by (simp add: spec.local_def spec.action.inf_rel spec.map.surj_sf_action)

lemma return:
  shows "spec.local (spec.return v) = spec.return v"
by (simp add: spec.return_def spec.local.action
              Times_Int_Times map_prod_image_Times map_prod_snd_snd_image_Id)

lemma bind_le: ―‹ Converse does not hold ›
  shows "spec.local (f ⤜ g) ≤ spec.local f ⤜ (λv. spec.local (g v))"
by (simp add: spec.local_def spec.bind.inf_rel spec.map.bind_le)

lemma interference:
  shows "spec.local (spec.rel ({env} × UNIV)) = spec.rel ({env} × UNIV)"
by (simp add: spec.local_def spec.map.rel map_prod_image_Times map_prod_image_relprod
        flip: spec.rel.inf)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "map"›

lemma local_le:
  shows "spec.map id sf vf (spec.local P) ≤ spec.local (spec.map id (map_prod id sf) vf P)"
by (fastforce intro: spec.map.mono inf.mono spec.rel.mono
               simp: spec.local_def spec.map.comp spec.map.inf_rel spec.local.qrm_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "vmap"›

lemma local:
  shows "spec.vmap vf (spec.local P) = spec.local (spec.vmap vf P)"
by (simp add: spec.local_def spec.map.comp spec.map.inf_rel spec.rel.reflcl(1)[where A=UNIV])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap"›

lemma smap_snd:
  fixes P :: "('a, 'ls × 't, 'w) spec"
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  shows "spec.invmap id sf vf (spec.smap snd P)
       = spec.smap snd (spec.invmap id (map_prod id sf) vf P)" (is "?lhs = ?rhs")
proof(rule spec.singleton.antisym)
  have smap_snd_aux:
    "∃zs. trace.natural' (ls, sf s) xs = trace.natural' (ls, sf s) (map (map_prod id (map_prod id sf)) zs)
        ∧ trace.natural' s (map (map_prod id snd) zs) = trace.natural' s ys" (is "∃zs. ?P ls s ys zs")
    if "trace.natural' (sf s) (map (map_prod id sf) ys) = trace.natural' (sf s) (map (map_prod id snd) xs)"
   for ls and s :: "'s" and sf :: "'s ⇒ 't" and xs :: "('a × 'ls × 't) list" and ys :: "('a × 's) list"
    using that
  proof(induct xs arbitrary: ls s ys)
    case (Nil ls s ys) then show ?case
      by (fastforce intro: exI[where x="map (map_prod id (Pair ls)) ys"]
                     simp: comp_def trace.natural'.eq_Nil_conv)
  next
    case (Cons x xs ls s ys) show ?case
    proof(cases "snd (snd x) = sf s")
      case True with Cons.prems show ?thesis
        by (cases x) (fastforce dest: Cons.hyps[where ls="fst (snd x)"]
                               intro: exI[where x="(fst x, fst (snd x), s) # zs" for zs]
                           simp flip: id_def)
    next
      case False
      with Cons.prems obtain a s⇩x us s' zs
        where "x = (a, s⇩x, sf s')"
        and "sf s' ≠ sf s"
        and "snd ` map_prod id sf ` set us ⊆ {sf s}"
        and "ys = us @ (a, s') # zs"
        and "trace.natural' (sf s') (map (map_prod id sf) zs) = trace.natural' (sf s') (map (map_prod id snd) xs)"
        by (cases x) (clarsimp simp: trace.natural'.eq_Cons_conv map_eq_append_conv simp flip: id_def)
      with False show ?thesis
        by (fastforce simp: comp_def trace.natural'.append image_subset_iff trace.natural'.eq_Nil_conv
                     intro: exI[where x="map (map_prod id (Pair ls)) us @ (a, (s⇩x, s')) # zs" for zs]
                      dest: Cons.hyps[where ls="fst (snd x)"])
    qed
  qed
  fix σ
  assume "⦉σ⦊ ≤ ?lhs"
  then obtain ls xs v i
    where *: "⦉(ls, sf (trace.init σ)), xs, v⦊ ≤ P"
      and **: "trace.natural' (sf (trace.init σ)) (map (map_prod id sf) (trace.rest σ))
             = trace.natural' (sf (trace.init σ)) (map (map_prod id snd) (take i xs))"
      and ***: "if i ≤ length xs then trace.term σ = None else map_option vf (trace.term σ) = v"
    apply (clarsimp simp: spec.singleton.le_conv spec.singleton_le_conv)
    apply (erule trace.less_eq_takeE)
    apply (erule trace.take.naturalE)
    apply (clarsimp simp: trace.take.map trace.natural_def trace.split_all not_le
                   split: if_split_asm)
    apply (metis order.strict_iff_not take_all)
    done
  from smap_snd_aux[OF **] obtain zs
    where "trace.natural' (ls, sf (trace.init σ)) (take i xs)
         = trace.natural' (ls, sf (trace.init σ)) (map (map_prod id (map_prod id sf)) zs)"
      and "trace.natural' (trace.init σ) (map (map_prod id snd) zs)
         = trace.natural' (trace.init σ) (trace.rest σ)"
    by blast
  with * *** show "⦉σ⦊ ≤ ?rhs"
    apply -
    unfolding spec.singleton.le_conv
    apply (rule exI[where x="trace.T (ls, trace.init σ) zs (if i ≤ length xs then None else trace.term σ)"])
    apply (clarsimp simp: spec.singleton_le_conv trace.natural_def trace.less_eq_None
                   split: if_splits
                   elim!: order.trans[rotated])
    apply (metis append_take_drop_id prefixI trace.natural'.append)
    done
next
  show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
    using that
    by (fastforce dest: spec.singleton.map_le[where af=id and sf=sf and vf=vf]
                  simp: spec.singleton.le_conv)
qed

lemma local:
  fixes P :: "('a agent, 'ls × 't, 'v) spec"
  fixes sf :: "'s ⇒ 't"
  shows "spec.invmap id sf vf (spec.local P) = spec.local (spec.invmap id (map_prod id sf) vf P)"
by (auto simp: spec.local_def spec.local.qrm_def ac_simps
               spec.invmap.smap_snd spec.invmap.inf spec.invmap.rel
  intro!: arg_cong[where f="λr. spec.smap snd (spec.invmap id (map_prod id sf) vf P ⊓ spec.rel r)"])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "none"›

lemma local:
  shows "spec.term.none (spec.local P) = spec.local (spec.term.none P)"
by (simp add: spec.local_def spec.term.none.inf spec.term.none.inf_none_rel spec.term.none.map)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "all"›

lemma local:
  shows "spec.term.all (spec.local P) = spec.local (spec.term.all P)"
by (simp add: spec.local_def spec.term.all.map spec.term.all.rel spec.term.all.inf)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "closed"›

lemma local:
  assumes "P ∈ spec.term.closed _"
  shows "spec.local P ∈ spec.term.closed _"
by (rule spec.term.closed_clI)
   (simp add: spec.term.all.local spec.term.all.monomorphic
        flip: spec.term.closed_conv[OF assms, simplified])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Local state transformations\label{sec:local_state-transformations} ›

text‹

We want to reorder, introduce and eliminate actions that affect local state while preserving
observable behaviour under \<^const>‹spec.local›.

The closure that arises from \<^const>‹spec.local›, i.e.:

›

lemma
  defines "cl ≡ spec.map_invmap.cl _ _ _ id snd id"
  assumes "spec.local.interference ⊓ P
        ≤ cl (spec.local.interference ⊓ Q)"
  shows "spec.local P ≤ spec.local Q"
unfolding spec.local_def
by (strengthen ord_to_strengthen(1)[OF assms(2)])
   (simp add: spec.map_invmap.galois cl_def spec.map_invmap.cl_def)

text‹

expresses all transformations, but does not decompose over \<^const>‹spec.bind›; in other
words we do not have ‹cl f ⤜ (λv. cl (g v)) ≤ cl (f ⤜ g)› as the
local states that ‹cl f› terminates with may not satisfy ‹g›. (Observe that we do not expect the
converse to hold as then all local states would need to be preserved.)

We therefore define a closure that preserves the observable state and
the initial and optionally final (if terminating) local states via a projection:

›

setup ‹Sign.mandatory_path "seq_ctxt"›

definition prj :: "bool ⇒ ('a, 'ls × 's, 'v) trace.t ⇒ ('a, 's, 'v) trace.t × 'ls × 'ls option" where
  "prj T σ = (♮(trace.map id snd id σ),
                fst (trace.init σ),
                if T then map_option ⟨fst (trace.final σ)⟩ (trace.term σ) else None)"

setup ‹Sign.mandatory_path "prj"›

lemma natural:
  shows "seq_ctxt.prj T (♮σ) = seq_ctxt.prj T σ"
by (simp add: seq_ctxt.prj_def trace.natural.map_natural)

lemma idle:
  shows "seq_ctxt.prj T (trace.T s [] None) = (trace.T (snd s) [] None, fst s, None)"
by (simp add: seq_ctxt.prj_def trace.natural.simps)

lemmas simps[simp] =
  seq_ctxt.prj.natural

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

interpretation seq_ctxt: galois.image_vimage "seq_ctxt.prj T" for T .

setup ‹Sign.mandatory_path "seq_ctxt.equivalent"›

lemma partial_sel_equivE:
  assumes "seq_ctxt.equivalent T σ⇩1 σ⇩2"
  obtains "trace.init σ⇩1 = trace.init σ⇩2"
      and "trace.term σ⇩1 = trace.term σ⇩2"
      and "⟦T; ∃v. trace.term σ⇩1 = Some v⟧ ⟹ trace.final σ⇩1 = trace.final σ⇩2"
using assms
by (cases σ⇩1)
   (force intro: prod_eqI
           simp: seq_ctxt.prj_def trace.natural.trace_conv
      simp flip: trace.final'.map[where af=id and sf=snd]
           cong: trace.final'.natural'_cong)

lemma downwards_existsE:
  assumes "σ⇩1' ≤ σ⇩1"
  assumes "seq_ctxt.equivalent T σ⇩1 σ⇩2"
  obtains σ⇩2'
    where "σ⇩2' ≤ σ⇩2"
      and "seq_ctxt.equivalent T σ⇩1' σ⇩2'"
using assms
apply atomize_elim
apply (clarsimp simp: seq_ctxt.prj_def)
apply (rule trace.natural.less_eqE[OF trace.map.mono sym], assumption, assumption)
apply (clarsimp split: if_split_asm)
 apply (cases "trace.term σ⇩1'")
  apply (fastforce simp: trace.natural_def elim: trace.less_eqE trace.map.less_eqR)+
done

lemma downwards_existsE2:
  assumes "σ⇩1' ≤ σ⇩1"
  assumes "seq_ctxt.equivalent T σ⇩1' σ⇩2'"
  obtains σ⇩2
    where "σ⇩2' ≤ σ⇩2"
      and "seq_ctxt.equivalent T σ⇩1 σ⇩2"
proof(atomize_elim, use ‹σ⇩1' ≤ σ⇩1› in ‹induct rule: trace.less_eqE›)
  case prefix
  from prefix(3) obtain zs
    where *: "σ⇩1 = trace.T (trace.init σ⇩1) (trace.rest σ⇩1' @ zs) (trace.term σ⇩1)"
    by (cases σ⇩1) (auto elim: prefixE)
  show ?case
  proof(cases "trace.term σ⇩1")
    case None with assms(2) prefix(1,2) * show ?thesis
      by (cases σ⇩1, cases σ⇩2')
         (fastforce intro!: exI[where x="trace.T (trace.init σ⇩1) (trace.rest σ⇩2' @ zs) (trace.term σ⇩1)"]
                      simp: seq_ctxt.prj_def trace.natural_def
                            trace.natural'.append trace.less_eq_same_append_conv
                      cong: trace.final'.natural'_cong)
  next
    case (Some v)
    from assms(2) prefix(2)
    have "snd (trace.final σ⇩1') = trace.final (trace.map id snd id σ⇩2')"
      by (cases σ⇩1', cases σ⇩2')
         (clarsimp simp: seq_ctxt.prj_def trace.natural_def trace.final'.map
                  dest!: arg_cong[where f="λxs. trace.final' (snd (trace.init σ⇩1)) xs"])
    with Some assms(2) prefix(1,2) * show ?thesis
      apply (cases σ⇩1)
      apply (cases σ⇩2')
      apply (rule exI[where x="trace.T (trace.init σ⇩1) (trace.rest σ⇩2' @ (undefined, trace.final σ⇩1') # zs) (trace.term σ⇩1)"])
      apply (clarsimp simp: seq_ctxt.prj_def trace.natural_def trace.natural'.append trace.less_eq_same_append_conv)
      apply (clarsimp cong: trace.final'.natural'_cong)
      done
  qed
next
  case (maximal v) with assms(2) show ?case
    by blast
qed

lemma map_sf_eq_id:
  assumes "seq_ctxt.equivalent True σ⇩1 σ⇩2"
  shows "seq_ctxt.equivalent True (trace.map af id vf σ⇩1) (trace.map af id vf σ⇩2)"
using assms
by (auto simp: seq_ctxt.prj_def comp_def trace.final'.map[where sf=id, simplified] trace.natural_def
    simp flip: trace.natural'.map_inj_on_sf
         dest: arg_cong[where f="map (map_prod af id)"])

lemma mono:
  assumes "T ⟹ T'"
  assumes "seq_ctxt.equivalent T' σ⇩1 σ⇩2"
  shows "seq_ctxt.equivalent T σ⇩1 σ⇩2"
using assms by (clarsimp simp: seq_ctxt.prj_def)

lemma append:
  assumes "seq_ctxt.equivalent True (trace.T s xs (Some v)) (trace.T s' xs' v')"
  assumes "seq_ctxt.equivalent T (trace.T (trace.final' s xs) ys w) (trace.T t' ys' w')"
  shows "seq_ctxt.equivalent T (trace.T s (xs @ ys) w) (trace.T s' (xs' @ ys') w')"
using assms
by (clarsimp simp: seq_ctxt.prj_def trace.natural_def trace.natural'.append
        simp flip: trace.final'.map[where af=id and sf=snd]
             cong: trace.final'.natural'_cong if_cong)
  (simp; metis trace.final'.map[where af=id and sf=fst])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "seq_ctxt"›

definition cl :: "bool ⇒ ('a, 'ls × 's, 'v) spec ⇒ ('a, 'ls × 's, 'v) spec" where
  "cl T P = ⨆(spec.singleton ` {σ⇩1. ∃σ⇩2. ⦉σ⇩2⦊ ≤ P ∧ seq_ctxt.equivalent T σ⇩1 σ⇩2})"

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "singleton.seq_ctxt"›

lemma cl_le_conv[spec.singleton.le_conv]:
  shows "⦉σ⦊ ≤ spec.seq_ctxt.cl T P ⟷ (∃σ'. ⦉σ'⦊ ≤ P ∧ seq_ctxt.equivalent T σ σ')" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
    by (clarsimp simp: spec.seq_ctxt.cl_def spec.singleton_le_conv)
       (force elim: seq_ctxt.equivalent.downwards_existsE[where T=T]
              dest: order.trans[OF spec.singleton.mono])
  show "?rhs ⟹ ?lhs"
    unfolding spec.seq_ctxt.cl_def spec.singleton_le_conv by blast
qed

setup ‹Sign.parent_path›

interpretation seq_ctxt: closure_complete_distrib_lattice_distributive_class "spec.seq_ctxt.cl T" for F
proof standard
  show "P ≤ spec.seq_ctxt.cl T Q ⟷ spec.seq_ctxt.cl T P ≤ spec.seq_ctxt.cl T Q" (is "?lhs ⟷ ?rhs")
    for P Q :: "('a, 'ls × 's, 'v) spec"
  proof(rule iffI)
    show "?lhs ⟹ ?rhs"
      by (rule spec.singleton_le_extI)
         (force simp: spec.singleton.seq_ctxt.cl_le_conv dest: order.trans[rotated])
    show "?rhs ⟹ ?lhs"
      by (metis spec.singleton.seq_ctxt.cl_le_conv spec.singleton_le_ext_conv)
  qed
  show "spec.seq_ctxt.cl T (⨆ X) ≤ ⨆ (spec.seq_ctxt.cl T ` X) ⊔ spec.seq_ctxt.cl T ⊥"
    for X :: "('a, 'ls × 's, 'v) spec set"
    by (auto simp: spec.seq_ctxt.cl_def)
qed

setup ‹Sign.mandatory_path "idle.seq_ctxt"›

lemma cl_le_conv[spec.idle_le]:
  shows "spec.idle ≤ spec.seq_ctxt.cl T P ⟷ spec.idle ≤ P" (is "?lhs ⟷ ?rhs")
proof(rule iffI[OF _ order.trans[OF _ spec.seq_ctxt.expansive]])
  show "?lhs ⟹ ?rhs"
    by (clarsimp simp: spec.idle_def spec.singleton.le_conv)
       (metis "trace.take.0" seq_ctxt.equivalent.partial_sel_equivE spec.singleton.takeI trace.t.sel(1))
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "seq_ctxt.cl"›

lemma bot[simp]:
  shows "spec.seq_ctxt.cl T ⊥ = ⊥"
by (simp add: spec.seq_ctxt.cl_def spec.singleton.not_bot)

lemma mono:
  assumes "T' ⟹ T"
  assumes "P ≤ P'"
  shows "spec.seq_ctxt.cl T P ≤ spec.seq_ctxt.cl T' P'"
unfolding spec.seq_ctxt.cl_def
by (strengthen ord_to_strengthen(1)[OF ‹P ≤ P'›])
   (blast intro: seq_ctxt.equivalent.mono[OF assms(1)])

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

lemma Sup:
  shows "spec.seq_ctxt.cl T (⨆X) = ⨆(spec.seq_ctxt.cl T ` X)"
by (simp add: spec.seq_ctxt.cl_Sup)

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

lemma singleton:
  shows "spec.seq_ctxt.cl T ⦉σ⦊ = ⨆(spec.singleton ` {σ'. seq_ctxt.equivalent T σ σ'})" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by (clarsimp simp: spec.seq_ctxt.cl_def spec.singleton_le_conv)
       (metis seq_ctxt.equivalent.downwards_existsE2 seq_ctxt.prj.natural trace.natural.mono)
  show "?rhs ≤ ?lhs"
    by (fastforce simp: spec.seq_ctxt.cl_def)
qed

lemma idle: ―‹ not ‹simp› friendly ›
  shows "spec.seq_ctxt.cl T (spec.idle :: ('a, 'ls × 's, 'v) spec)
       = spec.term.none (spec.rel (UNIV × (UNIV ×⇩R Id)) :: ('a, 'ls × 's, 'w) spec)" (is "?lhs = ?rhs")
proof(rule spec.singleton.antisym)
  have *: "s = s'"
    if "snd ` set xs ⊆ {(ls⇩0, s⇩0)}"
   and "trace.natural' s⇩0 (map (map_prod id snd) ys) = trace.natural' s⇩0 (map (map_prod id snd) xs)"
   and "(a, (ls, s), ls', s') ∈ trace.steps' (ls⇩0, s⇩0) ys"
   for xs ys :: "('a × ('ls × 's)) list" and ls⇩0 s⇩0 a ls s ls' and s'
    using that
  proof(induct ys rule: rev_induct)
    case snoc from snoc.prems show ?case
      by (auto simp: trace.natural'.append trace.steps'.append split_pairs
                     trace.final'.map[where s="(ls⇩0, s⇩0)" and sf=snd, simplified]
                     trace.natural'.map_natural'[where sf=snd and s="(ls⇩0, s⇩0)", simplified]
          simp flip: id_def trace.natural'.eq_Nil_conv
              split: if_split_asm
               dest: arg_cong[where f="λxs. trace.natural' s⇩0 (map (map_prod id snd) xs)"]
              intro: snoc.hyps[OF snoc.prems(1)])
  qed simp
  show "⦉σ⦊ ≤ ?rhs" if "⦉σ⦊ ≤ ?lhs" for σ
    using that
    by (cases σ)
       (clarsimp simp: spec.singleton.le_conv * trace.split_all seq_ctxt.prj_def trace.natural_def)
  have *: "s' = snd s"
    if "trace.steps' s xs ⊆ UNIV × (UNIV ×⇩R Id)"
   and "(a, (ls', s')) ∈ set xs"
   for a s ls' s' and xs :: "('a × ('ls × 's)) list"
    using that by (induct xs arbitrary: s) (auto simp: trace.steps'.Cons_eq_if split: if_splits)
  show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
    using that
    by (cases "trace.init σ")
       (fastforce simp: spec.singleton.le_conv seq_ctxt.prj_def trace.natural_def map_prod.comp
                  dest: *
                 intro: exI[where x="trace.map id (map_prod ⟨fst (trace.init σ)⟩ id) id σ"])
qed

lemma invmap_le:
  shows "spec.seq_ctxt.cl True (spec.invmap af id vf P) ≤ spec.invmap af id vf (spec.seq_ctxt.cl True P)"
by (rule spec.singleton_le_extI)
   (auto simp: spec.singleton.le_conv dest: seq_ctxt.equivalent.map_sf_eq_id)

lemma map_le:
  shows "spec.map af id vf (spec.seq_ctxt.cl True P) ≤ spec.seq_ctxt.cl True (spec.map af id vf P)"
by (rule spec.singleton_le_extI)
   (clarsimp simp: spec.singleton.le_conv
            dest!: seq_ctxt.equivalent.map_sf_eq_id[where af=af and vf=vf];
    meson order.refl order.trans spec.singleton.seq_ctxt.cl_le_conv)

setup ‹Sign.parent_path›

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

lemma cl:
  shows "spec.term.none (spec.seq_ctxt.cl T P) = spec.seq_ctxt.cl T (spec.term.none P)"
by (rule spec.singleton.antisym)
   (auto simp: spec.singleton.le_conv seq_ctxt.prj_def trace.split_Ex trace.natural_def)

lemma cl_True_False:
  shows "spec.seq_ctxt.cl True (spec.term.none f) = spec.seq_ctxt.cl False (spec.term.none f)"
by (rule spec.singleton.antisym)
   (auto simp: spec.singleton.le_conv seq_ctxt.prj_def trace.split_Ex trace.natural_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term.all.seq_ctxt"›

lemma cl_le:
  shows "spec.seq_ctxt.cl T (spec.term.all P) ≤ spec.term.all (spec.seq_ctxt.cl T P)"
by (metis spec.seq_ctxt.mono_cl spec.term.galois spec.term.lower_upper_contractive spec.term.none.seq_ctxt.cl)

lemma cl_False:
  shows "spec.seq_ctxt.cl False (spec.term.all P) = spec.term.all (spec.seq_ctxt.cl False P)"
by (rule spec.singleton.antisym)
   (auto simp: spec.singleton.le_conv seq_ctxt.prj_def trace.split_Ex trace.natural_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "bind.seq_ctxt"›

lemma cl_le:
  shows "spec.seq_ctxt.cl True f ⤜ (λv. spec.seq_ctxt.cl T (g v)) ≤ spec.seq_ctxt.cl T (f ⤜ g)"
proof(induct rule: spec.bind_le)
  case incomplete show ?case
    by (simp add: spec.seq_ctxt.cl.mono spec.term.none.seq_ctxt.cl)
next
  case (continue σ⇩f σ⇩g v)
  then obtain σ⇩f' σ⇩g'
    where *: "⦉σ⇩f'⦊ ≤ f" "seq_ctxt.equivalent True σ⇩f σ⇩f'"
             "⦉σ⇩g'⦊ ≤ g v" "seq_ctxt.equivalent T σ⇩g σ⇩g'"
    by (clarsimp simp: spec.singleton.seq_ctxt.cl_le_conv)
  let ?σ = "trace.T (trace.init σ⇩f') (trace.rest σ⇩f' @ trace.rest σ⇩g') (trace.term σ⇩g')"
  from continue(2,3) *
  have "⦉?σ⦊ ≤ f ⤜ g"
   by (cases σ⇩f', cases σ⇩g')
      (fastforce intro: spec.bind.continueI[where v=v]  elim: seq_ctxt.equivalent.partial_sel_equivE)
  moreover
  from continue(2,3) *(2,4)
  have "seq_ctxt.equivalent T (trace.T (trace.init σ⇩f) (trace.rest σ⇩f @ trace.rest σ⇩g) (trace.term σ⇩g)) ?σ"
    by (cases σ⇩f, cases σ⇩g, cases σ⇩f', cases σ⇩g') (auto intro: seq_ctxt.equivalent.append)
  ultimately show ?case
    by (auto simp: spec.singleton.seq_ctxt.cl_le_conv)
qed

lemma clL_le:
  shows "spec.seq_ctxt.cl True f ⤜ g ≤ spec.seq_ctxt.cl T (f ⤜ g)"
by (strengthen ord_to_strengthen(2)[OF spec.bind.seq_ctxt.cl_le])
   (rule spec.bind.mono[OF order.refl spec.seq_ctxt.expansive])

lemma clR_le:
  shows "f ⤜ (λv. spec.seq_ctxt.cl T (g v)) ≤ spec.seq_ctxt.cl T (f ⤜ g)"
by (strengthen ord_to_strengthen(2)[OF spec.bind.seq_ctxt.cl_le])
   (rule spec.bind.mono[OF spec.seq_ctxt.expansive order.refl])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "seq_ctxt"›

lemma cl_local_le: ―‹ the RHS is the closure that arises from \<^const>‹spec.local›, ignoring the constraint ›
  shows "spec.seq_ctxt.cl T P ≤ spec.map_invmap.cl _ _ _ id snd id P"
by (fastforce simp: spec.map_invmap.cl_def spec.seq_ctxt.cl_def seq_ctxt.prj_def spec.map.Sup
                    spec.map.singleton spec.singleton.map_le_conv spec.singleton_le_conv
         simp flip: spec.map_invmap.galois)

lemma cl_local:
  shows "spec.local (spec.seq_ctxt.cl T (spec.local.interference ⊓ P))
       = spec.local P" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by (simp add: spec.local_def spec.map_invmap.galois le_infI2 spec.seq_ctxt.cl_local_le
            flip: spec.map_invmap.cl_def)
  show "?rhs ≤ ?lhs"
    unfolding spec.local_def by (strengthen ord_to_strengthen(2)[OF spec.seq_ctxt.expansive]) simp
qed

lemma cl_imp_local_le:
  assumes "spec.local.interference ⊓ P
        ≤ spec.seq_ctxt.cl False (spec.local.interference ⊓ Q)"
  shows "spec.local P ≤ spec.local Q"
by (subst (1 2) spec.seq_ctxt.cl_local[where T=False, symmetric])
   (use assms spec.seq_ctxt.cl[where T=False] in ‹auto intro: spec.local.mono›)

lemma cl_inf_pre:
  shows "spec.pre P ⊓ spec.seq_ctxt.cl T c = spec.seq_ctxt.cl T (spec.pre P ⊓ c)"
by (fastforce simp: spec.singleton.le_conv
             intro: spec.singleton.antisym
              elim: seq_ctxt.equivalent.partial_sel_equivE)

lemma cl_pre_le_conv:
  shows "spec.seq_ctxt.cl T c ≤ spec.pre P ⟷ c ≤ spec.pre P" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  from spec.seq_ctxt.cl_inf_pre[where P=P and c=c, symmetric]
  show "?lhs ⟹ ?rhs"
    by (auto intro: order.trans[OF spec.seq_ctxt.expansive])
  from spec.seq_ctxt.cl_inf_pre[where P=P and c=c, symmetric]
  show "?rhs ⟹ ?lhs"
    by (simp add: inf.absorb_iff2)
qed

lemma cl_inf_post:
  shows "spec.post Q ⊓ spec.seq_ctxt.cl True c = spec.seq_ctxt.cl True (spec.post Q ⊓ c)"
by (fastforce simp: spec.singleton.le_conv
             intro: spec.singleton.antisym
              elim: seq_ctxt.equivalent.partial_sel_equivE
             split: option.split)

lemma cl_post_le_conv:
  shows "spec.seq_ctxt.cl True c ≤ spec.post Q ⟷ c ≤ spec.post Q" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  from spec.seq_ctxt.cl_inf_post[where Q=Q and c=c, symmetric]
  show "?lhs ⟹ ?rhs"
    by (auto intro: order.trans[OF spec.seq_ctxt.expansive])
  from spec.seq_ctxt.cl_inf_post[where Q=Q and c=c, symmetric]
  show "?rhs ⟹ ?lhs"
    by (simp add: inf.absorb_iff2)
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsubsection‹ Permuting local actions\label{sec:local_state-permuting} ›

text‹

We can reorder operations on the local state as these are not observable.

Firstly: an initial action ‹F› that does not change the observable state can be swapped with an
arbitrary action ‹G›.

›

setup ‹Sign.mandatory_path "spec.seq_ctxt"›

lemma cl_action_permuteL_le:
  fixes F  :: "('v × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes G  :: "'v ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes G' :: "('v' × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes F' :: "'v' ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
    ―‹ ‹F› does not change ‹'s›, can be partial ›
  assumes F: "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F⟧ ⟹ snd s' = snd s"
    ―‹ The final state and return value are independent of the order of actions.
        ‹F'› does not change ‹'s›, cannot be partial ›
  assumes FGG'F': "⋀v w a a' s s' t. ⟦P s; (v, a', s, t) ∈ F; (w, a, t, s') ∈ G v⟧
                   ⟹ ∃v' a'' a''' s'' t'. (v', a'', s, t') ∈ G' ∧ (w, a''', t', s'') ∈ F' v'
                          ∧ snd s' = snd t' ∧ (snd s ≠ snd t' ⟶ a'' = a) ∧ (T ⟶ fst s'' = fst s') ∧ snd s'' = snd t'"
  shows "(spec.action F ⤜ (λv. spec.action (G v))) ⊓ spec.pre P
      ≤ spec.seq_ctxt.cl T (spec.action G' ⤜ (λv. spec.action (F' v)))" (is "_ ≤ ?rhs")
unfolding spec.bind.inf_pre
proof(rule order.trans[OF spec.bind.mono[OF spec.pre.inf_action_le(2) order.refl]],
      induct rule: spec.bind_le)
  case incomplete
  from F have "spec.term.none (spec.action (F ∩ UNIV × UNIV × Pre P)) ≤ spec.seq_ctxt.cl T spec.idle"
    by (fastforce intro: spec.term.none.mono[OF spec.action.rel_le]
                   simp: spec.seq_ctxt.cl.idle[where 'w='v])
  also have "... ≤ ?rhs"
    by (simp add: spec.idle_le spec.seq_ctxt.cl.mono)
  finally show ?case .
next
  case (continue σ⇩f σ⇩g v) then show ?case
    apply -
    apply (erule (1) spec.singleton.action_Some_leE)
    apply (erule (1) spec.singleton.action_not_idle_leE)
    apply clarsimp
    apply (frule (1) F)
    apply (frule (2) FGG'F')
    apply (clarsimp simp: spec.singleton.seq_ctxt.cl_le_conv)
    apply (intro exI conjI)
     apply (rule spec.bind.continueI)
      apply (rule spec.action.stepI, assumption, blast)
     apply (rule spec.action.stepI[where w="trace.term σ⇩g"], simp, force)
    apply (clarsimp simp: seq_ctxt.prj_def trace.stuttering.equiv.append_conv
                      trace.stuttering.equiv.simps(3)[where xs="[x]" and ys="[]" for x, simplified])
    apply (rule exI[where x="[]"])
    apply (simp add: image_image trace.natural'.eq_Nil_conv
                     trace_steps'_snd_le_const trace_natural'_took_step_shared_changes)
    apply (intro conjI impI)
    apply (simp add: trace_steps'_snd_le_const)
    done
qed

text‹

Secondly: an initial action ‹G› that does change the observable state can be swapped with an
arbitrary action action ‹F› that does not observably change the state.

›

lemma cl_action_permuteR_le:
  fixes G  :: "('v × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes F  :: "'v ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes F' :: "('v' × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes G' :: "'v' ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
    ―‹ ‹F› does not stall if ‹G› makes an observable state change ›
  assumes G: "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ G; snd s' ≠ snd s⟧
              ⟹ ∃v' w a'' t s''. (v', a'', s, t) ∈ F' ∧ (w, a, t, s'') ∈ G' v' ∧ snd t = snd s ∧ snd s'' = snd s'"
    ―‹ The final state and return value are independent of the order of actions ›
  assumes GFF'G': "⋀v w a a' s s' t. ⟦P s; (v, a, s, t) ∈ G; (w, a', t, s') ∈ F v⟧
                   ⟹ snd s' = snd t ∧ (∃v' a'' a''' s'' t'. (v', a'', s, t') ∈ F' ∧ (w, a''', t', s'') ∈ G' v'
                                                       ∧ snd t' = snd s ∧ (T ⟶ fst s'' = fst s') ∧ snd s'' = snd s' ∧ (snd s'' ≠ snd t' ⟶ a''' = a))"
  shows "(spec.action G ⤜ (λv. spec.action (F v))) ⊓ spec.pre P
      ≤ spec.seq_ctxt.cl T (spec.action F' ⤜ (λv. spec.action (G' v)))"
unfolding spec.bind.inf_pre
proof(rule order.trans[OF spec.bind.mono[OF spec.pre.inf_action_le(2) order.refl]],
      induct rule: spec.bind_le)
  case incomplete show ?case
    unfolding spec.term.galois
  proof(induct rule: spec.action_le)
    case idle show ?case
      by (simp add: spec.idle_le)
  next
    case (step v a s s') then show ?case
    proof(cases "snd s' = snd s")
      case True with step show ?thesis
        by (clarsimp simp: spec.singleton.le_conv intro!: exI[where x=None] exI[where x="trace.T s [] None"])
           (simp add: seq_ctxt.prj_def trace.natural.simps order.trans[OF spec.idle.minimal_le] spec.idle_le)
    next
      case False with step show ?thesis
        by (fastforce simp: spec.singleton.le_conv seq_ctxt.prj_def trace.natural.simps
                      dest: G
                     intro: spec.bind.continueI
                      elim: spec.action.stepI)
    qed
  qed
next
  case (continue σ⇩f σ⇩g v) then show ?case
    apply -
    apply (erule (1) spec.singleton.action_Some_leE)
    apply (erule (1) spec.singleton.action_not_idle_leE)
    apply clarsimp
    apply (drule (2) GFF'G')
    apply (clarsimp simp: spec.singleton.seq_ctxt.cl_le_conv)
    apply (intro exI conjI)
     apply (rule spec.bind.continueI)
      apply (rule spec.action.stepI, assumption, blast)
     apply (rule spec.action.stepI[where w="trace.term σ⇩g"], simp, force)
    apply (clarsimp simp: seq_ctxt.prj_def trace.stuttering.equiv.append_conv
                          trace.stuttering.equiv.simps(1)[where xs="[x]" for x, simplified])
    apply (rule exI)
    apply (rule exI[where x="[]"])
    apply (intro conjI)
      apply simp
     apply (fastforce simp: trace.natural'.eq_Nil_conv
                      dest: trace_natural'_took_step_shared_changes trace_natural'_took_step_shared_same)
    apply (auto simp: trace.natural'.eq_Nil_conv
            simp flip: trace.final'.map[where af=id and sf=snd]
                dest!: arg_cong[where f=snd] trace_natural'_took_step_shared_same)
    done
qed

lemma cl_action_bind_action_pre_post:
  fixes F' :: "('v × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes G' :: "'v ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes Q :: "'w ⇒ ('ls × 's) pred"
  assumes "⋀v w a a' s s' s''. ⟦P s; (v, a, s, s') ∈ F; (w, a', s', s'') ∈ G v⟧ ⟹ Q w s''"
  shows "spec.pre P ⊓ spec.seq_ctxt.cl True (spec.action F ⤜ (λv. spec.action (G v))) ≤ spec.post Q"
unfolding spec.seq_ctxt.cl_inf_pre spec.seq_ctxt.cl_post_le_conv spec.bind.inf_pre
proof(induct rule: spec.bind_le)
  case incomplete show ?case
    by (simp add: spec.term.none.post_le)
next
  case (continue σ⇩f σ⇩g v) with assms show ?case
    by (cases σ⇩f)
       (fastforce simp: spec.singleton.le_conv spec.singleton.action_le_conv trace.steps'.step_conv
                 split: option.split_asm)
qed

lemma cl_rev_kleene_star_action_permute_le:
  fixes F G :: "(unit × 'a × ('ls × 's) × ('ls × 's)) set"
    ―‹ ‹F› does not stall if ‹G› changes the observable state ›
  assumes G: "⋀a s s'. ⟦((), a, s, s') ∈ G; snd s' ≠ snd s⟧
            ⟹ ∃w a'' t s''. ((), a'', s, t) ∈ F ∧ ((), a, t, s'') ∈ G ∧ snd t = snd s ∧ snd s'' = snd s'"
    ―‹ The final state is independent of order of actions, ‹F› does not change ‹'s›, can be partial ›
  assumes GFFG: "⋀a a' s s' t. ⟦((), a, s, t) ∈ G; ((), a', t, s') ∈ F⟧
                       ⟹ snd s' = snd t ∧ (∃a'' a''' t'. ((), a'', s, t') ∈ F ∧ ((), a''', t', s') ∈ G
                                                       ∧ snd t' = snd s ∧ (snd s' ≠ snd t' ⟶ a''' = a))"
  shows "spec.kleene.rev_star (spec.action G) ⤜ (λ_::unit. spec.action F)
      ≤ spec.seq_ctxt.cl True (spec.action F ⪢ spec.kleene.rev_star (spec.action G))" (is "?lhs spec.kleene.rev_star ≤ ?rhs")
proof(induct rule: spec.kleene.rev_star.fixp_induct[where P="λR. ?lhs R ≤ ?rhs", case_names adm bot step])
  case (step S)
  from assms have "S (spec.action G) ⪢ spec.action G ⪢ spec.action F
     ≤ S (spec.action G) ⤜ (λx. spec.seq_ctxt.cl True (spec.action F ⤜ (λv. spec.action G)))"
    by (simp add: spec.bind.bind)
       (strengthen ord_to_strengthen(1)[OF spec.seq_ctxt.cl_action_permuteR_le[where P="⊤" and T=True, simplified]]; force)
  also have "… ≤ ?rhs"
    apply (strengthen ord_to_strengthen(1)[OF spec.bind.seq_ctxt.clR_le])
    apply (subst spec.bind.bind[symmetric])
    apply (strengthen ord_to_strengthen(1)[OF step])
    apply (strengthen ord_to_strengthen(1)[OF spec.bind.seq_ctxt.clL_le[where T=True]])
    apply (strengthen ord_to_strengthen(2)[OF spec.kleene.fold_rev_starR])
    apply (simp add: spec.bind.bind)
    done
  moreover have "spec.return () ⪢ spec.action F ≤ ?rhs"
    apply (simp add: spec.bind.returnL spec.idle_le)
    apply (rule order.trans[OF _ spec.seq_ctxt.expansive])
    apply (rule order.trans[OF _ spec.bind.mono[OF order.refl spec.kleene.epsilon_rev_star_le]])
    apply simp
    done
  ultimately show ?case
    by (simp add: spec.bind.supL)
qed simp_all

lemma cl_local_action_interference_permute_le: ―‹ local actions permute with interference ›
  fixes F :: "(unit × 'a agent × ('ls × 's) × ('ls × 's)) set"
  fixes r :: "'s rel"
    ―‹ ‹F› does not block ›
  assumes "⋀s ls. ∃v a ls'. (v, a, (ls, s), (ls', s)) ∈ F"
    ―‹ ‹F› is insensitive to and does not modify the shared state ›
  assumes "⋀v a s s' s'' ls ls'. (v, a, (ls, s), (ls', s')) ∈ F
                  ⟹ s' = s ∧ (v, a, (ls, s''), (ls', s'')) ∈ F"
  shows "spec.rel (A × (Id ×⇩R r)) ⤜ (λ_::unit. spec.action F)
      ≤ spec.seq_ctxt.cl True (spec.action F ⪢ spec.rel (A × (Id ×⇩R r)))"
by (simp add: spec.rel.monomorphic_conv spec.kleene.star_rev_star spec.rel.act_def)
   (rule spec.seq_ctxt.cl_rev_kleene_star_action_permute_le; use assms in fastforce)

lemma cl_action_mumble_trailing_le:
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F⟧
                  ⟹ ∃a' ls'. (v, a', s, (ls', snd s')) ∈ F'
                             ∧ (snd s' ≠ snd s ⟶ a' = a) ∧ (T ⟶ ls' = fst s')"
  shows "spec.action F ⊓ spec.pre P ≤ spec.seq_ctxt.cl T (spec.action F')"
proof(rule order.trans[OF spec.pre.inf_action_le(2)], induct rule: spec.action_le)
  case idle show ?case
    by (simp add: spec.idle_le)
next
  case (step v a s s')
  then obtain a' ls' where "(v, a', s, (ls', snd s')) ∈ F'" and "snd s' ≠ snd s ⟶ a' = a" and "T ⟶ ls' = fst s'"
    by (blast dest: assms)
  then show ?case
    unfolding spec.singleton.le_conv
    by (fastforce intro: exI[where x="trace.T s [(a', (ls', snd s'))] (Some v)"] spec.action.stepI
                   simp: seq_ctxt.prj_def trace.natural.simps(2)[where xs="[]"])
qed

lemma cl_action_mumbleL_le:
  assumes "⋀w a s s'. ⟦P s; (w, a, s, s') ∈ G⟧
               ⟹ ∃v a' a'' t s''. (v, a', s, t) ∈ F' ∧ (w, a'', t, s'') ∈ G' v
                              ∧ snd t = snd s ∧ (T ⟶ fst s'' = fst s')
                              ∧ snd s'' = snd s' ∧ (snd s'' ≠ snd t ⟶ a'' = a)"
  shows "spec.action G ⊓ spec.pre P ≤ spec.seq_ctxt.cl T (spec.action F' ⤜ (λv. spec.action (G' v)))"
using assms by (fastforce intro!: spec.seq_ctxt.cl_action_permuteR_le[where F="λv. ({v} × UNIV × Id)", simplified spec.return_def[symmetric], simplified])

lemma cl_action_mumbleR_le:
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ G⟧
               ⟹ ∃w a' a'' t. (w, a', s, t) ∈ G' ∧ (v, a'', t, s') ∈ F' w
                              ∧ snd t = snd s' ∧ (snd t ≠ snd s ⟶ a' = a)"
  shows "spec.action G ⊓ spec.pre P ≤ spec.seq_ctxt.cl T (spec.action G' ⤜ (λv. spec.action (F' v)))"
using assms by (fastforce intro!: spec.seq_ctxt.cl_action_permuteL_le[where F="({()} × UNIV × Id)", simplified, simplified spec.idle_le spec.bind.returnL spec.return_def[symmetric]])

lemma cl_action_mumble_expandL_le:
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F⟧ ⟹ snd s' = snd s"
  assumes "⋀v w a a' s s' s''. ⟦P s; (v, a, s, s') ∈ F; (w, a', s', s'') ∈ G v⟧
                 ⟹ ∃s'''. (w, a', s, s''') ∈ G' ∧ snd s''' = snd s'' ∧ (T ⟶ fst s''' = fst s'')"
  shows "(spec.action F ⤜ (λv. spec.action (G v))) ⊓ spec.pre P ≤ spec.seq_ctxt.cl T (spec.action G')"
using assms by (fastforce intro!: spec.seq_ctxt.cl_action_permuteL_le[where F'="λv. ({v} × UNIV × Id)", simplified spec.return_def[symmetric], simplified])

lemma cl_action_mumble_expandR_le:
  assumes "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ G; snd s' ≠ snd s⟧ ⟹ ∃v' s''. (v', a, s, s'') ∈ G' ∧ snd s'' = snd s'"
  assumes "⋀v w a a' s s' t. ⟦P s; (v, a, s, t) ∈ G; (w, a', t, s') ∈ F v⟧
                 ⟹ snd s' = snd t ∧ (∃a'' s''. (w, a'', s, s'') ∈ G' ∧ snd s'' = snd s' ∧ (T ⟶ fst s'' = fst s') ∧ (snd s'' ≠ snd s ⟶ a'' = a))"
  shows "(spec.action G ⤜ (λv. spec.action (F v))) ⊓ spec.pre P ≤ spec.seq_ctxt.cl T (spec.action G')"
using assms by (fastforce intro!: spec.seq_ctxt.cl_action_permuteR_le[where F'="({()} × UNIV × Id)", simplified, simplified spec.idle_le spec.bind.returnL spec.return_def[symmetric]])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.local"›

lemma init_write_interference_permute_le:
  fixes P :: "('a agent, 'ls × 's, 'v) spec"
  shows "spec.local (spec.rel ({env} × UNIV) ⤜ (λ_::unit. spec.write (proc a) (map_prod ⟨ls⟩ id) ⪢ P))
      ≤ spec.local (spec.write (proc a) (map_prod ⟨ls⟩ id) ⪢ (spec.rel ({env} × UNIV) ⤜ (λ_::unit. P)))"
apply (rule spec.seq_ctxt.cl_imp_local_le)
apply (simp add: ac_simps spec.bind.inf_rel spec.action.inf_rel
           flip: spec.rel.inf spec.bind.bind)
apply (rule order.trans[OF _ spec.bind.seq_ctxt.cl_le])
apply (rule spec.bind.mono[OF _ spec.seq_ctxt.expansive])
apply (rule spec.seq_ctxt.cl_local_action_interference_permute_le)
apply auto
done

lemma init_write_interference2_permute_le:
  fixes P :: "('a agent, 'ls × 's, 'v) spec"
  shows "spec.local (spec.rel (A × (Id ×⇩R r)) ⤜ (λ_::unit. spec.write (proc a) (map_prod ⟨ls⟩ id) ⪢ P))
      ≤ spec.local (spec.write (proc a) (map_prod ⟨ls⟩ id) ⪢ (spec.rel (A × (Id ×⇩R r)) ⤜ (λ_::unit. P)))"
apply (rule spec.seq_ctxt.cl_imp_local_le)
apply (simp add: ac_simps spec.bind.inf_rel spec.action.inf_rel
           flip: spec.rel.inf spec.bind.bind)
apply (rule order.trans[OF _ spec.bind.seq_ctxt.cl_le])
apply (rule spec.bind.mono[OF _ spec.seq_ctxt.expansive])
apply (rule spec.seq_ctxt.cl_local_action_interference_permute_le)
apply auto
done

lemma trailing_local_act:
  fixes F :: "'v ⇒ ('w × 'a agent × ('ls × 's) × ('ls × 's)) set"
  shows "spec.local (P ⤜ (λv. spec.action (F v)))
       = spec.local (P ⤜ (λv. spec.action {(w, a, (ls, s), (ls, s')) |w a ls s ls' s'. (w, a, (ls, s), (ls', s')) ∈ F v ∧ (a = env ⟶ ls' = ls)}))" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    apply (rule spec.seq_ctxt.cl_imp_local_le)
    apply (simp add: spec.bind.inf_rel spec.action.inf_rel)
    apply (rule order.trans[OF _ spec.bind.seq_ctxt.clR_le])
    apply (rule spec.bind.mono[OF order.refl])
    apply (rule spec.seq_ctxt.cl_action_mumble_trailing_le[where P=⊤, simplified])
    apply (force simp: spec.local.qrm_def)
    done
  show "?rhs ≤ ?lhs"
    apply (rule spec.seq_ctxt.cl_imp_local_le)
    apply (simp add: spec.bind.inf_rel spec.action.inf_rel)
    apply (rule order.trans[OF _ spec.bind.seq_ctxt.clR_le])
    apply (rule spec.bind.mono[OF order.refl])
    apply (rule spec.seq_ctxt.cl_action_mumble_trailing_le[where P=⊤, simplified])
    apply (force simp: spec.local.qrm_def)
    done
qed

setup ‹Sign.parent_path›


subsection‹ ∗‹spec.localize›\label{sec:local_state-spec_localize} ›

text‹

We can transform a process into one with the same observable behavior that ignores a local state.
For compositionality we allow the ‹env› steps to change the local state but not the ‹self› steps.

›

setup ‹Sign.mandatory_path "spec"›

definition localize :: "'ls rel ⇒ ('a agent, 's, 'v) spec ⇒ ('a agent, 'ls × 's, 'v) spec" where
  "localize r P = spec.rel ({env} × (r ×⇩R UNIV) ∪ range proc × (Id ×⇩R UNIV)) ⊓ spec.sinvmap snd P"

setup ‹Sign.mandatory_path "idle"›

lemma localize_le:
  assumes "spec.idle ≤ P"
  shows "spec.idle ≤ spec.localize r P"
by (simp add: spec.localize_def spec.idle.rel_le spec.idle.invmap_le[OF assms] spec.idle.term.all_le_conv)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "none"›

lemma localize:
  shows "spec.term.none (spec.localize r P) = spec.localize r (spec.term.none P)"
by (simp add: spec.localize_def spec.term.none.inf spec.term.none.inf_none_rel)
   (simp add: spec.term.none.invmap)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "all"›

lemma localize:
  shows "spec.term.all (spec.localize r P) = spec.localize r (spec.term.all P)"
by (simp add: spec.localize_def spec.term.all.rel spec.term.all.inf spec.term.all.invmap)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "closed"›

lemma localize:
  assumes "P ∈ spec.term.closed _"
  shows "spec.localize r P ∈ spec.term.closed _"
by (rule spec.term.closed_clI)
   (simp add: spec.term.all.localize spec.term.all.monomorphic
        flip: spec.term.closed_conv[OF assms, simplified])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "localize"›

lemma singleton:
  fixes σ :: "('a agent, 's, 'v) trace.t"
  shows "spec.localize Id ⦉σ⦊ = (⨆ls::'ls. ⦉trace.map id (Pair ls) id σ⦊)" (is "?lhs = ?rhs")
proof(rule antisym)
  have *: "map (map_prod id (map_prod ⟨ls⟩ id)) xs = xs"
    if "trace.steps' (ls, s) xs ⊆ UNIV × (Id ×⇩R UNIV)"
   for ls s and xs :: "('a agent × ('ls × 's)) list"
    using that by (induct xs arbitrary: s) (auto simp: trace.steps'.Cons_eq_if split: if_split_asm)
  have "∃x. ⦉σ''⦊ ≤ ⦉trace.map id (Pair x) id σ⦊"
    if "⦉trace.map id snd id σ'⦊ ≤ ⦉σ⦊"
   and "σ'' ≤ σ'"
   and "trace.steps' (trace.init σ'') (trace.rest σ'') ⊆ UNIV × (Id ×⇩R UNIV)"
   for σ' σ'' :: "('a agent, 'ls × 's, 'v) trace.t"
    using that
    by - (cases σ'',
          drule spec.singleton.map_le[where  af=id and sf="Pair (fst (trace.init σ''))" and vf=id],
          fastforce dest: * trace.map.mono[where af=id and sf="λx. (fst (trace.init σ''), snd x)" and vf=id] spec.singleton.mono
                   intro: exI[where x="fst (trace.init σ'')"]
                    simp: map_prod_def split_def
               simp flip: id_def)
  then show "?lhs ≤ ?rhs"
    by (simp add: spec.localize_def spec.invmap.singleton inf_Sup spec.singleton.inf_rel
            flip: Times_Un_distrib1)
  show "?rhs ≤ ?lhs"
    by (auto simp: spec.localize_def spec.invmap.singleton spec.singleton.le_conv trace_steps'_map
            intro: exI[where x="trace.map id (Pair a) id σ" for a])
qed

lemma bot:
  shows "spec.localize r ⊥ = ⊥"
by (simp add: spec.localize_def spec.invmap.bot)

lemma top:
  shows "spec.localize r ⊤ = spec.rel ({env} × (r ×⇩R UNIV) ∪ range proc × (Id ×⇩R UNIV))"
by (simp add: spec.localize_def spec.invmap.top)

lemma Sup:
  shows "spec.localize r (⨆X) = (⨆x∈X. spec.localize r x)"
by (simp add: spec.localize_def spec.invmap.Sup inf_Sup image_image)

lemmas sup = spec.localize.Sup[where X="{X, Y}" for X Y, simplified]

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

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

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≤) r"
  assumes "monotone orda (≤) P"
  shows "monotone orda (≤) (λx. spec.localize (r x) (P x))"
using assms by (simp add: monotone_def spec.localize.mono)

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) P"
  shows "mcont luba orda Sup (≤) (λx. spec.localize r (P x))"
using assms by (simp add: spec.localize_def)

lemma bind:
  shows "spec.localize r (f ⤜ g) = spec.localize r f ⤜ (λv. spec.localize r (g v))"
by (simp add: spec.localize_def spec.invmap.bind spec.bind.inf_rel)

lemma action:
  fixes F :: "('v × 'a agent × 's × 's) set"
  shows "spec.localize r (spec.action F)
       = spec.rel ({env} × (r ×⇩R Id))
        ⤜ (λ_::unit. spec.action ((map_prod id (map_prod id (map_prod snd snd)) -` F)
                                    ∩ UNIV × ({env} × (r ×⇩R UNIV) ∪ range proc × (Id ×⇩R UNIV) ∪ UNIV × Id))
        ⤜ (λv. spec.rel ({env} × (r ×⇩R Id)) ⤜ (λ_::unit. spec.return v)))"
by (simp add: spec.localize_def spec.invmap.action spec.bind.inf_rel spec.action.inf_rel_reflcl spec.return.inf_rel
              map_prod_snd_snd_vimage inf_sup_distrib Times_Int_Times relprod_inter
              spec.rel.reflcl
        flip: spec.rel.inf)

lemma return:
  shows "(spec.localize r (spec.return v) :: ('a agent, 'ls × 's, 'v) spec)
       = spec.rel ({env} × (r ×⇩R Id)) ⤜ (λ_::unit. spec.return v)"
apply (simp add: spec.return_def spec.localize.action)
apply (simp add: ac_simps map_prod_vimage_Times inf_sup_distrib1 Times_Int_Times
                 map_prod_snd_snd_vimage relprod_inter relprod_inter_Id spec.idle_le
           flip: spec.return_def)
apply (simp add: sup.absorb1 Sigma_mono
           flip: sup.assoc Times_Un_distrib2)
apply (subst spec.action.return_const[where W="{()}"], simp, simp)
apply (simp add: spec.bind.bind spec.bind.return
           flip: spec.rel.act_def[where r="{env} × (r ×⇩R Id)", simplified ac_simps])
apply (simp add: spec.rel.wind_bind
           flip: spec.rel.unfoldL spec.bind.bind)
done

lemma rel:
  shows "spec.localize r (spec.rel s)
       = spec.rel (({env} × (r ×⇩R UNIV) ∪ range proc × (Id ×⇩R UNIV))
                    ∩ map_prod id (map_prod snd snd) -` (s ∪ UNIV × Id))"
by (simp add: spec.localize_def spec.invmap.rel flip: spec.rel.inf)

lemma rel_le:
  shows "spec.localize Id P ≤ spec.rel (UNIV × (Id ×⇩R UNIV))"
unfolding spec.localize_def by (blast intro: le_infI1 spec.rel.mono)

lemma parallel:
  shows "spec.localize UNIV (P ∥ Q) = spec.localize UNIV P ∥ spec.localize UNIV Q"
by (simp add: spec.localize_def spec.invmap.parallel spec.parallel.inf_rel)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "action"›

lemma localize_le:
  assumes "Id ⊆ r"
  shows "spec.action (map_prod id (map_prod id (map_prod snd snd)) -` F ∩ UNIV × UNIV × (Id ×⇩R UNIV))
      ≤ spec.localize r (spec.action F)"
unfolding spec.localize.action
by (strengthen ord_to_strengthen[OF spec.return.rel_le])
   (use assms in ‹force intro!: spec.action.mono
                          simp: spec.bind.return spec.bind.returnL spec.idle_le›)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference.closed"›

lemma localize:
  assumes "P ∈ spec.interference.closed ({env} × UNIV)"
  shows "spec.localize UNIV P ∈ spec.interference.closed ({env} × UNIV)"
by (force simp: spec.localize_def
         intro: spec.interference.closed.rel subsetD[OF spec.interference.closed.antimono, rotated]
                spec.interference.closed.invmap[where sf=snd and vf=id, OF assms])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "local"›

lemma localize:
  assumes "Id ⊆ r"
  shows "spec.local (spec.localize r P) = P" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by (simp add: ac_simps spec.local_def spec.local.qrm_def spec.localize_def spec.map_invmap.galois)
  from assms show "?rhs ≤ ?lhs"
    by (simp add: spec.local_def spec.local.qrm_def spec.localize_def ac_simps)
       (simp add: spec.map.rel spec.rel.UNIV relprod_inter inf.absorb1
                  inf_sup_distrib Times_Int_Times map_prod_image_Times map_prod_image_relprod
            flip: Sigma_Un_distrib1 spec.map.inf_distr spec.rel.inf)
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec"›

setup ‹Sign.mandatory_path "bind"›

lemma smap_sndL:
  assumes "UNIV × (Id ×⇩R UNIV) ⊆ r"
  shows "spec.smap snd f ⤜ g = spec.smap snd (f ⤜ (λv. spec.rel r ⊓ spec.sinvmap snd (g v)))" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
  proof(induct rule: spec.bind_le)
    case incomplete show ?case by (simp add: spec.map.mono spec.term.none.map)
  next
    case (continue σ⇩f' σ⇩g v)
    from ‹⦉σ⇩f'⦊ ≤ spec.smap snd f›
    obtain σ⇩f
      where *: "⦉σ⇩f⦊ ≤ f" "⦉σ⇩f'⦊ ≤ ⦉trace.map id snd id σ⇩f⦊"
      by (clarsimp simp: spec.singleton.le_conv)
    let ?σ = "trace.T (trace.init σ⇩f)
                      (trace.rest σ⇩f @ map (map_prod id (Pair (fst (trace.final σ⇩f)))) (trace.rest σ⇩g))
                      (trace.term σ⇩g)"
    from continue(3) ‹⦉σ⇩f'⦊ ≤ ⦉trace.map id snd id σ⇩f⦊›
    have "trace.final σ⇩f' = snd (trace.final σ⇩f)"
      by (cases σ⇩f')
         (clarsimp simp flip: trace.final'.map[where af=id and sf=snd]
                        cong: trace.final'.natural'_cong)
    with assms continue(2,3,4) *
    have "⦉?σ⦊ ≤ f ⤜ (λv. spec.rel r ⊓ spec.sinvmap snd (g v))"
      by (cases σ⇩f; cases σ⇩g)
         (force intro!: spec.bind.continueI[where v=v]
                 simp: spec.singleton.le_conv spec.singleton_le_conv trace_steps'_map
                       trace.natural_def comp_def)
    moreover
    from continue(3) ‹⦉σ⇩f'⦊ ≤ ⦉trace.map id snd id σ⇩f⦊›
    have "⦉trace.init σ⇩f', trace.rest σ⇩f' @ trace.rest σ⇩g, trace.term σ⇩g⦊ ≤ ⦉trace.map id snd id ?σ⦊"
      by (clarsimp simp: comp_def spec.singleton_le_conv trace.natural_def trace.natural'.append
                   cong: trace.final'.natural'_cong)
    ultimately show ?case
      by (force simp: spec.singleton.le_conv)
  qed
  show "?rhs ≤ ?lhs"
    by (simp add: spec.bind.mono
                  spec.invmap.bind spec.map_invmap.galois spec.map_invmap.upper_lower_expansive)
qed

lemma smap_sndR:
  assumes "UNIV × (Id ×⇩R UNIV) ⊆ r"
  shows "f ⤜ (λv. spec.smap snd (g v)) = spec.smap snd (spec.rel r ⊓ spec.sinvmap snd f ⤜ g)" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
  proof(induct rule: spec.bind_le)
    case incomplete show ?case
    proof(rule spec.singleton_le_extI)
      show "⦉σ⦊ ≤ ?rhs" if "⦉σ⦊ ≤ spec.term.none f" for σ
        using assms that
        by (cases σ)
           (force simp: comp_def spec.singleton.le_conv trace_steps'_map
                intro!: exI[where x="trace.T (undefined, trace.init σ)
                                             (map (map_prod id (Pair undefined))
                                             (trace.rest σ)) None"]
                        spec.bind.incompleteI)
    qed
  next
    case (continue σ⇩f σ⇩g' v)
    from ‹⦉σ⇩g'⦊ ≤ spec.smap snd (g v)›
    obtain σ⇩g
      where "⦉σ⇩g⦊ ≤ g v" and "⦉σ⇩g'⦊ ≤ ⦉trace.map id snd id σ⇩g⦊"
      by (clarsimp simp: spec.singleton.le_conv)
    let ?σ = "trace.T (fst (trace.init σ⇩g), trace.init σ⇩f)
                      (map (map_prod id (Pair (fst (trace.init σ⇩g)))) (trace.rest σ⇩f) @ trace.rest σ⇩g)
                      (trace.term σ⇩g)"
    from continue(2) ‹⦉σ⇩g'⦊ ≤ ⦉trace.map id snd id σ⇩g⦊›
    have "snd (trace.init σ⇩g) = trace.final σ⇩f"
      by (metis spec.singleton_le_conv trace.less_eqE trace.natural.sel(1) trace.t.map_sel(1))
    with assms continue(1,3) ‹⦉σ⇩g⦊ ≤ g v›
    have "⦉?σ⦊ ≤ spec.rel r ⊓ spec.sinvmap snd f ⤜ g"
      by (cases σ⇩f, cases σ⇩g)
         (rule spec.bind.continueI[where v=v];
          force simp: spec.singleton.le_conv comp_def trace_steps'_map trace.final'.map)
    moreover
    from continue(2) ‹⦉σ⇩g'⦊ ≤ ⦉trace.map id snd id σ⇩g⦊›
    have "⦉trace.init σ⇩f, trace.rest σ⇩f @ trace.rest σ⇩g', trace.term σ⇩g'⦊ ≤ ⦉trace.map id snd id ?σ⦊"
      by (cases σ⇩f)
         (clarsimp simp: comp_def spec.singleton_le_conv trace.natural_def trace.natural'.append;
          metis order_le_less same_prefix_prefix trace.less_eqE trace.less_eq_None(2) trace.t.sel(1) trace.t.sel(2) trace.t.sel(3))
    ultimately show ?case
      by (force simp: spec.singleton.le_conv)
  qed
  show "?rhs ≤ ?lhs"
    by (simp add: spec.bind.mono
                  spec.invmap.bind spec.map_invmap.galois spec.map_invmap.upper_lower_expansive)
qed

lemma localL:
  shows "spec.local f ⤜ g = spec.local (f ⤜ (λv. spec.localize Id (g v)))"
unfolding spec.local_def spec.localize_def spec.local.qrm_def
by (subst spec.bind.smap_sndL[where r="{env} × (Id ×⇩R UNIV) ∪ range proc × (Id ×⇩R UNIV)"];
    fastforce simp: ac_simps spec.bind.inf_rel inf_sup_distrib1 Times_Int_Times
         simp flip: spec.rel.inf)

lemma localR:
  shows "f ⤜ (λv. spec.local (g v)) = spec.local (spec.localize Id f ⤜ g)"
unfolding spec.local_def spec.localize_def spec.local.qrm_def
by (subst spec.bind.smap_sndR[where r="{env} × (Id ×⇩R UNIV) ∪ range proc × (Id ×⇩R UNIV)"];
    fastforce simp: ac_simps spec.bind.inf_rel inf_sup_distrib1 Times_Int_Times
         simp flip: spec.rel.inf)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "local"›

setup ‹Sign.mandatory_path "cam"›

lemma cl_le:
  shows "spec.local (spec.cam.cl ({env} × (s ×⇩R r)) P) ≤ spec.cam.cl ({env} × r) (spec.local P)"
unfolding spec.cam.cl_def spec.local.sup spec.term.all.local spec.term.none.local[symmetric]
by (fastforce intro: le_supI2 spec.term.none.mono spec.bind.mono spec.rel.mono
          simp flip: spec.map_invmap.galois spec.rel.inf
               simp: spec.local_def spec.map_invmap.galois spec.bind.inf_rel spec.invmap.bind spec.invmap.rel)

lemma cl:
  assumes "Id ⊆ r⇩l"
  shows "spec.local (spec.cam.cl ({env} × (r⇩l ×⇩R r)) P)
       = spec.cam.cl ({env} × r) (spec.local P)" (is "?lhs = ?rhs")
proof(rule antisym[OF spec.local.cam.cl_le])
  have "spec.local (spec.term.all P) ⪢ spec.rel ({env} × r)
     ≤ spec.local (spec.term.all P ⪢ spec.rel ({env} × (r⇩l ×⇩R r)))"
  proof(induct rule: spec.bind_le)
    case incomplete show ?case
      by (simp add: spec.term.none.local spec.local.mono order.trans[OF _ spec.term.none.bindL_le])
  next
    case (continue σ⇩f σ⇩g v)
    from ‹trace.term σ⇩f = Some v› ‹⦉σ⇩f⦊ ≤ spec.local (spec.term.all P)›
    obtain s xs w
      where P: "⦉s, xs, w⦊ ≤ P"
               "trace.steps' s xs ⊆ spec.local.qrm"
               "⦉σ⇩f⦊ ≤ ⦉snd s, map (map_prod id snd) xs, trace.term σ⇩f⦊"
      by (clarsimp simp: spec.singleton.local_le_conv spec.singleton.le_conv spec.singleton_le_conv
                         trace.split_all trace.natural_def)
    let ?σ = "trace.T s
                      (xs @ map (map_prod id (Pair (fst (trace.final' s xs)))) (trace.rest σ⇩g))
                      (trace.term σ⇩g)"
    from assms continue(2,3,4) P(1,3)
    have "⦉?σ⦊ ≤ spec.term.all P ⤜ (λ_::'g. spec.rel ({env} × (r⇩l ×⇩R r)))"
      by (cases σ⇩f)
         (fastforce intro: spec.bind.continueI
                     simp: spec.singleton.le_conv trace.steps'.map(1)[where af=id and sf="Pair (fst (trace.final' s xs))" and s="snd (trace.final' s xs)", simplified]
                simp flip: trace.final'.map[where af=id and sf=snd]
                     cong: trace.final'.natural'_cong)
    moreover
    from continue(2,3,4) P(2,3)
    have "trace.steps' (trace.init ?σ) (trace.rest ?σ) ⊆ spec.local.qrm"
      by (fastforce simp: spec.singleton.le_conv spec.singleton_le_conv trace.natural_def trace.natural'.append
                          trace.steps'.append trace.steps'.map(1)[where af=id and sf="Pair (fst (trace.final' s xs))" and s="snd (trace.final' s xs)", simplified]
               simp flip: trace.final'.map[where af=id and sf=snd]
                    cong: trace.final'.natural'_cong)
    moreover
    from ‹trace.term σ⇩f = Some v› ‹⦉σ⇩f⦊ ≤ ⦉snd s, map (map_prod id snd) xs, trace.term σ⇩f⦊›
    have "⦉trace.init σ⇩f, trace.rest σ⇩f @ trace.rest σ⇩g, trace.term σ⇩g⦊ ≤ ⦉trace.map id snd id ?σ⦊"
      by (cases σ⇩f)
         (simp add: spec.singleton_le_conv trace.natural'.append trace.natural_def comp_def
              cong: trace.final'.natural'_cong)
    ultimately show ?case
      by (force simp: spec.singleton.local_le_conv spec.singleton.le_conv)
  qed
  then show "?rhs ≤ ?lhs"
    by (auto simp: spec.cam.cl_def spec.local.sup spec.term.all.local
        simp flip: spec.term.none.local
            intro: le_supI2 spec.term.none.mono)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "cam.closed"›

lemma local:
  assumes "Id ⊆ s"
  assumes "P ∈ spec.cam.closed ({env} × (s ×⇩R r))"
  shows "spec.local P ∈ spec.cam.closed ({env} × r)"
by (metis spec.cam.closed spec.cam.closed_conv[OF assms(2)] spec.local.cam.cl[OF assms(1)])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference"›

lemma cl_le:
  shows "spec.local (spec.interference.cl ({env} × (s ×⇩R r)) P)
      ≤ spec.interference.cl ({env} × r) (spec.local P)"
by (force intro: spec.interference.cl.mono
           simp: spec.local_def spec.map_invmap.upper_lower_expansive spec.map_invmap.galois
                 spec.invmap.interference.cl spec.interference.cl.inf_rel)

lemma cl:
  assumes "Id ⊆ s"
  shows "spec.local (spec.interference.cl ({env} × (s ×⇩R r)) P)
       = spec.interference.cl ({env} × r) (spec.local P)"
apply (rule antisym[OF spec.local.interference.cl_le])
apply (simp add: spec.interference.cl_def spec.bind.bind spec.bind.localL spec.bind.localR
                 spec.invmap.bind spec.invmap.return spec.invmap.rel
           flip: spec.local.cam.cl[OF order.refl])
apply (simp add: spec.localize.bind spec.localize.rel spec.localize.return)
apply (simp add: spec.rel.wind_bind_trailing flip: spec.bind.bind)
apply (simp add: ac_simps inf_sup_distrib1 map_prod_vimage_Times Times_Int_Times
                 map_prod_snd_snd_vimage relprod_inter spec.rel.reflcl spec.rel.Id UNIV_unit)
apply (intro spec.local.mono spec.bind.mono spec.rel.mono spec.cam.cl.mono)
using assms apply force+
done

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference.closed"›

lemma local:
  assumes "P ∈ spec.interference.closed ({env} × (Id ×⇩R r))"
  shows "spec.local P ∈ spec.interference.closed ({env} × r)"
by (rule spec.interference.closed_clI)
   (simp flip: spec.interference.closed_conv[OF assms] spec.local.interference.cl[OF order.refl])

lemma local_UNIV:
  assumes "P ∈ spec.interference.closed ({env} × UNIV)"
  shows "spec.local P ∈ spec.interference.closed ({env} × UNIV)"
proof -
  have *: "{env} × (Id ×⇩R UNIV) ⊆ {env} × UNIV" by blast
  show ?thesis
    by (rule spec.interference.closed_clI)
       (simp flip: spec.interference.closed_conv[OF subsetD[OF spec.interference.closed.antimono[OF *] assms]]
                   spec.local.interference.cl[OF order.refl])
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ ∗‹spec.local\_init›\label{sec:local_state-spec_local_init} ›

setup ‹Sign.mandatory_path "spec"›

definition local_init :: "'a ⇒ 'ls ⇒ ('a agent, 'ls × 's, 'v) spec ⇒ ('a agent, 's, 'v) spec" where
  "local_init a ls P = spec.local (spec.write (proc a) (map_prod ⟨ls⟩ id) ⪢ P)"

setup ‹Sign.mandatory_path "singleton"›

lemma local_init_le_conv:
  shows "⦉σ⦊ ≤ spec.local_init a ls P
         ⟷ ⦉σ⦊ ≤ spec.idle ∨ (∃σ'. ⦉σ'⦊ ≤ P
                                  ∧ trace.steps σ' ⊆ spec.local.qrm
                                  ∧ ⦉σ⦊ ≤ ⦉trace.map id snd id σ'⦊
                                  ∧ fst (trace.init σ') = ls)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  assume ?lhs
  then obtain σ'
        where "⦉σ'⦊ ≤ spec.write (proc a) (map_prod ⟨ls⟩ id) ⪢ P"
          and "trace.steps' (trace.init σ') (trace.rest σ') ⊆ spec.local.qrm"
          and "⦉σ⦊ ≤ ⦉trace.map id snd id σ'⦊"
    by (clarsimp simp: spec.local_init_def spec.singleton.local_le_conv)
  then show ?rhs
  proof(induct rule: spec.singleton.bind_le)
    case incomplete then show ?case
      by (cases σ')
         (rule disjI1;
          fastforce simp: spec.singleton.le_conv spec.singleton.action_le_conv trace.steps'.step_conv
          elim!: order.trans)
  next
    case (continue σ⇩f σ⇩g v⇩f) then show ?case
      by (cases σ⇩g)
         (rule disjI2; erule (1) spec.singleton.action_Some_leE;
          force simp: exI[where x=σ⇩g] spec.singleton.le_conv image_image
                      trace.steps'.append trace_steps'_snd_le_const)
  qed
next
  show "?rhs ⟹ ?lhs"
    by (fastforce simp: spec.local_init_def spec.idle_le trace.split_all spec.singleton.local_le_conv
                intro!: spec.bind.continueI[where xs="[]", simplified] spec.action.stutterI
                 elim!: order.trans)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "idle"›

lemma local_init_le[spec.idle_le]:
  shows "spec.idle ≤ spec.local_init a ls P"
by (simp add: spec.local_init_def spec.idle_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "local_init"›

lemma Sup:
  shows "spec.local_init a ls (⨆X) = (⨆x∈X. spec.local_init a ls x) ⊔ spec.idle"
apply (simp add: spec.local_init_def spec.local.Sup spec.local.sup image_image
                 spec.bind.SUPR(1)[where X=X and g=pred_K, simplified]
                 spec.bind.botR spec.local.action
           flip: bot_fun_def spec.term.none.local)
apply (subst spec.return.cong, force, force)
apply (simp add: spec.term.none.return spec.term.none.Sup spec.term.none.sup spec.term.none.idle
                 sup.absorb2)
done

lemma Sup_not_empty:
  assumes "X ≠ {}"
  shows "spec.local_init a ls (⨆X) = (⨆x∈X. spec.local_init a ls x)"
by (subst spec.local_init.Sup) (meson assms spec.local_init.Sup sup.absorb1 SUPI spec.idle_le ex_in_conv)

lemmas sup = spec.local_init.Sup_not_empty[where X="{X, Y}" for X Y, simplified]

lemma bot:
  shows "spec.local_init a ls ⊥ = spec.idle"
using spec.local_init.Sup[where X="{}"] by simp

lemma top:
  shows "spec.local_init a ls ⊤ = (⊤ :: ('a agent, 's, 'v) spec)"
proof -
  have "⦉σ⦊ ≤ spec.local_init a ls ⊤" for σ :: "('a agent, 's, 'v) trace.t"
    by (fastforce simp: spec.local_init_def spec.local.qrm_def spec.singleton.local_le_conv trace.steps'.map comp_def
                 intro: exI[where x="trace.T (ls, trace.init σ) (map (map_prod id (Pair ls)) (trace.rest σ)) (trace.term σ)"]
                        spec.bind.continueI[where xs="[]", simplified] spec.action.stutterI)
  then show ?thesis
    by (fastforce intro: top_le spec.singleton_le_extI simp: spec.local_init_def)
qed

lemma monotone:
  shows "mono (spec.local_init a ls :: ('a agent, 'ls × 's, 'v) spec ⇒ _)"
proof(rule monotoneI)
  show "spec.local_init a ls P ≤ spec.local_init a ls P'" if "P ≤ P'" for P P' :: "('a agent, 'ls × 's, 'v) spec"
    unfolding spec.local_init_def by (strengthen ord_to_strengthen(1)[OF ‹P ≤ P'›]) simp
qed

lemmas strengthen[strg] = st_monotone[OF spec.local_init.monotone]
lemmas mono = monotoneD[OF spec.local_init.monotone]

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≤) P"
  shows "monotone orda (≤) (λx. spec.local_init a ls (P x))"
by (simp add: monotone2monotone[OF spec.local_init.monotone assms])

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) P"
  shows "mcont luba orda Sup (≤) (λx. spec.local_init a ls (P x))"
by (simp add: spec.local_init_def assms)

lemma action:
  fixes F  :: "('v × 'a agent × ('ls × 's) × ('ls × 's)) set"
  shows "spec.local_init a ls (spec.action F)
       = spec.action {(v, a, s, s') |v a ls' s s'. (v, a, (ls, s), (ls', s')) ∈ F ∧ (a = env ⟶ ls' = ls)}" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    apply (subst (3) spec.local.localize[where r=UNIV, symmetric], simp)
    apply (simp add: spec.local_init_def)
    apply (rule spec.seq_ctxt.cl_imp_local_le)
    apply (simp add: spec.localize.action spec.bind.inf_rel spec.action.inf_rel spec.return.inf_rel)
    apply (strengthen ord_to_strengthen(2)[OF spec.return.rel_le])
    apply (fastforce intro: spec.seq_ctxt.cl_action_mumble_expandL_le[where P=⊤, simplified]
                      simp: spec.local.qrm_def spec.bind.returnL spec.idle_le)
    done
  show "?rhs ≤ ?lhs"
    apply (subst (1) spec.local.localize[where r=UNIV, symmetric], simp)
    apply (simp add: spec.local_init_def)
    apply (rule spec.seq_ctxt.cl_imp_local_le)
    apply (simp add: spec.localize.action spec.bind.inf_rel spec.action.inf_rel spec.return.inf_rel
                     spec.rel.Id spec.bind.returnL spec.idle_le UNIV_unit
               flip: spec.rel.inf)
    apply (fastforce intro: spec.seq_ctxt.cl_action_mumbleL_le[where P=⊤, simplified]
                      simp: spec.local.qrm_def)
    done
qed

lemma return:
  shows "spec.local_init a ls (spec.return v) = spec.return v"
by (auto simp: spec.local_init.action spec.return_def intro: arg_cong[where f=spec.action])

lemma localize_le:
  assumes "spec.idle ≤ P"
  shows "spec.local_init a ls (spec.localize r P) ≤ P"
unfolding spec.local_init_def spec.localize_def
apply (rule order.trans[OF spec.local.bind_le])
apply (simp add: spec.local.action)
apply (subst spec.return.cong, force, force)
apply (simp add: assms spec.bind.SupL spec.bind.supL
                 spec.bind.returnL spec.idle.local_le spec.idle.invmap_le spec.idle.rel_le)
apply (simp add: le_infI2 spec.local_def spec.map_invmap.galois)
done

lemma localize:
  assumes "spec.idle ≤ P"
  assumes "Id ⊆ r"
  shows "spec.local_init a ls (spec.localize r P) = P" (is "?lhs = ?rhs")
proof(rule antisym[OF spec.local_init.localize_le[OF assms(1)] spec.singleton_le_extI])
  show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
    using that
    by (cases σ)
       (fastforce simp: spec.local_init_def spec.localize_def spec.local.qrm_def comp_def
                        spec.singleton.le_conv spec.singleton.local_le_conv trace_steps'_map
                 intro: exI[where x="trace.map id (Pair ls) id σ"] subsetD[OF ‹Id ⊆ r›]
                        spec.bind.continueI[where xs="[]", simplified] spec.action.stutterI)
qed

lemma inf_interference:
  shows "spec.local_init a ls P = spec.local_init a ls (P ⊓ spec.local.interference)"
unfolding spec.local_init_def
by (subst spec.local.inf_interference)
   (auto simp: ac_simps spec.bind.inf_rel spec.action.inf_rel
        intro: arg_cong[where f="λx. spec.local (spec.action x ⤜ (λx. P ⊓ spec.local.interference))"])

lemma eq_local:
  assumes "spec.idle ≤ P"
  shows "(⨆ls. spec.local_init a ls P) = spec.local P"
proof -
  have "spec.local (spec.action {((), proc a, (ls, s), ls', s) |ls' ls s. True} ⪢ P)
      = spec.local P" (is "?lhs = ?rhs")
proof(rule antisym)
  have "?rhs = spec.return () ⪢ ?rhs"
    by (simp add: spec.bind.returnL assms spec.idle.local_le)
  also have "… = spec.smap snd (spec.sinvmap snd (spec.return ()) ⪢ spec.rel spec.local.qrm ⊓ P)"
    by (simp add: spec.local_def spec.bind.smap_sndR[where r=UNIV, simplified spec.rel.UNIV])
  also have "?lhs ≤ …"
    by (force intro: spec.map.mono spec.bind.mono le_infI2 spec.action.rel_le
               simp: spec.local_def spec.invmap.return spec.bind.bind spec.bind.return spec.bind.inf_rel)
  finally show "?lhs ≤ ?rhs" .
  show "?rhs ≤ ?lhs"
    by (force simp: assms
             intro: spec.local.mono order.trans[OF spec.bind.returnL_le[where g="⟨P⟩" and v="()"]]
                    spec.return.action_le spec.bind.mono)
  qed
  then show ?thesis
    by (simp add: spec.local_init_def UNION_eq
            flip: spec.local.Sup[where X="(λls. spec.write (proc a) (map_prod ⟨ls⟩ id) ⪢ P) ` UNIV", simplified, simplified image_image]
                  spec.bind.SUPL spec.action.SUP_not_empty)
qed

lemma ag_le:
  shows "spec.local_init a ls (⦃P⦄, Id ×⇩R A ⊢ UNIV ×⇩R G, ⦃λv s. Q v (snd s)⦄)
      ≤ ⦃λs. P (ls, s)⦄, A ⊢ G, ⦃Q⦄"
apply (subst ag.reflcl_a)
apply (simp add: spec.local_init_def spec.local_def spec.local.qrm_def
                 spec.map_invmap.galois spec.invmap.ag map_prod_snd_snd_vimage)
apply (subst inf.commute)
apply (subst heyting[symmetric])
apply (subst sup.commute, subst ag.assm_heyting)
apply (force intro: ag.spec.bind[rotated] ag.spec.action[where Q="λ_. FST ((=) ls) ❙∧ P"] ag.mono)
done

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "bind"›

lemma local_initL:
  shows "spec.local_init a ls f ⤜ g = spec.local_init a ls (f ⤜ (λv. spec.localize Id (g v)))"
by (simp add: spec.local_init_def spec.bind.localL spec.bind.bind)

lemma local_initR:
  shows "f ⤜ (λv. spec.local_init a ls (g v)) = spec.local_init a ls (spec.localize Id f ⤜ g)"
oops

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "sinvmap"›

lemma local_init:
  fixes P :: "('a agent, 'ls × 't, 'v) spec"
  fixes sf :: "'s ⇒ 't"
  shows "spec.sinvmap sf (spec.local_init a ls P)
       = spec.local_init a ls (spec.rel (UNIV × (Id ×⇩R map_prod sf sf -` Id))
                                 ⤜ (λ_::unit. spec.sinvmap (map_prod id sf) P))" (is "?lhs = ?rhs")
proof(rule antisym)
  let ?r = "UNIV × (Id ×⇩R map_prod sf sf -` Id)"
  have "?lhs = spec.local (spec.rel ?r ⤜
                 (λ_::unit. spec.action ({((), proc a, (ls', s), ls, s') |ls' s s'. sf s = sf s'}) ⤜
                   (λ_::unit. spec.rel ?r ⤜ (λ_::unit. spec.sinvmap (map_prod id sf) P))))"
    by (simp add: spec.local_init_def spec.invmap.local spec.invmap.bind spec.invmap.action
                  spec.bind.bind map_prod_conv map_prod_map_prod_vimage_Id)
  also have "… ≤ spec.local (spec.rel ?r ⤜
                    (λ_::unit. spec.write (proc a) (map_prod ⟨ls⟩ id) ⤜
                      (λ_::unit. spec.rel.act ?r ⤜
                        (λ_::unit. spec.rel ?r ⤜ (λ_::unit. spec.sinvmap (map_prod id sf) P)))))"
    apply (rule spec.seq_ctxt.cl_imp_local_le)
    apply (simp add: ac_simps spec.bind.inf_rel spec.action.inf_rel spec.rel.act_def flip: spec.rel.inf)
    apply (subst (4) spec.bind.bind[symmetric])
    apply ( (rule spec.seq_ctxt.cl_action_mumbleL_le[where P="⊤", simplified]; force)
          | rule order.trans[OF spec.bind.mono spec.bind.seq_ctxt.cl_le] spec.seq_ctxt.expansive )+
    done
  also have "… = spec.local (spec.rel ?r ⤜
                    (λ_::unit. spec.write (proc a) (map_prod ⟨ls⟩ id) ⤜
                      (λ_::unit. spec.rel ?r ⤜ (λ_::unit. spec.sinvmap (map_prod id sf) P))))"
    by (simp add: spec.rel.wind_bind flip: spec.bind.bind spec.rel.unfoldL)
  also have "… ≤ spec.local (spec.write (proc a) (map_prod ⟨ls⟩ id) ⤜
                    (λ_::unit. spec.rel ?r ⤜
                      (λ_::unit. spec.rel ?r ⤜ (λ_::unit. spec.sinvmap (map_prod id sf) P))))"
    by (rule spec.local.init_write_interference2_permute_le)
  also have "… = spec.local (spec.write (proc a) (map_prod ⟨ls⟩ id) ⤜
                    (λ_::unit. spec.rel ?r ⤜ (λ_::unit. spec.sinvmap (map_prod id sf) P)))"
    by (simp add: spec.rel.wind_bind flip: spec.bind.bind)
  also have "… = ?rhs"
    by (simp add: spec.local_init_def)
  finally show "?lhs ≤ ?rhs" .
  show "?rhs ≤ ?lhs"
    by (fastforce simp: spec.local_init_def spec.invmap.local spec.invmap.bind spec.invmap.action
                        map_prod_conv spec.bind.bind map_prod_map_prod_vimage_Id
                 intro: spec.local.mono order.trans[OF _ spec.bind.relL_le] spec.bind.mono spec.action.mono)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "vmap"›

lemma local_init:
  shows "spec.vmap vf (spec.local_init a ls P) = spec.local_init a ls (spec.vmap vf P)"
by (simp add: spec.local_init_def spec.vmap.local spec.map.bind_inj_sf spec.map.id)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "vinvmap"›

lemma local_init:
  shows "spec.vinvmap vf (spec.local_init a ls P) = spec.local_init a ls (spec.vinvmap vf P)"
by (simp add: spec.local_init_def spec.invmap.local spec.invmap.bind spec.invmap.action spec.rel.Id UNIV_unit
              spec.bind.returnL spec.idle_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term.none"›

lemma local_init:
  shows "spec.term.none (spec.local_init a ls P) = spec.local_init a ls (spec.term.none P)"
by (simp add: spec.local_init_def spec.term.none.local spec.term.none.bind)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term.all"›

lemma local_init:
  shows "spec.term.all (spec.local_init a ls P)
       = spec.local_init a ls (spec.term.all P) ⊔ ⨆range spec.return"
apply (simp add: spec.local_init_def spec.term.all.local spec.term.all.bind spec.term.all.action
                 spec.local.Sup spec.local.sup spec.local.action spec.local.return image_image ac_simps)
apply (subst (2) spec.return.cong, force, force intro!: exI[where x="proc a"])
apply (rule antisym; clarsimp simp: le_supI1 le_supI2 SUP_upper SUP_upper2 spec.idle_le)
done

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference.closed"›

lemma local_init:
  assumes "P ∈ spec.interference.closed ({env} × (Id ×⇩R r))"
  shows "spec.local_init a ls P ∈ spec.interference.closed ({env} × r)"
by (rule spec.interference.closed_clI)
   (simp add: spec.local_init_def spec.bind.bind spec.interference.cl.action
              spec.interference.cl.bindR[OF assms] spec.interference.closed.bind_relL[OF assms]
              order.trans[OF spec.local.init_write_interference2_permute_le[simplified]]
        flip: spec.local.interference.cl[where s=Id])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Hoist to ∗‹('s, 'v) prog›\label{sec:local_state-prog} ›

setup ‹Sign.mandatory_path "prog"›

lift_definition local :: "('ls × 's, 'v) prog ⇒ ('s, 'v) prog" is spec.local
by (blast intro: spec.interference.closed.local subsetD[OF spec.interference.closed.antimono, rotated])

definition local_init :: "'ls ⇒ ('ls × 's, 'v) prog ⇒ ('s, 'v) prog" where
  "local_init ls P = prog.local (prog.write (map_prod ⟨ls⟩ id) ⪢ P)"
  ―‹ equivalent to lifting \<^const>‹spec.local_init›; see ‹prog.p2s.local_init› ›

lift_definition localize :: "('s, 'v) prog ⇒ ('ls × 's, 'v) prog" is "spec.localize UNIV"
by (rule spec.interference.closed.localize)

setup ‹Sign.mandatory_path "p2s"›

lemmas local[prog.p2s.simps] = prog.local.rep_eq

lemma local_init[prog.p2s.simps]:
  shows "prog.p2s (prog.local_init ls P) = spec.local_init () ls (prog.p2s P)" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by (simp add: prog.local_init_def spec.local_init_def
                  prog.p2s.simps prog.p2s.action prog.p2s.interference_wind_bind
                  map_prod_image_Collect spec.interference.cl.action spec.bind.bind
                  order.trans[OF spec.local.init_write_interference_permute_le[simplified]])
  show "?rhs ≤ ?lhs"
    by (simp add: prog.local_init_def spec.local_init_def prog.p2s.simps prog.p2s.action
                  map_prod_image_Collect
                  spec.local.mono[OF spec.bind.mono[OF spec.interference.expansive order.refl]])
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "local"›

lemma Sup:
  shows "prog.local (⨆X) = (⨆x∈X. prog.local x)"
by transfer
   (simp add: spec.local.Sup spec.local.sup spec.interference.cl.bot spec.local.interference
        flip: spec.term.none.local)

lemmas sup = prog.local.Sup[where X="{X, Y}" for X Y, simplified]

lemma bot:
  shows "prog.local ⊥ = ⊥"
using prog.local.Sup[where X="{}"] by simp

lemma top:
  shows "prog.local ⊤ = ⊤"
by transfer (simp add: spec.local.top)

lemma monotone:
  shows "mono prog.local"
by (rule monotoneI) (transfer; erule monotoneD[OF spec.local.monotone])

lemmas strengthen[strg] = st_monotone[OF prog.local.monotone]
lemmas mono = monotoneD[OF prog.local.monotone]
lemmas mono2mono[cont_intro, partial_function_mono]
  = monotone2monotone[OF prog.local.monotone, simplified, of orda P for orda P]

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) P"
  shows "mcont luba orda Sup (≤) (λx. prog.local (P x))"
proof(rule mcontI)
  from assms show "monotone orda (≤) (λx. prog.local (P x))"
    by (blast intro: mcont_mono prog.local.mono2mono)
  from assms show "cont luba orda Sup (≤) (λx. prog.local (P x))"
    by (fastforce intro: contI dest: mcont_cont contD simp: prog.local.Sup image_image)
qed

lemma bind_botR:
  shows "prog.local (P ⤜ ⊥) = prog.local P ⤜ ⊥"
by (simp add: prog.p2s.simps spec.interference.cl.bot bot_fun_def
              spec.interference.closed.bind_relR spec.interference.closed.local_UNIV
        flip: spec.bind.botR prog.p2s_inject)
   (simp add: spec.bind.localL spec.localize.bot)

lemma action:
  shows "prog.local (prog.action F) = prog.action (map_prod id (map_prod snd snd) ` F)"
by transfer
   (force simp: spec.local.interference.cl[OF subset_UNIV, where r=UNIV, simplified] spec.local.action
         intro: arg_cong[where f="λF. spec.interference.cl ({env} × UNIV) (spec.action F)"])

lemma return:
  shows "prog.local (prog.return v) = prog.return v"
by (simp add: prog.return_def prog.local.action map_prod_image_Times map_prod_snd_snd_image_Id)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "local_init"›

lemma transfer[transfer_rule]:
  shows "rel_fun (=) (rel_fun cr_prog cr_prog) (spec.local_init ()) prog.local_init"
by (simp add: cr_prog_def prog.p2s.local_init rel_fun_def)

lemma Sup:
  shows "prog.local_init ls (⨆X) = (⨆x∈X. prog.local_init ls x)"
by (simp add: prog.local_init_def prog.bind.SupR prog.local.Sup prog.local.sup image_image
                 prog.local.bind_botR prog.local.action)
   (subst prog.return.cong; force simp: prog.bind.returnL)

lemmas sup = prog.local_init.Sup[where X="{X, Y}" for X Y, simplified]

lemma bot[simp]:
  shows "prog.local_init ls ⊥ = ⊥"
using prog.local_init.Sup[where ls=ls and X="{}"] by simp

lemma top:
  shows "prog.local_init ls ⊤ = ⊤"
by (simp add: prog.p2s.simps spec.local_init.top flip: prog.p2s_inject)

lemma monotone:
  shows "mono (prog.local_init ls)"
unfolding prog.local_init_def by simp

lemmas strengthen[strg] = st_monotone[OF prog.local_init.monotone]
lemmas mono = monotoneD[OF prog.local_init.monotone]

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≤) P"
  shows "monotone orda (≤) (λx. prog.local_init ls (P x))"
by (simp add: monotone2monotone[OF prog.local_init.monotone assms])

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) P"
  shows "mcont luba orda Sup (≤) (λx. prog.local_init ls (P x))"
proof(rule mcontI)
  from assms show "monotone orda (≤) (λx. prog.local_init ls (P x))"
    by (blast intro: mcont_mono prog.local_init.mono2mono)
  from assms show "cont luba orda Sup (≤) (λx. prog.local_init ls (P x))"
    by (fastforce intro: contI dest: mcont_cont contD simp: prog.local_init.Sup image_image)
qed

lemma bind_botR:
  shows "prog.local_init ls (P ⤜ ⊥) = prog.local_init ls P ⤜ ⊥"
by (simp add: prog.local_init_def prog.local.bind_botR flip: prog.bind.bind)

lemma return:
  shows "prog.local_init ls (prog.return v) = prog.return v" (is "?lhs = ?rhs")
proof -
  have "prog.p2s ?rhs = spec.local_init () ls (spec.localize UNIV (spec.rel ({env} × UNIV)
                                            ⤜ (λ_::unit. spec.return v)))"
    by (simp add: prog.p2s.simps prog.p2s.return spec.interference.cl.return
                  spec.local_init.localize spec.idle_le)
  also have "… = spec.local_init () ls (spec.rel ({env} × UNIV) ⤜ (λ_::unit. spec.return v))"
    by (simp add: spec.localize.bind spec.localize.rel spec.localize.return
                  spec.bind.inf_rel spec.return.inf_rel
                  map_prod_vimage_Times map_prod_snd_snd_vimage
                  ac_simps Int_Un_distrib Int_Un_distrib2 Times_Int_Times relprod_inter spec.rel.reflcl
                  spec.rel.wind_bind_trailing times_subset_iff Id_le_relprod_conv
      flip: spec.rel.inf spec.bind.bind)
  also have "… = prog.p2s ?lhs"
    by (simp add: prog.p2s.simps prog.p2s.return spec.interference.cl.return)
  finally show ?thesis
    by (simp add: p2s_inject)
qed

lemma eq_local:
  shows "(⨆ls. prog.local_init ls P) = prog.local P"
by transfer
   (simp add: spec.local_init.eq_local spec.idle_le sup.absorb1 spec.interference.least
              spec.interference.closed.local_UNIV)

setup ‹Sign.parent_path›

lemma localize_alt_def:
  shows "prog.localize P = prog.rel (Id ×⇩R UNIV) ⊓ prog.sinvmap snd P"
by transfer (simp add: spec.localize_def ac_simps)

setup ‹Sign.mandatory_path "localize"›

lemma Sup:
  shows "prog.localize (⨆X) = (⨆x∈X. prog.localize x)"
by (simp add: prog.localize_alt_def prog.invmap.Sup inf_Sup inf_sup_distrib image_image prog.bind.inf_rel
              inv_image_alt_def map_prod_snd_snd_vimage relprod_inter
              prog.rel.Id prog.rel.empty prog.bind.returnL prog.invmap.bot UNIV_unit
        flip: prog.rel.inf)

lemmas sup = prog.localize.Sup[where X="{X, Y}" for X Y, simplified]

lemma bot:
  shows "prog.localize ⊥ = ⊥"
using prog.localize.Sup[where X="{}"] by simp

lemma top:
  shows "prog.localize ⊤ = prog.rel (Id ×⇩R UNIV)"
by transfer (simp add: spec.localize.top ac_simps)

lemma monotone:
  shows "mono prog.localize"
by (rule monotoneI) (transfer; simp add: spec.interference.cl.mono spec.localize.mono)

lemmas strengthen[strg] = st_monotone[OF prog.localize.monotone]
lemmas mono = monotoneD[OF prog.localize.monotone]
lemmas mono2mono[cont_intro, partial_function_mono]
  = monotone2monotone[OF prog.localize.monotone, simplified, of orda P for orda P]

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) P"
  shows "mcont luba orda Sup (≤) (λx. prog.localize (P x))"
proof(rule mcontI)
  from assms show "monotone orda (≤) (λx. prog.localize (P x))"
    by (blast intro: mcont_mono prog.localize.mono2mono)
  from assms show "cont luba orda Sup (≤) (λx. prog.localize (P x))"
    by (fastforce intro: contI dest: mcont_cont contD simp: prog.localize.Sup image_image)
qed

lemmas p2s[prog.p2s.simps] = prog.localize.rep_eq

lemma bind:
  shows "prog.localize (f ⤜ g) = prog.localize f ⤜ (λv. prog.localize (g v))"
by transfer
   (simp add: spec.localize.bind spec.interference.least spec.interference.closed.bind spec.bind.mono)

lemma parallel:
  shows "prog.localize (P ∥ Q) = prog.localize P ∥ prog.localize Q"
by transfer (simp add: spec.localize.parallel)

lemma rel:
  fixes r :: "'s rel"
  shows "prog.localize (prog.rel r) = prog.rel (Id ×⇩R r)"
by (subst (2) prog.rel.reflcl[symmetric])
   (transfer; auto simp: spec.localize.rel intro: arg_cong[where f=spec.rel])

lemma action:
  shows "prog.localize (prog.action F)
       = prog.action (map_prod id (map_prod snd snd) -` F ∩ UNIV × (Id ×⇩R UNIV))"
by (simp add: prog.localize_alt_def prog.invmap.action prog.bind.inf_rel prog.action.inf_rel
              map_prod_snd_snd_vimage relprod_inter prog.rel.Id UNIV_unit refl_relprod_conv
              prog.bind.return prog.return.rel_le
              inf.absorb2
        flip: prog.rel.inf)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "local"›

lemma localize:
  fixes P :: "('s, 'v) prog"
  shows "prog.local (prog.localize P :: ('ls × 's, 'v) prog) = P"
by transfer
   (simp add: spec.local.interference.cl[where r=UNIV and s=UNIV, simplified] spec.local.localize
        flip: spec.interference.closed_conv)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Refinement rules \label{sec:local_state-refinement} ›

setup ‹Sign.mandatory_path "spec"›

text‹

We use ‹localizeA› to hoist assumes similarly to \<^const>‹spec.localize›.

›

definition localizeA :: "(sequential, 's, 'v) spec ⇒ (sequential, 'ls × 's, 'v) spec" where
  "localizeA P = spec.local.interference ⊓ spec.sinvmap snd P"

setup ‹Sign.mandatory_path "localizeA"›

lemma bot:
  shows "spec.localizeA ⊥ = ⊥"
by (simp add: spec.localizeA_def spec.invmap.bot)

lemma top:
  shows "spec.localizeA ⊤ = spec.local.interference"
by (simp add: spec.localizeA_def spec.invmap.top)

lemma ag_assm:
  shows "spec.localizeA (ag.assm A) = ag.assm (Id ×⇩R A)"
apply (simp add: spec.localizeA_def spec.invmap.rel spec.local.qrm_def flip: spec.rel.inf)
apply (subst (1 2) spec.rel.reflcl[where A=UNIV, symmetric])
apply (auto intro: arg_cong[where f=spec.rel])
done

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "refinement"›

setup ‹Sign.mandatory_path "spec"›

lemma localI: ―‹ Introduce local state ›
  fixes A :: "(sequential, 's, 'v) spec"
  fixes c :: "(sequential, 'ls × 's, 'v) spec"
  fixes c' :: "(sequential, 's, 'v) spec"
  fixes P :: "'s pred"
  fixes Q :: "'v ⇒ 's pred"
  assumes "c ≤ ⦃λs. P (snd s)⦄, spec.localizeA A ⊩ spec.sinvmap snd c', ⦃λv s. Q v (snd s)⦄"
  shows "spec.local c ≤ ⦃P⦄, A ⊩ c', ⦃Q⦄"
apply (simp only: spec.local_def spec.map_invmap.galois spec.invmap.refinement id_apply)
apply (subst inf.commute)
apply (subst heyting[symmetric])
apply (strengthen ord_to_strengthen[OF assms])
apply (strengthen ord_to_strengthen[OF refinement.heyting_le])
apply (simp add: refinement.mono[OF order.refl _ _ order.refl] heyting spec.localizeA_def)
done

setup ‹Sign.mandatory_path "seq_ctxt"›

lemma local_seq_ctxt_cl:
  fixes A :: "(sequential, 's, 'v) spec"
  fixes P :: "'s pred"
  fixes Q :: "'v ⇒ 's pred"
  fixes c :: "(sequential, 'ls × 's, 'v) spec"
  fixes c' :: "(sequential, 'ls × 's, 'v) spec"
  assumes "spec.local.interference ⊓ c
        ≤ ⦃λs. P (snd s)⦄, spec.localizeA A ⊩ spec.seq_ctxt.cl False (spec.local.interference ⊓ c'), ⦃λv s. Q v (snd s)⦄"
  shows "spec.local c ≤ ⦃P⦄, A ⊩ spec.local c', ⦃Q⦄"
apply (simp only: spec.local_def spec.map_invmap.galois spec.invmap.refinement id_apply)
apply (subst inf.left_idem[symmetric]) ―‹ non-linear use of env constraint ›
apply (strengthen ord_to_strengthen(1)[OF assms])
apply (subst inf.commute)
apply (subst heyting[symmetric])
apply (strengthen ord_to_strengthen(2)[OF refinement.heyting_le])
apply (subst inf.commute, fold spec.localizeA_def)
apply (rule refinement.mono[OF order.refl order.refl _ order.refl])
apply (strengthen ord_to_strengthen(1)[OF spec.seq_ctxt.cl_local_le])
apply (simp add: heyting flip: spec.map_invmap.cl_def)
done

lemma cl_bind:
  fixes f :: "('a agent, 'ls × 's, 'v) spec"
  fixes g :: "'v ⇒ ('a agent, 'ls × 's, 'w) spec"
  assumes g: "⋀v. g v ≤ ⦃Q' v⦄, refinement.spec.bind.res (spec.pre P ⊓ spec.term.all A ⊓ spec.seq_ctxt.cl True f') A v ⊩ spec.seq_ctxt.cl T (g' v), ⦃Q⦄"
  assumes f: "f ≤ ⦃P⦄, spec.term.all A ⊩ spec.seq_ctxt.cl True f', ⦃Q'⦄"
  shows "f ⤜ g ≤ ⦃P⦄, A ⊩ spec.seq_ctxt.cl T (f' ⤜ g'), ⦃Q⦄"
by (strengthen ord_to_strengthen[OF spec.bind.seq_ctxt.cl_le]) (rule refinement.spec.bind[OF assms])

lemma cl_action_permuteL:
  fixes F  :: "('v × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes G  :: "'v ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes G' :: "('v' × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes F' :: "'v' ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes Q :: "'w ⇒ ('ls × 's) pred"
  assumes F: "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ F⟧ ⟹ snd s' = snd s"
  assumes FGG'F': "⋀v w a a' s s' t. ⟦P s; (v, a', s, t) ∈ F; (w, a, t, s') ∈ G v⟧
                   ⟹ ∃v' a'' a''' t'. (v', a'', s, t') ∈ G' ∧ (w, a''', t', s') ∈ F' v'
                          ∧ snd s' = snd t' ∧ (snd s ≠ snd t' ⟶ a'' = a)"
  assumes Q: "⋀v w a a' s s' s''. ⟦P s; (v, a, s, s') ∈ G'; (w, a', s', s'') ∈ F' v⟧ ⟹ Q w s''"
  shows "spec.action F ⤜ (λv. spec.action (G v)) ≤ ⦃P⦄, A ⊩ spec.seq_ctxt.cl T (spec.action G' ⤜ (λv. spec.action (F' v))), ⦃Q⦄"
apply (strengthen ord_to_strengthen[OF top_greatest[where a=T]])
apply (rule order.trans[OF spec.seq_ctxt.cl_action_permuteL_le[where T=True and F'=F' and G'=G', simplified heyting[symmetric]]])
  apply (erule (1) F)
 apply (drule (2) FGG'F', blast)
apply (simp only: refinement_def spec.pre.next_imp_eq_heyting spec.idle_le inf.bounded_iff)
apply (rule order.trans[OF _ heyting.mono[OF order.refl spec.next_imp.mono[OF top_greatest order.refl]]])
apply (simp add: heyting heyting.detachment spec.seq_ctxt.cl_action_bind_action_pre_post[OF Q])
done

lemma cl_action_permuteR:
  fixes G  :: "('v × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes F  :: "'v ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes F' :: "('v' × 'a × ('ls × 's) × ('ls × 's)) set"
  fixes G' :: "'v' ⇒ ('w × 'a × ('ls × 's) × ('ls × 's)) set"
  assumes G: "⋀v a s s'. ⟦P s; (v, a, s, s') ∈ G; snd s' ≠ snd s⟧
              ⟹ ∃v' w a'' t s''. (v', a'', s, t) ∈ F' ∧ (w, a, t, s'') ∈ G' v' ∧ snd t = snd s ∧ snd s'' = snd s'"
  assumes GFF'G': "⋀v w a a' s s' t. ⟦P s; (v, a, s, t) ∈ G; (w, a', t, s') ∈ F v⟧
                   ⟹ snd s' = snd t ∧ (∃v' a'' a''' t'. (v', a'', s, t') ∈ F' ∧ (w, a''', t', s') ∈ G' v'
                                                        ∧ snd t' = snd s ∧ (snd s' ≠ snd t' ⟶ a''' = a))"
  assumes Q: "⋀v w a a' s s' s''. ⟦P s; (v, a, s, s') ∈ F'; (w, a', s', s'') ∈ G' v⟧ ⟹ Q w s''"
  shows "spec.action G ⤜ (λv. spec.action (F v)) ≤ ⦃P⦄, A ⊩ spec.seq_ctxt.cl T (spec.action F' ⤜ (λv. spec.action (G' v))), ⦃Q⦄"
apply (strengthen ord_to_strengthen[OF top_greatest[where a=T]])
apply (rule order.trans[OF spec.seq_ctxt.cl_action_permuteR_le[where T=True, simplified heyting[symmetric]]])
  apply (erule (2) G)
 apply (drule (2) GFF'G', blast)
apply (simp only: refinement_def spec.pre.next_imp_eq_heyting spec.idle_le inf.bounded_iff)
apply (rule order.trans[OF _ heyting.mono[OF order.refl spec.next_imp.mono[OF top_greatest order.refl]]])
apply (simp add: heyting heyting.detachment spec.seq_ctxt.cl_action_bind_action_pre_post[OF Q])
done

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "prog"›

lemma localI: ―‹ Introduce local state ›
  fixes A :: "(sequential, 's, 'v) spec"
  fixes c :: "('ls × 's, 'v) prog"
  fixes c' :: "(sequential, 's, 'v) spec"
  fixes P :: "'s pred"
  fixes Q :: "'v ⇒ 's pred"
  assumes "prog.p2s c ≤ ⦃λs. P (snd s)⦄, spec.localizeA A ⊩ spec.sinvmap snd c', ⦃λv s. Q v (snd s)⦄"
  shows "prog.p2s (prog.local c) ≤ ⦃P⦄, A ⊩ c', ⦃Q⦄"
using assms by transfer (erule refinement.spec.localI)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsubsection‹ Data refinement \label{sec:local_state-data_refinement} ›

text‹

In this setting a (concrete) specification ‹c› is a ∗‹data refinement› of (abstract) specification
‹c'› if:
 ▪ the observable state changes coincide
 ▪ concrete local states are mapped to abstract local states by ‹sf› which then coincide

Observations:
 ▪ pre/post are in terms of the concrete local states
  ▪ ‹sf› can be used to lift these to the abstract local states
 ▪ we do not require ‹c› or ‹c'› to disallow the environment from changing the local state
 ▪ essentially a Skolemization of Lamport's existentials \<^citep>‹‹\S8› in "Lamport:1994"›

References:
 ▪ \<^citet>‹‹Chapter~14 ``Refinement Methods due to Abadi and Lamport and to Lynch''› in "deRoeverEngelhardt:1998"›
  ▪ in general ‹c› will need to be augmented with auxiliary variables

›

setup ‹Sign.mandatory_path "refinement"›

setup ‹Sign.mandatory_path "spec"›

lemma data:
  fixes A :: "(sequential, 's, 'v) spec"
  fixes c :: "(sequential, 'cls × 's, 'v) spec"
  fixes c' :: "(sequential, 'als × 's, 'v) spec"
  fixes sf :: "'cls ⇒ 'als"
  assumes "c ≤ ⦃λs. P (snd s)⦄, spec.localizeA A ⊩ spec.sinvmap (map_prod sf id) c', ⦃λv s. Q v (snd s)⦄"
  shows "spec.local c ≤ ⦃P⦄, A ⊩ spec.local c', ⦃Q⦄"
proof -
  have *: "spec.smap snd (spec.local.interference ⊓ spec.sinvmap (map_prod sf id) c')
        ≤ spec.smap snd (spec.local.interference ⊓ c')" (is "?lhs ≤ ?rhs")
  proof(rule spec.singleton_le_extI)
    show "⦉σ⦊ ≤ ?rhs" if "⦉σ⦊ ≤ ?lhs" for σ
      using that
      by (clarsimp simp: spec.singleton.le_conv)
         (fastforce simp: trace.steps'.map spec.local.qrm_def
               simp flip: id_def
                  intro!: exI[where x="trace.map id (map_prod sf id) id σ'" for σ'])
  qed
  show ?thesis
    apply (simp only: spec.local_def spec.map_invmap.galois spec.invmap.refinement id_apply)
    apply (subst inf.left_idem[symmetric]) ―‹ non-linear use of env constraint ›
    apply (strengthen ord_to_strengthen(1)[OF assms])
    apply (strengthen ord_to_strengthen(1)[OF refinement.inf_le])
    apply (subst inf.commute)
    apply (subst heyting[symmetric])
    apply (strengthen ord_to_strengthen(2)[OF refinement.heyting_le])
    apply (subst inf.commute, fold spec.localizeA_def)
    apply (rule refinement.mono[OF order.refl _ _ order.refl])
     apply (simp add: spec.localizeA_def; fail)
    apply (simp add: heyting inf.absorb1 * flip: spec.map_invmap.galois)
    done
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "prog"›

lemma data:
  fixes A :: "(sequential, 's, 'v) spec"
  fixes c :: "('cls × 's, 'v) prog"
  fixes c' :: "('als × 's, 'v) prog"
  fixes sf :: "'cls ⇒ 'als"
  assumes "prog.p2s c ≤ ⦃λs. P (snd s)⦄, spec.localizeA A ⊩ spec.sinvmap (map_prod sf id) (prog.p2s c'), ⦃λv s. Q v (snd s)⦄"
  shows "prog.p2s (prog.local c) ≤ ⦃P⦄, A ⊩ prog.p2s (prog.local c'), ⦃Q⦄"
using assms by transfer (erule refinement.spec.data)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Assume/guarantee \label{sec:local_state-ag} ›

setup ‹Sign.mandatory_path "ag"›

setup ‹Sign.mandatory_path "spec"›

lemma local:
  fixes A G :: "'s rel"
  fixes P :: "'s pred"
  fixes Q :: "'v ⇒ 's pred"
  fixes c :: "(sequential, 'ls × 's, 'v) spec"
  assumes "c ≤ ⦃λs. P (snd s)⦄, Id ×⇩R A ⊢ UNIV ×⇩R G, ⦃λv s. Q v (snd s)⦄"
  shows "spec.local c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
unfolding spec.local_def
apply (subst spec.map_invmap.galois)
apply (strengthen ord_to_strengthen(1)[OF assms])
apply (subst (1) ag.reflcl_ag)
apply (simp only: spec.invmap.ag inv_image_alt_def map_prod_snd_snd_vimage)
apply (subst inf.commute)
apply (subst heyting[symmetric])
apply (subst spec.local.qrm_def)
apply (subst sequential.range_proc_self)
apply (subst Un_commute, subst ag.assm_heyting)
apply (auto intro: ag.mono)
done

lemma localize_lift:
  fixes A G :: "'s rel"
  fixes P :: "'s ⇒ bool"
  fixes Q :: "'v ⇒ 's ⇒ bool"
  fixes c :: "(sequential, 's, 'v) spec"
  notes inf.bounded_iff[simp del]
  assumes c: "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  shows "spec.localize UNIV c ≤ ⦃λs. P (snd s)⦄, UNIV ×⇩R A ⊢ Id ×⇩R G, ⦃λv s::'ls × 's. Q v (snd s)⦄"
proof(rule ag.name_pre_state)
  fix s :: "'ls × 's" assume "P (snd s)"
  show "spec.localize UNIV c ≤ ⦃(=) s⦄, UNIV ×⇩R A ⊢ Id ×⇩R G, ⦃λv s. Q v (snd s)⦄"
apply (strengthen ord_to_strengthen[OF c])
apply (simp add: spec.localize_def spec.invmap.ag inv_image_snd)
apply (simp add: ac_simps ag_def heyting)

―‹ discharge pre ›
apply (subst (2) inf.commute)
apply (subst (2) inf.commute)
apply (subst inf.assoc)
apply (subst inf.assoc[symmetric])
apply (subst heyting.curry_conv)
apply (subst heyting.discharge)
 apply (simp add: ‹P (snd s)› predicate1I spec.pre.mono; fail)
apply (simp add: ac_simps)

―‹ discarge assume ›
apply (subst inf.assoc[symmetric])
apply (subst inf.assoc[symmetric])
apply (subst heyting.discharge)
 apply (force intro: le_infI2 spec.rel.mono)
apply (simp add: ac_simps)

―‹ establish post ›
apply (subst inf.bounded_iff, rule conjI)
 apply (simp add: le_infI2; fail)

―‹ establish guarantee ›
apply (force simp: inf.bounded_iff
        simp flip: inf.assoc spec.rel.inf
            intro: le_infI2 spec.rel.mono_reflcl)
done
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "prog"›

lemma local:
  fixes A G :: "'s rel"
  fixes P :: "'s pred"
  fixes Q :: "'v ⇒ 's pred"
  fixes c :: "('ls × 's, 'v) prog"
  assumes "prog.p2s c ≤ ⦃λs. P (snd s)⦄, Id ×⇩R A ⊢ UNIV ×⇩R G, ⦃λv s. Q v (snd s)⦄"
  shows "prog.p2s (prog.local c) ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
using assms by transfer (rule ag.spec.local)

lemma localize_lift:
  fixes A G :: "'s rel"
  fixes P :: "'s ⇒ bool"
  fixes Q :: "'v ⇒ 's ⇒ bool"
  fixes c :: "('s, 'v) prog"
  assumes "prog.p2s c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  shows "prog.p2s (prog.localize c) ≤ ⦃λs. P (snd s)⦄, UNIV ×⇩R A ⊢ Id ×⇩R G, ⦃λv s. Q v (snd s)⦄"
using assms by transfer (rule ag.spec.localize_lift)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Specification inhabitation\label{sec:local_state-inhabitation} ›

setup ‹Sign.mandatory_path "inhabits.spec"›

lemma localize:
  assumes "P -s, xs→ P'"
  assumes "Id ⊆ r"
  shows "spec.localize r P -(ls, s), map (map_prod id (Pair ls)) xs→ spec.localize r P'"
by (auto intro!: inhabits.inf inhabits.spec.rel.rel
           simp: spec.localize_def assms(1) trace_steps'_map subsetD[OF assms(2)] inhabits.spec.invmap comp_def)

lemma local:
  assumes "P -(ls, s), xs→ spec.return v"
  assumes "trace.steps' (ls, s) xs ⊆ spec.local.qrm"
  shows "spec.local P -s, map (map_prod id snd) xs→ spec.return v"
unfolding spec.local_def
by (rule inhabits.spec.map[where af=id and sf=snd and vf=id and s="(ls, s)", simplified])
   (rule inhabits.inf[OF inhabits.spec.rel.rel_term[OF assms(2), where v=v] assms(1), simplified])

lemma local_init:
  assumes "P -(ls, s), xs→ P'"
  assumes "trace.steps' (ls, s) xs ⊆ spec.local.qrm"
  shows "spec.local_init a ls P -s, map (map_prod id snd) xs→ spec.local_init a (fst (trace.final' (ls, s) xs)) P'"
proof -
  have "⦉s, map (map_prod id snd) xs, Some ()⦊ ⪢ spec.local_init a (fst (trace.final' (ls, s) xs)) P'
     ≤ spec.local_init a ls (⦉(ls, s), xs, Some ()⦊ ⤜ (λ_. P'))"
  proof(induct rule: spec.bind_le)
    case incomplete from assms(2) show ?case
      by (fastforce simp: spec.term.none.singleton spec.singleton.local_init_le_conv
                   intro: spec.bind.incompleteI)
  next
    case (continue σ⇩f σ⇩g v)
    consider (idle) "⦉σ⇩g⦊ ≤ spec.idle"
          | (steps) σ' where "⦉σ'⦊ ≤ P'"
                         and "trace.steps' (trace.init σ') (trace.rest σ') ⊆ spec.local.qrm"
                         and  "⦉σ⇩g⦊ ≤ ⦉trace.map id snd id σ'⦊"
                         and "fst (trace.init σ') = fst (trace.final' (ls, s) xs)"
      using disjE[OF iffD1[OF spec.singleton.local_init_le_conv continue(4)]] by metis
    then show ?case
    proof cases
      case idle with ‹♮σ⇩g ≠ trace.T (trace.init σ⇩g) [] None› show ?thesis
        by (simp add: spec.singleton.le_conv spec.singleton.local_init_le_conv
                      trace.natural_def trace.natural'.eq_Nil_conv)
    next
      case (steps σ')
      let ?σ' = "trace.T (ls, s) (xs @ trace.rest σ') (trace.term σ')"
      from continue(1,2,3) steps(3)
      have *: "snd (trace.final' (ls, s) xs) = snd (trace.init σ')"
        by (cases σ'; cases σ⇩f)
           (clarsimp; metis snd_conv spec.singleton_le_conv trace.natural.sel(1)
                            trace.final'.map trace.final'.natural' trace.less_eqE  trace.t.sel(1))
      with steps(4) have *: "trace.final' (ls, s) xs = trace.init σ'"
        by (simp add: prod.expand)
      from steps(1) *
      have "⦉?σ'⦊ ≤ ⦉(ls, s), xs, Some ()⦊ ⪢ P'"
        by (simp add: spec.bind.continueI[OF order.refl])
      moreover
      from assms(2) steps(2) *
      have "trace.steps ?σ' ⊆ spec.local.qrm"
        by (simp add: trace.steps'.append)
      moreover
      from continue(1-3) steps *
      have "⦉trace.init σ⇩f, trace.rest σ⇩f @ trace.rest σ⇩g, trace.term σ⇩g⦊ ≤ ⦉trace.map id snd id ?σ'⦊"
        by (auto simp: trace.less_eq_None spec.singleton_le_conv trace.natural_def trace.natural'.append
                 cong: trace.final'.natural'_cong
                 elim: trace.less_eqE)
      ultimately show ?thesis
        by (simp add: spec.singleton.local_init_le_conv exI[where x="?σ'"])
    qed
  qed
  then show ?thesis
    unfolding inhabits_def
    by (rule order.trans[OF _ spec.local_init.mono[OF assms(1)[unfolded inhabits_def]]])
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "prog.inhabits"›

lemma localize:
  assumes "prog.p2s P -s, xs→ prog.p2s P'"
  shows "prog.p2s (prog.localize P) -(ls, s), map (map_prod id (Pair ls)) xs→ prog.p2s (prog.localize P')"
using assms by transfer (rule inhabits.spec.localize; blast)

lemma local:
  assumes "prog.p2s P -(ls, s), xs→ spec.return v"
  assumes "trace.steps' (ls, s) xs ⊆ spec.local.qrm"
  shows "prog.p2s (prog.local P) -s, map (map_prod id snd) xs→ spec.return v"
using assms by transfer (rule inhabits.spec.local)

lemma local_init:
  assumes "prog.p2s P -(ls, s), xs→ prog.p2s P'"
  assumes "trace.steps' (ls, s) xs ⊆ spec.local.qrm"
  shows "prog.p2s (prog.local_init ls P) -s, map (map_prod id snd) xs→ prog.p2s (prog.local_init (fst (trace.final' (ls, s) xs)) P')"
using assms by transfer (rule inhabits.spec.local_init)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›
(*<*)

end
(*>*)