summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 03 Oct 2018 09:46:42 +0200 | |

changeset 69107 | c2de7a5c8de9 |

parent 69106 | 742c88258cf8 |

child 69108 | e2780bb26395 |

shuffle -> shuffles

--- a/src/HOL/Binomial.thy Tue Oct 02 21:37:26 2018 +0200 +++ b/src/HOL/Binomial.thy Wed Oct 03 09:46:42 2018 +0200 @@ -1243,21 +1243,21 @@ qed qed -lemma card_disjoint_shuffle: +lemma card_disjoint_shuffles: assumes "set xs \<inter> set ys = {}" - shows "card (shuffle xs ys) = (length xs + length ys) choose length xs" + shows "card (shuffles xs ys) = (length xs + length ys) choose length xs" using assms -proof (induction xs ys rule: shuffle.induct) +proof (induction xs ys rule: shuffles.induct) case (3 x xs y ys) - have "shuffle (x # xs) (y # ys) = (#) x ` shuffle xs (y # ys) \<union> (#) y ` shuffle (x # xs) ys" - by (rule shuffle.simps) - also have "card \<dots> = card ((#) x ` shuffle xs (y # ys)) + card ((#) y ` shuffle (x # xs) ys)" + have "shuffles (x # xs) (y # ys) = (#) x ` shuffles xs (y # ys) \<union> (#) y ` shuffles (x # xs) ys" + by (rule shuffles.simps) + also have "card \<dots> = card ((#) x ` shuffles xs (y # ys)) + card ((#) y ` shuffles (x # xs) ys)" by (rule card_Un_disjoint) (insert "3.prems", auto) - also have "card ((#) x ` shuffle xs (y # ys)) = card (shuffle xs (y # ys))" + also have "card ((#) x ` shuffles xs (y # ys)) = card (shuffles xs (y # ys))" by (rule card_image) auto also have "\<dots> = (length xs + length (y # ys)) choose length xs" using "3.prems" by (intro "3.IH") auto - also have "card ((#) y ` shuffle (x # xs) ys) = card (shuffle (x # xs) ys)" + also have "card ((#) y ` shuffles (x # xs) ys) = card (shuffles (x # xs) ys)" by (rule card_image) auto also have "\<dots> = (length (x # xs) + length ys) choose length (x # xs)" using "3.prems" by (intro "3.IH") auto

--- a/src/HOL/Library/Multiset.thy Tue Oct 02 21:37:26 2018 +0200 +++ b/src/HOL/Library/Multiset.thy Wed Oct 03 09:46:42 2018 +0200 @@ -1936,8 +1936,8 @@ ultimately show ?case by simp qed -lemma mset_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> mset zs = mset xs + mset ys" - by (induction xs ys arbitrary: zs rule: shuffle.induct) auto +lemma mset_shuffles: "zs \<in> shuffles xs ys \<Longrightarrow> mset zs = mset xs + mset ys" + by (induction xs ys arbitrary: zs rule: shuffles.induct) auto lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)" by (induct xs) simp_all

--- a/src/HOL/List.thy Tue Oct 02 21:37:26 2018 +0200 +++ b/src/HOL/List.thy Wed Oct 03 09:46:42 2018 +0200 @@ -266,10 +266,10 @@ termination by(relation "measure(\<lambda>(xs,ys). size xs + size ys)") auto -function shuffle where - "shuffle [] ys = {ys}" -| "shuffle xs [] = {xs}" -| "shuffle (x # xs) (y # ys) = (#) x ` shuffle xs (y # ys) \<union> (#) y ` shuffle (x # xs) ys" +function shuffles where + "shuffles [] ys = {ys}" +| "shuffles xs [] = {xs}" +| "shuffles (x # xs) (y # ys) = (#) x ` shuffles xs (y # ys) \<union> (#) y ` shuffles (x # xs) ys" by pat_completeness simp_all termination by lexicographic_order @@ -307,7 +307,7 @@ @{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\ @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ -@{lemma "shuffle [a,b] [c,d] = {[a,b,c,d],[a,c,b,d],[a,c,d,b],[c,a,b,d],[c,a,d,b],[c,d,a,b]}" +@{lemma "shuffles [a,b] [c,d] = {[a,b,c,d],[a,c,b,d],[a,c,d,b],[c,a,b,d],[c,a,d,b],[c,d,a,b]}" by (simp add: insert_commute)}\\ @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\ @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\ @@ -4532,145 +4532,145 @@ by (induct xs ys rule: splice.induct) auto -subsubsection \<open>@{const shuffle}\<close> - -lemma shuffle_commutes: "shuffle xs ys = shuffle ys xs" -by (induction xs ys rule: shuffle.induct) (simp_all add: Un_commute) - -lemma Nil_in_shuffle[simp]: "[] \<in> shuffle xs ys \<longleftrightarrow> xs = [] \<and> ys = []" - by (induct xs ys rule: shuffle.induct) auto - -lemma shuffleE: - "zs \<in> shuffle xs ys \<Longrightarrow> +subsubsection \<open>@{const shuffles}\<close> + +lemma shuffles_commutes: "shuffles xs ys = shuffles ys xs" +by (induction xs ys rule: shuffles.induct) (simp_all add: Un_commute) + +lemma Nil_in_shuffles[simp]: "[] \<in> shuffles xs ys \<longleftrightarrow> xs = [] \<and> ys = []" + by (induct xs ys rule: shuffles.induct) auto + +lemma shufflesE: + "zs \<in> shuffles xs ys \<Longrightarrow> (zs = xs \<Longrightarrow> ys = [] \<Longrightarrow> P) \<Longrightarrow> (zs = ys \<Longrightarrow> xs = [] \<Longrightarrow> P) \<Longrightarrow> - (\<And>x xs' z zs'. xs = x # xs' \<Longrightarrow> zs = z # zs' \<Longrightarrow> x = z \<Longrightarrow> zs' \<in> shuffle xs' ys \<Longrightarrow> P) \<Longrightarrow> - (\<And>y ys' z zs'. ys = y # ys' \<Longrightarrow> zs = z # zs' \<Longrightarrow> y = z \<Longrightarrow> zs' \<in> shuffle xs ys' \<Longrightarrow> P) \<Longrightarrow> P" - by (induct xs ys rule: shuffle.induct) auto - -lemma Cons_in_shuffle_iff: - "z # zs \<in> shuffle xs ys \<longleftrightarrow> - (xs \<noteq> [] \<and> hd xs = z \<and> zs \<in> shuffle (tl xs) ys \<or> - ys \<noteq> [] \<and> hd ys = z \<and> zs \<in> shuffle xs (tl ys))" - by (induct xs ys rule: shuffle.induct) auto - -lemma splice_in_shuffle [simp, intro]: "splice xs ys \<in> shuffle xs ys" -by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffle_iff shuffle_commutes) - -lemma Nil_in_shuffleI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffle xs ys" + (\<And>x xs' z zs'. xs = x # xs' \<Longrightarrow> zs = z # zs' \<Longrightarrow> x = z \<Longrightarrow> zs' \<in> shuffles xs' ys \<Longrightarrow> P) \<Longrightarrow> + (\<And>y ys' z zs'. ys = y # ys' \<Longrightarrow> zs = z # zs' \<Longrightarrow> y = z \<Longrightarrow> zs' \<in> shuffles xs ys' \<Longrightarrow> P) \<Longrightarrow> P" + by (induct xs ys rule: shuffles.induct) auto + +lemma Cons_in_shuffles_iff: + "z # zs \<in> shuffles xs ys \<longleftrightarrow> + (xs \<noteq> [] \<and> hd xs = z \<and> zs \<in> shuffles (tl xs) ys \<or> + ys \<noteq> [] \<and> hd ys = z \<and> zs \<in> shuffles xs (tl ys))" + by (induct xs ys rule: shuffles.induct) auto + +lemma splice_in_shuffles [simp, intro]: "splice xs ys \<in> shuffles xs ys" +by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffles_iff shuffles_commutes) + +lemma Nil_in_shufflesI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffles xs ys" by simp -lemma Cons_in_shuffle_leftI: "zs \<in> shuffle xs ys \<Longrightarrow> z # zs \<in> shuffle (z # xs) ys" +lemma Cons_in_shuffles_leftI: "zs \<in> shuffles xs ys \<Longrightarrow> z # zs \<in> shuffles (z # xs) ys" by (cases ys) auto -lemma Cons_in_shuffle_rightI: "zs \<in> shuffle xs ys \<Longrightarrow> z # zs \<in> shuffle xs (z # ys)" +lemma Cons_in_shuffles_rightI: "zs \<in> shuffles xs ys \<Longrightarrow> z # zs \<in> shuffles xs (z # ys)" by (cases xs) auto -lemma finite_shuffle [simp, intro]: "finite (shuffle xs ys)" - by (induction xs ys rule: shuffle.induct) simp_all - -lemma length_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> length zs = length xs + length ys" - by (induction xs ys arbitrary: zs rule: shuffle.induct) auto - -lemma set_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> set zs = set xs \<union> set ys" - by (induction xs ys arbitrary: zs rule: shuffle.induct) auto - -lemma distinct_disjoint_shuffle: - assumes "distinct xs" "distinct ys" "set xs \<inter> set ys = {}" "zs \<in> shuffle xs ys" +lemma finite_shuffles [simp, intro]: "finite (shuffles xs ys)" + by (induction xs ys rule: shuffles.induct) simp_all + +lemma length_shuffles: "zs \<in> shuffles xs ys \<Longrightarrow> length zs = length xs + length ys" + by (induction xs ys arbitrary: zs rule: shuffles.induct) auto + +lemma set_shuffles: "zs \<in> shuffles xs ys \<Longrightarrow> set zs = set xs \<union> set ys" + by (induction xs ys arbitrary: zs rule: shuffles.induct) auto + +lemma distinct_disjoint_shuffles: + assumes "distinct xs" "distinct ys" "set xs \<inter> set ys = {}" "zs \<in> shuffles xs ys" shows "distinct zs" using assms -proof (induction xs ys arbitrary: zs rule: shuffle.induct) +proof (induction xs ys arbitrary: zs rule: shuffles.induct) case (3 x xs y ys) show ?case proof (cases zs) case (Cons z zs') - with "3.prems" and "3.IH"[of zs'] show ?thesis by (force dest: set_shuffle) + with "3.prems" and "3.IH"[of zs'] show ?thesis by (force dest: set_shuffles) qed simp_all qed simp_all -lemma Cons_shuffle_subset1: "(#) x ` shuffle xs ys \<subseteq> shuffle (x # xs) ys" +lemma Cons_shuffles_subset1: "(#) x ` shuffles xs ys \<subseteq> shuffles (x # xs) ys" by (cases ys) auto -lemma Cons_shuffle_subset2: "(#) y ` shuffle xs ys \<subseteq> shuffle xs (y # ys)" +lemma Cons_shuffles_subset2: "(#) y ` shuffles xs ys \<subseteq> shuffles xs (y # ys)" by (cases xs) auto -lemma filter_shuffle: - "filter P ` shuffle xs ys = shuffle (filter P xs) (filter P ys)" +lemma filter_shuffles: + "filter P ` shuffles xs ys = shuffles (filter P xs) (filter P ys)" proof - have *: "filter P ` (#) x ` A = (if P x then (#) x ` filter P ` A else filter P ` A)" for x A by (auto simp: image_image) show ?thesis - by (induction xs ys rule: shuffle.induct) + by (induction xs ys rule: shuffles.induct) (simp_all split: if_splits add: image_Un * Un_absorb1 Un_absorb2 - Cons_shuffle_subset1 Cons_shuffle_subset2) + Cons_shuffles_subset1 Cons_shuffles_subset2) qed -lemma filter_shuffle_disjoint1: - assumes "set xs \<inter> set ys = {}" "zs \<in> shuffle xs ys" +lemma filter_shuffles_disjoint1: + assumes "set xs \<inter> set ys = {}" "zs \<in> shuffles xs ys" shows "filter (\<lambda>x. x \<in> set xs) zs = xs" (is "filter ?P _ = _") and "filter (\<lambda>x. x \<notin> set xs) zs = ys" (is "filter ?Q _ = _") using assms proof - - from assms have "filter ?P zs \<in> filter ?P ` shuffle xs ys" by blast - also have "filter ?P ` shuffle xs ys = shuffle (filter ?P xs) (filter ?P ys)" - by (rule filter_shuffle) + from assms have "filter ?P zs \<in> filter ?P ` shuffles xs ys" by blast + also have "filter ?P ` shuffles xs ys = shuffles (filter ?P xs) (filter ?P ys)" + by (rule filter_shuffles) also have "filter ?P xs = xs" by (rule filter_True) simp_all also have "filter ?P ys = []" by (rule filter_False) (insert assms(1), auto) - also have "shuffle xs [] = {xs}" by simp + also have "shuffles xs [] = {xs}" by simp finally show "filter ?P zs = xs" by simp next - from assms have "filter ?Q zs \<in> filter ?Q ` shuffle xs ys" by blast - also have "filter ?Q ` shuffle xs ys = shuffle (filter ?Q xs) (filter ?Q ys)" - by (rule filter_shuffle) + from assms have "filter ?Q zs \<in> filter ?Q ` shuffles xs ys" by blast + also have "filter ?Q ` shuffles xs ys = shuffles (filter ?Q xs) (filter ?Q ys)" + by (rule filter_shuffles) also have "filter ?Q ys = ys" by (rule filter_True) (insert assms(1), auto) also have "filter ?Q xs = []" by (rule filter_False) (insert assms(1), auto) - also have "shuffle [] ys = {ys}" by simp + also have "shuffles [] ys = {ys}" by simp finally show "filter ?Q zs = ys" by simp qed -lemma filter_shuffle_disjoint2: - assumes "set xs \<inter> set ys = {}" "zs \<in> shuffle xs ys" +lemma filter_shuffles_disjoint2: + assumes "set xs \<inter> set ys = {}" "zs \<in> shuffles xs ys" shows "filter (\<lambda>x. x \<in> set ys) zs = ys" "filter (\<lambda>x. x \<notin> set ys) zs = xs" - using filter_shuffle_disjoint1[of ys xs zs] assms - by (simp_all add: shuffle_commutes Int_commute) - -lemma partition_in_shuffle: - "xs \<in> shuffle (filter P xs) (filter (\<lambda>x. \<not>P x) xs)" + using filter_shuffles_disjoint1[of ys xs zs] assms + by (simp_all add: shuffles_commutes Int_commute) + +lemma partition_in_shuffles: + "xs \<in> shuffles (filter P xs) (filter (\<lambda>x. \<not>P x) xs)" proof (induction xs) case (Cons x xs) show ?case proof (cases "P x") case True - hence "x # xs \<in> (#) x ` shuffle (filter P xs) (filter (\<lambda>x. \<not>P x) xs)" + hence "x # xs \<in> (#) x ` shuffles (filter P xs) (filter (\<lambda>x. \<not>P x) xs)" by (intro imageI Cons.IH) - also have "\<dots> \<subseteq> shuffle (filter P (x # xs)) (filter (\<lambda>x. \<not>P x) (x # xs))" - by (simp add: True Cons_shuffle_subset1) + also have "\<dots> \<subseteq> shuffles (filter P (x # xs)) (filter (\<lambda>x. \<not>P x) (x # xs))" + by (simp add: True Cons_shuffles_subset1) finally show ?thesis . next case False - hence "x # xs \<in> (#) x ` shuffle (filter P xs) (filter (\<lambda>x. \<not>P x) xs)" + hence "x # xs \<in> (#) x ` shuffles (filter P xs) (filter (\<lambda>x. \<not>P x) xs)" by (intro imageI Cons.IH) - also have "\<dots> \<subseteq> shuffle (filter P (x # xs)) (filter (\<lambda>x. \<not>P x) (x # xs))" - by (simp add: False Cons_shuffle_subset2) + also have "\<dots> \<subseteq> shuffles (filter P (x # xs)) (filter (\<lambda>x. \<not>P x) (x # xs))" + by (simp add: False Cons_shuffles_subset2) finally show ?thesis . qed qed auto lemma inv_image_partition: assumes "\<And>x. x \<in> set xs \<Longrightarrow> P x" "\<And>y. y \<in> set ys \<Longrightarrow> \<not>P y" - shows "partition P -` {(xs, ys)} = shuffle xs ys" + shows "partition P -` {(xs, ys)} = shuffles xs ys" proof (intro equalityI subsetI) - fix zs assume zs: "zs \<in> shuffle xs ys" - hence [simp]: "set zs = set xs \<union> set ys" by (rule set_shuffle) + fix zs assume zs: "zs \<in> shuffles xs ys" + hence [simp]: "set zs = set xs \<union> set ys" by (rule set_shuffles) from assms have "filter P zs = filter (\<lambda>x. x \<in> set xs) zs" "filter (\<lambda>x. \<not>P x) zs = filter (\<lambda>x. x \<in> set ys) zs" by (intro filter_cong refl; force)+ moreover from assms have "set xs \<inter> set ys = {}" by auto ultimately show "zs \<in> partition P -` {(xs, ys)}" using zs - by (simp add: o_def filter_shuffle_disjoint1 filter_shuffle_disjoint2) + by (simp add: o_def filter_shuffles_disjoint1 filter_shuffles_disjoint2) next fix zs assume "zs \<in> partition P -` {(xs, ys)}" - thus "zs \<in> shuffle xs ys" using partition_in_shuffle[of zs] by (auto simp: o_def) + thus "zs \<in> shuffles xs ys" using partition_in_shuffles[of zs] by (auto simp: o_def) qed @@ -7346,22 +7346,22 @@ apply (erule_tac xs=x in list_all2_induct, simp, simp add: rel_fun_def) done -lemma shuffle_transfer [transfer_rule]: - "(list_all2 A ===> list_all2 A ===> rel_set (list_all2 A)) shuffle shuffle" +lemma shuffles_transfer [transfer_rule]: + "(list_all2 A ===> list_all2 A ===> rel_set (list_all2 A)) shuffles shuffles" proof (intro rel_funI, goal_cases) case (1 xs xs' ys ys') thus ?case - proof (induction xs ys arbitrary: xs' ys' rule: shuffle.induct) + proof (induction xs ys arbitrary: xs' ys' rule: shuffles.induct) case (3 x xs y ys xs' ys') from "3.prems" obtain x' xs'' where xs': "xs' = x' # xs''" by (cases xs') auto from "3.prems" obtain y' ys'' where ys': "ys' = y' # ys''" by (cases ys') auto have [transfer_rule]: "A x x'" "A y y'" "list_all2 A xs xs''" "list_all2 A ys ys''" using "3.prems" by (simp_all add: xs' ys') - have [transfer_rule]: "rel_set (list_all2 A) (shuffle xs (y # ys)) (shuffle xs'' ys')" and - [transfer_rule]: "rel_set (list_all2 A) (shuffle (x # xs) ys) (shuffle xs' ys'')" + have [transfer_rule]: "rel_set (list_all2 A) (shuffles xs (y # ys)) (shuffles xs'' ys')" and + [transfer_rule]: "rel_set (list_all2 A) (shuffles (x # xs) ys) (shuffles xs' ys'')" using "3.prems" by (auto intro!: "3.IH" simp: xs' ys') - have "rel_set (list_all2 A) ((#) x ` shuffle xs (y # ys) \<union> (#) y ` shuffle (x # xs) ys) - ((#) x' ` shuffle xs'' ys' \<union> (#) y' ` shuffle xs' ys'')" by transfer_prover + have "rel_set (list_all2 A) ((#) x ` shuffles xs (y # ys) \<union> (#) y ` shuffles (x # xs) ys) + ((#) x' ` shuffles xs'' ys' \<union> (#) y' ` shuffles xs' ys'')" by transfer_prover thus ?case by (simp add: xs' ys') qed (auto simp: rel_set_def) qed

--- a/src/HOL/Probability/Random_Permutations.thy Tue Oct 02 21:37:26 2018 +0200 +++ b/src/HOL/Probability/Random_Permutations.thy Wed Oct 03 09:46:42 2018 +0200 @@ -204,13 +204,13 @@ have "pmf ?lhs (xs, ys) = real (card (permutations_of_set A \<inter> partition P -` {(xs, ys)})) / fact (card A)" using assms by (auto simp: pmf_map measure_pmf_of_set) - also have "partition P -` {(xs, ys)} = shuffle xs ys" + also have "partition P -` {(xs, ys)} = shuffles xs ys" using True by (intro inv_image_partition) (auto simp: permutations_of_set_def) - also have "permutations_of_set A \<inter> shuffle xs ys = shuffle xs ys" - using True distinct_disjoint_shuffle[of xs ys] - by (auto simp: permutations_of_set_def dest: set_shuffle) - also have "card (shuffle xs ys) = length xs + length ys choose length xs" - using True by (intro card_disjoint_shuffle) (auto simp: permutations_of_set_def) + also have "permutations_of_set A \<inter> shuffles xs ys = shuffles xs ys" + using True distinct_disjoint_shuffles[of xs ys] + by (auto simp: permutations_of_set_def dest: set_shuffles) + also have "card (shuffles xs ys) = length xs + length ys choose length xs" + using True by (intro card_disjoint_shuffles) (auto simp: permutations_of_set_def) also have "length xs + length ys = card A" by (simp add: card_eq) also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))" by (subst binomial_fact) (auto intro!: card_mono assms)