--- a/src/HOL/Complete_Lattices.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy Tue May 17 19:27:42 2016 +0200
@@ -1276,6 +1276,8 @@
lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
by blast
+lemma inj_on_image: "inj_on f (\<Union>A) \<Longrightarrow> inj_on (op ` f) A"
+ unfolding inj_on_def by blast
subsubsection \<open>Distributive laws\<close>
--- a/src/HOL/Finite_Set.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Finite_Set.thy Tue May 17 19:27:42 2016 +0200
@@ -1501,6 +1501,41 @@
by (auto dest: card_subset_eq)
qed
+lemma remove_induct [case_names empty infinite remove]:
+ assumes empty: "P ({} :: 'a set)" and infinite: "\<not>finite B \<Longrightarrow> P B"
+ and remove: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
+ shows "P B"
+proof (cases "finite B")
+ assume "\<not>finite B"
+ thus ?thesis by (rule infinite)
+next
+ define A where "A = B"
+ assume "finite B"
+ hence "finite A" "A \<subseteq> B" by (simp_all add: A_def)
+ thus "P A"
+ proof (induction "card A" arbitrary: A)
+ case 0
+ hence "A = {}" by auto
+ with empty show ?case by simp
+ next
+ case (Suc n A)
+ from \<open>A \<subseteq> B\<close> and \<open>finite B\<close> have "finite A" by (rule finite_subset)
+ moreover from Suc.hyps have "A \<noteq> {}" by auto
+ moreover note \<open>A \<subseteq> B\<close>
+ moreover have "P (A - {x})" if x: "x \<in> A" for x
+ using x Suc.prems \<open>Suc n = card A\<close> by (intro Suc) auto
+ ultimately show ?case by (rule remove)
+ qed
+qed
+
+lemma finite_remove_induct [consumes 1, case_names empty remove]:
+ assumes finite: "finite B" and empty: "P ({} :: 'a set)"
+ and rm: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
+ defines "B' \<equiv> B"
+ shows "P B'"
+ by (induction B' rule: remove_induct) (simp_all add: assms)
+
+
text\<open>main cardinality theorem\<close>
lemma card_partition [rule_format]:
"finite C ==>
@@ -1562,6 +1597,10 @@
assumes "card A = 1" obtains x where "A = {x}"
using assms by (auto simp: card_Suc_eq)
+lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
+ unfolding is_singleton_def
+ by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
+
lemma card_le_Suc_iff: "finite A \<Longrightarrow>
Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
--- a/src/HOL/Groups_List.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Groups_List.thy Tue May 17 19:27:42 2016 +0200
@@ -255,6 +255,24 @@
finally show ?thesis by(simp add:listsum_map_eq_setsum_count)
qed
+lemma listsum_nonneg:
+ "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> listsum xs \<ge> 0"
+ by (induction xs) simp_all
+
+lemma listsum_map_filter:
+ "listsum (map f (filter P xs)) = listsum (map (\<lambda>x. if P x then f x else 0) xs)"
+ by (induction xs) simp_all
+
+lemma listsum_cong [fundef_cong]:
+ assumes "xs = ys"
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
+ shows "listsum (map f xs) = listsum (map g ys)"
+proof -
+ from assms(2) have "listsum (map f xs) = listsum (map g xs)"
+ by (induction xs) simp_all
+ with assms(1) show ?thesis by simp
+qed
+
subsection \<open>Further facts about @{const List.n_lists}\<close>
@@ -347,6 +365,16 @@
end
+lemma listprod_cong [fundef_cong]:
+ assumes "xs = ys"
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
+ shows "listprod (map f xs) = listprod (map g ys)"
+proof -
+ from assms(2) have "listprod (map f xs) = listprod (map g xs)"
+ by (induction xs) simp_all
+ with assms(1) show ?thesis by simp
+qed
+
text \<open>Some syntactic sugar:\<close>
syntax (ASCII)
--- a/src/HOL/Library/Disjoint_Sets.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Tue May 17 19:27:42 2016 +0200
@@ -38,6 +38,13 @@
"disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
unfolding disjoint_def by auto
+lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint (op ` f ` A)"
+ unfolding inj_on_def disjoint_def by blast
+
+lemma assumes "disjoint (A \<union> B)"
+ shows disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
+ using assms by (simp_all add: disjoint_def)
+
lemma disjoint_INT:
assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
@@ -84,7 +91,7 @@
lemma disjoint_family_on_disjoint_image:
"disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
unfolding disjoint_family_on_def disjoint_def by force
-
+
lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I"
by (auto simp: disjoint_family_on_def)
@@ -117,9 +124,60 @@
qed
qed
+lemma distinct_list_bind:
+ assumes "distinct xs" "\<And>x. x \<in> set xs \<Longrightarrow> distinct (f x)"
+ "disjoint_family_on (set \<circ> f) (set xs)"
+ shows "distinct (List.bind xs f)"
+ using assms
+ by (induction xs)
+ (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)
+
+lemma bij_betw_UNION_disjoint:
+ assumes disj: "disjoint_family_on A' I"
+ assumes bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
+ shows "bij_betw f (\<Union>i\<in>I. A i) (\<Union>i\<in>I. A' i)"
+unfolding bij_betw_def
+proof
+ from bij show eq: "f ` UNION I A = UNION I A'"
+ by (auto simp: bij_betw_def image_UN)
+ show "inj_on f (UNION I A)"
+ proof (rule inj_onI, clarify)
+ fix i j x y assume A: "i \<in> I" "j \<in> I" "x \<in> A i" "y \<in> A j" and B: "f x = f y"
+ from A bij[of i] bij[of j] have "f x \<in> A' i" "f y \<in> A' j"
+ by (auto simp: bij_betw_def)
+ with B have "A' i \<inter> A' j \<noteq> {}" by auto
+ with disj A have "i = j" unfolding disjoint_family_on_def by blast
+ with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
+ qed
+qed
+
lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
+text \<open>
+ The union of an infinite disjoint family of non-empty sets is infinite.
+\<close>
+lemma infinite_disjoint_family_imp_infinite_UNION:
+ assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A"
+ shows "\<not>finite (UNION A f)"
+proof -
+ def g \<equiv> "\<lambda>x. SOME y. y \<in> f x"
+ have g: "g x \<in> f x" if "x \<in> A" for x
+ unfolding g_def by (rule someI_ex, insert assms(2) that) blast
+ have inj_on_g: "inj_on g A"
+ proof (rule inj_onI, rule ccontr)
+ fix x y assume A: "x \<in> A" "y \<in> A" "g x = g y" "x \<noteq> y"
+ with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto
+ with A `x \<noteq> y` assms show False
+ by (auto simp: disjoint_family_on_def inj_on_def)
+ qed
+ from g have "g ` A \<subseteq> UNION A f" by blast
+ moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
+ using finite_imageD by blast
+ ultimately show ?thesis using finite_subset by blast
+qed
+
+
subsection \<open>Construct Disjoint Sequences\<close>
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 17 19:27:42 2016 +0200
@@ -864,6 +864,8 @@
declare [[coercion ennreal]]
+lemma ennreal_cong: "x = y \<Longrightarrow> ennreal x = ennreal y" by simp
+
lemma ennreal_cases[cases type: ennreal]:
fixes x :: ennreal
obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
@@ -949,6 +951,19 @@
lemma setsum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (setsum f I)"
by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)
+lemma listsum_ennreal[simp]:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0"
+ shows "listsum (map (\<lambda>x. ennreal (f x)) xs) = ennreal (listsum (map f xs))"
+using assms
+proof (induction xs)
+ case (Cons x xs)
+ from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (listsum (map f xs))"
+ by simp
+ also from Cons.prems have "\<dots> = ennreal (f x + listsum (map f xs))"
+ by (intro ennreal_plus [symmetric] listsum_nonneg) auto
+ finally show ?case by simp
+qed simp_all
+
lemma ennreal_of_nat_eq_real_of_nat: "of_nat i = ennreal (of_nat i)"
by (induction i) simp_all
--- a/src/HOL/Library/Extended_Real.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue May 17 19:27:42 2016 +0200
@@ -228,6 +228,8 @@
datatype ereal = ereal real | PInfty | MInfty
+lemma ereal_cong: "x = y \<Longrightarrow> ereal x = ereal y" by simp
+
instantiation ereal :: uminus
begin
@@ -771,6 +773,9 @@
then show ?thesis by simp
qed
+lemma listsum_ereal [simp]: "listsum (map (\<lambda>x. ereal (f x)) xs) = ereal (listsum (map f xs))"
+ by (induction xs) simp_all
+
lemma setsum_Pinfty:
fixes f :: "'a \<Rightarrow> ereal"
shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
--- a/src/HOL/Library/Indicator_Function.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Tue May 17 19:27:42 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Indicator Function\<close>
theory Indicator_Function
-imports Complex_Main
+imports Complex_Main Disjoint_Sets
begin
definition "indicator S x = (if x \<in> S then 1 else 0)"
@@ -28,6 +28,10 @@
lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A"
by (auto simp: indicator_def)
+lemma indicator_leI:
+ "(x \<in> A \<Longrightarrow> y \<in> B) \<Longrightarrow> (indicator A x :: 'a :: linordered_nonzero_semiring) \<le> indicator B y"
+ by (auto simp: indicator_def)
+
lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
unfolding indicator_def by auto
@@ -161,4 +165,14 @@
finally show ?thesis .
qed simp
+text \<open>
+ The indicator function of the union of a disjoint family of sets is the
+ sum over all the individual indicators.
+\<close>
+lemma indicator_UN_disjoint:
+ assumes "finite A" "disjoint_family_on f A"
+ shows "indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)"
+ using assms by (induction A rule: finite_induct)
+ (auto simp: disjoint_family_on_def indicator_def split: if_splits)
+
end
--- a/src/HOL/Library/Multiset.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Tue May 17 19:27:42 2016 +0200
@@ -417,6 +417,8 @@
qed
+
+
subsubsection \<open>Pointwise ordering induced by count\<close>
definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50)
@@ -1159,6 +1161,28 @@
lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
by (cases M) auto
+lemma image_mset_If:
+ "image_mset (\<lambda>x. if P x then f x else g x) A =
+ image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
+ by (induction A) (auto simp: add_ac)
+
+lemma image_mset_Diff:
+ assumes "B \<subseteq># A"
+ shows "image_mset f (A - B) = image_mset f A - image_mset f B"
+proof -
+ have "image_mset f (A - B + B) = image_mset f (A - B) + image_mset f B"
+ by simp
+ also from assms have "A - B + B = A"
+ by (simp add: subset_mset.diff_add)
+ finally show ?thesis by simp
+qed
+
+lemma count_image_mset:
+ "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
+ by (induction A)
+ (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
+
+
syntax (ASCII)
"_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ :# _#})")
syntax
@@ -1379,6 +1403,40 @@
lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
by (induct A rule: finite_induct) simp_all
+lemma mset_set_Union:
+ "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> mset_set (A \<union> B) = mset_set A + mset_set B"
+ by (induction A rule: finite_induct) (auto simp: add_ac)
+
+lemma filter_mset_mset_set [simp]:
+ "finite A \<Longrightarrow> filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
+proof (induction A rule: finite_induct)
+ case (insert x A)
+ from insert.hyps have "filter_mset P (mset_set (insert x A)) =
+ filter_mset P (mset_set A) + mset_set (if P x then {x} else {})"
+ by (simp add: add_ac)
+ also have "filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
+ by (rule insert.IH)
+ also from insert.hyps
+ have "\<dots> + mset_set (if P x then {x} else {}) =
+ mset_set ({x \<in> A. P x} \<union> (if P x then {x} else {}))" (is "_ = mset_set ?A")
+ by (intro mset_set_Union [symmetric]) simp_all
+ also from insert.hyps have "?A = {y\<in>insert x A. P y}" by auto
+ finally show ?case .
+qed simp_all
+
+lemma mset_set_Diff:
+ assumes "finite A" "B \<subseteq> A"
+ shows "mset_set (A - B) = mset_set A - mset_set B"
+proof -
+ from assms have "mset_set ((A - B) \<union> B) = mset_set (A - B) + mset_set B"
+ by (intro mset_set_Union) (auto dest: finite_subset)
+ also from assms have "A - B \<union> B = A" by blast
+ finally show ?thesis by simp
+qed
+
+lemma mset_set_set: "distinct xs \<Longrightarrow> mset_set (set xs) = mset xs"
+ by (induction xs) (simp_all add: add_ac)
+
context linorder
begin
@@ -1418,6 +1476,9 @@
"finite A \<Longrightarrow> set_mset (mset_set A) = A"
by (induct A rule: finite_induct) simp_all
+lemma mset_set_empty_iff: "mset_set A = {#} \<longleftrightarrow> A = {} \<or> infinite A"
+ using finite_set_mset_mset_set by fastforce
+
lemma infinite_set_mset_mset_set:
"\<not> finite A \<Longrightarrow> set_mset (mset_set A) = {}"
by simp
@@ -1430,6 +1491,22 @@
"sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps)
+lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
+ by (induction n) (simp_all add: atLeastLessThanSuc add_ac)
+
+lemma image_mset_map_of:
+ "distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
+proof (induction xs)
+ case (Cons x xs)
+ have "{#the (map_of (x # xs) i). i \<in># mset (map fst (x # xs))#} =
+ {#the (if i = fst x then Some (snd x) else map_of xs i).
+ i \<in># mset (map fst xs)#} + {#snd x#}" (is "_ = ?A + _") by simp
+ also from Cons.prems have "?A = {#the (map_of xs i). i :# mset (map fst xs)#}"
+ by (cases x, intro image_mset_cong) (auto simp: in_multiset_in_set)
+ also from Cons.prems have "\<dots> = mset (map snd xs)" by (intro Cons.IH) simp_all
+ finally show ?case by simp
+qed simp_all
+
subsection \<open>Replicate operation\<close>
@@ -1546,6 +1623,9 @@
(simp_all add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb not_in_iff)
qed
+lemma size_mset_set [simp]: "size (mset_set A) = card A"
+ by (simp only: size_eq_msetsum card_eq_setsum setsum_unfold_msetsum)
+
syntax (ASCII)
"_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
syntax
--- a/src/HOL/Library/Permutations.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Library/Permutations.thy Tue May 17 19:27:42 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Permutations, both general and specifically on finite sets.\<close>
theory Permutations
-imports Binomial
+imports Binomial Multiset Disjoint_Sets
begin
subsection \<open>Transpositions\<close>
@@ -30,6 +30,10 @@
lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
unfolding permutes_def by metis
+
+lemma permutes_not_in:
+ assumes "f permutes S" "x \<notin> S" shows "f x = x"
+ using assms by (auto simp: permutes_def)
lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S"
unfolding permutes_def
@@ -41,6 +45,9 @@
lemma permutes_inj: "p permutes S \<Longrightarrow> inj p"
unfolding permutes_def inj_on_def by blast
+lemma permutes_inj_on: "f permutes S \<Longrightarrow> inj_on f A"
+ unfolding permutes_def inj_on_def by auto
+
lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
unfolding permutes_def surj_def by metis
@@ -118,6 +125,25 @@
unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
by blast
+lemma permutes_invI:
+ assumes perm: "p permutes S"
+ and inv: "\<And>x. x \<in> S \<Longrightarrow> p' (p x) = x"
+ and outside: "\<And>x. x \<notin> S \<Longrightarrow> p' x = x"
+ shows "inv p = p'"
+proof
+ fix x show "inv p x = p' x"
+ proof (cases "x \<in> S")
+ assume [simp]: "x \<in> S"
+ from assms have "p' x = p' (p (inv p x))" by (simp add: permutes_inverses)
+ also from permutes_inv[OF perm]
+ have "\<dots> = inv p x" by (subst inv) (simp_all add: permutes_in_image)
+ finally show "inv p x = p' x" ..
+ qed (insert permutes_inv[OF perm], simp_all add: outside permutes_not_in)
+qed
+
+lemma permutes_vimage: "f permutes A \<Longrightarrow> f -` A = A"
+ by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv])
+
subsection \<open>The number of permutations on a finite set\<close>
@@ -813,9 +839,164 @@
lemma sign_idempotent: "sign p * sign p = 1"
by (simp add: sign_def)
+
+subsection \<open>Permuting a list\<close>
+
+text \<open>This function permutes a list by applying a permutation to the indices.\<close>
+
+definition permute_list :: "(nat \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "permute_list f xs = map (\<lambda>i. xs ! (f i)) [0..<length xs]"
+
+lemma permute_list_map:
+ assumes "f permutes {..<length xs}"
+ shows "permute_list f (map g xs) = map g (permute_list f xs)"
+ using permutes_in_image[OF assms] by (auto simp: permute_list_def)
+
+lemma permute_list_nth:
+ assumes "f permutes {..<length xs}" "i < length xs"
+ shows "permute_list f xs ! i = xs ! f i"
+ using permutes_in_image[OF assms(1)] assms(2)
+ by (simp add: permute_list_def)
+
+lemma permute_list_Nil [simp]: "permute_list f [] = []"
+ by (simp add: permute_list_def)
+
+lemma length_permute_list [simp]: "length (permute_list f xs) = length xs"
+ by (simp add: permute_list_def)
+
+lemma permute_list_compose:
+ assumes "g permutes {..<length xs}"
+ shows "permute_list (f \<circ> g) xs = permute_list g (permute_list f xs)"
+ using assms[THEN permutes_in_image] by (auto simp add: permute_list_def)
+
+lemma permute_list_ident [simp]: "permute_list (\<lambda>x. x) xs = xs"
+ by (simp add: permute_list_def map_nth)
+
+lemma permute_list_id [simp]: "permute_list id xs = xs"
+ by (simp add: id_def)
+
+lemma mset_permute_list [simp]:
+ assumes "f permutes {..<length (xs :: 'a list)}"
+ shows "mset (permute_list f xs) = mset xs"
+proof (rule multiset_eqI)
+ fix y :: 'a
+ from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x
+ using permutes_in_image[OF assms] by auto
+ have "count (mset (permute_list f xs)) y =
+ card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"
+ by (simp add: permute_list_def mset_map count_image_mset atLeast0LessThan)
+ also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}"
+ by auto
+ also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"
+ by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj)
+ also have "\<dots> = count (mset xs) y" by (simp add: count_mset length_filter_conv_card)
+ finally show "count (mset (permute_list f xs)) y = count (mset xs) y" by simp
+qed
+
+lemma set_permute_list [simp]:
+ assumes "f permutes {..<length xs}"
+ shows "set (permute_list f xs) = set xs"
+ by (rule mset_eq_setD[OF mset_permute_list]) fact
+
+lemma distinct_permute_list [simp]:
+ assumes "f permutes {..<length xs}"
+ shows "distinct (permute_list f xs) = distinct xs"
+ by (simp add: distinct_count_atmost_1 assms)
+
+lemma permute_list_zip:
+ assumes "f permutes A" "A = {..<length xs}"
+ assumes [simp]: "length xs = length ys"
+ shows "permute_list f (zip xs ys) = zip (permute_list f xs) (permute_list f ys)"
+proof -
+ from permutes_in_image[OF assms(1)] assms(2)
+ have [simp]: "f i < length ys \<longleftrightarrow> i < length ys" for i by simp
+ have "permute_list f (zip xs ys) = map (\<lambda>i. zip xs ys ! f i) [0..<length ys]"
+ by (simp_all add: permute_list_def zip_map_map)
+ also have "\<dots> = map (\<lambda>(x, y). (xs ! f x, ys ! f y)) (zip [0..<length ys] [0..<length ys])"
+ by (intro nth_equalityI) simp_all
+ also have "\<dots> = zip (permute_list f xs) (permute_list f ys)"
+ by (simp_all add: permute_list_def zip_map_map)
+ finally show ?thesis .
+qed
+
+lemma map_of_permute:
+ assumes "\<sigma> permutes fst ` set xs"
+ shows "map_of xs \<circ> \<sigma> = map_of (map (\<lambda>(x,y). (inv \<sigma> x, y)) xs)" (is "_ = map_of (map ?f _)")
+proof
+ fix x
+ from assms have "inj \<sigma>" "surj \<sigma>" by (simp_all add: permutes_inj permutes_surj)
+ thus "(map_of xs \<circ> \<sigma>) x = map_of (map ?f xs) x"
+ by (induction xs) (auto simp: inv_f_f surj_f_inv_f)
+qed
+
subsection \<open>More lemmas about permutations\<close>
+text \<open>
+ If two lists correspond to the same multiset, there exists a permutation
+ on the list indices that maps one to the other.
+\<close>
+lemma mset_eq_permutation:
+ assumes mset_eq: "mset (xs::'a list) = mset ys"
+ defines [simp]: "n \<equiv> length xs"
+ obtains f where "f permutes {..<length ys}" "permute_list f ys = xs"
+proof -
+ from mset_eq have [simp]: "length xs = length ys"
+ by (rule mset_eq_length)
+ def indices_of \<equiv> "\<lambda>(x::'a) xs. {i. i < length xs \<and> x = xs ! i}"
+ have indices_of_subset: "indices_of x xs \<subseteq> {..<length xs}" for x xs
+ unfolding indices_of_def by blast
+ have [simp]: "finite (indices_of x xs)" for x xs
+ by (rule finite_subset[OF indices_of_subset]) simp_all
+
+ have "\<forall>x\<in>set xs. \<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)"
+ proof
+ fix x
+ from mset_eq have "count (mset xs) x = count (mset ys) x" by simp
+ hence "card (indices_of x xs) = card (indices_of x ys)"
+ by (simp add: count_mset length_filter_conv_card indices_of_def)
+ thus "\<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)"
+ by (intro finite_same_card_bij) simp_all
+ qed
+ hence "\<exists>f. \<forall>x\<in>set xs. bij_betw (f x) (indices_of x xs) (indices_of x ys)"
+ by (rule bchoice)
+ then guess f .. note f = this
+ def g \<equiv> "\<lambda>i. if i < n then f (xs ! i) i else i"
+
+ have bij_f: "bij_betw (\<lambda>i. f (xs ! i) i) (indices_of x xs) (indices_of x ys)"
+ if x: "x \<in> set xs" for x
+ proof (subst bij_betw_cong)
+ from f x show "bij_betw (f x) (indices_of x xs) (indices_of x ys)" by blast
+ fix i assume "i \<in> indices_of x xs"
+ thus "f (xs ! i) i = f x i" by (simp add: indices_of_def)
+ qed
+
+ hence "bij_betw (\<lambda>i. f (xs ! i) i) (\<Union>x\<in>set xs. indices_of x xs) (\<Union>x\<in>set xs. indices_of x ys)"
+ by (intro bij_betw_UNION_disjoint) (auto simp add: disjoint_family_on_def indices_of_def)
+ also have "(\<Union>x\<in>set xs. indices_of x xs) = {..<n}" by (auto simp: indices_of_def)
+ also from mset_eq have "set xs = set ys" by (rule mset_eq_setD)
+ also have "(\<Union>x\<in>set ys. indices_of x ys) = {..<n}"
+ by (auto simp: indices_of_def set_conv_nth)
+ also have "bij_betw (\<lambda>i. f (xs ! i) i) {..<n} {..<n} \<longleftrightarrow> bij_betw g {..<n} {..<n}"
+ by (intro bij_betw_cong) (simp_all add: g_def)
+ finally have "g permutes {..<length ys}"
+ by (intro bij_imp_permutes refl) (simp_all add: g_def)
+
+ moreover have "permute_list g ys = xs"
+ proof (rule sym, intro nth_equalityI allI impI)
+ fix i assume i: "i < length xs"
+ from i have "permute_list g ys ! i = ys ! f (xs ! i) i"
+ by (simp add: permute_list_def g_def)
+ also from i have "i \<in> indices_of (xs ! i) xs" by (simp add: indices_of_def)
+ with bij_f[of "xs ! i"] i have "f (xs ! i) i \<in> indices_of (xs ! i) ys"
+ by (auto simp: bij_betw_def)
+ hence "ys ! f (xs ! i) i = xs ! i" by (simp add: indices_of_def)
+ finally show "xs ! i = permute_list g ys ! i" ..
+ qed simp_all
+
+ ultimately show ?thesis by (rule that)
+qed
+
lemma permutes_natset_le:
fixes S :: "'a::wellorder set"
assumes p: "p permutes S"
@@ -1047,5 +1228,154 @@
qed
qed
+
+subsection \<open>Constructing permutations from association lists\<close>
+
+definition list_permutes where
+ "list_permutes xs A \<longleftrightarrow> set (map fst xs) \<subseteq> A \<and> set (map snd xs) = set (map fst xs) \<and>
+ distinct (map fst xs) \<and> distinct (map snd xs)"
+
+lemma list_permutesI [simp]:
+ assumes "set (map fst xs) \<subseteq> A" "set (map snd xs) = set (map fst xs)" "distinct (map fst xs)"
+ shows "list_permutes xs A"
+proof -
+ from assms(2,3) have "distinct (map snd xs)"
+ by (intro card_distinct) (simp_all add: distinct_card del: set_map)
+ with assms show ?thesis by (simp add: list_permutes_def)
+qed
+
+definition permutation_of_list where
+ "permutation_of_list xs x = (case map_of xs x of None \<Rightarrow> x | Some y \<Rightarrow> y)"
+
+lemma permutation_of_list_Cons:
+ "permutation_of_list ((x,y) # xs) x' = (if x = x' then y else permutation_of_list xs x')"
+ by (simp add: permutation_of_list_def)
+
+fun inverse_permutation_of_list where
+ "inverse_permutation_of_list [] x = x"
+| "inverse_permutation_of_list ((y,x')#xs) x =
+ (if x = x' then y else inverse_permutation_of_list xs x)"
+
+declare inverse_permutation_of_list.simps [simp del]
+
+lemma inj_on_map_of:
+ assumes "distinct (map snd xs)"
+ shows "inj_on (map_of xs) (set (map fst xs))"
+proof (rule inj_onI)
+ fix x y assume xy: "x \<in> set (map fst xs)" "y \<in> set (map fst xs)"
+ assume eq: "map_of xs x = map_of xs y"
+ from xy obtain x' y'
+ where x'y': "map_of xs x = Some x'" "map_of xs y = Some y'"
+ by (cases "map_of xs x"; cases "map_of xs y")
+ (simp_all add: map_of_eq_None_iff)
+ moreover from this x'y' have "(x,x') \<in> set xs" "(y,y') \<in> set xs"
+ by (force dest: map_of_SomeD)+
+ moreover from this eq x'y' have "x' = y'" by simp
+ ultimately show "x = y" using assms
+ by (force simp: distinct_map dest: inj_onD[of _ _ "(x,x')" "(y,y')"])
+qed
+
+lemma inj_on_the: "None \<notin> A \<Longrightarrow> inj_on the A"
+ by (auto simp: inj_on_def option.the_def split: option.splits)
+
+lemma inj_on_map_of':
+ assumes "distinct (map snd xs)"
+ shows "inj_on (the \<circ> map_of xs) (set (map fst xs))"
+ by (intro comp_inj_on inj_on_map_of assms inj_on_the)
+ (force simp: eq_commute[of None] map_of_eq_None_iff)
+
+lemma image_map_of:
+ assumes "distinct (map fst xs)"
+ shows "map_of xs ` set (map fst xs) = Some ` set (map snd xs)"
+ using assms by (auto simp: rev_image_eqI)
+
+lemma the_Some_image [simp]: "the ` Some ` A = A"
+ by (subst image_image) simp
+
+lemma image_map_of':
+ assumes "distinct (map fst xs)"
+ shows "(the \<circ> map_of xs) ` set (map fst xs) = set (map snd xs)"
+ by (simp only: image_comp [symmetric] image_map_of assms the_Some_image)
+
+lemma permutation_of_list_permutes [simp]:
+ assumes "list_permutes xs A"
+ shows "permutation_of_list xs permutes A" (is "?f permutes _")
+proof (rule permutes_subset[OF bij_imp_permutes])
+ from assms show "set (map fst xs) \<subseteq> A"
+ by (simp add: list_permutes_def)
+ from assms have "inj_on (the \<circ> map_of xs) (set (map fst xs))" (is ?P)
+ by (intro inj_on_map_of') (simp_all add: list_permutes_def)
+ also have "?P \<longleftrightarrow> inj_on ?f (set (map fst xs))"
+ by (intro inj_on_cong)
+ (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)
+ finally have "bij_betw ?f (set (map fst xs)) (?f ` set (map fst xs))"
+ by (rule inj_on_imp_bij_betw)
+ also from assms have "?f ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)"
+ by (intro image_cong refl)
+ (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)
+ also from assms have "\<dots> = set (map fst xs)"
+ by (subst image_map_of') (simp_all add: list_permutes_def)
+ finally show "bij_betw ?f (set (map fst xs)) (set (map fst xs))" .
+qed (force simp: permutation_of_list_def dest!: map_of_SomeD split: option.splits)+
+
+lemma eval_permutation_of_list [simp]:
+ "permutation_of_list [] x = x"
+ "x = x' \<Longrightarrow> permutation_of_list ((x',y)#xs) x = y"
+ "x \<noteq> x' \<Longrightarrow> permutation_of_list ((x',y')#xs) x = permutation_of_list xs x"
+ by (simp_all add: permutation_of_list_def)
+
+lemma eval_inverse_permutation_of_list [simp]:
+ "inverse_permutation_of_list [] x = x"
+ "x = x' \<Longrightarrow> inverse_permutation_of_list ((y,x')#xs) x = y"
+ "x \<noteq> x' \<Longrightarrow> inverse_permutation_of_list ((y',x')#xs) x = inverse_permutation_of_list xs x"
+ by (simp_all add: inverse_permutation_of_list.simps)
+
+lemma permutation_of_list_id:
+ assumes "x \<notin> set (map fst xs)"
+ shows "permutation_of_list xs x = x"
+ using assms by (induction xs) (auto simp: permutation_of_list_Cons)
+
+lemma permutation_of_list_unique':
+ assumes "distinct (map fst xs)" "(x, y) \<in> set xs"
+ shows "permutation_of_list xs x = y"
+ using assms by (induction xs) (force simp: permutation_of_list_Cons)+
+
+lemma permutation_of_list_unique:
+ assumes "list_permutes xs A" "(x,y) \<in> set xs"
+ shows "permutation_of_list xs x = y"
+ using assms by (intro permutation_of_list_unique') (simp_all add: list_permutes_def)
+
+lemma inverse_permutation_of_list_id:
+ assumes "x \<notin> set (map snd xs)"
+ shows "inverse_permutation_of_list xs x = x"
+ using assms by (induction xs) auto
+
+lemma inverse_permutation_of_list_unique':
+ assumes "distinct (map snd xs)" "(x, y) \<in> set xs"
+ shows "inverse_permutation_of_list xs y = x"
+ using assms by (induction xs) (force simp: inverse_permutation_of_list.simps)+
+
+lemma inverse_permutation_of_list_unique:
+ assumes "list_permutes xs A" "(x,y) \<in> set xs"
+ shows "inverse_permutation_of_list xs y = x"
+ using assms by (intro inverse_permutation_of_list_unique') (simp_all add: list_permutes_def)
+
+lemma inverse_permutation_of_list_correct:
+ assumes "list_permutes xs (A :: 'a set)"
+ shows "inverse_permutation_of_list xs = inv (permutation_of_list xs)"
+proof (rule ext, rule sym, subst permutes_inv_eq)
+ from assms show "permutation_of_list xs permutes A" by simp
+next
+ fix x
+ show "permutation_of_list xs (inverse_permutation_of_list xs x) = x"
+ proof (cases "x \<in> set (map snd xs)")
+ case True
+ then obtain y where "(y, x) \<in> set xs" by force
+ with assms show ?thesis
+ by (simp add: inverse_permutation_of_list_unique permutation_of_list_unique)
+ qed (insert assms, auto simp: list_permutes_def
+ inverse_permutation_of_list_id permutation_of_list_id)
+qed
+
end
--- a/src/HOL/List.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/List.thy Tue May 17 19:27:42 2016 +0200
@@ -3298,9 +3298,19 @@
"\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
by(auto simp: distinct_conv_nth)
+lemma distinct_Ex1:
+ "distinct xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> (\<exists>!i. i < length xs \<and> xs ! i = x)"
+ by (auto simp: in_set_conv_nth nth_eq_iff_index_eq)
+
lemma inj_on_nth: "distinct xs \<Longrightarrow> \<forall>i \<in> I. i < length xs \<Longrightarrow> inj_on (nth xs) I"
by (rule inj_onI) (simp add: nth_eq_iff_index_eq)
+lemma bij_betw_nth:
+ assumes "distinct xs" "A = {..<length xs}" "B = set xs"
+ shows "bij_betw (op ! xs) A B"
+ using assms unfolding bij_betw_def
+ by (auto intro!: inj_on_nth simp: set_conv_nth)
+
lemma set_update_distinct: "\<lbrakk> distinct xs; n < length xs \<rbrakk> \<Longrightarrow>
set(xs[n := x]) = insert x (set xs - {xs!n})"
by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq)
@@ -6175,6 +6185,18 @@
"List.bind (x # xs) f = f x @ List.bind xs f"
by (simp_all add: bind_def)
+lemma list_bind_cong [fundef_cong]:
+ assumes "xs = ys" "(\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)"
+ shows "List.bind xs f = List.bind ys g"
+proof -
+ from assms(2) have "List.bind xs f = List.bind xs g"
+ by (induction xs) simp_all
+ with assms(1) show ?thesis by simp
+qed
+
+lemma set_list_bind: "set (List.bind xs f) = (\<Union>x\<in>set xs. set (f x))"
+ by (induction xs) simp_all
+
subsection \<open>Transfer\<close>
--- a/src/HOL/Nat.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Nat.thy Tue May 17 19:27:42 2016 +0200
@@ -1758,6 +1758,10 @@
shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
by (auto dest!: le_Suc_ex)
+lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> (a::nat)"
+ by (force dest: le_Suc_ex)
+
+
text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
lemma diff_le_mono:
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue May 17 19:27:42 2016 +0200
@@ -167,6 +167,12 @@
lemma pmf_nonneg[simp]: "0 \<le> pmf p x"
by transfer simp
+
+lemma pmf_not_neg [simp]: "\<not>pmf p x < 0"
+ by (simp add: not_less pmf_nonneg)
+
+lemma pmf_pos [simp]: "pmf p x \<noteq> 0 \<Longrightarrow> pmf p x > 0"
+ using pmf_nonneg[of p x] by linarith
lemma pmf_le_1: "pmf p x \<le> 1"
by (simp add: pmf.rep_eq)
@@ -183,6 +189,13 @@
lemma set_pmf_eq: "set_pmf M = {x. pmf M x \<noteq> 0}"
by (auto simp: set_pmf_iff)
+lemma set_pmf_eq': "set_pmf p = {x. pmf p x > 0}"
+proof safe
+ fix x assume "x \<in> set_pmf p"
+ hence "pmf p x \<noteq> 0" by (auto simp: set_pmf_eq)
+ with pmf_nonneg[of p x] show "pmf p x > 0" by simp
+qed (auto simp: set_pmf_eq)
+
lemma emeasure_pmf_single:
fixes M :: "'a pmf"
shows "emeasure M {x} = pmf M x"
@@ -198,6 +211,17 @@
using emeasure_measure_pmf_finite[of S M]
by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg setsum_nonneg pmf_nonneg)
+lemma setsum_pmf_eq_1:
+ assumes "finite A" "set_pmf p \<subseteq> A"
+ shows "(\<Sum>x\<in>A. pmf p x) = 1"
+proof -
+ have "(\<Sum>x\<in>A. pmf p x) = measure_pmf.prob p A"
+ by (simp add: measure_measure_pmf_finite assms)
+ also from assms have "\<dots> = 1"
+ by (subst measure_pmf.prob_eq_1) (auto simp: AE_measure_pmf_iff)
+ finally show ?thesis .
+qed
+
lemma nn_integral_measure_pmf_support:
fixes f :: "'a \<Rightarrow> ennreal"
assumes f: "finite A" and nn: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> set_pmf M \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = 0"
@@ -339,6 +363,8 @@
done
qed
+adhoc_overloading Monad_Syntax.bind bind_pmf
+
lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
unfolding pmf.rep_eq bind_pmf.rep_eq
by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg
@@ -363,7 +389,7 @@
finally show ?thesis .
qed
-lemma bind_pmf_cong:
+lemma bind_pmf_cong [fundef_cong]:
assumes "p = q"
shows "(\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g"
unfolding \<open>p = q\<close>[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq
@@ -518,6 +544,15 @@
lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x"
unfolding return_pmf.rep_eq by (intro emeasure_return) auto
+lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x"
+proof -
+ have "ennreal (measure_pmf.prob (return_pmf x) A) =
+ emeasure (measure_pmf (return_pmf x)) A"
+ by (simp add: measure_pmf.emeasure_eq_measure)
+ also have "\<dots> = ennreal (indicator A x)" by (simp add: ennreal_indicator)
+ finally show ?thesis by simp
+qed
+
lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y"
by (metis insertI1 set_return_pmf singletonD)
@@ -732,6 +767,27 @@
lemma pmf_eq_iff: "M = N \<longleftrightarrow> (\<forall>i. pmf M i = pmf N i)"
by (auto intro: pmf_eqI)
+lemma pmf_neq_exists_less:
+ assumes "M \<noteq> N"
+ shows "\<exists>x. pmf M x < pmf N x"
+proof (rule ccontr)
+ assume "\<not>(\<exists>x. pmf M x < pmf N x)"
+ hence ge: "pmf M x \<ge> pmf N x" for x by (auto simp: not_less)
+ from assms obtain x where "pmf M x \<noteq> pmf N x" by (auto simp: pmf_eq_iff)
+ with ge[of x] have gt: "pmf M x > pmf N x" by simp
+ have "1 = measure (measure_pmf M) UNIV" by simp
+ also have "\<dots> = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})"
+ by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
+ also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}"
+ by (simp add: measure_pmf_single)
+ also have "measure (measure_pmf N) (UNIV - {x}) \<le> measure (measure_pmf M) (UNIV - {x})"
+ by (subst (1 2) integral_pmf [symmetric])
+ (intro integral_mono integrable_pmf, simp_all add: ge)
+ also have "measure (measure_pmf M) {x} + \<dots> = 1"
+ by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
+ finally show False by simp_all
+qed
+
lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))"
unfolding pmf_eq_iff pmf_bind
proof
@@ -904,6 +960,9 @@
end
+lemma measure_pmf_posI: "x \<in> set_pmf p \<Longrightarrow> x \<in> A \<Longrightarrow> measure_pmf.prob p A > 0"
+ using measure_measure_pmf_not_zero[of p A] by (subst zero_less_measure_iff) blast
+
lemma cond_map_pmf:
assumes "set_pmf p \<inter> f -` s \<noteq> {}"
shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
@@ -1568,6 +1627,31 @@
end
+lemma map_pmf_of_set:
+ assumes "finite A" "A \<noteq> {}"
+ shows "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))"
+ (is "?lhs = ?rhs")
+proof (intro pmf_eqI)
+ fix x
+ from assms have "ennreal (pmf ?lhs x) = ennreal (pmf ?rhs x)"
+ by (subst ennreal_pmf_map)
+ (simp_all add: emeasure_pmf_of_set mset_set_empty_iff count_image_mset Int_commute)
+ thus "pmf ?lhs x = pmf ?rhs x" by simp
+qed
+
+lemma pmf_bind_pmf_of_set:
+ assumes "A \<noteq> {}" "finite A"
+ shows "pmf (bind_pmf (pmf_of_set A) f) x =
+ (\<Sum>xa\<in>A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs")
+proof -
+ from assms have "card A > 0" by auto
+ with assms have "ennreal ?lhs = ennreal ?rhs"
+ by (subst ennreal_pmf_bind)
+ (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric]
+ setsum_nonneg ennreal_of_nat_eq_real_of_nat)
+ thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg)
+qed
+
lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
by(rule pmf_eqI)(simp add: indicator_def)
@@ -1590,6 +1674,38 @@
qed
qed
+text \<open>
+ Choosing an element uniformly at random from the union of a disjoint family
+ of finite non-empty sets with the same size is the same as first choosing a set
+ from the family uniformly at random and then choosing an element from the chosen set
+ uniformly at random.
+\<close>
+lemma pmf_of_set_UN:
+ assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
+ "\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A"
+ shows "pmf_of_set (UNION A f) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
+ (is "?lhs = ?rhs")
+proof (intro pmf_eqI)
+ fix x
+ from assms have [simp]: "finite A"
+ using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast
+ from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) =
+ ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))"
+ by (subst pmf_of_set) auto
+ also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
+ by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
+ also from assms
+ have "indicator (\<Union>x\<in>A. f x) x / real \<dots> =
+ indicator (\<Union>x\<in>A. f x) x / (n * real (card A))"
+ by (simp add: setsum_divide_distrib [symmetric] mult_ac)
+ also from assms have "indicator (\<Union>x\<in>A. f x) x = (\<Sum>y\<in>A. indicator (f y) x)"
+ by (intro indicator_UN_disjoint) simp_all
+ also from assms have "ereal ((\<Sum>y\<in>A. indicator (f y) x) / (real n * real (card A))) =
+ ereal (pmf ?rhs x)"
+ by (subst pmf_bind_pmf_of_set) (simp_all add: setsum_divide_distrib)
+ finally show "pmf ?lhs x = pmf ?rhs x" by simp
+qed
+
lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
by (rule pmf_eqI) simp_all
@@ -1670,4 +1786,139 @@
end
+
+subsection \<open>PMFs from assiciation lists\<close>
+
+definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
+ "pmf_of_list xs = embed_pmf (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+
+definition pmf_of_list_wf where
+ "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> listsum (map snd xs) = 1"
+
+lemma pmf_of_list_wfI:
+ "(\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum (map snd xs) = 1 \<Longrightarrow> pmf_of_list_wf xs"
+ unfolding pmf_of_list_wf_def by simp
+
+context
+begin
+
+private lemma pmf_of_list_aux:
+ assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
+ assumes "listsum (map snd xs) = 1"
+ shows "(\<integral>\<^sup>+ x. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
+proof -
+ have "(\<integral>\<^sup>+ x. ennreal (listsum (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
+ (\<integral>\<^sup>+ x. ennreal (listsum (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
+ by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter) (auto intro: listsum_cong)
+ also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. (\<integral>\<^sup>+ x. ennreal (indicator {x'} x * p) \<partial>count_space UNIV))"
+ using assms(1)
+ proof (induction xs)
+ case (Cons x xs)
+ from Cons.prems have "snd x \<ge> 0" by simp
+ moreover have "b \<ge> 0" if "(a,b) \<in> set xs" for a b
+ using Cons.prems[of b] that by force
+ ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) =
+ (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
+ ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
+ by (intro nn_integral_cong, subst ennreal_plus [symmetric])
+ (auto simp: case_prod_unfold indicator_def intro!: listsum_nonneg)
+ also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
+ (\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
+ by (intro nn_integral_add)
+ (force intro!: listsum_nonneg AE_I2 intro: Cons simp: indicator_def)+
+ also have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV) =
+ (\<Sum>(x', p)\<leftarrow>xs. (\<integral>\<^sup>+ y. ennreal (indicator {x'} y * p) \<partial>count_space UNIV))"
+ using Cons(1) by (intro Cons) simp_all
+ finally show ?case by (simp add: case_prod_unfold)
+ qed simp
+ also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. ennreal p * (\<integral>\<^sup>+ x. indicator {x'} x \<partial>count_space UNIV))"
+ using assms(1)
+ by (intro listsum_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
+ (auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator
+ simp del: times_ereal.simps)+
+ also from assms have "\<dots> = listsum (map snd xs)" by (simp add: case_prod_unfold listsum_ennreal)
+ also have "\<dots> = 1" using assms(2) by simp
+ finally show ?thesis .
+qed
+
+lemma pmf_pmf_of_list:
+ assumes "pmf_of_list_wf xs"
+ shows "pmf (pmf_of_list xs) x = listsum (map snd (filter (\<lambda>z. fst z = x) xs))"
+ using assms pmf_of_list_aux[of xs] unfolding pmf_of_list_def pmf_of_list_wf_def
+ by (subst pmf_embed_pmf) (auto intro!: listsum_nonneg)
+
end
+
+lemma set_pmf_of_list:
+ assumes "pmf_of_list_wf xs"
+ shows "set_pmf (pmf_of_list xs) \<subseteq> set (map fst xs)"
+proof clarify
+ fix x assume A: "x \<in> set_pmf (pmf_of_list xs)"
+ show "x \<in> set (map fst xs)"
+ proof (rule ccontr)
+ assume "x \<notin> set (map fst xs)"
+ hence "[z\<leftarrow>xs . fst z = x] = []" by (auto simp: filter_empty_conv)
+ with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq)
+ qed
+qed
+
+lemma finite_set_pmf_of_list:
+ assumes "pmf_of_list_wf xs"
+ shows "finite (set_pmf (pmf_of_list xs))"
+ using assms by (rule finite_subset[OF set_pmf_of_list]) simp_all
+
+lemma emeasure_Int_set_pmf:
+ "emeasure (measure_pmf p) (A \<inter> set_pmf p) = emeasure (measure_pmf p) A"
+ by (rule emeasure_eq_AE) (auto simp: AE_measure_pmf_iff)
+
+lemma measure_Int_set_pmf:
+ "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 emeasure_pmf_of_list:
+ assumes "pmf_of_list_wf xs"
+ shows "emeasure (pmf_of_list xs) A = ennreal (listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
+proof -
+ have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
+ by simp
+ also from assms
+ have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])))"
+ by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
+ also from assms
+ have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. listsum (map snd [z\<leftarrow>xs . fst z = x]))"
+ by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: listsum_nonneg)
+ also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
+ indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
+ using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
+ also have "?S = (\<Sum>x\<in>set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)"
+ using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
+ also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
+ using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
+ also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
+ listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+ using assms by (simp add: pmf_pmf_of_list)
+ also have "\<dots> = (\<Sum>x\<in>set (map fst xs). listsum (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
+ by (intro setsum.cong) (auto simp: indicator_def)
+ also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
+ if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
+ by (intro setsum.cong refl, subst listsum_map_filter, subst listsum_setsum_nth) simp
+ also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
+ if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
+ by (rule setsum.commute)
+ also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
+ (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
+ by (auto intro!: setsum.cong setsum.neutral)
+ also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
+ by (intro setsum.cong refl) (simp_all add: setsum.delta)
+ also have "\<dots> = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
+ by (subst listsum_map_filter, subst listsum_setsum_nth) simp_all
+ finally show ?thesis .
+qed
+
+lemma measure_pmf_of_list:
+ assumes "pmf_of_list_wf xs"
+ shows "measure (pmf_of_list xs) A = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
+ using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def
+ by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: listsum_nonneg)
+
+end
--- a/src/HOL/Probability/Probability_Measure.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Tue May 17 19:27:42 2016 +0200
@@ -111,6 +111,9 @@
lemma (in prob_space) emeasure_le_1: "emeasure M S \<le> 1"
unfolding ennreal_1[symmetric] emeasure_eq_measure by (subst ennreal_le_iff) auto
+lemma (in prob_space) emeasure_ge_1_iff: "emeasure M A \<ge> 1 \<longleftrightarrow> emeasure M A = 1"
+ by (rule iffI, intro antisym emeasure_le_1) simp_all
+
lemma (in prob_space) AE_iff_emeasure_eq_1:
assumes [measurable]: "Measurable.pred M P"
shows "(AE x in M. P x) \<longleftrightarrow> emeasure M {x\<in>space M. P x} = 1"
@@ -125,6 +128,9 @@
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1"
using emeasure_space[of M X] by (simp add: emeasure_space_1)
+lemma (in prob_space) measure_ge_1_iff: "measure M A \<ge> 1 \<longleftrightarrow> measure M A = 1"
+ by (auto intro!: antisym)
+
lemma (in prob_space) AE_I_eq_1:
assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
shows "AE x in M. P x"
--- a/src/HOL/Set.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Set.thy Tue May 17 19:27:42 2016 +0200
@@ -1803,6 +1803,21 @@
lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
by blast
+
+subsubsection \<open>Singleton sets\<close>
+
+definition is_singleton :: "'a set \<Rightarrow> bool" where
+ "is_singleton A \<longleftrightarrow> (\<exists>x. A = {x})"
+
+lemma is_singletonI [simp, intro!]: "is_singleton {x}"
+ unfolding is_singleton_def by simp
+
+lemma is_singletonI': "A \<noteq> {} \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y) \<Longrightarrow> is_singleton A"
+ unfolding is_singleton_def by blast
+
+lemma is_singletonE: "is_singleton A \<Longrightarrow> (\<And>x. A = {x} \<Longrightarrow> P) \<Longrightarrow> P"
+ unfolding is_singleton_def by blast
+
subsubsection \<open>Getting the Contents of a Singleton Set\<close>
@@ -1812,6 +1827,9 @@
lemma the_elem_eq [simp]: "the_elem {x} = x"
by (simp add: the_elem_def)
+lemma is_singleton_the_elem: "is_singleton A \<longleftrightarrow> A = {the_elem A}"
+ by (auto simp: is_singleton_def)
+
lemma the_elem_image_unique:
assumes "A \<noteq> {}"
assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
@@ -1916,6 +1934,9 @@
lemma pairwise_singleton [simp]: "pairwise P {A}"
by (simp add: pairwise_def)
+lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
+ by blast
+
hide_const (open) member not_member
lemmas equalityI = subset_antisym
--- a/src/HOL/Set_Interval.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Set_Interval.thy Tue May 17 19:27:42 2016 +0200
@@ -1640,6 +1640,10 @@
finally show ?case .
qed
+lemma setsum_lessThan_Suc_shift:
+ "(\<Sum>i<Suc n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
+ by (induction n) (simp_all add: add_ac)
+
lemma setsum_atMost_shift:
fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
shows "(\<Sum>i\<le>n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
--- a/src/HOL/Wellfounded.thy Tue May 17 11:16:39 2016 +0200
+++ b/src/HOL/Wellfounded.thy Tue May 17 19:27:42 2016 +0200
@@ -112,6 +112,10 @@
obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
using Q wfE_pf[OF wf, of Q] by blast
+lemma wfE_min':
+ "wf R \<Longrightarrow> Q \<noteq> {} \<Longrightarrow> (\<And>z. z \<in> Q \<Longrightarrow> (\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q) \<Longrightarrow> thesis) \<Longrightarrow> thesis"
+ using wfE_min[of R _ Q] by blast
+
lemma wfI_min:
assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
shows "wf R"
@@ -918,6 +922,19 @@
apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
done
+lemma finite_subset_wf:
+ assumes "finite A"
+ shows "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
+proof (intro finite_acyclic_wf)
+ have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A" by blast
+ thus "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
+ by (rule finite_subset) (auto simp: assms finite_cartesian_product)
+next
+ have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}"
+ by (intro trancl_id transI) blast
+ also have " \<forall>x. (x, x) \<notin> \<dots>" by blast
+ finally show "acyclic {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" by (rule acyclicI)
+qed
hide_const (open) acc accp