src/HOL/Library/Perm.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 64911 f0e07600de47 child 67399 eab6ce8368fa permissions -rw-r--r--
executable domain membership checks
```     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.
```
```    15   But see theory \<open>src/HOL/ex/Perm_Fragments.thy\<close> for
```
```    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
```
```    23 proof
```
```    24   show "id \<in> ?perm" by simp
```
```    25 qed
```
```    26
```
```    27 setup_lifting type_definition_perm
```
```    28
```
```    29 notation "apply" (infixl "\<langle>\$\<rangle>" 999)
```
```    30 no_notation "apply" ("op \<langle>\$\<rangle>")
```
```    31
```
```    32 lemma bij_apply [simp]:
```
```    33   "bij (apply f)"
```
```    34   using "apply" [of f] by simp
```
```    35
```
```    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)
```
```    40
```
```    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)
```
```    44
```
```    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)
```
```    48
```
```    49 lift_definition affected :: "'a perm \<Rightarrow> 'a set"
```
```    50   is "\<lambda>f. {a. f a \<noteq> a}" .
```
```    51
```
```    52 lemma in_affected:
```
```    53   "a \<in> affected f \<longleftrightarrow> f \<langle>\$\<rangle> a \<noteq> a"
```
```    54   by transfer simp
```
```    55
```
```    56 lemma finite_affected [simp]:
```
```    57   "finite (affected f)"
```
```    58   by transfer simp
```
```    59
```
```    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
```
```    72
```
```    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"
```
```    86     by (simp add: in_affected)
```
```    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
```
```    91
```
```    92
```
```    93 subsection \<open>Identity, composition and inversion\<close>
```
```    94
```
```    95 instantiation Perm.perm :: (type) "{monoid_mult, inverse}"
```
```    96 begin
```
```    97
```
```    98 lift_definition one_perm :: "'a perm"
```
```    99   is id
```
```   100   by simp
```
```   101
```
```   102 lemma apply_one [simp]:
```
```   103   "apply 1 = id"
```
```   104   by (fact one_perm.rep_eq)
```
```   105
```
```   106 lemma affected_one [simp]:
```
```   107   "affected 1 = {}"
```
```   108   by transfer simp
```
```   109
```
```   110 lemma affected_empty_iff [simp]:
```
```   111   "affected f = {} \<longleftrightarrow> f = 1"
```
```   112   by transfer auto
```
```   113
```
```   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)
```
```   127
```
```   128 lemma apply_times:
```
```   129   "apply (f * g) = apply f \<circ> apply g"
```
```   130   by (fact times_perm.rep_eq)
```
```   131
```
```   132 lemma apply_sequence:
```
```   133   "f \<langle>\$\<rangle> (g \<langle>\$\<rangle> a) = apply (f * g) a"
```
```   134   by (simp add: apply_times)
```
```   135
```
```   136 lemma affected_times [simp]:
```
```   137   "affected (f * g) \<subseteq> affected f \<union> affected g"
```
```   138   by transfer auto
```
```   139
```
```   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}"
```
```   149     by (simp add: bij_inv)
```
```   150 qed
```
```   151
```
```   152 instance
```
```   153   by standard (transfer; simp add: comp_assoc)+
```
```   154
```
```   155 end
```
```   156
```
```   157 lemma apply_inverse:
```
```   158   "apply (inverse f) = inv (apply f)"
```
```   159   by (fact inverse_perm.rep_eq)
```
```   160
```
```   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
```
```   171
```
```   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
```
```   187
```
```   188 declare perm.inverse_distrib_swap [simp]
```
```   189
```
```   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
```
```   220
```
```   221 lemma apply_power:
```
```   222   "apply (f ^ n) = apply f ^^ n"
```
```   223   by (induct n) (simp_all add: apply_times)
```
```   224
```
```   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
```
```   234
```
```   235
```
```   236 subsection \<open>Orbit and order of elements\<close>
```
```   237
```
```   238 definition orbit :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a set"
```
```   239 where
```
```   240   "orbit f a = range (\<lambda>n. (f ^ n) \<langle>\$\<rangle> a)"
```
```   241
```
```   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)
```
```   246
```
```   247 lemma apply_power_self_in_orbit [simp]:
```
```   248   "(f ^ n) \<langle>\$\<rangle> a \<in> orbit f a"
```
```   249   by (rule in_orbitI) rule
```
```   250
```
```   251 lemma in_orbit_self [simp]:
```
```   252   "a \<in> orbit f a"
```
```   253   using apply_power_self_in_orbit [of _ 0] by simp
```
```   254
```
```   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
```
```   258
```
```   259 lemma orbit_not_empty [simp]:
```
```   260   "orbit f a \<noteq> {}"
```
```   261   using in_orbit_self [of a f] by blast
```
```   262
```
```   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"
```
```   268     by (simp add: in_affected)
```
```   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
```
```   278
```
```   279 definition order :: "'a perm \<Rightarrow> 'a \<Rightarrow> nat"
```
```   280 where
```
```   281   "order f = card \<circ> orbit f"
```
```   282
```
```   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)"
```
```   291     by (simp add: orbit_def)
```
```   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
```
```   302
```
```   303 lemma finite_orbit [simp]:
```
```   304   "finite (orbit f a)"
```
```   305 proof (cases "a \<in> affected f")
```
```   306   case False then show ?thesis
```
```   307     by (simp add: not_in_affected_iff_orbit_eq_singleton)
```
```   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
```
```   314
```
```   315 lemma orbit_1 [simp]:
```
```   316   "orbit 1 a = {a}"
```
```   317   by (auto simp add: orbit_def)
```
```   318
```
```   319 lemma order_1 [simp]:
```
```   320   "order 1 a = 1"
```
```   321   unfolding order_def by simp
```
```   322
```
```   323 lemma card_orbit_eq [simp]:
```
```   324   "card (orbit f a) = order f a"
```
```   325   by (simp add: order_def)
```
```   326
```
```   327 lemma order_greater_zero [simp]:
```
```   328   "order f a > 0"
```
```   329   by (simp only: card_gt_0_iff order_def comp_def) simp
```
```   330
```
```   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
```
```   341     by (simp add: not_in_affected_iff_orbit_eq_singleton)
```
```   342 next
```
```   343   assume ?Q
```
```   344   then have "orbit f a = {a}"
```
```   345     by (simp add: not_in_affected_iff_orbit_eq_singleton)
```
```   346   then have "card (orbit f a) = 1"
```
```   347     by simp
```
```   348   then show ?P
```
```   349     by simp
```
```   350 qed
```
```   351
```
```   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
```
```   359
```
```   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"
```
```   369     by (simp add: card_insert)
```
```   370   case False then have "order f a = 1"
```
```   371     by (simp add: order_eq_one_iff)
```
```   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
```
```   381
```
```   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"
```
```   388     by (simp add: not_le)
```
```   389   with order_greater_zero [of f a] have "order f a = 1"
```
```   390     by arith
```
```   391   with assms show False
```
```   392     by (simp add: order_eq_one_iff)
```
```   393 qed
```
```   394
```
```   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)
```
```   411         (simp_all add: power_add apply_times assms)
```
```   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
```
```   431
```
```   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)"
```
```   458         by (simp add: power_add apply_times)
```
```   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
```
```   471       by (simp add: lessThan_Suc)
```
```   472   qed
```
```   473   then show ?thesis by simp
```
```   474 qed
```
```   475
```
```   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
```
```   489
```
```   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
```
```   494
```
```   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
```
```   533
```
```   534 lemma apply_power_left_mult_order [simp]:
```
```   535   "(f ^ (n * order f a)) \<langle>\$\<rangle> a = a"
```
```   536   by (induct n) (simp_all add: power_add apply_times)
```
```   537
```
```   538 lemma apply_power_right_mult_order [simp]:
```
```   539   "(f ^ (order f a * n)) \<langle>\$\<rangle> a = a"
```
```   540   by (simp add: ac_simps)
```
```   541
```
```   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"
```
```   548     by (simp add: power_add [symmetric])
```
```   549   finally show ?thesis
```
```   550     by (simp add: apply_times)
```
```   551 qed
```
```   552
```
```   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
```
```   569
```
```   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
```
```   584
```
```   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)
```
```   589
```
```   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
```
```   608
```
```   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]
```
```   612     by (simp add: mod_eq_0_iff_dvd)
```
```   613
```
```   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"
```
```   625     by (simp add: apply_sequence)
```
```   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
```
```   629     unfolding apply_sequence power_add [symmetric]
```
```   630     apply (rule in_orbitI) apply rule
```
```   631     done
```
```   632 qed
```
```   633
```
```   634 lemma orbit_apply [simp]:
```
```   635   "orbit f (f \<langle>\$\<rangle> a) = orbit f a"
```
```   636   by (rule orbit_equiv) simp
```
```   637
```
```   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)
```
```   641
```
```   642 lemma orbit_apply_inverse [simp]:
```
```   643   "orbit f (inverse f \<langle>\$\<rangle> a) = orbit f a"
```
```   644   by (rule orbit_equiv) simp
```
```   645
```
```   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)
```
```   649
```
```   650 lemma orbit_apply_power [simp]:
```
```   651   "orbit f ((f ^ n) \<langle>\$\<rangle> a) = orbit f a"
```
```   652   by (rule orbit_equiv) simp
```
```   653
```
```   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)
```
```   657
```
```   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"
```
```   668     by (simp add: perm_power_inverse)
```
```   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)
```
```   678       (simp add: apply_inverse_eq_apply_power_order_minus_one
```
```   679       perm_power_inverse power_mult [symmetric])
```
```   680 qed
```
```   681
```
```   682 lemma order_inverse [simp]:
```
```   683   "order (inverse f) = order f"
```
```   684   by (simp add: order_def)
```
```   685
```
```   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
```
```   707       by (simp add: perm_power_inverse)
```
```   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"
```
```   713       by (simp add: power_add mult.assoc perm_power_inverse)
```
```   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"
```
```   723       by (simp add: power_add mult.assoc [symmetric] perm_power_inverse)
```
```   724     then show ?thesis
```
```   725       by (rule in_orbitI)
```
```   726   qed
```
```   727   with assms show False
```
```   728     by (auto dest: orbit_equiv)
```
```   729 qed
```
```   730
```
```   731
```
```   732 subsection \<open>Swaps\<close>
```
```   733
```
```   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
```
```   743
```
```   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)+
```
```   748
```
```   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
```
```   752
```
```   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)+
```
```   757
```
```   758 lemma swap_1 [simp]:
```
```   759   "\<langle>a\<leftrightarrow>a\<rangle> = 1"
```
```   760   by transfer simp
```
```   761
```
```   762 lemma swap_sym:
```
```   763   "\<langle>b\<leftrightarrow>a\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
```
```   764   by (transfer; auto simp add: Fun.swap_def)+
```
```   765
```
```   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)
```
```   769
```
```   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)
```
```   773
```
```   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)
```
```   777
```
```   778
```
```   779 subsection \<open>Permutations specified by cycles\<close>
```
```   780
```
```   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>"
```
```   786
```
```   787 text \<open>
```
```   788   We do not continue and restrict ourselves to syntax from here.
```
```   789   See also introductory note.
```
```   790 \<close>
```
```   791
```
```   792
```
```   793 subsection \<open>Syntax\<close>
```
```   794
```
```   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
```
```   801
```
```   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
```
```   809
```
```   810 unbundle no_permutation_syntax
```
```   811
```
```   812 end
```