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 (* This proof should work automatically *) 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) (* This proof should work automatically *) 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 <