author | paulson <lp15@cam.ac.uk> |
Tue, 10 Sep 2019 14:40:00 +0100 | |
changeset 70680 | b8cd7ea34e33 |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
11054 | 1 |
(* Title: HOL/Library/Permutation.thy |
15005 | 2 |
Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker |
11054 | 3 |
*) |
4 |
||
60500 | 5 |
section \<open>Permutations\<close> |
11054 | 6 |
|
15131 | 7 |
theory Permutation |
51542 | 8 |
imports Multiset |
15131 | 9 |
begin |
11054 | 10 |
|
70680 | 11 |
inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50) |
53238 | 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" |
|
11054 | 17 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
18 |
proposition perm_refl [iff]: "l <~~> l" |
17200 | 19 |
by (induct l) auto |
11054 | 20 |
|
21 |
||
60500 | 22 |
subsection \<open>Some examples of rule induction on permutations\<close> |
11054 | 23 |
|
70680 | 24 |
proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" |
25 |
by (induction "[] :: 'a list" ys pred: perm) simp_all |
|
11054 | 26 |
|
27 |
||
60500 | 28 |
text \<open>\medskip This more general theorem is easier to understand!\<close> |
11054 | 29 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
30 |
proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys" |
25379 | 31 |
by (induct pred: perm) simp_all |
11054 | 32 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
33 |
proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" |
25379 | 34 |
by (induct pred: perm) auto |
11054 | 35 |
|
36 |
||
60500 | 37 |
subsection \<open>Ways of making new permutations\<close> |
11054 | 38 |
|
60500 | 39 |
text \<open>We can insert the head anywhere in the list.\<close> |
11054 | 40 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
41 |
proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" |
17200 | 42 |
by (induct xs) auto |
11054 | 43 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
44 |
proposition perm_append_swap: "xs @ ys <~~> ys @ xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
45 |
by (induct xs) (auto intro: perm_append_Cons) |
11054 | 46 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
47 |
proposition perm_append_single: "a # xs <~~> xs @ [a]" |
17200 | 48 |
by (rule perm.trans [OF _ perm_append_swap]) simp |
11054 | 49 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
50 |
proposition perm_rev: "rev xs <~~> xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
51 |
by (induct xs) (auto intro!: perm_append_single intro: perm_sym) |
11054 | 52 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
53 |
proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys" |
17200 | 54 |
by (induct l) auto |
11054 | 55 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
56 |
proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l" |
17200 | 57 |
by (blast intro!: perm_append_swap perm_append1) |
11054 | 58 |
|
59 |
||
60500 | 60 |
subsection \<open>Further results\<close> |
11054 | 61 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
62 |
proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []" |
17200 | 63 |
by (blast intro: perm_empty_imp) |
11054 | 64 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
65 |
proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []" |
70680 | 66 |
using perm_sym by auto |
11054 | 67 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
68 |
proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]" |
25379 | 69 |
by (induct pred: perm) auto |
11054 | 70 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
71 |
proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]" |
17200 | 72 |
by (blast intro: perm_sing_imp) |
11054 | 73 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
74 |
proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]" |
17200 | 75 |
by (blast dest: perm_sym) |
11054 | 76 |
|
77 |
||
60500 | 78 |
subsection \<open>Removing elements\<close> |
11054 | 79 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
80 |
proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" |
17200 | 81 |
by (induct ys) auto |
11054 | 82 |
|
83 |
||
60500 | 84 |
text \<open>\medskip Congruence rule\<close> |
11054 | 85 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
86 |
proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" |
25379 | 87 |
by (induct pred: perm) auto |
11054 | 88 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
89 |
proposition remove_hd [simp]: "remove1 z (z # xs) = xs" |
15072 | 90 |
by auto |
11054 | 91 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
92 |
proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" |
63649 | 93 |
by (drule perm_remove_perm [where z = z]) auto |
11054 | 94 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
95 |
proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" |
70680 | 96 |
by (meson cons_perm_imp_perm perm.Cons) |
11054 | 97 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
98 |
proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" |
53238 | 99 |
by (induct zs arbitrary: xs ys rule: rev_induct) auto |
11054 | 100 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
101 |
proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys" |
17200 | 102 |
by (blast intro: append_perm_imp_perm perm_append1) |
11054 | 103 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
104 |
proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys" |
70680 | 105 |
by (meson perm.trans perm_append1_eq perm_append_swap) |
11054 | 106 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
107 |
theorem mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys" |
70680 | 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 |
|
15005 | 123 |
|
64587 | 124 |
proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
70680 | 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) |
|
15005 | 128 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
129 |
proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
60515 | 130 |
by (metis mset_eq_perm mset_eq_setD) |
25277 | 131 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
132 |
proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" |
70680 | 133 |
by (metis card_distinct distinct_card perm_length perm_set_eq) |
25277 | 134 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
135 |
theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" |
70680 | 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 |
|
25287 | 151 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
152 |
proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y" |
25379 | 153 |
by (metis List.set_remdups perm_set_eq eq_set_perm_remdups) |
25287 | 154 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
155 |
theorem permutation_Ex_bij: |
39075 | 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))" |
|
56796 | 158 |
using assms |
159 |
proof induct |
|
53238 | 160 |
case Nil |
56796 | 161 |
then show ?case |
162 |
unfolding bij_betw_def by simp |
|
39075 | 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)}" |
|
50037 | 168 |
by (auto simp: bij_betw_def) |
53238 | 169 |
fix i |
56796 | 170 |
assume "i < length (y # x # l)" |
39075 | 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) |
|
56796 | 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 |
|
53238 | 179 |
let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0" |
39075 | 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}" |
|
39078 | 184 |
by (simp_all add: lessThan_Suc_eq_insert_0) |
53238 | 185 |
show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" |
186 |
unfolding * |
|
39075 | 187 |
proof (rule bij_betw_combine) |
188 |
show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})" |
|
189 |
using bij unfolding bij_betw_def |
|
56154
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
55584
diff
changeset
|
190 |
by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def) |
39075 | 191 |
qed (auto simp: bij_betw_def) |
53238 | 192 |
fix i |
56796 | 193 |
assume "i < length (z # xs)" |
39075 | 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) |
|
56796 | 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 |
|
39075 | 203 |
show ?case |
53238 | 204 |
proof (intro exI[of _ "g \<circ> f"] conjI allI impI) |
39075 | 205 |
show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}" |
206 |
using bij by (rule bij_betw_trans) |
|
56796 | 207 |
fix i |
208 |
assume "i < length xs" |
|
209 |
with bij have "f i < length ys" |
|
210 |
unfolding bij_betw_def by force |
|
60500 | 211 |
with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i" |
53238 | 212 |
using trans(1,3)[THEN perm_length] perm by auto |
39075 | 213 |
qed |
214 |
qed |
|
215 |
||
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
216 |
proposition perm_finite: "finite {B. B <~~> A}" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
217 |
proof (rule finite_subset[where B="{xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"]) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
218 |
show "finite {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}" |
70680 | 219 |
using finite_lists_length_le by blast |
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
220 |
next |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
221 |
show "{B. B <~~> A} \<subseteq> {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
222 |
by (clarsimp simp add: perm_length perm_set_eq) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
223 |
qed |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
224 |
|
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
225 |
proposition perm_swap: |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
226 |
assumes "i < length xs" "j < length xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
227 |
shows "xs[i := xs ! j, j := xs ! i] <~~> xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
228 |
using assms by (simp add: mset_eq_perm[symmetric] mset_swap) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
229 |
|
11054 | 230 |
end |