author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64587  8355a6e2df79 
child 69597  ff784d5a5bfb 
permissions  rwrr 
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 

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 

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 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

24 
proposition xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" 
56796  25 
by (induct xs == "[] :: '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_empty_imp: "[] <~~> xs \<Longrightarrow> xs = []" 
17200  34 
by (drule perm_length) auto 
11054  35 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

36 
proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" 
25379  37 
by (induct pred: perm) auto 
11054  38 

39 

60500  40 
subsection \<open>Ways of making new permutations\<close> 
11054  41 

60500  42 
text \<open>We can insert the head anywhere in the list.\<close> 
11054  43 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

44 
proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" 
17200  45 
by (induct xs) auto 
11054  46 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

47 
proposition perm_append_swap: "xs @ ys <~~> ys @ xs" 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

48 
by (induct xs) (auto intro: perm_append_Cons) 
11054  49 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

50 
proposition perm_append_single: "a # xs <~~> xs @ [a]" 
17200  51 
by (rule perm.trans [OF _ perm_append_swap]) simp 
11054  52 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

53 
proposition perm_rev: "rev xs <~~> xs" 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

54 
by (induct xs) (auto intro!: perm_append_single intro: perm_sym) 
11054  55 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

56 
proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys" 
17200  57 
by (induct l) auto 
11054  58 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

59 
proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l" 
17200  60 
by (blast intro!: perm_append_swap perm_append1) 
11054  61 

62 

60500  63 
subsection \<open>Further results\<close> 
11054  64 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

65 
proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []" 
17200  66 
by (blast intro: perm_empty_imp) 
11054  67 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

68 
proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []" 
11054  69 
apply auto 
70 
apply (erule perm_sym [THEN perm_empty_imp]) 

71 
done 

72 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

73 
proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]" 
25379  74 
by (induct pred: perm) auto 
11054  75 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

76 
proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]" 
17200  77 
by (blast intro: perm_sing_imp) 
11054  78 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

79 
proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]" 
17200  80 
by (blast dest: perm_sym) 
11054  81 

82 

60500  83 
subsection \<open>Removing elements\<close> 
11054  84 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

85 
proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" 
17200  86 
by (induct ys) auto 
11054  87 

88 

60500  89 
text \<open>\medskip Congruence rule\<close> 
11054  90 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

91 
proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" 
25379  92 
by (induct pred: perm) auto 
11054  93 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

94 
proposition remove_hd [simp]: "remove1 z (z # xs) = xs" 
15072  95 
by auto 
11054  96 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

97 
proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" 
63649  98 
by (drule perm_remove_perm [where z = z]) auto 
11054  99 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

100 
proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" 
17200  101 
by (blast intro: cons_perm_imp_perm) 
11054  102 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

103 
proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" 
53238  104 
by (induct zs arbitrary: xs ys rule: rev_induct) auto 
11054  105 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

106 
proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys" 
17200  107 
by (blast intro: append_perm_imp_perm perm_append1) 
11054  108 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

109 
proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys" 
11054  110 
apply (safe intro!: perm_append2) 
111 
apply (rule append_perm_imp_perm) 

112 
apply (rule perm_append_swap [THEN perm.trans]) 

61585  113 
\<comment> \<open>the previous step helps this \<open>blast\<close> call succeed quickly\<close> 
11054  114 
apply (blast intro: perm_append_swap) 
115 
done 

116 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

117 
theorem mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys" 
17200  118 
apply (rule iffI) 
56796  119 
apply (erule_tac [2] perm.induct) 
120 
apply (simp_all add: union_ac) 

121 
apply (erule rev_mp) 

122 
apply (rule_tac x=ys in spec) 

123 
apply (induct_tac xs) 

124 
apply auto 

125 
apply (erule_tac x = "remove1 a x" in allE) 

126 
apply (drule sym) 

127 
apply simp 

17200  128 
apply (subgoal_tac "a \<in> set x") 
53238  129 
apply (drule_tac z = a in perm.Cons) 
56796  130 
apply (erule perm.trans) 
131 
apply (rule perm_sym) 

132 
apply (erule perm_remove) 

60495  133 
apply (drule_tac f=set_mset in arg_cong) 
56796  134 
apply simp 
15005  135 
done 
136 

64587  137 
proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
61699
diff
changeset

138 
apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv) 
60515  139 
apply (insert surj_mset) 
56796  140 
apply (drule surjD) 
15072  141 
apply (blast intro: sym)+ 
142 
done 

15005  143 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

144 
proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" 
60515  145 
by (metis mset_eq_perm mset_eq_setD) 
25277  146 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

147 
proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" 
25379  148 
apply (induct pred: perm) 
149 
apply simp_all 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
40122
diff
changeset

150 
apply fastforce 
25379  151 
apply (metis perm_set_eq) 
152 
done 

25277  153 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

154 
theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" 
25379  155 
apply (induct xs arbitrary: ys rule: length_induct) 
53238  156 
apply (case_tac "remdups xs") 
157 
apply simp_all 

158 
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

159 
prefer 2 apply (metis list.set(2) insert_iff set_remdups) 
56796  160 
apply (drule split_list) apply (elim exE conjE) 
161 
apply (drule_tac x = list in spec) apply (erule impE) prefer 2 

162 
apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2 

25379  163 
apply simp 
53238  164 
apply (subgoal_tac "a # list <~~> a # ysa @ zs") 
25379  165 
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

166 
apply (metis Cons Cons_eq_appendI distinct.simps(2) 
25379  167 
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff) 
56796  168 
apply (subgoal_tac "set (a # list) = 
169 
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

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 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

179 
proposition 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 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

182 
theorem permutation_Ex_bij: 
39075  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))" 

56796  185 
using assms 
186 
proof induct 

53238  187 
case Nil 
56796  188 
then show ?case 
189 
unfolding bij_betw_def by simp 

39075  190 
next 
191 
case (swap y x l) 

192 
show ?case 

193 
proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI) 

194 
show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}" 

50037  195 
by (auto simp: bij_betw_def) 
53238  196 
fix i 
56796  197 
assume "i < length (y # x # l)" 
39075  198 
show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i" 
199 
by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc) 

200 
qed 

201 
next 

202 
case (Cons xs ys z) 

56796  203 
then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" 
204 
and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" 

205 
by blast 

53238  206 
let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n)  0 \<Rightarrow> 0" 
39075  207 
show ?case 
208 
proof (intro exI[of _ ?f] allI conjI impI) 

209 
have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}" 

210 
"{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}" 

39078  211 
by (simp_all add: lessThan_Suc_eq_insert_0) 
53238  212 
show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" 
213 
unfolding * 

39075  214 
proof (rule bij_betw_combine) 
215 
show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})" 

216 
using bij unfolding bij_betw_def 

56154
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
55584
diff
changeset

217 
by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def) 
39075  218 
qed (auto simp: bij_betw_def) 
53238  219 
fix i 
56796  220 
assume "i < length (z # xs)" 
39075  221 
then show "(z # xs) ! i = (z # ys) ! (?f i)" 
222 
using perm by (cases i) auto 

223 
qed 

224 
next 

225 
case (trans xs ys zs) 

56796  226 
then obtain f g 
227 
where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" 

228 
and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" 

229 
by blast 

39075  230 
show ?case 
53238  231 
proof (intro exI[of _ "g \<circ> f"] conjI allI impI) 
39075  232 
show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}" 
233 
using bij by (rule bij_betw_trans) 

56796  234 
fix i 
235 
assume "i < length xs" 

236 
with bij have "f i < length ys" 

237 
unfolding bij_betw_def by force 

60500  238 
with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i" 
53238  239 
using trans(1,3)[THEN perm_length] perm by auto 
39075  240 
qed 
241 
qed 

242 

61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

243 
proposition perm_finite: "finite {B. B <~~> A}" 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

244 
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

245 
show "finite {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

246 
apply (cases A, simp) 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

247 
apply (rule card_ge_0_finite) 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

248 
apply (auto simp: card_lists_length_le) 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

249 
done 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

250 
next 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

251 
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

252 
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

253 
qed 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

254 

a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

255 
proposition perm_swap: 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

256 
assumes "i < length xs" "j < length xs" 
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

257 
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

258 
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

259 

11054  260 
end 