src/HOL/Probability/Sigma_Algebra.thy
changeset 50002 ce0d316b5b44
parent 49834 b27bbb021df1
child 50003 8c213922ed49
     1.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:00:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:40 2012 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4    with assms show ?thesis by auto
     1.5  qed
     1.6  
     1.7 -lemma (in semiring_of_sets) sets_Collect_finite_All:
     1.8 +lemma (in semiring_of_sets) sets_Collect_finite_All':
     1.9    assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
    1.10    shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
    1.11  proof -
    1.12 @@ -1209,6 +1209,15 @@
    1.13    "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
    1.14     unfolding measurable_def by auto
    1.15  
    1.16 +lemma measurable_sets_Collect:
    1.17 +  assumes f: "f \<in> measurable M N" and P: "{x\<in>space N. P x} \<in> sets N" shows "{x\<in>space M. P (f x)} \<in> sets M"
    1.18 +proof -
    1.19 +  have "f -` {x \<in> space N. P x} \<inter> space M = {x\<in>space M. P (f x)}"
    1.20 +    using measurable_space[OF f] by auto
    1.21 +  with measurable_sets[OF f P] show ?thesis
    1.22 +    by simp
    1.23 +qed
    1.24 +
    1.25  lemma measurable_sigma_sets:
    1.26    assumes B: "sets N = sigma_sets \<Omega> A" "A \<subseteq> Pow \<Omega>"
    1.27        and f: "f \<in> space M \<rightarrow> \<Omega>"
    1.28 @@ -1302,6 +1311,9 @@
    1.29  lemma measurable_ident[intro, simp]: "id \<in> measurable M M"
    1.30    by (auto simp add: measurable_def)
    1.31  
    1.32 +lemma measurable_ident'[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
    1.33 +  by (auto simp add: measurable_def)
    1.34 +
    1.35  lemma measurable_comp[intro]:
    1.36    fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
    1.37    shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
    1.38 @@ -1314,7 +1326,7 @@
    1.39    "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
    1.40    using measurable_comp[of f M N g L] by (simp add: comp_def)
    1.41  
    1.42 -lemma measurable_Least:
    1.43 +lemma sets_Least:
    1.44    assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
    1.45    shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
    1.46  proof -
    1.47 @@ -1371,6 +1383,368 @@
    1.48      measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
    1.49    using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
    1.50  
    1.51 +section {* Counting space *}
    1.52 +
    1.53 +definition count_space :: "'a set \<Rightarrow> 'a measure" where
    1.54 +  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
    1.55 +
    1.56 +lemma 
    1.57 +  shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
    1.58 +    and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
    1.59 +  using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
    1.60 +  by (auto simp: count_space_def)
    1.61 +
    1.62 +lemma measurable_count_space_eq1[simp]:
    1.63 +  "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
    1.64 + unfolding measurable_def by simp
    1.65 +
    1.66 +lemma measurable_count_space_eq2:
    1.67 +  assumes "finite A"
    1.68 +  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
    1.69 +proof -
    1.70 +  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
    1.71 +    with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
    1.72 +      by (auto dest: finite_subset)
    1.73 +    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
    1.74 +    ultimately have "f -` X \<inter> space M \<in> sets M"
    1.75 +      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
    1.76 +  then show ?thesis
    1.77 +    unfolding measurable_def by auto
    1.78 +qed
    1.79 +
    1.80 +lemma measurable_compose_countable:
    1.81 +  assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
    1.82 +  shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
    1.83 +  unfolding measurable_def
    1.84 +proof safe
    1.85 +  fix x assume "x \<in> space M" then show "f (g x) x \<in> space N"
    1.86 +    using f[THEN measurable_space] g[THEN measurable_space] by auto
    1.87 +next
    1.88 +  fix A assume A: "A \<in> sets N"
    1.89 +  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
    1.90 +    by auto
    1.91 +  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
    1.92 +    by (auto intro!: countable_UN measurable_sets)
    1.93 +  finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
    1.94 +qed
    1.95 +
    1.96 +subsection {* Measurable method *}
    1.97 +
    1.98 +lemma (in algebra) sets_Collect_finite_All:
    1.99 +  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
   1.100 +  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
   1.101 +proof -
   1.102 +  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})"
   1.103 +    by auto
   1.104 +  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
   1.105 +qed
   1.106 +
   1.107 +abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
   1.108 +
   1.109 +lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
   1.110 +proof
   1.111 +  assume "pred M P"
   1.112 +  then have "P -` {True} \<inter> space M \<in> sets M"
   1.113 +    by (auto simp: measurable_count_space_eq2)
   1.114 +  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
   1.115 +  finally show "{x\<in>space M. P x} \<in> sets M" .
   1.116 +next
   1.117 +  assume P: "{x\<in>space M. P x} \<in> sets M"
   1.118 +  moreover
   1.119 +  { fix X
   1.120 +    have "X \<in> Pow (UNIV :: bool set)" by simp
   1.121 +    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> {})}"
   1.122 +      unfolding UNIV_bool Pow_insert Pow_empty by auto
   1.123 +    then have "P -` X \<inter> space M \<in> sets M"
   1.124 +      by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
   1.125 +  then show "pred M P"
   1.126 +    by (auto simp: measurable_def)
   1.127 +qed
   1.128 +
   1.129 +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))"
   1.130 +  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
   1.131 +
   1.132 +lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
   1.133 +  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
   1.134 +
   1.135 +lemma measurable_count_space_const:
   1.136 +  "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   1.137 +  by auto
   1.138 +
   1.139 +lemma measurable_count_space:
   1.140 +  "f \<in> measurable (count_space A) (count_space UNIV)"
   1.141 +  by simp
   1.142 +
   1.143 +lemma measurable_compose_rev:
   1.144 +  assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L"
   1.145 +  shows "(\<lambda>x. f (g x)) \<in> measurable M N"
   1.146 +  using measurable_compose[OF g f] .
   1.147 +
   1.148 +ML {*
   1.149 +
   1.150 +structure Measurable =
   1.151 +struct
   1.152 +
   1.153 +datatype level = Concrete | Generic;
   1.154 +
   1.155 +structure Data = Generic_Data
   1.156 +(
   1.157 +  type T = thm list * thm list;
   1.158 +  val empty = ([], []);
   1.159 +  val extend = I;
   1.160 +  val merge = fn ((a, b), (c, d)) => (a @ c, b @ d);
   1.161 +);
   1.162 +
   1.163 +val debug =
   1.164 +  Attrib.setup_config_bool @{binding measurable_debug} (K false)
   1.165 +
   1.166 +val backtrack =
   1.167 +  Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
   1.168 +
   1.169 +fun get lv = (case lv of Concrete => fst | Generic => snd) o Data.get o Context.Proof; 
   1.170 +fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
   1.171 +
   1.172 +fun update f lv = Data.map (case lv of Concrete => apfst f | Generic => apsnd f);
   1.173 +fun add thms' = update (fn thms => thms @ thms');
   1.174 +
   1.175 +fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
   1.176 +
   1.177 +fun is_too_generic thm =
   1.178 +  let 
   1.179 +    val concl = concl_of thm
   1.180 +    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
   1.181 +  in is_Var (head_of concl') end
   1.182 +
   1.183 +fun import_theorem thm = if is_too_generic thm then [] else
   1.184 +  [thm] @ map_filter (try (fn th' => thm RS th'))
   1.185 +    [@{thm measurable_compose_rev}, @{thm pred_sets1}, @{thm pred_sets2}, @{thm sets_into_space}];
   1.186 +
   1.187 +fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
   1.188 +
   1.189 +fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
   1.190 +
   1.191 +fun TAKE n f thm = Seq.take n (f thm)
   1.192 +
   1.193 +fun nth_hol_goal thm i =
   1.194 +  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
   1.195 +
   1.196 +fun dest_measurable_fun t =
   1.197 +  (case t of
   1.198 +    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
   1.199 +  | _ => raise (TERM ("not a measurability predicate", [t])))
   1.200 +
   1.201 +fun indep (Bound i) t b = i < b orelse t <= i
   1.202 +  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
   1.203 +  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   1.204 +  | indep _ _ _ = true;
   1.205 +
   1.206 +fun cnt_prefixes ctxt (Abs (n, T, t)) = let
   1.207 +      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
   1.208 +      fun cnt_walk (Abs (ns, T, t)) Ts =
   1.209 +          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
   1.210 +        | cnt_walk (f $ g) Ts = let
   1.211 +            val n = length Ts - 1
   1.212 +          in
   1.213 +            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
   1.214 +            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
   1.215 +            (if is_countable (fastype_of1 (Ts, g)) andalso loose_bvar1 (g, n)
   1.216 +                andalso indep g n 0 andalso g <> Bound n
   1.217 +              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
   1.218 +              else [])
   1.219 +          end
   1.220 +        | cnt_walk _ _ = []
   1.221 +    in map (fn (t1, t2) => let
   1.222 +        val T1 = fastype_of1 ([T], t2)
   1.223 +        val T2 = fastype_of1 ([T], t)
   1.224 +      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
   1.225 +        [SOME T1, SOME T, SOME T2])
   1.226 +      end) (cnt_walk t [T])
   1.227 +    end
   1.228 +  | cnt_prefixes _ _ = []
   1.229 +
   1.230 +val split_fun_tac =
   1.231 +  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   1.232 +    let
   1.233 +      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
   1.234 +      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
   1.235 +      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
   1.236 +      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
   1.237 +    in if null cps then no_tac else debug_tac ctxt (K "split fun") (resolve_tac cps) i end
   1.238 +    handle TERM _ => no_tac) 1)
   1.239 +
   1.240 +fun single_measurable_tac ctxt facts =
   1.241 +  debug_tac ctxt (fn () => "single + " ^ Pretty.str_of (Pretty.block (map (Syntax.pretty_term ctxt o prop_of) facts)))
   1.242 +  (resolve_tac ((maps (import_theorem o Simplifier.norm_hhf) facts) @ get_all ctxt)
   1.243 +    APPEND' (split_fun_tac ctxt));
   1.244 +
   1.245 +fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
   1.246 +  (case nth_hol_goal thm n of
   1.247 +    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
   1.248 +  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
   1.249 +  | _ => true)
   1.250 +  handle TERM _ => true;
   1.251 +
   1.252 +fun measurable_tac' ctxt ss facts n =
   1.253 +  TAKE (Config.get ctxt backtrack)
   1.254 +  ((single_measurable_tac ctxt facts THEN'
   1.255 +   REPEAT o (single_measurable_tac ctxt facts APPEND'
   1.256 +             SOLVED' (fn n => COND (is_cond_formlua n) (debug_tac ctxt (K "simp") (asm_full_simp_tac ss) n) no_tac))) n);
   1.257 +
   1.258 +fun measurable_tac ctxt = measurable_tac' ctxt (simpset_of ctxt);
   1.259 +
   1.260 +val attr_add = Thm.declaration_attribute o add_thm;
   1.261 +
   1.262 +val attr : attribute context_parser =
   1.263 +  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
   1.264 +     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
   1.265 +
   1.266 +val method : (Proof.context -> Method.method) context_parser =
   1.267 +  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
   1.268 +
   1.269 +fun simproc ss redex = let
   1.270 +    val ctxt = Simplifier.the_context ss;
   1.271 +    val t = HOLogic.mk_Trueprop (term_of redex);
   1.272 +    fun tac {context = ctxt, ...} =
   1.273 +      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss) 1);
   1.274 +  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
   1.275 +
   1.276 +end
   1.277 +
   1.278 +*}
   1.279 +
   1.280 +attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
   1.281 +method_setup measurable = {* Measurable.method *} "measurability prover"
   1.282 +simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
   1.283 +
   1.284 +declare
   1.285 +  top[measurable]
   1.286 +  empty_sets[measurable (raw)]
   1.287 +  Un[measurable (raw)]
   1.288 +  Diff[measurable (raw)]
   1.289 +
   1.290 +declare
   1.291 +  measurable_count_space[measurable (raw)]
   1.292 +  measurable_ident[measurable (raw)]
   1.293 +  measurable_ident'[measurable (raw)]
   1.294 +  measurable_count_space_const[measurable (raw)]
   1.295 +  measurable_const[measurable (raw)]
   1.296 +  measurable_If[measurable (raw)]
   1.297 +  measurable_comp[measurable (raw)]
   1.298 +  measurable_sets[measurable (raw)]
   1.299 +
   1.300 +lemma predE[measurable (raw)]: 
   1.301 +  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
   1.302 +  unfolding pred_def .
   1.303 +
   1.304 +lemma pred_intros_imp'[measurable (raw)]:
   1.305 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
   1.306 +  by (cases K) auto
   1.307 +
   1.308 +lemma pred_intros_conj1'[measurable (raw)]:
   1.309 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
   1.310 +  by (cases K) auto
   1.311 +
   1.312 +lemma pred_intros_conj2'[measurable (raw)]:
   1.313 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
   1.314 +  by (cases K) auto
   1.315 +
   1.316 +lemma pred_intros_disj1'[measurable (raw)]:
   1.317 +  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
   1.318 +  by (cases K) auto
   1.319 +
   1.320 +lemma pred_intros_disj2'[measurable (raw)]:
   1.321 +  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
   1.322 +  by (cases K) auto
   1.323 +
   1.324 +lemma pred_intros_logic[measurable (raw)]:
   1.325 +  "pred M (\<lambda>x. x \<in> space M)"
   1.326 +  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
   1.327 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
   1.328 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
   1.329 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
   1.330 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
   1.331 +  "pred M (\<lambda>x. f x \<in> UNIV)"
   1.332 +  "pred M (\<lambda>x. f x \<in> {})"
   1.333 +  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
   1.334 +  "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))"
   1.335 +  "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))"
   1.336 +  "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))"
   1.337 +  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
   1.338 +  by (auto intro!: sets_Collect simp: iff_conv_conj_imp pred_def)
   1.339 +
   1.340 +lemma pred_intros_countable[measurable (raw)]:
   1.341 +  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
   1.342 +  shows 
   1.343 +    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
   1.344 +    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
   1.345 +  by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
   1.346 +
   1.347 +lemma pred_intros_countable_bounded[measurable (raw)]:
   1.348 +  fixes X :: "'i :: countable set"
   1.349 +  shows 
   1.350 +    "(\<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))"
   1.351 +    "(\<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))"
   1.352 +    "(\<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)"
   1.353 +    "(\<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)"
   1.354 +  by (auto simp: Bex_def Ball_def)
   1.355 +
   1.356 +lemma pred_intros_finite[measurable (raw)]:
   1.357 +  "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))"
   1.358 +  "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))"
   1.359 +  "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)"
   1.360 +  "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)"
   1.361 +  by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
   1.362 +
   1.363 +lemma countable_Un_Int[measurable (raw)]:
   1.364 +  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
   1.365 +  "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"
   1.366 +  by auto
   1.367 +
   1.368 +declare
   1.369 +  finite_UN[measurable (raw)]
   1.370 +  finite_INT[measurable (raw)]
   1.371 +
   1.372 +lemma sets_Int_pred[measurable (raw)]:
   1.373 +  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
   1.374 +  shows "A \<inter> B \<in> sets M"
   1.375 +proof -
   1.376 +  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
   1.377 +  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
   1.378 +    using space by auto
   1.379 +  finally show ?thesis .
   1.380 +qed
   1.381 +
   1.382 +lemma [measurable (raw generic)]:
   1.383 +  assumes f: "f \<in> measurable M N" and c: "{c} \<in> sets N"
   1.384 +  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
   1.385 +    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
   1.386 +  using measurable_sets[OF f c] by (auto simp: Int_def conj_commute eq_commute pred_def)
   1.387 +
   1.388 +lemma pred_le_const[measurable (raw generic)]:
   1.389 +  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
   1.390 +  using measurable_sets[OF f c]
   1.391 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   1.392 +
   1.393 +lemma pred_const_le[measurable (raw generic)]:
   1.394 +  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
   1.395 +  using measurable_sets[OF f c]
   1.396 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   1.397 +
   1.398 +lemma pred_less_const[measurable (raw generic)]:
   1.399 +  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
   1.400 +  using measurable_sets[OF f c]
   1.401 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   1.402 +
   1.403 +lemma pred_const_less[measurable (raw generic)]:
   1.404 +  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
   1.405 +  using measurable_sets[OF f c]
   1.406 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   1.407 +
   1.408 +declare
   1.409 +  Int[measurable (raw)]
   1.410 +
   1.411 +hide_const (open) pred
   1.412 +
   1.413  subsection {* Extend measure *}
   1.414  
   1.415  definition "extend_measure \<Omega> I G \<mu> =