--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Thu Aug 31 19:34:43 2017 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Thu Aug 31 20:19:55 2017 +0200
@@ -350,6 +350,25 @@
shows "(\<lambda>x. f x * c) abs_summable_on A"
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)
+lemma abs_summable_on_prod_PiE:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
+ assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+ assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
+ shows "(\<lambda>g. \<Prod>x\<in>A. f x (g x)) abs_summable_on PiE A B"
+proof -
+ define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
+ from assms have [simp]: "countable (B' x)" for x
+ by (auto simp: B'_def)
+ then interpret product_sigma_finite "count_space \<circ> B'"
+ unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
+ from assms have "integrable (PiM A (count_space \<circ> B')) (\<lambda>g. \<Prod>x\<in>A. f x (g x))"
+ by (intro product_integrable_prod) (auto simp: abs_summable_on_def B'_def)
+ also have "PiM A (count_space \<circ> B') = count_space (PiE A B')"
+ unfolding o_def using finite by (intro count_space_PiM_finite) simp_all
+ also have "PiE A B' = PiE A B" by (intro PiE_cong) (simp_all add: B'_def)
+ finally show ?thesis by (simp add: abs_summable_on_def)
+qed
+
lemma not_summable_infsetsum_eq:
@@ -366,6 +385,18 @@
by (subst integral_restrict_space [symmetric])
(auto simp: restrict_count_space_subset infsetsum_def)
+lemma nn_integral_conv_infsetsum:
+ assumes "f abs_summable_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+ shows "nn_integral (count_space A) f = ennreal (infsetsum f A)"
+ using assms unfolding infsetsum_def abs_summable_on_def
+ by (subst nn_integral_eq_integral) auto
+
+lemma infsetsum_conv_nn_integral:
+ assumes "nn_integral (count_space A) f \<noteq> \<infinity>" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+ shows "infsetsum f A = enn2real (nn_integral (count_space A) f)"
+ unfolding infsetsum_def using assms
+ by (subst integral_eq_nn_integral) auto
+
lemma infsetsum_cong [cong]:
"(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B"
unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto
--- a/src/HOL/Data_Structures/Splay_Map.thy Thu Aug 31 19:34:43 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,156 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section "Splay Tree Implementation of Maps"
-
-theory Splay_Map
-imports
- Splay_Set
- Map_by_Ordered
-begin
-
-function splay :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"splay x Leaf = Leaf" |
-"x = fst a \<Longrightarrow> splay x (Node t1 a t2) = Node t1 a t2" |
-"x = fst a \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" |
-"x < fst a \<Longrightarrow> splay x (Node Leaf a t) = Node Leaf a t" |
-"x < fst a \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" |
-"x < fst a \<Longrightarrow> x < fst b \<Longrightarrow> t1 \<noteq> Leaf \<Longrightarrow>
- splay x (Node (Node t1 a t2) b t3) =
- (case splay x t1 of Node t11 y t12 \<Rightarrow> Node t11 y (Node t12 a (Node t2 b t3)))" |
-"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" |
-"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
- splay x (Node (Node t1 a t2) b t3) =
- (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
-"fst a < x \<Longrightarrow> x = fst b \<Longrightarrow> splay x (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" |
-"fst a < x \<Longrightarrow> splay x (Node t a Leaf) = Node t a Leaf" |
-"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
- splay x (Node t1 a (Node t2 b t3)) =
- (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
-"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" |
-"fst a < x \<Longrightarrow> fst b < x \<Longrightarrow> splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" |
-"fst a < x \<Longrightarrow> fst b < x \<Longrightarrow> t3 \<noteq> Leaf \<Longrightarrow>
- splay x (Node t1 a (Node t2 b t3)) =
- (case splay x t3 of Node t31 y t32 \<Rightarrow> Node (Node (Node t1 a t2) b t31) y t32)"
-apply(atomize_elim)
-apply(auto)
-(* 1 subgoal *)
-apply (subst (asm) neq_Leaf_iff)
-apply(auto)
-apply (metis tree.exhaust surj_pair less_linear)+
-done
-
-termination splay
-by lexicographic_order
-
-lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
- Node al a ar \<Rightarrow> (case cmp x (fst a) of
- EQ \<Rightarrow> t |
- LT \<Rightarrow> (case al of
- Leaf \<Rightarrow> t |
- Node bl b br \<Rightarrow> (case cmp x (fst b) of
- EQ \<Rightarrow> Node bl b (Node br a ar) |
- LT \<Rightarrow> if bl = Leaf then Node bl b (Node br a ar)
- else case splay x bl of
- Node bll y blr \<Rightarrow> Node bll y (Node blr b (Node br a ar)) |
- GT \<Rightarrow> if br = Leaf then Node bl b (Node br a ar)
- else case splay x br of
- Node brl y brr \<Rightarrow> Node (Node bl b brl) y (Node brr a ar))) |
- GT \<Rightarrow> (case ar of
- Leaf \<Rightarrow> t |
- Node bl b br \<Rightarrow> (case cmp x (fst b) of
- EQ \<Rightarrow> Node (Node al a bl) b br |
- LT \<Rightarrow> if bl = Leaf then Node (Node al a bl) b br
- else case splay x bl of
- Node bll y blr \<Rightarrow> Node (Node al a bll) y (Node blr b br) |
- GT \<Rightarrow> if br=Leaf then Node (Node al a bl) b br
- else case splay x br of
- Node bll y blr \<Rightarrow> Node (Node (Node al a bl) b bll) y blr))))"
-by(auto cong: case_tree_cong split: tree.split)
-
-definition lookup :: "('a*'b)tree \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where "lookup t x =
- (case splay x t of Leaf \<Rightarrow> None | Node _ (a,b) _ \<Rightarrow> if x=a then Some b else None)"
-
-hide_const (open) insert
-
-fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"update x y t = (if t = Leaf then Node Leaf (x,y) Leaf
- else case splay x t of
- Node l a r \<Rightarrow> if x = fst a then Node l (x,y) r
- else if x < fst a then Node l (x,y) (Node Leaf a r) else Node (Node l a Leaf) (x,y) r)"
-
-definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"delete x t = (if t = Leaf then Leaf
- else case splay x t of Node l a r \<Rightarrow>
- if x = fst a
- then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r
- else Node l a r)"
-
-
-subsection "Functional Correctness Proofs"
-
-lemma splay_Leaf_iff: "(splay x t = Leaf) = (t = Leaf)"
-by(induction x t rule: splay.induct) (auto split: tree.splits)
-
-
-subsubsection "Proofs for lookup"
-
-lemma splay_map_of_inorder:
- "splay x t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
- map_of (inorder t) x = (if x = fst a then Some(snd a) else None)"
-by(induction x t arbitrary: l a r rule: splay.induct)
- (auto simp: map_of_simps splay_Leaf_iff split: tree.splits)
-
-lemma lookup_eq:
- "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
-by(auto simp: lookup_def splay_Leaf_iff splay_map_of_inorder split: tree.split)
-
-
-subsubsection "Proofs for update"
-
-lemma inorder_splay: "inorder(splay x t) = inorder t"
-by(induction x t rule: splay.induct)
- (auto simp: neq_Leaf_iff split: tree.split)
-
-lemma sorted_splay:
- "sorted1(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow>
- sorted(map fst (inorder l) @ x # map fst (inorder r))"
-unfolding inorder_splay[of x t, symmetric]
-by(induction x t arbitrary: l a r rule: splay.induct)
- (auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)
-
-lemma inorder_update:
- "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
-using inorder_splay[of x t, symmetric] sorted_splay[of t x]
-by(auto simp: upd_list_simps upd_list_Cons upd_list_snoc neq_Leaf_iff split: tree.split)
-
-
-subsubsection "Proofs for delete"
-
-lemma inorder_splay_maxD:
- "splay_max t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
- inorder l @ [a] = inorder t \<and> r = Leaf"
-by(induction t arbitrary: l a r rule: splay_max.induct)
- (auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits)
-
-lemma inorder_delete:
- "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-using inorder_splay[of x t, symmetric] sorted_splay[of t x]
-by (auto simp: del_list_simps del_list_sorted_app delete_def
- del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff
- split: tree.splits)
-
-
-subsubsection "Overall Correctness"
-
-interpretation Map_by_Ordered
-where empty = Leaf and lookup = lookup and update = update
-and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
-proof (standard, goal_cases)
- case 2 thus ?case by(simp add: lookup_eq)
-next
- case 3 thus ?case by(simp add: inorder_update del: update.simps)
-next
- case 4 thus ?case by(simp add: inorder_delete)
-qed auto
-
-end
--- a/src/HOL/Data_Structures/Splay_Set.thy Thu Aug 31 19:34:43 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,190 +0,0 @@
-(*
-Author: Tobias Nipkow
-Function follow AFP entry Splay_Tree, proofs are new.
-*)
-
-section "Splay Tree Implementation of Sets"
-
-theory Splay_Set
-imports
- "HOL-Library.Tree"
- Set_by_Ordered
- Cmp
-begin
-
-function splay :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"splay a Leaf = Leaf" |
-"splay a (Node t1 a t2) = Node t1 a t2" |
-"a<b \<Longrightarrow> splay a (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" |
-"x<a \<Longrightarrow> splay x (Node Leaf a t) = Node Leaf a t" |
-"x<a \<Longrightarrow> x<b \<Longrightarrow> splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" |
-"x<a \<Longrightarrow> x<b \<Longrightarrow> t1 \<noteq> Leaf \<Longrightarrow>
- splay x (Node (Node t1 a t2) b t3) =
- (case splay x t1 of Node t11 y t12 \<Rightarrow> Node t11 y (Node t12 a (Node t2 b t3)))" |
-"a<x \<Longrightarrow> x<b \<Longrightarrow> splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" |
-"a<x \<Longrightarrow> x<b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
- splay x (Node (Node t1 a t2) b t3) =
- (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
-"a<b \<Longrightarrow> splay b (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" |
-"a<x \<Longrightarrow> splay x (Node t a Leaf) = Node t a Leaf" |
-"a<x \<Longrightarrow> x<b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
- splay x (Node t1 a (Node t2 b t3)) =
- (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
-"a<x \<Longrightarrow> x<b \<Longrightarrow> splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" |
-"a<x \<Longrightarrow> b<x \<Longrightarrow> splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" |
-"a<x \<Longrightarrow> b<x \<Longrightarrow> t3 \<noteq> Leaf \<Longrightarrow>
- splay x (Node t1 a (Node t2 b t3)) =
- (case splay x t3 of Node t31 y t32 \<Rightarrow> Node (Node (Node t1 a t2) b t31) y t32)"
-apply(atomize_elim)
-apply(auto)
-(* 1 subgoal *)
-apply (subst (asm) neq_Leaf_iff)
-apply(auto)
-apply (metis tree.exhaust less_linear)+
-done
-
-termination splay
-by lexicographic_order
-
-(* no idea why this speeds things up below *)
-lemma case_tree_cong:
- "\<lbrakk> x = x'; y = y'; z = z' \<rbrakk> \<Longrightarrow> case_tree x y z = case_tree x' y' z'"
-by auto
-
-lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
- Node al a ar \<Rightarrow> (case cmp x a of
- EQ \<Rightarrow> t |
- LT \<Rightarrow> (case al of
- Leaf \<Rightarrow> t |
- Node bl b br \<Rightarrow> (case cmp x b of
- EQ \<Rightarrow> Node bl b (Node br a ar) |
- LT \<Rightarrow> if bl = Leaf then Node bl b (Node br a ar)
- else case splay x bl of
- Node bll y blr \<Rightarrow> Node bll y (Node blr b (Node br a ar)) |
- GT \<Rightarrow> if br = Leaf then Node bl b (Node br a ar)
- else case splay x br of
- Node brl y brr \<Rightarrow> Node (Node bl b brl) y (Node brr a ar))) |
- GT \<Rightarrow> (case ar of
- Leaf \<Rightarrow> t |
- Node bl b br \<Rightarrow> (case cmp x b of
- EQ \<Rightarrow> Node (Node al a bl) b br |
- LT \<Rightarrow> if bl = Leaf then Node (Node al a bl) b br
- else case splay x bl of
- Node bll y blr \<Rightarrow> Node (Node al a bll) y (Node blr b br) |
- GT \<Rightarrow> if br=Leaf then Node (Node al a bl) b br
- else case splay x br of
- Node bll y blr \<Rightarrow> Node (Node (Node al a bl) b bll) y blr))))"
-by(auto cong: case_tree_cong split: tree.split)
-
-definition is_root :: "'a \<Rightarrow> 'a tree \<Rightarrow> bool" where
-"is_root x t = (case t of Leaf \<Rightarrow> False | Node l a r \<Rightarrow> x = a)"
-
-definition "isin t x = is_root x (splay x t)"
-
-hide_const (open) insert
-
-fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"insert x t =
- (if t = Leaf then Node Leaf x Leaf
- else case splay x t of
- Node l a r \<Rightarrow>
- case cmp x a of
- EQ \<Rightarrow> Node l a r |
- LT \<Rightarrow> Node l x (Node Leaf a r) |
- GT \<Rightarrow> Node (Node l a Leaf) x r)"
-
-
-fun splay_max :: "'a tree \<Rightarrow> 'a tree" where
-"splay_max Leaf = Leaf" |
-"splay_max (Node l b Leaf) = Node l b Leaf" |
-"splay_max (Node l b (Node rl c rr)) =
- (if rr = Leaf then Node (Node l b rl) c Leaf
- else case splay_max rr of
- Node rrl m rrr \<Rightarrow> Node (Node (Node l b rl) c rrl) m rrr)"
-
-
-definition delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"delete x t =
- (if t = Leaf then Leaf
- else case splay x t of Node l a r \<Rightarrow>
- if x = a
- then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r
- else Node l a r)"
-
-
-subsection "Functional Correctness Proofs"
-
-lemma splay_Leaf_iff: "(splay a t = Leaf) = (t = Leaf)"
-by(induction a t rule: splay.induct) (auto split: tree.splits)
-
-lemma splay_max_Leaf_iff: "(splay_max t = Leaf) = (t = Leaf)"
-by(induction t rule: splay_max.induct)(auto split: tree.splits)
-
-
-subsubsection "Proofs for isin"
-
-lemma
- "splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
- x \<in> elems (inorder t) \<longleftrightarrow> x=a"
-by(induction x t arbitrary: l a r rule: splay.induct)
- (auto simp: elems_simps1 splay_Leaf_iff ball_Un split: tree.splits)
-
-lemma splay_elemsD:
- "splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
- x \<in> elems (inorder t) \<longleftrightarrow> x=a"
-by(induction x t arbitrary: l a r rule: splay.induct)
- (auto simp: elems_simps2 splay_Leaf_iff split: tree.splits)
-
-lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (auto simp: isin_def is_root_def splay_elemsD splay_Leaf_iff split: tree.splits)
-
-
-subsubsection "Proofs for insert"
-
-lemma inorder_splay: "inorder(splay x t) = inorder t"
-by(induction x t rule: splay.induct)
- (auto simp: neq_Leaf_iff split: tree.split)
-
-lemma sorted_splay:
- "sorted(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow>
- sorted(inorder l @ x # inorder r)"
-unfolding inorder_splay[of x t, symmetric]
-by(induction x t arbitrary: l a r rule: splay.induct)
- (auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)
-
-lemma inorder_insert:
- "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
-using inorder_splay[of x t, symmetric] sorted_splay[of t x]
-by(auto simp: ins_list_simps ins_list_Cons ins_list_snoc neq_Leaf_iff split: tree.split)
-
-
-subsubsection "Proofs for delete"
-
-lemma inorder_splay_maxD:
- "splay_max t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
- inorder l @ [a] = inorder t \<and> r = Leaf"
-by(induction t arbitrary: l a r rule: splay_max.induct)
- (auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits)
-
-lemma inorder_delete:
- "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-using inorder_splay[of x t, symmetric] sorted_splay[of t x]
-by (auto simp: del_list_simps del_list_sorted_app delete_def
- del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff
- split: tree.splits)
-
-
-subsubsection "Overall Correctness"
-
-interpretation Set_by_Ordered
-where empty = Leaf and isin = isin and insert = insert
-and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
-proof (standard, goal_cases)
- case 2 thus ?case by(simp add: isin_set)
-next
- case 3 thus ?case by(simp add: inorder_insert del: insert.simps)
-next
- case 4 thus ?case by(simp add: inorder_delete)
-qed auto
-
-end
--- a/src/HOL/Probability/Probability_Mass_Function.thy Thu Aug 31 19:34:43 2017 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Aug 31 20:19:55 2017 +0200
@@ -529,6 +529,25 @@
shows "integral\<^sup>L (map_pmf g p) f = integral\<^sup>L p (\<lambda>x. f (g x))"
by (simp add: integral_distr map_pmf_rep_eq)
+lemma pmf_abs_summable [intro]: "pmf p abs_summable_on A"
+ by (rule abs_summable_on_subset[OF _ subset_UNIV])
+ (auto simp: abs_summable_on_def integrable_iff_bounded nn_integral_pmf)
+
+lemma measure_pmf_conv_infsetsum: "measure (measure_pmf p) A = infsetsum (pmf p) A"
+ unfolding infsetsum_def by (simp add: integral_eq_nn_integral nn_integral_pmf measure_def)
+
+lemma infsetsum_pmf_eq_1:
+ assumes "set_pmf p \<subseteq> A"
+ shows "infsetsum (pmf p) A = 1"
+proof -
+ have "infsetsum (pmf p) A = lebesgue_integral (count_space UNIV) (pmf p)"
+ using assms unfolding infsetsum_altdef
+ by (intro Bochner_Integration.integral_cong) (auto simp: indicator_def set_pmf_eq)
+ also have "\<dots> = 1"
+ by (subst integral_eq_nn_integral) (auto simp: nn_integral_pmf)
+ finally show ?thesis .
+qed
+
lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)"
by transfer (simp add: distr_return)
@@ -2079,6 +2098,20 @@
"measure (measure_pmf p) (A \<inter> set_pmf p) = measure (measure_pmf p) A"
using emeasure_Int_set_pmf[of p A] by (simp add: Sigma_Algebra.measure_def)
+lemma measure_prob_cong_0:
+ assumes "\<And>x. x \<in> A - B \<Longrightarrow> pmf p x = 0"
+ assumes "\<And>x. x \<in> B - A \<Longrightarrow> pmf p x = 0"
+ shows "measure (measure_pmf p) A = measure (measure_pmf p) B"
+proof -
+ have "measure_pmf.prob p A = measure_pmf.prob p (A \<inter> set_pmf p)"
+ by (simp add: measure_Int_set_pmf)
+ also have "A \<inter> set_pmf p = B \<inter> set_pmf p"
+ using assms by (auto simp: set_pmf_eq)
+ also have "measure_pmf.prob p \<dots> = measure_pmf.prob p B"
+ by (simp add: measure_Int_set_pmf)
+ finally show ?thesis .
+qed
+
lemma emeasure_pmf_of_list:
assumes "pmf_of_list_wf xs"
shows "emeasure (pmf_of_list xs) A = ennreal (sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
--- a/src/HOL/ROOT Thu Aug 31 19:34:43 2017 +0200
+++ b/src/HOL/ROOT Thu Aug 31 20:19:55 2017 +0200
@@ -212,7 +212,6 @@
Tree234_Map
Brother12_Map
AA_Map
- Splay_Map
Leftist_Heap
Binomial_Heap
document_files "root.tex" "root.bib"