6 
6 
7 theory Permutation 
7 theory Permutation 
8 imports Multiset 
8 imports Multiset 
9 begin 
9 begin 
10 
10 
11 inductive 
11 inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ <~~> _" [50, 50] 50) (* FIXME proper infix, without ambiguity!? *) 
12 perm :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) 
12 where 
13 where 
13 Nil [intro!]: "[] <~~> []" 
14 Nil [intro!]: "[] <~~> []" 
14  swap [intro!]: "y # x # l <~~> x # y # l" 
15  swap [intro!]: "y # x # l <~~> x # y # l" 
15  Cons [intro!]: "xs <~~> ys \<Longrightarrow> z # xs <~~> z # ys" 
16  Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys" 
16  trans [intro]: "xs <~~> ys \<Longrightarrow> ys <~~> zs \<Longrightarrow> xs <~~> zs" 
17  trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs" 

18 
17 
19 lemma perm_refl [iff]: "l <~~> l" 
18 lemma perm_refl [iff]: "l <~~> l" 
20 by (induct l) auto 
19 by (induct l) auto 
21 
20 
22 
21 
23 subsection {* Some examples of rule induction on permutations *} 
22 subsection {* Some examples of rule induction on permutations *} 
24 
23 
25 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []" 
24 lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" 
26 by (induct xs == "[]::'a list" ys pred: perm) simp_all 
25 by (induct xs == "[]::'a list" ys pred: perm) simp_all 
27 
26 
28 
27 
29 text {* 
28 text {* 
30 \medskip This more general theorem is easier to understand! 
29 \medskip This more general theorem is easier to understand! 
31 *} 
30 *} 
32 
31 
33 lemma perm_length: "xs <~~> ys ==> length xs = length ys" 
32 lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys" 
34 by (induct pred: perm) simp_all 
33 by (induct pred: perm) simp_all 
35 
34 
36 lemma perm_empty_imp: "[] <~~> xs ==> xs = []" 
35 lemma perm_empty_imp: "[] <~~> xs \<Longrightarrow> xs = []" 
37 by (drule perm_length) auto 
36 by (drule perm_length) auto 
38 
37 
39 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs" 
38 lemma perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" 
40 by (induct pred: perm) auto 
39 by (induct pred: perm) auto 
41 
40 
42 
41 
43 subsection {* Ways of making new permutations *} 
42 subsection {* Ways of making new permutations *} 
44 
43 
91 by (blast dest: perm_sym) 
90 by (blast dest: perm_sym) 
92 
91 
93 
92 
94 subsection {* Removing elements *} 
93 subsection {* Removing elements *} 
95 
94 
96 lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove1 x ys" 
95 lemma perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" 
97 by (induct ys) auto 
96 by (induct ys) auto 
98 
97 
99 
98 
100 text {* \medskip Congruence rule *} 
99 text {* \medskip Congruence rule *} 
101 
100 
102 lemma perm_remove_perm: "xs <~~> ys ==> remove1 z xs <~~> remove1 z ys" 
101 lemma perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" 
103 by (induct pred: perm) auto 
102 by (induct pred: perm) auto 
104 
103 
105 lemma remove_hd [simp]: "remove1 z (z # xs) = xs" 
104 lemma remove_hd [simp]: "remove1 z (z # xs) = xs" 
106 by auto 
105 by auto 
107 
106 
108 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys" 
107 lemma cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" 
109 by (drule_tac z = z in perm_remove_perm) auto 
108 by (drule_tac z = z in perm_remove_perm) auto 
110 
109 
111 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)" 
110 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)" 
112 by (blast intro: cons_perm_imp_perm) 
111 by (blast intro: cons_perm_imp_perm) 
113 
112 
114 lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys ==> xs <~~> ys" 
113 lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" 
115 apply (induct zs arbitrary: xs ys rule: rev_induct) 
114 by (induct zs arbitrary: xs ys rule: rev_induct) auto 
116 apply (simp_all (no_asm_use)) 

117 apply blast 

118 done 

119 
115 
120 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)" 
116 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)" 
121 by (blast intro: append_perm_imp_perm perm_append1) 
117 by (blast intro: append_perm_imp_perm perm_append1) 
122 
118 
123 lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)" 
119 lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)" 
133 apply (erule_tac [2] perm.induct, simp_all add: union_ac) 
129 apply (erule_tac [2] perm.induct, simp_all add: union_ac) 
134 apply (erule rev_mp, rule_tac x=ys in spec) 
130 apply (erule rev_mp, rule_tac x=ys in spec) 
135 apply (induct_tac xs, auto) 
131 apply (induct_tac xs, auto) 
136 apply (erule_tac x = "remove1 a x" in allE, drule sym, simp) 
132 apply (erule_tac x = "remove1 a x" in allE, drule sym, simp) 
137 apply (subgoal_tac "a \<in> set x") 
133 apply (subgoal_tac "a \<in> set x") 
138 apply (drule_tac z=a in perm.Cons) 
134 apply (drule_tac z = a in perm.Cons) 
139 apply (erule perm.trans, rule perm_sym, erule perm_remove) 
135 apply (erule perm.trans, rule perm_sym, erule perm_remove) 
140 apply (drule_tac f=set_of in arg_cong, simp) 
136 apply (drule_tac f=set_of in arg_cong, simp) 
141 done 
137 done 
142 
138 
143 lemma multiset_of_le_perm_append: 
139 lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" 
144 "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" 

145 apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) 
140 apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) 
146 apply (insert surj_multiset_of, drule surjD) 
141 apply (insert surj_multiset_of, drule surjD) 
147 apply (blast intro: sym)+ 
142 apply (blast intro: sym)+ 
148 done 
143 done 
149 
144 
150 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys" 
145 lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" 
151 by (metis multiset_of_eq_perm multiset_of_eq_setD) 
146 by (metis multiset_of_eq_perm multiset_of_eq_setD) 
152 
147 
153 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys" 
148 lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" 
154 apply (induct pred: perm) 
149 apply (induct pred: perm) 
155 apply simp_all 
150 apply simp_all 
156 apply fastforce 
151 apply fastforce 
157 apply (metis perm_set_eq) 
152 apply (metis perm_set_eq) 
158 done 
153 done 
159 
154 
160 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys" 
155 lemma eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" 
161 apply (induct xs arbitrary: ys rule: length_induct) 
156 apply (induct xs arbitrary: ys rule: length_induct) 
162 apply (case_tac "remdups xs", simp, simp) 
157 apply (case_tac "remdups xs") 
163 apply (subgoal_tac "a : set (remdups ys)") 
158 apply simp_all 

159 apply (subgoal_tac "a \<in> set (remdups ys)") 
164 prefer 2 apply (metis set.simps(2) insert_iff set_remdups) 
160 prefer 2 apply (metis set.simps(2) insert_iff set_remdups) 
165 apply (drule split_list) apply(elim exE conjE) 
161 apply (drule split_list) apply(elim exE conjE) 
166 apply (drule_tac x=list in spec) apply(erule impE) prefer 2 
162 apply (drule_tac x=list in spec) apply(erule impE) prefer 2 
167 apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2 
163 apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2 
168 apply simp 
164 apply simp 
169 apply (subgoal_tac "a#list <~~> a#ysa@zs") 
165 apply (subgoal_tac "a # list <~~> a # ysa @ zs") 
170 apply (metis Cons_eq_appendI perm_append_Cons trans) 
166 apply (metis Cons_eq_appendI perm_append_Cons trans) 
171 apply (metis Cons Cons_eq_appendI distinct.simps(2) 
167 apply (metis Cons Cons_eq_appendI distinct.simps(2) 
172 distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff) 
168 distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff) 
173 apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)") 
169 apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)") 
174 apply (fastforce simp add: insert_ident) 
170 apply (fastforce simp add: insert_ident) 
178 apply (subgoal_tac "length (remdups xs) \<le> length xs") 
174 apply (subgoal_tac "length (remdups xs) \<le> length xs") 
179 apply simp 
175 apply simp 
180 apply (rule length_remdups_leq) 
176 apply (rule length_remdups_leq) 
181 done 
177 done 
182 
178 
183 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)" 
179 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> (set x = set y)" 
184 by (metis List.set_remdups perm_set_eq eq_set_perm_remdups) 
180 by (metis List.set_remdups perm_set_eq eq_set_perm_remdups) 
185 
181 
186 lemma permutation_Ex_bij: 
182 lemma permutation_Ex_bij: 
187 assumes "xs <~~> ys" 
183 assumes "xs <~~> ys" 
188 shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" 
184 shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" 
189 using assms proof induct 
185 using assms proof induct 
190 case Nil then show ?case unfolding bij_betw_def by simp 
186 case Nil 

187 then show ?case unfolding bij_betw_def by simp 
191 next 
188 next 
192 case (swap y x l) 
189 case (swap y x l) 
193 show ?case 
190 show ?case 
194 proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI) 
191 proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI) 
195 show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}" 
192 show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}" 
196 by (auto simp: bij_betw_def) 
193 by (auto simp: bij_betw_def) 
197 fix i assume "i < length(y#x#l)" 
194 fix i 

195 assume "i < length(y#x#l)" 
198 show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i" 
196 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) 
197 by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc) 
200 qed 
198 qed 
201 next 
199 next 
202 case (Cons xs ys z) 
200 case (Cons xs ys z) 
203 then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and 
201 then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and 
204 perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast 
202 perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast 
205 let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n)  0 \<Rightarrow> 0" 
203 let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n)  0 \<Rightarrow> 0" 
206 show ?case 
204 show ?case 
207 proof (intro exI[of _ ?f] allI conjI impI) 
205 proof (intro exI[of _ ?f] allI conjI impI) 
208 have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}" 
206 have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}" 
209 "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}" 
207 "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}" 
210 by (simp_all add: lessThan_Suc_eq_insert_0) 
208 by (simp_all add: lessThan_Suc_eq_insert_0) 
211 show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding * 
209 show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" 

210 unfolding * 
212 proof (rule bij_betw_combine) 
211 proof (rule bij_betw_combine) 
213 show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})" 
212 show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})" 
214 using bij unfolding bij_betw_def 
213 using bij unfolding bij_betw_def 
215 by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def) 
214 by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def) 
216 qed (auto simp: bij_betw_def) 
215 qed (auto simp: bij_betw_def) 
217 fix i assume "i < length (z#xs)" 
216 fix i 

217 assume "i < length (z#xs)" 
218 then show "(z # xs) ! i = (z # ys) ! (?f i)" 
218 then show "(z # xs) ! i = (z # ys) ! (?f i)" 
219 using perm by (cases i) auto 
219 using perm by (cases i) auto 
220 qed 
220 qed 
221 next 
221 next 
222 case (trans xs ys zs) 
222 case (trans xs ys zs) 
223 then obtain f g where 
223 then obtain f g where 
224 bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and 
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 
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 
226 show ?case 
227 proof (intro exI[of _ "g\<circ>f"] conjI allI impI) 
227 proof (intro exI[of _ "g \<circ> f"] conjI allI impI) 
228 show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}" 
228 show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}" 
229 using bij by (rule bij_betw_trans) 
229 using bij by (rule bij_betw_trans) 
230 fix i assume "i < length xs" 
230 fix i assume "i < length xs" 
231 with bij have "f i < length ys" unfolding bij_betw_def by force 
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" 
232 with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i" 
233 using trans(1,3)[THEN perm_length] perm by force 
233 using trans(1,3)[THEN perm_length] perm by auto 
234 qed 
234 qed 
235 qed 
235 qed 
236 
236 
237 end 
237 end 