src/HOL/Probability/Measurable.thy
author hoelzl
Tue May 20 19:24:39 2014 +0200 (2014-05-20)
changeset 57025 e7fd64f82876
parent 56993 e5366291d6aa
child 58965 a62cdcc5344b
permissions -rw-r--r--
add various lemmas
     1 (*  Title:      HOL/Probability/Measurable.thy
     2     Author:     Johannes Hölzl <hoelzl@in.tum.de>
     3 *)
     4 theory Measurable
     5   imports
     6     Sigma_Algebra
     7     "~~/src/HOL/Library/Order_Continuity"
     8 begin
     9 
    10 hide_const (open) Order_Continuity.continuous
    11 
    12 subsection {* Measurability prover *}
    13 
    14 lemma (in algebra) sets_Collect_finite_All:
    15   assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
    16   shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
    17 proof -
    18   have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
    19     by auto
    20   with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
    21 qed
    22 
    23 abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
    24 
    25 lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
    26 proof
    27   assume "pred M P"
    28   then have "P -` {True} \<inter> space M \<in> sets M"
    29     by (auto simp: measurable_count_space_eq2)
    30   also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
    31   finally show "{x\<in>space M. P x} \<in> sets M" .
    32 next
    33   assume P: "{x\<in>space M. P x} \<in> sets M"
    34   moreover
    35   { fix X
    36     have "X \<in> Pow (UNIV :: bool set)" by simp
    37     then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
    38       unfolding UNIV_bool Pow_insert Pow_empty by auto
    39     then have "P -` X \<inter> space M \<in> sets M"
    40       by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
    41   then show "pred M P"
    42     by (auto simp: measurable_def)
    43 qed
    44 
    45 lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"
    46   by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
    47 
    48 lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
    49   by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
    50 
    51 ML_file "measurable.ML"
    52 
    53 attribute_setup measurable = {*
    54   Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
    55     Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
    56     (false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm))
    57 *} "declaration of measurability theorems"
    58 
    59 attribute_setup measurable_dest = {*
    60   Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest))
    61 *} "add dest rule for measurability prover"
    62 
    63 attribute_setup measurable_app = {*
    64   Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app))
    65 *} "add application rule for measurability prover"
    66 
    67 method_setup measurable = {*
    68   Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts)))
    69 *} "measurability prover"
    70 
    71 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    72 
    73 declare
    74   measurable_compose_rev[measurable_dest]
    75   pred_sets1[measurable_dest]
    76   pred_sets2[measurable_dest]
    77   sets.sets_into_space[measurable_dest]
    78 
    79 declare
    80   sets.top[measurable]
    81   sets.empty_sets[measurable (raw)]
    82   sets.Un[measurable (raw)]
    83   sets.Diff[measurable (raw)]
    84 
    85 declare
    86   measurable_count_space[measurable (raw)]
    87   measurable_ident[measurable (raw)]
    88   measurable_ident_sets[measurable (raw)]
    89   measurable_const[measurable (raw)]
    90   measurable_If[measurable (raw)]
    91   measurable_comp[measurable (raw)]
    92   measurable_sets[measurable (raw)]
    93 
    94 lemma predE[measurable (raw)]: 
    95   "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
    96   unfolding pred_def .
    97 
    98 lemma pred_intros_imp'[measurable (raw)]:
    99   "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
   100   by (cases K) auto
   101 
   102 lemma pred_intros_conj1'[measurable (raw)]:
   103   "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
   104   by (cases K) auto
   105 
   106 lemma pred_intros_conj2'[measurable (raw)]:
   107   "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
   108   by (cases K) auto
   109 
   110 lemma pred_intros_disj1'[measurable (raw)]:
   111   "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
   112   by (cases K) auto
   113 
   114 lemma pred_intros_disj2'[measurable (raw)]:
   115   "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
   116   by (cases K) auto
   117 
   118 lemma pred_intros_logic[measurable (raw)]:
   119   "pred M (\<lambda>x. x \<in> space M)"
   120   "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
   121   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
   122   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
   123   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
   124   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
   125   "pred M (\<lambda>x. f x \<in> UNIV)"
   126   "pred M (\<lambda>x. f x \<in> {})"
   127   "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
   128   "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
   129   "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
   130   "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
   131   "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
   132   "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
   133   by (auto simp: iff_conv_conj_imp pred_def)
   134 
   135 lemma pred_intros_countable[measurable (raw)]:
   136   fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
   137   shows 
   138     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
   139     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
   140   by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
   141 
   142 lemma pred_intros_countable_bounded[measurable (raw)]:
   143   fixes X :: "'i :: countable set"
   144   shows 
   145     "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"
   146     "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
   147     "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
   148     "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
   149   by (auto simp: Bex_def Ball_def)
   150 
   151 lemma pred_intros_finite[measurable (raw)]:
   152   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
   153   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
   154   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
   155   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
   156   by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
   157 
   158 lemma countable_Un_Int[measurable (raw)]:
   159   "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
   160   "I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
   161   by auto
   162 
   163 declare
   164   finite_UN[measurable (raw)]
   165   finite_INT[measurable (raw)]
   166 
   167 lemma sets_Int_pred[measurable (raw)]:
   168   assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
   169   shows "A \<inter> B \<in> sets M"
   170 proof -
   171   have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
   172   also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
   173     using space by auto
   174   finally show ?thesis .
   175 qed
   176 
   177 lemma [measurable (raw generic)]:
   178   assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
   179   shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
   180     and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
   181 proof -
   182   show "pred M (\<lambda>x. f x = c)"
   183   proof cases
   184     assume "c \<in> space N"
   185     with measurable_sets[OF f c] show ?thesis
   186       by (auto simp: Int_def conj_commute pred_def)
   187   next
   188     assume "c \<notin> space N"
   189     with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
   190     then show ?thesis by (auto simp: pred_def cong: conj_cong)
   191   qed
   192   then show "pred M (\<lambda>x. c = f x)"
   193     by (simp add: eq_commute)
   194 qed
   195 
   196 lemma pred_le_const[measurable (raw generic)]:
   197   assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
   198   using measurable_sets[OF f c]
   199   by (auto simp: Int_def conj_commute eq_commute pred_def)
   200 
   201 lemma pred_const_le[measurable (raw generic)]:
   202   assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
   203   using measurable_sets[OF f c]
   204   by (auto simp: Int_def conj_commute eq_commute pred_def)
   205 
   206 lemma pred_less_const[measurable (raw generic)]:
   207   assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
   208   using measurable_sets[OF f c]
   209   by (auto simp: Int_def conj_commute eq_commute pred_def)
   210 
   211 lemma pred_const_less[measurable (raw generic)]:
   212   assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
   213   using measurable_sets[OF f c]
   214   by (auto simp: Int_def conj_commute eq_commute pred_def)
   215 
   216 declare
   217   sets.Int[measurable (raw)]
   218 
   219 lemma pred_in_If[measurable (raw)]:
   220   "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
   221     pred M (\<lambda>x. x \<in> (if P then A x else B x))"
   222   by auto
   223 
   224 lemma sets_range[measurable_dest]:
   225   "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
   226   by auto
   227 
   228 lemma pred_sets_range[measurable_dest]:
   229   "A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
   230   using pred_sets2[OF sets_range] by auto
   231 
   232 lemma sets_All[measurable_dest]:
   233   "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
   234   by auto
   235 
   236 lemma pred_sets_All[measurable_dest]:
   237   "\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
   238   using pred_sets2[OF sets_All, of A N f] by auto
   239 
   240 lemma sets_Ball[measurable_dest]:
   241   "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
   242   by auto
   243 
   244 lemma pred_sets_Ball[measurable_dest]:
   245   "\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
   246   using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
   247 
   248 lemma measurable_finite[measurable (raw)]:
   249   fixes S :: "'a \<Rightarrow> nat set"
   250   assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
   251   shows "pred M (\<lambda>x. finite (S x))"
   252   unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
   253 
   254 lemma measurable_Least[measurable]:
   255   assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
   256   shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
   257   unfolding measurable_def by (safe intro!: sets_Least) simp_all
   258 
   259 lemma measurable_Max_nat[measurable (raw)]: 
   260   fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool"
   261   assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
   262   shows "(\<lambda>x. Max {i. P i x}) \<in> measurable M (count_space UNIV)"
   263   unfolding measurable_count_space_eq2_countable
   264 proof safe
   265   fix n
   266 
   267   { fix x assume "\<forall>i. \<exists>n\<ge>i. P n x"
   268     then have "infinite {i. P i x}"
   269       unfolding infinite_nat_iff_unbounded_le by auto
   270     then have "Max {i. P i x} = the None"
   271       by (rule Max.infinite) }
   272   note 1 = this
   273 
   274   { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x"
   275     then have "finite {i. P i x}"
   276       by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded)
   277     with `P i x` have "P (Max {i. P i x}) x" "i \<le> Max {i. P i x}" "finite {i. P i x}"
   278       using Max_in[of "{i. P i x}"] by auto }
   279   note 2 = this
   280 
   281   have "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Max {i. P i x} = n}"
   282     by auto
   283   also have "\<dots> = 
   284     {x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else 
   285       if (\<exists>i. P i x) then P n x \<and> (\<forall>i>n. \<not> P i x)
   286       else Max {} = n}"
   287     by (intro arg_cong[where f=Collect] ext conj_cong)
   288        (auto simp add: 1 2 not_le[symmetric] intro!: Max_eqI)
   289   also have "\<dots> \<in> sets M"
   290     by measurable
   291   finally show "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M \<in> sets M" .
   292 qed simp
   293 
   294 lemma measurable_Min_nat[measurable (raw)]: 
   295   fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool"
   296   assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
   297   shows "(\<lambda>x. Min {i. P i x}) \<in> measurable M (count_space UNIV)"
   298   unfolding measurable_count_space_eq2_countable
   299 proof safe
   300   fix n
   301 
   302   { fix x assume "\<forall>i. \<exists>n\<ge>i. P n x"
   303     then have "infinite {i. P i x}"
   304       unfolding infinite_nat_iff_unbounded_le by auto
   305     then have "Min {i. P i x} = the None"
   306       by (rule Min.infinite) }
   307   note 1 = this
   308 
   309   { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x"
   310     then have "finite {i. P i x}"
   311       by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded)
   312     with `P i x` have "P (Min {i. P i x}) x" "Min {i. P i x} \<le> i" "finite {i. P i x}"
   313       using Min_in[of "{i. P i x}"] by auto }
   314   note 2 = this
   315 
   316   have "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Min {i. P i x} = n}"
   317     by auto
   318   also have "\<dots> = 
   319     {x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else 
   320       if (\<exists>i. P i x) then P n x \<and> (\<forall>i<n. \<not> P i x)
   321       else Min {} = n}"
   322     by (intro arg_cong[where f=Collect] ext conj_cong)
   323        (auto simp add: 1 2 not_le[symmetric] intro!: Min_eqI)
   324   also have "\<dots> \<in> sets M"
   325     by measurable
   326   finally show "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M \<in> sets M" .
   327 qed simp
   328 
   329 lemma measurable_count_space_insert[measurable (raw)]:
   330   "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
   331   by simp
   332 
   333 lemma measurable_card[measurable]:
   334   fixes S :: "'a \<Rightarrow> nat set"
   335   assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
   336   shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)"
   337   unfolding measurable_count_space_eq2_countable
   338 proof safe
   339   fix n show "(\<lambda>x. card (S x)) -` {n} \<inter> space M \<in> sets M"
   340   proof (cases n)
   341     case 0
   342     then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M = {x\<in>space M. infinite (S x) \<or> (\<forall>i. i \<notin> S x)}"
   343       by auto
   344     also have "\<dots> \<in> sets M"
   345       by measurable
   346     finally show ?thesis .
   347   next
   348     case (Suc i)
   349     then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M =
   350       (\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})"
   351       unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
   352     also have "\<dots> \<in> sets M"
   353       by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto
   354     finally show ?thesis .
   355   qed
   356 qed rule
   357 
   358 subsection {* Measurability for (co)inductive predicates *}
   359 
   360 lemma measurable_lfp:
   361   assumes "Order_Continuity.continuous F"
   362   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
   363   shows "pred M (lfp F)"
   364 proof -
   365   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
   366       by (induct i) (auto intro!: *) }
   367   then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
   368     by measurable
   369   also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
   370     by (auto simp add: bot_fun_def)
   371   also have "\<dots> = lfp F"
   372     by (rule continuous_lfp[symmetric]) fact
   373   finally show ?thesis .
   374 qed
   375 
   376 lemma measurable_gfp:
   377   assumes "Order_Continuity.down_continuous F"
   378   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
   379   shows "pred M (gfp F)"
   380 proof -
   381   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
   382       by (induct i) (auto intro!: *) }
   383   then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
   384     by measurable
   385   also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
   386     by (auto simp add: top_fun_def)
   387   also have "\<dots> = gfp F"
   388     by (rule down_continuous_gfp[symmetric]) fact
   389   finally show ?thesis .
   390 qed
   391 
   392 hide_const (open) pred
   393 
   394 end