--- a/NEWS Fri Nov 09 19:16:31 2012 +0100
+++ b/NEWS Fri Nov 09 19:21:47 2012 +0100
@@ -207,6 +207,9 @@
* Simproc "finite_Collect" rewrites set comprehensions into pointfree
expressions.
+* Preprocessing of the code generator rewrites set comprehensions into
+pointfree expressions.
+
* Quickcheck:
- added an optimisation for equality premises.
--- a/src/HOL/Algebra/Divisibility.thy Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Fri Nov 09 19:21:47 2012 +0100
@@ -244,7 +244,7 @@
apply (elim dividesE, intro dividesI, assumption)
apply (rule l_cancel[of c])
apply (simp add: m_assoc carr)+
-apply (fast intro: divides_mult_lI carr)
+apply (fast intro: carr)
done
lemma (in comm_monoid) divides_mult_rI [intro]:
--- a/src/HOL/Library/Permutation.thy Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Library/Permutation.thy Fri Nov 09 19:21:47 2012 +0100
@@ -193,7 +193,7 @@
show ?case
proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
- by (auto simp: bij_betw_def bij_betw_swap_iff)
+ by (auto simp: bij_betw_def)
fix i assume "i < length(y#x#l)"
show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
--- a/src/HOL/Old_Number_Theory/Primes.thy Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy Fri Nov 09 19:21:47 2012 +0100
@@ -24,7 +24,7 @@
lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1"
apply (auto simp add: prime_def)
- apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
+ apply (metis gcd_dvd1 gcd_dvd2)
done
text {*
--- a/src/HOL/Probability/Finite_Product_Measure.thy Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Fri Nov 09 19:21:47 2012 +0100
@@ -43,6 +43,15 @@
"extensional I \<inter> extensional I' = extensional (I \<inter> I')"
unfolding extensional_def by auto
+lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
+ by (auto simp: extensional_def)
+
+lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
+ unfolding restrict_def extensional_def by auto
+
+lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
+ unfolding restrict_def by (simp add: fun_eq_iff)
+
definition
"merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
@@ -85,6 +94,33 @@
"J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
by (auto simp: restrict_def)
+lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
+ unfolding merge_def by auto
+
+lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
+ unfolding merge_def extensional_def by auto
+
+lemma injective_vimage_restrict:
+ assumes J: "J \<subseteq> I"
+ and sets: "A \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" and ne: "(\<Pi>\<^isub>E i\<in>I. S i) \<noteq> {}"
+ and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i) = (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
+ shows "A = B"
+proof (intro set_eqI)
+ fix x
+ from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
+ have "J \<inter> (I - J) = {}" by auto
+ show "x \<in> A \<longleftrightarrow> x \<in> B"
+ proof cases
+ assume x: "x \<in> (\<Pi>\<^isub>E i\<in>J. S i)"
+ have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
+ using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub split: split_merge)
+ then show "x \<in> A \<longleftrightarrow> x \<in> B"
+ using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub eq split: split_merge)
+ next
+ assume "x \<notin> (\<Pi>\<^isub>E i\<in>J. S i)" with sets show "x \<in> A \<longleftrightarrow> x \<in> B" by auto
+ qed
+qed
+
lemma extensional_insert_undefined[intro, simp]:
assumes "a \<in> extensional (insert i I)"
shows "a(i := undefined) \<in> extensional I"
@@ -253,6 +289,24 @@
lemma prod_emb_PiE_same_index[simp]: "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^isub>E I E) = Pi\<^isub>E I E"
by (auto simp: prod_emb_def Pi_iff)
+lemma prod_emb_trans[simp]:
+ "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
+ by (auto simp add: Int_absorb1 prod_emb_def)
+
+lemma prod_emb_Pi:
+ assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
+ shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
+ using assms space_closed
+ by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
+
+lemma prod_emb_id:
+ "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
+ by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
+
+lemma prod_emb_mono:
+ "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
+ by (auto simp: prod_emb_def)
+
definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
"PiM I M = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
{(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
@@ -309,6 +363,17 @@
\<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
by (auto simp: prod_algebra_def Pi_iff)
+lemma prod_algebraI_finite:
+ "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
+ using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
+
+lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
+proof (safe intro!: Int_stableI)
+ fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
+ then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
+ by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
+qed
+
lemma prod_algebraE:
assumes A: "A \<in> prod_algebra I M"
obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
@@ -546,6 +611,14 @@
using A X by (auto intro!: measurable_sets)
qed (insert X, auto dest: measurable_space)
+lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
+ by (intro measurable_restrict measurable_component_singleton) auto
+
+lemma measurable_prod_emb[intro, simp]:
+ "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
+ unfolding prod_emb_def space_PiM[symmetric]
+ by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
+
lemma sets_in_Pi_aux:
"finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
{x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Fri Nov 09 19:21:47 2012 +0100
@@ -5,78 +5,9 @@
header {*Infinite Product Measure*}
theory Infinite_Product_Measure
- imports Probability_Measure Caratheodory
+ imports Probability_Measure Caratheodory Projective_Family
begin
-lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
- by (auto simp: extensional_def)
-
-lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
- unfolding restrict_def extensional_def by auto
-
-lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
- unfolding restrict_def by (simp add: fun_eq_iff)
-
-lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
- unfolding merge_def by auto
-
-lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
- unfolding merge_def extensional_def by auto
-
-lemma injective_vimage_restrict:
- assumes J: "J \<subseteq> I"
- and sets: "A \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" and ne: "(\<Pi>\<^isub>E i\<in>I. S i) \<noteq> {}"
- and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i) = (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
- shows "A = B"
-proof (intro set_eqI)
- fix x
- from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
- have "J \<inter> (I - J) = {}" by auto
- show "x \<in> A \<longleftrightarrow> x \<in> B"
- proof cases
- assume x: "x \<in> (\<Pi>\<^isub>E i\<in>J. S i)"
- have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
- using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub split: split_merge)
- then show "x \<in> A \<longleftrightarrow> x \<in> B"
- using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub eq split: split_merge)
- next
- assume "x \<notin> (\<Pi>\<^isub>E i\<in>J. S i)" with sets show "x \<in> A \<longleftrightarrow> x \<in> B" by auto
- qed
-qed
-
-lemma prod_algebraI_finite:
- "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
- using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
-
-lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
-proof (safe intro!: Int_stableI)
- fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
- then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
- by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
-qed
-
-lemma prod_emb_trans[simp]:
- "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
- by (auto simp add: Int_absorb1 prod_emb_def)
-
-lemma prod_emb_Pi:
- assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
- shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
- using assms space_closed
- by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
-
-lemma prod_emb_id:
- "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
- by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
-
-lemma measurable_prod_emb[intro, simp]:
- "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
- unfolding prod_emb_def space_PiM[symmetric]
- by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
-
-lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
- by (intro measurable_restrict measurable_component_singleton) auto
-
lemma (in product_prob_space) distr_restrict:
assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
@@ -118,200 +49,27 @@
by (auto intro!: measurable_restrict_subset simp: space_PiM)
qed
-abbreviation (in product_prob_space)
- "emb L K X \<equiv> prod_emb L M K X"
-
lemma (in product_prob_space) emeasure_prod_emb[simp]:
assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
- shows "emeasure (Pi\<^isub>M L M) (emb L J X) = emeasure (Pi\<^isub>M J M) X"
+ shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
by (subst distr_restrict[OF L])
(simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
-lemma (in product_prob_space) prod_emb_injective:
- assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
- assumes "prod_emb L M J X = prod_emb L M J Y"
- shows "X = Y"
-proof (rule injective_vimage_restrict)
- show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
- using sets[THEN sets_into_space] by (auto simp: space_PiM)
- have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
- using M.not_empty by auto
- from bchoice[OF this]
- show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
- show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
- using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
-qed fact
-
-definition (in product_prob_space) generator :: "('i \<Rightarrow> 'a) set set" where
- "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
-
-lemma (in product_prob_space) generatorI':
- "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> generator"
- unfolding generator_def by auto
-
-lemma (in product_prob_space) algebra_generator:
- assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
- unfolding algebra_def algebra_axioms_def ring_of_sets_iff
-proof (intro conjI ballI)
- let ?G = generator
- show "?G \<subseteq> Pow ?\<Omega>"
- by (auto simp: generator_def prod_emb_def)
- from `I \<noteq> {}` obtain i where "i \<in> I" by auto
- then show "{} \<in> ?G"
- by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
- simp: sigma_sets.Empty generator_def prod_emb_def)
- from `i \<in> I` show "?\<Omega> \<in> ?G"
- by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"]
- simp: generator_def prod_emb_def)
- fix A assume "A \<in> ?G"
- then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA"
- by (auto simp: generator_def)
- fix B assume "B \<in> ?G"
- then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB"
- by (auto simp: generator_def)
- let ?RA = "emb (JA \<union> JB) JA XA"
- let ?RB = "emb (JA \<union> JB) JB XB"
- have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
- using XA A XB B by auto
- show "A - B \<in> ?G" "A \<union> B \<in> ?G"
- unfolding * using XA XB by (safe intro!: generatorI') auto
-qed
-
-lemma (in product_prob_space) sets_PiM_generator:
- "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
-proof cases
- assume "I = {}" then show ?thesis
- unfolding generator_def
- by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong)
-next
- assume "I \<noteq> {}"
- show ?thesis
- proof
- show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
- unfolding sets_PiM
- proof (safe intro!: sigma_sets_subseteq)
- fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
- by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
- qed
- qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
-qed
-
-
-lemma (in product_prob_space) generatorI:
- "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
- unfolding generator_def by auto
-
-definition (in product_prob_space)
- "\<mu>G A =
- (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (Pi\<^isub>M J M) X))"
-
-lemma (in product_prob_space) \<mu>G_spec:
- assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
- shows "\<mu>G A = emeasure (Pi\<^isub>M J M) X"
- unfolding \<mu>G_def
-proof (intro the_equality allI impI ballI)
- fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)"
- have "emeasure (Pi\<^isub>M K M) Y = emeasure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) K Y)"
- using K J by simp
- also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
- using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
- also have "emeasure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) J X) = emeasure (Pi\<^isub>M J M) X"
- using K J by simp
- finally show "emeasure (Pi\<^isub>M J M) X = emeasure (Pi\<^isub>M K M) Y" ..
-qed (insert J, force)
+sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
+proof
+ fix J::"'i set" assume "finite J"
+ interpret f: finite_product_prob_space M J proof qed fact
+ show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
+ show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
+ (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
+ (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
+ by (auto simp add: sigma_finite_measure_def)
+ show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
+qed simp_all
-lemma (in product_prob_space) \<mu>G_eq:
- "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (Pi\<^isub>M J M) X"
- by (intro \<mu>G_spec) auto
-
-lemma (in product_prob_space) generator_Ex:
- assumes *: "A \<in> generator"
- shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (Pi\<^isub>M J M) X"
-proof -
- from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
- unfolding generator_def by auto
- with \<mu>G_spec[OF this] show ?thesis by auto
-qed
-
-lemma (in product_prob_space) generatorE:
- assumes A: "A \<in> generator"
- obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (Pi\<^isub>M J M) X"
-proof -
- from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
- "\<mu>G A = emeasure (Pi\<^isub>M J M) X" by auto
- then show thesis by (intro that) auto
-qed
-
-lemma (in product_prob_space) merge_sets:
- "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
- by simp
-
-lemma (in product_prob_space) merge_emb:
- assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
- shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
- emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
-proof -
- have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)"
- by (auto simp: restrict_def merge_def)
- have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)"
- by (auto simp: restrict_def merge_def)
- have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto
- have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
- have [simp]: "(K - J) \<inter> K = K - J" by auto
- from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
- by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
- auto
-qed
-
-lemma (in product_prob_space) positive_\<mu>G:
- assumes "I \<noteq> {}"
- shows "positive generator \<mu>G"
-proof -
- interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
- show ?thesis
- proof (intro positive_def[THEN iffD2] conjI ballI)
- from generatorE[OF G.empty_sets] guess J X . note this[simp]
- interpret J: finite_product_sigma_finite M J by default fact
- have "X = {}"
- by (rule prod_emb_injective[of J I]) simp_all
- then show "\<mu>G {} = 0" by simp
- next
- fix A assume "A \<in> generator"
- from generatorE[OF this] guess J X . note this[simp]
- interpret J: finite_product_sigma_finite M J by default fact
- show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
- qed
-qed
-
-lemma (in product_prob_space) additive_\<mu>G:
- assumes "I \<noteq> {}"
- shows "additive generator \<mu>G"
-proof -
- interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
- show ?thesis
- proof (intro additive_def[THEN iffD2] ballI impI)
- fix A assume "A \<in> generator" with generatorE guess J X . note J = this
- fix B assume "B \<in> generator" with generatorE guess K Y . note K = this
- assume "A \<inter> B = {}"
- have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
- using J K by auto
- interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
- have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
- apply (rule prod_emb_injective[of "J \<union> K" I])
- apply (insert `A \<inter> B = {}` JK J K)
- apply (simp_all add: Int prod_emb_Int)
- done
- have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
- using J K by simp_all
- then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
- by simp
- also have "\<dots> = emeasure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
- using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
- also have "\<dots> = \<mu>G A + \<mu>G B"
- using J K JK_disj by (simp add: plus_emeasure[symmetric])
- finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
- qed
-qed
+lemma (in product_prob_space) PiP_PiM_finite[simp]:
+ assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
+ using assms by (simp add: PiP_finite)
lemma (in product_prob_space) emeasure_PiM_emb_not_empty:
assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. X i \<in> sets (M i)"
@@ -337,7 +95,6 @@
ultimately have K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "X \<in> sets (Pi\<^isub>M K M)" "Z = emb I K X"
"K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = emeasure (Pi\<^isub>M K M) X"
by (auto simp: subset_insertI)
-
let ?M = "\<lambda>y. (\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
{ fix y assume y: "y \<in> space (Pi\<^isub>M J M)"
note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
@@ -402,7 +159,7 @@
using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
ultimately have "0 < ?a" by auto
- have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (Pi\<^isub>M J M) X"
+ have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (PiP J M (\<lambda>J. (Pi\<^isub>M J M))) X"
using A by (intro allI generator_Ex) auto
then obtain J' X' where J': "\<And>n. J' n \<noteq> {}" "\<And>n. finite (J' n)" "\<And>n. J' n \<subseteq> I" "\<And>n. X' n \<in> sets (Pi\<^isub>M (J' n) M)"
and A': "\<And>n. A n = emb I (J' n) (X' n)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Projective_Family.thy Fri Nov 09 19:21:47 2012 +0100
@@ -0,0 +1,300 @@
+(* Title: HOL/Probability/Projective_Family.thy
+ Author: Fabian Immler, TU München
+ Author: Johannes Hölzl, TU München
+*)
+
+header {*Projective Family*}
+
+theory Projective_Family
+imports Finite_Product_Measure Probability_Measure
+begin
+
+definition
+ PiP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
+ "PiP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
+ {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
+ (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j))
+ (\<lambda>(J, X). emeasure (P J) (Pi\<^isub>E J X))"
+
+lemma space_PiP[simp]: "space (PiP I M P) = space (PiM I M)"
+ by (auto simp add: PiP_def space_PiM prod_emb_def intro!: space_extend_measure)
+
+lemma sets_PiP[simp]: "sets (PiP I M P) = sets (PiM I M)"
+ by (auto simp add: PiP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure)
+
+lemma measurable_PiP1[simp]: "measurable (PiP I M P) M' = measurable (\<Pi>\<^isub>M i\<in>I. M i) M'"
+ unfolding measurable_def by auto
+
+lemma measurable_PiP2[simp]: "measurable M' (PiP I M P) = measurable M' (\<Pi>\<^isub>M i\<in>I. M i)"
+ unfolding measurable_def by auto
+
+locale projective_family =
+ fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)"
+ assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow>
+ (P H) (prod_emb H M J X) = (P J) X"
+ assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
+ assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
+ assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
+begin
+
+lemma emeasure_PiP:
+ assumes "finite J"
+ assumes "J \<subseteq> I"
+ assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)"
+ shows "emeasure (PiP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
+proof -
+ have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
+ proof safe
+ fix x j assume "x \<in> Pi J (restrict A J)" "j \<in> J"
+ hence "x j \<in> restrict A J j" by (auto simp: Pi_def)
+ also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto
+ finally show "x j \<in> space (M j)" .
+ qed
+ hence "emeasure (PiP J M P) (Pi\<^isub>E J A) =
+ emeasure (PiP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
+ using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def)
+ also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
+ proof (rule emeasure_extend_measure_Pair[OF PiP_def])
+ show "positive (sets (PiP J M P)) (P J)" unfolding positive_def by auto
+ show "countably_additive (sets (PiP J M P)) (P J)" unfolding countably_additive_def
+ by (auto simp: suminf_emeasure proj_sets[OF `finite J`])
+ show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))"
+ using assms by auto
+ fix K and X::"'i \<Rightarrow> 'a set"
+ show "prod_emb J M K (Pi\<^isub>E K X) \<in> Pow (\<Pi>\<^isub>E i\<in>J. space (M i))"
+ by (auto simp: prod_emb_def)
+ assume JX: "(K \<noteq> {} \<or> J = {}) \<and> finite K \<and> K \<subseteq> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))"
+ thus "emeasure (P J) (prod_emb J M K (Pi\<^isub>E K X)) = emeasure (P K) (Pi\<^isub>E K X)"
+ using assms
+ apply (cases "J = {}")
+ apply (simp add: prod_emb_id)
+ apply (fastforce simp add: intro!: projective sets_PiM_I_finite)
+ done
+ qed
+ finally show ?thesis .
+qed
+
+lemma PiP_finite:
+ assumes "finite J"
+ assumes "J \<subseteq> I"
+ shows "PiP J M P = P J" (is "?P = _")
+proof (rule measure_eqI_generator_eq)
+ let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
+ let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
+ let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
+ show "Int_stable ?J"
+ by (rule Int_stable_PiE)
+ interpret prob_space "P J" using prob_space `finite J` by simp
+ show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_PiP)
+ show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
+ show "sets (PiP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
+ using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
+ fix X assume "X \<in> ?J"
+ then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
+ with `finite J` have "X \<in> sets (PiP J M P)" by simp
+ have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E"
+ using E sets_into_space
+ by (auto intro!: prod_emb_PiE_same_index)
+ show "emeasure (PiP J M P) X = emeasure (P J) X"
+ unfolding X using E
+ by (intro emeasure_PiP assms) simp
+qed (insert `finite J`, auto intro!: prod_algebraI_finite)
+
+lemma emeasure_fun_emb[simp]:
+ assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
+ shows "emeasure (PiP L M P) (prod_emb L M J X) = emeasure (PiP J M P) X"
+ using assms
+ by (subst PiP_finite) (auto simp: PiP_finite finite_subset projective)
+
+lemma prod_emb_injective:
+ assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
+ assumes "prod_emb L M J X = prod_emb L M J Y"
+ shows "X = Y"
+proof (rule injective_vimage_restrict)
+ show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
+ using sets[THEN sets_into_space] by (auto simp: space_PiM)
+ have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
+ proof
+ fix i assume "i \<in> L"
+ interpret prob_space "P {i}" using prob_space by simp
+ from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
+ qed
+ from bchoice[OF this]
+ show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
+ show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
+ using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
+qed fact
+
+abbreviation
+ "emb L K X \<equiv> prod_emb L M K X"
+
+definition generator :: "('i \<Rightarrow> 'a) set set" where
+ "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
+
+lemma generatorI':
+ "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> generator"
+ unfolding generator_def by auto
+
+lemma algebra_generator:
+ assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
+ unfolding algebra_def algebra_axioms_def ring_of_sets_iff
+proof (intro conjI ballI)
+ let ?G = generator
+ show "?G \<subseteq> Pow ?\<Omega>"
+ by (auto simp: generator_def prod_emb_def)
+ from `I \<noteq> {}` obtain i where "i \<in> I" by auto
+ then show "{} \<in> ?G"
+ by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
+ simp: sigma_sets.Empty generator_def prod_emb_def)
+ from `i \<in> I` show "?\<Omega> \<in> ?G"
+ by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"]
+ simp: generator_def prod_emb_def)
+ fix A assume "A \<in> ?G"
+ then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA"
+ by (auto simp: generator_def)
+ fix B assume "B \<in> ?G"
+ then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB"
+ by (auto simp: generator_def)
+ let ?RA = "emb (JA \<union> JB) JA XA"
+ let ?RB = "emb (JA \<union> JB) JB XB"
+ have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
+ using XA A XB B by auto
+ show "A - B \<in> ?G" "A \<union> B \<in> ?G"
+ unfolding * using XA XB by (safe intro!: generatorI') auto
+qed
+
+lemma sets_PiM_generator:
+ "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
+proof cases
+ assume "I = {}" then show ?thesis
+ unfolding generator_def
+ by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong)
+next
+ assume "I \<noteq> {}"
+ show ?thesis
+ proof
+ show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
+ unfolding sets_PiM
+ proof (safe intro!: sigma_sets_subseteq)
+ fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
+ by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
+ qed
+ qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
+qed
+
+lemma generatorI:
+ "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
+ unfolding generator_def by auto
+
+definition
+ "\<mu>G A =
+ (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (PiP J M P) X))"
+
+lemma \<mu>G_spec:
+ assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
+ shows "\<mu>G A = emeasure (PiP J M P) X"
+ unfolding \<mu>G_def
+proof (intro the_equality allI impI ballI)
+ fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)"
+ have "emeasure (PiP K M P) Y = emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) K Y)"
+ using K J by simp
+ also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
+ using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
+ also have "emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (PiP J M P) X"
+ using K J by simp
+ finally show "emeasure (PiP J M P) X = emeasure (PiP K M P) Y" ..
+qed (insert J, force)
+
+lemma \<mu>G_eq:
+ "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (PiP J M P) X"
+ by (intro \<mu>G_spec) auto
+
+lemma generator_Ex:
+ assumes *: "A \<in> generator"
+ shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (PiP J M P) X"
+proof -
+ from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
+ unfolding generator_def by auto
+ with \<mu>G_spec[OF this] show ?thesis by auto
+qed
+
+lemma generatorE:
+ assumes A: "A \<in> generator"
+ obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (PiP J M P) X"
+proof -
+ from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
+ "\<mu>G A = emeasure (PiP J M P) X" by auto
+ then show thesis by (intro that) auto
+qed
+
+lemma merge_sets:
+ "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
+ by simp
+
+lemma merge_emb:
+ assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
+ shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
+ emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
+proof -
+ have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)"
+ by (auto simp: restrict_def merge_def)
+ have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)"
+ by (auto simp: restrict_def merge_def)
+ have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto
+ have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
+ have [simp]: "(K - J) \<inter> K = K - J" by auto
+ from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
+ by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
+ auto
+qed
+
+lemma positive_\<mu>G:
+ assumes "I \<noteq> {}"
+ shows "positive generator \<mu>G"
+proof -
+ interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
+ show ?thesis
+ proof (intro positive_def[THEN iffD2] conjI ballI)
+ from generatorE[OF G.empty_sets] guess J X . note this[simp]
+ have "X = {}"
+ by (rule prod_emb_injective[of J I]) simp_all
+ then show "\<mu>G {} = 0" by simp
+ next
+ fix A assume "A \<in> generator"
+ from generatorE[OF this] guess J X . note this[simp]
+ show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
+ qed
+qed
+
+lemma additive_\<mu>G:
+ assumes "I \<noteq> {}"
+ shows "additive generator \<mu>G"
+proof -
+ interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
+ show ?thesis
+ proof (intro additive_def[THEN iffD2] ballI impI)
+ fix A assume "A \<in> generator" with generatorE guess J X . note J = this
+ fix B assume "B \<in> generator" with generatorE guess K Y . note K = this
+ assume "A \<inter> B = {}"
+ have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
+ using J K by auto
+ have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
+ apply (rule prod_emb_injective[of "J \<union> K" I])
+ apply (insert `A \<inter> B = {}` JK J K)
+ apply (simp_all add: Int prod_emb_Int)
+ done
+ have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
+ using J K by simp_all
+ then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
+ by simp
+ also have "\<dots> = emeasure (PiP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
+ using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
+ also have "\<dots> = \<mu>G A + \<mu>G B"
+ using J K JK_disj by (simp add: plus_emeasure[symmetric])
+ finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
+ qed
+qed
+
+end
+
+end
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Fri Nov 09 19:21:47 2012 +0100
@@ -15,7 +15,6 @@
structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
struct
-
(* syntactic operations *)
fun mk_inf (t1, t2) =
@@ -110,10 +109,6 @@
fun dest_bound (Bound i) = i
| dest_bound t = raise TERM("dest_bound", [t]);
-fun mk_pattern t = case try ((map dest_bound) o HOLogic.strip_tuple) t of
- SOME p => Pattern p
- | NONE => raise TERM ("mk_pattern: only tuples of bound variables supported", [t]);
-
fun type_of_pattern Ts (Pattern bs) = HOLogic.mk_tupleT (map (nth Ts) bs)
fun term_of_pattern Ts (Pattern bs) =
@@ -141,40 +136,40 @@
val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
in (domain_type (fastype_of t''), t'') end
-fun mk_atom vs (Const (@{const_name "Set.member"}, _) $ x $ s) =
+fun mk_term vs t =
+ let
+ val bs = loose_bnos t
+ val vs' = map (nth (rev vs)) bs
+ val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs)
+ |> sort (fn (p1, p2) => int_ord (fst p1, fst p2))
+ |> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst')))))
+ val t' = subst_bounds (subst, t)
+ val tuple = Pattern bs
+ in (tuple, (vs', t')) end
+
+fun default_atom vs t =
+ let
+ val (tuple, (vs', t')) = mk_term vs t
+ val T = HOLogic.mk_tupleT (map snd vs')
+ val s = HOLogic.Collect_const T $ (snd (mk_split @{typ bool} vs' t'))
+ in
+ (tuple, Atom (tuple, s))
+ end
+
+fun mk_atom vs (t as Const (@{const_name "Set.member"}, _) $ x $ s) =
if not (null (loose_bnos s)) then
- raise TERM ("mk_atom: bound variables in the set expression", [s])
+ default_atom vs t
else
- (case try mk_pattern x of
- SOME pat => (pat, Atom (pat, s))
+ (case try ((map dest_bound) o HOLogic.strip_tuple) x of
+ SOME pat => (Pattern pat, Atom (Pattern pat, s))
| NONE =>
let
- val bs = loose_bnos x
- val vs' = map (nth (rev vs)) bs
- val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs)
- |> sort (fn (p1, p2) => int_ord (fst p1, fst p2))
- |> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst')))))
- val x' = subst_bounds (subst, x)
- val tuple = Pattern bs
+ val (tuple, (vs', x')) = mk_term vs x
val rT = HOLogic.dest_setT (fastype_of s)
- val (_, f) = mk_split rT vs' x'
- in (tuple, Atom (tuple, mk_vimage f s)) end)
- | mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) =
- apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
- | mk_atom vs t =
- let
- val bs = loose_bnos t
- val vs' = map (nth (rev vs)) bs
- val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs)
- |> sort (fn (p1, p2) => int_ord (fst p1, fst p2))
- |> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst')))))
- val t' = subst_bounds (subst, t)
- val tuple = Pattern bs
- val setT = HOLogic.mk_tupleT (map snd vs')
- val (_, s) = mk_split @{typ bool} vs' t'
- in
- (tuple, Atom (tuple, HOLogic.Collect_const setT $ s))
- end
+ val s = mk_vimage (snd (mk_split rT vs' x')) s
+ in (tuple, Atom (tuple, s)) end)
+ | mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
+ | mk_atom vs t = default_atom vs t
fun merge' [] (pats1, pats2) = ([], (pats1, pats2))
| merge' pat (pats, []) = (pat, (pats, []))
@@ -294,7 +289,7 @@
(0 upto (length vs - 1))
val (pats, fm) =
mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
- fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts)
+ fun mk_set (Atom pt) = foldr1 mk_sigma (map (lookup pt) pats)
| mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
| mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats)
@@ -331,10 +326,10 @@
val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
-val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
+fun elim_Collect_tac ss = dtac @{thm iffD1[OF mem_Collect_eq]}
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
THEN' REPEAT_DETERM o etac @{thm conjE}
- THEN' TRY o hyp_subst_tac;
+ THEN' TRY o hyp_subst_tac' ss;
fun intro_image_tac ctxt = rtac @{thm image_eqI}
THEN' (REPEAT_DETERM1 o
@@ -348,7 +343,7 @@
THEN' REPEAT_DETERM o CHANGED o
(TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps @{thms split_paired_all prod.cases}))
THEN' REPEAT_DETERM o etac @{thm Pair_inject}
- THEN' TRY o hyp_subst_tac)
+ THEN' TRY o hyp_subst_tac' ss)
fun tac1_of_formula ss (Int (fm1, fm2)) =
TRY o etac @{thm conjE}
@@ -392,21 +387,21 @@
ORELSE' etac @{thm conjE}
ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps [@{thm prod.cases}])) THEN'
- REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl})
+ REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac' ss THEN' TRY o rtac @{thm refl})
ORELSE' (etac @{thm imageE}
THEN' (REPEAT_DETERM o CHANGED o
(TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps @{thms split_paired_all prod.cases}))
THEN' REPEAT_DETERM o etac @{thm Pair_inject}
- THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl})))
+ THEN' TRY o hyp_subst_tac' ss THEN' TRY o rtac @{thm refl})))
ORELSE' etac @{thm ComplE}
ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
THEN' TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps [@{thm prod.cases}]))
- THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl}))
+ THEN' TRY o hyp_subst_tac' ss THEN' TRY o rtac @{thm refl}))
fun tac ss ctxt fm =
let
val subset_tac1 = rtac @{thm subsetI}
- THEN' elim_Collect_tac
+ THEN' elim_Collect_tac ss
THEN' intro_image_tac ctxt
THEN' tac1_of_formula ss fm
val subset_tac2 = rtac @{thm subsetI}
@@ -414,7 +409,7 @@
THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
THEN' REPEAT_DETERM o resolve_tac @{thms exI}
THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
- THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl}))))
+ THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac' ss) THEN' rtac @{thm refl}))))
THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ss f (i + j)) (strip_Int fm))))
in
@@ -528,11 +523,14 @@
fun code_simproc ss redex =
let
- val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex
+ fun unfold_conv thms =
+ Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+ (Raw_Simplifier.inherit_context ss empty_ss addsimps thms)
+ val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex
in
case base_simproc ss (Thm.rhs_of prep_thm) of
SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm],
- Raw_Simplifier.rewrite false @{thms eq_equal} (Thm.rhs_of rewr_thm)])
+ unfold_conv @{thms eq_equal} (Thm.rhs_of rewr_thm)])
| NONE => NONE
end;
--- a/src/Provers/hypsubst.ML Fri Nov 09 19:16:31 2012 +0100
+++ b/src/Provers/hypsubst.ML Fri Nov 09 19:21:47 2012 +0100
@@ -48,6 +48,7 @@
sig
val bound_hyp_subst_tac : int -> tactic
val hyp_subst_tac : int -> tactic
+ val hyp_subst_tac' : simpset -> int -> tactic
val blast_hyp_subst_tac : bool -> int -> tactic
val stac : thm -> int -> tactic
val hypsubst_setup : theory -> theory
@@ -126,12 +127,14 @@
(*Select a suitable equality assumption; substitute throughout the subgoal
If bnd is true, then it replaces Bound variables only. *)
- fun gen_hyp_subst_tac bnd =
+ fun gen_hyp_subst_tac opt_ss bnd =
let fun tac i st = SUBGOAL (fn (Bi, _) =>
let
val (k, _) = eq_var bnd true Bi
- val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
- |> Simplifier.set_mksimps (K (mk_eqs bnd))
+ val map_simpset = case opt_ss of
+ NONE => Simplifier.global_context (Thm.theory_of_thm st)
+ | SOME ss => Simplifier.inherit_context ss
+ val hyp_subst_ss = map_simpset empty_ss |> Simplifier.set_mksimps (K (mk_eqs bnd))
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
etac thin_rl i, rotate_tac (~k) i]
end handle THM _ => no_tac | EQ_VAR => no_tac) i st
@@ -195,11 +198,14 @@
(*Substitutes for Free or Bound variables*)
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
- gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
+ gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
+
+fun hyp_subst_tac' ss = FIRST' [ematch_tac [Data.thin_refl],
+ gen_hyp_subst_tac (SOME ss) false, vars_gen_hyp_subst_tac false];
(*Substitutes for Bound variables only -- this is always safe*)
val bound_hyp_subst_tac =
- gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
+ gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
(** Version for Blast_tac. Hyps that are affected by the substitution are