Theory PTA_Reachability

theory PTA_Reachability
  imports PTA
begin

section ‹Classifying Regions for Divergence›

subsection ‹Pairwise›

coinductive pairwise :: "('a  'a  bool)  'a stream  bool" for P where
  "P a b  pairwise P (b ## xs)  pairwise P (a ## b ## xs)"

lemma pairwise_Suc:
  "pairwise P xs  P (xs !! i) (xs !! (Suc i))"
  by (induction i arbitrary: xs) (force elim: pairwise.cases)+

lemma Suc_pairwise:
  " i. P (xs !! i) (xs !! (Suc i))  pairwise P xs"
  apply (coinduction arbitrary: xs)
  apply (subst stream.collapse[symmetric])
  apply (rewrite in "stl _" stream.collapse[symmetric])
  apply (intro exI conjI, rule HOL.refl)
   apply (erule allE[where x = 0]; simp; fail)
  by simp (metis snth.simps(2))

lemma pairwise_iff:
  "pairwise P xs  ( i. P (xs !! i) (xs !! (Suc i)))"
using pairwise_Suc Suc_pairwise by blast

lemma pairwise_stlD:
  "pairwise P xs  pairwise P (stl xs)"
by (auto elim: pairwise.cases)

lemma pairwise_pairD:
  "pairwise P xs  P (shd xs) (shd (stl xs))"
by (auto elim: pairwise.cases)

lemma pairwise_mp:
  assumes "pairwise P xs" and lift: " x y. x  sset xs  y  sset xs  P x y  Q x y"
  shows "pairwise Q xs" using assms
 apply (coinduction arbitrary: xs)
 subgoal for xs
 apply (subst stream.collapse[symmetric])
 apply (rewrite in "stl _" stream.collapse[symmetric])
 apply (intro exI conjI)
  apply (rule HOL.refl)
 by (auto intro: stl_sset dest: pairwise_pairD pairwise_stlD)
done

lemma pairwise_sdropD:
  "pairwise P (sdrop i xs)" if "pairwise P xs"
  using that
proof (coinduction arbitrary: i xs)
  case (pairwise i xs)
  then show ?case
    apply (inst_existentials "shd (sdrop i xs)" "shd (stl (sdrop i xs))" "stl (stl (sdrop i xs))")
    subgoal
      by (auto dest: pairwise_Suc) (metis sdrop_simps(1) sdrop_stl stream.collapse)
    subgoal
      by (inst_existentials "i - 1" "stl xs") (auto dest: pairwise_Suc pairwise_stlD)
    by (metis sdrop_simps(2) stream.collapse)
qed


subsection ‹Regions›

(* XXX Move. Rename? *)
lemma gt_GreaterD:
  assumes "u  region X I r" "valid_region X k I r" "c  X" "u c > k c"
  shows "I c = Greater (k c)"
proof -
  from assms have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
  with assms(4) show ?thesis by (cases "I c") auto
qed

lemma const_ConstD:
  assumes "u  region X I r" "valid_region X k I r" "c  X" "u c = d" "d  k c"
  shows "I c = Const d"
proof -
  from assms have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
  with assms(4,5) show ?thesis by (cases "I c") auto
qed

lemma not_Greater_bounded:
  assumes "I x  Greater (k x)" "x  X" "valid_region X k I r" "u  region X I r"
  shows "u x  k x"
proof -
  from assms have "intv_elem x u (I x)" "valid_intv (k x) (I x)" by auto
  with assms(1) show "u x  k x" by (cases "I x") auto
qed

lemma Greater_closed:
  fixes t :: "real"
  assumes "u  region X I r" "valid_region X k I r" "c  X" "I c = Greater (k c)" "t > k c"
  shows "u(c := t)  region X I r"
  using assms
  apply (intro region.intros)
     apply (auto; fail)
    apply standard
  subgoal for x
    by (cases "x = c"; cases "I x"; force intro!: intv_elem.intros)
  by auto

lemma Greater_unbounded_aux:
  assumes "finite X" "valid_region X k I r" "c  X" "I c = Greater (k c)"
  shows " u  region X I r. u c > t"
using assms Greater_closed[OF _ assms(2-4)] 
proof -
  let ?R = "region X I r"
  let ?t = "if t > k c then t + 1 else k c + 1"
  have t: "?t > k c" by auto
  from region_not_empty[OF assms(1,2)] obtain u where u: "u  ?R" by auto
  from Greater_closed[OF this assms(2-4) t] have "u(c:=?t)  ?R" by auto
  with t show ?thesis by (inst_existentials "u(c:=?t)") auto
qed


subsection ‹Unbounded and Zero Regions›

definition "unbounded x R   t.  u  R. u x > t"

definition "zero x R   u  R. u x = 0"

lemma Greater_unbounded:
  assumes "finite X" "valid_region X k I r" "c  X" "I c = Greater (k c)"
  shows "unbounded c (region X I r)"
using Greater_unbounded_aux[OF assms] unfolding unbounded_def by blast

lemma unbounded_Greater:
  assumes "valid_region X k I r" "c  X" "unbounded c (region X I r)"
  shows "I c = Greater (k c)"
using assms unfolding unbounded_def by (auto intro: gt_GreaterD)

lemma Const_zero:
  assumes "c  X" "I c = Const 0"
  shows "zero c (region X I r)"
using assms unfolding zero_def by force

lemma zero_Const:
  assumes "finite X" "valid_region X k I r" "c  X" "zero c (region X I r)"
  shows "I c = Const 0"
proof -
  from assms obtain u where "u  region X I r" by atomize_elim (auto intro: region_not_empty)
  with assms show ?thesis unfolding zero_def by (auto intro: const_ConstD)
qed

lemma zero_all:
  assumes "finite X" "valid_region X k I r" "c  X" "u  region X I r" "u c = 0"
  shows "zero c (region X I r)"
proof -
  from assms have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
  then have "I c = Const 0" using assms(5) by cases auto
  with assms have "u' c = 0" if "u'  region X I r" for u' using that by force
  then show ?thesis unfolding zero_def by blast
qed


section ‹Reachability›

subsection ‹Definitions›

locale Probabilistic_Timed_Automaton_Regions_Reachability =
  Probabilistic_Timed_Automaton_Regions k v n not_in_X A
    for k v n not_in_X and A :: "('c, t, 's) pta" +
  fixes φ ψ :: "('s * ('c, t) cval)  bool" fixes s
  assumes φ: " x y. x  S  timed_bisim x y  φ x  φ y"
  assumes ψ: " x y. x  S  timed_bisim x y  ψ x  ψ y"
  assumes s[intro, simp]: "s  S"
begin

definition "φ'  absp φ"
definition "ψ'  absp ψ"
definition "s'  abss s"

lemma s_s'_cfg_on[intro]:
  assumes "cfg  MDP.cfg_on s"
  shows "absc cfg  R_G.cfg_on s'"
proof -
  from assms s have "cfg  valid_cfg" unfolding MDP.valid_cfg_def by auto
  then have "absc cfg  R_G.cfg_on (state (absc cfg))" by (auto intro: R_G.valid_cfgD)
  with assms show ?thesis unfolding s'_def by (auto simp: state_absc)
qed

lemma s'_𝒮[simp, intro]:
  "s'  𝒮"
  unfolding s'_def using s by auto

lemma s'_s_cfg_on[intro]:
  assumes "cfg  R_G.cfg_on s'"
  shows "repcs s cfg  MDP.cfg_on s"
proof -
  from assms s have "cfg  R_G.valid_cfg" unfolding R_G.valid_cfg_def by auto
  with assms have "repcs s cfg  valid_cfg" by (auto simp: s'_def intro: R_G.valid_cfgD)
  then show ?thesis by (auto dest: MDP.valid_cfgD)
qed

lemma (in Probabilistic_Timed_Automaton_Regions) compatible_stream:
  assumes φ: " x y. x  S  x ~ y  φ x  φ y"
  assumes "pred_stream (λs. s  S) xs"
      and [intro]: "x  S"
    shows "pred_stream (λs. φ (reps (abss s)) = φ s) (x ## xs)"
unfolding stream.pred_set proof clarify
  fix l u
  assume A: "(l, u)  sset (x ## xs)"
  from assms have "pred_stream (λs. s  S) (x ## xs)" by auto
  with A have "(l, u)  S" by (fastforce simp: stream.pred_set)
  then have "abss (l, u)  𝒮" by auto
  then have "reps (abss (l, u)) ~ (l, u)" by simp
  with φ (l, u)  S show "φ (reps (abss (l, u))) = φ (l, u)" by blast
qed

lemma φ_stream':
  "pred_stream (λs. φ (reps (abss s)) = φ s) (x ## xs)" if "pred_stream (λs. s  S) xs" "x  S"
  using compatible_stream[of φ, OF φ that] .

lemma ψ_stream':
  "pred_stream (λs. ψ (reps (abss s)) = ψ s) (x ## xs)" if "pred_stream (λs. s  S) xs" "x  S"
  using compatible_stream[of ψ, OF ψ that] .

lemmas φ_stream = compatible_stream[of φ, OF φ]
lemmas ψ_stream = compatible_stream[of ψ, OF ψ]

subsection ‹Easier Result on All Configurations›

(* TODO: Rename *)
lemma suntil_reps:
  assumes
    "ssset (smap abss y). s  𝒮"
    "(holds φ' suntil holds ψ') (s' ## smap abss y)"
  shows "(holds φ suntil holds ψ) (s ## y)"
  using assms
  by (subst region_compatible_suntil[symmetric]; (intro φ_stream ψ_stream)?)
     (auto simp: φ'_def ψ'_def absp_def stream.pred_set 𝒮_abss_S s'_def comp_def)

(* TODO: Rename *)
lemma suntil_abss:
  assumes
    "ssset y. s  S"
    "(holds φ suntil holds ψ) (s ## y)"
  shows
    "(holds φ' suntil holds ψ') (s' ## smap abss y)"
  using assms
  by (subst (asm) region_compatible_suntil[symmetric]; (intro φ_stream ψ_stream)?)
     (auto simp: φ'_def ψ'_def absp_def stream.pred_set s'_def comp_def)

(* TODO: Generalize to CTL formulae *)
theorem P_sup_sunitl_eq:
  notes [measurable] = in_space_UNIV and [iff] = pred_stream_iff
  shows
    "(MDP.P_sup s  (λx. (holds φ suntil holds ψ)   (s  ## x)))
   = (R_G.P_sup s' (λx. (holds φ' suntil holds ψ') (s' ## x)))"
  unfolding MDP.P_sup_def R_G.P_sup_def
proof (rule SUP_eq, goal_cases)
  case prems: (1 cfg)
  let ?cfg' = "absc cfg"
  from prems have "cfg  valid_cfg" by (auto intro: MDP.valid_cfgI)
  then have "?cfg'  R_G.valid_cfg" by (auto intro: R_G.valid_cfgI)
  from cfg  valid_cfg have alw_S: "almost_everywhere (MDP.T cfg) (pred_stream (λs. s  S))"
    by (rule MDP.alw_S)
  from ?cfg' R_G.valid_cfg have alw_𝒮: "almost_everywhere (R_G.T ?cfg') (pred_stream (λs. s  𝒮))"
    by (rule R_G.alw_S)
  have "emeasure (MDP.T cfg) {x  space MDP.St. (holds φ suntil holds ψ) (s ## x)}
       = emeasure (R_G.T ?cfg') {x  space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}"
    apply (rule path_measure_eq_absc1_new[symmetric, where P = "pred_stream (λ s. s  𝒮)"
          and Q = "pred_stream (λ s. s  S)"]
        )
    using prems alw_S alw_𝒮 apply (auto intro: MDP.valid_cfgI simp: )[7]
    by (auto simp: S_abss_𝒮 intro: 𝒮_abss_S intro!: suntil_abss suntil_reps, measurable)
  with prems show ?case by (inst_existentials ?cfg') auto
next
  case prems: (2 cfg)
  let ?cfg' = "repcs s cfg"
  have "s = state ?cfg'" by simp
  from prems have "s' = state cfg" by auto
  have "pred_stream (λs. φ (reps (abss s)) = φ s) (state (repcs s cfg) ## x)"
    if "pred_stream (λs. s  S) x" for x
    using prems that by (intro φ_stream) auto
  moreover
  have "pred_stream (λs. ψ (reps (abss s)) = ψ s) (state (repcs s cfg) ## x)"
    if "pred_stream (λs. s  S) x" for x
    using prems that by (intro ψ_stream) auto
  ultimately
  have "emeasure (R_G.T cfg) {x  space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}
    = emeasure (MDP.T (repcs s cfg)) {x  space MDP.St. (holds φ suntil holds ψ) (s ## x)}"
    apply (rewrite in "s ## _" s = _)
    apply (subst s' = _)
    unfolding φ'_def ψ'_def s'_def
    apply (rule path_measure_eq_repcs''_new)
    using prems by (auto 4 3 simp: s'_def intro: R_G.valid_cfgI MDP.valid_cfgI)
  with prems show ?case by (inst_existentials ?cfg') auto
qed

end (* PTA Reachability Problem *)


subsection ‹Divergent Adversaries›

context Probabilistic_Timed_Automaton
begin

  definition "elapsed u u'  Max ({u' c - u c | c. c  𝒳}  {0})"

  definition "eq_elapsed u u'  elapsed u u' > 0  ( c  𝒳. u' c - u c = elapsed u u')"

  fun dur :: "('c, t) cval stream  nat  t" where
    "dur _ 0 = 0" |
    "dur (x ## y ## xs) (Suc i) = elapsed x y + dur (y ## xs) i"

  definition "divergent ω   t.  n. dur ω n > t"

  definition "div_cfg cfg  AE ω in MDP.MC.T cfg. divergent (smap (snd o state) ω)"

  definition "ℛ_div ω 
    x  𝒳. ( i. ( j  i. zero x (ω !! j))  ( j  i. ¬ zero x (ω !! j)))
       ( i.  j  i. unbounded x (ω !! j))"

  definition "R_G_div_cfg cfg  AE ω in MDP.MC.T cfg. ℛ_div (smap (snd o state) ω)"

end

context Probabilistic_Timed_Automaton_Regions
begin

definition "cfg_on_div st  MDP.cfg_on st  {cfg. div_cfg cfg}"

definition "R_G_cfg_on_div st  R_G.cfg_on st  {cfg. R_G_div_cfg cfg}"

lemma measurable_ℛ_div[measurable]: "Measurable.pred MDP.MC.S ℛ_div"
  unfolding ℛ_div_def
  by (intro
        pred_intros_finite[OF beta_interp.finite]
        pred_intros_logic pred_intros_countable
        measurable_count_space_const measurable_compose[OF measurable_snth]
     ) measurable

lemma elapsed_ge0[simp]: "elapsed x y  0"
  unfolding elapsed_def using finite(1) by auto

lemma dur_pos:
  "dur xs i  0"
 apply (induction i arbitrary: xs)
 apply (auto; fail)
 subgoal for i xs
   apply (subst stream.collapse[symmetric])
   apply (rewrite at "stl xs" stream.collapse[symmetric])
   apply (subst dur.simps)
 by simp
done

lemma dur_mono:
  "i  j  dur xs i  dur xs j"
proof (induction i arbitrary: xs j)
  case 0 show ?case by (auto intro: dur_pos)
next
  case (Suc i xs j)
  obtain x y ys where xs: "xs = x ## y ## ys" using stream.collapse by metis
  from Suc obtain j' where j': "j = Suc j'" by (cases j) auto
  with xs have "dur xs j = elapsed x y + dur (y ## ys) j'" by auto
  also from Suc j' have "  elapsed x y + dur (y ## ys) i" by auto
  also have "elapsed x y + dur (y ## ys) i = dur xs (Suc i)" by (simp add: xs)
  finally show ?case .
qed

lemma dur_monoD:
  assumes "dur xs i < dur xs j"
  shows "i < j" using assms
 by - (rule ccontr; auto 4 4 dest: leI dur_mono[where xs = xs])

lemma elapsed_0D:
  assumes "c  𝒳" "elapsed u u'  0"
  shows "u' c - u c  0"
proof -
  from assms have "u' c - u c  {u' c - u c | c. c  𝒳}  {0}" by auto
  with finite(1) have "u' c - u c  Max ({u' c - u c | c. c  𝒳}  {0})" by auto
  with assms(2) show ?thesis unfolding elapsed_def by auto
qed

lemma elapsed_ge:
  assumes "eq_elapsed u u'" "c  𝒳"
  shows "elapsed u u'  u' c - u c"
  using assms unfolding eq_elapsed_def by (auto intro: elapsed_ge0 order.trans[OF elapsed_0D])

lemma elapsed_eq:
  assumes "eq_elapsed u u'" "c  𝒳" "u' c - u c  0"
  shows "elapsed u u' = u' c - u c"
  using elapsed_ge[OF assms(1,2)] assms unfolding eq_elapsed_def by auto

lemma dur_shift:
  "dur ω (i + j) = dur ω i + dur (sdrop i ω) j"
 apply (induction i arbitrary: ω)
  apply simp
 subgoal for i ω
  apply simp
  apply (subst stream.collapse[symmetric])
  apply (rewrite at "stl ω" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply (rewrite in "dur ω" stream.collapse[symmetric])
  apply (rewrite in "dur (_ ## ) (Suc _)" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
 done
done

lemma dur_zero:
  assumes
    " i. xs !! i  ω !! i" " j  i. zero x (ω !! j)" "x  𝒳"
    " i. eq_elapsed (xs !! i) (xs !! Suc i)"
  shows "dur xs i = 0" using assms
proof (induction i arbitrary: xs ω)
  case 0
  then show ?case by simp
next
  case (Suc i xs ω)
  let ?x = "xs !! 0"
  let ?y = "xs !! 1"
  let ?ys = "stl (stl xs)"
  have xs: "xs = ?x ## ?y ## ?ys" by auto
  from Suc.prems have
    " i. (?y ## ?ys) !! i  stl ω !! i" " j  i. zero x (stl ω !! j)"
    " i. eq_elapsed (stl xs !! i) (stl xs !! Suc i)"
    by (metis snth.simps(2) | auto)+
  from Suc.IH[OF this(1,2) x  _] this(3) have [simp]: "dur (stl xs) i = 0" by auto
  from Suc.prems(1,2) have "?y x = 0" "?x x = 0" unfolding zero_def by force+
  then have *: "?y x - ?x x = 0" by simp
  have "dur xs (Suc i) = elapsed ?x ?y"
    apply (subst xs)
    apply (subst dur.simps)
    by simp
  also have " = 0"
    apply (subst elapsed_eq[OF _ x  _])
    unfolding One_nat_def using Suc.prems(4) apply blast
    using * by auto
  finally show ?case .
qed

lemma dur_zero_tail:
  assumes " i. xs !! i  ω !! i" " k  i. k  j  zero x (ω !! k)" "x  𝒳" "j  i"
          " i. eq_elapsed (xs !! i) (xs !! Suc i)"
  shows "dur xs j = dur xs i"
proof -
  from j  i dur_shift[of xs i "j - i"] have
    "dur xs j = dur xs i + dur (sdrop i xs) (j - i)"
  by simp
  also have " = dur xs i"
    using assms
    by (rewrite in "dur (sdrop _ _) _" dur_zero[where ω = "sdrop i ω"])
       (auto dest: prop_nth_sdrop_pair[of eq_elapsed] prop_nth_sdrop prop_nth_sdrop_pair[of "(∈)"])
  finally show ?thesis .
qed

lemma elapsed_ge_pos:
  fixes u :: "('c, t) cval"
  assumes "eq_elapsed u u'" "c  𝒳" "u  V" "u'  V"
  shows "elapsed u u'  u' c"
proof (cases "elapsed u u' = 0")
  case True
  with assms show ?thesis by (auto simp: V_def)
next
  case False
  from u  V c  𝒳 have "u c  0" by (auto simp: V_def)
  from False assms have "elapsed u u' = u' c - u c"
    unfolding eq_elapsed_def by (auto simp add: less_le)
  also from u c  0 have "  u' c" by simp
  finally show ?thesis .
qed

lemma dur_Suc:
  "dur xs (Suc i) - dur xs i = elapsed (xs !! i) (xs !! Suc i)"
 apply (induction i arbitrary: xs)
  apply simp
  apply (subst stream.collapse[symmetric])
  apply (rewrite in "stl _" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
 apply simp
 subgoal for i xs
  apply (subst stream.collapse[symmetric])
  apply (rewrite in "stl _" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
  apply (rewrite in "dur xs (Suc _)" stream.collapse[symmetric])
  apply (rewrite at "stl xs" in "_ ## stl xs" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
 done
done

inductive trans where
  succ: "t  0  u' = u  t  trans u u'" |
  reset: "set l  𝒳  u' = clock_set l 0 u  trans u u'" |
  id: "u = u'  trans u u'"

abbreviation "stream_trans  pairwise trans"

lemma K_cfg_trans:
  assumes "cfg  MDP.cfg_on (l, R)" "cfg'  K_cfg cfg" "state cfg' = (l', R')"
  shows "trans R R'"
using assms
 apply (simp add: set_K_cfg)
 apply (drule MDP.cfg_onD_action)
 apply (cases rule: K.cases)
    apply (auto intro: trans.intros)
using admissible_targets_clocks(2) by (blast intro: trans.intros(2))

lemma enabled_stream_trans:
  assumes "cfg  valid_cfg" "MDP.MC.enabled cfg xs"
  shows "stream_trans (smap (snd o state) xs)"
  using assms
proof (coinduction arbitrary: cfg xs)
  case prems: (pairwise cfg xs)
  let ?xs = "stl (stl xs)" let ?x = "shd xs" let ?y = "shd (stl xs)"
  from MDP.pred_stream_cfg_on[OF prems] have *:
    "pred_stream (λcfg. state cfg  S  cfg  MDP.cfg_on (state cfg)) xs" .
  obtain l R l' R' where eq: "state ?x = (l, R)" "state ?y = (l', R')" by force
  moreover from * have "?x  MDP.cfg_on (state ?x)" "?x  valid_cfg"
    by (auto intro: MDP.valid_cfgI simp: stream.pred_set)
  moreover from prems(2) have "?y  K_cfg ?x" by (auto elim: MDP.MC.enabled.cases)
  ultimately have "trans R R'"
    by (intro K_cfg_trans[where cfg = ?x and cfg' = ?y and l = l and l' = l']) metis+
  with ?x  valid_cfg prems(2) show ?case
    apply (inst_existentials R R' "smap (snd o state) ?xs")
      apply (simp add: eq; fail)+
    apply (rule disjI1, inst_existentials ?x "stl xs")
    by (auto simp: eq elim: MDP.MC.enabled.cases)
qed

lemma stream_trans_trans:
  assumes "stream_trans xs"
  shows "trans (xs !! i) (stl xs !! i)"
using pairwise_Suc assms by auto

lemma trans_eq_elapsed:
  assumes "trans u u'" "u  V"
  shows "eq_elapsed u u'"
using assms
proof cases
  case (succ t)
  with finite(1) show ?thesis by (auto simp: cval_add_def elapsed_def max_def eq_elapsed_def)
next
  case prems: (reset l)
  then have "u' c - u c  0" if "c  𝒳" for c
  using that u  V by (cases "c  set l") (auto simp: V_def)
  then have "elapsed u u' = 0" unfolding elapsed_def using finite(1)
   apply simp
   apply (subst Max_insert2)
  by auto
  then show ?thesis by (auto simp: eq_elapsed_def)
next
  case id
  then show ?thesis
    using finite(1) by (auto simp: Max_gr_iff elapsed_def eq_elapsed_def)
qed

lemma pairwise_trans_eq_elapsed:
  assumes "stream_trans xs" "pred_stream (λ u. u  V) xs"
  shows "pairwise eq_elapsed xs"
using trans_eq_elapsed assms by (auto intro: pairwise_mp simp: stream.pred_set)

lemma not_reset_dur:
  assumes "k>i. k  j  ¬ zero c ([xs !! k]⇩)" "j  i" "c  𝒳" "stream_trans xs"
    " i. eq_elapsed (xs !! i) (xs !! Suc i)" " i. xs !! i  V"
  shows "dur xs j - dur xs i = (xs !! j) c - (xs !! i) c"
  using assms
proof (induction j)
  case 0 then show ?case by simp
next
  case (Suc j)
  from stream_trans_trans[OF Suc.prems(4)] have trans: "trans (xs !! j) (xs !! Suc j)" by auto
  from Suc.prems have *:
    "¬ zero c ([xs !! Suc j]⇩)" "eq_elapsed (xs !! j) (xs !! Suc j)" if "Suc j > i"
    using that by auto
  from Suc.prems(6) have "xs !! j  V" "xs !! Suc j  V" by blast+
  then have regions: "[xs !! j]⇩  " "[xs !! Suc j]⇩  " by auto
  from trans have "(xs !! Suc j) c - (xs !! j) c  0" if "Suc j > i"
  proof (cases)
    case succ
    with regions show ?thesis by (auto simp: cval_add_def)
  next
    case prems: (reset l)
    show ?thesis
    proof (cases "c  set l")
      case False
      with prems show ?thesis by auto
    next
      case True
      with prems have "(xs !! Suc j) c = 0" by auto
      moreover from assms have "xs !! Suc j  [xs !! Suc j]⇩" by blast
      ultimately have
        "zero c ([xs !! Suc j]⇩)"
        using zero_all[OF finite(1) _ c  𝒳] regions(2) by (auto simp: ℛ_def)
      with * that show ?thesis by auto
    qed
  next
    case id then show ?thesis by simp
  qed
  with * c  𝒳 elapsed_eq have
    *: "elapsed (xs !! j) (xs !! Suc j) = (xs !! Suc j) c - (xs !! j) c"
    if "Suc j > i"
    using that by blast
  show ?case
  proof (cases "i = Suc j")
    case False
    with Suc have
      "dur xs (Suc j) - dur xs i = dur xs (Suc j) - dur xs j + (xs !! j) c - (xs !! i) c"
      by auto
    also have " = elapsed (xs !! j) (xs !! Suc j) + (xs !! j) c - (xs !! i) c"
      by (simp add: dur_Suc)
    also have
      " = (xs !! Suc j) c - (xs !! j) c  + (xs !! j) c - (xs !! i) c"
      using * False Suc.prems by auto
    also have " = (xs !! Suc j) c - (xs !! i) c" by simp
    finally show ?thesis by auto
  next
    case True
    then show ?thesis by simp
  qed
qed

lemma not_reset_dur':
  assumes "ji. ¬ zero c ([xs !! j]⇩)" "j  i" "c  𝒳" "stream_trans xs"
          " i. eq_elapsed (xs !! i) (xs !! Suc i)" " j. xs !! j  V"
  shows "dur xs j - dur xs i = (xs !! j) c - (xs !! i) c"
using assms not_reset_dur by auto

lemma not_reset_unbounded:
  assumes "ji. ¬ zero c ([xs !! j]⇩)" "j  i" "c  𝒳" "stream_trans xs"
          " i. eq_elapsed (xs !! i) (xs !! Suc i)" " j. xs !! j  V"
          "unbounded c ([xs !! i]⇩)"
  shows "unbounded c ([xs !! j]⇩)"
proof -
  let ?u = "xs !! i" let ?u' = "xs !! j" let ?R = "[xs !! i]⇩"
  from assms have "?u  ?R" by auto
  from assms(6) have "?R  " by auto
  then obtain I r where "?R = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  with assms(3,7) unbounded_Greater ?u  ?R have "?u c > k c" by force
  also from not_reset_dur'[OF assms(1-6)] dur_mono[OF j  i, of xs] have "?u' c  ?u c" by auto
  finally have "?u' c > k c" by auto
  let ?R' = "[xs !! j]⇩"
  from assms have "?u'  ?R'" by auto
  from assms(6) have "?R'  " by auto
  then obtain I r where "?R' = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  moreover with ?u' c > _ ?u'  _ gt_GreaterD c  𝒳 have "I c = Greater (k c)" by auto
  ultimately show ?thesis using Greater_unbounded[OF finite(1) _ c  𝒳] by auto
qed

lemma gt_unboundedD:
  assumes "u  R"
    and "R  "
    and "c  𝒳"
    and "real (k c) < u c"
  shows "unbounded c R"
proof -
  from assms obtain I r where "R = region 𝒳 I r" "valid_region 𝒳 k I r"
    unfolding ℛ_def by auto
  with Greater_unbounded[of 𝒳 k I r c] gt_GreaterD[of u 𝒳 I r k c] assms finite(1) show ?thesis
    by auto
qed

definition trans' :: "('c, t) cval  ('c, t) cval  bool" where
  "trans' u u' 
    (( c  𝒳. u c > k c  u' c > k c  u  u')  u' = u  0.5) 
    (( c  𝒳. u c = 0  u' c > 0  (c𝒳. d. d  k c  u' c = real d))
     u' = delayedR ([u']⇩) u)"

(* XXX Move *)
lemma zeroI:
  assumes "c  𝒳" "u  V" "u c = 0"
  shows "zero c ([u]⇩)"
proof -
  from assms have "u  [u]⇩" "[u]⇩  " by auto
  then obtain I r where "[u]⇩ = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  with zero_all[OF finite(1) this(2) c  𝒳] u  [u]⇩ u c = 0 show ?thesis by auto
qed

(* XXX Move, rename *)
lemma zeroD:
  "u x = 0" if "zero x ([u]⇩)" "u  V"
  using that by (metis regions_part_ex(1) zero_def)

lemma not_zeroD:
  assumes "¬ zero x ([u]⇩)" "u  V" "x  𝒳"
  shows "u x > 0"
proof -
  from zeroI assms have "u x  0" by auto
  moreover from assms have "u x  0" unfolding V_def by auto
  ultimately show ?thesis by auto
qed

(* XXX Move *)
lemma not_const_intv:
  assumes "u  V" "c𝒳. d. d  k c  u c = real d"
  shows "c𝒳. u  [u]⇩. d. d  k c  u c = real d"
proof -
  from assms have "u  [u]⇩" "[u]⇩  " by auto
  then obtain I r where I: "[u]⇩ = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  have "d. d  k c  u' c = real d" if "c  𝒳" "u'  [u]⇩" for c u'
  proof safe
    fix d assume A: "d  k c" "u' c = real d"
    from I that have "intv_elem c u' (I c)" "valid_intv (k c) (I c)" by auto
    then show False
      using A I u  [u]⇩ c  𝒳 assms(2) by (cases; fastforce)
  qed
  then show ?thesis by auto
qed

lemma K_cfg_trans':
  assumes "repcs (l, u) cfg  MDP.cfg_on (l, u)" "cfg'  K_cfg (repcs (l, u) cfg)"
          "state cfg' = (l', u')" "(l, u)  S" "cfg  R_G.valid_cfg" "abss (l, u) = state cfg"
  shows "trans' u u'"
using assms
 apply (simp add: set_K_cfg)
 apply (drule MDP.cfg_onD_action)
 apply (cases rule: K.cases)
 apply assumption
proof goal_cases
  case prems: (1 l u t)
  from assms _ = (l, u) have "repcs (l, u) cfg  valid_cfg" by (auto intro: MDP.valid_cfgI)
  then have "absc (repcs (l, u) cfg)  R_G.valid_cfg" by auto
  from prems have *: "rept (l, u) (action cfg) = return_pmf (l, u  t)" unfolding repcs_def by auto
  from abss _ = _ _ = (l, u) cfg  R_G.valid_cfg have
    "action cfg  𝒦 (abss (l, u))"
  by (auto dest: R_G_I)
  from abst_rept_id[OF this] * have "action cfg = abst (return_pmf (l, u  t))" by auto
  with prems have **: "action cfg = return_pmf (l, [u  t]⇩)" unfolding abst_def by auto
  show ?thesis
  proof (cases " c  𝒳. u c > k c")
    case True
    from prems have "u  t  [u]⇩" by (auto intro: upper_right_closed[OF True])
    with prems have "[u  t]⇩ = [u]⇩" by (auto dest: alpha_interp.region_unique_spec)
    with ** have "action cfg = return_pmf (l, [u]⇩)" by simp
    with True have "rept (l, u) (action cfg) = return_pmf (l, u  0.5)" 
    unfolding rept_def using prems by auto
    with * have "u  t = u  0.5" by auto
    moreover from prems have "u' = u  t" by auto
    moreover from prems True have " c  𝒳. u' c > k c" by (auto simp: cval_add_def)
    ultimately show ?thesis using True _ = (l, u) unfolding trans'_def by auto
  next
    case F: False
    show ?thesis
    proof (cases "c𝒳. u c = 0  0 < u' c  (c𝒳. d. d  k c  u' c = real d)")
      case True
      from prems have "u'  [u']⇩" by auto
      from prems have "[u  t]⇩  Succ  ([u]⇩)" by auto
      from True obtain c where "c  𝒳" "u c = 0" "u' c > 0" by auto
      with zeroI prems have "zero c ([u]⇩)" by auto
      moreover from u'  _ u' c > 0 have "¬ zero c ([u']⇩)" unfolding zero_def by fastforce
      ultimately have "[u  t]⇩  [u]⇩" using prems by auto
      moreover from True not_const_intv prems have
        " u  [u  t]⇩. c𝒳. d. d  k c  u c = real d"
      by auto
      ultimately have "R'. (l, u)  S 
                     action cfg = return_pmf (l, R') 
                     R'  Succ  ([u]⇩)  [u]⇩  R'  (uR'. c𝒳. d. d  k c  u c = real d)"
       apply -
       apply (rule exI[where x = "[u  t]⇩"])
       apply safe
      using prems ** by auto
      then have
        "rept (l, u) (action cfg)
       = return_pmf (l, delayedR (SOME R'. action cfg = return_pmf (l, R')) u)" 
      unfolding rept_def by auto
      with * ** prems have "u' = delayedR ([u  t]⇩) u" by auto
      with F True prems show ?thesis unfolding trans'_def by auto
    next
      case False
      with F _ = (l, u) show ?thesis unfolding trans'_def by auto
    qed
  qed
next
  case prems: (2 _ _ τ μ)
  then obtain X where X: "u' = ([X := 0]u)" "(X, l')  set_pmf μ" by auto
  from _  S have "u  V" by auto
  let ?r = "SOME r. set r = X"
  show ?case
  proof (cases "X = {}")
    case True
    with X have "u = u'" by auto
    with non_empty show ?thesis unfolding trans'_def by auto
  next
    case False
    then obtain x where "x  X" by auto
    moreover have "X  𝒳" using admissible_targets_clocks(1)[OF prems(10) X(2)] by auto
    ultimately have "x  𝒳" by auto
    from X  𝒳 finite(1) obtain r where "set r = X" using finite_list finite_subset by blast
    then have r: "set ?r = X" by (rule someI)
    with x  X X have "u' x = 0" by auto
    from X r u  V X  𝒳 have "u' x  u x" for x
      by (cases "x  X"; auto simp: V_def)
    have False if "u' x > 0  u x = 0" for x
      using u' _  _[of x] that by auto
    with u' x = 0 show ?thesis using x  𝒳 unfolding trans'_def by auto
  qed
next
  case 3
  with non_empty show ?case unfolding trans'_def by auto
qed

coinductive enabled_repcs where
  "enabled_repcs (shd xs) (stl xs)  shd xs = repcs st' cfg'  st'  rept st (action cfg)
   abss st' = state cfg'
   cfg'  R_G.valid_cfg
   enabled_repcs (repcs st cfg) xs"

(* XXX Move *)
lemma K_cfg_rept_in:
assumes "cfg  R_G.valid_cfg"
    and "abss st = state cfg"
    and "cfg'  K_cfg cfg"
  shows "(THE s'. s'  set_pmf (rept st (action cfg))  abss s' = state cfg')
          set_pmf (rept st (action cfg))"
proof -
  from assms(1,2) have "action cfg  𝒦 (abss st)" by (auto simp: R_G_I)
  from cfg'  _ have
    "cfg' = cont cfg (state cfg')" "state cfg'  action cfg"
  by (auto simp: set_K_cfg)
  with abst_rept_id[OF action _  _] pmf.set_map have
    "state cfg'  abss ` set_pmf (rept st (action cfg))" unfolding abst_def  by metis
  then obtain st' where
    "st'  rept st (action cfg)" "abss st' = state cfg'"
  unfolding abst_def by auto
  with K_cfg_rept_aux[OF assms(1,2) this(1)] show ?thesis by auto
qed

lemma enabled_repcsI:
  assumes "cfg  R_G.valid_cfg" "abss st = state cfg" "MDP.MC.enabled (repcs st cfg) xs"
  shows "enabled_repcs (repcs st cfg) xs" using assms
proof (coinduction arbitrary: cfg xs st)
  case prems: (enabled_repcs cfg xs st)
  let ?x = "shd xs" and ?y = "shd (stl xs)"
  let ?st = "THE s'. s'  set_pmf (rept st (action cfg))  abss s' = state (absc ?x)"
  from prems(3) have "?x  K_cfg (repcs st cfg)" by cases
  with K_cfg_map_repcs[OF prems(1,2)] obtain cfg' where
    "cfg'  K_cfg cfg" "?x = repcs (THE s'. s'  rept st (action cfg)  abss s' = state cfg') cfg'"
    by auto
  let ?st = "THE s'. s'  rept st (action cfg)  abss s' = state cfg'"
  from K_cfg_rept_action[OF prems(1,2) cfg'  _] have "abss ?st = state cfg'" .
  moreover from K_cfg_rept_in[OF prems(1,2) cfg'  _] have "?st  rept st (action cfg)" .
  moreover have "cfg'  R_G.valid_cfg" using cfg'  K_cfg cfg prems(1) by blast 
  moreover from absc_repcs_id[OF this abss ?st = state cfg'] ?x = _ have "absc ?x = cfg'"
    by auto
  moreover from prems(3) have "MDP.MC.enabled (shd xs) (stl xs)" by cases
  ultimately show ?case
    using ?x = _ by (inst_existentials xs ?st "absc ?x" st cfg) fastforce+
qed

lemma repcs_eq_rept:
  "rept st (action cfg) = rept st'' (action cfg'')" if "repcs st cfg = repcs st'' cfg''"
   by (metis (mono_tags, lifting) action_cfg_corec old.prod.case repcs_def that)

lemma enabled_stream_trans':
  assumes "cfg  R_G.valid_cfg" "abss st = state cfg" "MDP.MC.enabled (repcs st cfg) xs"
  shows "pairwise trans' (smap (snd o state) xs)"
using assms
proof (coinduction arbitrary: cfg xs st)
  case prems: (pairwise cfg xs)
  let ?xs = "stl xs"
  from prems have A: "enabled_repcs (repcs st cfg) xs" by (auto intro: enabled_repcsI)
  then obtain st' cfg' where
    "enabled_repcs (shd xs) (stl xs)" "shd xs = repcs st' cfg'" "st'  rept st (action cfg)"
    "abss st' = state cfg'" "cfg'  R_G.valid_cfg"
   apply atomize_elim
   apply (cases rule: enabled_repcs.cases)
   apply assumption
   subgoal for st' cfg' st'' cfg''
     by (inst_existentials st' cfg') (auto dest: repcs_eq_rept)
  done
  then obtain st'' cfg'' where
    "enabled_repcs (shd ?xs) (stl ?xs)"
    "shd ?xs = repcs st'' cfg''" "st''  rept st' (action cfg')" "abss st'' = state cfg''"
    by atomize_elim (subst (asm)enabled_repcs.simps, fastforce dest: repcs_eq_rept)
  let ?x = "shd xs" let ?y = "shd (stl xs)"
  let ?cfg = "repcs st cfg"
  from prems have "?cfg  valid_cfg" by auto
  from MDP.pred_stream_cfg_on[OF ?cfg  valid_cfg prems(3)] have *:
    "pred_stream (λcfg. state cfg  S  cfg  MDP.cfg_on (state cfg)) xs" .
  obtain l u l' u' where eq: "st' = (l, u)" "st'' = (l', u')"
    by force
  moreover from * have
    "?x  MDP.cfg_on (state ?x)" "?x  valid_cfg"
    by (auto intro: MDP.valid_cfgI simp: stream.pred_set)
  moreover from prems(3) have "?y  K_cfg ?x" by (auto elim: MDP.MC.enabled.cases)
  ultimately have "trans' u u'"
    using ?x = _ ?y = _ cfg'  _ abss st' = _
    by (intro K_cfg_trans') (auto dest: MDP.valid_cfg_state_in_S)
  with ?x  valid_cfg cfg'  R_G.valid_cfg prems(3) abss _ = state cfg' show ?case
    apply (inst_existentials u u' "smap (snd o state) (stl ?xs)")
    apply (simp add: eq ?x = _ ?y = _; fail)+
    by ((intro disjI1 exI)?; auto simp: ?x = _ ?y = _ eq elim: MDP.MC.enabled.cases)
qed

lemma divergent_ℛ_divergent:
  assumes in_S: "pred_stream (λ u. u  V) xs"
     and  div:  "divergent xs"
     and trans: "stream_trans xs"
  shows "ℛ_div (smap (λ u. [u]⇩) xs)" (is "ℛ_div ")
unfolding ℛ_div_def proof (safe, simp_all)
  fix x i
  assume x: "x  𝒳" and bounded: "i. ji. ¬ unbounded x ([xs !! j]⇩)"
  from in_S have xs_ω: "i. xs !! i   !! i" by (auto simp: stream.pred_set)
  from trans in_S have elapsed:
    " i. eq_elapsed (xs !! i) (xs !! Suc i)"
    by (fastforce intro: pairwise_trans_eq_elapsed pairwise_Suc[where P = eq_elapsed])
  { assume A: "j  i. ¬ zero x ([xs !! j]⇩)"
    let ?t = "dur xs i + k x"
    from div obtain j where j: "dur xs j > dur xs i + k x" unfolding divergent_def by auto
    then have "k x < dur xs j - dur xs i" by auto
    also with not_reset_dur'[OF A less_imp_le[OF dur_monoD], of xs] x  𝒳 assms elapsed have
      " = (xs !! j) x - (xs !! i) x"
      by (auto simp: stream.pred_set)
    also have "  (xs !! j) x"
      using assms(1) x  𝒳 unfolding V_def by (auto simp: stream.pred_set)
    finally have "unbounded x ([xs !! j]⇩)"
      using assms x  𝒳 by (intro gt_unboundedD) (auto simp: stream.pred_set)
    moreover from dur_monoD[of xs i j] j A have "j'  j. ¬ zero x ([xs !! j']⇩)" by auto
    ultimately have "ij. unbounded x ([xs !! i]⇩)"
      using elapsed assms x by (auto intro: not_reset_unbounded simp: stream.pred_set)
    with bounded have False by auto
  }
  then show "ji. zero x ([xs !! j]⇩)" by auto
  { assume A: "j  i. zero x ([xs !! j]⇩)"
    from div obtain j where j: "dur xs j > dur xs i" unfolding divergent_def by auto
    then have "j  i" by (auto dest: dur_monoD)
    from A have "j  i. zero x ( !! j)" by auto
    with dur_zero_tail[OF xs_ω _ x i  j elapsed] j have False by simp
  }
  then show "ji. ¬ zero x ([xs !! j]⇩)" by auto
qed

lemma (in -)
  fixes f :: "nat  real"
  assumes " i. f i  0" " i.  j  i. f j > d" "d > 0"
  shows " n. ( i  n. f i) > t"
  oops

(* TODO: Reduce this proof to a more general theorem *)
lemma dur_ev_exceedsI:
  assumes " i.  j  i. dur xs j - dur xs i  d" and "d > 0"
  obtains i where "dur xs i > t"
proof -
  have base: " i. dur xs i > t" if "t < d" for t
  proof -
    from assms obtain j where "dur xs j - dur xs 0  d" by fastforce
    with dur_pos[of xs 0] have "dur xs j  d" by simp
    with d > 0 t < d show ?thesis by - (rule exI[where x = j]; auto)
  qed
  have base2: " i. dur xs i > t" if "t  d" for t
  proof (cases "t = d")
    case False
    with t  d base show ?thesis by simp
  next
    case True
    from base d > 0 obtain i where "dur xs i > 0" by auto
    moreover from assms obtain j where "dur xs j - dur xs i  d" by auto
    ultimately have "dur xs j > d" by auto
    with t = d show ?thesis by auto
  qed
  show ?thesis
  proof (cases "t  0")
    case False
    with dur_pos have "dur xs 0 > t" by auto
    then show ?thesis by (fastforce intro: that)
  next
    case True
    let ?m = "nat t / d"
    from True have " i. dur xs i > ?m * d"
    proof (induction ?m arbitrary: t)
      case 0
      with base[OF 0 < d] show ?case by simp
    next
      case (Suc n t)
      let ?t = "t - d"
      show ?case
      proof (cases "t  d")
        case True
        have "?t / d = t / d - 1"
        (* Generated by sledgehammer *)
        (* Alternative: by (smt assms(2) diff_divide_distrib divide_self_if) *)
        proof -
          have "t / d + - 1 * ((t + - 1 * d) / d) + - 1 * (d / d) = 0"
            by (simp add: diff_divide_distrib)
          then have "t / d + - 1 * ((t + - 1 * d) / d) = 1"
            using assms(2) by fastforce
          then show ?thesis
            by algebra
        qed
        then have "?t / d = t / d - 1" by simp
        with Suc n = _ have "n = nat ?t / d" by simp
        with Suc t  d obtain i where "nat ?t / d * d < dur xs i" by fastforce
        from assms obtain j where "dur xs j - dur xs i  d" "j  i" by auto
        with dur xs i > _ have "nat ?t / d * d + d < dur xs j" by simp
        with True have "dur xs j > nat t / d * d"
        by (metis Suc.hyps(2) n = nat (t - d) / d add.commute distrib_left mult.commute 
                  mult.right_neutral of_nat_Suc) 
        then show ?thesis by blast
      next
        case False
        with t  0 d > 0 have "nat t / d  1" by simp
        then have "nat t / d * d  d"
        by (metis One_nat_def Suc n = _ Suc_leI add.right_neutral le_antisym mult.commute
                  mult.right_neutral of_nat_0 of_nat_Suc order_refl zero_less_Suc) 
        with base2 show ?thesis by auto
      qed
    qed
    then obtain i where "dur xs i > ?m * d" by atomize_elim
    moreover from t  0 d > 0 have "?m * d  t"
      using pos_divide_le_eq real_nat_ceiling_ge by blast
    ultimately show ?thesis using that[of i] by simp
  qed
qed

lemma not_reset_mono:
  assumes "stream_trans xs" "shd xs c1  shd xs c2" "stream_all (λ u. u  V) xs" "c2  𝒳"
  shows "(holds (λ u. u c1  u c2) until holds (λ u. u c1 = 0)) xs" using assms
proof (coinduction arbitrary: xs)
  case prems: (UNTIL xs)
  let ?xs = "stl xs"
  let ?x = "shd xs"
  let ?y = "shd ?xs"
  show ?case
  proof (cases "?x c1 = 0")
    case False
    show ?thesis
    proof (cases "?y c1 = 0")
      case False
      from prems have "trans ?x ?y" by (intro pairwise_pairD[of trans])
      then have "?y c1  ?y c2"
      proof cases
        case A: (reset t)
        show ?thesis
        proof (cases "c1  set t")
          case True
          with A False show ?thesis by auto
        next
          case False
          from prems have "?x c2  0" by (auto simp: V_def)
          with A have "?y c2  ?x c2" by (cases "c2  set t") auto
          with A False ?x c1  ?x c2 show ?thesis by auto
        qed
      qed (use prems in auto simp: cval_add_def)
      moreover from prems have "stream_trans ?xs" "stream_all (λ u. u  V) ?xs"
        by (auto intro: pairwise_stlD stl_sset)
      ultimately show ?thesis
        using prems by auto
    qed (use prems in auto intro: UNTIL.base)
  qed auto
qed

lemma ℛ_divergent_divergent_aux:
  fixes xs :: "('c, t) cval stream"
  assumes "stream_trans xs" "stream_all (λ u. u  V) xs"
          "(xs !! i) c1 = 0" " k > i. k  j  (xs !! k) c2 = 0"
          " k > i. k  j  (xs !! k) c1  0"
          "c1  𝒳" "c2  𝒳"
  shows "(xs !! j) c1  (xs !! j) c2"
proof -
  from assms obtain k where k: "k > i" "k  j" "(xs !! k) c2 = 0" by auto
  with assms(5) k  j have "(xs !! k) c1  0" by auto
  moreover from assms(2) c1  𝒳 have "(xs !! k) c1  0" by (auto simp: V_def)
  ultimately have "(xs !! k) c1 > 0" by auto
  with (xs !! k) c2 = 0 have "shd (sdrop k xs) c1  shd (sdrop k xs) c2" by auto
  from not_reset_mono[OF _ this] assms have
    "(holds (λu. u c2  u c1) until holds (λu. u c1 = 0)) (sdrop k xs)"
  by (auto intro: sset_sdrop pairwise_sdropD)
  from assms(5) k(2) k > i have " m  j - k. (sdrop k xs !! m) c1  0" by simp
  with holds_untilD[OF (_ until _) _, of "j - k"] have
    "(sdrop k xs !! (j - k)) c2  (sdrop k xs !! (j - k)) c1" .
  then show "(xs !! j) c2  (xs !! j) c1" using k(1,2) by simp
qed

lemma unbounded_all:
  assumes "R  " "u  R" "unbounded x R" "x  𝒳"
  shows "u x > k x"
proof -
  from assms obtain I r where R: "R = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  with unbounded_Greater x  𝒳 assms(3) have "I x = Greater (k x)" by simp
  with u  R R x  𝒳 show ?thesis by force
qed

lemma trans_not_delay_mono:
  "u' c  u c" if "trans u u'" "u  V" "x  𝒳" "u' x = 0" "c  𝒳"
  using trans u u'
proof (cases)
  case (reset l)
  with that show ?thesis by (cases "c  set l") (auto simp: V_def)
qed (use that in auto simp: cval_add_def V_def add_nonneg_eq_0_iff)

lemma dur_reset:
  assumes "pairwise eq_elapsed xs" "pred_stream (λ u. u  V) xs" "zero x ([xs !! Suc i]⇩)" "x  𝒳"
  shows "dur xs (Suc i) - dur xs i = 0"
proof -
  from assms(2) have in_V: "xs !! Suc i  V"
    unfolding stream.pred_set by auto (metis snth.simps(2) snth_sset)
  with elapsed_ge_pos[of "xs !! i" "xs !! Suc i" x] pairwise_Suc[OF assms(1)] assms(2-) have
    "elapsed (xs !! i) (xs !! Suc i)  (xs !! Suc i) x"
    unfolding stream.pred_set by auto
  with in_V assms(3) have "elapsed (xs !! i) (xs !! Suc i)  0" by (auto simp: zeroD)
  with elapsed_ge0[of "xs !! i" "xs !! Suc i"] have "elapsed (xs !! i) (xs !! Suc i) = 0"
    by linarith
  then show ?thesis by (subst dur_Suc)
qed

lemma resets_mono_0':
  assumes "pairwise eq_elapsed xs" "stream_all (λ u. u  V) xs" "stream_trans xs"
          " j  i. zero x ([xs !! j]⇩)" "x  𝒳" "c  𝒳"
  shows "(xs !! i) c = (xs !! 0) c  (xs !! i) c = 0"
using assms proof (induction i)
  case 0
  then show ?case by auto
next        
  case (Suc i)
  from Suc.prems have *: "(xs !! Suc i) x = 0" "(xs !! i) x = 0"
    by (blast intro: zeroD snth_sset, force intro: zeroD snth_sset)
  from pairwise_Suc[OF Suc.prems(3)] have "trans (xs !! i) (xs !! Suc i)" .
  then show ?case
  proof cases
    case prems: (succ t)
    with * have "t = 0" unfolding cval_add_def by auto
    with prems have "(xs !! Suc i) c = (xs !! i) c" unfolding cval_add_def by auto
    with Suc show ?thesis by auto
  next
    case prems: (reset l)
    then have "(xs !! Suc i) c = 0  (xs !! Suc i) c = (xs !! i) c" by (cases "c  set l") auto
    with Suc show ?thesis by auto
  next
    case id
    with Suc show ?thesis by auto
  qed
qed

lemma resets_mono':
  assumes "pairwise eq_elapsed xs" "pred_stream (λ u. u  V) xs" "stream_trans xs"
          " k  i. k  j  zero x ([xs !! k]⇩)" "x  𝒳" "c  𝒳" "i  j"
  shows "(xs !! j) c = (xs !! i) c  (xs !! j) c = 0" using assms
proof -
  from assms have 1: "stream_all (λ u. u  V) (sdrop i xs)"
    using sset_sdrop unfolding stream.pred_set by force
  from assms have 2: "pairwise eq_elapsed (sdrop i xs)" by (intro pairwise_sdropD)
  from assms have 3: "stream_trans (sdrop i xs)" by (intro pairwise_sdropD)
  from assms have 4:
    "kj - i. zero x ([sdrop i xs !! k]⇩)"
  by (simp add: le_diff_conv2 assms(6))
  from resets_mono_0'[OF 2 1 3 4 assms(5,6)] i  j show ?thesis by simp
qed

lemma resets_mono:
  assumes "pairwise eq_elapsed xs" "pred_stream (λ u. u  V) xs" "stream_trans xs"
          " k  i. k  j  zero x ([xs !! k]⇩)" "x  𝒳" "c  𝒳" "i  j"
  shows "(xs !! j) c  (xs !! i) c" using assms
  using assms by (auto simp: V_def dest: resets_mono'[where c = c] simp: stream.pred_set)

lemma ℛ_divergent_divergent_aux2:
  fixes M :: "(nat  bool) set"
  assumes " i.  P  M.  j  i. P j" "M  {}" "finite M"
  shows "i.ji.k>j. P  M. P j  P k  ( m < k. j < m  ¬ P m)
        ( Q  M.  m  k. j < m  Q m)"
proof
  fix i
  let ?j1 = "Max {LEAST m. m > i  P m | P. P  M}"
  from M  {} obtain P where "P  M" by auto
  let ?m = "LEAST m. m > i  P m"
  from assms(1) P  M obtain j where "j  Suc i" "P j" by auto
  then have "j > i" "P j" by auto
  with P  M have "?m > i  P ?m" by - (rule LeastI; auto)
  moreover with finite M P  M have "?j1  ?m" by - (rule Max_ge; auto)
  ultimately have "?j1  i" by simp
  moreover have " m > i. m  ?j1  P m" if "P  M" for P
  proof -
    let ?m = "LEAST m. m > i  P m"
    from assms(1) P  M obtain j where "j  Suc i" "P j" by auto
    then have "j > i" "P j" by auto
    with P  M have "?m > i  P ?m" by - (rule LeastI; auto)
    moreover with finite M P  M have "?j1  ?m" by - (rule Max_ge; auto)
    ultimately show ?thesis by auto
  qed
  ultimately obtain j1 where j1: "j1  i" " P  M.  m > i. j1  m  P m" by auto
  define k where "k Q = (LEAST k. k > j1  Q k)" for Q
  let ?k = "Max {k Q | Q. Q  M}"
  let ?P = "SOME P. P  M  k P = ?k"
  let ?j = "Max {j. i  j  j  j1  ?P j}"
  have "?k  {k Q | Q. Q  M}" using assms by - (rule Max_in; auto)
  then obtain P where P: "k P = ?k" "P  M" by auto
  have "?k  k Q" if "Q  M" for Q using assms that by - (rule Max_ge; auto)
  have *: "?P  M  k ?P = ?k" using P by - (rule someI[where x = P]; auto)
  with j1 have " m > i. j1  m  ?P m" by auto
  with finite _ have "?j  {j. i  j  j  j1  ?P j}" by - (rule Max_in; auto)
  have k: "k Q > j1  Q (k Q)" if "Q  M" for Q
  proof -
    from assms(1) Q  M obtain m where "m  Suc j1" "Q m" by auto
    then have "m > j1" "Q m" by auto
    then show "k Q > j1  Q (k Q)" unfolding k_def by - (rule LeastI; blast)
  qed
  with * ?j  _ have "?P ?k" "?j < ?k" by fastforce+
  have "¬ ?P m" if "?j < m" "m < ?k" for m
  proof (rule ccontr, simp)
    assume "?P m"
    have "m > j1"
    proof (rule ccontr)
      assume "¬ j1 < m"
      with ?j < m ?j  _ have "i  m" "m  j1" by auto
      with ?P m finite _ have "?j  m" by - (rule Max_ge; auto)
      with ?j < m show False by simp
    qed
    with ?P m finite _ have "k ?P  m" unfolding k_def by (auto intro: Least_le)
    with * m < ?k show False by auto
  qed
  moreover have " m  ?k. ?j < m  Q m" if "Q  M" for Q
  proof -
    from k[OF Q  M] have "k Q > j1  Q (k Q)" .
    moreover with finite _ Q  M have "k Q  ?k" by - (rule Max_ge; auto)
    moreover with ?j  _ k Q > _  _ have "?j < k Q" by auto
    ultimately show ?thesis by auto
  qed
  ultimately show
    "ji.k>j. P  M. P j  P k  ( m < k. j < m  ¬ P m)
        ( Q  M.  m  k. j < m  Q m)"
    using ?j < ?k ?j  _ ?P ?k * by (inst_existentials ?j ?k ?P; blast)
qed

lemma ℛ_divergent_divergent:
  assumes in_S: "pred_stream (λ u. u  V) xs"
    and div: "ℛ_div (smap (λ u. [u]⇩) xs)"
    and trans: "stream_trans xs"
    and trans': "pairwise trans' xs"
    and unbounded_not_const:
    "u. (c𝒳. real (k c) < u c)  ¬ ev (alw (λxs. shd xs = u)) xs"
  shows "divergent xs"
  unfolding divergent_def proof
  fix t
  from pairwise_trans_eq_elapsed[OF trans in_S] have eq_elapsed: "pairwise eq_elapsed xs" .
  define X1 where "X1 = {x. x  𝒳  (i.  j  i. unbounded x ([xs !! j]⇩))}"
  let ?i = "Max {(SOME i.  j  i. unbounded x ([xs !! j]⇩)) | x. x  𝒳}"
  from finite(1) non_empty have
    "?i  {(SOME i.  j  i. unbounded x ([xs !! j]⇩)) | x. x  𝒳}"
    by (intro Max_in) auto
  have "unbounded x ([xs !! j]⇩)" if "x  X1" "j  ?i" for x j
  proof -
    have "X1  𝒳" unfolding X1_def by auto
    with finite(1) non_empty x  X1 have *:
      "?i  (SOME i.  j  i. unbounded x ([xs !! j]⇩))" (is "?i  ?k")
      by (intro Max_ge) auto
    from x  X1 have " k.  j  k. unbounded x ([xs !! j]⇩)" by (auto simp: X1_def)
    then have " j  ?k. unbounded x ([xs !! j]⇩)" by (rule someI_ex)
    moreover from j  ?i ?i  _ have "j  ?k" by auto
    ultimately show ?thesis by blast
  qed
  then obtain i where unbounded: " x  X1.  j  i. unbounded x ([xs !! j]⇩)"
    using finite by auto
  show " n. t < dur xs n"
  proof (cases " x  𝒳. (i.  j  i. unbounded x ([xs !! j]⇩))")
    case True
    then have "X1 = 𝒳" unfolding X1_def by auto
    have "kj. 0.5  dur xs k - dur xs j" for j
    proof -
      let ?u = "xs !! max i j"
      from in_S have "?u  [?u]⇩" "[?u]⇩  "
        by (auto simp: stream.pred_set)
      moreover from unbounded X1 = 𝒳 have
        " x  𝒳. unbounded x ([?u]⇩)"
        by force
      ultimately have " x  𝒳. ?u x > k x"
        by (auto intro: unbounded_all)
      with unbounded_not_const have "¬ ev (alw (HLD {?u})) xs"
        unfolding HLD_iff by simp
      then obtain r where
        "r  max i j" "xs !! r  xs !! Suc r"
        apply atomize_elim
        apply (simp add: not_ev_iff not_alw_iff)
        apply (drule alw_sdrop[where n = "max i j"])
        apply (drule alwD)
        apply (subst (asm) (3) stream.collapse[symmetric])
        apply simp
        apply (drule ev_neq_start_implies_ev_neq[simplified comp_def])
        using stream.collapse[of "sdrop (max i j) xs"] by (auto 4 3 elim: ev_sdropD)
      let ?k = "Suc r"
      from in_S have "xs !! ?k  V" using snth_sset unfolding stream.pred_set by blast
      with in_S have *:
        "xs !! r  [xs !! r]⇩" "[xs !! r]⇩  "
        "xs !! ?k  [xs !! ?k]⇩" "[xs !! ?k]⇩  "
        by (auto simp: stream.pred_set)
      from r  _ have "r  i" "?k  i" by auto
      with unbounded X1 = 𝒳 have
        " x  𝒳. unbounded x ([xs !! r]⇩)" " x  𝒳. unbounded x ([xs !! ?k]⇩)"
        by (auto simp del: snth.simps(2))
      with in_S have " x  𝒳. (xs !! r) x > k x" " x  𝒳. (xs !! ?k) x > k x"
        using * by (auto intro: unbounded_all)
      moreover from trans' have "trans' (xs !! r) (xs !! ?k)"
        using pairwise_Suc by auto
      ultimately have "(xs !! ?k) = (xs !! r)  0.5"
        unfolding trans'_def using xs !! r  _ by auto
      moreover from pairwise_Suc[OF eq_elapsed] have "eq_elapsed (xs !! r) (xs !! ?k)"
        by auto
      ultimately have 
        "dur xs ?k - dur xs r = 0.5"
        using non_empty by (auto simp: cval_add_def dur_Suc elapsed_eq)
      with dur_mono[of j r xs] r  max i j have "dur xs ?k - dur xs j  0.5"
        by auto
      with r  max i j show ?thesis by - (rule exI[where x = ?k]; auto)
    qed
    then show ?thesis by - (rule dur_ev_exceedsI[where d = "0.5"]; auto)
  next
    case False
    define X2 where "X2 = 𝒳 - X1"
    from False have "X2  {}" unfolding X1_def X2_def by fastforce
    have inf_resets:
      "i. (ji. zero x ([xs !! j]⇩))  (ji. ¬ zero x ([xs !! j]⇩))" if "x  X2" for x
      using that div unfolding X1_def X2_def ℛ_div_def by fastforce
    have " j  i.  k > j.  x  X2. zero x ([xs !! j]⇩)  zero x ([xs !! k]⇩)
           ( m. j < m  m < k  ¬ zero x ([xs !! m]⇩))
           ( x  X2.  m. j < m  m  k  zero x ([xs !! m]⇩))
           ( x  X1.  m  j. unbounded x ([xs !! m]⇩))" for i
    proof -
      from unbounded obtain i' where i': " x  X1.  m  i'. unbounded x ([xs !! m]⇩)" by auto
      then obtain i' where i':
        "i'  i" " x  X1.  m  i'. unbounded x ([xs !! m]⇩)"
        by (cases "i'  i"; auto)
      from finite(1) have "finite X2" unfolding X2_def by auto
      with X2  {} ℛ_divergent_divergent_aux2[where M = "{λ i. zero x ([xs !! i]⇩) | x. x  X2}"]
        inf_resets
      have "ji'. k>j. P{λi. zero x ([xs !! i]⇩) |x. x  X2}. P j  P k
         (m<k. j < m  ¬ P m)  (Q{λi. zero x ([xs !! i]⇩) |x. x  X2}. mk. j < m  Q m)"
        by force
      then obtain j k x where
        "j  i'" "k > j" "x  X2" "zero x ([xs !! j]⇩)" "zero x ([xs !! k]⇩)"
        "m. j < m  m < k  ¬ zero x ([xs !! m]⇩)"
        "Q{λi. zero x ([xs !! i]⇩) |x. x  X2}. mk. j < m  Q m"
        by auto
      moreover from this(7) have "xX2. m  k. j < m  zero x ([xs !! m]⇩)" by auto
      ultimately show ?thesis using i'
        by (inst_existentials j k x) auto
    qed
    moreover have " j'  j. dur xs j' - dur xs i  0.5"
      if  x: "x  X2" "i < j" "zero x ([xs !! i]⇩)" "zero x ([xs !! j]⇩)"
        and not_reset: " m. i < m  m < j  ¬ zero x ([xs !! m]⇩)"
        and X2: " x  X2.  m. i < m  m  j  zero x ([xs !! m]⇩)"
        and X1: " x  X1.  m  i. unbounded x ([xs !! m]⇩)"
      for x i j
    proof -
      have "j'>j. ¬ zero x ([xs !! j']⇩)"
      proof -
        from inf_resets[OF x(1)] obtain j' where "j'  Suc j" "¬ zero x ([xs !! j']⇩)" by auto
        then show ?thesis by - (rule exI[where x = j']; auto)
      qed
      from inf_resets[OF x(1)] obtain j' where "j'  Suc j" "¬ zero x ([xs !! j']⇩)" by auto
      with nat_eventually_critical_path[OF x(4) this(2)]
      obtain j' where j':
        "j' > j" "¬ zero x ([xs !! j']⇩)" " m  j. m < j'  zero x ([xs !! m]⇩)"
        by auto
      from x  X2 have "x  𝒳" unfolding X2_def by simp
      with i < j not_reset not_reset_dur stream_trans _ in_S pairwise_Suc[OF eq_elapsed] have
        "dur xs (j - 1) - dur xs i = (xs !! (j - 1)) x - (xs !! i) x" (is "?d1 = ?d2")
        by (auto simp: stream.pred_set)
      moreover from zero x ([xs !! i]⇩) in_S have "(xs !! i) x = 0"
        by (auto intro: zeroD simp: stream.pred_set)
      ultimately have
        "dur xs (j - 1) - dur xs i = (xs !! (j - 1)) x" (is "?d1 = ?d2")
        by simp
      show ?thesis
      proof (cases "?d1  0.5")
        case True
          (* XXX Fix SMT *)
        with dur_mono[of "j - 1" j xs] have
          "5 / 10  dur xs j - dur xs i"
          by simp
        then show ?thesis by blast
      next
        case False
        have j_c_bound: "(xs !! j) c  ?d2" if "c  X2" for c
        proof (cases "(xs !! j) c = 0")
          case True
          from in_S j > _ True x  𝒳 show ?thesis by (auto simp: V_def stream.pred_set)
        next
          case False
          from X2 c  X2 in_S have "k>i. k  j  (xs !! k) c = 0"
            by (force simp: zeroD stream.pred_set)
          with False have
            "k>i. k  j - Suc 0  (xs !! k) c = 0"
            by (metis Suc_le_eq Suc_pred linorder_neqE_nat not_less not_less_zero)
          moreover from that have "c  𝒳" by (auto simp: X2_def)
          moreover from not_reset in_S x  𝒳 have
            "k>i. k  j - 1  (xs !! k) x  0"
            by (auto simp: zeroI stream.pred_set)
          ultimately have
            "(xs !! (j - 1)) c  ?d2"
            using trans in_S _ x = 0 x  𝒳
            by (auto intro: ℛ_divergent_divergent_aux that simp: stream.pred_set)
          moreover from
            trans_not_delay_mono[OF pairwise_Suc[OF trans], of "j - 1"]
            x  𝒳 c  𝒳 j > _ in_S x(4)
          have "(xs !! j) c  (xs !! (j - 1)) c" by (auto simp: zeroD stream.pred_set)
          ultimately show ?thesis by auto
        qed
        moreover from False ?d1 = ?d2 have "?d2 < 1" by auto
        moreover from in_S have "(xs !! j) c  0" if "c  𝒳" for c
          using that by (auto simp: V_def stream.pred_set)
        ultimately have frac_bound: "frac ((xs !! j) c)  ?d2" if "c  X2" for c
          using that frac_le_1I by (force simp: X2_def)

        let ?u = "(xs !! j)"
        from in_S have "[xs !! j]⇩  " by (auto simp: stream.pred_set)
        then obtain I r where region:
          "[xs !! j]⇩ = region 𝒳 I r" "valid_region 𝒳 k I r"
          unfolding ℛ_def by auto
        let ?S = "{frac (?u c) | c. c  𝒳  isIntv (I c)}"
        have 𝒳_X2: "c  X2" if "c  𝒳" "isIntv (I c)" for c
        proof -
          from X1 j > i have "xX1. unbounded x ([xs !! j]⇩)" by auto
          with unbounded_Greater[OF region(2) c  𝒳] region(1) that(2) have "c  X1" by auto
          with c  𝒳 show "c  X2" unfolding X2_def by auto
        qed
        have frac_bound: "frac ((xs !! j) c)  ?d2" if "c  𝒳" "isIntv (I c)" for c
          using frac_bound[OF 𝒳_X2] that .
        have "dur xs (j' - 1) = dur xs j" using j' x  𝒳 in_S eq_elapsed
          by (subst dur_zero_tail[where ω = "smap (λ u. [u]⇩) xs"])
            (auto dest: pairwise_Suc simp: stream.pred_set)
        moreover from dur_reset[OF eq_elapsed in_S, of x "j - 1"] x  𝒳 x(4) j > _ have
          "dur xs j = dur xs (j - 1)"
          by (auto simp: stream.pred_set)
        ultimately have "dur xs (j' - 1) = dur xs (j - 1)" by auto
        moreover have "dur xs j' - dur xs (j' - 1)  (1 - ?d2) / 2"
        proof -
          from j' > _ have "j' > 0" by auto
          with pairwise_Suc[OF trans', of "j' - 1"] have
            "trans' (xs !! (j' - 1)) (xs !! j')"
            by auto
          moreover from j' have
            "(xs !! (j' - 1)) x = 0" "(xs !! j') x > 0"
            using in_S x  𝒳 by (force intro: zeroD dest: not_zeroD simp: stream.pred_set)+
          moreover note delayedR_aux = calculation
          obtain t where
            "(xs !! j') = (xs !! (j' - 1))  t" "t  (1 - ?d2) / 2" "t  0"
          proof -
            from in_S have "[xs !! j']⇩  " by (auto simp: stream.pred_set)
            then obtain I' r' where region':
              "[xs !! j']⇩ = region 𝒳 I' r'" "valid_region 𝒳 k I' r'"
              unfolding ℛ_def by auto            
            let ?S' = "{frac ((xs !! (j' - 1)) c) |c. c  𝒳  Regions.isIntv (I' c)}"

            from finite(1) have "?d2  Max (?S'  {0})"
              apply -
              apply (rule Max.boundedI)
                apply fastforce
               apply fastforce
              apply safe
              subgoal premises prems for _ c d
              proof -
                from j' have "(xs !! (j' - 1)) c = ?u c  (xs !! (j' - 1)) c = 0"
                  by (intro resets_mono'[OF eq_elapsed in_S trans _ x  𝒳 c  𝒳]; auto)
                then show ?thesis
                proof (standard, goal_cases)
                  case A: 1
                  show ?thesis
                  proof (cases "c  X1")
                    case True
                    with X1 j' > j j > i have "unbounded c ([xs !! j']⇩)" by auto
                    with region' c  𝒳 have "I' c = Greater (k c)"
                      by (auto intro: unbounded_Greater)
                    with prems show ?thesis by auto
                  next
                    case False
                    with c  𝒳 have "c  X2" unfolding X2_def by auto
                    with j_c_bound have mono: "(xs !! j) c  (xs !! (j - 1)) x" .
                    from in_S c  𝒳 have "(xs !! (j' - 1)) c  0"
                      unfolding V_def stream.pred_set by auto
                    then have
                      "frac ((xs !! (j' - 1)) c)  (xs !! (j' - 1)) c"
                      using frac_le_self by auto
                    with A mono show ?thesis by auto
                  qed
                next
                  case prems: 2
                    (* XXX *)
                  have "frac (0 :: real) = (0 :: real)" by auto
                  then have "frac (0 :: real)  (0 :: real)" by linarith
                  moreover from in_S x  𝒳 have "(xs !! (j - 1)) x  0"
                    unfolding V_def stream.pred_set by auto
                  ultimately show ?thesis using prems by auto
                qed
              qed
              using in_S x  𝒳 by (auto simp: V_def stream.pred_set)
            then have le: "(1 - ?d2) / 2  (1 - Max (?S'  {0})) / 2" by simp

            let ?u = "xs !! j'"
            let ?u' = "xs !! (j' - 1)"
            from in_S have *: "?u'  V" "[?u']⇩  " "?u  V" "[?u]⇩  "
              by (auto simp: stream.pred_set)
            from pairwise_Suc[OF trans, of "j' - 1"] j' > j have
              "trans (xs !! (j' - 1)) (xs !! j')"
              by auto
            then have Succ:
              "[xs !! j']⇩  Succ  ([xs !! (j' - 1)]⇩)  ( t 0. ?u = ?u'  t)"
            proof cases
              case prems: (succ t)
              from * have "?u'  [?u']⇩" by auto
              with prems * show ?thesis by auto
            next
              case (reset l)
              with ?u'  V have "?u x  ?u' x" by (cases "x  set l") (auto simp: V_def)
              from j' have "zero x ([?u']⇩)" by auto
              with ?u'  V have "?u' x = 0" unfolding zero_def by auto
              with ?u x  _ ?u x > 0 show ?thesis by auto
            next
              case id
              with * Succ_refl[of  𝒳 k, folded ℛ_def, OF _ finite(1)] show ?thesis
                unfolding cval_add_def by auto
            qed
            then obtain t where t: "?u = xs !! (j' - 1)  t" "t  0" by auto
            note Succ = Succ[THEN conjunct1]

            show ?thesis
            proof (cases " c  X2.  d :: nat. ?u c = d")
              case True
              from True obtain c and d :: nat where c:
                "c  𝒳" "c  X2" "?u c = d"
                by (auto simp: X2_def)
              have "?u x > 0" by fact
              from pairwise_Suc[OF eq_elapsed, of "j' - 1"] j' > j have
                "eq_elapsed (xs !! (j' - 1)) ?u"
                by auto
              moreover from
                elapsed_eq[OF this x  𝒳] (xs !! (j' - 1)) x = 0 (xs !! j') x > 0
              have "elapsed (xs !! (j' - 1)) (xs !! j') > 0"
                by auto
              ultimately have
                "?u c - (xs !! (j' - 1)) c > 0"
                using c  𝒳 unfolding eq_elapsed_def by auto
              moreover from in_S have "xs !! (j' - 1)  V" by (auto simp: stream.pred_set)
              ultimately have "?u c > 0" using c  𝒳 unfolding V_def by auto
              from region' in_S c  𝒳 have "intv_elem c ?u (I' c)"
                by (force simp: stream.pred_set)
              with ?u c = d ?u c > 0 have "?u c  1" by auto
              moreover have "(xs !! (j' - 1)) c  0.5"
              proof -
                have "(xs !! (j' - 1)) c  (xs !! j) c"
                  (* XXX This proof is duplicated at least once above *)
                  using j'(1,3)
                  by (auto intro: resets_mono[OF eq_elapsed in_S trans _ x  𝒳 c  𝒳])
                also have "  ?d2" using j_c_bound[OF c  X2] .
                also from ?d1 = ?d2 ¬ 5 / 10  _ have "  0.5" by simp
                finally show ?thesis .
              qed
              moreover have "?d2  0" using in_S x  𝒳 by (auto simp: V_def stream.pred_set)
              ultimately have "?u c - (xs !! (j' - 1)) c  (1 - ?d2) / 2" by auto
              with t have "t  (1 - ?d2) / 2" unfolding cval_add_def by auto
              with t show ?thesis by (auto intro: that)
            next
              case F: False
              have not_const: "¬ isConst (I' c)" if "c  𝒳" for c
              proof (rule ccontr, simp)
                assume A: "isConst (I' c)"
                show False
                proof (cases "c  X1")
                  case True
                  with X1 j' > j j > _ have "unbounded c ([xs !! j']⇩)" by auto
                  with unbounded_Greater c  𝒳 region' have "isGreater (I' c)" by force
                  with A show False by auto
                next
                  case False
                  with c  𝒳 have "c  X2" unfolding X2_def by auto
                  from region' in_S c  𝒳 have "intv_elem c ?u (I' c)"
                    unfolding stream.pred_set  by force
                  with c  X2 A False F show False by auto
                qed
              qed
              have "x. x  k c  (xs !! j') c = real x" if "c  𝒳" for c
              proof (cases "c  X2"; safe)
                fix d
                assume "c  X2" "(xs !! j') c = real d"
                with F show False by auto
              next
                fix d
                assume "c  X2" 
                with that have "c  X1" unfolding X2_def by auto
                with X1 j' > j j > i have "unbounded c ([?u]⇩)" by auto
                from unbounded_all[OF _ _ this] c  𝒳 in_S have "?u c > k c"
                  by (force simp: stream.pred_set)
                moreover assume "?u c = real d" "d  k c"
                ultimately show False by auto
              qed
              with delayedR_aux have
                "(xs !! j') = delayedR ([xs !! j']⇩) (xs !! (j' - 1))"
                using x  𝒳 unfolding trans'_def by auto
              from not_const region'(1)  in_S Succ(1) have
                "t0. delayedR ([xs !! j']⇩) (xs !! (j' - 1)) = xs !! (j' - 1)  t 
                      (1 - Max (?S'  {0})) / 2  t"
                apply simp
                apply (rule delayedR_correct(2)[OF _ _ region'(2), simplified])
                by (auto simp: stream.pred_set)
              with le _ = delayedR _ _ show ?thesis by (auto intro: that)
            qed
          qed
          moreover from pairwise_Suc[OF eq_elapsed, of "j' - 1"] j' > 0 have
            "eq_elapsed (xs !! (j' - 1)) (xs !! j')"
            by auto
          ultimately show "dur xs j' - dur xs (j' - 1)  (1 - ?d2) / 2" 
            using j' > 0 dur_Suc[of _ "j' - 1"] x  𝒳 by (auto simp: cval_add_def elapsed_eq)
        qed
        moreover from dur_mono[of i "j - 1" xs] i < j have "dur xs i  dur xs (j - 1)" by simp
        ultimately have "dur xs j' - dur xs i  0.5" unfolding ?d1 = ?d2[symmetric] by auto
        then show ?thesis using j < j' by - (rule exI[where x = j']; auto)
      qed
    qed
    moreover
    have " j'  i. dur xs j' - dur xs i  0.5" for i
    proof -
      from calculation(1)[of i] obtain j k x where
        "ji" "k>j" "xX2" "zero x ([xs !! j]⇩)"
        "zero x ([xs !! k]⇩)"
        "m. j < m  m < k  ¬ zero x ([xs !! m]⇩)"
        "xX2. m>j. m  k  zero x ([xs !! m]⇩)"
        "xX1. mj. unbounded x ([xs !! m]⇩)"
        by auto
      from calculation(2)[OF this(3,2,4-8)] obtain j' where
        "j'k" "5 / 10  dur xs j' - dur xs j"
        by auto
      with dur_mono[of i j xs] j  i k > j show ?thesis by (intro exI[where x = j']; auto)
    qed
    then show ?thesis by - (rule dur_ev_exceedsI[where d = "0.5"]; auto)
  qed
qed

lemma cfg_on_div_absc:
  notes in_space_UNIV[measurable]
  assumes "cfg  cfg_on_div st" "st  S"
  shows "absc cfg  R_G_cfg_on_div (abss st)"
proof -
  from assms have *: "cfg  MDP.cfg_on st" "state cfg = st" "div_cfg cfg"
    unfolding cfg_on_div_def by auto
  with assms have "cfg  valid_cfg" by (auto intro: MDP.valid_cfgI)
  have "almost_everywhere (MDP.MC.T cfg) (MDP.MC.enabled cfg)"
    by (rule MDP.MC.AE_T_enabled)
  moreover from * have "AE x in MDP.MC.T cfg. divergent (smap (snd  state) x)"
    by (simp add: div_cfg_def)
  ultimately have "AE x in MDP.MC.T cfg. ℛ_div (smap (snd  state) (smap absc x))"
  proof eventually_elim
    case (elim ω)
    let ?xs = "smap (snd o state) ω"
    from MDP.pred_stream_cfg_on[OF _  valid_cfg MDP.MC.enabled _ _] have *:
      "pred_stream (λ x. x  S) (smap state ω)"
      by (auto simp: stream.pred_set)
    have "[snd (state x)]⇩ = snd (abss (state x))" if "x  sset ω" for x
    proof -
      from * that have "state x  S" by (auto simp: stream.pred_set)
      then have "snd (abss (state x)) = [snd (state x)]⇩" by (metis abss_S snd_conv surj_pair)
      then show ?thesis ..
    qed
    then have "smap (λz. [snd (state z)]⇩) ω = (smap (λz. snd (abss (state z))) ω)" by auto
    from * have  "pred_stream (λ u. u  V) ?xs"
      apply (simp add: map_def stream.pred_set)
      apply (subst (asm) surjective_pairing)
      using S_V by blast
    moreover have "stream_trans ?xs"
      by (rule enabled_stream_trans _  valid_cfg MDP.MC.enabled _ _)+
    ultimately show ?case using divergent _ smap _ ω = _
      by - (drule divergent_ℛ_divergent, auto simp add: stream.map_comp state_absc)
  qed
  with cfg  valid_cfg have "R_G_div_cfg (absc cfg)" unfolding R_G_div_cfg_def
    by (subst absc_distr_self) (auto intro: MDP.valid_cfgI simp: AE_distr_iff)
  with R_G.valid_cfgD cfg  valid_cfg * show ?thesis unfolding R_G_cfg_on_div_def by auto force
qed

definition
  "alternating cfg = (AE ω in MDP.MC.T cfg.
      alw (ev (HLD {cfg. cfg'  K_cfg cfg. fst (state cfg') = fst (state cfg)})) ω)"

lemma K_cfg_same_loc_iff:
  "(cfg' K_cfg cfg. fst (state cfg') = fst (state cfg))
   (cfg' K_cfg (absc cfg). fst (state cfg') = fst (state (absc cfg)))"
  if "cfg  valid_cfg"
  using that by (auto simp: state_absc fst_abss K_cfg_map_absc)

lemma (in -) stream_all2_flip:
  "stream_all2 (λa b. R b a) xs ys = stream_all2 R ys xs"
  by (standard; coinduction arbitrary: xs ys; auto dest: sym)

(* TODO: Lots of duplication here, e.g. with path_measure_eq_repcs1_new *)
lemma AE_alw_ev_same_loc_iff:
  assumes "cfg  valid_cfg"
  shows "alternating cfg  alternating (absc cfg)"
  unfolding alternating_def
  apply (simp add: MDP.MC.T.AE_iff_emeasure_eq_1)
  subgoal
  proof -
    show ?thesis (is "(?x = 1) = (?y = 1)")
    proof -
      have *: "stream_all2 (λs t. t = absc s) x y = stream_all2 (=) y (smap absc x)" for x y
        by (subst stream_all2_flip) simp
      have "?x = ?y"
        apply (rule T_eq_rel_half[where f = absc and S = valid_cfg, OF HOL.refl, rotated 2])
        subgoal
          apply (simp add: space_stream_space rel_set_strong_def)
          apply (intro allI impI)
          apply (frule stream.rel_mono_strong[where Ra = "λs t. t = absc s"])
          by (auto simp: * stream.rel_eq stream_all2_refl alw_holds_pred_stream_iff[symmetric]
              K_cfg_same_loc_iff HLD_def comp_def elim!: alw_ev_cong)
        subgoal
          by (rule rel_funI) (auto intro!: rel_pmf_reflI simp: pmf.rel_map(2) K_cfg_map_absc)
        using cfg  valid_cfg by simp+
      then show ?thesis
        by simp
    qed
  qed
  done

lemma AE_alw_ev_same_loc_iff':
  assumes "cfg  R_G.cfg_on (abss st)" "st  S"
  shows "alternating cfg  alternating (repcs st cfg)"
proof -
  from assms have "cfg  R_G.valid_cfg"
    by (auto intro: R_G.valid_cfgI)
  with assms show ?thesis
    by (subst AE_alw_ev_same_loc_iff) (auto simp: absc_repcs_id)
qed

lemma (in -) cval_add_non_id:
  False if "b  d = b" "d > 0" for d :: real
proof -
  from that(1) have "(b  d) x = b x"
    by (rule fun_cong)
  with d > 0 show False
    unfolding cval_add_def by simp
qed

lemma repcs_unbounded_AE_non_loop_end_strong:
  assumes "cfg  R_G.cfg_on (abss st)" "st  S"
    and "alternating cfg"
  shows "AE ω in MDP.MC.T (repcs st cfg).
      ( u :: ('c  real). ( c  𝒳. u c > real (k c)) 
      ¬ (ev (alw (λ xs. shd xs = u))) (smap (snd o state) ω))" (is "AE ω in ?M. ?P ω")
proof -
  from assms have "cfg  R_G.valid_cfg"
    by (auto intro: R_G.valid_cfgI)
  with assms(1) have "repcs st cfg  valid_cfg"
    by auto
  from R_G.valid_cfgD[OF cfg  R_G.valid_cfg] have "cfg  R_G.cfg_on (state cfg)" .
  let ?U = "λ u.  l  L. {μ  K (l, u). μ  return_pmf (l, u)  ( x  μ. fst x = l)}"
  let ?r = "λ u. Sup ({0}  (λ μ. measure_pmf μ {x. snd x = u}) ` ?U u)"
  have lt_1: "?r u < 1" for u
  proof -
    have *: "emeasure (measure_pmf μ) {x. snd x = u} < 1"
      if "μ  return_pmf (l, u)" "xset_pmf μ. fst x = l" for μ and l :: 's
    proof (rule ccontr)
      assume "¬ emeasure (measure_pmf μ) {x. snd x = u} < 1"
      then have "1 = emeasure (measure_pmf μ) {x. snd x = u}"
        using measure_pmf.emeasure_ge_1_iff by force
      also from that(2) have "  emeasure (measure_pmf μ) {(l, u)}"
        by (subst emeasure_Int_set_pmf[symmetric]) (auto intro!: emeasure_mono)
      finally show False
        by (simp add: measure_pmf.emeasure_ge_1_iff measure_pmf_eq_1_iff that(1))
    qed
    let ?S =
      "{map_pmf (λ (X, l). (l, ([X := 0]u))) μ | μ l g. (l, g, μ)  trans_of A}"
    have "(λ μ. measure_pmf μ {x. snd x = u}) ` ?U u
       {0, 1}  (λ μ. measure_pmf μ {x. snd x = u}) ` ?S"
      by (force elim!: K.cases)
    moreover have "finite ?S"
    proof -
      have "?S  (λ (l, g, μ). map_pmf (λ (X, l). (l, ([X := 0]u))) μ) ` trans_of A"
        by force
      also from finite(3) have "finite " ..
      finally show ?thesis .
    qed
    ultimately have "finite ((λ μ. measure_pmf μ {x. snd x = u}) ` ?U u)"
      by (auto intro: finite_subset)
    then show ?thesis
      by (fastforce intro: * finite_imp_Sup_less)
  qed
  { fix l :: 's and u :: "'c  real" and cfg :: "('s × ('c  real) set) cfg"
    assume unbounded: " c  𝒳. u c > k c" and "cfg  R_G.cfg_on (abss (l, u))" "abss (l, u)  𝒮"
      and same_loc: " cfg'  K_cfg cfg. fst (state cfg') = l"
    then have "cfg  R_G.valid_cfg" "repcs (l, u) cfg  valid_cfg"
      by (auto intro: R_G.valid_cfgI)
    then have cfg_on: "repcs (l, u) cfg  MDP.cfg_on (l, u)"
      by (auto dest: MDP.valid_cfgD)
    from cfg  R_G.cfg_on _ have "action cfg  𝒦 (abss (l, u))"
      by (rule R_G.cfg_onD_action)
        (* TODO: Pull out? *)
    have K_cfg_rept: "state ` K_cfg (repcs (l, u) cfg) = rept (l, u) (action cfg)"
      unfolding K_cfg_def by (force simp: action_repcs)
    have "l  L"
      using MDP.valid_cfg_state_in_S repcs (l, u) cfg  MDP.valid_cfg by fastforce
    moreover have "rept (l, u) (action cfg)  return_pmf (l, u)"
    proof (rule ccontr, simp)
      assume "rept (l, u) (action cfg) = return_pmf (l, u)"
      then have "action cfg = return_pmf (abss (l, u))"
        using abst_rept_id[OF action cfg  _]
        by (simp add: abst_def)
      moreover have "(l, u)  S"
        using _  𝒮 by (auto dest: 𝒮_abss_S)
      moreover have "abss (l, u) = (l, [u]⇩)"
        by (metis abss_S calculation(2))
      ultimately show False
        using rept (l, u) _ = _ unbounded unfolding rept_def by (auto dest: cval_add_non_id)
    qed
    moreover have "rept (l, u) (action cfg)  K (l, u)"
    proof -
      have "action (repcs (l, u) cfg)  K (l, u)"
        using cfg_on by blast
      then show ?thesis
        by (simp add: repcs_def)
    qed
    moreover have "xset_pmf (rept (l, u) (action cfg)). fst x = l"
      using same_loc K_cfg_same_loc_iff[of "repcs (l, u) cfg"]
        repcs (l, u) _  valid_cfg cfg  R_G.valid_cfg cfg  R_G.cfg_on _
      by (simp add: absc_repcs_id fst_abss K_cfg_rept[symmetric])
    ultimately have "rept (l, u) (action cfg)  ?U u"
      by blast
    then have "measure_pmf (rept (l, u) (action cfg)) {x. snd x = u}  ?r u"
      by (fastforce intro: Sup_upper)
    moreover have "rept (l, u) (action cfg) = action (repcs (l, u) cfg)"
      by (simp add: repcs_def)
    ultimately have "measure_pmf (action (repcs (l, u) cfg)) {x. snd x = u}  ?r u"
      by auto
  }
  note * = this
  let ?S = "{cfg.  cfg' s. cfg'  R_G.valid_cfg  cfg = repcs s cfg'  abss s = state cfg'}"
  have start: "repcs st cfg  ?S"
    using cfg  R_G.valid_cfg assms unfolding R_G_cfg_on_div_def
    by clarsimp (inst_existentials cfg "fst st" "snd st", auto)
  have step: "y  ?S" if "y  K_cfg x" "x  ?S" for x y
    using that apply safe
    subgoal for cfg' l u
      apply (inst_existentials "absc y" "state y")
      subgoal
        by blast
      subgoal
        by (metis
            K_cfg_valid_cfgD R_G.valid_cfgD R_G.valid_cfg_state_in_S absc_repcs_id cont_absc_1
            cont_repcs1 repcs_valid
            )
      subgoal
        by (simp add: state_absc)
      done
    done
  have **: "x  ?S" if "(repcs st cfg, x)  MDP.MC.acc" for x
  proof -
    from MDP.MC.acc_relfunD[OF that] obtain n where "((λ a b. b  K_cfg a) ^^ n) (repcs st cfg) x" .
    then show ?thesis
    proof (induction n arbitrary: x) (* XXX Extract induction rule *)
      case 0
      with start show ?case
        by simp
    next
      case (Suc n)
      from this(2)[simplified] show ?case
        apply (rule relcomppE)
        apply (erule step)
        apply (erule Suc.IH)
        done
    qed
  qed
  have ***: "almost_everywhere (MDP.MC.T (repcs st cfg)) (alw (HLD ?S))"
    by (rule AE_mp[OF MDP.MC.AE_T_reachable]) (fastforce dest: ** simp: HLD_iff elim: alw_mono)

  from alternating cfg assms have "alternating (repcs st cfg)"
    by (simp add: AE_alw_ev_same_loc_iff'[of _ st])
  then have alw_ev_same2: "almost_everywhere (MDP.MC.T (repcs st cfg))
     (alw (λω. HLD (state -` snd -` {u}) ω 
      ev (HLD {cfg. cfg'set_pmf (K_cfg cfg). fst (state cfg') = fst (state cfg)}) ω))"
    for u unfolding alternating_def by (auto elim: alw_mono)

  let ?X = "{cfg :: ('s × ('c  real)) cfg.  c  𝒳. snd (state cfg) c > k c}"
  let ?Y = "{cfg.  cfg'  K_cfg cfg. fst (state cfg') = fst (state cfg)}"

  have "(AE ω in ?M. ?P ω) 
    (AE ω in ?M.  u :: ('c  real).
      ( c  𝒳. u c > k c)  u  snd ` state ` (MDP.MC.acc `` {repcs st cfg}) 
      ¬ (ev (alw (λ xs. shd xs = u))) (smap (snd o state) ω))" (is "?L  ?R")
  proof
    assume ?L
    then show ?R
      by eventually_elim auto
  next
    assume ?R
    with MDP.MC.AE_T_reachable[of "repcs st cfg"] show ?L
    proof (eventually_elim, intro allI impI notI, goal_cases)
      case (1 ω u)
      then show ?case
        by - (intro alw_HLD_smap alw_disjoint_ccontr[where
              S = "(snd o state) ` MDP.MC.acc `` {repcs st cfg}"
              and R = "{u}" and ω = "smap (snd o state) ω"
              ]; auto simp: HLD_iff comp_def)
    qed
  qed

  also have " 
      ( u :: ('c  real).
        ( c  𝒳. u c > k c)  u  snd ` state ` (MDP.MC.acc `` {repcs st cfg}) 
        (AE ω in ?M. ¬ (ev (alw (λ xs. shd xs = u))) (smap (snd o state) ω)))"
    using MDP.MC.countable_reachable[of "repcs st cfg"]
    by - (rule AE_all_imp_countable,
        auto intro: countable_subset[where B = "snd ` state ` MDP.MC.acc `` {repcs st cfg}"])
  also show ?thesis
    unfolding calculation
    apply clarsimp
    subgoal for l u x
      apply (rule
          MDP.non_loop_tail_strong[simplified, of snd "snd (state x)" ?Y ?S "?r (snd (state x))"]
          )
      subgoal
        apply safe
        subgoal premises prems for cfg l1 u1 _ cfg' l2 u2
        proof -
          have [simp]: "l2 = l1" "u2 = u1"
            subgoal
              by (metis MDP.cfg_onD_state Pair_inject prems(4) state_repcs)
            subgoal
              by (metis MDP.cfg_onD_state prems(4) snd_conv state_repcs)
            done
          with prems have [simp]: "u2 = u"
            by (metis (l, u) = state x snd (l1, u1) = snd (state x) u2 = u1 snd_conv)
          have [simp]: "snd -` {snd (state x)} = {y. snd y = snd (state x)}"
            by (simp add: vimage_def)
          from prems show ?thesis
            apply simp
            apply (erule *[simplified])
            subgoal
              using prems(1) prems(2)[symmetric] prems(3-) by (auto simp: R_G.valid_cfg_def)
            subgoal
              using prems(1) prems(2)[symmetric] prems(3-) by (auto simp: R_G.valid_cfg_def)
            subgoal
              using K_cfg_same_loc_iff[of "repcs (l1, snd (state x)) cfg'"]
              by (simp add: absc_repcs_id) (metis fst_abss fst_conv repcs_valid)
            done
        qed
        done
      subgoal
        by (auto intro: lt_1[simplified])
        apply (rule MDP.valid_cfgD[OF repcs st cfg  valid_cfg]; fail)
      subgoal
        using *** unfolding alw_holds_pred_stream_iff[symmetric] HLD_def .
      subgoal
        by (rule alw_ev_same2)
      done
    done
qed

lemma cfg_on_div_repcs_strong:
  notes in_space_UNIV[measurable]
  assumes "cfg  R_G_cfg_on_div (abss st)" "st  S" and "alternating cfg"
  shows "repcs st cfg  cfg_on_div st"
proof -
  let ?st = "abss st"
  let ?cfg = "repcs st cfg"
  from assms have *:
    "cfg  R_G.cfg_on ?st" "state cfg = ?st" "R_G_div_cfg cfg"
    unfolding R_G_cfg_on_div_def by auto
  with assms have "cfg  R_G.valid_cfg" by (auto intro: R_G.valid_cfgI)
  with st  S _ = ?st have "?cfg  valid_cfg" by auto
  from *(1) st  S alternating cfg have
    "AE ω in MDP.MC.T ?cfg. u. (c𝒳. real (k c) < u c) 
                          ¬ ev (alw (λxs. shd xs = u)) (smap (snd  state) ω)"
    by (rule repcs_unbounded_AE_non_loop_end_strong)
  ― ‹Move to lower level›
  moreover from *(2,3) have "AE ω in MDP.MC.T ?cfg. ℛ_div (smap (snd  state) (smap absc ω))"
    unfolding R_G_div_cfg_def
    by (subst (asm) R_G_trace_space_distr_eq[OF cfg  R_G.valid_cfg]; simp add: AE_distr_iff)
  ultimately have "div_cfg ?cfg"
    unfolding div_cfg_def using MDP.MC.AE_T_enabled[of ?cfg]
  proof eventually_elim
    case prems: (elim ω)
      let ?xs = "smap (snd o state) ω"
      from MDP.pred_stream_cfg_on[OF _  valid_cfg MDP.MC.enabled _ _] have *:
        "pred_stream (λ x. x  S) (smap state ω)"
        by (auto simp: stream.pred_set)
      have "[snd (state x)]⇩ = snd (abss (state x))" if "x  sset ω" for x
      proof -
        from * that have "state x  S" by (auto simp: stream.pred_set)
        then have "snd (abss (state x)) = [snd (state x)]⇩" by (metis abss_S snd_conv surj_pair)
        then show ?thesis ..
      qed
      then have "smap (λz. [snd (state z)]⇩) ω = (smap (λz. snd (abss (state z))) ω)" by auto
      from * have  "pred_stream (λ u. u  V) ?xs"
        by (simp add: map_def stream.pred_set, subst (asm) surjective_pairing, blast)
      moreover have "stream_trans ?xs"
        by (rule enabled_stream_trans _  valid_cfg MDP.MC.enabled _ _)+
      moreover have "pairwise trans' ?xs"
        using _  R_G.valid_cfg state cfg = _[symmetric] MDP.MC.enabled _ _
        by (rule enabled_stream_trans')
      moreover from prems(1) have
        "u. (c𝒳. real (k c) < u c)  ¬ ev (alw (λxs. snd (shd xs) = u)) (smap state ω)"
        by (simp add: comp_def)
      ultimately show ?case using ℛ_div _
        by (simp add: stream.map_comp state_absc smap _ ω = _ ℛ_divergent_divergent comp_def)
    qed
  with MDP.valid_cfgD cfg  R_G.valid_cfg * show ?thesis unfolding cfg_on_div_def by auto force
qed

lemma repcs_unbounded_AE_non_loop_end:
  assumes "cfg  R_G.cfg_on (abss st)" "st  S"
  shows "AE ω in MDP.MC.T (repcs st cfg).
      ( s :: ('s × ('c  real)). ( c  𝒳. snd s c > k c) 
      ¬ (ev (alw (λ xs. shd xs = s))) (smap state ω))" (is "AE ω in ?M. ?P ω")
proof -
  from assms have "cfg  R_G.valid_cfg"
    by (auto intro: R_G.valid_cfgI)
  with assms(1) have "repcs st cfg  valid_cfg"
    by auto
  from R_G.valid_cfgD[OF cfg  R_G.valid_cfg] have "cfg  R_G.cfg_on (state cfg)" .
  let ?K = "λ x. {μ  K x. μ  return_pmf x}"
  let ?r = "λ x. Sup ((λ μ. measure_pmf μ {x}) ` ?K x)"
  have lt_1: "?r x < 1" if "μ  ?K x" for μ x
  proof -
    have *: "emeasure (measure_pmf μ) {x} < 1" if "μ  return_pmf x" for μ
    proof (rule ccontr)
      assume "¬ emeasure (measure_pmf μ) {x} < 1"
      then have "emeasure (measure_pmf μ) {x} = 1"
        using measure_pmf.emeasure_ge_1_iff by force
      with that show False
        by (simp add: measure_pmf_eq_1_iff)
    qed
    let ?S =
      "{map_pmf (λ (X, l). (l, ([X := 0]u))) μ | μ l u g.
          x = (l, u)  (l, g, μ)  trans_of A}"
    have "(λ μ. measure_pmf μ {x}) ` ?K x
       {0, 1}  (λ μ. measure_pmf μ {x}) ` ?S"
      by (force elim!: K.cases)
    moreover have "finite ?S"
    proof -
      have "?S  (λ (l, g, μ). map_pmf (λ (X, l). (l, (clock_set_set X 0(snd x)))) μ) ` trans_of A"
        by force
      also from finite(3) have "finite " ..
      finally show ?thesis .
    qed
    ultimately have "finite ((λ μ. measure_pmf μ {x}) ` ?K x)"
      by (auto intro: finite_subset)
    then show ?thesis
      using that by (auto intro: * finite_imp_Sup_less)
  qed
  { fix s :: "'s × ('c  real)" and cfg :: "('s × ('c  real) set) cfg"
    assume unbounded: " c  𝒳. snd s c > k c" and "cfg  R_G.cfg_on (abss s)" "abss s  𝒮"
    then have "repcs s cfg  valid_cfg"
      by (auto intro: R_G.valid_cfgI)
    then have cfg_on: "repcs s cfg  MDP.cfg_on s"
      by (auto dest: MDP.valid_cfgD)
    from cfg  _ have "action cfg  𝒦 (abss s)"
      by (rule R_G.cfg_onD_action)
    have "rept s (action cfg)  return_pmf s"
    proof (rule ccontr, simp)
      assume "rept s (action cfg) = return_pmf s"
      then have "action cfg = return_pmf (abss s)"
        using abst_rept_id[OF action cfg  _]
        by (simp add: abst_def)
      moreover have "(fst s, snd s)  S"
        using _  𝒮 by (auto dest: 𝒮_abss_S)
      moreover have "abss s = (fst s, [snd s]⇩)"
        by (metis abss_S calculation(2) prod.collapse)
      ultimately show False
        using rept s _ = _ unbounded unfolding rept_def by (cases s) (auto dest: cval_add_non_id)
    qed
    moreover have "rept s (action cfg)  K s"
    proof -
      have "action (repcs s cfg)  K s"
        using cfg_on by blast
      then show ?thesis
        by (simp add: repcs_def)
    qed
    ultimately have "rept s (action cfg)  ?K s"
      by blast
    then have "measure_pmf (rept s (action cfg)) {s}  ?r s"
      by (auto intro: Sup_upper)
    moreover have "rept s (action cfg) = action (repcs s cfg)"
      by (simp add: repcs_def)
    ultimately have "measure_pmf (action (repcs s cfg)) {s}  ?r s"
      by auto
    note this rept s (action cfg)  ?K s
  }
  note * = this
  let ?S = "{cfg.  cfg' s. cfg'  R_G.valid_cfg  cfg = repcs s cfg'  abss s = state cfg'}"
  have start: "repcs st cfg  ?S"
    using cfg  R_G.valid_cfg assms unfolding R_G_cfg_on_div_def
    by clarsimp (inst_existentials cfg "fst st" "snd st", auto)
  have step: "y  ?S" if "y  K_cfg x" "x  ?S" for x y
    using that apply safe
    subgoal for cfg' l u
      apply (inst_existentials "absc y" "state y")
      subgoal
        by blast
      subgoal
        by (metis
            K_cfg_valid_cfgD R_G.valid_cfgD R_G.valid_cfg_state_in_S absc_repcs_id cont_absc_1
            cont_repcs1 repcs_valid
            )
      subgoal
        by (simp add: state_absc)
      done
    done
  have **: "x  ?S" if "(repcs st cfg, x)  MDP.MC.acc" for x
  proof -
    from MDP.MC.acc_relfunD[OF that] obtain n where "((λ a b. b  K_cfg a) ^^ n) (repcs st cfg) x" .
    then show ?thesis
    proof (induction n arbitrary: x) (* XXX Extract induction rule *)
      case 0
      with start show ?case
        by simp
    next
      case (Suc n)
      from this(2)[simplified] show ?case
        by (elim relcomppE step Suc.IH)
    qed
  qed
  have ***: "almost_everywhere (MDP.MC.T (repcs st cfg)) (alw (HLD ?S))"
    by (rule AE_mp[OF MDP.MC.AE_T_reachable]) (fastforce dest: ** simp: HLD_iff elim: alw_mono)

  have "(AE ω in ?M. ?P ω) 
    (AE ω in ?M.  s :: ('s × ('c  real)).
      ( c  𝒳. snd s c > k c)  s  state ` (MDP.MC.acc `` {repcs st cfg}) 
      ¬ (ev (alw (λ xs. shd xs = s))) (smap state ω))" (is "?L  ?R")
  proof
    assume ?L
    then show ?R
      by eventually_elim auto
  next
    assume ?R
    with MDP.MC.AE_T_reachable[of "repcs st cfg"] show ?L
    proof (eventually_elim, intro allI impI notI, goal_cases)
      case (1 ω s)
      from this(1,2,5,6) show ?case
        by (intro alw_HLD_smap alw_disjoint_ccontr[where
              S = "state ` MDP.MC.acc `` {repcs st cfg}" and R = "{s}" and ω = "smap state ω"
              ]; simp add: HLD_iff comp_def; blast)
    qed
  qed

  also have " 
      ( s :: ('s × ('c  real)).
        ( c  𝒳. snd s c > k c)  s  state ` (MDP.MC.acc `` {repcs st cfg}) 
        (AE ω in ?M. ¬ (ev (alw (λ xs. shd xs = s))) (smap state ω)))"
    using MDP.MC.countable_reachable[of "repcs st cfg"]
    by - (rule AE_all_imp_countable,
        auto intro: countable_subset[where B = "state ` MDP.MC.acc `` {repcs st cfg}"])
  also show ?thesis
    unfolding calculation
    apply clarsimp
    subgoal for l u x
      apply (rule MDP.non_loop_tail'[simplified, of "state x" ?S "?r (state x)"])
      subgoal
        apply safe
        subgoal premises prems for cfg cfg' l' u'
        proof -
          from prems have "state x = (l', u')"
            by (metis MDP.cfg_onD_state state_repcs)
          with _ = state x have [simp]: "l = l'" "u = u'"
            by auto
          show ?thesis
            unfolding state x = _ using prems(1,3-) by (auto simp: R_G.valid_cfg_def intro: *)
        qed
        done
      subgoal
        apply (drule **)
        apply clarsimp
        apply (rule lt_1)
        apply (rule *)
        apply (auto dest: R_G.valid_cfg_state_in_S R_G.valid_cfgD)
        done
       apply (rule MDP.valid_cfgD[OF repcs st cfg  valid_cfg]; fail)
      using *** unfolding alw_holds_pred_stream_iff[symmetric] HLD_def .
    done
qed

end (* PTA Regions *)


subsection ‹Main Result› text_raw ‹ \label{thm:minmax} ›

context Probabilistic_Timed_Automaton_Regions_Reachability
begin

lemma R_G_cfg_on_valid:
  "cfg  R_G.valid_cfg" if "cfg  R_G_cfg_on_div s'"
  using that unfolding R_G_cfg_on_div_def R_G.valid_cfg_def by auto

lemma cfg_on_valid:
  "cfg  valid_cfg" if "cfg  cfg_on_div s"
  using that unfolding cfg_on_div_def MDP.valid_cfg_def by auto

abbreviation "path_measure P cfg  emeasure (MDP.T cfg) {xspace MDP.St. P x}"
abbreviation "R_G_path_measure P cfg  emeasure (R_G.T cfg) {xspace R_G.St. P x}"
abbreviation "progressive st  cfg_on_div st  {cfg. alternating cfg}"
abbreviation "R_G_progressive st  R_G_cfg_on_div st  {cfg. alternating cfg}"

text ‹Summary of our results on divergent configurations:›
lemma absc_valid_cfg_eq:
  "absc ` progressive s = R_G_progressive s'"
  apply safe
  subgoal
    unfolding s'_def by (rule cfg_on_div_absc) auto
  subgoal
    by (simp add: AE_alw_ev_same_loc_iff cfg_on_valid)
  subgoal for cfg
    unfolding s'_def
    by (frule cfg_on_div_repcs_strong)
       (auto 4 4
          simp: s'_def R_G_cfg_on_div_def AE_alw_ev_same_loc_iff'[symmetric]
          intro: R_G_cfg_on_valid absc_repcs_id[symmetric]
       )
  done

text ‹Main theorem:›
theorem Min_Max_reachability:
  notes in_space_UNIV[measurable] and [iff] = pred_stream_iff
  shows
  "(cfg progressive s.      path_measure     (λ x. (holds φ  suntil holds ψ)  (s  ## x)) cfg)
 = (cfg R_G_progressive s'. R_G_path_measure (λ x. (holds φ' suntil holds ψ') (s' ## x)) cfg)
  (cfg progressive s.      path_measure     (λ x. (holds φ  suntil holds ψ)  (s  ## x)) cfg)
 = (cfg R_G_progressive s'. R_G_path_measure (λ x. (holds φ' suntil holds ψ') (s' ## x)) cfg)"
proof (rule SUP_eq_and_INF_eq; rule bexI[rotated]; erule IntE)
  fix cfg assume cfg_div: "cfg  R_G_cfg_on_div s'" and "cfg  Collect alternating"
  then have "alternating cfg"
    by auto
  let ?cfg' = "repcs s cfg"
  from alternating cfg cfg_div have "alternating ?cfg'"
    by (simp add: R_G_cfg_on_div_def s'_def AE_alw_ev_same_loc_iff'[of _ s])
  with cfg_div alternating cfg show "?cfg'  cfg_on_div s  Collect alternating"
    by (auto intro: cfg_on_div_repcs_strong simp: s'_def)
  show "emeasure (R_G.T cfg)   {x  space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}
      = emeasure (MDP.T ?cfg') {x  space MDP.St. (holds φ suntil holds ψ)   (s ## x)}"
     (is "?a = ?b")
  proof -
    from cfg_div have "cfg  R_G.valid_cfg"
      by (rule R_G_cfg_on_valid)
    from cfg_div have "cfg  R_G.cfg_on s'"
      unfolding R_G_cfg_on_div_def by auto
    then have "state cfg = s'"
      by auto
    have "?a = ?b"
      apply (rule
          path_measure_eq_repcs''_new[
            of s cfg φ ψ, folded φ'_def ψ'_def, unfolded _ = s' state_repcs
            ]
          )
      subgoal
        unfolding s'_def ..
      subgoal
        by fact
      subgoal
        using ?cfg'  cfg_on_div s  _ by (blast intro: cfg_on_valid)
      subgoal premises prems for xs
        using prems s by (intro φ_stream)
      subgoal premises prems
        using prems s by (intro ψ_stream)
      done
    then show ?thesis
      by simp
  qed
next
  fix cfg assume cfg_div: "cfg  cfg_on_div s" and "cfg  Collect alternating"
  with absc_valid_cfg_eq show "absc cfg  R_G_cfg_on_div s'  Collect alternating"
    by auto
  show "emeasure (MDP.T cfg)        {x  space MDP.St. (holds φ suntil holds ψ)   (s ## x)}
      = emeasure (R_G.T (absc cfg)) {x  space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}"
    (is "?a = ?b")
  proof -
    have "absc cfg  R_G.valid_cfg"
      using R_G_cfg_on_valid absc cfg  R_G_cfg_on_div s'  _ by blast
    from cfg_div have "cfg  valid_cfg"
      by (simp add: cfg_on_valid)
    with absc cfg  R_G.valid_cfg have "?b = ?a"
      by (intro MDP.alw_S R_G.alw_S path_measure_eq_absc1_new
            [where P = "pred_stream (λs. s  𝒮)" and Q = "pred_stream (λs. s  S)"]
         )
         (auto simp: S_abss_𝒮 intro: 𝒮_abss_S intro!: suntil_abss suntil_reps, measurable)
    then show "?a = ?b"
      by simp
  qed
qed

end (* PTA Reachability Problem *)

end (* Theory *)