Moved material from AFP/Randomised_Social_Choice to distribution
authoreberlm
Tue May 17 17:05:35 2016 +0200 (2016-05-17)
changeset 63099af0e964aad7b
parent 63097 ee8edbcbb4ad
child 63100 aa5cffd8a606
Moved material from AFP/Randomised_Social_Choice to distribution
src/HOL/Complete_Lattices.thy
src/HOL/Finite_Set.thy
src/HOL/Groups_List.thy
src/HOL/Library/Disjoint_Sets.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Permutations.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Tue May 17 08:40:24 2016 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Tue May 17 17:05:35 2016 +0200
     1.3 @@ -1276,6 +1276,8 @@
     1.4  lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
     1.5    by blast
     1.6  
     1.7 +lemma inj_on_image: "inj_on f (\<Union>A) \<Longrightarrow> inj_on (op ` f) A"
     1.8 +  unfolding inj_on_def by blast
     1.9  
    1.10  subsubsection \<open>Distributive laws\<close>
    1.11  
     2.1 --- a/src/HOL/Finite_Set.thy	Tue May 17 08:40:24 2016 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue May 17 17:05:35 2016 +0200
     2.3 @@ -1501,6 +1501,41 @@
     2.4      by (auto dest: card_subset_eq)
     2.5  qed
     2.6  
     2.7 +lemma remove_induct [case_names empty infinite remove]:
     2.8 +  assumes empty: "P ({} :: 'a set)" and infinite: "\<not>finite B \<Longrightarrow> P B"
     2.9 +      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"
    2.10 +  shows "P B"
    2.11 +proof (cases "finite B")
    2.12 +  assume "\<not>finite B"
    2.13 +  thus ?thesis by (rule infinite)
    2.14 +next
    2.15 +  define A where "A = B"
    2.16 +  assume "finite B"
    2.17 +  hence "finite A" "A \<subseteq> B" by (simp_all add: A_def)
    2.18 +  thus "P A"
    2.19 +  proof (induction "card A" arbitrary: A)
    2.20 +    case 0
    2.21 +    hence "A = {}" by auto
    2.22 +    with empty show ?case by simp
    2.23 +  next
    2.24 +    case (Suc n A)
    2.25 +    from \<open>A \<subseteq> B\<close> and \<open>finite B\<close> have "finite A" by (rule finite_subset)
    2.26 +    moreover from Suc.hyps have "A \<noteq> {}" by auto
    2.27 +    moreover note \<open>A \<subseteq> B\<close>
    2.28 +    moreover have "P (A - {x})" if x: "x \<in> A" for x
    2.29 +      using x Suc.prems \<open>Suc n = card A\<close> by (intro Suc) auto
    2.30 +    ultimately show ?case by (rule remove)
    2.31 +  qed
    2.32 +qed
    2.33 +
    2.34 +lemma finite_remove_induct [consumes 1, case_names empty remove]:
    2.35 +  assumes finite: "finite B" and empty: "P ({} :: 'a set)" 
    2.36 +      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"
    2.37 +  defines "B' \<equiv> B"
    2.38 +  shows   "P B'"
    2.39 +  by (induction B' rule: remove_induct) (simp_all add: assms)
    2.40 +
    2.41 +
    2.42  text\<open>main cardinality theorem\<close>
    2.43  lemma card_partition [rule_format]:
    2.44    "finite C ==>
    2.45 @@ -1562,6 +1597,10 @@
    2.46      assumes "card A = 1" obtains x where "A = {x}"
    2.47    using assms by (auto simp: card_Suc_eq)
    2.48  
    2.49 +lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
    2.50 +  unfolding is_singleton_def
    2.51 +  by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
    2.52 +
    2.53  lemma card_le_Suc_iff: "finite A \<Longrightarrow>
    2.54    Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
    2.55  by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
     3.1 --- a/src/HOL/Groups_List.thy	Tue May 17 08:40:24 2016 +0200
     3.2 +++ b/src/HOL/Groups_List.thy	Tue May 17 17:05:35 2016 +0200
     3.3 @@ -255,6 +255,24 @@
     3.4    finally show ?thesis by(simp add:listsum_map_eq_setsum_count)
     3.5  qed
     3.6  
     3.7 +lemma listsum_nonneg: 
     3.8 +    "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> listsum xs \<ge> 0"
     3.9 +  by (induction xs) simp_all
    3.10 +
    3.11 +lemma listsum_map_filter:
    3.12 +  "listsum (map f (filter P xs)) = listsum (map (\<lambda>x. if P x then f x else 0) xs)"
    3.13 +  by (induction xs) simp_all
    3.14 +
    3.15 +lemma listsum_cong [fundef_cong]:
    3.16 +  assumes "xs = ys"
    3.17 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
    3.18 +  shows    "listsum (map f xs) = listsum (map g ys)"
    3.19 +proof -
    3.20 +  from assms(2) have "listsum (map f xs) = listsum (map g xs)"
    3.21 +    by (induction xs) simp_all
    3.22 +  with assms(1) show ?thesis by simp
    3.23 +qed
    3.24 +
    3.25  
    3.26  subsection \<open>Further facts about @{const List.n_lists}\<close>
    3.27  
    3.28 @@ -347,6 +365,16 @@
    3.29  
    3.30  end
    3.31  
    3.32 +lemma listprod_cong [fundef_cong]:
    3.33 +  assumes "xs = ys"
    3.34 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
    3.35 +  shows    "listprod (map f xs) = listprod (map g ys)"
    3.36 +proof -
    3.37 +  from assms(2) have "listprod (map f xs) = listprod (map g xs)"
    3.38 +    by (induction xs) simp_all
    3.39 +  with assms(1) show ?thesis by simp
    3.40 +qed
    3.41 +
    3.42  text \<open>Some syntactic sugar:\<close>
    3.43  
    3.44  syntax (ASCII)
     4.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Tue May 17 08:40:24 2016 +0200
     4.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Tue May 17 17:05:35 2016 +0200
     4.3 @@ -35,6 +35,13 @@
     4.4    "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
     4.5    unfolding disjoint_def by auto
     4.6  
     4.7 +lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint (op ` f ` A)"
     4.8 +  unfolding inj_on_def disjoint_def by blast
     4.9 +
    4.10 +lemma assumes "disjoint (A \<union> B)"
    4.11 +      shows   disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
    4.12 +  using assms by (simp_all add: disjoint_def)
    4.13 +  
    4.14  lemma disjoint_INT:
    4.15    assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
    4.16    shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
    4.17 @@ -81,7 +88,7 @@
    4.18  lemma disjoint_family_on_disjoint_image:
    4.19    "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
    4.20    unfolding disjoint_family_on_def disjoint_def by force
    4.21 -
    4.22 + 
    4.23  lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I"
    4.24    by (auto simp: disjoint_family_on_def)
    4.25  
    4.26 @@ -114,9 +121,60 @@
    4.27    qed
    4.28  qed
    4.29  
    4.30 +lemma distinct_list_bind: 
    4.31 +  assumes "distinct xs" "\<And>x. x \<in> set xs \<Longrightarrow> distinct (f x)" 
    4.32 +          "disjoint_family_on (set \<circ> f) (set xs)"
    4.33 +  shows   "distinct (List.bind xs f)"
    4.34 +  using assms
    4.35 +  by (induction xs)
    4.36 +     (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)
    4.37 +
    4.38 +lemma bij_betw_UNION_disjoint:
    4.39 +  assumes disj: "disjoint_family_on A' I"
    4.40 +  assumes bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
    4.41 +  shows   "bij_betw f (\<Union>i\<in>I. A i) (\<Union>i\<in>I. A' i)"
    4.42 +unfolding bij_betw_def
    4.43 +proof
    4.44 +  from bij show eq: "f ` UNION I A = UNION I A'"
    4.45 +    by (auto simp: bij_betw_def image_UN)
    4.46 +  show "inj_on f (UNION I A)"
    4.47 +  proof (rule inj_onI, clarify)
    4.48 +    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"
    4.49 +    from A bij[of i] bij[of j] have "f x \<in> A' i" "f y \<in> A' j"
    4.50 +      by (auto simp: bij_betw_def)
    4.51 +    with B have "A' i \<inter> A' j \<noteq> {}" by auto
    4.52 +    with disj A have "i = j" unfolding disjoint_family_on_def by blast
    4.53 +    with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
    4.54 +  qed
    4.55 +qed
    4.56 +
    4.57  lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
    4.58    using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
    4.59  
    4.60 +text \<open>
    4.61 +  The union of an infinite disjoint family of non-empty sets is infinite.
    4.62 +\<close>
    4.63 +lemma infinite_disjoint_family_imp_infinite_UNION:
    4.64 +  assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A"
    4.65 +  shows   "\<not>finite (UNION A f)"
    4.66 +proof -
    4.67 +  def g \<equiv> "\<lambda>x. SOME y. y \<in> f x"
    4.68 +  have g: "g x \<in> f x" if "x \<in> A" for x
    4.69 +    unfolding g_def by (rule someI_ex, insert assms(2) that) blast
    4.70 +  have inj_on_g: "inj_on g A"
    4.71 +  proof (rule inj_onI, rule ccontr)
    4.72 +    fix x y assume A: "x \<in> A" "y \<in> A" "g x = g y" "x \<noteq> y"
    4.73 +    with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto
    4.74 +    with A `x \<noteq> y` assms show False
    4.75 +      by (auto simp: disjoint_family_on_def inj_on_def)
    4.76 +  qed
    4.77 +  from g have "g ` A \<subseteq> UNION A f" by blast
    4.78 +  moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
    4.79 +    using finite_imageD by blast
    4.80 +  ultimately show ?thesis using finite_subset by blast
    4.81 +qed  
    4.82 +  
    4.83 +
    4.84  subsection \<open>Construct Disjoint Sequences\<close>
    4.85  
    4.86  definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
    4.87 @@ -149,5 +207,5 @@
    4.88  
    4.89  lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
    4.90    using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
    4.91 -
    4.92 +  
    4.93  end
     5.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 17 08:40:24 2016 +0200
     5.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 17 17:05:35 2016 +0200
     5.3 @@ -864,6 +864,8 @@
     5.4  
     5.5  declare [[coercion ennreal]]
     5.6  
     5.7 +lemma ennreal_cong: "x = y \<Longrightarrow> ennreal x = ennreal y" by simp
     5.8 +
     5.9  lemma ennreal_cases[cases type: ennreal]:
    5.10    fixes x :: ennreal
    5.11    obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
    5.12 @@ -949,6 +951,19 @@
    5.13  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)"
    5.14    by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)
    5.15  
    5.16 +lemma listsum_ennreal[simp]: 
    5.17 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0" 
    5.18 +  shows   "listsum (map (\<lambda>x. ennreal (f x)) xs) = ennreal (listsum (map f xs))"
    5.19 +using assms
    5.20 +proof (induction xs)
    5.21 +  case (Cons x xs)
    5.22 +  from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (listsum (map f xs))" 
    5.23 +    by simp
    5.24 +  also from Cons.prems have "\<dots> = ennreal (f x + listsum (map f xs))" 
    5.25 +    by (intro ennreal_plus [symmetric] listsum_nonneg) auto
    5.26 +  finally show ?case by simp
    5.27 +qed simp_all
    5.28 +
    5.29  lemma ennreal_of_nat_eq_real_of_nat: "of_nat i = ennreal (of_nat i)"
    5.30    by (induction i) simp_all
    5.31  
     6.1 --- a/src/HOL/Library/Extended_Real.thy	Tue May 17 08:40:24 2016 +0200
     6.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue May 17 17:05:35 2016 +0200
     6.3 @@ -228,6 +228,8 @@
     6.4  
     6.5  datatype ereal = ereal real | PInfty | MInfty
     6.6  
     6.7 +lemma ereal_cong: "x = y \<Longrightarrow> ereal x = ereal y" by simp
     6.8 +
     6.9  instantiation ereal :: uminus
    6.10  begin
    6.11  
    6.12 @@ -771,6 +773,9 @@
    6.13    then show ?thesis by simp
    6.14  qed
    6.15  
    6.16 +lemma listsum_ereal [simp]: "listsum (map (\<lambda>x. ereal (f x)) xs) = ereal (listsum (map f xs))"
    6.17 +  by (induction xs) simp_all
    6.18 +
    6.19  lemma setsum_Pinfty:
    6.20    fixes f :: "'a \<Rightarrow> ereal"
    6.21    shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
     7.1 --- a/src/HOL/Library/Indicator_Function.thy	Tue May 17 08:40:24 2016 +0200
     7.2 +++ b/src/HOL/Library/Indicator_Function.thy	Tue May 17 17:05:35 2016 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  section \<open>Indicator Function\<close>
     7.5  
     7.6  theory Indicator_Function
     7.7 -imports Complex_Main
     7.8 +imports Complex_Main Disjoint_Sets
     7.9  begin
    7.10  
    7.11  definition "indicator S x = (if x \<in> S then 1 else 0)"
    7.12 @@ -28,6 +28,10 @@
    7.13  lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A"
    7.14    by (auto simp: indicator_def)
    7.15  
    7.16 +lemma indicator_leI:
    7.17 +  "(x \<in> A \<Longrightarrow> y \<in> B) \<Longrightarrow> (indicator A x :: 'a :: linordered_nonzero_semiring) \<le> indicator B y"
    7.18 +  by (auto simp: indicator_def)
    7.19 +
    7.20  lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
    7.21    unfolding indicator_def by auto
    7.22  
    7.23 @@ -161,4 +165,14 @@
    7.24    finally show ?thesis .
    7.25  qed simp
    7.26  
    7.27 +text \<open>
    7.28 +  The indicator function of the union of a disjoint family of sets is the 
    7.29 +  sum over all the individual indicators.
    7.30 +\<close>
    7.31 +lemma indicator_UN_disjoint:
    7.32 +  assumes "finite A" "disjoint_family_on f A"
    7.33 +  shows   "indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)"
    7.34 +  using assms by (induction A rule: finite_induct)
    7.35 +                 (auto simp: disjoint_family_on_def indicator_def split: if_splits)
    7.36 +
    7.37  end
     8.1 --- a/src/HOL/Library/Multiset.thy	Tue May 17 08:40:24 2016 +0200
     8.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 17 17:05:35 2016 +0200
     8.3 @@ -417,6 +417,8 @@
     8.4  qed
     8.5  
     8.6  
     8.7 +
     8.8 +
     8.9  subsubsection \<open>Pointwise ordering induced by count\<close>
    8.10  
    8.11  definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
    8.12 @@ -1159,6 +1161,28 @@
    8.13  lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
    8.14    by (cases M) auto
    8.15  
    8.16 +lemma image_mset_If:
    8.17 +  "image_mset (\<lambda>x. if P x then f x else g x) A = 
    8.18 +     image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
    8.19 +  by (induction A) (auto simp: add_ac)
    8.20 +
    8.21 +lemma image_mset_Diff: 
    8.22 +  assumes "B \<subseteq># A"
    8.23 +  shows   "image_mset f (A - B) = image_mset f A - image_mset f B"
    8.24 +proof -
    8.25 +  have "image_mset f (A - B + B) = image_mset f (A - B) + image_mset f B"
    8.26 +    by simp
    8.27 +  also from assms have "A - B + B = A"
    8.28 +    by (simp add: subset_mset.diff_add) 
    8.29 +  finally show ?thesis by simp
    8.30 +qed
    8.31 +
    8.32 +lemma count_image_mset: 
    8.33 +  "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
    8.34 +  by (induction A)
    8.35 +     (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
    8.36 +
    8.37 +
    8.38  syntax (ASCII)
    8.39    "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
    8.40  syntax
    8.41 @@ -1379,6 +1403,40 @@
    8.42  lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
    8.43    by (induct A rule: finite_induct) simp_all
    8.44  
    8.45 +lemma mset_set_Union: 
    8.46 +  "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> mset_set (A \<union> B) = mset_set A + mset_set B"
    8.47 +  by (induction A rule: finite_induct) (auto simp: add_ac)
    8.48 +
    8.49 +lemma filter_mset_mset_set [simp]:
    8.50 +  "finite A \<Longrightarrow> filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
    8.51 +proof (induction A rule: finite_induct)
    8.52 +  case (insert x A)
    8.53 +  from insert.hyps have "filter_mset P (mset_set (insert x A)) = 
    8.54 +      filter_mset P (mset_set A) + mset_set (if P x then {x} else {})"
    8.55 +    by (simp add: add_ac)
    8.56 +  also have "filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
    8.57 +    by (rule insert.IH)
    8.58 +  also from insert.hyps 
    8.59 +    have "\<dots> + mset_set (if P x then {x} else {}) =
    8.60 +            mset_set ({x \<in> A. P x} \<union> (if P x then {x} else {}))" (is "_ = mset_set ?A")
    8.61 +     by (intro mset_set_Union [symmetric]) simp_all
    8.62 +  also from insert.hyps have "?A = {y\<in>insert x A. P y}" by auto
    8.63 +  finally show ?case .
    8.64 +qed simp_all
    8.65 +
    8.66 +lemma mset_set_Diff:
    8.67 +  assumes "finite A" "B \<subseteq> A"
    8.68 +  shows  "mset_set (A - B) = mset_set A - mset_set B"
    8.69 +proof -
    8.70 +  from assms have "mset_set ((A - B) \<union> B) = mset_set (A - B) + mset_set B"
    8.71 +    by (intro mset_set_Union) (auto dest: finite_subset)
    8.72 +  also from assms have "A - B \<union> B = A" by blast
    8.73 +  finally show ?thesis by simp
    8.74 +qed
    8.75 +
    8.76 +lemma mset_set_set: "distinct xs \<Longrightarrow> mset_set (set xs) = mset xs"
    8.77 +  by (induction xs) (simp_all add: add_ac)
    8.78 +
    8.79  context linorder
    8.80  begin
    8.81  
    8.82 @@ -1418,6 +1476,9 @@
    8.83    "finite A \<Longrightarrow> set_mset (mset_set A) = A"
    8.84  by (induct A rule: finite_induct) simp_all
    8.85  
    8.86 +lemma mset_set_empty_iff: "mset_set A = {#} \<longleftrightarrow> A = {} \<or> infinite A"
    8.87 +  using finite_set_mset_mset_set by fastforce
    8.88 +
    8.89  lemma infinite_set_mset_mset_set:
    8.90    "\<not> finite A \<Longrightarrow> set_mset (mset_set A) = {}"
    8.91  by simp
    8.92 @@ -1430,6 +1491,22 @@
    8.93    "sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
    8.94  by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps)
    8.95  
    8.96 +lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
    8.97 +  by (induction n) (simp_all add: atLeastLessThanSuc add_ac)
    8.98 +
    8.99 +lemma image_mset_map_of: 
   8.100 +  "distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
   8.101 +proof (induction xs)
   8.102 +  case (Cons x xs)
   8.103 +  have "{#the (map_of (x # xs) i). i \<in># mset (map fst (x # xs))#} = 
   8.104 +          {#the (if i = fst x then Some (snd x) else map_of xs i). 
   8.105 +             i \<in># mset (map fst xs)#} + {#snd x#}" (is "_ = ?A + _") by simp
   8.106 +  also from Cons.prems have "?A = {#the (map_of xs i). i :# mset (map fst xs)#}"
   8.107 +    by (cases x, intro image_mset_cong) (auto simp: in_multiset_in_set)
   8.108 +  also from Cons.prems have "\<dots> = mset (map snd xs)" by (intro Cons.IH) simp_all
   8.109 +  finally show ?case by simp
   8.110 +qed simp_all  
   8.111 +
   8.112  
   8.113  subsection \<open>Replicate operation\<close>
   8.114  
   8.115 @@ -1546,6 +1623,9 @@
   8.116        (simp_all add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb not_in_iff)
   8.117  qed
   8.118  
   8.119 +lemma size_mset_set [simp]: "size (mset_set A) = card A"
   8.120 +  by (simp only: size_eq_msetsum card_eq_setsum setsum_unfold_msetsum)
   8.121 +
   8.122  syntax (ASCII)
   8.123    "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
   8.124  syntax
     9.1 --- a/src/HOL/Library/Permutations.thy	Tue May 17 08:40:24 2016 +0200
     9.2 +++ b/src/HOL/Library/Permutations.thy	Tue May 17 17:05:35 2016 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  section \<open>Permutations, both general and specifically on finite sets.\<close>
     9.5  
     9.6  theory Permutations
     9.7 -imports Binomial
     9.8 +imports Binomial Multiset Disjoint_Sets
     9.9  begin
    9.10  
    9.11  subsection \<open>Transpositions\<close>
    9.12 @@ -30,6 +30,10 @@
    9.13  
    9.14  lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
    9.15    unfolding permutes_def by metis
    9.16 +  
    9.17 +lemma permutes_not_in:
    9.18 +  assumes "f permutes S" "x \<notin> S" shows "f x = x"
    9.19 +  using assms by (auto simp: permutes_def)
    9.20  
    9.21  lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S"
    9.22    unfolding permutes_def
    9.23 @@ -41,6 +45,9 @@
    9.24  lemma permutes_inj: "p permutes S \<Longrightarrow> inj p"
    9.25    unfolding permutes_def inj_on_def by blast
    9.26  
    9.27 +lemma permutes_inj_on: "f permutes S \<Longrightarrow> inj_on f A"
    9.28 +  unfolding permutes_def inj_on_def by auto
    9.29 +
    9.30  lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
    9.31    unfolding permutes_def surj_def by metis
    9.32  
    9.33 @@ -118,6 +125,25 @@
    9.34    unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
    9.35    by blast
    9.36  
    9.37 +lemma permutes_invI: 
    9.38 +  assumes perm: "p permutes S"
    9.39 +      and inv:  "\<And>x. x \<in> S \<Longrightarrow> p' (p x) = x" 
    9.40 +      and outside: "\<And>x. x \<notin> S \<Longrightarrow> p' x = x"
    9.41 +  shows   "inv p = p'"
    9.42 +proof
    9.43 +  fix x show "inv p x = p' x"
    9.44 +  proof (cases "x \<in> S")
    9.45 +    assume [simp]: "x \<in> S"
    9.46 +    from assms have "p' x = p' (p (inv p x))" by (simp add: permutes_inverses)
    9.47 +    also from permutes_inv[OF perm] 
    9.48 +      have "\<dots> = inv p x" by (subst inv) (simp_all add: permutes_in_image)
    9.49 +    finally show "inv p x = p' x" ..
    9.50 +  qed (insert permutes_inv[OF perm], simp_all add: outside permutes_not_in)
    9.51 +qed
    9.52 +
    9.53 +lemma permutes_vimage: "f permutes A \<Longrightarrow> f -` A = A"
    9.54 +  by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv])  
    9.55 +
    9.56  
    9.57  subsection \<open>The number of permutations on a finite set\<close>
    9.58  
    9.59 @@ -813,9 +839,164 @@
    9.60  lemma sign_idempotent: "sign p * sign p = 1"
    9.61    by (simp add: sign_def)
    9.62  
    9.63 + 
    9.64 +subsection \<open>Permuting a list\<close>
    9.65 +
    9.66 +text \<open>This function permutes a list by applying a permutation to the indices.\<close>
    9.67 +
    9.68 +definition permute_list :: "(nat \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    9.69 +  "permute_list f xs = map (\<lambda>i. xs ! (f i)) [0..<length xs]"
    9.70 +
    9.71 +lemma permute_list_map: 
    9.72 +  assumes "f permutes {..<length xs}"
    9.73 +  shows   "permute_list f (map g xs) = map g (permute_list f xs)"
    9.74 +  using permutes_in_image[OF assms] by (auto simp: permute_list_def)
    9.75 +
    9.76 +lemma permute_list_nth:
    9.77 +  assumes "f permutes {..<length xs}" "i < length xs"
    9.78 +  shows   "permute_list f xs ! i = xs ! f i"
    9.79 +  using permutes_in_image[OF assms(1)] assms(2) 
    9.80 +  by (simp add: permute_list_def)
    9.81 +
    9.82 +lemma permute_list_Nil [simp]: "permute_list f [] = []"
    9.83 +  by (simp add: permute_list_def)
    9.84 +
    9.85 +lemma length_permute_list [simp]: "length (permute_list f xs) = length xs"
    9.86 +  by (simp add: permute_list_def)
    9.87 +
    9.88 +lemma permute_list_compose: 
    9.89 +  assumes "g permutes {..<length xs}"
    9.90 +  shows   "permute_list (f \<circ> g) xs = permute_list g (permute_list f xs)"
    9.91 +  using assms[THEN permutes_in_image] by (auto simp add: permute_list_def)
    9.92 +
    9.93 +lemma permute_list_ident [simp]: "permute_list (\<lambda>x. x) xs = xs"
    9.94 +  by (simp add: permute_list_def map_nth)
    9.95 +
    9.96 +lemma permute_list_id [simp]: "permute_list id xs = xs"
    9.97 +  by (simp add: id_def)
    9.98 +
    9.99 +lemma mset_permute_list [simp]:
   9.100 +  assumes "f permutes {..<length (xs :: 'a list)}"
   9.101 +  shows   "mset (permute_list f xs) = mset xs"
   9.102 +proof (rule multiset_eqI)
   9.103 +  fix y :: 'a
   9.104 +  from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x
   9.105 +    using permutes_in_image[OF assms] by auto
   9.106 +  have "count (mset (permute_list f xs)) y = 
   9.107 +          card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"
   9.108 +    by (simp add: permute_list_def mset_map count_image_mset atLeast0LessThan)
   9.109 +  also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}"
   9.110 +    by auto
   9.111 +  also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"
   9.112 +    by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj)
   9.113 +  also have "\<dots> = count (mset xs) y" by (simp add: count_mset length_filter_conv_card)
   9.114 +  finally show "count (mset (permute_list f xs)) y = count (mset xs) y" by simp
   9.115 +qed
   9.116 +
   9.117 +lemma set_permute_list [simp]:
   9.118 +  assumes "f permutes {..<length xs}"
   9.119 +  shows   "set (permute_list f xs) = set xs"
   9.120 +  by (rule mset_eq_setD[OF mset_permute_list]) fact
   9.121 +
   9.122 +lemma distinct_permute_list [simp]:
   9.123 +  assumes "f permutes {..<length xs}"
   9.124 +  shows   "distinct (permute_list f xs) = distinct xs"
   9.125 +  by (simp add: distinct_count_atmost_1 assms)
   9.126 +
   9.127 +lemma permute_list_zip: 
   9.128 +  assumes "f permutes A" "A = {..<length xs}"
   9.129 +  assumes [simp]: "length xs = length ys"
   9.130 +  shows   "permute_list f (zip xs ys) = zip (permute_list f xs) (permute_list f ys)"
   9.131 +proof -
   9.132 +  from permutes_in_image[OF assms(1)] assms(2)
   9.133 +    have [simp]: "f i < length ys \<longleftrightarrow> i < length ys" for i by simp
   9.134 +  have "permute_list f (zip xs ys) = map (\<lambda>i. zip xs ys ! f i) [0..<length ys]"
   9.135 +    by (simp_all add: permute_list_def zip_map_map)
   9.136 +  also have "\<dots> = map (\<lambda>(x, y). (xs ! f x, ys ! f y)) (zip [0..<length ys] [0..<length ys])"
   9.137 +    by (intro nth_equalityI) simp_all
   9.138 +  also have "\<dots> = zip (permute_list f xs) (permute_list f ys)"
   9.139 +    by (simp_all add: permute_list_def zip_map_map)
   9.140 +  finally show ?thesis .
   9.141 +qed
   9.142 +
   9.143 +lemma map_of_permute: 
   9.144 +  assumes "\<sigma> permutes fst ` set xs"
   9.145 +  shows   "map_of xs \<circ> \<sigma> = map_of (map (\<lambda>(x,y). (inv \<sigma> x, y)) xs)" (is "_ = map_of (map ?f _)")
   9.146 +proof
   9.147 +  fix x
   9.148 +  from assms have "inj \<sigma>" "surj \<sigma>" by (simp_all add: permutes_inj permutes_surj)
   9.149 +  thus "(map_of xs \<circ> \<sigma>) x = map_of (map ?f xs) x"
   9.150 +    by (induction xs) (auto simp: inv_f_f surj_f_inv_f)
   9.151 +qed
   9.152 +
   9.153  
   9.154  subsection \<open>More lemmas about permutations\<close>
   9.155  
   9.156 +text \<open>
   9.157 +  If two lists correspond to the same multiset, there exists a permutation 
   9.158 +  on the list indices that maps one to the other.
   9.159 +\<close>
   9.160 +lemma mset_eq_permutation:
   9.161 +  assumes mset_eq: "mset (xs::'a list) = mset ys"
   9.162 +  defines [simp]: "n \<equiv> length xs"
   9.163 +  obtains f where "f permutes {..<length ys}" "permute_list f ys = xs"
   9.164 +proof -
   9.165 +  from mset_eq have [simp]: "length xs = length ys"
   9.166 +    by (rule mset_eq_length)
   9.167 +  def indices_of \<equiv> "\<lambda>(x::'a) xs. {i. i < length xs \<and> x = xs ! i}"
   9.168 +  have indices_of_subset: "indices_of x xs \<subseteq> {..<length xs}" for x xs
   9.169 +    unfolding indices_of_def by blast
   9.170 +  have [simp]: "finite (indices_of x xs)" for x xs
   9.171 +    by (rule finite_subset[OF indices_of_subset]) simp_all
   9.172 +
   9.173 +  have "\<forall>x\<in>set xs. \<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)"
   9.174 +  proof
   9.175 +    fix x
   9.176 +    from mset_eq have "count (mset xs) x = count (mset ys) x" by simp
   9.177 +    hence "card (indices_of x xs) = card (indices_of x ys)"
   9.178 +      by (simp add: count_mset length_filter_conv_card indices_of_def)
   9.179 +    thus "\<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)"
   9.180 +      by (intro finite_same_card_bij) simp_all
   9.181 +  qed
   9.182 +  hence "\<exists>f. \<forall>x\<in>set xs. bij_betw (f x) (indices_of x xs) (indices_of x ys)"
   9.183 +    by (rule bchoice)
   9.184 +  then guess f .. note f = this
   9.185 +  def g \<equiv> "\<lambda>i. if i < n then f (xs ! i) i else i"
   9.186 +
   9.187 +  have bij_f: "bij_betw (\<lambda>i. f (xs ! i) i) (indices_of x xs) (indices_of x ys)"
   9.188 +    if x: "x \<in> set xs" for x
   9.189 +  proof (subst bij_betw_cong)
   9.190 +    from f x show "bij_betw (f x) (indices_of x xs) (indices_of x ys)" by blast
   9.191 +    fix i assume "i \<in> indices_of x xs"
   9.192 +    thus "f (xs ! i) i = f x i" by (simp add: indices_of_def)
   9.193 +  qed
   9.194 +
   9.195 +  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)"
   9.196 +    by (intro bij_betw_UNION_disjoint) (auto simp add: disjoint_family_on_def indices_of_def)
   9.197 +  also have "(\<Union>x\<in>set xs. indices_of x xs) = {..<n}" by (auto simp: indices_of_def)
   9.198 +  also from mset_eq have "set xs = set ys" by (rule mset_eq_setD) 
   9.199 +  also have "(\<Union>x\<in>set ys. indices_of x ys) = {..<n}"
   9.200 +    by (auto simp: indices_of_def set_conv_nth)
   9.201 +  also have "bij_betw (\<lambda>i. f (xs ! i) i) {..<n} {..<n} \<longleftrightarrow> bij_betw g {..<n} {..<n}"
   9.202 +    by (intro bij_betw_cong) (simp_all add: g_def)
   9.203 +  finally have "g permutes {..<length ys}"
   9.204 +    by (intro bij_imp_permutes refl) (simp_all add: g_def)
   9.205 +
   9.206 +  moreover have "permute_list g ys = xs" 
   9.207 +  proof (rule sym, intro nth_equalityI allI impI)
   9.208 +    fix i assume i: "i < length xs"
   9.209 +    from i have "permute_list g ys ! i = ys ! f (xs ! i) i"
   9.210 +      by (simp add: permute_list_def g_def)
   9.211 +    also from i have "i \<in> indices_of (xs ! i) xs" by (simp add: indices_of_def)
   9.212 +    with bij_f[of "xs ! i"] i have "f (xs ! i) i \<in> indices_of (xs ! i) ys"
   9.213 +      by (auto simp: bij_betw_def)
   9.214 +    hence "ys ! f (xs ! i) i = xs ! i" by (simp add: indices_of_def)
   9.215 +    finally show "xs ! i = permute_list g ys ! i" ..
   9.216 +  qed simp_all
   9.217 +
   9.218 +  ultimately show ?thesis by (rule that)
   9.219 +qed
   9.220 +
   9.221  lemma permutes_natset_le:
   9.222    fixes S :: "'a::wellorder set"
   9.223    assumes p: "p permutes S"
   9.224 @@ -1047,5 +1228,154 @@
   9.225    qed
   9.226  qed
   9.227  
   9.228 +
   9.229 +subsection \<open>Constructing permutations from association lists\<close>
   9.230 +
   9.231 +definition list_permutes where
   9.232 +  "list_permutes xs A \<longleftrightarrow> set (map fst xs) \<subseteq> A \<and> set (map snd xs) = set (map fst xs) \<and> 
   9.233 +     distinct (map fst xs) \<and> distinct (map snd xs)"
   9.234 +
   9.235 +lemma list_permutesI [simp]:
   9.236 +  assumes "set (map fst xs) \<subseteq> A" "set (map snd xs) = set (map fst xs)" "distinct (map fst xs)"
   9.237 +  shows   "list_permutes xs A"
   9.238 +proof -
   9.239 +  from assms(2,3) have "distinct (map snd xs)"
   9.240 +    by (intro card_distinct) (simp_all add: distinct_card del: set_map)
   9.241 +  with assms show ?thesis by (simp add: list_permutes_def)
   9.242 +qed
   9.243 +
   9.244 +definition permutation_of_list where
   9.245 +  "permutation_of_list xs x = (case map_of xs x of None \<Rightarrow> x | Some y \<Rightarrow> y)"
   9.246 +
   9.247 +lemma permutation_of_list_Cons:
   9.248 +  "permutation_of_list ((x,y) # xs) x' = (if x = x' then y else permutation_of_list xs x')"
   9.249 +  by (simp add: permutation_of_list_def)
   9.250 +
   9.251 +fun inverse_permutation_of_list where
   9.252 +  "inverse_permutation_of_list [] x = x"
   9.253 +| "inverse_permutation_of_list ((y,x')#xs) x =
   9.254 +     (if x = x' then y else inverse_permutation_of_list xs x)"
   9.255 +
   9.256 +declare inverse_permutation_of_list.simps [simp del]
   9.257 +
   9.258 +lemma inj_on_map_of:
   9.259 +  assumes "distinct (map snd xs)"
   9.260 +  shows   "inj_on (map_of xs) (set (map fst xs))"
   9.261 +proof (rule inj_onI)
   9.262 +  fix x y assume xy: "x \<in> set (map fst xs)" "y \<in> set (map fst xs)"
   9.263 +  assume eq: "map_of xs x = map_of xs y"
   9.264 +  from xy obtain x' y' 
   9.265 +    where x'y': "map_of xs x = Some x'" "map_of xs y = Some y'" 
   9.266 +    by (cases "map_of xs x"; cases "map_of xs y")
   9.267 +       (simp_all add: map_of_eq_None_iff)
   9.268 +  moreover from this x'y' have "(x,x') \<in> set xs" "(y,y') \<in> set xs"
   9.269 +    by (force dest: map_of_SomeD)+
   9.270 +  moreover from this eq x'y' have "x' = y'" by simp
   9.271 +  ultimately show "x = y" using assms
   9.272 +    by (force simp: distinct_map dest: inj_onD[of _ _ "(x,x')" "(y,y')"])
   9.273 +qed
   9.274 +
   9.275 +lemma inj_on_the: "None \<notin> A \<Longrightarrow> inj_on the A"
   9.276 +  by (auto simp: inj_on_def option.the_def split: option.splits)
   9.277 +
   9.278 +lemma inj_on_map_of':
   9.279 +  assumes "distinct (map snd xs)"
   9.280 +  shows   "inj_on (the \<circ> map_of xs) (set (map fst xs))"
   9.281 +  by (intro comp_inj_on inj_on_map_of assms inj_on_the)
   9.282 +     (force simp: eq_commute[of None] map_of_eq_None_iff)
   9.283 +
   9.284 +lemma image_map_of:
   9.285 +  assumes "distinct (map fst xs)"
   9.286 +  shows   "map_of xs ` set (map fst xs) = Some ` set (map snd xs)"
   9.287 +  using assms by (auto simp: rev_image_eqI)
   9.288 +
   9.289 +lemma the_Some_image [simp]: "the ` Some ` A = A"
   9.290 +  by (subst image_image) simp
   9.291 +
   9.292 +lemma image_map_of':
   9.293 +  assumes "distinct (map fst xs)"
   9.294 +  shows   "(the \<circ> map_of xs) ` set (map fst xs) = set (map snd xs)"
   9.295 +  by (simp only: image_comp [symmetric] image_map_of assms the_Some_image)
   9.296 +
   9.297 +lemma permutation_of_list_permutes [simp]:
   9.298 +  assumes "list_permutes xs A"
   9.299 +  shows   "permutation_of_list xs permutes A" (is "?f permutes _")
   9.300 +proof (rule permutes_subset[OF bij_imp_permutes])
   9.301 +  from assms show "set (map fst xs) \<subseteq> A"
   9.302 +    by (simp add: list_permutes_def)
   9.303 +  from assms have "inj_on (the \<circ> map_of xs) (set (map fst xs))" (is ?P)
   9.304 +    by (intro inj_on_map_of') (simp_all add: list_permutes_def)
   9.305 +  also have "?P \<longleftrightarrow> inj_on ?f (set (map fst xs))"
   9.306 +    by (intro inj_on_cong)
   9.307 +       (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)
   9.308 +  finally have "bij_betw ?f (set (map fst xs)) (?f ` set (map fst xs))"
   9.309 +    by (rule inj_on_imp_bij_betw)
   9.310 +  also from assms have "?f ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)"
   9.311 +    by (intro image_cong refl)
   9.312 +       (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)
   9.313 +  also from assms have "\<dots> = set (map fst xs)" 
   9.314 +    by (subst image_map_of') (simp_all add: list_permutes_def)
   9.315 +  finally show "bij_betw ?f (set (map fst xs)) (set (map fst xs))" .
   9.316 +qed (force simp: permutation_of_list_def dest!: map_of_SomeD split: option.splits)+
   9.317 +
   9.318 +lemma eval_permutation_of_list [simp]:
   9.319 +  "permutation_of_list [] x = x"
   9.320 +  "x = x' \<Longrightarrow> permutation_of_list ((x',y)#xs) x = y"
   9.321 +  "x \<noteq> x' \<Longrightarrow> permutation_of_list ((x',y')#xs) x = permutation_of_list xs x"
   9.322 +  by (simp_all add: permutation_of_list_def)
   9.323 +
   9.324 +lemma eval_inverse_permutation_of_list [simp]:
   9.325 +  "inverse_permutation_of_list [] x = x"
   9.326 +  "x = x' \<Longrightarrow> inverse_permutation_of_list ((y,x')#xs) x = y"
   9.327 +  "x \<noteq> x' \<Longrightarrow> inverse_permutation_of_list ((y',x')#xs) x = inverse_permutation_of_list xs x"
   9.328 +  by (simp_all add: inverse_permutation_of_list.simps)
   9.329 +
   9.330 +lemma permutation_of_list_id:
   9.331 +  assumes "x \<notin> set (map fst xs)"
   9.332 +  shows   "permutation_of_list xs x = x"
   9.333 +  using assms by (induction xs) (auto simp: permutation_of_list_Cons)
   9.334 +
   9.335 +lemma permutation_of_list_unique':
   9.336 +  assumes "distinct (map fst xs)" "(x, y) \<in> set xs"
   9.337 +  shows   "permutation_of_list xs x = y"
   9.338 +  using assms by (induction xs) (force simp: permutation_of_list_Cons)+
   9.339 +
   9.340 +lemma permutation_of_list_unique:
   9.341 +  assumes "list_permutes xs A" "(x,y) \<in> set xs"
   9.342 +  shows   "permutation_of_list xs x = y"
   9.343 +  using assms by (intro permutation_of_list_unique') (simp_all add: list_permutes_def)
   9.344 +
   9.345 +lemma inverse_permutation_of_list_id:
   9.346 +  assumes "x \<notin> set (map snd xs)"
   9.347 +  shows   "inverse_permutation_of_list xs x = x"
   9.348 +  using assms by (induction xs) auto
   9.349 +
   9.350 +lemma inverse_permutation_of_list_unique':
   9.351 +  assumes "distinct (map snd xs)" "(x, y) \<in> set xs"
   9.352 +  shows   "inverse_permutation_of_list xs y = x"
   9.353 +  using assms by (induction xs) (force simp: inverse_permutation_of_list.simps)+
   9.354 +
   9.355 +lemma inverse_permutation_of_list_unique:
   9.356 +  assumes "list_permutes xs A" "(x,y) \<in> set xs"
   9.357 +  shows   "inverse_permutation_of_list xs y = x"
   9.358 +  using assms by (intro inverse_permutation_of_list_unique') (simp_all add: list_permutes_def)
   9.359 +
   9.360 +lemma inverse_permutation_of_list_correct:
   9.361 +  assumes "list_permutes xs (A :: 'a set)"
   9.362 +  shows   "inverse_permutation_of_list xs = inv (permutation_of_list xs)"
   9.363 +proof (rule ext, rule sym, subst permutes_inv_eq)
   9.364 +  from assms show "permutation_of_list xs permutes A" by simp
   9.365 +next
   9.366 +  fix x
   9.367 +  show "permutation_of_list xs (inverse_permutation_of_list xs x) = x"
   9.368 +  proof (cases "x \<in> set (map snd xs)")
   9.369 +    case True
   9.370 +    then obtain y where "(y, x) \<in> set xs" by force
   9.371 +    with assms show ?thesis
   9.372 +      by (simp add: inverse_permutation_of_list_unique permutation_of_list_unique)
   9.373 +  qed (insert assms, auto simp: list_permutes_def
   9.374 +         inverse_permutation_of_list_id permutation_of_list_id)
   9.375 +qed
   9.376 +
   9.377  end
   9.378  
    10.1 --- a/src/HOL/List.thy	Tue May 17 08:40:24 2016 +0200
    10.2 +++ b/src/HOL/List.thy	Tue May 17 17:05:35 2016 +0200
    10.3 @@ -3298,9 +3298,19 @@
    10.4    "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
    10.5  by(auto simp: distinct_conv_nth)
    10.6  
    10.7 +lemma distinct_Ex1: 
    10.8 +  "distinct xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> (\<exists>!i. i < length xs \<and> xs ! i = x)"
    10.9 +  by (auto simp: in_set_conv_nth nth_eq_iff_index_eq)
   10.10 +
   10.11  lemma inj_on_nth: "distinct xs \<Longrightarrow> \<forall>i \<in> I. i < length xs \<Longrightarrow> inj_on (nth xs) I"
   10.12  by (rule inj_onI) (simp add: nth_eq_iff_index_eq)
   10.13  
   10.14 +lemma bij_betw_nth:
   10.15 +  assumes "distinct xs" "A = {..<length xs}" "B = set xs" 
   10.16 +  shows   "bij_betw (op ! xs) A B"
   10.17 +  using assms unfolding bij_betw_def
   10.18 +  by (auto intro!: inj_on_nth simp: set_conv_nth)
   10.19 +
   10.20  lemma set_update_distinct: "\<lbrakk> distinct xs;  n < length xs \<rbrakk> \<Longrightarrow>
   10.21    set(xs[n := x]) = insert x (set xs - {xs!n})"
   10.22  by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq)
   10.23 @@ -6175,6 +6185,18 @@
   10.24    "List.bind (x # xs) f = f x @ List.bind xs f"
   10.25    by (simp_all add: bind_def)
   10.26  
   10.27 +lemma list_bind_cong [fundef_cong]:
   10.28 +  assumes "xs = ys" "(\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)"
   10.29 +  shows   "List.bind xs f = List.bind ys g"
   10.30 +proof -
   10.31 +  from assms(2) have "List.bind xs f = List.bind xs g"
   10.32 +    by (induction xs) simp_all
   10.33 +  with assms(1) show ?thesis by simp
   10.34 +qed
   10.35 +
   10.36 +lemma set_list_bind: "set (List.bind xs f) = (\<Union>x\<in>set xs. set (f x))"
   10.37 +  by (induction xs) simp_all  
   10.38 +
   10.39  
   10.40  subsection \<open>Transfer\<close>
   10.41  
    11.1 --- a/src/HOL/Nat.thy	Tue May 17 08:40:24 2016 +0200
    11.2 +++ b/src/HOL/Nat.thy	Tue May 17 17:05:35 2016 +0200
    11.3 @@ -1758,6 +1758,10 @@
    11.4    shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
    11.5    by (auto dest!: le_Suc_ex)
    11.6  
    11.7 +lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> (a::nat)"
    11.8 +  by (force dest: le_Suc_ex)
    11.9 +  
   11.10 +
   11.11  text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
   11.12  
   11.13  lemma diff_le_mono:
    12.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 17 08:40:24 2016 +0200
    12.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 17 17:05:35 2016 +0200
    12.3 @@ -167,6 +167,12 @@
    12.4  
    12.5  lemma pmf_nonneg[simp]: "0 \<le> pmf p x"
    12.6    by transfer simp
    12.7 +  
    12.8 +lemma pmf_not_neg [simp]: "\<not>pmf p x < 0"
    12.9 +  by (simp add: not_less pmf_nonneg)
   12.10 +
   12.11 +lemma pmf_pos [simp]: "pmf p x \<noteq> 0 \<Longrightarrow> pmf p x > 0"
   12.12 +  using pmf_nonneg[of p x] by linarith
   12.13  
   12.14  lemma pmf_le_1: "pmf p x \<le> 1"
   12.15    by (simp add: pmf.rep_eq)
   12.16 @@ -183,6 +189,13 @@
   12.17  lemma set_pmf_eq: "set_pmf M = {x. pmf M x \<noteq> 0}"
   12.18    by (auto simp: set_pmf_iff)
   12.19  
   12.20 +lemma set_pmf_eq': "set_pmf p = {x. pmf p x > 0}"
   12.21 +proof safe
   12.22 +  fix x assume "x \<in> set_pmf p"
   12.23 +  hence "pmf p x \<noteq> 0" by (auto simp: set_pmf_eq)
   12.24 +  with pmf_nonneg[of p x] show "pmf p x > 0" by simp
   12.25 +qed (auto simp: set_pmf_eq)
   12.26 +
   12.27  lemma emeasure_pmf_single:
   12.28    fixes M :: "'a pmf"
   12.29    shows "emeasure M {x} = pmf M x"
   12.30 @@ -198,6 +211,17 @@
   12.31    using emeasure_measure_pmf_finite[of S M]
   12.32    by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg setsum_nonneg pmf_nonneg)
   12.33  
   12.34 +lemma setsum_pmf_eq_1:
   12.35 +  assumes "finite A" "set_pmf p \<subseteq> A"
   12.36 +  shows   "(\<Sum>x\<in>A. pmf p x) = 1"
   12.37 +proof -
   12.38 +  have "(\<Sum>x\<in>A. pmf p x) = measure_pmf.prob p A"
   12.39 +    by (simp add: measure_measure_pmf_finite assms)
   12.40 +  also from assms have "\<dots> = 1"
   12.41 +    by (subst measure_pmf.prob_eq_1) (auto simp: AE_measure_pmf_iff)
   12.42 +  finally show ?thesis .
   12.43 +qed
   12.44 +
   12.45  lemma nn_integral_measure_pmf_support:
   12.46    fixes f :: "'a \<Rightarrow> ennreal"
   12.47    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"
   12.48 @@ -339,6 +363,8 @@
   12.49      done
   12.50  qed
   12.51  
   12.52 +adhoc_overloading Monad_Syntax.bind bind_pmf
   12.53 +
   12.54  lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
   12.55    unfolding pmf.rep_eq bind_pmf.rep_eq
   12.56    by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg
   12.57 @@ -363,7 +389,7 @@
   12.58    finally show ?thesis .
   12.59  qed
   12.60  
   12.61 -lemma bind_pmf_cong:
   12.62 +lemma bind_pmf_cong [fundef_cong]:
   12.63    assumes "p = q"
   12.64    shows "(\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g"
   12.65    unfolding \<open>p = q\<close>[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq
   12.66 @@ -518,6 +544,15 @@
   12.67  lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x"
   12.68    unfolding return_pmf.rep_eq by (intro emeasure_return) auto
   12.69  
   12.70 +lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x"
   12.71 +proof -
   12.72 +  have "ennreal (measure_pmf.prob (return_pmf x) A) = 
   12.73 +          emeasure (measure_pmf (return_pmf x)) A"
   12.74 +    by (simp add: measure_pmf.emeasure_eq_measure)
   12.75 +  also have "\<dots> = ennreal (indicator A x)" by (simp add: ennreal_indicator)
   12.76 +  finally show ?thesis by simp
   12.77 +qed
   12.78 +
   12.79  lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y"
   12.80    by (metis insertI1 set_return_pmf singletonD)
   12.81  
   12.82 @@ -732,6 +767,27 @@
   12.83  lemma pmf_eq_iff: "M = N \<longleftrightarrow> (\<forall>i. pmf M i = pmf N i)"
   12.84    by (auto intro: pmf_eqI)
   12.85  
   12.86 +lemma pmf_neq_exists_less:
   12.87 +  assumes "M \<noteq> N"
   12.88 +  shows   "\<exists>x. pmf M x < pmf N x"
   12.89 +proof (rule ccontr)
   12.90 +  assume "\<not>(\<exists>x. pmf M x < pmf N x)"
   12.91 +  hence ge: "pmf M x \<ge> pmf N x" for x by (auto simp: not_less)
   12.92 +  from assms obtain x where "pmf M x \<noteq> pmf N x" by (auto simp: pmf_eq_iff)
   12.93 +  with ge[of x] have gt: "pmf M x > pmf N x" by simp
   12.94 +  have "1 = measure (measure_pmf M) UNIV" by simp
   12.95 +  also have "\<dots> = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})"
   12.96 +    by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
   12.97 +  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}" 
   12.98 +    by (simp add: measure_pmf_single)
   12.99 +  also have "measure (measure_pmf N) (UNIV - {x}) \<le> measure (measure_pmf M) (UNIV - {x})"
  12.100 +    by (subst (1 2) integral_pmf [symmetric]) 
  12.101 +       (intro integral_mono integrable_pmf, simp_all add: ge)
  12.102 +  also have "measure (measure_pmf M) {x} + \<dots> = 1"
  12.103 +    by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
  12.104 +  finally show False by simp_all
  12.105 +qed
  12.106 +
  12.107  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))"
  12.108    unfolding pmf_eq_iff pmf_bind
  12.109  proof
  12.110 @@ -904,6 +960,9 @@
  12.111  
  12.112  end
  12.113  
  12.114 +lemma measure_pmf_posI: "x \<in> set_pmf p \<Longrightarrow> x \<in> A \<Longrightarrow> measure_pmf.prob p A > 0"
  12.115 +  using measure_measure_pmf_not_zero[of p A] by (subst zero_less_measure_iff) blast
  12.116 +
  12.117  lemma cond_map_pmf:
  12.118    assumes "set_pmf p \<inter> f -` s \<noteq> {}"
  12.119    shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
  12.120 @@ -1568,6 +1627,31 @@
  12.121  
  12.122  end
  12.123  
  12.124 +lemma map_pmf_of_set:
  12.125 +  assumes "finite A" "A \<noteq> {}"
  12.126 +  shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))" 
  12.127 +    (is "?lhs = ?rhs")
  12.128 +proof (intro pmf_eqI)
  12.129 +  fix x
  12.130 +  from assms have "ennreal (pmf ?lhs x) = ennreal (pmf ?rhs x)"
  12.131 +    by (subst ennreal_pmf_map)
  12.132 +       (simp_all add: emeasure_pmf_of_set mset_set_empty_iff count_image_mset Int_commute)
  12.133 +  thus "pmf ?lhs x = pmf ?rhs x" by simp
  12.134 +qed
  12.135 +
  12.136 +lemma pmf_bind_pmf_of_set:
  12.137 +  assumes "A \<noteq> {}" "finite A"
  12.138 +  shows   "pmf (bind_pmf (pmf_of_set A) f) x = 
  12.139 +             (\<Sum>xa\<in>A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs")
  12.140 +proof -
  12.141 +  from assms have "card A > 0" by auto
  12.142 +  with assms have "ennreal ?lhs = ennreal ?rhs"
  12.143 +    by (subst ennreal_pmf_bind) 
  12.144 +       (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric] 
  12.145 +        setsum_nonneg ennreal_of_nat_eq_real_of_nat)
  12.146 +  thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg)
  12.147 +qed
  12.148 +
  12.149  lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
  12.150  by(rule pmf_eqI)(simp add: indicator_def)
  12.151  
  12.152 @@ -1590,6 +1674,38 @@
  12.153    qed
  12.154  qed
  12.155  
  12.156 +text \<open>
  12.157 +  Choosing an element uniformly at random from the union of a disjoint family 
  12.158 +  of finite non-empty sets with the same size is the same as first choosing a set 
  12.159 +  from the family uniformly at random and then choosing an element from the chosen set 
  12.160 +  uniformly at random.  
  12.161 +\<close>
  12.162 +lemma pmf_of_set_UN:
  12.163 +  assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
  12.164 +          "\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A"
  12.165 +  shows   "pmf_of_set (UNION A f) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
  12.166 +            (is "?lhs = ?rhs")
  12.167 +proof (intro pmf_eqI)
  12.168 +  fix x
  12.169 +  from assms have [simp]: "finite A"
  12.170 +    using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast
  12.171 +  from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) =
  12.172 +    ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))"
  12.173 +    by (subst pmf_of_set) auto
  12.174 +  also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
  12.175 +    by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
  12.176 +  also from assms 
  12.177 +    have "indicator (\<Union>x\<in>A. f x) x / real \<dots> = 
  12.178 +              indicator (\<Union>x\<in>A. f x) x / (n * real (card A))"
  12.179 +      by (simp add: setsum_divide_distrib [symmetric] mult_ac)
  12.180 +  also from assms have "indicator (\<Union>x\<in>A. f x) x = (\<Sum>y\<in>A. indicator (f y) x)"
  12.181 +    by (intro indicator_UN_disjoint) simp_all
  12.182 +  also from assms have "ereal ((\<Sum>y\<in>A. indicator (f y) x) / (real n * real (card A))) =
  12.183 +                          ereal (pmf ?rhs x)"
  12.184 +    by (subst pmf_bind_pmf_of_set) (simp_all add: setsum_divide_distrib)
  12.185 +  finally show "pmf ?lhs x = pmf ?rhs x" by simp
  12.186 +qed
  12.187 +
  12.188  lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
  12.189    by (rule pmf_eqI) simp_all
  12.190  
  12.191 @@ -1670,4 +1786,139 @@
  12.192  
  12.193  end
  12.194  
  12.195 +
  12.196 +subsection \<open>PMFs from assiciation lists\<close>
  12.197 +
  12.198 +definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where 
  12.199 +  "pmf_of_list xs = embed_pmf (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
  12.200 +
  12.201 +definition pmf_of_list_wf where
  12.202 +  "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> listsum (map snd xs) = 1"
  12.203 +
  12.204 +lemma pmf_of_list_wfI:
  12.205 +  "(\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum (map snd xs) = 1 \<Longrightarrow> pmf_of_list_wf xs"
  12.206 +  unfolding pmf_of_list_wf_def by simp
  12.207 +
  12.208 +context
  12.209 +begin
  12.210 +
  12.211 +private lemma pmf_of_list_aux:
  12.212 +  assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
  12.213 +  assumes "listsum (map snd xs) = 1"
  12.214 +  shows "(\<integral>\<^sup>+ x. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
  12.215 +proof -
  12.216 +  have "(\<integral>\<^sup>+ x. ennreal (listsum (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
  12.217 +            (\<integral>\<^sup>+ x. ennreal (listsum (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
  12.218 +    by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter) (auto intro: listsum_cong)
  12.219 +  also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. (\<integral>\<^sup>+ x. ennreal (indicator {x'} x * p) \<partial>count_space UNIV))"
  12.220 +    using assms(1)
  12.221 +  proof (induction xs)
  12.222 +    case (Cons x xs)
  12.223 +    from Cons.prems have "snd x \<ge> 0" by simp
  12.224 +    moreover have "b \<ge> 0" if "(a,b) \<in> set xs" for a b
  12.225 +      using Cons.prems[of b] that by force
  12.226 +    ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) = 
  12.227 +            (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) + 
  12.228 +            ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
  12.229 +      by (intro nn_integral_cong, subst ennreal_plus [symmetric]) 
  12.230 +         (auto simp: case_prod_unfold indicator_def intro!: listsum_nonneg)
  12.231 +    also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) + 
  12.232 +                      (\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
  12.233 +      by (intro nn_integral_add)
  12.234 +         (force intro!: listsum_nonneg AE_I2 intro: Cons simp: indicator_def)+
  12.235 +    also have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV) =
  12.236 +               (\<Sum>(x', p)\<leftarrow>xs. (\<integral>\<^sup>+ y. ennreal (indicator {x'} y * p) \<partial>count_space UNIV))"
  12.237 +      using Cons(1) by (intro Cons) simp_all
  12.238 +    finally show ?case by (simp add: case_prod_unfold)
  12.239 +  qed simp
  12.240 +  also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. ennreal p * (\<integral>\<^sup>+ x. indicator {x'} x \<partial>count_space UNIV))"
  12.241 +    using assms(1)
  12.242 +    by (intro listsum_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
  12.243 +       (auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator
  12.244 +             simp del: times_ereal.simps)+
  12.245 +  also from assms have "\<dots> = listsum (map snd xs)" by (simp add: case_prod_unfold listsum_ennreal)
  12.246 +  also have "\<dots> = 1" using assms(2) by simp
  12.247 +  finally show ?thesis .
  12.248 +qed
  12.249 +
  12.250 +lemma pmf_pmf_of_list:
  12.251 +  assumes "pmf_of_list_wf xs"
  12.252 +  shows   "pmf (pmf_of_list xs) x = listsum (map snd (filter (\<lambda>z. fst z = x) xs))"
  12.253 +  using assms pmf_of_list_aux[of xs] unfolding pmf_of_list_def pmf_of_list_wf_def
  12.254 +  by (subst pmf_embed_pmf) (auto intro!: listsum_nonneg)
  12.255 +
  12.256  end
  12.257 +
  12.258 +lemma set_pmf_of_list:
  12.259 +  assumes "pmf_of_list_wf xs"
  12.260 +  shows   "set_pmf (pmf_of_list xs) \<subseteq> set (map fst xs)"
  12.261 +proof clarify
  12.262 +  fix x assume A: "x \<in> set_pmf (pmf_of_list xs)"
  12.263 +  show "x \<in> set (map fst xs)"
  12.264 +  proof (rule ccontr)
  12.265 +    assume "x \<notin> set (map fst xs)"
  12.266 +    hence "[z\<leftarrow>xs . fst z = x] = []" by (auto simp: filter_empty_conv)
  12.267 +    with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq)
  12.268 +  qed
  12.269 +qed
  12.270 +
  12.271 +lemma finite_set_pmf_of_list:
  12.272 +  assumes "pmf_of_list_wf xs"
  12.273 +  shows   "finite (set_pmf (pmf_of_list xs))"
  12.274 +  using assms by (rule finite_subset[OF set_pmf_of_list]) simp_all
  12.275 +
  12.276 +lemma emeasure_Int_set_pmf:
  12.277 +  "emeasure (measure_pmf p) (A \<inter> set_pmf p) = emeasure (measure_pmf p) A"
  12.278 +  by (rule emeasure_eq_AE) (auto simp: AE_measure_pmf_iff)
  12.279 +
  12.280 +lemma measure_Int_set_pmf:
  12.281 +  "measure (measure_pmf p) (A \<inter> set_pmf p) = measure (measure_pmf p) A"
  12.282 +  using emeasure_Int_set_pmf[of p A] by (simp add: Sigma_Algebra.measure_def)
  12.283 +
  12.284 +lemma emeasure_pmf_of_list:
  12.285 +  assumes "pmf_of_list_wf xs"
  12.286 +  shows   "emeasure (pmf_of_list xs) A = ennreal (listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
  12.287 +proof -
  12.288 +  have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
  12.289 +    by simp
  12.290 +  also from assms 
  12.291 +    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])))"
  12.292 +    by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
  12.293 +  also from assms 
  12.294 +    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. listsum (map snd [z\<leftarrow>xs . fst z = x]))"
  12.295 +    by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: listsum_nonneg)
  12.296 +  also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. 
  12.297 +      indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
  12.298 +    using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
  12.299 +  also have "?S = (\<Sum>x\<in>set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)"
  12.300 +    using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
  12.301 +  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
  12.302 +    using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
  12.303 +  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * 
  12.304 +                      listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
  12.305 +    using assms by (simp add: pmf_pmf_of_list)
  12.306 +  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). listsum (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
  12.307 +    by (intro setsum.cong) (auto simp: indicator_def)
  12.308 +  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
  12.309 +                     if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
  12.310 +    by (intro setsum.cong refl, subst listsum_map_filter, subst listsum_setsum_nth) simp
  12.311 +  also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs). 
  12.312 +                     if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
  12.313 +    by (rule setsum.commute)
  12.314 +  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then 
  12.315 +                     (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
  12.316 +    by (auto intro!: setsum.cong setsum.neutral)
  12.317 +  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
  12.318 +    by (intro setsum.cong refl) (simp_all add: setsum.delta)
  12.319 +  also have "\<dots> = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
  12.320 +    by (subst listsum_map_filter, subst listsum_setsum_nth) simp_all
  12.321 +  finally show ?thesis . 
  12.322 +qed
  12.323 +
  12.324 +lemma measure_pmf_of_list:
  12.325 +  assumes "pmf_of_list_wf xs"
  12.326 +  shows   "measure (pmf_of_list xs) A = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
  12.327 +  using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def
  12.328 +  by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: listsum_nonneg)
  12.329 +
  12.330 +end
    13.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue May 17 08:40:24 2016 +0200
    13.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue May 17 17:05:35 2016 +0200
    13.3 @@ -111,6 +111,9 @@
    13.4  lemma (in prob_space) emeasure_le_1: "emeasure M S \<le> 1"
    13.5    unfolding ennreal_1[symmetric] emeasure_eq_measure by (subst ennreal_le_iff) auto
    13.6  
    13.7 +lemma (in prob_space) emeasure_ge_1_iff: "emeasure M A \<ge> 1 \<longleftrightarrow> emeasure M A = 1"
    13.8 +  by (rule iffI, intro antisym emeasure_le_1) simp_all
    13.9 +
   13.10  lemma (in prob_space) AE_iff_emeasure_eq_1:
   13.11    assumes [measurable]: "Measurable.pred M P"
   13.12    shows "(AE x in M. P x) \<longleftrightarrow> emeasure M {x\<in>space M. P x} = 1"
   13.13 @@ -125,6 +128,9 @@
   13.14  lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1"
   13.15    using emeasure_space[of M X] by (simp add: emeasure_space_1)
   13.16  
   13.17 +lemma (in prob_space) measure_ge_1_iff: "measure M A \<ge> 1 \<longleftrightarrow> measure M A = 1"
   13.18 +  by (auto intro!: antisym)  
   13.19 +
   13.20  lemma (in prob_space) AE_I_eq_1:
   13.21    assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
   13.22    shows "AE x in M. P x"
    14.1 --- a/src/HOL/Set.thy	Tue May 17 08:40:24 2016 +0200
    14.2 +++ b/src/HOL/Set.thy	Tue May 17 17:05:35 2016 +0200
    14.3 @@ -1803,6 +1803,21 @@
    14.4  lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
    14.5    by blast
    14.6  
    14.7 +  
    14.8 +subsubsection \<open>Singleton sets\<close>
    14.9 +
   14.10 +definition is_singleton :: "'a set \<Rightarrow> bool" where
   14.11 +  "is_singleton A \<longleftrightarrow> (\<exists>x. A = {x})"
   14.12 +
   14.13 +lemma is_singletonI [simp, intro!]: "is_singleton {x}"
   14.14 +  unfolding is_singleton_def by simp
   14.15 +
   14.16 +lemma is_singletonI': "A \<noteq> {} \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y) \<Longrightarrow> is_singleton A"
   14.17 +  unfolding is_singleton_def by blast
   14.18 +
   14.19 +lemma is_singletonE: "is_singleton A \<Longrightarrow> (\<And>x. A = {x} \<Longrightarrow> P) \<Longrightarrow> P"
   14.20 +  unfolding is_singleton_def by blast
   14.21 +
   14.22  
   14.23  subsubsection \<open>Getting the Contents of a Singleton Set\<close>
   14.24  
   14.25 @@ -1812,6 +1827,9 @@
   14.26  lemma the_elem_eq [simp]: "the_elem {x} = x"
   14.27    by (simp add: the_elem_def)
   14.28  
   14.29 +lemma is_singleton_the_elem: "is_singleton A \<longleftrightarrow> A = {the_elem A}"
   14.30 +  by (auto simp: is_singleton_def)
   14.31 +
   14.32  lemma the_elem_image_unique:
   14.33    assumes "A \<noteq> {}"
   14.34    assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
   14.35 @@ -1916,6 +1934,9 @@
   14.36  lemma pairwise_singleton [simp]: "pairwise P {A}"
   14.37    by (simp add: pairwise_def)
   14.38  
   14.39 +lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
   14.40 +  by blast
   14.41 +
   14.42  hide_const (open) member not_member
   14.43  
   14.44  lemmas equalityI = subset_antisym
    15.1 --- a/src/HOL/Set_Interval.thy	Tue May 17 08:40:24 2016 +0200
    15.2 +++ b/src/HOL/Set_Interval.thy	Tue May 17 17:05:35 2016 +0200
    15.3 @@ -1640,6 +1640,10 @@
    15.4    finally show ?case .
    15.5  qed
    15.6  
    15.7 +lemma setsum_lessThan_Suc_shift:
    15.8 +  "(\<Sum>i<Suc n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
    15.9 +  by (induction n) (simp_all add: add_ac)
   15.10 +
   15.11  lemma setsum_atMost_shift:
   15.12    fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
   15.13    shows "(\<Sum>i\<le>n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
    16.1 --- a/src/HOL/Wellfounded.thy	Tue May 17 08:40:24 2016 +0200
    16.2 +++ b/src/HOL/Wellfounded.thy	Tue May 17 17:05:35 2016 +0200
    16.3 @@ -112,6 +112,10 @@
    16.4    obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
    16.5    using Q wfE_pf[OF wf, of Q] by blast
    16.6  
    16.7 +lemma wfE_min':
    16.8 +  "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"
    16.9 +  using wfE_min[of R _ Q] by blast
   16.10 +
   16.11  lemma wfI_min:
   16.12    assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
   16.13    shows "wf R"
   16.14 @@ -918,6 +922,19 @@
   16.15  apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
   16.16  done
   16.17  
   16.18 +lemma finite_subset_wf:
   16.19 +  assumes "finite A"
   16.20 +  shows   "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   16.21 +proof (intro finite_acyclic_wf)
   16.22 +  have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A" by blast
   16.23 +  thus "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" 
   16.24 +    by (rule finite_subset) (auto simp: assms finite_cartesian_product)
   16.25 +next
   16.26 +  have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}"
   16.27 +    by (intro trancl_id transI) blast
   16.28 +  also have " \<forall>x. (x, x) \<notin> \<dots>" by blast
   16.29 +  finally show "acyclic {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" by (rule acyclicI)
   16.30 +qed
   16.31  
   16.32  hide_const (open) acc accp
   16.33