# HG changeset patch
# User hoelzl
# Date 1394478973 -3600
# Node ID e0c9d76c2a6de8028e96f07aee21fc0cc3698151
# Parent  f92479477c52613cb6d8e68b3c9ceaf40f680913
add measurability rule for (co)inductive predicates

diff -r f92479477c52 -r e0c9d76c2a6d src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Mon Mar 10 20:04:40 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy	Mon Mar 10 20:16:13 2014 +0100
@@ -2,9 +2,13 @@
     Author:     Johannes Hölzl <hoelzl@in.tum.de>
 *)
 theory Measurable
-  imports Sigma_Algebra
+  imports
+    Sigma_Algebra
+    "~~/src/HOL/Library/Order_Continuity"
 begin
 
+hide_const (open) Order_Continuity.continuous
+
 subsection {* Measurability prover *}
 
 lemma (in algebra) sets_Collect_finite_All:
@@ -256,6 +260,42 @@
   "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
   by simp
 
+subsection {* Measurability for (co)inductive predicates *}
+
+lemma measurable_lfp:
+  assumes "P = lfp F"
+  assumes "Order_Continuity.continuous F"
+  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
+  shows "pred M P"
+proof -
+  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
+      by (induct i) (auto intro!: *) }
+  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
+    by measurable
+  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
+    by (auto simp add: bot_fun_def)
+  also have "\<dots> = P"
+    unfolding `P = lfp F` by (rule continuous_lfp[symmetric]) fact
+  finally show ?thesis .
+qed
+
+lemma measurable_gfp:
+  assumes "P = gfp F"
+  assumes "Order_Continuity.down_continuous F"
+  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
+  shows "pred M P"
+proof -
+  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
+      by (induct i) (auto intro!: *) }
+  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
+    by measurable
+  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
+    by (auto simp add: top_fun_def)
+  also have "\<dots> = P"
+    unfolding `P = gfp F` by (rule down_continuous_gfp[symmetric]) fact
+  finally show ?thesis .
+qed
+
 hide_const (open) pred
 
 end