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<