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