Theory Safety_Logic
theory Safety_Logic
imports
Aczel_Sequences
Galois
Heyting
Lifted_Predicates
begin
section‹ Safety logic\label{sec:safety_logic} ›
text‹
Following \<^citet>‹"AbadiPlotkin:1991" and "AbadiPlotkin:1993" and "AbadiLamport:1995"›
(see also \<^citet>‹‹\S5.5› in "AbadiMerz:1996"›), we work in the complete lattice of
stuttering-closed safety properties (i.e., stuttering-closed downsets)
and use this for logical purposes. We avoid many syntactic issues
via a shallow embedding into HOL.
›
subsection‹ Stuttering\label{sec:safety_logic-stuttering} ›
text‹
We define ∗‹stuttering equivalence› ala \<^citet>‹"Lamport:1994"›. This allows any
agent to repeat any state at any time. We define a normalisation function ‹(♮)› on
\<^typ>‹('a, 's, 'v) trace.t› and extract the (matroidal) closure over sets of
these from the Galois connection \<^locale>‹galois.image_vimage›.
›
setup ‹Sign.mandatory_path "trace"›
primrec natural' :: "'s ⇒ ('a × 's) list ⇒ ('a × 's) list" where
"natural' s [] = []"
| "natural' s (x # xs) = (if snd x = s then natural' s xs else x # natural' (snd x) xs)"
setup ‹Sign.mandatory_path "final'"›
lemma natural'[simp]:
shows "trace.final' s (trace.natural' s xs) = trace.final' s xs"
by (induct xs arbitrary: s) simp_all
lemma natural'_cong:
assumes "s = s'"
assumes "trace.natural' s xs = trace.natural' s xs'"
shows "trace.final' s xs = trace.final' s' xs'"
by (metis assms trace.final'.natural')
setup ‹Sign.parent_path›
setup ‹Sign.mandatory_path "natural'"›
lemma natural':
shows "trace.natural' s (trace.natural' s xs) = trace.natural' s xs"
by (induct xs arbitrary: s) simp_all
lemma length:
shows "length (trace.natural' s xs) ≤ length xs"
by (induct xs arbitrary: s) (simp_all add: le_SucI)
lemma subseq:
shows "subseq (trace.natural' s xs) xs"
by (induct xs arbitrary: s) auto
lemma remdups_adj:
shows "s # map snd (trace.natural' s xs) = remdups_adj (s # map snd xs)"
by (induct xs arbitrary: s) simp_all
lemma append:
shows "trace.natural' s (xs @ ys) = trace.natural' s xs @ trace.natural' (trace.final' s xs) ys"
by (induct xs arbitrary: s) simp_all
lemma eq_Nil_conv:
shows "trace.natural' s xs = [] ⟷ snd ` set xs ⊆ {s}"
and "[] = trace.natural' s xs ⟷ snd ` set xs ⊆ {s}"
by (induct xs arbitrary: s) simp_all
lemma eq_Cons_conv:
shows "trace.natural' s xs = y # ys
⟷ (∃xs' ys'. xs = xs' @ y # ys' ∧ snd ` set xs' ⊆ {s} ∧ snd y ≠ s ∧ trace.natural' (snd y) ys' = ys)" (is "?lhs ⟷ ?rhs")
and "y # ys = trace.natural' s xs
⟷ (∃xs' ys'. xs = xs' @ y # ys' ∧ snd ` set xs' ⊆ {s} ∧ snd y ≠ s ∧ trace.natural' (snd y) ys' = ys)" (is ?thesis1)
proof -
show "?lhs ⟷ ?rhs"
proof(rule iffI)
show "?lhs ⟹ ?rhs"
proof(induct xs)
case (Cons x xs) show ?case
proof(cases "s = snd x")
case True with Cons
obtain xs' ys'
where "xs = xs' @ y # ys'" and "snd ` set xs' ⊆ {s}" and "snd y ≠ s"
and "trace.natural' (snd y) ys' = ys"
by auto
with True show ?thesis by (simp add: exI[where x="x # xs'"])
qed (use Cons.prems in force)
qed simp
show "?rhs ⟹ ?lhs"
by (auto simp: trace.natural'.append trace.natural'.eq_Nil_conv)
qed
then show ?thesis1
by (rule eq_commute_conv)
qed
lemma eq_append_conv:
shows "trace.natural' s xs = ys @ zs
⟷ (∃ys' zs'. xs = ys' @ zs' ∧ trace.natural' s ys' = ys ∧ trace.natural' (trace.final' s ys) zs' = zs)" (is "?lhs = ?rhs")
and "ys @ zs = trace.natural' s xs
⟷ (∃ys' zs'. xs = ys' @ zs' ∧ trace.natural' s ys' = ys ∧ trace.natural' (trace.final' s ys) zs' = zs)" (is ?thesis1)
proof -
show "?lhs ⟷ ?rhs"
proof(rule iffI)
show "?lhs ⟹ ?rhs"
proof(induct ys arbitrary: s xs)
case (Cons y ys s xs)
from Cons.prems
obtain ys' zs'
where "xs = ys' @ y # zs'" and "snd ` set ys' ⊆ {s}"
and "snd y ≠ s" and "trace.natural' (snd y) zs' = ys @ zs"
by (clarsimp simp: trace.natural'.eq_Cons_conv)
with Cons.hyps[where s="snd y" and xs="zs'"] show ?case
by (clarsimp simp: trace.natural'.eq_Cons_conv) (metis append.assoc append_Cons)
qed fastforce
show "?rhs ⟹ ?lhs"
by (auto simp: trace.natural'.append)
qed
then show ?thesis1
by (rule eq_commute_conv)
qed
lemma replicate:
shows "trace.natural' s (replicate i as) = (if snd as = s ∨ i = 0 then [] else [as])"
by (auto simp: gr0_conv_Suc trace.natural'.eq_Nil_conv)
lemma map_natural':
shows "trace.natural' (sf s) (map (map_prod af sf) (trace.natural' s xs))
= trace.natural' (sf s) (map (map_prod af sf) xs)"
by (induct xs arbitrary: s; simp; metis)
lemma map_inj_on_sf:
assumes "inj_on sf (insert s (snd ` set xs))"
shows "trace.natural' (sf s) (map (map_prod af sf) xs) = map (map_prod af sf) (trace.natural' s xs)"
using assms
proof(induct xs arbitrary: s)
case (Cons x xs s)
from Cons.prems have "sf (snd x) ≠ sf s" if "snd x ≠ s"
by (meson image_eqI inj_onD insert_iff list.set_intros(1) that)
with Cons.prems show ?case
by (auto intro: Cons.hyps)
qed simp
lemma amap_noop:
assumes "trace.natural' s xs = map (map_prod af id) zs"
shows "trace.natural' s zs = zs"
using assms by (induct xs arbitrary: s zs) (auto split: if_split_asm)
lemma take:
shows "∃j≤length xs. take i (trace.natural' s xs) = trace.natural' s (take j xs)"
proof(induct xs arbitrary: s i)
case (Cons x xs s i) then show ?case by (cases i; fastforce)
qed simp
lemma idle_prefix:
assumes "snd ` set xs ⊆ {s}"
shows "trace.natural' s (xs @ ys) = trace.natural' s ys"
using assms by (simp add: trace.natural'.append trace.natural'.eq_Nil_conv)
lemma prefixE:
assumes "trace.natural' s ys = trace.natural' s (xs @ xsrest)"
obtains xs' xs'rest where "trace.natural' s xs = trace.natural' s xs'" and "ys = xs' @ xs'rest"
by (metis assms trace.natural'.eq_append_conv(2))
lemma aset_conv:
shows "a ∈ trace.aset (trace.T s (trace.natural' s xs) v)
⟷ (∃s' s''. (a, s', s'') ∈ set (trace.transitions' s xs) ∧ s' ≠ s'')"
by (induct xs arbitrary: s) (auto simp: trace.aset.simps)
setup ‹Sign.parent_path›
definition natural :: "('a, 's, 'v) trace.t ⇒ ('a, 's, 'v) trace.t" (‹♮›) where
"♮σ = trace.T (trace.init σ) (trace.natural' (trace.init σ) (trace.rest σ)) (trace.term σ)"
setup ‹Sign.mandatory_path "natural"›
lemma sel[simp]:
shows "trace.init (♮σ) = trace.init σ"
and "trace.rest (♮σ) = trace.natural' (trace.init σ) (trace.rest σ)"
and "trace.term (♮σ) = trace.term σ"
by (simp_all add: trace.natural_def)
lemma simps:
shows "♮(trace.T s [] v) = trace.T s [] v"
and "♮(trace.T s ((a, s) # xs) v) = ♮(trace.T s xs v)"
and "♮(trace.T s (trace.natural' s xs) v) = ♮(trace.T s xs v)"
by (simp_all add: trace.natural_def trace.natural'.natural')
lemma idempotent[simp]:
shows "♮(♮σ) = ♮σ"
by (simp add: trace.natural_def trace.natural'.natural')
lemma idle:
assumes "snd ` set xs ⊆ {s}"
shows "♮(trace.T s xs v) = trace.T s [] v"
by (simp add: assms trace.natural_def trace.natural'.eq_Nil_conv)
lemma trace_conv:
shows "♮(trace.T s xs v) = ♮σ ⟷ trace.init σ = s ∧ trace.natural' s xs = trace.natural' s (trace.rest σ) ∧ trace.term σ = v"
and "♮σ = ♮(trace.T s xs v) ⟷ trace.init σ = s ∧ trace.natural' s xs = trace.natural' s (trace.rest σ) ∧ trace.term σ = v"
by (cases σ; fastforce simp: trace.natural_def)+
lemma map_natural:
shows "♮(trace.map af sf vf (♮σ)) = ♮(trace.map af sf vf σ)"
by (simp add: trace.natural_def trace.natural'.map_natural')
lemma continue:
shows "♮(σ @-⇩S xsv) = ♮σ @-⇩S (trace.natural' (trace.final σ) (fst xsv), snd xsv)"
by (simp add: trace.natural_def trace.natural'.append split: option.split)
lemma replicate:
shows "♮(trace.T s (replicate i as) v)
= (trace.T s (if snd as = s ∨ i = 0 then [] else [as]) v)"
by (simp add: trace.natural_def trace.natural'.replicate)
lemma monotone:
shows "mono ♮"
using trace.natural.continue by (fastforce intro: monoI simp: trace.less_eq_t_def)
lemmas strengthen[strg] = st_monotone[OF trace.natural.monotone]
lemmas mono = monotoneD[OF trace.natural.monotone]
lemmas mono2mono[cont_intro, partial_function_mono]
= monotone2monotone[OF trace.natural.monotone, simplified, of orda P for orda P]
lemma less_eqE:
assumes "t ≤ u"
assumes "♮u' = ♮u"
obtains t' where "♮t = ♮t'" and "t' ≤ u'"
using assms
by atomize_elim
(fastforce simp: trace.natural_def trace.split_Ex trace.less_eq_None(2)[unfolded prefix_def]
elim!: trace.less_eqE prefixE trace.natural'.prefixE)
lemma less_eq_natural:
assumes "σ⇩1 ≤ ♮σ⇩2"
shows "♮σ⇩1 = σ⇩1"
using assms
by (cases σ⇩1)
(auto simp: trace.natural_def prefix_def trace.natural'.eq_append_conv trace.natural'.natural'
elim!: trace.less_eqE)
lemma map_le:
assumes "♮σ⇩1 ≤ ♮σ⇩2"
shows "♮(trace.map af sf vf σ⇩1) ≤ ♮(trace.map af sf vf σ⇩2)"
using trace.natural.mono[OF trace.map.mono[OF assms], simplified trace.natural.map_natural] .
lemma map_inj_on_sf:
assumes "inj_on sf (trace.sset σ)"
shows "♮(trace.map af sf vf σ) = trace.map af sf vf (♮σ)"
using assms by (cases σ) (simp add: trace.natural_def trace.natural'.map_inj_on_sf trace.sset.simps)
lemma take:
shows "∃j. ♮(trace.take i σ) = trace.take j (♮σ)"
by (meson trace.natural.mono trace.less_eq_take_def)
lemma take_natural:
shows "♮(trace.take i (♮σ)) = trace.take i (♮σ)"
using trace.natural.less_eq_natural by blast
lemma takeE:
shows "⟦σ⇩1 = ♮(trace.take i σ⇩2); ⋀j. ⟦σ⇩1 = trace.take j (♮σ⇩2)⟧ ⟹ thesis⟧ ⟹ thesis"
and "⟦♮(trace.take i σ⇩2) = σ⇩1; ⋀j. ⟦σ⇩1 = trace.take j (♮σ⇩2)⟧ ⟹ thesis⟧ ⟹ thesis"
using trace.natural.take by blast+
setup ‹Sign.parent_path›
setup ‹Sign.mandatory_path "aset"›
lemma natural_conv:
shows "a ∈ trace.aset (♮σ) ⟷ (∃s s'. (a, s, s') ∈ trace.steps σ)"
by (simp add: trace.natural_def trace.steps'_def trace.natural'.aset_conv)
setup ‹Sign.parent_path›
setup ‹Sign.mandatory_path "sset"›
lemma natural'[simp]:
shows "trace.sset (trace.T s⇩0 (trace.natural' s⇩0 xs) v) = trace.sset (trace.T s⇩0 xs v)"
by (induct xs arbitrary: s⇩0) (simp_all add: trace.sset.simps)
lemma natural[simp]:
shows "trace.sset (♮σ) = trace.sset σ"
by (simp add: trace.natural_def)
setup ‹Sign.parent_path›
setup ‹Sign.mandatory_path "vset"›
lemma natural[simp]:
shows "trace.vset (♮σ) = trace.vset σ"
by (cases σ) (simp add: trace.natural_def trace.t.simps(8))
setup ‹Sign.parent_path›
setup ‹Sign.mandatory_path "take"›
lemma natural:
shows "∃j≤Suc (length (trace.rest σ)). trace.take i (♮σ) = ♮(trace.take j σ)"
using trace.natural'.take[where i=i and s= "trace.init σ" and xs="trace.rest σ"]
by (auto simp: trace.natural_def trace.take_def not_le) (use Suc_n_not_le_n in blast)
lemma naturalE:
shows "⟦σ⇩1 = trace.take i (♮σ⇩2); ⋀j. ⟦j ≤ Suc (length (trace.rest σ⇩2)); σ⇩1 = ♮(trace.take j σ⇩2)⟧ ⟹ thesis⟧ ⟹ thesis"
and "⟦trace.take i (♮σ⇩2) = σ⇩1; ⋀j. ⟦j ≤ Suc (length (trace.rest σ⇩2)); ♮(trace.take j σ⇩2) = σ⇩1⟧ ⟹ thesis⟧ ⟹ thesis"
using trace.take.natural[of σ⇩2 i] by force+
setup ‹Sign.parent_path›
lemma steps'_alt_def:
shows "trace.steps' s xs = set (trace.transitions' s (trace.natural' s xs))"
by (induct xs arbitrary: s) auto
setup ‹Sign.mandatory_path "steps'"›
lemma natural':
shows "trace.steps' s (trace.natural' s xs) = trace.steps' s xs"
unfolding trace.steps'_def by (induct xs arbitrary: s) auto
lemma asetD:
assumes "trace.steps σ ⊆ r"
shows "∀a. a ∈ trace.aset (♮σ) ⟶ a ∈ fst ` r"
using assms by (force simp: trace.aset.natural_conv)
lemma range_initE:
assumes "trace.steps' s⇩0 xs ⊆ range af × range sf × range sf"
assumes "(a, s, s') ∈ trace.steps' s⇩0 xs"
obtains s⇩0' where "s⇩0 = sf s⇩0'"
using assms by (induct xs arbitrary: s s⇩0) (auto simp: trace.steps'_alt_def split: if_split_asm)
lemma map_range_conv:
shows "trace.steps' (sf s) xs ⊆ range af × range sf × range sf
⟷ (∃xs'. trace.natural' (sf s) xs = map (map_prod af sf) xs')" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
show "?lhs ⟹ ?rhs"
by (induct xs arbitrary: s) (auto 0 3 simp: Cons_eq_map_conv)
show "?rhs ⟹ ?lhs"
by (force simp: trace.steps'_alt_def trace.transitions'.map map_prod_conv)
qed
lemma step_conv:
shows "trace.steps' s xs = {x}
⟷ fst (snd x) = s ∧ fst (snd x) ≠ snd (snd x)
∧ (∃ys zs. snd ` set ys ⊆ {s} ∧ snd ` set zs ⊆ {snd (snd x)}
∧ xs = ys @ [(fst x, snd (snd x))] @ zs)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
show "?lhs ⟹ ?rhs"
by (fastforce dest!: arg_cong[where f="set"]
simp: trace.steps'_alt_def set_singleton_conv set_replicate_conv_if
trace.transitions'.eq_Nil_conv trace.transitions'.eq_Cons_conv
trace.natural'.eq_Nil_conv trace.natural'.eq_Cons_conv
split: if_split_asm)
show "?rhs ⟹ ?lhs"
by (clarsimp simp: trace.steps'.append)
qed
setup ‹Sign.parent_path›