theory Lib imports "Timed_Automata.Timed_Automata" "Timed_Automata.Approx_Beta" "MDP_Aux" "Finiteness" "Sequence_LTL" "Instantiate_Existentials" "Graphs" begin section ‹Misc› lemma measurable_pred_stream[measurable]: fixes P shows "Measurable.pred (stream_space (count_space UNIV)) (pred_stream P)" proof - have [measurable]: "Measurable.pred (count_space UNIV) P" by measurable then show ?thesis unfolding stream.pred_set sset_range by simp qed lemma pmf_map_pmf_cong: fixes f g and μ :: "'a pmf" assumes "⋀ x. x ∈ μ ⟹ f x = y1 ⟷ g x = y2" shows "pmf (map_pmf f μ) y1 = pmf (map_pmf g μ) y2" unfolding pmf_map by (rule measure_pmf.finite_measure_eq_AE; simp add: AE_measure_pmf_iff assms split: split_indicator ) lemma collect_pair_finite[intro]: notes finite_subset[intro] assumes "finite {x. P x}" "finite {x. Q x}" shows "finite {(x, y) . P x ∧ Q y ∧ R x y}" using assms proof - from assms have "finite {(x, y) . P x ∧ Q y}" by auto moreover have "{(x, y) . P x ∧ (Q y ∧ R x y)} ⊆ {(x, y) . P x ∧ Q y}" by auto ultimately show ?thesis by blast qed lemma collect_pair_finite'[intro]: notes finite_subset[intro] assumes "finite {(x, y). P x y}" shows "finite {(x, y) . P x y ∧ R x y}" using assms proof - from assms have "finite {(x, y) . P x y}" by auto moreover have "{(x, y) . P x y ∧ R x y} ⊆ {(x, y) . P x y}" by auto ultimately show ?thesis by blast qed text ‹This is what we actually need in this theory› lemma collect_pair_finite''[intro]: notes finite_subset[intro] assumes "finite {(x, y). P x ∧ Q y}" shows "finite {(x, y) . P x ∧ Q y ∧ R x y}" using assms proof - from assms have "finite {(x, y) . P x ∧ Q y}" by auto moreover have "{(x, y) . P x ∧ Q y ∧ R x y} ⊆ {(x, y) . P x ∧ Q y}" by auto ultimately show ?thesis by blast qed lemma finite_imageI'[intro]: assumes "finite {(x, y). P x y}" shows "finite {f x y | x y. P x y}" proof - from assms have "finite ((λ (x, y). f x y) ` {(x, y). P x y})" by auto moreover have "((λ (x, y). f x y) ` {(x, y). P x y}) = {f x y | x y. P x y}" by auto ultimately show ?thesis by auto qed lemma finite_imageI''[intro]: assumes "finite (A × B)" shows "finite {f x y | x y. x ∈ A ∧ y ∈ B ∧ R x y}" proof - from assms have "finite {f x y | x y. x ∈ A ∧ y ∈ B}" by auto moreover have "{f x y | x y. x ∈ A ∧ y ∈ B ∧ R x y} ⊆ {f x y | x y. x ∈ A ∧ y ∈ B}" by auto ultimately show ?thesis by (blast intro: finite_subset) qed (* TODO: Move/should be somewhere already *) lemma pred_stream_stl: "pred_stream φ xs ⟶ pred_stream φ (stl xs)" by (cases xs) auto (* TODO: Should be somewhere already *) lemma stream_all_pred_stream: "stream_all = pred_stream" by (intro ext) (simp add: stream.pred_set) lemma pred_stream_iff: "pred_stream P s ⟷ Ball (sset s) P" using stream_all_iff[unfolded stream_all_pred_stream] . (* TODO: Move *) lemma measure_pmf_eq_1_iff: "emeasure (measure_pmf μ) {x} = 1 ⟷ μ = return_pmf x" using measure_pmf.prob_eq_1[of "{x}" μ] set_pmf_subset_singleton[of μ x] by (auto simp: measure_pmf.emeasure_eq_measure AE_measure_pmf_iff) lemma HLD_mono: "HLD S ω" if "HLD R ω" "R ⊆ S" using that unfolding HLD_iff by auto lemma alw_HLD_smap: "alw (HLD (f ` S)) (smap f ω)" if "alw (HLD S) ω" using that by (auto 4 3 elim: HLD_mono alw_mono) lemma alw_disjoint_ccontr: assumes "alw (HLD S) ω" "ev (alw (HLD R)) ω" "R ∩ S = {}" shows False proof - from assms(1,2) obtain ω where "alw (HLD S) ω" "alw (HLD R) ω" by (auto intro: alw_sdrop sdrop_wait) with ‹R ∩ S = {}› show False by (auto 4 3 simp: HLD_iff dest: alwD) qed (* TODO: Move *) lemma stream_all2_refl: "stream_all2 P x x = pred_stream (λ x. P x x) x" by (simp add: stream.pred_rel eq_onp_def) (standard; coinduction arbitrary: x; auto) lemma AE_all_imp_countable: assumes "countable {x. Q x}" shows "(AE x in M. ∀y. Q y ⟶ P x y) = (∀y. Q y ⟶ (AE x in M. P x y))" using assms by (auto dest: AE_ball_countable) lemma AE_conj: "almost_everywhere M P = almost_everywhere M (λ x. P x ∧ Q x)" if "almost_everywhere M Q" by (auto intro: AE_mp[OF that]) (* TODO: move *) lemma list_hd_lastD: assumes "length xs > 1" obtains x y ys where "xs = x # ys @ [y]" using assms by atomize_elim (cases xs; simp; metis rev_exhaust) (* TODO: Move *) lemma SUP_eq_and_INF_eq: assumes "⋀i. i ∈ A ⟹ ∃j∈B. f i = g j" and "⋀j. j ∈ B ⟹ ∃i∈A. g j = f i" shows "⨆((f :: _ ⇒ _ :: complete_lattice) ` A) = ⨆(g ` B) ∧ ⨅(f ` A) = ⨅(g ` B)" by (auto 4 3 intro!: INF_eq SUP_eq dest: assms) (* TODO: Move *) lemma measurable_alw_stream[measurable]: fixes P assumes [measurable]: "Measurable.pred (stream_space (count_space UNIV)) P" shows "Measurable.pred (stream_space (count_space UNIV)) (alw P)" unfolding alw_iff_sdrop by measurable (* TODO: Move *) lemma ev_neq_start_implies_ev_neq: assumes "ev (Not o HLD {y}) (y ## xs)" shows "ev (λ xs. shd xs ≠ shd (stl xs)) (y ## xs)" using assms apply (induction "y ## xs" arbitrary: xs rule: ev.induct) apply (simp; fail) subgoal for xs apply (cases "shd xs = y") subgoal apply safe apply (rule ev.step) apply simp using stream.collapse[of xs, symmetric] by blast subgoal by auto done done (* TODO: Move *) lemma ev_sdropD: assumes "ev P xs" obtains i where "P (sdrop i xs)" using assms apply atomize_elim apply (induction rule: ev.induct) apply (inst_existentials "0 :: nat"; simp; fail) apply (erule exE) subgoal for xs i by (inst_existentials "i + 1") simp done (* TODO: Move *) lemma pred_stream_sconst: "pred_stream ((=) x) (sconst x)" by coinduction simp (* TODO: Move *) lemma alw_Stream: "alw P (x ## s) ⟷ P (x ## s) ∧ alw P s" by (subst alw.simps) simp (* TODO: Move *) lemma alw_True: "alw (λx. True) ω" by (auto intro: all_imp_alw) (* TODO: Move *) lemma alw_conjI: "alw (P aand Q) xs" if "alw P xs" "alw Q xs" using that by (simp add: alw_aand) (* TODO: Move *) lemma alw_ev_cong: "alw (ev S) xs = alw (ev R) xs" if "alw P xs" "⋀ x. P x ⟹ S x ⟷ R x" by (rule alw_cong[where P = "alw P"]) (auto simp: HLD_iff that elim!: ev_cong) lemma alw_ev_HLD_cong: "alw (ev (HLD S)) xs = alw (ev (HLD R)) xs" if "alw (HLD P) xs" "⋀ x. x ∈ P ⟹ x ∈ S ⟷ x ∈ R" by (rule alw_ev_cong, rule that; simp add: HLD_iff that) (* TODO: Move *) lemma measurable_eq_stream_space[measurable (raw)]: assumes [measurable]: "f ∈ M →⇩_{M}stream_space (count_space UNIV)" shows "Measurable.pred M (λx. f x = c)" proof - have *: "(λx. f x = c) = (λx. ∀i. f x !! i = c !! i)" by (auto intro: eqI_snth simp: fun_eq_iff) show ?thesis unfolding * by measurable qed (* TODO: rename, and change to LTL constants i.e. HLD, aand, nxt etc. *) lemma prop_nth_sdrop: assumes "∀ i≥j. P (ω !! i)" shows "∀ i. P (sdrop j ω !! i)" using assms by (induction j arbitrary: ω) fastforce+ lemma prop_nth_sdrop_pair: assumes "∀ i. P (ω !! i) (ω' !! i)" shows "∀ i. P (sdrop j ω !! i) (sdrop j ω' !! i)" using assms by (induction j arbitrary: ω ω') (auto, metis snth.simps(2)) lemma prop_nth_stl: "∀ i. P (xs !! i) ⟹ ∀ i. P (stl xs !! i)" by (metis snth.simps(2)) context Graph_Defs begin lemma steps_SCons_iff: "steps (x # y # xs) ⟷ E x y ∧ steps (y # xs)" by (auto elim: steps.cases) lemma steps_Single_True: "steps [x] = True" by auto lemma add_step_iff: "(∀ xs y. steps (x # xs @ [y]) ∧ length xs = Suc n ⟶ P xs y) ⟷ (∀ z xs y. steps (x # z # xs @ [y]) ∧ length xs = n ⟶ P (z # xs) y)" apply safe apply fastforce subgoal for xs y by (cases xs) auto done lemma compower_stepsD: assumes "(E ^^ n) s s'" obtains xs where "steps xs" "hd xs = s" "last xs = s'" "length xs = n + 1" using assms apply atomize_elim proof (induction n arbitrary: s') case 0 then show ?case by auto next case (Suc n) from Suc.prems show ?case by (auto 4 4 intro: steps_append_single dest: Suc.IH) qed lemma compower_stepsD': assumes "(E ^^ n) s s'" "n > 0" obtains xs where "steps (s # xs @ [s'])" "length xs + 1 = n" apply (rule compower_stepsD[OF assms(1)]) subgoal for xs by (auto simp: ‹n > 0› intro: list_hd_lastD[of xs]) done end context MC_syntax begin theorem AE_T_iff_n: fixes P :: "'s stream ⇒ bool" and x :: "'s" assumes "Measurable.pred (stream_space (count_space UNIV)) P" "n > 0" shows "almost_everywhere (T x) P = (∀xs y. Graph_Defs.steps (λ a b. b ∈ K a) (x # xs @ [y]) ∧ length xs + 1 = n ⟶ (AE ω in T y. P (xs @- y ## ω)))" using assms apply (induction n arbitrary: x P) apply (simp; fail) subgoal for n x P apply (cases n) subgoal by (subst AE_T_iff) (auto simp: Graph_Defs.steps_SCons_iff Graph_Defs.steps_Single_True) subgoal premises prems for n' proof - have *: "Measurable.pred (stream_space (count_space UNIV)) (λ ω. P (y ## ω))" for y using prems(2) by measurable with prems(1)[OF *] prems(3-) show ?thesis by (auto simp: AE_T_iff[OF prems(2)] Graph_Defs.steps_SCons_iff Graph_Defs.add_step_iff) qed done done lemma AE_alw_accD: fixes P assumes P: "Measurable.pred (stream_space (count_space UNIV)) P" assumes *: "almost_everywhere (T s) (alw P)" "(s, s') ∈ acc" shows "almost_everywhere (T s') (alw P)" using *(2,1) proof induction case (step y z) then have "almost_everywhere (T y) (alw P)" "z ∈ K y" by auto then have "AE ω in T z. alw P (z ## ω)" unfolding AE_T_iff[OF measurable_alw_stream[OF P], of y] by auto then show ?case by eventually_elim auto qed lemma acc_relfunD: assumes "(s, s') ∈ acc" obtains n where "((λ a b. b ∈ K a) ^^ n) s s'" using assms apply atomize_elim apply (drule rtrancl_imp_relpow) apply (erule exE) subgoal for n by (inst_existentials n) (induction n arbitrary: s'; auto) done (* TODO: If we can show measurable_alw_stream, then this subsumed by the lemma above *) lemma AE_all_accD: assumes "almost_everywhere (T s) (pred_stream P)" "(s, s') ∈ acc" shows "almost_everywhere (T s') (pred_stream P)" proof - from acc_relfunD[OF ‹_ ∈ acc›] obtain n where *: "((λ a b. b ∈ K a) ^^ n) s s'" . show ?thesis proof (cases "n = 0") case True with * assms(1) show ?thesis by auto next case False then have "n > 0" by simp with * obtain xs where "Graph_Defs.steps (λa b. b ∈ set_pmf (K a)) (s # xs @ [s'])" "Suc (length xs) = n" by (auto elim: Graph_Defs.compower_stepsD') with assms(1)[unfolded AE_T_iff_n[OF measurable_pred_stream ‹n > 0›, of P s]] show ?thesis by auto qed qed lemma AE_T_ev_HLD_infinite_strong': assumes "0 ≤ r" "r < 1" and r: "⋀x. x ∈ X ∩ Y ⟹ measure_pmf.prob (K x) Y ≤ r" and ae: "AE ω in T x. alw (λ ω. HLD Y ω ⟶ ev (HLD X) ω) ω" shows "AE ω in T x. ev (HLD (- Y)) ω" proof - define run where "run F = (HLD (Y - X)) suntil ((X ∩ Y) ⋅ Y ⋅ F)" for F have le_gfp: "alw (HLD Y) aand alw (λ ω. HLD Y ω ⟶ ev (HLD X) ω) ≤ gfp run" proof (rule gfp_upperbound; clarsimp) fix ω assume "alw (HLD Y) ω" "alw (λω. HLD Y ω ⟶ ev (HLD X) ω) ω" then have "ev (HLD X) ω" "alw (HLD Y) ω" "alw (λω. HLD Y ω ⟶ ev (HLD X) ω) ω" by auto then show "run (λxs. alw (HLD Y) xs ∧ alw (λω. HLD Y ω ⟶ ev (HLD X) ω) xs) ω" proof (induction ω rule: ev_induct_strong) case (base ω) then show ?case by (cases ω) (auto intro!: suntil.base simp: alw_Stream run_def) next case (step ω) show ?case unfolding run_def using ‹¬ HLD X ω› ‹alw (HLD Y) ω› step(3)[unfolded run_def] step(4,5) by (auto 0 4 simp: HLD_def intro: suntil.step) qed qed have cont_run: "inf_continuous run" apply (auto simp: inf_continuous_def fun_eq_iff run_def) subgoal premises that for M x f by (rule suntil_mono[OF _ _ that(2) alw_True]) auto subgoal premises that for M x using that(2)[THEN spec, of 0] that(2) proof (induction rule: suntil_induct_strong) case (base ω) then show ?case by (cases ω) (simp add: suntil_Stream) next case (step ω) then show ?case by (cases ω) (simp add: suntil_Stream) qed done have [measurable]: "Measurable.pred (stream_space (count_space UNIV)) (gfp run)" apply measurable apply (rule measurable_gfp[OF cont_run]) apply (auto simp: run_def) done have "emeasure (T x) {ω ∈ space (T x). alw (HLD Y) ω} ≤ emeasure (T x) {ω ∈ space (T x). ((alw (HLD Y)) aand (alw (λ ω. HLD Y ω ⟶ ev (HLD X) ω))) ω}" apply (rule emeasure_mono_AE) subgoal using ae by eventually_elim auto by measurable also have "… ≤ emeasure (T x) {ω ∈ space (T x). gfp run ω}" apply (rule emeasure_mono) subgoal using le_gfp by auto by measurable also have "… ≤ r ^ n" for n proof (induction n arbitrary: x) case 0 then show ?case by (simp add: T.emeasure_le_1) next case (Suc n) { fix x have "(∫⇧^{+}t. ∫⇧^{+}t'. emeasure (T t') {x∈space S. t∈X ∧ t∈Y ∧ t'∈Y ∧ gfp run x} ∂K t ∂K x) ≤ (∫⇧^{+}t. indicator (X ∩ Y) t * ∫⇧^{+}t'. indicator Y t' * ennreal (r ^ n) ∂K t ∂K x)" using Suc by (auto intro!: nn_integral_mono split: split_indicator) also have "… ≤ (∫⇧^{+}t. indicator (X ∩ Y) t * r ∂K x) * ennreal (r^n)" by (auto intro!: nn_integral_mono mult_right_mono r ennreal_leI split: split_indicator simp: nn_integral_multc mult.assoc[symmetric] measure_pmf.emeasure_eq_measure) also have "… = emeasure (K x) (X ∩ Y) * r^(Suc n)" by (simp add: ennreal_mult ‹0 ≤ r› nn_integral_multc ennreal_indicator mult.assoc) finally have *: "(∫⇧^{+}t. ∫⇧^{+}t'. emeasure (T t') {x∈space S. t ∈ X ∧ t ∈ Y ∧ t' ∈ Y ∧ gfp run x} ∂K t ∂K x) ≤ emeasure (K x) (X ∩ Y) * r^Suc n" . have "(∫⇧^{+}t. ∫⇧^{+}t'. emeasure (T t') {x ∈ space S. t ∈ X ∧ t ∈ Y ∧ t' ∈ Y ∧ gfp run x} ∂K t ∂K x) + ennreal (r^Suc n) * emeasure (measure_pmf (K x)) (Y - X) ≤ emeasure (K x) (X ∩ Y) * ennreal (r^Suc n) + ennreal (r^Suc n) * emeasure (measure_pmf (K x)) (Y - X)" by (intro add_mono_left *) also have "… = emeasure (K x) ((X ∩ Y) ∪ (Y - X)) * ennreal (r^Suc n)" by (subst plus_emeasure[symmetric]) (auto simp: field_simps) also have "… ≤ 1 * ennreal (r^Suc n)" by (intro mult_right_mono measure_pmf.emeasure_le_1) simp finally have "(∫⇧^{+}t. ∫⇧^{+}t'. emeasure (T t') {x ∈ space MC_syntax.S. t ∈ X ∧ t ∈ Y ∧ t' ∈ Y ∧ gfp run x} ∂K t ∂K x) + ennreal (r^Suc n) * emeasure (measure_pmf (K x)) (Y - X) ≤ 1 * ennreal (r^Suc n)" by simp } note * = this show ?case apply (subst gfp_unfold[OF inf_continuous_mono[OF cont_run]]) apply (subst run_def) apply (subst emeasure_suntil_disj) apply measurable [] subgoal for s by (rule AE_I2) (auto simp: HLD_iff) apply (rule le_funD[of _ _ x]) apply (rule lfp_lowerbound) apply (rule le_funI) apply (subst emeasure_Collect_T) apply measurable [] apply (subst emeasure_Collect_T) apply simp apply (simp add: nn_integral_cmult) using * by simp qed finally have "emeasure (T x) {ω ∈ space (T x). alw (HLD Y) ω} ≤ r^n" for n . then have "emeasure (T x) {ω ∈ space (T x). alw (HLD Y) ω} ≤ ennreal 0" using ‹0 ≤ r› ‹r < 1› by (intro LIMSEQ_le_const[OF tendsto_ennrealI[OF LIMSEQ_power_zero[of r]]]) auto then have *: "emeasure (T x) {ω ∈ space (T x). alw (HLD Y) ω} = 0" by simp show ?thesis by (rule AE_I[OF _ *]) (auto simp: not_ev_iff not_HLD[symmetric]) qed end context Markov_Decision_Process begin lemma cfg_on_inv: "pred_stream (λ cfg. cfg ∈ cfg_on (state cfg)) ω" if "MC.enabled cfg ω" "cfg ∈ cfg_on s" using that proof (coinduction arbitrary: ω cfg s) case prems: stream_pred note [simp] = ‹_ = ω›[symmetric] from prems(2) have "a ∈ set_pmf (K_cfg cfg)" "MC.enabled a w" by (auto simp: MC.enabled_Stream) moreover from ‹a ∈ _› have "a ∈ cont cfg ` set_pmf (action cfg)" by (simp add: set_K_cfg) ultimately show ?case using ‹cfg ∈ _› by auto qed lemma MC_T_not_sconst_strong: assumes "∀ l. ∀ cfg ∈ (⋃ x ∈ f -` {u}. cfg_on x) ∩ Y ∩ X. measure_pmf (action cfg) (f -` {u}) ≤ r" "r < 1" "cfg ∈ cfg_on x" "AE ω in MC.T cfg. pred_stream (λ x. x ∈ X) ω" "AE ω in MC.T cfg. alw (λ ω. HLD (f -` {u}) (smap state ω) ⟶ ev (HLD Y) ω) ω" shows "AE ω in MC.T cfg. smap (f o state) ω ≠ sconst u" proof - let ?U = "f -` {u}" let ?S = "(⋃ x ∈ f -` {u}. cfg_on x) ∩ X" let ?T = "Y ∩ ((⋃ x ∈ f -` {u}. cfg_on x) ∩ X)" have *: "emeasure (K_cfg cfg) ?S ≤ r" if "cfg ∈ ?T" for cfg proof - have "emeasure (K_cfg cfg) ?S ≤ emeasure (measure_pmf (action cfg)) ?U" unfolding K_cfg_def by (auto dest: cfg_onD_state intro!: emeasure_mono) also from assms(1) ‹cfg ∈ ?T› have "… ≤ r" by auto finally show ?thesis . qed have "AE ω in MC.T cfg. ev (HLD (- ?S)) ω" apply (rule MC.AE_T_ev_HLD_infinite_strong'[where r = "enn2real r" and ?X = Y]) apply (simp; fail) subgoal using ‹r < 1› by (metis ennreal_enn2real_if ennreal_less_one_iff zero_less_one) subgoal for x by (drule *) (metis Sigma_Algebra.measure_def assms(2) enn2real_mono ennreal_one_less_top less_trans) subgoal using assms(5) by (rule AE_mp) (rule AE_I2, intro impI, auto simp: HLD_iff elim: alw_mono) done then show ?thesis apply (rule AE_mp) proof (rule AE_mp[OF assms(4)], rule AE_mp[OF MC.AE_T_enabled], rule AE_I2, safe) fix ω assume "ω ∈ space (MC.T cfg)" "pred_stream (λω. ω ∈ X) ω" "MC.enabled cfg ω" "ev (HLD (- ?S)) ω" "smap (f ∘ state) ω = sconst u" from this(2,3) ‹cfg ∈ _› have "pred_stream (λ x. x ∈ cfg_on (state x)) ω" by (auto dest: cfg_onD_state intro!: cfg_on_inv) from ‹smap _ ω = _› have "pred_stream (λ y. y ∈ (⋃ x ∈ ?U. cfg_on x)) ω" proof - have "(f o state) cfg = u" if "cfg ∈ sset ω" for cfg using stream.set_map[of "f o state" ω] that ‹smap _ ω = _› by fastforce with ‹pred_stream (λ x. x ∈ cfg_on (state x)) ω› show ?thesis by (auto elim!: stream.pred_mono_strong) qed with ‹pred_stream (λω. ω ∈ X) ω› have "pred_stream (λ x. x ∈ ?S) ω" by (coinduction arbitrary: ω) auto then have "alw (HLD ?S) ω" by (simp add: alw_holds_pred_stream_iff HLD_def) with ‹ev (HLD (- ?S)) ω› show False unfolding not_ev_not[symmetric] not_HLD by simp qed qed lemma MC_T_not_sconst: assumes "∀ l. ∀ cfg ∈ (⋃ x ∈ f -` {u}. cfg_on x) ∩ X. measure_pmf (action cfg) (f -` {u}) ≤ r" "r < 1" "cfg ∈ cfg_on x" "AE ω in MC.T cfg. pred_stream (λ x. x ∈ X) ω" shows "AE ω in MC.T cfg. smap (f o state) ω ≠ sconst u" proof - let ?U = "f -` {u}" let ?S = "(⋃ x ∈ f -` {u}. cfg_on x) ∩ X" have *: "emeasure (K_cfg cfg) ?S ≤ r" if "cfg ∈ ?S" for cfg proof - have "emeasure (K_cfg cfg) ?S ≤ emeasure (measure_pmf (action cfg)) ?U" unfolding K_cfg_def by (auto dest: cfg_onD_state intro!: emeasure_mono) also from assms(1) ‹cfg ∈ ?S› have "… ≤ r" by auto finally show ?thesis . qed have "AE ω in MC.T cfg. ev (HLD (- ?S)) ω" apply (rule MC.AE_T_ev_HLD_infinite[where r = "enn2real r"]) subgoal using ‹r < 1› by (metis ennreal_enn2real_if ennreal_less_one_iff zero_less_one) apply (drule *) by (metis Sigma_Algebra.measure_def assms(2) enn2real_mono ennreal_one_less_top less_trans) then show ?thesis apply (rule AE_mp) proof (rule AE_mp[OF assms(4)], rule AE_mp[OF MC.AE_T_enabled], rule AE_I2, safe) fix ω assume "ω ∈ space (MC.T cfg)" "pred_stream (λω. ω ∈ X) ω" "MC.enabled cfg ω" "ev (HLD (- ?S)) ω" "smap (f ∘ state) ω = sconst u" from this(2,3) ‹cfg ∈ _› have "pred_stream (λ x. x ∈ cfg_on (state x)) ω" by (auto dest: cfg_onD_state intro!: cfg_on_inv) from ‹smap _ ω = _› have "pred_stream (λ y. y ∈ (⋃ x ∈ ?U. cfg_on x)) ω" proof - have "(f o state) cfg = u" if "cfg ∈ sset ω" for cfg using stream.set_map[of "f o state" ω] that ‹smap _ ω = _› by fastforce with ‹pred_stream (λ x. x ∈ cfg_on (state x)) ω› show ?thesis by (auto elim!: stream.pred_mono_strong) qed with ‹pred_stream (λω. ω ∈ X) ω› have "pred_stream (λ x. x ∈ ?S) ω" by (coinduction arbitrary: ω) auto then have "alw (HLD ?S) ω" by (simp add: alw_holds_pred_stream_iff HLD_def) with ‹ev (HLD (- ?S)) ω› show False unfolding not_ev_not[symmetric] not_HLD by simp qed qed lemma MC_T_not_sconst': assumes "∀ cfg ∈ cfg_on x ∩ X. measure_pmf (action cfg) {x} ≤ r" "r < 1" "cfg ∈ cfg_on x'" "AE ω in MC.T cfg. pred_stream (λ x. x ∈ X) ω" shows "AE ω in MC.T cfg. smap state ω ≠ sconst x" using assms by (rule MC_T_not_sconst[where f = id, simplified]) lemma K_cfg_cfg_onI: "cfg' ∈ cfg_on (state cfg')" if "cfg ∈ cfg_on x" "cfg' ∈ K_cfg cfg" using that by (force simp: set_K_cfg) lemma MC_acc_cfg_onI: "cfg' ∈ cfg_on (state cfg')" if "(cfg, cfg') ∈ MC.acc" "cfg ∈ cfg_on x" proof - from that(1) obtain n where "((λ a b. b ∈ K_cfg a) ^^ n) cfg cfg'" by (erule MC.acc_relfunD) with ‹cfg ∈ cfg_on x› show ?thesis by (induction n arbitrary: cfg') (auto intro: K_cfg_cfg_onI) qed lemma non_loop_tail_strong: assumes "∀ l. ∀ cfg ∈ (⋃ x ∈ f -` {u}. cfg_on x) ∩ Y ∩ X. measure_pmf (action cfg) (f -` {u}) ≤ r" "r < 1" "cfg ∈ cfg_on x" "AE ω in MC.T cfg. pred_stream (λ x. x ∈ X) ω" "AE ω in MC.T cfg. alw (λ ω. HLD (f -` {u}) (smap state ω) ⟶ ev (HLD Y) ω) ω" shows "AE ω in MC.T cfg. ¬ (ev (alw (λ xs. shd xs = u))) (smap (f o state) ω)" (is "AE ω in ?M. ?P ω") proof - have *: "?P ω ⟷ alw (λ xs. smap (f o state) xs ≠ sconst u) ω" for ω apply (simp add: not_ev_iff) apply (rule arg_cong2[where f = alw]) apply (rule ext) subgoal for xs using MC.alw_HLD_iff_sconst[of u "smap (f o state) xs"] by (simp add: HLD_iff) by (rule HOL.refl) have "AE ω in ?M. alw (λ xs. smap (f o state) xs ≠ sconst u) ω" apply (rule MC.AE_T_alw) subgoal by (intro pred_intros_logic measurable_eq_stream_space) measurable using assms by - (erule MC_T_not_sconst_strong, auto intro: MC.AE_all_accD MC.AE_alw_accD elim: MC_acc_cfg_onI ) with * show ?thesis by simp qed lemma non_loop_tail: assumes "∀ l. ∀ cfg ∈ (⋃ x ∈ f -` {u}. cfg_on x) ∩ X. measure_pmf (action cfg) (f -` {u}) ≤ r" "r < 1" "cfg ∈ cfg_on x" "AE ω in MC.T cfg. pred_stream (λ x. x ∈ X) ω" shows "AE ω in MC.T cfg. ¬ (ev (alw (λ xs. shd xs = u))) (smap (f o state) ω)" (is "AE ω in ?M. ?P ω") proof - have *: "?P ω ⟷ alw (λ xs. smap (f o state) xs ≠ sconst u) ω" for ω apply (simp add: not_ev_iff) apply (rule arg_cong2[where f = alw]) apply (rule ext) subgoal for xs using MC.alw_HLD_iff_sconst[of u "smap (f o state) xs"] by (simp add: HLD_iff) by (rule HOL.refl) have "AE ω in ?M. alw (λ xs. smap (f o state) xs ≠ sconst u) ω" apply (rule MC.AE_T_alw) subgoal by (intro pred_intros_logic measurable_eq_stream_space) measurable using assms by - (erule MC_T_not_sconst, auto intro: MC.AE_all_accD elim: MC_acc_cfg_onI) with * show ?thesis by simp qed lemma non_loop_tail': assumes "∀ cfg ∈ cfg_on x ∩ X. measure_pmf (action cfg) {x} ≤ r" "r < 1" "cfg ∈ cfg_on y" "AE ω in MC.T cfg. pred_stream (λ x. x ∈ X) ω" shows "AE ω in MC.T cfg. ¬ (ev (alw (λ xs. shd xs = x))) (smap state ω)" using assms by simp (erule non_loop_tail[where f = id, simplified]) end lemma (in Regions) intv_const_mono: assumes "u ∈ region X I r" "c1 ∈ X" "c2 ∈ X" "u c1 ≤ u c2" "¬ isGreater (I c2)" shows "intv_const (I c1) ≤ intv_const (I c2)" proof - from assms have "intv_elem c1 u (I c1)" "intv_elem c2 u (I c2)" by auto with ‹u c1 ≤ u c2› ‹¬ _› show ?thesis by (cases "I c1"; cases "I c2"; auto) qed lemma sset_sdrop: assumes "x ∈ sset (sdrop i xs)" shows "x ∈ sset xs" using assms by (auto simp: sset_range) lemma holds_untilD: assumes "(holds P until holds Q) xs" "∀ i ≤ j. ¬ Q (xs !! i)" shows "P (xs !! j)" using assms proof (induction j arbitrary: xs) case 0 then show ?case by cases auto next case (Suc j) from Suc.prems show ?case by cases (auto dest!: Suc.IH) qed (* TODO: Move *) lemma frac_le_self: assumes "x ≥ 0" shows "frac x ≤ x" using assms less_trans [of "frac x" 1 x] by (auto simp add: le_less frac_eq not_less frac_lt_1) lemma frac_le_1I: assumes "0 ≤ x" "x ≤ 1" "x ≤ y" shows "frac x ≤ y" using assms dual_order.trans frac_le_self by auto lemma frac_le_1I': assumes "0 ≤ x" "x ≤ y" "y < 1" shows "frac x ≤ frac y" proof - from assms have "frac y = y" by (simp add: frac_eq) moreover from assms have "frac x ≤ y" by (auto intro: frac_le_1I) ultimately show ?thesis by simp qed (* XXX Move *) lemmas [intro] = order.strict_implies_order[OF frac_lt_1] lemma nat_eventually_critical: assumes "P i" "¬ P j" "i < j" shows "∃ k ≥ i. P k ∧ ¬ P (Suc k)" using assms by (metis dec_induct less_le) lemma nat_eventually_critical_path: fixes i :: nat assumes "P i" "¬ P j" "i < j" shows "∃ k > i. k ≤ j ∧ ¬ P k ∧ (∀ m ≥ i. m < k ⟶ P m)" proof - let ?S = "{k. i < k ∧ k ≤ j ∧ ¬ P k}" let ?k = "Min ?S" from assms have "j ∈ ?S" by auto moreover have "finite ?S" by auto ultimately have "i < ?k" "?k ≤ j" "¬ P ?k" using Min_in[of ?S] by blast+ moreover have "P m" if "i ≤ m" "m < ?k" for m proof (cases "i = m") case True with ‹P i› show ?thesis by simp next case False with ‹i ≤ m› have "i < m" by simp with Min_le[OF ‹finite _›] ‹m < ?k› ‹?k ≤ j› show ?thesis by fastforce qed ultimately show ?thesis using ‹P i› by - (rule exI[where x = ?k]; blast) qed subsection ‹MDP Invariant› locale Markov_Decision_Process_Invariant = Markov_Decision_Process K for K :: "'s ⇒ 's pmf set"+ fixes S :: "'s set" assumes invariant: "⋀ s D. s ∈ S ⟹ D ∈ K s ⟹ (∀s' ∈ D. s' ∈ S)" begin lemma E_invariant: "{s'. (s, s') ∈ E} ⊆ S" if "s ∈ S" using that by (auto dest: invariant simp: E_def) definition "valid_cfg = (⋃s∈S. cfg_on s)" lemma valid_cfgI: "s ∈ S ⟹ cfg ∈ cfg_on s ⟹ cfg ∈ valid_cfg" by (auto simp: valid_cfg_def) lemma valid_cfgD: "cfg ∈ valid_cfg ⟹ cfg ∈ cfg_on (state cfg)" by (auto simp: valid_cfg_def) lemma action_closed: "s ∈ S ⟹ cfg ∈ cfg_on s ⟹ t ∈ action cfg ⟹ t ∈ S" using cfg_onD_action[of cfg s] invariant[of s] by auto lemma shows valid_cfg_state_in_S: "cfg ∈ valid_cfg ⟹ state cfg ∈ S" and valid_cfg_action: "cfg ∈ valid_cfg ⟹ s ∈ action cfg ⟹ s ∈ S" and valid_cfg_cont: "cfg ∈ valid_cfg ⟹ s ∈ action cfg ⟹ cont cfg s ∈ valid_cfg" by (auto simp: valid_cfg_def intro!: bexI[of _ s] intro: action_closed) lemma valid_K_cfg[intro]: "cfg ∈ valid_cfg ⟹ cfg' ∈ K_cfg cfg ⟹ cfg' ∈ valid_cfg" by (auto simp add: K_cfg_def valid_cfg_cont) lemma pred_stream_valid_cfg: assumes valid: "cfg ∈ valid_cfg" assumes enabled: "MC.enabled cfg xs" shows "pred_stream (λ cfg. cfg ∈ valid_cfg) xs" using assms by (coinduction arbitrary: cfg xs) (subst (asm) MC.enabled_iff; auto) lemma pred_stream_cfg_on: assumes valid: "cfg ∈ valid_cfg" assumes enabled: "MC.enabled cfg xs" shows "pred_stream (λ cfg. state cfg ∈ S ∧ cfg ∈ cfg_on (state cfg)) xs" using valid pred_stream_valid_cfg[OF _ enabled] unfolding stream.pred_set by (auto intro: valid_cfgI dest: valid_cfgD valid_cfg_state_in_S) lemma alw_S: "almost_everywhere (T cfg) (pred_stream (λs. s ∈ S))" if "cfg ∈ valid_cfg" unfolding T_def using pred_stream_cfg_on ‹cfg ∈ valid_cfg› by (subst AE_distr_iff) (measurable, auto simp: stream.pred_set intro: AE_mp[OF MC.AE_T_enabled]) end context Finite_Markov_Decision_Process begin sublocale Invariant: Markov_Decision_Process_Invariant rewrites "Invariant.valid_cfg = valid_cfg" proof - show "Markov_Decision_Process_Invariant K S" by standard (auto dest: set_pmf_closed) then show "Markov_Decision_Process_Invariant.valid_cfg K S = valid_cfg" by (subst Markov_Decision_Process_Invariant.valid_cfg_def; simp add: valid_cfg_def) qed lemmas pred_stream_cfg_on = Invariant.pred_stream_cfg_on and pred_stream_valid_cfg = Invariant.pred_stream_valid_cfg and alw_S = Invariant.alw_S and valid_cfg_state_in_S = Invariant.valid_cfg_state_in_S end end