Theory Programs
theory Programs
imports
Refinement
begin
section‹ A programming language\label{sec:programs} ›
text‹
The \<^typ>‹('a, 's, 'v) spec› lattice of
\S\ref{sec:safety_logic-logic} is adequate for logic but is deficient
as a programming language. In particular we wish to interpret the
parallel composition as intersection
(\S\ref{sec:constructions-parallel_composition}) which requires
processes to contain enough interference opportunities. Similarly we
want the customary ``laws of programming''
\<^citep>‹"HoareEtAl:1987"› to hold without side
conditions.
These points are discussed at some length by
\<^citet>‹‹\S3.2› in "Zwiers:1989"› and also
\<^citet>‹‹Lemma~6.7› in "Foster:2020"›.
Our ‹('v, 's) prog› lattice (\S\ref{sec:programs-prog})
therefore handles the common case of the familiar constructs for
sequential programming, and we lean on our \<^typ>‹('a, 's, 'v)
spec› lattice for other constructions such as interleaving
parallel composition (\S\ref{sec:constructions-parallel_composition})
and local state (\S\ref{sec:local_state}). It allows arbitrary
interference by the environment before and after every program action.
›
subsection‹ The ∗‹('s, 'v) prog› lattice \label{sec:programs-prog} ›
text‹
According to \<^citet>‹‹\S2.1› in "MuellerOlm:1997"›, ‹('s, 'v) prog› is
a ∗‹sub-lattice› of \<^typ>‹('a, 's, 'v) spec› as the corresponding \<^const>‹inf› and \<^const>‹sup›
operations coincide. However it is not a ∗‹complete› sub-lattice as \<^const>‹Sup› in ‹('s, 'v) prog›
needs 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‹
We can readily convert a \<^typ>‹('s, 'v) prog› into a
\<^typ>‹('a agent, 's, 'v) spec›. More interestingly, on
\<^typ>‹('s, 'v) prog› we have a Galois connection that
embeds specifications into programs. (This connection is termed a
∗‹Galois insertion› by
\<^citet>‹"MeltonSchmidtStrecker:1985"› as we also have
‹prog.s2p.p2s›; Cousot says ``Galois retraction''.)
See 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:
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
"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:
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‹
We lift the combinators directly from the \<^typ>‹('a,
's ,'v) spec› lattice (\S\ref{sec:safety_logic}), but need to
interference-close primitive actions. Control flow is expressed via
HOL's ‹if-then-else› construct and other case combinators
where the scrutinee is a pure value. This means that the atomicity of a process is completely
determined 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:
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 \<^typ>‹('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⇩1 :: "(_, _) prog"
shows supL: "(f⇩1 ⊔ f⇩2) ⤜ g = (f⇩1 ⤜ g) ⊔ (f⇩2 ⤜ g)"
and supR: "f ⤜ (λx. g⇩1 x ⊔ g⇩2 x) = (f ⤜ g⇩1) ⊔ (f ⤜ g⇩2)"
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:
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"
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"
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"
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:
shows "prog.rel r ⪢ prog.rel r = prog.rel r"
by transfer (simp add: spec.rel.wind_bind)
lemma wind_bind_leading:
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:
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‹
We specialize the rules of \S\ref{sec:refinement-spec} to the
\<^typ>‹('s, 'v) prog› lattice. Observe that, as
preconditions, postconditions and assumes are not interference closed,
we apply the \<^const>‹prog.p2s› morphism and work in the more
capacious \<^typ>‹(sequential, 's, 'v) spec›
lattice. This syntactic noise could be elided with another definition.
›
subsubsection‹ Introduction rules\label{sec:programs-refinement-intros} ›
text‹
Refinement 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‹
Refinement quadruples ‹⦃P⦄, A ⊩ G, ⦃Q⦄› denote points in the \<^typ>‹('s, 'v) prog› lattice
provided ‹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⇩1 ⊔ c⇩2) ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄
⟷ prog.p2s c⇩1 ≤ ⦃P⦄, A ⊩ G, ⦃Q⦄ ∧ prog.p2s c⇩2 ≤ ⦃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⇩1 ≤ ⦃P⇩1⦄, refinement.spec.env_hyp (λa. if a then P⇩1 else P⇩2) A UNIV (λa. if a then prog.p2s c⇩1' else prog.p2s c⇩2') True ⊩ prog.p2s c⇩1', ⦃Q⇩1⦄"
assumes "prog.p2s c⇩2 ≤ ⦃P⇩2⦄, refinement.spec.env_hyp (λa. if a then P⇩1 else P⇩2) A UNIV (λa. if a then prog.p2s c⇩1' else prog.p2s c⇩2') False ⊩ prog.p2s c⇩2', ⦃Q⇩2⦄"
shows "prog.p2s (prog.parallel c⇩1 c⇩2) ≤ ⦃P⇩1 ❙∧ P⇩2⦄, A ⊩ prog.p2s (prog.parallel c⇩1' c⇩2'), ⦃λv. Q⇩1 v ❙∧ Q⇩2 v⦄"
unfolding prog.parallel_alt_def
by (rule refinement.pre[OF refinement.prog.Parallel[where A="A" and P="λa. if a then P⇩1 else P⇩2" and Ps'="λa. if a then c⇩1' else c⇩2'" and Q="λa. if a then Q⇩1 () else Q⇩2 ()"]])
(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‹
Similarly we specialize the assume/guarantee program logic of
\S\ref{sec:refinement-ag} to \<^typ>‹('s, 'v) prog›.
References:
▪ \<^citet>‹"XudeRoeverHe:1997" and "deRoeverEtAl:2001"›
▪ \<^citet>‹‹\S7› in "PrensaNieto:2003"›
▪ \<^citet>‹‹\S3› in "Vafeiadis:2008"›
›
subsubsection‹ Galois considerations\label{sec:programs-ag-galois} ›
text‹
For suitably stable ‹P›, ‹Q›, ‹⦃P⦄, A ⊢ G, ⦃Q⦄› is interference closed and hence denotes a
point in \<^typ>‹('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⇩1 ⊔ c⇩2) ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄ ⟷ prog.p2s c⇩1 ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄ ∧ prog.p2s c⇩2 ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
by (simp add: prog.p2s.simps)
lemmas sup = iffD2[OF ag.prog.sup_conv, unfolded conj_explode]
lemma bind:
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:
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
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⇩1 ≤ ⦃P⇩1⦄, A ∪ G⇩2 ⊢ G⇩1, ⦃Q⇩1⦄"
assumes "prog.p2s c⇩2 ≤ ⦃P⇩2⦄, A ∪ G⇩1 ⊢ G⇩2, ⦃Q⇩2⦄"
shows "prog.p2s (prog.parallel c⇩1 c⇩2) ≤ ⦃P⇩1 ❙∧ P⇩2⦄, A ⊢ G⇩1 ∪ G⇩2, ⦃λv. Q⇩1 v ❙∧ Q⇩2 v⦄"
unfolding prog.parallel_alt_def
by (rule ag.pre[OF ag.prog.Parallel[where A="A" and G="λa. if a then G⇩1 else G⇩2" and P="⟨P⇩1 ❙∧ P⇩2⟩" and Q="λa. if a then Q⇩1 () else Q⇩2 ()"]])
(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⇩1 ≤ ⦃P⇩1⦄, A ⊢ G, ⦃Q⦄"
assumes "¬b ⟹ prog.p2s c⇩2 ≤ ⦃P⇩2⦄, A ⊢ G, ⦃Q⦄"
shows "prog.p2s (if b then c⇩1 else c⇩2) ≤ ⦃if b then P⇩1 else P⇩2⦄, 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‹
Here we show that the key rule for \<^const>‹prog.Parallel› (@{thm [source] "ag.spec.Parallel"})
can be established using the @{thm [source] "spec.ag_circular"} rule (\S\ref{sec:abadi_plotkin}).
The following proof is complicated by the need to discard a lot of
contextual information.
›
notepad
begin
have imp_discharge_leL1:
"x' ≤ x ⟹ x' ⊓ (x ⊓ y ❙⟶⇩H z) = x' ⊓ (y ❙⟶⇩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"])
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]
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])
unfolding ag_def
apply (simp add: heyting ac_simps)
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)
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)
apply (rule inf_le2)
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)
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)
apply (simp add: ac_simps spec.invmap.heyting spec.invmap.inf spec.invmap.rel
spec.invmap.pre spec.invmap.post)
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)
apply (subst LHS_rel)
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 (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)
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)
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)
apply (rule le_infI[rotated])
apply (rule le_infI1)
apply (rule spec.rel.mono_reflcl, blast)
apply (subst (2) INF_inf_const1[symmetric], force)
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