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