# HG changeset patch
# User hoelzl
# Date 1354719548 -3600
# Node ID 3d8863c41fe854ea85371074ac54dae8bbac6b64
# Parent  d00e2b0ca0699f5e50c557d3cf050c239ec1dbee
Move the measurability prover to its own file

diff -r d00e2b0ca069 -r 3d8863c41fe8 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 05 15:58:48 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 05 15:59:08 2012 +0100
@@ -6,7 +6,9 @@
 header {*Borel spaces*}
 
 theory Borel_Space
-  imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
+imports
+  Measurable
+  "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
 section "Generic Borel spaces"
@@ -33,7 +35,7 @@
 lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
   unfolding borel_def by auto
 
-lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
+lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
   unfolding borel_def pred_def by auto
 
 lemma borel_open[measurable (raw generic)]:
diff -r d00e2b0ca069 -r 3d8863c41fe8 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Dec 05 15:58:48 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Dec 05 15:59:08 2012 +0100
@@ -513,7 +513,7 @@
 lemma sets_in_Pi[measurable (raw)]:
   "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
   (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
-  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
+  Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
   unfolding pred_def
   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
 
@@ -526,7 +526,7 @@
 qed
 
 lemma sets_in_extensional[measurable (raw)]:
-  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
+  "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
   unfolding pred_def
   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
 
diff -r d00e2b0ca069 -r 3d8863c41fe8 src/HOL/Probability/Measurable.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Measurable.thy	Wed Dec 05 15:59:08 2012 +0100
@@ -0,0 +1,247 @@
+(*  Title:      HOL/Probability/measurable.ML
+    Author:     Johannes Hölzl <hoelzl@in.tum.de>
+*)
+theory Measurable
+  imports Sigma_Algebra
+begin
+
+subsection {* Measurability prover *}
+
+lemma (in algebra) sets_Collect_finite_All:
+  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
+  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
+proof -
+  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})"
+    by auto
+  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
+qed
+
+abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
+
+lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
+proof
+  assume "pred M P"
+  then have "P -` {True} \<inter> space M \<in> sets M"
+    by (auto simp: measurable_count_space_eq2)
+  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
+  finally show "{x\<in>space M. P x} \<in> sets M" .
+next
+  assume P: "{x\<in>space M. P x} \<in> sets M"
+  moreover
+  { fix X
+    have "X \<in> Pow (UNIV :: bool set)" by simp
+    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> {})}"
+      unfolding UNIV_bool Pow_insert Pow_empty by auto
+    then have "P -` X \<inter> space M \<in> sets M"
+      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
+  then show "pred M P"
+    by (auto simp: measurable_def)
+qed
+
+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))"
+  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
+
+lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
+  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
+
+ML_file "measurable.ML"
+
+attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
+attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
+attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
+method_setup measurable = {* Measurable.method *} "measurability prover"
+simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
+
+declare
+  measurable_compose_rev[measurable_dest]
+  pred_sets1[measurable_dest]
+  pred_sets2[measurable_dest]
+  sets.sets_into_space[measurable_dest]
+
+declare
+  sets.top[measurable]
+  sets.empty_sets[measurable (raw)]
+  sets.Un[measurable (raw)]
+  sets.Diff[measurable (raw)]
+
+declare
+  measurable_count_space[measurable (raw)]
+  measurable_ident[measurable (raw)]
+  measurable_ident_sets[measurable (raw)]
+  measurable_const[measurable (raw)]
+  measurable_If[measurable (raw)]
+  measurable_comp[measurable (raw)]
+  measurable_sets[measurable (raw)]
+
+lemma predE[measurable (raw)]: 
+  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
+  unfolding pred_def .
+
+lemma pred_intros_imp'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
+  by (cases K) auto
+
+lemma pred_intros_conj1'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
+  by (cases K) auto
+
+lemma pred_intros_conj2'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
+  by (cases K) auto
+
+lemma pred_intros_disj1'[measurable (raw)]:
+  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
+  by (cases K) auto
+
+lemma pred_intros_disj2'[measurable (raw)]:
+  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
+  by (cases K) auto
+
+lemma pred_intros_logic[measurable (raw)]:
+  "pred M (\<lambda>x. x \<in> space M)"
+  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
+  "pred M (\<lambda>x. f x \<in> UNIV)"
+  "pred M (\<lambda>x. f x \<in> {})"
+  "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
+  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
+  "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))"
+  "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))"
+  "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))"
+  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
+  by (auto simp: iff_conv_conj_imp pred_def)
+
+lemma pred_intros_countable[measurable (raw)]:
+  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
+  shows 
+    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
+    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
+  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
+
+lemma pred_intros_countable_bounded[measurable (raw)]:
+  fixes X :: "'i :: countable set"
+  shows 
+    "(\<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))"
+    "(\<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))"
+    "(\<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)"
+    "(\<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)"
+  by (auto simp: Bex_def Ball_def)
+
+lemma pred_intros_finite[measurable (raw)]:
+  "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))"
+  "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))"
+  "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)"
+  "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)"
+  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
+
+lemma countable_Un_Int[measurable (raw)]:
+  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
+  "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"
+  by auto
+
+declare
+  finite_UN[measurable (raw)]
+  finite_INT[measurable (raw)]
+
+lemma sets_Int_pred[measurable (raw)]:
+  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
+  shows "A \<inter> B \<in> sets M"
+proof -
+  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
+  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
+    using space by auto
+  finally show ?thesis .
+qed
+
+lemma [measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
+  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
+    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
+proof -
+  show "pred M (\<lambda>x. f x = c)"
+  proof cases
+    assume "c \<in> space N"
+    with measurable_sets[OF f c] show ?thesis
+      by (auto simp: Int_def conj_commute pred_def)
+  next
+    assume "c \<notin> space N"
+    with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
+    then show ?thesis by (auto simp: pred_def cong: conj_cong)
+  qed
+  then show "pred M (\<lambda>x. c = f x)"
+    by (simp add: eq_commute)
+qed
+
+lemma pred_le_const[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_le[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_less_const[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_less[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+declare
+  sets.Int[measurable (raw)]
+
+lemma pred_in_If[measurable (raw)]:
+  "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
+    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
+  by auto
+
+lemma sets_range[measurable_dest]:
+  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
+  by auto
+
+lemma pred_sets_range[measurable_dest]:
+  "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)"
+  using pred_sets2[OF sets_range] by auto
+
+lemma sets_All[measurable_dest]:
+  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
+  by auto
+
+lemma pred_sets_All[measurable_dest]:
+  "\<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)"
+  using pred_sets2[OF sets_All, of A N f] by auto
+
+lemma sets_Ball[measurable_dest]:
+  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
+  by auto
+
+lemma pred_sets_Ball[measurable_dest]:
+  "\<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)"
+  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
+
+lemma measurable_finite[measurable (raw)]:
+  fixes S :: "'a \<Rightarrow> nat set"
+  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
+  shows "pred M (\<lambda>x. finite (S x))"
+  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
+
+lemma measurable_Least[measurable]:
+  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
+  shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
+  unfolding measurable_def by (safe intro!: sets_Least) simp_all
+
+lemma measurable_count_space_insert[measurable (raw)]:
+  "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
+  by simp
+
+hide_const (open) pred
+
+end
diff -r d00e2b0ca069 -r 3d8863c41fe8 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Dec 05 15:58:48 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Dec 05 15:59:08 2012 +0100
@@ -8,7 +8,7 @@
 
 theory Measure_Space
 imports
-  Sigma_Algebra
+  Measurable
   "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
 begin
 
diff -r d00e2b0ca069 -r 3d8863c41fe8 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 05 15:58:48 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 05 15:59:08 2012 +0100
@@ -252,7 +252,7 @@
   "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
   by (auto simp: algebra_iff_Int)
 
-section {* Restricted algebras *}
+subsection {* Restricted algebras *}
 
 abbreviation (in algebra)
   "restricted_space A \<equiv> (op \<inter> A) ` M"
@@ -707,7 +707,7 @@
   qed
 qed
 
-section "Disjoint families"
+subsection "Disjoint families"
 
 definition
   disjoint_family_on  where
@@ -866,7 +866,7 @@
     by (intro disjointD[OF d]) auto
 qed
 
-section {* Ring generated by a semiring *}
+subsection {* Ring generated by a semiring *}
 
 definition (in semiring_of_sets)
   "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
@@ -996,7 +996,7 @@
     by (blast intro!: sigma_sets_mono elim: generated_ringE)
 qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
 
-section {* Measure type *}
+subsection {* Measure type *}
 
 definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
   "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)"
@@ -1138,7 +1138,7 @@
 lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
   by auto
 
-section {* Constructing simple @{typ "'a measure"} *}
+subsection {* Constructing simple @{typ "'a measure"} *}
 
 lemma emeasure_measure_of:
   assumes M: "M = measure_of \<Omega> A \<mu>"
@@ -1231,7 +1231,7 @@
   shows "sigma \<Omega> M = sigma \<Omega> N"
   by (rule measure_eqI) (simp_all add: emeasure_sigma)
 
-section {* Measurable functions *}
+subsection {* Measurable functions *}
 
 definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
   "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
@@ -1428,7 +1428,7 @@
     measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
   using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
 
-section {* Counting space *}
+subsection {* Counting space *}
 
 definition count_space :: "'a set \<Rightarrow> 'a measure" where
   "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
@@ -1473,45 +1473,6 @@
   finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
 qed
 
-subsection {* Measurable method *}
-
-lemma (in algebra) sets_Collect_finite_All:
-  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
-  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
-proof -
-  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})"
-    by auto
-  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
-qed
-
-abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
-
-lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
-proof
-  assume "pred M P"
-  then have "P -` {True} \<inter> space M \<in> sets M"
-    by (auto simp: measurable_count_space_eq2)
-  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
-  finally show "{x\<in>space M. P x} \<in> sets M" .
-next
-  assume P: "{x\<in>space M. P x} \<in> sets M"
-  moreover
-  { fix X
-    have "X \<in> Pow (UNIV :: bool set)" by simp
-    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> {})}"
-      unfolding UNIV_bool Pow_insert Pow_empty by auto
-    then have "P -` X \<inter> space M \<in> sets M"
-      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
-  then show "pred M P"
-    by (auto simp: measurable_def)
-qed
-
-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))"
-  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
-
-lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
-  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
-
 lemma measurable_count_space_const:
   "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   by (simp add: measurable_const)
@@ -1525,420 +1486,6 @@
   shows "(\<lambda>x. f (g x)) \<in> measurable M N"
   using measurable_compose[OF g f] .
 
-ML {*
-
-structure Measurable =
-struct
-
-datatype level = Concrete | Generic;
-
-structure Data = Generic_Data
-(
-  type T = {
-    concrete_thms : thm Item_Net.T,
-    generic_thms : thm Item_Net.T,
-    dest_thms : thm Item_Net.T,
-    app_thms : thm Item_Net.T }
-  val empty = {
-    concrete_thms = Thm.full_rules,
-    generic_thms = Thm.full_rules,
-    dest_thms = Thm.full_rules,
-    app_thms = Thm.full_rules};
-  val extend = I;
-  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
-      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
-    concrete_thms = Item_Net.merge (ct1, ct2),
-    generic_thms = Item_Net.merge (gt1, gt2),
-    dest_thms = Item_Net.merge (dt1, dt2),
-    app_thms = Item_Net.merge (at1, at2) };
-);
-
-val debug =
-  Attrib.setup_config_bool @{binding measurable_debug} (K false)
-
-val backtrack =
-  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
-
-val split =
-  Attrib.setup_config_bool @{binding measurable_split} (K true)
-
-fun TAKE n tac = Seq.take n o tac
-
-fun get lv =
-  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
-  Data.get o Context.Proof;
-
-fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
-
-fun map_data f1 f2 f3 f4
-  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
-  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
-
-fun map_concrete_thms f = map_data f I I I
-fun map_generic_thms f = map_data I f I I
-fun map_dest_thms f = map_data I I f I
-fun map_app_thms f = map_data I I I f
-
-fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
-fun add thms' = update (fold Item_Net.update thms');
-
-val get_dest = Item_Net.content o #dest_thms o Data.get;
-val add_dest = Data.map o map_dest_thms o Item_Net.update;
-
-val get_app = Item_Net.content o #app_thms o Data.get;
-val add_app = Data.map o map_app_thms o Item_Net.update;
-
-fun is_too_generic thm =
-  let 
-    val concl = concl_of thm
-    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
-  in is_Var (head_of concl') end
-
-fun import_theorem ctxt thm = if is_too_generic thm then [] else
-  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
-
-fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
-
-fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
-
-fun nth_hol_goal thm i =
-  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
-
-fun dest_measurable_fun t =
-  (case t of
-    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
-  | _ => raise (TERM ("not a measurability predicate", [t])))
-
-fun is_cond_formula n thm = if length (prems_of thm) < n then false else
-  (case nth_hol_goal thm n of
-    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
-  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
-  | _ => true)
-  handle TERM _ => true;
-
-fun indep (Bound i) t b = i < b orelse t <= i
-  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
-  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
-  | indep _ _ _ = true;
-
-fun cnt_prefixes ctxt (Abs (n, T, t)) = let
-      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
-      fun cnt_walk (Abs (ns, T, t)) Ts =
-          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
-        | cnt_walk (f $ g) Ts = let
-            val n = length Ts - 1
-          in
-            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
-            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
-            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
-                andalso indep g n 0 andalso g <> Bound n
-              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
-              else [])
-          end
-        | cnt_walk _ _ = []
-    in map (fn (t1, t2) => let
-        val T1 = type_of1 ([T], t2)
-        val T2 = type_of1 ([T], t)
-      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
-        [SOME T1, SOME T, SOME T2])
-      end) (cnt_walk t [T])
-    end
-  | cnt_prefixes _ _ = []
-
-val split_countable_tac =
-  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
-    let
-      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
-      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
-      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
-      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
-    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
-    handle TERM _ => no_tac) 1)
-
-fun measurable_tac' ctxt ss facts = let
-
-    val imported_thms =
-      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
-
-    fun debug_facts msg () =
-      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
-        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
-
-    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
-
-    val split_app_tac =
-      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
-        let
-          fun app_prefixes (Abs (n, T, (f $ g))) = let
-                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
-              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
-            | app_prefixes _ = []
-
-          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
-            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
-          val thy = Proof_Context.theory_of ctxt
-          val tunify = Sign.typ_unify thy
-          val thms = map
-              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
-              (get_app (Context.Proof ctxt))
-          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
-          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
-            let
-              val inst =
-                (Vartab.empty, ~1)
-                |> tunify (T, thmT)
-                |> tunify (Tf, thmTf)
-                |> tunify (Tc, thmTc)
-                |> Vartab.dest o fst
-              val subst = subst_TVars (map (apsnd snd) inst)
-            in
-              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
-                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
-            end
-          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
-        in if null cps then no_tac
-            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
-              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
-        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
-        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
-
-    fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
-
-    val depth_measurable_tac = REPEAT_cnt (fn n =>
-       (COND (is_cond_formula 1)
-        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ss) 1))
-        ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
-          (split_app_tac ctxt 1) APPEND
-          (splitter 1)))) 0
-
-  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
-
-fun measurable_tac ctxt facts =
-  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
-
-val attr_add = Thm.declaration_attribute o add_thm;
-
-val attr : attribute context_parser =
-  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
-     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
-
-val dest_attr : attribute context_parser =
-  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
-
-val app_attr : attribute context_parser =
-  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
-
-val method : (Proof.context -> Method.method) context_parser =
-  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
-
-fun simproc ss redex = let
-    val ctxt = Simplifier.the_context ss;
-    val t = HOLogic.mk_Trueprop (term_of redex);
-    fun tac {context = ctxt, prems = _ } =
-      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
-  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
-
-end
-
-*}
-
-attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
-attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
-attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
-method_setup measurable = {* Measurable.method *} "measurability prover"
-simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
-
-declare
-  measurable_compose_rev[measurable_dest]
-  pred_sets1[measurable_dest]
-  pred_sets2[measurable_dest]
-  sets.sets_into_space[measurable_dest]
-
-declare
-  sets.top[measurable]
-  sets.empty_sets[measurable (raw)]
-  sets.Un[measurable (raw)]
-  sets.Diff[measurable (raw)]
-
-declare
-  measurable_count_space[measurable (raw)]
-  measurable_ident[measurable (raw)]
-  measurable_ident_sets[measurable (raw)]
-  measurable_const[measurable (raw)]
-  measurable_If[measurable (raw)]
-  measurable_comp[measurable (raw)]
-  measurable_sets[measurable (raw)]
-
-lemma predE[measurable (raw)]: 
-  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
-  unfolding pred_def .
-
-lemma pred_intros_imp'[measurable (raw)]:
-  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
-  by (cases K) auto
-
-lemma pred_intros_conj1'[measurable (raw)]:
-  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
-  by (cases K) auto
-
-lemma pred_intros_conj2'[measurable (raw)]:
-  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
-  by (cases K) auto
-
-lemma pred_intros_disj1'[measurable (raw)]:
-  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
-  by (cases K) auto
-
-lemma pred_intros_disj2'[measurable (raw)]:
-  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
-  by (cases K) auto
-
-lemma pred_intros_logic[measurable (raw)]:
-  "pred M (\<lambda>x. x \<in> space M)"
-  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
-  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
-  "pred M (\<lambda>x. f x \<in> UNIV)"
-  "pred M (\<lambda>x. f x \<in> {})"
-  "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
-  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
-  "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))"
-  "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))"
-  "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))"
-  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
-  by (auto simp: iff_conv_conj_imp pred_def)
-
-lemma pred_intros_countable[measurable (raw)]:
-  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
-  shows 
-    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
-    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
-  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
-
-lemma pred_intros_countable_bounded[measurable (raw)]:
-  fixes X :: "'i :: countable set"
-  shows 
-    "(\<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))"
-    "(\<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))"
-    "(\<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)"
-    "(\<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)"
-  by (auto simp: Bex_def Ball_def)
-
-lemma pred_intros_finite[measurable (raw)]:
-  "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))"
-  "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))"
-  "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)"
-  "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)"
-  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
-
-lemma countable_Un_Int[measurable (raw)]:
-  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
-  "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"
-  by auto
-
-declare
-  finite_UN[measurable (raw)]
-  finite_INT[measurable (raw)]
-
-lemma sets_Int_pred[measurable (raw)]:
-  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
-  shows "A \<inter> B \<in> sets M"
-proof -
-  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
-  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
-    using space by auto
-  finally show ?thesis .
-qed
-
-lemma [measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
-  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
-    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
-proof -
-  show "pred M (\<lambda>x. f x = c)"
-  proof cases
-    assume "c \<in> space N"
-    with measurable_sets[OF f c] show ?thesis
-      by (auto simp: Int_def conj_commute pred_def)
-  next
-    assume "c \<notin> space N"
-    with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
-    then show ?thesis by (auto simp: pred_def cong: conj_cong)
-  qed
-  then show "pred M (\<lambda>x. c = f x)"
-    by (simp add: eq_commute)
-qed
-
-lemma pred_le_const[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-lemma pred_const_le[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-lemma pred_less_const[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-lemma pred_const_less[measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
-  using measurable_sets[OF f c]
-  by (auto simp: Int_def conj_commute eq_commute pred_def)
-
-declare
-  sets.Int[measurable (raw)]
-
-lemma pred_in_If[measurable (raw)]:
-  "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
-    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
-  by auto
-
-lemma sets_range[measurable_dest]:
-  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
-  by auto
-
-lemma pred_sets_range[measurable_dest]:
-  "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)"
-  using pred_sets2[OF sets_range] by auto
-
-lemma sets_All[measurable_dest]:
-  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
-  by auto
-
-lemma pred_sets_All[measurable_dest]:
-  "\<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)"
-  using pred_sets2[OF sets_All, of A N f] by auto
-
-lemma sets_Ball[measurable_dest]:
-  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
-  by auto
-
-lemma pred_sets_Ball[measurable_dest]:
-  "\<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)"
-  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
-
-lemma measurable_finite[measurable (raw)]:
-  fixes S :: "'a \<Rightarrow> nat set"
-  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
-  shows "pred M (\<lambda>x. finite (S x))"
-  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
-
-lemma measurable_Least[measurable]:
-  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
-  shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
-  unfolding measurable_def by (safe intro!: sets_Least) simp_all
-
-lemma measurable_count_space_insert[measurable (raw)]:
-  "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
-  by simp
-
-hide_const (open) pred
 
 subsection {* Extend measure *}
 
@@ -2365,7 +1912,7 @@
     by blast
 qed
 
-section {* Dynkin systems *}
+subsection {* Dynkin systems *}
 
 locale dynkin_system = subset_class +
   assumes space: "\<Omega> \<in> M"
diff -r d00e2b0ca069 -r 3d8863c41fe8 src/HOL/Probability/measurable.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/measurable.ML	Wed Dec 05 15:59:08 2012 +0100
@@ -0,0 +1,238 @@
+(*  Title:      HOL/Probability/measurable.ML
+    Author:     Johannes Hölzl <hoelzl@in.tum.de>
+
+Measurability prover.
+*)
+
+signature MEASURABLE = 
+sig
+  datatype level = Concrete | Generic
+
+  val simproc : simpset -> cterm -> thm option
+  val method : (Proof.context -> Method.method) context_parser
+  val measurable_tac : Proof.context -> thm list -> tactic
+
+  val attr : attribute context_parser
+  val dest_attr : attribute context_parser
+  val app_attr : attribute context_parser
+
+  val get : level -> Proof.context -> thm list
+  val get_all : Proof.context -> thm list
+
+  val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
+
+end ;
+
+structure Measurable : MEASURABLE =
+struct
+
+datatype level = Concrete | Generic;
+
+structure Data = Generic_Data
+(
+  type T = {
+    concrete_thms : thm Item_Net.T,
+    generic_thms : thm Item_Net.T,
+    dest_thms : thm Item_Net.T,
+    app_thms : thm Item_Net.T }
+  val empty = {
+    concrete_thms = Thm.full_rules,
+    generic_thms = Thm.full_rules,
+    dest_thms = Thm.full_rules,
+    app_thms = Thm.full_rules};
+  val extend = I;
+  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
+      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
+    concrete_thms = Item_Net.merge (ct1, ct2),
+    generic_thms = Item_Net.merge (gt1, gt2),
+    dest_thms = Item_Net.merge (dt1, dt2),
+    app_thms = Item_Net.merge (at1, at2) };
+);
+
+val debug =
+  Attrib.setup_config_bool @{binding measurable_debug} (K false)
+
+val backtrack =
+  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
+
+val split =
+  Attrib.setup_config_bool @{binding measurable_split} (K true)
+
+fun TAKE n tac = Seq.take n o tac
+
+fun get lv =
+  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
+  Data.get o Context.Proof;
+
+fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
+
+fun map_data f1 f2 f3 f4
+  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
+  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
+
+fun map_concrete_thms f = map_data f I I I
+fun map_generic_thms f = map_data I f I I
+fun map_dest_thms f = map_data I I f I
+fun map_app_thms f = map_data I I I f
+
+fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
+fun add thms' = update (fold Item_Net.update thms');
+
+val get_dest = Item_Net.content o #dest_thms o Data.get;
+val add_dest = Data.map o map_dest_thms o Item_Net.update;
+
+val get_app = Item_Net.content o #app_thms o Data.get;
+val add_app = Data.map o map_app_thms o Item_Net.update;
+
+fun is_too_generic thm =
+  let 
+    val concl = concl_of thm
+    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
+  in is_Var (head_of concl') end
+
+fun import_theorem ctxt thm = if is_too_generic thm then [] else
+  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
+
+fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
+
+fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
+
+fun nth_hol_goal thm i =
+  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
+
+fun dest_measurable_fun t =
+  (case t of
+    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
+  | _ => raise (TERM ("not a measurability predicate", [t])))
+
+fun is_cond_formula n thm = if length (prems_of thm) < n then false else
+  (case nth_hol_goal thm n of
+    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
+  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
+  | _ => true)
+  handle TERM _ => true;
+
+fun indep (Bound i) t b = i < b orelse t <= i
+  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
+  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
+  | indep _ _ _ = true;
+
+fun cnt_prefixes ctxt (Abs (n, T, t)) = let
+      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
+      fun cnt_walk (Abs (ns, T, t)) Ts =
+          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
+        | cnt_walk (f $ g) Ts = let
+            val n = length Ts - 1
+          in
+            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
+            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
+            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
+                andalso indep g n 0 andalso g <> Bound n
+              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
+              else [])
+          end
+        | cnt_walk _ _ = []
+    in map (fn (t1, t2) => let
+        val T1 = type_of1 ([T], t2)
+        val T2 = type_of1 ([T], t)
+      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
+        [SOME T1, SOME T, SOME T2])
+      end) (cnt_walk t [T])
+    end
+  | cnt_prefixes _ _ = []
+
+val split_countable_tac =
+  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+    let
+      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
+      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
+      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
+      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
+    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
+    handle TERM _ => no_tac) 1)
+
+fun measurable_tac' ctxt ss facts = let
+
+    val imported_thms =
+      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
+
+    fun debug_facts msg () =
+      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
+        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
+
+    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
+
+    val split_app_tac =
+      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+        let
+          fun app_prefixes (Abs (n, T, (f $ g))) = let
+                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
+              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
+            | app_prefixes _ = []
+
+          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
+            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
+          val thy = Proof_Context.theory_of ctxt
+          val tunify = Sign.typ_unify thy
+          val thms = map
+              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
+              (get_app (Context.Proof ctxt))
+          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
+          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
+            let
+              val inst =
+                (Vartab.empty, ~1)
+                |> tunify (T, thmT)
+                |> tunify (Tf, thmTf)
+                |> tunify (Tc, thmTc)
+                |> Vartab.dest o fst
+              val subst = subst_TVars (map (apsnd snd) inst)
+            in
+              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
+                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
+            end
+          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
+        in if null cps then no_tac
+            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
+              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
+        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
+        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
+
+    fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
+
+    val depth_measurable_tac = REPEAT_cnt (fn n =>
+       (COND (is_cond_formula 1)
+        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ss) 1))
+        ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
+          (split_app_tac ctxt 1) APPEND
+          (splitter 1)))) 0
+
+  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
+
+fun measurable_tac ctxt facts =
+  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
+
+val attr_add = Thm.declaration_attribute o add_thm;
+
+val attr : attribute context_parser =
+  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
+     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
+
+val dest_attr : attribute context_parser =
+  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
+
+val app_attr : attribute context_parser =
+  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
+
+val method : (Proof.context -> Method.method) context_parser =
+  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
+
+fun simproc ss redex = let
+    val ctxt = Simplifier.the_context ss;
+    val t = HOLogic.mk_Trueprop (term_of redex);
+    fun tac {context = ctxt, prems = _ } =
+      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
+  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
+
+end
+