1 (* Title: HOL/Library/Permutation.thy |
|
2 Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker |
|
3 *) |
|
4 |
|
5 section \<open>Permutations\<close> |
|
6 |
|
7 theory Permutation |
|
8 imports Multiset |
|
9 begin |
|
10 |
|
11 inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50) |
|
12 where |
|
13 Nil [intro!]: "[] <~~> []" |
|
14 | swap [intro!]: "y # x # l <~~> x # y # l" |
|
15 | Cons [intro!]: "xs <~~> ys \<Longrightarrow> z # xs <~~> z # ys" |
|
16 | trans [intro]: "xs <~~> ys \<Longrightarrow> ys <~~> zs \<Longrightarrow> xs <~~> zs" |
|
17 |
|
18 proposition perm_refl [iff]: "l <~~> l" |
|
19 by (induct l) auto |
|
20 |
|
21 |
|
22 subsection \<open>Some examples of rule induction on permutations\<close> |
|
23 |
|
24 proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" |
|
25 by (induction "[] :: 'a list" ys pred: perm) simp_all |
|
26 |
|
27 |
|
28 text \<open>\medskip This more general theorem is easier to understand!\<close> |
|
29 |
|
30 proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys" |
|
31 by (induct pred: perm) simp_all |
|
32 |
|
33 proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" |
|
34 by (induct pred: perm) auto |
|
35 |
|
36 |
|
37 subsection \<open>Ways of making new permutations\<close> |
|
38 |
|
39 text \<open>We can insert the head anywhere in the list.\<close> |
|
40 |
|
41 proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" |
|
42 by (induct xs) auto |
|
43 |
|
44 proposition perm_append_swap: "xs @ ys <~~> ys @ xs" |
|
45 by (induct xs) (auto intro: perm_append_Cons) |
|
46 |
|
47 proposition perm_append_single: "a # xs <~~> xs @ [a]" |
|
48 by (rule perm.trans [OF _ perm_append_swap]) simp |
|
49 |
|
50 proposition perm_rev: "rev xs <~~> xs" |
|
51 by (induct xs) (auto intro!: perm_append_single intro: perm_sym) |
|
52 |
|
53 proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys" |
|
54 by (induct l) auto |
|
55 |
|
56 proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l" |
|
57 by (blast intro!: perm_append_swap perm_append1) |
|
58 |
|
59 |
|
60 subsection \<open>Further results\<close> |
|
61 |
|
62 proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []" |
|
63 by (blast intro: perm_empty_imp) |
|
64 |
|
65 proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []" |
|
66 using perm_sym by auto |
|
67 |
|
68 proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]" |
|
69 by (induct pred: perm) auto |
|
70 |
|
71 proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]" |
|
72 by (blast intro: perm_sing_imp) |
|
73 |
|
74 proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]" |
|
75 by (blast dest: perm_sym) |
|
76 |
|
77 |
|
78 subsection \<open>Removing elements\<close> |
|
79 |
|
80 proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" |
|
81 by (induct ys) auto |
|
82 |
|
83 |
|
84 text \<open>\medskip Congruence rule\<close> |
|
85 |
|
86 proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" |
|
87 by (induct pred: perm) auto |
|
88 |
|
89 proposition remove_hd [simp]: "remove1 z (z # xs) = xs" |
|
90 by auto |
|
91 |
|
92 proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" |
|
93 by (drule perm_remove_perm [where z = z]) auto |
|
94 |
|
95 proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" |
|
96 by (meson cons_perm_imp_perm perm.Cons) |
|
97 |
|
98 proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" |
|
99 by (induct zs arbitrary: xs ys rule: rev_induct) auto |
|
100 |
|
101 proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys" |
|
102 by (blast intro: append_perm_imp_perm perm_append1) |
|
103 |
|
104 proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys" |
|
105 by (meson perm.trans perm_append1_eq perm_append_swap) |
|
106 |
|
107 theorem mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys" |
|
108 proof |
|
109 assume "mset xs = mset ys" |
|
110 then show "xs <~~> ys" |
|
111 proof (induction xs arbitrary: ys) |
|
112 case (Cons x xs) |
|
113 then have "x \<in> set ys" |
|
114 using mset_eq_setD by fastforce |
|
115 then show ?case |
|
116 by (metis Cons.IH Cons.prems mset_remove1 perm.Cons perm.trans perm_remove perm_sym remove_hd) |
|
117 qed auto |
|
118 next |
|
119 assume "xs <~~> ys" |
|
120 then show "mset xs = mset ys" |
|
121 by induction (simp_all add: union_ac) |
|
122 qed |
|
123 |
|
124 proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
|
125 apply (rule iffI) |
|
126 apply (metis mset_append mset_eq_perm mset_subset_eq_exists_conv surjD surj_mset) |
|
127 by (metis mset_append mset_eq_perm mset_subset_eq_exists_conv) |
|
128 |
|
129 proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
|
130 by (metis mset_eq_perm mset_eq_setD) |
|
131 |
|
132 proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" |
|
133 by (metis card_distinct distinct_card perm_length perm_set_eq) |
|
134 |
|
135 theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" |
|
136 proof (induction xs arbitrary: ys rule: length_induct) |
|
137 case (1 xs) |
|
138 show ?case |
|
139 proof (cases "remdups xs") |
|
140 case Nil |
|
141 with "1.prems" show ?thesis |
|
142 using "1.prems" by auto |
|
143 next |
|
144 case (Cons x us) |
|
145 then have "x \<in> set (remdups ys)" |
|
146 using "1.prems" set_remdups by fastforce |
|
147 then show ?thesis |
|
148 using "1.prems" mset_eq_perm set_eq_iff_mset_remdups_eq by blast |
|
149 qed |
|
150 qed |
|
151 |
|
152 proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y" |
|
153 by (metis List.set_remdups perm_set_eq eq_set_perm_remdups) |
|
154 |
|
155 theorem permutation_Ex_bij: |
|
156 assumes "xs <~~> ys" |
|
157 shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" |
|
158 using assms |
|
159 proof induct |
|
160 case Nil |
|
161 then show ?case |
|
162 unfolding bij_betw_def by simp |
|
163 next |
|
164 case (swap y x l) |
|
165 show ?case |
|
166 proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI) |
|
167 show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}" |
|
168 by (auto simp: bij_betw_def) |
|
169 fix i |
|
170 assume "i < length (y # x # l)" |
|
171 show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i" |
|
172 by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc) |
|
173 qed |
|
174 next |
|
175 case (Cons xs ys z) |
|
176 then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" |
|
177 and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" |
|
178 by blast |
|
179 let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0" |
|
180 show ?case |
|
181 proof (intro exI[of _ ?f] allI conjI impI) |
|
182 have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}" |
|
183 "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}" |
|
184 by (simp_all add: lessThan_Suc_eq_insert_0) |
|
185 show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" |
|
186 unfolding * |
|
187 proof (rule bij_betw_combine) |
|
188 show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})" |
|
189 using bij unfolding bij_betw_def |
|
190 by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def) |
|
191 qed (auto simp: bij_betw_def) |
|
192 fix i |
|
193 assume "i < length (z # xs)" |
|
194 then show "(z # xs) ! i = (z # ys) ! (?f i)" |
|
195 using perm by (cases i) auto |
|
196 qed |
|
197 next |
|
198 case (trans xs ys zs) |
|
199 then obtain f g |
|
200 where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" |
|
201 and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" |
|
202 by blast |
|
203 show ?case |
|
204 proof (intro exI[of _ "g \<circ> f"] conjI allI impI) |
|
205 show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}" |
|
206 using bij by (rule bij_betw_trans) |
|
207 fix i |
|
208 assume "i < length xs" |
|
209 with bij have "f i < length ys" |
|
210 unfolding bij_betw_def by force |
|
211 with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i" |
|
212 using trans(1,3)[THEN perm_length] perm by auto |
|
213 qed |
|
214 qed |
|
215 |
|
216 proposition perm_finite: "finite {B. B <~~> A}" |
|
217 proof (rule finite_subset[where B="{xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"]) |
|
218 show "finite {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}" |
|
219 using finite_lists_length_le by blast |
|
220 next |
|
221 show "{B. B <~~> A} \<subseteq> {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}" |
|
222 by (clarsimp simp add: perm_length perm_set_eq) |
|
223 qed |
|
224 |
|
225 proposition perm_swap: |
|
226 assumes "i < length xs" "j < length xs" |
|
227 shows "xs[i := xs ! j, j := xs ! i] <~~> xs" |
|
228 using assms by (simp add: mset_eq_perm[symmetric] mset_swap) |
|
229 |
|
230 end |
|