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  x ~ y  φ x  φ y"
  assumes ψ: " x y. x  S  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<