add measurability rule for (co)inductive predicates
authorhoelzl
Mon Mar 10 20:16:13 2014 +0100 (2014-03-10)
changeset 56021e0c9d76c2a6d
parent 56020 f92479477c52
child 56044 f78b4c3e8e84
add measurability rule for (co)inductive predicates
src/HOL/Probability/Measurable.thy
     1.1 --- a/src/HOL/Probability/Measurable.thy	Mon Mar 10 20:04:40 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Mon Mar 10 20:16:13 2014 +0100
     1.3 @@ -2,9 +2,13 @@
     1.4      Author:     Johannes Hölzl <hoelzl@in.tum.de>
     1.5  *)
     1.6  theory Measurable
     1.7 -  imports Sigma_Algebra
     1.8 +  imports
     1.9 +    Sigma_Algebra
    1.10 +    "~~/src/HOL/Library/Order_Continuity"
    1.11  begin
    1.12  
    1.13 +hide_const (open) Order_Continuity.continuous
    1.14 +
    1.15  subsection {* Measurability prover *}
    1.16  
    1.17  lemma (in algebra) sets_Collect_finite_All:
    1.18 @@ -256,6 +260,42 @@
    1.19    "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
    1.20    by simp
    1.21  
    1.22 +subsection {* Measurability for (co)inductive predicates *}
    1.23 +
    1.24 +lemma measurable_lfp:
    1.25 +  assumes "P = lfp F"
    1.26 +  assumes "Order_Continuity.continuous F"
    1.27 +  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
    1.28 +  shows "pred M P"
    1.29 +proof -
    1.30 +  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
    1.31 +      by (induct i) (auto intro!: *) }
    1.32 +  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
    1.33 +    by measurable
    1.34 +  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
    1.35 +    by (auto simp add: bot_fun_def)
    1.36 +  also have "\<dots> = P"
    1.37 +    unfolding `P = lfp F` by (rule continuous_lfp[symmetric]) fact
    1.38 +  finally show ?thesis .
    1.39 +qed
    1.40 +
    1.41 +lemma measurable_gfp:
    1.42 +  assumes "P = gfp F"
    1.43 +  assumes "Order_Continuity.down_continuous F"
    1.44 +  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
    1.45 +  shows "pred M P"
    1.46 +proof -
    1.47 +  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
    1.48 +      by (induct i) (auto intro!: *) }
    1.49 +  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
    1.50 +    by measurable
    1.51 +  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
    1.52 +    by (auto simp add: top_fun_def)
    1.53 +  also have "\<dots> = P"
    1.54 +    unfolding `P = gfp F` by (rule down_continuous_gfp[symmetric]) fact
    1.55 +  finally show ?thesis .
    1.56 +qed
    1.57 +
    1.58  hide_const (open) pred
    1.59  
    1.60  end