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_left_pos)+
  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 ⇒ real ⇒ real ⇒ bool" where
  "checker3 se ve ae so vo ao ≡ 
    let distance = so - se;
        precond  = check_precond se ve ae so vo ao;
        s_stop_e = se + rel_dist_to_stop ve ae;
        s_stop_o = so + rel_dist_to_stop vo ao 
    in precond ∧ (s_stop_e < so 
               ∨ (so ≤ s_stop_e ∧ s_stop_e < s_stop_o ∧
                 (¬(ao > ae ∧ vo < ve ∧ ve - ae / ao * vo < 0 ∧ distance * (ao - ae) ≤ (vo - ve)2 / 2))))"

theorem checker2_eq_checker3:
  "checker2 se ve ae so vo ao ⟷ checker3 se ve ae so vo ao"
  apply (auto simp: checker2_def checker3_def Let_def first_safe_dist_def not_less
    suff_cond_safe_dist2_def second_safe_dist_def rel_dist_to_stop_def check_precond_def)
proof goal_cases
  case 1
  then interpret safe_distance
    by unfold_locales auto
  from fst_leq_snd_safe_distance 1
  show ?case
    by (auto simp: fst_safe_distance_def snd_safe_distance_def)
next
  case 2
  then interpret safe_distance
    by unfold_locales auto
  from fst_leq_snd_safe_distance 2
  show ?case
    by (auto simp: fst_safe_distance_def snd_safe_distance_def field_split_simps)
next
  case 3
  then interpret safe_distance
    by unfold_locales auto
  from fst_leq_snd_safe_distance 3
  show ?case
    by (auto simp: fst_safe_distance_def snd_safe_distance_def field_split_simps)
qed

subsubsection ‹Approximate Checker›

lemma checker2_def': "checker2 a b c d e f = (
  let distance   = d - a;
      precond    = check_precond a b c d e f;
      safe_dist1 = first_safe_dist b c;
      safe_dist2 = second_safe_dist b c e f;
      C          = c < f ∧ e < b ∧ b * f > c * e;
      P1         = (e - b)2 < 2 * distance * (f - c);
      P2         = - b2 / c + e2 / f < 2 * distance
  in precond ∧ (safe_dist1 < distance ∨
                safe_dist1 ≥ distance ∧ (C ∧ P1 ∨ ¬C ∧ P2)))"
  unfolding checker2_def
  by (auto simp: Let_def field_split_simps check_precond_def second_safe_dist_def
    rel_dist_to_stop_def)

lemma power2_less_sqrt_iff: "(x::real)2 < y ⟷ (y ≥ 0 ∧ abs x < sqrt y)"
  apply (auto simp: real_less_rsqrt abs_real_def less_sqrt_iff)
   apply (meson le_less le_less_trans not_less power2_less_0)+
  done

schematic_goal checker_form: "interpret_form ?x ?y ⟹ checker se ve ae so vo ao"
  unfolding checker_eq_checker2 checker2_eq_checker3 checker3_def check_precond_def first_safe_dist_def second_safe_dist_def
    suff_cond_safe_dist2_def Let_def t_stop_def s_stop_def
    rel_dist_to_stop_def
    discriminant_def
    not_le not_less
    de_Morgan_conj
    de_Morgan_disj
    power2_less_sqrt_iff
  apply (tactic ‹(Reification.tac @{context} @{thms interpret_form.simps interpret_floatarith.simps interpret_floatarith_divide interpret_floatarith_diff}) NONE 1›)
  apply assumption
  done

context includes floatarith_notation begin                                            
definition "checker' p se ve ae so vo ao = approx_form p
           (Conj (Conj (Less (Var (Suc (Suc 0))) (Var (Suc (Suc (Suc 0)))))
                   (Conj (LessEqual (Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) (Var (Suc (Suc (Suc (Suc (Suc 0)))))))
                     (Conj (LessEqual (Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) (Var (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))
                       (Conj (Less (Var 0) (Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))
                         (Less (Var (Suc 0)) (Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))
             (Disj (Less (Add (Var (Suc (Suc 0)))
                           (Mult (Minus (Power (Var (Suc (Suc (Suc (Suc (Suc 0)))))) 2)) (Inverse (Mult (Var (Suc (Suc (Suc (Suc 0))))) (Var 0)))))
                     (Var (Suc (Suc (Suc 0)))))
               (Conj (LessEqual (Var (Suc (Suc (Suc 0))))
                       (Add (Var (Suc (Suc 0)))
                         (Mult (Minus (Power (Var (Suc (Suc (Suc (Suc (Suc 0)))))) 2)) (Inverse (Mult (Var (Suc (Suc (Suc (Suc 0))))) (Var 0))))))
                 (Conj (Less (Add (Var (Suc (Suc 0)))
                               (Mult (Minus (Power (Var (Suc (Suc (Suc (Suc (Suc 0)))))) 2)) (Inverse (Mult (Var (Suc (Suc (Suc (Suc 0))))) (Var 0)))))
                         (Add (Var (Suc (Suc (Suc 0))))
                           (Mult (Minus (Power (Var (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) 2))
                             (Inverse (Mult (Var (Suc (Suc (Suc (Suc 0))))) (Var (Suc 0)))))))
                   (Disj (LessEqual (Var (Suc 0)) (Var 0))
                     (Disj (LessEqual (Var (Suc (Suc (Suc (Suc (Suc 0)))))) (Var (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))
                       (Disj (LessEqual (Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))
                               (Add (Var (Suc (Suc (Suc (Suc (Suc 0))))))
                                 (Minus (Mult (Mult (Var 0) (Inverse (Var (Suc 0)))) (Var (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))
                         (Less (Mult (Power (Add (Var (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) (Minus (Var (Suc (Suc (Suc (Suc (Suc 0)))))))) 2)
                                 (Inverse (Var (Suc (Suc (Suc (Suc 0)))))))
                           (Mult (Add (Var (Suc (Suc (Suc 0)))) (Minus (Var (Suc (Suc 0))))) (Add (Var (Suc 0)) (Minus (Var 0))))))))))))
  ([ae, ao, se, so, Interval' (Float 2 0) (Float 2 0), ve, vo, Interval' (Float 0 1) (Float 0 1)]) (replicate 8 0)"

lemma less_Suc_iff_disj: "i < Suc x ⟷ i = x ∨ i < x"
  by auto

lemma checker'_soundness_correctness:
  assumes "a ∈ {real_of_float al .. real_of_float au}"
  assumes "b ∈ {real_of_float bl .. real_of_float bu}"
  assumes "c ∈ {real_of_float cl .. real_of_float cu}"
  assumes "d ∈ {real_of_float dl .. real_of_float du}"
  assumes "e ∈ {real_of_float el .. real_of_float eu}"
  assumes "f ∈ {real_of_float fl .. real_of_float fu}"
  assumes chk: "checker' p (Interval' al au) (Interval' bl bu) (Interval' cl cu) (Interval' dl du) (Interval' el eu) (Interval' fl fu)"
  shows "checker a b c d e f"
  apply (rule checker_form)
  apply (rule approx_form_aux)
   apply (rule chk[unfolded checker'_def])
  using assms(1-6)
  unfolding bounded_by_def
proof (auto split: option.splits)
  fix i x2
  assume *: "[Interval' cl cu, Interval' fl fu, Interval' al au, Interval' dl du, 
           Interval' (Float 2 0) (Float 2 0), Interval' bl bu, Interval' el eu, Interval' 0 0] ! i = Some x2"
  assume " i < Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))"
  then consider "i = 0" | "i = 1" | "i = 2" | "i = 3" | "i = 4" | "i = 5" | "i = 6" | "i = 7"
    by linarith
  thus " [c, f, a, d, 2, b, e, 0] ! i ∈r x2"
    apply cases using assms(1-6) *
    by (auto intro!: in_real_intervalI dest!: Interval'_eq_Some)
qed
    
lemma approximate_soundness_correctness:
  assumes "a ∈ {real_of_float al .. real_of_float au}"
  assumes "b ∈ {real_of_float bl .. real_of_float bu}"
  assumes "c ∈ {real_of_float cl .. real_of_float cu}"
  assumes "d ∈ {real_of_float dl .. real_of_float du}"
  assumes "e ∈ {real_of_float el .. real_of_float eu}"
  assumes "f ∈ {real_of_float fl .. real_of_float fu}"
  assumes chk: "checker' p (Interval' al au) (Interval' bl bu) (Interval' cl cu) (Interval' dl du) (Interval' el eu) (Interval' fl fu)"
  shows checker'_precond: "check_precond a b c d e f"
    and checker'_no_collision: "safe_distance.no_collision c b a f e d  {0..}"
  unfolding atomize_conj
  apply (subst soundness_correctness[symmetric])
  using checker'_soundness_correctness[OF assms]
  by (auto simp: checker_def Let_def)

subsubsection ‹Symbolic Checker›

definition symbolic_checker :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
  "symbolic_checker se ve ae so vo ao ≡
    let e_stop = - ve / ae;
        o_stop = - vo / ao
    in check_precond se ve ae so vo ao ∧
       (¬quadroot_in 0 (min e_stop o_stop) (1/2 * (ao - ae)) (vo - ve) (so - se) ∧
       ¬quadroot_in e_stop o_stop (1/2 * ao) vo (so - movement.p ae ve se e_stop) ∧
       ¬quadroot_in o_stop e_stop (1/2 * ae) ve (se - movement.p ao vo so o_stop))"

theorem symbolic_soundness_correctness:
  "symbolic_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 -
  {
    assume c: "check_precond se ve ae so vo ao"
    then interpret safe_distance ae ve se ao vo so
      by (simp add: check_precond_safe_distance)
    have "symbolic_checker se ve ae so vo ao = no_collision {0..}"
      using c
      unfolding symbolic_checker symbolic_checker_def ego.s_t_stop other.s_t_stop ego.p_max_def other.p_max_def
      by (auto simp: Let_def movement.t_stop_def)
  }
  then show ?thesis
    by (auto simp: symbolic_checker_def Let_def)
qed
end

end