--- a/NEWS Thu Oct 11 20:38:02 2012 +0200
+++ b/NEWS Thu Oct 11 21:02:19 2012 +0200
@@ -62,6 +62,16 @@
*** HOL ***
+* Theory "Library/Multiset":
+
+ - Renamed constants
+ fold_mset ~> Multiset.fold -- for coherence with other fold combinators
+
+ - Renamed facts
+ fold_mset_commute ~> fold_mset_comm -- for coherence with fold_comm
+
+INCOMPATIBILITY.
+
* Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY.
* Class "comm_monoid_diff" formalises properties of bounded
--- a/src/HOL/Library/Multiset.thy Thu Oct 11 20:38:02 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Oct 11 21:02:19 2012 +0200
@@ -657,146 +657,82 @@
subsection {* The fold combinator *}
-text {*
- The intended behaviour is
- @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
- if @{text f} is associative-commutative.
-*}
-
-text {*
- The graph of @{text "fold_mset"}, @{text "z"}: the start element,
- @{text "f"}: folding function, @{text "A"}: the multiset, @{text
- "y"}: the result.
-*}
-inductive
- fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool"
- for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
- and z :: 'b
+definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
where
- emptyI [intro]: "fold_msetG f z {#} z"
-| insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)"
+ "fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
-inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x"
-inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y"
-
-definition
- fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where
- "fold_mset f z A = (THE x. fold_msetG f z A x)"
-
-lemma Diff1_fold_msetG:
- "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
-apply (frule_tac x = x in fold_msetG.insertI)
-apply auto
-done
-
-lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
-apply (induct A)
- apply blast
-apply clarsimp
-apply (drule_tac x = x in fold_msetG.insertI)
-apply auto
-done
-
-lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
-unfolding fold_mset_def by blast
+lemma fold_mset_empty [simp]:
+ "fold f s {#} = s"
+ by (simp add: fold_def)
context comp_fun_commute
begin
-lemma fold_msetG_insertE_aux:
- "fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A - {#a#}) y'"
-proof (induct set: fold_msetG)
- case (insertI A y x) show ?case
- proof (cases "x = a")
- assume "x = a" with insertI show ?case by auto
+lemma fold_mset_insert:
+ "fold f s (M + {#x#}) = f x (fold f s M)"
+proof -
+ interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
+ by (fact comp_fun_commute_funpow)
+ interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
+ by (fact comp_fun_commute_funpow)
+ show ?thesis
+ proof (cases "x \<in> set_of M")
+ case False
+ then have *: "count (M + {#x#}) x = 1" by simp
+ from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) =
+ Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
+ by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
+ with False * show ?thesis
+ by (simp add: fold_def del: count_union)
next
- assume "x \<noteq> a"
- then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
- using insertI by auto
- have "f x y = f a (f x y')"
- unfolding y by (rule fun_left_comm)
- moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
- using y' and `x \<noteq> a`
- by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
- ultimately show ?case by fast
+ case True
+ def N \<equiv> "set_of M - {x}"
+ from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto
+ then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
+ Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
+ by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
+ with * show ?thesis by (simp add: fold_def del: count_union) simp
qed
-qed simp
-
-lemma fold_msetG_insertE:
- assumes "fold_msetG f z (A + {#x#}) v"
- obtains y where "v = f x y" and "fold_msetG f z A y"
-using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
-
-lemma fold_msetG_determ:
- "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
-proof (induct arbitrary: y set: fold_msetG)
- case (insertI A y x v)
- from `fold_msetG f z (A + {#x#}) v`
- obtain y' where "v = f x y'" and "fold_msetG f z A y'"
- by (rule fold_msetG_insertE)
- from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
- with `v = f x y'` show "v = f x y" by simp
-qed fast
-
-lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
-unfolding fold_mset_def by (blast intro: fold_msetG_determ)
-
-lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
-proof -
- from fold_msetG_nonempty fold_msetG_determ
- have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
- then show ?thesis unfolding fold_mset_def by (rule theI')
qed
-lemma fold_mset_insert:
- "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
-by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
+corollary fold_mset_single [simp]:
+ "fold f s {#x#} = f x s"
+proof -
+ have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
+ then show ?thesis by simp
+qed
-lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
-by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])
-
-lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
-using fold_mset_insert [of z "{#}"] by simp
+lemma fold_mset_fun_comm:
+ "f x (fold f s M) = fold f (f x s) M"
+ by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
lemma fold_mset_union [simp]:
- "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
-proof (induct A)
+ "fold f s (M + N) = fold f (fold f s M) N"
+proof (induct M)
case empty then show ?case by simp
next
- case (add A x)
- have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac)
- then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))"
- by (simp add: fold_mset_insert)
- also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
- by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
- finally show ?case .
+ case (add M x)
+ have "M + {#x#} + N = (M + N) + {#x#}"
+ by (simp add: add_ac)
+ with add show ?case by (simp add: fold_mset_insert fold_mset_fun_comm)
qed
lemma fold_mset_fusion:
assumes "comp_fun_commute g"
- shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
+ shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold g w A) = fold f (h w) A" (is "PROP ?P")
proof -
interpret comp_fun_commute g by (fact assms)
show "PROP ?P" by (induct A) auto
qed
-lemma fold_mset_rec:
- assumes "a \<in># A"
- shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))"
-proof -
- from assms obtain A' where "A = A' + {#a#}"
- by (blast dest: multi_member_split)
- then show ?thesis by simp
-qed
-
end
text {*
A note on code generation: When defining some function containing a
- subterm @{term"fold_mset F"}, code generation is not automatic. When
+ subterm @{term "fold F"}, code generation is not automatic. When
interpreting locale @{text left_commutative} with @{text F}, the
- would be code thms for @{const fold_mset} become thms like
- @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but
+ would be code thms for @{const fold} become thms like
+ @{term "fold F z {#} = z"} where @{text F} is not a pattern but
contains defined symbols, i.e.\ is not a code thm. Hence a separate
constant with its own code thms needs to be introduced for @{text
F}. See the image operator below.
@@ -806,36 +742,46 @@
subsection {* Image *}
definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
- "image_mset f = fold_mset (op + o single o f) {#}"
+ "image_mset f = fold (plus o single o f) {#}"
-interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
-proof qed (simp add: add_ac fun_eq_iff)
+lemma comp_fun_commute_mset_image:
+ "comp_fun_commute (plus o single o f)"
+proof
+qed (simp add: add_ac fun_eq_iff)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
-by (simp add: image_mset_def)
+ by (simp add: image_mset_def)
lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
-by (simp add: image_mset_def)
-
-lemma image_mset_insert:
- "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
-by (simp add: image_mset_def add_ac)
+proof -
+ interpret comp_fun_commute "plus o single o f"
+ by (fact comp_fun_commute_mset_image)
+ show ?thesis by (simp add: image_mset_def)
+qed
lemma image_mset_union [simp]:
- "image_mset f (M+N) = image_mset f M + image_mset f N"
-apply (induct N)
- apply simp
-apply (simp add: add_assoc [symmetric] image_mset_insert)
-done
+ "image_mset f (M + N) = image_mset f M + image_mset f N"
+proof -
+ interpret comp_fun_commute "plus o single o f"
+ by (fact comp_fun_commute_mset_image)
+ show ?thesis by (induct N) (simp_all add: image_mset_def add_ac)
+qed
+
+corollary image_mset_insert:
+ "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
+ by simp
-lemma set_of_image_mset [simp]: "set_of (image_mset f M) = image f (set_of M)"
-by (induct M) simp_all
+lemma set_of_image_mset [simp]:
+ "set_of (image_mset f M) = image f (set_of M)"
+ by (induct M) simp_all
-lemma size_image_mset [simp]: "size (image_mset f M) = size M"
-by (induct M) simp_all
+lemma size_image_mset [simp]:
+ "size (image_mset f M) = size M"
+ by (induct M) simp_all
-lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
-by (cases M) auto
+lemma image_mset_is_empty_iff [simp]:
+ "image_mset f M = {#} \<longleftrightarrow> M = {#}"
+ by (cases M) auto
syntax
"_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
@@ -989,7 +935,7 @@
lemma fold_multiset_equiv:
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
and equiv: "multiset_of xs = multiset_of ys"
- shows "fold f xs = fold f ys"
+ shows "List.fold f xs = List.fold f ys"
using f equiv [symmetric]
proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
@@ -999,8 +945,8 @@
have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
by (rule Cons.prems(1)) (simp_all add: *)
moreover from * have "x \<in> set ys" by simp
- ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
- moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
+ ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
+ moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps)
ultimately show ?case by simp
qed
@@ -1915,5 +1861,7 @@
multiset_postproc
*}
+hide_const (open) fold
+
end
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Oct 11 20:38:02 2012 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Oct 11 21:02:19 2012 +0200
@@ -36,54 +36,66 @@
"ALL i :# M. P i"?
*)
-definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
+context comm_monoid_mult
+begin
+
+definition msetprod :: "'a multiset \<Rightarrow> 'a"
where
+ "msetprod M = Multiset.fold times 1 M"
+
+lemma msetprod_empty [simp]:
+ "msetprod {#} = 1"
+ by (simp add: msetprod_def)
+
+lemma msetprod_singleton [simp]:
+ "msetprod {#x#} = x"
+proof -
+ interpret comp_fun_commute times
+ by (fact comp_fun_commute)
+ show ?thesis by (simp add: msetprod_def)
+qed
+
+lemma msetprod_Un [simp]:
+ "msetprod (A + B) = msetprod A * msetprod B"
+proof -
+ interpret comp_fun_commute times
+ by (fact comp_fun_commute)
+ show ?thesis by (induct B) (simp_all add: msetprod_def mult_ac)
+qed
+
+lemma msetprod_multiplicity:
"msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
+ by (simp add: msetprod_def setprod_def Multiset.fold_def fold_image_def funpow_times_power)
-abbreviation (in comm_monoid_mult) msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
+abbreviation msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
where
"msetprod_image f M \<equiv> msetprod (image_mset f M)"
+end
+
syntax
"_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
("(3PROD _:#_. _)" [0, 51, 10] 10)
+syntax (xsymbols)
+ "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+ ("(3\<Pi>_\<in>#_. _)" [0, 51, 10] 10)
+
+syntax (HTML output)
+ "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+ ("(3\<Pi>_\<in>#_. _)" [0, 51, 10] 10)
+
translations
"PROD i :# A. b" == "CONST msetprod_image (\<lambda>i. b) A"
-lemma msetprod_empty: "msetprod {#} = 1"
- by (simp add: msetprod_def)
-
-lemma msetprod_singleton: "msetprod {#x#} = x"
- by (simp add: msetprod_def)
-
-lemma msetprod_Un: "msetprod (A + B) = msetprod A * msetprod B"
- apply (simp add: msetprod_def power_add)
- apply (subst setprod_Un2)
- apply auto
- apply (subgoal_tac
- "(PROD x:set_of A - set_of B. x ^ count A x * x ^ count B x) =
- (PROD x:set_of A - set_of B. x ^ count A x)")
- apply (erule ssubst)
- apply (subgoal_tac
- "(PROD x:set_of B - set_of A. x ^ count A x * x ^ count B x) =
- (PROD x:set_of B - set_of A. x ^ count B x)")
- apply (erule ssubst)
- apply (subgoal_tac "(PROD x:set_of A. x ^ count A x) =
- (PROD x:set_of A - set_of B. x ^ count A x) *
- (PROD x:set_of A Int set_of B. x ^ count A x)")
- apply (erule ssubst)
- apply (subgoal_tac "(PROD x:set_of B. x ^ count B x) =
- (PROD x:set_of B - set_of A. x ^ count B x) *
- (PROD x:set_of A Int set_of B. x ^ count B x)")
- apply (erule ssubst)
- apply (subst setprod_timesf)
- apply (force simp add: mult_ac)
- apply (subst setprod_Un_disjoint [symmetric])
- apply (auto intro: setprod_cong)
- apply (subst setprod_Un_disjoint [symmetric])
- apply (auto intro: setprod_cong)
- done
+lemma (in comm_semiring_1) dvd_msetprod:
+ assumes "x \<in># A"
+ shows "x dvd msetprod A"
+proof -
+ from assms have "A = (A - {#x#}) + {#x#}" by simp
+ then obtain B where "A = B + {#x#}" ..
+ then show ?thesis by simp
+qed
subsection {* unique factorization: multiset version *}
@@ -104,7 +116,7 @@
} moreover {
assume "n > 1" and "prime n"
then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
- by (auto simp add: msetprod_def)
+ by auto
} moreover {
assume "n > 1" and "~ prime n"
with not_prime_eq_prod_nat
@@ -132,10 +144,10 @@
assume M: "a : set_of M"
with assms have a: "prime a" by auto
with M have "a ^ count M a dvd (PROD i :# M. i)"
- by (auto intro: dvd_setprod simp add: msetprod_def)
+ by (auto simp add: msetprod_multiplicity intro: dvd_setprod)
also have "... dvd (PROD i :# N. i)" by (rule assms)
also have "... = (PROD i : (set_of N). i ^ (count N i))"
- by (simp add: msetprod_def)
+ by (simp add: msetprod_multiplicity)
also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
proof (cases)
assume "a : set_of N"
@@ -330,7 +342,7 @@
lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
n = (PROD p : prime_factors n. p^(multiplicity p n))"
apply (frule multiset_prime_factorization)
- apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
+ apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity)
done
lemma prime_factorization_int:
@@ -363,7 +375,7 @@
apply force
apply force
using assms
- apply (simp add: Abs_multiset_inverse set_of_def msetprod_def)
+ apply (simp add: Abs_multiset_inverse set_of_def msetprod_multiplicity)
done
with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
by (simp add: Abs_multiset_inverse)
--- a/src/HOL/Power.thy Thu Oct 11 20:38:02 2012 +0200
+++ b/src/HOL/Power.thy Thu Oct 11 21:02:19 2012 +0200
@@ -90,6 +90,19 @@
unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
unfolding power_Suc power_add Let_def mult_assoc ..
+lemma funpow_times_power:
+ "(times x ^^ f x) = times (x ^ f x)"
+proof (induct "f x" arbitrary: f)
+ case 0 then show ?case by (simp add: fun_eq_iff)
+next
+ case (Suc n)
+ def g \<equiv> "\<lambda>x. f x - 1"
+ with Suc have "n = g x" by simp
+ with Suc have "times x ^^ g x = times (x ^ g x)" by simp
+ moreover from Suc g_def have "f x = g x + 1" by simp
+ ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult_assoc)
+qed
+
end
context comm_monoid_mult
@@ -727,3 +740,4 @@
Power Arith
end
+
--- a/src/HOL/Probability/Binary_Product_Measure.thy Thu Oct 11 20:38:02 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Thu Oct 11 21:02:19 2012 +0200
@@ -476,7 +476,7 @@
"x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
by (rule measurable_compose[OF measurable_Pair]) auto
-lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
+lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst':
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x"
shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
using f proof induct
@@ -512,7 +512,7 @@
qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add
positive_integral_monotone_convergence_SUP
measurable_compose_Pair1 positive_integral_positive
- borel_measurable_positive_integral_fst positive_integral_mono incseq_def le_fun_def
+ borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def
cong: positive_integral_cong)
lemma (in pair_sigma_finite) positive_integral_fst_measurable:
@@ -521,10 +521,21 @@
(is "?C f \<in> borel_measurable M1")
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
using f
- borel_measurable_positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
+ borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
unfolding positive_integral_max_0 by auto
+lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
+ "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
+ using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
+
+lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
+ assumes "(\<lambda>(x, y). f x y) \<in> borel_measurable (M2 \<Otimes>\<^isub>M M1)" shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M1) \<in> borel_measurable M2"
+proof -
+ interpret Q: pair_sigma_finite M2 M1 by default
+ from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
+qed
+
lemma (in pair_sigma_finite) positive_integral_snd_measurable:
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
--- a/src/HOL/Probability/Information.thy Thu Oct 11 20:38:02 2012 +0200
+++ b/src/HOL/Probability/Information.thy Thu Oct 11 21:02:19 2012 +0200
@@ -1007,17 +1007,6 @@
"\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
(count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
-lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
- "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
- using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
-
-lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
- assumes "(\<lambda>(x, y). f x y) \<in> borel_measurable (M2 \<Otimes>\<^isub>M M1)" shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M1) \<in> borel_measurable M2"
-proof -
- interpret Q: pair_sigma_finite M2 M1 by default
- from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
-qed
-
lemma (in information_space)
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
assumes Px: "distributed M S X Px"