src/HOL/Probability/Measurable.thy
author hoelzl
Mon Mar 10 20:16:13 2014 +0100 (2014-03-10)
changeset 56021 e0c9d76c2a6d
parent 53043 8cbfbeb566a4
child 56045 1ca060139a59
permissions -rw-r--r--
add measurability rule for (co)inductive predicates
     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_count_space_insert[measurable (raw)]:
   260   "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
   261   by simp
   262 
   263 subsection {* Measurability for (co)inductive predicates *}
   264 
   265 lemma measurable_lfp:
   266   assumes "P = lfp F"
   267   assumes "Order_Continuity.continuous F"
   268   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
   269   shows "pred M P"
   270 proof -
   271   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
   272       by (induct i) (auto intro!: *) }
   273   then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
   274     by measurable
   275   also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
   276     by (auto simp add: bot_fun_def)
   277   also have "\<dots> = P"
   278     unfolding `P = lfp F` by (rule continuous_lfp[symmetric]) fact
   279   finally show ?thesis .
   280 qed
   281 
   282 lemma measurable_gfp:
   283   assumes "P = gfp F"
   284   assumes "Order_Continuity.down_continuous F"
   285   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
   286   shows "pred M P"
   287 proof -
   288   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
   289       by (induct i) (auto intro!: *) }
   290   then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
   291     by measurable
   292   also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
   293     by (auto simp add: top_fun_def)
   294   also have "\<dots> = P"
   295     unfolding `P = gfp F` by (rule down_continuous_gfp[symmetric]) fact
   296   finally show ?thesis .
   297 qed
   298 
   299 hide_const (open) pred
   300 
   301 end