author | nipkow |
Wed, 17 Jun 2015 17:21:11 +0200 | |
changeset 60495 | d7ff0a1df90a |
parent 60397 | f8a513fedb31 |
child 60502 | aa58872267ee |
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 |
||
58881 | 5 |
section {* Permutations *} |
11054 | 6 |
|
15131 | 7 |
theory Permutation |
51542 | 8 |
imports Multiset |
15131 | 9 |
begin |
11054 | 10 |
|
53238 | 11 |
inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ <~~> _" [50, 50] 50) (* FIXME proper infix, without ambiguity!? *) |
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 |
|
18 |
lemma perm_refl [iff]: "l <~~> l" |
|
17200 | 19 |
by (induct l) auto |
11054 | 20 |
|
21 |
||
22 |
subsection {* Some examples of rule induction on permutations *} |
|
23 |
||
53238 | 24 |
lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" |
56796 | 25 |
by (induct xs == "[] :: 'a list" ys pred: perm) simp_all |
11054 | 26 |
|
27 |
||
56796 | 28 |
text {* \medskip This more general theorem is easier to understand! *} |
11054 | 29 |
|
53238 | 30 |
lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys" |
25379 | 31 |
by (induct pred: perm) simp_all |
11054 | 32 |
|
53238 | 33 |
lemma perm_empty_imp: "[] <~~> xs \<Longrightarrow> xs = []" |
17200 | 34 |
by (drule perm_length) auto |
11054 | 35 |
|
53238 | 36 |
lemma perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" |
25379 | 37 |
by (induct pred: perm) auto |
11054 | 38 |
|
39 |
||
40 |
subsection {* Ways of making new permutations *} |
|
41 |
||
56796 | 42 |
text {* We can insert the head anywhere in the list. *} |
11054 | 43 |
|
44 |
lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" |
|
17200 | 45 |
by (induct xs) auto |
11054 | 46 |
|
47 |
lemma perm_append_swap: "xs @ ys <~~> ys @ xs" |
|
17200 | 48 |
apply (induct xs) |
49 |
apply simp_all |
|
11054 | 50 |
apply (blast intro: perm_append_Cons) |
51 |
done |
|
52 |
||
53 |
lemma perm_append_single: "a # xs <~~> xs @ [a]" |
|
17200 | 54 |
by (rule perm.trans [OF _ perm_append_swap]) simp |
11054 | 55 |
|
56 |
lemma perm_rev: "rev xs <~~> xs" |
|
17200 | 57 |
apply (induct xs) |
58 |
apply simp_all |
|
11153 | 59 |
apply (blast intro!: perm_append_single intro: perm_sym) |
11054 | 60 |
done |
61 |
||
53238 | 62 |
lemma perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys" |
17200 | 63 |
by (induct l) auto |
11054 | 64 |
|
53238 | 65 |
lemma perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l" |
17200 | 66 |
by (blast intro!: perm_append_swap perm_append1) |
11054 | 67 |
|
68 |
||
69 |
subsection {* Further results *} |
|
70 |
||
56796 | 71 |
lemma perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []" |
17200 | 72 |
by (blast intro: perm_empty_imp) |
11054 | 73 |
|
56796 | 74 |
lemma perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []" |
11054 | 75 |
apply auto |
76 |
apply (erule perm_sym [THEN perm_empty_imp]) |
|
77 |
done |
|
78 |
||
53238 | 79 |
lemma perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]" |
25379 | 80 |
by (induct pred: perm) auto |
11054 | 81 |
|
56796 | 82 |
lemma perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]" |
17200 | 83 |
by (blast intro: perm_sing_imp) |
11054 | 84 |
|
56796 | 85 |
lemma perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]" |
17200 | 86 |
by (blast dest: perm_sym) |
11054 | 87 |
|
88 |
||
89 |
subsection {* Removing elements *} |
|
90 |
||
53238 | 91 |
lemma perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" |
17200 | 92 |
by (induct ys) auto |
11054 | 93 |
|
94 |
||
95 |
text {* \medskip Congruence rule *} |
|
96 |
||
53238 | 97 |
lemma perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" |
25379 | 98 |
by (induct pred: perm) auto |
11054 | 99 |
|
36903 | 100 |
lemma remove_hd [simp]: "remove1 z (z # xs) = xs" |
15072 | 101 |
by auto |
11054 | 102 |
|
53238 | 103 |
lemma cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" |
17200 | 104 |
by (drule_tac z = z in perm_remove_perm) auto |
11054 | 105 |
|
56796 | 106 |
lemma cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" |
17200 | 107 |
by (blast intro: cons_perm_imp_perm) |
11054 | 108 |
|
53238 | 109 |
lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" |
110 |
by (induct zs arbitrary: xs ys rule: rev_induct) auto |
|
11054 | 111 |
|
56796 | 112 |
lemma perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys" |
17200 | 113 |
by (blast intro: append_perm_imp_perm perm_append1) |
11054 | 114 |
|
56796 | 115 |
lemma perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys" |
11054 | 116 |
apply (safe intro!: perm_append2) |
117 |
apply (rule append_perm_imp_perm) |
|
118 |
apply (rule perm_append_swap [THEN perm.trans]) |
|
119 |
-- {* the previous step helps this @{text blast} call succeed quickly *} |
|
120 |
apply (blast intro: perm_append_swap) |
|
121 |
done |
|
122 |
||
56796 | 123 |
lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys" |
17200 | 124 |
apply (rule iffI) |
56796 | 125 |
apply (erule_tac [2] perm.induct) |
126 |
apply (simp_all add: union_ac) |
|
127 |
apply (erule rev_mp) |
|
128 |
apply (rule_tac x=ys in spec) |
|
129 |
apply (induct_tac xs) |
|
130 |
apply auto |
|
131 |
apply (erule_tac x = "remove1 a x" in allE) |
|
132 |
apply (drule sym) |
|
133 |
apply simp |
|
17200 | 134 |
apply (subgoal_tac "a \<in> set x") |
53238 | 135 |
apply (drule_tac z = a in perm.Cons) |
56796 | 136 |
apply (erule perm.trans) |
137 |
apply (rule perm_sym) |
|
138 |
apply (erule perm_remove) |
|
60495 | 139 |
apply (drule_tac f=set_mset in arg_cong) |
56796 | 140 |
apply simp |
15005 | 141 |
done |
142 |
||
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
58881
diff
changeset
|
143 |
lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
17200 | 144 |
apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) |
56796 | 145 |
apply (insert surj_multiset_of) |
146 |
apply (drule surjD) |
|
15072 | 147 |
apply (blast intro: sym)+ |
148 |
done |
|
15005 | 149 |
|
53238 | 150 |
lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
25379 | 151 |
by (metis multiset_of_eq_perm multiset_of_eq_setD) |
25277 | 152 |
|
53238 | 153 |
lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" |
25379 | 154 |
apply (induct pred: perm) |
155 |
apply simp_all |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
40122
diff
changeset
|
156 |
apply fastforce |
25379 | 157 |
apply (metis perm_set_eq) |
158 |
done |
|
25277 | 159 |
|
53238 | 160 |
lemma eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" |
25379 | 161 |
apply (induct xs arbitrary: ys rule: length_induct) |
53238 | 162 |
apply (case_tac "remdups xs") |
163 |
apply simp_all |
|
164 |
apply (subgoal_tac "a \<in> set (remdups ys)") |
|
57816
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
56796
diff
changeset
|
165 |
prefer 2 apply (metis list.set(2) insert_iff set_remdups) |
56796 | 166 |
apply (drule split_list) apply (elim exE conjE) |
167 |
apply (drule_tac x = list in spec) apply (erule impE) prefer 2 |
|
168 |
apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2 |
|
25379 | 169 |
apply simp |
53238 | 170 |
apply (subgoal_tac "a # list <~~> a # ysa @ zs") |
25379 | 171 |
apply (metis Cons_eq_appendI perm_append_Cons trans) |
40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
39916
diff
changeset
|
172 |
apply (metis Cons Cons_eq_appendI distinct.simps(2) |
25379 | 173 |
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff) |
56796 | 174 |
apply (subgoal_tac "set (a # list) = |
175 |
set (ysa @ a # zs) \<and> distinct (a # list) \<and> distinct (ysa @ a # zs)") |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
40122
diff
changeset
|
176 |
apply (fastforce simp add: insert_ident) |
25379 | 177 |
apply (metis distinct_remdups set_remdups) |
30742 | 178 |
apply (subgoal_tac "length (remdups xs) < Suc (length xs)") |
179 |
apply simp |
|
180 |
apply (subgoal_tac "length (remdups xs) \<le> length xs") |
|
181 |
apply simp |
|
182 |
apply (rule length_remdups_leq) |
|
25379 | 183 |
done |
25287 | 184 |
|
56796 | 185 |
lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y" |
25379 | 186 |
by (metis List.set_remdups perm_set_eq eq_set_perm_remdups) |
25287 | 187 |
|
39075 | 188 |
lemma permutation_Ex_bij: |
189 |
assumes "xs <~~> ys" |
|
190 |
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" |
|
56796 | 191 |
using assms |
192 |
proof induct |
|
53238 | 193 |
case Nil |
56796 | 194 |
then show ?case |
195 |
unfolding bij_betw_def by simp |
|
39075 | 196 |
next |
197 |
case (swap y x l) |
|
198 |
show ?case |
|
199 |
proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI) |
|
200 |
show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}" |
|
50037 | 201 |
by (auto simp: bij_betw_def) |
53238 | 202 |
fix i |
56796 | 203 |
assume "i < length (y # x # l)" |
39075 | 204 |
show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i" |
205 |
by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc) |
|
206 |
qed |
|
207 |
next |
|
208 |
case (Cons xs ys z) |
|
56796 | 209 |
then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" |
210 |
and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" |
|
211 |
by blast |
|
53238 | 212 |
let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0" |
39075 | 213 |
show ?case |
214 |
proof (intro exI[of _ ?f] allI conjI impI) |
|
215 |
have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}" |
|
216 |
"{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}" |
|
39078 | 217 |
by (simp_all add: lessThan_Suc_eq_insert_0) |
53238 | 218 |
show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" |
219 |
unfolding * |
|
39075 | 220 |
proof (rule bij_betw_combine) |
221 |
show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})" |
|
222 |
using bij unfolding bij_betw_def |
|
56154
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
55584
diff
changeset
|
223 |
by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def) |
39075 | 224 |
qed (auto simp: bij_betw_def) |
53238 | 225 |
fix i |
56796 | 226 |
assume "i < length (z # xs)" |
39075 | 227 |
then show "(z # xs) ! i = (z # ys) ! (?f i)" |
228 |
using perm by (cases i) auto |
|
229 |
qed |
|
230 |
next |
|
231 |
case (trans xs ys zs) |
|
56796 | 232 |
then obtain f g |
233 |
where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" |
|
234 |
and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" |
|
235 |
by blast |
|
39075 | 236 |
show ?case |
53238 | 237 |
proof (intro exI[of _ "g \<circ> f"] conjI allI impI) |
39075 | 238 |
show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}" |
239 |
using bij by (rule bij_betw_trans) |
|
56796 | 240 |
fix i |
241 |
assume "i < length xs" |
|
242 |
with bij have "f i < length ys" |
|
243 |
unfolding bij_betw_def by force |
|
39075 | 244 |
with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i" |
53238 | 245 |
using trans(1,3)[THEN perm_length] perm by auto |
39075 | 246 |
qed |
247 |
qed |
|
248 |
||
11054 | 249 |
end |