(* 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" ("op ⟨$⟩") 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 add: in_affected [symmetric]) with * have "f ⟨$⟩ a ∉ affected f" by simp then have "f ⟨$⟩ (f ⟨$⟩ a) = f ⟨$⟩ a" by (simp add: in_affected) 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" by (simp add: apply_times) 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}" by (simp add: bij_inv) 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" by (simp add: in_affected) then have "(f ^ n) ⟨$⟩ a = a" for n by (induct n) (simp_all add: apply_times) then show ?Q by (auto simp add: orbit_def) 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)" by (simp add: orbit_def) 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 by (simp add: not_in_affected_iff_orbit_eq_singleton) 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}" by (auto simp add: orbit_def) 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" by (simp add: order_def) 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 by (simp add: not_in_affected_iff_orbit_eq_singleton) next assume ?Q then have "orbit f a = {a}" by (simp add: not_in_affected_iff_orbit_eq_singleton) 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] apply (auto simp add: neq_iff) 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" by (simp add: card_insert) case False then have "order f a = 1" by (simp add: order_eq_one_iff) 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" by (simp add: not_le) with order_greater_zero [of f a] have "order f a = 1" by arith with assms show False by (simp add: order_eq_one_iff) 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" by (auto simp add: orbit_def) 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) (simp_all add: power_add apply_times assms) 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)" by (simp add: power_add apply_times) 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 by (simp add: lessThan_Suc) 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" by (auto simp add: orbit_def) from inj_on_apply_range [of f a] have "card ?A = order f a" by (auto simp add: card_image) 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) (simp add: apply_sequence mult.assoc [symmetric]) 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" by (induct n) (simp_all add: power_add apply_times) lemma apply_power_right_mult_order [simp]: "(f ^ (order f a * n)) ⟨$⟩ a = a" by (simp add: ac_simps) 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" by (simp add: power_add [symmetric]) finally show ?thesis by (simp add: apply_times) 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)" by (auto simp add: mod_Suc) ultimately show ?case using Suc by (simp_all add: apply_times power_Suc2 [of _ n] power_Suc [of _ m] del: power_Suc) (simp add: apply_sequence mult.assoc [symmetric]) 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] by (simp add: mod_eq_0_iff_dvd) 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" by (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE) from b have "(inverse (f ^ n)) ⟨$⟩ b = (inverse (f ^ n)) ⟨$⟩ ((f ^ n) ⟨$⟩ a)" by simp then have a: "a = (inverse (f ^ n)) ⟨$⟩ b" by (simp add: apply_sequence) then show "?A ⊆ ?B" apply (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE) unfolding apply_times comp_def apply_inverse_power_eq unfolding apply_sequence power_add [symmetric] 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" by (simp add: perm_power_inverse) then have "b = apply (inverse f ^ (n * (order (inverse f ^ n) a - 1))) a" by (simp add: apply_inverse_eq_apply_power_order_minus_one power_mult) 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) (simp add: apply_inverse_eq_apply_power_order_minus_one perm_power_inverse power_mult [symmetric]) qed lemma order_inverse [simp]: "order (inverse f) = order f" by (simp add: order_def) 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" by (simp add: apply_sequence perm_power_inverse) have "a ∈ orbit f b" proof (cases n m rule: linorder_cases) case equal with * show ?thesis by (simp add: perm_power_inverse) 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" by (simp add: power_add mult.assoc perm_power_inverse) 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" by (simp add: power_add mult.assoc [symmetric] perm_power_inverse) 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}" by (auto simp add: Fun.swap_def) 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. See also introductory note. › 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" ("op ⟨$⟩") end unbundle no_permutation_syntax end