Move the measurability prover to its own file
authorhoelzl
Wed Dec 05 15:59:08 2012 +0100 (2012-12-05)
changeset 503873d8863c41fe8
parent 50386 d00e2b0ca069
child 50388 a5b666e0c3c2
Move the measurability prover to its own file
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/measurable.ML
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 05 15:58:48 2012 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 05 15:59:08 2012 +0100
     1.3 @@ -6,7 +6,9 @@
     1.4  header {*Borel spaces*}
     1.5  
     1.6  theory Borel_Space
     1.7 -  imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
     1.8 +imports
     1.9 +  Measurable
    1.10 +  "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
    1.11  begin
    1.12  
    1.13  section "Generic Borel spaces"
    1.14 @@ -33,7 +35,7 @@
    1.15  lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
    1.16    unfolding borel_def by auto
    1.17  
    1.18 -lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
    1.19 +lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
    1.20    unfolding borel_def pred_def by auto
    1.21  
    1.22  lemma borel_open[measurable (raw generic)]:
     2.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Dec 05 15:58:48 2012 +0100
     2.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Dec 05 15:59:08 2012 +0100
     2.3 @@ -513,7 +513,7 @@
     2.4  lemma sets_in_Pi[measurable (raw)]:
     2.5    "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
     2.6    (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
     2.7 -  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
     2.8 +  Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
     2.9    unfolding pred_def
    2.10    by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
    2.11  
    2.12 @@ -526,7 +526,7 @@
    2.13  qed
    2.14  
    2.15  lemma sets_in_extensional[measurable (raw)]:
    2.16 -  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
    2.17 +  "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
    2.18    unfolding pred_def
    2.19    by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
    2.20  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Probability/Measurable.thy	Wed Dec 05 15:59:08 2012 +0100
     3.3 @@ -0,0 +1,247 @@
     3.4 +(*  Title:      HOL/Probability/measurable.ML
     3.5 +    Author:     Johannes Hölzl <hoelzl@in.tum.de>
     3.6 +*)
     3.7 +theory Measurable
     3.8 +  imports Sigma_Algebra
     3.9 +begin
    3.10 +
    3.11 +subsection {* Measurability prover *}
    3.12 +
    3.13 +lemma (in algebra) sets_Collect_finite_All:
    3.14 +  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
    3.15 +  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
    3.16 +proof -
    3.17 +  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})"
    3.18 +    by auto
    3.19 +  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
    3.20 +qed
    3.21 +
    3.22 +abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
    3.23 +
    3.24 +lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
    3.25 +proof
    3.26 +  assume "pred M P"
    3.27 +  then have "P -` {True} \<inter> space M \<in> sets M"
    3.28 +    by (auto simp: measurable_count_space_eq2)
    3.29 +  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
    3.30 +  finally show "{x\<in>space M. P x} \<in> sets M" .
    3.31 +next
    3.32 +  assume P: "{x\<in>space M. P x} \<in> sets M"
    3.33 +  moreover
    3.34 +  { fix X
    3.35 +    have "X \<in> Pow (UNIV :: bool set)" by simp
    3.36 +    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> {})}"
    3.37 +      unfolding UNIV_bool Pow_insert Pow_empty by auto
    3.38 +    then have "P -` X \<inter> space M \<in> sets M"
    3.39 +      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
    3.40 +  then show "pred M P"
    3.41 +    by (auto simp: measurable_def)
    3.42 +qed
    3.43 +
    3.44 +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))"
    3.45 +  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
    3.46 +
    3.47 +lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
    3.48 +  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
    3.49 +
    3.50 +ML_file "measurable.ML"
    3.51 +
    3.52 +attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
    3.53 +attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
    3.54 +attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
    3.55 +method_setup measurable = {* Measurable.method *} "measurability prover"
    3.56 +simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    3.57 +
    3.58 +declare
    3.59 +  measurable_compose_rev[measurable_dest]
    3.60 +  pred_sets1[measurable_dest]
    3.61 +  pred_sets2[measurable_dest]
    3.62 +  sets.sets_into_space[measurable_dest]
    3.63 +
    3.64 +declare
    3.65 +  sets.top[measurable]
    3.66 +  sets.empty_sets[measurable (raw)]
    3.67 +  sets.Un[measurable (raw)]
    3.68 +  sets.Diff[measurable (raw)]
    3.69 +
    3.70 +declare
    3.71 +  measurable_count_space[measurable (raw)]
    3.72 +  measurable_ident[measurable (raw)]
    3.73 +  measurable_ident_sets[measurable (raw)]
    3.74 +  measurable_const[measurable (raw)]
    3.75 +  measurable_If[measurable (raw)]
    3.76 +  measurable_comp[measurable (raw)]
    3.77 +  measurable_sets[measurable (raw)]
    3.78 +
    3.79 +lemma predE[measurable (raw)]: 
    3.80 +  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
    3.81 +  unfolding pred_def .
    3.82 +
    3.83 +lemma pred_intros_imp'[measurable (raw)]:
    3.84 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
    3.85 +  by (cases K) auto
    3.86 +
    3.87 +lemma pred_intros_conj1'[measurable (raw)]:
    3.88 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
    3.89 +  by (cases K) auto
    3.90 +
    3.91 +lemma pred_intros_conj2'[measurable (raw)]:
    3.92 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
    3.93 +  by (cases K) auto
    3.94 +
    3.95 +lemma pred_intros_disj1'[measurable (raw)]:
    3.96 +  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
    3.97 +  by (cases K) auto
    3.98 +
    3.99 +lemma pred_intros_disj2'[measurable (raw)]:
   3.100 +  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
   3.101 +  by (cases K) auto
   3.102 +
   3.103 +lemma pred_intros_logic[measurable (raw)]:
   3.104 +  "pred M (\<lambda>x. x \<in> space M)"
   3.105 +  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
   3.106 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
   3.107 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
   3.108 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
   3.109 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
   3.110 +  "pred M (\<lambda>x. f x \<in> UNIV)"
   3.111 +  "pred M (\<lambda>x. f x \<in> {})"
   3.112 +  "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
   3.113 +  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
   3.114 +  "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))"
   3.115 +  "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))"
   3.116 +  "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))"
   3.117 +  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
   3.118 +  by (auto simp: iff_conv_conj_imp pred_def)
   3.119 +
   3.120 +lemma pred_intros_countable[measurable (raw)]:
   3.121 +  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
   3.122 +  shows 
   3.123 +    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
   3.124 +    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
   3.125 +  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
   3.126 +
   3.127 +lemma pred_intros_countable_bounded[measurable (raw)]:
   3.128 +  fixes X :: "'i :: countable set"
   3.129 +  shows 
   3.130 +    "(\<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))"
   3.131 +    "(\<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))"
   3.132 +    "(\<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)"
   3.133 +    "(\<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)"
   3.134 +  by (auto simp: Bex_def Ball_def)
   3.135 +
   3.136 +lemma pred_intros_finite[measurable (raw)]:
   3.137 +  "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))"
   3.138 +  "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))"
   3.139 +  "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)"
   3.140 +  "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)"
   3.141 +  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
   3.142 +
   3.143 +lemma countable_Un_Int[measurable (raw)]:
   3.144 +  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
   3.145 +  "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"
   3.146 +  by auto
   3.147 +
   3.148 +declare
   3.149 +  finite_UN[measurable (raw)]
   3.150 +  finite_INT[measurable (raw)]
   3.151 +
   3.152 +lemma sets_Int_pred[measurable (raw)]:
   3.153 +  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
   3.154 +  shows "A \<inter> B \<in> sets M"
   3.155 +proof -
   3.156 +  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
   3.157 +  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
   3.158 +    using space by auto
   3.159 +  finally show ?thesis .
   3.160 +qed
   3.161 +
   3.162 +lemma [measurable (raw generic)]:
   3.163 +  assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
   3.164 +  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
   3.165 +    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
   3.166 +proof -
   3.167 +  show "pred M (\<lambda>x. f x = c)"
   3.168 +  proof cases
   3.169 +    assume "c \<in> space N"
   3.170 +    with measurable_sets[OF f c] show ?thesis
   3.171 +      by (auto simp: Int_def conj_commute pred_def)
   3.172 +  next
   3.173 +    assume "c \<notin> space N"
   3.174 +    with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
   3.175 +    then show ?thesis by (auto simp: pred_def cong: conj_cong)
   3.176 +  qed
   3.177 +  then show "pred M (\<lambda>x. c = f x)"
   3.178 +    by (simp add: eq_commute)
   3.179 +qed
   3.180 +
   3.181 +lemma pred_le_const[measurable (raw generic)]:
   3.182 +  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
   3.183 +  using measurable_sets[OF f c]
   3.184 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   3.185 +
   3.186 +lemma pred_const_le[measurable (raw generic)]:
   3.187 +  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
   3.188 +  using measurable_sets[OF f c]
   3.189 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   3.190 +
   3.191 +lemma pred_less_const[measurable (raw generic)]:
   3.192 +  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
   3.193 +  using measurable_sets[OF f c]
   3.194 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   3.195 +
   3.196 +lemma pred_const_less[measurable (raw generic)]:
   3.197 +  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
   3.198 +  using measurable_sets[OF f c]
   3.199 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   3.200 +
   3.201 +declare
   3.202 +  sets.Int[measurable (raw)]
   3.203 +
   3.204 +lemma pred_in_If[measurable (raw)]:
   3.205 +  "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
   3.206 +    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
   3.207 +  by auto
   3.208 +
   3.209 +lemma sets_range[measurable_dest]:
   3.210 +  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
   3.211 +  by auto
   3.212 +
   3.213 +lemma pred_sets_range[measurable_dest]:
   3.214 +  "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)"
   3.215 +  using pred_sets2[OF sets_range] by auto
   3.216 +
   3.217 +lemma sets_All[measurable_dest]:
   3.218 +  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
   3.219 +  by auto
   3.220 +
   3.221 +lemma pred_sets_All[measurable_dest]:
   3.222 +  "\<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)"
   3.223 +  using pred_sets2[OF sets_All, of A N f] by auto
   3.224 +
   3.225 +lemma sets_Ball[measurable_dest]:
   3.226 +  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
   3.227 +  by auto
   3.228 +
   3.229 +lemma pred_sets_Ball[measurable_dest]:
   3.230 +  "\<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)"
   3.231 +  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
   3.232 +
   3.233 +lemma measurable_finite[measurable (raw)]:
   3.234 +  fixes S :: "'a \<Rightarrow> nat set"
   3.235 +  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
   3.236 +  shows "pred M (\<lambda>x. finite (S x))"
   3.237 +  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
   3.238 +
   3.239 +lemma measurable_Least[measurable]:
   3.240 +  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
   3.241 +  shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
   3.242 +  unfolding measurable_def by (safe intro!: sets_Least) simp_all
   3.243 +
   3.244 +lemma measurable_count_space_insert[measurable (raw)]:
   3.245 +  "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
   3.246 +  by simp
   3.247 +
   3.248 +hide_const (open) pred
   3.249 +
   3.250 +end
     4.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Dec 05 15:58:48 2012 +0100
     4.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Dec 05 15:59:08 2012 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  
     4.5  theory Measure_Space
     4.6  imports
     4.7 -  Sigma_Algebra
     4.8 +  Measurable
     4.9    "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 05 15:58:48 2012 +0100
     5.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 05 15:59:08 2012 +0100
     5.3 @@ -252,7 +252,7 @@
     5.4    "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
     5.5    by (auto simp: algebra_iff_Int)
     5.6  
     5.7 -section {* Restricted algebras *}
     5.8 +subsection {* Restricted algebras *}
     5.9  
    5.10  abbreviation (in algebra)
    5.11    "restricted_space A \<equiv> (op \<inter> A) ` M"
    5.12 @@ -707,7 +707,7 @@
    5.13    qed
    5.14  qed
    5.15  
    5.16 -section "Disjoint families"
    5.17 +subsection "Disjoint families"
    5.18  
    5.19  definition
    5.20    disjoint_family_on  where
    5.21 @@ -866,7 +866,7 @@
    5.22      by (intro disjointD[OF d]) auto
    5.23  qed
    5.24  
    5.25 -section {* Ring generated by a semiring *}
    5.26 +subsection {* Ring generated by a semiring *}
    5.27  
    5.28  definition (in semiring_of_sets)
    5.29    "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
    5.30 @@ -996,7 +996,7 @@
    5.31      by (blast intro!: sigma_sets_mono elim: generated_ringE)
    5.32  qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
    5.33  
    5.34 -section {* Measure type *}
    5.35 +subsection {* Measure type *}
    5.36  
    5.37  definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
    5.38    "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)"
    5.39 @@ -1138,7 +1138,7 @@
    5.40  lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
    5.41    by auto
    5.42  
    5.43 -section {* Constructing simple @{typ "'a measure"} *}
    5.44 +subsection {* Constructing simple @{typ "'a measure"} *}
    5.45  
    5.46  lemma emeasure_measure_of:
    5.47    assumes M: "M = measure_of \<Omega> A \<mu>"
    5.48 @@ -1231,7 +1231,7 @@
    5.49    shows "sigma \<Omega> M = sigma \<Omega> N"
    5.50    by (rule measure_eqI) (simp_all add: emeasure_sigma)
    5.51  
    5.52 -section {* Measurable functions *}
    5.53 +subsection {* Measurable functions *}
    5.54  
    5.55  definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
    5.56    "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
    5.57 @@ -1428,7 +1428,7 @@
    5.58      measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
    5.59    using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
    5.60  
    5.61 -section {* Counting space *}
    5.62 +subsection {* Counting space *}
    5.63  
    5.64  definition count_space :: "'a set \<Rightarrow> 'a measure" where
    5.65    "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
    5.66 @@ -1473,45 +1473,6 @@
    5.67    finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
    5.68  qed
    5.69  
    5.70 -subsection {* Measurable method *}
    5.71 -
    5.72 -lemma (in algebra) sets_Collect_finite_All:
    5.73 -  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
    5.74 -  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
    5.75 -proof -
    5.76 -  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})"
    5.77 -    by auto
    5.78 -  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
    5.79 -qed
    5.80 -
    5.81 -abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
    5.82 -
    5.83 -lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
    5.84 -proof
    5.85 -  assume "pred M P"
    5.86 -  then have "P -` {True} \<inter> space M \<in> sets M"
    5.87 -    by (auto simp: measurable_count_space_eq2)
    5.88 -  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
    5.89 -  finally show "{x\<in>space M. P x} \<in> sets M" .
    5.90 -next
    5.91 -  assume P: "{x\<in>space M. P x} \<in> sets M"
    5.92 -  moreover
    5.93 -  { fix X
    5.94 -    have "X \<in> Pow (UNIV :: bool set)" by simp
    5.95 -    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> {})}"
    5.96 -      unfolding UNIV_bool Pow_insert Pow_empty by auto
    5.97 -    then have "P -` X \<inter> space M \<in> sets M"
    5.98 -      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
    5.99 -  then show "pred M P"
   5.100 -    by (auto simp: measurable_def)
   5.101 -qed
   5.102 -
   5.103 -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))"
   5.104 -  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
   5.105 -
   5.106 -lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
   5.107 -  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
   5.108 -
   5.109  lemma measurable_count_space_const:
   5.110    "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   5.111    by (simp add: measurable_const)
   5.112 @@ -1525,420 +1486,6 @@
   5.113    shows "(\<lambda>x. f (g x)) \<in> measurable M N"
   5.114    using measurable_compose[OF g f] .
   5.115  
   5.116 -ML {*
   5.117 -
   5.118 -structure Measurable =
   5.119 -struct
   5.120 -
   5.121 -datatype level = Concrete | Generic;
   5.122 -
   5.123 -structure Data = Generic_Data
   5.124 -(
   5.125 -  type T = {
   5.126 -    concrete_thms : thm Item_Net.T,
   5.127 -    generic_thms : thm Item_Net.T,
   5.128 -    dest_thms : thm Item_Net.T,
   5.129 -    app_thms : thm Item_Net.T }
   5.130 -  val empty = {
   5.131 -    concrete_thms = Thm.full_rules,
   5.132 -    generic_thms = Thm.full_rules,
   5.133 -    dest_thms = Thm.full_rules,
   5.134 -    app_thms = Thm.full_rules};
   5.135 -  val extend = I;
   5.136 -  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
   5.137 -      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
   5.138 -    concrete_thms = Item_Net.merge (ct1, ct2),
   5.139 -    generic_thms = Item_Net.merge (gt1, gt2),
   5.140 -    dest_thms = Item_Net.merge (dt1, dt2),
   5.141 -    app_thms = Item_Net.merge (at1, at2) };
   5.142 -);
   5.143 -
   5.144 -val debug =
   5.145 -  Attrib.setup_config_bool @{binding measurable_debug} (K false)
   5.146 -
   5.147 -val backtrack =
   5.148 -  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
   5.149 -
   5.150 -val split =
   5.151 -  Attrib.setup_config_bool @{binding measurable_split} (K true)
   5.152 -
   5.153 -fun TAKE n tac = Seq.take n o tac
   5.154 -
   5.155 -fun get lv =
   5.156 -  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
   5.157 -  Data.get o Context.Proof;
   5.158 -
   5.159 -fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
   5.160 -
   5.161 -fun map_data f1 f2 f3 f4
   5.162 -  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
   5.163 -  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
   5.164 -
   5.165 -fun map_concrete_thms f = map_data f I I I
   5.166 -fun map_generic_thms f = map_data I f I I
   5.167 -fun map_dest_thms f = map_data I I f I
   5.168 -fun map_app_thms f = map_data I I I f
   5.169 -
   5.170 -fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
   5.171 -fun add thms' = update (fold Item_Net.update thms');
   5.172 -
   5.173 -val get_dest = Item_Net.content o #dest_thms o Data.get;
   5.174 -val add_dest = Data.map o map_dest_thms o Item_Net.update;
   5.175 -
   5.176 -val get_app = Item_Net.content o #app_thms o Data.get;
   5.177 -val add_app = Data.map o map_app_thms o Item_Net.update;
   5.178 -
   5.179 -fun is_too_generic thm =
   5.180 -  let 
   5.181 -    val concl = concl_of thm
   5.182 -    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
   5.183 -  in is_Var (head_of concl') end
   5.184 -
   5.185 -fun import_theorem ctxt thm = if is_too_generic thm then [] else
   5.186 -  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
   5.187 -
   5.188 -fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
   5.189 -
   5.190 -fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
   5.191 -
   5.192 -fun nth_hol_goal thm i =
   5.193 -  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
   5.194 -
   5.195 -fun dest_measurable_fun t =
   5.196 -  (case t of
   5.197 -    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
   5.198 -  | _ => raise (TERM ("not a measurability predicate", [t])))
   5.199 -
   5.200 -fun is_cond_formula n thm = if length (prems_of thm) < n then false else
   5.201 -  (case nth_hol_goal thm n of
   5.202 -    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
   5.203 -  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
   5.204 -  | _ => true)
   5.205 -  handle TERM _ => true;
   5.206 -
   5.207 -fun indep (Bound i) t b = i < b orelse t <= i
   5.208 -  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
   5.209 -  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   5.210 -  | indep _ _ _ = true;
   5.211 -
   5.212 -fun cnt_prefixes ctxt (Abs (n, T, t)) = let
   5.213 -      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
   5.214 -      fun cnt_walk (Abs (ns, T, t)) Ts =
   5.215 -          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
   5.216 -        | cnt_walk (f $ g) Ts = let
   5.217 -            val n = length Ts - 1
   5.218 -          in
   5.219 -            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
   5.220 -            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
   5.221 -            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
   5.222 -                andalso indep g n 0 andalso g <> Bound n
   5.223 -              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
   5.224 -              else [])
   5.225 -          end
   5.226 -        | cnt_walk _ _ = []
   5.227 -    in map (fn (t1, t2) => let
   5.228 -        val T1 = type_of1 ([T], t2)
   5.229 -        val T2 = type_of1 ([T], t)
   5.230 -      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
   5.231 -        [SOME T1, SOME T, SOME T2])
   5.232 -      end) (cnt_walk t [T])
   5.233 -    end
   5.234 -  | cnt_prefixes _ _ = []
   5.235 -
   5.236 -val split_countable_tac =
   5.237 -  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   5.238 -    let
   5.239 -      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
   5.240 -      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
   5.241 -      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
   5.242 -      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
   5.243 -    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
   5.244 -    handle TERM _ => no_tac) 1)
   5.245 -
   5.246 -fun measurable_tac' ctxt ss facts = let
   5.247 -
   5.248 -    val imported_thms =
   5.249 -      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
   5.250 -
   5.251 -    fun debug_facts msg () =
   5.252 -      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
   5.253 -        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
   5.254 -
   5.255 -    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
   5.256 -
   5.257 -    val split_app_tac =
   5.258 -      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   5.259 -        let
   5.260 -          fun app_prefixes (Abs (n, T, (f $ g))) = let
   5.261 -                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
   5.262 -              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
   5.263 -            | app_prefixes _ = []
   5.264 -
   5.265 -          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
   5.266 -            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
   5.267 -          val thy = Proof_Context.theory_of ctxt
   5.268 -          val tunify = Sign.typ_unify thy
   5.269 -          val thms = map
   5.270 -              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
   5.271 -              (get_app (Context.Proof ctxt))
   5.272 -          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
   5.273 -          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
   5.274 -            let
   5.275 -              val inst =
   5.276 -                (Vartab.empty, ~1)
   5.277 -                |> tunify (T, thmT)
   5.278 -                |> tunify (Tf, thmTf)
   5.279 -                |> tunify (Tc, thmTc)
   5.280 -                |> Vartab.dest o fst
   5.281 -              val subst = subst_TVars (map (apsnd snd) inst)
   5.282 -            in
   5.283 -              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
   5.284 -                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
   5.285 -            end
   5.286 -          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
   5.287 -        in if null cps then no_tac
   5.288 -            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
   5.289 -              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
   5.290 -        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
   5.291 -        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
   5.292 -
   5.293 -    fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
   5.294 -
   5.295 -    val depth_measurable_tac = REPEAT_cnt (fn n =>
   5.296 -       (COND (is_cond_formula 1)
   5.297 -        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ss) 1))
   5.298 -        ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
   5.299 -          (split_app_tac ctxt 1) APPEND
   5.300 -          (splitter 1)))) 0
   5.301 -
   5.302 -  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
   5.303 -
   5.304 -fun measurable_tac ctxt facts =
   5.305 -  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
   5.306 -
   5.307 -val attr_add = Thm.declaration_attribute o add_thm;
   5.308 -
   5.309 -val attr : attribute context_parser =
   5.310 -  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
   5.311 -     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
   5.312 -
   5.313 -val dest_attr : attribute context_parser =
   5.314 -  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
   5.315 -
   5.316 -val app_attr : attribute context_parser =
   5.317 -  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
   5.318 -
   5.319 -val method : (Proof.context -> Method.method) context_parser =
   5.320 -  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
   5.321 -
   5.322 -fun simproc ss redex = let
   5.323 -    val ctxt = Simplifier.the_context ss;
   5.324 -    val t = HOLogic.mk_Trueprop (term_of redex);
   5.325 -    fun tac {context = ctxt, prems = _ } =
   5.326 -      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
   5.327 -  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
   5.328 -
   5.329 -end
   5.330 -
   5.331 -*}
   5.332 -
   5.333 -attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
   5.334 -attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
   5.335 -attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
   5.336 -method_setup measurable = {* Measurable.method *} "measurability prover"
   5.337 -simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
   5.338 -
   5.339 -declare
   5.340 -  measurable_compose_rev[measurable_dest]
   5.341 -  pred_sets1[measurable_dest]
   5.342 -  pred_sets2[measurable_dest]
   5.343 -  sets.sets_into_space[measurable_dest]
   5.344 -
   5.345 -declare
   5.346 -  sets.top[measurable]
   5.347 -  sets.empty_sets[measurable (raw)]
   5.348 -  sets.Un[measurable (raw)]
   5.349 -  sets.Diff[measurable (raw)]
   5.350 -
   5.351 -declare
   5.352 -  measurable_count_space[measurable (raw)]
   5.353 -  measurable_ident[measurable (raw)]
   5.354 -  measurable_ident_sets[measurable (raw)]
   5.355 -  measurable_const[measurable (raw)]
   5.356 -  measurable_If[measurable (raw)]
   5.357 -  measurable_comp[measurable (raw)]
   5.358 -  measurable_sets[measurable (raw)]
   5.359 -
   5.360 -lemma predE[measurable (raw)]: 
   5.361 -  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
   5.362 -  unfolding pred_def .
   5.363 -
   5.364 -lemma pred_intros_imp'[measurable (raw)]:
   5.365 -  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
   5.366 -  by (cases K) auto
   5.367 -
   5.368 -lemma pred_intros_conj1'[measurable (raw)]:
   5.369 -  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
   5.370 -  by (cases K) auto
   5.371 -
   5.372 -lemma pred_intros_conj2'[measurable (raw)]:
   5.373 -  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
   5.374 -  by (cases K) auto
   5.375 -
   5.376 -lemma pred_intros_disj1'[measurable (raw)]:
   5.377 -  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
   5.378 -  by (cases K) auto
   5.379 -
   5.380 -lemma pred_intros_disj2'[measurable (raw)]:
   5.381 -  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
   5.382 -  by (cases K) auto
   5.383 -
   5.384 -lemma pred_intros_logic[measurable (raw)]:
   5.385 -  "pred M (\<lambda>x. x \<in> space M)"
   5.386 -  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
   5.387 -  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
   5.388 -  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
   5.389 -  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
   5.390 -  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
   5.391 -  "pred M (\<lambda>x. f x \<in> UNIV)"
   5.392 -  "pred M (\<lambda>x. f x \<in> {})"
   5.393 -  "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
   5.394 -  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
   5.395 -  "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))"
   5.396 -  "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))"
   5.397 -  "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))"
   5.398 -  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
   5.399 -  by (auto simp: iff_conv_conj_imp pred_def)
   5.400 -
   5.401 -lemma pred_intros_countable[measurable (raw)]:
   5.402 -  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
   5.403 -  shows 
   5.404 -    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
   5.405 -    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
   5.406 -  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
   5.407 -
   5.408 -lemma pred_intros_countable_bounded[measurable (raw)]:
   5.409 -  fixes X :: "'i :: countable set"
   5.410 -  shows 
   5.411 -    "(\<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))"
   5.412 -    "(\<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))"
   5.413 -    "(\<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)"
   5.414 -    "(\<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)"
   5.415 -  by (auto simp: Bex_def Ball_def)
   5.416 -
   5.417 -lemma pred_intros_finite[measurable (raw)]:
   5.418 -  "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))"
   5.419 -  "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))"
   5.420 -  "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)"
   5.421 -  "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)"
   5.422 -  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
   5.423 -
   5.424 -lemma countable_Un_Int[measurable (raw)]:
   5.425 -  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
   5.426 -  "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"
   5.427 -  by auto
   5.428 -
   5.429 -declare
   5.430 -  finite_UN[measurable (raw)]
   5.431 -  finite_INT[measurable (raw)]
   5.432 -
   5.433 -lemma sets_Int_pred[measurable (raw)]:
   5.434 -  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
   5.435 -  shows "A \<inter> B \<in> sets M"
   5.436 -proof -
   5.437 -  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
   5.438 -  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
   5.439 -    using space by auto
   5.440 -  finally show ?thesis .
   5.441 -qed
   5.442 -
   5.443 -lemma [measurable (raw generic)]:
   5.444 -  assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
   5.445 -  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
   5.446 -    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
   5.447 -proof -
   5.448 -  show "pred M (\<lambda>x. f x = c)"
   5.449 -  proof cases
   5.450 -    assume "c \<in> space N"
   5.451 -    with measurable_sets[OF f c] show ?thesis
   5.452 -      by (auto simp: Int_def conj_commute pred_def)
   5.453 -  next
   5.454 -    assume "c \<notin> space N"
   5.455 -    with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
   5.456 -    then show ?thesis by (auto simp: pred_def cong: conj_cong)
   5.457 -  qed
   5.458 -  then show "pred M (\<lambda>x. c = f x)"
   5.459 -    by (simp add: eq_commute)
   5.460 -qed
   5.461 -
   5.462 -lemma pred_le_const[measurable (raw generic)]:
   5.463 -  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
   5.464 -  using measurable_sets[OF f c]
   5.465 -  by (auto simp: Int_def conj_commute eq_commute pred_def)
   5.466 -
   5.467 -lemma pred_const_le[measurable (raw generic)]:
   5.468 -  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
   5.469 -  using measurable_sets[OF f c]
   5.470 -  by (auto simp: Int_def conj_commute eq_commute pred_def)
   5.471 -
   5.472 -lemma pred_less_const[measurable (raw generic)]:
   5.473 -  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
   5.474 -  using measurable_sets[OF f c]
   5.475 -  by (auto simp: Int_def conj_commute eq_commute pred_def)
   5.476 -
   5.477 -lemma pred_const_less[measurable (raw generic)]:
   5.478 -  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
   5.479 -  using measurable_sets[OF f c]
   5.480 -  by (auto simp: Int_def conj_commute eq_commute pred_def)
   5.481 -
   5.482 -declare
   5.483 -  sets.Int[measurable (raw)]
   5.484 -
   5.485 -lemma pred_in_If[measurable (raw)]:
   5.486 -  "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
   5.487 -    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
   5.488 -  by auto
   5.489 -
   5.490 -lemma sets_range[measurable_dest]:
   5.491 -  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
   5.492 -  by auto
   5.493 -
   5.494 -lemma pred_sets_range[measurable_dest]:
   5.495 -  "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)"
   5.496 -  using pred_sets2[OF sets_range] by auto
   5.497 -
   5.498 -lemma sets_All[measurable_dest]:
   5.499 -  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
   5.500 -  by auto
   5.501 -
   5.502 -lemma pred_sets_All[measurable_dest]:
   5.503 -  "\<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)"
   5.504 -  using pred_sets2[OF sets_All, of A N f] by auto
   5.505 -
   5.506 -lemma sets_Ball[measurable_dest]:
   5.507 -  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
   5.508 -  by auto
   5.509 -
   5.510 -lemma pred_sets_Ball[measurable_dest]:
   5.511 -  "\<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)"
   5.512 -  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
   5.513 -
   5.514 -lemma measurable_finite[measurable (raw)]:
   5.515 -  fixes S :: "'a \<Rightarrow> nat set"
   5.516 -  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
   5.517 -  shows "pred M (\<lambda>x. finite (S x))"
   5.518 -  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
   5.519 -
   5.520 -lemma measurable_Least[measurable]:
   5.521 -  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
   5.522 -  shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
   5.523 -  unfolding measurable_def by (safe intro!: sets_Least) simp_all
   5.524 -
   5.525 -lemma measurable_count_space_insert[measurable (raw)]:
   5.526 -  "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
   5.527 -  by simp
   5.528 -
   5.529 -hide_const (open) pred
   5.530  
   5.531  subsection {* Extend measure *}
   5.532  
   5.533 @@ -2365,7 +1912,7 @@
   5.534      by blast
   5.535  qed
   5.536  
   5.537 -section {* Dynkin systems *}
   5.538 +subsection {* Dynkin systems *}
   5.539  
   5.540  locale dynkin_system = subset_class +
   5.541    assumes space: "\<Omega> \<in> M"
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Probability/measurable.ML	Wed Dec 05 15:59:08 2012 +0100
     6.3 @@ -0,0 +1,238 @@
     6.4 +(*  Title:      HOL/Probability/measurable.ML
     6.5 +    Author:     Johannes Hölzl <hoelzl@in.tum.de>
     6.6 +
     6.7 +Measurability prover.
     6.8 +*)
     6.9 +
    6.10 +signature MEASURABLE = 
    6.11 +sig
    6.12 +  datatype level = Concrete | Generic
    6.13 +
    6.14 +  val simproc : simpset -> cterm -> thm option
    6.15 +  val method : (Proof.context -> Method.method) context_parser
    6.16 +  val measurable_tac : Proof.context -> thm list -> tactic
    6.17 +
    6.18 +  val attr : attribute context_parser
    6.19 +  val dest_attr : attribute context_parser
    6.20 +  val app_attr : attribute context_parser
    6.21 +
    6.22 +  val get : level -> Proof.context -> thm list
    6.23 +  val get_all : Proof.context -> thm list
    6.24 +
    6.25 +  val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
    6.26 +
    6.27 +end ;
    6.28 +
    6.29 +structure Measurable : MEASURABLE =
    6.30 +struct
    6.31 +
    6.32 +datatype level = Concrete | Generic;
    6.33 +
    6.34 +structure Data = Generic_Data
    6.35 +(
    6.36 +  type T = {
    6.37 +    concrete_thms : thm Item_Net.T,
    6.38 +    generic_thms : thm Item_Net.T,
    6.39 +    dest_thms : thm Item_Net.T,
    6.40 +    app_thms : thm Item_Net.T }
    6.41 +  val empty = {
    6.42 +    concrete_thms = Thm.full_rules,
    6.43 +    generic_thms = Thm.full_rules,
    6.44 +    dest_thms = Thm.full_rules,
    6.45 +    app_thms = Thm.full_rules};
    6.46 +  val extend = I;
    6.47 +  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
    6.48 +      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
    6.49 +    concrete_thms = Item_Net.merge (ct1, ct2),
    6.50 +    generic_thms = Item_Net.merge (gt1, gt2),
    6.51 +    dest_thms = Item_Net.merge (dt1, dt2),
    6.52 +    app_thms = Item_Net.merge (at1, at2) };
    6.53 +);
    6.54 +
    6.55 +val debug =
    6.56 +  Attrib.setup_config_bool @{binding measurable_debug} (K false)
    6.57 +
    6.58 +val backtrack =
    6.59 +  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
    6.60 +
    6.61 +val split =
    6.62 +  Attrib.setup_config_bool @{binding measurable_split} (K true)
    6.63 +
    6.64 +fun TAKE n tac = Seq.take n o tac
    6.65 +
    6.66 +fun get lv =
    6.67 +  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
    6.68 +  Data.get o Context.Proof;
    6.69 +
    6.70 +fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
    6.71 +
    6.72 +fun map_data f1 f2 f3 f4
    6.73 +  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
    6.74 +  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
    6.75 +
    6.76 +fun map_concrete_thms f = map_data f I I I
    6.77 +fun map_generic_thms f = map_data I f I I
    6.78 +fun map_dest_thms f = map_data I I f I
    6.79 +fun map_app_thms f = map_data I I I f
    6.80 +
    6.81 +fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
    6.82 +fun add thms' = update (fold Item_Net.update thms');
    6.83 +
    6.84 +val get_dest = Item_Net.content o #dest_thms o Data.get;
    6.85 +val add_dest = Data.map o map_dest_thms o Item_Net.update;
    6.86 +
    6.87 +val get_app = Item_Net.content o #app_thms o Data.get;
    6.88 +val add_app = Data.map o map_app_thms o Item_Net.update;
    6.89 +
    6.90 +fun is_too_generic thm =
    6.91 +  let 
    6.92 +    val concl = concl_of thm
    6.93 +    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
    6.94 +  in is_Var (head_of concl') end
    6.95 +
    6.96 +fun import_theorem ctxt thm = if is_too_generic thm then [] else
    6.97 +  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
    6.98 +
    6.99 +fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
   6.100 +
   6.101 +fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
   6.102 +
   6.103 +fun nth_hol_goal thm i =
   6.104 +  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
   6.105 +
   6.106 +fun dest_measurable_fun t =
   6.107 +  (case t of
   6.108 +    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
   6.109 +  | _ => raise (TERM ("not a measurability predicate", [t])))
   6.110 +
   6.111 +fun is_cond_formula n thm = if length (prems_of thm) < n then false else
   6.112 +  (case nth_hol_goal thm n of
   6.113 +    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
   6.114 +  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
   6.115 +  | _ => true)
   6.116 +  handle TERM _ => true;
   6.117 +
   6.118 +fun indep (Bound i) t b = i < b orelse t <= i
   6.119 +  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
   6.120 +  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   6.121 +  | indep _ _ _ = true;
   6.122 +
   6.123 +fun cnt_prefixes ctxt (Abs (n, T, t)) = let
   6.124 +      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
   6.125 +      fun cnt_walk (Abs (ns, T, t)) Ts =
   6.126 +          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
   6.127 +        | cnt_walk (f $ g) Ts = let
   6.128 +            val n = length Ts - 1
   6.129 +          in
   6.130 +            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
   6.131 +            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
   6.132 +            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
   6.133 +                andalso indep g n 0 andalso g <> Bound n
   6.134 +              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
   6.135 +              else [])
   6.136 +          end
   6.137 +        | cnt_walk _ _ = []
   6.138 +    in map (fn (t1, t2) => let
   6.139 +        val T1 = type_of1 ([T], t2)
   6.140 +        val T2 = type_of1 ([T], t)
   6.141 +      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
   6.142 +        [SOME T1, SOME T, SOME T2])
   6.143 +      end) (cnt_walk t [T])
   6.144 +    end
   6.145 +  | cnt_prefixes _ _ = []
   6.146 +
   6.147 +val split_countable_tac =
   6.148 +  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   6.149 +    let
   6.150 +      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
   6.151 +      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
   6.152 +      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
   6.153 +      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
   6.154 +    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
   6.155 +    handle TERM _ => no_tac) 1)
   6.156 +
   6.157 +fun measurable_tac' ctxt ss facts = let
   6.158 +
   6.159 +    val imported_thms =
   6.160 +      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
   6.161 +
   6.162 +    fun debug_facts msg () =
   6.163 +      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
   6.164 +        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
   6.165 +
   6.166 +    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
   6.167 +
   6.168 +    val split_app_tac =
   6.169 +      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   6.170 +        let
   6.171 +          fun app_prefixes (Abs (n, T, (f $ g))) = let
   6.172 +                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
   6.173 +              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
   6.174 +            | app_prefixes _ = []
   6.175 +
   6.176 +          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
   6.177 +            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
   6.178 +          val thy = Proof_Context.theory_of ctxt
   6.179 +          val tunify = Sign.typ_unify thy
   6.180 +          val thms = map
   6.181 +              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
   6.182 +              (get_app (Context.Proof ctxt))
   6.183 +          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
   6.184 +          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
   6.185 +            let
   6.186 +              val inst =
   6.187 +                (Vartab.empty, ~1)
   6.188 +                |> tunify (T, thmT)
   6.189 +                |> tunify (Tf, thmTf)
   6.190 +                |> tunify (Tc, thmTc)
   6.191 +                |> Vartab.dest o fst
   6.192 +              val subst = subst_TVars (map (apsnd snd) inst)
   6.193 +            in
   6.194 +              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
   6.195 +                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
   6.196 +            end
   6.197 +          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
   6.198 +        in if null cps then no_tac
   6.199 +            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
   6.200 +              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
   6.201 +        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
   6.202 +        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
   6.203 +
   6.204 +    fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
   6.205 +
   6.206 +    val depth_measurable_tac = REPEAT_cnt (fn n =>
   6.207 +       (COND (is_cond_formula 1)
   6.208 +        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ss) 1))
   6.209 +        ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
   6.210 +          (split_app_tac ctxt 1) APPEND
   6.211 +          (splitter 1)))) 0
   6.212 +
   6.213 +  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
   6.214 +
   6.215 +fun measurable_tac ctxt facts =
   6.216 +  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
   6.217 +
   6.218 +val attr_add = Thm.declaration_attribute o add_thm;
   6.219 +
   6.220 +val attr : attribute context_parser =
   6.221 +  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
   6.222 +     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
   6.223 +
   6.224 +val dest_attr : attribute context_parser =
   6.225 +  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
   6.226 +
   6.227 +val app_attr : attribute context_parser =
   6.228 +  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
   6.229 +
   6.230 +val method : (Proof.context -> Method.method) context_parser =
   6.231 +  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
   6.232 +
   6.233 +fun simproc ss redex = let
   6.234 +    val ctxt = Simplifier.the_context ss;
   6.235 +    val t = HOLogic.mk_Trueprop (term_of redex);
   6.236 +    fun tac {context = ctxt, prems = _ } =
   6.237 +      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
   6.238 +  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
   6.239 +
   6.240 +end
   6.241 +