Theory Atomic

(*<*)
theory Atomic
imports
  "ConcurrentHOL.ConcurrentHOL"
begin

(*>*)
section‹ Atomic sections \label{sec:atomic} ›

text‹

By restricting the environment to stuttering steps we can consider arbitrary processes to be atomic,
i.e., free of interference.

›

setup ‹Sign.mandatory_path "spec"›

definition atomic :: "'a ⇒ ('a, 's, 'v) spec ⇒ ('a, 's, 'v) spec" where
  "atomic a P = P ⊓ spec.rel ({a} × UNIV)"

setup ‹Sign.mandatory_path "idle"›

lemma atomic_le_conv[spec.idle_le]:
  shows "spec.idle ≤ spec.atomic a P ⟷ spec.idle ≤ P"
by (simp add: spec.atomic_def spec.idle.rel_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "none"›

lemma atomic:
  shows "spec.term.none (spec.atomic a P) = spec.atomic a (spec.term.none P)"
by (simp add: spec.atomic_def spec.term.none.inf spec.term.none.inf_rel)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "all"›

lemma atomic:
  shows "spec.term.all (spec.atomic a P) = spec.atomic a (spec.term.all P)"
by (simp add: spec.atomic_def spec.term.all.inf spec.term.all.rel)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "atomic"›

lemma bot[simp]:
  shows "spec.atomic a ⊥ = ⊥"
by (simp add: spec.atomic_def)

lemma top[simp]:
  shows "spec.atomic a ⊤ = spec.rel ({a} × UNIV)"
by (simp add: spec.atomic_def)

lemma contractive:
  shows "spec.atomic a P ≤ P"
by (simp add: spec.atomic_def)

lemma idempotent[simp]:
  shows "spec.atomic a (spec.atomic a P) = spec.atomic a P"
by (simp add: spec.atomic_def)

lemma monotone:
  shows "mono (spec.atomic a)"
by (simp add: spec.atomic_def monoI le_infI1)

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

lemma Sup:
  shows "spec.atomic a (⨆X) = ⨆(spec.atomic a ` X)"
by (simp add: spec.atomic_def ac_simps heyting.inf_Sup_distrib)

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

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

lemma Inf_not_empty:
  assumes "X ≠ {}"
  shows "spec.atomic a (⨅X) = ⨅(spec.atomic a ` X)"
using assms by (simp add: spec.atomic_def INF_inf_const2)

lemmas inf = spec.atomic.Inf_not_empty[where X="{P, Q}" for P Q, simplified]

lemma idle:
  shows "spec.atomic a spec.idle = spec.idle"
by (simp add: spec.atomic_def inf.absorb1 spec.idle.rel_le)

lemma action:
  shows "spec.atomic a (spec.action F) = spec.action (F ∩ UNIV × ({a} × UNIV ∪ UNIV × Id))"
by (simp add: spec.atomic_def spec.action.inf_rel_reflcl)

lemma return:
  shows "spec.atomic a (spec.return v) = spec.return v"
by (simp add: spec.return_def spec.atomic.action Times_Int_Times)

lemma bind:
  shows "spec.atomic a (f ⤜ g) = spec.atomic a f ⤜ (λv. spec.atomic a (g v))"
by (simp add: spec.atomic_def spec.bind.inf_rel ac_simps)

lemma map_le:
  fixes af :: "'a ⇒ 'b"
  shows "spec.map af sf vf (spec.atomic a P) ≤ spec.atomic (af a) (spec.map af sf vf P)"
by (auto simp: spec.atomic_def spec.map.inf_rel
       intro!: spec.map.mono inf.mono order.refl spec.rel.mono)

lemma invmap:
  fixes af :: "'a ⇒ 'b"
  shows "spec.atomic a (spec.invmap af sf vf P) ≤ spec.invmap af sf vf (spec.atomic (af a) P)"
by (auto simp: spec.atomic_def spec.invmap.inf spec.invmap.rel
       intro!: le_infI2 spec.rel.mono)

lemma rel:
  shows "spec.atomic a (spec.rel r) = spec.rel (r ∩ {a} × UNIV)"
by (simp add: spec.atomic_def flip: spec.rel.inf)

lemma interference:
  shows "spec.atomic (proc a) (spec.rel ({env} × UNIV)) = spec.rel {}"
by (simp add: spec.atomic.rel flip: Times_Int_distrib1)

setup ‹Sign.mandatory_path "cam"›

lemma cl:
  shows "spec.atomic (proc a) (spec.cam.cl ({env} × UNIV) P) = spec.atomic (proc a) P"
by (simp add: spec.cam.cl_def spec.atomic.sup spec.atomic.bind spec.atomic.interference
              spec.rel.empty spec.term.none.bind spec.term.none.Sup spec.term.none.return
              image_image spec.bind.botR spec.bind.idleR sup_iff_le
        flip: spec.term.none.atomic spec.term.all.atomic)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "interference"›

lemma cl:
  shows "spec.atomic (proc a) (spec.interference.cl ({env} × UNIV) P) = spec.return () ⪢ spec.atomic (proc a) P"
by (simp add: spec.interference.cl_def UNIV_unit spec.atomic.bind spec.atomic.interference
              spec.rel.empty spec.atomic.cam.cl spec.bind.return spec.atomic.return)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "prog"›

lift_definition atomic :: "('s, 'v) prog ⇒ ('s, 'v) prog" is
  "λP. spec.interference.cl ({env} × UNIV) (spec.atomic self P)" ..

setup ‹Sign.mandatory_path "atomic"›

lemma bot[simp]:
  shows "prog.atomic ⊥ = ⊥"
by transfer
   (simp add: spec.interference.cl.bot spec.atomic.interference spec.interference.cl.rel
        flip: spec.term.none.atomic spec.term.none.interference.cl)

lemma contractive:
  shows "prog.atomic P ≤ P"
by transfer (simp add: spec.atomic.contractive spec.interference.least)

lemma idempotent[simp]:
  shows "prog.atomic (prog.atomic P) = prog.atomic P"
by transfer (metis spec.atomic.idempotent spec.atomic.interference.cl spec.interference.closed_conv)

lemma monotone:
  shows "mono prog.atomic"
by (rule monoI) (transfer; simp add: spec.atomic.mono spec.interference.mono_cl)

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

lemma Sup:
  shows "prog.atomic (⨆X) = ⨆(prog.atomic ` X)"
by transfer
   (simp add: spec.atomic.Sup spec.atomic.sup spec.interference.cl_Sup spec.interference.cl_sup
              image_image spec.interference.cl.bot spec.atomic.interference spec.interference.cl.rel
        flip: spec.term.none.atomic spec.term.none.interference.cl)

lemmas sup = prog.atomic.Sup[where X="{P, Q}" for P Q, simplified]

lemma mcont:
  shows "mcont Sup (≤) Sup (≤) prog.atomic"
by (simp add: mcontI contI prog.atomic.Sup)

lemmas mcont2mcont[cont_intro] = mcont2mcont[OF prog.atomic.mcont, of luba orda P for luba orda P]

lemma Inf_le:
  shows "prog.atomic (⨅X) ≤ ⨅(prog.atomic ` X)"
by transfer (simp add: Inf_lower le_INF_iff spec.atomic.mono spec.interference.mono_cl)

lemmas inf_le = prog.atomic.Inf_le[where X="{P, Q}" for P Q, simplified]

lemma action:
  shows "prog.atomic (prog.action F) = prog.action F"
by transfer
   (simp add: spec.atomic.interference.cl spec.atomic.action spec.bind.returnL spec.idle.action_le;
    rule arg_cong; blast)

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

lemma bind_le:
  shows "prog.atomic (f ⤜ g) ≤ prog.atomic f ⤜ (λv. prog.atomic (g v))"
by transfer
   (simp add: spec.atomic.bind spec.bind.mono
              spec.interference.closed.bind spec.interference.expansive spec.interference.least)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "p2s"›

lemmas atomic = prog.atomic.rep_eq

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Inhabitation ›

setup ‹Sign.mandatory_path "inhabits.spec"›

lemma atomic:
  assumes "P -s, xs→ P'"
  assumes "trace.steps' s xs ⊆ {a} × UNIV"
  shows "spec.atomic a P -s, xs→ spec.atomic a P'"
unfolding spec.atomic_def by (rule inhabits.inf[OF assms(1) inhabits.spec.rel.rel[OF assms(2)]])

lemma atomic_term:
  assumes "P -s, xs→ spec.return v"
  assumes "trace.steps' s xs ⊆ {a} × UNIV"
  shows "spec.atomic a P -s, xs→ spec.return v"
by (rule inhabits.spec.atomic[where P'="spec.return v", simplified spec.atomic.return, OF assms])

lemma atomic_diverge:
  assumes "P -s, xs→ ⊥"
  assumes "trace.steps' s xs ⊆ {a} × UNIV"
  shows "spec.atomic a P -s, xs→ ⊥"
by (rule inhabits.spec.atomic[where P'="⊥", simplified spec.atomic.bot, OF assms])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "inhabits.prog"›

lemma atomic_term:
  assumes "prog.p2s P -s, xs→ spec.return v"
  assumes "trace.steps' s xs ⊆ {self} × UNIV"
  shows "prog.p2s (prog.atomic P) -s, xs→ spec.return v"
unfolding prog.p2s.atomic
by (rule inhabits.mono[OF spec.interference.expansive order.refl
                          inhabits.spec.atomic_term[OF assms]])

lemma atomic_diverge:
  assumes "prog.p2s P -s, xs→ ⊥"
  assumes "trace.steps' s xs ⊆ {self} × UNIV"
  shows "prog.p2s (prog.atomic P) -s, xs→ ⊥"
unfolding prog.p2s.atomic
by (rule inhabits.mono[OF spec.interference.expansive order.refl
                               inhabits.spec.atomic_diverge[OF assms]])

setup ‹Sign.parent_path›


subsection‹ Assume/guarantee ›

setup ‹Sign.mandatory_path "ag.prog"›

lemma atomic:
  assumes "prog.p2s c ≤ ⦃P⦄, Id ⊢ G, ⦃Q⦄"
  assumes P: "stable A P"
  assumes Q: "⋀v. stable A (Q v)"
  shows "prog.p2s (prog.atomic c) ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
apply (subst ag.assm_heyting[where A=A and r=A, simplified, symmetric])
apply (simp add: prog.p2s.atomic)
apply (strengthen ord_to_strengthen[OF assms(1)])
apply (simp add: spec.atomic_def heyting ac_simps spec.interference.cl.inf_rel inf_sup_distrib Times_Int_Times
      flip: spec.rel.inf)
using assms
apply (force intro: order.trans[OF _ spec.interference.cl_ag_le[where A=A and r=A, simplified]]
                    spec.interference.cl.mono[OF order.refl] ag.pre_a
          simp add: heyting[symmetric] ag.assm_heyting[where r="{}", simplified])
done

setup ‹Sign.parent_path›
(*<*)

end
(*>*)