--- 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)]:
--- 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
--- /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
--- 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
--- 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"
--- /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
+