# Theory Safe_Distance_Reaction

```✐‹creator "Albert Rizaldi" "Fabian Immler›

section ‹Safe Distance with Reaction Time›

theory Safe_Distance_Reaction
imports
Safe_Distance
begin

subsection ‹Normal Safe Distance›

locale safe_distance_normal = safe_distance +
fixes δ :: real
assumes pos_react: "0 < δ"
begin

sublocale ego2: braking_movement a⇩e v⇩e "(ego.q δ)" ..

lemma ego2_s_init: "ego2.s 0 = ego.q δ" unfolding ego2.s_def by auto

definition τ :: "real ⇒ real" where
"τ t = t - δ"

definition τ' :: "real ⇒ real" where
"τ' t = 1"

lemma τ_continuous[continuous_intros]: "continuous_on T τ"
unfolding τ_def by (auto intro: continuous_intros)

lemma isCont_τ[continuous_intros]: "isCont τ x"
using τ_continuous[of UNIV] by (auto simp: continuous_on_eq_continuous_at)

lemma del_has_vector_derivative[derivative_intros]: "(τ has_vector_derivative τ' t) (at t within u)"
by (auto simp: τ_def[abs_def] τ'_def has_vector_derivative_def algebra_simps
intro!: derivative_eq_intros)

lemma del_has_real_derivative[derivative_intros]: "(τ has_real_derivative τ' t) (at t within u)"
using del_has_vector_derivative
by (simp add:has_real_derivative_iff_has_vector_derivative)

lemma delay_image: "τ ` {δ..} = {0..}"
proof (rule subset_antisym, unfold image_def, unfold τ_def)
show "{y. ∃x∈{δ..}. y = x - δ} ⊆ {0..}" by auto
next
show "{0..} ⊆ {y. ∃x∈{δ..}. y = x - δ}"
proof (rule subsetI)
fix a
assume "(a::real) ∈ {0..}"
hence "0 ≤ a" by simp
hence "∃x∈{δ..}. a = x - δ" using bexI[where x = "a + δ"] by auto
thus "a ∈ {y. ∃x∈{δ..}. y = x - δ}" by auto
qed
qed

lemma s_delayed_has_real_derivative[derivative_intros]:
assumes "δ ≤ t"
shows "((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ) * τ' t) (at t within {δ..})"
proof (rule DERIV_image_chain)
from assms have 0: "0 ≤ t - δ" by simp
from ego2.t_stop_nonneg have 1: "v⇩e / a⇩e ≤ 0" unfolding ego2.t_stop_def by simp
from ego2.decel have 2: "a⇩e ≠ 0" by simp
show "(ego2.s has_real_derivative ego2.s' (t - δ)) (at (τ t) within τ ` {δ..})"
using ego2.s_has_real_derivative[OF 0 1 2] sym[OF delay_image]
unfolding τ_def by simp
next
from del_has_real_derivative show "(τ has_real_derivative τ' t) (at t within {δ..})"
by auto
qed

lemma s_delayed_has_real_derivative' [derivative_intros]:
assumes "δ ≤ t"
shows "((ego2.s ∘ τ) has_field_derivative (ego2.s' ∘ τ) t) (at t within {δ..})"
proof -
from s_delayed_has_real_derivative[OF assms] have
"((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ) * τ' t) (at t within {δ..})"
by auto
hence "((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ) * 1) (at t within {δ..})"
using τ'_def[of t] by metis
hence "((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ)) (at t within {δ..})"
by (simp add:algebra_simps)
thus ?thesis unfolding comp_def τ_def by auto
qed

lemma s_delayed_has_vector_derivative' [derivative_intros]:
assumes "δ ≤ t"
shows "((ego2.s ∘ τ) has_vector_derivative (ego2.s' ∘ τ) t) (at t within {δ..})"
using s_delayed_has_real_derivative'[OF assms]
by (simp add:has_real_derivative_iff_has_vector_derivative)

definition u :: "real ⇒ real" where
"u t = (     if t ≤ 0 then s⇩e
else if t ≤ δ then ego.q t
else          (ego2.s ∘ τ) t)"

lemma init_u: "t ≤ 0 ⟹ u t = s⇩e" unfolding u_def by auto

lemma u_delta: "u δ = ego2.s 0"
proof -
have "u δ = ego.q δ" using pos_react unfolding u_def by auto
also have "... = ego2.s 0" unfolding ego2.s_def by auto
finally show "u δ = ego2.s 0" .
qed

lemma q_delta: "ego.q δ = ego2.s 0" using u_delta pos_react unfolding u_def by auto

definition u' :: "real ⇒ real" where
"u' t = (if t ≤ δ then ego.q' t else ego2.s' (t - δ))"

lemma u'_delta: "u' δ = ego2.s' 0"
proof -
have "u' δ = ego.q' δ" unfolding u'_def by auto
also have "... = v⇩e" unfolding ego2.q'_def by simp
also have "... = ego2.p' 0" unfolding ego2.p'_def by simp
also have "... = ego2.s' 0" using ego2.t_stop_nonneg unfolding ego2.s'_def by auto
finally show "u' δ = ego.s' 0" .
qed

lemma q'_delta: "ego.q' δ = ego2.s' 0" using u'_delta unfolding u'_def by auto

lemma u_has_real_derivative[derivative_intros]:
assumes nonneg_t: "t ≥ 0"
shows "(u has_real_derivative u' t) (at t within {0..})"
proof -
from pos_react have "0 ≤ δ" by simp

have temp: "((λt. if t ∈ {0 .. δ} then ego.q t else (ego2.s ∘ τ) t) has_real_derivative
(if t ∈ {0..δ} then ego.q' t else (ego2.s' ∘ τ) t)) (at t within {0..})" (is "(?f1 has_real_derivative ?f2) (?net)")
unfolding u_def[abs_def] u'_def
has_real_derivative_iff_has_vector_derivative
apply (rule has_vector_derivative_If_within_closures[where T = "{δ..}"])
using ‹0 ≤ δ› q_delta q'_delta ego.s_has_vector_derivative[OF assms] ego.decel ego.t_stop_nonneg
s_delayed_has_vector_derivative'[of "t"] τ_def
unfolding comp_def
by (auto simp: assms  max_def insert_absorb
intro!: ego.q_has_vector_derivative)
show ?thesis
unfolding has_vector_derivative_def has_real_derivative_iff_has_vector_derivative
u'_def u_def[abs_def]
proof (rule has_derivative_transform[where f="(λt. if t ∈ {0..δ} then ego.q t else (ego2.s ∘ τ) t)"])
from nonneg_t show " t ∈ {0..}" by auto
next
fix x
assume "(x::real) ∈ {0..}"
hence  "x ≤ δ ⟷ x ∈ {0 .. δ}" by simp
thus  " (if x ≤ 0 then s⇩e else if x ≤ δ then ego.q x else (ego2.s ∘ τ) x) =
(if x ∈ {0..δ} then ego.q x else (ego2.s ∘ τ) x)" using pos_react unfolding ego.q_def by auto
next
from temp have "(?f1 has_vector_derivative ?f2) ?net"
using has_real_derivative_iff_has_vector_derivative by auto
moreover with assms have "t ∈ {0 .. δ} ⟷ t ≤ δ" by auto
ultimately show " ((λt. if t ∈ {0..δ} then ego.q t else (ego2.s ∘ τ) t) has_derivative
(λx. x *⇩R (if t ≤ δ then ego2.q' t else ego2.s' (t - δ)))) (at t within {0..})"
unfolding comp_def τ_def has_vector_derivative_def by auto
qed
qed

definition t_stop :: real where
"t_stop = ego2.t_stop + δ"

lemma t_stop_nonneg: "0 ≤ t_stop"
unfolding t_stop_def
using ego2.t_stop_nonneg pos_react
by auto

lemma t_stop_pos: "0 < t_stop"
unfolding t_stop_def
using ego2.t_stop_nonneg pos_react
by auto

lemma t_stop_zero:
assumes "t_stop ≤ x"
assumes "x ≤ δ"
shows "v⇩e = 0"
using assms unfolding t_stop_def using ego2.t_stop_nonneg pos_react ego2.t_stop_zero by auto

lemma u'_stop_zero: "u' t_stop = 0"
unfolding u'_def t_stop_def ego2.q'_def ego2.s'_def
using ego2.t_stop_nonneg ego2.p'_stop_zero decelerate_ego ego2.t_stop_zero by auto

definition u_max :: real where
"u_max = u (ego2.t_stop + δ)"

lemma u_max_eq: "u_max = ego.q δ - v⇩e⇧2 / a⇩e / 2"
proof (cases "ego2.t_stop = 0")
assume "ego2.t_stop = 0"
hence "v⇩e = 0" using ego2.t_stop_zero by simp
with ‹ego2.t_stop = 0› show "u_max = ego.q δ - v⇩e⇧2 / a⇩e / 2"  unfolding u_max_def u_def using pos_react by auto
next
assume "ego2.t_stop ≠ 0"
hence "u_max = (ego2.s ∘ τ) (ego2.t_stop + δ)"
unfolding u_max_def u_def  using ego2.t_stop_nonneg pos_react by auto
moreover have "... = ego2.s ego2.t_stop" unfolding comp_def τ_def by auto
moreover have "... = ego2.p_max"
unfolding ego2.s_def ego2.p_max_def using ‹ego2.t_stop ≠ 0› ego2.t_stop_nonneg by auto
moreover have "... = ego.q δ - v⇩e⇧2 / a⇩e / 2" using ego2.p_max_eq .
ultimately show ?thesis by auto
qed

lemma u_mono:
assumes "x ≤ y" "y ≤ t_stop"
shows "u x ≤ u y"
proof -
have "y ≤ 0 ∨ (0 < y ∧ y ≤ δ) ∨ δ < y" by auto

moreover
{ assume "y ≤ 0"
with assms have "x ≤ 0" by auto
with ‹y ≤ 0› have "u x ≤ u y" unfolding u_def by auto }

moreover
{ assume "0 < y ∧ y ≤ δ"
with assms have "x ≤ δ" by auto
hence "u x ≤ u y"
proof (cases "x ≤ 0")
assume "x ≤ 0"
with ‹x ≤ δ› and ‹0 < y ∧ y ≤ δ› show "u x ≤ u y"  unfolding u_def using ego.q_min by auto
next
assume "¬ x ≤ 0"
with ‹0 < y ∧ y ≤ δ› and assms show "u x ≤ u y"
unfolding u_def  using ego.q_mono by auto
qed }

moreover
{ assume "δ < y"
have "u x ≤ u y"
proof (cases "δ < x")
assume "δ < x"
with pos_react have "¬ x ≤ 0" by auto
moreover from ‹δ < y› and pos_react have "¬ y ≤ 0" by auto
ultimately show "u x ≤ u y"  unfolding u_def comp_def
using assms ego2.s_mono[of "x - δ" "y - δ"] ‹δ < y› ‹δ < x› by (auto simp:τ_def)
next
assume "¬ δ < x"
hence "x ≤ δ" by simp
hence "u x ≤ ego.q δ" unfolding u_def using pos_react nonneg_vel_ego
by (auto simp add:ego.q_def mult_left_mono)
also have "... = ego2.s (τ δ)" unfolding ego2.s_def unfolding τ_def by auto
also have "... ≤ ego2.s (τ y)" unfolding τ_def using ‹δ < y› by (auto simp add:ego2.s_mono)
also have "... = u y" unfolding u_def using ‹δ < y› pos_react by auto
ultimately show "u x ≤ u y" by auto
qed }

ultimately show "u x ≤ u y" by auto
qed

lemma u_antimono: "x ≤ y ⟹ t_stop ≤ x ⟹ u y ≤ u x"
proof -
assume 1: "x ≤ y"
assume 2: "t_stop ≤ x"
hence "δ ≤ x" unfolding τ_def t_stop_def using pos_react ego2.t_stop_nonneg by auto
with 1 have "δ ≤ y" by auto
from 1 and 2 have 3: "t_stop ≤ y" by auto
show "u y ≤ u x"
proof (cases "x ≠ δ ∧ y ≠ δ")
assume "x ≠ δ ∧ y ≠ δ"
hence "x ≠ δ" and "y ≠ δ" by auto
have "u y ≤ (ego2.s ∘ τ) y" unfolding u_def using ‹δ ≤ y› ‹y ≠ δ› pos_react by auto
also have "... ≤ (ego2.s ∘ τ) x" unfolding comp_def
proof (intro ego2.s_antimono)
show "τ x ≤ τ y" unfolding τ_def using ‹x ≤ y› by auto
next
show "ego2.t_stop ≤ τ x" unfolding τ_def using ‹t_stop ≤ x› by (auto simp: t_stop_def)
qed
also have "... ≤ u x" unfolding u_def using ‹δ ≤ x›‹x ≠ δ› pos_react by auto
ultimately show "u y ≤ u x" by auto
next
assume "¬ (x ≠ δ ∧ y ≠ δ)"
have "x ≠ δ ⟶ y ≠ δ"
proof (rule impI; erule contrapos_pp[where Q="¬ x = δ"])
assume "¬ y ≠ δ"
hence "y = δ" by simp
with ‹t_stop ≤ y› have "ego2.t_stop = 0" unfolding t_stop_def
using ego2.t_stop_nonneg by auto
with ‹t_stop ≤ x› have "x = δ" unfolding t_stop_def using ‹x ≤ y› ‹y = δ› by auto
thus "¬ x ≠ δ" by auto
qed
with ‹¬ (x ≠ δ ∧ y ≠ δ)› have "(x = δ ∧ y = δ) ∨ (x = δ)" by auto

moreover
{ assume "x = δ ∧ y = δ"
hence "x = δ" and "y = δ" by auto
hence "u y ≤ ego.q δ" unfolding u_def using pos_react by auto
also have "... ≤ u x" unfolding u_def using ‹x = δ› pos_react by auto
ultimately have "u y ≤ u x" by auto }

moreover
{ assume "x = δ"
hence "ego2.t_stop = 0" using ‹t_stop ≤ x› ego2.t_stop_nonneg by (auto simp:t_stop_def)
hence "v⇩e = 0" by (rule ego2.t_stop_zero)
hence "u y ≤ ego.q δ"
using pos_react ‹x = δ› ‹x ≤ y› ‹v⇩e = 0›
unfolding u_def comp_def τ_def ego2.s_def ego2.p_def ego2.p_max_def ego2.t_stop_def
by auto
also have "... ≤ u x" using ‹x = δ› pos_react unfolding u_def by auto
ultimately have "u y ≤ u x" by auto }

ultimately show ?thesis by auto
qed
qed

lemma u_max: "u x ≤ u_max"
unfolding u_max_def using t_stop_def
by (cases "x ≤ t_stop") (auto intro: u_mono u_antimono)

lemma u_eq_u_stop: "NO_MATCH t_stop x ⟹ x ≥ t_stop ⟹ u x = u_max"
proof -
assume "t_stop ≤ x"
with t_stop_pos have "0 < x" by auto
from ‹t_stop ≤ x› have "δ ≤ x" unfolding t_stop_def using ego2.t_stop_nonneg by auto
show  "u x = u_max"
proof (cases "x ≤ δ")
assume "x ≤ δ"
with ‹t_stop ≤ x› have "v⇩e = 0" by (rule t_stop_zero)
also have "x = δ" using ‹x ≤ δ› and ‹δ ≤ x› by auto
ultimately have "u x = ego.q δ" unfolding u_def using pos_react by auto
also have "... = u_max" unfolding u_max_eq using ‹v⇩e = 0› by auto
ultimately show "u x = u_max" by simp
next
assume "¬ x ≤ δ"
hence "δ < x" by auto
hence "u x = (ego2.s ∘ τ) x" unfolding u_def using pos_react by auto
also have "... = ego2.s ego2.t_stop"
proof (unfold comp_def; unfold τ_def; intro order.antisym)
have "x - δ ≥ ego2.t_stop" using ‹t_stop ≤ x› unfolding t_stop_def by auto
thus "ego2.s (x - δ) ≤ ego2.s ego2.t_stop" by (rule ego2.s_antimono) simp
next
have "x - δ ≥ ego2.t_stop" using ‹t_stop ≤ x› unfolding t_stop_def by auto
thus "ego2.s ego2.t_stop ≤ ego2.s (x - δ)" using ego2.t_stop_nonneg by (rule ego2.s_mono)
qed
also have "... = u_max" unfolding u_max_eq ego2.s_t_stop ego2.p_max_eq by auto
ultimately show "u x = u_max" by auto
qed
qed

lemma at_least_delta:
assumes "x ≤ δ"
assumes "t_stop ≤ x"
shows "ego.q x = ego2.s (x - δ)"
using assms ego2.t_stop_nonneg
unfolding t_stop_def ego2.s_def less_eq_real_def by auto

lemma continuous_on_u[continuous_intros]: "continuous_on T u"
unfolding u_def[abs_def]
using t_stop_nonneg pos_react at_least_delta
proof (intro continuous_on_subset[where t=T and s = "{..0} ∪ ({0..δ} ∪ ({δ .. t_stop} ∪ {t_stop ..}))"] continuous_on_If continuous_intros)
fix x
assume " ¬ x ≤ δ"
assume "x ∈ {0..δ}"
hence "0 ≤ x" and "x ≤ δ" by auto
thus "ego.q x = (ego2.s ∘ τ) x"
unfolding comp_def τ_def ego2.s_def
using ‹¬ x ≤ δ› by auto
next
fix x
assume "x ∈ {δ..t_stop} ∪ {t_stop..}"
hence "δ ≤ x" unfolding t_stop_def using pos_react ego.t_stop_nonneg by auto
also assume "x ≤ δ"
ultimately have "x = δ" by auto
thus "ego.q x = (ego2.s ∘ τ) x" unfolding comp_def τ_def ego2.s_def by auto
next
fix t::real
assume "t ∈ {.. 0}"
hence "t ≤ 0" by auto
also assume "¬ t ≤ 0"
ultimately have "t = 0" by auto
hence "s⇩e = ego.q t" unfolding ego.q_def by auto
with pos_react ‹t = 0› show "s⇩e = (if t ≤ δ then ego.q t else (ego2.s ∘ τ) t)" by auto
next
fix t::real
assume "t ∈ {0..δ} ∪ ({δ..t_stop} ∪ {t_stop..})"
hence "0 ≤ t" using pos_react ego2.t_stop_nonneg by (auto simp: t_stop_def)
also assume "t ≤ 0"
ultimately have "t = 0" by auto
hence " s⇩e = (if t ≤ δ then ego.q t else (ego2.s ∘ τ) t)" using pos_react ego.init_q by auto
thus "s⇩e = (if t ≤ δ then ego.q t else (ego2.s ∘ τ) t)" by auto
next
show "T ⊆ {..0} ∪ ({0..δ} ∪ ({δ..t_stop} ∪ {t_stop..}))" by auto
qed

lemma isCont_u[continuous_intros]: "isCont u x"
using continuous_on_u[of UNIV]
by (auto simp:continuous_on_eq_continuous_at)

definition collision_react :: "real set ⇒ bool" where
"collision_react time_set ≡ (∃t∈time_set. u t = other.s t )"

abbreviation no_collision_react :: "real set ⇒ bool" where
"no_collision_react time_set ≡ ¬ collision_react time_set"

lemma no_collision_reactI:
assumes "⋀t. t ∈ S ⟹ u t ≠ other.s t"
shows "no_collision_react S"
using assms
unfolding collision_react_def
by blast

lemma no_collision_union:
assumes "no_collision_react S"
assumes "no_collision_react T"
shows "no_collision_react (S ∪ T)"
using assms
unfolding collision_react_def
by auto

lemma collision_trim_subset:
assumes "collision_react S"
assumes "no_collision_react T"
assumes "T ⊆ S"
shows "collision_react (S - T)"
using assms
unfolding collision_react_def by auto

theorem cond_1r : "u_max < s⇩o ⟹ no_collision_react {0..}"
proof (rule no_collision_reactI, simp)
fix t :: real
assume "0 ≤ t"
have "u t ≤ u_max" by (rule u_max)
also assume "... < s⇩o"
also have "... = other.s 0"
by (simp add: other.init_s)
also have "... ≤ other.s t"
using ‹0 ≤ t› hyps
by (intro other.s_mono) auto
finally show "u t ≠ other.s t"
by simp
qed

definition safe_distance_1r :: real where
"safe_distance_1r = v⇩e * δ - v⇩e⇧2 / a⇩e / 2"

lemma sd_1r_eq: "(s⇩o - s⇩e > safe_distance_1r) = (u_max < s⇩o)"
proof -
have "(s⇩o - s⇩e > safe_distance_1r) = (s⇩o - s⇩e > v⇩e * δ - v⇩e⇧2 / a⇩e / 2)" unfolding safe_distance_1r_def by auto
moreover have "... = (s⇩e + v⇩e * δ - v⇩e⇧2 / a⇩e / 2 < s⇩o)" by auto
ultimately show ?thesis using u_max_eq ego.q_def by auto
qed

lemma sd_1r_correct:
assumes "s⇩o - s⇩e > safe_distance_1r"
shows "no_collision_react {0..}"
proof -
from assms have "u_max < s⇩o" using sd_1r_eq by auto
thus ?thesis by (rule cond_1r)
qed

lemma u_other_strict_ivt:
assumes "u t > other.s t"
shows "collision_react {0..<t}"
proof cases
assume "0 ≤ t"
with assms in_front
have "∃x≥0. x ≤ t ∧ other.s x - u x = 0"
by (intro IVT2) (auto simp: init_u other.init_s continuous_diff isCont_u other.isCont_s)
then show ?thesis
using assms
by (auto simp add: algebra_simps collision_react_def Bex_def order.order_iff_strict)
qed(insert assms hyps, auto simp: collision_react_def init_u other.init_s)

lemma collision_react_subset: "collision_react s ⟹ s ⊆ t ⟹ collision_react t"
by (auto simp:collision_react_def)

lemma u_other_ivt:
assumes "u t ≥ other.s t"
shows "collision_react {0 .. t}"
proof cases
assume "u t > other.s t"
from u_other_strict_ivt[OF this]
show ?thesis
by (rule collision_react_subset) auto
qed (insert hyps assms; cases "t ≥ 0"; force simp: collision_react_def init_u other.init_s)

theorem cond_2r:
assumes "u_max ≥ other.s_stop"
shows "collision_react {0 ..}"
using assms
apply(intro collision_react_subset[where t="{0..}" and s ="{0 .. max t_stop other.t_stop}"])
apply(intro u_other_ivt[where t ="max t_stop other.t_stop"])
apply(auto simp: u_eq_u_stop other.s_eq_s_stop)
done

definition ego_other2 :: "real ⇒ real" where
"ego_other2 t = other.s t - u t"

lemma continuous_on_ego_other2[continuous_intros]: "continuous_on T ego_other2"
unfolding ego_other2_def[abs_def]
by (intro continuous_intros)

lemma isCont_ego_other2[continuous_intros]: "isCont ego_other2 x"
using continuous_on_ego_other2[of UNIV]
by (auto simp: continuous_on_eq_continuous_at)

definition ego_other2' :: "real ⇒ real" where
"ego_other2' t  = other.s' t - u' t"

lemma ego_other2_has_real_derivative[derivative_intros]:
assumes "0 ≤ t"
shows "(ego_other2 has_real_derivative ego_other2' t) (at t within {0..})"
using assms other.t_stop_nonneg decelerate_other
unfolding other.t_stop_def
by (auto simp: ego_other2_def[abs_def] ego_other2'_def  algebra_simps
intro!: derivative_eq_intros)

theorem cond_3r_1:
assumes "u δ ≥ other.s δ"
shows "collision_react {0 .. δ}"
proof (unfold collision_react_def)
have 1: "∃t≥0. t ≤ δ ∧ ego_other2 t = 0"
proof (intro IVT2)
show "ego_other2 δ ≤ 0" unfolding ego_other2_def using assms by auto
next
show "0 ≤ ego_other2 0" unfolding ego_other2_def
using other.init_s[of 0] init_u[of 0] in_front by auto
next
show "0 ≤ δ" using pos_react by auto
next
show "∀t. 0 ≤ t ∧ t ≤ δ ⟶ isCont ego_other2 t"
using isCont_ego_other2 by auto
qed
then obtain t where "0 ≤ t ∧ t ≤ δ ∧ ego_other2 t = 0" by auto
hence "t ∈ {0 .. δ}" and "u t = other.s t" unfolding ego_other2_def by auto
thus "∃t∈{0..δ}. u t = other.s t" by (intro bexI)
qed

definition distance0 :: real where
"distance0 =  v⇩e * δ - v⇩o * δ - a⇩o * δ⇧2 / 2"

definition distance0_2 :: real where
"distance0_2 = v⇩e * δ + 1 / 2 * v⇩o⇧2 / a⇩o"

theorem cond_3r_1':
assumes "s⇩o - s⇩e ≤ distance0"
assumes "δ ≤ other.t_stop"
shows "collision_react {0 .. δ}"
proof -
from assms have "u δ ≥ other.s δ" unfolding distance0_def other.s_def
other.p_def u_def ego.q_def using pos_react by auto
thus ?thesis using cond_3r_1 by auto
qed

theorem distance0_2_eq:
assumes "δ > other.t_stop"
shows "(u δ < other.s δ) = (s⇩o - s⇩e > distance0_2)"
proof -
from assms have "(u δ < other.s δ) = (ego.q δ < other.p_max)"
using u_def other.s_def pos_react by auto
also have "... = (s⇩e + v⇩e * δ < s⇩o + v⇩o * (- v⇩o / a⇩o) + 1 / 2 * a⇩o * (- v⇩o / a⇩o)⇧2)"
using ego.q_def other.p_max_def other.p_def other.t_stop_def by auto
also have "... = (v⇩e * δ - v⇩o * (- v⇩o / a⇩o) - 1 / 2 * a⇩o * (- v⇩o / a⇩o)⇧2 < s⇩o - s⇩e)" by linarith
also have "... = (v⇩e * δ + v⇩o⇧2 / a⇩o - 1 / 2 * v⇩o⇧2 / a⇩o < s⇩o - s⇩e)"
using other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
also have "... = (v⇩e * δ + 1 / 2 * v⇩o⇧2 / a⇩o < s⇩o - s⇩e)" by linarith
thus ?thesis using distance0_2_def by (simp add: calculation)
qed

theorem cond_3r_1'_2:
assumes "s⇩o - s⇩e ≤ distance0_2"
assumes "δ > other.t_stop"
shows "collision_react {0 .. δ}"
proof -
from assms distance0_2_eq have "u δ ≥ other.s δ" unfolding distance0_def other.s_def
other.p_def u_def ego.q_def using pos_react by auto
thus ?thesis using cond_3r_1 by auto
qed

definition safe_distance_3r :: real where
"safe_distance_3r = v⇩e * δ - v⇩e⇧2 / 2 / a⇩e - v⇩o * δ - 1/2 * a⇩o * δ⇧2"

lemma distance0_at_most_sd3r:
"distance0 ≤ safe_distance_3r"
unfolding distance0_def safe_distance_3r_def using nonneg_vel_ego decelerate_ego
by (auto simp add:field_simps)

definition safe_distance_4r :: real where
"safe_distance_4r = (v⇩o + a⇩o * δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e) - v⇩o * δ - 1/2 * a⇩o * δ⇧2 + v⇩e * δ"

lemma distance0_at_most_sd4r:
assumes "a⇩o > a⇩e"
shows "distance0 ≤ safe_distance_4r"
proof -
from assms have "a⇩o ≥ a⇩e" by auto
have "0 ≤ (v⇩o + a⇩o * δ - v⇩e)⇧2 / (2 * a⇩o - 2 * a⇩e)"
by (rule divide_nonneg_nonneg) (auto simp add:assms ‹a⇩e ≤ a⇩o›)
thus ?thesis unfolding distance0_def safe_distance_4r_def
by auto
qed

definition safe_distance_2r :: real where
"safe_distance_2r = v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o"

lemma vo_start_geq_ve:
assumes "δ ≤ other.t_stop"
assumes "other.s' δ ≥ v⇩e"
shows "u δ < other.s δ"
proof -
from assms have "v⇩e ≤ v⇩o + a⇩o * δ" unfolding other.s'_def other.p'_def by auto
with  mult_right_mono[OF this, of "δ"] have "v⇩e * δ ≤ v⇩o * δ + a⇩o * δ⇧2" (is "?l0 ≤ ?r0")
using pos_react by (auto simp add:field_simps power_def)
hence "s⇩e + ?l0 ≤ s⇩e + ?r0" by auto
also have "... < s⇩o + ?r0" using in_front by auto
also have "... < s⇩o + v⇩o * δ + a⇩o * δ⇧2 / 2" using decelerate_other pos_react by auto
finally show ?thesis using pos_react assms(1)
unfolding u_def ego.q_def other.s_def other.t_stop_def other.p_def by auto
qed

theorem so_star_stop_leq_se_stop:
assumes "δ ≤ other.t_stop"
assumes "other.s' δ < v⇩e"
assumes "¬ (a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
shows "0 ≤ - v⇩e⇧2 / a⇩e / 2 + (v⇩o + a⇩o * δ)⇧2 / a⇩o / 2"
proof -
consider "v⇩e - a⇩e / a⇩o * other.s' δ ≥ 0" | "¬ (v⇩e - a⇩e / a⇩o * other.s' δ ≥ 0)" by auto
thus ?thesis
proof (cases)
case 1
hence "v⇩e - a⇩e / a⇩o * (v⇩o + a⇩o * δ) ≥ 0" unfolding other.s'_def other.p'_def
by (auto simp add:assms(1))
hence "v⇩e - a⇩e / a⇩o * v⇩o - a⇩e * δ ≥ 0" (is "?l0 ≥ 0") using decelerate_other
by (auto simp add:field_simps)
hence "?l0 / a⇩e ≤ 0" using divide_right_mono_neg[OF ‹?l0 ≥ 0›] decelerate_ego by auto
hence "0 ≥ v⇩e / a⇩e - v⇩o / a⇩o - δ" using decelerate_ego by (auto simp add:field_simps)
hence *: "- v⇩e / a⇩e ≥ - (v⇩o + a⇩o * δ) / a⇩o" using decelerate_other by (auto simp add:field_simps)
from assms have **: "v⇩o + a⇩o * δ ≤ v⇩e" unfolding other.s'_def other.p'_def by auto
have vo_star_nneg: "v⇩o + a⇩o * δ ≥ 0"
proof -
from assms(1) have "- v⇩o ≤ a⇩o * δ" unfolding other.t_stop_def using decelerate_other
by (auto simp add:field_simps)
thus ?thesis by auto
qed
from mult_mono[OF * ** _ ‹0 ≤ v⇩o + a⇩o * δ›]
have "- (v⇩o + a⇩o * δ) / a⇩o * (v⇩o + a⇩o * δ) ≤ - v⇩e / a⇩e * v⇩e" using nonneg_vel_ego decelerate_ego
by (auto simp add:field_simps)
hence "- (v⇩o + a⇩o * δ)⇧2 / a⇩o ≤ - v⇩e⇧2 / a⇩e " by (auto simp add: field_simps power_def)
thus ?thesis by (auto simp add:field_simps)
next
case 2
with assms have "a⇩o ≤ a⇩e" by auto
from assms(2) have "(v⇩o + a⇩o * δ) ≤ v⇩e" unfolding other.s'_def using assms unfolding other.p'_def
by auto
have vo_star_nneg: "v⇩o + a⇩o * δ ≥ 0"
proof -
from assms(1) have "- v⇩o ≤ a⇩o * δ" unfolding other.t_stop_def using decelerate_other
by (auto simp add:field_simps)
thus ?thesis by auto
qed
with mult_mono[OF ‹v⇩o + a⇩o * δ ≤ v⇩e› ‹v⇩o + a⇩o * δ ≤ v⇩e›] have *: "(v⇩o + a⇩o * δ)⇧2 ≤ v⇩e⇧2"
using nonneg_vel_ego by (auto simp add:power_def)
from ‹a⇩o ≤ a⇩e› have "- 1 /a⇩o ≤ - 1 / a⇩e" using decelerate_ego decelerate_other
by (auto simp add:field_simps)
from mult_mono[OF * this] have "(v⇩o + a⇩o * δ)⇧2 * (- 1 / a⇩o) ≤ v⇩e⇧2 * (- 1 / a⇩e)"
using nonneg_vel_ego decelerate_other by (auto simp add:field_simps)
then show ?thesis by auto
qed
qed

theorem distance0_at_most_distance2r:
assumes "δ ≤ other.t_stop"
assumes "other.s' δ < v⇩e"
assumes "¬ (a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
shows "distance0 ≤ safe_distance_2r"
proof -
from so_star_stop_leq_se_stop[OF assms] have " 0 ≤ - v⇩e⇧2 / a⇩e / 2 + (v⇩o + a⇩o * δ)⇧2 / a⇩o / 2 " (is "0 ≤ ?term")
by auto
have "safe_distance_2r = v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o" unfolding safe_distance_2r_def by auto
also have "... = v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + (v⇩o + a⇩o * δ)⇧2 / 2 / a⇩o - v⇩o * δ - a⇩o * δ⇧2 / 2"
using decelerate_other by (auto simp add:field_simps power_def)
also have "... = v⇩e * δ - v⇩o * δ - a⇩o * δ⇧2 / 2 + ?term" (is "_ = ?left + ?term")
by (auto simp add:field_simps)
finally have "safe_distance_2r = distance0 + ?term" unfolding distance0_def by auto
with ‹0 ≤ ?term› show "distance0 ≤ safe_distance_2r" by auto
qed

theorem dist0_sd2r_1:
assumes "δ ≤ other.t_stop"
assumes "¬ (a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
assumes "s⇩o - s⇩e > safe_distance_2r"
shows "s⇩o - s⇩e > distance0"
proof (cases "other.s' δ ≥ v⇩e")
assume "v⇩e ≤ other.s' δ"
from vo_start_geq_ve[OF assms(1) this] have "u δ < other.s δ" by auto
thus ?thesis unfolding distance0_def u_def using pos_react assms(1) unfolding ego.q_def
other.s_def other.p_def by auto
next
assume "¬ v⇩e ≤ other.s' δ"
hence "v⇩e > other.s' δ" by auto
from distance0_at_most_distance2r[OF assms(1) this assms(2)] have "distance0 ≤ safe_distance_2r"
by auto
with assms(3) show ?thesis by auto
qed

theorem sd2r_eq:
assumes "δ > other.t_stop"
shows "(u_max < other.s δ) = (s⇩o - s⇩e > safe_distance_2r)"
proof -
from assms have "(u_max < other.s δ) = (ego2.s (- v⇩e / a⇩e) < other.p_max)"
using u_max_def ego2.t_stop_def u_def other.s_def τ_def pos_react ego2.p_max_eq ego2.s_t_stop u_max_eq by auto
also have "... = (s⇩e + v⇩e * δ + v⇩e * (- v⇩e / a⇩e) + 1 / 2 * a⇩e * (- v⇩e / a⇩e)⇧2 < s⇩o + v⇩o * (- v⇩o / a⇩o) + 1 / 2 * a⇩o * (- v⇩o / a⇩o)⇧2)"
using ego2.s_def ego2.p_def ego.q_def other.p_max_def other.p_def other.t_stop_def ego2.p_max_def ego2.s_t_stop ego2.t_stop_def by auto
also have "... = (v⇩e * δ + v⇩e * (- v⇩e / a⇩e) + 1 / 2 * a⇩e * (- v⇩e / a⇩e)⇧2 - v⇩o * (- v⇩o / a⇩o) - 1 / 2 * a⇩o * (- v⇩o / a⇩o)⇧2 < s⇩o  - s⇩e)" by linarith
also have "... = (v⇩e * δ - v⇩e⇧2 / a⇩e + 1 / 2 * v⇩e⇧2 / a⇩e + v⇩o⇧2 / a⇩o - 1 / 2 * v⇩o⇧2 / a⇩o < s⇩o  - s⇩e)"
using ego2.p_def ego2.p_max_def ego2.p_max_eq ego2.t_stop_def other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
also have "... = (v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o  < s⇩o - s⇩e)" by linarith
thus ?thesis using distance0_2_def by (simp add: calculation safe_distance_2r_def)
qed

theorem dist0_sd2r_2:
assumes "δ > - v⇩o / a⇩o"
assumes "s⇩o - s⇩e > safe_distance_2r"
shows "s⇩o - s⇩e > distance0_2"
proof -
have "- v⇩e⇧2 / 2 / a⇩e ≥ 0" using zero_le_power2 hyps(3) divide_nonneg_neg by (auto simp add:field_simps)
hence "v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o ≥ v⇩e * δ + v⇩o⇧2 / 2 / a⇩o" by simp
hence "safe_distance_2r ≥ distance0_2" using safe_distance_2r_def distance0_2_def by auto
thus ?thesis using assms(2) by linarith
qed
end

subsection ‹Safe Distance Delta›

locale safe_distance_no_collsion_delta = safe_distance_normal +
assumes no_collision_delta: "u δ < other.s δ"
begin

sublocale delayed_safe_distance: safe_distance a⇩e v⇩e "ego.q δ" a⇩o "other.s' δ" "other.s δ"
proof (unfold_locales)
from nonneg_vel_ego show "0 ≤ v⇩e" by auto
next
from nonneg_vel_other show "0 ≤ other.s' δ" unfolding other.s'_def other.p'_def other.t_stop_def
using decelerate_other by (auto simp add: field_split_simps)
next
from decelerate_ego show "a⇩e < 0" by auto
next
from decelerate_other show "a⇩o < 0" by auto
next
from no_collision_delta show "ego.q δ < other.s δ" unfolding u_def using pos_react by auto
qed

lemma no_collision_react_initially_strict:
assumes "s⇩o ≤ u_max"
assumes "u_max < other.s_stop"
shows "no_collision_react {0 <..< δ}"
proof (rule no_collision_reactI)
fix t::real
assume "t ∈ {0 <..< δ}"
show "u t ≠ other.s t"
proof (rule ccontr)
assume "¬ u t ≠ other.s t"
hence "ego_other2 t = 0" unfolding ego_other2_def by auto
from ‹t ∈ {0 <..< δ}› have "ego_other2 t = other.s t - ego.q t"
unfolding ego_other2_def u_def using ego.init_q by auto
have "δ ≤ other.t_stop ∨ other.t_stop < δ" by auto

moreover
{ assume le_t_stop: "δ ≤ other.t_stop"
with ‹ego_other2 t = other.s t - ego.q t› have "ego_other2 t = other.p t - ego.q t"
unfolding other.s_def using ‹t ∈ {0 <..< δ}› by auto
with ‹ego_other2 t = 0› have "other.p t - ego.q t = 0" by auto
hence eq: "(s⇩o- s⇩e) + (v⇩o - v⇩e) * t + (1/2 * a⇩o) * t⇧2 = 0"
unfolding other.p_def ego.q_def by (auto simp: algebra_simps)
define p where "p ≡ λx. (1/2 * a⇩o) * x⇧2 + (v⇩o - v⇩e) * x + (s⇩o - s⇩e)"
have "0 < 1/2 * a⇩o"
proof (intro p_convex[where p=p and b="v⇩o - v⇩e" and c="s⇩o - s⇩e"])
show "0 < t" using ‹t ∈ {0 <..< δ}› by auto
next
show "t < δ" using  ‹t ∈ {0 <..< δ}› by auto
next
show "p t < p 0" unfolding p_def using eq in_front by (auto simp: algebra_simps)
next
from eq have "p t = 0" unfolding p_def by auto
also have "... < p δ"  using no_collision_delta pos_react le_t_stop
unfolding p_def u_def other.s_def ego.q_def other.p_def by (auto simp:algebra_simps)
finally have "p t < p δ" by simp
thus "p t ≤ p δ" by auto
next
show "p = (λx. 1 / 2 * a⇩o * x⇧2 + (v⇩o - v⇩e) * x + (s⇩o - s⇩e))" unfolding p_def
by (rule refl)
qed
hence "0 < a⇩o" by auto
with decelerate_other have False by simp }

moreover
{ assume gt_t_stop: "δ > other.t_stop"
have t_lt_t_stop: "t < other.t_stop"
proof (rule ccontr)
assume "¬ t < other.t_stop"
hence "other.t_stop ≤ t" by simp
from ‹ego_other2 t = 0› have "ego.q t = other.p_max"
unfolding ego_other2_def u_def other.s_def comp_def τ_def other.p_max_def
using ‹t ∈ {0 <..< δ}› ‹other.t_stop ≤ t› gt_t_stop by (auto split:if_splits)
have "ego.q t = u t" unfolding u_def using ‹t ∈ {0 <..< δ}› by auto
also have "... ≤ u_max" using u_max by auto
also have "... < other.p_max" using assms(2) other.s_t_stop by auto
finally have "ego.q t < other.p_max" by auto
with ‹ego.q t = other.p_max› show False by auto
qed

with ‹ego_other2 t = other.s t - ego.q t› have "ego_other2 t = other.p t - ego.q t"
unfolding other.s_def using ‹t ∈ {0 <..< δ}› by auto
with ‹ego_other2 t = 0› have "other.p t - ego.q t = 0" by auto
hence eq: "(s⇩o- s⇩e) + (v⇩o - v⇩e) * t + (1/2 * a⇩o) * t⇧2 = 0"
unfolding other.p_def ego.q_def by (auto simp: algebra_simps)
define p where "p ≡ λx. (1/2 * a⇩o) * x⇧2 + (v⇩o - v⇩e) * x + (s⇩o - s⇩e)"
have "0 < 1/2 * a⇩o"
proof (intro p_convex[where p=p and b="v⇩o - v⇩e" and c="s⇩o - s⇩e"])
show "0 < t" using ‹t ∈ {0 <..< δ}› by auto
next
show "t < other.t_stop" using t_lt_t_stop by auto
next
show "p t < p 0" unfolding p_def using eq in_front by (auto simp: algebra_simps)
next
from eq have zero: "p t = 0" unfolding p_def by auto
have eq: "p other.t_stop = ego_other2 other.t_stop"
unfolding ego_other2_def other.s_t_stop u_def ego.q_def
other.s_def other.p_def p_def
using ‹δ > other.t_stop› other.t_stop_nonneg other.t_stop_def
by (auto simp: diff_divide_distrib left_diff_distrib')
have "u other.t_stop ≤ u_max" using u_max by auto
also have "... < other.s_stop" using assms by auto
finally have "0 ≤ other.s_stop - u other.t_stop" by auto
hence "0 ≤ ego_other2 other.t_stop" unfolding ego_other2_def by auto
hence "0 ≤ p other.t_stop" using eq by auto
with zero show "p t ≤ p other.t_stop" by auto
next
show "p = (λx. 1 / 2 * a⇩o * x⇧2 + (v⇩o - v⇩e) * x + (s⇩o - s⇩e))"
unfolding p_def by (rule refl)
qed
hence False using decelerate_other by auto }

ultimately show False by auto
qed
qed

lemma no_collision_react_initially:
assumes "s⇩o ≤ u_max"
assumes "u_max < other.s_stop"
shows "no_collision_react {0 .. δ}"
proof -
have "no_collision_react {0 <..< δ}" by (rule no_collision_react_initially_strict[OF assms])
have "u 0 ≠ other.s 0" using init_u other.init_s in_front by auto
hence "no_collision_react {0}" unfolding collision_react_def by auto
with ‹no_collision_react {0 <..< δ}› have "no_collision_react ({0} ∪ {0 <..< δ})"
using no_collision_union[of "{0}" "{0 <..< δ}"] by auto
moreover have "{0} ∪ {0 <..< δ} = {0 ..< δ}" using pos_react by auto
ultimately have "no_collision_react {0 ..< δ}" by auto

have "u δ ≠ other.s δ" using no_collision_delta by auto
hence "no_collision_react {δ}" unfolding collision_react_def by auto
with ‹no_collision_react {0 ..< δ}› have "no_collision_react ({δ} ∪ {0 ..< δ})"
using no_collision_union[of "{δ}" "{0 ..< δ}"] by auto
moreover have "{δ} ∪ {0 ..< δ} = {0 .. δ}" using pos_react by auto
ultimately show "no_collision_react {0 .. δ}" by auto
qed

lemma collision_after_delta:
assumes "s⇩o ≤ u_max"
assumes "u_max < other.s_stop"
shows "collision_react {0 ..} ⟷ collision_react {δ..}"
proof
assume "collision_react {0 ..}"
have "no_collision_react {0 .. δ}" by (rule no_collision_react_initially[OF assms])
with ‹collision_react {0..}› have "collision_react ({0..} - {0 .. δ})"
using pos_react by (auto intro: collision_trim_subset)

moreover have "{0..} - {0 .. δ} = {δ <..}" using pos_react by auto
ultimately have "collision_react {δ <..}" by auto
thus "collision_react {δ ..}" by (auto intro:collision_react_subset)
next
assume "collision_react {δ..}"
moreover have "{δ..} ⊆ {0 ..}" using pos_react by auto
ultimately show "collision_react {0 ..}" by (rule collision_react_subset)
qed

lemma collision_react_strict:
assumes "s⇩o ≤ u_max"
assumes "u_max < other.s_stop"
shows "collision_react {δ ..} ⟷ collision_react {δ <..}"
proof
assume asm: "collision_react {δ ..}"
have "no_collision_react {δ}" using no_collision_delta unfolding collision_react_def by auto
moreover have "{δ <..} ⊆ {δ ..}" by auto
ultimately have "collision_react ({δ ..} - {δ})" using asm collision_trim_subset by simp
moreover have "{δ <..} = {δ ..} - {δ}" by auto
ultimately show "collision_react {δ <..}" by auto
next
assume "collision_react {δ <..}"
thus "collision_react {δ ..}"
using collision_react_subset[where t="{δ ..}" and s="{δ <..}"] by fastforce
qed

lemma delayed_other_s_stop_eq: "delayed_safe_distance.other.s_stop = other.s_stop"
proof (unfold other.s_t_stop; unfold delayed_safe_distance.other.s_t_stop; unfold movement.p_max_eq)
have "δ ≤ other.t_stop ∨ other.t_stop < δ" by auto

moreover
{ assume "δ ≤ other.t_stop"
hence "other.s δ - (other.s' δ)⇧2 / a⇩o / 2 = s⇩o - v⇩o⇧2 / a⇩o / 2"
unfolding other.s_def other.s'_def
using  pos_react decelerate_other
by (auto simp add: other.p_def other.p'_def power2_eq_square field_split_simps) }

moreover
{ assume "other.t_stop < δ"
hence "other.s δ - (other.s' δ)⇧2 / a⇩o / 2 = s⇩o - v⇩o⇧2 / a⇩o / 2"
unfolding other.s_def other.s'_def other.p_max_eq
using pos_react decelerate_other
by (auto) }

ultimately show "other.s δ - (other.s' δ)⇧2 / a⇩o / 2 = s⇩o - v⇩o⇧2 / a⇩o / 2" by auto
qed

lemma delayed_cond3':
assumes "other.s δ ≤ u_max"
assumes "u_max < other.s_stop"
shows "delayed_safe_distance.collision {0 ..} ⟷
(a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ other.s δ - ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
proof (rule delayed_safe_distance.cond_3')
have "other.s δ ≤ u_max" using ‹other.s δ ≤ u_max› .
also have "... = ego2.s_stop" unfolding u_max_eq ego2.s_t_stop ego2.p_max_eq by (rule refl)
finally show "other.s δ ≤ ego2.s_stop" by auto
next
have "ego2.s_stop = u_max" unfolding ego2.s_t_stop ego2.p_max_eq u_max_eq by (rule refl)
also have "... < other.s_stop" using assms by auto
also have "... ≤ delayed_safe_distance.other.s_stop" using delayed_other_s_stop_eq by auto
finally show "ego2.s_stop < delayed_safe_distance.other.s_stop" by auto
qed

lemma delayed_other_t_stop_eq:
assumes "δ ≤ other.t_stop"
shows "delayed_safe_distance.other.t_stop + δ = other.t_stop"
using assms decelerate_other
unfolding delayed_safe_distance.other.t_stop_def other.t_stop_def other.s'_def
movement.t_stop_def other.p'_def
by (auto simp add: field_split_simps)

lemma delayed_other_s_eq:
assumes "0 ≤ t"
shows "delayed_safe_distance.other.s t = other.s (t + δ)"
proof (cases "δ ≤ other.t_stop")
assume 1: "δ ≤ other.t_stop"
have "t + δ ≤ other.t_stop ∨ other.t_stop < t + δ" by auto
moreover
{ assume "t + δ ≤ other.t_stop"
hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p t"
using delayed_other_t_stop_eq [OF 1] assms
unfolding delayed_safe_distance.other.s_def by auto

also have "... = other.p (t + δ)"
unfolding movement.p_def other.s_def other.s'_def other.p'_def
using pos_react 1
by (auto simp add: power2_eq_square field_split_simps)

also have "... = other.s (t + δ)"
unfolding other.s_def
using assms pos_react ‹t + δ ≤ other.t_stop› by auto

finally have "delayed_safe_distance.other.s t = other.s (t + δ)" by auto }

moreover
{ assume "other.t_stop < t + δ"
hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p_max"
using delayed_other_t_stop_eq [OF 1] assms delayed_safe_distance.other.t_stop_nonneg
unfolding delayed_safe_distance.other.s_def by auto

also have "... = other.p_max"
unfolding movement.p_max_eq other.s_def other.s'_def other.p_def other.p'_def
using pos_react 1 decelerate_other
by (auto simp add: power2_eq_square field_split_simps)

also have "... = other.s (t + δ)"
unfolding other.s_def
using assms pos_react ‹other.t_stop < t + δ› by auto

finally have "delayed_safe_distance.other.s t = other.s (t + δ)" by auto }

ultimately show ?thesis by auto
next
assume "¬ δ ≤ other.t_stop"
hence "other.t_stop < δ" by auto
hence "other.s' δ = 0" and "other.s δ = other.p_max"
unfolding other.s'_def other.s_def using pos_react by auto
hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p_max"
unfolding delayed_safe_distance.other.s_def using assms decelerate_other
by (auto simp add:movement.p_max_eq movement.p_def movement.t_stop_def)
also have "... = other.p_max"
unfolding movement.p_max_eq using ‹other.s' δ = 0› ‹other.s δ = other.p_max›
using other.p_max_eq by auto
also have "... = other.s (t + δ)"
unfolding other.s_def using pos_react assms ‹other.t_stop < δ› by auto
finally show "delayed_safe_distance.other.s t = other.s (t + δ)" by auto
qed

lemma translate_collision_range:
assumes "s⇩o ≤ u_max"
assumes "u_max < other.s_stop"
shows "delayed_safe_distance.collision {0 ..} ⟷ collision_react {δ ..}"
proof
assume "delayed_safe_distance.collision {0 ..}"
then obtain t where eq: "ego2.s t = delayed_safe_distance.other.s t" and "0 ≤ t"
unfolding delayed_safe_distance.collision_def by auto

have "ego2.s t = (ego2.s ∘ τ) (t + δ)" unfolding comp_def τ_def by auto
also have "... = u (t + δ)" unfolding u_def using ‹0 ≤ t› pos_react
by (auto simp: τ_def ego2.init_s)
finally have left:"ego2.s t = u (t + δ)" by auto

have right: "delayed_safe_distance.other.s t = other.s (t + δ)"
using delayed_other_s_eq pos_react ‹0 ≤ t› by auto

with eq and left have "u (t + δ) = other.s (t + δ)" by auto
moreover have "δ ≤ t + δ" using ‹0 ≤ t› by auto
ultimately show "collision_react {δ ..}" unfolding collision_react_def by auto
next
assume "collision_react {δ ..}"
hence "collision_react {δ <..}" using collision_react_strict[OF assms] by simp
then obtain t where eq: "u t = other.s t" and "δ < t"
unfolding collision_react_def by auto
moreover hence "u t = (ego2.s ∘ τ) t" unfolding u_def using pos_react by auto
moreover have "other.s t = delayed_safe_distance.other.s (t - δ)"
using delayed_other_s_eq ‹δ < t› by auto
ultimately have "ego2.s (t - δ) = delayed_safe_distance.other.s (t - δ)"
unfolding comp_def τ_def by auto
with ‹δ < t› show "delayed_safe_distance.collision {0 ..}"
unfolding delayed_safe_distance.collision_def by auto
qed

theorem cond_3r_2:
assumes "s⇩o ≤ u_max"
assumes "u_max < other.s_stop"
assumes "other.s δ ≤ u_max"
shows "collision_react {0 ..} ⟷
(a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
proof -
have "collision_react {0 ..} ⟷ collision_react {δ ..}" by (rule collision_after_delta[OF assms(1) assms(2)])
also have "... ⟷ delayed_safe_distance.collision {0 ..}" by (simp add: translate_collision_range[OF assms(1) assms(2)])
also have "... ⟷  (a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
by (rule delayed_cond3'[OF assms(3) assms(2)])
finally show "collision_react {0 ..} ⟷  (a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
by auto
qed

lemma sd_2r_correct_for_3r_2:
assumes "s⇩o - s⇩e > safe_distance_2r"
assumes "other.s δ ≤ u_max"
assumes "¬ (a⇩o > a⇩e ∧ other.s' δ < v⇩e ∧ v⇩e - a⇩e / a⇩o * other.s' δ < 0)"
shows "no_collision_react {0..}"
proof -
from assms have "s⇩o - s⇩e > v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o" unfolding safe_distance_2r_def by auto
hence "s⇩o - v⇩o⇧2 / 2 / a⇩o > s⇩e + v⇩e * δ - v⇩e⇧2 / 2 / a⇩e" by auto
hence "s⇩o - v⇩o⇧2 / a⇩o + v⇩o⇧2 / 2 / a⇩o > s⇩e + v⇩e * δ - v⇩e⇧2 / 2 / a⇩e" by auto
hence "s⇩o + v⇩o * (- v⇩o / a⇩o) + 1/2 * a⇩o * (-v⇩o / a⇩o)⇧2 > s⇩e + v⇩e * δ - v⇩e⇧2 / 2 / a⇩e"
using other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
hence "other.s_stop > u_max" unfolding other.s_def using u_max_eq other.t_stop_def
using ego.q_def other.p_def other.p_max_def other.s_def other.s_t_stop by auto
thus ?thesis
using assms(2) assms(3) collision_after_delta cond_1r delayed_cond3' translate_collision_range by linarith
qed

lemma sd2_at_most_sd4:
assumes "a⇩o > a⇩e"
shows "safe_distance_2r ≤ safe_distance_4r"
proof -
have "a⇩o ≠ 0" and "a⇩e ≠ 0" and "a⇩o - a⇩e ≠ 0" and "0 < 2 * (a⇩o - a⇩e)" using hyps assms(1) by auto
have "0 ≤ (- v⇩e * a⇩o + v⇩o * a⇩e + a⇩o * a⇩e * δ) * (- v⇩e * a⇩o + v⇩o * a⇩e + a⇩o * a⇩e * δ)"
(is "0 ≤ (?l1 + ?l2 + ?l3) * ?r") by auto
also have "... = v⇩e⇧2 * a⇩o⇧2 + v⇩o⇧2 * a⇩e⇧2 + a⇩o⇧2 * a⇩e⇧2 * δ⇧2 - 2 * v⇩e * a⇩o * v⇩o * a⇩e - 2 * a⇩o⇧2 * a⇩e * δ * v⇩e + 2 * a⇩o * a⇩e⇧2 * δ * v⇩o"
(is "?lhs = ?rhs")
by (auto simp add:algebra_simps power_def)
finally have "0 ≤ ?rhs" by auto
hence "(- v⇩e⇧2 * a⇩o / a⇩e - v⇩o⇧2 * a⇩e / a⇩o) * (a⇩o * a⇩e) ≤ (a⇩o * a⇩e * δ⇧2 - 2 * v⇩e * v⇩o - 2 * a⇩o * δ * v⇩e + 2 * a⇩e * δ * v⇩o) * (a⇩o * a⇩e)"
by (auto simp add: algebra_simps power_def)
hence "2 * v⇩e * δ * (a⇩o - a⇩e) - v⇩e⇧2 * a⇩o / a⇩e + v⇩e⇧2 + v⇩o⇧2 - v⇩o⇧2 * a⇩e / a⇩o ≤ v⇩o⇧2 + a⇩o⇧2 * δ⇧2 + v⇩e⇧2 + 2 * v⇩o * δ * a⇩o - 2 * v⇩e * v⇩o - 2 * a⇩o * δ * v⇩e - 2 * v⇩o * δ * a⇩o + 2 * a⇩e * δ * v⇩o - a⇩o⇧2 * δ⇧2 + a⇩o * a⇩e * δ⇧2 + 2 * v⇩e * δ * (a⇩o - a⇩e)"
by (auto simp add: ego2.decel other.decel)
hence "2 * v⇩e * δ * (a⇩o - a⇩e) - v⇩e⇧2 * a⇩o / a⇩e + v⇩e⇧2 + v⇩o⇧2 - v⇩o⇧2 * a⇩e / a⇩o ≤ (v⇩o + δ * a⇩o - v⇩e)⇧2 - 2 * v⇩o * δ * a⇩o + 2 * a⇩e * δ * v⇩o - a⇩o⇧2 * δ⇧2 + a⇩o * a⇩e * δ⇧2 + 2 * v⇩e * δ * (a⇩o - a⇩e)"
by (auto simp add: algebra_simps power_def)
hence "v⇩e * δ * 2 * (a⇩o - a⇩e) - v⇩e⇧2 / 2 / a⇩e * 2 * a⇩o + v⇩e⇧2 / 2 / a⇩e * 2 * a⇩e + v⇩o⇧2 / 2 / a⇩o * 2 * a⇩o - v⇩o⇧2 / 2 / a⇩o * 2 * a⇩e ≤ (v⇩o + δ * a⇩o - v⇩e)⇧2 - v⇩o * δ * 2 * a⇩o - v⇩o * δ * 2 * -a⇩e - a⇩o * δ⇧2 / 2 * 2 * a⇩o - a⇩o * δ⇧2 / 2 * 2 * -a⇩e + v⇩e * δ * 2 * (a⇩o - a⇩e)"
(is "?lhs1 ≤ ?rhs1")
by (simp add: ‹a⇩o ≠ 0› ‹a⇩e ≠ 0› power2_eq_square algebra_simps)
hence "v⇩e * δ * 2 * (a⇩o - a⇩e) - v⇩e⇧2 / 2 / a⇩e * 2 * (a⇩o - a⇩e) + v⇩o⇧2 / 2 / a⇩o * 2 * (a⇩o - a⇩e) ≤ (v⇩o + a⇩o * δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e) * 2 * (a⇩o - a⇩e) - v⇩o * δ * 2 * (a⇩o - a⇩e) - a⇩o * δ⇧2 / 2 * 2 * (a⇩o - a⇩e) + v⇩e * δ * 2 *(a⇩o - a⇩e)"
(is "?lhs2 ≤ ?rhs2")
proof -
assume "?lhs1 ≤ ?rhs1"
have "?lhs1 = ?lhs2" by (auto simp add:field_simps)
moreover
have "?rhs1 = ?rhs2" using ‹a⇩o - a⇩e ≠ 0› by (auto simp add:field_simps)
ultimately show ?thesis using ‹?lhs1 ≤ ?rhs1› by auto
qed
hence "(v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o) * 2 * (a⇩o - a⇩e) ≤ ((v⇩o + a⇩o * δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e) - v⇩o * δ - 1/2 * a⇩o * δ⇧2 + v⇩e * δ) * 2 *(a⇩o - a⇩e)"
by (simp add: algebra_simps)
hence "v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o ≤ (v⇩o + a⇩o * δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e) - v⇩o * δ - 1/2 * a⇩o * δ⇧2 + v⇩e * δ"
using ‹a⇩o > a⇩e› mult_le_cancel_right_pos[OF ‹0 < 2 * (a⇩o - a⇩e)›, of "(v⇩e * δ - v⇩e⇧2 / 2 / a⇩e + v⇩o⇧2 / 2 / a⇩o)"
"(v⇩o + a⇩o * δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e) - v⇩o * δ - 1/2 * a⇩o * δ⇧2 + v⇩e * δ"] semiring_normalization_rules(18)
by (metis (no_types, lifting))
thus ?thesis using safe_distance_2r_def safe_distance_4r_def by auto
qed

lemma sd_4r_correct:
assumes "s⇩o - s⇩e > safe_distance_4r"
assumes "other.s δ ≤ u_max"
assumes "δ ≤ other.t_stop"
assumes "a⇩o > a⇩e"
shows "no_collision_react {0..}"
proof -
from assms have "s⇩o - s⇩e > (v⇩o + a⇩o * δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e) - v⇩o * δ - 1/2 * a⇩o * δ⇧2 + v⇩e * δ"
unfolding safe_distance_4r_def by auto
hence "s⇩o + v⇩o * δ + 1/2 * a⇩o * δ⇧2 - s⇩e - v⇩e * δ > (v⇩o + a⇩o * δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e)" by linarith
hence "other.s δ -  ego.q δ > (other.s' δ - v⇩e)⇧2 / 2 / (a⇩o - a⇩e)"
using assms(3) ego.q_def other.p_def other.s_def other.p'_def other.s'_def pos_react by auto
hence "other.s δ -  ego.q δ > delayed_safe_distance.snd_safe_distance"
by (simp add: delayed_safe_distance.snd_safe_distance_def)
hence c: "¬ (other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance)" by linarith
have "u_max < other.s_stop"
unfolding u_max_eq other.s_t_stop other.p_max_eq ego.q_def using assms(1) sd2_at_most_sd4[OF assms(4)]
unfolding safe_distance_4r_def safe_distance_2r_def by auto
consider "s⇩o ≤ u_max" | "s⇩o > u_max" by linarith
thus ?thesis
proof (cases)
case 1
from cond_3r_2[OF this ‹u_max < other.s_stop› assms(2)]  show ?thesis
using c by auto
next
case 2
then show ?thesis using cond_1r by auto
qed
qed

text ‹Irrelevant, this Safe Distance is unreachable in the checker.›
definition safe_distance_5r :: real where
"safe_distance_5r = v⇩e⇧2 / 2 / (a⇩o - a⇩e) + v⇩o⇧2 / 2 / a⇩o + v⇩e * δ"

lemma sd_5r_correct:
assumes "s⇩o - s⇩e > safe_distance_5r"
assumes "u_max < other.s_stop"
assumes "other.s δ ≤ u_max"
assumes "δ > other.t_stop"
shows</```