Theory HMLSL_Perfect

(*  Title:      perfect/HMLSL_Perfect.thy
    Author:     Sven Linker

Defines HMLSL with perfect sensors for cars. Cars can perceive both
the physical size and braking distance of all other cars.
*)

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