# 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
"∀s∈sset (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
"∀s∈sset 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 "∀j≥i. ¬ 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 "∀j≥i. ¬ 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' ∧ (∀u∈R'. ∀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. ∃j≥i. ¬ 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 "∀i≥j. 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 "∃j≥i. 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 "∃j≥i. ¬ 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:
"∀k≤j - 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.∃j≥i.∃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
"∃j≥i<```