# HG changeset patch # User eberlm # Date 1463497535 -7200 # Node ID af0e964aad7b6e01513237b9f94509603a280a41 # Parent ee8edbcbb4adcd39c456a1cd2197883db1abef7b Moved material from AFP/Randomised_Social_Choice to distribution diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Complete_Lattices.thy Tue May 17 17:05:35 2016 +0200 @@ -1276,6 +1276,8 @@ lemma UN_singleton [simp]: "(\x\A. {x}) = A" by blast +lemma inj_on_image: "inj_on f (\A) \ inj_on (op ` f) A" + unfolding inj_on_def by blast subsubsection \Distributive laws\ diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Finite_Set.thy Tue May 17 17:05:35 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: "\finite B \ P B" + and remove: "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A" + shows "P B" +proof (cases "finite B") + assume "\finite B" + thus ?thesis by (rule infinite) +next + define A where "A = B" + assume "finite B" + hence "finite A" "A \ 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 \A \ B\ and \finite B\ have "finite A" by (rule finite_subset) + moreover from Suc.hyps have "A \ {}" by auto + moreover note \A \ B\ + moreover have "P (A - {x})" if x: "x \ A" for x + using x Suc.prems \Suc n = card A\ 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: "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A" + defines "B' \ B" + shows "P B'" + by (induction B' rule: remove_induct) (simp_all add: assms) + + text\main cardinality theorem\ 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 \ 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 \ Suc n \ card A = (\a B. A = insert a B \ a \ B \ n \ card B \ finite B)" by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Groups_List.thy --- a/src/HOL/Groups_List.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Groups_List.thy Tue May 17 17:05:35 2016 +0200 @@ -255,6 +255,24 @@ finally show ?thesis by(simp add:listsum_map_eq_setsum_count) qed +lemma listsum_nonneg: + "(\x. x \ set xs \ (x :: 'a :: ordered_comm_monoid_add) \ 0) \ listsum xs \ 0" + by (induction xs) simp_all + +lemma listsum_map_filter: + "listsum (map f (filter P xs)) = listsum (map (\x. if P x then f x else 0) xs)" + by (induction xs) simp_all + +lemma listsum_cong [fundef_cong]: + assumes "xs = ys" + assumes "\x. x \ set xs \ 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 \Further facts about @{const List.n_lists}\ @@ -347,6 +365,16 @@ end +lemma listprod_cong [fundef_cong]: + assumes "xs = ys" + assumes "\x. x \ set xs \ 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 \Some syntactic sugar:\ syntax (ASCII) diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Library/Disjoint_Sets.thy --- a/src/HOL/Library/Disjoint_Sets.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Library/Disjoint_Sets.thy Tue May 17 17:05:35 2016 +0200 @@ -35,6 +35,13 @@ "disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}" unfolding disjoint_def by auto +lemma disjoint_image: "inj_on f (\A) \ disjoint A \ disjoint (op ` f ` A)" + unfolding inj_on_def disjoint_def by blast + +lemma assumes "disjoint (A \ B)" + shows disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B" + using assms by (simp_all add: disjoint_def) + lemma disjoint_INT: assumes *: "\i. i \ I \ disjoint (F i)" shows "disjoint {\i\I. X i | X. \i\I. X i \ F i}" @@ -81,7 +88,7 @@ lemma disjoint_family_on_disjoint_image: "disjoint_family_on A I \ disjoint (A ` I)" unfolding disjoint_family_on_def disjoint_def by force - + lemma disjoint_family_on_vimageI: "disjoint_family_on F I \ disjoint_family_on (\i. f -` F i) I" by (auto simp: disjoint_family_on_def) @@ -114,9 +121,60 @@ qed qed +lemma distinct_list_bind: + assumes "distinct xs" "\x. x \ set xs \ distinct (f x)" + "disjoint_family_on (set \ 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: "\i. i \ I \ bij_betw f (A i) (A' i)" + shows "bij_betw f (\i\I. A i) (\i\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 \ I" "j \ I" "x \ A i" "y \ A j" and B: "f x = f y" + from A bij[of i] bij[of j] have "f x \ A' i" "f y \ A' j" + by (auto simp: bij_betw_def) + with B have "A' i \ A' j \ {}" 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 \ disjoint B \ \C \ \B = {} \ disjoint (C \ B)" using disjoint_UN[of "{C, B}" "\x. x"] by (auto simp add: disjoint_family_on_def) +text \ + The union of an infinite disjoint family of non-empty sets is infinite. +\ +lemma infinite_disjoint_family_imp_infinite_UNION: + assumes "\finite A" "\x. x \ A \ f x \ {}" "disjoint_family_on f A" + shows "\finite (UNION A f)" +proof - + def g \ "\x. SOME y. y \ f x" + have g: "g x \ f x" if "x \ 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 \ A" "y \ A" "g x = g y" "x \ y" + with g[of x] g[of y] have "g x \ f x" "g x \ f y" by auto + with A `x \ y` assms show False + by (auto simp: disjoint_family_on_def inj_on_def) + qed + from g have "g ` A \ UNION A f" by blast + moreover from inj_on_g \\finite A\ have "\finite (g ` A)" + using finite_imageD by blast + ultimately show ?thesis using finite_subset by blast +qed + + subsection \Construct Disjoint Sequences\ definition disjointed :: "(nat \ 'a set) \ nat \ 'a set" where @@ -149,5 +207,5 @@ lemma disjointed_mono: "mono A \ disjointed A (Suc n) = A (Suc n) - A n" using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) - + end diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Library/Extended_Nonnegative_Real.thy --- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 17 17:05:35 2016 +0200 @@ -864,6 +864,8 @@ declare [[coercion ennreal]] +lemma ennreal_cong: "x = y \ ennreal x = ennreal y" by simp + lemma ennreal_cases[cases type: ennreal]: fixes x :: ennreal obtains (real) r :: real where "0 \ r" "x = ennreal r" | (top) "x = top" @@ -949,6 +951,19 @@ lemma setsum_ennreal[simp]: "(\i. i \ I \ 0 \ f i) \ (\i\I. ennreal (f i)) = ennreal (setsum f I)" by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg) +lemma listsum_ennreal[simp]: + assumes "\x. x \ set xs \ f x \ 0" + shows "listsum (map (\x. ennreal (f x)) xs) = ennreal (listsum (map f xs))" +using assms +proof (induction xs) + case (Cons x xs) + from Cons have "(\x\x # xs. ennreal (f x)) = ennreal (f x) + ennreal (listsum (map f xs))" + by simp + also from Cons.prems have "\ = 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 diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Library/Extended_Real.thy Tue May 17 17:05:35 2016 +0200 @@ -228,6 +228,8 @@ datatype ereal = ereal real | PInfty | MInfty +lemma ereal_cong: "x = y \ 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 (\x. ereal (f x)) xs) = ereal (listsum (map f xs))" + by (induction xs) simp_all + lemma setsum_Pinfty: fixes f :: "'a \ ereal" shows "(\x\P. f x) = \ \ finite P \ (\i\P. f i = \)" diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Library/Indicator_Function.thy --- a/src/HOL/Library/Indicator_Function.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Library/Indicator_Function.thy Tue May 17 17:05:35 2016 +0200 @@ -5,7 +5,7 @@ section \Indicator Function\ theory Indicator_Function -imports Complex_Main +imports Complex_Main Disjoint_Sets begin definition "indicator S x = (if x \ S then 1 else 0)" @@ -28,6 +28,10 @@ lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \ x \ A" by (auto simp: indicator_def) +lemma indicator_leI: + "(x \ A \ y \ B) \ (indicator A x :: 'a :: linordered_nonzero_semiring) \ indicator B y" + by (auto simp: indicator_def) + lemma split_indicator: "P (indicator S x) \ ((x \ S \ P 1) \ (x \ S \ P 0))" unfolding indicator_def by auto @@ -161,4 +165,14 @@ finally show ?thesis . qed simp +text \ + The indicator function of the union of a disjoint family of sets is the + sum over all the individual indicators. +\ +lemma indicator_UN_disjoint: + assumes "finite A" "disjoint_family_on f A" + shows "indicator (UNION A f) x = (\y\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 diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Library/Multiset.thy Tue May 17 17:05:35 2016 +0200 @@ -417,6 +417,8 @@ qed + + subsubsection \Pointwise ordering induced by count\ definition subseteq_mset :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) @@ -1159,6 +1161,28 @@ lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \ M = {#}" by (cases M) auto +lemma image_mset_If: + "image_mset (\x. if P x then f x else g x) A = + image_mset f (filter_mset P A) + image_mset g (filter_mset (\x. \P x) A)" + by (induction A) (auto simp: add_ac) + +lemma image_mset_Diff: + assumes "B \# 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 = (\y\f -` {x} \ 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 \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ :# _#})") syntax @@ -1379,6 +1403,40 @@ lemma elem_mset_set[simp, intro]: "finite A \ x \# mset_set A \ x \ A" by (induct A rule: finite_induct) simp_all +lemma mset_set_Union: + "finite A \ finite B \ A \ B = {} \ mset_set (A \ 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 \ filter_mset P (mset_set A) = mset_set {x\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\A. P x}" + by (rule insert.IH) + also from insert.hyps + have "\ + mset_set (if P x then {x} else {}) = + mset_set ({x \ A. P x} \ (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\insert x A. P y}" by auto + finally show ?case . +qed simp_all + +lemma mset_set_Diff: + assumes "finite A" "B \ A" + shows "mset_set (A - B) = mset_set A - mset_set B" +proof - + from assms have "mset_set ((A - B) \ B) = mset_set (A - B) + mset_set B" + by (intro mset_set_Union) (auto dest: finite_subset) + also from assms have "A - B \ B = A" by blast + finally show ?thesis by simp +qed + +lemma mset_set_set: "distinct xs \ mset_set (set xs) = mset xs" + by (induction xs) (simp_all add: add_ac) + context linorder begin @@ -1418,6 +1476,9 @@ "finite A \ set_mset (mset_set A) = A" by (induct A rule: finite_induct) simp_all +lemma mset_set_empty_iff: "mset_set A = {#} \ A = {} \ infinite A" + using finite_set_mset_mset_set by fastforce + lemma infinite_set_mset_mset_set: "\ finite A \ 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.. {#the (map_of xs i). i \# mset (map fst xs)#} = mset (map snd xs)" +proof (induction xs) + case (Cons x xs) + have "{#the (map_of (x # xs) i). i \# mset (map fst (x # xs))#} = + {#the (if i = fst x then Some (snd x) else map_of xs i). + i \# 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 "\ = mset (map snd xs)" by (intro Cons.IH) simp_all + finally show ?case by simp +qed simp_all + subsection \Replicate operation\ @@ -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 \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10) syntax diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/Library/Permutations.thy Tue May 17 17:05:35 2016 +0200 @@ -5,7 +5,7 @@ section \Permutations, both general and specifically on finite sets.\ theory Permutations -imports Binomial +imports Binomial Multiset Disjoint_Sets begin subsection \Transpositions\ @@ -30,6 +30,10 @@ lemma permutes_in_image: "p permutes S \ p x \ S \ x \ S" unfolding permutes_def by metis + +lemma permutes_not_in: + assumes "f permutes S" "x \ S" shows "f x = x" + using assms by (auto simp: permutes_def) lemma permutes_image: "p permutes S \ p ` S = S" unfolding permutes_def @@ -41,6 +45,9 @@ lemma permutes_inj: "p permutes S \ inj p" unfolding permutes_def inj_on_def by blast +lemma permutes_inj_on: "f permutes S \ inj_on f A" + unfolding permutes_def inj_on_def by auto + lemma permutes_surj: "p permutes s \ 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: "\x. x \ S \ p' (p x) = x" + and outside: "\x. x \ S \ p' x = x" + shows "inv p = p'" +proof + fix x show "inv p x = p' x" + proof (cases "x \ S") + assume [simp]: "x \ S" + from assms have "p' x = p' (p (inv p x))" by (simp add: permutes_inverses) + also from permutes_inv[OF perm] + have "\ = 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 \ f -` A = A" + by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv]) + subsection \The number of permutations on a finite set\ @@ -813,9 +839,164 @@ lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def) + +subsection \Permuting a list\ + +text \This function permutes a list by applying a permutation to the indices.\ + +definition permute_list :: "(nat \ nat) \ 'a list \ 'a list" where + "permute_list f xs = map (\i. xs ! (f i)) [0.. 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 (\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 {.. x < length xs" for x + using permutes_in_image[OF assms] by auto + have "count (mset (permute_list f xs)) y = + card ((\i. xs ! f i) -` {y} \ {..i. xs ! f i) -` {y} \ {.. y = xs ! i}" + by auto + also from assms have "card \ = card {i. i < length xs \ y = xs ! i}" + by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj) + also have "\ = 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 {.. i < length ys" for i by simp + have "permute_list f (zip xs ys) = map (\i. zip xs ys ! f i) [0.. = map (\(x, y). (xs ! f x, ys ! f y)) (zip [0.. = 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 "\ permutes fst ` set xs" + shows "map_of xs \ \ = map_of (map (\(x,y). (inv \ x, y)) xs)" (is "_ = map_of (map ?f _)") +proof + fix x + from assms have "inj \" "surj \" by (simp_all add: permutes_inj permutes_surj) + thus "(map_of xs \ \) x = map_of (map ?f xs) x" + by (induction xs) (auto simp: inv_f_f surj_f_inv_f) +qed + subsection \More lemmas about permutations\ +text \ + If two lists correspond to the same multiset, there exists a permutation + on the list indices that maps one to the other. +\ +lemma mset_eq_permutation: + assumes mset_eq: "mset (xs::'a list) = mset ys" + defines [simp]: "n \ length xs" + obtains f where "f permutes {.. "\(x::'a) xs. {i. i < length xs \ x = xs ! i}" + have indices_of_subset: "indices_of x xs \ {..x\set xs. \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 "\f. bij_betw f (indices_of x xs) (indices_of x ys)" + by (intro finite_same_card_bij) simp_all + qed + hence "\f. \x\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 \ "\i. if i < n then f (xs ! i) i else i" + + have bij_f: "bij_betw (\i. f (xs ! i) i) (indices_of x xs) (indices_of x ys)" + if x: "x \ 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 \ indices_of x xs" + thus "f (xs ! i) i = f x i" by (simp add: indices_of_def) + qed + + hence "bij_betw (\i. f (xs ! i) i) (\x\set xs. indices_of x xs) (\x\set xs. indices_of x ys)" + by (intro bij_betw_UNION_disjoint) (auto simp add: disjoint_family_on_def indices_of_def) + also have "(\x\set xs. indices_of x xs) = {..x\set ys. indices_of x ys) = {..i. f (xs ! i) i) {.. bij_betw g {.. indices_of (xs ! i) xs" by (simp add: indices_of_def) + with bij_f[of "xs ! i"] i have "f (xs ! i) i \ 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 \Constructing permutations from association lists\ + +definition list_permutes where + "list_permutes xs A \ set (map fst xs) \ A \ set (map snd xs) = set (map fst xs) \ + distinct (map fst xs) \ distinct (map snd xs)" + +lemma list_permutesI [simp]: + assumes "set (map fst xs) \ 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 \ x | Some y \ 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 \ set (map fst xs)" "y \ 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') \ set xs" "(y,y') \ 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 \ A \ 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 \ 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 \ 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) \ A" + by (simp add: list_permutes_def) + from assms have "inj_on (the \ map_of xs) (set (map fst xs))" (is ?P) + by (intro inj_on_map_of') (simp_all add: list_permutes_def) + also have "?P \ 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 \ 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 "\ = 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' \ permutation_of_list ((x',y)#xs) x = y" + "x \ x' \ 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' \ inverse_permutation_of_list ((y,x')#xs) x = y" + "x \ x' \ 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 \ 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) \ 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) \ 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 \ 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) \ 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) \ 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 \ set (map snd xs)") + case True + then obtain y where "(y, x) \ 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 diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/List.thy --- a/src/HOL/List.thy Tue May 17 08:40:24 2016 +0200 +++ b/src/HOL/List.thy Tue May 17 17:05:35 2016 +0200 @@ -3298,9 +3298,19 @@ "\ distinct xs; i < length xs; j < length xs \ \ (xs!i = xs!j) = (i = j)" by(auto simp: distinct_conv_nth) +lemma distinct_Ex1: + "distinct xs \ x \ set xs \ (\!i. i < length xs \ xs ! i = x)" + by (auto simp: in_set_conv_nth nth_eq_iff_index_eq) + lemma inj_on_nth: "distinct xs \ \i \ I. i < length xs \ inj_on (nth xs) I" by (rule inj_onI) (simp add: nth_eq_iff_index_eq) +lemma bij_betw_nth: + assumes "distinct xs" "A = {.. distinct xs; n < length xs \ \ 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" "(\x. x \ set xs \ 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) = (\x\set xs. set (f x))" + by (induction xs) simp_all + subsection \Transfer\