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_real_derivative_iff_has_vector_derivative)

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

lemma s_delayed_has_real_derivative[derivative_intros]:
  assumes "δ  t"
  shows "((ego2.s  τ) has_field_derivative ego2.s' (t - δ) * τ' t) (at t within {δ..})"
proof (rule DERIV_image_chain)
  from assms have 0: "0  t - δ" by simp
  from ego2.t_stop_nonneg have 1: "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_real_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_real_derivative_iff_has_vector_derivative
    apply (rule has_vector_derivative_If_within_closures[where T = "{δ..}"])
    using 0  δ q_delta q'_delta ego.s_has_vector_derivative[OF assms] ego.decel ego.t_stop_nonneg 
    s_delayed_has_vector_derivative'[of "t"] τ_def
    unfolding comp_def
    by (auto simp: assms  max_def insert_absorb   
      intro!: ego.q_has_vector_derivative)
  show ?thesis
    unfolding has_vector_derivative_def has_real_derivative_iff_has_vector_derivative
      u'_def u_def[abs_def] 
    proof (rule has_derivative_transform[where f="(λt. if t  {0..δ} then ego.q t else (ego2.s  τ) t)"])
      from nonneg_t show " t  {0..}" by auto
    next
      fix x
      assume "(x::real)  {0..}"
      hence  "x  δ  x  {0 .. δ}" by simp
      thus  " (if x  0 then 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_real_derivative_iff_has_vector_derivative by auto      
      moreover with assms have "t  {0 .. δ}  t  δ" by auto
      ultimately show " ((λt. if t  {0..δ} then ego.q t else (ego2.s  τ) t) has_derivative
              (λx. x *R (if t  δ then ego2.q' t else ego2.s' (t - δ)))) (at t within {0..})" 
      unfolding comp_def τ_def has_vector_derivative_def by auto
    qed 
qed

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

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

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

lemma t_stop_zero:
  assumes "t_stop  x"
  assumes "x  δ"
  shows "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_right_pos[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</