Theory Lib
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
lemma pred_stream_stl: "pred_stream φ xs ⟶ pred_stream φ (stl xs)"
by (cases xs) auto
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] .
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
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])
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)
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)
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
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
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
lemma pred_stream_sconst:
"pred_stream ((=) x) (sconst x)"
by coinduction simp
lemma alw_Stream: "alw P (x ## s) ⟷ P (x ## s) ∧ alw P s"
by (subst alw.simps) simp
lemma alw_True: "alw (λx. True) ω"
by (auto intro: all_imp_alw)
lemma alw_conjI:
"alw (P aand Q) xs" if "alw P xs" "alw Q xs"
using that by (simp add: alw_aand)
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)
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
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
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
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
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