63122
|
1 |
(*
|
|
2 |
Title: Set_Permutations.thy
|
|
3 |
Author: Manuel Eberl, TU München
|
|
4 |
|
|
5 |
The set of permutations of a finite set, i.e. the set of all
|
|
6 |
lists that contain every element of the set once.
|
|
7 |
*)
|
|
8 |
|
|
9 |
section \<open>Set Permutations\<close>
|
|
10 |
|
|
11 |
theory Set_Permutations
|
|
12 |
imports
|
|
13 |
Complex_Main
|
|
14 |
"~~/src/HOL/Library/Disjoint_Sets"
|
|
15 |
"~~/src/HOL/Library/Permutations"
|
|
16 |
begin
|
|
17 |
|
|
18 |
subsection \<open>Definition and general facts\<close>
|
|
19 |
|
|
20 |
definition permutations_of_set :: "'a set \<Rightarrow> 'a list set" where
|
|
21 |
"permutations_of_set A = {xs. set xs = A \<and> distinct xs}"
|
|
22 |
|
|
23 |
lemma permutations_of_setI [intro]:
|
|
24 |
assumes "set xs = A" "distinct xs"
|
|
25 |
shows "xs \<in> permutations_of_set A"
|
|
26 |
using assms unfolding permutations_of_set_def by simp
|
|
27 |
|
|
28 |
lemma permutations_of_setD:
|
|
29 |
assumes "xs \<in> permutations_of_set A"
|
|
30 |
shows "set xs = A" "distinct xs"
|
|
31 |
using assms unfolding permutations_of_set_def by simp_all
|
|
32 |
|
|
33 |
lemma permutations_of_set_lists: "permutations_of_set A \<subseteq> lists A"
|
|
34 |
unfolding permutations_of_set_def by auto
|
|
35 |
|
|
36 |
lemma permutations_of_set_empty [simp]: "permutations_of_set {} = {[]}"
|
|
37 |
by (auto simp: permutations_of_set_def)
|
|
38 |
|
|
39 |
lemma UN_set_permutations_of_set [simp]:
|
|
40 |
"finite A \<Longrightarrow> (\<Union>xs\<in>permutations_of_set A. set xs) = A"
|
|
41 |
using finite_distinct_list by (auto simp: permutations_of_set_def)
|
|
42 |
|
|
43 |
lemma permutations_of_set_nonempty:
|
|
44 |
assumes "A \<noteq> {}"
|
|
45 |
shows "permutations_of_set A =
|
|
46 |
(\<Union>x\<in>A. (\<lambda>xs. x # xs) ` permutations_of_set (A - {x}))" (is "?lhs = ?rhs")
|
|
47 |
proof (intro equalityI subsetI)
|
|
48 |
fix ys assume ys: "ys \<in> permutations_of_set A"
|
|
49 |
with assms have "ys \<noteq> []" by (auto simp: permutations_of_set_def)
|
|
50 |
then obtain x xs where xs: "ys = x # xs" by (cases ys) simp_all
|
|
51 |
from xs ys have "x \<in> A" "xs \<in> permutations_of_set (A - {x})"
|
|
52 |
by (auto simp: permutations_of_set_def)
|
|
53 |
with xs show "ys \<in> ?rhs" by auto
|
|
54 |
next
|
|
55 |
fix ys assume ys: "ys \<in> ?rhs"
|
|
56 |
then obtain x xs where xs: "ys = x # xs" "x \<in> A" "xs \<in> permutations_of_set (A - {x})"
|
|
57 |
by auto
|
|
58 |
with ys show "ys \<in> ?lhs" by (auto simp: permutations_of_set_def)
|
|
59 |
qed
|
|
60 |
|
|
61 |
lemma permutations_of_set_singleton [simp]: "permutations_of_set {x} = {[x]}"
|
|
62 |
by (subst permutations_of_set_nonempty) auto
|
|
63 |
|
|
64 |
lemma permutations_of_set_doubleton:
|
|
65 |
"x \<noteq> y \<Longrightarrow> permutations_of_set {x,y} = {[x,y], [y,x]}"
|
|
66 |
by (subst permutations_of_set_nonempty)
|
|
67 |
(simp_all add: insert_Diff_if insert_commute)
|
|
68 |
|
|
69 |
lemma rev_permutations_of_set [simp]:
|
|
70 |
"rev ` permutations_of_set A = permutations_of_set A"
|
|
71 |
proof
|
|
72 |
have "rev ` rev ` permutations_of_set A \<subseteq> rev ` permutations_of_set A"
|
|
73 |
unfolding permutations_of_set_def by auto
|
|
74 |
also have "rev ` rev ` permutations_of_set A = permutations_of_set A"
|
|
75 |
by (simp add: image_image)
|
|
76 |
finally show "permutations_of_set A \<subseteq> rev ` permutations_of_set A" .
|
|
77 |
next
|
|
78 |
show "rev ` permutations_of_set A \<subseteq> permutations_of_set A"
|
|
79 |
unfolding permutations_of_set_def by auto
|
|
80 |
qed
|
|
81 |
|
|
82 |
lemma length_finite_permutations_of_set:
|
|
83 |
"xs \<in> permutations_of_set A \<Longrightarrow> length xs = card A"
|
|
84 |
by (auto simp: permutations_of_set_def distinct_card)
|
|
85 |
|
|
86 |
lemma permutations_of_set_infinite:
|
|
87 |
"\<not>finite A \<Longrightarrow> permutations_of_set A = {}"
|
|
88 |
by (auto simp: permutations_of_set_def)
|
|
89 |
|
|
90 |
lemma finite_permutations_of_set [simp]: "finite (permutations_of_set A)"
|
|
91 |
proof (cases "finite A")
|
|
92 |
assume fin: "finite A"
|
|
93 |
have "permutations_of_set A \<subseteq> {xs. set xs \<subseteq> A \<and> length xs = card A}"
|
|
94 |
unfolding permutations_of_set_def by (auto simp: distinct_card)
|
|
95 |
moreover from fin have "finite \<dots>" using finite_lists_length_eq by blast
|
|
96 |
ultimately show ?thesis by (rule finite_subset)
|
|
97 |
qed (simp_all add: permutations_of_set_infinite)
|
|
98 |
|
|
99 |
lemma permutations_of_set_empty_iff [simp]:
|
|
100 |
"permutations_of_set A = {} \<longleftrightarrow> \<not>finite A"
|
|
101 |
unfolding permutations_of_set_def using finite_distinct_list[of A] by auto
|
|
102 |
|
|
103 |
lemma card_permutations_of_set [simp]:
|
|
104 |
"finite A \<Longrightarrow> card (permutations_of_set A) = fact (card A)"
|
|
105 |
proof (induction A rule: finite_remove_induct)
|
|
106 |
case (remove A)
|
|
107 |
hence "card (permutations_of_set A) =
|
|
108 |
card (\<Union>x\<in>A. op # x ` permutations_of_set (A - {x}))"
|
|
109 |
by (simp add: permutations_of_set_nonempty)
|
|
110 |
also from remove.hyps have "\<dots> = (\<Sum>i\<in>A. card (op # i ` permutations_of_set (A - {i})))"
|
|
111 |
by (intro card_UN_disjoint) auto
|
|
112 |
also have "\<dots> = (\<Sum>i\<in>A. card (permutations_of_set (A - {i})))"
|
|
113 |
by (intro setsum.cong) (simp_all add: card_image)
|
|
114 |
also from remove have "\<dots> = card A * fact (card A - 1)" by simp
|
|
115 |
also from remove.hyps have "\<dots> = fact (card A)"
|
|
116 |
by (cases "card A") simp_all
|
|
117 |
finally show ?case .
|
|
118 |
qed simp_all
|
|
119 |
|
|
120 |
lemma permutations_of_set_image_inj:
|
|
121 |
assumes inj: "inj_on f A"
|
|
122 |
shows "permutations_of_set (f ` A) = map f ` permutations_of_set A"
|
|
123 |
proof (cases "finite A")
|
|
124 |
assume "\<not>finite A"
|
|
125 |
with inj show ?thesis
|
|
126 |
by (auto simp add: permutations_of_set_infinite dest: finite_imageD)
|
|
127 |
next
|
|
128 |
assume finite: "finite A"
|
|
129 |
show ?thesis
|
|
130 |
proof (rule sym, rule card_seteq)
|
|
131 |
from inj show "map f ` permutations_of_set A \<subseteq> permutations_of_set (f ` A)"
|
|
132 |
by (auto simp: permutations_of_set_def distinct_map)
|
|
133 |
|
|
134 |
from inj have "card (map f ` permutations_of_set A) = card (permutations_of_set A)"
|
|
135 |
by (intro card_image inj_on_mapI) (auto simp: permutations_of_set_def)
|
|
136 |
also from finite inj have "\<dots> = card (permutations_of_set (f ` A))"
|
|
137 |
by (simp add: card_image)
|
|
138 |
finally show "card (permutations_of_set (f ` A)) \<le>
|
|
139 |
card (map f ` permutations_of_set A)" by simp
|
|
140 |
qed simp_all
|
|
141 |
qed
|
|
142 |
|
|
143 |
lemma permutations_of_set_image_permutes:
|
|
144 |
"\<sigma> permutes A \<Longrightarrow> map \<sigma> ` permutations_of_set A = permutations_of_set A"
|
|
145 |
by (subst permutations_of_set_image_inj [symmetric])
|
|
146 |
(simp_all add: permutes_inj_on permutes_image)
|
|
147 |
|
|
148 |
|
|
149 |
subsection \<open>Code generation\<close>
|
|
150 |
|
|
151 |
text \<open>
|
|
152 |
We define an auxiliary version with an accumulator to avoid
|
|
153 |
having to map over the results.
|
|
154 |
\<close>
|
|
155 |
function permutations_of_set_aux where
|
|
156 |
"permutations_of_set_aux acc A =
|
|
157 |
(if \<not>finite A then {} else if A = {} then {acc} else
|
|
158 |
(\<Union>x\<in>A. permutations_of_set_aux (x#acc) (A - {x})))"
|
|
159 |
by auto
|
|
160 |
termination by (relation "Wellfounded.measure (card \<circ> snd)") (simp_all add: card_gt_0_iff)
|
|
161 |
|
|
162 |
lemma permutations_of_set_aux_altdef:
|
|
163 |
"permutations_of_set_aux acc A = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A"
|
|
164 |
proof (cases "finite A")
|
|
165 |
assume "finite A"
|
|
166 |
thus ?thesis
|
|
167 |
proof (induction A arbitrary: acc rule: finite_psubset_induct)
|
|
168 |
case (psubset A acc)
|
|
169 |
show ?case
|
|
170 |
proof (cases "A = {}")
|
|
171 |
case False
|
|
172 |
note [simp del] = permutations_of_set_aux.simps
|
|
173 |
from psubset.hyps False
|
|
174 |
have "permutations_of_set_aux acc A =
|
|
175 |
(\<Union>y\<in>A. permutations_of_set_aux (y#acc) (A - {y}))"
|
|
176 |
by (subst permutations_of_set_aux.simps) simp_all
|
|
177 |
also have "\<dots> = (\<Union>y\<in>A. (\<lambda>xs. rev xs @ acc) ` (\<lambda>xs. y # xs) ` permutations_of_set (A - {y}))"
|
|
178 |
by (intro SUP_cong refl, subst psubset) (auto simp: image_image)
|
|
179 |
also from False have "\<dots> = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A"
|
|
180 |
by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN)
|
|
181 |
finally show ?thesis .
|
|
182 |
qed simp_all
|
|
183 |
qed
|
|
184 |
qed (simp_all add: permutations_of_set_infinite)
|
|
185 |
|
|
186 |
declare permutations_of_set_aux.simps [simp del]
|
|
187 |
|
|
188 |
lemma permutations_of_set_aux_correct:
|
|
189 |
"permutations_of_set_aux [] A = permutations_of_set A"
|
|
190 |
by (simp add: permutations_of_set_aux_altdef)
|
|
191 |
|
|
192 |
|
|
193 |
text \<open>
|
|
194 |
In another refinement step, we define a version on lists.
|
|
195 |
\<close>
|
|
196 |
declare length_remove1 [termination_simp]
|
|
197 |
|
|
198 |
fun permutations_of_set_aux_list where
|
|
199 |
"permutations_of_set_aux_list acc xs =
|
|
200 |
(if xs = [] then [acc] else
|
|
201 |
List.bind xs (\<lambda>x. permutations_of_set_aux_list (x#acc) (List.remove1 x xs)))"
|
|
202 |
|
|
203 |
definition permutations_of_set_list where
|
|
204 |
"permutations_of_set_list xs = permutations_of_set_aux_list [] xs"
|
|
205 |
|
|
206 |
declare permutations_of_set_aux_list.simps [simp del]
|
|
207 |
|
|
208 |
lemma permutations_of_set_aux_list_refine:
|
|
209 |
assumes "distinct xs"
|
|
210 |
shows "set (permutations_of_set_aux_list acc xs) = permutations_of_set_aux acc (set xs)"
|
|
211 |
using assms
|
|
212 |
by (induction acc xs rule: permutations_of_set_aux_list.induct)
|
|
213 |
(subst permutations_of_set_aux_list.simps,
|
|
214 |
subst permutations_of_set_aux.simps,
|
|
215 |
simp_all add: set_list_bind cong: SUP_cong)
|
|
216 |
|
|
217 |
|
|
218 |
text \<open>
|
|
219 |
The permutation lists contain no duplicates if the inputs contain no duplicates.
|
|
220 |
Therefore, these functions can easily be used when working with a representation of
|
|
221 |
sets by distinct lists.
|
|
222 |
The same approach should generalise to any kind of set implementation that supports
|
|
223 |
a monadic bind operation, and since the results are disjoint, merging should be cheap.
|
|
224 |
\<close>
|
|
225 |
lemma distinct_permutations_of_set_aux_list:
|
|
226 |
"distinct xs \<Longrightarrow> distinct (permutations_of_set_aux_list acc xs)"
|
|
227 |
by (induction acc xs rule: permutations_of_set_aux_list.induct)
|
|
228 |
(subst permutations_of_set_aux_list.simps,
|
|
229 |
auto intro!: distinct_list_bind simp: disjoint_family_on_def
|
|
230 |
permutations_of_set_aux_list_refine permutations_of_set_aux_altdef)
|
|
231 |
|
|
232 |
lemma distinct_permutations_of_set_list:
|
|
233 |
"distinct xs \<Longrightarrow> distinct (permutations_of_set_list xs)"
|
|
234 |
by (simp add: permutations_of_set_list_def distinct_permutations_of_set_aux_list)
|
|
235 |
|
|
236 |
lemma permutations_of_list:
|
|
237 |
"permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))"
|
|
238 |
by (simp add: permutations_of_set_aux_correct [symmetric]
|
|
239 |
permutations_of_set_aux_list_refine permutations_of_set_list_def)
|
|
240 |
|
|
241 |
lemma permutations_of_list_code [code]:
|
|
242 |
"permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))"
|
|
243 |
"permutations_of_set (List.coset xs) =
|
|
244 |
Code.abort (STR ''Permutation of set complement not supported'')
|
|
245 |
(\<lambda>_. permutations_of_set (List.coset xs))"
|
|
246 |
by (simp_all add: permutations_of_list)
|
|
247 |
|
|
248 |
value [code] "permutations_of_set (set ''abcd'')"
|
|
249 |
|
|
250 |
end |