src/HOL/Library/Perm.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 64911 f0e07600de47
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned proofs;
haftmann@63375
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@63375
     2
haftmann@63375
     3
section \<open>Permutations as abstract type\<close>
haftmann@63375
     4
haftmann@63375
     5
theory Perm
haftmann@63375
     6
imports Main
haftmann@63375
     7
begin
haftmann@63375
     8
haftmann@63375
     9
text \<open>
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 \<open>src/HOL/ex/Perm_Fragments.thy\<close> for
haftmann@63375
    16
  fragments on that.
haftmann@63375
    17
\<close>
haftmann@63375
    18
haftmann@63375
    19
subsection \<open>Abstract type of permutations\<close>
haftmann@63375
    20
haftmann@63375
    21
typedef 'a perm = "{f :: 'a \<Rightarrow> 'a. bij f \<and> finite {a. f a \<noteq> a}}"
haftmann@63375
    22
  morphisms "apply" Perm
wenzelm@63433
    23
proof
wenzelm@63433
    24
  show "id \<in> ?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 "\<langle>$\<rangle>" 999)
haftmann@63375
    30
no_notation "apply" ("op \<langle>$\<rangle>")
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 "\<And>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> 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 \<longleftrightarrow> (\<forall>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> a)"
haftmann@63375
    43
  by (auto intro: perm_eqI)
haftmann@63375
    44
haftmann@63375
    45
lemma apply_inj:
haftmann@63375
    46
  "f \<langle>$\<rangle> a = f \<langle>$\<rangle> b \<longleftrightarrow> 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 \<Rightarrow> 'a set"
haftmann@63375
    50
  is "\<lambda>f. {a. f a \<noteq> a}" .
haftmann@63375
    51
haftmann@63375
    52
lemma in_affected:
haftmann@63375
    53
  "a \<in> affected f \<longleftrightarrow> f \<langle>$\<rangle> a \<noteq> 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 \<langle>$\<rangle> a \<in> affected f \<longleftrightarrow> a \<in> affected f"
haftmann@63375
    62
proof transfer
haftmann@63375
    63
  fix f :: "'a \<Rightarrow> 'a" and a :: 'a
haftmann@63375
    64
  assume "bij f \<and> finite {b. f b \<noteq> b}"
haftmann@63375
    65
  then have "bij f" by simp
haftmann@63375
    66
  interpret bijection f by standard (rule \<open>bij f\<close>)
haftmann@63375
    67
  have "f a \<in> {a. f a = a} \<longleftrightarrow> a \<in> {a. f a = a}" (is "?P \<longleftrightarrow> ?Q")
haftmann@63375
    68
    by auto
haftmann@63375
    69
  then show "f a \<in> {a. f a \<noteq> a} \<longleftrightarrow> a \<in> {a. f a \<noteq> 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) \<noteq> 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 \<langle>$\<rangle> a \<noteq> a"
haftmann@63375
    82
    by (simp add: in_affected [symmetric])
wenzelm@63540
    83
  with * have "f \<langle>$\<rangle> a \<notin> affected f"
haftmann@63375
    84
    by simp
haftmann@63375
    85
  then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
haftmann@63375
    86
    by (simp add: in_affected)
haftmann@63375
    87
  then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> 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 \<open>Identity, composition and inversion\<close>
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 = {} \<longleftrightarrow> f = 1"
haftmann@63375
   112
  by transfer auto
haftmann@63375
   113
haftmann@63375
   114
lift_definition times_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm"
haftmann@63375
   115
  is comp
haftmann@63375
   116
proof
haftmann@63375
   117
  fix f g :: "'a \<Rightarrow> 'a"
haftmann@63375
   118
  assume "bij f \<and> finite {a. f a \<noteq> a}"
haftmann@63375
   119
    "bij g \<and>finite {a. g a \<noteq> a}"
haftmann@63375
   120
  then have "finite ({a. f a \<noteq> a} \<union> {a. g a \<noteq> a})"
haftmann@63375
   121
    by simp
haftmann@63375
   122
  moreover have "{a. (f \<circ> g) a \<noteq> a} \<subseteq> {a. f a \<noteq> a} \<union> {a. g a \<noteq> a}"
haftmann@63375
   123
    by auto
haftmann@63375
   124
  ultimately show "finite {a. (f \<circ> g) a \<noteq> 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 \<circ> apply g"
haftmann@63375
   130
  by (fact times_perm.rep_eq)
haftmann@63375
   131
haftmann@63375
   132
lemma apply_sequence:
haftmann@63375
   133
  "f \<langle>$\<rangle> (g \<langle>$\<rangle> 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) \<subseteq> affected f \<union> affected g"
haftmann@63375
   138
  by transfer auto
haftmann@63375
   139
haftmann@63375
   140
lift_definition inverse_perm :: "'a perm \<Rightarrow> 'a perm"
haftmann@63375
   141
  is inv
haftmann@63375
   142
proof transfer
haftmann@63375
   143
  fix f :: "'a \<Rightarrow> 'a" and a
haftmann@63375
   144
  assume "bij f \<and> finite {b. f b \<noteq> b}"
haftmann@63375
   145
  then have "bij f" and fin: "finite {b. f b \<noteq> b}"
haftmann@63375
   146
    by auto
haftmann@63375
   147
  interpret bijection f by standard (rule \<open>bij f\<close>)
haftmann@63375
   148
  from fin show "bij (inv f) \<and> finite {a. inv f a \<noteq> 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 \<Rightarrow> 'a" and a
haftmann@63375
   165
  assume "bij f \<and> finite {b. f b \<noteq> b}"
haftmann@63375
   166
  then have "bij f" by simp
haftmann@63375
   167
  interpret bijection f by standard (rule \<open>bij f\<close>)
haftmann@63375
   168
  show "{a. inv f a \<noteq> a} = {a. f a \<noteq> 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 \<Rightarrow> 'a" and a
haftmann@63375
   180
    assume "bij f \<and> finite {b. f b \<noteq> b}"
haftmann@63375
   181
    then have "bij f" by simp
haftmann@63375
   182
    interpret bijection f by standard (rule \<open>bij f\<close>)
haftmann@63375
   183
    show "inv f \<circ> 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 \<inter> 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 \<in> affected f \<Longrightarrow> a \<notin> affected g"
haftmann@63375
   196
    "a \<in> affected g \<Longrightarrow> a \<notin> affected f" for a
haftmann@63375
   197
    by auto
haftmann@63375
   198
  consider "a \<in> affected f \<and> a \<notin> affected g
haftmann@63375
   199
        \<and> f \<langle>$\<rangle> a \<in> affected f"
haftmann@63375
   200
    | "a \<notin> affected f \<and> a \<in> affected g
haftmann@63375
   201
        \<and> f \<langle>$\<rangle> a \<notin> affected f"
haftmann@63375
   202
    | "a \<notin> affected f \<and> a \<notin> affected g"
haftmann@63375
   203
    using assms by auto
haftmann@63375
   204
  then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a"
haftmann@63375
   205
  proof cases
wenzelm@63540
   206
    case 1
wenzelm@63540
   207
    with * have "f \<langle>$\<rangle> a \<notin> 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 \<langle>$\<rangle> a \<notin> 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 \<open>Orbit and order of elements\<close>
haftmann@63375
   237
haftmann@63375
   238
definition orbit :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a set"
haftmann@63375
   239
where
haftmann@63375
   240
  "orbit f a = range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)"
haftmann@63375
   241
haftmann@63375
   242
lemma in_orbitI:
haftmann@63375
   243
  assumes "(f ^ n) \<langle>$\<rangle> a = b"
haftmann@63375
   244
  shows "b \<in> 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) \<langle>$\<rangle> a \<in> 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 \<in> 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 \<langle>$\<rangle> a \<in> 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 \<noteq> {}"
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 \<notin> affected f \<longleftrightarrow> orbit f a = {a}" (is "?P \<longleftrightarrow> ?Q")
haftmann@63375
   265
proof
haftmann@63375
   266
  assume ?P
haftmann@63375
   267
  then have "f \<langle>$\<rangle> a = a"
haftmann@63375
   268
    by (simp add: in_affected)
haftmann@63375
   269
  then have "(f ^ n) \<langle>$\<rangle> 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 \<Rightarrow> 'a \<Rightarrow> nat"
haftmann@63375
   280
where
wenzelm@63993
   281
  "order f = card \<circ> orbit f"
haftmann@63375
   282
haftmann@63375
   283
lemma orbit_subset_eq_affected:
haftmann@63375
   284
  assumes "a \<in> affected f"
haftmann@63375
   285
  shows "orbit f a \<subseteq> affected f"
haftmann@63375
   286
proof (rule ccontr)
haftmann@63375
   287
  assume "\<not> orbit f a \<subseteq> affected f"
haftmann@63375
   288
  then obtain b where "b \<in> orbit f a" and "b \<notin> affected f"
haftmann@63375
   289
    by auto
haftmann@63375
   290
  then have "b \<in> range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)"
haftmann@63375
   291
    by (simp add: orbit_def)
haftmann@63375
   292
  then obtain n where "b = (f ^ n) \<langle>$\<rangle> a"
haftmann@63375
   293
    by blast
haftmann@63375
   294
  with \<open>b \<notin> affected f\<close>
haftmann@63375
   295
  have "(f ^ n) \<langle>$\<rangle> a \<notin> affected f"
haftmann@63375
   296
    by simp
haftmann@63375
   297
  then have "f \<langle>$\<rangle> a \<notin> 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 \<in> 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 \<subseteq> 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 \<longleftrightarrow> a \<notin> affected f" (is "?P \<longleftrightarrow> ?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 \<open>orbit f a = {b}\<close> 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 \<ge> 2 \<longleftrightarrow> a \<in> 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 \<noteq> 1"
haftmann@63375
   362
  shows "order f a \<le> card (affected f)"
haftmann@63375
   363
proof (cases "a \<in> affected f")
haftmann@63375
   364
  from assms have "affected f \<noteq> {}"
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) \<ge> 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 \<open>card (affected f) \<ge> 1\<close> show ?thesis
haftmann@63375
   373
    by simp
haftmann@63375
   374
next
haftmann@63375
   375
  case True
haftmann@63375
   376
  have "card (orbit f a) \<le> 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 \<in> affected f"
haftmann@63375
   384
  shows "order f a \<ge> 2"
haftmann@63375
   385
proof (rule ccontr)
haftmann@63375
   386
  assume "\<not> 2 \<le> 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) \<langle>$\<rangle> a = a"
haftmann@63375
   397
  shows "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n})"
haftmann@63375
   398
proof  -
haftmann@63375
   399
  have "orbit f a = (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n}" (is "_ = ?B")
haftmann@63375
   400
  proof (rule set_eqI, rule)
haftmann@63375
   401
    fix b
haftmann@63375
   402
    assume "b \<in> orbit f a"
haftmann@63375
   403
    then obtain m where "(f ^ m) \<langle>$\<rangle> 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))) \<langle>$\<rangle> a"
haftmann@63375
   406
      by simp
haftmann@63375
   407
    also have "\<dots> = (f ^ (m mod n)) \<langle>$\<rangle> ((f ^ (n * (m div n))) \<langle>$\<rangle> a)"
haftmann@63375
   408
      by (simp only: power_add apply_times) simp
haftmann@63375
   409
    also have "(f ^ (n * q)) \<langle>$\<rangle> 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)) \<langle>$\<rangle> a" .
haftmann@63375
   413
    moreover from \<open>n > 0\<close>
haftmann@63375
   414
    have "m mod n < n" 
haftmann@63375
   415
      by simp
haftmann@63375
   416
    ultimately show "b \<in> ?B"
haftmann@63375
   417
      by auto
haftmann@63375
   418
  next
haftmann@63375
   419
    fix b
haftmann@63375
   420
    assume "b \<in> ?B"
haftmann@63375
   421
    then obtain m where "(f ^ m) \<langle>$\<rangle> a = b"
haftmann@63375
   422
      by blast
haftmann@63375
   423
    then show "b \<in> 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 (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<order f a}"
haftmann@63375
   434
proof -
haftmann@63375
   435
  have "inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}"
haftmann@63375
   436
    if "n \<le> 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 (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}"
haftmann@63375
   444
      by simp
haftmann@63375
   445
    have "(f ^ n) \<langle>$\<rangle> a \<notin> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}"
haftmann@63375
   446
    proof
haftmann@63375
   447
      assume "(f ^ n) \<langle>$\<rangle> a \<in> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}"
haftmann@63375
   448
      then obtain m where *: "(f ^ m) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> 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 \<open>m < n\<close> have "n = m + (n - m)"
haftmann@63375
   453
        and nm: "0 < n - m" "n - m \<le> n"
haftmann@63375
   454
        by arith+
haftmann@63375
   455
      with * have "(f ^ m) \<langle>$\<rangle> a = (f ^ (m + (n - m))) \<langle>$\<rangle> a"
haftmann@63375
   456
        by simp
haftmann@63375
   457
      then have "(f ^ m) \<langle>$\<rangle> a = (f ^ m) \<langle>$\<rangle> ((f ^ (n - m)) \<langle>$\<rangle> a)"
haftmann@63375
   458
        by (simp add: power_add apply_times)
haftmann@63375
   459
      then have "(f ^ (n - m)) \<langle>$\<rangle> a = a"
haftmann@63375
   460
        by simp
haftmann@63375
   461
      with \<open>n - m > 0\<close>
haftmann@63375
   462
      have "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m})"
haftmann@63375
   463
         by (rule order_witness_unfold)
haftmann@63375
   464
      also have "card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m}) \<le> card {0..<n - m}"
haftmann@63375
   465
        by (rule card_image_le) simp
haftmann@63375
   466
      finally have "order f a \<le> 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 = (\<lambda>n. (f ^ n) \<langle>$\<rangle> a) ` {..<order f a}" (is "_ = ?A")
haftmann@63375
   478
proof (rule sym, rule card_subset_eq)
haftmann@63375
   479
  show "finite (orbit f a)"
haftmann@63375
   480
    by simp
haftmann@63375
   481
  show "?A \<subseteq> 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 \<in> orbit f a"
haftmann@63375
   492
  obtains n where "b = (f ^ n) \<langle>$\<rangle> 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) \<langle>$\<rangle> a = a"
haftmann@63375
   497
proof -
haftmann@63375
   498
  have "(f ^ order f a) \<langle>$\<rangle> a \<in> orbit f a"
haftmann@63375
   499
    by simp
haftmann@63375
   500
  then obtain n where
haftmann@63375
   501
    *: "(f ^ order f a) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> 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 \<open>n < order f a\<close>
haftmann@63375
   513
      have "m < order f a"
haftmann@63375
   514
      by simp
haftmann@63375
   515
    with Suc *
haftmann@63375
   516
    have "(inverse f) \<langle>$\<rangle> ((f ^ Suc (order f a - 1)) \<langle>$\<rangle> a) =
haftmann@63375
   517
      (inverse f) \<langle>$\<rangle> ((f ^ Suc m) \<langle>$\<rangle> a)"
haftmann@63375
   518
      by simp
haftmann@63375
   519
    then have "(f ^ (order f a - 1)) \<langle>$\<rangle> a =
haftmann@63375
   520
      (f ^ m) \<langle>$\<rangle> 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: \<open>m < order f a\<close>)
haftmann@63375
   527
    with Suc have "n = order f a"
haftmann@63375
   528
      by auto
haftmann@63375
   529
    with \<open>n < order f a\<close>
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)) \<langle>$\<rangle> 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)) \<langle>$\<rangle> 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)) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a"
haftmann@63375
   544
proof -
haftmann@63375
   545
  have "(f ^ n) \<langle>$\<rangle> a = (f ^ (n mod order f a + order f a * (n div order f a))) \<langle>$\<rangle> a"
haftmann@63375
   546
    by simp
haftmann@63375
   547
  also have "\<dots> = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \<langle>$\<rangle> a"
haftmann@63375
   548
    by (simp add: power_add [symmetric])
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) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a \<longleftrightarrow> m mod order f a = n mod order f a" (is "?P \<longleftrightarrow> ?Q")
haftmann@63375
   555
proof
haftmann@63375
   556
  assume ?Q
haftmann@63375
   557
  then have "(f ^ (m mod order f a)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> 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)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> 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) \<langle>$\<rangle> a = (f ^ (order f a - 1)) \<langle>$\<rangle> 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) \<langle>$\<rangle> a = a"
haftmann@63375
   578
    by simp
haftmann@63375
   579
  then have *: "(inverse f) \<langle>$\<rangle> ((f ^ order f a) \<langle>$\<rangle> a) = (inverse f) \<langle>$\<rangle> 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) \<langle>$\<rangle> a \<in> 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)) \<langle>$\<rangle> a = (f ^ (order f a - n mod order f a)) \<langle>$\<rangle> 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) \<langle>$\<rangle> a = a \<longleftrightarrow> 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 \<in> 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) \<langle>$\<rangle> a"
haftmann@63375
   619
    by (rule in_orbitE)
haftmann@63375
   620
  then show "?B \<subseteq> ?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)) \<langle>$\<rangle> b = (inverse (f ^ n)) \<langle>$\<rangle> ((f ^ n) \<langle>$\<rangle> a)"
haftmann@63375
   623
    by simp
haftmann@63375
   624
  then have a: "a = (inverse (f ^ n)) \<langle>$\<rangle> b"
haftmann@63375
   625
    by (simp add: apply_sequence)
haftmann@63375
   626
  then show "?A \<subseteq> ?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 \<langle>$\<rangle> 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 \<langle>$\<rangle> 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 \<langle>$\<rangle> 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 \<langle>$\<rangle> 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) \<langle>$\<rangle> 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) \<langle>$\<rangle> 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 \<in> orbit f a"
haftmann@63375
   663
  then obtain n where b: "b = (f ^ n) \<langle>$\<rangle> 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 \<in> orbit (inverse f) a"
haftmann@63375
   672
    by simp
haftmann@63375
   673
next
haftmann@63375
   674
  fix b a
haftmann@63375
   675
  assume "b \<in> orbit (inverse f) a"
haftmann@63375
   676
  then show "b \<in> 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 \<noteq> orbit f b"
haftmann@63375
   688
  shows "orbit f a \<inter> orbit f b = {}"
haftmann@63375
   689
proof (rule ccontr)
haftmann@63375
   690
  assume "orbit f a \<inter> orbit f b \<noteq> {}"
haftmann@63375
   691
  then obtain c where "c \<in> orbit f a \<inter> orbit f b"
haftmann@63375
   692
    by blast
haftmann@63375
   693
  then have "c \<in> orbit f a" and "c \<in> orbit f b"
haftmann@63375
   694
    by auto
haftmann@63375
   695
  then obtain m n where "c = (f ^ m) \<langle>$\<rangle> a"
haftmann@63375
   696
    and "c = apply (f ^ n) b" by (blast elim!: in_orbitE)
haftmann@63375
   697
  then have "(f ^ m) \<langle>$\<rangle> a = apply (f ^ n) b"
haftmann@63375
   698
    by simp
haftmann@63375
   699
  then have "apply (inverse f ^ m) ((f ^ m) \<langle>$\<rangle> 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 \<in> 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 \<in> 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 \<open>Swaps\<close>
haftmann@63375
   733
haftmann@63375
   734
lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm"  ("\<langle>_\<leftrightarrow>_\<rangle>")
haftmann@63375
   735
  is "\<lambda>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 \<noteq> c} \<subseteq> {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 \<noteq> 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
  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> a = b"
haftmann@63375
   746
  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> b = a"
haftmann@63375
   747
  by (transfer; simp)+
haftmann@63375
   748
haftmann@63375
   749
lemma apply_swap_same [simp]:
haftmann@63375
   750
  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = c"
haftmann@63375
   751
  by transfer simp
haftmann@63375
   752
haftmann@63375
   753
lemma apply_swap_eq_iff [simp]:
haftmann@63375
   754
  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
haftmann@63375
   755
  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> 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
  "\<langle>a\<leftrightarrow>a\<rangle> = 1"
haftmann@63375
   760
  by transfer simp
haftmann@63375
   761
haftmann@63375
   762
lemma swap_sym:
haftmann@63375
   763
  "\<langle>b\<leftrightarrow>a\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
haftmann@63375
   764
  by (transfer; auto simp add: Fun.swap_def)+
haftmann@63375
   765
haftmann@63375
   766
lemma swap_self [simp]:
haftmann@63375
   767
  "\<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> = 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 \<noteq> b \<Longrightarrow> affected \<langle>a\<leftrightarrow>b\<rangle> = {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 \<langle>a\<leftrightarrow>b\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
haftmann@63375
   776
  by transfer (auto intro: inv_equality simp: Fun.swap_def)
haftmann@63375
   777
haftmann@63375
   778
haftmann@63375
   779
subsection \<open>Permutations specified by cycles\<close>
haftmann@63375
   780
haftmann@63375
   781
fun cycle :: "'a list \<Rightarrow> 'a perm"  ("\<langle>_\<rangle>")
haftmann@63375
   782
where
haftmann@63375
   783
  "\<langle>[]\<rangle> = 1"
haftmann@63375
   784
| "\<langle>[a]\<rangle> = 1"
haftmann@63375
   785
| "\<langle>a # b # as\<rangle> = \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
haftmann@63375
   786
haftmann@63375
   787
text \<open>
haftmann@63375
   788
  We do not continue and restrict ourselves to syntax from here.
haftmann@63375
   789
  See also introductory note.
haftmann@63375
   790
\<close>
haftmann@63375
   791
haftmann@63375
   792
haftmann@63375
   793
subsection \<open>Syntax\<close>
haftmann@63375
   794
haftmann@63375
   795
bundle no_permutation_syntax
haftmann@63375
   796
begin
haftmann@63375
   797
  no_notation swap    ("\<langle>_\<leftrightarrow>_\<rangle>")
haftmann@63375
   798
  no_notation cycle   ("\<langle>_\<rangle>")
haftmann@63375
   799
  no_notation "apply" (infixl "\<langle>$\<rangle>" 999)
haftmann@63375
   800
end
haftmann@63375
   801
haftmann@63375
   802
bundle permutation_syntax
haftmann@63375
   803
begin
haftmann@63375
   804
  notation swap       ("\<langle>_\<leftrightarrow>_\<rangle>")
haftmann@63375
   805
  notation cycle      ("\<langle>_\<rangle>")
haftmann@63375
   806
  notation "apply"    (infixl "\<langle>$\<rangle>" 999)
haftmann@63375
   807
  no_notation "apply" ("op \<langle>$\<rangle>")
haftmann@63375
   808
end
haftmann@63375
   809
haftmann@63375
   810
unbundle no_permutation_syntax
haftmann@63375
   811
haftmann@63375
   812
end