Session Safe_Distance

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_field_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_field_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_field_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_field_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_field_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_field_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_field_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_field_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 "x0. 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..}  (t0. 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 "t0. 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  (tS. 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

Theory Safe_Distance_Reaction

✐‹creator "Albert Rizaldi" "Fabian Immler›

section ‹Safe Distance with Reaction Time›

theory Safe_Distance_Reaction
imports
  Safe_Distance
begin

subsection ‹Normal Safe Distance›
                                    
locale safe_distance_normal = safe_distance +
  fixes δ :: real
  assumes pos_react: "0 < δ"
begin

sublocale ego2: braking_movement ae ve "(ego.q δ)" ..

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

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

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

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

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

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

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

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

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

lemma s_delayed_has_vector_derivative' [derivative_intros]:
  assumes "δ  t"
  shows "((ego2.s  τ) has_vector_derivative (ego2.s'  τ) t) (at t within {δ..})"
  using s_delayed_has_real_derivative'[OF assms]
  by (simp add:has_field_derivative_iff_has_vector_derivative)
  
definition u :: "real  real" where
  "u t = (     if t  0 then se
          else if t  δ then ego.q t 
          else          (ego2.s  τ) t)"

lemma init_u: "t  0  u t = se" unfolding u_def by auto

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    ultimately show ?thesis by auto
  qed
qed

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

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

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

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

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

definition collision_react :: "real set  bool" where
  "collision_react time_set  (ttime_set. u t = other.s t )"

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

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

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

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

theorem cond_1r : "u_max < so  no_collision_react {0..}"
proof (rule no_collision_reactI, simp)
  fix t :: real
  assume "0  t"
  have "u t  u_max" by (rule u_max)
  also assume "... < 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 "u t  other.s t"
    by simp
qed

definition safe_distance_1r :: real where 
  "safe_distance_1r = ve * δ - ve2 / ae / 2"

lemma sd_1r_eq: "(so - se > safe_distance_1r) = (u_max < so)"
proof -
  have "(so - se > safe_distance_1r) = (so - se > ve * δ - ve2 / ae / 2)" unfolding safe_distance_1r_def by auto
  moreover have "... = (se + ve * δ - ve2 / ae / 2 < so)" by auto
  ultimately show ?thesis using u_max_eq ego.q_def by auto
qed

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

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

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

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

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

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

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

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

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

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

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

definition distance0 :: real where 
  "distance0 =  ve * δ - vo * δ - ao * δ2 / 2"

definition distance0_2 :: real where 
  "distance0_2 = ve * δ + 1 / 2 * vo2 / ao"

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

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

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

definition safe_distance_3r :: real where
  "safe_distance_3r = ve * δ - ve2 / 2 / ae - vo * δ - 1/2 * ao * δ2"

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

definition safe_distance_4r :: real where 
  "safe_distance_4r = (vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ"

lemma distance0_at_most_sd4r:
  assumes "ao > ae"
  shows "distance0  safe_distance_4r"
proof -
  from assms have "ao  ae" by auto
  have "0  (vo + ao * δ - ve)2 / (2 * ao - 2 * ae)"
    by (rule divide_nonneg_nonneg) (auto simp add:assms ae  ao)
  thus ?thesis unfolding distance0_def safe_distance_4r_def
    by auto
qed

definition safe_distance_2r :: real where 
  "safe_distance_2r = ve * δ - ve2 / 2 / ae + vo2 / 2 / ao"

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

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

theorem distance0_at_most_distance2r:
  assumes "δ  other.t_stop"
  assumes "other.s' δ < ve"
  assumes "¬ (ao > ae  other.s' δ < ve  ve - ae / ao * other.s' δ < 0)"
  shows "distance0  safe_distance_2r"
proof -
  from so_star_stop_leq_se_stop[OF assms] have " 0  - ve2 / ae / 2 + (vo + ao * δ)2 / ao / 2 " (is "0  ?term")
    by auto
  have "safe_distance_2r = ve * δ - ve2 / 2 / ae + vo2 / 2 / ao" unfolding safe_distance_2r_def by auto
  also have "... = ve * δ - ve2 / 2 / ae + (vo + ao * δ)2 / 2 / ao - vo * δ - ao * δ2 / 2"
    using decelerate_other by (auto simp add:field_simps power_def)
  also have "... = ve * δ - vo * δ - ao * δ2 / 2 + ?term" (is "_ = ?left + ?term")
    by (auto simp add:field_simps)
  finally have "safe_distance_2r = distance0 + ?term" unfolding distance0_def by auto
  with 0  ?term show "distance0  safe_distance_2r" by auto
qed

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

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

theorem dist0_sd2r_2:
  assumes "δ > - vo / ao"
  assumes "so - se > safe_distance_2r"
  shows "so - se > distance0_2"
proof -
  have "- ve2 / 2 / ae  0" using zero_le_power2 hyps(3) divide_nonneg_neg by (auto simp add:field_simps)
  hence "ve * δ - ve2 / 2 / ae + vo2 / 2 / ao  ve * δ + vo2 / 2 / ao" by simp
  hence "safe_distance_2r  distance0_2" using safe_distance_2r_def distance0_2_def by auto
  thus ?thesis using assms(2) by linarith
qed
end

subsection ‹Safe Distance Delta›

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

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

lemma no_collision_react_initially_strict:
  assumes "so  u_max"
  assumes "u_max < other.s_stop"
  shows "no_collision_react {0 <..< δ}"
proof (rule no_collision_reactI)
  fix t::real
  assume "t  {0 <..< δ}" 
  show "u t  other.s t"
  proof (rule ccontr)
    assume "¬ u t  other.s t"
    hence "ego_other2 t = 0" unfolding ego_other2_def by auto
    from t  {0 <..< δ} have "ego_other2 t = other.s t - ego.q t" 
      unfolding ego_other2_def u_def using ego.init_q by auto
    have "δ  other.t_stop  other.t_stop < δ" by auto
    
    moreover
    { assume le_t_stop: "δ  other.t_stop"
      with ‹ego_other2 t = other.s t - ego.q t have "ego_other2 t = other.p t - ego.q t"
        unfolding other.s_def using t  {0 <..< δ} by auto
      with ‹ego_other2 t = 0 have "other.p t - ego.q t = 0" by auto
      hence eq: "(so- se) + (vo - ve) * t + (1/2 * ao) * t2 = 0"
        unfolding other.p_def ego.q_def by (auto simp: algebra_simps)
      define p where "p  λx. (1/2 * ao) * x2 + (vo - ve) * x + (so - se)"
      have "0 < 1/2 * ao"
      proof (intro p_convex[where p=p and b="vo - ve" and c="so - se"])
          show "0 < t" using t  {0 <..< δ} by auto
        next
          show "t < δ" using  t  {0 <..< δ} by auto
        next
          show "p t < p 0" unfolding p_def using eq in_front by (auto simp: algebra_simps)
        next
          from eq have "p t = 0" unfolding p_def by auto
          also have "... < p δ"  using no_collision_delta pos_react le_t_stop             
            unfolding p_def u_def other.s_def ego.q_def other.p_def by (auto simp:algebra_simps)
          finally have "p t < p δ" by simp
          thus "p t  p δ" by auto
        next
          show "p = (λx. 1 / 2 * ao * x2 + (vo - ve) * x + (so - se))" unfolding p_def
          by (rule refl)
      qed
      hence "0 < ao" by auto
      with decelerate_other have False by simp }

    moreover
    { assume gt_t_stop: "δ > other.t_stop"
      have t_lt_t_stop: "t < other.t_stop"
      proof (rule ccontr)
        assume "¬ t < other.t_stop"
        hence "other.t_stop  t" by simp
        from ‹ego_other2 t = 0 have "ego.q t = other.p_max"
          unfolding ego_other2_def u_def other.s_def comp_def τ_def other.p_max_def
          using t  {0 <..< δ} ‹other.t_stop  t gt_t_stop by (auto split:if_splits)
        have "ego.q t = u t" unfolding u_def using t  {0 <..< δ} by auto
        also have "...  u_max" using u_max by auto
        also have "... < other.p_max" using assms(2) other.s_t_stop by auto
        finally have "ego.q t < other.p_max" by auto
        with ‹ego.q t = other.p_max› show False by auto  
      qed
      
      with ‹ego_other2 t = other.s t - ego.q t have "ego_other2 t = other.p t - ego.q t"
        unfolding other.s_def using t  {0 <..< δ} by auto
      with ‹ego_other2 t = 0 have "other.p t - ego.q t = 0" by auto
      hence eq: "(so- se) + (vo - ve) * t + (1/2 * ao) * t2 = 0"
        unfolding other.p_def ego.q_def by (auto simp: algebra_simps)
      define p where "p  λx. (1/2 * ao) * x2 + (vo - ve) * x + (so - se)"
      have "0 < 1/2 * ao"
      proof (intro p_convex[where p=p and b="vo - ve" and c="so - se"])
          show "0 < t" using t  {0 <..< δ} by auto
        next
          show "t < other.t_stop" using t_lt_t_stop by auto
        next
          show "p t < p 0" unfolding p_def using eq in_front by (auto simp: algebra_simps)
        next
          from eq have zero: "p t = 0" unfolding p_def by auto
          have eq: "p other.t_stop = ego_other2 other.t_stop" 
            unfolding ego_other2_def other.s_t_stop u_def ego.q_def 
                      other.s_def other.p_def p_def
            using δ > other.t_stop› other.t_stop_nonneg other.t_stop_def
            by (auto simp: diff_divide_distrib left_diff_distrib')
          have "u other.t_stop  u_max" using u_max by auto
          also have "... < other.s_stop" using assms by auto
          finally have "0  other.s_stop - u other.t_stop" by auto
          hence "0  ego_other2 other.t_stop" unfolding ego_other2_def by auto
          hence "0  p other.t_stop" using eq by auto
          with zero show "p t  p other.t_stop" by auto
        next
          show "p = (λx. 1 / 2 * ao * x2 + (vo - ve) * x + (so - se))"
          unfolding p_def by (rule refl)
      qed 
      hence False using decelerate_other by auto }

     ultimately show False by auto
  qed
qed

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

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

lemma collision_after_delta:
  assumes "so  u_max"
  assumes "u_max < other.s_stop"
  shows "collision_react {0 ..}  collision_react {δ..}" 
proof
  assume "collision_react {0 ..}"
  have "no_collision_react {0 .. δ}" by (rule no_collision_react_initially[OF assms])
  with ‹collision_react {0..} have "collision_react ({0..} - {0 .. δ})"
  using pos_react by (auto intro: collision_trim_subset)
  
  moreover have "{0..} - {0 .. δ} = {δ <..}" using pos_react by auto
  ultimately have "collision_react {δ <..}" by auto
  thus "collision_react {δ ..}" by (auto intro:collision_react_subset)
next
  assume "collision_react {δ..}"
  moreover have "{δ..}  {0 ..}" using pos_react by auto
  ultimately show "collision_react {0 ..}" by (rule collision_react_subset)
qed

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

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

  moreover
  { assume "δ  other.t_stop"
    hence "other.s δ - (other.s' δ)2 / ao / 2 = so - vo2 / ao / 2"
    unfolding other.s_def other.s'_def
    using  pos_react decelerate_other
    by (auto simp add: other.p_def other.p'_def power2_eq_square field_split_simps) }

  moreover
  { assume "other.t_stop < δ"
    hence "other.s δ - (other.s' δ)2 / ao / 2 = so - vo2 / ao / 2"
    unfolding other.s_def other.s'_def other.p_max_eq
    using pos_react decelerate_other 
    by (auto) }

  ultimately show "other.s δ - (other.s' δ)2 / ao / 2 = so - vo2 / ao / 2" by auto
qed

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

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

lemma delayed_other_s_eq:
  assumes "0  t"
  shows "delayed_safe_distance.other.s t = other.s (t + δ)"
proof (cases "δ  other.t_stop")
  assume 1: "δ  other.t_stop"
  have "t + δ  other.t_stop  other.t_stop < t + δ" by auto
  moreover
  { assume "t + δ  other.t_stop"
    hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p t"    
      using delayed_other_t_stop_eq [OF 1] assms
      unfolding delayed_safe_distance.other.s_def by auto 
    
    also have "... = other.p (t + δ)" 
      unfolding movement.p_def other.s_def other.s'_def other.p'_def
      using pos_react 1 
      by (auto simp add: power2_eq_square field_split_simps)
      
    also have "... = other.s (t + δ)"
      unfolding other.s_def 
      using assms pos_react t + δ  other.t_stop› by auto

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

  moreover
  { assume "other.t_stop < t + δ"
    hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p_max"
      using delayed_other_t_stop_eq [OF 1] assms delayed_safe_distance.other.t_stop_nonneg
      unfolding delayed_safe_distance.other.s_def by auto
    
    also have "... = other.p_max" 
      unfolding movement.p_max_eq other.s_def other.s'_def other.p_def other.p'_def
      using pos_react 1 decelerate_other 
      by (auto simp add: power2_eq_square field_split_simps)

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

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

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

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

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

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

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

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

lemma sd_2r_correct_for_3r_2:
  assumes "so - se > safe_distance_2r"
  assumes "other.s δ  u_max"
  assumes "¬ (ao > ae  other.s' δ < ve  ve - ae / ao * other.s' δ < 0)"
  shows "no_collision_react {0..}"
proof -
  from assms have "so - se > ve * δ - ve2 / 2 / ae + vo2 / 2 / ao" unfolding safe_distance_2r_def by auto
  hence "so - vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so - vo2 / ao + vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so + vo * (- vo / ao) + 1/2 * ao * (-vo / ao)2 > se + ve * δ - ve2 / 2 / ae"
    using other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
  hence "other.s_stop > u_max" unfolding other.s_def using u_max_eq other.t_stop_def
    using ego.q_def other.p_def other.p_max_def other.s_def other.s_t_stop by auto
  thus ?thesis
    using assms(2) assms(3) collision_after_delta cond_1r delayed_cond3' translate_collision_range by linarith
qed

lemma sd2_at_most_sd4:
  assumes "ao > ae"
  shows "safe_distance_2r  safe_distance_4r"
proof -
  have "ao  0" and "ae  0" and "ao - ae  0" and "0 < 2 * (ao - ae)" using hyps assms(1) by auto
  have "0  (- ve * ao + vo * ae + ao * ae * δ) * (- ve * ao + vo * ae + ao * ae * δ)"
    (is "0  (?l1 + ?l2 + ?l3) * ?r") by auto
  also have "... = ve2 * ao2 + vo2 * ae2 + ao2 * ae2 * δ2 - 2 * ve * ao * vo * ae - 2 * ao2 * ae * δ * ve + 2 * ao * ae2 * δ * vo"
    (is "?lhs = ?rhs")
    by (auto simp add:algebra_simps power_def)
  finally have "0  ?rhs" by auto
  hence "(- ve2 * ao / ae - vo2 * ae / ao) * (ao * ae)  (ao * ae * δ2 - 2 * ve * vo - 2 * ao * δ * ve + 2 * ae * δ * vo) * (ao * ae)"
    by (auto simp add: algebra_simps power_def)
  hence "2 * ve * δ * (ao - ae) - ve2 * ao / ae + ve2 + vo2 - vo2 * ae / ao  vo2 + ao2 * δ2 + ve2 + 2 * vo * δ * ao - 2 * ve * vo - 2 * ao * δ * ve - 2 * vo * δ * ao + 2 * ae * δ * vo - ao2 * δ2 + ao * ae * δ2 + 2 * ve * δ * (ao - ae)"
    by (auto simp add: ego2.decel other.decel)
  hence "2 * ve * δ * (ao - ae) - ve2 * ao / ae + ve2 + vo2 - vo2 * ae / ao  (vo + δ * ao - ve)2 - 2 * vo * δ * ao + 2 * ae * δ * vo - ao2 * δ2 + ao * ae * δ2 + 2 * ve * δ * (ao - ae)"
    by (auto simp add: algebra_simps power_def)
  hence "ve * δ * 2 * (ao - ae) - ve2 / 2 / ae * 2 * ao + ve2 / 2 / ae * 2 * ae + vo2 / 2 / ao * 2 * ao - vo2 / 2 / ao * 2 * ae  (vo + δ * ao - ve)2 - vo * δ * 2 * ao - vo * δ * 2 * -ae - ao * δ2 / 2 * 2 * ao - ao * δ2 / 2 * 2 * -ae + ve * δ * 2 * (ao - ae)"
    (is "?lhs1  ?rhs1")
    by (simp add: ao  0 ae  0 power2_eq_square algebra_simps)
  hence "ve * δ * 2 * (ao - ae) - ve2 / 2 / ae * 2 * (ao - ae) + vo2 / 2 / ao * 2 * (ao - ae)  (vo + ao * δ - ve)2 / 2 / (ao - ae) * 2 * (ao - ae) - vo * δ * 2 * (ao - ae) - ao * δ2 / 2 * 2 * (ao - ae) + ve * δ * 2 *(ao - ae)"
    (is "?lhs2  ?rhs2")
  proof -
    assume "?lhs1  ?rhs1"
    have "?lhs1 = ?lhs2" by (auto simp add:field_simps)
    moreover
    have "?rhs1 = ?rhs2" using ao - ae  0 by (auto simp add:field_simps)
    ultimately show ?thesis using ?lhs1  ?rhs1 by auto
  qed
  hence "(ve * δ - ve2 / 2 / ae + vo2 / 2 / ao) * 2 * (ao - ae)  ((vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ) * 2 *(ao - ae)"
    by (simp add: algebra_simps)
  hence "ve * δ - ve2 / 2 / ae + vo2 / 2 / ao  (vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ"
    using ao > ae mult_le_cancel_iff1[OF 0 < 2 * (ao - ae), of "(ve * δ - ve2 / 2 / ae + vo2 / 2 / ao)"
    "(vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ"] semiring_normalization_rules(18)
    by (metis (no_types, lifting))
  thus ?thesis using safe_distance_2r_def safe_distance_4r_def by auto
qed

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

text ‹Irrelevant, this Safe Distance is unreachable in the checker.›
definition safe_distance_5r :: real where 
  "safe_distance_5r = ve2 / 2 / (ao - ae) + vo2 / 2 / ao + ve * δ"

lemma sd_5r_correct:
  assumes "so - se > safe_distance_5r"
  assumes "u_max < other.s_stop"
  assumes "other.s δ  u_max"
  assumes "δ > other.t_stop"
  shows "no_collision_react {0..}"
proof -
  from assms have "so - se > ve2 / 2 / (ao - ae) + vo2 / 2 / ao + ve * δ"
    unfolding safe_distance_5r_def by auto
  hence "so + vo2 / 2 / ao - se - ve * δ > (0 - ve)2 / 2 / (ao - ae)"
    using assms(2-4) unfolding other.s_def other.s_t_stop
    apply (auto simp: movement.p_t_stop split: if_splits)
    using cond_1r cond_2r other.s_t_stop by linarith+
  hence "other.s δ -  ego.q δ > (other.s' δ - ve)2 / 2 / (ao - ae)"
    using assms(2) assms(3) assms(4) other.s_def other.s_t_stop by auto
  hence "other.s δ -  ego.q δ > delayed_safe_distance.snd_safe_distance"
    by (simp add: delayed_safe_distance.snd_safe_distance_def)
  hence "¬ (other.s δ -  ego.q δ  delayed_safe_distance.snd_safe_distance)" by linarith
  thus ?thesis using assms(2) assms(3) cond_1r cond_3r_2 by linarith
qed

lemma translate_no_collision_range:
  "delayed_safe_distance.no_collision {0 ..}  no_collision_react {δ ..}"  
proof
  assume left: "delayed_safe_distance.no_collision {0 ..}" 
  show "no_collision_react {δ ..}" 
  proof (unfold collision_react_def; simp; rule ballI)
    fix t::real  
    assume "t  {δ ..}"
    hence "δ  t" by simp
    with pos_react have "0  t - δ" by simp
    with left have ineq: "ego2.s (t - δ)  delayed_safe_distance.other.s (t - δ)"
      unfolding delayed_safe_distance.collision_def by auto
    have "ego2.s (t - δ) = (ego2.s  τ) t" unfolding comp_def τ_def by auto
    also have "... = u t" unfolding u_def using δ  t pos_react 
      by (auto simp: τ_def ego2.init_s)
    finally have "ego2.s (t - δ) = u t" by auto

    moreover have "delayed_safe_distance.other.s (t - δ) = other.s t"
      using delayed_other_s_eq pos_react δ  t by auto
  
    ultimately show "u t  other.s t" using ineq by auto
  qed
next
  assume right: "no_collision_react {δ ..}"
  show "delayed_safe_distance.no_collision {0 ..}"
  proof (unfold delayed_safe_distance.collision_def; simp; rule ballI)
    fix t ::real
    assume "t  {0 ..}"
    hence "0  t" by auto
    hence "δ  t + δ" by auto
    with right have ineq: "u (t + δ)  other.s (t + δ)" unfolding collision_react_def by auto
            
    have "u (t + δ) = ego2.s t" unfolding u_def comp_def τ_def 
      using 0  t pos_react δ  t+ δ by (auto simp add:ego2.init_s)
    moreover have "other.s (t + δ) = delayed_safe_distance.other.s t"
      using delayed_other_s_eq[of t] using 0  t by auto
    ultimately show "ego2.s t  delayed_safe_distance.other.s t" using ineq by auto
  qed
qed

lemma delayed_cond1:
  assumes "other.s δ > u_max"
  shows "delayed_safe_distance.no_collision {0 ..}"
proof -
  have "ego2.s_stop = u_max"  unfolding ego2.s_t_stop ego2.p_max_eq u_max_eq by auto
  also have "... < other.s δ" using assms by simp
  finally have "ego2.s_stop < other.s δ" by auto
  thus "delayed_safe_distance.no_collision {0 ..}" by (simp add: delayed_safe_distance.cond_1)
qed

theorem cond_3r_3:
  assumes "so  u_max"
  assumes "u_max < other.s_stop"
  assumes "other.s δ > u_max"
  shows "no_collision_react {0 ..}"
proof -
  have eq: "{0 ..} = {0 .. δ}  {δ ..}" using pos_react by auto
  show ?thesis unfolding eq 
  proof (intro no_collision_union)
    show "no_collision_react {0 .. δ}" by (rule no_collision_react_initially[OF assms(1) assms(2)])  
  next
    have "delayed_safe_distance.no_collision {0 ..}" by (rule delayed_cond1[OF assms(3)])
    with translate_no_collision_range show "no_collision_react {δ ..}" by auto
  qed
qed

lemma sd_2r_correct_for_3r_3:
  assumes "so - se > safe_distance_2r"
  assumes "other.s δ > u_max"
  shows "no_collision_react {0..}"
proof -
  from assms have "so - se > ve * δ - ve2 / 2 / ae + vo2 / 2 / ao" unfolding safe_distance_2r_def by auto
  hence "so - vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so - vo2 / ao + vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so + vo * (- vo / ao) + 1/2 * ao * (-vo / ao)2 > se + ve * δ - ve2 / 2 / ae"
    using other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
  hence "other.s_stop > u_max" unfolding other.s_def using u_max_eq other.t_stop_def
    using ego.q_def other.p_def other.p_max_def other.s_def other.s_t_stop by auto
  thus ?thesis
    using assms(2) cond_1r cond_3r_3 by linarith
qed

lemma sd_3r_correct:
  assumes "so - se > safe_distance_3r"
  assumes "δ  other.t_stop"
  shows "no_collision_react {0 ..}"
proof -
  from assms have "so - se > ve * δ - ve2 / 2 / ae - vo * δ - 1/2 * ao * δ2" unfolding safe_distance_3r_def by auto
  hence "so + vo * δ + 1/2 * ao * δ2 > se + ve * δ - ve2 / 2 / ae" by auto
  hence "other.s δ > u_max" using other.s_def u_max_eq assms(2) ego.q_def other.p_def pos_react by auto
  thus ?thesis using cond_1r cond_3r_3 delayed_other_s_stop_eq delayed_safe_distance.other.s0_le_s_stop by linarith
qed

lemma sd_2_at_least_sd_3:
  assumes "δ  other.t_stop"
  shows "safe_distance_3r  safe_distance_2r"
proof -
  from assms have "δ = other.t_stop  δ < other.t_stop" by auto
  then have "safe_distance_3r = safe_distance_2r  safe_distance_3r > safe_distance_2r"
  proof (rule Meson.disj_forward)
      assume "δ = other.t_stop"
      hence "δ = - vo / ao" unfolding other.t_stop_def by auto
      hence "- vo * δ - 1/2 * ao * δ2 = - vo  * other.t_stop - 1/2 * ao * other.t_stop2" by (simp add: movement.t_stop_def)
      thus "safe_distance_3r = safe_distance_2r"
        using other.p_def other.p_max_def other.p_max_eq safe_distance_2r_def safe_distance_3r_def by auto
    next
      assume "δ < other.t_stop"
      hence "δ < - vo / ao" unfolding other.t_stop_def by auto
      hence "0 < vo + ao * δ"
        using other.decel other.p'_def other.p'_pos_iff by auto
      hence "0 < vo + 1/2 * ao * (δ + other.t_stop)" by (auto simp add:field_simps other.t_stop_def)
      hence "0 > vo * (δ - other.t_stop) + 1/2 * ao * (δ + other.t_stop) * (δ - other.t_stop)"
        using δ < other.t_stop›  mult_less_cancel_left_neg[where c="δ - other.t_stop" and a ="vo + 1 / 2 * ao * (δ + other.t_stop)" and b="0"]
        by (auto simp add: field_simps)
      hence " (δ + other.t_stop) * (δ - other.t_stop) = (δ2 - other.t_stop2)"
        by (simp add: power2_eq_square square_diff_square_factored)
      hence "0 > vo * (δ - other.t_stop) + 1/2 * ao * (δ2 - other.t_stop2)"
        by (metis (no_types, hide_lams) vo * (δ - other.t_stop) + 1 / 2 * ao * (δ + other.t_stop) * (δ - other.t_stop) < 0 divide_divide_eq_left divide_divide_eq_right times_divide_eq_left)
      hence "0 > vo * δ - vo * other.t_stop  + 1/2 * ao * δ2 -  1/2 * ao * other.t_stop2 "
        by (simp add: right_diff_distrib)
      hence "- vo * δ - 1/2 * ao * δ2 > - vo  * (- vo / ao) - 1/2 * ao * (- vo / ao)2"
        unfolding movement.t_stop_def by argo
      thus "safe_distance_3r > safe_distance_2r"
        using other.p_def other.p_max_def other.p_max_eq other.t_stop_def safe_distance_2r_def safe_distance_3r_def by auto
  qed
  thus ?thesis by auto
qed
end

subsection ‹Checker Design›

text ‹
  We define two checkers for different cases: 
   one checker for the case that δ ≤ other.t_stop (other.t_stop = - vo / ao)›
   a second checker for the case that δ > other.t_stop›

definition check_precond_r1 :: "real  real  real  real  real  real  real  bool" where
  "check_precond_r1 se ve ae so vo ao δ  so > se  0  ve  0  vo  ae < 0  ao < 0  0 < δ  δ  - vo / ao"

definition safe_distance0 :: "real  real  real  real  real" where 
  "safe_distance0 ve ao vo δ = ve * δ - vo * δ - ao * δ2 / 2"

definition safe_distance_1r :: "real  real  real  real" where 
  "safe_distance_1r ae ve δ = ve * δ - ve2 / ae / 2"

definition safe_distance_2r :: "real  real  real  real  real  real" where 
  "safe_distance_2r ae ve ao vo δ = ve * δ - ve2 / 2 / ae + vo2 / 2 / ao"

definition safe_distance_4r :: "real  real  real  real  real  real" where
  "safe_distance_4r ae ve ao vo δ = (vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1 / 2 * ao * δ2 + ve * δ"

definition safe_distance_3r :: "real  real  real  real  real  real" where 
  "safe_distance_3r ae ve ao vo δ = ve * δ - ve2 / 2 / ae - vo * δ - 1 / 2 * ao * δ2"

definition checker_r1 :: "real  real  real  real  real  real  real  bool" where
  "checker_r1 se ve ae so vo ao δ  
    let distance      = so - se;
				precond       = check_precond_r1 se ve ae so vo ao δ;
        vo_star       = vo + ao * δ;
        t_stop_o_star = - vo_star / ao;
        t_stop_e      = - ve / ae;
        safe_dist0    = safe_distance_1r ae ve δ;
        safe_dist1    = safe_distance_2r ae ve ao vo δ;
        safe_dist2    = safe_distance_4r ae ve ao vo δ;
        safe_dist3    = safe_distance_3r ae ve ao vo δ
    in
      if ¬ precond then False
      else if distance > safe_dist0  distance > safe_dist3 then True
      else if (ao > ae  vo_star < ve  t_stop_e < t_stop_o_star) then distance > safe_dist2
      else distance > safe_dist1"

theorem checker_r1_correctness:
  "(checker_r1 se ve ae so vo ao δ  check_precond_r1 se ve ae so vo ao δ  
   safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})"
proof
  assume asm: "checker_r1 se ve ae so vo ao δ"
  have pre: "check_precond_r1 se ve ae so vo ao δ"
  proof (rule ccontr)
    assume "¬ check_precond_r1 se ve ae so vo ao δ"
    with asm show "False" unfolding checker_r1_def Let_def by auto
  qed
  from pre have sdn': "safe_distance_normal ae ve se ao vo so δ"
    by (unfold_locales) (auto simp add: check_precond_r1_def)
  interpret sdn: safe_distance_normal ae ve se ao vo so δ
    rewrites "sdn.distance0 = safe_distance0 ve ao vo δ" and
             "sdn.safe_distance_1r = safe_distance_1r ae ve δ" and
             "sdn.safe_distance_2r = safe_distance_2r ae ve ao vo δ" and
             "sdn.safe_distance_4r = safe_distance_4r ae ve ao vo δ" and
             "sdn.safe_distance_3r = safe_distance_3r ae ve ao vo δ"
  proof -
    from sdn' show "safe_distance_normal ae ve se ao vo so δ" by auto
  next
    show "safe_distance_normal.distance0 ve ao vo δ = safe_distance0 ve ao vo δ "
      unfolding safe_distance_normal.distance0_def[OF sdn'] safe_distance0_def by auto
  next
    show "safe_distance_normal.safe_distance_1r ae ve δ = safe_distance_1r ae ve δ"
      unfolding safe_distance_normal.safe_distance_1r_def[OF sdn'] safe_distance_1r_def by auto
  next
    show "safe_distance_normal.safe_distance_2r ae ve ao vo δ = safe_distance_2r ae ve ao vo δ"
      unfolding safe_distance_normal.safe_distance_2r_def[OF sdn'] safe_distance_2r_def by auto
  next
    show "safe_distance_normal.safe_distance_4r ae ve ao vo δ = safe_distance_4r ae ve ao vo δ "
      unfolding safe_distance_normal.safe_distance_4r_def[OF sdn'] safe_distance_4r_def by auto
  next
    show "safe_distance_normal.safe_distance_3r ae ve ao vo δ = safe_distance_3r ae ve ao vo δ"
      unfolding safe_distance_normal.safe_distance_3r_def[OF sdn'] safe_distance_3r_def by auto
  qed
  have "0 < δ" and "δ  - vo / ao" using pre unfolding check_precond_r1_def by auto
  define so_delta where "so_delta = so + vo * δ + ao * δ2 / 2"
  define q_e_delta where "q_e_delta  se + ve * δ"
  define u_stop_e where "u_stop_e  q_e_delta - ve2 / (2 * ae)"
  define vo_star where "vo_star = vo + ao * δ"
  define t_stop_o_star where "t_stop_o_star  - vo_star / ao"
  define t_stop_e where "t_stop_e = - ve / ae"
  define distance where "distance  so - se"
  define distance0 where "distance0 = safe_distance0 ve ao vo δ"
  define safe_dist0 where "safe_dist0 = safe_distance_1r ae ve δ"
  define safe_dist2 where "safe_dist2  safe_distance_4r ae ve ao vo δ"
  define safe_dist1 where "safe_dist1  safe_distance_2r ae ve ao vo δ"
  define safe_dist3 where "safe_dist3 = safe_distance_3r ae ve ao vo δ"
  note abb = so_delta_def q_e_delta_def u_stop_e_def vo_star_def t_stop_o_star_def t_stop_e_def
             distance_def safe_dist2_def safe_dist1_def safe_dist0_def safe_dist3_def distance0_def
  consider "distance > safe_dist0" | "distance > safe_dist3" | "distance  safe_dist0  distance  safe_dist3"
    by linarith
  hence "sdn.no_collision_react {0..}"
  proof (cases)
    case 1
    then show ?thesis using sdn.sd_1r_correct unfolding  abb by auto
  next
    case 2
    hence pre2: "distance > distance0" using sdn.distance0_at_most_sd3r unfolding abb by auto
    hence "sdn.u δ < sdn.other.s δ" using pre unfolding sdn.u_def sdn.ego.q_def
      sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
      by auto
    from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
      by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ)
    show ?thesis using sdr.sd_3r_correct 2 pre unfolding check_precond_r1_def abb sdn.other.t_stop_def
      by auto
  next
    case 3
    hence "distance  safe_dist3" by auto
    hence "sdn.other.s δ  sdn.u_max" using pre unfolding check_precond_r1_def sdn.other.s_def sdn.other.t_stop_def
      sdn.other.p_def sdn.u_max_eq sdn.ego.q_def abb sdn.safe_distance_3r_def by auto
    have " (ao > ae  vo_star < ve  t_stop_e < t_stop_o_star)  ¬  (ao > ae  vo_star < ve  t_stop_e < t_stop_o_star) "
      by auto
    moreover
    { assume cond: "(ao > ae  vo_star < ve  t_stop_e < t_stop_o_star)"
      with 3 pre have "distance > safe_dist2" using asm unfolding checker_r1_def
          Let_def abb by auto
      with sdn.distance0_at_most_sd4r have "distance > distance0" unfolding abb using cond by auto
      hence "sdn.u δ < sdn.other.s δ" using pre unfolding sdn.u_def sdn.ego.q_def
          sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
        by auto
      from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
        by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ)
      from sdr.sd_4r_correct[OF _ ‹sdn.other.s δ  sdn.u_max›] distance > safe_dist2
        have ?thesis using pre cond  unfolding check_precond_r1_def sdn.other.t_stop_def abb by auto }
    moreover
    { assume not_cond: "¬  (ao > ae  vo_star < ve  t_stop_e < t_stop_o_star)"
      with 3 pre have "distance > safe_dist1" using asm unfolding checker_r1_def
        Let_def abb by auto
      with sdn.dist0_sd2r_1 have "distance > distance0" using pre not_cond unfolding check_precond_r1_def
        sdn.other.t_stop_def sdn.other.s'_def sdn.other.p'_def abb by (auto simp add:field_simps)
      hence "sdn.u δ < sdn.other.s δ" using pre unfolding sdn.u_def sdn.ego.q_def
          sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
        by auto
      from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
        by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ)
      from sdr.sd_2r_correct_for_3r_2[OF _ ‹sdn.other.s δ  sdn.u_max›] not_cond distance > safe_dist1
        have ?thesis using pre unfolding abb sdn.other.s'_def check_precond_r1_def sdn.other.t_stop_def sdn.other.p'_def
        by (auto simp add:field_simps) }
    ultimately show ?thesis by auto
  qed
  with pre show " check_precond_r1 se ve ae so vo ao δ  sdn.no_collision_react {0..}" by auto
next
  assume "check_precond_r1 se ve ae so vo ao δ  safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..}"
  hence pre: "check_precond_r1 se ve ae so vo ao δ" and as2: "safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..}"
  by auto
  show "checker_r1 se ve ae so vo ao δ "
  proof (rule ccontr)
    assume as1: "¬ checker_r1 se ve ae so vo ao δ"
    from pre have "0 < δ" and "δ  - vo / ao" unfolding check_precond_r1_def by auto
    define so_delta where "so_delta = so + vo * δ + ao * δ2 / 2"
    define q_e_delta where "q_e_delta  se + ve * δ"
    define u_stop_e where "u_stop_e  q_e_delta - ve2 / (2 * ae)"
    define vo_star where "vo_star  vo + ao * δ"
    define t_stop_o_star where "t_stop_o_star  - vo_star / ao"
    define t_stop_e where "t_stop_e  - ve / ae"
    define distance where "distance  so - se"
    define distance0 where "distance0  safe_distance0 ve ao vo δ"
    define safe_dist0 where "safe_dist0  safe_distance_1r ae ve δ"
    define safe_dist2 where "safe_dist2  safe_distance_4r ae ve ao vo δ"
    define safe_dist1 where "safe_dist1  safe_distance_2r ae ve ao vo δ"
    define safe_dist3 where "safe_dist3  safe_distance_3r ae ve ao vo δ"
    note abb = so_delta_def q_e_delta_def u_stop_e_def vo_star_def t_stop_o_star_def t_stop_e_def
               distance_def safe_dist2_def safe_dist1_def safe_dist0_def safe_dist3_def distance0_def
    from pre have sdn': "safe_distance_normal ae ve se ao vo so δ"
      by (unfold_locales) (auto simp add: check_precond_r1_def)
    interpret sdn: safe_distance_normal ae ve se ao vo so δ
      rewrites "sdn.distance0 = safe_distance0 ve ao vo δ" and
               "sdn.safe_distance_1r = safe_distance_1r ae ve δ" and
               "sdn.safe_distance_2r = safe_distance_2r ae ve ao vo δ" and
               "sdn.safe_distance_4r = safe_distance_4r ae ve ao vo δ" and
               "sdn.safe_distance_3r = safe_distance_3r ae ve ao vo δ"
    proof -
      from sdn' show "safe_distance_normal ae ve se ao vo so δ" by auto
    next
      show "safe_distance_normal.distance0 ve ao vo δ = safe_distance0 ve ao vo δ "
        unfolding safe_distance_normal.distance0_def[OF sdn'] safe_distance0_def by auto
    next
      show "safe_distance_normal.safe_distance_1r ae ve δ = safe_distance_1r ae ve δ"
        unfolding safe_distance_normal.safe_distance_1r_def[OF sdn'] safe_distance_1r_def by auto
    next
      show "safe_distance_normal.safe_distance_2r ae ve ao vo δ = safe_distance_2r ae ve ao vo δ"
        unfolding safe_distance_normal.safe_distance_2r_def[OF sdn'] safe_distance_2r_def by auto
    next
      show "safe_distance_normal.safe_distance_4r ae ve ao vo δ = safe_distance_4r ae ve ao vo δ "
        unfolding safe_distance_normal.safe_distance_4r_def[OF sdn'] safe_distance_4r_def by auto
    next
      show "safe_distance_normal.safe_distance_3r ae ve ao vo δ = safe_distance_3r ae ve ao vo δ"
        unfolding safe_distance_normal.safe_distance_3r_def[OF sdn'] safe_distance_3r_def by auto
    qed
    have "¬ distance > distance0   distance > distance0" by auto
    moreover
    { assume "¬ distance > distance0"
      hence "distance  distance0" by auto
      with sdn.cond_3r_1' have "sdn.collision_react {0..δ}" using pre unfolding check_precond_r1_def abb
        sdn.other.t_stop_def by auto
      with sdn.collision_react_subset have "sdn.collision_react {0..}" by auto
      with as2 have "False" by auto }
    moreover
    { assume if2: "distance > distance0"
      have "¬ (distance > safe_dist0  distance > safe_dist3)"
      proof (rule ccontr)
        assume "¬ ¬ (safe_dist0 < distance  safe_dist3 < distance)"
        hence "(safe_dist0 < distance  safe_dist3 < distance)" by auto
        with as1 show "False" using pre if2 unfolding checker_r1_def Let_def abb
          by auto
      qed
      hence if31: "distance  safe_dist0" and if32: "distance  safe_dist3" by auto
      have "sdn.u δ < sdn.other.s δ" using if2 pre unfolding sdn.u_def sdn.ego.q_def
          sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
          by auto
      from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
        by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ)
      have " so  sdn.u_max" using if31 unfolding sdn.u_max_eq sdn.ego.q_def abb
        sdn.safe_distance_1r_def by auto
      have "sdn.other.s δ  sdn.u_max" using if32 pre unfolding sdn.other.s_def check_precond_r1_def
        sdn.other.t_stop_def sdn.other.p_def sdn.u_max_eq sdn.ego.q_def abb sdn.safe_distance_3r_def
        by auto
      consider "(ao > ae  vo_star < ve  t_stop_e < t_stop_o_star)" |
               "¬ (ao > ae  vo_star < ve  t_stop_e < t_stop_o_star)" by auto
      hence "False"
      proof (cases)
        case 1
        hence rest_conjunct:"(ae < ao  sdn.other.s' δ < ve  ve - ae / ao * sdn.other.s' δ < 0)"
          using pre unfolding check_precond_r1_def unfolding sdn.other.s'_def sdn.other.t_stop_def
          sdn.other.p'_def abb by (auto simp add:field_simps)
        from 1 have "distance  safe_dist2" using as1 pre if2 if31 if32 unfolding checker_r1_def
          Let_def abb by auto
        hence cond_f: "sdn.other.s δ - sdn.ego.q δ  sdr.delayed_safe_distance.snd_safe_distance"
          using pre unfolding check_precond_r1_def sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def
          sdn.ego.q_def sdr.delayed_safe_distance.snd_safe_distance_def using sdn.other.s'_def[of "δ"]
          unfolding sdn.other.t_stop_def sdn.other.p'_def abb sdn.safe_distance_4r_def
          by auto
        have "distance > safe_dist1  distance  safe_dist1" by auto
        moreover
        { assume "distance > safe_dist1"
          hence "sdn.u_max < sdn.other.s_stop" unfolding sdn.u_max_eq sdn.ego.q_def sdn.other.s_t_stop
              sdn.other.p_max_eq abb sdn.safe_distance_2r_def by (auto simp add:field_simps)
          from sdr.cond_3r_2[OF so  sdn.u_max› this ‹sdn.other.s δ  sdn.u_max›]
          have "sdn.collision_react {0..}" using cond_f rest_conjunct by auto
          with as2 have "False" by auto }
        moreover
        { assume "distance  safe_dist1"
          hence "sdn.u_max  sdn.other.s_stop" unfolding sdn.u_max_eq sdn.ego.q_def sdn.other.s_t_stop
              sdn.other.p_max_eq abb sdn.safe_distance_2r_def by (auto simp add:field_simps)
          with sdn.cond_2r[OF this] have "sdn.collision_react {0..}" by auto
          with as2 have "False" by auto }
        ultimately show ?thesis by auto
      next
        case 2
        hence "distance  safe_dist1" using as1 pre if2 if31 if32 unfolding checker_r1_def
          Let_def abb by auto
        hence "sdn.u_max  sdn.other.s_stop" unfolding sdn.u_max_eq sdn.ego.q_def sdn.other.s_t_stop
          sdn.other.p_max_eq abb sdn.safe_distance_2r_def by (auto simp add:field_simps)
        with sdn.cond_2r[OF this] have "sdn.collision_react {0..}" by auto
        with as2 show "False" by auto
      qed }
    ultimately show "False" by auto
  qed
qed

definition check_precond_r2 :: "real  real  real  real  real  real  real  bool" where 
  "check_precond_r2 se ve ae so vo ao δ  so > se  0  ve  0  vo  ae < 0  ao < 0  0 < δ  δ > - vo / ao"

definition safe_distance0_2 :: "real  real  real  real  real" where 
  "safe_distance0_2 ve ao vo δ = ve * δ + 1 / 2 * vo2 / ao"

definition checker_r2 :: "real  real  real  real  real  real  real  bool" where
  "checker_r2 se ve ae so vo ao δ  
    let distance   = so - se;
				precond    = check_precond_r2 se ve ae so vo ao δ;
        safe_dist0 = safe_distance_1r ae ve δ;
        safe_dist1 = safe_distance_2r ae ve ao vo δ 
    in
      if ¬ precond then False
      else if distance > safe_dist0 then True
      else distance > safe_dist1"

theorem checker_r2_correctness:
  "(checker_r2 se ve ae so vo ao δ  check_precond_r2 se ve ae so vo ao δ  
    safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})"
proof
  assume asm: "checker_r2 se ve ae so vo ao δ"
  have pre: "check_precond_r2 se ve ae so vo ao δ"
  proof (rule ccontr)
    assume "¬ check_precond_r2 se ve ae so vo ao δ"
      with asm show "False" unfolding checker_r2_def Let_def by auto
    qed
      from pre have sdn': "safe_distance_normal ae ve se ao vo so δ"
    by (unfold_locales) (auto simp add: check_precond_r2_def)
  interpret sdn: safe_distance_normal ae ve se ao vo so δ
    rewrites "sdn.distance0_2 = safe_distance0_2 ve ao vo δ" and
             "sdn.safe_distance_1r = safe_distance_1r ae ve δ" and
             "sdn.safe_distance_2r = safe_distance_2r ae ve ao vo δ"
  proof -
    from sdn' show "safe_distance_normal ae ve se ao vo so δ" by auto
  next
    show "safe_distance_normal.distance0_2 ve ao vo δ = safe_distance0_2 ve ao vo δ"
      unfolding safe_distance_normal.distance0_2_def[OF sdn'] safe_distance0_2_def by auto
  next
    show "safe_distance_normal.safe_distance_1r ae ve δ = safe_distance_1r ae ve δ"
      unfolding safe_distance_normal.safe_distance_1r_def[OF sdn'] safe_distance_1r_def by auto
  next
    show "safe_distance_normal.safe_distance_2r ae ve ao vo δ = safe_distance_2r ae ve ao vo δ"
      unfolding safe_distance_normal.safe_distance_2r_def[OF sdn'] safe_distance_2r_def by auto
  qed
  have "0 < δ" and "δ > - vo / ao" using pre unfolding check_precond_r2_def by auto
  define distance where "distance  so - se"
  define distance0_2 where "distance0_2 = safe_distance0_2 ve ao vo δ"
  define safe_dist0 where "safe_dist0 = safe_distance_1r ae ve δ"
  define safe_dist1 where "safe_dist1  safe_distance_2r ae ve ao vo δ"
  note abb = distance_def safe_dist1_def safe_dist0_def distance0_2_def
  consider "distance > safe_dist0" | "distance  safe_dist0"
    by linarith
  hence "sdn.no_collision_react {0..}"
  proof (cases)
    case 1
    then show ?thesis using sdn.sd_1r_correct unfolding abb by auto
  next
    case 2
    hence "(so  sdn.u_max)" using distance_def safe_dist0_def sdn.sd_1r_eq by linarith
    with 2 pre have "distance > safe_dist1" using asm unfolding checker_r2_def Let_def abb by auto
    with sdn.dist0_sd2r_2 have "distance > distance0_2" using abb - vo / ao < δ by auto
    hence "sdn.u δ < sdn.other.s δ" using abb sdn.distance0_2_eq δ > - vo / ao sdn.other.t_stop_def by auto
    have "sdn.u_max < sdn.other.s δ" using abb sdn.sd2r_eq  δ > - vo / ao sdn.other.t_stop_def distance > safe_dist1 by auto
    from pre interpret