# Theory Perm

theory Perm
imports Main
```(* Author: Florian Haftmann, TU Muenchen *)

section ‹Permutations as abstract type›

theory Perm
imports Main
begin

text ‹
This theory introduces basics about permutations, i.e. almost
everywhere fix bijections.  But it is by no means complete.
Grieviously missing are cycles since these would require more
elaboration, e.g. the concept of distinct lists equivalent
under rotation, which maybe would also deserve its own theory.
But see theory ‹src/HOL/ex/Perm_Fragments.thy› for
fragments on that.
›

subsection ‹Abstract type of permutations›

typedef 'a perm = "{f :: 'a ⇒ 'a. bij f ∧ finite {a. f a ≠ a}}"
morphisms "apply" Perm
proof
show "id ∈ ?perm" by simp
qed

setup_lifting type_definition_perm

notation "apply" (infixl "⟨\$⟩" 999)
no_notation "apply" ("(⟨\$⟩)")

lemma bij_apply [simp]:
"bij (apply f)"
using "apply" [of f] by simp

lemma perm_eqI:
assumes "⋀a. f ⟨\$⟩ a = g ⟨\$⟩ a"
shows "f = g"
using assms by transfer (simp add: fun_eq_iff)

lemma perm_eq_iff:
"f = g ⟷ (∀a. f ⟨\$⟩ a = g ⟨\$⟩ a)"
by (auto intro: perm_eqI)

lemma apply_inj:
"f ⟨\$⟩ a = f ⟨\$⟩ b ⟷ a = b"
by (rule inj_eq) (rule bij_is_inj, simp)

lift_definition affected :: "'a perm ⇒ 'a set"
is "λf. {a. f a ≠ a}" .

lemma in_affected:
"a ∈ affected f ⟷ f ⟨\$⟩ a ≠ a"
by transfer simp

lemma finite_affected [simp]:
"finite (affected f)"
by transfer simp

lemma apply_affected [simp]:
"f ⟨\$⟩ a ∈ affected f ⟷ a ∈ affected f"
proof transfer
fix f :: "'a ⇒ 'a" and a :: 'a
assume "bij f ∧ finite {b. f b ≠ b}"
then have "bij f" by simp
interpret bijection f by standard (rule ‹bij f›)
have "f a ∈ {a. f a = a} ⟷ a ∈ {a. f a = a}" (is "?P ⟷ ?Q")
by auto
then show "f a ∈ {a. f a ≠ a} ⟷ a ∈ {a. f a ≠ a}"
by simp
qed

lemma card_affected_not_one:
"card (affected f) ≠ 1"
proof
interpret bijection "apply f"
by standard (rule bij_apply)
assume "card (affected f) = 1"
then obtain a where *: "affected f = {a}"
by (rule card_1_singletonE)
then have **: "f ⟨\$⟩ a ≠ a"
by (simp flip: in_affected)
with * have "f ⟨\$⟩ a ∉ affected f"
by simp
then have "f ⟨\$⟩ (f ⟨\$⟩ a) = f ⟨\$⟩ a"
then have "inv (apply f) (f ⟨\$⟩ (f ⟨\$⟩ a)) = inv (apply f) (f ⟨\$⟩ a)"
by simp
with ** show False by simp
qed

subsection ‹Identity, composition and inversion›

instantiation Perm.perm :: (type) "{monoid_mult, inverse}"
begin

lift_definition one_perm :: "'a perm"
is id
by simp

lemma apply_one [simp]:
"apply 1 = id"
by (fact one_perm.rep_eq)

lemma affected_one [simp]:
"affected 1 = {}"
by transfer simp

lemma affected_empty_iff [simp]:
"affected f = {} ⟷ f = 1"
by transfer auto

lift_definition times_perm :: "'a perm ⇒ 'a perm ⇒ 'a perm"
is comp
proof
fix f g :: "'a ⇒ 'a"
assume "bij f ∧ finite {a. f a ≠ a}"
"bij g ∧finite {a. g a ≠ a}"
then have "finite ({a. f a ≠ a} ∪ {a. g a ≠ a})"
by simp
moreover have "{a. (f ∘ g) a ≠ a} ⊆ {a. f a ≠ a} ∪ {a. g a ≠ a}"
by auto
ultimately show "finite {a. (f ∘ g) a ≠ a}"
by (auto intro: finite_subset)
qed (auto intro: bij_comp)

lemma apply_times:
"apply (f * g) = apply f ∘ apply g"
by (fact times_perm.rep_eq)

lemma apply_sequence:
"f ⟨\$⟩ (g ⟨\$⟩ a) = apply (f * g) a"

lemma affected_times [simp]:
"affected (f * g) ⊆ affected f ∪ affected g"
by transfer auto

lift_definition inverse_perm :: "'a perm ⇒ 'a perm"
is inv
proof transfer
fix f :: "'a ⇒ 'a" and a
assume "bij f ∧ finite {b. f b ≠ b}"
then have "bij f" and fin: "finite {b. f b ≠ b}"
by auto
interpret bijection f by standard (rule ‹bij f›)
from fin show "bij (inv f) ∧ finite {a. inv f a ≠ a}"
qed

instance
by standard (transfer; simp add: comp_assoc)+

end

lemma apply_inverse:
"apply (inverse f) = inv (apply f)"
by (fact inverse_perm.rep_eq)

lemma affected_inverse [simp]:
"affected (inverse f) = affected f"
proof transfer
fix f :: "'a ⇒ 'a" and a
assume "bij f ∧ finite {b. f b ≠ b}"
then have "bij f" by simp
interpret bijection f by standard (rule ‹bij f›)
show "{a. inv f a ≠ a} = {a. f a ≠ a}"
by simp
qed

global_interpretation perm: group times "1::'a perm" inverse
proof
fix f :: "'a perm"
show "1 * f = f"
by transfer simp
show "inverse f * f = 1"
proof transfer
fix f :: "'a ⇒ 'a" and a
assume "bij f ∧ finite {b. f b ≠ b}"
then have "bij f" by simp
interpret bijection f by standard (rule ‹bij f›)
show "inv f ∘ f = id"
by simp
qed
qed

declare perm.inverse_distrib_swap [simp]

lemma perm_mult_commute:
assumes "affected f ∩ affected g = {}"
shows "g * f = f * g"
proof (rule perm_eqI)
fix a
from assms have *: "a ∈ affected f ⟹ a ∉ affected g"
"a ∈ affected g ⟹ a ∉ affected f" for a
by auto
consider "a ∈ affected f ∧ a ∉ affected g
∧ f ⟨\$⟩ a ∈ affected f"
| "a ∉ affected f ∧ a ∈ affected g
∧ f ⟨\$⟩ a ∉ affected f"
| "a ∉ affected f ∧ a ∉ affected g"
using assms by auto
then show "(g * f) ⟨\$⟩ a = (f * g) ⟨\$⟩ a"
proof cases
case 1
with * have "f ⟨\$⟩ a ∉ affected g"
by auto
with 1 show ?thesis by (simp add: in_affected apply_times)
next
case 2
with * have "g ⟨\$⟩ a ∉ affected f"
by auto
with 2 show ?thesis by (simp add: in_affected apply_times)
next
case 3
then show ?thesis by (simp add: in_affected apply_times)
qed
qed

lemma apply_power:
"apply (f ^ n) = apply f ^^ n"
by (induct n) (simp_all add: apply_times)

lemma perm_power_inverse:
"inverse f ^ n = inverse ((f :: 'a perm) ^ n)"
proof (induct n)
case 0 then show ?case by simp
next
case (Suc n)
then show ?case
unfolding power_Suc2 [of f] by simp
qed

subsection ‹Orbit and order of elements›

definition orbit :: "'a perm ⇒ 'a ⇒ 'a set"
where
"orbit f a = range (λn. (f ^ n) ⟨\$⟩ a)"

lemma in_orbitI:
assumes "(f ^ n) ⟨\$⟩ a = b"
shows "b ∈ orbit f a"
using assms by (auto simp add: orbit_def)

lemma apply_power_self_in_orbit [simp]:
"(f ^ n) ⟨\$⟩ a ∈ orbit f a"
by (rule in_orbitI) rule

lemma in_orbit_self [simp]:
"a ∈ orbit f a"
using apply_power_self_in_orbit [of _ 0] by simp

lemma apply_self_in_orbit [simp]:
"f ⟨\$⟩ a ∈ orbit f a"
using apply_power_self_in_orbit [of _ 1] by simp

lemma orbit_not_empty [simp]:
"orbit f a ≠ {}"
using in_orbit_self [of a f] by blast

lemma not_in_affected_iff_orbit_eq_singleton:
"a ∉ affected f ⟷ orbit f a = {a}" (is "?P ⟷ ?Q")
proof
assume ?P
then have "f ⟨\$⟩ a = a"
then have "(f ^ n) ⟨\$⟩ a = a" for n
by (induct n) (simp_all add: apply_times)
then show ?Q
next
assume ?Q
then show ?P
by (auto simp add: orbit_def in_affected dest: range_eq_singletonD [of _ _ 1])
qed

definition order :: "'a perm ⇒ 'a ⇒ nat"
where
"order f = card ∘ orbit f"

lemma orbit_subset_eq_affected:
assumes "a ∈ affected f"
shows "orbit f a ⊆ affected f"
proof (rule ccontr)
assume "¬ orbit f a ⊆ affected f"
then obtain b where "b ∈ orbit f a" and "b ∉ affected f"
by auto
then have "b ∈ range (λn. (f ^ n) ⟨\$⟩ a)"
then obtain n where "b = (f ^ n) ⟨\$⟩ a"
by blast
with ‹b ∉ affected f›
have "(f ^ n) ⟨\$⟩ a ∉ affected f"
by simp
then have "f ⟨\$⟩ a ∉ affected f"
by (induct n) (simp_all add: apply_times)
with assms show False
by simp
qed

lemma finite_orbit [simp]:
"finite (orbit f a)"
proof (cases "a ∈ affected f")
case False then show ?thesis
next
case True then have "orbit f a ⊆ affected f"
by (rule orbit_subset_eq_affected)
then show ?thesis using finite_affected
by (rule finite_subset)
qed

lemma orbit_1 [simp]:
"orbit 1 a = {a}"

lemma order_1 [simp]:
"order 1 a = 1"
unfolding order_def by simp

lemma card_orbit_eq [simp]:
"card (orbit f a) = order f a"

lemma order_greater_zero [simp]:
"order f a > 0"
by (simp only: card_gt_0_iff order_def comp_def) simp

lemma order_eq_one_iff:
"order f a = Suc 0 ⟷ a ∉ affected f" (is "?P ⟷ ?Q")
proof
assume ?P then have "card (orbit f a) = 1"
by simp
then obtain b where "orbit f a = {b}"
by (rule card_1_singletonE)
with in_orbit_self [of a f]
have "b = a" by simp
with ‹orbit f a = {b}› show ?Q
next
assume ?Q
then have "orbit f a = {a}"
then have "card (orbit f a) = 1"
by simp
then show ?P
by simp
qed

lemma order_greater_eq_two_iff:
"order f a ≥ 2 ⟷ a ∈ affected f"
using order_eq_one_iff [of f a]
using order_greater_zero [of f a]
apply simp
done

lemma order_less_eq_affected:
assumes "f ≠ 1"
shows "order f a ≤ card (affected f)"
proof (cases "a ∈ affected f")
from assms have "affected f ≠ {}"
by simp
then obtain B b where "affected f = insert b B"
by blast
with finite_affected [of f] have "card (affected f) ≥ 1"
case False then have "order f a = 1"
with ‹card (affected f) ≥ 1› show ?thesis
by simp
next
case True
have "card (orbit f a) ≤ card (affected f)"
by (rule card_mono) (simp_all add: True orbit_subset_eq_affected card_mono)
then show ?thesis
by simp
qed

lemma affected_order_greater_eq_two:
assumes "a ∈ affected f"
shows "order f a ≥ 2"
proof (rule ccontr)
assume "¬ 2 ≤ order f a"
then have "order f a < 2"
with order_greater_zero [of f a] have "order f a = 1"
by arith
with assms show False
qed

lemma order_witness_unfold:
assumes "n > 0" and "(f ^ n) ⟨\$⟩ a = a"
shows "order f a = card ((λm. (f ^ m) ⟨\$⟩ a) ` {0..<n})"
proof  -
have "orbit f a = (λm. (f ^ m) ⟨\$⟩ a) ` {0..<n}" (is "_ = ?B")
proof (rule set_eqI, rule)
fix b
assume "b ∈ orbit f a"
then obtain m where "(f ^ m) ⟨\$⟩ a = b"
then have "b = (f ^ (m mod n + n * (m div n))) ⟨\$⟩ a"
by simp
also have "… = (f ^ (m mod n)) ⟨\$⟩ ((f ^ (n * (m div n))) ⟨\$⟩ a)"
by (simp only: power_add apply_times) simp
also have "(f ^ (n * q)) ⟨\$⟩ a = a" for q
by (induct q)
finally have "b = (f ^ (m mod n)) ⟨\$⟩ a" .
moreover from ‹n > 0›
have "m mod n < n"
by simp
ultimately show "b ∈ ?B"
by auto
next
fix b
assume "b ∈ ?B"
then obtain m where "(f ^ m) ⟨\$⟩ a = b"
by blast
then show "b ∈ orbit f a"
by (rule in_orbitI)
qed
then have "card (orbit f a) = card ?B"
by (simp only:)
then show ?thesis
by simp
qed

lemma inj_on_apply_range:
"inj_on (λm. (f ^ m) ⟨\$⟩ a) {..<order f a}"
proof -
have "inj_on (λm. (f ^ m) ⟨\$⟩ a) {..<n}"
if "n ≤ order f a" for n
using that proof (induct n)
case 0 then show ?case by simp
next
case (Suc n)
then have prem: "n < order f a"
by simp
with Suc.hyps have hyp: "inj_on (λm. (f ^ m) ⟨\$⟩ a) {..<n}"
by simp
have "(f ^ n) ⟨\$⟩ a ∉ (λm. (f ^ m) ⟨\$⟩ a) ` {..<n}"
proof
assume "(f ^ n) ⟨\$⟩ a ∈ (λm. (f ^ m) ⟨\$⟩ a) ` {..<n}"
then obtain m where *: "(f ^ m) ⟨\$⟩ a = (f ^ n) ⟨\$⟩ a" and "m < n"
by auto
interpret bijection "apply (f ^ m)"
by standard simp
from ‹m < n› have "n = m + (n - m)"
and nm: "0 < n - m" "n - m ≤ n"
by arith+
with * have "(f ^ m) ⟨\$⟩ a = (f ^ (m + (n - m))) ⟨\$⟩ a"
by simp
then have "(f ^ m) ⟨\$⟩ a = (f ^ m) ⟨\$⟩ ((f ^ (n - m)) ⟨\$⟩ a)"
then have "(f ^ (n - m)) ⟨\$⟩ a = a"
by simp
with ‹n - m > 0›
have "order f a = card ((λm. (f ^ m) ⟨\$⟩ a) ` {0..<n - m})"
by (rule order_witness_unfold)
also have "card ((λm. (f ^ m) ⟨\$⟩ a) ` {0..<n - m}) ≤ card {0..<n - m}"
by (rule card_image_le) simp
finally have "order f a ≤ n - m"
by simp
with prem show False by simp
qed
with hyp show ?case
qed
then show ?thesis by simp
qed

lemma orbit_unfold_image:
"orbit f a = (λn. (f ^ n) ⟨\$⟩ a) ` {..<order f a}" (is "_ = ?A")
proof (rule sym, rule card_subset_eq)
show "finite (orbit f a)"
by simp
show "?A ⊆ orbit f a"
from inj_on_apply_range [of f a]
have "card ?A = order f a"
then show "card ?A = card (orbit f a)"
by simp
qed

lemma in_orbitE:
assumes "b ∈ orbit f a"
obtains n where "b = (f ^ n) ⟨\$⟩ a" and "n < order f a"
using assms unfolding orbit_unfold_image by blast

lemma apply_power_order [simp]:
"(f ^ order f a) ⟨\$⟩ a = a"
proof -
have "(f ^ order f a) ⟨\$⟩ a ∈ orbit f a"
by simp
then obtain n where
*: "(f ^ order f a) ⟨\$⟩ a = (f ^ n) ⟨\$⟩ a"
and "n < order f a"
by (rule in_orbitE)
show ?thesis
proof (cases n)
case 0 with * show ?thesis by simp
next
case (Suc m)
from order_greater_zero [of f a]
have "Suc (order f a - 1) = order f a"
by arith
from Suc ‹n < order f a›
have "m < order f a"
by simp
with Suc *
have "(inverse f) ⟨\$⟩ ((f ^ Suc (order f a - 1)) ⟨\$⟩ a) =
(inverse f) ⟨\$⟩ ((f ^ Suc m) ⟨\$⟩ a)"
by simp
then have "(f ^ (order f a - 1)) ⟨\$⟩ a =
(f ^ m) ⟨\$⟩ a"
by (simp only: power_Suc apply_times)
with inj_on_apply_range
have "order f a - 1 = m"
by (rule inj_onD)
(simp_all add: ‹m < order f a›)
with Suc have "n = order f a"
by auto
with ‹n < order f a›
show ?thesis by simp
qed
qed

lemma apply_power_left_mult_order [simp]:
"(f ^ (n * order f a)) ⟨\$⟩ a = a"

lemma apply_power_right_mult_order [simp]:
"(f ^ (order f a * n)) ⟨\$⟩ a = a"

lemma apply_power_mod_order_eq [simp]:
"(f ^ (n mod order f a)) ⟨\$⟩ a = (f ^ n) ⟨\$⟩ a"
proof -
have "(f ^ n) ⟨\$⟩ a = (f ^ (n mod order f a + order f a * (n div order f a))) ⟨\$⟩ a"
by simp
also have "… = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) ⟨\$⟩ a"
finally show ?thesis
qed

lemma apply_power_eq_iff:
"(f ^ m) ⟨\$⟩ a = (f ^ n) ⟨\$⟩ a ⟷ m mod order f a = n mod order f a" (is "?P ⟷ ?Q")
proof
assume ?Q
then have "(f ^ (m mod order f a)) ⟨\$⟩ a = (f ^ (n mod order f a)) ⟨\$⟩ a"
by simp
then show ?P
by simp
next
assume ?P
then have "(f ^ (m mod order f a)) ⟨\$⟩ a = (f ^ (n mod order f a)) ⟨\$⟩ a"
by simp
with inj_on_apply_range
show ?Q
by (rule inj_onD) simp_all
qed

lemma apply_inverse_eq_apply_power_order_minus_one:
"(inverse f) ⟨\$⟩ a = (f ^ (order f a - 1)) ⟨\$⟩ a"
proof (cases "order f a")
case 0 with order_greater_zero [of f a] show ?thesis
by simp
next
case (Suc n)
moreover have "(f ^ order f a) ⟨\$⟩ a = a"
by simp
then have *: "(inverse f) ⟨\$⟩ ((f ^ order f a) ⟨\$⟩ a) = (inverse f) ⟨\$⟩ a"
by simp
ultimately show ?thesis
by (simp add: apply_sequence mult.assoc [symmetric])
qed

lemma apply_inverse_self_in_orbit [simp]:
"(inverse f) ⟨\$⟩ a ∈ orbit f a"
using apply_inverse_eq_apply_power_order_minus_one [symmetric]
by (rule in_orbitI)

lemma apply_inverse_power_eq:
"(inverse (f ^ n)) ⟨\$⟩ a = (f ^ (order f a - n mod order f a)) ⟨\$⟩ a"
proof (induct n)
case 0 then show ?case by simp
next
case (Suc n)
define m where "m = order f a - n mod order f a - 1"
moreover have "order f a - n mod order f a > 0"
by simp
ultimately have *: "order f a - n mod order f a = Suc m"
by arith
moreover from * have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)"
ultimately show ?case
using Suc
by (simp_all add: apply_times power_Suc2 [of _ n] power_Suc [of _ m] del: power_Suc)
qed

lemma apply_power_eq_self_iff:
"(f ^ n) ⟨\$⟩ a = a ⟷ order f a dvd n"
using apply_power_eq_iff [of f n a 0]

lemma orbit_equiv:
assumes "b ∈ orbit f a"
shows "orbit f b = orbit f a" (is "?B = ?A")
proof
from assms obtain n where "n < order f a" and b: "b = (f ^ n) ⟨\$⟩ a"
by (rule in_orbitE)
then show "?B ⊆ ?A"
from b have "(inverse (f ^ n)) ⟨\$⟩ b = (inverse (f ^ n)) ⟨\$⟩ ((f ^ n) ⟨\$⟩ a)"
by simp
then have a: "a = (inverse (f ^ n)) ⟨\$⟩ b"
then show "?A ⊆ ?B"
unfolding apply_times comp_def apply_inverse_power_eq
apply (rule in_orbitI) apply rule
done
qed

lemma orbit_apply [simp]:
"orbit f (f ⟨\$⟩ a) = orbit f a"
by (rule orbit_equiv) simp

lemma order_apply [simp]:
"order f (f ⟨\$⟩ a) = order f a"
by (simp only: order_def comp_def orbit_apply)

lemma orbit_apply_inverse [simp]:
"orbit f (inverse f ⟨\$⟩ a) = orbit f a"
by (rule orbit_equiv) simp

lemma order_apply_inverse [simp]:
"order f (inverse f ⟨\$⟩ a) = order f a"
by (simp only: order_def comp_def orbit_apply_inverse)

lemma orbit_apply_power [simp]:
"orbit f ((f ^ n) ⟨\$⟩ a) = orbit f a"
by (rule orbit_equiv) simp

lemma order_apply_power [simp]:
"order f ((f ^ n) ⟨\$⟩ a) = order f a"
by (simp only: order_def comp_def orbit_apply_power)

lemma orbit_inverse [simp]:
"orbit (inverse f) = orbit f"
proof (rule ext, rule set_eqI, rule)
fix b a
assume "b ∈ orbit f a"
then obtain n where b: "b = (f ^ n) ⟨\$⟩ a" "n < order f a"
by (rule in_orbitE)
then have "b = apply (inverse (inverse f) ^ n) a"
by simp
then have "b = apply (inverse (inverse f ^ n)) a"
then have "b = apply (inverse f ^ (n * (order (inverse f ^ n) a - 1))) a"
then show "b ∈ orbit (inverse f) a"
by simp
next
fix b a
assume "b ∈ orbit (inverse f) a"
then show "b ∈ orbit f a"
by (rule in_orbitE)
perm_power_inverse power_mult [symmetric])
qed

lemma order_inverse [simp]:
"order (inverse f) = order f"

lemma orbit_disjoint:
assumes "orbit f a ≠ orbit f b"
shows "orbit f a ∩ orbit f b = {}"
proof (rule ccontr)
assume "orbit f a ∩ orbit f b ≠ {}"
then obtain c where "c ∈ orbit f a ∩ orbit f b"
by blast
then have "c ∈ orbit f a" and "c ∈ orbit f b"
by auto
then obtain m n where "c = (f ^ m) ⟨\$⟩ a"
and "c = apply (f ^ n) b" by (blast elim!: in_orbitE)
then have "(f ^ m) ⟨\$⟩ a = apply (f ^ n) b"
by simp
then have "apply (inverse f ^ m) ((f ^ m) ⟨\$⟩ a) =
apply (inverse f ^ m) (apply (f ^ n) b)"
by simp
then have *: "apply (inverse f ^ m * f ^ n) b = a"
have "a ∈ orbit f b"
proof (cases n m rule: linorder_cases)
case equal with * show ?thesis
next
case less
moreover define q where "q = m - n"
ultimately have "m = q + n" by arith
with * have "apply (inverse f ^ q) b = a"
then have "a ∈ orbit (inverse f) b"
by (rule in_orbitI)
then show ?thesis
by simp
next
case greater
moreover define q where "q = n - m"
ultimately have "n = m + q" by arith
with * have "apply (f ^ q) b = a"
then show ?thesis
by (rule in_orbitI)
qed
with assms show False
by (auto dest: orbit_equiv)
qed

subsection ‹Swaps›

lift_definition swap :: "'a ⇒ 'a ⇒ 'a perm"  ("⟨_↔_⟩")
is "λa b. Fun.swap a b id"
proof
fix a b :: 'a
have "{c. Fun.swap a b id c ≠ c} ⊆ {a, b}"
then show "finite {c. Fun.swap a b id c ≠ c}"
by (rule finite_subset) simp
qed simp

lemma apply_swap_simp [simp]:
"⟨a↔b⟩ ⟨\$⟩ a = b"
"⟨a↔b⟩ ⟨\$⟩ b = a"
by (transfer; simp)+

lemma apply_swap_same [simp]:
"c ≠ a ⟹ c ≠ b ⟹ ⟨a↔b⟩ ⟨\$⟩ c = c"
by transfer simp

lemma apply_swap_eq_iff [simp]:
"⟨a↔b⟩ ⟨\$⟩ c = a ⟷ c = b"
"⟨a↔b⟩ ⟨\$⟩ c = b ⟷ c = a"
by (transfer; auto simp add: Fun.swap_def)+

lemma swap_1 [simp]:
"⟨a↔a⟩ = 1"
by transfer simp

lemma swap_sym:
"⟨b↔a⟩ = ⟨a↔b⟩"
by (transfer; auto simp add: Fun.swap_def)+

lemma swap_self [simp]:
"⟨a↔b⟩ * ⟨a↔b⟩ = 1"
by transfer (simp add: Fun.swap_def fun_eq_iff)

lemma affected_swap:
"a ≠ b ⟹ affected ⟨a↔b⟩ = {a, b}"
by transfer (auto simp add: Fun.swap_def)

lemma inverse_swap [simp]:
"inverse ⟨a↔b⟩ = ⟨a↔b⟩"
by transfer (auto intro: inv_equality simp: Fun.swap_def)

subsection ‹Permutations specified by cycles›

fun cycle :: "'a list ⇒ 'a perm"  ("⟨_⟩")
where
"⟨[]⟩ = 1"
| "⟨[a]⟩ = 1"
| "⟨a # b # as⟩ = ⟨a # as⟩ * ⟨a↔b⟩"

text ‹
We do not continue and restrict ourselves to syntax from here.
›

subsection ‹Syntax›

bundle no_permutation_syntax
begin
no_notation swap    ("⟨_↔_⟩")
no_notation cycle   ("⟨_⟩")
no_notation "apply" (infixl "⟨\$⟩" 999)
end

bundle permutation_syntax
begin
notation swap       ("⟨_↔_⟩")
notation cycle      ("⟨_⟩")
notation "apply"    (infixl "⟨\$⟩" 999)
no_notation "apply" ("(⟨\$⟩)")
end

unbundle no_permutation_syntax

end
```