# HG changeset patch # User haftmann # Date 1616662335 0 # Node ID 1d8a79aa2a99cd24f37df4db25bec313b513e8bc # Parent 6b480efe1bc36355cad7bdaea59d546e3f240fc1 dedicated session for combinatorial material diff -r 6b480efe1bc3 -r 1d8a79aa2a99 CONTRIBUTORS --- a/CONTRIBUTORS Wed Mar 24 21:17:19 2021 +0100 +++ b/CONTRIBUTORS Thu Mar 25 08:52:15 2021 +0000 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* March 2021: Florian Haftmann + Dedicated session for combinatorics. + * March 2021: Simon Foster and Leo Freitas More symbol definitions for Z Notation: Isabelle fonts and LaTeX macros. diff -r 6b480efe1bc3 -r 1d8a79aa2a99 NEWS --- a/NEWS Wed Mar 24 21:17:19 2021 +0100 +++ b/NEWS Thu Mar 25 08:52:15 2021 +0000 @@ -61,13 +61,6 @@ more small lemmas. Some theorems that were stated awkwardly before were corrected. Minor INCOMPATIBILITY. -* Theory "Permutation" in HOL-Library has been renamed to the more -specific "List_Permutation". Note that most notions from that -theory are already present in theory "Permutations". INCOMPATIBILITY. - -* Lemma "permutes_induct" has been given stronger -hypotheses and named premises. INCOMPATIBILITY. - * Theorems "antisym" and "eq_iff" in class "order" have been renamed to "order.antisym" and "order.eq_iff", to coexist locally with "antisym" and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant @@ -79,6 +72,19 @@ INCOMPATIBILITY; note that for most applications less elementary lemmas exists. +* Dedicated session HOL-Combinatorics. INCOMPATIBILITY: theories +"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling", +"Multiset_Permutations" have been +moved there from session HOL-Library. See theory "Guide" for an +overview about existing material on basic combinatorics. + +* Theory "Permutation" in HOL-Library has been renamed to the more +specific "List_Permutation". Note that most notions from that +theory are already present in theory "Permutations". INCOMPATIBILITY. + +* Lemma "permutes_induct" has been given stronger +hypotheses and named premises. INCOMPATIBILITY. + *** ML *** diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Algebra/Cycles.thy --- a/src/HOL/Algebra/Cycles.thy Wed Mar 24 21:17:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,557 +0,0 @@ -(* Title: HOL/Algebra/Cycles.thy - Author: Paulo Emílio de Vilhena -*) - -theory Cycles - imports "HOL-Library.Permutations" "HOL-Library.FuncSet" -begin - -section \Cycles\ - -subsection \Definitions\ - -abbreviation cycle :: "'a list \ bool" - where "cycle cs \ distinct cs" - -fun cycle_of_list :: "'a list \ 'a \ 'a" - where - "cycle_of_list (i # j # cs) = (Fun.swap i j id) \ (cycle_of_list (j # cs))" - | "cycle_of_list cs = id" - - -subsection \Basic Properties\ - -text \We start proving that the function derived from a cycle rotates its support list.\ - -lemma id_outside_supp: - assumes "x \ set cs" shows "(cycle_of_list cs) x = x" - using assms by (induct cs rule: cycle_of_list.induct) (simp_all) - -lemma permutation_of_cycle: "permutation (cycle_of_list cs)" -proof (induct cs rule: cycle_of_list.induct) - case 1 thus ?case - using permutation_compose[OF permutation_swap_id] unfolding comp_apply by simp -qed simp_all - -lemma cycle_permutes: "(cycle_of_list cs) permutes (set cs)" - using permutation_bijective[OF permutation_of_cycle] id_outside_supp[of _ cs] - by (simp add: bij_iff permutes_def) - -theorem cyclic_rotation: - assumes "cycle cs" shows "map ((cycle_of_list cs) ^^ n) cs = rotate n cs" -proof - - { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1) - proof (induction cs rule: cycle_of_list.induct) - case (1 i j cs) thus ?case - proof (cases) - assume "cs = Nil" thus ?thesis by simp - next - assume "cs \ Nil" hence ge_two: "length (j # cs) \ 2" - using not_less by auto - have "map (cycle_of_list (i # j # cs)) (i # j # cs) = - map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp - also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))" - by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) - also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp - also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp - also have " ... = j # cs @ [i]" - by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq) - also have " ... = rotate1 (i # j # cs)" by simp - finally show ?thesis . - qed - qed simp_all } - note cyclic_rotation' = this - - show ?thesis - using cyclic_rotation' by (induct n) (auto, metis map_map rotate1_rotate_swap rotate_map) -qed - -corollary cycle_is_surj: - assumes "cycle cs" shows "(cycle_of_list cs) ` (set cs) = (set cs)" - using cyclic_rotation[OF assms, of "Suc 0"] by (simp add: image_set) - -corollary cycle_is_id_root: - assumes "cycle cs" shows "(cycle_of_list cs) ^^ (length cs) = id" -proof - - have "map ((cycle_of_list cs) ^^ (length cs)) cs = cs" - unfolding cyclic_rotation[OF assms] by simp - hence "((cycle_of_list cs) ^^ (length cs)) i = i" if "i \ set cs" for i - using that map_eq_conv by fastforce - moreover have "((cycle_of_list cs) ^^ n) i = i" if "i \ set cs" for i n - using id_outside_supp[OF that] by (induct n) (simp_all) - ultimately show ?thesis - by fastforce -qed - -corollary cycle_of_list_rotate_independent: - assumes "cycle cs" shows "(cycle_of_list cs) = (cycle_of_list (rotate n cs))" -proof - - { fix cs :: "'a list" assume cs: "cycle cs" - have "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" - proof - - from cs have rotate1_cs: "cycle (rotate1 cs)" by simp - hence "map (cycle_of_list (rotate1 cs)) (rotate1 cs) = (rotate 2 cs)" - using cyclic_rotation[OF rotate1_cs, of 1] by (simp add: numeral_2_eq_2) - moreover have "map (cycle_of_list cs) (rotate1 cs) = (rotate 2 cs)" - using cyclic_rotation[OF cs] - by (metis One_nat_def Suc_1 funpow.simps(2) id_apply map_map rotate0 rotate_Suc) - ultimately have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i \ set cs" for i - using that map_eq_conv unfolding sym[OF set_rotate1[of cs]] by fastforce - moreover have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i \ set cs" for i - using that by (simp add: id_outside_supp) - ultimately show "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" - by blast - qed } note rotate1_lemma = this - - show ?thesis - using rotate1_lemma[of "rotate n cs"] by (induct n) (auto, metis assms distinct_rotate rotate1_lemma) -qed - - -subsection\Conjugation of cycles\ - -lemma conjugation_of_cycle: - assumes "cycle cs" and "bij p" - shows "p \ (cycle_of_list cs) \ (inv p) = cycle_of_list (map p cs)" - using assms -proof (induction cs rule: cycle_of_list.induct) - case (1 i j cs) - have "p \ cycle_of_list (i # j # cs) \ inv p = - (p \ (Fun.swap i j id) \ inv p) \ (p \ cycle_of_list (j # cs) \ inv p)" - by (simp add: assms(2) bij_is_inj fun.map_comp) - also have " ... = (Fun.swap (p i) (p j) id) \ (p \ cycle_of_list (j # cs) \ inv p)" - by (simp add: "1.prems"(2) bij_is_inj bij_swap_comp comp_swap o_assoc) - finally have "p \ cycle_of_list (i # j # cs) \ inv p = - (Fun.swap (p i) (p j) id) \ (cycle_of_list (map p (j # cs)))" - using "1.IH" "1.prems"(1) assms(2) by fastforce - thus ?case by (metis cycle_of_list.simps(1) list.simps(9)) -next - case "2_1" thus ?case - by (metis bij_is_surj comp_id cycle_of_list.simps(2) list.simps(8) surj_iff) -next - case "2_2" thus ?case - by (metis bij_is_surj comp_id cycle_of_list.simps(3) list.simps(8) list.simps(9) surj_iff) -qed - - -subsection\When Cycles Commute\ - -lemma cycles_commute: - assumes "cycle p" "cycle q" and "set p \ set q = {}" - shows "(cycle_of_list p) \ (cycle_of_list q) = (cycle_of_list q) \ (cycle_of_list p)" -proof - { fix p :: "'a list" and q :: "'a list" and i :: "'a" - assume A: "cycle p" "cycle q" "set p \ set q = {}" "i \ set p" "i \ set q" - have "((cycle_of_list p) \ (cycle_of_list q)) i = - ((cycle_of_list q) \ (cycle_of_list p)) i" - proof - - have "((cycle_of_list p) \ (cycle_of_list q)) i = (cycle_of_list p) i" - using id_outside_supp[OF A(5)] by simp - also have " ... = ((cycle_of_list q) \ (cycle_of_list p)) i" - using id_outside_supp[of "(cycle_of_list p) i"] cycle_is_surj[OF A(1)] A(3,4) by fastforce - finally show ?thesis . - qed } note aui_lemma = this - - fix i consider "i \ set p" "i \ set q" | "i \ set p" "i \ set q" | "i \ set p" "i \ set q" - using \set p \ set q = {}\ by blast - thus "((cycle_of_list p) \ (cycle_of_list q)) i = ((cycle_of_list q) \ (cycle_of_list p)) i" - proof cases - case 1 thus ?thesis - using aui_lemma[OF assms] by simp - next - case 2 thus ?thesis - using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps) - next - case 3 thus ?thesis - by (simp add: id_outside_supp) - qed -qed - - -subsection \Cycles from Permutations\ - -subsubsection \Exponentiation of permutations\ - -text \Some important properties of permutations before defining how to extract its cycles.\ - -lemma permutation_funpow: - assumes "permutation p" shows "permutation (p ^^ n)" - using assms by (induct n) (simp_all add: permutation_compose) - -lemma permutes_funpow: - assumes "p permutes S" shows "(p ^^ n) permutes S" - using assms by (induct n) (simp add: permutes_def, metis funpow_Suc_right permutes_compose) - -lemma funpow_diff: - assumes "inj p" and "i \ j" "(p ^^ i) a = (p ^^ j) a" shows "(p ^^ (j - i)) a = a" -proof - - have "(p ^^ i) ((p ^^ (j - i)) a) = (p ^^ i) a" - using assms(2-3) by (metis (no_types) add_diff_inverse_nat funpow_add not_le o_def) - thus ?thesis - unfolding inj_eq[OF inj_fn[OF assms(1)], of i] . -qed - -lemma permutation_is_nilpotent: - assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > 0" -proof - - obtain S where "finite S" and "p permutes S" - using assms unfolding permutation_permutes by blast - hence "\n. (p ^^ n) = id \ n > 0" - proof (induct S arbitrary: p) - case empty thus ?case - using id_funpow[of 1] unfolding permutes_empty by blast - next - case (insert s S) - have "(\n. (p ^^ n) s) ` UNIV \ (insert s S)" - using permutes_in_image[OF permutes_funpow[OF insert(4)], of _ s] by auto - hence "\ inj_on (\n. (p ^^ n) s) UNIV" - using insert(1) infinite_iff_countable_subset unfolding sym[OF finite_insert, of S s] by metis - then obtain i j where ij: "i < j" "(p ^^ i) s = (p ^^ j) s" - unfolding inj_on_def by (metis nat_neq_iff) - hence "(p ^^ (j - i)) s = s" - using funpow_diff[OF permutes_inj[OF insert(4)]] le_eq_less_or_eq by blast - hence "p ^^ (j - i) permutes S" - using permutes_superset[OF permutes_funpow[OF insert(4), of "j - i"], of S] by auto - then obtain n where n: "((p ^^ (j - i)) ^^ n) = id" "n > 0" - using insert(3) by blast - thus ?case - using ij(1) nat_0_less_mult_iff zero_less_diff unfolding funpow_mult by metis - qed - thus thesis - using that by blast -qed - -lemma permutation_is_nilpotent': - assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > m" -proof - - obtain n where "(p ^^ n) = id" and "n > 0" - using permutation_is_nilpotent[OF assms] by blast - then obtain k where "n * k > m" - by (metis dividend_less_times_div mult_Suc_right) - from \(p ^^ n) = id\ have "p ^^ (n * k) = id" - by (induct k) (simp, metis funpow_mult id_funpow) - with \n * k > m\ show thesis - using that by blast -qed - - -subsubsection \Extraction of cycles from permutations\ - -definition least_power :: "('a \ 'a) \ 'a \ nat" - where "least_power f x = (LEAST n. (f ^^ n) x = x \ n > 0)" - -abbreviation support :: "('a \ 'a) \ 'a \ 'a list" - where "support p x \ map (\i. (p ^^ i) x) [0..< (least_power p x)]" - - -lemma least_powerI: - assumes "(f ^^ n) x = x" and "n > 0" - shows "(f ^^ (least_power f x)) x = x" and "least_power f x > 0" - using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ - -lemma least_power_le: - assumes "(f ^^ n) x = x" and "n > 0" shows "least_power f x \ n" - using assms unfolding least_power_def by (simp add: Least_le) - -lemma least_power_of_permutation: - assumes "permutation p" shows "(p ^^ (least_power p a)) a = a" and "least_power p a > 0" - using permutation_is_nilpotent[OF assms] least_powerI by (metis id_apply)+ - -lemma least_power_gt_one: - assumes "permutation p" and "p a \ a" shows "least_power p a > Suc 0" - using least_power_of_permutation[OF assms(1)] assms(2) - by (metis Suc_lessI funpow.simps(2) funpow_simps_right(1) o_id) - -lemma least_power_minimal: - assumes "(p ^^ n) a = a" shows "(least_power p a) dvd n" -proof (cases "n = 0", simp) - let ?lpow = "least_power p" - - assume "n \ 0" then have "n > 0" by simp - hence "(p ^^ (?lpow a)) a = a" and "least_power p a > 0" - using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ - hence aux_lemma: "(p ^^ ((?lpow a) * k)) a = a" for k :: nat - by (induct k) (simp_all add: funpow_add) - - have "(p ^^ (n mod ?lpow a)) ((p ^^ (n - (n mod ?lpow a))) a) = (p ^^ n) a" - by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_less o_apply) - with \(p ^^ n) a = a\ have "(p ^^ (n mod ?lpow a)) a = a" - using aux_lemma by (simp add: minus_mod_eq_mult_div) - hence "?lpow a \ n mod ?lpow a" if "n mod ?lpow a > 0" - using least_power_le[OF _ that, of p a] by simp - with \least_power p a > 0\ show "(least_power p a) dvd n" - using mod_less_divisor not_le by blast -qed - -lemma least_power_dvd: - assumes "permutation p" shows "(least_power p a) dvd n \ (p ^^ n) a = a" -proof - show "(p ^^ n) a = a \ (least_power p a) dvd n" - using least_power_minimal[of _ p] by simp -next - have "(p ^^ ((least_power p a) * k)) a = a" for k :: nat - using least_power_of_permutation(1)[OF assms(1)] by (induct k) (simp_all add: funpow_add) - thus "(least_power p a) dvd n \ (p ^^ n) a = a" by blast -qed - -theorem cycle_of_permutation: - assumes "permutation p" shows "cycle (support p a)" -proof - - have "(least_power p a) dvd (j - i)" if "i \ j" "j < least_power p a" and "(p ^^ i) a = (p ^^ j) a" for i j - using funpow_diff[OF bij_is_inj that(1,3)] assms by (simp add: permutation least_power_dvd) - moreover have "i = j" if "i \ j" "j < least_power p a" and "(least_power p a) dvd (j - i)" for i j - using that le_eq_less_or_eq nat_dvd_not_less by auto - ultimately have "inj_on (\i. (p ^^ i) a) {..< (least_power p a)}" - unfolding inj_on_def by (metis le_cases lessThan_iff) - thus ?thesis - by (simp add: atLeast_upt distinct_map) -qed - - -subsection \Decomposition on Cycles\ - -text \We show that a permutation can be decomposed on cycles\ - -subsubsection \Preliminaries\ - -lemma support_set: - assumes "permutation p" shows "set (support p a) = range (\i. (p ^^ i) a)" -proof - show "set (support p a) \ range (\i. (p ^^ i) a)" - by auto -next - show "range (\i. (p ^^ i) a) \ set (support p a)" - proof (auto) - fix i - have "(p ^^ i) a = (p ^^ (i mod (least_power p a))) ((p ^^ (i - (i mod (least_power p a)))) a)" - by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_le o_apply) - also have " ... = (p ^^ (i mod (least_power p a))) a" - using least_power_dvd[OF assms] by (metis dvd_minus_mod) - also have " ... \ (\i. (p ^^ i) a) ` {0..< (least_power p a)}" - using least_power_of_permutation(2)[OF assms] by fastforce - finally show "(p ^^ i) a \ (\i. (p ^^ i) a) ` {0..< (least_power p a)}" . - qed -qed - -lemma disjoint_support: - assumes "permutation p" shows "disjoint (range (\a. set (support p a)))" (is "disjoint ?A") -proof (rule disjointI) - { fix i j a b - assume "set (support p a) \ set (support p b) \ {}" have "set (support p a) \ set (support p b)" - unfolding support_set[OF assms] - proof (auto) - from \set (support p a) \ set (support p b) \ {}\ - obtain i j where ij: "(p ^^ i) a = (p ^^ j) b" - by auto - - fix k - have "(p ^^ k) a = (p ^^ (k + (least_power p a) * l)) a" for l - using least_power_dvd[OF assms] by (induct l) (simp, metis dvd_triv_left funpow_add o_def) - then obtain m where "m \ i" and "(p ^^ m) a = (p ^^ k) a" - using least_power_of_permutation(2)[OF assms] - by (metis dividend_less_times_div le_eq_less_or_eq mult_Suc_right trans_less_add2) - hence "(p ^^ m) a = (p ^^ (m - i)) ((p ^^ i) a)" - by (metis Nat.le_imp_diff_is_add funpow_add o_apply) - with \(p ^^ m) a = (p ^^ k) a\ have "(p ^^ k) a = (p ^^ ((m - i) + j)) b" - unfolding ij by (simp add: funpow_add) - thus "(p ^^ k) a \ range (\i. (p ^^ i) b)" - by blast - qed } note aux_lemma = this - - fix supp_a supp_b - assume "supp_a \ ?A" and "supp_b \ ?A" - then obtain a b where a: "supp_a = set (support p a)" and b: "supp_b = set (support p b)" - by auto - assume "supp_a \ supp_b" thus "supp_a \ supp_b = {}" - using aux_lemma unfolding a b by blast -qed - -lemma disjoint_support': - assumes "permutation p" - shows "set (support p a) \ set (support p b) = {} \ a \ set (support p b)" -proof - - have "a \ set (support p a)" - using least_power_of_permutation(2)[OF assms] by force - show ?thesis - proof - assume "set (support p a) \ set (support p b) = {}" - with \a \ set (support p a)\ show "a \ set (support p b)" - by blast - next - assume "a \ set (support p b)" show "set (support p a) \ set (support p b) = {}" - proof (rule ccontr) - assume "set (support p a) \ set (support p b) \ {}" - hence "set (support p a) = set (support p b)" - using disjoint_support[OF assms] by (meson UNIV_I disjoint_def image_iff) - with \a \ set (support p a)\ and \a \ set (support p b)\ show False - by simp - qed - qed -qed - -lemma support_coverture: - assumes "permutation p" shows "\ { set (support p a) | a. p a \ a } = { a. p a \ a }" -proof - show "{ a. p a \ a } \ \ { set (support p a) | a. p a \ a }" - proof - fix a assume "a \ { a. p a \ a }" - have "a \ set (support p a)" - using least_power_of_permutation(2)[OF assms, of a] by force - with \a \ { a. p a \ a }\ show "a \ \ { set (support p a) | a. p a \ a }" - by blast - qed -next - show "\ { set (support p a) | a. p a \ a } \ { a. p a \ a }" - proof - fix b assume "b \ \ { set (support p a) | a. p a \ a }" - then obtain a i where "p a \ a" and "(p ^^ i) a = b" - by auto - have "p a = a" if "(p ^^ i) a = (p ^^ Suc i) a" - using funpow_diff[OF bij_is_inj _ that] assms unfolding permutation by simp - with \p a \ a\ and \(p ^^ i) a = b\ show "b \ { a. p a \ a }" - by auto - qed -qed - -theorem cycle_restrict: - assumes "permutation p" and "b \ set (support p a)" shows "p b = (cycle_of_list (support p a)) b" -proof - - note least_power_props [simp] = least_power_of_permutation[OF assms(1)] - - have "map (cycle_of_list (support p a)) (support p a) = rotate1 (support p a)" - using cyclic_rotation[OF cycle_of_permutation[OF assms(1)], of 1 a] by simp - hence "map (cycle_of_list (support p a)) (support p a) = tl (support p a) @ [ a ]" - by (simp add: hd_map rotate1_hd_tl) - also have " ... = map p (support p a)" - proof (rule nth_equalityI, auto) - fix i assume "i < least_power p a" show "(tl (support p a) @ [a]) ! i = p ((p ^^ i) a)" - proof (cases) - assume i: "i = least_power p a - 1" - hence "(tl (support p a) @ [ a ]) ! i = a" - by (metis (no_types, lifting) diff_zero length_map length_tl length_upt nth_append_length) - also have " ... = p ((p ^^ i) a)" - by (metis (mono_tags, hide_lams) least_power_props i Suc_diff_1 funpow_simps_right(2) funpow_swap1 o_apply) - finally show ?thesis . - next - assume "i \ least_power p a - 1" - with \i < least_power p a\ have "i < least_power p a - 1" - by simp - hence "(tl (support p a) @ [ a ]) ! i = (p ^^ (Suc i)) a" - by (metis One_nat_def Suc_eq_plus1 add.commute length_map length_upt map_tl nth_append nth_map_upt tl_upt) - thus ?thesis - by simp - qed - qed - finally have "map (cycle_of_list (support p a)) (support p a) = map p (support p a)" . - thus ?thesis - using assms(2) by auto -qed - - -subsubsection\Decomposition\ - -inductive cycle_decomp :: "'a set \ ('a \ 'a) \ bool" - where - empty: "cycle_decomp {} id" - | comp: "\ cycle_decomp I p; cycle cs; set cs \ I = {} \ \ - cycle_decomp (set cs \ I) ((cycle_of_list cs) \ p)" - - -lemma semidecomposition: - assumes "p permutes S" and "finite S" - shows "(\y. if y \ (S - set (support p a)) then p y else y) permutes (S - set (support p a))" -proof (rule bij_imp_permutes) - show "(if b \ (S - set (support p a)) then p b else b) = b" if "b \ S - set (support p a)" for b - using that by auto -next - have is_permutation: "permutation p" - using assms unfolding permutation_permutes by blast - - let ?q = "\y. if y \ (S - set (support p a)) then p y else y" - show "bij_betw ?q (S - set (support p a)) (S - set (support p a))" - proof (rule bij_betw_imageI) - show "inj_on ?q (S - set (support p a))" - using permutes_inj[OF assms(1)] unfolding inj_on_def by auto - next - have aux_lemma: "set (support p s) \ (S - set (support p a))" if "s \ S - set (support p a)" for s - proof - - have "(p ^^ i) s \ S" for i - using that unfolding permutes_in_image[OF permutes_funpow[OF assms(1)]] by simp - thus ?thesis - using that disjoint_support'[OF is_permutation, of s a] by auto - qed - have "(p ^^ 1) s \ set (support p s)" for s - unfolding support_set[OF is_permutation] by blast - hence "p s \ set (support p s)" for s - by simp - hence "p ` (S - set (support p a)) \ S - set (support p a)" - using aux_lemma by blast - moreover have "(p ^^ ((least_power p s) - 1)) s \ set (support p s)" for s - unfolding support_set[OF is_permutation] by blast - hence "\s' \ set (support p s). p s' = s" for s - using least_power_of_permutation[OF is_permutation] by (metis Suc_diff_1 funpow.simps(2) o_apply) - hence "S - set (support p a) \ p ` (S - set (support p a))" - using aux_lemma - by (clarsimp simp add: image_iff) (metis image_subset_iff) - ultimately show "?q ` (S - set (support p a)) = (S - set (support p a))" - by auto - qed -qed - -theorem cycle_decomposition: - assumes "p permutes S" and "finite S" shows "cycle_decomp S p" - using assms -proof(induct "card S" arbitrary: S p rule: less_induct) - case less show ?case - proof (cases) - assume "S = {}" thus ?thesis - using empty less(2) by auto - next - have is_permutation: "permutation p" - using less(2-3) unfolding permutation_permutes by blast - - assume "S \ {}" then obtain s where "s \ S" - by blast - define q where "q = (\y. if y \ (S - set (support p s)) then p y else y)" - have "(cycle_of_list (support p s) \ q) = p" - proof - fix a - consider "a \ S - set (support p s)" | "a \ set (support p s)" | "a \ S" "a \ set (support p s)" - by blast - thus "((cycle_of_list (support p s) \ q)) a = p a" - proof cases - case 1 - have "(p ^^ 1) a \ set (support p a)" - unfolding support_set[OF is_permutation] by blast - with \a \ S - set (support p s)\ have "p a \ set (support p s)" - using disjoint_support'[OF is_permutation, of a s] by auto - with \a \ S - set (support p s)\ show ?thesis - using id_outside_supp[of _ "support p s"] unfolding q_def by simp - next - case 2 thus ?thesis - using cycle_restrict[OF is_permutation] unfolding q_def by simp - next - case 3 thus ?thesis - using id_outside_supp[OF 3(2)] less(2) permutes_not_in unfolding q_def by fastforce - qed - qed - - moreover from \s \ S\ have "(p ^^ i) s \ S" for i - unfolding permutes_in_image[OF permutes_funpow[OF less(2)]] . - hence "set (support p s) \ (S - set (support p s)) = S" - by auto - - moreover have "s \ set (support p s)" - using least_power_of_permutation[OF is_permutation] by force - with \s \ S\ have "card (S - set (support p s)) < card S" - using less(3) by (metis DiffE card_seteq linorder_not_le subsetI) - hence "cycle_decomp (S - set (support p s)) q" - using less(1)[OF _ semidecomposition[OF less(2-3)], of s] less(3) unfolding q_def by blast - - moreover show ?thesis - using comp[OF calculation(3) cycle_of_permutation[OF is_permutation], of s] - unfolding calculation(1-2) by blast - qed -qed - -end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Thu Mar 25 08:52:15 2021 +0000 @@ -6,7 +6,7 @@ section \Divisibility in monoids and rings\ theory Divisibility - imports "HOL-Library.List_Permutation" Coset Group + imports "HOL-Combinatorics.List_Permutation" Coset Group begin section \Factorial Monoids\ diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Algebra/Sym_Groups.thy --- a/src/HOL/Algebra/Sym_Groups.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Algebra/Sym_Groups.thy Thu Mar 25 08:52:15 2021 +0000 @@ -3,8 +3,9 @@ *) theory Sym_Groups - imports Cycles Solvable_Groups - + imports + "HOL-Combinatorics.Cycles" + Solvable_Groups begin section \Symmetric Groups\ @@ -169,8 +170,20 @@ using assms empty by (induct set: "finite", fastforce, simp add: single) lemma swapidseq_ext_imp_swapidseq: - assumes "swapidseq_ext S n p" shows "swapidseq n p" - using assms by (induction, simp, simp, meson comp_Suc) + \swapidseq n p\ if \swapidseq_ext S n p\ +using that proof induction + case empty + then show ?case + by (simp add: fun_eq_iff) +next + case (single S n p a) + then show ?case by simp +next + case (comp S n p a b) + then have \swapidseq (Suc n) (Fun.swap a b id \ p)\ + by (simp add: comp_Suc) + then show ?case by (simp add: comp_def) +qed lemma swapidseq_ext_zero_imp_id: assumes "swapidseq_ext S 0 p" shows "p = id" diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Analysis/Determinants.thy --- a/src/HOL/Analysis/Determinants.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Analysis/Determinants.thy Thu Mar 25 08:52:15 2021 +0000 @@ -6,8 +6,8 @@ theory Determinants imports + "HOL-Combinatorics.Permutations" Cartesian_Space - "HOL-Library.Permutations" begin subsection \Trace\ diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Analysis/Vitali_Covering_Theorem.thy --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy Thu Mar 25 08:52:15 2021 +0000 @@ -5,8 +5,9 @@ section \Vitali Covering Theorem and an Application to Negligibility\ theory Vitali_Covering_Theorem - imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Permutations" - +imports + "HOL-Combinatorics.Permutations" + Equivalence_Lebesgue_Henstock_Integration begin lemma stretch_Galois: diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Mar 25 08:52:15 2021 +0000 @@ -29,17 +29,15 @@ Euclidean_Algorithm.Lcm "Gcd :: _ poly set \ _" "Lcm :: _ poly set \ _" - permutations_of_set - permutations_of_multiset ]] text \ If code generation fails with a message like \"List.set" is not a constructor, on left hand side of equation: ...\, - feel free to add an RBT implementation for the corrsponding operation - of delete that code equation (see above). + feel free to add an RBT implementation for the corresponding operation + or delete that code equation (see above). \ - + export_code _ checking SML OCaml? Haskell? Scala end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/Combinatorics.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/Combinatorics.thy Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,13 @@ + +section \Basic combinatorics in Isabelle/HOL (and the Archive of Formal Proofs)\ + +theory Combinatorics +imports + Stirling + Permutations + List_Permutation + Multiset_Permutations + Cycles +begin + +end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/Cycles.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/Cycles.thy Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,556 @@ +(* Author: Paulo Emílio de Vilhena +*) + +theory Cycles + imports "HOL-Library.FuncSet" Permutations +begin + +section \Cycles\ + +subsection \Definitions\ + +abbreviation cycle :: "'a list \ bool" + where "cycle cs \ distinct cs" + +fun cycle_of_list :: "'a list \ 'a \ 'a" + where + "cycle_of_list (i # j # cs) = (Fun.swap i j id) \ (cycle_of_list (j # cs))" + | "cycle_of_list cs = id" + + +subsection \Basic Properties\ + +text \We start proving that the function derived from a cycle rotates its support list.\ + +lemma id_outside_supp: + assumes "x \ set cs" shows "(cycle_of_list cs) x = x" + using assms by (induct cs rule: cycle_of_list.induct) (simp_all) + +lemma permutation_of_cycle: "permutation (cycle_of_list cs)" +proof (induct cs rule: cycle_of_list.induct) + case 1 thus ?case + using permutation_compose[OF permutation_swap_id] unfolding comp_apply by simp +qed simp_all + +lemma cycle_permutes: "(cycle_of_list cs) permutes (set cs)" + using permutation_bijective[OF permutation_of_cycle] id_outside_supp[of _ cs] + by (simp add: bij_iff permutes_def) + +theorem cyclic_rotation: + assumes "cycle cs" shows "map ((cycle_of_list cs) ^^ n) cs = rotate n cs" +proof - + { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1) + proof (induction cs rule: cycle_of_list.induct) + case (1 i j cs) thus ?case + proof (cases) + assume "cs = Nil" thus ?thesis by simp + next + assume "cs \ Nil" hence ge_two: "length (j # cs) \ 2" + using not_less by auto + have "map (cycle_of_list (i # j # cs)) (i # j # cs) = + map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp + also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))" + by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) + also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp + also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp + also have " ... = j # cs @ [i]" + by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq) + also have " ... = rotate1 (i # j # cs)" by simp + finally show ?thesis . + qed + qed simp_all } + note cyclic_rotation' = this + + show ?thesis + using cyclic_rotation' by (induct n) (auto, metis map_map rotate1_rotate_swap rotate_map) +qed + +corollary cycle_is_surj: + assumes "cycle cs" shows "(cycle_of_list cs) ` (set cs) = (set cs)" + using cyclic_rotation[OF assms, of "Suc 0"] by (simp add: image_set) + +corollary cycle_is_id_root: + assumes "cycle cs" shows "(cycle_of_list cs) ^^ (length cs) = id" +proof - + have "map ((cycle_of_list cs) ^^ (length cs)) cs = cs" + unfolding cyclic_rotation[OF assms] by simp + hence "((cycle_of_list cs) ^^ (length cs)) i = i" if "i \ set cs" for i + using that map_eq_conv by fastforce + moreover have "((cycle_of_list cs) ^^ n) i = i" if "i \ set cs" for i n + using id_outside_supp[OF that] by (induct n) (simp_all) + ultimately show ?thesis + by fastforce +qed + +corollary cycle_of_list_rotate_independent: + assumes "cycle cs" shows "(cycle_of_list cs) = (cycle_of_list (rotate n cs))" +proof - + { fix cs :: "'a list" assume cs: "cycle cs" + have "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" + proof - + from cs have rotate1_cs: "cycle (rotate1 cs)" by simp + hence "map (cycle_of_list (rotate1 cs)) (rotate1 cs) = (rotate 2 cs)" + using cyclic_rotation[OF rotate1_cs, of 1] by (simp add: numeral_2_eq_2) + moreover have "map (cycle_of_list cs) (rotate1 cs) = (rotate 2 cs)" + using cyclic_rotation[OF cs] + by (metis One_nat_def Suc_1 funpow.simps(2) id_apply map_map rotate0 rotate_Suc) + ultimately have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i \ set cs" for i + using that map_eq_conv unfolding sym[OF set_rotate1[of cs]] by fastforce + moreover have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i \ set cs" for i + using that by (simp add: id_outside_supp) + ultimately show "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" + by blast + qed } note rotate1_lemma = this + + show ?thesis + using rotate1_lemma[of "rotate n cs"] by (induct n) (auto, metis assms distinct_rotate rotate1_lemma) +qed + + +subsection\Conjugation of cycles\ + +lemma conjugation_of_cycle: + assumes "cycle cs" and "bij p" + shows "p \ (cycle_of_list cs) \ (inv p) = cycle_of_list (map p cs)" + using assms +proof (induction cs rule: cycle_of_list.induct) + case (1 i j cs) + have "p \ cycle_of_list (i # j # cs) \ inv p = + (p \ (Fun.swap i j id) \ inv p) \ (p \ cycle_of_list (j # cs) \ inv p)" + by (simp add: assms(2) bij_is_inj fun.map_comp) + also have " ... = (Fun.swap (p i) (p j) id) \ (p \ cycle_of_list (j # cs) \ inv p)" + by (simp add: "1.prems"(2) bij_is_inj bij_swap_comp comp_swap o_assoc) + finally have "p \ cycle_of_list (i # j # cs) \ inv p = + (Fun.swap (p i) (p j) id) \ (cycle_of_list (map p (j # cs)))" + using "1.IH" "1.prems"(1) assms(2) by fastforce + thus ?case by (metis cycle_of_list.simps(1) list.simps(9)) +next + case "2_1" thus ?case + by (metis bij_is_surj comp_id cycle_of_list.simps(2) list.simps(8) surj_iff) +next + case "2_2" thus ?case + by (metis bij_is_surj comp_id cycle_of_list.simps(3) list.simps(8) list.simps(9) surj_iff) +qed + + +subsection\When Cycles Commute\ + +lemma cycles_commute: + assumes "cycle p" "cycle q" and "set p \ set q = {}" + shows "(cycle_of_list p) \ (cycle_of_list q) = (cycle_of_list q) \ (cycle_of_list p)" +proof + { fix p :: "'a list" and q :: "'a list" and i :: "'a" + assume A: "cycle p" "cycle q" "set p \ set q = {}" "i \ set p" "i \ set q" + have "((cycle_of_list p) \ (cycle_of_list q)) i = + ((cycle_of_list q) \ (cycle_of_list p)) i" + proof - + have "((cycle_of_list p) \ (cycle_of_list q)) i = (cycle_of_list p) i" + using id_outside_supp[OF A(5)] by simp + also have " ... = ((cycle_of_list q) \ (cycle_of_list p)) i" + using id_outside_supp[of "(cycle_of_list p) i"] cycle_is_surj[OF A(1)] A(3,4) by fastforce + finally show ?thesis . + qed } note aui_lemma = this + + fix i consider "i \ set p" "i \ set q" | "i \ set p" "i \ set q" | "i \ set p" "i \ set q" + using \set p \ set q = {}\ by blast + thus "((cycle_of_list p) \ (cycle_of_list q)) i = ((cycle_of_list q) \ (cycle_of_list p)) i" + proof cases + case 1 thus ?thesis + using aui_lemma[OF assms] by simp + next + case 2 thus ?thesis + using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps) + next + case 3 thus ?thesis + by (simp add: id_outside_supp) + qed +qed + + +subsection \Cycles from Permutations\ + +subsubsection \Exponentiation of permutations\ + +text \Some important properties of permutations before defining how to extract its cycles.\ + +lemma permutation_funpow: + assumes "permutation p" shows "permutation (p ^^ n)" + using assms by (induct n) (simp_all add: permutation_compose) + +lemma permutes_funpow: + assumes "p permutes S" shows "(p ^^ n) permutes S" + using assms by (induct n) (simp add: permutes_def, metis funpow_Suc_right permutes_compose) + +lemma funpow_diff: + assumes "inj p" and "i \ j" "(p ^^ i) a = (p ^^ j) a" shows "(p ^^ (j - i)) a = a" +proof - + have "(p ^^ i) ((p ^^ (j - i)) a) = (p ^^ i) a" + using assms(2-3) by (metis (no_types) add_diff_inverse_nat funpow_add not_le o_def) + thus ?thesis + unfolding inj_eq[OF inj_fn[OF assms(1)], of i] . +qed + +lemma permutation_is_nilpotent: + assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > 0" +proof - + obtain S where "finite S" and "p permutes S" + using assms unfolding permutation_permutes by blast + hence "\n. (p ^^ n) = id \ n > 0" + proof (induct S arbitrary: p) + case empty thus ?case + using id_funpow[of 1] unfolding permutes_empty by blast + next + case (insert s S) + have "(\n. (p ^^ n) s) ` UNIV \ (insert s S)" + using permutes_in_image[OF permutes_funpow[OF insert(4)], of _ s] by auto + hence "\ inj_on (\n. (p ^^ n) s) UNIV" + using insert(1) infinite_iff_countable_subset unfolding sym[OF finite_insert, of S s] by metis + then obtain i j where ij: "i < j" "(p ^^ i) s = (p ^^ j) s" + unfolding inj_on_def by (metis nat_neq_iff) + hence "(p ^^ (j - i)) s = s" + using funpow_diff[OF permutes_inj[OF insert(4)]] le_eq_less_or_eq by blast + hence "p ^^ (j - i) permutes S" + using permutes_superset[OF permutes_funpow[OF insert(4), of "j - i"], of S] by auto + then obtain n where n: "((p ^^ (j - i)) ^^ n) = id" "n > 0" + using insert(3) by blast + thus ?case + using ij(1) nat_0_less_mult_iff zero_less_diff unfolding funpow_mult by metis + qed + thus thesis + using that by blast +qed + +lemma permutation_is_nilpotent': + assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > m" +proof - + obtain n where "(p ^^ n) = id" and "n > 0" + using permutation_is_nilpotent[OF assms] by blast + then obtain k where "n * k > m" + by (metis dividend_less_times_div mult_Suc_right) + from \(p ^^ n) = id\ have "p ^^ (n * k) = id" + by (induct k) (simp, metis funpow_mult id_funpow) + with \n * k > m\ show thesis + using that by blast +qed + + +subsubsection \Extraction of cycles from permutations\ + +definition least_power :: "('a \ 'a) \ 'a \ nat" + where "least_power f x = (LEAST n. (f ^^ n) x = x \ n > 0)" + +abbreviation support :: "('a \ 'a) \ 'a \ 'a list" + where "support p x \ map (\i. (p ^^ i) x) [0..< (least_power p x)]" + + +lemma least_powerI: + assumes "(f ^^ n) x = x" and "n > 0" + shows "(f ^^ (least_power f x)) x = x" and "least_power f x > 0" + using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ + +lemma least_power_le: + assumes "(f ^^ n) x = x" and "n > 0" shows "least_power f x \ n" + using assms unfolding least_power_def by (simp add: Least_le) + +lemma least_power_of_permutation: + assumes "permutation p" shows "(p ^^ (least_power p a)) a = a" and "least_power p a > 0" + using permutation_is_nilpotent[OF assms] least_powerI by (metis id_apply)+ + +lemma least_power_gt_one: + assumes "permutation p" and "p a \ a" shows "least_power p a > Suc 0" + using least_power_of_permutation[OF assms(1)] assms(2) + by (metis Suc_lessI funpow.simps(2) funpow_simps_right(1) o_id) + +lemma least_power_minimal: + assumes "(p ^^ n) a = a" shows "(least_power p a) dvd n" +proof (cases "n = 0", simp) + let ?lpow = "least_power p" + + assume "n \ 0" then have "n > 0" by simp + hence "(p ^^ (?lpow a)) a = a" and "least_power p a > 0" + using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ + hence aux_lemma: "(p ^^ ((?lpow a) * k)) a = a" for k :: nat + by (induct k) (simp_all add: funpow_add) + + have "(p ^^ (n mod ?lpow a)) ((p ^^ (n - (n mod ?lpow a))) a) = (p ^^ n) a" + by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_less o_apply) + with \(p ^^ n) a = a\ have "(p ^^ (n mod ?lpow a)) a = a" + using aux_lemma by (simp add: minus_mod_eq_mult_div) + hence "?lpow a \ n mod ?lpow a" if "n mod ?lpow a > 0" + using least_power_le[OF _ that, of p a] by simp + with \least_power p a > 0\ show "(least_power p a) dvd n" + using mod_less_divisor not_le by blast +qed + +lemma least_power_dvd: + assumes "permutation p" shows "(least_power p a) dvd n \ (p ^^ n) a = a" +proof + show "(p ^^ n) a = a \ (least_power p a) dvd n" + using least_power_minimal[of _ p] by simp +next + have "(p ^^ ((least_power p a) * k)) a = a" for k :: nat + using least_power_of_permutation(1)[OF assms(1)] by (induct k) (simp_all add: funpow_add) + thus "(least_power p a) dvd n \ (p ^^ n) a = a" by blast +qed + +theorem cycle_of_permutation: + assumes "permutation p" shows "cycle (support p a)" +proof - + have "(least_power p a) dvd (j - i)" if "i \ j" "j < least_power p a" and "(p ^^ i) a = (p ^^ j) a" for i j + using funpow_diff[OF bij_is_inj that(1,3)] assms by (simp add: permutation least_power_dvd) + moreover have "i = j" if "i \ j" "j < least_power p a" and "(least_power p a) dvd (j - i)" for i j + using that le_eq_less_or_eq nat_dvd_not_less by auto + ultimately have "inj_on (\i. (p ^^ i) a) {..< (least_power p a)}" + unfolding inj_on_def by (metis le_cases lessThan_iff) + thus ?thesis + by (simp add: atLeast_upt distinct_map) +qed + + +subsection \Decomposition on Cycles\ + +text \We show that a permutation can be decomposed on cycles\ + +subsubsection \Preliminaries\ + +lemma support_set: + assumes "permutation p" shows "set (support p a) = range (\i. (p ^^ i) a)" +proof + show "set (support p a) \ range (\i. (p ^^ i) a)" + by auto +next + show "range (\i. (p ^^ i) a) \ set (support p a)" + proof (auto) + fix i + have "(p ^^ i) a = (p ^^ (i mod (least_power p a))) ((p ^^ (i - (i mod (least_power p a)))) a)" + by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_le o_apply) + also have " ... = (p ^^ (i mod (least_power p a))) a" + using least_power_dvd[OF assms] by (metis dvd_minus_mod) + also have " ... \ (\i. (p ^^ i) a) ` {0..< (least_power p a)}" + using least_power_of_permutation(2)[OF assms] by fastforce + finally show "(p ^^ i) a \ (\i. (p ^^ i) a) ` {0..< (least_power p a)}" . + qed +qed + +lemma disjoint_support: + assumes "permutation p" shows "disjoint (range (\a. set (support p a)))" (is "disjoint ?A") +proof (rule disjointI) + { fix i j a b + assume "set (support p a) \ set (support p b) \ {}" have "set (support p a) \ set (support p b)" + unfolding support_set[OF assms] + proof (auto) + from \set (support p a) \ set (support p b) \ {}\ + obtain i j where ij: "(p ^^ i) a = (p ^^ j) b" + by auto + + fix k + have "(p ^^ k) a = (p ^^ (k + (least_power p a) * l)) a" for l + using least_power_dvd[OF assms] by (induct l) (simp, metis dvd_triv_left funpow_add o_def) + then obtain m where "m \ i" and "(p ^^ m) a = (p ^^ k) a" + using least_power_of_permutation(2)[OF assms] + by (metis dividend_less_times_div le_eq_less_or_eq mult_Suc_right trans_less_add2) + hence "(p ^^ m) a = (p ^^ (m - i)) ((p ^^ i) a)" + by (metis Nat.le_imp_diff_is_add funpow_add o_apply) + with \(p ^^ m) a = (p ^^ k) a\ have "(p ^^ k) a = (p ^^ ((m - i) + j)) b" + unfolding ij by (simp add: funpow_add) + thus "(p ^^ k) a \ range (\i. (p ^^ i) b)" + by blast + qed } note aux_lemma = this + + fix supp_a supp_b + assume "supp_a \ ?A" and "supp_b \ ?A" + then obtain a b where a: "supp_a = set (support p a)" and b: "supp_b = set (support p b)" + by auto + assume "supp_a \ supp_b" thus "supp_a \ supp_b = {}" + using aux_lemma unfolding a b by blast +qed + +lemma disjoint_support': + assumes "permutation p" + shows "set (support p a) \ set (support p b) = {} \ a \ set (support p b)" +proof - + have "a \ set (support p a)" + using least_power_of_permutation(2)[OF assms] by force + show ?thesis + proof + assume "set (support p a) \ set (support p b) = {}" + with \a \ set (support p a)\ show "a \ set (support p b)" + by blast + next + assume "a \ set (support p b)" show "set (support p a) \ set (support p b) = {}" + proof (rule ccontr) + assume "set (support p a) \ set (support p b) \ {}" + hence "set (support p a) = set (support p b)" + using disjoint_support[OF assms] by (meson UNIV_I disjoint_def image_iff) + with \a \ set (support p a)\ and \a \ set (support p b)\ show False + by simp + qed + qed +qed + +lemma support_coverture: + assumes "permutation p" shows "\ { set (support p a) | a. p a \ a } = { a. p a \ a }" +proof + show "{ a. p a \ a } \ \ { set (support p a) | a. p a \ a }" + proof + fix a assume "a \ { a. p a \ a }" + have "a \ set (support p a)" + using least_power_of_permutation(2)[OF assms, of a] by force + with \a \ { a. p a \ a }\ show "a \ \ { set (support p a) | a. p a \ a }" + by blast + qed +next + show "\ { set (support p a) | a. p a \ a } \ { a. p a \ a }" + proof + fix b assume "b \ \ { set (support p a) | a. p a \ a }" + then obtain a i where "p a \ a" and "(p ^^ i) a = b" + by auto + have "p a = a" if "(p ^^ i) a = (p ^^ Suc i) a" + using funpow_diff[OF bij_is_inj _ that] assms unfolding permutation by simp + with \p a \ a\ and \(p ^^ i) a = b\ show "b \ { a. p a \ a }" + by auto + qed +qed + +theorem cycle_restrict: + assumes "permutation p" and "b \ set (support p a)" shows "p b = (cycle_of_list (support p a)) b" +proof - + note least_power_props [simp] = least_power_of_permutation[OF assms(1)] + + have "map (cycle_of_list (support p a)) (support p a) = rotate1 (support p a)" + using cyclic_rotation[OF cycle_of_permutation[OF assms(1)], of 1 a] by simp + hence "map (cycle_of_list (support p a)) (support p a) = tl (support p a) @ [ a ]" + by (simp add: hd_map rotate1_hd_tl) + also have " ... = map p (support p a)" + proof (rule nth_equalityI, auto) + fix i assume "i < least_power p a" show "(tl (support p a) @ [a]) ! i = p ((p ^^ i) a)" + proof (cases) + assume i: "i = least_power p a - 1" + hence "(tl (support p a) @ [ a ]) ! i = a" + by (metis (no_types, lifting) diff_zero length_map length_tl length_upt nth_append_length) + also have " ... = p ((p ^^ i) a)" + by (metis (mono_tags, hide_lams) least_power_props i Suc_diff_1 funpow_simps_right(2) funpow_swap1 o_apply) + finally show ?thesis . + next + assume "i \ least_power p a - 1" + with \i < least_power p a\ have "i < least_power p a - 1" + by simp + hence "(tl (support p a) @ [ a ]) ! i = (p ^^ (Suc i)) a" + by (metis One_nat_def Suc_eq_plus1 add.commute length_map length_upt map_tl nth_append nth_map_upt tl_upt) + thus ?thesis + by simp + qed + qed + finally have "map (cycle_of_list (support p a)) (support p a) = map p (support p a)" . + thus ?thesis + using assms(2) by auto +qed + + +subsubsection\Decomposition\ + +inductive cycle_decomp :: "'a set \ ('a \ 'a) \ bool" + where + empty: "cycle_decomp {} id" + | comp: "\ cycle_decomp I p; cycle cs; set cs \ I = {} \ \ + cycle_decomp (set cs \ I) ((cycle_of_list cs) \ p)" + + +lemma semidecomposition: + assumes "p permutes S" and "finite S" + shows "(\y. if y \ (S - set (support p a)) then p y else y) permutes (S - set (support p a))" +proof (rule bij_imp_permutes) + show "(if b \ (S - set (support p a)) then p b else b) = b" if "b \ S - set (support p a)" for b + using that by auto +next + have is_permutation: "permutation p" + using assms unfolding permutation_permutes by blast + + let ?q = "\y. if y \ (S - set (support p a)) then p y else y" + show "bij_betw ?q (S - set (support p a)) (S - set (support p a))" + proof (rule bij_betw_imageI) + show "inj_on ?q (S - set (support p a))" + using permutes_inj[OF assms(1)] unfolding inj_on_def by auto + next + have aux_lemma: "set (support p s) \ (S - set (support p a))" if "s \ S - set (support p a)" for s + proof - + have "(p ^^ i) s \ S" for i + using that unfolding permutes_in_image[OF permutes_funpow[OF assms(1)]] by simp + thus ?thesis + using that disjoint_support'[OF is_permutation, of s a] by auto + qed + have "(p ^^ 1) s \ set (support p s)" for s + unfolding support_set[OF is_permutation] by blast + hence "p s \ set (support p s)" for s + by simp + hence "p ` (S - set (support p a)) \ S - set (support p a)" + using aux_lemma by blast + moreover have "(p ^^ ((least_power p s) - 1)) s \ set (support p s)" for s + unfolding support_set[OF is_permutation] by blast + hence "\s' \ set (support p s). p s' = s" for s + using least_power_of_permutation[OF is_permutation] by (metis Suc_diff_1 funpow.simps(2) o_apply) + hence "S - set (support p a) \ p ` (S - set (support p a))" + using aux_lemma + by (clarsimp simp add: image_iff) (metis image_subset_iff) + ultimately show "?q ` (S - set (support p a)) = (S - set (support p a))" + by auto + qed +qed + +theorem cycle_decomposition: + assumes "p permutes S" and "finite S" shows "cycle_decomp S p" + using assms +proof(induct "card S" arbitrary: S p rule: less_induct) + case less show ?case + proof (cases) + assume "S = {}" thus ?thesis + using empty less(2) by auto + next + have is_permutation: "permutation p" + using less(2-3) unfolding permutation_permutes by blast + + assume "S \ {}" then obtain s where "s \ S" + by blast + define q where "q = (\y. if y \ (S - set (support p s)) then p y else y)" + have "(cycle_of_list (support p s) \ q) = p" + proof + fix a + consider "a \ S - set (support p s)" | "a \ set (support p s)" | "a \ S" "a \ set (support p s)" + by blast + thus "((cycle_of_list (support p s) \ q)) a = p a" + proof cases + case 1 + have "(p ^^ 1) a \ set (support p a)" + unfolding support_set[OF is_permutation] by blast + with \a \ S - set (support p s)\ have "p a \ set (support p s)" + using disjoint_support'[OF is_permutation, of a s] by auto + with \a \ S - set (support p s)\ show ?thesis + using id_outside_supp[of _ "support p s"] unfolding q_def by simp + next + case 2 thus ?thesis + using cycle_restrict[OF is_permutation] unfolding q_def by simp + next + case 3 thus ?thesis + using id_outside_supp[OF 3(2)] less(2) permutes_not_in unfolding q_def by fastforce + qed + qed + + moreover from \s \ S\ have "(p ^^ i) s \ S" for i + unfolding permutes_in_image[OF permutes_funpow[OF less(2)]] . + hence "set (support p s) \ (S - set (support p s)) = S" + by auto + + moreover have "s \ set (support p s)" + using least_power_of_permutation[OF is_permutation] by force + with \s \ S\ have "card (S - set (support p s)) < card S" + using less(3) by (metis DiffE card_seteq linorder_not_le subsetI) + hence "cycle_decomp (S - set (support p s)) q" + using less(1)[OF _ semidecomposition[OF less(2-3)], of s] less(3) unfolding q_def by blast + + moreover show ?thesis + using comp[OF calculation(3) cycle_of_permutation[OF is_permutation], of s] + unfolding calculation(1-2) by blast + qed +qed + +end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/Guide.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/Guide.thy Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,8 @@ + +section \Basic combinatorics in Isabelle/HOL (and the Archive of Formal Proofs)\ + +theory Guide +imports Combinatorics +begin + +end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/List_Permutation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/List_Permutation.thy Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,184 @@ +(* Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker +*) + +section \Permuted Lists\ + +theory List_Permutation +imports Permutations +begin + +text \ + Note that multisets already provide the notion of permutated list and hence + this theory mostly echoes material already logically present in theory + \<^text>\Permutations\; it should be seldom needed. +\ + +subsection \An inductive definition \ldots\ + +inductive perm :: "'a list \ 'a list \ bool" (infixr \<~~>\ 50) +where + Nil [intro!]: "[] <~~> []" +| swap [intro!]: "y # x # l <~~> x # y # l" +| Cons [intro!]: "xs <~~> ys \ z # xs <~~> z # ys" +| trans [intro]: "xs <~~> ys \ ys <~~> zs \ xs <~~> zs" + +proposition perm_refl [iff]: "l <~~> l" + by (induct l) auto + +text \\ldots that is equivalent to an already existing notion:\ + +lemma perm_iff_eq_mset: + \xs <~~> ys \ mset xs = mset ys\ +proof + assume \mset xs = mset ys\ + then show \xs <~~> ys\ + proof (induction xs arbitrary: ys) + case Nil + then show ?case + by simp + next + case (Cons x xs) + from Cons.prems [symmetric] have \mset xs = mset (remove1 x ys)\ + by simp + then have \xs <~~> remove1 x ys\ + by (rule Cons.IH) + then have \x # xs <~~> x # remove1 x ys\ + by (rule perm.Cons) + moreover from Cons.prems have \x \ set ys\ + by (auto dest: union_single_eq_member) + then have \x # remove1 x ys <~~> ys\ + by (induction ys) auto + ultimately show \x # xs <~~> ys\ + by (rule perm.trans) + qed +next + assume \xs <~~> ys\ + then show \mset xs = mset ys\ + by induction simp_all +qed + +theorem mset_eq_perm: \mset xs = mset ys \ xs <~~> ys\ + by (simp add: perm_iff_eq_mset) + + +subsection \Nontrivial conclusions\ + +proposition perm_swap: + \xs[i := xs ! j, j := xs ! i] <~~> xs\ + if \i < length xs\ \j < length xs\ + using that by (simp add: perm_iff_eq_mset mset_swap) + +proposition mset_le_perm_append: "mset xs \# mset ys \ (\zs. xs @ zs <~~> ys)" + by (auto simp add: perm_iff_eq_mset mset_subset_eq_exists_conv ex_mset dest: sym) + +proposition perm_set_eq: "xs <~~> ys \ set xs = set ys" + by (rule mset_eq_setD) (simp add: perm_iff_eq_mset) + +proposition perm_distinct_iff: "xs <~~> ys \ distinct xs \ distinct ys" + by (rule mset_eq_imp_distinct_iff) (simp add: perm_iff_eq_mset) + +theorem eq_set_perm_remdups: "set xs = set ys \ remdups xs <~~> remdups ys" + by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) + +proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \ set x = set y" + by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) + +theorem permutation_Ex_bij: + assumes "xs <~~> ys" + shows "\f. bij_betw f {.. (\imset xs = mset ys\ \length xs = length ys\ + by (auto simp add: perm_iff_eq_mset dest: mset_eq_length) + from \mset xs = mset ys\ obtain p where \p permutes {.. \permute_list p ys = xs\ + by (rule mset_eq_permutation) + then have \bij_betw p {.. + by (simp add: \length xs = length ys\ permutes_imp_bij) + moreover have \\i + using \permute_list p ys = xs\ \length xs = length ys\ \p permutes {.. permute_list_nth + by auto + ultimately show ?thesis + by blast +qed + +proposition perm_finite: "finite {B. B <~~> A}" + using mset_eq_finite by (auto simp add: perm_iff_eq_mset) + + +subsection \Trivial conclusions:\ + +proposition perm_empty_imp: "[] <~~> ys \ ys = []" + by (simp add: perm_iff_eq_mset) + + +text \\medskip This more general theorem is easier to understand!\ + +proposition perm_length: "xs <~~> ys \ length xs = length ys" + by (rule mset_eq_length) (simp add: perm_iff_eq_mset) + +proposition perm_sym: "xs <~~> ys \ ys <~~> xs" + by (simp add: perm_iff_eq_mset) + + +text \We can insert the head anywhere in the list.\ + +proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" + by (simp add: perm_iff_eq_mset) + +proposition perm_append_swap: "xs @ ys <~~> ys @ xs" + by (simp add: perm_iff_eq_mset) + +proposition perm_append_single: "a # xs <~~> xs @ [a]" + by (simp add: perm_iff_eq_mset) + +proposition perm_rev: "rev xs <~~> xs" + by (simp add: perm_iff_eq_mset) + +proposition perm_append1: "xs <~~> ys \ l @ xs <~~> l @ ys" + by (simp add: perm_iff_eq_mset) + +proposition perm_append2: "xs <~~> ys \ xs @ l <~~> ys @ l" + by (simp add: perm_iff_eq_mset) + +proposition perm_empty [iff]: "[] <~~> xs \ xs = []" + by (simp add: perm_iff_eq_mset) + +proposition perm_empty2 [iff]: "xs <~~> [] \ xs = []" + by (simp add: perm_iff_eq_mset) + +proposition perm_sing_imp: "ys <~~> xs \ xs = [y] \ ys = [y]" + by (simp add: perm_iff_eq_mset) + +proposition perm_sing_eq [iff]: "ys <~~> [y] \ ys = [y]" + by (simp add: perm_iff_eq_mset) + +proposition perm_sing_eq2 [iff]: "[y] <~~> ys \ ys = [y]" + by (simp add: perm_iff_eq_mset) + +proposition perm_remove: "x \ set ys \ ys <~~> x # remove1 x ys" + by (simp add: perm_iff_eq_mset) + + +text \\medskip Congruence rule\ + +proposition perm_remove_perm: "xs <~~> ys \ remove1 z xs <~~> remove1 z ys" + by (simp add: perm_iff_eq_mset) + +proposition remove_hd [simp]: "remove1 z (z # xs) = xs" + by (simp add: perm_iff_eq_mset) + +proposition cons_perm_imp_perm: "z # xs <~~> z # ys \ xs <~~> ys" + by (simp add: perm_iff_eq_mset) + +proposition cons_perm_eq [simp]: "z#xs <~~> z#ys \ xs <~~> ys" + by (simp add: perm_iff_eq_mset) + +proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \ xs <~~> ys" + by (simp add: perm_iff_eq_mset) + +proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \ xs <~~> ys" + by (simp add: perm_iff_eq_mset) + +proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \ xs <~~> ys" + by (simp add: perm_iff_eq_mset) + +end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/Multiset_Permutations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/Multiset_Permutations.thy Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,513 @@ +(* Author: Manuel Eberl (TU München) + +Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose +entries correspond to the multiset (resp. set). +*) + +section \Permutations of a Multiset\ + +theory Multiset_Permutations +imports + Complex_Main + Permutations +begin + +(* TODO Move *) +lemma mset_tl: "xs \ [] \ mset (tl xs) = mset xs - {#hd xs#}" + by (cases xs) simp_all + +lemma mset_set_image_inj: + assumes "inj_on f A" + shows "mset_set (f ` A) = image_mset f (mset_set A)" +proof (cases "finite A") + case True + from this and assms show ?thesis by (induction A) auto +qed (insert assms, simp add: finite_image_iff) + +lemma multiset_remove_induct [case_names empty remove]: + assumes "P {#}" "\A. A \ {#} \ (\x. x \# A \ P (A - {#x#})) \ P A" + shows "P A" +proof (induction A rule: full_multiset_induct) + case (less A) + hence IH: "P B" if "B \# A" for B using that by blast + show ?case + proof (cases "A = {#}") + case True + thus ?thesis by (simp add: assms) + next + case False + hence "P (A - {#x#})" if "x \# A" for x + using that by (intro IH) (simp add: mset_subset_diff_self) + from False and this show "P A" by (rule assms) + qed +qed + +lemma map_list_bind: "map g (List.bind xs f) = List.bind xs (map g \ f)" + by (simp add: List.bind_def map_concat) + +lemma mset_eq_mset_set_imp_distinct: + "finite A \ mset_set A = mset xs \ distinct xs" +proof (induction xs arbitrary: A) + case (Cons x xs A) + from Cons.prems(2) have "x \# mset_set A" by simp + with Cons.prems(1) have [simp]: "x \ A" by simp + from Cons.prems have "x \# mset_set (A - {x})" by simp + also from Cons.prems have "mset_set (A - {x}) = mset_set A - {#x#}" + by (subst mset_set_Diff) simp_all + also have "mset_set A = mset (x#xs)" by (simp add: Cons.prems) + also have "\ - {#x#} = mset xs" by simp + finally have [simp]: "x \ set xs" by (simp add: in_multiset_in_set) + from Cons.prems show ?case by (auto intro!: Cons.IH[of "A - {x}"] simp: mset_set_Diff) +qed simp_all +(* END TODO *) + + +subsection \Permutations of a multiset\ + +definition permutations_of_multiset :: "'a multiset \ 'a list set" where + "permutations_of_multiset A = {xs. mset xs = A}" + +lemma permutations_of_multisetI: "mset xs = A \ xs \ permutations_of_multiset A" + by (simp add: permutations_of_multiset_def) + +lemma permutations_of_multisetD: "xs \ permutations_of_multiset A \ mset xs = A" + by (simp add: permutations_of_multiset_def) + +lemma permutations_of_multiset_Cons_iff: + "x # xs \ permutations_of_multiset A \ x \# A \ xs \ permutations_of_multiset (A - {#x#})" + by (auto simp: permutations_of_multiset_def) + +lemma permutations_of_multiset_empty [simp]: "permutations_of_multiset {#} = {[]}" + unfolding permutations_of_multiset_def by simp + +lemma permutations_of_multiset_nonempty: + assumes nonempty: "A \ {#}" + shows "permutations_of_multiset A = + (\x\set_mset A. ((#) x) ` permutations_of_multiset (A - {#x#}))" (is "_ = ?rhs") +proof safe + fix xs assume "xs \ permutations_of_multiset A" + hence mset_xs: "mset xs = A" by (simp add: permutations_of_multiset_def) + hence "xs \ []" by (auto simp: nonempty) + then obtain x xs' where xs: "xs = x # xs'" by (cases xs) simp_all + with mset_xs have "x \ set_mset A" "xs' \ permutations_of_multiset (A - {#x#})" + by (auto simp: permutations_of_multiset_def) + with xs show "xs \ ?rhs" by auto +qed (auto simp: permutations_of_multiset_def) + +lemma permutations_of_multiset_singleton [simp]: "permutations_of_multiset {#x#} = {[x]}" + by (simp add: permutations_of_multiset_nonempty) + +lemma permutations_of_multiset_doubleton: + "permutations_of_multiset {#x,y#} = {[x,y], [y,x]}" + by (simp add: permutations_of_multiset_nonempty insert_commute) + +lemma rev_permutations_of_multiset [simp]: + "rev ` permutations_of_multiset A = permutations_of_multiset A" +proof + have "rev ` rev ` permutations_of_multiset A \ rev ` permutations_of_multiset A" + unfolding permutations_of_multiset_def by auto + also have "rev ` rev ` permutations_of_multiset A = permutations_of_multiset A" + by (simp add: image_image) + finally show "permutations_of_multiset A \ rev ` permutations_of_multiset A" . +next + show "rev ` permutations_of_multiset A \ permutations_of_multiset A" + unfolding permutations_of_multiset_def by auto +qed + +lemma length_finite_permutations_of_multiset: + "xs \ permutations_of_multiset A \ length xs = size A" + by (auto simp: permutations_of_multiset_def) + +lemma permutations_of_multiset_lists: "permutations_of_multiset A \ lists (set_mset A)" + by (auto simp: permutations_of_multiset_def) + +lemma finite_permutations_of_multiset [simp]: "finite (permutations_of_multiset A)" +proof (rule finite_subset) + show "permutations_of_multiset A \ {xs. set xs \ set_mset A \ length xs = size A}" + by (auto simp: permutations_of_multiset_def) + show "finite {xs. set xs \ set_mset A \ length xs = size A}" + by (rule finite_lists_length_eq) simp_all +qed + +lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \ {}" +proof - + from ex_mset[of A] guess xs .. + thus ?thesis by (auto simp: permutations_of_multiset_def) +qed + +lemma permutations_of_multiset_image: + "permutations_of_multiset (image_mset f A) = map f ` permutations_of_multiset A" +proof safe + fix xs assume A: "xs \ permutations_of_multiset (image_mset f A)" + from ex_mset[of A] obtain ys where ys: "mset ys = A" .. + with A have "mset xs = mset (map f ys)" + by (simp add: permutations_of_multiset_def) + from mset_eq_permutation[OF this] guess \ . note \ = this + with ys have "xs = map f (permute_list \ ys)" + by (simp add: permute_list_map) + moreover from \ ys have "permute_list \ ys \ permutations_of_multiset A" + by (simp add: permutations_of_multiset_def) + ultimately show "xs \ map f ` permutations_of_multiset A" by blast +qed (auto simp: permutations_of_multiset_def) + + +subsection \Cardinality of permutations\ + +text \ + In this section, we prove some basic facts about the number of permutations of a multiset. +\ + +context +begin + +private lemma multiset_prod_fact_insert: + "(\y\set_mset (A+{#x#}). fact (count (A+{#x#}) y)) = + (count A x + 1) * (\y\set_mset A. fact (count A y))" +proof - + have "(\y\set_mset (A+{#x#}). fact (count (A+{#x#}) y)) = + (\y\set_mset (A+{#x#}). (if y = x then count A x + 1 else 1) * fact (count A y))" + by (intro prod.cong) simp_all + also have "\ = (count A x + 1) * (\y\set_mset (A+{#x#}). fact (count A y))" + by (simp add: prod.distrib) + also have "(\y\set_mset (A+{#x#}). fact (count A y)) = (\y\set_mset A. fact (count A y))" + by (intro prod.mono_neutral_right) (auto simp: not_in_iff) + finally show ?thesis . +qed + +private lemma multiset_prod_fact_remove: + "x \# A \ (\y\set_mset A. fact (count A y)) = + count A x * (\y\set_mset (A-{#x#}). fact (count (A-{#x#}) y))" + using multiset_prod_fact_insert[of "A - {#x#}" x] by simp + +lemma card_permutations_of_multiset_aux: + "card (permutations_of_multiset A) * (\x\set_mset A. fact (count A x)) = fact (size A)" +proof (induction A rule: multiset_remove_induct) + case (remove A) + have "card (permutations_of_multiset A) = + card (\x\set_mset A. (#) x ` permutations_of_multiset (A - {#x#}))" + by (simp add: permutations_of_multiset_nonempty remove.hyps) + also have "\ = (\x\set_mset A. card (permutations_of_multiset (A - {#x#})))" + by (subst card_UN_disjoint) (auto simp: card_image) + also have "\ * (\x\set_mset A. fact (count A x)) = + (\x\set_mset A. card (permutations_of_multiset (A - {#x#})) * + (\y\set_mset A. fact (count A y)))" + by (subst sum_distrib_right) simp_all + also have "\ = (\x\set_mset A. count A x * fact (size A - 1))" + proof (intro sum.cong refl) + fix x assume x: "x \# A" + have "card (permutations_of_multiset (A - {#x#})) * (\y\set_mset A. fact (count A y)) = + count A x * (card (permutations_of_multiset (A - {#x#})) * + (\y\set_mset (A - {#x#}). fact (count (A - {#x#}) y)))" (is "?lhs = _") + by (subst multiset_prod_fact_remove[OF x]) simp_all + also note remove.IH[OF x] + also from x have "size (A - {#x#}) = size A - 1" by (simp add: size_Diff_submset) + finally show "?lhs = count A x * fact (size A - 1)" . + qed + also have "(\x\set_mset A. count A x * fact (size A - 1)) = + size A * fact (size A - 1)" + by (simp add: sum_distrib_right size_multiset_overloaded_eq) + also from remove.hyps have "\ = fact (size A)" + by (cases "size A") auto + finally show ?case . +qed simp_all + +theorem card_permutations_of_multiset: + "card (permutations_of_multiset A) = fact (size A) div (\x\set_mset A. fact (count A x))" + "(\x\set_mset A. fact (count A x) :: nat) dvd fact (size A)" + by (simp_all flip: card_permutations_of_multiset_aux[of A]) + +lemma card_permutations_of_multiset_insert_aux: + "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) = + (size A + 1) * card (permutations_of_multiset A)" +proof - + note card_permutations_of_multiset_aux[of "A + {#x#}"] + also have "fact (size (A + {#x#})) = (size A + 1) * fact (size A)" by simp + also note multiset_prod_fact_insert[of A x] + also note card_permutations_of_multiset_aux[of A, symmetric] + finally have "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) * + (\y\set_mset A. fact (count A y)) = + (size A + 1) * card (permutations_of_multiset A) * + (\x\set_mset A. fact (count A x))" by (simp only: mult_ac) + thus ?thesis by (subst (asm) mult_right_cancel) simp_all +qed + +lemma card_permutations_of_multiset_remove_aux: + assumes "x \# A" + shows "card (permutations_of_multiset A) * count A x = + size A * card (permutations_of_multiset (A - {#x#}))" +proof - + from assms have A: "A - {#x#} + {#x#} = A" by simp + from assms have B: "size A = size (A - {#x#}) + 1" + by (subst A [symmetric], subst size_union) simp + show ?thesis + using card_permutations_of_multiset_insert_aux[of "A - {#x#}" x, unfolded A] assms + by (simp add: B) +qed + +lemma real_card_permutations_of_multiset_remove: + assumes "x \# A" + shows "real (card (permutations_of_multiset (A - {#x#}))) = + real (card (permutations_of_multiset A) * count A x) / real (size A)" + using assms by (subst card_permutations_of_multiset_remove_aux[OF assms]) auto + +lemma real_card_permutations_of_multiset_remove': + assumes "x \# A" + shows "real (card (permutations_of_multiset A)) = + real (size A * card (permutations_of_multiset (A - {#x#}))) / real (count A x)" + using assms by (subst card_permutations_of_multiset_remove_aux[OF assms, symmetric]) simp + +end + + + +subsection \Permutations of a set\ + +definition permutations_of_set :: "'a set \ 'a list set" where + "permutations_of_set A = {xs. set xs = A \ distinct xs}" + +lemma permutations_of_set_altdef: + "finite A \ permutations_of_set A = permutations_of_multiset (mset_set A)" + by (auto simp add: permutations_of_set_def permutations_of_multiset_def mset_set_set + in_multiset_in_set [symmetric] mset_eq_mset_set_imp_distinct) + +lemma permutations_of_setI [intro]: + assumes "set xs = A" "distinct xs" + shows "xs \ permutations_of_set A" + using assms unfolding permutations_of_set_def by simp + +lemma permutations_of_setD: + assumes "xs \ permutations_of_set A" + shows "set xs = A" "distinct xs" + using assms unfolding permutations_of_set_def by simp_all + +lemma permutations_of_set_lists: "permutations_of_set A \ lists A" + unfolding permutations_of_set_def by auto + +lemma permutations_of_set_empty [simp]: "permutations_of_set {} = {[]}" + by (auto simp: permutations_of_set_def) + +lemma UN_set_permutations_of_set [simp]: + "finite A \ (\xs\permutations_of_set A. set xs) = A" + using finite_distinct_list by (auto simp: permutations_of_set_def) + +lemma permutations_of_set_infinite: + "\finite A \ permutations_of_set A = {}" + by (auto simp: permutations_of_set_def) + +lemma permutations_of_set_nonempty: + "A \ {} \ permutations_of_set A = + (\x\A. (\xs. x # xs) ` permutations_of_set (A - {x}))" + by (cases "finite A") + (simp_all add: permutations_of_multiset_nonempty mset_set_empty_iff mset_set_Diff + permutations_of_set_altdef permutations_of_set_infinite) + +lemma permutations_of_set_singleton [simp]: "permutations_of_set {x} = {[x]}" + by (subst permutations_of_set_nonempty) auto + +lemma permutations_of_set_doubleton: + "x \ y \ permutations_of_set {x,y} = {[x,y], [y,x]}" + by (subst permutations_of_set_nonempty) + (simp_all add: insert_Diff_if insert_commute) + +lemma rev_permutations_of_set [simp]: + "rev ` permutations_of_set A = permutations_of_set A" + by (cases "finite A") (simp_all add: permutations_of_set_altdef permutations_of_set_infinite) + +lemma length_finite_permutations_of_set: + "xs \ permutations_of_set A \ length xs = card A" + by (auto simp: permutations_of_set_def distinct_card) + +lemma finite_permutations_of_set [simp]: "finite (permutations_of_set A)" + by (cases "finite A") (simp_all add: permutations_of_set_infinite permutations_of_set_altdef) + +lemma permutations_of_set_empty_iff [simp]: + "permutations_of_set A = {} \ \finite A" + unfolding permutations_of_set_def using finite_distinct_list[of A] by auto + +lemma card_permutations_of_set [simp]: + "finite A \ card (permutations_of_set A) = fact (card A)" + by (simp add: permutations_of_set_altdef card_permutations_of_multiset del: One_nat_def) + +lemma permutations_of_set_image_inj: + assumes inj: "inj_on f A" + shows "permutations_of_set (f ` A) = map f ` permutations_of_set A" + by (cases "finite A") + (simp_all add: permutations_of_set_infinite permutations_of_set_altdef + permutations_of_multiset_image mset_set_image_inj inj finite_image_iff) + +lemma permutations_of_set_image_permutes: + "\ permutes A \ map \ ` permutations_of_set A = permutations_of_set A" + by (subst permutations_of_set_image_inj [symmetric]) + (simp_all add: permutes_inj_on permutes_image) + + +subsection \Code generation\ + +text \ + First, we give code an implementation for permutations of lists. +\ + +declare length_remove1 [termination_simp] + +fun permutations_of_list_impl where + "permutations_of_list_impl xs = (if xs = [] then [[]] else + List.bind (remdups xs) (\x. map ((#) x) (permutations_of_list_impl (remove1 x xs))))" + +fun permutations_of_list_impl_aux where + "permutations_of_list_impl_aux acc xs = (if xs = [] then [acc] else + List.bind (remdups xs) (\x. permutations_of_list_impl_aux (x#acc) (remove1 x xs)))" + +declare permutations_of_list_impl_aux.simps [simp del] +declare permutations_of_list_impl.simps [simp del] + +lemma permutations_of_list_impl_Nil [simp]: + "permutations_of_list_impl [] = [[]]" + by (simp add: permutations_of_list_impl.simps) + +lemma permutations_of_list_impl_nonempty: + "xs \ [] \ permutations_of_list_impl xs = + List.bind (remdups xs) (\x. map ((#) x) (permutations_of_list_impl (remove1 x xs)))" + by (subst permutations_of_list_impl.simps) simp_all + +lemma set_permutations_of_list_impl: + "set (permutations_of_list_impl xs) = permutations_of_multiset (mset xs)" + by (induction xs rule: permutations_of_list_impl.induct) + (subst permutations_of_list_impl.simps, + simp_all add: permutations_of_multiset_nonempty set_list_bind) + +lemma distinct_permutations_of_list_impl: + "distinct (permutations_of_list_impl xs)" + by (induction xs rule: permutations_of_list_impl.induct, + subst permutations_of_list_impl.simps) + (auto intro!: distinct_list_bind simp: distinct_map o_def disjoint_family_on_def) + +lemma permutations_of_list_impl_aux_correct': + "permutations_of_list_impl_aux acc xs = + map (\xs. rev xs @ acc) (permutations_of_list_impl xs)" + by (induction acc xs rule: permutations_of_list_impl_aux.induct, + subst permutations_of_list_impl_aux.simps, subst permutations_of_list_impl.simps) + (auto simp: map_list_bind intro!: list_bind_cong) + +lemma permutations_of_list_impl_aux_correct: + "permutations_of_list_impl_aux [] xs = map rev (permutations_of_list_impl xs)" + by (simp add: permutations_of_list_impl_aux_correct') + +lemma distinct_permutations_of_list_impl_aux: + "distinct (permutations_of_list_impl_aux acc xs)" + by (simp add: permutations_of_list_impl_aux_correct' distinct_map + distinct_permutations_of_list_impl inj_on_def) + +lemma set_permutations_of_list_impl_aux: + "set (permutations_of_list_impl_aux [] xs) = permutations_of_multiset (mset xs)" + by (simp add: permutations_of_list_impl_aux_correct set_permutations_of_list_impl) + +declare set_permutations_of_list_impl_aux [symmetric, code] + +value [code] "permutations_of_multiset {#1,2,3,4::int#}" + + + +text \ + Now we turn to permutations of sets. We define an auxiliary version with an + accumulator to avoid having to map over the results. +\ +function permutations_of_set_aux where + "permutations_of_set_aux acc A = + (if \finite A then {} else if A = {} then {acc} else + (\x\A. permutations_of_set_aux (x#acc) (A - {x})))" +by auto +termination by (relation "Wellfounded.measure (card \ snd)") (simp_all add: card_gt_0_iff) + +lemma permutations_of_set_aux_altdef: + "permutations_of_set_aux acc A = (\xs. rev xs @ acc) ` permutations_of_set A" +proof (cases "finite A") + assume "finite A" + thus ?thesis + proof (induction A arbitrary: acc rule: finite_psubset_induct) + case (psubset A acc) + show ?case + proof (cases "A = {}") + case False + note [simp del] = permutations_of_set_aux.simps + from psubset.hyps False + have "permutations_of_set_aux acc A = + (\y\A. permutations_of_set_aux (y#acc) (A - {y}))" + by (subst permutations_of_set_aux.simps) simp_all + also have "\ = (\y\A. (\xs. rev xs @ acc) ` (\xs. y # xs) ` permutations_of_set (A - {y}))" + apply (rule arg_cong [of _ _ Union], rule image_cong) + apply (simp_all add: image_image) + apply (subst psubset) + apply auto + done + also from False have "\ = (\xs. rev xs @ acc) ` permutations_of_set A" + by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN) + finally show ?thesis . + qed simp_all + qed +qed (simp_all add: permutations_of_set_infinite) + +declare permutations_of_set_aux.simps [simp del] + +lemma permutations_of_set_aux_correct: + "permutations_of_set_aux [] A = permutations_of_set A" + by (simp add: permutations_of_set_aux_altdef) + + +text \ + In another refinement step, we define a version on lists. +\ +declare length_remove1 [termination_simp] + +fun permutations_of_set_aux_list where + "permutations_of_set_aux_list acc xs = + (if xs = [] then [acc] else + List.bind xs (\x. permutations_of_set_aux_list (x#acc) (List.remove1 x xs)))" + +definition permutations_of_set_list where + "permutations_of_set_list xs = permutations_of_set_aux_list [] xs" + +declare permutations_of_set_aux_list.simps [simp del] + +lemma permutations_of_set_aux_list_refine: + assumes "distinct xs" + shows "set (permutations_of_set_aux_list acc xs) = permutations_of_set_aux acc (set xs)" + using assms + by (induction acc xs rule: permutations_of_set_aux_list.induct) + (subst permutations_of_set_aux_list.simps, + subst permutations_of_set_aux.simps, + simp_all add: set_list_bind) + + +text \ + The permutation lists contain no duplicates if the inputs contain no duplicates. + Therefore, these functions can easily be used when working with a representation of + sets by distinct lists. + The same approach should generalise to any kind of set implementation that supports + a monadic bind operation, and since the results are disjoint, merging should be cheap. +\ +lemma distinct_permutations_of_set_aux_list: + "distinct xs \ distinct (permutations_of_set_aux_list acc xs)" + by (induction acc xs rule: permutations_of_set_aux_list.induct) + (subst permutations_of_set_aux_list.simps, + auto intro!: distinct_list_bind simp: disjoint_family_on_def + permutations_of_set_aux_list_refine permutations_of_set_aux_altdef) + +lemma distinct_permutations_of_set_list: + "distinct xs \ distinct (permutations_of_set_list xs)" + by (simp add: permutations_of_set_list_def distinct_permutations_of_set_aux_list) + +lemma permutations_of_list: + "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" + by (simp add: permutations_of_set_aux_correct [symmetric] + permutations_of_set_aux_list_refine permutations_of_set_list_def) + +lemma permutations_of_list_code [code]: + "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" + "permutations_of_set (List.coset xs) = + Code.abort (STR ''Permutation of set complement not supported'') + (\_. permutations_of_set (List.coset xs))" + by (simp_all add: permutations_of_list) + +value [code] "permutations_of_set (set ''abcd'')" + +end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/Permutations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/Permutations.thy Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,1628 @@ +(* Author: Amine Chaieb, University of Cambridge +*) + +section \Permutations, both general and specifically on finite sets.\ + +theory Permutations + imports + "HOL-Library.Multiset" + "HOL-Library.Disjoint_Sets" +begin + +subsection \Auxiliary\ + +abbreviation (input) fixpoints :: \('a \ 'a) \ 'a set\ + where \fixpoints f \ {x. f x = x}\ + +lemma inj_on_fixpoints: + \inj_on f (fixpoints f)\ + by (rule inj_onI) simp + +lemma bij_betw_fixpoints: + \bij_betw f (fixpoints f) (fixpoints f)\ + using inj_on_fixpoints by (auto simp add: bij_betw_def) + + +subsection \Basic definition and consequences\ + +definition permutes :: \('a \ 'a) \ 'a set \ bool\ (infixr \permutes\ 41) + where \p permutes S \ (\x. x \ S \ p x = x) \ (\y. \!x. p x = y)\ + +lemma bij_imp_permutes: + \p permutes S\ if \bij_betw p S S\ and stable: \\x. x \ S \ p x = x\ +proof - + note \bij_betw p S S\ + moreover have \bij_betw p (- S) (- S)\ + by (auto simp add: stable intro!: bij_betw_imageI inj_onI) + ultimately have \bij_betw p (S \ - S) (S \ - S)\ + by (rule bij_betw_combine) simp + then have \\!x. p x = y\ for y + by (simp add: bij_iff) + with stable show ?thesis + by (simp add: permutes_def) +qed + +context + fixes p :: \'a \ 'a\ and S :: \'a set\ + assumes perm: \p permutes S\ +begin + +lemma permutes_inj: + \inj p\ + using perm by (auto simp: permutes_def inj_on_def) + +lemma permutes_image: + \p ` S = S\ +proof (rule set_eqI) + fix x + show \x \ p ` S \ x \ S\ + proof + assume \x \ p ` S\ + then obtain y where \y \ S\ \p y = x\ + by blast + with perm show \x \ S\ + by (cases \y = x\) (auto simp add: permutes_def) + next + assume \x \ S\ + with perm obtain y where \y \ S\ \p y = x\ + by (metis permutes_def) + then show \x \ p ` S\ + by blast + qed +qed + +lemma permutes_not_in: + \x \ S \ p x = x\ + using perm by (auto simp: permutes_def) + +lemma permutes_image_complement: + \p ` (- S) = - S\ + by (auto simp add: permutes_not_in) + +lemma permutes_in_image: + \p x \ S \ x \ S\ + using permutes_image permutes_inj by (auto dest: inj_image_mem_iff) + +lemma permutes_surj: + \surj p\ +proof - + have \p ` (S \ - S) = p ` S \ p ` (- S)\ + by (rule image_Un) + then show ?thesis + by (simp add: permutes_image permutes_image_complement) +qed + +lemma permutes_inv_o: + shows "p \ inv p = id" + and "inv p \ p = id" + using permutes_inj permutes_surj + unfolding inj_iff [symmetric] surj_iff [symmetric] by auto + +lemma permutes_inverses: + shows "p (inv p x) = x" + and "inv p (p x) = x" + using permutes_inv_o [unfolded fun_eq_iff o_def] by auto + +lemma permutes_inv_eq: + \inv p y = x \ p x = y\ + by (auto simp add: permutes_inverses) + +lemma permutes_inj_on: + \inj_on p A\ + by (rule inj_on_subset [of _ UNIV]) (auto intro: permutes_inj) + +lemma permutes_bij: + \bij p\ + unfolding bij_def by (metis permutes_inj permutes_surj) + +lemma permutes_imp_bij: + \bij_betw p S S\ + by (simp add: bij_betw_def permutes_image permutes_inj_on) + +lemma permutes_subset: + \p permutes T\ if \S \ T\ +proof (rule bij_imp_permutes) + define R where \R = T - S\ + with that have \T = R \ S\ \R \ S = {}\ + by auto + then have \p x = x\ if \x \ R\ for x + using that by (auto intro: permutes_not_in) + then have \p ` R = R\ + by simp + with \T = R \ S\ show \bij_betw p T T\ + by (simp add: bij_betw_def permutes_inj_on image_Un permutes_image) + fix x + assume \x \ T\ + with \T = R \ S\ show \p x = x\ + by (simp add: permutes_not_in) +qed + +lemma permutes_imp_permutes_insert: + \p permutes insert x S\ + by (rule permutes_subset) auto + +end + +lemma permutes_id [simp]: + \id permutes S\ + by (auto intro: bij_imp_permutes) + +lemma permutes_empty [simp]: + \p permutes {} \ p = id\ +proof + assume \p permutes {}\ + then show \p = id\ + by (auto simp add: fun_eq_iff permutes_not_in) +next + assume \p = id\ + then show \p permutes {}\ + by simp +qed + +lemma permutes_sing [simp]: + \p permutes {a} \ p = id\ +proof + assume perm: \p permutes {a}\ + show \p = id\ + proof + fix x + from perm have \p ` {a} = {a}\ + by (rule permutes_image) + with perm show \p x = id x\ + by (cases \x = a\) (auto simp add: permutes_not_in) + qed +next + assume \p = id\ + then show \p permutes {a}\ + by simp +qed + +lemma permutes_univ: "p permutes UNIV \ (\y. \!x. p x = y)" + by (simp add: permutes_def) + +lemma permutes_swap_id: "a \ S \ b \ S \ Fun.swap a b id permutes S" + by (rule bij_imp_permutes) (auto simp add: swap_id_eq) + +lemma permutes_superset: + \p permutes T\ if \p permutes S\ \\x. x \ S - T \ p x = x\ +proof - + define R U where \R = T \ S\ and \U = S - T\ + then have \T = R \ (T - S)\ \S = R \ U\ \R \ U = {}\ + by auto + from that \U = S - T\ have \p ` U = U\ + by simp + from \p permutes S\ have \bij_betw p (R \ U) (R \ U)\ + by (simp add: permutes_imp_bij \S = R \ U\) + moreover have \bij_betw p U U\ + using that \U = S - T\ by (simp add: bij_betw_def permutes_inj_on) + ultimately have \bij_betw p R R\ + using \R \ U = {}\ \R \ U = {}\ by (rule bij_betw_partition) + then have \p permutes R\ + proof (rule bij_imp_permutes) + fix x + assume \x \ R\ + with \R = T \ S\ \p permutes S\ show \p x = x\ + by (cases \x \ S\) (auto simp add: permutes_not_in that(2)) + qed + then have \p permutes R \ (T - S)\ + by (rule permutes_subset) simp + with \T = R \ (T - S)\ show ?thesis + by simp +qed + +lemma permutes_bij_inv_into: \<^marker>\contributor \Lukas Bulwahn\\ + fixes A :: "'a set" + and B :: "'b set" + assumes "p permutes A" + and "bij_betw f A B" + shows "(\x. if x \ B then f (p (inv_into A f x)) else x) permutes B" +proof (rule bij_imp_permutes) + from assms have "bij_betw p A A" "bij_betw f A B" "bij_betw (inv_into A f) B A" + by (auto simp add: permutes_imp_bij bij_betw_inv_into) + then have "bij_betw (f \ p \ inv_into A f) B B" + by (simp add: bij_betw_trans) + then show "bij_betw (\x. if x \ B then f (p (inv_into A f x)) else x) B B" + by (subst bij_betw_cong[where g="f \ p \ inv_into A f"]) auto +next + fix x + assume "x \ B" + then show "(if x \ B then f (p (inv_into A f x)) else x) = x" by auto +qed + +lemma permutes_image_mset: \<^marker>\contributor \Lukas Bulwahn\\ + assumes "p permutes A" + shows "image_mset p (mset_set A) = mset_set A" + using assms by (metis image_mset_mset_set bij_betw_imp_inj_on permutes_imp_bij permutes_image) + +lemma permutes_implies_image_mset_eq: \<^marker>\contributor \Lukas Bulwahn\\ + assumes "p permutes A" "\x. x \ A \ f x = f' (p x)" + shows "image_mset f' (mset_set A) = image_mset f (mset_set A)" +proof - + have "f x = f' (p x)" if "x \# mset_set A" for x + using assms(2)[of x] that by (cases "finite A") auto + with assms have "image_mset f (mset_set A) = image_mset (f' \ p) (mset_set A)" + by (auto intro!: image_mset_cong) + also have "\ = image_mset f' (image_mset p (mset_set A))" + by (simp add: image_mset.compositionality) + also have "\ = image_mset f' (mset_set A)" + proof - + from assms permutes_image_mset have "image_mset p (mset_set A) = mset_set A" + by blast + then show ?thesis by simp + qed + finally show ?thesis .. +qed + + +subsection \Group properties\ + +lemma permutes_compose: "p permutes S \ q permutes S \ q \ p permutes S" + unfolding permutes_def o_def by metis + +lemma permutes_inv: + assumes "p permutes S" + shows "inv p permutes S" + using assms unfolding permutes_def permutes_inv_eq[OF assms] by metis + +lemma permutes_inv_inv: + assumes "p permutes S" + shows "inv (inv p) = p" + unfolding fun_eq_iff permutes_inv_eq[OF assms] permutes_inv_eq[OF permutes_inv[OF assms]] + 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 + show "inv p x = p' x" for x + proof (cases "x \ S") + case True + from assms have "p' x = p' (p (inv p x))" + by (simp add: permutes_inverses) + also from permutes_inv[OF perm] True have "\ = inv p x" + by (subst inv) (simp_all add: permutes_in_image) + finally show ?thesis .. + next + case False + with permutes_inv[OF perm] show ?thesis + by (simp_all add: outside permutes_not_in) + qed +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 \Mapping permutations with bijections\ + +lemma bij_betw_permutations: + assumes "bij_betw f A B" + shows "bij_betw (\\ x. if x \ B then f (\ (inv_into A f x)) else x) + {\. \ permutes A} {\. \ permutes B}" (is "bij_betw ?f _ _") +proof - + let ?g = "(\\ x. if x \ A then inv_into A f (\ (f x)) else x)" + show ?thesis + proof (rule bij_betw_byWitness [of _ ?g], goal_cases) + case 3 + show ?case using permutes_bij_inv_into[OF _ assms] by auto + next + case 4 + have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms) + { + fix \ assume "\ permutes B" + from permutes_bij_inv_into[OF this bij_inv] and assms + have "(\x. if x \ A then inv_into A f (\ (f x)) else x) permutes A" + by (simp add: inv_into_inv_into_eq cong: if_cong) + } + from this show ?case by (auto simp: permutes_inv) + next + case 1 + thus ?case using assms + by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left + dest: bij_betwE) + next + case 2 + moreover have "bij_betw (inv_into A f) B A" + by (intro bij_betw_inv_into assms) + ultimately show ?case using assms + by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right + dest: bij_betwE) + qed +qed + +lemma bij_betw_derangements: + assumes "bij_betw f A B" + shows "bij_betw (\\ x. if x \ B then f (\ (inv_into A f x)) else x) + {\. \ permutes A \ (\x\A. \ x \ x)} {\. \ permutes B \ (\x\B. \ x \ x)}" + (is "bij_betw ?f _ _") +proof - + let ?g = "(\\ x. if x \ A then inv_into A f (\ (f x)) else x)" + show ?thesis + proof (rule bij_betw_byWitness [of _ ?g], goal_cases) + case 3 + have "?f \ x \ x" if "\ permutes A" "\x. x \ A \ \ x \ x" "x \ B" for \ x + using that and assms by (metis bij_betwE bij_betw_imp_inj_on bij_betw_imp_surj_on + inv_into_f_f inv_into_into permutes_imp_bij) + with permutes_bij_inv_into[OF _ assms] show ?case by auto + next + case 4 + have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms) + have "?g \ permutes A" if "\ permutes B" for \ + using permutes_bij_inv_into[OF that bij_inv] and assms + by (simp add: inv_into_inv_into_eq cong: if_cong) + moreover have "?g \ x \ x" if "\ permutes B" "\x. x \ B \ \ x \ x" "x \ A" for \ x + using that and assms by (metis bij_betwE bij_betw_imp_surj_on f_inv_into_f permutes_imp_bij) + ultimately show ?case by auto + next + case 1 + thus ?case using assms + by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left + dest: bij_betwE) + next + case 2 + moreover have "bij_betw (inv_into A f) B A" + by (intro bij_betw_inv_into assms) + ultimately show ?case using assms + by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right + dest: bij_betwE) + qed +qed + + +subsection \The number of permutations on a finite set\ + +lemma permutes_insert_lemma: + assumes "p permutes (insert a S)" + shows "Fun.swap a (p a) id \ p permutes S" + apply (rule permutes_superset[where S = "insert a S"]) + apply (rule permutes_compose[OF assms]) + apply (rule permutes_swap_id, simp) + using permutes_in_image[OF assms, of a] + apply simp + apply (auto simp add: Ball_def Fun.swap_def) + done + +lemma permutes_insert: "{p. p permutes (insert a S)} = + (\(b, p). Fun.swap a b id \ p) ` {(b, p). b \ insert a S \ p \ {p. p permutes S}}" +proof - + have "p permutes insert a S \ + (\b q. p = Fun.swap a b id \ q \ b \ insert a S \ q permutes S)" for p + proof - + have "\b q. p = Fun.swap a b id \ q \ b \ insert a S \ q permutes S" + if p: "p permutes insert a S" + proof - + let ?b = "p a" + let ?q = "Fun.swap a (p a) id \ p" + have *: "p = Fun.swap a ?b id \ ?q" + by (simp add: fun_eq_iff o_assoc) + have **: "?b \ insert a S" + unfolding permutes_in_image[OF p] by simp + from permutes_insert_lemma[OF p] * ** show ?thesis + by blast + qed + moreover have "p permutes insert a S" + if bq: "p = Fun.swap a b id \ q" "b \ insert a S" "q permutes S" for b q + proof - + from permutes_subset[OF bq(3), of "insert a S"] have q: "q permutes insert a S" + by auto + have a: "a \ insert a S" + by simp + from bq(1) permutes_compose[OF q permutes_swap_id[OF a bq(2)]] show ?thesis + by simp + qed + ultimately show ?thesis by blast + qed + then show ?thesis by auto +qed + +lemma card_permutations: + assumes "card S = n" + and "finite S" + shows "card {p. p permutes S} = fact n" + using assms(2,1) +proof (induct arbitrary: n) + case empty + then show ?case by simp +next + case (insert x F) + { + fix n + assume card_insert: "card (insert x F) = n" + let ?xF = "{p. p permutes insert x F}" + let ?pF = "{p. p permutes F}" + let ?pF' = "{(b, p). b \ insert x F \ p \ ?pF}" + let ?g = "(\(b, p). Fun.swap x b id \ p)" + have xfgpF': "?xF = ?g ` ?pF'" + by (rule permutes_insert[of x F]) + from \x \ F\ \finite F\ card_insert have Fs: "card F = n - 1" + by auto + from \finite F\ insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" + by auto + then have "finite ?pF" + by (auto intro: card_ge_0_finite) + with \finite F\ card.insert_remove have pF'f: "finite ?pF'" + apply (simp only: Collect_case_prod Collect_mem_eq) + apply (rule finite_cartesian_product) + apply simp_all + done + + have ginj: "inj_on ?g ?pF'" + proof - + { + fix b p c q + assume bp: "(b, p) \ ?pF'" + assume cq: "(c, q) \ ?pF'" + assume eq: "?g (b, p) = ?g (c, q)" + from bp cq have pF: "p permutes F" and qF: "q permutes F" + by auto + from pF \x \ F\ eq have "b = ?g (b, p) x" + by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff) + also from qF \x \ F\ eq have "\ = ?g (c, q) x" + by (auto simp: fun_upd_def fun_eq_iff) + also from qF \x \ F\ have "\ = c" + by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff) + finally have "b = c" . + then have "Fun.swap x b id = Fun.swap x c id" + by simp + with eq have "Fun.swap x b id \ p = Fun.swap x b id \ q" + by simp + then have "Fun.swap x b id \ (Fun.swap x b id \ p) = Fun.swap x b id \ (Fun.swap x b id \ q)" + by simp + then have "p = q" + by (simp add: o_assoc) + with \b = c\ have "(b, p) = (c, q)" + by simp + } + then show ?thesis + unfolding inj_on_def by blast + qed + from \x \ F\ \finite F\ card_insert have "n \ 0" + by auto + then have "\m. n = Suc m" + by presburger + then obtain m where n: "n = Suc m" + by blast + from pFs card_insert have *: "card ?xF = fact n" + unfolding xfgpF' card_image[OF ginj] + using \finite F\ \finite ?pF\ + by (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product) (simp add: n) + from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" + by (simp add: xfgpF' n) + from * have "card ?xF = fact n" + unfolding xFf by blast + } + with insert show ?case by simp +qed + +lemma finite_permutations: + assumes "finite S" + shows "finite {p. p permutes S}" + using card_permutations[OF refl assms] by (auto intro: card_ge_0_finite) + + +subsection \Hence a sort of induction principle composing by swaps\ + +lemma permutes_induct [consumes 2, case_names id swap]: + \P p\ if \p permutes S\ \finite S\ + and id: \P id\ + and swap: \\a b p. a \ S \ b \ S \ p permutes S \ P p \ P (Fun.swap a b id \ p)\ +using \finite S\ \p permutes S\ swap proof (induction S arbitrary: p) + case empty + with id show ?case + by (simp only: permutes_empty) +next + case (insert x S p) + define q where \q = Fun.swap x (p x) id \ p\ + then have swap_q: \Fun.swap x (p x) id \ q = p\ + by (simp add: o_assoc) + from \p permutes insert x S\ have \q permutes S\ + by (simp add: q_def permutes_insert_lemma) + then have \q permutes insert x S\ + by (simp add: permutes_imp_permutes_insert) + from \q permutes S\ have \P q\ + by (auto intro: insert.IH insert.prems(2) permutes_imp_permutes_insert) + have \x \ insert x S\ + by simp + moreover from \p permutes insert x S\ have \p x \ insert x S\ + using permutes_in_image [of p \insert x S\ x] by simp + ultimately have \P (Fun.swap x (p x) id \ q)\ + using \q permutes insert x S\ \P q\ + by (rule insert.prems(2)) + then show ?case + by (simp add: swap_q) +qed + +lemma permutes_rev_induct [consumes 2, case_names id swap]: + \P p\ if \p permutes S\ \finite S\ + and id': \P id\ + and swap': \\a b p. a \ S \ b \ S \ p permutes S \ P p \ P (Fun.swap a b p)\ +using \p permutes S\ \finite S\ proof (induction rule: permutes_induct) + case id + from id' show ?case . +next + case (swap a b p) + have \P (Fun.swap (inv p a) (inv p b) p)\ + by (rule swap') (auto simp add: swap permutes_in_image permutes_inv) + also have \Fun.swap (inv p a) (inv p b) p = Fun.swap a b id \ p\ + by (rule bij_swap_comp [symmetric]) (rule permutes_bij, rule swap) + finally show ?case . +qed + + +subsection \Permutations of index set for iterated operations\ + +lemma (in comm_monoid_set) permute: + assumes "p permutes S" + shows "F g S = F (g \ p) S" +proof - + from \p permutes S\ have "inj p" + by (rule permutes_inj) + then have "inj_on p S" + by (auto intro: subset_inj_on) + then have "F g (p ` S) = F (g \ p) S" + by (rule reindex) + moreover from \p permutes S\ have "p ` S = S" + by (rule permutes_image) + ultimately show ?thesis + by simp +qed + + +subsection \Permutations as transposition sequences\ + +inductive swapidseq :: "nat \ ('a \ 'a) \ bool" + where + id[simp]: "swapidseq 0 id" + | comp_Suc: "swapidseq n p \ a \ b \ swapidseq (Suc n) (Fun.swap a b id \ p)" + +declare id[unfolded id_def, simp] + +definition "permutation p \ (\n. swapidseq n p)" + + +subsection \Some closure properties of the set of permutations, with lengths\ + +lemma permutation_id[simp]: "permutation id" + unfolding permutation_def by (rule exI[where x=0]) simp + +declare permutation_id[unfolded id_def, simp] + +lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)" + apply clarsimp + using comp_Suc[of 0 id a b] + apply simp + done + +lemma permutation_swap_id: "permutation (Fun.swap a b id)" +proof (cases "a = b") + case True + then show ?thesis by simp +next + case False + then show ?thesis + unfolding permutation_def + using swapidseq_swap[of a b] by blast +qed + + +lemma swapidseq_comp_add: "swapidseq n p \ swapidseq m q \ swapidseq (n + m) (p \ q)" +proof (induct n p arbitrary: m q rule: swapidseq.induct) + case (id m q) + then show ?case by simp +next + case (comp_Suc n p a b m q) + have eq: "Suc n + m = Suc (n + m)" + by arith + show ?case + apply (simp only: eq comp_assoc) + apply (rule swapidseq.comp_Suc) + using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) + apply blast+ + done +qed + +lemma permutation_compose: "permutation p \ permutation q \ permutation (p \ q)" + unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis + +lemma swapidseq_endswap: "swapidseq n p \ a \ b \ swapidseq (Suc n) (p \ Fun.swap a b id)" + by (induct n p rule: swapidseq.induct) + (use swapidseq_swap[of a b] in \auto simp add: comp_assoc intro: swapidseq.comp_Suc\) + +lemma swapidseq_inverse_exists: "swapidseq n p \ \q. swapidseq n q \ p \ q = id \ q \ p = id" +proof (induct n p rule: swapidseq.induct) + case id + then show ?case + by (rule exI[where x=id]) simp +next + case (comp_Suc n p a b) + from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" + by blast + let ?q = "q \ Fun.swap a b id" + note H = comp_Suc.hyps + from swapidseq_swap[of a b] H(3) have *: "swapidseq 1 (Fun.swap a b id)" + by simp + from swapidseq_comp_add[OF q(1) *] have **: "swapidseq (Suc n) ?q" + by simp + have "Fun.swap a b id \ p \ ?q = Fun.swap a b id \ (p \ q) \ Fun.swap a b id" + by (simp add: o_assoc) + also have "\ = id" + by (simp add: q(2)) + finally have ***: "Fun.swap a b id \ p \ ?q = id" . + have "?q \ (Fun.swap a b id \ p) = q \ (Fun.swap a b id \ Fun.swap a b id) \ p" + by (simp only: o_assoc) + then have "?q \ (Fun.swap a b id \ p) = id" + by (simp add: q(3)) + with ** *** show ?case + by blast +qed + +lemma swapidseq_inverse: + assumes "swapidseq n p" + shows "swapidseq n (inv p)" + using swapidseq_inverse_exists[OF assms] inv_unique_comp[of p] by auto + +lemma permutation_inverse: "permutation p \ permutation (inv p)" + using permutation_def swapidseq_inverse by blast + + + +subsection \Various combinations of transpositions with 2, 1 and 0 common elements\ + +lemma swap_id_common:" a \ c \ b \ c \ + Fun.swap a b id \ Fun.swap a c id = Fun.swap b c id \ Fun.swap a b id" + by (simp add: fun_eq_iff Fun.swap_def) + +lemma swap_id_common': "a \ b \ a \ c \ + Fun.swap a c id \ Fun.swap b c id = Fun.swap b c id \ Fun.swap a b id" + by (simp add: fun_eq_iff Fun.swap_def) + +lemma swap_id_independent: "a \ c \ a \ d \ b \ c \ b \ d \ + Fun.swap a b id \ Fun.swap c d id = Fun.swap c d id \ Fun.swap a b id" + by (simp add: fun_eq_iff Fun.swap_def) + + +subsection \The identity map only has even transposition sequences\ + +lemma symmetry_lemma: + assumes "\a b c d. P a b c d \ P a b d c" + and "\a b c d. a \ b \ c \ d \ + a = c \ b = d \ a = c \ b \ d \ a \ c \ b = d \ a \ c \ a \ d \ b \ c \ b \ d \ + P a b c d" + shows "\a b c d. a \ b \ c \ d \ P a b c d" + using assms by metis + +lemma swap_general: "a \ b \ c \ d \ + Fun.swap a b id \ Fun.swap c d id = id \ + (\x y z. x \ a \ y \ a \ z \ a \ x \ y \ + Fun.swap a b id \ Fun.swap c d id = Fun.swap x y id \ Fun.swap a z id)" +proof - + assume neq: "a \ b" "c \ d" + have "a \ b \ c \ d \ + (Fun.swap a b id \ Fun.swap c d id = id \ + (\x y z. x \ a \ y \ a \ z \ a \ x \ y \ + Fun.swap a b id \ Fun.swap c d id = Fun.swap x y id \ Fun.swap a z id))" + apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) + apply (simp_all only: swap_commute) + apply (case_tac "a = c \ b = d") + apply (clarsimp simp only: swap_commute swap_id_idempotent) + apply (case_tac "a = c \ b \ d") + apply (rule disjI2) + apply (rule_tac x="b" in exI) + apply (rule_tac x="d" in exI) + apply (rule_tac x="b" in exI) + apply (clarsimp simp add: fun_eq_iff Fun.swap_def) + apply (case_tac "a \ c \ b = d") + apply (rule disjI2) + apply (rule_tac x="c" in exI) + apply (rule_tac x="d" in exI) + apply (rule_tac x="c" in exI) + apply (clarsimp simp add: fun_eq_iff Fun.swap_def) + apply (rule disjI2) + apply (rule_tac x="c" in exI) + apply (rule_tac x="d" in exI) + apply (rule_tac x="b" in exI) + apply (clarsimp simp add: fun_eq_iff Fun.swap_def) + done + with neq show ?thesis by metis +qed + +lemma swapidseq_id_iff[simp]: "swapidseq 0 p \ p = id" + using swapidseq.cases[of 0 p "p = id"] by auto + +lemma swapidseq_cases: "swapidseq n p \ + n = 0 \ p = id \ (\a b q m. n = Suc m \ p = Fun.swap a b id \ q \ swapidseq m q \ a \ b)" + apply (rule iffI) + apply (erule swapidseq.cases[of n p]) + apply simp + apply (rule disjI2) + apply (rule_tac x= "a" in exI) + apply (rule_tac x= "b" in exI) + apply (rule_tac x= "pa" in exI) + apply (rule_tac x= "na" in exI) + apply simp + apply auto + apply (rule comp_Suc, simp_all) + done + +lemma fixing_swapidseq_decrease: + assumes "swapidseq n p" + and "a \ b" + and "(Fun.swap a b id \ p) a = a" + shows "n \ 0 \ swapidseq (n - 1) (Fun.swap a b id \ p)" + using assms +proof (induct n arbitrary: p a b) + case 0 + then show ?case + by (auto simp add: Fun.swap_def fun_upd_def) +next + case (Suc n p a b) + from Suc.prems(1) swapidseq_cases[of "Suc n" p] + obtain c d q m where + cdqm: "Suc n = Suc m" "p = Fun.swap c d id \ q" "swapidseq m q" "c \ d" "n = m" + by auto + consider "Fun.swap a b id \ Fun.swap c d id = id" + | x y z where "x \ a" "y \ a" "z \ a" "x \ y" + "Fun.swap a b id \ Fun.swap c d id = Fun.swap x y id \ Fun.swap a z id" + using swap_general[OF Suc.prems(2) cdqm(4)] by metis + then show ?case + proof cases + case 1 + then show ?thesis + by (simp only: cdqm o_assoc) (simp add: cdqm) + next + case prems: 2 + then have az: "a \ z" + by simp + from prems have *: "(Fun.swap x y id \ h) a = a \ h a = a" for h + by (simp add: Fun.swap_def) + from cdqm(2) have "Fun.swap a b id \ p = Fun.swap a b id \ (Fun.swap c d id \ q)" + by simp + then have "Fun.swap a b id \ p = Fun.swap x y id \ (Fun.swap a z id \ q)" + by (simp add: o_assoc prems) + then have "(Fun.swap a b id \ p) a = (Fun.swap x y id \ (Fun.swap a z id \ q)) a" + by simp + then have "(Fun.swap x y id \ (Fun.swap a z id \ q)) a = a" + unfolding Suc by metis + then have "(Fun.swap a z id \ q) a = a" + by (simp only: *) + from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az this] + have **: "swapidseq (n - 1) (Fun.swap a z id \ q)" "n \ 0" + by blast+ + from \n \ 0\ have ***: "Suc n - 1 = Suc (n - 1)" + by auto + show ?thesis + apply (simp only: cdqm(2) prems o_assoc ***) + apply (simp only: Suc_not_Zero simp_thms comp_assoc) + apply (rule comp_Suc) + using ** prems + apply blast+ + done + qed +qed + +lemma swapidseq_identity_even: + assumes "swapidseq n (id :: 'a \ 'a)" + shows "even n" + using \swapidseq n id\ +proof (induct n rule: nat_less_induct) + case H: (1 n) + consider "n = 0" + | a b :: 'a and q m where "n = Suc m" "id = Fun.swap a b id \ q" "swapidseq m q" "a \ b" + using H(2)[unfolded swapidseq_cases[of n id]] by auto + then show ?case + proof cases + case 1 + then show ?thesis by presburger + next + case h: 2 + from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]] + have m: "m \ 0" "swapidseq (m - 1) (id :: 'a \ 'a)" + by auto + from h m have mn: "m - 1 < n" + by arith + from H(1)[rule_format, OF mn m(2)] h(1) m(1) show ?thesis + by presburger + qed +qed + + +subsection \Therefore we have a welldefined notion of parity\ + +definition "evenperm p = even (SOME n. swapidseq n p)" + +lemma swapidseq_even_even: + assumes m: "swapidseq m p" + and n: "swapidseq n p" + shows "even m \ even n" +proof - + from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" + by blast + from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]] show ?thesis + by arith +qed + +lemma evenperm_unique: + assumes p: "swapidseq n p" + and n:"even n = b" + shows "evenperm p = b" + unfolding n[symmetric] evenperm_def + apply (rule swapidseq_even_even[where p = p]) + apply (rule someI[where x = n]) + using p + apply blast+ + done + + +subsection \And it has the expected composition properties\ + +lemma evenperm_id[simp]: "evenperm id = True" + by (rule evenperm_unique[where n = 0]) simp_all + +lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)" + by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap) + +lemma evenperm_comp: + assumes "permutation p" "permutation q" + shows "evenperm (p \ q) \ evenperm p = evenperm q" +proof - + from assms obtain n m where n: "swapidseq n p" and m: "swapidseq m q" + unfolding permutation_def by blast + have "even (n + m) \ (even n \ even m)" + by arith + from evenperm_unique[OF n refl] evenperm_unique[OF m refl] + and evenperm_unique[OF swapidseq_comp_add[OF n m] this] show ?thesis + by blast +qed + +lemma evenperm_inv: + assumes "permutation p" + shows "evenperm (inv p) = evenperm p" +proof - + from assms obtain n where n: "swapidseq n p" + unfolding permutation_def by blast + show ?thesis + by (rule evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]) +qed + + +subsection \A more abstract characterization of permutations\ + +lemma permutation_bijective: + assumes "permutation p" + shows "bij p" +proof - + from assms obtain n where n: "swapidseq n p" + unfolding permutation_def by blast + from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" + by blast + then show ?thesis + unfolding bij_iff + apply (auto simp add: fun_eq_iff) + apply metis + done +qed + +lemma permutation_finite_support: + assumes "permutation p" + shows "finite {x. p x \ x}" +proof - + from assms obtain n where "swapidseq n p" + unfolding permutation_def by blast + then show ?thesis + proof (induct n p rule: swapidseq.induct) + case id + then show ?case by simp + next + case (comp_Suc n p a b) + let ?S = "insert a (insert b {x. p x \ x})" + from comp_Suc.hyps(2) have *: "finite ?S" + by simp + from \a \ b\ have **: "{x. (Fun.swap a b id \ p) x \ x} \ ?S" + by (auto simp: Fun.swap_def) + show ?case + by (rule finite_subset[OF ** *]) + qed +qed + +lemma permutation_lemma: + assumes "finite S" + and "bij p" + and "\x. x \ S \ p x = x" + shows "permutation p" + using assms +proof (induct S arbitrary: p rule: finite_induct) + case empty + then show ?case + by simp +next + case (insert a F p) + let ?r = "Fun.swap a (p a) id \ p" + let ?q = "Fun.swap a (p a) id \ ?r" + have *: "?r a = a" + by (simp add: Fun.swap_def) + from insert * have **: "\x. x \ F \ ?r x = x" + by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3)) + have "bij ?r" + by (rule bij_swap_compose_bij[OF insert(4)]) + have "permutation ?r" + by (rule insert(3)[OF \bij ?r\ **]) + then have "permutation ?q" + by (simp add: permutation_compose permutation_swap_id) + then show ?case + by (simp add: o_assoc) +qed + +lemma permutation: "permutation p \ bij p \ finite {x. p x \ x}" + (is "?lhs \ ?b \ ?f") +proof + assume ?lhs + with permutation_bijective permutation_finite_support show "?b \ ?f" + by auto +next + assume "?b \ ?f" + then have "?f" "?b" by blast+ + from permutation_lemma[OF this] show ?lhs + by blast +qed + +lemma permutation_inverse_works: + assumes "permutation p" + shows "inv p \ p = id" + and "p \ inv p = id" + using permutation_bijective [OF assms] by (auto simp: bij_def inj_iff surj_iff) + +lemma permutation_inverse_compose: + assumes p: "permutation p" + and q: "permutation q" + shows "inv (p \ q) = inv q \ inv p" +proof - + note ps = permutation_inverse_works[OF p] + note qs = permutation_inverse_works[OF q] + have "p \ q \ (inv q \ inv p) = p \ (q \ inv q) \ inv p" + by (simp add: o_assoc) + also have "\ = id" + by (simp add: ps qs) + finally have *: "p \ q \ (inv q \ inv p) = id" . + have "inv q \ inv p \ (p \ q) = inv q \ (inv p \ p) \ q" + by (simp add: o_assoc) + also have "\ = id" + by (simp add: ps qs) + finally have **: "inv q \ inv p \ (p \ q) = id" . + show ?thesis + by (rule inv_unique_comp[OF * **]) +qed + + +subsection \Relation to \permutes\\ + +lemma permutes_imp_permutation: + \permutation p\ if \finite S\ \p permutes S\ +proof - + from \p permutes S\ have \{x. p x \ x} \ S\ + by (auto dest: permutes_not_in) + then have \finite {x. p x \ x}\ + using \finite S\ by (rule finite_subset) + moreover from \p permutes S\ have \bij p\ + by (auto dest: permutes_bij) + ultimately show ?thesis + by (simp add: permutation) +qed + +lemma permutation_permutesE: + assumes \permutation p\ + obtains S where \finite S\ \p permutes S\ +proof - + from assms have fin: \finite {x. p x \ x}\ + by (simp add: permutation) + from assms have \bij p\ + by (simp add: permutation) + also have \UNIV = {x. p x \ x} \ {x. p x = x}\ + by auto + finally have \bij_betw p {x. p x \ x} {x. p x \ x}\ + by (rule bij_betw_partition) (auto simp add: bij_betw_fixpoints) + then have \p permutes {x. p x \ x}\ + by (auto intro: bij_imp_permutes) + with fin show thesis .. +qed + +lemma permutation_permutes: "permutation p \ (\S. finite S \ p permutes S)" + by (auto elim: permutation_permutesE intro: permutes_imp_permutation) + + +subsection \Sign of a permutation as a real number\ + +definition sign :: \('a \ 'a) \ int\ \ \TODO: prefer less generic name\ + where \sign p = (if evenperm p then (1::int) else -1)\ + +lemma sign_nz: "sign p \ 0" + by (simp add: sign_def) + +lemma sign_id: "sign id = 1" + by (simp add: sign_def) + +lemma sign_inverse: "permutation p \ sign (inv p) = sign p" + by (simp add: sign_def evenperm_inv) + +lemma sign_compose: "permutation p \ permutation q \ sign (p \ q) = sign p * sign q" + by (simp add: sign_def evenperm_comp) + +lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)" + by (simp add: sign_def evenperm_swap) + +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]: + fixes xs :: "'a list" + 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 + from assms have "inj \" "surj \" + by (simp_all add: permutes_inj permutes_surj) + then show "(map_of xs \ \) x = map_of (map ?f xs) x" for x + by (induct xs) (auto simp: inv_f_f surj_f_inv_f) +qed + + +subsection \More lemmas about permutations\ + +text \The following few lemmas were contributed by Lukas Bulwahn.\ + +lemma count_image_mset_eq_card_vimage: + assumes "finite A" + shows "count (image_mset f (mset_set A)) b = card {a \ A. f a = b}" + using assms +proof (induct A) + case empty + show ?case by simp +next + case (insert x F) + show ?case + proof (cases "f x = b") + case True + with insert.hyps + have "count (image_mset f (mset_set (insert x F))) b = Suc (card {a \ F. f a = f x})" + by auto + also from insert.hyps(1,2) have "\ = card (insert x {a \ F. f a = f x})" + by simp + also from \f x = b\ have "card (insert x {a \ F. f a = f x}) = card {a \ insert x F. f a = b}" + by (auto intro: arg_cong[where f="card"]) + finally show ?thesis + using insert by auto + next + case False + then have "{a \ F. f a = b} = {a \ insert x F. f a = b}" + by auto + with insert False show ?thesis + by simp + qed +qed + +\ \Prove \image_mset_eq_implies_permutes\ ...\ +lemma image_mset_eq_implies_permutes: + fixes f :: "'a \ 'b" + assumes "finite A" + and mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)" + obtains p where "p permutes A" and "\x\A. f x = f' (p x)" +proof - + from \finite A\ have [simp]: "finite {a \ A. f a = (b::'b)}" for f b by auto + have "f ` A = f' ` A" + proof - + from \finite A\ have "f ` A = f ` (set_mset (mset_set A))" + by simp + also have "\ = f' ` set_mset (mset_set A)" + by (metis mset_eq multiset.set_map) + also from \finite A\ have "\ = f' ` A" + by simp + finally show ?thesis . + qed + have "\b\(f ` A). \p. bij_betw p {a \ A. f a = b} {a \ A. f' a = b}" + proof + fix b + from mset_eq have "count (image_mset f (mset_set A)) b = count (image_mset f' (mset_set A)) b" + by simp + with \finite A\ have "card {a \ A. f a = b} = card {a \ A. f' a = b}" + by (simp add: count_image_mset_eq_card_vimage) + then show "\p. bij_betw p {a\A. f a = b} {a \ A. f' a = b}" + by (intro finite_same_card_bij) simp_all + qed + then have "\p. \b\f ` A. bij_betw (p b) {a \ A. f a = b} {a \ A. f' a = b}" + by (rule bchoice) + then obtain p where p: "\b\f ` A. bij_betw (p b) {a \ A. f a = b} {a \ A. f' a = b}" .. + define p' where "p' = (\a. if a \ A then p (f a) a else a)" + have "p' permutes A" + proof (rule bij_imp_permutes) + have "disjoint_family_on (\i. {a \ A. f' a = i}) (f ` A)" + by (auto simp: disjoint_family_on_def) + moreover + have "bij_betw (\a. p (f a) a) {a \ A. f a = b} {a \ A. f' a = b}" if "b \ f ` A" for b + using p that by (subst bij_betw_cong[where g="p b"]) auto + ultimately + have "bij_betw (\a. p (f a) a) (\b\f ` A. {a \ A. f a = b}) (\b\f ` A. {a \ A. f' a = b})" + by (rule bij_betw_UNION_disjoint) + moreover have "(\b\f ` A. {a \ A. f a = b}) = A" + by auto + moreover from \f ` A = f' ` A\ have "(\b\f ` A. {a \ A. f' a = b}) = A" + by auto + ultimately show "bij_betw p' A A" + unfolding p'_def by (subst bij_betw_cong[where g="(\a. p (f a) a)"]) auto + next + show "\x. x \ A \ p' x = x" + by (simp add: p'_def) + qed + moreover from p have "\x\A. f x = f' (p' x)" + unfolding p'_def using bij_betwE by fastforce + ultimately show ?thesis .. +qed + +\ \... and derive the existing property:\ +lemma mset_eq_permutation: + fixes xs ys :: "'a list" + assumes mset_eq: "mset xs = mset ys" + obtains p where "p permutes {..i. xs ! i) (mset_set {..i. ys ! i) (mset_set {..i\{..i \ S. p i \ i" + shows "p = id" +proof - + have "p n = n" for n + using assms + proof (induct n arbitrary: S rule: less_induct) + case (less n) + show ?case + proof (cases "n \ S") + case False + with less(2) show ?thesis + unfolding permutes_def by metis + next + case True + with less(3) have "p n < n \ p n = n" + by auto + then show ?thesis + proof + assume "p n < n" + with less have "p (p n) = p n" + by metis + with permutes_inj[OF less(2)] have "p n = n" + unfolding inj_def by blast + with \p n < n\ have False + by simp + then show ?thesis .. + qed + qed + qed + then show ?thesis by (auto simp: fun_eq_iff) +qed + +lemma permutes_natset_ge: + fixes S :: "'a::wellorder set" + assumes p: "p permutes S" + and le: "\i \ S. p i \ i" + shows "p = id" +proof - + have "i \ inv p i" if "i \ S" for i + proof - + from that permutes_in_image[OF permutes_inv[OF p]] have "inv p i \ S" + by simp + with le have "p (inv p i) \ inv p i" + by blast + with permutes_inverses[OF p] show ?thesis + by simp + qed + then have "\i\S. inv p i \ i" + by blast + from permutes_natset_le[OF permutes_inv[OF p] this] have "inv p = inv id" + by simp + then show ?thesis + apply (subst permutes_inv_inv[OF p, symmetric]) + apply (rule inv_unique_comp) + apply simp_all + done +qed + +lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}" + apply (rule set_eqI) + apply auto + using permutes_inv_inv permutes_inv + apply auto + apply (rule_tac x="inv x" in exI) + apply auto + done + +lemma image_compose_permutations_left: + assumes "q permutes S" + shows "{q \ p |p. p permutes S} = {p. p permutes S}" + apply (rule set_eqI) + apply auto + apply (rule permutes_compose) + using assms + apply auto + apply (rule_tac x = "inv q \ x" in exI) + apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o) + done + +lemma image_compose_permutations_right: + assumes "q permutes S" + shows "{p \ q | p. p permutes S} = {p . p permutes S}" + apply (rule set_eqI) + apply auto + apply (rule permutes_compose) + using assms + apply auto + apply (rule_tac x = "x \ inv q" in exI) + apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc) + done + +lemma permutes_in_seg: "p permutes {1 ..n} \ i \ {1..n} \ 1 \ p i \ p i \ n" + by (simp add: permutes_def) metis + +lemma sum_permutations_inverse: "sum f {p. p permutes S} = sum (\p. f(inv p)) {p. p permutes S}" + (is "?lhs = ?rhs") +proof - + let ?S = "{p . p permutes S}" + have *: "inj_on inv ?S" + proof (auto simp add: inj_on_def) + fix q r + assume q: "q permutes S" + and r: "r permutes S" + and qr: "inv q = inv r" + then have "inv (inv q) = inv (inv r)" + by simp + with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r" + by metis + qed + have **: "inv ` ?S = ?S" + using image_inverse_permutations by blast + have ***: "?rhs = sum (f \ inv) ?S" + by (simp add: o_def) + from sum.reindex[OF *, of f] show ?thesis + by (simp only: ** ***) +qed + +lemma setum_permutations_compose_left: + assumes q: "q permutes S" + shows "sum f {p. p permutes S} = sum (\p. f(q \ p)) {p. p permutes S}" + (is "?lhs = ?rhs") +proof - + let ?S = "{p. p permutes S}" + have *: "?rhs = sum (f \ ((\) q)) ?S" + by (simp add: o_def) + have **: "inj_on ((\) q) ?S" + proof (auto simp add: inj_on_def) + fix p r + assume "p permutes S" + and r: "r permutes S" + and rp: "q \ p = q \ r" + then have "inv q \ q \ p = inv q \ q \ r" + by (simp add: comp_assoc) + with permutes_inj[OF q, unfolded inj_iff] show "p = r" + by simp + qed + have "((\) q) ` ?S = ?S" + using image_compose_permutations_left[OF q] by auto + with * sum.reindex[OF **, of f] show ?thesis + by (simp only:) +qed + +lemma sum_permutations_compose_right: + assumes q: "q permutes S" + shows "sum f {p. p permutes S} = sum (\p. f(p \ q)) {p. p permutes S}" + (is "?lhs = ?rhs") +proof - + let ?S = "{p. p permutes S}" + have *: "?rhs = sum (f \ (\p. p \ q)) ?S" + by (simp add: o_def) + have **: "inj_on (\p. p \ q) ?S" + proof (auto simp add: inj_on_def) + fix p r + assume "p permutes S" + and r: "r permutes S" + and rp: "p \ q = r \ q" + then have "p \ (q \ inv q) = r \ (q \ inv q)" + by (simp add: o_assoc) + with permutes_surj[OF q, unfolded surj_iff] show "p = r" + by simp + qed + from image_compose_permutations_right[OF q] have "(\p. p \ q) ` ?S = ?S" + by auto + with * sum.reindex[OF **, of f] show ?thesis + by (simp only:) +qed + + +subsection \Sum over a set of permutations (could generalize to iteration)\ + +lemma sum_over_permutations_insert: + assumes fS: "finite S" + and aS: "a \ S" + shows "sum f {p. p permutes (insert a S)} = + sum (\b. sum (\q. f (Fun.swap a b id \ q)) {p. p permutes S}) (insert a S)" +proof - + have *: "\f a b. (\(b, p). f (Fun.swap a b id \ p)) = f \ (\(b,p). Fun.swap a b id \ p)" + by (simp add: fun_eq_iff) + have **: "\P Q. {(a, b). a \ P \ b \ Q} = P \ Q" + by blast + show ?thesis + unfolding * ** sum.cartesian_product permutes_insert + proof (rule sum.reindex) + let ?f = "(\(b, y). Fun.swap a b id \ y)" + let ?P = "{p. p permutes S}" + { + fix b c p q + assume b: "b \ insert a S" + assume c: "c \ insert a S" + assume p: "p permutes S" + assume q: "q permutes S" + assume eq: "Fun.swap a b id \ p = Fun.swap a c id \ q" + from p q aS have pa: "p a = a" and qa: "q a = a" + unfolding permutes_def by metis+ + from eq have "(Fun.swap a b id \ p) a = (Fun.swap a c id \ q) a" + by simp + then have bc: "b = c" + by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def + cong del: if_weak_cong split: if_split_asm) + from eq[unfolded bc] have "(\p. Fun.swap a c id \ p) (Fun.swap a c id \ p) = + (\p. Fun.swap a c id \ p) (Fun.swap a c id \ q)" by simp + then have "p = q" + unfolding o_assoc swap_id_idempotent by simp + with bc have "b = c \ p = q" + by blast + } + then show "inj_on ?f (insert a S \ ?P)" + unfolding inj_on_def by clarify metis + qed +qed + + +subsection \Constructing permutations from association lists\ + +definition list_permutes :: "('a \ 'a) list \ 'a set \ bool" + 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 :: "('a \ 'a) list \ 'a \ 'a" + 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 :: "('a \ 'a) list \ 'a \ 'a" + 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 x'y' have *: "(x, x') \ set xs" "(y, y') \ set xs" + by (force dest: map_of_SomeD)+ + moreover from * 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: "x \ set (map fst xs) \ permutation_of_list xs x = x" + by (induct xs) (auto simp: permutation_of_list_Cons) + +lemma permutation_of_list_unique': + "distinct (map fst xs) \ (x, y) \ set xs \ permutation_of_list xs x = y" + by (induct xs) (force simp: permutation_of_list_Cons)+ + +lemma permutation_of_list_unique: + "list_permutes xs A \ (x, y) \ set xs \ permutation_of_list xs x = y" + by (intro permutation_of_list_unique') (simp_all add: list_permutes_def) + +lemma inverse_permutation_of_list_id: + "x \ set (map snd xs) \ inverse_permutation_of_list xs x = x" + by (induct xs) auto + +lemma inverse_permutation_of_list_unique': + "distinct (map snd xs) \ (x, y) \ set xs \ inverse_permutation_of_list xs y = x" + by (induct xs) (force simp: inverse_permutation_of_list.simps(2))+ + +lemma inverse_permutation_of_list_unique: + "list_permutes xs A \ (x,y) \ set xs \ inverse_permutation_of_list xs y = x" + by (intro inverse_permutation_of_list_unique') (simp_all add: list_permutes_def) + +lemma inverse_permutation_of_list_correct: + fixes A :: "'a set" + assumes "list_permutes xs A" + 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 + show "permutation_of_list xs (inverse_permutation_of_list xs x) = x" for x + proof (cases "x \ set (map snd xs)") + case True + then obtain y where "(y, x) \ set xs" by auto + with assms show ?thesis + by (simp add: inverse_permutation_of_list_unique permutation_of_list_unique) + next + case False + with assms show ?thesis + by (auto simp: list_permutes_def inverse_permutation_of_list_id permutation_of_list_id) + qed +qed + +end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/Stirling.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/Stirling.thy Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,307 @@ +(* Author: Amine Chaieb + Author: Florian Haftmann + Author: Lukas Bulwahn + Author: Manuel Eberl +*) + +section \Stirling numbers of first and second kind\ + +theory Stirling +imports Main +begin + +subsection \Stirling numbers of the second kind\ + +fun Stirling :: "nat \ nat \ nat" + where + "Stirling 0 0 = 1" + | "Stirling 0 (Suc k) = 0" + | "Stirling (Suc n) 0 = 0" + | "Stirling (Suc n) (Suc k) = Suc k * Stirling n (Suc k) + Stirling n k" + +lemma Stirling_1 [simp]: "Stirling (Suc n) (Suc 0) = 1" + by (induct n) simp_all + +lemma Stirling_less [simp]: "n < k \ Stirling n k = 0" + by (induct n k rule: Stirling.induct) simp_all + +lemma Stirling_same [simp]: "Stirling n n = 1" + by (induct n) simp_all + +lemma Stirling_2_2: "Stirling (Suc (Suc n)) (Suc (Suc 0)) = 2 ^ Suc n - 1" +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + have "Stirling (Suc (Suc (Suc n))) (Suc (Suc 0)) = + 2 * Stirling (Suc (Suc n)) (Suc (Suc 0)) + Stirling (Suc (Suc n)) (Suc 0)" + by simp + also have "\ = 2 * (2 ^ Suc n - 1) + 1" + by (simp only: Suc Stirling_1) + also have "\ = 2 ^ Suc (Suc n) - 1" + proof - + have "(2::nat) ^ Suc n - 1 > 0" + by (induct n) simp_all + then have "2 * ((2::nat) ^ Suc n - 1) > 0" + by simp + then have "2 \ 2 * ((2::nat) ^ Suc n)" + by simp + with add_diff_assoc2 [of 2 "2 * 2 ^ Suc n" 1] + have "2 * 2 ^ Suc n - 2 + (1::nat) = 2 * 2 ^ Suc n + 1 - 2" . + then show ?thesis + by (simp add: nat_distrib) + qed + finally show ?case by simp +qed + +lemma Stirling_2: "Stirling (Suc n) (Suc (Suc 0)) = 2 ^ n - 1" + using Stirling_2_2 by (cases n) simp_all + + +subsection \Stirling numbers of the first kind\ + +fun stirling :: "nat \ nat \ nat" + where + "stirling 0 0 = 1" + | "stirling 0 (Suc k) = 0" + | "stirling (Suc n) 0 = 0" + | "stirling (Suc n) (Suc k) = n * stirling n (Suc k) + stirling n k" + +lemma stirling_0 [simp]: "n > 0 \ stirling n 0 = 0" + by (cases n) simp_all + +lemma stirling_less [simp]: "n < k \ stirling n k = 0" + by (induct n k rule: stirling.induct) simp_all + +lemma stirling_same [simp]: "stirling n n = 1" + by (induct n) simp_all + +lemma stirling_Suc_n_1: "stirling (Suc n) (Suc 0) = fact n" + by (induct n) auto + +lemma stirling_Suc_n_n: "stirling (Suc n) n = Suc n choose 2" + by (induct n) (auto simp add: numerals(2)) + +lemma stirling_Suc_n_2: + assumes "n \ Suc 0" + shows "stirling (Suc n) 2 = (\k=1..n. fact n div k)" + using assms +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + show ?case + proof (cases n) + case 0 + then show ?thesis + by (simp add: numerals(2)) + next + case Suc + then have geq1: "Suc 0 \ n" + by simp + have "stirling (Suc (Suc n)) 2 = Suc n * stirling (Suc n) 2 + stirling (Suc n) (Suc 0)" + by (simp only: stirling.simps(4)[of "Suc n"] numerals(2)) + also have "\ = Suc n * (\k=1..n. fact n div k) + fact n" + using Suc.hyps[OF geq1] + by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult) + also have "\ = Suc n * (\k=1..n. fact n div k) + Suc n * fact n div Suc n" + by (metis nat.distinct(1) nonzero_mult_div_cancel_left) + also have "\ = (\k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n" + by (simp add: sum_distrib_left div_mult_swap dvd_fact) + also have "\ = (\k=1..Suc n. fact (Suc n) div k)" + by simp + finally show ?thesis . + qed +qed + +lemma of_nat_stirling_Suc_n_2: + assumes "n \ Suc 0" + shows "(of_nat (stirling (Suc n) 2)::'a::field_char_0) = fact n * (\k=1..n. (1 / of_nat k))" + using assms +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + show ?case + proof (cases n) + case 0 + then show ?thesis + by (auto simp add: numerals(2)) + next + case Suc + then have geq1: "Suc 0 \ n" + by simp + have "(of_nat (stirling (Suc (Suc n)) 2)::'a) = + of_nat (Suc n * stirling (Suc n) 2 + stirling (Suc n) (Suc 0))" + by (simp only: stirling.simps(4)[of "Suc n"] numerals(2)) + also have "\ = of_nat (Suc n) * (fact n * (\k = 1..n. 1 / of_nat k)) + fact n" + using Suc.hyps[OF geq1] + by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult) + also have "\ = fact (Suc n) * (\k = 1..n. 1 / of_nat k) + fact (Suc n) * (1 / of_nat (Suc n))" + using of_nat_neq_0 by auto + also have "\ = fact (Suc n) * (\k = 1..Suc n. 1 / of_nat k)" + by (simp add: distrib_left) + finally show ?thesis . + qed +qed + +lemma sum_stirling: "(\k\n. stirling n k) = fact n" +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + have "(\k\Suc n. stirling (Suc n) k) = stirling (Suc n) 0 + (\k\n. stirling (Suc n) (Suc k))" + by (simp only: sum.atMost_Suc_shift) + also have "\ = (\k\n. stirling (Suc n) (Suc k))" + by simp + also have "\ = (\k\n. n * stirling n (Suc k) + stirling n k)" + by simp + also have "\ = n * (\k\n. stirling n (Suc k)) + (\k\n. stirling n k)" + by (simp add: sum.distrib sum_distrib_left) + also have "\ = n * fact n + fact n" + proof - + have "n * (\k\n. stirling n (Suc k)) = n * ((\k\Suc n. stirling n k) - stirling n 0)" + by (metis add_diff_cancel_left' sum.atMost_Suc_shift) + also have "\ = n * (\k\n. stirling n k)" + by (cases n) simp_all + also have "\ = n * fact n" + using Suc.hyps by simp + finally have "n * (\k\n. stirling n (Suc k)) = n * fact n" . + moreover have "(\k\n. stirling n k) = fact n" + using Suc.hyps . + ultimately show ?thesis by simp + qed + also have "\ = fact (Suc n)" by simp + finally show ?case . +qed + +lemma stirling_pochhammer: + "(\k\n. of_nat (stirling n k) * x ^ k) = (pochhammer x n :: 'a::comm_semiring_1)" +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + have "of_nat (n * stirling n 0) = (0 :: 'a)" by (cases n) simp_all + then have "(\k\Suc n. of_nat (stirling (Suc n) k) * x ^ k) = + (of_nat (n * stirling n 0) * x ^ 0 + + (\i\n. of_nat (n * stirling n (Suc i)) * (x ^ Suc i))) + + (\i\n. of_nat (stirling n i) * (x ^ Suc i))" + by (subst sum.atMost_Suc_shift) (simp add: sum.distrib ring_distribs) + also have "\ = pochhammer x (Suc n)" + by (subst sum.atMost_Suc_shift [symmetric]) + (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc flip: Suc) + finally show ?case . +qed + + +text \A row of the Stirling number triangle\ + +definition stirling_row :: "nat \ nat list" + where "stirling_row n = [stirling n k. k \ [0.. n \ stirling_row n ! k = stirling n k" + by (simp add: stirling_row_def del: upt_Suc) + +lemma length_stirling_row [simp]: "length (stirling_row n) = Suc n" + by (simp add: stirling_row_def) + +lemma stirling_row_nonempty [simp]: "stirling_row n \ []" + using length_stirling_row[of n] by (auto simp del: length_stirling_row) + + +subsubsection \Efficient code\ + +text \ + Naively using the defining equations of the Stirling numbers of the first + kind to compute them leads to exponential run time due to repeated + computations. We can use memoisation to compute them row by row without + repeating computations, at the cost of computing a few unneeded values. + + As a bonus, this is very efficient for applications where an entire row of + Stirling numbers is needed. +\ + +definition zip_with_prev :: "('a \ 'a \ 'b) \ 'a \ 'a list \ 'b list" + where "zip_with_prev f x xs = map2 f (x # xs) xs" + +lemma zip_with_prev_altdef: + "zip_with_prev f x xs = + (if xs = [] then [] else f x (hd xs) # [f (xs!i) (xs!(i+1)). i \ [0..i. f (xs ! i) (xs ! (i + 1))) [0..a b. a + n * b) y xs @ [1]" + by (induct xs arbitrary: y) (simp_all add: zip_with_prev_def) + +lemma stirling_row_code [code]: + "stirling_row 0 = [1]" + "stirling_row (Suc n) = stirling_row_aux n 0 (stirling_row n)" +proof goal_cases + case 1 + show ?case by (simp add: stirling_row_def) +next + case 2 + have "stirling_row (Suc n) = + 0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \ [0.. Suc n" + by simp + then consider "i = 0 \ i = Suc n" | "i > 0" "i \ n" + by linarith + then show ?case + proof cases + case 1 + then show ?thesis + by (auto simp: nth_stirling_row nth_append) + next + case 2 + then show ?thesis + by (cases i) (simp_all add: nth_append nth_stirling_row) + qed + next + case length + then show ?case by simp + qed + also have "0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \ [0..a b. a + n * b) 0 (stirling_row n) @ [1]" + by (cases n) (auto simp add: zip_with_prev_altdef stirling_row_def hd_map simp del: upt_Suc) + also have "\ = stirling_row_aux n 0 (stirling_row n)" + by (simp add: stirling_row_aux_correct) + finally show ?case . +qed + +lemma stirling_code [code]: + "stirling n k = + (if k = 0 then (if n = 0 then 1 else 0) + else if k > n then 0 + else if k = n then 1 + else stirling_row n ! k)" + by (simp add: nth_stirling_row) + +end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Combinatorics/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Combinatorics/document/root.tex Thu Mar 25 08:52:15 2021 +0000 @@ -0,0 +1,23 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} + +\isabellestyle{literal} +\usepackage{pdfsetup}\urlstyle{rm} + + +\hyphenation{Isabelle} + +\begin{document} + +\title{Basic combinatorics in Isabelle/HOL (and the Archive of Formal Proofs)} +\maketitle + +\tableofcontents + +\parindent 0pt \parskip 0.5ex + +\input{session} + +\end{document} diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Library/Disjoint_FSets.thy --- a/src/HOL/Library/Disjoint_FSets.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Library/Disjoint_FSets.thy Thu Mar 25 08:52:15 2021 +0000 @@ -1,5 +1,4 @@ -(* Title: HOL/Library/Disjoint_FSets.thy - Author: Lars Hupel, TU München +(* Author: Lars Hupel, TU München *) section \Disjoint FSets\ @@ -7,7 +6,7 @@ theory Disjoint_FSets imports "HOL-Library.Finite_Map" - "HOL-Library.Disjoint_Sets" + Disjoint_Sets begin context diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Library/Disjoint_Sets.thy --- a/src/HOL/Library/Disjoint_Sets.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Library/Disjoint_Sets.thy Thu Mar 25 08:52:15 2021 +0000 @@ -1,5 +1,4 @@ -(* Title: HOL/Library/Disjoint_Sets.thy - Author: Johannes Hölzl, TU München +(* Author: Johannes Hölzl, TU München *) section \Partitions and Disjoint Sets\ diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Library/Library.thy Thu Mar 25 08:52:15 2021 +0000 @@ -51,13 +51,11 @@ Lattice_Constructions Linear_Temporal_Logic_on_Streams ListVector - List_Permutation Lub_Glb Mapping Monad_Syntax More_List Multiset_Order - Multiset_Permutations Nonpos_Ints Numeral_Type Omega_Words_Fun @@ -68,7 +66,6 @@ Pattern_Aliases Periodic_Fun Perm - Permutations Poly_Mapping Power_By_Squaring Preorder @@ -89,7 +86,6 @@ Set_Idioms Signed_Division State_Monad - Stirling Stream Sorting_Algorithms Sublist diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Library/List_Permutation.thy --- a/src/HOL/Library/List_Permutation.thy Wed Mar 24 21:17:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,185 +0,0 @@ -(* Title: HOL/Library/List_Permutation.thy - Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker -*) - -section \Permuted Lists\ - -theory List_Permutation -imports Permutations -begin - -text \ - Note that multisets already provide the notion of permutated list and hence - this theory mostly echoes material already logically present in theory - \<^text>\Permutations\; it should be seldom needed. -\ - -subsection \An inductive definition \ldots\ - -inductive perm :: "'a list \ 'a list \ bool" (infixr \<~~>\ 50) -where - Nil [intro!]: "[] <~~> []" -| swap [intro!]: "y # x # l <~~> x # y # l" -| Cons [intro!]: "xs <~~> ys \ z # xs <~~> z # ys" -| trans [intro]: "xs <~~> ys \ ys <~~> zs \ xs <~~> zs" - -proposition perm_refl [iff]: "l <~~> l" - by (induct l) auto - -text \\ldots that is equivalent to an already existing notion:\ - -lemma perm_iff_eq_mset: - \xs <~~> ys \ mset xs = mset ys\ -proof - assume \mset xs = mset ys\ - then show \xs <~~> ys\ - proof (induction xs arbitrary: ys) - case Nil - then show ?case - by simp - next - case (Cons x xs) - from Cons.prems [symmetric] have \mset xs = mset (remove1 x ys)\ - by simp - then have \xs <~~> remove1 x ys\ - by (rule Cons.IH) - then have \x # xs <~~> x # remove1 x ys\ - by (rule perm.Cons) - moreover from Cons.prems have \x \ set ys\ - by (auto dest: union_single_eq_member) - then have \x # remove1 x ys <~~> ys\ - by (induction ys) auto - ultimately show \x # xs <~~> ys\ - by (rule perm.trans) - qed -next - assume \xs <~~> ys\ - then show \mset xs = mset ys\ - by induction simp_all -qed - -theorem mset_eq_perm: \mset xs = mset ys \ xs <~~> ys\ - by (simp add: perm_iff_eq_mset) - - -subsection \Nontrivial conclusions\ - -proposition perm_swap: - \xs[i := xs ! j, j := xs ! i] <~~> xs\ - if \i < length xs\ \j < length xs\ - using that by (simp add: perm_iff_eq_mset mset_swap) - -proposition mset_le_perm_append: "mset xs \# mset ys \ (\zs. xs @ zs <~~> ys)" - by (auto simp add: perm_iff_eq_mset mset_subset_eq_exists_conv ex_mset dest: sym) - -proposition perm_set_eq: "xs <~~> ys \ set xs = set ys" - by (rule mset_eq_setD) (simp add: perm_iff_eq_mset) - -proposition perm_distinct_iff: "xs <~~> ys \ distinct xs \ distinct ys" - by (rule mset_eq_imp_distinct_iff) (simp add: perm_iff_eq_mset) - -theorem eq_set_perm_remdups: "set xs = set ys \ remdups xs <~~> remdups ys" - by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) - -proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \ set x = set y" - by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) - -theorem permutation_Ex_bij: - assumes "xs <~~> ys" - shows "\f. bij_betw f {.. (\imset xs = mset ys\ \length xs = length ys\ - by (auto simp add: perm_iff_eq_mset dest: mset_eq_length) - from \mset xs = mset ys\ obtain p where \p permutes {.. \permute_list p ys = xs\ - by (rule mset_eq_permutation) - then have \bij_betw p {.. - by (simp add: \length xs = length ys\ permutes_imp_bij) - moreover have \\i - using \permute_list p ys = xs\ \length xs = length ys\ \p permutes {.. permute_list_nth - by auto - ultimately show ?thesis - by blast -qed - -proposition perm_finite: "finite {B. B <~~> A}" - using mset_eq_finite by (auto simp add: perm_iff_eq_mset) - - -subsection \Trivial conclusions:\ - -proposition perm_empty_imp: "[] <~~> ys \ ys = []" - by (simp add: perm_iff_eq_mset) - - -text \\medskip This more general theorem is easier to understand!\ - -proposition perm_length: "xs <~~> ys \ length xs = length ys" - by (rule mset_eq_length) (simp add: perm_iff_eq_mset) - -proposition perm_sym: "xs <~~> ys \ ys <~~> xs" - by (simp add: perm_iff_eq_mset) - - -text \We can insert the head anywhere in the list.\ - -proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" - by (simp add: perm_iff_eq_mset) - -proposition perm_append_swap: "xs @ ys <~~> ys @ xs" - by (simp add: perm_iff_eq_mset) - -proposition perm_append_single: "a # xs <~~> xs @ [a]" - by (simp add: perm_iff_eq_mset) - -proposition perm_rev: "rev xs <~~> xs" - by (simp add: perm_iff_eq_mset) - -proposition perm_append1: "xs <~~> ys \ l @ xs <~~> l @ ys" - by (simp add: perm_iff_eq_mset) - -proposition perm_append2: "xs <~~> ys \ xs @ l <~~> ys @ l" - by (simp add: perm_iff_eq_mset) - -proposition perm_empty [iff]: "[] <~~> xs \ xs = []" - by (simp add: perm_iff_eq_mset) - -proposition perm_empty2 [iff]: "xs <~~> [] \ xs = []" - by (simp add: perm_iff_eq_mset) - -proposition perm_sing_imp: "ys <~~> xs \ xs = [y] \ ys = [y]" - by (simp add: perm_iff_eq_mset) - -proposition perm_sing_eq [iff]: "ys <~~> [y] \ ys = [y]" - by (simp add: perm_iff_eq_mset) - -proposition perm_sing_eq2 [iff]: "[y] <~~> ys \ ys = [y]" - by (simp add: perm_iff_eq_mset) - -proposition perm_remove: "x \ set ys \ ys <~~> x # remove1 x ys" - by (simp add: perm_iff_eq_mset) - - -text \\medskip Congruence rule\ - -proposition perm_remove_perm: "xs <~~> ys \ remove1 z xs <~~> remove1 z ys" - by (simp add: perm_iff_eq_mset) - -proposition remove_hd [simp]: "remove1 z (z # xs) = xs" - by (simp add: perm_iff_eq_mset) - -proposition cons_perm_imp_perm: "z # xs <~~> z # ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) - -proposition cons_perm_eq [simp]: "z#xs <~~> z#ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) - -proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) - -proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) - -proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) - -end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Library/Multiset_Permutations.thy --- a/src/HOL/Library/Multiset_Permutations.thy Wed Mar 24 21:17:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,515 +0,0 @@ -(* Title: HOL/Library/Multiset_Permutations.thy - Author: Manuel Eberl (TU München) - -Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose -entries correspond to the multiset (resp. set). -*) - -section \Permutations of a Multiset\ - -theory Multiset_Permutations -imports - Complex_Main - Multiset - Permutations -begin - -(* TODO Move *) -lemma mset_tl: "xs \ [] \ mset (tl xs) = mset xs - {#hd xs#}" - by (cases xs) simp_all - -lemma mset_set_image_inj: - assumes "inj_on f A" - shows "mset_set (f ` A) = image_mset f (mset_set A)" -proof (cases "finite A") - case True - from this and assms show ?thesis by (induction A) auto -qed (insert assms, simp add: finite_image_iff) - -lemma multiset_remove_induct [case_names empty remove]: - assumes "P {#}" "\A. A \ {#} \ (\x. x \# A \ P (A - {#x#})) \ P A" - shows "P A" -proof (induction A rule: full_multiset_induct) - case (less A) - hence IH: "P B" if "B \# A" for B using that by blast - show ?case - proof (cases "A = {#}") - case True - thus ?thesis by (simp add: assms) - next - case False - hence "P (A - {#x#})" if "x \# A" for x - using that by (intro IH) (simp add: mset_subset_diff_self) - from False and this show "P A" by (rule assms) - qed -qed - -lemma map_list_bind: "map g (List.bind xs f) = List.bind xs (map g \ f)" - by (simp add: List.bind_def map_concat) - -lemma mset_eq_mset_set_imp_distinct: - "finite A \ mset_set A = mset xs \ distinct xs" -proof (induction xs arbitrary: A) - case (Cons x xs A) - from Cons.prems(2) have "x \# mset_set A" by simp - with Cons.prems(1) have [simp]: "x \ A" by simp - from Cons.prems have "x \# mset_set (A - {x})" by simp - also from Cons.prems have "mset_set (A - {x}) = mset_set A - {#x#}" - by (subst mset_set_Diff) simp_all - also have "mset_set A = mset (x#xs)" by (simp add: Cons.prems) - also have "\ - {#x#} = mset xs" by simp - finally have [simp]: "x \ set xs" by (simp add: in_multiset_in_set) - from Cons.prems show ?case by (auto intro!: Cons.IH[of "A - {x}"] simp: mset_set_Diff) -qed simp_all -(* END TODO *) - - -subsection \Permutations of a multiset\ - -definition permutations_of_multiset :: "'a multiset \ 'a list set" where - "permutations_of_multiset A = {xs. mset xs = A}" - -lemma permutations_of_multisetI: "mset xs = A \ xs \ permutations_of_multiset A" - by (simp add: permutations_of_multiset_def) - -lemma permutations_of_multisetD: "xs \ permutations_of_multiset A \ mset xs = A" - by (simp add: permutations_of_multiset_def) - -lemma permutations_of_multiset_Cons_iff: - "x # xs \ permutations_of_multiset A \ x \# A \ xs \ permutations_of_multiset (A - {#x#})" - by (auto simp: permutations_of_multiset_def) - -lemma permutations_of_multiset_empty [simp]: "permutations_of_multiset {#} = {[]}" - unfolding permutations_of_multiset_def by simp - -lemma permutations_of_multiset_nonempty: - assumes nonempty: "A \ {#}" - shows "permutations_of_multiset A = - (\x\set_mset A. ((#) x) ` permutations_of_multiset (A - {#x#}))" (is "_ = ?rhs") -proof safe - fix xs assume "xs \ permutations_of_multiset A" - hence mset_xs: "mset xs = A" by (simp add: permutations_of_multiset_def) - hence "xs \ []" by (auto simp: nonempty) - then obtain x xs' where xs: "xs = x # xs'" by (cases xs) simp_all - with mset_xs have "x \ set_mset A" "xs' \ permutations_of_multiset (A - {#x#})" - by (auto simp: permutations_of_multiset_def) - with xs show "xs \ ?rhs" by auto -qed (auto simp: permutations_of_multiset_def) - -lemma permutations_of_multiset_singleton [simp]: "permutations_of_multiset {#x#} = {[x]}" - by (simp add: permutations_of_multiset_nonempty) - -lemma permutations_of_multiset_doubleton: - "permutations_of_multiset {#x,y#} = {[x,y], [y,x]}" - by (simp add: permutations_of_multiset_nonempty insert_commute) - -lemma rev_permutations_of_multiset [simp]: - "rev ` permutations_of_multiset A = permutations_of_multiset A" -proof - have "rev ` rev ` permutations_of_multiset A \ rev ` permutations_of_multiset A" - unfolding permutations_of_multiset_def by auto - also have "rev ` rev ` permutations_of_multiset A = permutations_of_multiset A" - by (simp add: image_image) - finally show "permutations_of_multiset A \ rev ` permutations_of_multiset A" . -next - show "rev ` permutations_of_multiset A \ permutations_of_multiset A" - unfolding permutations_of_multiset_def by auto -qed - -lemma length_finite_permutations_of_multiset: - "xs \ permutations_of_multiset A \ length xs = size A" - by (auto simp: permutations_of_multiset_def) - -lemma permutations_of_multiset_lists: "permutations_of_multiset A \ lists (set_mset A)" - by (auto simp: permutations_of_multiset_def) - -lemma finite_permutations_of_multiset [simp]: "finite (permutations_of_multiset A)" -proof (rule finite_subset) - show "permutations_of_multiset A \ {xs. set xs \ set_mset A \ length xs = size A}" - by (auto simp: permutations_of_multiset_def) - show "finite {xs. set xs \ set_mset A \ length xs = size A}" - by (rule finite_lists_length_eq) simp_all -qed - -lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \ {}" -proof - - from ex_mset[of A] guess xs .. - thus ?thesis by (auto simp: permutations_of_multiset_def) -qed - -lemma permutations_of_multiset_image: - "permutations_of_multiset (image_mset f A) = map f ` permutations_of_multiset A" -proof safe - fix xs assume A: "xs \ permutations_of_multiset (image_mset f A)" - from ex_mset[of A] obtain ys where ys: "mset ys = A" .. - with A have "mset xs = mset (map f ys)" - by (simp add: permutations_of_multiset_def) - from mset_eq_permutation[OF this] guess \ . note \ = this - with ys have "xs = map f (permute_list \ ys)" - by (simp add: permute_list_map) - moreover from \ ys have "permute_list \ ys \ permutations_of_multiset A" - by (simp add: permutations_of_multiset_def) - ultimately show "xs \ map f ` permutations_of_multiset A" by blast -qed (auto simp: permutations_of_multiset_def) - - -subsection \Cardinality of permutations\ - -text \ - In this section, we prove some basic facts about the number of permutations of a multiset. -\ - -context -begin - -private lemma multiset_prod_fact_insert: - "(\y\set_mset (A+{#x#}). fact (count (A+{#x#}) y)) = - (count A x + 1) * (\y\set_mset A. fact (count A y))" -proof - - have "(\y\set_mset (A+{#x#}). fact (count (A+{#x#}) y)) = - (\y\set_mset (A+{#x#}). (if y = x then count A x + 1 else 1) * fact (count A y))" - by (intro prod.cong) simp_all - also have "\ = (count A x + 1) * (\y\set_mset (A+{#x#}). fact (count A y))" - by (simp add: prod.distrib) - also have "(\y\set_mset (A+{#x#}). fact (count A y)) = (\y\set_mset A. fact (count A y))" - by (intro prod.mono_neutral_right) (auto simp: not_in_iff) - finally show ?thesis . -qed - -private lemma multiset_prod_fact_remove: - "x \# A \ (\y\set_mset A. fact (count A y)) = - count A x * (\y\set_mset (A-{#x#}). fact (count (A-{#x#}) y))" - using multiset_prod_fact_insert[of "A - {#x#}" x] by simp - -lemma card_permutations_of_multiset_aux: - "card (permutations_of_multiset A) * (\x\set_mset A. fact (count A x)) = fact (size A)" -proof (induction A rule: multiset_remove_induct) - case (remove A) - have "card (permutations_of_multiset A) = - card (\x\set_mset A. (#) x ` permutations_of_multiset (A - {#x#}))" - by (simp add: permutations_of_multiset_nonempty remove.hyps) - also have "\ = (\x\set_mset A. card (permutations_of_multiset (A - {#x#})))" - by (subst card_UN_disjoint) (auto simp: card_image) - also have "\ * (\x\set_mset A. fact (count A x)) = - (\x\set_mset A. card (permutations_of_multiset (A - {#x#})) * - (\y\set_mset A. fact (count A y)))" - by (subst sum_distrib_right) simp_all - also have "\ = (\x\set_mset A. count A x * fact (size A - 1))" - proof (intro sum.cong refl) - fix x assume x: "x \# A" - have "card (permutations_of_multiset (A - {#x#})) * (\y\set_mset A. fact (count A y)) = - count A x * (card (permutations_of_multiset (A - {#x#})) * - (\y\set_mset (A - {#x#}). fact (count (A - {#x#}) y)))" (is "?lhs = _") - by (subst multiset_prod_fact_remove[OF x]) simp_all - also note remove.IH[OF x] - also from x have "size (A - {#x#}) = size A - 1" by (simp add: size_Diff_submset) - finally show "?lhs = count A x * fact (size A - 1)" . - qed - also have "(\x\set_mset A. count A x * fact (size A - 1)) = - size A * fact (size A - 1)" - by (simp add: sum_distrib_right size_multiset_overloaded_eq) - also from remove.hyps have "\ = fact (size A)" - by (cases "size A") auto - finally show ?case . -qed simp_all - -theorem card_permutations_of_multiset: - "card (permutations_of_multiset A) = fact (size A) div (\x\set_mset A. fact (count A x))" - "(\x\set_mset A. fact (count A x) :: nat) dvd fact (size A)" - by (simp_all flip: card_permutations_of_multiset_aux[of A]) - -lemma card_permutations_of_multiset_insert_aux: - "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) = - (size A + 1) * card (permutations_of_multiset A)" -proof - - note card_permutations_of_multiset_aux[of "A + {#x#}"] - also have "fact (size (A + {#x#})) = (size A + 1) * fact (size A)" by simp - also note multiset_prod_fact_insert[of A x] - also note card_permutations_of_multiset_aux[of A, symmetric] - finally have "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) * - (\y\set_mset A. fact (count A y)) = - (size A + 1) * card (permutations_of_multiset A) * - (\x\set_mset A. fact (count A x))" by (simp only: mult_ac) - thus ?thesis by (subst (asm) mult_right_cancel) simp_all -qed - -lemma card_permutations_of_multiset_remove_aux: - assumes "x \# A" - shows "card (permutations_of_multiset A) * count A x = - size A * card (permutations_of_multiset (A - {#x#}))" -proof - - from assms have A: "A - {#x#} + {#x#} = A" by simp - from assms have B: "size A = size (A - {#x#}) + 1" - by (subst A [symmetric], subst size_union) simp - show ?thesis - using card_permutations_of_multiset_insert_aux[of "A - {#x#}" x, unfolded A] assms - by (simp add: B) -qed - -lemma real_card_permutations_of_multiset_remove: - assumes "x \# A" - shows "real (card (permutations_of_multiset (A - {#x#}))) = - real (card (permutations_of_multiset A) * count A x) / real (size A)" - using assms by (subst card_permutations_of_multiset_remove_aux[OF assms]) auto - -lemma real_card_permutations_of_multiset_remove': - assumes "x \# A" - shows "real (card (permutations_of_multiset A)) = - real (size A * card (permutations_of_multiset (A - {#x#}))) / real (count A x)" - using assms by (subst card_permutations_of_multiset_remove_aux[OF assms, symmetric]) simp - -end - - - -subsection \Permutations of a set\ - -definition permutations_of_set :: "'a set \ 'a list set" where - "permutations_of_set A = {xs. set xs = A \ distinct xs}" - -lemma permutations_of_set_altdef: - "finite A \ permutations_of_set A = permutations_of_multiset (mset_set A)" - by (auto simp add: permutations_of_set_def permutations_of_multiset_def mset_set_set - in_multiset_in_set [symmetric] mset_eq_mset_set_imp_distinct) - -lemma permutations_of_setI [intro]: - assumes "set xs = A" "distinct xs" - shows "xs \ permutations_of_set A" - using assms unfolding permutations_of_set_def by simp - -lemma permutations_of_setD: - assumes "xs \ permutations_of_set A" - shows "set xs = A" "distinct xs" - using assms unfolding permutations_of_set_def by simp_all - -lemma permutations_of_set_lists: "permutations_of_set A \ lists A" - unfolding permutations_of_set_def by auto - -lemma permutations_of_set_empty [simp]: "permutations_of_set {} = {[]}" - by (auto simp: permutations_of_set_def) - -lemma UN_set_permutations_of_set [simp]: - "finite A \ (\xs\permutations_of_set A. set xs) = A" - using finite_distinct_list by (auto simp: permutations_of_set_def) - -lemma permutations_of_set_infinite: - "\finite A \ permutations_of_set A = {}" - by (auto simp: permutations_of_set_def) - -lemma permutations_of_set_nonempty: - "A \ {} \ permutations_of_set A = - (\x\A. (\xs. x # xs) ` permutations_of_set (A - {x}))" - by (cases "finite A") - (simp_all add: permutations_of_multiset_nonempty mset_set_empty_iff mset_set_Diff - permutations_of_set_altdef permutations_of_set_infinite) - -lemma permutations_of_set_singleton [simp]: "permutations_of_set {x} = {[x]}" - by (subst permutations_of_set_nonempty) auto - -lemma permutations_of_set_doubleton: - "x \ y \ permutations_of_set {x,y} = {[x,y], [y,x]}" - by (subst permutations_of_set_nonempty) - (simp_all add: insert_Diff_if insert_commute) - -lemma rev_permutations_of_set [simp]: - "rev ` permutations_of_set A = permutations_of_set A" - by (cases "finite A") (simp_all add: permutations_of_set_altdef permutations_of_set_infinite) - -lemma length_finite_permutations_of_set: - "xs \ permutations_of_set A \ length xs = card A" - by (auto simp: permutations_of_set_def distinct_card) - -lemma finite_permutations_of_set [simp]: "finite (permutations_of_set A)" - by (cases "finite A") (simp_all add: permutations_of_set_infinite permutations_of_set_altdef) - -lemma permutations_of_set_empty_iff [simp]: - "permutations_of_set A = {} \ \finite A" - unfolding permutations_of_set_def using finite_distinct_list[of A] by auto - -lemma card_permutations_of_set [simp]: - "finite A \ card (permutations_of_set A) = fact (card A)" - by (simp add: permutations_of_set_altdef card_permutations_of_multiset del: One_nat_def) - -lemma permutations_of_set_image_inj: - assumes inj: "inj_on f A" - shows "permutations_of_set (f ` A) = map f ` permutations_of_set A" - by (cases "finite A") - (simp_all add: permutations_of_set_infinite permutations_of_set_altdef - permutations_of_multiset_image mset_set_image_inj inj finite_image_iff) - -lemma permutations_of_set_image_permutes: - "\ permutes A \ map \ ` permutations_of_set A = permutations_of_set A" - by (subst permutations_of_set_image_inj [symmetric]) - (simp_all add: permutes_inj_on permutes_image) - - -subsection \Code generation\ - -text \ - First, we give code an implementation for permutations of lists. -\ - -declare length_remove1 [termination_simp] - -fun permutations_of_list_impl where - "permutations_of_list_impl xs = (if xs = [] then [[]] else - List.bind (remdups xs) (\x. map ((#) x) (permutations_of_list_impl (remove1 x xs))))" - -fun permutations_of_list_impl_aux where - "permutations_of_list_impl_aux acc xs = (if xs = [] then [acc] else - List.bind (remdups xs) (\x. permutations_of_list_impl_aux (x#acc) (remove1 x xs)))" - -declare permutations_of_list_impl_aux.simps [simp del] -declare permutations_of_list_impl.simps [simp del] - -lemma permutations_of_list_impl_Nil [simp]: - "permutations_of_list_impl [] = [[]]" - by (simp add: permutations_of_list_impl.simps) - -lemma permutations_of_list_impl_nonempty: - "xs \ [] \ permutations_of_list_impl xs = - List.bind (remdups xs) (\x. map ((#) x) (permutations_of_list_impl (remove1 x xs)))" - by (subst permutations_of_list_impl.simps) simp_all - -lemma set_permutations_of_list_impl: - "set (permutations_of_list_impl xs) = permutations_of_multiset (mset xs)" - by (induction xs rule: permutations_of_list_impl.induct) - (subst permutations_of_list_impl.simps, - simp_all add: permutations_of_multiset_nonempty set_list_bind) - -lemma distinct_permutations_of_list_impl: - "distinct (permutations_of_list_impl xs)" - by (induction xs rule: permutations_of_list_impl.induct, - subst permutations_of_list_impl.simps) - (auto intro!: distinct_list_bind simp: distinct_map o_def disjoint_family_on_def) - -lemma permutations_of_list_impl_aux_correct': - "permutations_of_list_impl_aux acc xs = - map (\xs. rev xs @ acc) (permutations_of_list_impl xs)" - by (induction acc xs rule: permutations_of_list_impl_aux.induct, - subst permutations_of_list_impl_aux.simps, subst permutations_of_list_impl.simps) - (auto simp: map_list_bind intro!: list_bind_cong) - -lemma permutations_of_list_impl_aux_correct: - "permutations_of_list_impl_aux [] xs = map rev (permutations_of_list_impl xs)" - by (simp add: permutations_of_list_impl_aux_correct') - -lemma distinct_permutations_of_list_impl_aux: - "distinct (permutations_of_list_impl_aux acc xs)" - by (simp add: permutations_of_list_impl_aux_correct' distinct_map - distinct_permutations_of_list_impl inj_on_def) - -lemma set_permutations_of_list_impl_aux: - "set (permutations_of_list_impl_aux [] xs) = permutations_of_multiset (mset xs)" - by (simp add: permutations_of_list_impl_aux_correct set_permutations_of_list_impl) - -declare set_permutations_of_list_impl_aux [symmetric, code] - -value [code] "permutations_of_multiset {#1,2,3,4::int#}" - - - -text \ - Now we turn to permutations of sets. We define an auxiliary version with an - accumulator to avoid having to map over the results. -\ -function permutations_of_set_aux where - "permutations_of_set_aux acc A = - (if \finite A then {} else if A = {} then {acc} else - (\x\A. permutations_of_set_aux (x#acc) (A - {x})))" -by auto -termination by (relation "Wellfounded.measure (card \ snd)") (simp_all add: card_gt_0_iff) - -lemma permutations_of_set_aux_altdef: - "permutations_of_set_aux acc A = (\xs. rev xs @ acc) ` permutations_of_set A" -proof (cases "finite A") - assume "finite A" - thus ?thesis - proof (induction A arbitrary: acc rule: finite_psubset_induct) - case (psubset A acc) - show ?case - proof (cases "A = {}") - case False - note [simp del] = permutations_of_set_aux.simps - from psubset.hyps False - have "permutations_of_set_aux acc A = - (\y\A. permutations_of_set_aux (y#acc) (A - {y}))" - by (subst permutations_of_set_aux.simps) simp_all - also have "\ = (\y\A. (\xs. rev xs @ acc) ` (\xs. y # xs) ` permutations_of_set (A - {y}))" - apply (rule arg_cong [of _ _ Union], rule image_cong) - apply (simp_all add: image_image) - apply (subst psubset) - apply auto - done - also from False have "\ = (\xs. rev xs @ acc) ` permutations_of_set A" - by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN) - finally show ?thesis . - qed simp_all - qed -qed (simp_all add: permutations_of_set_infinite) - -declare permutations_of_set_aux.simps [simp del] - -lemma permutations_of_set_aux_correct: - "permutations_of_set_aux [] A = permutations_of_set A" - by (simp add: permutations_of_set_aux_altdef) - - -text \ - In another refinement step, we define a version on lists. -\ -declare length_remove1 [termination_simp] - -fun permutations_of_set_aux_list where - "permutations_of_set_aux_list acc xs = - (if xs = [] then [acc] else - List.bind xs (\x. permutations_of_set_aux_list (x#acc) (List.remove1 x xs)))" - -definition permutations_of_set_list where - "permutations_of_set_list xs = permutations_of_set_aux_list [] xs" - -declare permutations_of_set_aux_list.simps [simp del] - -lemma permutations_of_set_aux_list_refine: - assumes "distinct xs" - shows "set (permutations_of_set_aux_list acc xs) = permutations_of_set_aux acc (set xs)" - using assms - by (induction acc xs rule: permutations_of_set_aux_list.induct) - (subst permutations_of_set_aux_list.simps, - subst permutations_of_set_aux.simps, - simp_all add: set_list_bind) - - -text \ - The permutation lists contain no duplicates if the inputs contain no duplicates. - Therefore, these functions can easily be used when working with a representation of - sets by distinct lists. - The same approach should generalise to any kind of set implementation that supports - a monadic bind operation, and since the results are disjoint, merging should be cheap. -\ -lemma distinct_permutations_of_set_aux_list: - "distinct xs \ distinct (permutations_of_set_aux_list acc xs)" - by (induction acc xs rule: permutations_of_set_aux_list.induct) - (subst permutations_of_set_aux_list.simps, - auto intro!: distinct_list_bind simp: disjoint_family_on_def - permutations_of_set_aux_list_refine permutations_of_set_aux_altdef) - -lemma distinct_permutations_of_set_list: - "distinct xs \ distinct (permutations_of_set_list xs)" - by (simp add: permutations_of_set_list_def distinct_permutations_of_set_aux_list) - -lemma permutations_of_list: - "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" - by (simp add: permutations_of_set_aux_correct [symmetric] - permutations_of_set_aux_list_refine permutations_of_set_list_def) - -lemma permutations_of_list_code [code]: - "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))" - "permutations_of_set (List.coset xs) = - Code.abort (STR ''Permutation of set complement not supported'') - (\_. permutations_of_set (List.coset xs))" - by (simp_all add: permutations_of_list) - -value [code] "permutations_of_set (set ''abcd'')" - -end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Wed Mar 24 21:17:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1627 +0,0 @@ -(* Title: HOL/Library/Permutations.thy - Author: Amine Chaieb, University of Cambridge -*) - -section \Permutations, both general and specifically on finite sets.\ - -theory Permutations - imports Multiset Disjoint_Sets -begin - -subsection \Auxiliary\ - -abbreviation (input) fixpoints :: \('a \ 'a) \ 'a set\ - where \fixpoints f \ {x. f x = x}\ - -lemma inj_on_fixpoints: - \inj_on f (fixpoints f)\ - by (rule inj_onI) simp - -lemma bij_betw_fixpoints: - \bij_betw f (fixpoints f) (fixpoints f)\ - using inj_on_fixpoints by (auto simp add: bij_betw_def) - - -subsection \Basic definition and consequences\ - -definition permutes :: \('a \ 'a) \ 'a set \ bool\ (infixr \permutes\ 41) - where \p permutes S \ (\x. x \ S \ p x = x) \ (\y. \!x. p x = y)\ - -lemma bij_imp_permutes: - \p permutes S\ if \bij_betw p S S\ and stable: \\x. x \ S \ p x = x\ -proof - - note \bij_betw p S S\ - moreover have \bij_betw p (- S) (- S)\ - by (auto simp add: stable intro!: bij_betw_imageI inj_onI) - ultimately have \bij_betw p (S \ - S) (S \ - S)\ - by (rule bij_betw_combine) simp - then have \\!x. p x = y\ for y - by (simp add: bij_iff) - with stable show ?thesis - by (simp add: permutes_def) -qed - -context - fixes p :: \'a \ 'a\ and S :: \'a set\ - assumes perm: \p permutes S\ -begin - -lemma permutes_inj: - \inj p\ - using perm by (auto simp: permutes_def inj_on_def) - -lemma permutes_image: - \p ` S = S\ -proof (rule set_eqI) - fix x - show \x \ p ` S \ x \ S\ - proof - assume \x \ p ` S\ - then obtain y where \y \ S\ \p y = x\ - by blast - with perm show \x \ S\ - by (cases \y = x\) (auto simp add: permutes_def) - next - assume \x \ S\ - with perm obtain y where \y \ S\ \p y = x\ - by (metis permutes_def) - then show \x \ p ` S\ - by blast - qed -qed - -lemma permutes_not_in: - \x \ S \ p x = x\ - using perm by (auto simp: permutes_def) - -lemma permutes_image_complement: - \p ` (- S) = - S\ - by (auto simp add: permutes_not_in) - -lemma permutes_in_image: - \p x \ S \ x \ S\ - using permutes_image permutes_inj by (auto dest: inj_image_mem_iff) - -lemma permutes_surj: - \surj p\ -proof - - have \p ` (S \ - S) = p ` S \ p ` (- S)\ - by (rule image_Un) - then show ?thesis - by (simp add: permutes_image permutes_image_complement) -qed - -lemma permutes_inv_o: - shows "p \ inv p = id" - and "inv p \ p = id" - using permutes_inj permutes_surj - unfolding inj_iff [symmetric] surj_iff [symmetric] by auto - -lemma permutes_inverses: - shows "p (inv p x) = x" - and "inv p (p x) = x" - using permutes_inv_o [unfolded fun_eq_iff o_def] by auto - -lemma permutes_inv_eq: - \inv p y = x \ p x = y\ - by (auto simp add: permutes_inverses) - -lemma permutes_inj_on: - \inj_on p A\ - by (rule inj_on_subset [of _ UNIV]) (auto intro: permutes_inj) - -lemma permutes_bij: - \bij p\ - unfolding bij_def by (metis permutes_inj permutes_surj) - -lemma permutes_imp_bij: - \bij_betw p S S\ - by (simp add: bij_betw_def permutes_image permutes_inj_on) - -lemma permutes_subset: - \p permutes T\ if \S \ T\ -proof (rule bij_imp_permutes) - define R where \R = T - S\ - with that have \T = R \ S\ \R \ S = {}\ - by auto - then have \p x = x\ if \x \ R\ for x - using that by (auto intro: permutes_not_in) - then have \p ` R = R\ - by simp - with \T = R \ S\ show \bij_betw p T T\ - by (simp add: bij_betw_def permutes_inj_on image_Un permutes_image) - fix x - assume \x \ T\ - with \T = R \ S\ show \p x = x\ - by (simp add: permutes_not_in) -qed - -lemma permutes_imp_permutes_insert: - \p permutes insert x S\ - by (rule permutes_subset) auto - -end - -lemma permutes_id [simp]: - \id permutes S\ - by (auto intro: bij_imp_permutes) - -lemma permutes_empty [simp]: - \p permutes {} \ p = id\ -proof - assume \p permutes {}\ - then show \p = id\ - by (auto simp add: fun_eq_iff permutes_not_in) -next - assume \p = id\ - then show \p permutes {}\ - by simp -qed - -lemma permutes_sing [simp]: - \p permutes {a} \ p = id\ -proof - assume perm: \p permutes {a}\ - show \p = id\ - proof - fix x - from perm have \p ` {a} = {a}\ - by (rule permutes_image) - with perm show \p x = id x\ - by (cases \x = a\) (auto simp add: permutes_not_in) - qed -next - assume \p = id\ - then show \p permutes {a}\ - by simp -qed - -lemma permutes_univ: "p permutes UNIV \ (\y. \!x. p x = y)" - by (simp add: permutes_def) - -lemma permutes_swap_id: "a \ S \ b \ S \ Fun.swap a b id permutes S" - by (rule bij_imp_permutes) (auto simp add: swap_id_eq) - -lemma permutes_superset: - \p permutes T\ if \p permutes S\ \\x. x \ S - T \ p x = x\ -proof - - define R U where \R = T \ S\ and \U = S - T\ - then have \T = R \ (T - S)\ \S = R \ U\ \R \ U = {}\ - by auto - from that \U = S - T\ have \p ` U = U\ - by simp - from \p permutes S\ have \bij_betw p (R \ U) (R \ U)\ - by (simp add: permutes_imp_bij \S = R \ U\) - moreover have \bij_betw p U U\ - using that \U = S - T\ by (simp add: bij_betw_def permutes_inj_on) - ultimately have \bij_betw p R R\ - using \R \ U = {}\ \R \ U = {}\ by (rule bij_betw_partition) - then have \p permutes R\ - proof (rule bij_imp_permutes) - fix x - assume \x \ R\ - with \R = T \ S\ \p permutes S\ show \p x = x\ - by (cases \x \ S\) (auto simp add: permutes_not_in that(2)) - qed - then have \p permutes R \ (T - S)\ - by (rule permutes_subset) simp - with \T = R \ (T - S)\ show ?thesis - by simp -qed - -lemma permutes_bij_inv_into: \<^marker>\contributor \Lukas Bulwahn\\ - fixes A :: "'a set" - and B :: "'b set" - assumes "p permutes A" - and "bij_betw f A B" - shows "(\x. if x \ B then f (p (inv_into A f x)) else x) permutes B" -proof (rule bij_imp_permutes) - from assms have "bij_betw p A A" "bij_betw f A B" "bij_betw (inv_into A f) B A" - by (auto simp add: permutes_imp_bij bij_betw_inv_into) - then have "bij_betw (f \ p \ inv_into A f) B B" - by (simp add: bij_betw_trans) - then show "bij_betw (\x. if x \ B then f (p (inv_into A f x)) else x) B B" - by (subst bij_betw_cong[where g="f \ p \ inv_into A f"]) auto -next - fix x - assume "x \ B" - then show "(if x \ B then f (p (inv_into A f x)) else x) = x" by auto -qed - -lemma permutes_image_mset: \<^marker>\contributor \Lukas Bulwahn\\ - assumes "p permutes A" - shows "image_mset p (mset_set A) = mset_set A" - using assms by (metis image_mset_mset_set bij_betw_imp_inj_on permutes_imp_bij permutes_image) - -lemma permutes_implies_image_mset_eq: \<^marker>\contributor \Lukas Bulwahn\\ - assumes "p permutes A" "\x. x \ A \ f x = f' (p x)" - shows "image_mset f' (mset_set A) = image_mset f (mset_set A)" -proof - - have "f x = f' (p x)" if "x \# mset_set A" for x - using assms(2)[of x] that by (cases "finite A") auto - with assms have "image_mset f (mset_set A) = image_mset (f' \ p) (mset_set A)" - by (auto intro!: image_mset_cong) - also have "\ = image_mset f' (image_mset p (mset_set A))" - by (simp add: image_mset.compositionality) - also have "\ = image_mset f' (mset_set A)" - proof - - from assms permutes_image_mset have "image_mset p (mset_set A) = mset_set A" - by blast - then show ?thesis by simp - qed - finally show ?thesis .. -qed - - -subsection \Group properties\ - -lemma permutes_compose: "p permutes S \ q permutes S \ q \ p permutes S" - unfolding permutes_def o_def by metis - -lemma permutes_inv: - assumes "p permutes S" - shows "inv p permutes S" - using assms unfolding permutes_def permutes_inv_eq[OF assms] by metis - -lemma permutes_inv_inv: - assumes "p permutes S" - shows "inv (inv p) = p" - unfolding fun_eq_iff permutes_inv_eq[OF assms] permutes_inv_eq[OF permutes_inv[OF assms]] - 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 - show "inv p x = p' x" for x - proof (cases "x \ S") - case True - from assms have "p' x = p' (p (inv p x))" - by (simp add: permutes_inverses) - also from permutes_inv[OF perm] True have "\ = inv p x" - by (subst inv) (simp_all add: permutes_in_image) - finally show ?thesis .. - next - case False - with permutes_inv[OF perm] show ?thesis - by (simp_all add: outside permutes_not_in) - qed -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 \Mapping permutations with bijections\ - -lemma bij_betw_permutations: - assumes "bij_betw f A B" - shows "bij_betw (\\ x. if x \ B then f (\ (inv_into A f x)) else x) - {\. \ permutes A} {\. \ permutes B}" (is "bij_betw ?f _ _") -proof - - let ?g = "(\\ x. if x \ A then inv_into A f (\ (f x)) else x)" - show ?thesis - proof (rule bij_betw_byWitness [of _ ?g], goal_cases) - case 3 - show ?case using permutes_bij_inv_into[OF _ assms] by auto - next - case 4 - have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms) - { - fix \ assume "\ permutes B" - from permutes_bij_inv_into[OF this bij_inv] and assms - have "(\x. if x \ A then inv_into A f (\ (f x)) else x) permutes A" - by (simp add: inv_into_inv_into_eq cong: if_cong) - } - from this show ?case by (auto simp: permutes_inv) - next - case 1 - thus ?case using assms - by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left - dest: bij_betwE) - next - case 2 - moreover have "bij_betw (inv_into A f) B A" - by (intro bij_betw_inv_into assms) - ultimately show ?case using assms - by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right - dest: bij_betwE) - qed -qed - -lemma bij_betw_derangements: - assumes "bij_betw f A B" - shows "bij_betw (\\ x. if x \ B then f (\ (inv_into A f x)) else x) - {\. \ permutes A \ (\x\A. \ x \ x)} {\. \ permutes B \ (\x\B. \ x \ x)}" - (is "bij_betw ?f _ _") -proof - - let ?g = "(\\ x. if x \ A then inv_into A f (\ (f x)) else x)" - show ?thesis - proof (rule bij_betw_byWitness [of _ ?g], goal_cases) - case 3 - have "?f \ x \ x" if "\ permutes A" "\x. x \ A \ \ x \ x" "x \ B" for \ x - using that and assms by (metis bij_betwE bij_betw_imp_inj_on bij_betw_imp_surj_on - inv_into_f_f inv_into_into permutes_imp_bij) - with permutes_bij_inv_into[OF _ assms] show ?case by auto - next - case 4 - have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms) - have "?g \ permutes A" if "\ permutes B" for \ - using permutes_bij_inv_into[OF that bij_inv] and assms - by (simp add: inv_into_inv_into_eq cong: if_cong) - moreover have "?g \ x \ x" if "\ permutes B" "\x. x \ B \ \ x \ x" "x \ A" for \ x - using that and assms by (metis bij_betwE bij_betw_imp_surj_on f_inv_into_f permutes_imp_bij) - ultimately show ?case by auto - next - case 1 - thus ?case using assms - by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left - dest: bij_betwE) - next - case 2 - moreover have "bij_betw (inv_into A f) B A" - by (intro bij_betw_inv_into assms) - ultimately show ?case using assms - by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right - dest: bij_betwE) - qed -qed - - -subsection \The number of permutations on a finite set\ - -lemma permutes_insert_lemma: - assumes "p permutes (insert a S)" - shows "Fun.swap a (p a) id \ p permutes S" - apply (rule permutes_superset[where S = "insert a S"]) - apply (rule permutes_compose[OF assms]) - apply (rule permutes_swap_id, simp) - using permutes_in_image[OF assms, of a] - apply simp - apply (auto simp add: Ball_def Fun.swap_def) - done - -lemma permutes_insert: "{p. p permutes (insert a S)} = - (\(b, p). Fun.swap a b id \ p) ` {(b, p). b \ insert a S \ p \ {p. p permutes S}}" -proof - - have "p permutes insert a S \ - (\b q. p = Fun.swap a b id \ q \ b \ insert a S \ q permutes S)" for p - proof - - have "\b q. p = Fun.swap a b id \ q \ b \ insert a S \ q permutes S" - if p: "p permutes insert a S" - proof - - let ?b = "p a" - let ?q = "Fun.swap a (p a) id \ p" - have *: "p = Fun.swap a ?b id \ ?q" - by (simp add: fun_eq_iff o_assoc) - have **: "?b \ insert a S" - unfolding permutes_in_image[OF p] by simp - from permutes_insert_lemma[OF p] * ** show ?thesis - by blast - qed - moreover have "p permutes insert a S" - if bq: "p = Fun.swap a b id \ q" "b \ insert a S" "q permutes S" for b q - proof - - from permutes_subset[OF bq(3), of "insert a S"] have q: "q permutes insert a S" - by auto - have a: "a \ insert a S" - by simp - from bq(1) permutes_compose[OF q permutes_swap_id[OF a bq(2)]] show ?thesis - by simp - qed - ultimately show ?thesis by blast - qed - then show ?thesis by auto -qed - -lemma card_permutations: - assumes "card S = n" - and "finite S" - shows "card {p. p permutes S} = fact n" - using assms(2,1) -proof (induct arbitrary: n) - case empty - then show ?case by simp -next - case (insert x F) - { - fix n - assume card_insert: "card (insert x F) = n" - let ?xF = "{p. p permutes insert x F}" - let ?pF = "{p. p permutes F}" - let ?pF' = "{(b, p). b \ insert x F \ p \ ?pF}" - let ?g = "(\(b, p). Fun.swap x b id \ p)" - have xfgpF': "?xF = ?g ` ?pF'" - by (rule permutes_insert[of x F]) - from \x \ F\ \finite F\ card_insert have Fs: "card F = n - 1" - by auto - from \finite F\ insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" - by auto - then have "finite ?pF" - by (auto intro: card_ge_0_finite) - with \finite F\ card.insert_remove have pF'f: "finite ?pF'" - apply (simp only: Collect_case_prod Collect_mem_eq) - apply (rule finite_cartesian_product) - apply simp_all - done - - have ginj: "inj_on ?g ?pF'" - proof - - { - fix b p c q - assume bp: "(b, p) \ ?pF'" - assume cq: "(c, q) \ ?pF'" - assume eq: "?g (b, p) = ?g (c, q)" - from bp cq have pF: "p permutes F" and qF: "q permutes F" - by auto - from pF \x \ F\ eq have "b = ?g (b, p) x" - by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff) - also from qF \x \ F\ eq have "\ = ?g (c, q) x" - by (auto simp: fun_upd_def fun_eq_iff) - also from qF \x \ F\ have "\ = c" - by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff) - finally have "b = c" . - then have "Fun.swap x b id = Fun.swap x c id" - by simp - with eq have "Fun.swap x b id \ p = Fun.swap x b id \ q" - by simp - then have "Fun.swap x b id \ (Fun.swap x b id \ p) = Fun.swap x b id \ (Fun.swap x b id \ q)" - by simp - then have "p = q" - by (simp add: o_assoc) - with \b = c\ have "(b, p) = (c, q)" - by simp - } - then show ?thesis - unfolding inj_on_def by blast - qed - from \x \ F\ \finite F\ card_insert have "n \ 0" - by auto - then have "\m. n = Suc m" - by presburger - then obtain m where n: "n = Suc m" - by blast - from pFs card_insert have *: "card ?xF = fact n" - unfolding xfgpF' card_image[OF ginj] - using \finite F\ \finite ?pF\ - by (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product) (simp add: n) - from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" - by (simp add: xfgpF' n) - from * have "card ?xF = fact n" - unfolding xFf by blast - } - with insert show ?case by simp -qed - -lemma finite_permutations: - assumes "finite S" - shows "finite {p. p permutes S}" - using card_permutations[OF refl assms] by (auto intro: card_ge_0_finite) - - -subsection \Hence a sort of induction principle composing by swaps\ - -lemma permutes_induct [consumes 2, case_names id swap]: - \P p\ if \p permutes S\ \finite S\ - and id: \P id\ - and swap: \\a b p. a \ S \ b \ S \ p permutes S \ P p \ P (Fun.swap a b id \ p)\ -using \finite S\ \p permutes S\ swap proof (induction S arbitrary: p) - case empty - with id show ?case - by (simp only: permutes_empty) -next - case (insert x S p) - define q where \q = Fun.swap x (p x) id \ p\ - then have swap_q: \Fun.swap x (p x) id \ q = p\ - by (simp add: o_assoc) - from \p permutes insert x S\ have \q permutes S\ - by (simp add: q_def permutes_insert_lemma) - then have \q permutes insert x S\ - by (simp add: permutes_imp_permutes_insert) - from \q permutes S\ have \P q\ - by (auto intro: insert.IH insert.prems(2) permutes_imp_permutes_insert) - have \x \ insert x S\ - by simp - moreover from \p permutes insert x S\ have \p x \ insert x S\ - using permutes_in_image [of p \insert x S\ x] by simp - ultimately have \P (Fun.swap x (p x) id \ q)\ - using \q permutes insert x S\ \P q\ - by (rule insert.prems(2)) - then show ?case - by (simp add: swap_q) -qed - -lemma permutes_rev_induct [consumes 2, case_names id swap]: - \P p\ if \p permutes S\ \finite S\ - and id': \P id\ - and swap': \\a b p. a \ S \ b \ S \ p permutes S \ P p \ P (Fun.swap a b p)\ -using \p permutes S\ \finite S\ proof (induction rule: permutes_induct) - case id - from id' show ?case . -next - case (swap a b p) - have \P (Fun.swap (inv p a) (inv p b) p)\ - by (rule swap') (auto simp add: swap permutes_in_image permutes_inv) - also have \Fun.swap (inv p a) (inv p b) p = Fun.swap a b id \ p\ - by (rule bij_swap_comp [symmetric]) (rule permutes_bij, rule swap) - finally show ?case . -qed - - -subsection \Permutations of index set for iterated operations\ - -lemma (in comm_monoid_set) permute: - assumes "p permutes S" - shows "F g S = F (g \ p) S" -proof - - from \p permutes S\ have "inj p" - by (rule permutes_inj) - then have "inj_on p S" - by (auto intro: subset_inj_on) - then have "F g (p ` S) = F (g \ p) S" - by (rule reindex) - moreover from \p permutes S\ have "p ` S = S" - by (rule permutes_image) - ultimately show ?thesis - by simp -qed - - -subsection \Permutations as transposition sequences\ - -inductive swapidseq :: "nat \ ('a \ 'a) \ bool" - where - id[simp]: "swapidseq 0 id" - | comp_Suc: "swapidseq n p \ a \ b \ swapidseq (Suc n) (Fun.swap a b id \ p)" - -declare id[unfolded id_def, simp] - -definition "permutation p \ (\n. swapidseq n p)" - - -subsection \Some closure properties of the set of permutations, with lengths\ - -lemma permutation_id[simp]: "permutation id" - unfolding permutation_def by (rule exI[where x=0]) simp - -declare permutation_id[unfolded id_def, simp] - -lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)" - apply clarsimp - using comp_Suc[of 0 id a b] - apply simp - done - -lemma permutation_swap_id: "permutation (Fun.swap a b id)" -proof (cases "a = b") - case True - then show ?thesis by simp -next - case False - then show ?thesis - unfolding permutation_def - using swapidseq_swap[of a b] by blast -qed - - -lemma swapidseq_comp_add: "swapidseq n p \ swapidseq m q \ swapidseq (n + m) (p \ q)" -proof (induct n p arbitrary: m q rule: swapidseq.induct) - case (id m q) - then show ?case by simp -next - case (comp_Suc n p a b m q) - have eq: "Suc n + m = Suc (n + m)" - by arith - show ?case - apply (simp only: eq comp_assoc) - apply (rule swapidseq.comp_Suc) - using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) - apply blast+ - done -qed - -lemma permutation_compose: "permutation p \ permutation q \ permutation (p \ q)" - unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis - -lemma swapidseq_endswap: "swapidseq n p \ a \ b \ swapidseq (Suc n) (p \ Fun.swap a b id)" - by (induct n p rule: swapidseq.induct) - (use swapidseq_swap[of a b] in \auto simp add: comp_assoc intro: swapidseq.comp_Suc\) - -lemma swapidseq_inverse_exists: "swapidseq n p \ \q. swapidseq n q \ p \ q = id \ q \ p = id" -proof (induct n p rule: swapidseq.induct) - case id - then show ?case - by (rule exI[where x=id]) simp -next - case (comp_Suc n p a b) - from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" - by blast - let ?q = "q \ Fun.swap a b id" - note H = comp_Suc.hyps - from swapidseq_swap[of a b] H(3) have *: "swapidseq 1 (Fun.swap a b id)" - by simp - from swapidseq_comp_add[OF q(1) *] have **: "swapidseq (Suc n) ?q" - by simp - have "Fun.swap a b id \ p \ ?q = Fun.swap a b id \ (p \ q) \ Fun.swap a b id" - by (simp add: o_assoc) - also have "\ = id" - by (simp add: q(2)) - finally have ***: "Fun.swap a b id \ p \ ?q = id" . - have "?q \ (Fun.swap a b id \ p) = q \ (Fun.swap a b id \ Fun.swap a b id) \ p" - by (simp only: o_assoc) - then have "?q \ (Fun.swap a b id \ p) = id" - by (simp add: q(3)) - with ** *** show ?case - by blast -qed - -lemma swapidseq_inverse: - assumes "swapidseq n p" - shows "swapidseq n (inv p)" - using swapidseq_inverse_exists[OF assms] inv_unique_comp[of p] by auto - -lemma permutation_inverse: "permutation p \ permutation (inv p)" - using permutation_def swapidseq_inverse by blast - - - -subsection \Various combinations of transpositions with 2, 1 and 0 common elements\ - -lemma swap_id_common:" a \ c \ b \ c \ - Fun.swap a b id \ Fun.swap a c id = Fun.swap b c id \ Fun.swap a b id" - by (simp add: fun_eq_iff Fun.swap_def) - -lemma swap_id_common': "a \ b \ a \ c \ - Fun.swap a c id \ Fun.swap b c id = Fun.swap b c id \ Fun.swap a b id" - by (simp add: fun_eq_iff Fun.swap_def) - -lemma swap_id_independent: "a \ c \ a \ d \ b \ c \ b \ d \ - Fun.swap a b id \ Fun.swap c d id = Fun.swap c d id \ Fun.swap a b id" - by (simp add: fun_eq_iff Fun.swap_def) - - -subsection \The identity map only has even transposition sequences\ - -lemma symmetry_lemma: - assumes "\a b c d. P a b c d \ P a b d c" - and "\a b c d. a \ b \ c \ d \ - a = c \ b = d \ a = c \ b \ d \ a \ c \ b = d \ a \ c \ a \ d \ b \ c \ b \ d \ - P a b c d" - shows "\a b c d. a \ b \ c \ d \ P a b c d" - using assms by metis - -lemma swap_general: "a \ b \ c \ d \ - Fun.swap a b id \ Fun.swap c d id = id \ - (\x y z. x \ a \ y \ a \ z \ a \ x \ y \ - Fun.swap a b id \ Fun.swap c d id = Fun.swap x y id \ Fun.swap a z id)" -proof - - assume neq: "a \ b" "c \ d" - have "a \ b \ c \ d \ - (Fun.swap a b id \ Fun.swap c d id = id \ - (\x y z. x \ a \ y \ a \ z \ a \ x \ y \ - Fun.swap a b id \ Fun.swap c d id = Fun.swap x y id \ Fun.swap a z id))" - apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) - apply (simp_all only: swap_commute) - apply (case_tac "a = c \ b = d") - apply (clarsimp simp only: swap_commute swap_id_idempotent) - apply (case_tac "a = c \ b \ d") - apply (rule disjI2) - apply (rule_tac x="b" in exI) - apply (rule_tac x="d" in exI) - apply (rule_tac x="b" in exI) - apply (clarsimp simp add: fun_eq_iff Fun.swap_def) - apply (case_tac "a \ c \ b = d") - apply (rule disjI2) - apply (rule_tac x="c" in exI) - apply (rule_tac x="d" in exI) - apply (rule_tac x="c" in exI) - apply (clarsimp simp add: fun_eq_iff Fun.swap_def) - apply (rule disjI2) - apply (rule_tac x="c" in exI) - apply (rule_tac x="d" in exI) - apply (rule_tac x="b" in exI) - apply (clarsimp simp add: fun_eq_iff Fun.swap_def) - done - with neq show ?thesis by metis -qed - -lemma swapidseq_id_iff[simp]: "swapidseq 0 p \ p = id" - using swapidseq.cases[of 0 p "p = id"] by auto - -lemma swapidseq_cases: "swapidseq n p \ - n = 0 \ p = id \ (\a b q m. n = Suc m \ p = Fun.swap a b id \ q \ swapidseq m q \ a \ b)" - apply (rule iffI) - apply (erule swapidseq.cases[of n p]) - apply simp - apply (rule disjI2) - apply (rule_tac x= "a" in exI) - apply (rule_tac x= "b" in exI) - apply (rule_tac x= "pa" in exI) - apply (rule_tac x= "na" in exI) - apply simp - apply auto - apply (rule comp_Suc, simp_all) - done - -lemma fixing_swapidseq_decrease: - assumes "swapidseq n p" - and "a \ b" - and "(Fun.swap a b id \ p) a = a" - shows "n \ 0 \ swapidseq (n - 1) (Fun.swap a b id \ p)" - using assms -proof (induct n arbitrary: p a b) - case 0 - then show ?case - by (auto simp add: Fun.swap_def fun_upd_def) -next - case (Suc n p a b) - from Suc.prems(1) swapidseq_cases[of "Suc n" p] - obtain c d q m where - cdqm: "Suc n = Suc m" "p = Fun.swap c d id \ q" "swapidseq m q" "c \ d" "n = m" - by auto - consider "Fun.swap a b id \ Fun.swap c d id = id" - | x y z where "x \ a" "y \ a" "z \ a" "x \ y" - "Fun.swap a b id \ Fun.swap c d id = Fun.swap x y id \ Fun.swap a z id" - using swap_general[OF Suc.prems(2) cdqm(4)] by metis - then show ?case - proof cases - case 1 - then show ?thesis - by (simp only: cdqm o_assoc) (simp add: cdqm) - next - case prems: 2 - then have az: "a \ z" - by simp - from prems have *: "(Fun.swap x y id \ h) a = a \ h a = a" for h - by (simp add: Fun.swap_def) - from cdqm(2) have "Fun.swap a b id \ p = Fun.swap a b id \ (Fun.swap c d id \ q)" - by simp - then have "Fun.swap a b id \ p = Fun.swap x y id \ (Fun.swap a z id \ q)" - by (simp add: o_assoc prems) - then have "(Fun.swap a b id \ p) a = (Fun.swap x y id \ (Fun.swap a z id \ q)) a" - by simp - then have "(Fun.swap x y id \ (Fun.swap a z id \ q)) a = a" - unfolding Suc by metis - then have "(Fun.swap a z id \ q) a = a" - by (simp only: *) - from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az this] - have **: "swapidseq (n - 1) (Fun.swap a z id \ q)" "n \ 0" - by blast+ - from \n \ 0\ have ***: "Suc n - 1 = Suc (n - 1)" - by auto - show ?thesis - apply (simp only: cdqm(2) prems o_assoc ***) - apply (simp only: Suc_not_Zero simp_thms comp_assoc) - apply (rule comp_Suc) - using ** prems - apply blast+ - done - qed -qed - -lemma swapidseq_identity_even: - assumes "swapidseq n (id :: 'a \ 'a)" - shows "even n" - using \swapidseq n id\ -proof (induct n rule: nat_less_induct) - case H: (1 n) - consider "n = 0" - | a b :: 'a and q m where "n = Suc m" "id = Fun.swap a b id \ q" "swapidseq m q" "a \ b" - using H(2)[unfolded swapidseq_cases[of n id]] by auto - then show ?case - proof cases - case 1 - then show ?thesis by presburger - next - case h: 2 - from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]] - have m: "m \ 0" "swapidseq (m - 1) (id :: 'a \ 'a)" - by auto - from h m have mn: "m - 1 < n" - by arith - from H(1)[rule_format, OF mn m(2)] h(1) m(1) show ?thesis - by presburger - qed -qed - - -subsection \Therefore we have a welldefined notion of parity\ - -definition "evenperm p = even (SOME n. swapidseq n p)" - -lemma swapidseq_even_even: - assumes m: "swapidseq m p" - and n: "swapidseq n p" - shows "even m \ even n" -proof - - from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" - by blast - from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]] show ?thesis - by arith -qed - -lemma evenperm_unique: - assumes p: "swapidseq n p" - and n:"even n = b" - shows "evenperm p = b" - unfolding n[symmetric] evenperm_def - apply (rule swapidseq_even_even[where p = p]) - apply (rule someI[where x = n]) - using p - apply blast+ - done - - -subsection \And it has the expected composition properties\ - -lemma evenperm_id[simp]: "evenperm id = True" - by (rule evenperm_unique[where n = 0]) simp_all - -lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)" - by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap) - -lemma evenperm_comp: - assumes "permutation p" "permutation q" - shows "evenperm (p \ q) \ evenperm p = evenperm q" -proof - - from assms obtain n m where n: "swapidseq n p" and m: "swapidseq m q" - unfolding permutation_def by blast - have "even (n + m) \ (even n \ even m)" - by arith - from evenperm_unique[OF n refl] evenperm_unique[OF m refl] - and evenperm_unique[OF swapidseq_comp_add[OF n m] this] show ?thesis - by blast -qed - -lemma evenperm_inv: - assumes "permutation p" - shows "evenperm (inv p) = evenperm p" -proof - - from assms obtain n where n: "swapidseq n p" - unfolding permutation_def by blast - show ?thesis - by (rule evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]) -qed - - -subsection \A more abstract characterization of permutations\ - -lemma permutation_bijective: - assumes "permutation p" - shows "bij p" -proof - - from assms obtain n where n: "swapidseq n p" - unfolding permutation_def by blast - from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" - by blast - then show ?thesis - unfolding bij_iff - apply (auto simp add: fun_eq_iff) - apply metis - done -qed - -lemma permutation_finite_support: - assumes "permutation p" - shows "finite {x. p x \ x}" -proof - - from assms obtain n where "swapidseq n p" - unfolding permutation_def by blast - then show ?thesis - proof (induct n p rule: swapidseq.induct) - case id - then show ?case by simp - next - case (comp_Suc n p a b) - let ?S = "insert a (insert b {x. p x \ x})" - from comp_Suc.hyps(2) have *: "finite ?S" - by simp - from \a \ b\ have **: "{x. (Fun.swap a b id \ p) x \ x} \ ?S" - by (auto simp: Fun.swap_def) - show ?case - by (rule finite_subset[OF ** *]) - qed -qed - -lemma permutation_lemma: - assumes "finite S" - and "bij p" - and "\x. x \ S \ p x = x" - shows "permutation p" - using assms -proof (induct S arbitrary: p rule: finite_induct) - case empty - then show ?case - by simp -next - case (insert a F p) - let ?r = "Fun.swap a (p a) id \ p" - let ?q = "Fun.swap a (p a) id \ ?r" - have *: "?r a = a" - by (simp add: Fun.swap_def) - from insert * have **: "\x. x \ F \ ?r x = x" - by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3)) - have "bij ?r" - by (rule bij_swap_compose_bij[OF insert(4)]) - have "permutation ?r" - by (rule insert(3)[OF \bij ?r\ **]) - then have "permutation ?q" - by (simp add: permutation_compose permutation_swap_id) - then show ?case - by (simp add: o_assoc) -qed - -lemma permutation: "permutation p \ bij p \ finite {x. p x \ x}" - (is "?lhs \ ?b \ ?f") -proof - assume ?lhs - with permutation_bijective permutation_finite_support show "?b \ ?f" - by auto -next - assume "?b \ ?f" - then have "?f" "?b" by blast+ - from permutation_lemma[OF this] show ?lhs - by blast -qed - -lemma permutation_inverse_works: - assumes "permutation p" - shows "inv p \ p = id" - and "p \ inv p = id" - using permutation_bijective [OF assms] by (auto simp: bij_def inj_iff surj_iff) - -lemma permutation_inverse_compose: - assumes p: "permutation p" - and q: "permutation q" - shows "inv (p \ q) = inv q \ inv p" -proof - - note ps = permutation_inverse_works[OF p] - note qs = permutation_inverse_works[OF q] - have "p \ q \ (inv q \ inv p) = p \ (q \ inv q) \ inv p" - by (simp add: o_assoc) - also have "\ = id" - by (simp add: ps qs) - finally have *: "p \ q \ (inv q \ inv p) = id" . - have "inv q \ inv p \ (p \ q) = inv q \ (inv p \ p) \ q" - by (simp add: o_assoc) - also have "\ = id" - by (simp add: ps qs) - finally have **: "inv q \ inv p \ (p \ q) = id" . - show ?thesis - by (rule inv_unique_comp[OF * **]) -qed - - -subsection \Relation to \permutes\\ - -lemma permutes_imp_permutation: - \permutation p\ if \finite S\ \p permutes S\ -proof - - from \p permutes S\ have \{x. p x \ x} \ S\ - by (auto dest: permutes_not_in) - then have \finite {x. p x \ x}\ - using \finite S\ by (rule finite_subset) - moreover from \p permutes S\ have \bij p\ - by (auto dest: permutes_bij) - ultimately show ?thesis - by (simp add: permutation) -qed - -lemma permutation_permutesE: - assumes \permutation p\ - obtains S where \finite S\ \p permutes S\ -proof - - from assms have fin: \finite {x. p x \ x}\ - by (simp add: permutation) - from assms have \bij p\ - by (simp add: permutation) - also have \UNIV = {x. p x \ x} \ {x. p x = x}\ - by auto - finally have \bij_betw p {x. p x \ x} {x. p x \ x}\ - by (rule bij_betw_partition) (auto simp add: bij_betw_fixpoints) - then have \p permutes {x. p x \ x}\ - by (auto intro: bij_imp_permutes) - with fin show thesis .. -qed - -lemma permutation_permutes: "permutation p \ (\S. finite S \ p permutes S)" - by (auto elim: permutation_permutesE intro: permutes_imp_permutation) - - -subsection \Sign of a permutation as a real number\ - -definition sign :: \('a \ 'a) \ int\ \ \TODO: prefer less generic name\ - where \sign p = (if evenperm p then (1::int) else -1)\ - -lemma sign_nz: "sign p \ 0" - by (simp add: sign_def) - -lemma sign_id: "sign id = 1" - by (simp add: sign_def) - -lemma sign_inverse: "permutation p \ sign (inv p) = sign p" - by (simp add: sign_def evenperm_inv) - -lemma sign_compose: "permutation p \ permutation q \ sign (p \ q) = sign p * sign q" - by (simp add: sign_def evenperm_comp) - -lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)" - by (simp add: sign_def evenperm_swap) - -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]: - fixes xs :: "'a list" - 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 - from assms have "inj \" "surj \" - by (simp_all add: permutes_inj permutes_surj) - then show "(map_of xs \ \) x = map_of (map ?f xs) x" for x - by (induct xs) (auto simp: inv_f_f surj_f_inv_f) -qed - - -subsection \More lemmas about permutations\ - -text \The following few lemmas were contributed by Lukas Bulwahn.\ - -lemma count_image_mset_eq_card_vimage: - assumes "finite A" - shows "count (image_mset f (mset_set A)) b = card {a \ A. f a = b}" - using assms -proof (induct A) - case empty - show ?case by simp -next - case (insert x F) - show ?case - proof (cases "f x = b") - case True - with insert.hyps - have "count (image_mset f (mset_set (insert x F))) b = Suc (card {a \ F. f a = f x})" - by auto - also from insert.hyps(1,2) have "\ = card (insert x {a \ F. f a = f x})" - by simp - also from \f x = b\ have "card (insert x {a \ F. f a = f x}) = card {a \ insert x F. f a = b}" - by (auto intro: arg_cong[where f="card"]) - finally show ?thesis - using insert by auto - next - case False - then have "{a \ F. f a = b} = {a \ insert x F. f a = b}" - by auto - with insert False show ?thesis - by simp - qed -qed - -\ \Prove \image_mset_eq_implies_permutes\ ...\ -lemma image_mset_eq_implies_permutes: - fixes f :: "'a \ 'b" - assumes "finite A" - and mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)" - obtains p where "p permutes A" and "\x\A. f x = f' (p x)" -proof - - from \finite A\ have [simp]: "finite {a \ A. f a = (b::'b)}" for f b by auto - have "f ` A = f' ` A" - proof - - from \finite A\ have "f ` A = f ` (set_mset (mset_set A))" - by simp - also have "\ = f' ` set_mset (mset_set A)" - by (metis mset_eq multiset.set_map) - also from \finite A\ have "\ = f' ` A" - by simp - finally show ?thesis . - qed - have "\b\(f ` A). \p. bij_betw p {a \ A. f a = b} {a \ A. f' a = b}" - proof - fix b - from mset_eq have "count (image_mset f (mset_set A)) b = count (image_mset f' (mset_set A)) b" - by simp - with \finite A\ have "card {a \ A. f a = b} = card {a \ A. f' a = b}" - by (simp add: count_image_mset_eq_card_vimage) - then show "\p. bij_betw p {a\A. f a = b} {a \ A. f' a = b}" - by (intro finite_same_card_bij) simp_all - qed - then have "\p. \b\f ` A. bij_betw (p b) {a \ A. f a = b} {a \ A. f' a = b}" - by (rule bchoice) - then obtain p where p: "\b\f ` A. bij_betw (p b) {a \ A. f a = b} {a \ A. f' a = b}" .. - define p' where "p' = (\a. if a \ A then p (f a) a else a)" - have "p' permutes A" - proof (rule bij_imp_permutes) - have "disjoint_family_on (\i. {a \ A. f' a = i}) (f ` A)" - by (auto simp: disjoint_family_on_def) - moreover - have "bij_betw (\a. p (f a) a) {a \ A. f a = b} {a \ A. f' a = b}" if "b \ f ` A" for b - using p that by (subst bij_betw_cong[where g="p b"]) auto - ultimately - have "bij_betw (\a. p (f a) a) (\b\f ` A. {a \ A. f a = b}) (\b\f ` A. {a \ A. f' a = b})" - by (rule bij_betw_UNION_disjoint) - moreover have "(\b\f ` A. {a \ A. f a = b}) = A" - by auto - moreover from \f ` A = f' ` A\ have "(\b\f ` A. {a \ A. f' a = b}) = A" - by auto - ultimately show "bij_betw p' A A" - unfolding p'_def by (subst bij_betw_cong[where g="(\a. p (f a) a)"]) auto - next - show "\x. x \ A \ p' x = x" - by (simp add: p'_def) - qed - moreover from p have "\x\A. f x = f' (p' x)" - unfolding p'_def using bij_betwE by fastforce - ultimately show ?thesis .. -qed - -\ \... and derive the existing property:\ -lemma mset_eq_permutation: - fixes xs ys :: "'a list" - assumes mset_eq: "mset xs = mset ys" - obtains p where "p permutes {..i. xs ! i) (mset_set {..i. ys ! i) (mset_set {..i\{..i \ S. p i \ i" - shows "p = id" -proof - - have "p n = n" for n - using assms - proof (induct n arbitrary: S rule: less_induct) - case (less n) - show ?case - proof (cases "n \ S") - case False - with less(2) show ?thesis - unfolding permutes_def by metis - next - case True - with less(3) have "p n < n \ p n = n" - by auto - then show ?thesis - proof - assume "p n < n" - with less have "p (p n) = p n" - by metis - with permutes_inj[OF less(2)] have "p n = n" - unfolding inj_def by blast - with \p n < n\ have False - by simp - then show ?thesis .. - qed - qed - qed - then show ?thesis by (auto simp: fun_eq_iff) -qed - -lemma permutes_natset_ge: - fixes S :: "'a::wellorder set" - assumes p: "p permutes S" - and le: "\i \ S. p i \ i" - shows "p = id" -proof - - have "i \ inv p i" if "i \ S" for i - proof - - from that permutes_in_image[OF permutes_inv[OF p]] have "inv p i \ S" - by simp - with le have "p (inv p i) \ inv p i" - by blast - with permutes_inverses[OF p] show ?thesis - by simp - qed - then have "\i\S. inv p i \ i" - by blast - from permutes_natset_le[OF permutes_inv[OF p] this] have "inv p = inv id" - by simp - then show ?thesis - apply (subst permutes_inv_inv[OF p, symmetric]) - apply (rule inv_unique_comp) - apply simp_all - done -qed - -lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}" - apply (rule set_eqI) - apply auto - using permutes_inv_inv permutes_inv - apply auto - apply (rule_tac x="inv x" in exI) - apply auto - done - -lemma image_compose_permutations_left: - assumes "q permutes S" - shows "{q \ p |p. p permutes S} = {p. p permutes S}" - apply (rule set_eqI) - apply auto - apply (rule permutes_compose) - using assms - apply auto - apply (rule_tac x = "inv q \ x" in exI) - apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o) - done - -lemma image_compose_permutations_right: - assumes "q permutes S" - shows "{p \ q | p. p permutes S} = {p . p permutes S}" - apply (rule set_eqI) - apply auto - apply (rule permutes_compose) - using assms - apply auto - apply (rule_tac x = "x \ inv q" in exI) - apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc) - done - -lemma permutes_in_seg: "p permutes {1 ..n} \ i \ {1..n} \ 1 \ p i \ p i \ n" - by (simp add: permutes_def) metis - -lemma sum_permutations_inverse: "sum f {p. p permutes S} = sum (\p. f(inv p)) {p. p permutes S}" - (is "?lhs = ?rhs") -proof - - let ?S = "{p . p permutes S}" - have *: "inj_on inv ?S" - proof (auto simp add: inj_on_def) - fix q r - assume q: "q permutes S" - and r: "r permutes S" - and qr: "inv q = inv r" - then have "inv (inv q) = inv (inv r)" - by simp - with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r" - by metis - qed - have **: "inv ` ?S = ?S" - using image_inverse_permutations by blast - have ***: "?rhs = sum (f \ inv) ?S" - by (simp add: o_def) - from sum.reindex[OF *, of f] show ?thesis - by (simp only: ** ***) -qed - -lemma setum_permutations_compose_left: - assumes q: "q permutes S" - shows "sum f {p. p permutes S} = sum (\p. f(q \ p)) {p. p permutes S}" - (is "?lhs = ?rhs") -proof - - let ?S = "{p. p permutes S}" - have *: "?rhs = sum (f \ ((\) q)) ?S" - by (simp add: o_def) - have **: "inj_on ((\) q) ?S" - proof (auto simp add: inj_on_def) - fix p r - assume "p permutes S" - and r: "r permutes S" - and rp: "q \ p = q \ r" - then have "inv q \ q \ p = inv q \ q \ r" - by (simp add: comp_assoc) - with permutes_inj[OF q, unfolded inj_iff] show "p = r" - by simp - qed - have "((\) q) ` ?S = ?S" - using image_compose_permutations_left[OF q] by auto - with * sum.reindex[OF **, of f] show ?thesis - by (simp only:) -qed - -lemma sum_permutations_compose_right: - assumes q: "q permutes S" - shows "sum f {p. p permutes S} = sum (\p. f(p \ q)) {p. p permutes S}" - (is "?lhs = ?rhs") -proof - - let ?S = "{p. p permutes S}" - have *: "?rhs = sum (f \ (\p. p \ q)) ?S" - by (simp add: o_def) - have **: "inj_on (\p. p \ q) ?S" - proof (auto simp add: inj_on_def) - fix p r - assume "p permutes S" - and r: "r permutes S" - and rp: "p \ q = r \ q" - then have "p \ (q \ inv q) = r \ (q \ inv q)" - by (simp add: o_assoc) - with permutes_surj[OF q, unfolded surj_iff] show "p = r" - by simp - qed - from image_compose_permutations_right[OF q] have "(\p. p \ q) ` ?S = ?S" - by auto - with * sum.reindex[OF **, of f] show ?thesis - by (simp only:) -qed - - -subsection \Sum over a set of permutations (could generalize to iteration)\ - -lemma sum_over_permutations_insert: - assumes fS: "finite S" - and aS: "a \ S" - shows "sum f {p. p permutes (insert a S)} = - sum (\b. sum (\q. f (Fun.swap a b id \ q)) {p. p permutes S}) (insert a S)" -proof - - have *: "\f a b. (\(b, p). f (Fun.swap a b id \ p)) = f \ (\(b,p). Fun.swap a b id \ p)" - by (simp add: fun_eq_iff) - have **: "\P Q. {(a, b). a \ P \ b \ Q} = P \ Q" - by blast - show ?thesis - unfolding * ** sum.cartesian_product permutes_insert - proof (rule sum.reindex) - let ?f = "(\(b, y). Fun.swap a b id \ y)" - let ?P = "{p. p permutes S}" - { - fix b c p q - assume b: "b \ insert a S" - assume c: "c \ insert a S" - assume p: "p permutes S" - assume q: "q permutes S" - assume eq: "Fun.swap a b id \ p = Fun.swap a c id \ q" - from p q aS have pa: "p a = a" and qa: "q a = a" - unfolding permutes_def by metis+ - from eq have "(Fun.swap a b id \ p) a = (Fun.swap a c id \ q) a" - by simp - then have bc: "b = c" - by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def - cong del: if_weak_cong split: if_split_asm) - from eq[unfolded bc] have "(\p. Fun.swap a c id \ p) (Fun.swap a c id \ p) = - (\p. Fun.swap a c id \ p) (Fun.swap a c id \ q)" by simp - then have "p = q" - unfolding o_assoc swap_id_idempotent by simp - with bc have "b = c \ p = q" - by blast - } - then show "inj_on ?f (insert a S \ ?P)" - unfolding inj_on_def by clarify metis - qed -qed - - -subsection \Constructing permutations from association lists\ - -definition list_permutes :: "('a \ 'a) list \ 'a set \ bool" - 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 :: "('a \ 'a) list \ 'a \ 'a" - 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 :: "('a \ 'a) list \ 'a \ 'a" - 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 x'y' have *: "(x, x') \ set xs" "(y, y') \ set xs" - by (force dest: map_of_SomeD)+ - moreover from * 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: "x \ set (map fst xs) \ permutation_of_list xs x = x" - by (induct xs) (auto simp: permutation_of_list_Cons) - -lemma permutation_of_list_unique': - "distinct (map fst xs) \ (x, y) \ set xs \ permutation_of_list xs x = y" - by (induct xs) (force simp: permutation_of_list_Cons)+ - -lemma permutation_of_list_unique: - "list_permutes xs A \ (x, y) \ set xs \ permutation_of_list xs x = y" - by (intro permutation_of_list_unique') (simp_all add: list_permutes_def) - -lemma inverse_permutation_of_list_id: - "x \ set (map snd xs) \ inverse_permutation_of_list xs x = x" - by (induct xs) auto - -lemma inverse_permutation_of_list_unique': - "distinct (map snd xs) \ (x, y) \ set xs \ inverse_permutation_of_list xs y = x" - by (induct xs) (force simp: inverse_permutation_of_list.simps(2))+ - -lemma inverse_permutation_of_list_unique: - "list_permutes xs A \ (x,y) \ set xs \ inverse_permutation_of_list xs y = x" - by (intro inverse_permutation_of_list_unique') (simp_all add: list_permutes_def) - -lemma inverse_permutation_of_list_correct: - fixes A :: "'a set" - assumes "list_permutes xs A" - 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 - show "permutation_of_list xs (inverse_permutation_of_list xs x) = x" for x - proof (cases "x \ set (map snd xs)") - case True - then obtain y where "(y, x) \ set xs" by auto - with assms show ?thesis - by (simp add: inverse_permutation_of_list_unique permutation_of_list_unique) - next - case False - with assms show ?thesis - by (auto simp: list_permutes_def inverse_permutation_of_list_id permutation_of_list_id) - qed -qed - -end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Library/Stirling.thy --- a/src/HOL/Library/Stirling.thy Wed Mar 24 21:17:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,308 +0,0 @@ -(* Title: HOL/Library/Stirling.thy - Author: Amine Chaieb - Author: Florian Haftmann - Author: Lukas Bulwahn - Author: Manuel Eberl -*) - -section \Stirling numbers of first and second kind\ - -theory Stirling -imports Main -begin - -subsection \Stirling numbers of the second kind\ - -fun Stirling :: "nat \ nat \ nat" - where - "Stirling 0 0 = 1" - | "Stirling 0 (Suc k) = 0" - | "Stirling (Suc n) 0 = 0" - | "Stirling (Suc n) (Suc k) = Suc k * Stirling n (Suc k) + Stirling n k" - -lemma Stirling_1 [simp]: "Stirling (Suc n) (Suc 0) = 1" - by (induct n) simp_all - -lemma Stirling_less [simp]: "n < k \ Stirling n k = 0" - by (induct n k rule: Stirling.induct) simp_all - -lemma Stirling_same [simp]: "Stirling n n = 1" - by (induct n) simp_all - -lemma Stirling_2_2: "Stirling (Suc (Suc n)) (Suc (Suc 0)) = 2 ^ Suc n - 1" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - have "Stirling (Suc (Suc (Suc n))) (Suc (Suc 0)) = - 2 * Stirling (Suc (Suc n)) (Suc (Suc 0)) + Stirling (Suc (Suc n)) (Suc 0)" - by simp - also have "\ = 2 * (2 ^ Suc n - 1) + 1" - by (simp only: Suc Stirling_1) - also have "\ = 2 ^ Suc (Suc n) - 1" - proof - - have "(2::nat) ^ Suc n - 1 > 0" - by (induct n) simp_all - then have "2 * ((2::nat) ^ Suc n - 1) > 0" - by simp - then have "2 \ 2 * ((2::nat) ^ Suc n)" - by simp - with add_diff_assoc2 [of 2 "2 * 2 ^ Suc n" 1] - have "2 * 2 ^ Suc n - 2 + (1::nat) = 2 * 2 ^ Suc n + 1 - 2" . - then show ?thesis - by (simp add: nat_distrib) - qed - finally show ?case by simp -qed - -lemma Stirling_2: "Stirling (Suc n) (Suc (Suc 0)) = 2 ^ n - 1" - using Stirling_2_2 by (cases n) simp_all - - -subsection \Stirling numbers of the first kind\ - -fun stirling :: "nat \ nat \ nat" - where - "stirling 0 0 = 1" - | "stirling 0 (Suc k) = 0" - | "stirling (Suc n) 0 = 0" - | "stirling (Suc n) (Suc k) = n * stirling n (Suc k) + stirling n k" - -lemma stirling_0 [simp]: "n > 0 \ stirling n 0 = 0" - by (cases n) simp_all - -lemma stirling_less [simp]: "n < k \ stirling n k = 0" - by (induct n k rule: stirling.induct) simp_all - -lemma stirling_same [simp]: "stirling n n = 1" - by (induct n) simp_all - -lemma stirling_Suc_n_1: "stirling (Suc n) (Suc 0) = fact n" - by (induct n) auto - -lemma stirling_Suc_n_n: "stirling (Suc n) n = Suc n choose 2" - by (induct n) (auto simp add: numerals(2)) - -lemma stirling_Suc_n_2: - assumes "n \ Suc 0" - shows "stirling (Suc n) 2 = (\k=1..n. fact n div k)" - using assms -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - show ?case - proof (cases n) - case 0 - then show ?thesis - by (simp add: numerals(2)) - next - case Suc - then have geq1: "Suc 0 \ n" - by simp - have "stirling (Suc (Suc n)) 2 = Suc n * stirling (Suc n) 2 + stirling (Suc n) (Suc 0)" - by (simp only: stirling.simps(4)[of "Suc n"] numerals(2)) - also have "\ = Suc n * (\k=1..n. fact n div k) + fact n" - using Suc.hyps[OF geq1] - by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult) - also have "\ = Suc n * (\k=1..n. fact n div k) + Suc n * fact n div Suc n" - by (metis nat.distinct(1) nonzero_mult_div_cancel_left) - also have "\ = (\k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n" - by (simp add: sum_distrib_left div_mult_swap dvd_fact) - also have "\ = (\k=1..Suc n. fact (Suc n) div k)" - by simp - finally show ?thesis . - qed -qed - -lemma of_nat_stirling_Suc_n_2: - assumes "n \ Suc 0" - shows "(of_nat (stirling (Suc n) 2)::'a::field_char_0) = fact n * (\k=1..n. (1 / of_nat k))" - using assms -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - show ?case - proof (cases n) - case 0 - then show ?thesis - by (auto simp add: numerals(2)) - next - case Suc - then have geq1: "Suc 0 \ n" - by simp - have "(of_nat (stirling (Suc (Suc n)) 2)::'a) = - of_nat (Suc n * stirling (Suc n) 2 + stirling (Suc n) (Suc 0))" - by (simp only: stirling.simps(4)[of "Suc n"] numerals(2)) - also have "\ = of_nat (Suc n) * (fact n * (\k = 1..n. 1 / of_nat k)) + fact n" - using Suc.hyps[OF geq1] - by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult) - also have "\ = fact (Suc n) * (\k = 1..n. 1 / of_nat k) + fact (Suc n) * (1 / of_nat (Suc n))" - using of_nat_neq_0 by auto - also have "\ = fact (Suc n) * (\k = 1..Suc n. 1 / of_nat k)" - by (simp add: distrib_left) - finally show ?thesis . - qed -qed - -lemma sum_stirling: "(\k\n. stirling n k) = fact n" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - have "(\k\Suc n. stirling (Suc n) k) = stirling (Suc n) 0 + (\k\n. stirling (Suc n) (Suc k))" - by (simp only: sum.atMost_Suc_shift) - also have "\ = (\k\n. stirling (Suc n) (Suc k))" - by simp - also have "\ = (\k\n. n * stirling n (Suc k) + stirling n k)" - by simp - also have "\ = n * (\k\n. stirling n (Suc k)) + (\k\n. stirling n k)" - by (simp add: sum.distrib sum_distrib_left) - also have "\ = n * fact n + fact n" - proof - - have "n * (\k\n. stirling n (Suc k)) = n * ((\k\Suc n. stirling n k) - stirling n 0)" - by (metis add_diff_cancel_left' sum.atMost_Suc_shift) - also have "\ = n * (\k\n. stirling n k)" - by (cases n) simp_all - also have "\ = n * fact n" - using Suc.hyps by simp - finally have "n * (\k\n. stirling n (Suc k)) = n * fact n" . - moreover have "(\k\n. stirling n k) = fact n" - using Suc.hyps . - ultimately show ?thesis by simp - qed - also have "\ = fact (Suc n)" by simp - finally show ?case . -qed - -lemma stirling_pochhammer: - "(\k\n. of_nat (stirling n k) * x ^ k) = (pochhammer x n :: 'a::comm_semiring_1)" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - have "of_nat (n * stirling n 0) = (0 :: 'a)" by (cases n) simp_all - then have "(\k\Suc n. of_nat (stirling (Suc n) k) * x ^ k) = - (of_nat (n * stirling n 0) * x ^ 0 + - (\i\n. of_nat (n * stirling n (Suc i)) * (x ^ Suc i))) + - (\i\n. of_nat (stirling n i) * (x ^ Suc i))" - by (subst sum.atMost_Suc_shift) (simp add: sum.distrib ring_distribs) - also have "\ = pochhammer x (Suc n)" - by (subst sum.atMost_Suc_shift [symmetric]) - (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc flip: Suc) - finally show ?case . -qed - - -text \A row of the Stirling number triangle\ - -definition stirling_row :: "nat \ nat list" - where "stirling_row n = [stirling n k. k \ [0.. n \ stirling_row n ! k = stirling n k" - by (simp add: stirling_row_def del: upt_Suc) - -lemma length_stirling_row [simp]: "length (stirling_row n) = Suc n" - by (simp add: stirling_row_def) - -lemma stirling_row_nonempty [simp]: "stirling_row n \ []" - using length_stirling_row[of n] by (auto simp del: length_stirling_row) - - -subsubsection \Efficient code\ - -text \ - Naively using the defining equations of the Stirling numbers of the first - kind to compute them leads to exponential run time due to repeated - computations. We can use memoisation to compute them row by row without - repeating computations, at the cost of computing a few unneeded values. - - As a bonus, this is very efficient for applications where an entire row of - Stirling numbers is needed. -\ - -definition zip_with_prev :: "('a \ 'a \ 'b) \ 'a \ 'a list \ 'b list" - where "zip_with_prev f x xs = map2 f (x # xs) xs" - -lemma zip_with_prev_altdef: - "zip_with_prev f x xs = - (if xs = [] then [] else f x (hd xs) # [f (xs!i) (xs!(i+1)). i \ [0..i. f (xs ! i) (xs ! (i + 1))) [0..a b. a + n * b) y xs @ [1]" - by (induct xs arbitrary: y) (simp_all add: zip_with_prev_def) - -lemma stirling_row_code [code]: - "stirling_row 0 = [1]" - "stirling_row (Suc n) = stirling_row_aux n 0 (stirling_row n)" -proof goal_cases - case 1 - show ?case by (simp add: stirling_row_def) -next - case 2 - have "stirling_row (Suc n) = - 0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \ [0.. Suc n" - by simp - then consider "i = 0 \ i = Suc n" | "i > 0" "i \ n" - by linarith - then show ?case - proof cases - case 1 - then show ?thesis - by (auto simp: nth_stirling_row nth_append) - next - case 2 - then show ?thesis - by (cases i) (simp_all add: nth_append nth_stirling_row) - qed - next - case length - then show ?case by simp - qed - also have "0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \ [0..a b. a + n * b) 0 (stirling_row n) @ [1]" - by (cases n) (auto simp add: zip_with_prev_altdef stirling_row_def hd_map simp del: upt_Suc) - also have "\ = stirling_row_aux n 0 (stirling_row n)" - by (simp add: stirling_row_aux_correct) - finally show ?case . -qed - -lemma stirling_code [code]: - "stirling n k = - (if k = 0 then (if n = 0 then 1 else 0) - else if k > n then 0 - else if k = n then 1 - else stirling_row n ! k)" - by (simp add: nth_stirling_row) - -end diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Probability/Random_Permutations.thy --- a/src/HOL/Probability/Random_Permutations.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Probability/Random_Permutations.thy Thu Mar 25 08:52:15 2021 +0000 @@ -12,8 +12,8 @@ theory Random_Permutations imports + "HOL-Combinatorics.Multiset_Permutations" Probability_Mass_Function - "HOL-Library.Multiset_Permutations" begin text \ diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/ROOT --- a/src/HOL/ROOT Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/ROOT Thu Mar 25 08:52:15 2021 +0000 @@ -93,6 +93,7 @@ document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" + "HOL-Combinatorics" "HOL-Computational_Algebra" theories Analysis @@ -124,6 +125,15 @@ document_files "root.tex" +session "HOL-Combinatorics" (main timing) in "Combinatorics" = "HOL" + + sessions + "HOL-Library" + theories + Combinatorics + Guide + document_files + "root.tex" + session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra @@ -390,6 +400,7 @@ " sessions "HOL-Cardinals" + "HOL-Combinatorics" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) @@ -805,6 +816,8 @@ ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + + sessions + "HOL-Combinatorics" theories Probability document_files "root.tex"