author | wenzelm |
Thu, 24 Dec 2020 00:07:51 +0100 | |
changeset 72996 | cdcd2785db94 |
parent 72536 | 589645894305 |
permissions | -rw-r--r-- |
63375 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
2 |
||
3 |
section \<open>Permutations as abstract type\<close> |
|
4 |
||
5 |
theory Perm |
|
6 |
imports Main |
|
7 |
begin |
|
8 |
||
9 |
text \<open> |
|
10 |
This theory introduces basics about permutations, i.e. almost |
|
11 |
everywhere fix bijections. But it is by no means complete. |
|
12 |
Grieviously missing are cycles since these would require more |
|
13 |
elaboration, e.g. the concept of distinct lists equivalent |
|
14 |
under rotation, which maybe would also deserve its own theory. |
|
64911 | 15 |
But see theory \<open>src/HOL/ex/Perm_Fragments.thy\<close> for |
63375 | 16 |
fragments on that. |
17 |
\<close> |
|
18 |
||
19 |
subsection \<open>Abstract type of permutations\<close> |
|
20 |
||
21 |
typedef 'a perm = "{f :: 'a \<Rightarrow> 'a. bij f \<and> finite {a. f a \<noteq> a}}" |
|
22 |
morphisms "apply" Perm |
|
63433 | 23 |
proof |
24 |
show "id \<in> ?perm" by simp |
|
25 |
qed |
|
63375 | 26 |
|
27 |
setup_lifting type_definition_perm |
|
28 |
||
29 |
notation "apply" (infixl "\<langle>$\<rangle>" 999) |
|
30 |
||
31 |
lemma bij_apply [simp]: |
|
32 |
"bij (apply f)" |
|
33 |
using "apply" [of f] by simp |
|
34 |
||
35 |
lemma perm_eqI: |
|
36 |
assumes "\<And>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> a" |
|
37 |
shows "f = g" |
|
38 |
using assms by transfer (simp add: fun_eq_iff) |
|
39 |
||
40 |
lemma perm_eq_iff: |
|
41 |
"f = g \<longleftrightarrow> (\<forall>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> a)" |
|
42 |
by (auto intro: perm_eqI) |
|
43 |
||
44 |
lemma apply_inj: |
|
45 |
"f \<langle>$\<rangle> a = f \<langle>$\<rangle> b \<longleftrightarrow> a = b" |
|
46 |
by (rule inj_eq) (rule bij_is_inj, simp) |
|
47 |
||
48 |
lift_definition affected :: "'a perm \<Rightarrow> 'a set" |
|
49 |
is "\<lambda>f. {a. f a \<noteq> a}" . |
|
50 |
||
51 |
lemma in_affected: |
|
52 |
"a \<in> affected f \<longleftrightarrow> f \<langle>$\<rangle> a \<noteq> a" |
|
53 |
by transfer simp |
|
54 |
||
55 |
lemma finite_affected [simp]: |
|
56 |
"finite (affected f)" |
|
57 |
by transfer simp |
|
58 |
||
59 |
lemma apply_affected [simp]: |
|
60 |
"f \<langle>$\<rangle> a \<in> affected f \<longleftrightarrow> a \<in> affected f" |
|
61 |
proof transfer |
|
62 |
fix f :: "'a \<Rightarrow> 'a" and a :: 'a |
|
63 |
assume "bij f \<and> finite {b. f b \<noteq> b}" |
|
64 |
then have "bij f" by simp |
|
65 |
interpret bijection f by standard (rule \<open>bij f\<close>) |
|
66 |
have "f a \<in> {a. f a = a} \<longleftrightarrow> a \<in> {a. f a = a}" (is "?P \<longleftrightarrow> ?Q") |
|
67 |
by auto |
|
68 |
then show "f a \<in> {a. f a \<noteq> a} \<longleftrightarrow> a \<in> {a. f a \<noteq> a}" |
|
69 |
by simp |
|
70 |
qed |
|
71 |
||
72 |
lemma card_affected_not_one: |
|
73 |
"card (affected f) \<noteq> 1" |
|
74 |
proof |
|
75 |
interpret bijection "apply f" |
|
76 |
by standard (rule bij_apply) |
|
77 |
assume "card (affected f) = 1" |
|
78 |
then obtain a where *: "affected f = {a}" |
|
79 |
by (rule card_1_singletonE) |
|
63540 | 80 |
then have **: "f \<langle>$\<rangle> a \<noteq> a" |
68406 | 81 |
by (simp flip: in_affected) |
63540 | 82 |
with * have "f \<langle>$\<rangle> a \<notin> affected f" |
63375 | 83 |
by simp |
84 |
then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a" |
|
85 |
by (simp add: in_affected) |
|
86 |
then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)" |
|
87 |
by simp |
|
63540 | 88 |
with ** show False by simp |
63375 | 89 |
qed |
90 |
||
91 |
||
92 |
subsection \<open>Identity, composition and inversion\<close> |
|
93 |
||
94 |
instantiation Perm.perm :: (type) "{monoid_mult, inverse}" |
|
95 |
begin |
|
96 |
||
97 |
lift_definition one_perm :: "'a perm" |
|
98 |
is id |
|
99 |
by simp |
|
100 |
||
101 |
lemma apply_one [simp]: |
|
102 |
"apply 1 = id" |
|
103 |
by (fact one_perm.rep_eq) |
|
104 |
||
105 |
lemma affected_one [simp]: |
|
106 |
"affected 1 = {}" |
|
107 |
by transfer simp |
|
108 |
||
109 |
lemma affected_empty_iff [simp]: |
|
110 |
"affected f = {} \<longleftrightarrow> f = 1" |
|
111 |
by transfer auto |
|
112 |
||
113 |
lift_definition times_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" |
|
114 |
is comp |
|
115 |
proof |
|
116 |
fix f g :: "'a \<Rightarrow> 'a" |
|
117 |
assume "bij f \<and> finite {a. f a \<noteq> a}" |
|
118 |
"bij g \<and>finite {a. g a \<noteq> a}" |
|
119 |
then have "finite ({a. f a \<noteq> a} \<union> {a. g a \<noteq> a})" |
|
120 |
by simp |
|
121 |
moreover have "{a. (f \<circ> g) a \<noteq> a} \<subseteq> {a. f a \<noteq> a} \<union> {a. g a \<noteq> a}" |
|
122 |
by auto |
|
123 |
ultimately show "finite {a. (f \<circ> g) a \<noteq> a}" |
|
124 |
by (auto intro: finite_subset) |
|
125 |
qed (auto intro: bij_comp) |
|
126 |
||
127 |
lemma apply_times: |
|
128 |
"apply (f * g) = apply f \<circ> apply g" |
|
129 |
by (fact times_perm.rep_eq) |
|
130 |
||
131 |
lemma apply_sequence: |
|
132 |
"f \<langle>$\<rangle> (g \<langle>$\<rangle> a) = apply (f * g) a" |
|
133 |
by (simp add: apply_times) |
|
134 |
||
135 |
lemma affected_times [simp]: |
|
136 |
"affected (f * g) \<subseteq> affected f \<union> affected g" |
|
137 |
by transfer auto |
|
138 |
||
139 |
lift_definition inverse_perm :: "'a perm \<Rightarrow> 'a perm" |
|
140 |
is inv |
|
141 |
proof transfer |
|
142 |
fix f :: "'a \<Rightarrow> 'a" and a |
|
143 |
assume "bij f \<and> finite {b. f b \<noteq> b}" |
|
144 |
then have "bij f" and fin: "finite {b. f b \<noteq> b}" |
|
145 |
by auto |
|
146 |
interpret bijection f by standard (rule \<open>bij f\<close>) |
|
147 |
from fin show "bij (inv f) \<and> finite {a. inv f a \<noteq> a}" |
|
148 |
by (simp add: bij_inv) |
|
149 |
qed |
|
150 |
||
151 |
instance |
|
152 |
by standard (transfer; simp add: comp_assoc)+ |
|
153 |
||
154 |
end |
|
155 |
||
156 |
lemma apply_inverse: |
|
157 |
"apply (inverse f) = inv (apply f)" |
|
158 |
by (fact inverse_perm.rep_eq) |
|
159 |
||
160 |
lemma affected_inverse [simp]: |
|
161 |
"affected (inverse f) = affected f" |
|
162 |
proof transfer |
|
163 |
fix f :: "'a \<Rightarrow> 'a" and a |
|
164 |
assume "bij f \<and> finite {b. f b \<noteq> b}" |
|
165 |
then have "bij f" by simp |
|
166 |
interpret bijection f by standard (rule \<open>bij f\<close>) |
|
167 |
show "{a. inv f a \<noteq> a} = {a. f a \<noteq> a}" |
|
168 |
by simp |
|
169 |
qed |
|
170 |
||
171 |
global_interpretation perm: group times "1::'a perm" inverse |
|
172 |
proof |
|
173 |
fix f :: "'a perm" |
|
174 |
show "1 * f = f" |
|
175 |
by transfer simp |
|
176 |
show "inverse f * f = 1" |
|
177 |
proof transfer |
|
178 |
fix f :: "'a \<Rightarrow> 'a" and a |
|
179 |
assume "bij f \<and> finite {b. f b \<noteq> b}" |
|
180 |
then have "bij f" by simp |
|
181 |
interpret bijection f by standard (rule \<open>bij f\<close>) |
|
182 |
show "inv f \<circ> f = id" |
|
183 |
by simp |
|
184 |
qed |
|
185 |
qed |
|
186 |
||
187 |
declare perm.inverse_distrib_swap [simp] |
|
188 |
||
189 |
lemma perm_mult_commute: |
|
190 |
assumes "affected f \<inter> affected g = {}" |
|
191 |
shows "g * f = f * g" |
|
192 |
proof (rule perm_eqI) |
|
193 |
fix a |
|
194 |
from assms have *: "a \<in> affected f \<Longrightarrow> a \<notin> affected g" |
|
195 |
"a \<in> affected g \<Longrightarrow> a \<notin> affected f" for a |
|
196 |
by auto |
|
197 |
consider "a \<in> affected f \<and> a \<notin> affected g |
|
198 |
\<and> f \<langle>$\<rangle> a \<in> affected f" |
|
199 |
| "a \<notin> affected f \<and> a \<in> affected g |
|
200 |
\<and> f \<langle>$\<rangle> a \<notin> affected f" |
|
201 |
| "a \<notin> affected f \<and> a \<notin> affected g" |
|
202 |
using assms by auto |
|
203 |
then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a" |
|
204 |
proof cases |
|
63540 | 205 |
case 1 |
206 |
with * have "f \<langle>$\<rangle> a \<notin> affected g" |
|
63375 | 207 |
by auto |
63540 | 208 |
with 1 show ?thesis by (simp add: in_affected apply_times) |
63375 | 209 |
next |
63540 | 210 |
case 2 |
211 |
with * have "g \<langle>$\<rangle> a \<notin> affected f" |
|
63375 | 212 |
by auto |
63540 | 213 |
with 2 show ?thesis by (simp add: in_affected apply_times) |
63375 | 214 |
next |
63540 | 215 |
case 3 |
216 |
then show ?thesis by (simp add: in_affected apply_times) |
|
63375 | 217 |
qed |
218 |
qed |
|
219 |
||
220 |
lemma apply_power: |
|
221 |
"apply (f ^ n) = apply f ^^ n" |
|
222 |
by (induct n) (simp_all add: apply_times) |
|
223 |
||
224 |
lemma perm_power_inverse: |
|
225 |
"inverse f ^ n = inverse ((f :: 'a perm) ^ n)" |
|
226 |
proof (induct n) |
|
227 |
case 0 then show ?case by simp |
|
228 |
next |
|
229 |
case (Suc n) |
|
230 |
then show ?case |
|
231 |
unfolding power_Suc2 [of f] by simp |
|
232 |
qed |
|
233 |
||
234 |
||
235 |
subsection \<open>Orbit and order of elements\<close> |
|
236 |
||
237 |
definition orbit :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a set" |
|
238 |
where |
|
239 |
"orbit f a = range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)" |
|
240 |
||
241 |
lemma in_orbitI: |
|
242 |
assumes "(f ^ n) \<langle>$\<rangle> a = b" |
|
243 |
shows "b \<in> orbit f a" |
|
244 |
using assms by (auto simp add: orbit_def) |
|
245 |
||
246 |
lemma apply_power_self_in_orbit [simp]: |
|
247 |
"(f ^ n) \<langle>$\<rangle> a \<in> orbit f a" |
|
248 |
by (rule in_orbitI) rule |
|
249 |
||
250 |
lemma in_orbit_self [simp]: |
|
251 |
"a \<in> orbit f a" |
|
252 |
using apply_power_self_in_orbit [of _ 0] by simp |
|
253 |
||
254 |
lemma apply_self_in_orbit [simp]: |
|
255 |
"f \<langle>$\<rangle> a \<in> orbit f a" |
|
256 |
using apply_power_self_in_orbit [of _ 1] by simp |
|
257 |
||
258 |
lemma orbit_not_empty [simp]: |
|
259 |
"orbit f a \<noteq> {}" |
|
260 |
using in_orbit_self [of a f] by blast |
|
261 |
||
262 |
lemma not_in_affected_iff_orbit_eq_singleton: |
|
263 |
"a \<notin> affected f \<longleftrightarrow> orbit f a = {a}" (is "?P \<longleftrightarrow> ?Q") |
|
264 |
proof |
|
265 |
assume ?P |
|
266 |
then have "f \<langle>$\<rangle> a = a" |
|
267 |
by (simp add: in_affected) |
|
268 |
then have "(f ^ n) \<langle>$\<rangle> a = a" for n |
|
269 |
by (induct n) (simp_all add: apply_times) |
|
270 |
then show ?Q |
|
271 |
by (auto simp add: orbit_def) |
|
272 |
next |
|
273 |
assume ?Q |
|
274 |
then show ?P |
|
275 |
by (auto simp add: orbit_def in_affected dest: range_eq_singletonD [of _ _ 1]) |
|
276 |
qed |
|
277 |
||
278 |
definition order :: "'a perm \<Rightarrow> 'a \<Rightarrow> nat" |
|
279 |
where |
|
63993 | 280 |
"order f = card \<circ> orbit f" |
63375 | 281 |
|
282 |
lemma orbit_subset_eq_affected: |
|
283 |
assumes "a \<in> affected f" |
|
284 |
shows "orbit f a \<subseteq> affected f" |
|
285 |
proof (rule ccontr) |
|
286 |
assume "\<not> orbit f a \<subseteq> affected f" |
|
287 |
then obtain b where "b \<in> orbit f a" and "b \<notin> affected f" |
|
288 |
by auto |
|
289 |
then have "b \<in> range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)" |
|
290 |
by (simp add: orbit_def) |
|
291 |
then obtain n where "b = (f ^ n) \<langle>$\<rangle> a" |
|
292 |
by blast |
|
293 |
with \<open>b \<notin> affected f\<close> |
|
294 |
have "(f ^ n) \<langle>$\<rangle> a \<notin> affected f" |
|
295 |
by simp |
|
296 |
then have "f \<langle>$\<rangle> a \<notin> affected f" |
|
297 |
by (induct n) (simp_all add: apply_times) |
|
298 |
with assms show False |
|
299 |
by simp |
|
300 |
qed |
|
301 |
||
302 |
lemma finite_orbit [simp]: |
|
303 |
"finite (orbit f a)" |
|
304 |
proof (cases "a \<in> affected f") |
|
305 |
case False then show ?thesis |
|
306 |
by (simp add: not_in_affected_iff_orbit_eq_singleton) |
|
307 |
next |
|
308 |
case True then have "orbit f a \<subseteq> affected f" |
|
309 |
by (rule orbit_subset_eq_affected) |
|
310 |
then show ?thesis using finite_affected |
|
311 |
by (rule finite_subset) |
|
312 |
qed |
|
313 |
||
314 |
lemma orbit_1 [simp]: |
|
315 |
"orbit 1 a = {a}" |
|
316 |
by (auto simp add: orbit_def) |
|
317 |
||
318 |
lemma order_1 [simp]: |
|
319 |
"order 1 a = 1" |
|
320 |
unfolding order_def by simp |
|
321 |
||
322 |
lemma card_orbit_eq [simp]: |
|
323 |
"card (orbit f a) = order f a" |
|
324 |
by (simp add: order_def) |
|
325 |
||
326 |
lemma order_greater_zero [simp]: |
|
327 |
"order f a > 0" |
|
328 |
by (simp only: card_gt_0_iff order_def comp_def) simp |
|
329 |
||
330 |
lemma order_eq_one_iff: |
|
331 |
"order f a = Suc 0 \<longleftrightarrow> a \<notin> affected f" (is "?P \<longleftrightarrow> ?Q") |
|
332 |
proof |
|
333 |
assume ?P then have "card (orbit f a) = 1" |
|
334 |
by simp |
|
335 |
then obtain b where "orbit f a = {b}" |
|
336 |
by (rule card_1_singletonE) |
|
337 |
with in_orbit_self [of a f] |
|
338 |
have "b = a" by simp |
|
339 |
with \<open>orbit f a = {b}\<close> show ?Q |
|
340 |
by (simp add: not_in_affected_iff_orbit_eq_singleton) |
|
341 |
next |
|
342 |
assume ?Q |
|
343 |
then have "orbit f a = {a}" |
|
344 |
by (simp add: not_in_affected_iff_orbit_eq_singleton) |
|
345 |
then have "card (orbit f a) = 1" |
|
346 |
by simp |
|
347 |
then show ?P |
|
348 |
by simp |
|
349 |
qed |
|
350 |
||
351 |
lemma order_greater_eq_two_iff: |
|
352 |
"order f a \<ge> 2 \<longleftrightarrow> a \<in> affected f" |
|
353 |
using order_eq_one_iff [of f a] |
|
354 |
apply (auto simp add: neq_iff) |
|
355 |
using order_greater_zero [of f a] |
|
356 |
apply simp |
|
357 |
done |
|
358 |
||
359 |
lemma order_less_eq_affected: |
|
360 |
assumes "f \<noteq> 1" |
|
361 |
shows "order f a \<le> card (affected f)" |
|
362 |
proof (cases "a \<in> affected f") |
|
363 |
from assms have "affected f \<noteq> {}" |
|
364 |
by simp |
|
365 |
then obtain B b where "affected f = insert b B" |
|
366 |
by blast |
|
367 |
with finite_affected [of f] have "card (affected f) \<ge> 1" |
|
72302
d7d90ed4c74e
fixed some remarkably ugly proofs
paulson <lp15@cam.ac.uk>
parents:
70335
diff
changeset
|
368 |
by (simp add: card.insert_remove) |
63375 | 369 |
case False then have "order f a = 1" |
370 |
by (simp add: order_eq_one_iff) |
|
371 |
with \<open>card (affected f) \<ge> 1\<close> show ?thesis |
|
372 |
by simp |
|
373 |
next |
|
374 |
case True |
|
375 |
have "card (orbit f a) \<le> card (affected f)" |
|
376 |
by (rule card_mono) (simp_all add: True orbit_subset_eq_affected card_mono) |
|
377 |
then show ?thesis |
|
378 |
by simp |
|
379 |
qed |
|
380 |
||
381 |
lemma affected_order_greater_eq_two: |
|
382 |
assumes "a \<in> affected f" |
|
383 |
shows "order f a \<ge> 2" |
|
384 |
proof (rule ccontr) |
|
385 |
assume "\<not> 2 \<le> order f a" |
|
386 |
then have "order f a < 2" |
|
387 |
by (simp add: not_le) |
|
388 |
with order_greater_zero [of f a] have "order f a = 1" |
|
389 |
by arith |
|
390 |
with assms show False |
|
391 |
by (simp add: order_eq_one_iff) |
|
392 |
qed |
|
393 |
||
394 |
lemma order_witness_unfold: |
|
395 |
assumes "n > 0" and "(f ^ n) \<langle>$\<rangle> a = a" |
|
396 |
shows "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n})" |
|
397 |
proof - |
|
398 |
have "orbit f a = (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n}" (is "_ = ?B") |
|
399 |
proof (rule set_eqI, rule) |
|
400 |
fix b |
|
401 |
assume "b \<in> orbit f a" |
|
402 |
then obtain m where "(f ^ m) \<langle>$\<rangle> a = b" |
|
403 |
by (auto simp add: orbit_def) |
|
404 |
then have "b = (f ^ (m mod n + n * (m div n))) \<langle>$\<rangle> a" |
|
405 |
by simp |
|
406 |
also have "\<dots> = (f ^ (m mod n)) \<langle>$\<rangle> ((f ^ (n * (m div n))) \<langle>$\<rangle> a)" |
|
407 |
by (simp only: power_add apply_times) simp |
|
408 |
also have "(f ^ (n * q)) \<langle>$\<rangle> a = a" for q |
|
409 |
by (induct q) |
|
410 |
(simp_all add: power_add apply_times assms) |
|
411 |
finally have "b = (f ^ (m mod n)) \<langle>$\<rangle> a" . |
|
412 |
moreover from \<open>n > 0\<close> |
|
413 |
have "m mod n < n" |
|
414 |
by simp |
|
415 |
ultimately show "b \<in> ?B" |
|
416 |
by auto |
|
417 |
next |
|
418 |
fix b |
|
419 |
assume "b \<in> ?B" |
|
420 |
then obtain m where "(f ^ m) \<langle>$\<rangle> a = b" |
|
421 |
by blast |
|
422 |
then show "b \<in> orbit f a" |
|
423 |
by (rule in_orbitI) |
|
424 |
qed |
|
425 |
then have "card (orbit f a) = card ?B" |
|
426 |
by (simp only:) |
|
427 |
then show ?thesis |
|
428 |
by simp |
|
429 |
qed |
|
430 |
||
431 |
lemma inj_on_apply_range: |
|
432 |
"inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<order f a}" |
|
433 |
proof - |
|
434 |
have "inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}" |
|
435 |
if "n \<le> order f a" for n |
|
436 |
using that proof (induct n) |
|
437 |
case 0 then show ?case by simp |
|
438 |
next |
|
439 |
case (Suc n) |
|
440 |
then have prem: "n < order f a" |
|
441 |
by simp |
|
442 |
with Suc.hyps have hyp: "inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}" |
|
443 |
by simp |
|
444 |
have "(f ^ n) \<langle>$\<rangle> a \<notin> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}" |
|
445 |
proof |
|
446 |
assume "(f ^ n) \<langle>$\<rangle> a \<in> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}" |
|
447 |
then obtain m where *: "(f ^ m) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a" and "m < n" |
|
448 |
by auto |
|
449 |
interpret bijection "apply (f ^ m)" |
|
450 |
by standard simp |
|
451 |
from \<open>m < n\<close> have "n = m + (n - m)" |
|
452 |
and nm: "0 < n - m" "n - m \<le> n" |
|
453 |
by arith+ |
|
454 |
with * have "(f ^ m) \<langle>$\<rangle> a = (f ^ (m + (n - m))) \<langle>$\<rangle> a" |
|
455 |
by simp |
|
456 |
then have "(f ^ m) \<langle>$\<rangle> a = (f ^ m) \<langle>$\<rangle> ((f ^ (n - m)) \<langle>$\<rangle> a)" |
|
457 |
by (simp add: power_add apply_times) |
|
458 |
then have "(f ^ (n - m)) \<langle>$\<rangle> a = a" |
|
459 |
by simp |
|
460 |
with \<open>n - m > 0\<close> |
|
461 |
have "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m})" |
|
462 |
by (rule order_witness_unfold) |
|
463 |
also have "card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m}) \<le> card {0..<n - m}" |
|
464 |
by (rule card_image_le) simp |
|
465 |
finally have "order f a \<le> n - m" |
|
466 |
by simp |
|
467 |
with prem show False by simp |
|
468 |
qed |
|
469 |
with hyp show ?case |
|
470 |
by (simp add: lessThan_Suc) |
|
471 |
qed |
|
472 |
then show ?thesis by simp |
|
473 |
qed |
|
474 |
||
475 |
lemma orbit_unfold_image: |
|
476 |
"orbit f a = (\<lambda>n. (f ^ n) \<langle>$\<rangle> a) ` {..<order f a}" (is "_ = ?A") |
|
477 |
proof (rule sym, rule card_subset_eq) |
|
478 |
show "finite (orbit f a)" |
|
479 |
by simp |
|
480 |
show "?A \<subseteq> orbit f a" |
|
481 |
by (auto simp add: orbit_def) |
|
482 |
from inj_on_apply_range [of f a] |
|
483 |
have "card ?A = order f a" |
|
484 |
by (auto simp add: card_image) |
|
485 |
then show "card ?A = card (orbit f a)" |
|
486 |
by simp |
|
487 |
qed |
|
488 |
||
489 |
lemma in_orbitE: |
|
490 |
assumes "b \<in> orbit f a" |
|
491 |
obtains n where "b = (f ^ n) \<langle>$\<rangle> a" and "n < order f a" |
|
492 |
using assms unfolding orbit_unfold_image by blast |
|
493 |
||
494 |
lemma apply_power_order [simp]: |
|
495 |
"(f ^ order f a) \<langle>$\<rangle> a = a" |
|
496 |
proof - |
|
497 |
have "(f ^ order f a) \<langle>$\<rangle> a \<in> orbit f a" |
|
498 |
by simp |
|
499 |
then obtain n where |
|
500 |
*: "(f ^ order f a) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a" |
|
501 |
and "n < order f a" |
|
502 |
by (rule in_orbitE) |
|
503 |
show ?thesis |
|
504 |
proof (cases n) |
|
505 |
case 0 with * show ?thesis by simp |
|
506 |
next |
|
507 |
case (Suc m) |
|
508 |
from order_greater_zero [of f a] |
|
509 |
have "Suc (order f a - 1) = order f a" |
|
510 |
by arith |
|
511 |
from Suc \<open>n < order f a\<close> |
|
512 |
have "m < order f a" |
|
513 |
by simp |
|
514 |
with Suc * |
|
515 |
have "(inverse f) \<langle>$\<rangle> ((f ^ Suc (order f a - 1)) \<langle>$\<rangle> a) = |
|
516 |
(inverse f) \<langle>$\<rangle> ((f ^ Suc m) \<langle>$\<rangle> a)" |
|
517 |
by simp |
|
518 |
then have "(f ^ (order f a - 1)) \<langle>$\<rangle> a = |
|
519 |
(f ^ m) \<langle>$\<rangle> a" |
|
520 |
by (simp only: power_Suc apply_times) |
|
521 |
(simp add: apply_sequence mult.assoc [symmetric]) |
|
522 |
with inj_on_apply_range |
|
523 |
have "order f a - 1 = m" |
|
524 |
by (rule inj_onD) |
|
525 |
(simp_all add: \<open>m < order f a\<close>) |
|
526 |
with Suc have "n = order f a" |
|
527 |
by auto |
|
528 |
with \<open>n < order f a\<close> |
|
529 |
show ?thesis by simp |
|
530 |
qed |
|
531 |
qed |
|
532 |
||
533 |
lemma apply_power_left_mult_order [simp]: |
|
534 |
"(f ^ (n * order f a)) \<langle>$\<rangle> a = a" |
|
535 |
by (induct n) (simp_all add: power_add apply_times) |
|
536 |
||
537 |
lemma apply_power_right_mult_order [simp]: |
|
538 |
"(f ^ (order f a * n)) \<langle>$\<rangle> a = a" |
|
539 |
by (simp add: ac_simps) |
|
540 |
||
541 |
lemma apply_power_mod_order_eq [simp]: |
|
542 |
"(f ^ (n mod order f a)) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a" |
|
543 |
proof - |
|
544 |
have "(f ^ n) \<langle>$\<rangle> a = (f ^ (n mod order f a + order f a * (n div order f a))) \<langle>$\<rangle> a" |
|
545 |
by simp |
|
546 |
also have "\<dots> = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \<langle>$\<rangle> a" |
|
68406 | 547 |
by (simp flip: power_add) |
63375 | 548 |
finally show ?thesis |
549 |
by (simp add: apply_times) |
|
550 |
qed |
|
551 |
||
552 |
lemma apply_power_eq_iff: |
|
553 |
"(f ^ m) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a \<longleftrightarrow> m mod order f a = n mod order f a" (is "?P \<longleftrightarrow> ?Q") |
|
554 |
proof |
|
555 |
assume ?Q |
|
556 |
then have "(f ^ (m mod order f a)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> a" |
|
557 |
by simp |
|
558 |
then show ?P |
|
559 |
by simp |
|
560 |
next |
|
561 |
assume ?P |
|
562 |
then have "(f ^ (m mod order f a)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> a" |
|
563 |
by simp |
|
564 |
with inj_on_apply_range |
|
565 |
show ?Q |
|
566 |
by (rule inj_onD) simp_all |
|
567 |
qed |
|
568 |
||
569 |
lemma apply_inverse_eq_apply_power_order_minus_one: |
|
570 |
"(inverse f) \<langle>$\<rangle> a = (f ^ (order f a - 1)) \<langle>$\<rangle> a" |
|
571 |
proof (cases "order f a") |
|
572 |
case 0 with order_greater_zero [of f a] show ?thesis |
|
573 |
by simp |
|
574 |
next |
|
575 |
case (Suc n) |
|
576 |
moreover have "(f ^ order f a) \<langle>$\<rangle> a = a" |
|
577 |
by simp |
|
578 |
then have *: "(inverse f) \<langle>$\<rangle> ((f ^ order f a) \<langle>$\<rangle> a) = (inverse f) \<langle>$\<rangle> a" |
|
579 |
by simp |
|
580 |
ultimately show ?thesis |
|
581 |
by (simp add: apply_sequence mult.assoc [symmetric]) |
|
582 |
qed |
|
583 |
||
584 |
lemma apply_inverse_self_in_orbit [simp]: |
|
585 |
"(inverse f) \<langle>$\<rangle> a \<in> orbit f a" |
|
586 |
using apply_inverse_eq_apply_power_order_minus_one [symmetric] |
|
587 |
by (rule in_orbitI) |
|
588 |
||
589 |
lemma apply_inverse_power_eq: |
|
590 |
"(inverse (f ^ n)) \<langle>$\<rangle> a = (f ^ (order f a - n mod order f a)) \<langle>$\<rangle> a" |
|
591 |
proof (induct n) |
|
592 |
case 0 then show ?case by simp |
|
593 |
next |
|
594 |
case (Suc n) |
|
595 |
define m where "m = order f a - n mod order f a - 1" |
|
596 |
moreover have "order f a - n mod order f a > 0" |
|
597 |
by simp |
|
63539 | 598 |
ultimately have *: "order f a - n mod order f a = Suc m" |
63375 | 599 |
by arith |
63539 | 600 |
moreover from * have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)" |
63375 | 601 |
by (auto simp add: mod_Suc) |
602 |
ultimately show ?case |
|
603 |
using Suc |
|
604 |
by (simp_all add: apply_times power_Suc2 [of _ n] power_Suc [of _ m] del: power_Suc) |
|
605 |
(simp add: apply_sequence mult.assoc [symmetric]) |
|
606 |
qed |
|
607 |
||
608 |
lemma apply_power_eq_self_iff: |
|
609 |
"(f ^ n) \<langle>$\<rangle> a = a \<longleftrightarrow> order f a dvd n" |
|
610 |
using apply_power_eq_iff [of f n a 0] |
|
611 |
by (simp add: mod_eq_0_iff_dvd) |
|
612 |
||
613 |
lemma orbit_equiv: |
|
614 |
assumes "b \<in> orbit f a" |
|
615 |
shows "orbit f b = orbit f a" (is "?B = ?A") |
|
616 |
proof |
|
617 |
from assms obtain n where "n < order f a" and b: "b = (f ^ n) \<langle>$\<rangle> a" |
|
618 |
by (rule in_orbitE) |
|
619 |
then show "?B \<subseteq> ?A" |
|
620 |
by (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE) |
|
621 |
from b have "(inverse (f ^ n)) \<langle>$\<rangle> b = (inverse (f ^ n)) \<langle>$\<rangle> ((f ^ n) \<langle>$\<rangle> a)" |
|
622 |
by simp |
|
623 |
then have a: "a = (inverse (f ^ n)) \<langle>$\<rangle> b" |
|
624 |
by (simp add: apply_sequence) |
|
625 |
then show "?A \<subseteq> ?B" |
|
626 |
apply (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE) |
|
627 |
unfolding apply_times comp_def apply_inverse_power_eq |
|
628 |
unfolding apply_sequence power_add [symmetric] |
|
629 |
apply (rule in_orbitI) apply rule |
|
630 |
done |
|
631 |
qed |
|
632 |
||
633 |
lemma orbit_apply [simp]: |
|
634 |
"orbit f (f \<langle>$\<rangle> a) = orbit f a" |
|
635 |
by (rule orbit_equiv) simp |
|
636 |
||
637 |
lemma order_apply [simp]: |
|
638 |
"order f (f \<langle>$\<rangle> a) = order f a" |
|
639 |
by (simp only: order_def comp_def orbit_apply) |
|
640 |
||
641 |
lemma orbit_apply_inverse [simp]: |
|
642 |
"orbit f (inverse f \<langle>$\<rangle> a) = orbit f a" |
|
643 |
by (rule orbit_equiv) simp |
|
644 |
||
645 |
lemma order_apply_inverse [simp]: |
|
646 |
"order f (inverse f \<langle>$\<rangle> a) = order f a" |
|
647 |
by (simp only: order_def comp_def orbit_apply_inverse) |
|
648 |
||
649 |
lemma orbit_apply_power [simp]: |
|
650 |
"orbit f ((f ^ n) \<langle>$\<rangle> a) = orbit f a" |
|
651 |
by (rule orbit_equiv) simp |
|
652 |
||
653 |
lemma order_apply_power [simp]: |
|
654 |
"order f ((f ^ n) \<langle>$\<rangle> a) = order f a" |
|
655 |
by (simp only: order_def comp_def orbit_apply_power) |
|
656 |
||
657 |
lemma orbit_inverse [simp]: |
|
658 |
"orbit (inverse f) = orbit f" |
|
659 |
proof (rule ext, rule set_eqI, rule) |
|
660 |
fix b a |
|
661 |
assume "b \<in> orbit f a" |
|
662 |
then obtain n where b: "b = (f ^ n) \<langle>$\<rangle> a" "n < order f a" |
|
663 |
by (rule in_orbitE) |
|
664 |
then have "b = apply (inverse (inverse f) ^ n) a" |
|
665 |
by simp |
|
666 |
then have "b = apply (inverse (inverse f ^ n)) a" |
|
667 |
by (simp add: perm_power_inverse) |
|
668 |
then have "b = apply (inverse f ^ (n * (order (inverse f ^ n) a - 1))) a" |
|
669 |
by (simp add: apply_inverse_eq_apply_power_order_minus_one power_mult) |
|
670 |
then show "b \<in> orbit (inverse f) a" |
|
671 |
by simp |
|
672 |
next |
|
673 |
fix b a |
|
674 |
assume "b \<in> orbit (inverse f) a" |
|
675 |
then show "b \<in> orbit f a" |
|
676 |
by (rule in_orbitE) |
|
677 |
(simp add: apply_inverse_eq_apply_power_order_minus_one |
|
678 |
perm_power_inverse power_mult [symmetric]) |
|
679 |
qed |
|
680 |
||
681 |
lemma order_inverse [simp]: |
|
682 |
"order (inverse f) = order f" |
|
683 |
by (simp add: order_def) |
|
684 |
||
685 |
lemma orbit_disjoint: |
|
686 |
assumes "orbit f a \<noteq> orbit f b" |
|
687 |
shows "orbit f a \<inter> orbit f b = {}" |
|
688 |
proof (rule ccontr) |
|
689 |
assume "orbit f a \<inter> orbit f b \<noteq> {}" |
|
690 |
then obtain c where "c \<in> orbit f a \<inter> orbit f b" |
|
691 |
by blast |
|
692 |
then have "c \<in> orbit f a" and "c \<in> orbit f b" |
|
693 |
by auto |
|
694 |
then obtain m n where "c = (f ^ m) \<langle>$\<rangle> a" |
|
695 |
and "c = apply (f ^ n) b" by (blast elim!: in_orbitE) |
|
696 |
then have "(f ^ m) \<langle>$\<rangle> a = apply (f ^ n) b" |
|
697 |
by simp |
|
698 |
then have "apply (inverse f ^ m) ((f ^ m) \<langle>$\<rangle> a) = |
|
699 |
apply (inverse f ^ m) (apply (f ^ n) b)" |
|
700 |
by simp |
|
701 |
then have *: "apply (inverse f ^ m * f ^ n) b = a" |
|
702 |
by (simp add: apply_sequence perm_power_inverse) |
|
703 |
have "a \<in> orbit f b" |
|
704 |
proof (cases n m rule: linorder_cases) |
|
705 |
case equal with * show ?thesis |
|
706 |
by (simp add: perm_power_inverse) |
|
707 |
next |
|
708 |
case less |
|
709 |
moreover define q where "q = m - n" |
|
710 |
ultimately have "m = q + n" by arith |
|
711 |
with * have "apply (inverse f ^ q) b = a" |
|
712 |
by (simp add: power_add mult.assoc perm_power_inverse) |
|
713 |
then have "a \<in> orbit (inverse f) b" |
|
714 |
by (rule in_orbitI) |
|
715 |
then show ?thesis |
|
716 |
by simp |
|
717 |
next |
|
718 |
case greater |
|
719 |
moreover define q where "q = n - m" |
|
720 |
ultimately have "n = m + q" by arith |
|
721 |
with * have "apply (f ^ q) b = a" |
|
722 |
by (simp add: power_add mult.assoc [symmetric] perm_power_inverse) |
|
723 |
then show ?thesis |
|
724 |
by (rule in_orbitI) |
|
725 |
qed |
|
726 |
with assms show False |
|
727 |
by (auto dest: orbit_equiv) |
|
728 |
qed |
|
729 |
||
730 |
||
731 |
subsection \<open>Swaps\<close> |
|
732 |
||
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
733 |
lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm" ("\<langle>_ \<leftrightarrow> _\<rangle>") |
63375 | 734 |
is "\<lambda>a b. Fun.swap a b id" |
735 |
proof |
|
736 |
fix a b :: 'a |
|
737 |
have "{c. Fun.swap a b id c \<noteq> c} \<subseteq> {a, b}" |
|
738 |
by (auto simp add: Fun.swap_def) |
|
739 |
then show "finite {c. Fun.swap a b id c \<noteq> c}" |
|
740 |
by (rule finite_subset) simp |
|
741 |
qed simp |
|
742 |
||
743 |
lemma apply_swap_simp [simp]: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
744 |
"\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> a = b" |
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
745 |
"\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> b = a" |
63375 | 746 |
by (transfer; simp)+ |
747 |
||
748 |
lemma apply_swap_same [simp]: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
749 |
"c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = c" |
63375 | 750 |
by transfer simp |
751 |
||
752 |
lemma apply_swap_eq_iff [simp]: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
753 |
"\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b" |
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
754 |
"\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a" |
63375 | 755 |
by (transfer; auto simp add: Fun.swap_def)+ |
756 |
||
757 |
lemma swap_1 [simp]: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
758 |
"\<langle>a \<leftrightarrow> a\<rangle> = 1" |
63375 | 759 |
by transfer simp |
760 |
||
761 |
lemma swap_sym: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
762 |
"\<langle>b \<leftrightarrow> a\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>" |
63375 | 763 |
by (transfer; auto simp add: Fun.swap_def)+ |
764 |
||
765 |
lemma swap_self [simp]: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
766 |
"\<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> = 1" |
63375 | 767 |
by transfer (simp add: Fun.swap_def fun_eq_iff) |
768 |
||
769 |
lemma affected_swap: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
770 |
"a \<noteq> b \<Longrightarrow> affected \<langle>a \<leftrightarrow> b\<rangle> = {a, b}" |
63375 | 771 |
by transfer (auto simp add: Fun.swap_def) |
772 |
||
773 |
lemma inverse_swap [simp]: |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
774 |
"inverse \<langle>a \<leftrightarrow> b\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>" |
63375 | 775 |
by transfer (auto intro: inv_equality simp: Fun.swap_def) |
776 |
||
777 |
||
778 |
subsection \<open>Permutations specified by cycles\<close> |
|
779 |
||
780 |
fun cycle :: "'a list \<Rightarrow> 'a perm" ("\<langle>_\<rangle>") |
|
781 |
where |
|
782 |
"\<langle>[]\<rangle> = 1" |
|
783 |
| "\<langle>[a]\<rangle> = 1" |
|
784 |
| "\<langle>a # b # as\<rangle> = \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>" |
|
785 |
||
786 |
text \<open> |
|
787 |
We do not continue and restrict ourselves to syntax from here. |
|
788 |
See also introductory note. |
|
789 |
\<close> |
|
790 |
||
791 |
||
792 |
subsection \<open>Syntax\<close> |
|
793 |
||
794 |
bundle no_permutation_syntax |
|
795 |
begin |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
796 |
no_notation swap ("\<langle>_ \<leftrightarrow> _\<rangle>") |
63375 | 797 |
no_notation cycle ("\<langle>_\<rangle>") |
798 |
no_notation "apply" (infixl "\<langle>$\<rangle>" 999) |
|
799 |
end |
|
800 |
||
801 |
bundle permutation_syntax |
|
802 |
begin |
|
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
72302
diff
changeset
|
803 |
notation swap ("\<langle>_ \<leftrightarrow> _\<rangle>") |
63375 | 804 |
notation cycle ("\<langle>_\<rangle>") |
805 |
notation "apply" (infixl "\<langle>$\<rangle>" 999) |
|
806 |
end |
|
807 |
||
808 |
unbundle no_permutation_syntax |
|
809 |
||
810 |
end |