src/HOL/Probability/Measurable.thy
 changeset 56021 e0c9d76c2a6d parent 53043 8cbfbeb566a4 child 56045 1ca060139a59
```     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
```