Theory MDP_Reachability_Problem
theory MDP_Reachability_Problem
imports Markov_Decision_Process
begin
inductive_set directed_towards :: "'a set ⇒ ('a × 'a) set ⇒ 'a set" for A r where
start: "⋀x. x ∈ A ⟹ x ∈ directed_towards A r"
| step: "⋀x y. y ∈ directed_towards A r ⟹ (x, y) ∈ r ⟹ x ∈ directed_towards A r"
hide_fact (open) start step
lemma directed_towards_mono:
assumes "s ∈ directed_towards A F" "F ⊆ G" shows "s ∈ directed_towards A G"
using assms by induct (auto intro: directed_towards.intros)
lemma directed_eq_rtrancl: "x ∈ directed_towards A r ⟷ (∃a∈A. (x, a) ∈ r⇧*)"
proof
assume "x ∈ directed_towards A r" then show "∃a∈A. (x, a) ∈ r⇧*"
by induction (auto intro: converse_rtrancl_into_rtrancl)
next
assume "∃a∈A. (x, a) ∈ r⇧*"
then obtain a where "(x, a) ∈ r⇧*" "a ∈ A" by auto
then show "x ∈ directed_towards A r"
by (induction rule: converse_rtrancl_induct)
(auto intro: directed_towards.start directed_towards.step)
qed
lemma directed_eq_rtrancl_Image: "directed_towards A r = (r⇧*)¯ `` A"
unfolding set_eq_iff directed_eq_rtrancl Image_iff by simp
locale Reachability_Problem = Finite_Markov_Decision_Process K S for K :: "'s ⇒ 's pmf set" and S +
fixes S1 S2 :: "'s set"
assumes S1: "S1 ⊆ S" and S2: "S2 ⊆ S" and S1_S2: "S1 ∩ S2 = {}"
begin
lemma [measurable]:
"S ∈ sets (count_space UNIV)" "S1 ∈ sets (count_space UNIV)" "S2 ∈ sets (count_space UNIV)"
by auto
definition
"v = (λcfg∈valid_cfg. emeasure (T cfg) {x∈space St. (HLD S1 suntil HLD S2) (state cfg ## x)})"
lemma v_eq: "cfg ∈ valid_cfg ⟹
v cfg = emeasure (T cfg) {x∈space St. (HLD S1 suntil HLD S2) (state cfg ## x)}"
by (auto simp add: v_def)
lemma real_v: "cfg ∈ valid_cfg ⟹ enn2real (v cfg) = 𝒫(ω in T cfg. (HLD S1 suntil HLD S2) (state cfg ## ω))"
by (auto simp add: v_def T.emeasure_eq_measure)
lemma v_le_1: "cfg ∈ valid_cfg ⟹ v cfg ≤ 1"
by (auto simp add: v_def T.emeasure_eq_measure)
lemma v_neq_Pinf[simp]: "cfg ∈ valid_cfg ⟹ v cfg ≠ top"
by (auto simp add: v_def)
lemma v_1_AE: "cfg ∈ valid_cfg ⟹ v cfg = 1 ⟷ (AE ω in T cfg. (HLD S1 suntil HLD S2) (state cfg ## ω))"
unfolding v_eq T.emeasure_eq_measure ennreal_eq_1 space_T[symmetric, of cfg]
by (rule T.prob_Collect_eq_1) simp
lemma v_0_AE: "cfg ∈ valid_cfg ⟹ v cfg = 0 ⟷ (AE x in T cfg. not (HLD S1 suntil HLD S2) (state cfg ## x))"
unfolding v_eq T.emeasure_eq_measure space_T[symmetric, of cfg] ennreal_eq_zero_iff[OF measure_nonneg]
by (rule T.prob_Collect_eq_0) simp
lemma v_S2[simp]: "cfg ∈ valid_cfg ⟹ state cfg ∈ S2 ⟹ v cfg = 1"
using S2 by (subst v_1_AE) (auto simp: suntil_Stream)
lemma v_nS12[simp]: "cfg ∈ valid_cfg ⟹ state cfg ∉ S1 ⟹ state cfg ∉ S2 ⟹ v cfg = 0"
by (subst v_0_AE) (auto simp: suntil_Stream)
lemma v_nS[simp]: "cfg ∉ valid_cfg ⟹ v cfg = undefined"
by (auto simp add: v_def)
lemma v_S1:
assumes cfg[simp, intro]: "cfg ∈ valid_cfg" and cfg_S1[simp]: "state cfg ∈ S1"
shows "v cfg = (∫⇧+s. v (cont cfg s) ∂action cfg)"
proof -
have [simp]: "state cfg ∉ S2"
using cfg_S1 S1_S2 S1 by blast
show ?thesis
by (auto simp: v_eq emeasure_Collect_T[of _ cfg] K_cfg_def map_pmf_rep_eq nn_integral_distr
AE_measure_pmf_iff suntil_Stream[of _ _ "state cfg"]
valid_cfg_cont
intro!: nn_integral_cong_AE)
qed
lemma real_v_integrable:
"integrable (action cfg) (λs. enn2real (v (cont cfg s)))"
by (rule measure_pmf.integrable_const_bound[where B="max 1 (enn2real undefined)"])
(auto simp add: v_def measure_def[symmetric] le_max_iff_disj)
lemma real_v_integral_eq:
assumes cfg[simp]: "cfg ∈ valid_cfg"
shows "enn2real (∫⇧+ s. v (cont cfg s) ∂action cfg) = ∫ s. enn2real (v (cont cfg s)) ∂action cfg"
by (subst integral_eq_nn_integral)
(auto simp: AE_measure_pmf_iff v_eq T.emeasure_eq_measure valid_cfg_cont
intro!: arg_cong[where f=enn2real] nn_integral_cong_AE)
lemma v_eq_0_coinduct[consumes 3, case_names valid nS2 cont]:
assumes *: "P cfg"
assumes valid: "⋀cfg. P cfg ⟹ cfg ∈ valid_cfg"
assumes nS2: "⋀cfg. P cfg ⟹ state cfg ∉ S2"
assumes cont: "⋀cfg cfg'. P cfg ⟹ state cfg ∈ S1 ⟹ cfg' ∈ K_cfg cfg ⟹ P cfg' ∨ v cfg' = 0"
shows "v cfg = 0"
proof -
from * valid[OF *]
have "AE x in MC_syntax.T K_cfg cfg. ¬ (HLD S1 suntil HLD S2) (state cfg ## smap state x)"
unfolding stream.map[symmetric] suntil_smap hld_smap'
proof (coinduction arbitrary: cfg rule: MC.AE_not_suntil_coinduct_strong)
case (ψ cfg) then show ?case
by (auto simp del: cfg_onD_state dest: nS2)
next
case (φ cfg' cfg)
then have *: "P cfg" "state cfg ∈ S1" "cfg' ∈ K_cfg cfg" and [simp, intro]: "cfg ∈ valid_cfg"
by auto
with cont[OF *] show ?case
by (subst (asm) v_0_AE)
(auto simp: suntil_Stream T_def AE_distr_iff suntil_smap hld_smap' cong del: AE_cong)
qed
then have "AE ω in T cfg. ¬ (HLD S1 suntil HLD S2) (state cfg ## ω)"
unfolding T_def by (subst AE_distr_iff) simp_all
with valid[OF *] show ?thesis
by (simp add: v_0_AE)
qed
definition "p = (λs∈S. P_sup s (λω. (HLD S1 suntil HLD S2) (s ## ω)))"
lemma p_eq_SUP_v: "s ∈ S ⟹ p s = ⨆ (v ` cfg_on s)"
by (auto simp add: p_def v_def P_sup_def T.emeasure_eq_measure intro: valid_cfgI intro!: SUP_cong cong: SUP_cong_simp)
lemma v_le_p: "cfg ∈ valid_cfg ⟹ v cfg ≤ p (state cfg)"
by (subst p_eq_SUP_v) (auto intro!: SUP_upper dest: valid_cfgD valid_cfg_state_in_S)
lemma p_eq_0_imp: "cfg ∈ valid_cfg ⟹ p (state cfg) = 0 ⟹ v cfg = 0"
using v_le_p[of cfg] by (auto intro: antisym)
lemma p_eq_0_iff: "s ∈ S ⟹ p s = 0 ⟷ (∀cfg∈cfg_on s. v cfg = 0)"
unfolding p_eq_SUP_v by (subst SUP_eq_iff) auto
lemma p_le_1: "s ∈ S ⟹ p s ≤ 1"
by (auto simp: p_eq_SUP_v intro!: SUP_least v_le_1 intro: valid_cfgI)
lemma p_undefined[simp]: "s ∉ S ⟹ p s = undefined"
by (simp add: p_def)
lemma p_not_inf[simp]: "s ∈ S ⟹ p s ≠ top"
using p_le_1[of s] by (auto simp: top_unique)
lemma p_S1: "s ∈ S1 ⟹ p s = (⨆D∈K s. ∫⇧+ t. p t ∂measure_pmf D)"
using S1 S1_S2 K_closed[of s] unfolding p_def
by (simp add: P_sup_iterate[of _ s] subset_eq set_eq_iff suntil_Stream[of _ _ s])
(auto intro!: SUP_cong nn_integral_cong_AE simp add: AE_measure_pmf_iff)
lemma p_S2[simp]: "s ∈ S2 ⟹ p s = 1"
using S2 by (auto simp: v_S2[OF valid_cfgI] p_eq_SUP_v)
lemma p_nS12: "s ∈ S ⟹ s ∉ S1 ⟹ s ∉ S2 ⟹ p s = 0"
by (auto simp: p_eq_SUP_v v_nS12[OF valid_cfgI])
lemma p_pos:
assumes "(s, t) ∈ (SIGMA s:S1. ⋃D∈K s. set_pmf D)⇧*" "t ∈ S2" shows "0 < p s"
using assms proof (induction rule: converse_rtrancl_induct)
case (step s t')
then obtain D where "s ∈ S1" "D ∈ K s" "t' ∈ D" "0 < p t'"
by auto
with S1 set_pmf_closed[of s D] have in_S: "⋀t. t ∈ D ⟹ t ∈ S"
by auto
from ‹t' ∈ D› ‹0 < p t'› have "0 < pmf D t' * p t'"
by (auto simp add: ennreal_zero_less_mult_iff pmf_positive)
also have "… ≤ (∫⇧+t. p t' * indicator {t'} t∂D)"
using in_S[OF ‹t' ∈ D›]
by (subst nn_integral_cmult_indicator) (auto simp: ac_simps emeasure_pmf_single)
also have "… ≤ (∫⇧+t. p t ∂D)"
by (auto intro!: nn_integral_mono_AE split: split_indicator simp: in_S AE_measure_pmf_iff
simp del: nn_integral_indicator_singleton)
also have "… ≤ p s"
using ‹s ∈ S1› ‹D ∈ K s› by (auto intro: SUP_upper simp add: p_S1)
finally show ?case .
qed simp
definition F_sup :: "('s ⇒ ennreal) ⇒ 's ⇒ ennreal" where
"F_sup f = (λs∈S. if s ∈ S2 then 1 else if s ∈ S1 then SUP D∈K s. ∫⇧+t. f t ∂measure_pmf D else 0)"
lemma F_sup_cong: "(⋀s. s ∈ S ⟹ f s = g s) ⟹ F_sup f s = F_sup g s"
using K_closed[of s]
by (auto simp: F_sup_def AE_measure_pmf_iff subset_eq
intro!: SUP_cong nn_integral_cong_AE)
lemma continuous_F_sup: "sup_continuous F_sup"
unfolding sup_continuous_def fun_eq_iff F_sup_def[abs_def]
by (auto simp: SUP_apply[abs_def] nn_integral_monotone_convergence_SUP intro: SUP_commute)
lemma mono_F_sup: "mono F_sup"
by (intro sup_continuous_mono continuous_F_sup)
lemma lfp_F_sup_iterate: "lfp F_sup = (SUP i. (F_sup ^^ i) (λx∈S. 0))"
proof -
{ have "(SUP i. (F_sup ^^ i) ⊥) = (SUP i. (F_sup ^^ i) (λx∈S. 0))"
proof (rule SUP_eq)
fix i show "∃j∈UNIV. (F_sup ^^ i) ⊥ ≤ (F_sup ^^ j) (λx∈S. 0)"
by (intro bexI[of _ i] funpow_mono mono_F_sup) auto
have *: "(λx∈S. 0) ≤ F_sup ⊥"
using K_wf by (auto simp: F_sup_def le_fun_def)
show "∃j∈UNIV. (F_sup ^^ i) (λx∈S. 0) ≤ (F_sup ^^ j) ⊥"
by (auto intro!: exI[of _ "Suc i"] funpow_mono mono_F_sup *
simp del: funpow.simps simp add: funpow_Suc_right le_funI)
qed }
then show ?thesis
by (auto simp: sup_continuous_lfp continuous_F_sup)
qed
lemma p_eq_lfp_F_sup: "p = lfp F_sup"
proof -
{ fix s assume "s ∈ S" let ?F = "λP. HLD S2 or (HLD S1 aand nxt P)"
have "P_sup s (λω. (HLD S1 suntil HLD S2) (s ## ω)) = (⨆i. P_sup s (λω. (?F ^^ i) ⊥ (s ## ω)))"
proof (simp add: suntil_def, rule P_sup_lfp)
show "(##) s ∈ measurable St St"
by simp
fix P assume P: "Measurable.pred St P"
show "Measurable.pred St (HLD S2 or (HLD S1 aand (λω. P (stl ω))))"
by (intro pred_intros_logic measurable_compose[OF _ P] measurable_compose[OF measurable_shd]) auto
qed (auto simp: sup_continuous_def)
also have "… = (SUP i. (F_sup ^^ i) (λx∈S. 0) s)"
proof (rule SUP_cong)
fix i from ‹s ∈ S› show "P_sup s (λω. (?F ^^ i) ⊥ (s##ω)) = (F_sup ^^ i) (λx∈S. 0) s"
proof (induct i arbitrary: s)
case (Suc n) show ?case
proof (subst P_sup_iterate)
show "Measurable.pred St (λω. (?F ^^ Suc n) ⊥ (s ## ω))"
apply (intro measurable_compose[OF measurable_Stream[OF measurable_const measurable_ident_sets[OF refl]] measurable_predpow])
apply simp
apply (simp add: bot_fun_def[abs_def])
apply (intro pred_intros_logic measurable_compose[OF measurable_stl] measurable_compose[OF measurable_shd])
apply auto
done
next
show "(⨆D∈K s. ∫⇧+ t. P_sup t (λω. (?F ^^ Suc n) ⊥ (s ## t ## ω)) ∂measure_pmf D) =
(F_sup ^^ Suc n) (λx∈S. 0) s"
unfolding funpow.simps comp_def
using S1 S2 ‹s ∈ S›
by (subst F_sup_cong[OF Suc(1)[symmetric]])
(auto simp add: F_sup_def measure_pmf.emeasure_space_1[simplified] K_wf subset_eq)
qed
qed simp
qed simp
finally have "lfp F_sup s = P_sup s (λω. (HLD S1 suntil HLD S2) (s ## ω))"
by (simp add: lfp_F_sup_iterate image_comp) }
moreover have "⋀s. s ∉ S ⟹ lfp F_sup s = undefined"
by (subst lfp_unfold[OF mono_F_sup]) (auto simp add: F_sup_def)
ultimately show ?thesis
by (auto simp: p_def)
qed
definition "S⇩e = {s∈S. p s = 0}"
lemma S⇩e: "S⇩e ⊆ S"
by (auto simp add: S⇩e_def)
lemma v_S⇩e: "cfg ∈ valid_cfg ⟹ state cfg ∈ S⇩e ⟹ v cfg = 0"
using p_eq_0_imp[of cfg] by (auto simp: S⇩e_def)
lemma S⇩e_nS2: "S⇩e ∩ S2 = {}"
by (auto simp: S⇩e_def)
lemma S⇩e_E1: "s ∈ S⇩e ∩ S1 ⟹ (s, t) ∈ E ⟹ t ∈ S⇩e"
unfolding S⇩e_def using S1
by (auto simp: p_S1 SUP_eq_iff K_wf nn_integral_0_iff_AE AE_measure_pmf_iff E_def
intro: set_pmf_closed antisym
cong: rev_conj_cong)
lemma S⇩e_E2: "s ∈ S1 ⟹ (⋀t. (s, t) ∈ E ⟹ t ∈ S⇩e) ⟹ s ∈ S⇩e"
unfolding S⇩e_def using S1 S1_S2
by (force simp: p_S1 SUP_eq_iff K_wf nn_integral_0_iff_AE AE_measure_pmf_iff E_def
cong: rev_conj_cong)
lemma S⇩e_E_iff: "s ∈ S1 ⟹ s ∈ S⇩e ⟷ (∀t. (s, t) ∈ E ⟶ t ∈ S⇩e)"
using S⇩e_E1[of s] S⇩e_E2[of s] by blast
definition "S⇩r = S - (S⇩e ∪ S2)"
lemma S⇩r: "S⇩r ⊆ S"
by (auto simp: S⇩r_def)
lemma S⇩r_S1: "S⇩r ⊆ S1"
by (auto simp: p_nS12 S⇩r_def S⇩e_def)
lemma S⇩r_eq: "S⇩r = S1 - S⇩e"
using S1_S2 S1 S2 by (auto simp add: S⇩r_def S⇩e_def p_nS12)
lemma v_neq_0_imp: "cfg ∈ valid_cfg ⟹ v cfg ≠ 0 ⟹ state cfg ∈ S⇩r ∪ S2"
using p_eq_0_imp[of cfg] by (auto simp add: S⇩r_def S⇩e_def valid_cfg_state_in_S)
lemma valid_cfg_action_in_K: "cfg ∈ valid_cfg ⟹ action cfg ∈ K (state cfg)"
by (auto dest!: valid_cfgD)
lemma K_cfg_E: "cfg ∈ valid_cfg ⟹ cfg' ∈ K_cfg cfg ⟹ (state cfg, state cfg') ∈ E"
by (auto simp: E_def K_cfg_def valid_cfg_action_in_K)
lemma S⇩r_directed_towards_S2:
assumes s: "s ∈ S⇩r"
shows "s ∈ directed_towards S2 {(s, t) | s t. s ∈ S⇩r ∧ (s, t) ∈ E}" (is "s ∈ ?D")
proof -
{ fix cfg assume "s ∉ ?D" "cfg ∈ cfg_on s"
with s S⇩r have "state cfg ∈ S⇩r" "state cfg ∉ ?D" "cfg ∈ valid_cfg"
by (auto intro: valid_cfgI)
then have "v cfg = 0"
proof (coinduction arbitrary: cfg rule: v_eq_0_coinduct)
case (cont cfg' cfg)
with v_neq_0_imp[of cfg'] show ?case
by (auto intro: directed_towards.intros K_cfg_E)
qed (auto intro: directed_towards.intros) }
with p_eq_0_iff[of s] s show ?thesis
unfolding S⇩r_def S⇩e_def by blast
qed
definition "proper ct ⟷ ct ∈ Pi⇩E S K ∧ (∀s∈S⇩r. v (simple ct s) > 0)"
lemma S⇩r_nS2: "s ∈ S⇩r ⟹ s ∉ S2"
by (auto simp: S⇩r_def)
lemma properD1: "proper ct ⟹ ct ∈ Pi⇩E S K"
by (auto simp: proper_def)
lemma proper_eq:
assumes ct[simp, intro]: "ct ∈ Pi⇩E S K"
shows "proper ct ⟷ S⇩r ⊆ directed_towards S2 (SIGMA s:S⇩r. ct s)"
(is "_ ⟷ _ ⊆ ?D")
proof -
have *[simp]: "⋀s. s ∈ S⇩r ⟹ s ∈ S" and ct': "ct ∈ Pi S K"
using ct by (auto simp: S⇩r_def simp del: ct)
{ fix s t have "s ∈ S ⟹ t ∈ ct s ⟹ t ∈ S"
using K_closed[of s] ct' by (auto simp add: subset_eq) }
note ct_closed = this
let ?C = "simple ct"
from ct have valid_C[simp]: "⋀s. s ∈ S ⟹ ?C s ∈ valid_cfg"
by (auto simp add: PiE_def)
{ fix s assume "s ∈ ?D"
then have "0 < v (?C s)"
proof induct
case (step s t)
then have s: "s ∈ S⇩r" and t: "t ∈ ct s" and [simp]: "s ∈ S"
by auto
with S⇩r_S1 ct have "v (?C s) = (∫⇧+t. v (?C t) ∂ct s)"
by (subst v_S1) (auto intro!: nn_integral_cong_AE AE_pmfI)
also have "… ≠ 0"
using ct t step
by (subst nn_integral_0_iff_AE) (auto simp add: AE_measure_pmf_iff zero_less_iff_neq_zero)
finally show ?case
using ct by (auto simp add: less_le)
qed (subst v_S2, insert S2, auto) }
moreover
{ fix s assume s: "s ∉ ?D" "s ∈ S⇩r"
with ct' have C: "?C s ∈ cfg_on s" and [simp]: "s ∈ S"
by auto
from s have "v (?C s) = 0"
proof (coinduction arbitrary: s rule: v_eq_0_coinduct)
case (cont cfg s)
with S1 obtain t where "cfg = ?C t" "t ∈ ct s" "s ∈ S"
by (auto simp: set_K_cfg subset_eq)
with cont(1,2) v_neq_0_imp[of "?C t"] ct_closed[of s t] show ?case
by (intro exI[of _ t] disjCI) (auto intro: directed_towards.intros)
qed (auto simp: S⇩r_nS2) }
ultimately show ?thesis
unfolding proper_def using ct by (force simp del: v_nS v_S2 v_nS12 ct)
qed
lemma exists_proper:
obtains ct where "proper ct"
proof atomize_elim
define r where "r = rec_nat S2 (λ_ S'. {s∈S⇩r. ∃t∈S'. (s, t) ∈ E})"
then have [simp]: "r 0 = S2" "⋀n. r (Suc n) = {s∈S⇩r. ∃t∈r n. (s, t) ∈ E}"
by simp_all
{ fix s assume "s ∈ S⇩r"
then have "s ∈ directed_towards S2 {(s, t) | s t. s ∈ S⇩r ∧ (s, t) ∈ E}"
by (rule S⇩r_directed_towards_S2)
from this ‹s∈S⇩r› have "∃n. s ∈ r n"
proof induction
case (step s t)
show ?case
proof cases
assume "t ∈ S2" with step.prems step.hyps show ?thesis
by (intro exI[of _ "Suc 0"]) force
next
assume "t ∉ S2"
with step obtain n where "t ∈ r n" "t ∈ S⇩r"
by (auto elim: directed_towards.cases)
with ‹t∈S⇩r› step.hyps show ?thesis
by (intro exI[of _ "Suc n"]) force
qed
qed (simp add: S⇩r_def) }
note r = this
{ fix s assume "s ∈ S"
have "∃D∈K s. s ∈ S⇩r ⟶ (∃t∈D. ∃n. t ∈ r n ∧ (∀m. s ∈ r m ⟶ n < m))"
proof cases
assume s: "s ∈ S⇩r"
define n where "n = (LEAST n. s ∈ r n)"
then have "s ∈ r n" and n: "⋀i. i < n ⟹ s ∉ r i"
using r s by (auto intro: LeastI_ex dest: not_less_Least)
with s have "n ≠ 0"
by (intro notI) (auto simp: S⇩r_def)
then obtain n' where "n = Suc n'"
by (cases n) auto
with ‹s ∈ r n› obtain t D where "D ∈ K s" "t ∈ D" "t ∈ r n'"
by (auto simp: E_def)
with n ‹n = Suc n'› s show ?thesis
by (auto intro!: bexI[of _ D] bexI[of _ t] exI[of _ n'] simp: not_less_eq[symmetric])
qed (insert K_wf ‹s∈S›, auto) }
then obtain ct where ct: "⋀s. s ∈ S ⟹ ct s ∈ K s"
"⋀s. s ∈ S ⟹ s ∈ S⇩r ⟹ ∃t∈ct s. ∃n. t ∈ r n ∧ (∀m. s ∈ r m ⟶ n < m)"
by metis
then have *: "restrict ct S ∈ Pi⇩E S K"
by auto
moreover
{ fix s assume "s ∈ S⇩r"
then obtain n where "s ∈ r n"
by (metis r)
with ‹s ∈ S⇩r› have "s ∈ directed_towards S2 (SIGMA s : S⇩r. ct s)"
proof (induction n arbitrary: s rule: less_induct)
case (less n s)
moreover with S⇩r have "s ∈ S" by auto
ultimately obtain t m where "t ∈ ct s" "t ∈ r m" "m < n"
using ct[of s] by (auto simp: E_def)
with less.IH[of m t] ‹s ∈ S⇩r› show ?case
by (cases m) (auto intro: directed_towards.intros)
qed }
ultimately show "∃ct. proper ct"
using S⇩r S2
by (auto simp: proper_eq[OF *] subset_eq
intro!: exI[of _ "restrict ct S"]
cong: Sigma_cong)
qed
definition "l_desc X ct l s ⟷
s ∈ directed_towards S2 (SIGMA s : X. {l s}) ∧
v (simple ct s) ≤ v (simple ct (l s)) ∧
l s ∈ maximal (λs. v (simple ct s)) (ct s)"
lemma exists_l_desc:
assumes ct: "proper ct"
shows "∃l∈S⇩r → S⇩r ∪ S2. ∀s∈S⇩r. l_desc S⇩r ct l s"
proof -
have ct_closed: "⋀s t. s ∈ S ⟹ t ∈ ct s ⟹ t ∈ S"
using ct K_closed by (auto simp: proper_def PiE_iff)
have ct_Pi: "ct ∈ Pi S K"
using ct by (auto simp: proper_def)
have "finite S⇩r"
using S_finite by (auto simp: S⇩r_def)
then show ?thesis
proof (induct rule: finite_induct_select)
case (select X)
then obtain l where l: "l ∈ X → X ∪ S2" and desc: "⋀s. s ∈ X ⟹ l_desc X ct l s"
by auto
obtain x where x: "x ∈ S⇩r - X"
using ‹X ⊂ S⇩r› by auto
then have "x ∈ S"
by (auto simp: S⇩r_def)
let ?C = "simple ct"
let ?v = "λs. v (?C s)" and ?E = "λs. set_pmf (ct s)"
let ?M = "λs. maximal ?v (?E s)"
have finite_E[simp]: "⋀s. s ∈ S ⟹ finite (?E s)"
using K_closed ct by (intro finite_subset[OF _ S_finite]) (auto simp: proper_def subset_eq)
have valid_C[simp]: "⋀s. s ∈ S ⟹ ?C s ∈ valid_cfg"
using ct by (auto simp: proper_def intro!: simple_valid_cfg)
have E_ne[simp]: "⋀s. ?E s ≠ {}"
by (rule set_pmf_not_empty)
have "∃s∈S⇩r - X. ∃t∈?M s. t ∈ S2 ∪ X"
proof (rule ccontr)
assume "¬ ?thesis"
then have not_M: "⋀s. s ∈ S⇩r - X ⟹ ?M s ∩ (S2 ∪ X) = {}"
by auto
let ?S⇩m = "maximal ?v (S⇩r - X)"
have "finite (S⇩r - X)" "S⇩r - X ≠ {}"
using ‹X ⊂ S⇩r› by (auto intro!: finite_subset[OF _ S_finite] simp: S⇩r_def)
from maximal_ne[OF this] obtain s⇩m where s⇩m: "s⇩m ∈ ?S⇩m"
by force
have "∃s⇩0∈?S⇩m. ∃t∈?E s⇩0. t ∉ ?S⇩m"
proof (rule ccontr)
assume "¬ ?thesis"
then have S⇩m: "⋀s⇩0 t. s⇩0 ∈ ?S⇩m ⟹ t ∈ ?E s⇩0 ⟹ t ∈ ?S⇩m" by blast
from ‹s⇩m ∈ ?S⇩m› have [simp]: "s⇩m ∈ S" and "s⇩m ∈ S⇩r"
by (auto simp: S⇩r_def dest: maximalD1)
from ‹s⇩m ∈ ?S⇩m› have "v (?C s⇩m) = 0"
proof (coinduction arbitrary: s⇩m rule: v_eq_0_coinduct)
case (cont t s⇩m) with S1 show ?case
by (intro exI[of _ "state t"] disjCI conjI S⇩m[of s⇩m "state t"])
(auto simp: set_K_cfg)
qed (auto simp: S⇩r_def ct_Pi dest!: maximalD1)
with ‹s⇩m ∈ S⇩r› ‹proper ct› show False
by (auto simp: proper_def)
qed
then obtain s⇩0 t where "s⇩0 ∈ ?S⇩m" and t: "t ∈ ?E s⇩0" "t ∉ ?S⇩m"
by metis
with S⇩r_S1 have s⇩0: "s⇩0 ∈ S⇩r - X" and [simp]: "s⇩0 ∈ S" and "s⇩0 ∈ S1"
by (auto simp: S⇩r_def dest: maximalD1)
from ‹proper ct› ‹s⇩0 ∈ S› s⇩0 have "?v s⇩0 ≠ 0"
by (auto simp add: proper_def)
then have "0 < ?v s⇩0" by (simp add: zero_less_iff_neq_zero)
{ fix t assume "t ∈ S⇩e ∪ S2 ∪ X" "t ∈ ?E s⇩0" and "?v s⇩0 ≤ ?v t"
moreover have "t ∈ S⇩e ⟹ ?v t = 0"
by (simp add: p_eq_0_imp S⇩e_def ct_Pi)
ultimately have t: "t ∈ S2 ∪ X" "t ∈ ?E s⇩0"
using ‹0 < ?v s⇩0› by (auto simp: S⇩e_def)
have "maximal ?v (?E s⇩0 ∩ (S2 ∪ X)) ≠ {}"
using finite_E t by (intro maximal_ne) auto
moreover
{ fix x y assume x: "x ∈ S2 ∪ X" "x ∈ ?E s⇩0"
and *: "∀y∈?E s⇩0 ∩ (S2 ∪ X). ?v y ≤ ?v x" and y: "y ∈ ?E s⇩0"
with S2 ‹s⇩0 ∈ S›[THEN ct_closed] have [simp]: "x ∈ S" "y ∈ S"
by auto
have "?v y ≤ ?v x"
proof cases
assume "y ∈ S⇩r - X"
then have "?v y ≤ ?v s⇩0"
using ‹s⇩0 ∈ ?S⇩m› by (auto intro: maximalD2)
also note ‹?v s⇩0 ≤ ?v t›
also have "?v t ≤ ?v x"
using * t by auto
finally show ?thesis .
next
assume "y ∉ S⇩r - X" with y * show ?thesis
by (auto simp: S⇩r_def v_S⇩e[of "?C y"] ct_Pi)
qed }
then have "maximal ?v (?E s⇩0 ∩ (S2 ∪ X)) ⊆ maximal ?v (?E s⇩0)"
by (auto simp: maximal_def)
moreover note not_M[OF s⇩0]
ultimately have False
by (blast dest: maximalD1) }
then have less_s⇩0: "⋀t. t ∈ S⇩e ∪ S2 ∪ X ⟹ t ∈ ?E s⇩0 ⟹ ?v t < ?v s⇩0"
by (auto simp add: not_le[symmetric])
let ?K = "ct s⇩0"
have "?v s⇩0 = (∫⇧+ x. ?v x ∂?K)"
using v_S1[of "?C s⇩0"] ‹s⇩0 ∈ S1› ‹s⇩0 ∈ S›
by (auto simp add: ct_Pi intro!: nn_integral_cong_AE AE_pmfI)
also have "… < (∫⇧+x. ?v s⇩0 ∂?K)"
proof (intro nn_integral_less)
have "(∫⇧+x. ?v x ∂?K) ≤ (∫⇧+x. 1 ∂?K)"
using ct ct_closed[of s⇩0]
by (intro nn_integral_mono_AE)
(auto intro!: v_le_1 simp: AE_measure_pmf_iff proper_def ct_Pi)
then show "(∫⇧+x. ?v x ∂?K) ≠ ∞"
by (auto simp: top_unique)
have "?v t < ?v s⇩0"
proof cases
assume "t ∈ S⇩e ∪ S2 ∪ X" then show ?thesis
using less_s⇩0[of t] t by simp
next
assume "t ∉ S⇩e ∪ S2 ∪ X"
with t(1) ct_closed[of s⇩0 t] have "t ∈ S⇩r - X"
unfolding S⇩r_def by (auto simp: E_def)
with t(2) show ?thesis
using ‹s⇩0 ∈ ?S⇩m› by (auto simp: maximal_def not_le intro: less_le_trans)
qed
then show "¬ (AE x in ?K. ?v s⇩0 ≤ ?v x)"
using t by (auto simp: not_le AE_measure_pmf_iff E_def cong del: AE_cong intro!: exI[of _ "t"])
show "AE x in ?K. ?v x ≤ ?v s⇩0"
proof (subst AE_measure_pmf_iff, safe)
fix t assume t: "t ∈ ?E s⇩0"
show "?v t ≤ ?v s⇩0"
proof cases
assume "t ∈ S⇩e ∪ S2 ∪ X" then show ?thesis
using less_s⇩0[of t] t by simp
next
assume "t ∉ S⇩e ∪ S2 ∪ X" with t ‹s⇩0 ∈ ?S⇩m› ‹s⇩0 ∈ S› show ?thesis
by (elim maximalD2) (auto simp: S⇩r_def intro!: ct_closed[of _ t])
qed
qed
qed (insert ct_closed[of s⇩0], auto simp: AE_measure_pmf_iff)
also have "… = ?v s⇩0"
using ‹s⇩0 ∈ S› measure_pmf.emeasure_space_1[of "ct s⇩0"] by simp
finally show False
by simp
qed
then obtain s t where s: "s ∈ S⇩r - X" and t: "t ∈ S2 ∪ X" "t ∈ ?M s"
by auto
with S2 ‹X ⊂ S⇩r› have "s ∉ S2" and "s ∈ S ∧ s ∉ S2" and "s ∉ X"and [simp]: "t ∈ S"
by (auto simp add: S⇩r_def)
define l' where "l' = l(s := t)"
then have l'_s[simp, intro]: "l' s = t"
by simp
let ?D = "λX l. directed_towards S2 (SIGMA s : X. {l s})"
{ fix s' assume "s' ∈ ?D X l" "s' ∈ X"
from this(1) have "s' ∈ ?D (insert s X) l'"
by (rule directed_towards_mono) (auto simp: l'_def ‹s ∉ X›) }
note directed_towards_l' = this
show ?case
proof (intro bexI ballI, elim insertE)
show "s ∈ S⇩r - X" by fact
show "l' ∈ insert s X → insert s X ∪ S2"
using s t l by (auto simp: l'_def)
next
fix s' assume s': "s' ∈ X"
moreover
from desc[OF s'] have "s' ∈ ?D X l" and *: "?v s' ≤ ?v (l s')" "l s' ∈ ?M s'"
by (auto simp: l_desc_def)
moreover have "l' s' = l s'"
using ‹s' ∈ X› s by (auto simp add: l'_def)
ultimately show "l_desc (insert s X) ct l' s'"
by (auto simp: l_desc_def intro!: directed_towards_l')
next
fix s' assume "s' = s"
show "l_desc (insert s X) ct l' s'"
unfolding ‹s' = s› l_desc_def l'_s
proof (intro conjI)
show "s ∈ ?D (insert s X) l'"
proof cases
assume "t ∉ S2"
with t have "t ∈ X" by auto
with desc have "t ∈ ?D X l"
by (simp add: l_desc_def)
then show ?thesis
by (force intro: directed_towards.step[OF directed_towards_l'] ‹t ∈ X›)
qed (force intro: directed_towards.step directed_towards.start)
from ‹s ∈ S⇩r - X› S⇩r_S1 have [simp]: "s ∈ S1" "s ∈ S"
by (auto simp: S⇩r_def)
show "?v s ≤ ?v t"
using t(2)[THEN maximalD2] ct
by (auto simp add: v_S1 AE_measure_pmf_iff proper_def Pi_iff PiE_def
intro!: measure_pmf.nn_integral_le_const)
qed fact
qed
qed simp
qed
lemma F_v_memoryless:
obtains ct where "ct ∈ Pi⇩E S K" "v∘simple ct = F_sup (v∘simple ct)"
proof atomize_elim
define R where "R = {(ct(s := D), ct) | ct s D.
ct ∈ Pi⇩E S K ∧ proper ct ∧ s ∈ S⇩r ∧ D ∈ K s ∧ v (simple ct s) < (∫⇧+t. v (simple ct t) ∂D) }"
{ fix ct ct' assume ct_ct': "(ct', ct) ∈ R"
let ?v = "λs. v (simple ct s)" and ?v' = "λs. v (simple ct' s)"
from ct_ct' obtain s D where "ct ∈ Pi⇩E S K" "proper ct" and s: "s ∈ S⇩r" and D: "D ∈ K s"
and not_maximal: "?v s < (∫⇧+t. ?v t ∂D)" and ct'_eq: "ct' = ct(s := D)"
by (auto simp: R_def)
with S⇩r_S1 have ct: "ct ∈ Pi S K" and "s ∈ S" and "s ∈ S1"
by (auto simp: S⇩r_def)
then have valid_ct[simp]: "⋀s. s ∈ S ⟹ simple ct s ∈ cfg_on s"
by simp
from ct'_eq have [simp]: "ct' s = D" "⋀t. t ≠ s ⟹ ct' t = ct t"
by simp_all
from ct_ct' S⇩r have ct'_E: "ct' ∈ Pi⇩E S K"
by (auto simp: ct'_eq R_def)
from ct s D have ct': "ct' ∈ Pi S K"
by (auto simp: ct'_eq)
then have valid_ct'[simp]: "⋀s. s ∈ S ⟹ simple ct' s ∈ cfg_on s"
by simp
from exists_l_desc[OF ‹proper ct›]
obtain l where l: "l ∈ S⇩r → S⇩r ∪ S2" and "⋀s. s ∈ S⇩r ⟹ l_desc S⇩r ct l s"
by auto
then have directed_l: "⋀s. s ∈ S⇩r ⟹ s ∈ directed_towards S2 (SIGMA s:S⇩r. {l s})"
and v_l_mono: "⋀s. s ∈ S⇩r ⟹ ?v s ≤ ?v (l s)"
and l_in_Ea: "⋀s. s ∈ S⇩r ⟹ l s ∈ ct s"
by (auto simp: l_desc_def dest!: maximalD1)
let ?E = "λct. SIGMA s:S⇩r. ct s"
let ?D = "λct. directed_towards S2 (?E ct)"
have finite_E[simp]: "⋀s. s ∈ S ⟹ finite (ct' s)"
using ct' K_closed by (intro rev_finite_subset[OF S_finite]) auto
have "maximal ?v (ct' s) ≠ {}"
using ct' D ‹s∈S› finite_E[of s] by (intro maximal_ne set_pmf_not_empty) (auto simp del: finite_E)
then obtain s' where s': "s' ∈ maximal ?v (ct' s)"
by blast
with K_closed[OF ‹s ∈ S›] D have "s' ∈ S"
by (auto dest!: maximalD1)
have "s' ≠ s"
proof
assume [simp]: "s' = s"
have "?v s < (∫⇧+t. ?v t ∂D)"
by fact
also have "… ≤ (∫⇧+t. ?v s ∂D)"
using ‹s ∈ S› s' D by (intro nn_integral_mono_AE) (auto simp: AE_measure_pmf_iff intro: maximalD2)
finally show False
using measure_pmf.emeasure_space_1[of D] by (simp add: ‹s ∈ S› ct)
qed
have "p s' ≠ 0"
proof
assume "p s' = 0"
then have "?v s' = 0"
using v_le_p[of "simple ct s'"] ct ‹s' ∈ S› by (auto intro!: antisym ct)
then have "(∫⇧+t. ?v t ∂D) = 0"
using maximalD2[OF s'] by (subst nn_integral_0_iff_AE) (auto simp: ‹s∈S› D AE_measure_pmf_iff)
then have "?v s < 0"
using not_maximal by auto
then show False
using ‹s∈S› by (simp add: ct)
qed
with ‹s' ∈ S› have "s' ∈ S2 ∪ S⇩r"
by (auto simp: S⇩r_def S⇩e_def)
have l_acyclic: "(s', s) ∉ (SIGMA s:S⇩r. {l s})^+"
proof
assume "(s', s) ∈ (SIGMA s:S⇩r. {l s})^+"
then have "?v s' ≤ ?v s"
by induct (blast intro: order_trans v_l_mono)+
also have "… < (∫⇧+t. ?v t ∂D)"
using not_maximal .
also have "… ≤ (∫⇧+t. ?v s' ∂D)"
using s' by (intro nn_integral_mono_AE) (auto simp: ‹s ∈ S› D AE_measure_pmf_iff intro: maximalD2)
finally show False
using measure_pmf.emeasure_space_1[of D] by (simp add:‹s' ∈ S› ct)
qed
from ‹s' ∈ S2 ∪ S⇩r› have "s' ∈ ?D ct'"
proof
assume "s' ∈ S⇩r"
then have "l s' ∈ directed_towards S2 (SIGMA s:S⇩r. {l s})"
using l directed_l[of "l s'"] by (auto intro: directed_towards.start)
moreover from ‹s' ∈ S⇩r› have "(s', l s') ∈ (SIGMA s:S⇩r. {l s})^+"
by auto
ultimately have "l s' ∈ ?D ct'"
proof induct
case (step t t')
then have t: "t ≠ s" "t ∈ S⇩r" "t' = l t"
using l_acyclic by auto
from step have "(s', t') ∈ (SIGMA s:S⇩r. {l s})⇧+"
by (blast intro: trancl_into_trancl)
from step(2)[OF this] show ?case
by (rule directed_towards.step) (simp add: l_in_Ea t)
qed (rule directed_towards.start)
then show "s' ∈ ?D ct'"
by (rule directed_towards.step)
(simp add: l_in_Ea ‹s' ∈ S⇩r› ‹s ∈ S⇩r› ‹s' ≠ s›)
qed (rule directed_towards.start)
have proper: "proper ct'"
unfolding proper_eq[OF ct'_E]
proof
fix t assume "t ∈ S⇩r"
from directed_l[OF this] show "t ∈ ?D ct'"
proof induct
case (step t t')
show ?case
proof cases
assume "t = s"
with ‹s ∈ S⇩r› s'[THEN maximalD1] have "(t, s') ∈ ?E ct'"
by auto
with ‹s' ∈ ?D ct'› show ?thesis
by (rule directed_towards.step)
next
assume "t ≠ s"
with step have "(t, t') ∈ ?E ct'"
by (auto simp: l_in_Ea)
with step.hyps(2) show ?thesis
by (rule directed_towards.step)
qed
qed (rule directed_towards.start)
qed
have "?v ≤ ?v'"
proof (intro le_funI leI notI)
fix t' assume *: "?v' t' < ?v t'"
then have "t' ∈ S"
by (metis v_nS simple_valid_cfg_iff ct' ct order.irrefl)
define Δ where "Δ t = enn2real (?v t) - enn2real (?v' t)" for t
with * ‹t' ∈ S› have "0 < Δ t'"
by (cases "?v t'" "?v' t'" rule: ennreal2_cases) (auto simp add: ct' ct ennreal_less_iff)
{ fix t assume t: "t ∈ maximal Δ S"
with ‹t' ∈ S› have "Δ t' ≤ Δ t"
by (auto intro: maximalD2)
with ‹0 < Δ t'› have "0 < Δ t" by simp
with t have "t ∈ S⇩r"
by (auto simp add: S⇩r_def v_S⇩e ct ct' Δ_def dest!: maximalD1) }
note max_is_S⇩r = this
{ fix s assume "s ∈ S"
with v_le_1[of "simple ct' s"] v_le_1[of "simple ct s"]
have "¦Δ s¦ ≤ 1"
by (cases "?v s" "?v' s" rule: ennreal2_cases) (auto simp: Δ_def ct ct') }
note Δ_le_1[simp] = this
then have ennreal_Δ: "⋀s. s ∈ S ⟹ Δ s = ?v s - ?v' s"
by (auto simp add: Δ_def v_def T.emeasure_eq_measure ct ct' ennreal_minus)
from ‹s ∈ S› S_finite have "maximal Δ S ≠ {}"
by (intro maximal_ne) auto
then obtain t where "t ∈ maximal Δ S" by auto
from max_is_S⇩r[OF this] proper have "t ∈ ?D ct'"
unfolding proper_eq[OF ct'_E] by auto
from this ‹t ∈ maximal Δ S› show False
proof induct
case (start t)
then have "t ∈ S⇩r"
by (intro max_is_S⇩r)
with ‹t ∈ S2› show False
by (auto simp: S⇩r_def)
next
case (step t t')
then have t': "t' ∈ ct' t" and "t ∈ S⇩r" and t: "t ∈ maximal Δ S"
by (auto intro: max_is_S⇩r simp: comp_def)
then have "t' ∈ S" "t ∈ S1" "t ∈ S"
using S⇩r_S1 S1
by (auto simp: Pi_closed[OF ct'])
have "Δ t ≤ Δ t'"
proof (intro leI notI)
assume less: "Δ t' < Δ t"
have "(∫s. Δ s ∂ct' t) < (∫s. Δ t ∂ct' t)"
proof (intro measure_pmf.integral_less_AE)
show "emeasure (ct' t) {t'} ≠ 0" "{t'} ∈ sets (ct' t)"
"AE s in ct' t. s∈{t'} ⟶ Δ s ≠ Δ t"
using t' less by (auto simp add: emeasure_pmf_single_eq_zero_iff)
show "AE s in ct' t. Δ s ≤ Δ t"
using ct' ct t D
by (auto simp add: AE_measure_pmf_iff ct ‹t∈S› Pi_iff E_def Pi_closed[OF ct']
intro!: maximalD2[of t Δ] intro: Pi_closed[OF ct'] maximalD1)
show "integrable (ct' t) (λ_. Δ t)" "integrable (ct' t) Δ"
using ct ct' ‹t ∈ S› D
by (auto intro!: measure_pmf.integrable_const_bound[where B=1] Δ_le_1
simp: AE_measure_pmf_iff dest: Pi_closed)
qed
also have "… = Δ t"
using measure_pmf.prob_space[of "ct' t"] by simp
also have "Δ t ≤ (∫s. enn2real (?v s) ∂ct' t) - (∫s. enn2real (?v' s) ∂ct' t)"
proof -
have "?v t ≤ (∫⇧+s. ?v s ∂ct' t)"
proof cases
assume "t = s" with not_maximal show ?thesis by simp
next
assume "t ≠ s" with S1 ‹t∈S1› ‹t ∈ S› ct ct' show ?thesis
by (subst v_S1) (auto intro!: nn_integral_mono_AE AE_pmfI)
qed
also have "… = ennreal (∫s. enn2real (?v s) ∂ct' t)"
using ct ct' ‹t∈S›
by (intro measure_pmf.ennreal_integral_real[symmetric, where B=1])
(auto simp: AE_measure_pmf_iff one_ennreal_def[symmetric]
intro!: v_le_1 simple_valid_cfg intro: Pi_closed)
finally have "enn2real (?v t) ≤ (∫s. enn2real (?v s) ∂ct' t)"
using ct ‹t∈S› by (simp add: v_def T.emeasure_eq_measure)
moreover
{ have "?v' t = (∫⇧+s. ?v' s ∂ct' t)"
using ct ct' ‹t ∈ S› ‹t ∈ S1› S1 by (subst v_S1) (auto intro!: nn_integral_cong_AE AE_pmfI)
also have "… = ennreal (∫s. enn2real (?v' s) ∂ct' t)"
using ct' ‹t∈S›
by (intro measure_pmf.ennreal_integral_real[symmetric, where B=1])
(auto simp: AE_measure_pmf_iff one_ennreal_def[symmetric]
intro!: v_le_1 simple_valid_cfg intro: Pi_closed)
finally have "enn2real (?v' t) = (∫s. enn2real (?v' s) ∂ct' t)"
using ct' ‹t∈S› by (simp add: v_def T.emeasure_eq_measure) }
ultimately show ?thesis
using ‹t ∈ S› by (simp add: Δ_def ennreal_minus_mono)
qed
also have "… = (∫s. Δ s ∂ct' t)"
unfolding Δ_def using Pi_closed[OF ct ‹t∈S›] Pi_closed[OF ct' ‹t∈S›] ct ct'
by (intro Bochner_Integration.integral_diff[symmetric] measure_pmf.integrable_const_bound[where B=1])
(auto simp: AE_measure_pmf_iff real_v)
finally show False
by simp
qed
with t[THEN maximalD2] ‹t ∈ S› ‹t' ∈ S› have "Δ t = Δ t'"
by (auto intro: antisym)
with t ‹t' ∈ S› have "t' ∈ maximal Δ S"
by (auto simp: maximal_def)
then show ?case
by fact
qed
qed
moreover have "?v s < ?v' s"
proof -
have "?v s < (∫⇧+t. ?v t ∂D)"
by fact
also have "… ≤ (∫⇧+t. ?v' t ∂D)"
using ‹?v ≤ ?v'› ‹s∈S› D ct ct'
by (intro nn_integral_mono) (auto simp: le_fun_def)
also have "… = ?v' s"
using ‹s∈S1› S1 ct' ‹s ∈ S› by (subst (2) v_S1) (auto intro!: nn_integral_cong_AE AE_pmfI)
finally show ?thesis .
qed
ultimately have "?v < ?v'"
by (auto simp: less_le le_fun_def fun_eq_iff)
note this proper ct' }
note v_strict = this(1) and proper = this(2) and sc'_R = this(3)
have "finite (Pi⇩E S K × Pi⇩E S K)"
by (intro finite_PiE S_finite K_finite finite_SigmaI)
then have "finite R"
by (rule rev_finite_subset) (auto simp add: PiE_iff S⇩r_def R_def intro: extensional_arb)
moreover
from v_strict have "acyclic R"
by (rule acyclicI_order)
ultimately have "wf R"
by (rule finite_acyclic_wf)
from exists_proper obtain ct' where ct': "proper ct'" .
define ct where "ct = restrict ct' S"
with ct' have sc_Pi: "ct ∈ Pi S K" and "ct' ∈ Pi S K"
by (auto simp: proper_def)
then have ct: "ct ∈ {ct ∈ Pi⇩E S K. proper ct}"
using ct' directed_towards_mono[where F="SIGMA s:S⇩r. ct' s" and G="SIGMA s:S⇩r. ct s"]
apply simp
apply (subst proper_eq)
by (auto simp: ct_def proper_eq[OF properD1[OF ct']] subset_eq S⇩r_def)
show "∃ct. ct ∈ Pi⇩E S K ∧ v∘simple ct = F_sup (v∘simple ct)"
proof (rule wfE_min[OF ‹wf R› ct])
fix ct assume ct: "ct ∈ {ct ∈ Pi⇩E S K. proper ct}"
then have "ct ∈ Pi S K" "proper ct"
by (auto simp: proper_def)
assume min: "⋀ct'. (ct', ct) ∈ R ⟹ ct' ∉ {ct ∈ Pi⇩E S K. proper ct}"
let ?v = "λs. v (simple ct s)"
{ fix s assume "s ∈ S" "s ∈ S1" "s ∉ S2"
with ct have "ct s ∈ K s" "?v s ≤ integral⇧N (ct s) ?v"
by (auto simp: v_S1 PiE_def intro!: nn_integral_mono_AE AE_pmfI)
moreover
{ have "0 ≤ ?v s"
using ‹s∈S› ct by (simp add: PiE_def)
also assume v_less: "?v s < (⨆D∈K s. ∫⇧+ s. v (simple ct s) ∂measure_pmf D)"
also have "… ≤ p s"
unfolding p_S1[OF ‹s∈S1›] using ‹s∈S› ct v_le_p[OF simple_valid_cfg, OF ‹ct ∈ Pi S K›]
by (auto intro!: SUP_mono nn_integral_mono_AE bexI
simp: PiE_def AE_measure_pmf_iff set_pmf_closed)
finally have "s ∈ S⇩r"
using ‹s∈S› ‹s∉S2› by (simp add: S⇩r_def S⇩e_def)
from v_less obtain D where "D ∈ K s" "?v s < integral⇧N D ?v"
by (auto simp: less_SUP_iff)
with ct ‹s∈S› ‹s∈S⇩r› have "(ct(s:=D), ct) ∈ R" "ct(s:=D) ∈ Pi⇩E S K"
unfolding R_def by (auto simp: PiE_def extensional_def)
from proper[OF this(1)] min[OF this(1)] ct ‹D ∈ K s› ‹s∈S› this(2)
have False
by simp }
ultimately have "?v s = (⨆D∈K s. ∫⇧+ s. ?v s ∂measure_pmf D)"
by (auto intro: antisym SUP_upper2[where i="ct s"] leI)
also have "… = (⨆D∈K s. integral⇧N (measure_pmf D) (λs∈S. ?v s))"
using ‹s∈S› by (auto intro!: SUP_cong nn_integral_cong v_nS simp: ct simple_valid_cfg_iff ‹ct ∈ Pi S K›)
finally have "?v s = (⨆D∈K s. integral⇧N (measure_pmf D) (λs∈S. ?v s))" . }
then have "?v = F_sup ?v"
unfolding F_sup_def using ct
by (auto intro!: ext v_S2 simple_cfg_on v_nS v_nS12 SUP_cong nn_integral_cong
simp: PiE_def simple_valid_cfg_iff)
with ct show ?thesis
by (auto simp: comp_def)
qed
qed
lemma p_v_memoryless:
obtains ct where "ct ∈ Pi⇩E S K" "p = v∘simple ct"
proof -
obtain ct where ct_PiE: "ct ∈ Pi⇩E S K" and eq: "v∘simple ct = F_sup (v∘simple ct)"
by (rule F_v_memoryless)
then have ct: "ct ∈ Pi S K"
by (simp add: PiE_def)
have "p = v∘simple ct"
proof (rule antisym)
show "p ≤ v∘simple ct"
unfolding p_eq_lfp_F_sup by (rule lfp_lowerbound) (metis order_refl eq)
show "v∘simple ct ≤ p"
proof (rule le_funI)
fix s show "(v∘simple ct) s ≤ p s"
using v_le_p[of "simple ct s"]
by (cases "s ∈ S") (auto simp del: simp add: v_def ct)
qed
qed
with ct_PiE that show thesis by auto
qed
definition "n = (λs∈S. P_inf s (λω. (HLD S1 suntil HLD S2) (s ## ω)))"
lemma n_eq_INF_v: "s ∈ S ⟹ n s = (⨅cfg∈cfg_on s. v cfg)"
by (auto simp add: n_def v_def P_inf_def T.emeasure_eq_measure valid_cfgI intro!: INF_cong)
lemma n_le_v: "s ∈ S ⟹ cfg ∈ cfg_on s ⟹ n s ≤ v cfg"
by (subst n_eq_INF_v) (blast intro!: INF_lower)+
lemma n_eq_1_imp: "s ∈ S ⟹ cfg ∈ cfg_on s ⟹ n s = 1 ⟹ v cfg = 1"
using n_le_v[of s cfg] v_le_1[of cfg] by (auto intro: antisym valid_cfgI)
lemma n_eq_1_iff: "s ∈ S ⟹ n s = 1 ⟷ (∀cfg∈cfg_on s. v cfg = 1)"
apply rule
apply (metis n_eq_1_imp)
apply (auto simp: n_eq_INF_v intro!: INF_eqI)
done
lemma n_le_1: "s ∈ S ⟹ n s ≤ 1"
by (auto simp: n_eq_INF_v intro!: INF_lower2[OF simple_cfg_on[of arb_act]] v_le_1)
lemma n_undefined[simp]: "s ∉ S ⟹ n s = undefined"
by (simp add: n_def)
lemma n_eq_0: "s ∈ S ⟹ cfg ∈ cfg_on s ⟹ v cfg = 0 ⟹ n s = 0"
using n_le_v[of s cfg] by auto
lemma n_not_inf[simp]: "s ∈ S ⟹ n s ≠ top"
using n_le_1[of s] by (auto simp: top_unique)
lemma n_S1: "s ∈ S1 ⟹ n s = (⨅D∈K s. ∫⇧+ t. n t ∂measure_pmf D)"
using S1 S1_S2 unfolding n_def
apply auto
apply (subst P_inf_iterate)
apply (auto intro!: nn_integral_cong_AE INF_cong intro: set_pmf_closed
simp: AE_measure_pmf_iff suntil_Stream set_eq_iff)
done
lemma n_S2[simp]: "s ∈ S2 ⟹ n s = 1"
using S2 by (auto simp add: n_eq_INF_v valid_cfgI)
lemma n_nS12: "s ∈ S ⟹ s ∉ S1 ⟹ s ∉ S2 ⟹ n s = 0"
by (auto simp add: n_eq_INF_v valid_cfgI)
lemma n_pos:
assumes "P s" "s ∈ S1" "wf R"
assumes cont: "⋀s D. P s ⟹ s ∈ S1 ⟹ D ∈ K s ⟹ ∃w∈D. ((w, s) ∈ R ∧ w ∈ S1 ∧ P w) ∨ 0 < n w"
shows "0 < n s"
using ‹wf R› ‹P s› ‹s∈S1›
proof (induction s)
case (less s)
with S1 have [simp]: "s ∈ S" by auto
let ?I = "λD::'s pmf. ∫⇧+t. n t ∂D"
have "0 < Min (?I`K s)"
proof (safe intro!: Min_gr_iff [THEN iffD2])
fix D assume [simp]: "D ∈ K s"
from cont[OF ‹P s› ‹s ∈ S1› ‹D ∈ K s›]
obtain w where w: "w ∈ D" "0 < n w"
by (force intro: less.IH)
have in_S: "⋀t. t ∈ D ⟹ t ∈ S"
using set_pmf_closed[OF ‹s ∈ S› ‹D ∈ K s›] by auto
from w have "0 < pmf D w * n w"
by (simp add: pmf_positive ennreal_zero_less_mult_iff)
also have "… = (∫⇧+t. n w * indicator {w} t ∂D)"
by (subst nn_integral_cmult_indicator)
(auto simp: ac_simps emeasure_pmf_single in_S ‹w ∈ D›)
also have "… ≤ (∫⇧+t. n t ∂D)"
by (intro nn_integral_mono_AE) (auto split: split_indicator simp: AE_measure_pmf_iff in_S)
finally show "0 < (∫⇧+t. n t ∂D)" .
qed (insert K_wf K_finite ‹s∈S›, auto)
also have "… = n s"
unfolding n_S1[OF ‹s ∈ S1›]
using K_wf K_finite ‹s∈S› by (intro Min_Inf) auto
finally show "0 < n s" .
qed
definition F_inf :: "('s ⇒ ennreal) ⇒ ('s ⇒ ennreal)" where
"F_inf f = (λs∈S. if s ∈ S2 then 1 else if s ∈ S1 then (⨅D∈K s. ∫⇧+ t. f t ∂measure_pmf D) else 0)"
lemma F_inf_n: "F_inf n = n"
by (simp add: F_inf_def n_nS12 n_S1 fun_eq_iff)
lemma F_inf_nS[simp]: "s ∉ S ⟹ F_inf f s = undefined"
by (simp add: F_inf_def)
lemma mono_F_inf: "mono F_inf"
by (auto intro!: INF_superset_mono nn_integral_mono simp: mono_def F_inf_def le_fun_def)
lemma S1_nS2: "s ∈ S1 ⟹ s ∉ S2"
using S1_S2 by auto
lemma n_eq_lfp_F_inf: "n = lfp F_inf"
proof (intro antisym lfp_lowerbound le_funI)
fix s let ?I = "λD. (∫⇧+t. lfp F_inf t ∂measure_pmf D)"
define ct where "ct s = (SOME D. D ∈ K s ∧ (s ∈ S1 ⟶ lfp F_inf s = ?I D))" for s
{ fix s assume s: "s ∈ S"
then have "finite (?I ` K s)"
by (auto intro: K_finite)
with s obtain D where "D ∈ K s" "(∫⇧+t. lfp F_inf t ∂D) = Min (?I ` K s)"
by (auto simp: K_wf dest!: Min_in)
note this(2)
also have "… = (INF D ∈ K s. ?I D)"
using s K_wf by (subst Min_Inf) (auto intro: K_finite)
also have "s ∈ S1 ⟹ … = lfp F_inf s"
using s S1_S2 by (subst (3) lfp_unfold[OF mono_F_inf]) (auto simp add: F_inf_def)
finally have "∃D. D ∈ K s ∧ (s ∈ S1 ⟶ lfp F_inf s = ?I D)"
using ‹D ∈ K s› by auto
then have "ct s ∈ K s ∧ (s ∈ S1 ⟶ lfp F_inf s = ?I (ct s))"
unfolding ct_def by (rule someI_ex)
then have "ct s ∈ K s" "s ∈ S1 ⟹ lfp F_inf s = ?I (ct s)"
by auto }
note ct = this
then have Pi_ct: "ct ∈ Pi S K"
by auto
then have valid_ct[simp]: "⋀s. s ∈ S ⟹ simple ct s ∈ valid_cfg"
by simp
let ?F = "λP. HLD S2 or (HLD S1 aand nxt P)"
define P where "P s n =
emeasure (T (simple ct s)) {x∈space (T (simple ct s)). (?F ^^ n) (λx. False) (s ## x)}"
for s n
{ assume "s ∈ S"
with S1 have [simp, measurable]: "s ∈ S" by auto
then have "n s ≤ v (simple ct s)"
by (intro n_le_v) (auto intro: simple_cfg_on[OF Pi_ct])
also have "… = emeasure (T (simple ct s)) {x∈space (T (simple ct s)). lfp ?F (s ## x)}"
using S1_S2
by (simp add: v_eq[OF simple_valid_cfg[OF Pi_ct ‹s∈S›]])
(simp add: suntil_lfp space_T[symmetric, of "simple ct s"] del: space_T)
also have "… = (⨆n. P s n)" unfolding P_def
apply (rule emeasure_lfp2[where P="λM. ∃s. M = T (simple ct s)" and M="T (simple ct s)"])
apply (intro exI[of _ s] refl)
apply (auto simp: sup_continuous_def) []
apply auto []
proof safe
fix A s assume "⋀N. ∃s. N = T (simple ct s) ⟹ Measurable.pred N A"
then have "⋀s. Measurable.pred (T (simple ct s)) A"
by metis
then have "⋀s. Measurable.pred St A"
by simp
then show "Measurable.pred (T (simple ct s)) (λxs. HLD S2 xs ∨ HLD S1 xs ∧ nxt A xs)"
by simp
qed
also have "… ≤ lfp F_inf s"
proof (intro SUP_least)
fix n from ‹s∈S› show "P s n ≤ lfp F_inf s"
proof (induct n arbitrary: s)
case 0 with S1 show ?case
by (subst lfp_unfold[OF mono_F_inf]) (auto simp: P_def)
next
case (Suc n)
show ?case
proof cases
assume "s ∈ S1" with S1_S2 S1 have s[simp]: "s ∉ S2" "s ∈ S" "s ∈ S1" by auto
have "P s (Suc n) = (∫⇧+t. P t n ∂ct s)"
unfolding P_def space_T
apply (subst emeasure_Collect_T)
apply (rule measurable_compose[OF measurable_Stream[OF measurable_const measurable_ident_sets[OF refl]]])
apply (measurable, assumption)
apply (auto simp: K_cfg_def map_pmf_rep_eq nn_integral_distr
intro!: nn_integral_cong_AE AE_pmfI)
done
also have "… ≤ (∫⇧+t. lfp F_inf t ∂ct s)"
using Pi_closed[OF Pi_ct ‹s ∈ S›]
by (auto intro!: nn_integral_mono_AE Suc simp: AE_measure_pmf_iff)
also have "… = lfp F_inf s"
by (intro ct(2)[symmetric]) auto
finally show ?thesis .
next
assume "s ∉ S1" with S2 ‹s ∈ S› show ?case
using T.emeasure_space_1[of "simple ct s"]
by (subst lfp_unfold[OF mono_F_inf]) (auto simp: F_inf_def P_def)
qed
qed
qed
finally have "n s ≤ lfp F_inf s" . }
moreover have "s ∉ S ⟹ n s ≤ lfp F_inf s"
by (subst lfp_unfold[OF mono_F_inf]) (simp add: n_def F_inf_def)
ultimately show "n s ≤ lfp F_inf s"
by blast
qed (simp add: F_inf_n)
lemma real_n: "s ∈ S ⟹ ennreal (enn2real (n s)) = n s"
by (cases "n s") simp_all
lemma real_p: "s ∈ S ⟹ ennreal (enn2real (p s)) = p s"
by (cases "p s") simp_all
lemma p_ub:
fixes x
assumes "s ∈ S"
assumes solution: "⋀s D. s ∈ S1 ⟹ D ∈ K s ⟹ (∑t∈S. pmf D t * x t) ≤ x s"
assumes solution_0: "⋀s. s ∈ S ⟹ p s = 0 ⟹ x s = 0"
assumes solution_S2: "⋀s. s ∈ S2 ⟹ x s = 1"
shows "enn2real (p s) ≤ x s" (is "?y s ≤ _")
proof -
let ?p = "λs. enn2real (p s)"
from p_v_memoryless obtain sc where "sc ∈ Pi⇩E S K" and p_eq: "p = v ∘ simple sc"
by auto
then have sch: "⋀s. s ∈ S ⟹ sc s ∈ K s" and sc_Pi: "sc ∈ Pi S K"
by (auto simp: PiE_iff)
interpret sc: MC_syntax sc .
define N where "N = {s∈S. p s = 0} ∪ S2"
{ fix s assume "s ∈ S" "s ∉ N"
with p_nS12 have "s ∈ S1"
by (auto simp add: N_def) }
note N = this
have N_S: "N ⊆ S"
using S2 by (auto simp: N_def)
have finite_sc[intro]: "s ∈ S ⟹ finite (sc s)" for s
using ‹sc ∈ Pi⇩E S K› by (auto simp: PiE_iff intro: set_pmf_finite)
show ?thesis
proof cases
assume "s ∈ S - N"
then show ?thesis
proof (rule mono_les)
show "(⋃x∈S - N. set_pmf (sc x)) ⊆ S - N ∪ N"
using Pi_closed[OF sc_Pi] by auto
show "finite ((λs. ?p s - x s) ` (S - N ∪ N))"
using N_S by (intro finite_imageI finite_subset[OF _ S_finite]) auto
next
fix s assume "s ∈ N" then show "?p s ≤ x s"
by (auto simp: N_def solution_S2 solution_0)
next
fix s assume s: "s ∈ S - N"
then show "integrable (sc s) x" "integrable (sc s) ?p"
by (auto intro!: integrable_measure_pmf_finite set_pmf_finite sch)
from s have "s ∈ S1" "s ∈ S"
using p_nS12[of s] by (auto simp: N_def)
then show "?p s ≤ (∫ t. ?p t ∂sc s) + 0"
unfolding p_eq using real_v_integral_eq[of "simple sc s"]
by (auto simp add: v_S1 sc_Pi intro!: integral_mono_AE integrable_measure_pmf_finite AE_pmfI)
show "(∫ t. x t ∂sc s) + 0 ≤ x s"
using solution[OF ‹s ∈ S1› sch[OF ‹s ∈ S›]]
by (subst integral_measure_pmf[where A=S])
(auto intro: S_finite Pi_closed[OF sc_Pi] ‹s ∈ S› simp: ac_simps)
define X where "X = (SIGMA x:UNIV. sc x)"
show "∃t∈N. (s, t) ∈ X⇧*"
proof (rule ccontr)
assume "¬ ?thesis"
then have *: "∀t∈N. (s, t) ∉ X⇧*"
by auto
with ‹s∈S› have "v (simple sc s) = 0"
proof (coinduction arbitrary: s rule: v_eq_0_coinduct)
case (valid t) with sch show ?case
by auto
next
case (nS2 s) then show ?case
by (auto simp: N_def)
next
case (cont cfg s)
then have "(s, state cfg) ∈ X⇧*"
by (auto simp: X_def set_K_cfg)
with cont show ?case
by (auto simp: set_K_cfg intro!: exI intro: Pi_closed[OF sc_Pi])
(blast intro: rtrancl_trans)
qed
then have "p s = 0"
unfolding p_eq by simp
with ‹s∈S› have "s∈N"
by (auto simp: N_def)
with * show False
by auto
qed
qed
next
assume "s ∉ S - N" with ‹s ∈ S› show "?p s ≤ x s"
by (auto simp: N_def solution_0 solution_S2)
qed
qed
lemma n_lb:
fixes x
assumes "s ∈ S"
assumes solution: "⋀s D. s ∈ S1 ⟹ D ∈ K s ⟹ x s ≤ (∑t∈S. pmf D t * x t)"
assumes solution_n0: "⋀s. s ∈ S ⟹ n s = 0 ⟹ x s = 0"
assumes solution_S2: "⋀s. s ∈ S2 ⟹ x s = 1"
shows "x s ≤ enn2real (n s)" (is "_ ≤ ?y s")
proof -
let ?I = "λD::'s pmf. ∫⇧+x. n x ∂D"
{ fix s assume "s ∈ S1"
with S1 S1_S2 have "n s = (⨅D∈K s. ?I D)"
by (subst n_eq_lfp_F_inf, subst lfp_unfold[OF mono_F_inf])
(auto simp add: F_inf_def n_eq_lfp_F_inf)
moreover have "(⨅D∈K s. ∫⇧+x. n x ∂measure_pmf D) = Min (?I`K s)"
using ‹s ∈ S1› S1 K_wf
by (intro cInf_eq_Min finite_imageI K_finite) auto
moreover have "Min (?I`K s) ∈ ?I`K s"
using ‹s ∈ S1› S1 K_wf by (intro Min_in finite_imageI K_finite) auto
ultimately have "∃D∈K s. (∫⇧+x. n x ∂D) = n s"
by auto }
then have "⋀s. s ∈ S ⟹ ∃D∈K s. s ∈ S1 ⟶ (∫⇧+x. n x ∂D) = n s"
using K_wf by auto
then obtain sc where sch: "⋀s. s ∈ S ⟹ sc s ∈ K s"
and n_sc: "⋀s. s ∈ S1 ⟹ (∫⇧+x. n x ∂sc s) = n s"
by (metis S1 subsetD)
then have sc_Pi: "sc ∈ Pi S K"
by auto
define N where "N = {s∈S. n s = 0} ∪ S2"
with S2 have N_S: "N ⊆ S"
by auto
{ fix s assume "s ∈ S" "s ∉ N"
with n_nS12 have "s ∈ S1"
by (auto simp add: N_def) }
note N = this
let ?n = "λs. enn2real (n s)"
show ?thesis
proof cases
assume "s ∈ S - N"
then show ?thesis
proof (rule mono_les)
show "(⋃x∈S - N. set_pmf (sc x)) ⊆ S - N ∪ N"
using Pi_closed[OF sc_Pi] by auto
show "finite ((λs. x s - ?n s) ` (S - N ∪ N))"
using N_S by (intro finite_imageI finite_subset[OF _ S_finite]) auto
next
fix s assume "s ∈ N" then show "x s ≤ ?n s"
by (auto simp: N_def solution_S2 solution_n0)
next
fix s assume s: "s ∈ S - N"
then show "integrable (sc s) x" "integrable (sc s) ?n"
by (auto intro!: integrable_measure_pmf_finite set_pmf_finite sch)
from s have "s ∈ S1" "s ∈ S"
using n_nS12[of s] by (auto simp: N_def)
then have "(∫ t. ?n t ∂sc s) = ?n s"
apply (subst n_sc[symmetric, of s])
apply simp_all
apply (subst integral_eq_nn_integral)
apply (auto simp: Pi_closed[OF sc_Pi] AE_measure_pmf_iff
intro!: arg_cong[where f=enn2real] nn_integral_cong_AE real_n)
done
then show "(∫ t. ?n t ∂sc s) + 0 ≤ ?n s"
by simp
show "x s ≤ (∫ t. x t ∂sc s) + 0"
using solution[OF ‹s ∈ S1› sch[OF ‹s ∈ S›]]
by (subst integral_measure_pmf[where A=S])
(auto intro: S_finite Pi_closed[OF sc_Pi] ‹s ∈ S› simp: ac_simps)
define X where "X = (SIGMA x:UNIV. sc x)"
show "∃t∈N. (s, t) ∈ X⇧*"
proof (rule ccontr)
assume "¬ ?thesis"
then have *: "∀t∈N. (s, t) ∉ X⇧*"
by auto
with ‹s∈S› have "v (simple sc s) = 0"
proof (coinduction arbitrary: s rule: v_eq_0_coinduct)
case (valid t) with sch show ?case
by auto
next
case (nS2 s) then show ?case
by (auto simp: N_def)
next
case (cont cfg s)
then have "(s, state cfg) ∈ X⇧*"
by (auto simp: X_def set_K_cfg)
with cont show ?case
by (auto simp: set_K_cfg intro!: exI intro: Pi_closed[OF sc_Pi])
(blast intro: rtrancl_trans)
qed
from n_eq_0[OF ‹s ∈ S› simple_cfg_on this] have "n s = 0"
by (auto simp: sc_Pi)
with ‹s∈S› have "s∈N"
by (auto simp: N_def)
with * show False
by auto
qed
qed
next
assume "s ∉ S - N" with ‹s ∈ S› show "x s ≤ ?n s"
by (auto simp: N_def solution_n0 solution_S2)
qed
qed
end
end