Quelle  Programs.thy

(*<*)
theory Programs
imports
  Refinement
begin

(*>*)
section‹ A programming language\label{sec:programs} ›

text‹

  🍋‹('a, 's, 'v) spec› lattice of
 S\ref{sec:safety_logic-logic} is adequate for logic but is deficient
  a programming language. In particular we wish to interpret the
  composition as intersection
 \S\ref{sec:constructions-parallel_composition}) which requires
  to contain enough interference opportunities. Similarly we
  the customary ``laws of programming''
 🍋‹"HoareEtAl:1987"› to hold without side
 .

  points are discussed at some length by
 🍋‹‹\S3.2› in "Zwiers:1989"› and also
 🍋‹‹Lemma~6.7› in "Foster:2020"›.

  ‹('v, 's) prog› lattice (\S\ref{sec:programs-prog})
  handles the common case of the familiar constructs for
  programming, and we lean on our 🍋‹('a, 's, 'v)
 › lattice for other constructions such as interleaving
  composition (\S\ref{sec:constructions-parallel_composition})
  local state (\S\ref{sec:local_state}). It allows arbitrary
  by the environment before and after every program action.

 ›


subsection‹ The 🪙‹('s, 'v) prog› lattice \label{sec:programs-prog} ›

text‹

  to 🍋‹‹\S2.1› in "MuellerOlm:1997"›, ‹('s, 'v) prog› is
  🪙‹sub-lattice› of 🍋‹('a, 's, 'v) spec› as the corresponding const‹inf› and const‹sup›
  coincide. However it is not a 🪙‹complete› sub-lattice as const‹Sup› in ‹('s, 'v) prog›
  to account for the higher bottom of that lattice.

 ›

typedef ('s, 'v) prog = "spec.interference.closed ({env} × UNIV) :: (sequential, 's, 'v) spec set"
morphisms p2s Abs_t
by blast

hide_const (open) p2s

setup_lifting type_definition_prog

instantiation prog :: (type, type) complete_distrib_lattice
begin

lift_definition bot_prog :: "('s, 'v) prog" is "spec.interference.cl ({env} × UNIV) ⊥" ..
lift_definition top_prog :: "('s, 'v) prog" is ⊤ ..
lift_definition sup_prog :: "('s, 'v) prog ==> ('s, 'v) prog ==> ('s, 'v) prog" is sup ..
lift_definition inf_prog :: "('s, 'v) prog ==> ('s, 'v) prog ==> ('s, 'v) prog" is inf ..
lift_definition less_eq_prog :: "('s, 'v) prog ==> ('s, 'v) prog ==> bool" is less_eq .
lift_definition less_prog :: "('s, 'v) prog ==> ('s, 'v) prog ==> bool" is less .
lift_definition Inf_prog :: "('s, 'v) prog set ==> ('s, 'v) prog" is Inf ..
lift_definition Sup_prog :: "('s, 'v) prog set ==> ('s, 'v) prog" is "λX. Sup X ⊔ spec.interference.cl ({env} × UNIV) ⊥" ..

instance
by standard (transfer; auto simp: Inf_lower InfI SupI le_supI1 spec.interference.least)+

end


subsection‹ Morphisms to and from the 🪙‹(sequential, 's, 'v) spec› lattice\label{sec:programs-morphisms} ›

text‹

  can readily convert a 🍋‹('s, 'v) prog› into a
 🍋‹('a agent, 's, 'v) spec›. More interestingly, on
 🍋‹('s, 'v) prog› we have a Galois connection that
  specifications into programs. (This connection is termed a
 🪙‹Galois insertion› by
 🍋‹"MeltonSchmidtStrecker:1985"› as we also have
 ‹prog.s2p.p2s›; Cousot says ``Galois retraction''.)

  also \S\ref{sec:programs-refinement-galois} and
 S\ref{sec:programs-ag-galois}.

 ›

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

lemmas p2s[iff] = prog.p2s

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.interference.cl"›

lemmas p2s = spec.interference.closed_conv[OF spec.interference.closed.p2s, symmetric, of P for P]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec.idle"›

lemmas p2s_le[spec.idle_le]
  = spec.interference.le_closedE[OF spec.idle.interference.cl_le spec.interference.closed.p2s, of P for P]
lemmas p2s_minimal[iff] = order.trans[OF spec.idle.minimal_le spec.idle.p2s_le]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "prog"›

lemma p2s_leI:
  assumes "prog.p2s c ≤ prog.p2s d"
  shows "c ≤ d"
by (simp add: assms less_eq_prog.rep_eq)

setup ‹Sign.mandatory_path "p2s"›

named_theorems simps ‹simp rules for const‹p2s››

lemmas bot = bot_prog.rep_eq
lemmas top = top_prog.rep_eq
lemmas inf = inf_prog.rep_eq
lemmas sup = sup_prog.rep_eq
lemmas Inf = Inf_prog.rep_eq
lemmas Sup = Sup_prog.rep_eq

lemma Sup_not_empty:
  assumes "X ≠ {}"
  shows "prog.p2s (⊔X) = ⊔(prog.p2s ` X)"
using assms by transfer (simp add: sup.absorb1 less_eq_Sup spec.interference.least)

lemma SUP_not_empty:
  assumes "X ≠ {}"
  shows " prog.p2s (⊔x∈X. f x) = (⊔x∈X. prog.p2s (f x))"
by (simp add: assms prog.p2s.Sup_not_empty[where X="f ` X", simplified image_image])


lemma monotone:
  shows "mono prog.p2s"
by (rule monoI) (transfer; simp)

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

lemma mcont: ―‹ Morally @{thm [source] galois.complete_lattice.mcont_lower} ›
  shows "mcont Sup (≤) Sup (≤) prog.p2s"
by (simp add: contI mcontI prog.p2s.Sup_not_empty)

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

lemmas Let_distrib = Let_distrib[where f=prog.p2s]

lemmas [prog.p2s.simps] =
  prog.p2s.bot
  prog.p2s.top
  prog.p2s.inf
  prog.p2s.sup
  prog.p2s.Inf
  prog.p2s.Sup_not_empty
  spec.interference.cl.p2s
  prog.p2s.Let_distrib

lemma interference_wind_bind:
  shows "spec.rel ({env} × UNIV) 🍋 (λ_::unit. prog.p2s P) = prog.p2s P"
by (subst (1 2) spec.interference.closed_conv[OF prog.p2s])
   (simp add: spec.interference.cl_def spec.rel.wind_bind flip: spec.bind.bind)

setup ‹Sign.parent_path›

definition s2p :: "(sequential, 's, 'v) spec ==> ('s, 'v) prog" where ―‹ Morally the upper of a Galois connection ›
  "s2p P = ⊔{c. prog.p2s c ≤ P}"

setup ‹Sign.mandatory_path "s2p"›

lemma bottom:
  shows "prog.s2p ⊥ = ⊥"
by (simp add: prog.s2p_def bot.extremum_uniqueI less_eq_prog.rep_eq)

lemma top:
  shows "prog.s2p ⊤ = ⊤"
by (simp add: prog.s2p_def)

lemma monotone:
  shows "mono prog.s2p"
by (fastforce simp: prog.s2p_def intro: monotoneI Sup_subset_mono)

lemmas strengthen[strg] = st_monotone[OF prog.s2p.monotone]
lemmas mono = monotoneD[OF prog.s2p.monotone]
lemmas mono2mono[cont_intro, partial_function_mono] = monotone2monotone[OF prog.s2p.monotone, simplified]

lemma p2s:
  shows "prog.s2p (prog.p2s P) = P"
by (auto simp: prog.s2p_def simp flip: less_eq_prog.rep_eq intro: Sup_eqI)

lemma Sup_le:
  shows "⊔(prog.s2p ` X) ≤ prog.s2p (⊔X)"
by (simp add: prog.s2p_def Collect_mono SUPE Sup_subset_mono Sup_upper2)

lemma sup_le:
  shows "prog.s2p x ⊔ prog.s2p y ≤ prog.s2p (x ⊔ y)"
using prog.s2p.Sup_le[where X="{x, y}"] by simp

lemma Inf:
  shows "prog.s2p (⊓X) = ⊓(prog.s2p ` X)" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by (simp add: prog.s2p_def SupI Sup_le_iff le_Inf_iff)
  show "?rhs ≤ ?lhs"
    by (fastforce simp: prog.s2p_def prog.p2s.mono
                        Inf_Sup[where A="(λx. {c. prog.p2s c ≤ x}) ` X", simplified image_image]
                        le_Inf_iff INF_lower2
                  elim: order.trans[rotated]
                 intro: Sup_subset_mono)
qed

lemma inf:
  shows "prog.s2p (x ⊓ y) = prog.s2p x ⊓ prog.s2p y"
using prog.s2p.Inf[where X="{x, y}"] by simp

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "p2s_s2p"›

lemma galois: ―‹ the Galois connection ›
  shows "prog.p2s c ≤ S
     ⟷ c ≤ prog.s2p S ∧ spec.term.none (spec.rel ({env} × UNIV) :: (_, _, unit) spec) ≤ S" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ==> ?rhs"
    by (metis order.trans prog.s2p.mono prog.s2p.p2s spec.interference.closed.p2s
              spec.term.none.interference.closed.rel_le)
  show "?rhs ==> ?lhs"
    unfolding prog.s2p_def by transfer (force simp: spec.interference.cl.bot elim: order.trans)
qed

lemma le:
  shows "prog.p2s (prog.s2p S) ≤ spec.interference.cl ({env} × UNIV) S"
by (metis bot_prog.rep_eq prog.p2s_s2p.galois prog.s2p.mono spec.interference.cl_bot_least
          spec.interference.expansive)

lemma insertion:
  fixes S :: "(sequential, 's, 'v) spec"
  assumes "S ∈ spec.interference.closed ({env} × UNIV)"
  shows "prog.p2s (prog.s2p S) = S"
by (metis assms prog.p2s_cases prog.s2p.p2s)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Programming language constructs\label{sec:programs-language} ›

text‹

  lift the combinators directly from the 🍋‹('a,
 s ,'v) spec› lattice (\S\ref{sec:safety_logic}), but need to
 -close primitive actions. Control flow is expressed via
 's ‹if-then-else› construct and other case combinators
  the scrutinee is a pure value. This means that the atomicity of a process is completely
  by occurrences of ‹prog.action›.

 ›

setup ‹Sign.mandatory_path "prog"›

lift_definition bind :: "('s, 'v) prog ==> ('v ==> ('s, 'w) prog) ==> ('s, 'w) prog" is
  spec.bind ..

adhoc_overloading
  Monad_Syntax.bind ⇌ prog.bind

lift_definition action :: "('v × 's × 's) set ==> ('s, 'v) prog" is
  "λF. spec.interference.cl ({env} × UNIV) (spec.action (map_prod id (Pair self) ` F))" ..

abbreviation (input) det_action :: "('s ==> ('v × 's)) ==> ('s, 'v) prog" where
  "det_action f ≡ prog.action {(v, s, s'). (v, s') = f s}"

definition return :: "'v ==> ('s, 'v) prog" where
  "return v = prog.action ({v} × Id)"

definition guard :: "'s pred ==> ('s, unit) prog" where
  "guard g ≡ prog.action ({()} × Diag g)"

abbreviation (input) read :: "('s ==> 'v) ==> ('s, 'v) prog" where
  "read F ≡ prog.action {(F s, s, s) |s. True}"

abbreviation (input) "write" :: "('s ==> 's) ==> ('s, unit) prog" where
  "write F ≡ prog.action {((), s, F s) |s. True}"

lift_definition Parallel :: "'a set ==> ('a ==> ('s, unit) prog) ==> ('s, unit) prog" is spec.Parallel
by (rule spec.interference.closed.Parallel)

lift_definition parallel :: "('s, unit) prog ==> ('s, unit) prog ==> ('s, unit) prog" is spec.parallel
by (simp add: spec.parallel_def spec.interference.closed.Parallel)

lift_definition vmap :: "('v ==> 'w) ==> ('s, 'v) prog ==> ('s, 'w) prog" is spec.vmap
by (rule subsetD[OF spec.interference.closed.antimono spec.interference.closed.map_sf_id, rotated])
   auto

adhoc_overloading
  Parallel ⇌ prog.Parallel
adhoc_overloading
  parallel ⇌ prog.parallel

lemma return_alt_def:
  shows "prog.return v = prog.read ⟨v⟩"
by (auto simp: prog.return_def intro: arg_cong[where f="prog.action"])

lemma parallel_alt_def:
  shows "prog.parallel P Q = prog.Parallel UNIV (λa::bool. if a then P else Q)"
by transfer (simp add: spec.parallel_def)

lift_definition rel :: "'s rel ==> ('s, 'v) prog" is "λr. spec.rel ({env} × UNIV ∪ {self} × r)"
by (simp add: spec.interference.closed.rel)

lift_definition steps :: "('s, 'v) prog ==> 's rel" is "λP. spec.steps P `` {self}" .

lift_definition invmap :: "('s ==> 't) ==> ('v ==> 'w) ==> ('t, 'w) prog ==> ('s, 'v) prog" is
  "spec.invmap id"
by (rule subsetD[OF spec.interference.closed.antimono spec.interference.closed.invmap, rotated])
   auto

abbreviation sinvmap ::"('s ==> 't) ==> ('t, 'v) prog ==> ('s, 'v) prog" where
  "sinvmap sf ≡ prog.invmap sf id"
abbreviation vinvmap ::"('v ==> 'w) ==> ('s, 'w) prog ==> ('s, 'v) prog" where
  "vinvmap vf ≡ prog.invmap id vf"

declare prog.bind_def[code del]
declare prog.action_def[code del]
declare prog.return_def[code del]
declare prog.Parallel_def[code del]
declare prog.parallel_def[code del]
declare prog.vmap_def[code del]
declare prog.rel_def[code del]
declare prog.steps_def[code del]
declare prog.invmap_def[code del]


subsubsection‹ Laws of programming \label{sec:programs-laws} ›

setup ‹Sign.mandatory_path "p2s"›

lemma bind[prog.p2s.simps]:
  shows "prog.p2s (f 🍋 g) = prog.p2s f 🍋 (λx. prog.p2s (g x))"
by transfer simp

lemmas action = prog.action.rep_eq

lemma return:
  shows "prog.p2s (prog.return v) = spec.interference.cl ({env} × UNIV) (spec.return v)"
by (simp add: prog.return_def prog.p2s.action map_prod_image_Times Pair_image
        flip: spec.return_alt_def)

lemma guard:
  shows "prog.p2s (prog.guard g) = spec.interference.cl ({env} × UNIV) (spec.guard g)"
by (simp add: prog.guard_def prog.p2s.action map_prod_image_Times Pair_image
        flip: spec.guard.alt_def[where A="{self}"])

lemmas Parallel[prog.p2s.simps] = prog.Parallel.rep_eq[simplified, of as Ps for as Ps, unfolded comp_def]
lemmas parallel[prog.p2s.simps] = prog.parallel.rep_eq
lemmas invmap[prog.p2s.simps] = prog.invmap.rep_eq
lemmas rel[prog.p2s.simps] = prog.rel.rep_eq

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "return"›

lemma transfer[transfer_rule]:
  shows "rel_fun (=) cr_prog (λv. spec.interference.cl ({env} × UNIV) (spec.return v)) prog.return"
by (simp add: rel_funI cr_prog_def prog.p2s.return)

lemma cong:
  fixes F :: "('v × 's × 's) set"
  assumes "∧v s s'. (v, s, s') ∈ F ==> s' = s"
  assumes "∧v s s' s''. v ∈ fst ` F ==> (v, s, s) ∈ F"
  shows "prog.action F = (⊔(v, s, s')∈F. prog.return v)"
using assms
by transfer
   (subst spec.return.cong;
    fastforce simp: spec.interference.cl.action spec.interference.cl.return
                    spec.interference.cl.Sup spec.interference.cl.sup spec.interference.cl.idle
                    spec.interference.cl.bot image_image split_def
             intro: map_prod_imageI[where f=id, simplified])

lemma rel_le:
  shows "prog.return v ≤ prog.rel r"
by transfer (simp add: spec.interference.least spec.interference.closed.rel spec.return.rel_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "action"›

lemma empty:
  shows "prog.action {} = ⊥"
by transfer
   (simp add: spec.action.empty spec.interference.cl.bot spec.interference.cl.idle
        flip: bot_fun_def spec.bind.botR)

lemma monotone:
  shows "mono (prog.action :: _ ==> ('s, 'v) prog)"
proof(transfer, rule monotoneI)
  show "spec.interference.cl ({env} × UNIV) (spec.action (map_prod id (Pair self) ` F))
     ≤ spec.interference.cl ({env} × UNIV) (spec.action (map_prod id (Pair self) ` F'))"
    if "F ⊆ F'" for F F' :: "('v × 's × 's) set"
    by (strengthen ord_to_strengthen(1)[OF ‹F ⊆ F'›]) simp
qed

lemmas strengthen[strg] = st_monotone[OF prog.action.monotone]
lemmas mono = monotoneD[OF prog.action.monotone]
lemmas mono2mono[cont_intro, partial_function_mono] = monotone2monotone[OF prog.action.monotone, simplified]

lemma Sup:
  shows "prog.action (⊔Fs) = (⊔F∈Fs. prog.action F)"
by transfer
   (simp add: spec.interference.cl.bot spec.interference.cl.Sup spec.interference.cl.sup
              spec.interference.cl.idle spec.interference.cl.action spec.action.Sup image_Union image_image
        flip: bot_fun_def spec.bind.botR)

lemmas sup = prog.action.Sup[where Fs="{F, G}" for F G, simplified]

lemma Inf_le:
  shows "prog.action (⊓Fs) ≤ (⊓F∈Fs. prog.action F)"
apply transfer
apply (strengthen ord_to_strengthen(1)[OF image_Inter_subseteq])
apply (strengthen ord_to_strengthen(1)[OF spec.action.Inf_le])
apply (strengthen ord_to_strengthen(1)[OF spec.interference.cl_Inf_le])
apply (blast intro: Inf_mono)
done

lemma inf_le:
  shows "prog.action (F ⊓ G) ≤ prog.action F ⊓ prog.action G"
using prog.action.Inf_le[where Fs="{F, G}"] by simp

lemma sinvmap_le: ―‹ a strict refinement ›
  shows "prog.p2s (prog.action (map_prod id (map_prod sf sf) -` F))
      ≤ spec.sinvmap sf (prog.p2s (prog.action F))"
by (force intro: order.trans[OF _ spec.interference.cl.mono[OF order.refl spec.action.invmap_le]]
                 spec.interference.cl.mono spec.action.mono
           simp: prog.p2s.action spec.invmap.interference.cl)

lemma return_const:
  fixes F :: "'s rel"
  fixes V :: "'v set"
  fixes W :: "'w set"
  assumes "V ≠ {}"
  assumes "W ≠ {}"
  shows "prog.action (V × F) = prog.action (W × F) 🍋 (⊔v∈V. prog.return v)"
using assms(1)
by (simp add: prog.p2s.simps prog.p2s.action prog.p2s.return image_image
              map_prod_image_Times spec.action.return_const[OF assms]
              spec.bind.SUPR_not_empty spec.interference.cl.bind_return
              spec.interference.cl.return spec.interference.cl_Sup_not_empty
              spec.interference.closed.bind_relR
        flip: prog.p2s_inject)

lemma rel_le:
  assumes "∧v s s'. (v, s, s') ∈ F ==> (s, s') ∈ r ∨ s = s'"
  shows "prog.action F ≤ prog.rel r"
by (auto intro: order.trans[OF spec.interference.cl.mono[OF order.refl
                                                            spec.action.rel_le[where r="{self} × r ∪ {env} × UNIV"]]]
          dest: assms
          simp: less_eq_prog.rep_eq prog.p2s.simps prog.p2s.action spec.interference.cl.rel ac_simps)

lemma invmap_le:
  shows "prog.action (map_prod vf (map_prod sf sf) -` F) ≤ prog.invmap sf vf (prog.action F)"
by transfer
   (force simp: spec.invmap.interference.cl
         intro: spec.interference.cl.mono
                spec.action.mono order.trans[OF _ spec.interference.cl.mono[OF order.refl spec.action.invmap_le]])

lemma action_le:
  shows "spec.action (map_prod id (Pair self) ` F) ≤ prog.p2s (prog.action F)"
by (simp add: prog.p2s.action spec.interference.expansive)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "bind"›

lemmas if_distrL = if_distrib[where f="λx. x 🍋 g" for g :: "_ ==> (_, _) prog"]

lemma mono:
  assumes "f ≤ f'"
  assumes "∧x. g x ≤ g' x"
  shows "prog.bind f g ≤ prog.bind f' g'"
using assms by transfer (simp add: spec.bind.mono)

lemma strengthen[strg]:
  assumes "st_ord F f f'"
  assumes "∧x. st_ord F (g x) (g' x)"
  shows "st_ord F (prog.bind f g) (prog.bind f' g')"
using assms by (cases F; clarsimp intro!: prog.bind.mono)

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≤) f"
  assumes "∧x. monotone orda (≤) (λy. g y x)"
  shows "monotone orda (≤) (λx. prog.bind (f x) (g x))"
using assms by transfer simp

text‹ The monad laws hold unconditionally in the 🍋‹('s, 'v) prog› lattice. ›

lemma bind:
  shows "f 🍋 g 🍋 h = prog.bind f (λx. g x 🍋 h)"
by transfer (simp add: spec.bind.bind)

lemma return:
  shows returnL: "(🍋) (prog.return v) = (λg :: 'v ==> ('s, 'w) prog. g v)" (is ?thesis1)
    and returnR: "f 🍋 prog.return = f" (is ?thesis2)
proof -
  have "prog.return v 🍋 g = g v" for g :: "'v ==> ('s, 'w) prog"
    by transfer
       (simp add: map_prod_image_Times Pair_image spec.action.read_agents
                  spec.interference.cl.return spec.bind.bind
                  spec.bind.returnL spec.idle_le prog.p2s_induct spec.interference.closed.bind_relL
            flip: spec.return_def)
  then show ?thesis1
    by (simp add: fun_eq_iff)
  show ?thesis2
    by transfer
       (simp add: map_prod_image_Times Pair_image spec.action.read_agents
            flip: spec.interference.cl.bindL spec.return_def spec.interference.closed_conv)
qed

lemma botL:
  shows "prog.bind ⊥ = ⊥"
by (simp add: fun_eq_iff prog.p2s.simps spec.interference.cl.bot
        flip: prog.p2s_inject)

lemma botR_le:
  shows "prog.bind f ⟨⊥⟩ ≤ f" (is ?thesis1)
    and "prog.bind f ⊥ ≤ f" (is ?thesis2)
proof -
  show ?thesis1
    by (metis bot.extremum dual_order.refl prog.bind.mono prog.bind.returnR)
  then show ?thesis2
    by (simp add: bot_fun_def)
qed

lemma
  fixes f :: "(_, _) prog"
  fixes f₁ :: "(_, _) prog"
  shows supL: "(f₁ ⊔ f₂) 🍋 g = (f₁ 🍋 g) ⊔ (f₂ 🍋 g)"
    and supR: "f 🍋 (λx. g₁ x ⊔ g₂ x) = (f 🍋 g₁) ⊔ (f 🍋 g₂)"
by (transfer; blast intro: spec.bind.supL spec.bind.supR)+

lemma SUPL:
  fixes X :: "_ set"
  fixes f :: "_ ==> (_, _) prog"
  shows "(⊔x∈X. f x) 🍋 g = (⊔x∈X. f x 🍋 g)"
by transfer
   (simp add: spec.interference.cl.bot spec.bind.supL spec.bind.bind spec.bind.SUPL
        flip: spec.bind.botR bot_fun_def)

lemma SUPR:
  fixes X :: "_ set"
  fixes f :: "(_, _) prog"
  shows "f 🍋 (λv. ⊔x∈X. g x v) = (⊔x∈X. f 🍋 g x) ⊔ (f 🍋 ⊥)"
unfolding bot_fun_def
by transfer
   (simp add: spec.bind.supL spec.bind.supR spec.bind.bind spec.bind.SUPR ac_simps le_supI2
              spec.interference.closed.bind_rel_botR
              sup.absorb2 spec.interference.closed.bind spec.interference.least spec.bind.mono
        flip: spec.bind.botR)

lemma SupR:
  fixes X :: "_ set"
  fixes f :: "(_, _) prog"
  shows "f 🍋 (⊔X) = (⊔x∈X. f 🍋 x) ⊔ (f 🍋 ⊥)"
by (simp add: prog.bind.SUPR[where g="λx v. x", simplified])

lemma SUPR_not_empty:
  fixes f :: "(_, _) prog"
  assumes "X ≠ {}"
  shows "f 🍋 (λv. ⊔x∈X. g x v) = (⊔x∈X. f 🍋 g x)"
using iffD2[OF ex_in_conv assms]
by (subst trans[OF prog.bind.SUPR sup.absorb1]; force intro: SUPI prog.bind.mono)

lemma mcont2mcont[cont_intro]:
  assumes "mcont luba orda Sup (≤) f"
  assumes "∧v. mcont luba orda Sup (≤) (λx. g x v)"
  shows "mcont luba orda Sup (≤) (λx. prog.bind (f x) (g x))"
proof(rule ccpo.mcont2mcont'[OF complete_lattice_ccpo _ _ assms(1)])
  show "mcont Sup (≤) Sup (≤) (λf. prog.bind f (g x))" for x
    by (intro mcontI contI monotoneI) (simp_all add: prog.bind.mono flip: prog.bind.SUPL)
  show "mcont luba orda Sup (≤) (λx. prog.bind f (g x))" for f
    by (intro mcontI monotoneI contI)
       (simp_all add: mcont_monoD[OF assms(2)] prog.bind.mono
                flip: prog.bind.SUPR_not_empty contD[OF mcont_cont[OF assms(2)]])
qed

lemma inf_rel:
  shows "prog.rel r ⊓ (f 🍋 g) = prog.rel r ⊓ f 🍋 (λx. prog.rel r ⊓ g x)"
    and "(f 🍋 g) ⊓ prog.rel r = prog.rel r ⊓ f 🍋 (λx. prog.rel r ⊓ g x)"
by (transfer; simp add: spec.bind.inf_rel)+

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "guard"›

lemma bot:
  shows "prog.guard ⊥ = ⊥"
    and "prog.guard ⟨False⟩ = ⊥"
by (simp_all add: prog.guard_def prog.action.empty)

lemma top:
  shows "prog.guard (⊤::'a pred) = prog.return ()" (is ?thesis1)
    and "prog.guard (⟨True⟩::'a pred) = prog.return ()" (is ?thesis2)
proof -
  show ?thesis1
    unfolding prog.guard_def prog.return_def by transfer (simp add: Id_def)
  then show ?thesis2
    by (simp add: top_fun_def)
qed

lemma return_le:
  shows "prog.guard g ≤ prog.return ()"
unfolding prog.guard_def Diag_def prog.return_def
by transfer (blast intro: spec.interference.cl.mono spec.action.mono)

lemma monotone:
  shows "mono (prog.guard :: 's pred ==> _)"
proof(rule monoI)
  show "prog.guard g ≤ prog.guard h" if "g ≤ h" for g h :: "'s pred"
    unfolding prog.guard_def
    by (strengthen ord_to_strengthen(1)[OF that]) (rule order.refl)
qed

lemmas strengthen[strg] = st_monotone[OF prog.guard.monotone]
lemmas mono = monotoneD[OF prog.guard.monotone]
lemmas mono2mono[cont_intro, partial_function_mono] = monotone2monotone[OF prog.guard.monotone, simplified]

lemma less: ―‹ Non-triviality ›
  assumes "g < g'"
  shows "prog.guard g < prog.guard g'"
proof(rule le_neq_trans)
  show "prog.guard g ≤ prog.guard g'"
    by (strengthen ord_to_strengthen(1)[OF order_less_imp_le[OF assms]]) simp
  from assms obtain s where "g' s" "¬g s" by (metis leD predicate1I)
  from ‹¬g s› have "¬(•trace.T s [] (Some ())•) ≤ prog.p2s (prog.guard g)"
    by (fastforce simp: trace.split_all prog.p2s.guard spec.guard_def spec.interference.cl.action
                        spec.singleton.le_conv spec.singleton.action_le_conv trace.steps'.step_conv
                  elim: spec.singleton.bind_le)
  moreover
  from ‹g' s› have "(•trace.T s [] (Some ())•) ≤ prog.p2s (prog.guard g')"
    by (force simp: prog.p2s.guard prog.p2s.action spec.guard_def
             intro: order.trans[OF _ spec.interference.expansive] spec.action.stutterI)
  ultimately show "prog.guard g ≠ prog.guard g'" by metis
qed

lemma "if":
  shows "(if b then t else e) = (prog.guard ⟨b⟩ 🍋 t) ⊔ (prog.guard ⟨¬b⟩ 🍋 e)"
by (auto simp: prog.guard.bot prog.guard.top prog.bind.returnL prog.bind.botL)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "Parallel"›

lemma bot:
  assumes "∧a. a ∈ bs ==> Ps a = ⊥"
  assumes "as ∩ bs ≠ {}"
  shows "prog.Parallel as Ps = prog.Parallel (as - bs) Ps 🍋 ⊥"
by (auto simp: assms(1)
               prog.p2s.simps spec.interference.cl.bot
               spec.interference.closed.bind_rel_unitR spec.interference.closed.Parallel
               spec.term.none.Parallel_some_agents[OF _ assms(2), where Ps'="⟨spec.rel ({env} × UNIV)⟩"]
               spec.Parallel.discard_interference[where as=as and bs="as ∩ bs"]
     simp del: Int_iff
    simp flip: prog.p2s_inject spec.bind.botR spec.bind.bind
        intro: arg_cong[OF spec.Parallel.cong])

lemma mono:
  assumes "∧a. a ∈ as ==> Ps a ≤ Ps' a"
  shows "prog.Parallel as Ps ≤ prog.Parallel as Ps'"
using assms by transfer (blast intro: spec.Parallel.mono)

lemma strengthen_Parallel[strg]:
  assumes "∧a. a ∈ as ==> st_ord F (Ps a) (Ps' a)"
  shows "st_ord F (prog.Parallel as Ps) (prog.Parallel as Ps')"
using assms by (cases F) (auto simp: prog.Parallel.mono)

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "∧a. a ∈ as ==> monotone orda (≤) (F a)"
  shows "monotone orda (≤) (λf. prog.Parallel as (λa. F a f))"
using assms by transfer (simp add: spec.Parallel.mono2mono)

lemma cong:
  assumes "as = as'"
  assumes "∧a. a ∈ as' ==> Ps a = Ps' a"
  shows "prog.Parallel as Ps = prog.Parallel as' Ps'"
using assms by transfer (rule spec.Parallel.cong; simp)

lemma no_agents:
  shows "prog.Parallel {} Ps = prog.return ()"
by transfer
   (simp add: spec.Parallel.no_agents spec.interference.cl.return map_prod_image_Times Pair_image
              spec.action.read_agents)

lemma singleton_agents:
  shows "prog.Parallel {a} Ps = Ps a"
by transfer (rule spec.Parallel.singleton_agents)

lemma rename_UNIV:
  assumes "inj_on f as"
  shows "prog.Parallel as Ps
       = prog.Parallel UNIV (λb. if b ∈ f ` as then Ps (inv_into as f b) else prog.return ())"
by (simp add: prog.p2s.simps if_distrib prog.p2s.return spec.interference.cl.return
              spec.Parallel.rename_UNIV[OF assms]
        flip: prog.p2s_inject
        cong: spec.Parallel.cong if_cong)

lemmas rename = spec.Parallel.rename[transferred]

lemma return:
  assumes "∧a. a ∈ bs ==> Ps a = prog.return ()"
  shows "prog.Parallel as Ps = prog.Parallel (as - bs) Ps"
by (subst (1 2) prog.Parallel.rename_UNIV[where f=id, simplified])
   (auto intro: arg_cong[where f="prog.Parallel UNIV"]
          simp: assms fun_eq_iff f_inv_into_f[where f=id, simplified])

lemma unwind:
  assumes a: "f 🍋 g ≤ Ps a" ―‹ The selected process starts with action ‹f› ›
  assumes "a ∈ as"
  shows "f 🍋 (λv. prog.Parallel as (Ps(a:=g v))) ≤ prog.Parallel as Ps"
using assms by transfer (simp add: spec.Parallel.unwind spec.interference.closed.bind_relL)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "parallel"›

lemmas commute = spec.parallel.commute[transferred]
lemmas assoc = spec.parallel.assoc[transferred]
lemmas mono = spec.parallel.mono[transferred]

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

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

lemma bot:
  shows botL: "prog.parallel ⊥ P = P 🍋 ⊥" (is ?thesis1)
    and botR: "prog.parallel P ⊥ = P 🍋 ⊥" (is ?thesis2)
proof -
  show ?thesis1
    by (simp add: prog.parallel_alt_def prog.Parallel.bot[where bs="{True}", simplified]
                  prog.Parallel.singleton_agents
            cong: prog.Parallel.cong)
  then show ?thesis2
    by (simp add: prog.parallel.commute)
qed

lemma return:
  shows returnL: "prog.return () ∥ P = P" (is ?thesis1)
    and returnR: "P ∥ prog.return () = P" (is ?thesis2)
proof -
  show ?thesis1
    by (simp add: prog.parallel_alt_def prog.Parallel.return[where bs="{True}", simplified]
                  prog.Parallel.singleton_agents)
  then show ?thesis2
    by (simp add: prog.parallel.commute)
qed

lemma Sup_not_empty:
  fixes X :: "(_, unit) prog set"
  assumes "X ≠ {}"
  shows SupL_not_empty: "⊔X ∥ Q = (⊔P∈X. P ∥ Q)" (is "?thesis1 Q")
    and SupR_not_empty: "P ∥ ⊔X = (⊔Q∈X. P ∥ Q)" (is ?thesis2)
proof -
  from assms show "?thesis1 Q" for Q
    by (simp add: prog.p2s.parallel prog.p2s.Sup_not_empty[OF assms] image_image
                  spec.parallel.Sup prog.p2s.SUP_not_empty
            flip: prog.p2s_inject)
  then show ?thesis2
    by (simp add: prog.parallel.commute)
qed

lemma sup:
  fixes P :: "(_, unit) prog"
  shows supL: "P ⊔ Q ∥ R = (P ∥ R) ⊔ (Q ∥ R)"
    and supR: "P ∥ Q ⊔ R = (P ∥ Q) ⊔ (P ∥ R)"
using prog.parallel.SupL_not_empty[where X="{P, Q}"] prog.parallel.SupR_not_empty[where X="{Q, R}"] by simp_all

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

lemma unwindL:
  fixes f :: "('s, 'v) prog"
  assumes a: "f 🍋 g ≤ P" ―‹ The selected process starts with action ‹f› ›
  shows "f 🍋 (λv. g v ∥ Q) ≤ P ∥ Q"
unfolding prog.parallel_alt_def
by (strengthen ord_to_strengthen[OF prog.Parallel.unwind[where a=True]])
   (auto simp: prog.Parallel.mono prog.bind.mono intro: assms)

lemma unwindR:
  fixes f :: "('s, 'v) prog"
  assumes a: "f 🍋 g ≤ Q" ―‹ The selected process starts with action ‹f› ›
  shows "f 🍋 (λv. P ∥ g v) ≤ P ∥ Q"
by (subst (1 2) prog.parallel.commute) (rule prog.parallel.unwindL[OF assms])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "bind"›

lemma parallel_le:
  fixes P :: "(_, _) prog"
  shows "P 🍋 Q ≤ P ∥ Q"
by (strengthen ord_to_strengthen[OF prog.parallel.unwindL[where g=prog.return, simplified prog.bind.returnR, OF order.refl]])
   (simp add: prog.parallel.return)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap"›

lemma bot:
  shows "prog.invmap sf vf ⊥ = (prog.rel (map_prod sf sf -` Id) :: (_, unit) prog) 🍋 ⊥"
by (auto simp: prog.p2s.simps spec.interference.cl.bot spec.rel.wind_bind_trailing
               spec.invmap.bind spec.invmap.rel spec.invmap.bot
    simp flip: prog.p2s_inject spec.bind.botR spec.bind.bind bot_fun_def
        intro: arg_cong[where f="λr. spec.rel r 🍋 ⊥"])

lemma id:
  shows "prog.invmap id id P = P"
    and "prog.invmap (λx. x) (λx. x) P = P"
by (transfer; simp add: spec.invmap.id id_def)+

lemma comp:
  shows "prog.invmap sf vf (prog.invmap sg vg P) = prog.invmap (λs. sg (sf s)) (λs. vg (vf s)) P" (is "?thesis1 P")
    and "prog.invmap sf vf ∘ prog.invmap sg vg = prog.invmap (sg ∘ sf) (vg ∘ vf)" (is "?thesis2")
proof -
  show "?thesis1 P" for P by transfer (simp add: spec.invmap.comp id_def)
  then show ?thesis2 by (simp add: comp_def)
qed

lemma monotone:
  shows "mono (prog.invmap sf vf)"
unfolding monotone_def by transfer (simp add: spec.invmap.mono)

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

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≤) t"
  shows "monotone orda (≤) (λx. prog.invmap sf vf (t x))"
by (rule monotone2monotone[OF prog.invmap.monotone assms]) simp_all

lemma Sup:
  fixes sf :: "'s ==> 't"
  fixes vf :: "'v ==> 'w"
  shows "prog.invmap sf vf (⊔X) = ⊔(prog.invmap sf vf ` X) ⊔ prog.invmap sf vf ⊥"
by transfer
   (simp add: spec.invmap.bot spec.invmap.Sup spec.invmap.sup spec.invmap.bind spec.invmap.rel
              spec.interference.cl.bot map_prod_vimage_Times ac_simps
              sup.absorb2 spec.bind.mono[OF spec.rel.mono order.refl]
        flip: spec.bind.botR spec.bind.bind spec.rel.unwind_bind_trailing bot_fun_def inv_image_alt_def)

lemma Sup_not_empty:
  assumes "X ≠ {}"
  shows "prog.invmap sf vf (⊔X) = ⊔(prog.invmap sf vf ` X)"
using iffD2[OF ex_in_conv assms]
by (clarsimp simp: prog.invmap.Sup sup.absorb1 SUPI prog.invmap.mono[OF bot_least])

lemma mcont:
  shows "mcont Sup (≤) Sup (≤) (prog.invmap sf vf)"
by (simp add: contI mcontI prog.invmap.monotone prog.invmap.Sup_not_empty)

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

lemma bind:
  shows "prog.invmap sf vf (f 🍋 g) = prog.sinvmap sf f 🍋 (λv. prog.invmap sf vf (g v))"
by transfer (simp add: spec.invmap.bind)

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

lemma invmap_image_vimage_commute:
  shows "map_prod id (map_prod id sf) -` map_prod id (Pair self) ` F
       = map_prod id (Pair self) ` map_prod id sf -` F"
by (auto simp: map_prod_conv)

lemma action:
  shows "prog.invmap sf vf (prog.action F)
       = prog.rel (map_prod sf sf -` Id)
          🍋 (λ_::unit. prog.action (map_prod id (map_prod sf sf) -` F)
            🍋 (λv. prog.rel (map_prod sf sf -` Id)
              🍋 (λ_::unit. ⊔v'∈vf -` {v}. prog.return v')))"
proof -
  have *: "{env} × UNIV ∪ {self} × map_prod sf sf -` Id
         = {env} × UNIV ∪ UNIV × map_prod sf sf -` Id" by auto
  show ?thesis
    by (simp add: ac_simps prog.p2s.simps prog.p2s.action
                  spec.interference.cl.action spec.invmap.bind spec.invmap.rel spec.invmap.action spec.invmap.return
                  spec.bind.bind spec.bind.return
                  prog.invmap.invmap_image_vimage_commute map_prod_vimage_Times *
            flip: prog.p2s_inject)
       (simp add: prog.p2s.Sup image_image prog.p2s.simps prog.p2s.return spec.interference.cl.return
                  spec.interference.cl.bot spec.bind.supR
                  spec.rel.wind_bind_leading spec.rel.wind_bind_trailing
            flip: spec.bind.botR spec.bind.SUPR spec.bind.bind)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "vmap"›

lemma bot:
  shows "prog.vmap vf ⊥ = ⊥"
by transfer
   (simp add: spec.interference.cl.bot spec.vmap.unit_rel
        flip: spec.term.none.map_gen[where vf="⟨()⟩"])

lemma unitL:
  shows "f 🍋 g = prog.vmap ⟨()⟩ f 🍋 g"
by transfer (metis spec.vmap.unitL)

lemma eq_return:
  shows "prog.vmap vf P = P 🍋 prog.return ∘ vf" (is ?thesis1)
    and "prog.vmap vf P = P 🍋 (λv. prog.return (vf v))" (is ?thesis2)
proof -
  show ?thesis1
    by transfer
       (simp add: comp_def spec.vmap.eq_return spec.interference.cl.return spec.interference.closed.bind_relR)
  then show ?thesis2
    by (simp add: comp_def)
qed

lemma action:
  shows "prog.vmap vf (prog.action F) = prog.action (map_prod vf id ` F)"
by transfer (simp add: spec.map.interference.cl_sf_id spec.map.surj_sf_action image_comp)

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

setup ‹Sign.parent_path›

interpretation kleene: kleene "prog.return ()" "λx y. prog.bind x ⟨y⟩"
by standard
   (simp_all add: prog.bind.bind prog.bind.return prog.bind.botL prog.bind.supL prog.bind.supR)

interpretation rel: galois.complete_lattice_class prog.steps prog.rel
proof
  show "prog.steps P ⊆ r ⟷ P ≤ prog.rel r" for P :: "('a, 'b) prog" and r :: "'a rel"
    by transfer (auto simp flip: spec.rel.galois)
qed

setup ‹Sign.mandatory_path "rel"›

lemma empty:
  shows "prog.rel {} = ⊔range prog.return"
by (simp add: prog.p2s.simps prog.p2s.return image_image
              spec.interference.cl.bot spec.interference.cl.return
              spec.term.closed.bind_all_return[OF spec.term.closed.rel] spec.term.all.rel
              sup.absorb1 spec.term.galois
        flip: prog.p2s_inject spec.bind.SUPR_not_empty)

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

lemmas Inf = prog.rel.upper_Inf
lemmas inf = prog.rel.upper_inf

lemma reflcl:
  shows "prog.rel (r ∪ Id) = (prog.rel r :: ('s, 'v) prog)" (is ?thesis1)
    and "prog.rel (Id ∪ r) = (prog.rel r :: ('s, 'v) prog)" (is ?thesis2)
proof -
  show ?thesis1
    by transfer
       (subst (2) spec.rel.reflcl[where A=UNIV, symmetric];
        auto intro: arg_cong[where f="spec.rel"])
  then show ?thesis2
    by (simp add: ac_simps)
qed

lemma minus_Id:
  shows "prog.rel (r - Id) = prog.rel r"
by (metis Un_Diff_cancel2 prog.rel.reflcl(1))

lemma Id:
  shows "prog.rel Id = ⊔range prog.return"
by (simp add: prog.rel.reflcl(1)[where r="{}", simplified] prog.rel.empty)

lemma unfoldL:
  fixes r :: "'s rel"
  assumes "Id ⊆ r"
  shows "prog.rel r = prog.action ({()} × r) 🍋 prog.rel r"
proof -
  have *: "spec.rel ({env} × UNIV)
             🍋 (λv::unit. spec.action (map_prod id (Pair self) ` ({()} × r))
             🍋 (λv::unit. spec.rel ({env} × UNIV ∪ {self} × r)))
         = spec.rel ({env} × UNIV ∪ {self} × r)" (is "?lhs = ?rhs")
    if "Id ⊆ r"
   for r :: "'s rel"
  proof(rule antisym)
    let ?r' = "{env} × UNIV ∪ {self} × r"
    have "?lhs ≤ spec.rel ?r' 🍋 (λ_::unit. spec.rel ?r' 🍋 (λ_::unit. spec.rel ?r'))"
      by (fastforce intro: spec.bind.mono spec.rel.mono spec.action.mono
                           order.trans[OF _ spec.rel.monomorphic_act_le]
                     simp: spec.rel.act_def)
    also have "… = ?rhs"
      by (simp add: spec.rel.wind_bind)
    finally show "?lhs ≤ ?rhs" .
    from that show "?rhs ≤ ?lhs"
      apply -
      apply (rule order.trans[OF _
              spec.bind.mono[OF spec.return.rel_le
                spec.bind.mono[OF spec.action.mono[where x="{()} × {self} × Id"] order.refl]]])
       apply (subst spec.return.cong; simp add: image_image spec.bind.supL spec.bind.supR spec.bind.returnL spec.idle_le)
      apply (fastforce simp: map_prod_image_Times)
      done
  qed
  from assms show ?thesis
    by transfer (simp add: * spec.interference.cl.action spec.bind.bind spec.rel.wind_bind_leading)
qed

lemma wind_bind: ―‹ arbitrary interstitial return type ›
  shows "prog.rel r 🍋 prog.rel r = prog.rel r"
by transfer (simp add: spec.rel.wind_bind)

lemma wind_bind_leading: ―‹ arbitrary interstitial return type ›
  assumes "r' ⊆ r"
  shows "prog.rel r' 🍋 prog.rel r = prog.rel r"
using assms by transfer (subst spec.rel.wind_bind_leading; blast)

lemma wind_bind_trailing: ―‹ arbitrary interstitial return type ›
  assumes "r' ⊆ r"
  shows "prog.rel r 🍋 prog.rel r' = prog.rel r" (is "?lhs = ?rhs")
using assms by transfer (subst spec.rel.wind_bind_trailing; blast)

text‹ Interstitial unit, for unfolding ›

lemmas unwind_bind = prog.rel.wind_bind[where 'c=unit, symmetric]
lemmas unwind_bind_leading = prog.rel.wind_bind_leading[where 'c=unit, symmetric]
lemmas unwind_bind_trailing = prog.rel.wind_bind_trailing[where 'c=unit, symmetric]

lemma mono_conv:
  shows "prog.rel r = prog.kleene.star (prog.action ({()} × r⁼))" (is "?lhs = ?rhs")
proof(rule antisym)
  have "spec.kleene.star (spec.rel.act ({env} × UNIV ∪ {self} × r)) ≤ prog.p2s ?rhs"
  proof(induct rule: spec.kleene.star.fixp_induct[case_names adm bot step])
    case (step R) show ?case
    proof(induct rule: le_supI[case_names act_step ret])
      case act_step
      have *: "spec.rel.act ({env} × UNIV ∪ {self} × r) ≤ prog.p2s (prog.action ({()} × r⁼))"
        by (auto simp: spec.rel.act_alt_def Times_Un_distrib2 spec.action.sup
                       prog.p2s.sup prog.p2s.return spec.interference.cl.return prog.action.sup map_prod_conv
            simp flip: prog.return_def
                intro: spec.action.mono le_supI2 spec.action.rel_le spec.return.rel_le
                       le_supI1[OF order.trans[OF spec.action.mono prog.action.action_le]])
      show ?case
        apply (subst prog.kleene.star.simps)
        apply (strengthen ord_to_strengthen(1)[OF step])
        apply (simp add: prog.p2s.simps le_supI1[OF spec.bind.mono[OF * order.refl]])
        done
    next
      case ret show ?case
        by (simp add: order.trans[OF _ prog.p2s.mono[OF prog.kleene.epsilon_star_le]]
                      prog.p2s.return spec.interference.expansive)
    qed
  qed simp_all
  then show "?lhs ≤ ?rhs"
    by (simp add: prog.p2s_leI prog.p2s.simps spec.rel.monomorphic_conv)
  show "?rhs ≤ ?lhs"
  proof(induct rule: prog.kleene.star.fixp_induct[case_names adm bot step])
    case (step R) show ?case
      apply (strengthen ord_to_strengthen(1)[OF step])
      apply (simp add: prog.return.rel_le)
      apply (subst (2) prog.rel.unwind_bind)
      apply (auto intro: prog.bind.mono prog.action.rel_le)
      done
  qed simp_all
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "action"›

lemma inf_rel:
  assumes "refl r"
  shows "prog.action F ⊓ prog.rel r = prog.action (F ∩ UNIV × r)" (is ?thesis1)
    and "prog.rel r ⊓ prog.action F = prog.action (F ∩ UNIV × r)" (is ?thesis2)
proof -
  from assms have "refl (({env} × UNIV ∪ {self} × r) `` {a})" for a
    by (fastforce dest: reflD intro: reflI)
  then show ?thesis1
    by transfer (simp add: spec.interference.cl.inf_rel spec.action.inf_rel; rule arg_cong; blast)
  then show ?thesis2
    by (rule inf_commute_conv)
qed

lemma inf_rel_reflcl:
  shows "prog.action F ⊓ prog.rel r = prog.action (F ∩ UNIV × r⁼)"
    and "prog.rel r ⊓ prog.action F = prog.action (F ∩ UNIV × r⁼)"
by (simp_all add: refl_on_def prog.rel.reflcl ac_simps flip: prog.action.inf_rel)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "return"›

lemma not_bot:
  shows "prog.return v ≠ (⊥ :: ('s, 'v) prog)"
using prog.guard.less[where g="⊥::'s pred" and g'=top]
by (force dest: arg_cong[where f="prog.vmap (λ_::'v. ())"]
          simp: prog.vmap.return prog.vmap.bot fun_eq_iff prog.guard.bot prog.guard.top
     simp flip: top.not_eq_extremum)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap"›

lemma return:
  shows "prog.invmap sf vf (prog.return v)
       = prog.rel (map_prod sf sf -` Id) 🍋 (λ_::unit. ⊔v'∈vf -` {v}. prog.return v')"
apply (simp add: prog.return_def prog.invmap.action map_prod_vimage_Times)
apply (simp add: prog.action.return_const[where V="{v}" and W="{()}"] prog.bind.bind prog.bind.return)
apply (subst prog.bind.bind[symmetric], subst prog.rel.unfoldL[symmetric];
       force simp: prog.rel.wind_bind simp flip: prog.bind.bind)
done

lemma split_vinvmap:
  fixes P :: "('s, 'v) prog"
  shows "prog.invmap sf vf P = prog.sinvmap sf P 🍋 (λv. ⊔v'∈vf -` {v}. prog.return v')"
proof -
  note sic_invmap = spec.interference.closed.invmap[where af=id and r="{env} × UNIV",
                                                    simplified map_prod_vimage_Times, simplified]
  show ?thesis
    apply transfer
    apply (simp add: spec.bind.supR sup.absorb1 spec.interference.cl.bot bot_fun_def
                     spec.interference.closed.bind_relR sic_invmap spec.bind.mono
               flip: spec.bind.botR)
    apply (subst (1) spec.invmap.split_vinvmap)
    apply (subst (1) spec.interference.closed.bind_relR[symmetric], erule sic_invmap)
    apply (simp add: spec.bind.SUPR spec.bind.supR spec.interference.cl.return
              sup.absorb1 bot_fun_def spec.interference.closed.bind_relR sic_invmap spec.bind.mono)
    done
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Refinement for 🪙‹('s, 'v) prog›\label{sec:programs-refinement} ›

text‹

  specialize the rules of \S\ref{sec:refinement-spec} to the
 🍋‹('s, 'v) prog› lattice. Observe that, as
 , postconditions and assumes are not interference closed,
  apply the const‹prog.p2s› morphism and work in the more
  🍋‹(sequential, 's, 'v) spec›
 . This syntactic noise could be elided with another definition.

 ›


subsubsection‹ Introduction rules\label{sec:programs-refinement-intros} ›

text‹

  is a way of showing inequalities and equalities between programs.

 ›

setup ‹Sign.mandatory_path "refinement.prog"›

lemma leI:
  assumes "prog.p2s c ≤ {⟨True⟩}, ⊤ ⊨!!! prog.p2s d, {λ_. ⟨True⟩}"
  shows "c ≤ d"
using assms by (simp add: refinement_def prog.p2s_leI)

lemma eqI:
  assumes "prog.p2s c ≤ {⟨True⟩}, ⊤ ⊨!!! prog.p2s d, {λ_. ⟨True⟩}"
  assumes "prog.p2s d ≤ {⟨True⟩}, ⊤ ⊨!!! prog.p2s c, {λ_. ⟨True⟩}"
  shows "c = d"
by (rule antisym; simp add: assms refinement.prog.leI)

setup ‹Sign.parent_path›


subsubsection‹ Galois considerations\label{sec:programs-refinement-galois} ›

text‹

  quadruples ‹{P}, A ⊨!!! G, {Q}› denote points in the 🍋‹('s, 'v) prog› lattice
  ‹G› is suitably interference closed.

 ›

setup ‹Sign.mandatory_path "refinement.prog"›

lemma galois:
  assumes "spec.term.none (spec.rel ({env} × UNIV) :: (_, _, unit) spec) ≤ G"
  shows "prog.p2s c ≤ {P}, A ⊨!!! G, {Q} ⟷ c ≤ prog.s2p ({P}, A ⊨!!! G, {Q})"
by (simp add: assms prog.p2s_s2p.galois refinement_def spec.next_imp.contains spec.term.none.post_le)

lemmas s2p_refinement = iffD1[OF refinement.prog.galois, rotated]

lemma p2s_s2p:
  assumes "spec.term.none (spec.rel ({env} × UNIV) :: (_, _, unit) spec) ≤ G"
  shows "prog.p2s (prog.s2p ({P}, A ⊨!!! G, {Q})) ≤ {P}, A ⊨!!! G, {Q}"
using assms by (simp add: refinement.prog.galois)

setup ‹Sign.parent_path›


subsubsection‹ Rules\label{sec:programs-refinement-rules} ›

setup ‹Sign.mandatory_path "refinement.prog"›

lemma bot[iff]:
  shows "prog.p2s ⊥ ≤ {P}, A ⊨!!! prog.p2s c', {Q}"
by (simp add: refinement.prog.galois spec.term.none.interference.closed.rel_le)

lemma sup_conv:
  shows "prog.p2s (c₁ ⊔ c₂) ≤ {P}, A ⊨!!! G, {Q}
     ⟷ prog.p2s c₁ ≤ {P}, A ⊨!!! G, {Q} ∧ prog.p2s c₂ ≤ {P}, A ⊨!!! G, {Q}"
by (simp add: prog.p2s.simps)

lemmas sup = iffD2[OF refinement.prog.sup_conv, unfolded conj_explode]

lemma "if":
  assumes "i ==> prog.p2s t ≤ {P}, A ⊨!!! prog.p2s t', {Q}"
  assumes "¬i ==> prog.p2s e ≤ {P'}, A ⊨!!! prog.p2s e', {Q}"
  shows "prog.p2s (if i then t else e) ≤ {if i then P else P'}, A ⊨!!! prog.p2s (if i then t' else e'), {Q}"
using assms by fastforce

lemmas if' = refinement.prog.if[where P=P and P'=P, simplified] for P

lemma case_option:
  assumes "opt = None ==> prog.p2s none ≤ {P_n}, A ⊨!!! prog.p2s none', {Q}"
  assumes "∧v. opt = Some v ==> prog.p2s (some v) ≤ {P_s v}, A ⊨!!! prog.p2s (some' v), {Q}"
  shows "prog.p2s (case_option none some opt) ≤ {case opt of None ==> P_n | Some v ==> P_s v}, A ⊨!!! prog.p2s (case_option none' some' opt), {Q}"
using assms by (simp add: option.case_eq_if)

lemma case_sum:
  assumes "∧v. x = Inl v ==> prog.p2s (left v) ≤ {P_l v}, A ⊨!!! prog.p2s (left' v), {Q}"
  assumes "∧v. x = Inr v ==> prog.p2s (right v) ≤ {P_r v}, A ⊨!!! prog.p2s (right' v), {Q}"
  shows "prog.p2s (case_sum left right x) ≤ {case_sum P_l P_r x}, A ⊨!!! prog.p2s (case_sum left' right' x), {Q}"
using assms by (simp add: sum.case_eq_if)

lemma case_list:
  assumes "x = [] ==> prog.p2s nil ≤ {P_n}, A ⊨!!! prog.p2s nil', {Q}"
  assumes "∧v vs. x = v # vs ==> prog.p2s (cons v vs) ≤ {P_c v vs}, A ⊨!!! prog.p2s (cons' v vs), {Q}"
  shows "prog.p2s (case_list nil cons x) ≤ {case_list P_n P_c x}, A ⊨!!! prog.p2s (case_list nil' cons' x), {Q}"
using assms by (simp add: list.case_eq_if)

lemma action:
  fixes F :: "('v × 's × 's) set"
  assumes "∧v s s'. [P s; (v, s, s') ∈ F; (self, s, s') ∈ spec.steps A ∨ s = s'] ==> Q v s'"
  assumes "∧v s s'. [P s; (v, s, s') ∈ F] ==> (v, s, s') ∈ F'"
  assumes sP: "stable (spec.steps A `` {env}) P"
  assumes "∧v s s'. [P s; (v, s, s') ∈ F] ==> stable (spec.steps A `` {env}) (Q v)"
  shows "prog.p2s (prog.action F) ≤ {P}, A ⊨!!! prog.p2s (prog.action F'), {Q}"
unfolding prog.p2s.action spec.interference.cl.action
apply (rule refinement.pre_a[OF _ spec.rel.upper_lower_expansive])
apply (rule refinement.spec.bind[rotated])
 apply (rule refinement.spec.rel_mono[OF order.refl];
        fastforce simp: spec.term.all.rel spec.steps.rel
                 intro: sP antimonoD[OF stable.antimono_rel, unfolded le_bool_def, rule_format, rotated])
apply (strengthen ord_to_strengthen(1)[OF inf_le2])
apply (strengthen ord_to_strengthen(1)[OF refinement.spec.bind.res.rel_le[OF order.refl]])
apply (rule refinement.spec.bind[rotated, where Q'="λv s. Q v s ∧ stable (spec.steps A `` {env}) (Q v)"])
 apply (rule refinement.spec.action;
        fastforce simp: spec.initial_steps.term.all spec.initial_steps.rel
             intro: assms)
apply (rule refinement.gen_asm)
 apply (rule refinement.spec.bind[rotated])
  apply (rule refinement.spec.rel_mono[OF order.refl];
         fastforce simp: spec.steps.term.all spec.rel.lower_upper_lower
                   elim: antimonoD[OF stable.antimono_rel, unfolded le_bool_def, rule_format, rotated]
                   dest: subsetD[OF spec.steps.refinement.spec.bind.res_le])
 apply (rule refinement.spec.return)
apply (simp only: spec.idle_le)
done

lemma return:
  assumes sQ: "stable (spec.steps A `` {env}) (Q v)"
  shows "prog.p2s (prog.return v) ≤ {Q v}, A ⊨!!! prog.p2s (prog.return v), {Q}"
unfolding prog.return_def using assms by (blast intro: refinement.prog.action)

lemma invmap_return:
  assumes sQ: "stable (spec.steps A `` {env}) (Q v)"
  assumes "vf v = v'"
  shows "prog.p2s (prog.return v) ≤ {Q v}, A ⊨!!! prog.p2s (prog.invmap sf vf (prog.return v')), {Q}"
unfolding prog.invmap.return
by (strengthen ord_to_strengthen(2)[OF prog.return.rel_le])
   (simp add: assms(2) refinement.pre_g[OF refinement.prog.return[where Q=Q, OF sQ]]
              SUP_upper prog.bind.return prog.p2s.mono)

lemma bind_abstract:
  fixes f :: "('s, 'v) prog"
  fixes f' :: "('s, 'v') prog"
  fixes g :: "'v ==> ('s, 'w) prog"
  fixes g' :: "'v' ==> ('s, 'w) prog"
  fixes vf :: "'v ==> 'v'"
  assumes "∧v. prog.p2s (g v) ≤ {Q' (vf v)}, refinement.spec.bind.res (spec.pre P ⊓ spec.term.all A ⊓ prog.p2s f') A (vf v) ⊨!!! prog.p2s (g' (vf v)), {Q}"
  assumes "prog.p2s f ≤ {P}, spec.term.all A ⊨!!! spec.vinvmap vf (prog.p2s f'), {λv. Q' (vf v)}"
  shows "prog.p2s (f 🍋 g) ≤ {P}, A ⊨!!! prog.p2s (f' 🍋 g'), {Q}"
by (simp add: prog.p2s.simps refinement.spec.bind_abstract[OF assms])

lemma bind:
  assumes "∧v. prog.p2s (g v) ≤ {Q' v}, refinement.spec.bind.res (spec.pre P ⊓ spec.term.all A ⊓ prog.p2s f') A v ⊨!!! prog.p2s (g' v), {Q}"
  assumes "prog.p2s f ≤ {P}, spec.term.all A ⊨!!! prog.p2s f', {Q'}"
  shows "prog.p2s (f 🍋 g) ≤ {P}, A ⊨!!! prog.p2s (f' 🍋 g'), {Q}"
by (simp add: prog.p2s.simps refinement.spec.bind[OF assms])

lemmas rev_bind = refinement.prog.bind[rotated]

lemma Parallel:
  fixes A :: "(sequential, 's, unit) spec"
  fixes Q :: "'a ==> 's pred"
  fixes Ps :: "'a ==> ('s, unit) prog"
  fixes Ps' :: "'a ==> ('s, unit) prog"
  assumes "∧a. a ∈ as ==> prog.p2s (Ps a) ≤ {P a}, refinement.spec.env_hyp P A as (prog.p2s ∘ Ps') a ⊨!!! prog.p2s (Ps' a), {λrv. Q a}"
  shows "prog.p2s (prog.Parallel as Ps) ≤ {⊓a∈as. P a}, A ⊨!!! prog.p2s (prog.Parallel as Ps'), {λrv. ⊓a∈as. Q a}"
using assms by transfer (simp add: refinement.spec.Parallel comp_def)

lemma parallel:
  assumes "prog.p2s c₁ ≤ {P₁}, refinement.spec.env_hyp (λa. if a then P₁ else P₂) A UNIV (λa. if a then prog.p2s c₁' else prog.p2s c₂') True ⊨!!! prog.p2s c₁', {Q₁}"
  assumes "prog.p2s c₂ ≤ {P₂}, refinement.spec.env_hyp (λa. if a then P₁ else P₂) A UNIV (λa. if a then prog.p2s c₁' else prog.p2s c₂') False ⊨!!! prog.p2s c₂', {Q₂}"
  shows "prog.p2s (prog.parallel c₁ c₂) ≤ {P₁ \<and> P₂}, A ⊨!!! prog.p2s (prog.parallel c₁' c₂'), {λv. Q₁ v \<and> Q₂ v}"
unfolding prog.parallel_alt_def
by (rule refinement.pre[OF refinement.prog.Parallel[where A="A" and P="λa. if a then P₁ else P₂" and Ps'="λa. if a then c₁' else c₂'" and Q="λa. if a then Q₁ () else Q₂ ()"]])
   (use assms in ‹force simp: if_distrib comp_def›)+

setup ‹Sign.parent_path›


subsection‹ A relational assume/guarantee program logic for the 🪙‹('s, 'v) prog› lattice\label{sec:programs-ag} ›

text‹

  we specialize the assume/guarantee program logic of
 S\ref{sec:refinement-ag} to 🍋‹('s, 'v) prog›.

 :
 ▪ 🍋‹"XudeRoeverHe:1997" and "deRoeverEtAl:2001"›
 ▪ 🍋‹‹\S7› in "PrensaNieto:2003"›
 ▪ 🍋‹‹\S3› in "Vafeiadis:2008"›

 ›

subsubsection‹ Galois considerations\label{sec:programs-ag-galois} ›

text‹

  suitably stable ‹P›, ‹Q›, ‹{P}, A ⊨ G, {Q}› is interference closed and hence denotes a
  in 🍋‹('s, 'v) prog›. In other words we can replace programs with their specifications.

 ›

setup ‹Sign.mandatory_path "ag.prog"›

lemma galois:
  shows "prog.p2s c ≤ {P}, A ⊨ G, {Q} ⟷ c ≤ prog.s2p ({P}, A ⊨ G, {Q})"
by (simp add: prog.p2s_s2p.galois ag.spec.term.none_inteference)

lemmas s2p_ag = iffD1[OF ag.prog.galois]

lemma p2s_s2p_ag:
  shows "prog.p2s (prog.s2p ({P}, A ⊨ G, {Q})) ≤ {P}, A ⊨ G, {Q}"
by (simp add: ag.prog.galois)

lemma p2s_s2p_ag_stable:
  assumes "stable A P"
  assumes "∧v. stable A (Q v)"
  shows "prog.p2s (prog.s2p ({P}, A ⊨ G, {Q})) = {P}, A ⊨ G, {Q}"
by (rule prog.p2s_s2p.insertion[OF spec.interference.closed_ag[where r=UNIV, simplified, OF assms]])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "prog.ag"›

lemma bot[iff]:
  shows "prog.p2s ⊥ ≤ {P}, A ⊨ G, {Q}"
by (simp add: ag.prog.galois)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag"›

setup ‹Sign.mandatory_path "prog"›

lemma sup_conv:
  shows "prog.p2s (c₁ ⊔ c₂) ≤ {P}, A ⊨ G, {Q} ⟷ prog.p2s c₁ ≤ {P}, A ⊨ G, {Q} ∧ prog.p2s c₂ ≤ {P}, A ⊨ G, {Q}"
by (simp add: prog.p2s.simps)

lemmas sup = iffD2[OF ag.prog.sup_conv, unfolded conj_explode]

lemma bind: ―‹ Assumptions in weakest-pre order ›
  assumes "∧v. prog.p2s (g v) ≤ {Q' v}, A ⊨ G, {Q}"
  assumes "prog.p2s f ≤ {P}, A ⊨ G, {Q'}"
  shows "prog.p2s (f 🍋 g) ≤ {P}, A ⊨ G, {Q}"
by (simp add: prog.p2s.simps) (rule ag.spec.bind; fact)

lemma action: ―‹ Conclusion is insufficiently instantiated for use ›
  fixes F :: "('v × 's × 's) set"
  assumes Q: "∧v s s'. [P s; (v, s, s') ∈ F] ==> Q v s'"
  assumes G: "∧v s s'. [P s; s ≠ s'; (v, s, s') ∈ F] ==> (s, s') ∈ G"
  assumes sP: "stable A P"
  assumes sQ: "∧s s' v. [P s; (v, s, s') ∈ F] ==> stable A (Q v)"
  shows "prog.p2s (prog.action F) ≤ {P}, A ⊨ G, {Q}"
unfolding prog.p2s.action spec.interference.cl.action ―‹ sp proof ›
by (rule ag.gen_asm
         ag.spec.bind[rotated] ag.spec.stable_interference ag.spec.return
         ag.spec.action[where Q="λv s. Q v s ∧ (∃s s'. P s ∧ (v, s, s') ∈ F)"]
   | use assms in auto)+

lemma guard:
  assumes "∧s. [P s; g s] ==> Q () s"
  assumes "stable A P"
  assumes "stable A (Q ())"
  shows "prog.p2s (prog.guard g) ≤ {P}, A ⊨ G, {Q}"
using assms by (fastforce simp: prog.guard_def intro: ag.prog.action split: if_splits)

lemma Parallel:
  assumes "∧a. a ∈ as ==> prog.p2s (Ps a) ≤ {P a}, A ∪ (∪a'∈as-{a}. G a') ⊨ G a, {λv. Q a}"
  shows "prog.p2s (prog.Parallel as Ps) ≤ {⊓a∈as. P a}, A ⊨ ∪a∈as. G a, {λv. ⊓a∈as. Q a}"
using assms by transfer (fast intro: ag.spec.Parallel)

lemma parallel:
  assumes "prog.p2s c₁ ≤ {P₁}, A ∪ G₂ ⊨ G₁, {Q₁}"
  assumes "prog.p2s c₂ ≤ {P₂}, A ∪ G₁ ⊨ G₂, {Q₂}"
  shows "prog.p2s (prog.parallel c₁ c₂) ≤ {P₁ \<and> P₂}, A ⊨ G₁ ∪ G₂, {λv. Q₁ v \<and> Q₂ v}"
unfolding prog.parallel_alt_def
by (rule ag.pre[OF ag.prog.Parallel[where A="A" and G="λa. if a then G₁ else G₂" and P="⟨P₁ \<and> P₂⟩" and Q="λa. if a then Q₁ () else Q₂ ()"]])
   (use assms in ‹auto intro: ag.pre_imp›)

lemma return:
  assumes sQ: "stable A (Q v)"
  shows "prog.p2s (prog.return v) ≤ {Q v}, A ⊨ G, {Q}"
using assms by (auto simp: prog.return_def intro: ag.prog.action)

lemma "if":
  assumes "b ==> prog.p2s c₁ ≤ {P₁}, A ⊨ G, {Q}"
  assumes "¬b ==> prog.p2s c₂ ≤ {P₂}, A ⊨ G, {Q}"
  shows "prog.p2s (if b then c₁ else c₂) ≤ {if b then P₁ else P₂}, A ⊨ G, {Q}"
using assms by (fastforce intro: ag.pre_ag)

lemma case_option:
  assumes "x = None ==> prog.p2s none ≤ {P_n}, A ⊨ G, {Q}"
  assumes "∧v. x = Some v ==> prog.p2s (some v) ≤ {P_s v}, A ⊨ G, {Q}"
  shows "prog.p2s (case_option none some x) ≤ {case x of None ==> P_n | Some v ==> P_s v}, A ⊨ G, {Q}"
using assms by (fastforce intro: ag.pre_ag split: option.split)

lemma case_sum:
  assumes "∧v. x = Inl v ==> prog.p2s (left v) ≤ {P_l v}, A ⊨ G, {Q}"
  assumes "∧v. x = Inr v ==> prog.p2s (right v) ≤ {P_r v}, A ⊨ G, {Q}"
  shows "prog.p2s (case_sum left right x) ≤ {case_sum P_l P_r x}, A ⊨ G, {Q}"
using assms by (fastforce intro: ag.pre_ag split: sum.split)

lemma case_list:
  assumes "x = [] ==> prog.p2s nil ≤ {P_n}, A ⊨ G, {Q}"
  assumes "∧v vs. x = v # vs ==> prog.p2s (cons v vs) ≤ {P_c v vs}, A ⊨ G, {Q}"
  shows "prog.p2s (case_list nil cons x) ≤ {case_list P_n P_c x}, A ⊨ G, {Q}"
using assms by (fastforce intro: ag.pre_ag split: list.split)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsubsection‹ A proof of the parallel rule using Abadi and Plotkin's composition principle\label{sec:abadi_plotkin-parallel} ›

text‹

  we show that the key rule for const‹prog.Parallel› (@{thm [source] "ag.spec.Parallel"})
  be established using the @{thm [source] "spec.ag_circular"} rule (\S\ref{sec:abadi_plotkin}).

  following proof is complicated by the need to discard a lot of
  information.

 ›

notepad
begin

have imp_discharge_leL1:
  "x' ≤ x ==> x' ⊓ (x ⊓ y \<longrightarrow>_H z) = x' ⊓ (y \<longrightarrow>_H z)" for x x' y z
by (simp add: heyting.curry_conv heyting.discharge(1))

have LHS_rel:
   "{proc x} × UNIV ∪ (-{proc x}) × (A ∪ (Id ∪ ∪ (G ` (as - {x}))))
  = ((-(proc ` as)) × (A ∪ (Id ∪ ∪ (G ` (as - {x}))))
      ∪ ({proc x} × UNIV ∪ proc ` (as - {x}) × (A ∪ (Id ∪ ∪ (G ` (as - {x}))))))" for A G as x
by blast

have rel_agents_split:
  "spec.rel (as × r ∪ s) = spec.rel (as × r ∪ fst ` s × UNIV) ⊓ spec.rel (as × UNIV ∪ s)"
  if "fst ` s ∩ as = {}" for as r s
using that by (fastforce simp: image_iff simp flip: spec.rel.inf intro: arg_cong[where f="spec.rel"])

―‹ @{thm [source] ag.spec.Parallel} ›
fix as :: "'a set"
fix A :: "'s rel"
fix G :: "'a ==> 's rel"
fix P :: "'a ==> 's pred"
fix Q :: "'a ==> 's pred"
fix Ps :: "'a ==> (sequential, 's, unit) spec"
assume proc_ag: "∧a. a ∈ as ==> Ps a ≤ {P a}, A ∪ (∪a'∈as-{a}. G a') ⊨ G a, {λv. Q a}"
have "spec.Parallel as Ps ≤ {⊓a∈as. P a}, A ⊨ ∪a∈as. G a, {λv. ⊓a∈as. Q a}" (is "?lhs ≤ ?rhs")
proof(cases "as = {}")
  case True then show ?thesis
    by (simp add: spec.Parallel.no_agents ag.interference_le)
next
  case False then show ?thesis
apply -
supply inf.bounded_iff[simp del] ―‹ preserve RHS ›

―‹ replace ‹Ps› with a/g specs. guard against empty ‹A›, ‹G› ›
apply (strengthen ord_to_strengthen(1)[OF proc_ag], assumption)
apply (subst ag.reflcl_ag)
apply (strengthen ord_to_strengthen(2)[OF reflcl_cl.sup_cl_le])

―‹ Circular concurrent reasoning ›
unfolding ag_def

―‹ Move a/g hypotheses to LHS, normalize ›
apply (simp add: heyting ac_simps)

―‹ Discharge ‹spec.pre P› ›
apply (subst inf_assoc[symmetric])
apply (subst inf_commute)
apply (subst inf_assoc)
apply (subst (2) inf_commute)
apply (subst spec.Parallel.inf_pre, assumption)
apply (simp add: ac_simps)
―‹ Idiom for rewriting under a quantifier, here const‹spec.Parallel› ›
apply (rule order.trans)
 apply (rule inf.mono[OF order.refl])
 apply (rule spec.Parallel.mono)
 apply (subst imp_discharge_leL1)
  apply (simp add: Inf_lower spec.pre.INF; fail)
 ―‹ Discard const‹spec.pre› hypothesis ›
 apply (rule inf_le2)

―‹ Move environment assumption ‹A› hypothesis under const‹spec.toSequential› and the const‹Inf› ›
unfolding spec.Parallel_def
apply (subst inf.commute)
apply (subst spec.map.inf_distr)
apply (subst spec.invmap.rel)
apply (simp add: ac_simps flip: INF_inf_const1)

―‹ Eradicate const‹spec.toSequential›: move to parallel space ›
apply (simp add: spec.map_invmap.galois spec.invmap.inf spec.invmap.post spec.invmap.rel
           flip: spec.term.all.invmap spec.term.all.map)

―‹ Eradicate const‹spec.toConcurrent› ›
apply (simp add: ac_simps spec.invmap.heyting spec.invmap.inf spec.invmap.rel
                 spec.invmap.pre spec.invmap.post)

―‹ Normalize the relations ›
apply (simp add: inf_sup_distrib1 Times_Int_Times map_prod_vimage_Times ac_simps spec.rel.reflcl
           flip: spec.rel.inf image_Int inf.assoc)

―‹ Discharge environment assumption ‹A› and that for agents in ‹-as› ›
apply (subst LHS_rel)
―‹ Idiom for rewriting under a quantifier, here const‹Inf› ›
apply (rule order.trans)
 apply (rule INF_mono[where B=as])
 apply (rule rev_bexI, assumption)
 apply (subst (2) rel_agents_split, fastforce)
 apply (subst imp_discharge_leL1)
  apply (rule spec.rel.mono, fastforce simp: image_Un)
 apply (rule order.refl)
apply (simp flip: sup.assoc Times_Un_distrib1)
apply (simp add: ac_simps INF_inf_const1)

―‹ Apply Abadi/Plotkin ›

―‹ Change coordinates ›
apply (subst INF_rename_bij[where X="proc ` as" and π="the_inv proc"])
 apply (fastforce simp: bij_betw_iff_bijections)
apply (simp add: image_comp cong: INF_cong)

―‹ The circular reasoning principle only applies to the relational part as const‹spec.post› is not termination closed.
 Therefore split the goal ›
apply (subst heyting.infR)
apply (subst INF_inf_distrib[symmetric])
apply (rule order.trans)
 apply (rule inf_mono[OF order.refl])+
 apply (rule order.trans[rotated])
  apply (rule spec.ag_circular[where
             as="proc ` as"
         and Ps="λa. spec.rel ({a} × (Id ∪ G (the_inv proc a)) ∪ insert env (proc ` (- {the_inv proc a})) × UNIV)",
          simplified spec.idle_le spec.term.closed.rel, simplified,
          OF subsetD[OF spec.cam.closed.antimono spec.cam.closed.rel[OF order.refl]]])
  apply (clarsimp simp: image_iff)
  apply (metis ComplI agent.exhaust singletonD)
 apply (rule INFI)
 apply (simp add: heyting ac_simps flip: spec.rel.INF INF_inf_const1)
  ―‹ Idiom for rewriting under a quantifier, here const‹Inf› ›
 apply (rule order.trans)
  apply (rule INF_mono[where B=as])
  apply (rule rev_bexI, assumption)
  apply (subst heyting.discharge)
   apply (rule spec.rel.mono_reflcl)
   apply fastforce
  apply (simp flip: spec.rel.inf)
  apply (rule order.refl)
 apply (simp flip: spec.rel.INF)
 apply (rule spec.rel.mono)
 apply (clarsimp simp: image_iff)
 apply (metis ComplI agent.exhaust singletonD)
apply (simp add: ac_simps flip: spec.rel.INF)
apply (subst inf.assoc[symmetric])
apply (simp flip: spec.rel.inf)

―‹ Conclude guarantee ‹G› ›
apply (rule le_infI[rotated])
 apply (rule le_infI1)
 apply (rule spec.rel.mono_reflcl, blast)

―‹ Conclude ‹spec.post Q› ›
apply (subst (2) INF_inf_const1[symmetric], force)
―‹ Idiom for rewriting under a quantifier, here const‹Inf› ›
apply (rule order.trans)
 apply (rule INF_mono[where B=as])
 apply (rule rev_bexI, blast)
 apply (subst heyting.discharge)
  apply (force intro: spec.rel.mono)
 apply (rule order.refl)
apply (simp add: spec.post.Ball flip: INF_inf_distrib)
done
qed

end


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

setup ‹Sign.mandatory_path "inhabits.prog"›

lemma Sup:
  assumes "prog.p2s P -s, xs→ P'"
  assumes "P ∈ X"
  shows "prog.p2s (⊔X) -s, xs→ P'"
by (auto simp: prog.p2s.Sup intro: inhabits.Sup inhabits.supL assms)

lemma supL:
  assumes "prog.p2s P -s, xs→ P'"
  shows "prog.p2s (P ⊔ Q) -s, xs→ P'"
by (simp add: prog.p2s.simps assms inhabits.supL)

lemma supR:
  assumes "prog.p2s Q -s, xs→ Q'"
  shows "prog.p2s (P ⊔ Q) -s, xs→ Q'"
by (simp add: prog.p2s.simps assms inhabits.supR)

lemma bind:
  assumes "prog.p2s f -s, xs→ prog.p2s f'"
  shows "prog.p2s (f 🍋 g) -s, xs→ prog.p2s (f' 🍋 g)"
by (simp add: prog.p2s.simps inhabits.spec.bind assms)

lemma return:
  shows "prog.p2s (prog.return v) -s, []→ spec.return v"
by (metis prog.p2s.return inhabits.pre inhabits.tau[OF spec.idle.interference.cl_le]
          spec.interference.expansive)

lemma action_step:
  fixes F :: "('v × 's × 's) set"
  assumes "(v, s, s') ∈ F"
  shows "prog.p2s (prog.action F) -s, [(self, s')]→ prog.p2s (prog.return v)"
apply (simp only: prog.p2s.action prog.p2s.return spec.interference.cl.action spec.interference.cl.return)
apply (rule inhabits.pre[OF _ order.refl])
 apply (rule inhabits.spec.bind'[OF inhabits.spec.rel.term])
 apply (simp add: spec.bind.returnL spec.idle_le)
 apply (rule inhabits.spec.bind'[OF inhabits.spec.action.step])
  using assms apply force
 apply (simp add: spec.bind.returnL spec.idle_le)
 apply (rule inhabits.tau)
 apply (simp add: spec.idle_le)
apply simp
done

lemma action_stutter:
  fixes F :: "('v × 's × 's) set"
  assumes "(v, s, s) ∈ F"
  shows "prog.p2s (prog.action F) -s, []→ prog.p2s (prog.return v)"
apply (simp only: prog.p2s.action prog.p2s.return spec.interference.cl.action spec.interference.cl.return)
apply (rule inhabits.pre[OF _ order.refl])
 apply (rule inhabits.spec.bind'[OF inhabits.spec.rel.term])
 apply (simp add: spec.bind.returnL spec.idle_le)
 apply (rule inhabits.spec.bind'[OF inhabits.spec.action.stutter])
  using assms apply force
 apply (simp add: spec.bind.returnL spec.idle_le)
 apply (rule inhabits.tau)
 apply (simp add: spec.idle_le)
apply simp
done

lemma parallelL:
  assumes "prog.p2s P -s, xs→ prog.p2s P'"
  shows "prog.p2s (P ∥ Q) -s, xs→ prog.p2s (P' ∥ Q)"
by (simp add: prog.p2s.simps inhabits.spec.parallelL assms prog.p2s.interference_wind_bind)

lemma parallelR:
  assumes "prog.p2s Q -s, xs→ prog.p2s Q'"
  shows "prog.p2s (P ∥ Q) -s, xs→ prog.p2s (P ∥ Q')"
by (simp add: prog.p2s.simps inhabits.spec.parallelR assms prog.p2s.interference_wind_bind)

setup ‹Sign.parent_path›
(*<*)

end
(*>*)