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.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.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.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.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.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.107 +abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
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.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.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.135 +lemma measurable_count_space_const:
1.136 +  "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
1.137 +  by auto
1.139 +lemma measurable_count_space:
1.140 +  "f \<in> measurable (count_space A) (count_space UNIV)"
1.141 +  by simp
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.148 +ML {*
1.150 +structure Measurable =
1.151 +struct
1.153 +datatype level = Concrete | Generic;
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.163 +val debug =
1.164 +  Attrib.setup_config_bool @{binding measurable_debug} (K false)
1.166 +val backtrack =
1.167 +  Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
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.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.175 +fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
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.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.187 +fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
1.189 +fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
1.191 +fun TAKE n f thm = Seq.take n (f thm)
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.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.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.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.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.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.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.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.258 +fun measurable_tac ctxt = measurable_tac' ctxt (simpset_of ctxt);
1.260 +val attr_add = Thm.declaration_attribute o add_thm;
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.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.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.276 +end
1.278 +*}
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.284 +declare
1.285 +  top[measurable]
1.286 +  empty_sets[measurable (raw)]
1.287 +  Un[measurable (raw)]
1.288 +  Diff[measurable (raw)]
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.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.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.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.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.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.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.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.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.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.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.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.368 +declare
1.369 +  finite_UN[measurable (raw)]
1.370 +  finite_INT[measurable (raw)]
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.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.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.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.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.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.408 +declare
1.409 +  Int[measurable (raw)]
1.411 +hide_const (open) pred
1.413  subsection {* Extend measure *}
1.415  definition "extend_measure \<Omega> I G \<mu> =