# Theory Safe_Distance

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

section ‹Safe Distance›

theory Safe_Distance
imports
"HOL-Analysis.Multivariate_Analysis"
"HOL-Decision_Procs.Approximation"
Sturm_Sequences.Sturm
begin

text ‹
This theory is about formalising the safe distance rule. The safe distance rule is obtained
from Vienna Convention which basically states the following thing.

``The car at all times must maintain a safe distance towards the vehicle in front of it,
such that whenever the vehicle in front and the ego vehicle apply maximum deceleration,
there will not be a collision.''

To formalise this safe distance rule we have to define first what is a safe distance.
To define this safe distance, we have to model the physics of the movement of the vehicle.
The following model is sufficient.

‹s = s⇩0 + v⇩0 * t + 1 / 2 * a⇩0 * t⇧2›

Assumptions in this model are :
▪ Both vehicles are assumed to be point mass. The exact location of the ego vehicle
is the front-most occupancy of the ego vehicle. Similarly for the other vehicle,
its exact location is the rearmost occupancy of the other vehicle.

▪ Both cars can never drive backward.
›

lemmas [simp del] = div_mult_self1 div_mult_self2 div_mult_self3 div_mult_self4

lemma discriminant: "a * x⇧2 + b * x + c = (0::real) ⟹ 0 ≤ b⇧2 - 4 * a * c"
by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))")

assumes D : "D = b⇧2 - 4 * a * c"
assumes nn: "0 ≤ D"
assumes x1: "x⇩1 = (-b + sqrt D) / (2 * a)"
assumes x2: "x⇩2 = (-b - sqrt D) / (2 * a)"
assumes a : "a ≠ 0"
shows "a * x⇧2 + b * x + c = a * (x - x⇩1) * (x - x⇩2)"
using nn
by (simp add: D x1 x2)
(simp add: assms power2_eq_square power3_eq_cube field_split_simps)

assumes D : "D = b⇧2 - 4 * a * c"
assumes x1: "x⇩1 = (-b + sqrt D) / (2 * a)"
assumes x2: "x⇩2 = (-b - sqrt D) / (2 * a)"
assumes a : "a ≠ 0"
shows "a * x⇧2 + b * x + c = 0 ⟷ (D ≥ 0 ∧ (x = x⇩1 ∨ x = x⇩2))" (is "?z ⟷ _")
using quadratic_eq_factoring[OF D _ x1 x2 a, of x] discriminant[of a x b c] a
by (auto simp: D)

subsection ‹Convexity Condition›

lemma p_convex:
fixes a b c x y z :: real
assumes p_def: "p = (λx. a * x⇧2 + b * x + c)"
assumes less : "x < y" "y < z"
and ge   : "p x > p y" "p y ≤ p z"
shows "a > 0"
using less ge unfolding p_def
by (sos "((((A<0 * (A<1 * A<2)) * R<1) + (((A<2 * R<1) * (R<1/4 * [y + ~1*z]^2)) +
(((A<=1 * R<1) * (R<1 * [x + ~1*y]^2)) + (((A<=1 * (A<0 * (A<1 * R<1))) * (R<1/4 * [1]^2)) +
(((A<=0 * R<1) * (R<1/4 * [~1*y^2 + x*y + ~1*x*z + y*z]^2)) +
((A<=0 * (A<0 * (A<1 * R<1))) * (R<1 * [x + ~1/2*y + ~1/2*z]^2))))))))")

definition root_in :: "real ⇒ real ⇒ (real ⇒ real) ⇒ bool" where
"root_in m M f = (∃x∈{m .. M}. f x = 0)"

definition quadroot_in :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
"quadroot_in m M a b c = root_in m M (λx. a * x^2 + b * x + c)"

lemma card_iff_exists: "0 < card X ⟷ finite X ∧ (∃x. x ∈ X)"
by (auto simp: card_gt_0_iff)

"quadroot_in m M a b c ⟷ (a = 0 ∧ b = 0 ∧ c = 0 ∧ m ≤ M) ∨
(m ≤ M ∧ poly [:c, b, a:] m = 0) ∨
count_roots_between [:c, b, a:] m M > 0"
apply (cases "a = 0 ∧ b = 0 ∧ c = 0 ∧ m ≤ M")
apply (force simp: quadroot_in_def root_in_def)
apply (cases "m ≤ M ∧ poly [:c, b, a:] m = 0")
apply (force simp: quadroot_in_def root_in_def algebra_simps power2_eq_square count_roots_between_correct card_iff_exists)
proof -
assume H: "¬ (a = 0 ∧ b = 0 ∧ c = 0 ∧ m ≤ M)" "¬ (m ≤ M ∧ poly [:c, b, a:] m = 0)"
hence "poly [:c, b, a:] m ≠ 0 ∨ m > M"
by auto
then have "quadroot_in m M a b c ⟷ 0 < count_roots_between [:c, b, a:] m M"
proof (rule disjE)
assume pnz: "poly [:c, b, a:] m ≠ 0"
then have nz: "[:c, b, a:] ≠ 0" by auto
show ?thesis
unfolding count_roots_between_correct card_iff_exists
apply safe
apply (rule finite_subset[where B="{x. poly [:c, b, a:] x = 0}"])
apply force
apply (rule poly_roots_finite)
apply (rule nz)
using pnz
apply (auto simp add: count_roots_between_correct quadroot_in_def root_in_def card_iff_exists
algebra_simps power2_eq_square)
apply (case_tac "x = m")
apply (force simp: algebra_simps)
apply force
done
qed (auto simp: quadroot_in_def count_roots_between_correct root_in_def card_eq_0_iff)
then show "quadroot_in m M a b c = (a = 0 ∧ b = 0 ∧ c = 0 ∧ m ≤ M ∨
m ≤ M ∧ poly [:c, b, a:] m = 0 ∨
0 < count_roots_between [:c, b, a:] m M)"
using H by metis
qed

fixes a b c :: real
assumes "a = 0"
shows "¬ quadroot_in m M a b c ⟷
((b = 0 ∧ c = 0 ∧ M < m) ∨ (b = 0 ∧ c ≠ 0) ∨
(b ≠ 0 ∧ (let x = - c / b in m > x ∨ x > M)))"
proof -
have "quadroot_in m M a b c ⟷ (b = 0 ⟶ quadroot_in m M a b c) ∧ (b ≠ 0 ⟶ quadroot_in m M a b c)"
by auto
also have "(b = 0 ⟶ quadroot_in m M a b c) ⟷
((b = 0 ⟶ c = 0 ⟶ m ≤ M) ∧ (b ≠ 0 ∨ c = 0))"
by (auto simp: quadroot_in_def Let_def root_in_def assms field_split_simps
intro!: bexI[where x="-c / b"])
also have "(b ≠ 0 ⟶ quadroot_in m M a b c) ⟷ (b = 0 ∨ (let x = -c / b in m ≤ x ∧ x ≤ M))"
apply (auto simp: quadroot_in_def Let_def root_in_def assms field_split_simps
intro!: bexI[where x="-c / b"])
by (metis mult.commute mult_le_cancel_left_neg add_eq_0_iff mult_le_cancel_left_pos)+
finally show ?thesis
by (simp add: Let_def not_less not_le)
qed

assumes "a ≠ 0"
shows "quadroot_in m M a b c =
(let D = b^2 - 4 * a * c in D ≥ 0 ∧
((let x = (-b + sqrt D)/(2*a) in m ≤ x ∧ x ≤ M) ∨
(let x = (-b - sqrt D)/(2*a) in m ≤ x ∧ x ≤ M)))"
by (auto simp: quadroot_in_def Let_def root_in_def quadratic_eq_zeroes_iff[OF refl refl refl assms])

shows "¬quadroot_in m M a b c ⟷
(a = 0 ⟶¬quadroot_in m M a b c) ∧
(a = 0 ∨ ¬quadroot_in m M a b c)"
by auto

subsection ‹Movement›

locale movement =
fixes a v s0 :: real
begin

text ‹
Function to compute the distance using the equation

‹s(t) = s⇩0 + v⇩0 * t + 1 / 2 * a⇩0 * t⇧2›

Input parameters:
▪ ‹s⇩0›: initial distance
▪ ‹v⇩0›: initial velocity (positive means forward direction and the converse is true)
▪ ‹a›: acceleration (positive for increasing and negative for decreasing)
▪ ‹t›: time

For the time ‹t < 0›, we assume the output of the function is ‹s⇩0›. Otherwise, the output
is calculated according to the equation above.
›

subsubsection ‹Continuous Dynamics›

definition p :: "real ⇒ real" where
"p t = s0 + v * t + 1/2 * a * t⇧2"

lemma p_all_zeroes:
assumes D: "D = v⇧2 - 2 * a * s0"
shows "p t = 0 ⟷ ((a ≠ 0 ∧ 0 ≤ D ∧ ((t = (- v + sqrt D) / a) ∨ t = (- v - sqrt D) / a)) ∨
(a = 0 ∧ v = 0 ∧ s0 = 0) ∨ (a = 0 ∧ v ≠ 0 ∧ t = (- s0 / v)))"
using quadratic_eq_zeroes_iff[OF refl refl refl, of "a / 2" t v s0]
by (auto simp: movement.p_def D power2_eq_square field_split_simps)

lemma p_zero[simp]: "p 0 = s0"
by (simp add: p_def)

lemma p_continuous[continuous_intros]: "continuous_on T p"
unfolding p_def by (auto intro!: continuous_intros)

lemma isCont_p[continuous_intros]: "isCont p x"
using p_continuous[of UNIV]
by (auto simp: continuous_on_eq_continuous_at)

definition p' :: "real ⇒ real" where
"p' t = v + a * t"

lemma p'_zero: "p' 0 = v"
by (simp add: p'_def)

lemma p_has_vector_derivative[derivative_intros]: "(p has_vector_derivative p' t) (at t within s)"
by (auto simp: p_def[abs_def] p'_def has_vector_derivative_def algebra_simps
intro!: derivative_eq_intros)

lemma p_has_real_derivative[derivative_intros]: "(p has_real_derivative p' t) (at t within s)"
using p_has_vector_derivative
by (simp add: has_real_derivative_iff_has_vector_derivative)

definition p'' :: "real ⇒ real" where
"p'' t = a"

lemma p'_has_vector_derivative[derivative_intros]: "(p' has_vector_derivative p'' t) (at t within s)"
by (auto simp: p'_def[abs_def] p''_def has_vector_derivative_def algebra_simps
intro!: derivative_eq_intros)

lemma p'_has_real_derivative[derivative_intros]: "(p' has_real_derivative p'' t) (at t within s)"
using p'_has_vector_derivative
by (simp add: has_real_derivative_iff_has_vector_derivative)

definition t_stop :: real where
"t_stop = - v / a"

lemma p'_stop_zero: "p' t_stop = (if a = 0 then v else 0)" by (auto simp: p'_def t_stop_def)

lemma p'_pos_iff: "p' x > 0 ⟷ (if a > 0 then x > -v / a else if a < 0 then x < -v / a else v > 0)"
by (auto simp: p'_def field_split_simps)

lemma le_t_stop_iff: "a ≠ 0 ⟹ x ≤ t_stop ⟷ (if a < 0 then p' x ≥ 0 else p' x ≤ 0)"
by (auto simp: p'_def field_split_simps t_stop_def)

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

lemma isCont_p'[continuous_intros]: "isCont p' x"
using p'_continuous[of UNIV] by (auto simp: continuous_on_eq_continuous_at)

definition p_max :: real where
"p_max = p t_stop"

lemmas p_t_stop = p_max_def[symmetric]

lemma p_max_eq: "p_max = s0 - v⇧2 / a / 2"
by (auto simp: p_max_def p_def t_stop_def field_split_simps power2_eq_square)

subsubsection ‹Hybrid Dynamics›

definition s :: "real ⇒ real" where
"s t = (     if t ≤ 0      then s0
else if t ≤ t_stop then p t
else                p_max)"

definition q :: "real ⇒ real" where
"q t = s0 + v * t"

definition q' :: "real ⇒ real" where
"q' t = v"

lemma init_q: "q 0 = s0" unfolding q_def by auto

lemma q_continuous[continuous_intros]: "continuous_on T q"
unfolding q_def by (auto intro: continuous_intros)

lemma isCont_q[continuous_intros]: "isCont q x"
using q_continuous[of UNIV]
by (auto simp:continuous_on_eq_continuous_at)

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

lemma q_has_real_derivative[derivative_intros]: "(q has_real_derivative q' t) (at t within u)"
using q_has_vector_derivative

lemma s_cond_def:
"t ≤ 0 ⟹ s t = s0"
"0 ≤ t ⟹ t ≤ t_stop ⟹ s t = p t"
by (simp_all add: s_def)

end

locale braking_movement = movement +
assumes decel: "a < 0"
assumes nonneg_vel: "v ≥ 0"
begin

lemma t_stop_nonneg: "0 ≤ t_stop"
using decel nonneg_vel
by (auto simp: t_stop_def divide_simps)

lemma t_stop_pos:
assumes "v ≠ 0"
shows "0 < t_stop"
using decel nonneg_vel assms
by (auto simp: t_stop_def divide_simps)

lemma t_stop_zero:
assumes "t_stop = 0"
shows "v = 0"
using assms decel
by (auto simp: t_stop_def)

lemma t_stop_zero_not_moving: "t_stop = 0 ⟹ q t = s0"
unfolding q_def using t_stop_zero by auto

abbreviation "s_stop ≡ s t_stop"

lemma s_t_stop: "s_stop = p_max"
using t_stop_nonneg
by (auto simp: s_def t_stop_def p_max_def p_def)

lemma s0_le_s_stop: "s0 ≤ s_stop"
proof (rule subst[where t="s_stop" and s="p_max"])
show "p_max = s_stop" by (rule sym[OF s_t_stop])
next
show "s0 ≤ p_max"
proof (rule subst[where t="p_max" and s="s0 - v⇧2 / a / 2"])
show " s0 - v⇧2 / a / 2 = p_max" using p_max_eq by auto
next
have "0 ≤ - v⇧2 / a / 2" using decel zero_le_square[of v]
proof -
have f1: "a ≤ 0"
using ‹a < 0› by linarith
have "(- 1 * v⇧2 ≤ 0) = (0 ≤ v⇧2)"
by auto
then have "0 ≤ - 1 * v⇧2 / a"
using f1 by (meson zero_le_divide_iff zero_le_power2)
then show ?thesis
by force
qed
thus "s0 ≤ s0 - v⇧2 / a / 2" by auto
qed
qed

lemma p_mono: "x ≤ y ⟹ y ≤ t_stop ⟹ p x ≤ p y"
using decel
proof -
assume "x ≤ y" and "y ≤ t_stop" and "a < 0"
hence "x + y ≤ - 2 * v / a"
unfolding t_stop_def by auto
hence "-1 / 2 * a * (x + y) ≤ v" (is "?lhs0 ≤ ?rhs0")
using ‹a < 0› by (auto simp add: field_simps)
hence "?lhs0 * (x- y) ≥ ?rhs0 * (x - y)"
using ‹x ≤ y› by sos
hence "v * x + 1 / 2 * a * x⇧2 ≤ v * y + 1 / 2 * a * y⇧2"
by (auto simp add: field_simps power_def)
thus " p x ≤ p y"
unfolding p_max_def p_def t_stop_def by auto
qed

lemma p_antimono: "x ≤ y ⟹ t_stop ≤ x ⟹ p y ≤ p x"
using decel
proof -
assume "x ≤ y" and "t_stop ≤ x" and "a < 0"
hence "- 2 * v / a ≤ x + y"
unfolding t_stop_def by auto
hence "v ≤ - 1/ 2 * a * (x + y)"
using ‹a < 0› by (auto simp add: field_simps)
hence "v * (x - y) ≥ -1/2 * a * (x⇧2 - y⇧2) "
using ‹x ≤ y› by sos
hence "v * y + 1/2 * a * y⇧2 ≤ v * x + 1/2 * a * x⇧2"
by (auto simp add: field_simps)
thus "p y ≤ p x"
unfolding p_max_def p_def t_stop_def by auto
qed

lemma p_strict_mono: "x < y ⟹ y ≤ t_stop ⟹ p x < p y"
using decel
proof -
assume "x < y" and "y ≤ t_stop" and "a < 0"
hence "x + y < - 2 * v / a"
unfolding t_stop_def by auto
hence "-1 / 2 * a * (x + y) < v" (is "?lhs0 < ?rhs0")
using ‹a < 0› by (auto simp add: field_simps)
hence "?lhs0 * (x- y) > ?rhs0 * (x - y)"
using ‹x < y› by sos
hence "v * x + 1 / 2 * a * x⇧2 < v * y + 1 / 2 * a * y⇧2"
by (auto simp add: field_simps power_def)
thus " p x < p y"
unfolding p_max_def p_def t_stop_def by auto
qed

lemma p_strict_antimono: "x < y ⟹ t_stop ≤ x⟹ p y < p x"
using decel
proof -
assume "x < y" and "t_stop ≤ x" and "a < 0"
hence "- 2 * v / a < x + y"
unfolding t_stop_def by auto
hence "v < - 1/ 2 * a * (x + y)"
using ‹a < 0› by (auto simp add: field_simps)
hence "v * (x - y) > -1/2 * a * (x⇧2 - y⇧2) "
using ‹x < y› by sos
hence "v * y + 1/2 * a * y⇧2 < v * x + 1/2 * a * x⇧2"
by (auto simp add: field_simps)
thus "p y < p x"
unfolding p_max_def p_def t_stop_def by auto
qed

lemma p_max: "p x ≤ p_max"
unfolding p_max_def
by (cases "x ≤ t_stop") (auto intro: p_mono p_antimono)

lemma continuous_on_s[continuous_intros]: "continuous_on T s"
unfolding s_def[abs_def]
using t_stop_nonneg
by (intro continuous_on_subset[where t=T and s = "{.. 0}∪({0 .. t_stop} ∪ {t_stop ..})"] continuous_on_If)
(auto simp: p_continuous p_max_def antisym_conv[where x=0])

lemma isCont_s[continuous_intros]: "isCont s x"
using continuous_on_s[of UNIV]
by (auto simp: continuous_on_eq_continuous_at)

definition s' :: "real ⇒ real" where
"s' t = (if t ≤ t_stop then p' t else 0)"

lemma s_has_real_derivative:
assumes "t ≥ 0" "v / a ≤ 0" "a ≠ 0"
shows "(s has_real_derivative s' t) (at t within {0..})"
proof -
from assms have *: "t ≤ t_stop ⟷ t ∈ {0 .. t_stop}" by simp
from assms have "0 ≤ t_stop" by (auto simp: t_stop_def)
have "((λt. if t ∈ {0 .. t_stop} then p t else p_max) has_real_derivative
(if t ∈ {0..t_stop} then p' t else 0)) (at t within {0..})"
unfolding s_def[abs_def] s'_def
has_real_derivative_iff_has_vector_derivative
apply (rule has_vector_derivative_If_within_closures[where T = "{t_stop ..}"])
using ‹0 ≤ t_stop› ‹a ≠ 0›
by (auto simp: assms p'_stop_zero p_t_stop max_def insert_absorb
intro!: p_has_vector_derivative)
from _ _ this show ?thesis
unfolding has_vector_derivative_def has_real_derivative_iff_has_vector_derivative
s'_def s_def[abs_def] *
by (rule has_derivative_transform)
(auto simp: assms s_def p_max_def t_stop_def)
qed

lemma s_has_vector_derivative[derivative_intros]:
assumes "t ≥ 0" "v / a ≤ 0" "a ≠ 0"
shows  "(s has_vector_derivative s' t) (at t within {0..})"
using s_has_real_derivative[OF assms]
by (simp add: has_real_derivative_iff_has_vector_derivative)

lemma s_has_field_derivative[derivative_intros]:
assumes "t ≥ 0" "v / a ≤ 0" "a ≠ 0"
shows "(s has_field_derivative s' t) (at t within {0..})"
using s_has_vector_derivative[OF assms]

lemma s_has_real_derivative_at:
assumes "0 < x" "0 ≤ v" "a < 0"
shows "(s has_real_derivative s' x) (at x)"
proof -
from assms have "(s has_real_derivative s' x) (at x within {0 ..})"
by (intro s_has_real_derivative) (auto intro!: divide_nonneg_nonpos)
then have "(s has_real_derivative s' x) (at x within {0<..})"
by (rule DERIV_subset) auto
then show "(s has_real_derivative s' x) (at x)" using assms
by (subst (asm) at_within_open) auto
qed

lemma s_delayed_has_field_derivative[derivative_intros]:
assumes "δ < t" "0 ≤ v" "a < 0"
shows "((λx. s (x - δ)) has_field_derivative s' (t - δ)) (at t within {δ<..})"
proof -
from assms have "((λx. s (x + - δ)) has_real_derivative s' (t - δ)) (at t)"
using DERIV_shift[of "s" "(s' (t - δ))" t "-δ"] s_has_real_derivative_at
by auto

thus "((λx. s (x - δ)) has_field_derivative s' (t - δ)) (at t within {δ<..})"
using has_field_derivative_at_within by auto
qed

lemma s_delayed_has_vector_derivative[derivative_intros]:
assumes "δ < t" "0 ≤ v" "a < 0"
shows  "((λx. s (x - δ)) has_vector_derivative s' (t - δ)) (at t within {δ<..})"
using s_delayed_has_field_derivative[OF assms]

lemma s'_nonneg: "0 ≤ v ⟹ a ≤ 0 ⟹ 0 ≤ s' x"
by (auto simp: s'_def p'_def t_stop_def field_split_simps)

lemma s'_pos: "0 ≤ x ⟹ x < t_stop ⟹ 0 ≤ v ⟹ a ≤ 0 ⟹ 0 < s' x"
by (intro le_neq_trans s'_nonneg)
(auto simp: s'_def p'_def t_stop_def field_split_simps)

subsubsection ‹Monotonicity of Movement›

lemma s_mono:
assumes "t ≥ u" "u ≥ 0"
shows "s t ≥ s u"
using p_mono[of u t] assms p_max[of u] by (auto simp: s_def)

lemma s_strict_mono:
assumes "u < t" "t ≤ t_stop" "u ≥ 0"
shows "s u < s t"
using p_strict_mono[of u t] assms p_max[of u] by (auto simp: s_def)

lemma s_antimono:
assumes "x ≤ y"
assumes "t_stop ≤ x"
shows "s y ≤ s x"
proof -
from assms have "t_stop ≤ y" by auto
hence "s y ≤ p_max" unfolding s_def p_max_eq
using p_max_def p_max_eq s0_le_s_stop s_t_stop by auto
also have "... ≤ s x"
using ‹t_stop ≤ x› s_mono s_t_stop t_stop_nonneg by fastforce
ultimately show "s y ≤ s x" by auto
qed

lemma init_s : "t ≤ 0 ⟹ s t = s0"
using decel nonneg_vel by (simp add: divide_simps s_def)

lemma q_min: "0 ≤ t ⟹ s0 ≤ q t"
unfolding q_def using nonneg_vel by auto

lemma q_mono: "x ≤ y ⟹ q x ≤ q y"
unfolding q_def using nonneg_vel by (auto simp: mult_left_mono)

subsubsection ‹Maximum at Stopping Time›

lemma s_max: "s x ≤ s_stop"
using p_max[of x] p_max[of 0] unfolding s_t_stop by (auto simp: s_def)

lemma s_eq_s_stop: "NO_MATCH t_stop x ⟹ x ≥ t_stop ⟹ s x = s_stop"
using t_stop_nonneg by (auto simp: s_def p_max_def)

end

subsection ‹Safe Distance›

locale safe_distance =
fixes a⇩e v⇩e s⇩e :: real
fixes a⇩o v⇩o s⇩o :: real
assumes nonneg_vel_ego   : "0 ≤ v⇩e"
assumes nonneg_vel_other : "0 ≤ v⇩o"
assumes decelerate_ego   : "a⇩e < 0"
assumes decelerate_other : "a⇩o < 0"
assumes in_front         : "s⇩e < s⇩o"
begin

lemmas hyps =
nonneg_vel_ego
nonneg_vel_other
decelerate_ego
decelerate_other
in_front

sublocale ego: braking_movement a⇩e v⇩e s⇩e by (unfold_locales; rule hyps)
sublocale other: braking_movement a⇩o v⇩o s⇩o by (unfold_locales; rule hyps)
sublocale ego_other: movement "a⇩o - a⇩e" "v⇩o - v⇩e" "s⇩o - s⇩e" by unfold_locales

subsubsection ‹Collision›

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

abbreviation no_collision :: "real set ⇒ bool" where
"no_collision time_set ≡ ¬ collision time_set"

lemma no_collision_initially : "no_collision {.. 0}"
using decelerate_ego nonneg_vel_ego
using decelerate_other nonneg_vel_other in_front
by (auto simp: divide_simps collision_def ego.s_def other.s_def)

lemma no_collisionI:
"(⋀t. t ∈ S ⟹ ego.s t ≠ other.s t) ⟹ no_collision S"
unfolding collision_def by blast

theorem cond_1: "ego.s_stop < s⇩o ⟹ no_collision {0..}"
proof (rule no_collisionI, simp)
fix t::real
assume "t ≥ 0"
have "ego.s t ≤ ego.s_stop"
by (rule ego.s_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 "ego.s t ≠ other.s t"
by simp
qed

lemma ego_other_strict_ivt:
assumes "ego.s t > other.s t"
shows "collision {0 ..< t}"
proof cases
have [simp]: "s⇩e < s⇩o ⟹ ego.s 0 ≤ other.s 0"
by (simp add: movement.s_def)
assume "0 ≤ t"
with assms in_front
have "∃x≥0. x ≤ t ∧ other.s x - ego.s x = 0"
by (intro IVT2, auto simp: continuous_diff other.isCont_s ego.isCont_s)
then show ?thesis
using assms
by (auto simp add: algebra_simps collision_def Bex_def order.order_iff_strict)
qed (insert assms hyps, auto simp: collision_def ego.init_s other.init_s intro!: bexI[where x=0])

lemma collision_subset: "collision s ⟹ s ⊆ t ⟹ collision t"
by (auto simp: collision_def)

lemma ego_other_ivt:
assumes "ego.s t ≥ other.s t"
shows "collision {0 .. t}"
proof cases
assume "ego.s t > other.s t"
from ego_other_strict_ivt[OF this]
show ?thesis
by (rule collision_subset) auto
qed (insert hyps assms; cases "t ≥ 0"; force simp: collision_def ego.init_s other.init_s)

theorem cond_2:
assumes "ego.s_stop ≥ other.s_stop"
shows "collision {0 ..}"
using assms
apply (intro collision_subset[where t="{0 ..}" and s = "{0 .. max ego.t_stop other.t_stop}"])
apply (intro ego_other_ivt[where t = "max ego.t_stop other.t_stop"])
apply (auto simp: ego.s_eq_s_stop other.s_eq_s_stop)
done

abbreviation D2 :: "real" where
"D2 ≡ (v⇩o - v⇩e)^2 - 2 * (a⇩o - a⇩e) * (s⇩o - s⇩e)"

abbreviation t⇩D' :: "real" where
"t⇩D' ≡ sqrt (2 * (ego.s_stop - other.s_stop) / a⇩o)"

lemma pos_via_half_dist:
"dist a b < b / 2 ⟹ b > 0 ⟹ a > 0"
by (auto simp: dist_real_def abs_real_def split: if_splits)

lemma collision_within_p:
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop"
shows "collision {0..} ⟷ (∃t≥0. ego.p t = other.p t ∧ t < ego.t_stop ∧ t < other.t_stop)"
proof (auto simp: collision_def, goal_cases)
case (2 t)
then show ?case
by (intro bexI[where x = t]) (auto simp: ego.s_def other.s_def)
next
case (1 t)
then show ?case using assms hyps ego.t_stop_nonneg other.t_stop_nonneg
apply (auto simp: ego.s_def other.s_def ego.s_t_stop other.s_t_stop ego.p_t_stop other.p_t_stop not_le
split: if_splits)
defer
proof goal_cases
case 1
from 1 have le: "ego.t_stop ≤ other.t_stop" by auto
from 1 have "ego.t_stop < t" by simp
from other.s_strict_mono[OF this] 1
have "other.s ego.t_stop < other.s t"
by auto
also have "… = ego.s ego.t_stop"
using ego.s_t_stop ego.t_stop_nonneg 1 other.s_def by auto
finally have "other.s ego.t_stop < ego.s ego.t_stop" .
from ego_other_strict_ivt[OF this] le in_front
show ?case
by (auto simp add: collision_def) (auto simp: movement.s_def split: if_splits)
next
case 2
from 2 have "other.p_max = ego.p t" by simp
also have "… ≤ ego.p ego.t_stop"
using 2
by (intro ego.p_mono) auto
also have "… = ego.p_max"
by (simp add: ego.p_t_stop)
also note ‹… < other.p_max›
finally show ?case by arith
next
case 3
thus "∃t≥0. ego.p t = other.p t ∧ t < ego.t_stop ∧ t < other.t_stop"
apply (cases "t = other.t_stop")
apply (simp add: other.p_t_stop )
apply (metis (no_types) ego.p_max not_le)
apply (cases "t = ego.t_stop")
apply (simp add: ego.p_t_stop)
defer
apply force
proof goal_cases
case (1)
let ?d = "λt. other.p' t - ego.p' t"
define d' where "d' = ?d ego.t_stop / 2"
have d_cont: "isCont ?d ego.t_stop"
unfolding ego.t_stop_def other.p'_def ego.p'_def by simp
have "?d ego.t_stop > 0"
using 1
by (simp add: ego.p'_stop_zero other.p'_pos_iff) (simp add: ego.t_stop_def other.t_stop_def)
then have "d' > 0" by (auto simp: d'_def)
from d_cont[unfolded continuous_at_eps_delta, THEN spec, rule_format, OF ‹d' > 0›]
obtain e where e: "e > 0" "⋀x. dist x ego.t_stop < e ⟹ ?d x > 0"
unfolding d'_def
using ‹?d ego.t_stop > 0› pos_via_half_dist
by force
define t' where "t' = ego.t_stop - min (ego.t_stop / 2) (e / 2)"
have "0 < ego.t_stop" using 1 by auto
have "other.p t' - ego.p t' < other.p ego.t_stop - ego.p ego.t_stop"
apply (rule DERIV_pos_imp_increasing[of t'])
apply (force simp: t'_def e min_def ‹0 < ego.t_stop›)
apply (auto intro!: exI[where x = "?d x" for x] intro!: derivative_intros e)
using ‹e > 0›
apply (auto simp: t'_def dist_real_def algebra_simps)
done
also have "… = 0" using 1 by (simp add: ego.p_t_stop)
finally have less: "other.p t' < ego.p t'" by simp
have "t' > 0"
using 1 by (auto simp: t'_def algebra_simps min_def)
have "t' < ego.t_stop" by (auto simp: t'_def ‹e > 0› ‹ego.t_stop > 0›)
from less_le_trans[OF ‹t' < ego.t_stop› ‹ego.t_stop ≤ other.t_stop›]
have "t' < other.t_stop" .
from ego_other_strict_ivt[of t'] less
have "collision {0..<t'}"
using ‹t' > 0› ‹t' < ego.t_stop› ‹t' < other.t_stop›
by (auto simp: other.s_def ego.s_def split: if_splits)
thus ?case
using ‹t' > 0› ‹t' < ego.t_stop› ‹t' < other.t_stop›
apply (auto simp: collision_def ego.s_def other.s_def movement.p_def
split: if_splits)
apply (rule_tac x = t in exI)
apply (auto simp: movement.p_def)[]
done
qed
qed
qed

lemma collision_within_eq:
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop"
shows "collision {0..} ⟷ collision {0 ..< min ego.t_stop other.t_stop}"
unfolding collision_within_p[OF assms]
unfolding collision_def
by (safe; force
simp: ego.s_def other.s_def movement.p_def ego.t_stop_def other.t_stop_def
split: if_splits)

lemma collision_excluded: "(⋀t. t ∈ T ⟹ ego.s t ≠ other.s t) ⟹ collision S ⟷ collision (S - T)"
by (auto simp: collision_def)

lemma collision_within_less:
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop"
shows "collision {0..} ⟷ collision {0 <..< min ego.t_stop other.t_stop}"
proof -
note collision_within_eq[OF assms]
also have "collision {0 ..< min ego.t_stop other.t_stop} ⟷
collision ({0 ..< min ego.t_stop other.t_stop} - {0})"
using hyps assms
by (intro collision_excluded) (auto simp: ego.s_def other.s_def)
also have "{0 ..< min ego.t_stop other.t_stop} - {0} = {0 <..< min ego.t_stop other.t_stop}"
by auto
finally show ?thesis
unfolding collision_def
by (safe;
force
simp: ego.s_def other.s_def movement.p_def ego.t_stop_def other.t_stop_def
split: if_splits)
qed

theorem cond_3:
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop"
shows "collision {0..} ⟷ (a⇩o > a⇩e ∧ v⇩o < v⇩e ∧ 0 ≤ D2 ∧ sqrt D2 > v⇩e - a⇩e / a⇩o * v⇩o)"
proof -
have "v⇩o ≠ 0"
using assms(1) assms(2) movement.s_def movement.t_stop_def by auto
with hyps have "v⇩o > 0" by auto
note hyps = hyps this
define t1 where "t1 = (- (v⇩o - v⇩e) + sqrt D2) / (a⇩o - a⇩e)"
define t2 where "t2 = (- (v⇩o - v⇩e) - sqrt D2) / (a⇩o - a⇩e)"
define bounded where "bounded ≡ λt. (0 ≤ t ∧ t ≤ ego.t_stop ∧ t ≤ other.t_stop)"
have ego_other_conv:
"⋀t. bounded t ⟹ ego.p t = other.p t ⟷ ego_other.p t = 0"
by (auto simp: movement.p_def field_split_simps)
let ?r = "{0 <..< min ego.t_stop other.t_stop}"
have D2: "D2 = (v⇩o - v⇩e)⇧2 - 4 * ((a⇩o - a⇩e) / 2) * (s⇩o - s⇩e)" by simp
define D where "D = D2"
note D = D_def[symmetric]
define x1 where "x1 ≡ (- (v⇩o - v⇩e) + sqrt D2) / (2 * ((a⇩o - a⇩e) / 2))"
define x2 where "x2 ≡ (- (v⇩o - v⇩e) - sqrt D2) / (2 * ((a⇩o - a⇩e) / 2))"
have x2: "x2 =(- (v⇩o - v⇩e) - sqrt D2) / (a⇩o - a⇩e)"
by (simp add: x2_def field_split_simps)
have x1: "x1 =(- (v⇩o - v⇩e) + sqrt D2) / (a⇩o - a⇩e)"
by (simp add: x1_def field_split_simps)
from collision_within_less[OF assms]
have coll_eq: "collision {0..} = collision ?r"
by (auto simp add: bounded_def)
also have "… ⟷ (a⇩o > a⇩e ∧ v⇩o < v⇩e ∧ 0 ≤ D2 ∧ sqrt D2 > v⇩e - a⇩e / a⇩o * v⇩o)"
proof safe
assume H: "a⇩e < a⇩o" "v⇩o < v⇩e" "0 ≤ D2"
assume sqrt: "sqrt D2 > v⇩e - a⇩e / a⇩o * v⇩o"
have nz: "(a⇩o - a⇩e) / 2 ≠ 0" using ‹a⇩e < a⇩o› by simp
note sol = quadratic_eq_zeroes_iff[OF D2 x1_def[THEN meta_eq_to_obj_eq] x2_def[THEN meta_eq_to_obj_eq] nz]
from sol[of x2] ‹0 ≤ D2›
have "other.p x2 = ego.p x2"
by (auto simp: ego.p_def other.p_def field_split_simps)
moreover
have "x2 > 0"
proof (rule ccontr)
assume "¬ 0 < x2"
then have "ego_other.p x2 ≥ ego_other.p 0"
using H hyps
by (intro DERIV_nonpos_imp_nonincreasing[of x2])
(auto intro!: exI[where x="ego_other.p' x" for x] derivative_eq_intros
simp: ego_other.p'_def add_nonpos_nonpos mult_nonneg_nonpos)
also have "ego_other.p 0 > 0" using hyps by (simp add: ego_other.p_def)
finally (xtrans) show False using ‹other.p x2 = ego.p x2›
by (simp add: movement.p_def field_split_simps power2_eq_square)
qed
moreover
have "x2 < other.t_stop"
using sqrt H hyps
by (auto simp: x2 other.t_stop_def field_split_simps power2_eq_square)

ultimately
show "collision {0<..<min ego.t_stop other.t_stop}"
proof (cases "x2 < ego.t_stop", goal_cases)
case 2
then have "other.s x2 = other.p x2"
by (auto simp: other.s_def)
also from 2 have "… ≤ ego.p ego.t_stop"
by (auto intro!: ego.p_antimono)
also have "… = ego.s x2"
using 2 by (auto simp: ego.s_def ego.p_t_stop)
finally have "other.s x2 ≤ ego.s x2" .
from ego_other_ivt[OF this]
show ?thesis
unfolding coll_eq[symmetric]
by (rule collision_subset) auto
qed (auto simp: collision_def ego.s_def other.s_def not_le intro!: bexI[where x=x2])
next
let ?max = "max ego.t_stop other.t_stop"
let ?min = "min ego.t_stop other.t_stop"
assume "collision ?r"
then obtain t where t: "ego.p t = other.p t" "0 < t" "t < ?min"
by (auto simp: collision_def ego.s_def other.s_def)
then have "t < - (v⇩e / a⇩e)" "t < - (v⇩o / a⇩o)" "t < other.t_stop"
by (simp_all add: ego.t_stop_def other.t_stop_def)
from t have "ego_other.p t = 0"
by (auto simp: movement.p_def field_split_simps)
from t have "t < ?max" by auto
from hyps assms have "0 < ego_other.p 0"
by simp
from ego_other.p_def[abs_def, THEN meta_eq_to_obj_eq]
have eop_eq: "ego_other.p = (λt. 1 / 2 * (a⇩o - a⇩e) * t⇧2 + (v⇩o - v⇩e) * t + (s⇩o - s⇩e))"
by (simp add: algebra_simps)
show "a⇩o > a⇩e"
proof -
have "ego.p other.t_stop ≤ ego.p_max"
by (rule ego.p_max)
also have "... ≤ other.p other.t_stop" using hyps assms
by (auto simp:other.s_def ego.s_def ego.p_t_stop split:if_splits)
finally have "0 ≤ ego_other.p other.t_stop"
by (auto simp add:movement.p_def field_simps)
from p_convex[OF eop_eq, of 0 t other.t_stop, simplified ‹ego_other.p t = 0›,
OF ‹0 < t› ‹t < other.t_stop› ‹0 < ego_other.p 0› ‹0 ≤ ego_other.p other.t_stop›]
show "a⇩o > a⇩e" by (simp add: algebra_simps)
qed
have rewr: "4 * ((a⇩o - a⇩e) / 2) = 2 * (a⇩o - a⇩e)" by simp
from ‹a⇩o > a⇩e› ‹ego_other.p t = 0› ego_other.p_all_zeroes[OF D2[symmetric], of t]
have "0 ≤ D2" and disj: "(t = (- (v⇩o - v⇩e) + sqrt D2) / (a⇩o - a⇩e) ∨ t = (- (v⇩o - v⇩e) - sqrt D2) / (a⇩o - a⇩e))"
using hyps assms
unfolding rewr by simp_all
show "0 ≤ D2" by fact
from add_strict_mono[OF ‹t < - (v⇩e / a⇩e)› ‹t < - (v⇩o / a⇩o)›] ‹0 < t› ‹a⇩o > a⇩e›
have "0 < - (v⇩e / a⇩e) + - (v⇩o / a⇩o)" by (simp add: divide_simps)
then have "0 > v⇩e * a⇩o + a⇩e * v⇩o" using hyps
by (simp add: field_split_simps split: if_splits)
show "v⇩o < v⇩e"
using ‹a⇩e < a⇩o› ‹movement.p (a⇩o - a⇩e) (v⇩o - v⇩e) (s⇩o - s⇩e) t = 0› in_front  t(2)
apply (auto simp: movement.p_def divide_less_0_iff algebra_simps power2_eq_square)
by (smt divide_less_0_iff mult_le_cancel_right mult_mono mult_nonneg_nonneg nonneg_vel_ego)
from disj have "x2 < ?min"
proof rule
assume "t = (- (v⇩o - v⇩e) - sqrt D2) / (a⇩o - a⇩e)"
then show ?thesis
using ‹t < ?min›
by (simp add: x2)
next
assume "t = (- (v⇩o - v⇩e) + sqrt D2) / (a⇩o - a⇩e)"
also have "… ≥ x2"
unfolding x2
apply (rule divide_right_mono)
apply (subst (2) diff_conv_add_uminus)
using ‹a⇩o > a⇩e› ‹D2 ≥ 0›
by auto
also (xtrans) note ‹t < ?min›
finally show ?thesis .
qed
then show "sqrt D2 > v⇩e - a⇩e / a⇩o * v⇩o"
using hyps ‹a⇩o > a⇩e›
by (auto simp: x2 field_split_simps other.t_stop_def)
qed
finally show ?thesis .
qed

subsubsection ‹Formalising Safe Distance›

text ‹First definition for Safe Distance based on ‹cond_1›.›
definition absolute_safe_distance :: real where
"absolute_safe_distance = - v⇩e⇧2 / (2 * a⇩e)"

lemma absolute_safe_distance:
assumes "s⇩o - s⇩e > absolute_safe_distance"
shows "no_collision {0..}"
proof -
from assms hyps absolute_safe_distance_def have "ego.s_stop < s⇩o"
by (auto simp add:ego.s_def ego.p_def ego.t_stop_def power_def)
thus ?thesis by (rule cond_1)
qed

text ‹First Fallback for Safe Distance.›
definition fst_safe_distance :: real where
"fst_safe_distance = v⇩o⇧2 / (2 * a⇩o) - v⇩e⇧2 / (2 * a⇩e)"

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

lemma snd_leq_fst_exp: "distance_leq_d2 ≤ fst_safe_distance"
proof -
have "0 ≤ (other.t_stop - ego.t_stop)⇧2" by auto
hence "- ego.t_stop⇧2 ≤ other.t_stop⇧2 - 2 * other.t_stop * ego.t_stop" by (simp add:power_def algebra_simps)
with hyps(3) have "- ego.t_stop⇧2 * (a⇩e / 2) ≥ (other.t_stop⇧2 - 2 * other.t_stop * ego.t_stop) * (a⇩e / 2)"
by (smt half_gt_zero_iff mult_le_cancel_right)
with ego.t_stop_def other.t_stop_def hyps
have "- v⇩e⇧2 / (2 * a⇩e) ≥ a⇩e * v⇩o⇧2 / (2 * a⇩o⇧2) - v⇩o * v⇩e / a⇩o" by (simp add:power_def algebra_simps)
with fst_safe_distance_def distance_leq_d2_def
have 1: "fst_safe_distance ≥  a⇩e * v⇩o⇧2 / (2 * a⇩o⇧2) - v⇩o * v⇩e / a⇩o + v⇩o⇧2 / (2 * a⇩o)" by (auto simp add:algebra_simps)
have "a⇩e * v⇩o⇧2 / (2 * a⇩o⇧2) - v⇩o * v⇩e / a⇩o + v⇩o⇧2 / (2 * a⇩o) = distance_leq_d2" (is "?LHS = _")
proof -
have "?LHS = a⇩e * v⇩o⇧2 / (2 * a⇩o⇧2) - v⇩o * v⇩e / a⇩o + a⇩o * v⇩o⇧2 / (2 * a⇩o⇧2)"
by (auto simp add: algebra_simps power_def)
also have "...  = distance_leq_d2"
by (auto simp add: power_def field_split_simps distance_leq_d2_def)
finally show ?thesis by auto
qed
with 1 show ?thesis by auto
qed

lemma sqrt_D2_leq_stop_time_diff:
assumes "a⇩e < a⇩o"
assumes "0 ≤ v⇩e - a⇩e / a⇩o * v⇩o "
assumes "s⇩o - s⇩e ≥ distance_leq_d2"
shows "sqrt D2 ≤ v⇩e - a⇩e / a⇩o * v⇩o"
proof -
from assms have "- 2 * (a⇩o - a⇩e) * (s⇩o - s⇩e) ≤ - 2 * (a⇩o - a⇩e) * distance_leq_d2" (is "?L ≤ ?R")
by simp
hence "D2 ≤ (v⇩o - v⇩e)⇧2 - 2 * (a⇩o - a⇩e) * distance_leq_d2" by (simp add: algebra_simps)
also have "... = (v⇩e - a⇩e / a⇩o * v⇩o)⇧2"
proof -
from distance_leq_d2_def
have 1: "(v⇩o - v⇩e)⇧2 - 2 * (a⇩o - a⇩e) * distance_leq_d2 =
(v⇩o - v⇩e)⇧2 - (a⇩o - a⇩e) * (a⇩e + a⇩o) / a⇩o⇧2 * v⇩o⇧2 + 2 * (a⇩o - a⇩e) * v⇩o * v⇩e / a⇩o"
by (auto simp add: field_split_simps)
with hyps(4) have "... = (v⇩e - a⇩e / a⇩o * v⇩o)⇧2"
by (auto simp add: power_def field_split_simps)
with 1 show ?thesis by auto
qed
finally show ?thesis  by (smt assms(2) real_le_lsqrt real_sqrt_le_0_iff)
qed

lemma cond2_imp_pos_vo:
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop"
shows "v⇩o ≠ 0"
proof (rule ccontr)
assume "¬ v⇩o ≠ 0"
with other.s_def other.t_stop_def have "other.s_stop = s⇩o" by auto
with assms(2) have "ego.s_stop < s⇩o" by auto
with assms(1) show "False" by auto
qed

lemma cond2_imp_gt_fst_sd:
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop"
shows "fst_safe_distance < s⇩o - s⇩e"
proof (cases "v⇩e ≠ 0")
case True
from fst_safe_distance_def assms ego.s_def ego.t_stop_pos[OF ‹v⇩e ≠ 0›] ego.p_def ego.t_stop_def
other.s_def other.t_stop_pos[OF cond2_imp_pos_vo[OF assms]] other.p_def other.t_stop_def hyps
show ?thesis by (simp add: power_def algebra_simps)
next
case False
with fst_safe_distance_def  have "fst_safe_distance = v⇩o⇧2 / (2 * a⇩o)" by auto
also have "... ≤ 0"  by (simp add: divide_nonneg_neg hyps)
also have "... < s⇩o - s⇩e" by (simp add: algebra_simps hyps)
finally show ?thesis by auto
qed

text ‹Second Fallback for Safe Distance.›
definition snd_safe_distance :: real where
"snd_safe_distance = (v⇩o - v⇩e)⇧2 / (2 * (a⇩o - a⇩e))"

lemma fst_leq_snd_safe_distance:
assumes "a⇩e < a⇩o"
shows"fst_safe_distance ≤ snd_safe_distance"
proof -
have "0 ≤ (v⇩o / a⇩o - v⇩e / a⇩e)⇧2" by auto
hence 1: "0 ≤ (v⇩o / a⇩o)⇧2 - 2 * v⇩o * v⇩e / (a⇩o * a⇩e) + (v⇩e / a⇩e)⇧2" by (auto simp add: power_def algebra_simps)
from hyps have "0 ≤ a⇩o * a⇩e"  by (simp add: mult_nonpos_nonpos)
from mult_right_mono[OF 1 this] hyps
have "0 ≤ v⇩o⇧2 * a⇩e / a⇩o - 2 * v⇩o * v⇩e  + v⇩e⇧2 * a⇩o / a⇩e" by (auto simp add: power_def algebra_simps)
with hyps have 2: "(v⇩o⇧2 / (2 * a⇩o) - v⇩e⇧2 / (2 * a⇩e)) * (2 * (a⇩o - a⇩e)) ≤ (v⇩o - v⇩e)⇧2"
by (auto simp add: power_def field_split_simps)
from assms have "0 ≤ 2 * (a⇩o - a⇩e)" by auto
from divide_right_mono[OF 2 this] assms fst_safe_distance_def snd_safe_distance_def
show ?thesis by auto
qed

lemma snd_safe_distance_iff_nonneg_D2:
assumes "a⇩e < a⇩o"
shows "s⇩o - s⇩e ≤ snd_safe_distance ⟷ 0 ≤ D2"
proof -
from snd_safe_distance_def assms pos_le_divide_eq[of "2 * (a⇩o - a⇩e)"]
have "s⇩o - s⇩e ≤ snd_safe_distance ⟷ (s⇩o - s⇩e) * (2 * (a⇩o - a⇩e)) ≤ (v⇩o - v⇩e)⇧2" by auto
also have "... ⟷ 0 ≤ D2" by (auto simp add: algebra_simps)
finally show ?thesis by auto
qed

lemma t_stop_diff_neg_means_leq_D2:
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop" "a⇩e < a⇩o" "0 ≤ D2"
shows "v⇩e - a⇩e / a⇩o * v⇩o < 0 ⟷ sqrt D2 > v⇩e - a⇩e / a⇩o * v⇩o"
proof
assume only_if: "v⇩e - a⇩e / a⇩o * v⇩o < 0"
from assms have "... ≤ sqrt D2" by auto
with only_if show "v⇩e - a⇩e / a⇩o * v⇩o < sqrt D2" by linarith
next
assume if_part: "v⇩e - a⇩e / a⇩o * v⇩o < sqrt D2"
from cond2_imp_gt_fst_sd[OF assms(1) assms(2)] snd_leq_fst_exp have "distance_leq_d2 ≤ s⇩o - s⇩e" by auto
from if_part and sqrt_D2_leq_stop_time_diff [OF ‹a⇩e < a⇩o› _ ‹distance_leq_d2 ≤ s⇩o - s⇩e›]
show " v⇩e - a⇩e / a⇩o * v⇩o < 0"  by linarith
qed

theorem cond_3':
assumes "s⇩o ≤ ego.s_stop" "ego.s_stop < other.s_stop"
shows "collision {0..} ⟷ (a⇩o > a⇩e ∧ v⇩o < v⇩e ∧ s⇩o - s⇩e ≤ snd_safe_distance ∧ v⇩e - a⇩e / a⇩o * v⇩o < 0)"
proof (cases "a⇩o ≤ a⇩e ∨ v⇩o ≥ v⇩e")
case True
with cond_3[OF assms] show ?thesis by auto
next
case False
from ‹¬ (a⇩o ≤ a⇩e ∨ v⇩e ≤ v⇩o)› have "a⇩o > a⇩e" by auto
from ‹¬ (a⇩o ≤ a⇩e ∨ v⇩e ≤ v⇩o)› have "v⇩o < v⇩e" by auto
show ?thesis
proof -
from snd_safe_distance_iff_nonneg_D2 [OF ‹a⇩o > a⇩e›]
have 1: "(a⇩e < a⇩o ∧ v⇩o < v⇩e ∧ s⇩o - s⇩e ≤ snd_safe_distance ∧ v⇩e - a⇩e / a⇩o * v⇩o < 0) ⟷
(a⇩e < a⇩o ∧ v⇩o < v⇩e ∧ 0 ≤ D2 ∧ v⇩e - a⇩e / a⇩o * v⇩o < 0)" by auto

from t_stop_diff_neg_means_leq_D2[OF assms ‹a⇩e < a⇩o›]
have "... = (a⇩e < a⇩o ∧ v⇩o < v⇩e ∧ 0 ≤ D2 ∧ sqrt D2 > v⇩e - a⇩e / a⇩o * v⇩o)" by auto

with 1 cond_3[OF assms] show ?thesis by blast
qed
qed

definition d :: "real ⇒ real" where
"d t = (
if t ≤ 0 then s⇩o - s⇩e
else if t ≤ ego.t_stop ∧ t ≤ other.t_stop then ego_other.p t
else if ego.t_stop ≤ t ∧ t ≤ other.t_stop then other.p t - ego.s_stop
else if other.t_stop ≤ t ∧ t ≤ ego.t_stop then other.s_stop - ego.p t
else other.s_stop - ego.s_stop
)"

lemma d_diff: "d t = other.s t - ego.s t"
by (auto simp: d_def ego.s_eq_s_stop other.s_eq_s_stop ego.s_cond_def other.s_cond_def
movement.p_def field_split_simps)

lemma collision_d: "collision S ⟷ (∃t∈S. d t = 0)"
by (force simp: d_diff collision_def )

lemma collision_restrict: "collision {0..} ⟷ collision {0..max ego.t_stop other.t_stop}"
by (auto simp: max.coboundedI1 ego.t_stop_nonneg min_def
ego.s_eq_s_stop other.s_eq_s_stop collision_def
intro!: bexI[where x = "min t (max (movement.t_stop a⇩e v⇩e) (movement.t_stop a⇩o v⇩o))" for t])

lemma collision_union: "collision (A ∪ B) ⟷ collision A ∨ collision B"
by (auto simp: collision_def)

lemma symbolic_checker:
"collision {0..} ⟷
(quadroot_in 0 (min ego.t_stop other.t_stop) (1/2 * (a⇩o - a⇩e)) (v⇩o - v⇩e) (s⇩o - s⇩e)) ∨
(quadroot_in ego.t_stop other.t_stop (1/2 * a⇩o) v⇩o (s⇩o - ego.s_stop)) ∨
(quadroot_in other.t_stop ego.t_stop (1/2 * a⇩e) v⇩e (s⇩e - other.s_stop))"
(is "_ ⟷ ?q1 ∨ ?q2 ∨ ?q3")
proof -
have *: "{0..max ego.t_stop other.t_stop} =
{0 .. min ego.t_stop other.t_stop} ∪ {ego.t_stop .. other.t_stop} ∪ {other.t_stop .. ego.t_stop}"
using ego.t_stop_nonneg other.t_stop_nonneg
by auto
have "collision {0..min (movement.t_stop a⇩e v⇩e) (movement.t_stop a⇩o v⇩o)} = ?q1"
by (force simp: collision_def quadroot_in_def root_in_def d_def
power2_eq_square field_split_simps movement.p_def movement.s_cond_def)
moreover
have "collision {ego.t_stop .. other.t_stop} = ?q2"
using ego.t_stop_nonneg
by (force simp: collision_def quadroot_in_def root_in_def d_def
ego.s_eq_s_stop movement.s_cond_def movement.p_def)
moreover
have "collision {other.t_stop .. ego.t_stop} = ?q3"
using other.t_stop_nonneg
by (force simp: collision_def quadroot_in_def root_in_def d_def
other.s_eq_s_stop movement.s_cond_def movement.p_def)
ultimately
show ?thesis
unfolding collision_restrict * collision_union
by auto
qed

end

subsection ‹Checker Design›

definition rel_dist_to_stop :: "real ⇒ real ⇒ real" where
"rel_dist_to_stop v a ≡ - v⇧2 / (2 * a)"

context includes floatarith_notation begin
definition rel_dist_to_stop_expr :: "nat ⇒ nat ⇒ floatarith" where
"rel_dist_to_stop_expr v a = Mult (Minus (Power (Var v) 2)) (Inverse (Mult (Num 2) (Var a)))"

definition rel_dist_to_stop' :: "nat ⇒ float interval option ⇒ float interval option ⇒ float interval option" where
"rel_dist_to_stop' p v a = approx p (rel_dist_to_stop_expr 0 1) [v, a]"

lemma rel_dist_to_stop': "interpret_floatarith (rel_dist_to_stop_expr 0 1) [v, a] = rel_dist_to_stop v a"
by (simp add: rel_dist_to_stop_def rel_dist_to_stop_expr_def inverse_eq_divide)

definition first_safe_dist :: "real ⇒ real ⇒ real" where
"first_safe_dist v⇩e a⇩e ≡ rel_dist_to_stop v⇩e a⇩e"

definition second_safe_dist :: "real ⇒ real ⇒ real ⇒ real ⇒ real" where
"second_safe_dist v⇩e a⇩e v⇩o a⇩o ≡ rel_dist_to_stop v⇩e a⇩e - rel_dist_to_stop v⇩o a⇩o"

definition second_safe_dist_expr :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ floatarith" where
"second_safe_dist_expr ve ae vo ao = Add (rel_dist_to_stop_expr ve ae) (Minus (rel_dist_to_stop_expr vo ao))"

definition second_safe_dist' :: "nat ⇒ float interval option ⇒ float interval option
⇒ float interval option ⇒ float interval option ⇒ float interval option" where
"second_safe_dist' p v⇩e a⇩e v⇩o a⇩o = approx p (second_safe_dist_expr 0 1 2 3) [v⇩e, a⇩e, v⇩o, a⇩o]"

lemma second_safe_dist':
"interpret_floatarith (second_safe_dist_expr 0 1 2 3) [v, a, v', a'] = second_safe_dist v a v' a'"
by (simp add: second_safe_dist_def second_safe_dist_expr_def rel_dist_to_stop_def rel_dist_to_stop_expr_def inverse_eq_divide)

definition t_stop :: "real ⇒ real ⇒ real" where
"t_stop v a ≡ - v / a"

definition t_stop_expr :: "nat ⇒ nat ⇒ floatarith" where
"t_stop_expr v a = Minus (Mult (Var v) (Inverse (Var a)))"
end

definition s_stop :: "real ⇒ real ⇒ real ⇒ real" where
"s_stop s v a ≡ s + rel_dist_to_stop v a"

definition discriminant :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real" where
"discriminant s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ≡ (v⇩o - v⇩e)⇧2 - 2 * (a⇩o - a⇩e) * (s⇩o - s⇩e)"

definition suff_cond_safe_dist2 :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
"suff_cond_safe_dist2 s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ≡
let D2 = discriminant s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o
in ¬ (a⇩e < a⇩o ∧ v⇩o < v⇩e ∧ 0 ≤ D2 ∧ v⇩e - a⇩e / a⇩o * v⇩o < sqrt D2
)"

lemma less_sqrt_iff: "y ≥ 0 ⟹ x < sqrt y ⟷ (x ≥ 0 ⟶ x⇧2 < y)"
by (smt real_le_lsqrt real_less_rsqrt real_sqrt_ge_zero)

lemma suff_cond_safe_dist2_code[code]:
"suff_cond_safe_dist2 s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o =
(let D2 = discriminant s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o in
(a⇩e < a⇩o ⟶ v⇩o < v⇩e ⟶ 0 ≤ D2 ⟶ (v⇩e - a⇩e / a⇩o * v⇩o ≥ 0 ∧ (v⇩e - a⇩e / a⇩o * v⇩o)⇧2 ≥ D2)))"
using real_sqrt_ge_zero real_less_rsqrt less_sqrt_iff
by (auto simp: suff_cond_safe_dist2_def Let_def)

text ‹
There are two expressions for safe distance. The first safe distance ‹first_safe_dist› is always valid.
Whenever the distance is bigger than ‹first_safe_dist›, it is guarantee to be collision free.
The second one is ‹second_safe_dist›. If the sufficient condition ‹suff_cond_safe_dist2› is satisfied and
the distance is bigger than ‹second_safe_dist›, it is guaranteed to be collision free.
›

definition check_precond :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
"check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ⟷ s⇩o > s⇩e ∧ 0 ≤ v⇩e ∧ 0 ≤ v⇩o ∧ a⇩e < 0 ∧ a⇩o < 0 "

lemma check_precond_safe_distance:
"check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o = safe_distance a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o"
proof
assume "safe_distance a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o"
then interpret safe_distance a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o .
show "check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o"
by (auto simp: check_precond_def in_front nonneg_vel_ego other.nonneg_vel ego.decel other.decel)
qed (unfold_locales; auto simp: check_precond_def)

subsubsection ‹Prescriptive Checker›

definition checker :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
"checker s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ≡
let distance   = s⇩o - s⇩e;
precond    = check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o;
safe_dist1 = first_safe_dist v⇩e a⇩e;
safe_dist2 = second_safe_dist v⇩e a⇩e v⇩o a⇩o;
cond2      = suff_cond_safe_dist2 s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o
in precond ∧ (safe_dist1 < distance ∨ (safe_dist2 < distance ∧ distance ≤ safe_dist1 ∧ cond2))"

lemma aux_logic:
assumes "a ⟹ b"
assumes "b ⟹ a ⟷ c"
shows "a ⟷ b ∧ c"
using assms by blast

theorem soundness_correctness:
"checker s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ⟷ check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ∧ safe_distance.no_collision a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o {0..}"
proof (rule aux_logic, simp add: checker_def Let_def)
assume cp: "check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o"
then have in_front': "s⇩o > s⇩e"
and nonneg_vel_ego: "0 ≤ v⇩e"
and nonneg_vel_other: "0 ≤ v⇩o"
and decelerate_ego: "a⇩e < 0"
and decelerate_other: "a⇩o < 0"
by (auto simp: check_precond_def)

from in_front' have in_front: "0 < s⇩o - s⇩e" by arith

interpret safe_distance a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o by (unfold_locales; fact)
interpret ego: braking_movement a⇩e v⇩e s⇩e by (unfold_locales; fact)
interpret other: braking_movement a⇩o v⇩o s⇩o by (unfold_locales; fact)

have "ego.p_max < s⇩o ∨ other.p_max ≤ ego.p_max ∨ s⇩o ≤ ego.p_max ∧ ego.p_max < other.p_max"
by arith
then show "checker s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o = safe_distance.no_collision a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o {0..}"
proof (elim disjE)
assume "ego.p_max < s⇩o"
then have "checker s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o"
using ‹a⇩e < 0› cp
by (simp add: checker_def Let_def first_safe_dist_def rel_dist_to_stop_def ego.p_max_def
ego.p_def ego.t_stop_def algebra_simps power2_eq_square)
moreover
have "no_collision {0..}"
using ‹ego.p_max < s⇩o›
by (intro cond_1) (auto simp: ego.s_t_stop)
ultimately show ?thesis by auto
next
assume "other.p_max ≤ ego.p_max"
then have "¬ checker s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o"
using ‹a⇩e < 0› ‹a⇩o < 0› other.nonneg_vel
by (auto simp add: checker_def Let_def first_safe_dist_def second_safe_dist_def
rel_dist_to_stop_def movement.p_max_def
movement.p_def movement.t_stop_def algebra_simps power2_eq_square)
(smt divide_nonneg_neg mult_nonneg_nonneg)
moreover have "collision {0..}"
using ‹other.p_max ≤ ego.p_max›
by (intro cond_2) (auto simp: other.s_t_stop ego.s_t_stop)
ultimately show ?thesis by auto
next
assume H: "s⇩o ≤ ego.p_max ∧ ego.p_max < other.p_max"
then have "checker s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o = (¬ (a⇩e < a⇩o ∧ v⇩o < v⇩e ∧ 0 ≤ D2 ∧ v⇩e - a⇩e / a⇩o * v⇩o < sqrt D2))"
using ‹a⇩e < 0› ‹a⇩o < 0› cp
by (simp add: checker_def Let_def first_safe_dist_def rel_dist_to_stop_def ego.p_max_def
ego.p_def ego.t_stop_def algebra_simps power2_eq_square second_safe_dist_def
suff_cond_safe_dist2_def discriminant_def not_less other.p_max_def other.p_def other.t_stop_def)
also have "… = no_collision {0..}"
using H
unfolding Not_eq_iff
by (intro cond_3[symmetric]) (auto simp: ego.s_t_stop other.s_t_stop)
finally show ?thesis by auto
qed
qed

definition checker2 :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
"checker2 s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ≡
let distance   = s⇩o - s⇩e;
precond    = check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o;
safe_dist1 = first_safe_dist v⇩e a⇩e;
safe_dist2 = second_safe_dist v⇩e a⇩e v⇩o a⇩o;
safe_dist3 = - rel_dist_to_stop (v⇩o - v⇩e) (a⇩o - a⇩e)
in
if ¬ precond then False
else if distance > safe_dist1 then True
else if a⇩o > a⇩e ∧ v⇩o < v⇩e ∧ v⇩e - a⇩e / a⇩o * v⇩o < 0 then distance > safe_dist3
else distance > safe_dist2"

theorem checker_eq_checker2: "checker s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o ⟷ checker2 s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o"
proof (cases "check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o")
case False
with checker_def checker2_def
show ?thesis by auto
next
case True
with check_precond_def safe_distance_def
have "safe_distance a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o"  by (simp add: check_precond_safe_distance)

from this interpret safe_distance a⇩e v⇩e s⇩e a⇩o v⇩o s⇩o by auto
interpret ego: braking_movement a⇩e v⇩e s⇩e by (unfold_locales; fact)
interpret other: braking_movement a⇩o v⇩o s⇩o by (unfold_locales; fact)

from ‹check_precond s⇩e v⇩e a⇩e s⇩o v⇩o a⇩o›  cond_3 cond_3'[symmetric] fst_leq_snd_safe_distance
ego.s_t_stop ego.p_max_def ego.p_def ego.t_stop_def hyps other.s_t_stop other.p_max_def other.p_def
other.t_stop_def checker2_def checker_def suff_cond_safe_dist2_def fst_safe_distance_def
first_safe_dist_def snd_safe_distance_def second_safe_dist_def rel_dist_to_stop_def discriminant_def
show ?thesis
by (auto simp add:power_def Let_def split: if_splits)
qed

definition checker3 :: "real ⇒ real ⇒ real ⇒ real ```