Theory Safety_Closure
theory Safety_Closure
imports
ConcurrentHOL.TLS
begin
section‹ Observations about safety closure\label{sec:safety_closure} ›
text‹
We demonstrate that ‹Sup› does not distribute in \<^typ>‹('a, 's, 'v) tls› as it does in
\<^typ>‹('a, 's, 'v) spec›: specifically a ‹Sup› of a set of safety properties in the former need not
be a safety property, whereas in the latter it is (see \S\ref{sec:safety_logic-logic}).
›
corec bnats :: "nat ⇒ ('a × nat, 'v) tllist" where
"bnats i = TCons (undefined, i) (bnats (Suc i))"
definition bnat :: "('a, nat, 'v) behavior.t" where
"bnat = behavior.B 0 (bnats 1)"
definition tnats :: "nat ⇒ nat ⇒ ('a × nat) list" where
"tnats i j = map (Pair undefined) (upt i j)"
definition tnat :: "nat ⇒ ('a, nat, 'v) trace.t" where
"tnat i = trace.T 0 (tnats (Suc 0) (Suc i)) None"
lemma tnat_simps[simp]:
shows "tnats i i = []"
and "trace.init (tnat i) = 0"
and "trace.rest (tnat i) = tnats 1 (Suc i)"
and "length (tnats i j) = j - i"
by (simp_all add: tnats_def tnat_def)
lemma take_tnats:
shows "take i (tnats j k) = tnats j (min (i + j) k)"
by (simp add: tnats_def take_map add.commute split: split_min)
lemma take_tnat:
shows "trace.take i (tnat j) = tnat (min i j)"
by (simp add: trace.take_def take_tnats tnat_def)
lemma mono_tnat:
shows "mono tnat"
by (rule monoI) (auto simp: trace.less_eq_take_def take_tnat split: split_min)
lemma final'_tnats:
shows "trace.final' i (tnats j k) = (if j < k then k - 1 else i)"
by (simp add: tnats_def trace.final'_def comp_def)
lemma sset_tnat:
shows "trace.sset (tnat i) = {j. j ≤ i}"
by (force simp: tnat_def tnats_def trace.sset.simps)
lemma natural'_tnats:
shows "trace.natural' i (tnats (Suc i) (Suc j)) = tnats (Suc i) (Suc j)"
proof -
have "trace.natural' i (map (Pair undefined) (upt (Suc i) (Suc j)))
= map (Pair undefined) (upt (Suc i) (Suc j))" for j
by (induct j arbitrary: i) (simp_all add: trace.natural'.append)
from this show ?thesis unfolding tnats_def .
qed
lemma natural_tnat:
shows "♮(tnat i) = tnat i"
by (simp add: tnat_def trace.natural_def natural'_tnats del: upt_Suc)
lemma ttake_bnats:
shows "ttake i (bnats j) = (tnats j (i + j), None)"
by (induct i arbitrary: j) (subst bnats.code; simp add: tnats_def upt_rec)+
lemma take_bnat_tnat:
shows "behavior.take i bnat = tnat i"
by (simp add: bnat_def tnat_def behavior.take_def ttake_bnats)
unbundle tls.extra_notation
definition bnat_approx :: "(unit, nat, unit) spec set" where
"bnat_approx = {⦉behavior.take i bnat⦊ |i. True}"
lemma bnat_approx_alt_def:
shows "bnat_approx = {⦉tnat i⦊ |i. True}"
by (simp add: bnat_approx_def take_bnat_tnat)
lemma not_tls_from_spec_Sup_distrib:
shows "¬tls.from_spec (⨆bnat_approx) ≤ ⨆(tls.from_spec ` bnat_approx)" (is "¬?lhs ≤ ?rhs")
proof -
have "⦉bnat⦊⇩T ≤ ?lhs"
proof -
have *: "∃j. behavior.take i ω ∈ raw.spec.cl {behavior.take j bnat}" if "bnat ≃⇩T ω"
for i and ω :: "('a, nat, 'b) behavior.t"
by (rule behavior.stuttering.equiv.takeE[OF sym[OF that], where i=i])
(force simp: raw.spec.cl_def simp flip: trace.stuttering.cl.downwards.cl)
note spec.singleton.transfer[transfer_rule]
show ?thesis
unfolding bnat_approx_def
by transfer
(force dest: * simp: TLS.raw.singleton_def raw.from_spec_def Safety_Logic.raw.singleton_def
simp flip: ex_simps elim!: behavior.stuttering.clE)
qed
moreover
have "¬(∀j. tnat j ≤ tnat i)" for i
by (auto intro!: exI[where x="Suc i"] dest!: monoD[OF trace.sset.mono] simp: sset_tnat)
then have "¬⦉bnat⦊⇩T ≤ ?rhs"
by (fastforce simp: bnat_approx_def tls.singleton.le_conv spec.singleton_le_conv take_bnat_tnat natural_tnat)
ultimately show ?thesis
by (blast dest: order.trans)
qed
definition bnat' :: "(unit, nat, unit) tls set" where
"bnat' = tls.from_spec ` bnat_approx"
lemma not_tls_safety_cl_Sup_distrib:
shows "¬tls.safety.cl (⨆bnat') ≤ ⨆(tls.safety.cl ` bnat')"
proof -
have "(⨆x∈bnat_approx. tls.to_spec (tls.from_spec x)) = ⨆bnat_approx" (is "?lhs = ?rhs")
proof(rule antisym)
show "?lhs ≤ ?rhs"
by (simp add: Sup_upper2 tls.safety.lower_upper_contractive)
have "∃ω ia ib. (∀i. ♮ (behavior.take i ω) ≤ tnat ib) ∧ tnat i = behavior.take ia ω"
for i
by (rule exI[where x="behavior.B 0 (tshift2 (tnats (Suc 0) (Suc i), None) (trepeat (undefined, i)))"])
(force simp: behavior.take.tshift ttake_trepeat trace.take.continue take_tnat
trace.natural.continue trace.natural'.replicate natural_tnat not_le final'_tnats
simp flip: tnat_def
split: split_min
intro: monoD[OF mono_tnat])
then show "?rhs ≤ ?lhs"
by (clarsimp simp: bnat_approx_alt_def spec.singleton.le_conv tls.singleton.le_conv
spec.singleton_le_conv natural_tnat
simp flip: ex_simps;
fast)
qed
then show ?thesis
by (simp add: bnat'_def tls.safety.cl_def tls.safety.upper_lower_upper tls.to_spec.Sup
not_tls_from_spec_Sup_distrib image_image)
qed
definition cl_bnat' :: "(unit, nat, unit) tls set" where
"cl_bnat' = tls.safety.cl ` bnat'"
lemma not_tls_safety_closed_Sup:
shows "cl_bnat' ⊆ tls.safety.closed"
and "⨆cl_bnat' ∉ tls.safety.closed"
unfolding cl_bnat'_def
using not_tls_safety_cl_Sup_distrib
by (blast intro: tls.safety.expansive complete_lattice_class.Sup_mono
dest: tls.safety.least[rotated, where x="⨆bnat'"])+
paragraph‹ Negation does not preserve \<^const>‹tls.safety.closed› ›
notepad
begin
have "tls.always (tls.state_prop id) ∈ tls.safety.closed"
by (simp add: tls.safety.closed.always tls.safety.closed.state_prop)
have "-tls.always (tls.state_prop id) ∉ tls.safety.closed"
proof -
let ?P = "behavior.B True (trepeat (undefined, True)) :: ('a, bool, 'c) behavior.t"
have "∃ω'. behavior.take i ?P = behavior.take i ω'
∧ (∃j ω''. behavior.dropn j ω' = Some ω'' ∧ ¬ behavior.init ω'')"
for i
by (auto simp: behavior.dropn.continue behavior.take.continue behavior.take.trepeat
trace.take.replicate case_tllist_trepeat
exI[where x="behavior.take i ?P @-⇩B trepeat (undefined, False)"]
exI[where x="Suc i"])
then have "⦉?P⦊⇩T ≤ tls.safety.cl (-tls.always (tls.state_prop id))"
by (clarsimp simp: tls.singleton.le_conv; fast)
moreover
have "behavior.init ω'"
if "behavior.dropn i (behavior.B True (trepeat (undefined, True))) = Some ω'"
for i and ω' :: "('a, bool, 'c) behavior.t"
using that
by (cases i) (auto simp: behavior.dropn_alt_def tdropn_trepeat case_tllist_trepeat)
then have "¬⦉?P⦊⇩T ≤ -tls.always (tls.state_prop id)"
by (auto simp: tls.singleton.le_conv)
ultimately show ?thesis
using tls.safety.le_closedE by blast
qed
end
subsection‹ Liveness\label{sec:safety_closure-liveness} ›
text‹
Famously arbitrary properties on infinite sequences can be decomposed into ∗‹safety› and ∗‹liveness›
properties. The latter have been identified with the topologically dense sets.
References:
▪ \<^citet>‹"AlpernSchneider:1985" and "Schneider:1987"›: topological account
▪ \<^citet>‹"Kindler:1994"›: overview
▪ \<^citet>‹‹\S8.5.3› in "Lynch:1996"›
▪ \<^citet>‹"ManoliosTrefler:2003"›: lattice-theoretic account
▪ \<^citet>‹"Maier:2004"›: an intuitionistic semantics for LTL (including next/X/‹○›) over finite and infinite sequences
›
setup ‹Sign.mandatory_path "raw.safety"›
lemma dense_alt_def:
shows "(raw.safety.dense :: ('a, 's, 'v) behavior.t set set)
= {P. ∀σ. ∃xsv. σ @-⇩B xsv ∈ P}" (is "?lhs = ?rhs")
proof(rule antisym)
have "∃xsv. σ @-⇩B xsv ∈ P" if "raw.safety.cl P = UNIV" for P and σ :: "('a, 's, 'v) trace.t"
using that
by (auto simp: behavior.take.continue
simp flip: trace.take.Ex_all
elim!: raw.safety.cl_altE[where i="Suc (length (trace.rest σ))"]
dest!: subsetD[where c="σ @-⇩B TNil undefined", OF Set.equalityD2])
(metis behavior.continue.take_drop_id behavior.continue.tshift2)
then show "?lhs ⊆ ?rhs"
by (clarsimp simp: raw.safety.dense_def)
next
have "ω ∈ raw.safety.cl P" if "∀σ. ∃xsv. σ @-⇩B xsv ∈ P" for P and ω :: "('a, 's, 'v) behavior.t"
proof(rule raw.safety.cl_altI)
fix i
from spec[OF that, where x="behavior.take i ω"]
obtain xsv where "behavior.take i ω @-⇩B xsv ∈ P" ..
moreover
have "behavior.take i ω = behavior.take i (behavior.take i ω @-⇩B xsv)"
by (clarsimp simp: behavior.take.continue behavior.take.all_continue
trace.take.behavior.take length_ttake not_le
split: enat.split split_min)
ultimately show "∃ω'∈P. behavior.take i ω = behavior.take i ω'" ..
qed
then show "?rhs ⊆ ?lhs"
by (auto simp: raw.safety.dense_def)
qed
setup ‹Sign.parent_path›
setup ‹Sign.mandatory_path "tls"›
definition live :: "('a, 's, 'v) tls set" where
"live = tls.safety.dense"
setup ‹Sign.mandatory_path "live"›
lemma not_bot:
shows "⊥ ∉ tls.live"
by (simp add: tls.live_def tls.safety.dense_def tls.bot_not_top)
lemma top:
shows "⊤ ∈ tls.live"
by (simp add: tls.live_def tls.safety.dense_top)
lemma live_le:
assumes "P ∈ tls.live"
assumes "P ≤ Q"
shows "Q ∈ tls.live"
using assms by (simp add: tls.live_def tls.safety.dense_le)
lemma inf_safety_eq_top:
shows "tls.live ⊓ tls.safety.closed = {⊤}"
unfolding tls.live_def by (rule tls.safety.dense_inf_closed)
lemma terminating:
shows "tls.eventually tls.terminated ∈ tls.live"
by (simp add: tls.live_def tls.safety.dense_def tls.safety.cl.eventually[OF tls.terminated.not_bot])
text‹
However this definition of liveness does not endorse traditional ∗‹response› properties.
›
corec alternating :: "bool ⇒ ('a × bool, 'b) tllist" where
"alternating b = TCons (undefined, b) (alternating (¬b))"
abbreviation (input) "A b ≡ behavior.B b (tls.live.alternating (¬b))"
lemma dropn_alternating:
shows "behavior.dropn i (tls.live.A b) = Some (tls.live.A (if even i then b else ¬b))"
proof(induct i arbitrary: b)
case (Suc i) show ?case
by (subst tls.live.alternating.code) (simp add: behavior.dropn.Suc Suc[of "¬b", simplified])
qed simp
notepad
begin
let ?P = "tls.leads_to (tls.state_prop id) (tls.state_prop Not) :: ('a, bool, unit) tls"
let ?ω = "⦉behavior.B True (TNil ())⦊⇩T :: ('a, bool, unit) tls"
have "¬?ω ≤ ?P"
by (auto simp: tls.singleton.le_conv split: nat.split)
then have "¬?ω ≤ tls.safety.cl ?P"
by (simp add: tls.safety.cl.terminated_iff tls.singleton.terminated_le_conv behavior.sset.simps)
then have "?P ∉ tls.live"
by (auto simp: tls.live_def tls.safety.dense_def
dest: order.trans[where a="?ω", OF top_greatest eq_refl[OF sym]])
let ?ω' = "⦉tls.live.A True⦊⇩T :: ('a, bool, unit) tls"
have "?ω' ≤ ?P"
by (clarsimp simp: tls.singleton.le_conv tls.live.dropn_alternating[where b=True, simplified]) presburger
let ?Q = "tls.always (tls.terminated ❙⟶⇩B tls.state_prop Not) :: ('a, bool, unit) tls"
have "?Q ∈ tls.safety.closed"
by (simp add: tls.safety.closed.always tls.safety.closed.boolean_implication
tls.safety.closed.not_terminated tls.safety.closed.state_prop)
moreover have "¬?ω ≤ ?Q"
by (auto simp: tls.singleton.le_conv behavior.sset.simps split: nat.split)
then have "?Q ≠ ⊤"
by (auto dest: order.trans[where a="?ω", OF top_greatest eq_refl[OF sym]])
ultimately have "?Q ∉ tls.live"
using tls.live.inf_safety_eq_top by auto
moreover
have "tls.terminated ⊓ (tls.state_prop id ❙⟶⇩B tls.eventually (tls.state_prop Not)) ≤ tls.state_prop Not"
by (simp add: boolean_implication.conv_sup inf_sup_distrib tls.state_prop.simps tls.terminated.inf_eventually)
then have "?P ≤ ?Q"
by - (rule tls.always.mono;
simp add: tls.terminated.inf_always flip: boolean_implication.shunt2)
ultimately have "?P ∉ tls.live"
by (blast dest: tls.live.live_le)
end
setup ‹Sign.parent_path›
paragraph‹ The famous decomposition ›
definition Safe :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
"Safe P = tls.safety.cl P"
definition Live :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
"Live P = P ⊔ -tls.safety.cl P"
lemma decomp:
shows "P = tls.Safe P ⊓ tls.Live P"
by (simp add: tls.Safe_def tls.Live_def boolean_algebra.conj_disj_distrib inf.absorb2 tls.safety.expansive)
setup ‹Sign.mandatory_path "safety.closed"›
lemma Safe:
shows "tls.Safe P ∈ tls.safety.closed"
by (simp add: tls.Safe_def)
setup ‹Sign.parent_path›
setup ‹Sign.mandatory_path "live"›
lemma Live:
shows "tls.Live P ∈ tls.live"
by (simp add: tls.live_def tls.safety.dense_def tls.Live_def sup_shunt tls.safety.cl.sup tls.safety.expansive)
setup ‹Sign.parent_path›
setup ‹Sign.parent_path›
end