Theory HMLSL_Perfect
section‹HMLSL for Perfect Sensors›
text ‹
Within this section, we instantiate HMLSL for cars with
perfect sensors.
›
theory HMLSL_Perfect
imports "../HMLSL" "Perfect_Sensors"
begin
locale hmlsl_perfect = perfect_sensors + restriction
begin
interpretation hmlsl : hmlsl "perfect :: cars ⇒ traffic ⇒ cars ⇒ real"
proof unfold_locales
fix e ts c
show " 0 < perfect e ts c"
by (metis less_add_same_cancel2 less_trans perfect_def traffic.psGeZero
traffic.sdGeZero)
qed
notation hmlsl.re (‹re'(_')›)
notation hmlsl.cl(‹cl'(_')›)
notation hmlsl.len (‹len›)
text ‹
The spatial atoms are independent of the perspective of the view.
Hence we can prove several lemmas on the relation between the hybrid modality
and the spatial atoms.
›
lemma at_res1:"⊨(re(c)) ❙→ (❙∀d. ❙@d re(c))"
by (metis (no_types, lifting) perfect_sensors.switch_length_stable
restriction.switch_restrict_stable view.switch_def)
lemma at_res2:"⊨(❙∀d. ❙@d re(c)) ❙→ re(c)"
using view.switch_refl by blast
lemma at_res:"⊨re(c) ❙↔ (❙∀d. ❙@d re(c))"
using at_res1 at_res2 by blast
lemma at_res_inst:"⊨ (❙@d re(c)) ❙→re(c)"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts,v ⊨( ❙@d re(c))"
obtain v' where v'_def:"(v=(d)> v') "
using view.switch_always_exists by blast
with assm have v':"ts,v' ⊨ re(c)" by blast
with v' show "ts,v ⊨re(c)"
using restriction.switch_restrict_stable perfect_sensors.switch_length_stable v'_def
view.switch_def
by (metis (no_types, lifting) all_own_ext_eq_len_eq)
qed
lemma at_clm1:"⊨cl(c) ❙→ (❙∀d. ❙@d cl(c))"
by (metis (no_types, lifting) all_own_ext_eq_len_eq view.switch_def
restriction.switch_restrict_stable)
lemma at_clm2:"⊨(❙∀d. ❙@d cl(c)) ❙→ cl(c)"
using view.switch_def by auto
lemma at_clm:"⊨cl(c) ❙↔ (❙∀d. ❙@d cl(c))"
using at_clm1 at_clm2 by blast
lemma at_clm_inst:"⊨ (❙@d cl(c)) ❙→cl(c)"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts,v ⊨( ❙@d cl(c))"
obtain v' where v'_def:"(v=(d)> v') "
using view.switch_always_exists by blast
with assm have v':"ts,v' ⊨ cl(c)" by blast
with v' show "ts,v ⊨cl(c)"
using restriction.switch_restrict_stable switch_length_stable v'_def view.switch_def
by (metis (no_types, lifting) all_own_ext_eq_len_eq)
qed
text‹
With the definition of sensors, we can also express how the spatial situation
changes after the different transitions. In particular, we can prove
lemmas corresponding to the activity and stability rules of the
proof system for MLSL \<^cite>‹"Linker2015a"›.
Observe that we were not able to prove these rules for basic HMLSL, since
its generic sensor function allows for instantiations where the perceived length changes
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 blast
hence restr_subs_res:"restrict v (res ts) c ⊑ restrict v (res ts') c"
by (simp add: restriction.restrict_view assm)
have "clm ts c ⊑ res ts' c" using assm traffic.create_res_subseteq2 by blast
hence restr_subs_clm:"restrict v (clm ts) c ⊑ restrict v (res ts') c"
by (simp add: restriction.restrict_view assm)
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
thus " ts,v ⊨ (re(c) ❙∨ cl(c))"
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 inter_empty2 local.hmlsl.free_no_clm
restriction.create_reservation_restrict_union restriction.restrict_def'
un_empty_absorb1)
hence 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
thus " ts,v ⊨ (re(c) ❙∨ cl(c))"
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 perfect_sensors.create_reservation_length_stable restriction.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 perfect_sensors.withdraw_reservation_length_stable
restriction.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)"
show ?thesis
by (metis inf.absorb1 order_trans perfect_sensors.create_reservation_length_stable
re restriction.restrict_def' restriction.restrict_subseteq
traffic.create_res_subseteq1 ts'_def)
next
assume cl:"ts,v ⊨cl(c)"
show ?thesis
by (metis cl inf.absorb1 order_trans perfect_sensors.create_reservation_length_stable
restriction.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 blast
lemma reservation:"⊨(❙□r(c) re(c)) ❙↔ (re(c) ❙∨ cl(c))"
using reservation1 reservation2 by blast
end
end