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