Theory HMLSL_Regular
section‹HMLSL for Regular Sensors›
text ‹
Within this section, we instantiate HMLSL for cars with
regular sensors.
›
theory HMLSL_Regular
imports "../HMLSL" Regular_Sensors
begin
locale hmlsl_regular = regular_sensors + restriction
begin
interpretation hmlsl : hmlsl "regular :: cars ⇒ traffic ⇒ cars ⇒ real"
proof unfold_locales
fix e ts c
show " 0 < regular e ts c"
by (metis less_add_same_cancel2 less_trans regular_def
traffic.psGeZero traffic.sdGeZero)
qed
notation hmlsl.re (‹re'(_')›)
notation hmlsl.cl(‹cl'(_')›)
notation hmlsl.len (‹len›)
text ‹
The spatial atoms are dependent of the perspective of the view,
hence we cannot prove similar lemmas as for perfect sensors.
However, we can still prove
lemmas corresponding to the activity and stability rules of the
proof system for MLSL \<^cite>‹"Linker2015a"›.
Similar to the situation with perfect sensors, needed to instantiate the
sensor function, to ensure that the perceived length does not change
during spatial transitions.
›
lemma backwards_res_act:
"(ts ❙─r(c) ❙→ ts') ∧ (ts',v ⊨ re(c)) ⟶ (ts,v ⊨ re(c) ❙∨ cl(c))"
proof
assume assm:"(ts ❙─r(c) ❙→ ts') ∧ (ts',v ⊨ re(c))"
from assm have len_eq:"len v ts c = len v ts' c"
using create_reservation_length_stable by blast
have "res ts c ⊑ res ts' c" using assm traffic.create_res_subseteq1
by auto
hence restr_subs_res:"restrict v (res ts) c ⊑ restrict v (res ts') c"
using assm restriction.restrict_view by auto
have "clm ts c ⊑ res ts' c" using assm traffic.create_res_subseteq2
using assm restriction.restrict_view by auto
hence restr_subs_clm:"restrict v (clm ts) c ⊑ restrict v (res ts') c"
using assm restriction.restrict_view by auto
have "restrict v (res ts) c = ∅ ∨ restrict v (res ts) c ≠ ∅" by simp
then show " ts,v ⊨ (re(c) ❙∨ cl(c))"
proof
assume restr_res_nonempty:"restrict v (res ts) c ≠ ∅"
hence restrict_one:"|restrict v (res ts) c | = 1"
using nat_int.card_non_empty_geq_one nat_int.card_subset_le dual_order.antisym
restr_subs_res assm by fastforce
have "restrict v (res ts ) c ⊑ lan v" using restr_subs_res assm by auto
hence "restrict v (res ts)c = lan v" using restriction.restrict_eq_lan_subs
restrict_one assm by auto
then show ?thesis using assm len_eq by auto
next
assume restr_res_empty:"restrict v (res ts) c = ∅"
then have clm_non_empty: "restrict v (clm ts) c ≠ ∅"
by (metis assm bot.extremum inf.absorb1 inf_commute local.hmlsl.free_no_clm
restriction.create_reservation_restrict_union restriction.restrict_def
un_empty_absorb1)
then have restrict_one:"|restrict v (clm ts) c | = 1"
using nat_int.card_non_empty_geq_one nat_int.card_subset_le dual_order.antisym
restr_subs_clm assm by fastforce
have "restrict v (clm ts ) c ⊑ lan v" using restr_subs_clm assm by auto
hence "restrict v (clm ts)c = lan v" using restriction.restrict_eq_lan_subs
restrict_one assm by auto
then show ?thesis using assm len_eq by auto
qed
qed
lemma backwards_res_act_somewhere:
"(ts ❙─r(c)❙→ ts') ∧ (ts',v ⊨ ❙⟨re(c)❙⟩) ⟶ (ts,v ⊨❙⟨ re(c) ❙∨ cl(c)❙⟩ )"
using backwards_res_act by blast
lemma backwards_res_stab:
"(ts ❙─r(d) ❙→ ts') ∧ (d ≠c) ∧ (ts',v ⊨ re(c)) ⟶ (ts,v ⊨ re(c))"
using regular_sensors.create_reservation_length_stable restrict_def'
traffic.create_res_subseteq1_neq by auto
lemma backwards_c_res_stab:
"(ts ❙─c(d,n) ❙→ ts') ∧ (ts',v ⊨ re(c)) ⟶ (ts,v ⊨ re(c))"
using create_claim_length_stable traffic.create_clm_eq_res
by (metis (mono_tags, lifting) traffic.create_claim_def)
lemma backwards_wdc_res_stab:
"(ts ❙─wdc(d) ❙→ ts') ∧ (ts',v ⊨ re(c)) ⟶ (ts,v ⊨ re(c))"
using withdraw_claim_length_stable traffic.withdraw_clm_eq_res
by (metis (mono_tags, lifting) traffic.withdraw_claim_def)
lemma backwards_wdr_res_stab:
"(ts ❙─wdr(d,n) ❙→ ts') ∧ (ts',v ⊨ re(c)) ⟶ (ts,v ⊨ re(c))"
by (metis inf.absorb1 order_trans regular_sensors.withdraw_reservation_length_stable
restrict_def' restriction.restrict_res traffic.withdraw_res_subseteq)
text‹
We now proceed to prove the \emph{reservation lemma}, which was
crucial in the manual safety proof \cite {Hilscher2011}.
›
lemma reservation1: "⊨(re(c) ❙∨ cl(c)) ❙→ ❙□r(c) re(c)"
proof (rule allI| rule impI)+
fix ts v ts'
assume assm:"ts,v ⊨re(c) ❙∨ cl(c)" and ts'_def:"ts ❙─r(c)❙→ts'"
from assm show "ts',v ⊨ re(c)"
proof
assume re:"ts,v ⊨re(c)"
then show ?thesis
by (metis inf.absorb1 order_trans regular_sensors.create_reservation_length_stable
restrict_def' restriction.restrict_subseteq traffic.create_res_subseteq1 ts'_def)
next
assume cl:"ts,v ⊨cl(c)"
then show ?thesis
by (metis inf.absorb1 order_trans regular_sensors.create_reservation_length_stable
restrict_def' restriction.restrict_subseteq traffic.create_res_subseteq2 ts'_def)
qed
qed
lemma reservation2: "⊨(❙□r(c) re(c)) ❙→ (re(c) ❙∨ cl(c))"
using backwards_res_act traffic.always_create_res
by metis
lemma reservation:"⊨(❙□r(c) re(c)) ❙↔ (re(c) ❙∨ cl(c))"
using reservation1 reservation2 by blast
end
end