src/HOL/Library/Perm.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 64911 f0e07600de47
child 67399 eab6ce8368fa
permissions -rw-r--r--
more robust sorted_entries;
     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