Theory Safety_Regular
section‹Safety for Cars with Regular Sensors›
text‹
This section contains the definition of requirements for
lane change and distance controllers for cars, with the assumption
of regular sensors. Using these definitions, we show that safety
is an invariant along all possible behaviour of cars.
However, we need to slightly amend our notion of safety, compared
to the safety proof for perfect sensors.
›
theory Safety_Regular
imports HMLSL_Regular
begin
context hmlsl_regular
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.space (‹space›)
notation hmlsl.re (‹re'(_')›)
notation hmlsl.cl(‹cl'(_')›)
notation hmlsl.len (‹len›)
text‹
First we show that the same "safety" theorem as for perfect senors can be
proven. However, we will subsequently show that this theorem does not
ensure safety from the perspective of each car.
The controller definitions for this "flawed" safety are the same as for perfect sensors.
›
abbreviation safe::"cars⇒σ"
where "safe e ≡ ❙∀ c. ❙¬(c ❙= e) ❙→ ❙¬❙⟨re(c) ❙∧ re(e) ❙⟩"
abbreviation DC::"σ"
where "DC ≡ ❙G(❙∀ c d. ❙¬(c ❙= d) ❙→
❙¬❙⟨re(c) ❙∧ re(d)❙⟩ ❙→ ❙□❙τ ❙¬❙⟨re(c) ❙∧ re(d)❙⟩)"
abbreviation pcc::"cars ⇒ cars ⇒ σ"
where "pcc c d ≡ ❙¬ (c ❙= d) ❙∧ ❙⟨ cl(d) ❙∧ (re(c) ❙∨ cl(c))❙⟩"
abbreviation LC::"σ"
where "LC ≡ ❙G ( ❙∀d.( ❙∃ c. pcc c d) ❙→ ❙□r(d) ❙⊥)"
text‹
The safety proof is exactly the same as for perfect sensors. Note
in particular, that we fix a single car \(e\) for which we show
safety.
›
theorem safety_flawed:"⊨( ❙∀e. safe e ) ❙∧ DC ❙∧ LC ❙→ ❙G (❙∀ e. safe e)"
proof (rule allI|rule impI)+
fix ts v ts'
fix e c:: cars
assume assm:"ts,v ⊨ ( ❙∀e. safe e ) ❙∧ DC ❙∧ LC"
assume abs:"(ts ❙⇒ ts')"
assume neg:"ts,v ⊨❙¬(c ❙= e)"
from assm have init:"ts,v ⊨ ( ❙∀e. safe e )" by simp
from assm have DC :"ts,v ⊨ DC" by simp
from assm have LC: "ts,v ⊨ LC" by simp
show "ts',move ts ts' v ⊨ ❙¬ ❙⟨re(c) ❙∧ re(e)❙⟩" using abs
proof (induction)
case (refl )
have "move ts ts v = v" using move_nothing by simp
thus ?case using init move_nothing neg by simp
next
case (evolve ts' ts'' )
have local_DC:
"ts',move ts ts' v ⊨ ❙∀ c d. ❙¬(c ❙= d) ❙→
❙¬❙⟨re(c) ❙∧ re(d)❙⟩ ❙→ ❙□❙τ ❙¬❙⟨re(c) ❙∧ re(d)❙⟩"
using evolve.hyps DC by simp
show ?case
proof (rule )
assume e_def: " (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
from evolve.IH and e_def and neg have
ts'_safe:"ts',move ts ts' v ⊨ ❙¬(c ❙= e) ❙∧ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩" by blast
hence no_coll_after_evol:"ts',move ts ts' v ⊨ ❙□❙τ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩"
using local_DC by blast
have move_eq:"move ts' ts'' (move ts ts' v) = move ts ts'' v"
using "evolve.hyps" abstract.evolve abstract.refl move_trans
by (meson traffic.abstract.evolve traffic.abstract.refl traffic.move_trans)
from no_coll_after_evol and evolve.hyps have
"ts'',move ts' ts'' (move ts ts' v) ⊨ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩"
by blast
thus False using e_def using move_eq by fastforce
qed
next
case (cr_res ts' ts'')
have local_LC: "ts',move ts ts' v ⊨( ❙∀d.( ❙∃ c. pcc c d) ❙→ ❙□r(d) ❙⊥) "
using LC cr_res.hyps by blast
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_res cr_res.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
using cr_res.hyps local.create_reservation_def local.move_def by auto
show ?case
proof (rule)
assume e_def:" (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
obtain d where d_def: "ts' ❙─r(d) ❙→ ts''" using cr_res.hyps by blast
have "d = e ∨ d ≠ e" by simp
thus False
proof
assume eq:"d = e"
hence e_trans:"ts' ❙─r(e) ❙→ ts''" using d_def by simp
from e_def have "ts'',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
with backwards_res_act have "ts',v' ⊨ re(c) ❙∧ (re(e) ❙∨ cl(e))"
using e_def backwards_res_stab neg
by (metis (no_types, lifting) d_def eq)
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts',v' ⊨ re(c) ❙∧ (re(e) ❙∨ cl(e)))"
using v'_def by blast
hence "ts',move ts ts'' v ⊨❙⟨ re(c) ❙∧ (re(e) ❙∨ cl(e)) ❙⟩"
using somewhere_leq by meson
hence "ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩ ❙∨ ❙⟨ re(c) ❙∧ cl(e)❙⟩ "
using hmlsl.somewhere_and_or_distr by blast
thus False
proof
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩"
have "ts',move ts ts' v ⊨ ❙¬ (c ❙= e)" using neg by blast
thus False using assm' cr_res.IH e_def move_stab by force
next
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ cl(e)❙⟩"
hence "ts',move ts ts'' v ⊨ ❙¬ (c ❙=e) ❙∧ ❙⟨ re(c) ❙∧ cl(e)❙⟩"
using neg by force
hence "ts',move ts ts'' v ⊨❙¬ (c ❙=e) ❙∧ ❙⟨ cl(e) ❙∧ (re(c) ❙∨ cl(c)) ❙⟩" by blast
hence pcc:"ts',move ts ts'' v ⊨ pcc c e" by blast
have "ts',move ts ts'' v ⊨( ❙∃ c. pcc c e) ❙→ ❙□r(e) ❙⊥ "
using local_LC move_stab by fastforce
hence "ts',move ts ts'' v ⊨ ❙□r(e) ❙⊥" using pcc by blast
thus "ts'',move ts ts'' v ⊨ ❙⊥" using e_trans by blast
qed
next
assume neq:"d ≠ e"
have "c=d ∨ c ≠ d" by simp
thus False
proof
assume neq2:"c ≠ d"
from e_def have "ts'',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
with backwards_res_stab have overlap: "ts',v' ⊨ re(c) ❙∧ (re(e))"
using e_def backwards_res_stab neg neq2
by (metis (no_types, lifting) d_def neq)
hence unsafe2:"ts',move ts ts'' v ⊨❙⟨re(c) ❙∧ re(e)❙⟩"
using somewhere_leq v'_def by blast
from cr_res.IH have "ts',move ts ts'' v ⊨ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩"
using move_stab by force
thus False using unsafe2 by best
next
assume eq2:"c = d"
hence e_trans:"ts' ❙─r(c) ❙→ ts''" using d_def by simp
from e_def have "ts'',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
with backwards_res_act have "ts',v' ⊨ (re(c) ❙∨ cl(c)) ❙∧ (re(e) )"
using e_def backwards_res_stab neg
by (metis (no_types, lifting) d_def eq2)
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts',v' ⊨ (re(c) ❙∨ cl(c)) ❙∧ (re(e)))"
using v'_def by blast
hence "ts',move ts ts'' v ⊨❙⟨ (re(c) ❙∨ cl(c)) ❙∧ (re(e) ) ❙⟩"
using somewhere_leq by meson
hence "ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩ ❙∨ ❙⟨ cl(c) ❙∧ re(e)❙⟩ "
using hmlsl.somewhere_and_or_distr by blast
thus False
proof
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩"
have "ts',move ts ts'' v ⊨ ❙¬ (c ❙= e)" using neg by blast
thus False using assm' cr_res.IH e_def move_stab by fastforce
next
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ cl(c) ❙∧ re(e)❙⟩"
hence "ts',move ts ts'' v ⊨ ❙¬ (c ❙=e) ❙∧ ❙⟨ cl(c) ❙∧ re(e)❙⟩"
using neg by blast
hence "ts',move ts ts'' v ⊨❙¬ (c ❙=e) ❙∧ ❙⟨ cl(c) ❙∧ (re(e) ❙∨ cl(e))❙⟩"
by blast
hence pcc:"ts',move ts ts'' v ⊨ pcc e c" by blast
have "ts',move ts ts'' v ⊨( ❙∃ d. pcc d c) ❙→ ❙□r(c) ❙⊥ "
using local_LC move_stab by fastforce
hence "ts',move ts ts'' v ⊨ ❙□r(c) ❙⊥" using pcc by blast
thus "ts'',move ts ts'' v ⊨ ❙⊥" using e_trans by blast
qed
qed
qed
qed
next
case (cr_clm ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_clm cr_clm.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis abstract.simps cr_clm.hyps move_trans)
show ?case
proof (rule)
assume e_def: "(ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
obtain d where d_def: "∃n. (ts' ❙─c(d,n) ❙→ ts'')" using cr_clm.hyps by blast
then obtain n where n_def:" (ts' ❙─c(d,n) ❙→ ts'')" by blast
from e_def have "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq by fastforce
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using n_def backwards_c_res_stab by blast
hence "ts',move ts ts'' v ⊨ ❙⟨re(c) ❙∧re(e) ❙⟩"
using e_def v'_def somewhere_leq by meson
thus False using cr_clm.IH move_stab by fastforce
qed
next
case (wd_res ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_wdr wd_res.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis abstract.simps wd_res.hyps move_trans)
show ?case
proof (rule)
assume e_def:" (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
obtain d and n where n_def:" (ts' ❙─wdr(d,n) ❙→ ts'')"
using wd_res.hyps by auto
from e_def have "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq by fastforce
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using n_def backwards_wdr_res_stab by blast
hence "ts',move ts ts'' v ⊨❙⟨re(c) ❙∧re(e)❙⟩" using
v'_def somewhere_leq by meson
thus False using wd_res.IH move_stab by fastforce
qed
next
case (wd_clm ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_wdc wd_clm.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis abstract.simps wd_clm.hyps move_trans)
show ?case
proof (rule)
assume e_def: " (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
obtain d where d_def: " (ts' ❙─wdc(d) ❙→ ts'')" using wd_clm.hyps by blast
from e_def have "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq by fastforce
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
from this have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using d_def backwards_wdc_res_stab by blast
hence "ts',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩" using v'_def somewhere_leq by meson
thus False using wd_clm.IH move_stab by fastforce
qed
qed
qed
text‹
As stated above, the flawed safety theorem does not ensure safety for
the perspective of each car.
In particular, we can construct a traffic snapshot and a view, such that
it satisfies our safety predicate for each car, but if we switch the
perspective of the view to another car, the situation is unsafe. A
visualisation of this situation can be found in the publication
of this work at iFM 2017 \<^cite>‹"Linker2017"›.
›
lemma safety_not_invariant_switch:
"∃ts v. (ts,v ⊨ ❙∀e. safe(e) ❙∧ ( ❙∃ c. ❙@c ❙¬( ❙∀e. safe(e))))"
proof -
obtain d c ::cars where assumption:"d ≠c"
using cars.at_least_two_cars_exists by best
obtain pos' where pos'_def:"∀(c::cars). (pos' c) = (5::real)" by best
obtain po where pos_def:"po = (pos'(c:=0))(d:=2)" by best
obtain re where res_def:"∀(c::cars). re c = Abs_nat_int{0}" by best
obtain cl where clm_def:"∀(c::cars). cl c= ∅" by best
obtain dy where dyn_def:"∀c::cars. ∀x::real . (dy c) x = (0::real)" by force
obtain sd where sd_def:"∀(c::cars). sd c = (2::real)" by best
obtain ps where ps_def:"∀(c::cars). ps c = (1::real)" by best
obtain ts_rep where ts_rep_def:"ts_rep= (po, re, cl, dy, ps, sd)" by best
have disj:"∀c .((re c) ⊓ (cl c) = ∅)" by (simp add: clm_def nat_int.inter_empty1)
have re_geq_one:"∀c. |re c| ≥ 1"
by (simp add: Abs_nat_int_inverse nat_int.card'_def res_def)
have re_leq_two:"∀c. |re c| ≤ 2"
using nat_int.card'.rep_eq res_def nat_int.rep_single by auto
have cl_leq_one:"∀c. |cl c| ≤ 1"
using nat_int.card_empty_zero clm_def by (simp )
have add_leq_two:"∀c . |re c| + |cl c| ≤ 2"
using nat_int.card_empty_zero clm_def re_leq_two by (simp )
have clNextRe :
"∀c. ((cl c) ≠ ∅ ⟶ (∃ n. Rep_nat_int (re c) ∪ Rep_nat_int (cl c) = {n, n+1}))"
by (simp add: clm_def)
from dyn_def have dyn_geq_zero:"∀c. ∀x. (dy c x) ≥ 0" by auto
from ps_def have ps_ge_zero :"∀c. ps c> 0" by auto
from sd_def have sd_ge_zero: "∀c. sd c > 0" by auto
have ts_in_type: " ts_rep ∈
{ts :: (cars⇒real)*(cars⇒lanes)*(cars⇒lanes)*(cars⇒real⇒real)*(cars⇒real)*(cars⇒real).
(∀c. ((fst (snd ts))) c ⊓ ((fst (snd (snd ts)))) c = ∅ ) ∧
(∀c. |(fst (snd ts)) c| ≥ 1) ∧
(∀c. |(fst (snd ts)) c| ≤ 2) ∧
(∀c. |(fst (snd (snd ts)) c)| ≤ 1) ∧
(∀c. |(fst (snd ts)) c| + |(fst (snd (snd ts))) c| ≤ 2) ∧
(∀c. (fst(snd(snd (ts)))) c ≠ ∅ ⟶
(∃ n. Rep_nat_int ((fst (snd ts)) c) ∪ Rep_nat_int ((fst (snd (snd ts))) c)
= {n, n+1})) ∧
(∀c . fst (snd (snd (snd (snd (ts))))) c > 0) ∧
(∀c. snd (snd (snd (snd (snd (ts))))) c > 0)
} "
using pos_def res_def clm_def disj re_geq_one re_leq_two cl_leq_one add_leq_two
ps_ge_zero sd_ge_zero ts_rep_def
by auto
obtain v where v_def:
"v=⦇ext = Abs_real_int (0,3), lan = Abs_nat_int{0}, own = d⦈"
by best
obtain ts where ts_def:"ts=Abs_traffic ts_rep"
by blast
have size:"∀c. physical_size ts c = 1" using ps_def physical_size_def ts_rep_def
ts_in_type ts_def ps_ge_zero using Abs_traffic_inverse
by auto
have safe:" ts,v ⊨ ❙∀e. safe(e) "
proof
have other_len_zero:"∀e. e ≠c ∧ e ≠d ⟶ ∥ len v ts e∥ = 0"
proof (rule allI|rule impI)+
fix e
assume e_def:" e ≠c ∧ e ≠d"
have position:"pos ts e = 5" using e_def ts_def ts_rep_def ts_in_type ts_def
Abs_traffic_inverse pos_def fun_upd_apply pos'_def traffic.pos_def
by auto
have "regular (own v) ts e = 1"
using e_def v_def sensors_def ps_def ts_def size regular_def by auto
then have space:"space ts v e = Abs_real_int (5,6)"
using e_def pos_def position hmlsl.space_def by auto
have "left (space ts v e) > right (ext v)"
using space v_def Abs_real_int_inverse by auto
thus "∥ len v ts e∥ = 0"
using hmlsl.len_def real_int.length_def Abs_real_int_inverse by auto
qed
have no_cars:"∀e. e ≠c ∧ e ≠d ⟶ (ts,v ⊨ ❙¬ ❙⟨ re(e) ❙∨ cl(e) ❙⟩)"
proof (rule allI|rule impI|rule notI)+
fix e
assume neq:"e ≠c ∧ e ≠d"
assume contra:"ts,v ⊨ ❙⟨ re(e) ❙∨ cl(e) ❙⟩"
from other_len_zero have len_e:"∥len v ts e∥ = 0" using neq by auto
from contra obtain v' where v'_def:"v' ≤ v ∧ (ts,v' ⊨re(e) ❙∨ cl(e))"
using somewhere_leq by force
from v'_def and len_e have len_v':"∥len v' ts e∥ = 0"
using hmlsl.len_empty_subview by blast
from v'_def have "ts,v' ⊨re(e) ❙∨ cl(e)" by blast
thus False using len_v' by auto
qed
have sensors_c:"regular (own v) ts c = 1"
using v_def regular_def ps_def ts_def size assumption by auto
have space_c:"space ts v c = Abs_real_int (0,1)"
using pos_def ts_def ts_rep_def ts_in_type Abs_traffic_inverse
fun_upd_apply sensors_c assumption hmlsl.space_def traffic.pos_def
by auto
have lc:"left (space ts v c) = 0" using space_c Abs_real_int_inverse by auto
have rv:"right (ext v) = 3" using v_def Abs_real_int_inverse by auto
have lv:"left (ext v) = 0" using v_def Abs_real_int_inverse by auto
have rc:"right (space ts v c) = 1" using space_c Abs_real_int_inverse by auto
have len_c:"len v ts c = Abs_real_int(0,1)"
using space_c v_def hmlsl.len_def lc lv rv rc by auto
have sensors_d:"regular (own v) ts d = 3"
using v_def regular_def braking_distance_def ts_def size sd_def
Abs_traffic_inverse ts_in_type ts_rep_def
by auto
have space_d:"space ts v d = Abs_real_int(2,5)"
using pos_def ts_def ts_rep_def ts_in_type Abs_traffic_inverse
fun_upd_apply sensors_d assumption hmlsl.space_def traffic.pos_def
by auto
have ld:"left (space ts v d) = 2" using space_d Abs_real_int_inverse by auto
have rd: "right (space ts v d) = 5" using space_d Abs_real_int_inverse by auto
have len_d :"len v ts d = Abs_real_int(2,3)"
using space_d v_def hmlsl.len_def ld rd lv rv by auto
have no_overlap_c_d:"ts,v ⊨❙¬ ❙⟨re(c) ❙∧ re(d)❙⟩"
proof (rule notI)
assume contra:"ts,v ⊨ ❙⟨re(c) ❙∧ re(d)❙⟩"
obtain v' where v'_def:"(v' ≤ v) ∧ (ts,v' ⊨re(c) ❙∧ re(d))"
using somewhere_leq contra by force
hence len_eq:"len v' ts c = len v' ts d" by simp
from v'_def have v'_c:"∥len v' ts c∥ > 0"
and v'_d:"∥len v' ts d∥ > 0" by simp+
from v'_c have v'_rel_c:
"left (space ts v' c) < right (ext v') ∧ right (space ts v' c) > left (ext v')"
using hmlsl.len_non_empty_inside by blast
from v'_d have v'_rel_d:
"left (space ts v' d) < right (ext v') ∧ right (space ts v' d) > left (ext v')"
using hmlsl.len_non_empty_inside by blast
have less_len:"len v' ts c ≤ len v ts c"
using hmlsl.view_leq_len_leq v'_c v'_def less_eq_view_ext_def by blast
have sp_eq_c:"space ts v' c = space ts v c"
using v'_def less_eq_view_ext_def regular_def hmlsl.space_def by auto
have sp_eq_d:"space ts v' d = space ts v d"
using v'_def less_eq_view_ext_def regular_def hmlsl.space_def by auto
have "right (ext v') > 0 ∧ right (ext v') > 2"
using ld lc v'_rel_c v'_rel_d sp_eq_c sp_eq_d by auto
hence r_v':"right (ext v') > 2" by blast
have "left (ext v') < 1 ∧ left (ext v') < 5"
using rd rc v'_rel_c v'_rel_d sp_eq_c sp_eq_d by auto
hence l_v':"left (ext v') < 1" by blast
have "len v' ts c ≠ ext v' "
proof
assume "len v' ts c = ext v'"
hence eq:"right (len v' ts c) = right (ext v')" by simp
from less_len have "right (len v' ts c) ≤ right (len v ts c)"
by (simp add: less_eq_real_int_def)
with len_c have "right (len v' ts c) ≤ 1 "
using Abs_real_int_inverse by auto
thus False using r_v' eq by linarith
qed
thus False using v'_def by blast
qed
fix x
show "ts,v ⊨ safe(x)"
proof (rule allI|rule impI)+
fix y
assume x_neg_y: "ts,v ⊨ ❙¬(y ❙= x)"
show "ts,v ⊨❙¬❙⟨re(y) ❙∧ re(x)❙⟩"
proof (cases "y ≠c ∧ y ≠d")
assume "y ≠ c ∧ y ≠ d"
hence "(ts,v ⊨ ❙¬ ❙⟨ re(y) ❙∨ cl(y) ❙⟩)" using no_cars by blast
hence "ts,v ⊨ ❙¬ ❙⟨ re(y) ❙⟩" by blast
then show ?thesis by blast
next
assume "¬(y ≠c ∧ y ≠d)"
hence "y = c ∨ y = d" by blast
thus ?thesis
proof
assume y_eq_c:"y=c"
thus ?thesis
proof (cases "x=d")
assume "x=d"
then show "ts,v ⊨❙¬ ❙⟨re(y) ❙∧ re(x)❙⟩"
using no_overlap_c_d y_eq_c by blast
next
assume x:"x ≠d"
have x2:"x ≠c" using y_eq_c x_neg_y by blast
hence "(ts,v ⊨ ❙¬ ❙⟨ re(x) ❙∨ cl(x) ❙⟩)" using no_cars x by blast
hence "ts,v ⊨ ❙¬ ❙⟨ re(x) ❙⟩" by blast
thus ?thesis by blast
qed
next
assume y_eq_c:"y=d"
thus ?thesis
proof (cases "x=c")
assume "x=c"
thus "ts,v ⊨❙¬ ❙⟨re(y) ❙∧ re(x)❙⟩" using no_overlap_c_d y_eq_c by blast
next
assume x:"x ≠c"
have x2:"x ≠d" using y_eq_c x_neg_y by blast
hence "(ts,v ⊨ ❙¬ ❙⟨ re(x) ❙∨ cl(x) ❙⟩)" using no_cars x by blast
hence "ts,v ⊨ ❙¬ ❙⟨ re(x) ❙⟩" by blast
thus ?thesis by blast
qed
qed
qed
qed
qed
have unsafe:"ts,v ⊨ (❙∃ c. (❙@c ❙¬( ❙∀e. safe(e))))"
proof -
have "ts,v ⊨ (❙@c ❙¬( ❙∀e. safe(e)))"
proof (rule allI|rule impI|rule notI)+
fix vc
assume sw:"( v=c>vc)"
have spatial_vc:"ext v = ext vc ∧ lan v = lan vc"
using switch_def sw by blast
assume safe: "ts,vc⊨ ( ❙∀e. safe(e))"
obtain vc' where vc'_def:
"vc'=⦇ext = Abs_real_int (2,3), lan = Abs_nat_int {0}, own = c⦈"
by best
have own_eq:"own vc' = own vc" using sw switch_def vc'_def by auto
have ext_vc:"ext vc = Abs_real_int (0,3)" using spatial_vc v_def by force
have right_ok:"right (ext vc) ≥ right (ext vc')"
using vc'_def ext_vc Abs_real_int_inverse by auto
have left_ok:"left (ext vc') ≥ left (ext vc)"
using vc'_def ext_vc Abs_real_int_inverse by auto
hence ext_leq: "ext vc' ≤ ext vc"
using right_ok left_ok less_eq_real_int_def by auto
have "lan vc = Abs_nat_int{0}" using v_def switch_def sw by force
hence lan_leq:"lan vc' ⊑ lan vc" using vc'_def order_refl by force
have leqvc:"vc' ≤ vc"
using ext_leq lan_leq own_eq less_eq_view_ext_def by force
have sensors_c:"regular (own vc') ts c = 3"
using vc'_def regular_def ps_def traffic.braking_distance_def
ts_def sd_def size assumption Abs_traffic_inverse ts_in_type ts_rep_def
by auto
have space_c:"space ts vc' c = Abs_real_int (0,3)"
using pos_def ts_def ts_rep_def ts_in_type Abs_traffic_inverse
fun_upd_apply sensors_c assumption hmlsl.space_def traffic.pos_def
by auto
have lc:"left (space ts vc' c) = 0" using space_c Abs_real_int_inverse by auto
have rv:"right (ext vc') = 3" using vc'_def Abs_real_int_inverse by auto
have lv:"left (ext vc') = 2" using vc'_def Abs_real_int_inverse by auto
have rc:"right (space ts vc' c) = 3" using space_c Abs_real_int_inverse by auto
have len_c:"len vc' ts c = Abs_real_int(2,3)"
using space_c v_def hmlsl.len_def lc lv rv rc by auto
have res_c: "restrict vc' (res ts) c = Abs_nat_int {0}"
using ts_def ts_rep_def ts_in_type Abs_traffic_inverse res_def traffic.res_def
inf_idem restrict_def vc'_def
by force
have sensors_d:"regular (own vc') ts d = 1"
using vc'_def regular_def ts_def size sd_def Abs_traffic_inverse ts_in_type
ts_rep_def assumption
by auto
have space_d:"space ts vc' d = Abs_real_int(2,3)"
using pos_def ts_def ts_rep_def ts_in_type Abs_traffic_inverse
fun_upd_apply sensors_d assumption hmlsl.space_def traffic.pos_def
by auto
have ld:"left (space ts vc' d) = 2" using space_d Abs_real_int_inverse by auto
have rd: "right (space ts vc' d) = 3" using space_d Abs_real_int_inverse by auto
have len_d :"len vc' ts d = Abs_real_int(2,3)"
using space_d v_def hmlsl.len_def ld rd lv rv
by auto
have res_d:"restrict vc' (res ts) d = Abs_nat_int {0}"
using ts_def ts_rep_def ts_in_type Abs_traffic_inverse res_def traffic.res_def
inf_idem restrict_def vc'_def by force
have "ts,vc' ⊨ re(c) ❙∧ re(d)" using
len_d len_c vc'_def ts_def ts_rep_def ts_in_type Abs_traffic_inverse
res_c res_d nat_int.card'_def
Abs_real_int_inverse real_int.length_def traffic.res_def
nat_int.singleton2 Abs_nat_int_inverse
by auto
with leqvc have "ts,vc ⊨ ❙⟨re(c) ❙∧ re(d)❙⟩" using somewhere_leq by blast
with assumption have "ts,vc ⊨ ❙¬ (c ❙= d) ❙∧ ❙⟨ re(c) ❙∧ re(d) ❙⟩" by blast
with safe show False by blast
qed
thus ?thesis by blast
qed
from safe and unsafe have "ts,v ⊨ ❙∀e. safe(e) ❙∧ (❙∃ c. (❙@c ❙¬( ❙∀e. safe(e))))"
by blast
thus ?thesis by blast
qed
text‹
Now we show how to amend the controller specifications to gain safety as an invariant
even with regular sensors.
The distance controller can be strengthened, by requiring that we switch
to the perspective of one of the cars involved first, before checking
for the collision. Since all variables are universally quantified,
this ensures that no collision exists for the perspective of any car.
›
abbreviation DC'::"σ"
where "DC' ≡ ❙G ( ❙∀ c d. ❙¬(c ❙= d) ❙→
(❙@d ❙¬❙⟨re(c) ❙∧ re(d)❙⟩) ❙→ ❙□❙τ ❙@d ❙¬❙⟨re(c) ❙∧ re(d)❙⟩)"
text‹
The amendment to the lane change controller is slightly different. Instead
of checking the potential collision only from the perspective of the
car \(d\) trying to change lanes, we require that also no other car may
perceive a potential collision. Note that the restriction to \(d\)'s
behaviour can only be enforced within \(d\), if the information from
the other car is somehow passed to \(d\). Hence, we require the
cars to communicate in some way. However, we do not need to specifiy,
\emph{how} this communication is implemented.
›
abbreviation LC'::"σ"
where "LC' ≡ ❙G ( ❙∀d. (❙∃ c. (❙@c (pcc c d)) ❙∨ (❙@d (pcc c d))) ❙→ ❙□r(d) ❙⊥ ) "
text‹
With these new controllers, we can prove a stronger theorem than before. Instead
of proving safety from the perspective of a single car as previously, we now
only consider a traffic situation to be safe, if it satisfies the safety
predicate from the perspective of \emph{all} cars. Note that this immediately
implies the safety invariance theorem proven for perfect sensors.
›
theorem safety:"⊨ (❙∀e. ❙@e ( safe e ) ) ❙∧ DC' ❙∧ LC' ❙→ ❙G(❙∀ e. ❙@ e (safe e))"
proof (rule allI; rule allI;rule impI; rule allI; rule impI; rule allI)
fix ts v ts' e
assume assm:"ts,v ⊨ ( ❙∀e. ❙@e (safe e) ) ❙∧ DC' ❙∧ LC'"
assume abs:"(ts ❙⇒ ts')"
from assm have init:"ts,v ⊨ ( ❙∀e. ❙@e (safe e) )" by simp
from assm have DC :"ts,v ⊨ DC'" by simp
from assm have LC: "ts,v ⊨ LC'" by simp
show "ts',move ts ts' v ⊨ ( ❙@e (safe e))" using abs
proof (induction)
case (refl )
have "move ts ts v = v" using move_nothing by blast
thus ?case using move_nothing init by simp
next
case (evolve ts' ts'' )
have local_DC:
"ts',move ts ts' v ⊨ ❙∀ c d. ❙¬(c ❙= d) ❙→
(❙@d ❙¬❙⟨re(c) ❙∧ re(d)❙⟩ ) ❙→ ( ❙□❙τ ❙@d ❙¬❙⟨re(c) ❙∧ re(d)❙⟩)"
using evolve.hyps DC by simp
show ?case
proof (rule ccontr)
assume "¬ (ts'',move ts ts'' v ⊨ ( ❙@e (safe e)))"
then have e_def:"ts'',move ts ts'' v ⊨ ❙¬(❙@e (safe e))" by best
hence "ts'',move ts ts'' v ⊨ ❙@e (❙¬ safe e)"
using switch_always_exists switch_unique by fastforce
then obtain ve where ve_def:
"((move ts ts'' v) =e> ve) ∧ (ts'',ve ⊨ ❙¬ safe e)"
using switch_always_exists by fastforce
hence unsafe:"ts'',ve ⊨ ❙∃ c. ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
then obtain c where c_def:"ts'',ve ⊨ ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
from evolve.IH and c_def have
ts'_safe:"ts',move ts ts' v ⊨ ❙@e (❙¬(c ❙= e) ❙∧ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩)"
by blast
hence not_eq:"ts',move ts ts' v ⊨❙@e (❙¬(c ❙= e))"
and safe':"ts',move ts ts' v ⊨ ❙@e ( ❙¬❙⟨re(c) ❙∧ re(e)❙⟩)"
using hmlsl.at_conj_distr by simp+
from not_eq have not_eq_v:"ts',move ts ts' v ⊨❙¬(c ❙=e)"
using hmlsl.at_eq switch_always_exists by auto
have
"ts',move ts ts' v ⊨ ❙¬(c ❙= e) ❙→
(❙@e ❙¬❙⟨re(c) ❙∧ re(e)❙⟩ ) ❙→ (❙□❙τ ❙@e ❙¬❙⟨re(c) ❙∧ re(e)❙⟩)"
using local_DC by simp
hence dc:"ts',move ts ts' v ⊨ (❙@e ❙¬❙⟨re(c) ❙∧ re(e)❙⟩ ) ❙→
(❙□❙τ ❙@e ❙¬❙⟨re(c) ❙∧ re(e)❙⟩)"
using not_eq_v
by simp
hence no_coll_after_evol:"ts',move ts ts' v ⊨ ( ❙□❙τ ❙@e ❙¬❙⟨re(c) ❙∧ re(e)❙⟩)"
using safe'
by simp
hence 1:"ts'',move ts' ts'' (move ts ts' v) ⊨ ❙@e ❙¬ ❙⟨re(c) ❙∧ re(e)❙⟩"
using evolve.hyps by simp
have move_eq:"move ts' ts'' (move ts ts' v) = move ts ts'' v"
using "evolve.hyps" abstract.evolve abstract.refl move_trans
by blast
from 1 have "ts'', move ts ts'' v ⊨ ❙@e ❙¬❙⟨re(c) ❙∧ re(e)❙⟩"
using move_eq by fastforce
hence "ts'',ve ⊨ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩" using ve_def by blast
thus False using c_def by blast
qed
next
case (cr_clm ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_clm cr_clm.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis abstract.simps cr_clm.hyps move_trans)
show ?case
proof (rule ccontr)
assume "¬ (ts'',move ts ts'' v ⊨ ( ❙@e (safe e)))"
then have e_def:"ts'',move ts ts'' v ⊨ ❙¬(❙@e (safe e))" by best
hence "ts'',move ts ts'' v ⊨ ❙@e (❙¬ safe e)"
using switch_always_exists switch_unique
by fastforce
then obtain ve where ve_def:
"((move ts ts'' v) =e> ve) ∧ (ts'',ve ⊨ ❙¬ safe e)"
using switch_always_exists by fastforce
hence unsafe:"ts'',ve ⊨ ❙∃ c. ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
then obtain c where c_def:"ts'',ve ⊨ ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩"
by blast
hence c_neq_e:"ts'',ve ⊨❙¬ (c ❙= e)" by blast
obtain d n where d_def: " (ts' ❙─c(d,n) ❙→ ts'')" using cr_clm.hyps by blast
from c_def have "∃v'. (v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq by fastforce
then obtain v' where v'_def:"(v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using d_def backwards_c_res_stab by blast
hence "ts',ve ⊨ ❙¬ safe (e)"
using c_neq_e c_def v'_def somewhere_leq by meson
thus False using cr_clm.IH move_stab ve_def by fastforce
qed
next
case (wd_res ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_wdr wd_res.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis abstract.simps wd_res.hyps move_trans)
show ?case
proof (rule ccontr)
assume "¬ (ts'',move ts ts'' v ⊨ ( ❙@e (safe e)))"
then have e_def:"ts'',move ts ts'' v ⊨ ❙¬(❙@e (safe e))" by best
hence "ts'',move ts ts'' v ⊨ ❙@e (❙¬ safe e)"
using switch_always_exists switch_unique by (fastforce)
then obtain ve where ve_def:
"((move ts ts'' v) =e> ve) ∧ (ts'',ve ⊨ ❙¬ safe e)"
using switch_always_exists by fastforce
hence unsafe:"ts'',ve ⊨ ❙∃ c. ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
then obtain c where c_def:"ts'',ve ⊨ ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
hence c_neq_e:"ts'',ve ⊨❙¬ (c ❙= e)" by blast
obtain d n where n_def:
"(ts' ❙─wdr(d,n) ❙→ ts'')" using wd_res.hyps by blast
from c_def have "∃v'. (v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq by fastforce
then obtain v' where v'_def:"(v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using n_def backwards_wdr_res_stab by blast
hence "ts',ve ⊨ ❙¬ safe (e)"
using c_neq_e c_def v'_def somewhere_leq by meson
thus False using wd_res.IH move_stab ve_def by fastforce
qed
next
case (wd_clm ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_wdc wd_clm.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis abstract.simps wd_clm.hyps move_trans)
show ?case
proof (rule ccontr)
assume "¬ (ts'',move ts ts'' v ⊨ ( ❙@e (safe e)))"
then have e_def:"ts'',move ts ts'' v ⊨ ❙¬(❙@e (safe e))" by best
then obtain ve where ve_def:
"((move ts ts'' v) =e> ve) ∧ (ts'',ve ⊨ ❙¬ safe e)"
using switch_always_exists by fastforce
hence unsafe:"ts'',ve ⊨ ❙∃ c. ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
then obtain c where c_def:"ts'',ve ⊨ ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
hence c_neq_e:"ts'',ve ⊨❙¬ (c ❙= e)" by blast
obtain d where d_def: "(ts' ❙─wdc(d) ❙→ ts'')" using wd_clm.hyps by blast
from c_def have "∃v'. (v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq by fastforce
then obtain v' where v'_def:
"(v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))" by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using d_def backwards_wdc_res_stab by blast
hence "ts',ve ⊨ ❙¬ safe (e)"
using c_neq_e c_def v'_def somewhere_leq by meson
thus False using wd_clm.IH move_stab ve_def by fastforce
qed
next
case (cr_res ts' ts'')
have local_LC:
"ts',move ts ts' v ⊨ ❙∀d.( ❙∃ c. (❙@c (pcc c d)) ❙∨ (❙@d (pcc c d))) ❙→ ❙□r(d) ❙⊥"
using LC cr_res.hyps(1) by blast
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using move_stability_res cr_res.hyps move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis abstract.simps cr_res.hyps move_trans)
show ?case
proof (rule ccontr)
obtain d where d_def: "(ts' ❙─r(d) ❙→ ts'')"
using cr_res.hyps by blast
assume "¬ (ts'',move ts ts'' v ⊨ ( ❙@e (safe e)))"
then have e_def:"ts'',move ts ts'' v ⊨ ❙¬(❙@e (safe e))" by best
hence "ts'',move ts ts'' v ⊨ ❙@e (❙¬ safe e)"
using switch_always_exists switch_unique by fast
then obtain ve where ve_def:
"((move ts ts'' v) =e> ve) ∧ (ts'',ve ⊨ ❙¬ safe e)"
using switch_always_exists by fastforce
hence unsafe:"ts'',ve ⊨ ❙∃ c. ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
then obtain c where c_def:"ts'',ve ⊨ ❙¬(c ❙= e) ❙∧ ❙⟨ re(c) ❙∧ re(e)❙⟩" by blast
hence c_neq_e:"ts'',ve ⊨❙¬(c ❙= e)" by blast
show False
proof (cases "d=e")
case True
hence e_trans:"ts' ❙─r(e) ❙→ ts''" using d_def by simp
from c_def have "ts'',ve ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))" by blast
with backwards_res_act have "ts',v' ⊨ re(c) ❙∧ (re(e) ❙∨ cl(e))"
using c_def backwards_res_stab c_neq_e
by (metis (no_types, lifting) d_def True)
hence "∃v'. (v' ≤ ve) ∧ (ts',v' ⊨ re(c) ❙∧ (re(e) ❙∨ cl(e)))"
using v'_def by blast
hence "ts',ve ⊨❙⟨ re(c) ❙∧ (re(e) ❙∨ cl(e)) ❙⟩"
using somewhere_leq by meson
hence "ts',ve ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩ ❙∨ ❙⟨ re(c) ❙∧ cl(e)❙⟩ "
using hmlsl.somewhere_and_or_distr by metis
then show False
proof
assume assm':"ts',ve ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩"
have "ts',move ts ts' v ⊨ ❙¬ (c ❙= e)" using c_def by blast
thus False using assm' cr_res.IH c_def move_stab ve_def by force
next
assume assm':"ts',ve ⊨ ❙⟨ re(c) ❙∧ cl(e)❙⟩"
hence "ts',ve ⊨ ❙¬ (c ❙=e) ❙∧ ❙⟨ re(c) ❙∧ cl(e)❙⟩" using c_def by force
hence "ts',ve ⊨ pcc c e" by blast
hence "ts',move ts ts' v ⊨ ❙@e (pcc c e)"
using ve_def move_stab switch_unique by fastforce
hence pcc:"ts',move ts ts' v ⊨ (❙@c (pcc c e)) ❙∨ (❙@e (pcc c e))"
by blast
have
"ts',move ts ts' v ⊨(❙∃ c.(❙@c (pcc c e)) ❙∨ (❙@e (pcc c e))) ❙→ ❙□r(e) ❙⊥"
using local_LC e_def by blast
thus "ts'',move ts ts'' v ⊨ ❙⊥" using e_trans pcc by blast
qed
next
case False
then have neq:"d ≠e" .
show False
proof (cases "c=d")
case False
from c_def have "ts'',ve ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))" by blast
with backwards_res_stab have overlap: "ts',v' ⊨ re(c) ❙∧ (re(e))"
using c_def backwards_res_stab c_neq_e False
by (metis (no_types, lifting) d_def neq)
hence unsafe2:"ts',ve ⊨❙¬ safe(e)"
using c_neq_e somewhere_leq v'_def by blast
from cr_res.IH have "ts',move ts ts'' v ⊨ ❙@e (safe(e))"
using move_stab by force
thus False using unsafe2 ve_def by best
next
case True
hence e_trans:"ts' ❙─r(c) ❙→ ts''" using d_def by simp
from c_def have "ts'',ve ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ ve) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))" by blast
with backwards_res_act have "ts',v' ⊨ (re(c) ❙∨ cl(c)) ❙∧ (re(e) )"
using c_def backwards_res_stab c_neq_e
by (metis (no_types, lifting) d_def True)
hence "∃v'. (v' ≤ ve) ∧ (ts',v' ⊨ (re(c) ❙∨ cl(c)) ❙∧ (re(e)))"
using v'_def by blast
hence "ts',ve ⊨❙⟨ (re(c) ❙∨ cl(c)) ❙∧ (re(e) ) ❙⟩"
using somewhere_leq move_stab
by meson
hence "ts',ve ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩ ❙∨ ❙⟨ cl(c) ❙∧ re(e)❙⟩ "
using hmlsl.somewhere_and_or_distr by blast
thus False
proof
assume assm':"ts',ve ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩"
have "ts',ve ⊨ ❙¬ (c ❙= e)" using c_def by blast
thus False using assm' cr_res.IH c_def move_stab ve_def by fastforce
next
assume assm':"ts',ve ⊨ ❙⟨ cl(c) ❙∧ re(e)❙⟩"
hence "ts',ve ⊨ ❙¬ (c ❙=e) ❙∧ ❙⟨ cl(c) ❙∧ re(e)❙⟩" using c_def by blast
hence "ts',ve ⊨❙¬ (c ❙=e) ❙∧ ❙⟨ cl(c) ❙∧ (re(e) ❙∨ cl(e)) ❙⟩" by blast
hence "ts',ve ⊨ pcc e c" by blast
hence "ts',move ts ts' v ⊨ ❙@e (pcc e c)"
using ve_def move_stab switch_unique by fastforce
hence pcc:"ts', move ts ts' v ⊨ (❙@e (pcc e c)) ❙∨ (❙@c (pcc e c))"
by blast
have
"ts',move ts ts' v ⊨(❙∃ d.(❙@d (pcc d c)) ❙∨ (❙@c (pcc d c))) ❙→ ❙□r(c) ❙⊥"
using local_LC move_stab c_def e_def by blast
hence "ts',move ts ts' v ⊨ ❙□r(c) ❙⊥" using pcc by blast
thus "ts'',move ts ts'' v ⊨ ❙⊥" using e_trans by blast
qed
qed
qed
qed
qed
qed
end
end