author  wenzelm 
Tue, 27 Aug 2013 22:40:39 +0200  
changeset 53238  01ef0a103fc9 
parent 51542  738598beeb26 
child 55584  a879f14b6f95 
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 

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 