(* 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 existing notion› abbreviation (input) perm :: ‹'a list ⇒ 'a list ⇒ bool› (infixr ‹<~~>› 50) where ‹xs <~~> ys ≡ mset xs = mset ys› 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: mset_swap) proposition mset_le_perm_append: "mset xs ⊆# mset ys ⟷ (∃zs. xs @ zs <~~> ys)" by (auto simp add: 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 proposition perm_distinct_iff: "xs <~~> ys ⟹ distinct xs ⟷ distinct ys" by (rule mset_eq_imp_distinct_iff) simp theorem eq_set_perm_remdups: "set xs = set ys ⟹ remdups xs <~~> remdups ys" by (simp add: set_eq_iff_mset_remdups_eq) proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y ⟷ set x = set y" by (simp add: set_eq_iff_mset_remdups_eq) theorem permutation_Ex_bij: assumes "xs <~~> ys" shows "∃f. bij_betw f {..<length xs} {..<length ys} ∧ (∀i<length xs. xs ! i = ys ! (f i))" proof - from assms have ‹mset xs = mset ys› ‹length xs = length ys› by (auto simp add: dest: mset_eq_length) from ‹mset xs = mset ys› obtain p where ‹p permutes {..<length ys}› ‹permute_list p ys = xs› by (rule mset_eq_permutation) then have ‹bij_betw p {..<length xs} {..<length ys}› by (simp add: ‹length xs = length ys› permutes_imp_bij) moreover have ‹∀i<length xs. xs ! i = ys ! (p i)› using ‹permute_list p ys = xs› ‹length xs = length ys› ‹p permutes {..<length ys}› permute_list_nth by auto ultimately show ?thesis by blast qed proposition perm_finite: "finite {B. B <~~> A}" using mset_eq_finite by auto subsection ‹Trivial conclusions:› proposition perm_empty_imp: "[] <~~> ys ⟹ ys = []" by simp 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 proposition perm_sym: "xs <~~> ys ⟹ ys <~~> xs" by simp text ‹We can insert the head anywhere in the list.› proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" by simp proposition perm_append_swap: "xs @ ys <~~> ys @ xs" by simp proposition perm_append_single: "a # xs <~~> xs @ [a]" by simp proposition perm_rev: "rev xs <~~> xs" by simp proposition perm_append1: "xs <~~> ys ⟹ l @ xs <~~> l @ ys" by simp proposition perm_append2: "xs <~~> ys ⟹ xs @ l <~~> ys @ l" by simp proposition perm_empty [iff]: "[] <~~> xs ⟷ xs = []" by simp proposition perm_empty2 [iff]: "xs <~~> [] ⟷ xs = []" by simp proposition perm_sing_imp: "ys <~~> xs ⟹ xs = [y] ⟹ ys = [y]" by simp proposition perm_sing_eq [iff]: "ys <~~> [y] ⟷ ys = [y]" by simp proposition perm_sing_eq2 [iff]: "[y] <~~> ys ⟷ ys = [y]" by simp proposition perm_remove: "x ∈ set ys ⟹ ys <~~> x # remove1 x ys" by simp text ‹\medskip Congruence rule› proposition perm_remove_perm: "xs <~~> ys ⟹ remove1 z xs <~~> remove1 z ys" by simp proposition remove_hd [simp]: "remove1 z (z # xs) = xs" by simp proposition cons_perm_imp_perm: "z # xs <~~> z # ys ⟹ xs <~~> ys" by simp proposition cons_perm_eq [simp]: "z#xs <~~> z#ys ⟷ xs <~~> ys" by simp proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys ⟹ xs <~~> ys" by simp proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys ⟷ xs <~~> ys" by simp proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs ⟷ xs <~~> ys" by simp end