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 = s0 + v0 * t + 1 / 2 * a0 * t2›

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

subsection ‹Quadratic Equations›

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

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

lemma quadratic_eq_zeroes_iff:
  assumes D : "D = b2 - 4 * a * c"
  assumes x1: "x1 = (-b + sqrt D) / (2 * a)"
  assumes x2: "x2 = (-b - sqrt D) / (2 * a)"
  assumes a : "a ≠ 0"
  shows "a * x2 + b * x + c = 0 ⟷ (D ≥ 0 ∧ (x = x1 ∨ x = x2))" (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 * x2 + 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)
  
lemma quadroot_in_sturm[code]:
  "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

lemma check_quadroot_linear:
  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_iff2)+
  finally show ?thesis
    by (simp add: Let_def not_less not_le)
qed 

lemma check_quadroot_nonlinear:
  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])

lemma ncheck_quadroot:
  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) = s0 + v0 * t + 1 / 2 * a0 * t2›
  
  Input parameters: 
   ▪ ‹s0›: initial distance
   ▪ ‹v0›: 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 ‹s0›. 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 * t2"

lemma p_all_zeroes:
  assumes D: "D = v2 - 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 - v2 / 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
  by (simp add:has_real_derivative_iff_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 - v2 / a / 2"]) 
    show " s0 - v2 / a / 2 = p_max" using p_max_eq by auto
  next
    have "0 ≤ - v2 / a / 2" using decel zero_le_square[of v]
    proof -
      have f1: "a ≤ 0"
        using ‹a < 0› by linarith
      have "(- 1 * v2 ≤ 0) = (0 ≤ v2)"
        by auto
      then have "0 ≤ - 1 * v2 / a"
        using f1 by (meson zero_le_divide_iff zero_le_power2)
      then show ?thesis
        by force
    qed
    thus "s0 ≤ s0 - v2 / 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 * x2 ≤ v * y + 1 / 2 * a * y2"
    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 * (x2 - y2) "
    using ‹x ≤ y› by sos
  hence "v * y + 1/2 * a * y2 ≤ v * x + 1/2 * a * x2"
    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 * x2 < v * y + 1 / 2 * a * y2"
    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 * (x2 - y2) "
    using ‹x < y› by sos
  hence "v * y + 1/2 * a * y2 < v * x + 1/2 * a * x2"
    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]
  by(simp add: has_real_derivative_iff_has_vector_derivative)
  
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]  
  by(simp add:has_real_derivative_iff_has_vector_derivative)

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 ae ve se :: real
  fixes ao vo so :: real
  assumes nonneg_vel_ego   : "0 ≤ ve"
  assumes nonneg_vel_other : "0 ≤ vo"
  assumes decelerate_ego   : "ae < 0"
  assumes decelerate_other : "ao < 0"
  assumes in_front         : "se < so"
begin

lemmas hyps =
  nonneg_vel_ego   
  nonneg_vel_other 
  decelerate_ego   
  decelerate_other 
  in_front

sublocale ego: braking_movement ae ve se by (unfold_locales; rule hyps)
sublocale other: braking_movement ao vo so by (unfold_locales; rule hyps)
sublocale ego_other: movement "ao - ae" "vo - ve" "so - se" 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 < so ⟹ 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 "… < so"
  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]: "se < so ⟹ 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 ≡ (vo - ve)^2 - 2 * (ao - ae) * (so - se)"

abbreviation tD' :: "real" where
  "tD' ≡ sqrt (2 * (ego.s_stop - other.s_stop) / ao)"

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 "so ≤ 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 "so ≤ 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 "so ≤ 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 "so ≤ ego.s_stop" "ego.s_stop < other.s_stop"
  shows "collision {0..} ⟷ (ao > ae ∧ vo < ve ∧ 0 ≤ D2 ∧ sqrt D2 > ve - ae / ao * vo)"
proof -
  have "vo ≠ 0"
    using assms(1) assms(2) movement.s_def movement.t_stop_def by auto
  with hyps have "vo > 0" by auto
  note hyps = hyps this
  define t1 where "t1 = (- (vo - ve) + sqrt D2) / (ao - ae)"
  define t2 where "t2 = (- (vo - ve) - sqrt D2) / (ao - ae)"
  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 = (vo - ve)2 - 4 * ((ao - ae) / 2) * (so - se)" by simp
  define D where "D = D2"
  note D = D_def[symmetric]
  define x1 where "x1 ≡ (- (vo - ve) + sqrt D2) / (2 * ((ao - ae) / 2))"
  define x2 where "x2 ≡ (- (vo - ve) - sqrt D2) / (2 * ((ao - ae) / 2))"
  have x2: "x2 =(- (vo - ve) - sqrt D2) / (ao - ae)"
    by (simp add: x2_def field_split_simps)
  have x1: "x1 =(- (vo - ve) + sqrt D2) / (ao - ae)"
    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 "… ⟷ (ao > ae ∧ vo < ve ∧ 0 ≤ D2 ∧ sqrt D2 > ve - ae / ao * vo)"
  proof safe
    assume H: "ae < ao" "vo < ve" "0 ≤ D2"
    assume sqrt: "sqrt D2 > ve - ae / ao * vo"
    have nz: "(ao - ae) / 2 ≠ 0" using ‹ae < ao› 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 < - (ve / ae)" "t < - (vo / ao)" "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 * (ao - ae) * t2 + (vo - ve) * t + (so - se))"
      by (simp add: algebra_simps)
    show "ao > ae"
    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 "ao > ae" by (simp add: algebra_simps)
    qed
    have rewr: "4 * ((ao - ae) / 2) = 2 * (ao - ae)" by simp
    from ‹ao > ae› ‹ego_other.p t = 0› ego_other.p_all_zeroes[OF D2[symmetric], of t]
    have "0 ≤ D2" and disj: "(t = (- (vo - ve) + sqrt D2) / (ao - ae) ∨ t = (- (vo - ve) - sqrt D2) / (ao - ae))"
      using hyps assms
      unfolding rewr by simp_all
    show "0 ≤ D2" by fact
    from add_strict_mono[OF ‹t < - (ve / ae)› ‹t < - (vo / ao)›] ‹0 < t› ‹ao > ae›
    have "0 < - (ve / ae) + - (vo / ao)" by (simp add: divide_simps)
    then have "0 > ve * ao + ae * vo" using hyps
      by (simp add: field_split_simps split: if_splits)
    show "vo < ve"
      using ‹ae < ao› ‹movement.p (ao - ae) (vo - ve) (so - se) 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 = (- (vo - ve) - sqrt D2) / (ao - ae)"
      then show ?thesis
        using ‹t < ?min›
        by (simp add: x2)
    next
      assume "t = (- (vo - ve) + sqrt D2) / (ao - ae)"
      also have "… ≥ x2"
        unfolding x2
        apply (rule divide_right_mono)
         apply (subst (2) diff_conv_add_uminus)
         apply (rule add_left_mono)
        using ‹ao > ae› ‹D2 ≥ 0›
        by auto
      also (xtrans) note ‹t < ?min›
      finally show ?thesis .
    qed
    then show "sqrt D2 > ve - ae / ao * vo"
      using hyps ‹ao > ae›
      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 = - ve2 / (2 * ae)"

lemma absolute_safe_distance:
  assumes "so - se > absolute_safe_distance"
  shows "no_collision {0..}"
  proof -
  from assms hyps absolute_safe_distance_def have "ego.s_stop < so" 
    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 = vo2 / (2 * ao) - ve2 / (2 * ae)"

definition distance_leq_d2 :: real where
  "distance_leq_d2 = (ae + ao) / (2 * ao2) * vo2 - vo * ve / ao"

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_stop2 ≤ other.t_stop2 - 2 * other.t_stop * ego.t_stop" by (simp add:power_def algebra_simps) 
  with hyps(3) have "- ego.t_stop2 * (ae / 2) ≥ (other.t_stop2 - 2 * other.t_stop * ego.t_stop) * (ae / 2)"
    by (smt half_gt_zero_iff mult_le_cancel_right)
  with ego.t_stop_def other.t_stop_def hyps 
  have "- ve2 / (2 * ae) ≥ ae * vo2 / (2 * ao2) - vo * ve / ao" by (simp add:power_def algebra_simps)
  with fst_safe_distance_def distance_leq_d2_def
  have 1: "fst_safe_distance ≥  ae * vo2 / (2 * ao2) - vo * ve / ao + vo2 / (2 * ao)" by (auto simp add:algebra_simps)
  have "ae * vo2 / (2 * ao2) - vo * ve / ao + vo2 / (2 * ao) = distance_leq_d2" (is "?LHS = _")
  proof -
    have "?LHS = ae * vo2 / (2 * ao2) - vo * ve / ao + ao * vo2 / (2 * ao2)"  
      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 "ae < ao"
  assumes "0 ≤ ve - ae / ao * vo "
  assumes "so - se ≥ distance_leq_d2"
  shows "sqrt D2 ≤ ve - ae / ao * vo"
proof -
  from assms have "- 2 * (ao - ae) * (so - se) ≤ - 2 * (ao - ae) * distance_leq_d2" (is "?L ≤ ?R") 
  by simp
  hence "D2 ≤ (vo - ve)2 - 2 * (ao - ae) * distance_leq_d2" by (simp add: algebra_simps)
  also have "... = (ve - ae / ao * vo)2"
  proof -
    from distance_leq_d2_def
    have 1: "(vo - ve)2 - 2 * (ao - ae) * distance_leq_d2 = 
             (vo - ve)2 - (ao - ae) * (ae + ao) / ao2 * vo2 + 2 * (ao - ae) * vo * ve / ao"
      by (auto simp add: field_split_simps)
    with hyps(4) have "... = (ve - ae / ao * vo)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 "so ≤ ego.s_stop" "ego.s_stop < other.s_stop"
  shows "vo ≠ 0"
proof (rule ccontr)
  assume "¬ vo ≠ 0"
  with other.s_def other.t_stop_def have "other.s_stop = so" by auto
  with assms(2) have "ego.s_stop < so" by auto
  with assms(1) show "False" by auto
qed

lemma cond2_imp_gt_fst_sd:
  assumes "so ≤ ego.s_stop" "ego.s_stop < other.s_stop"
  shows "fst_safe_distance < so - se"
proof (cases "ve ≠ 0")
  case True
  from fst_safe_distance_def assms ego.s_def ego.t_stop_pos[OF ‹ve ≠ 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 = vo2 / (2 * ao)" by auto
  also have "... ≤ 0"  by (simp add: divide_nonneg_neg hyps)
  also have "... < so - se" 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 = (vo - ve)2 / (2 * (ao - ae))"

lemma fst_leq_snd_safe_distance:
  assumes "ae < ao"
  shows"fst_safe_distance ≤ snd_safe_distance"
proof -
  have "0 ≤ (vo / ao - ve / ae)2" by auto
  hence 1: "0 ≤ (vo / ao)2 - 2 * vo * ve / (ao * ae) + (ve / ae)2" by (auto simp add: power_def algebra_simps)
  from hyps have "0 ≤ ao * ae"  by (simp add: mult_nonpos_nonpos)  
  from mult_right_mono[OF 1 this] hyps
  have "0 ≤ vo2 * ae / ao - 2 * vo * ve  + ve2 * ao / ae" by (auto simp add: power_def algebra_simps)
  with hyps have 2: "(vo2 / (2 * ao) - ve2 / (2 * ae)) * (2 * (ao - ae)) ≤ (vo - ve)2"
    by (auto simp add: power_def field_split_simps)
  from assms have "0 ≤ 2 * (ao - ae)" 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 "ae < ao"
  shows "so - se ≤ snd_safe_distance ⟷ 0 ≤ D2"
proof -
  from snd_safe_distance_def assms pos_le_divide_eq[of "2 * (ao - ae)"]
  have "so - se ≤ snd_safe_distance ⟷ (so - se) * (2 * (ao - ae)) ≤ (vo - ve)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 "so ≤ ego.s_stop" "ego.s_stop < other.s_stop" "ae < ao" "0 ≤ D2"
  shows "ve - ae / ao * vo < 0 ⟷ sqrt D2 > ve - ae / ao * vo"
proof
  assume only_if: "ve - ae / ao * vo < 0"
  from assms have "... ≤ sqrt D2" by auto
  with only_if show "ve - ae / ao * vo < sqrt D2" by linarith
next
  assume if_part: "ve - ae / ao * vo < sqrt D2"
  from cond2_imp_gt_fst_sd[OF assms(1) assms(2)] snd_leq_fst_exp have "distance_leq_d2 ≤ so - se" by auto
  from if_part and sqrt_D2_leq_stop_time_diff [OF ‹ae < ao› _ ‹distance_leq_d2 ≤ so - se›]
  show " ve - ae / ao * vo < 0"  by linarith
qed

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

    from t_stop_diff_neg_means_leq_D2[OF assms ‹ae < ao›]
    have "... = (ae < ao ∧ vo < ve ∧ 0 ≤ D2 ∧ sqrt D2 > ve - ae / ao * vo)" 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 so - se
    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 ae ve) (movement.t_stop ao vo))" 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 * (ao - ae)) (vo - ve) (so - se)) ∨
    (quadroot_in ego.t_stop other.t_stop (1/2 * ao) vo (so - ego.s_stop)) ∨
    (quadroot_in other.t_stop ego.t_stop (1/2 * ae) ve (se - 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 ae ve) (movement.t_stop ao vo)} = ?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 ≡ - v2 / (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 ve ae ≡ rel_dist_to_stop ve ae"

definition second_safe_dist :: "real ⇒ real ⇒ real ⇒ real ⇒ real" where
  "second_safe_dist ve ae vo ao ≡ rel_dist_to_stop ve ae - rel_dist_to_stop vo ao"

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 ve ae vo ao = approx p (second_safe_dist_expr 0 1 2 3) [ve, ae, vo, ao]"

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 se ve ae so vo ao ≡ (vo - ve)2 - 2 * (ao - ae) * (so - se)"

definition suff_cond_safe_dist2 :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
  "suff_cond_safe_dist2 se ve ae so vo ao ≡ 
    let D2 = discriminant se ve ae so vo ao 
    in ¬ (ae < ao ∧ vo < ve ∧ 0 ≤ D2 ∧ ve - ae / ao * vo < sqrt D2
  )"

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

lemma suff_cond_safe_dist2_code[code]:
  "suff_cond_safe_dist2 se ve ae so vo ao =
    (let D2 = discriminant se ve ae so vo ao in
      (ae < ao ⟶ vo < ve ⟶ 0 ≤ D2 ⟶ (ve - ae / ao * vo ≥ 0 ∧ (ve - ae / ao * vo)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 se ve ae so vo ao ⟷ so > se ∧ 0 ≤ ve ∧ 0 ≤ vo ∧ ae < 0 ∧ ao < 0 "

lemma check_precond_safe_distance: 
  "check_precond se ve ae so vo ao = safe_distance ae ve se ao vo so"
proof
  assume "safe_distance ae ve se ao vo so"
  then interpret safe_distance ae ve se ao vo so .
  show "check_precond se ve ae so vo ao"
    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 se ve ae so vo ao ≡
    let distance   = so - se;
        precond    = check_precond se ve ae so vo ao;
        safe_dist1 = first_safe_dist ve ae; 
        safe_dist2 = second_safe_dist ve ae vo ao;
        cond2      = suff_cond_safe_dist2 se ve ae so vo ao 
    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 se ve ae so vo ao ⟷ check_precond se ve ae so vo ao ∧ safe_distance.no_collision ae ve se ao vo so {0..}"
proof (rule aux_logic, simp add: checker_def Let_def)
  assume cp: "check_precond se ve ae so vo ao"
  then have in_front': "so > se"
    and nonneg_vel_ego: "0 ≤ ve"
    and nonneg_vel_other: "0 ≤ vo"
    and decelerate_ego: "ae < 0"
    and decelerate_other: "ao < 0"
    by (auto simp: check_precond_def)

  from in_front' have in_front: "0 < so - se" by arith

  interpret safe_distance ae ve se ao vo so by (unfold_locales; fact)
  interpret ego: braking_movement ae ve se by (unfold_locales; fact)
  interpret other: braking_movement ao vo so by (unfold_locales; fact)

  have "ego.p_max < so ∨ other.p_max ≤ ego.p_max ∨ so ≤ ego.p_max ∧ ego.p_max < other.p_max"
    by arith
  then show "checker se ve ae so vo ao = safe_distance.no_collision ae ve se ao vo so {0..}"
  proof (elim disjE)
    assume "ego.p_max < so"
    then have "checker se ve ae so vo ao"
      using ‹ae < 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 < so›
      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 se ve ae so vo ao"
      using ‹ae < 0› ‹ao < 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: "so ≤ ego.p_max ∧ ego.p_max < other.p_max"
    then have "checker se ve ae so vo ao = (¬ (ae < ao ∧ vo < ve ∧ 0 ≤ D2 ∧ ve - ae / ao * vo < sqrt D2))"
      using ‹ae < 0› ‹ao < 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 se ve ae so vo ao ≡ 
    let distance   = so - se;
        precond    = check_precond se ve ae so vo ao;
        safe_dist1 = first_safe_dist ve ae; 
        safe_dist2 = second_safe_dist ve ae vo ao;
        safe_dist3 = - rel_dist_to_stop (vo - ve) (ao - ae) 
    in
      if ¬ precond then False 
      else if distance > safe_dist1 then True 
      else if ao > ae ∧ vo < ve ∧ ve - ae / ao * vo < 0 then distance > safe_dist3
      else distance > safe_dist2"

theorem checker_eq_checker2: "checker se ve ae so vo ao ⟷ checker2 se ve ae so vo ao"
proof (cases "check_precond se ve ae so vo ao")
  case False
  with checker_def checker2_def
  show ?thesis by auto
next
  case True
  with check_precond_def safe_distance_def 
  have "safe_distance ae ve se ao vo so"  by (simp add: check_precond_safe_distance)
  
  from this interpret safe_distance ae ve se ao vo so by auto
  interpret ego: braking_movement ae ve se by (unfold_locales; fact)
  interpret other: braking_movement ao vo so by (unfold_locales; fact)

  from ‹check_precond se ve ae so vo ao›  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 ⇒