(* Author: Florian Haftmann, TU Muenchen *)
section \<open>Permutations as abstract type\<close>
theory Perm
imports Main
begin
text \<open>
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 @{text "src/HOL/ex/Perm_Fragments.thy"} for
fragments on that.
\<close>
subsection \<open>Abstract type of permutations\<close>
typedef 'a perm = "{f :: 'a \<Rightarrow> 'a. bij f \<and> finite {a. f a \<noteq> a}}"
morphisms "apply" Perm
proof
show "id \<in> ?perm" by simp
qed
setup_lifting type_definition_perm
notation "apply" (infixl "\<langle>$\<rangle>" 999)
no_notation "apply" ("op \<langle>$\<rangle>")
lemma bij_apply [simp]:
"bij (apply f)"
using "apply" [of f] by simp
lemma perm_eqI:
assumes "\<And>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> a"
shows "f = g"
using assms by transfer (simp add: fun_eq_iff)
lemma perm_eq_iff:
"f = g \<longleftrightarrow> (\<forall>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> a)"
by (auto intro: perm_eqI)
lemma apply_inj:
"f \<langle>$\<rangle> a = f \<langle>$\<rangle> b \<longleftrightarrow> a = b"
by (rule inj_eq) (rule bij_is_inj, simp)
lift_definition affected :: "'a perm \<Rightarrow> 'a set"
is "\<lambda>f. {a. f a \<noteq> a}" .
lemma in_affected:
"a \<in> affected f \<longleftrightarrow> f \<langle>$\<rangle> a \<noteq> a"
by transfer simp
lemma finite_affected [simp]:
"finite (affected f)"
by transfer simp
lemma apply_affected [simp]:
"f \<langle>$\<rangle> a \<in> affected f \<longleftrightarrow> a \<in> affected f"
proof transfer
fix f :: "'a \<Rightarrow> 'a" and a :: 'a
assume "bij f \<and> finite {b. f b \<noteq> b}"
then have "bij f" by simp
interpret bijection f by standard (rule \<open>bij f\<close>)
have "f a \<in> {a. f a = a} \<longleftrightarrow> a \<in> {a. f a = a}" (is "?P \<longleftrightarrow> ?Q")
by auto
then show "f a \<in> {a. f a \<noteq> a} \<longleftrightarrow> a \<in> {a. f a \<noteq> a}"
by simp
qed
lemma card_affected_not_one:
"card (affected f) \<noteq> 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 \<langle>$\<rangle> a \<noteq> a"
by (simp add: in_affected [symmetric])
with * have "f \<langle>$\<rangle> a \<notin> affected f"
by simp
then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
by (simp add: in_affected)
then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)"
by simp
with ** show False by simp
qed
subsection \<open>Identity, composition and inversion\<close>
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 = {} \<longleftrightarrow> f = 1"
by transfer auto
lift_definition times_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm"
is comp
proof
fix f g :: "'a \<Rightarrow> 'a"
assume "bij f \<and> finite {a. f a \<noteq> a}"
"bij g \<and>finite {a. g a \<noteq> a}"
then have "finite ({a. f a \<noteq> a} \<union> {a. g a \<noteq> a})"
by simp
moreover have "{a. (f \<circ> g) a \<noteq> a} \<subseteq> {a. f a \<noteq> a} \<union> {a. g a \<noteq> a}"
by auto
ultimately show "finite {a. (f \<circ> g) a \<noteq> a}"
by (auto intro: finite_subset)
qed (auto intro: bij_comp)
lemma apply_times:
"apply (f * g) = apply f \<circ> apply g"
by (fact times_perm.rep_eq)
lemma apply_sequence:
"f \<langle>$\<rangle> (g \<langle>$\<rangle> a) = apply (f * g) a"
by (simp add: apply_times)
lemma affected_times [simp]:
"affected (f * g) \<subseteq> affected f \<union> affected g"
by transfer auto
lift_definition inverse_perm :: "'a perm \<Rightarrow> 'a perm"
is inv
proof transfer
fix f :: "'a \<Rightarrow> 'a" and a
assume "bij f \<and> finite {b. f b \<noteq> b}"
then have "bij f" and fin: "finite {b. f b \<noteq> b}"
by auto
interpret bijection f by standard (rule \<open>bij f\<close>)
from fin show "bij (inv f) \<and> finite {a. inv f a \<noteq> 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 \<Rightarrow> 'a" and a
assume "bij f \<and> finite {b. f b \<noteq> b}"
then have "bij f" by simp
interpret bijection f by standard (rule \<open>bij f\<close>)
show "{a. inv f a \<noteq> a} = {a. f a \<noteq> 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 \<Rightarrow> 'a" and a
assume "bij f \<and> finite {b. f b \<noteq> b}"
then have "bij f" by simp
interpret bijection f by standard (rule \<open>bij f\<close>)
show "inv f \<circ> f = id"
by simp
qed
qed
declare perm.inverse_distrib_swap [simp]
lemma perm_mult_commute:
assumes "affected f \<inter> affected g = {}"
shows "g * f = f * g"
proof (rule perm_eqI)
fix a
from assms have *: "a \<in> affected f \<Longrightarrow> a \<notin> affected g"
"a \<in> affected g \<Longrightarrow> a \<notin> affected f" for a
by auto
consider "a \<in> affected f \<and> a \<notin> affected g
\<and> f \<langle>$\<rangle> a \<in> affected f"
| "a \<notin> affected f \<and> a \<in> affected g
\<and> f \<langle>$\<rangle> a \<notin> affected f"
| "a \<notin> affected f \<and> a \<notin> affected g"
using assms by auto
then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a"
proof cases
case 1
with * have "f \<langle>$\<rangle> a \<notin> affected g"
by auto
with 1 show ?thesis by (simp add: in_affected apply_times)
next
case 2
with * have "g \<langle>$\<rangle> a \<notin> 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 \<open>Orbit and order of elements\<close>
definition orbit :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a set"
where
"orbit f a = range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)"
lemma in_orbitI:
assumes "(f ^ n) \<langle>$\<rangle> a = b"
shows "b \<in> orbit f a"
using assms by (auto simp add: orbit_def)
lemma apply_power_self_in_orbit [simp]:
"(f ^ n) \<langle>$\<rangle> a \<in> orbit f a"
by (rule in_orbitI) rule
lemma in_orbit_self [simp]:
"a \<in> orbit f a"
using apply_power_self_in_orbit [of _ 0] by simp
lemma apply_self_in_orbit [simp]:
"f \<langle>$\<rangle> a \<in> orbit f a"
using apply_power_self_in_orbit [of _ 1] by simp
lemma orbit_not_empty [simp]:
"orbit f a \<noteq> {}"
using in_orbit_self [of a f] by blast
lemma not_in_affected_iff_orbit_eq_singleton:
"a \<notin> affected f \<longleftrightarrow> orbit f a = {a}" (is "?P \<longleftrightarrow> ?Q")
proof
assume ?P
then have "f \<langle>$\<rangle> a = a"
by (simp add: in_affected)
then have "(f ^ n) \<langle>$\<rangle> 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 \<Rightarrow> 'a \<Rightarrow> nat"
where
"order f = card \<circ> orbit f"
lemma orbit_subset_eq_affected:
assumes "a \<in> affected f"
shows "orbit f a \<subseteq> affected f"
proof (rule ccontr)
assume "\<not> orbit f a \<subseteq> affected f"
then obtain b where "b \<in> orbit f a" and "b \<notin> affected f"
by auto
then have "b \<in> range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)"
by (simp add: orbit_def)
then obtain n where "b = (f ^ n) \<langle>$\<rangle> a"
by blast
with \<open>b \<notin> affected f\<close>
have "(f ^ n) \<langle>$\<rangle> a \<notin> affected f"
by simp
then have "f \<langle>$\<rangle> a \<notin> 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 \<in> 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 \<subseteq> 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 \<longleftrightarrow> a \<notin> affected f" (is "?P \<longleftrightarrow> ?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 \<open>orbit f a = {b}\<close> 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 \<ge> 2 \<longleftrightarrow> a \<in> 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 \<noteq> 1"
shows "order f a \<le> card (affected f)"
proof (cases "a \<in> affected f")
from assms have "affected f \<noteq> {}"
by simp
then obtain B b where "affected f = insert b B"
by blast
with finite_affected [of f] have "card (affected f) \<ge> 1"
by (simp add: card_insert)
case False then have "order f a = 1"
by (simp add: order_eq_one_iff)
with \<open>card (affected f) \<ge> 1\<close> show ?thesis
by simp
next
case True
have "card (orbit f a) \<le> 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 \<in> affected f"
shows "order f a \<ge> 2"
proof (rule ccontr)
assume "\<not> 2 \<le> 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) \<langle>$\<rangle> a = a"
shows "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n})"
proof -
have "orbit f a = (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n}" (is "_ = ?B")
proof (rule set_eqI, rule)
fix b
assume "b \<in> orbit f a"
then obtain m where "(f ^ m) \<langle>$\<rangle> a = b"
by (auto simp add: orbit_def)
then have "b = (f ^ (m mod n + n * (m div n))) \<langle>$\<rangle> a"
by simp
also have "\<dots> = (f ^ (m mod n)) \<langle>$\<rangle> ((f ^ (n * (m div n))) \<langle>$\<rangle> a)"
by (simp only: power_add apply_times) simp
also have "(f ^ (n * q)) \<langle>$\<rangle> a = a" for q
by (induct q)
(simp_all add: power_add apply_times assms)
finally have "b = (f ^ (m mod n)) \<langle>$\<rangle> a" .
moreover from \<open>n > 0\<close>
have "m mod n < n"
by simp
ultimately show "b \<in> ?B"
by auto
next
fix b
assume "b \<in> ?B"
then obtain m where "(f ^ m) \<langle>$\<rangle> a = b"
by blast
then show "b \<in> 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 (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<order f a}"
proof -
have "inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}"
if "n \<le> 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 (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}"
by simp
have "(f ^ n) \<langle>$\<rangle> a \<notin> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}"
proof
assume "(f ^ n) \<langle>$\<rangle> a \<in> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}"
then obtain m where *: "(f ^ m) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a" and "m < n"
by auto
interpret bijection "apply (f ^ m)"
by standard simp
from \<open>m < n\<close> have "n = m + (n - m)"
and nm: "0 < n - m" "n - m \<le> n"
by arith+
with * have "(f ^ m) \<langle>$\<rangle> a = (f ^ (m + (n - m))) \<langle>$\<rangle> a"
by simp
then have "(f ^ m) \<langle>$\<rangle> a = (f ^ m) \<langle>$\<rangle> ((f ^ (n - m)) \<langle>$\<rangle> a)"
by (simp add: power_add apply_times)
then have "(f ^ (n - m)) \<langle>$\<rangle> a = a"
by simp
with \<open>n - m > 0\<close>
have "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m})"
by (rule order_witness_unfold)
also have "card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m}) \<le> card {0..<n - m}"
by (rule card_image_le) simp
finally have "order f a \<le> 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 = (\<lambda>n. (f ^ n) \<langle>$\<rangle> a) ` {..<order f a}" (is "_ = ?A")
proof (rule sym, rule card_subset_eq)
show "finite (orbit f a)"
by simp
show "?A \<subseteq> 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 \<in> orbit f a"
obtains n where "b = (f ^ n) \<langle>$\<rangle> a" and "n < order f a"
using assms unfolding orbit_unfold_image by blast
lemma apply_power_order [simp]:
"(f ^ order f a) \<langle>$\<rangle> a = a"
proof -
have "(f ^ order f a) \<langle>$\<rangle> a \<in> orbit f a"
by simp
then obtain n where
*: "(f ^ order f a) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> 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 \<open>n < order f a\<close>
have "m < order f a"
by simp
with Suc *
have "(inverse f) \<langle>$\<rangle> ((f ^ Suc (order f a - 1)) \<langle>$\<rangle> a) =
(inverse f) \<langle>$\<rangle> ((f ^ Suc m) \<langle>$\<rangle> a)"
by simp
then have "(f ^ (order f a - 1)) \<langle>$\<rangle> a =
(f ^ m) \<langle>$\<rangle> 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: \<open>m < order f a\<close>)
with Suc have "n = order f a"
by auto
with \<open>n < order f a\<close>
show ?thesis by simp
qed
qed
lemma apply_power_left_mult_order [simp]:
"(f ^ (n * order f a)) \<langle>$\<rangle> a = a"
by (induct n) (simp_all add: power_add apply_times)
lemma apply_power_right_mult_order [simp]:
"(f ^ (order f a * n)) \<langle>$\<rangle> a = a"
by (simp add: ac_simps)
lemma apply_power_mod_order_eq [simp]:
"(f ^ (n mod order f a)) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a"
proof -
have "(f ^ n) \<langle>$\<rangle> a = (f ^ (n mod order f a + order f a * (n div order f a))) \<langle>$\<rangle> a"
by simp
also have "\<dots> = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \<langle>$\<rangle> a"
by (simp add: power_add [symmetric])
finally show ?thesis
by (simp add: apply_times)
qed
lemma apply_power_eq_iff:
"(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")
proof
assume ?Q
then have "(f ^ (m mod order f a)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> a"
by simp
then show ?P
by simp
next
assume ?P
then have "(f ^ (m mod order f a)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> 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) \<langle>$\<rangle> a = (f ^ (order f a - 1)) \<langle>$\<rangle> 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) \<langle>$\<rangle> a = a"
by simp
then have *: "(inverse f) \<langle>$\<rangle> ((f ^ order f a) \<langle>$\<rangle> a) = (inverse f) \<langle>$\<rangle> a"
by simp
ultimately show ?thesis
by (simp add: apply_sequence mult.assoc [symmetric])
qed
lemma apply_inverse_self_in_orbit [simp]:
"(inverse f) \<langle>$\<rangle> a \<in> 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)) \<langle>$\<rangle> a = (f ^ (order f a - n mod order f a)) \<langle>$\<rangle> 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) \<langle>$\<rangle> a = a \<longleftrightarrow> 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 \<in> 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) \<langle>$\<rangle> a"
by (rule in_orbitE)
then show "?B \<subseteq> ?A"
by (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE)
from b have "(inverse (f ^ n)) \<langle>$\<rangle> b = (inverse (f ^ n)) \<langle>$\<rangle> ((f ^ n) \<langle>$\<rangle> a)"
by simp
then have a: "a = (inverse (f ^ n)) \<langle>$\<rangle> b"
by (simp add: apply_sequence)
then show "?A \<subseteq> ?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 \<langle>$\<rangle> a) = orbit f a"
by (rule orbit_equiv) simp
lemma order_apply [simp]:
"order f (f \<langle>$\<rangle> a) = order f a"
by (simp only: order_def comp_def orbit_apply)
lemma orbit_apply_inverse [simp]:
"orbit f (inverse f \<langle>$\<rangle> a) = orbit f a"
by (rule orbit_equiv) simp
lemma order_apply_inverse [simp]:
"order f (inverse f \<langle>$\<rangle> a) = order f a"
by (simp only: order_def comp_def orbit_apply_inverse)
lemma orbit_apply_power [simp]:
"orbit f ((f ^ n) \<langle>$\<rangle> a) = orbit f a"
by (rule orbit_equiv) simp
lemma order_apply_power [simp]:
"order f ((f ^ n) \<langle>$\<rangle> 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 \<in> orbit f a"
then obtain n where b: "b = (f ^ n) \<langle>$\<rangle> 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 \<in> orbit (inverse f) a"
by simp
next
fix b a
assume "b \<in> orbit (inverse f) a"
then show "b \<in> 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 \<noteq> orbit f b"
shows "orbit f a \<inter> orbit f b = {}"
proof (rule ccontr)
assume "orbit f a \<inter> orbit f b \<noteq> {}"
then obtain c where "c \<in> orbit f a \<inter> orbit f b"
by blast
then have "c \<in> orbit f a" and "c \<in> orbit f b"
by auto
then obtain m n where "c = (f ^ m) \<langle>$\<rangle> a"
and "c = apply (f ^ n) b" by (blast elim!: in_orbitE)
then have "(f ^ m) \<langle>$\<rangle> a = apply (f ^ n) b"
by simp
then have "apply (inverse f ^ m) ((f ^ m) \<langle>$\<rangle> 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 \<in> 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 \<in> 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 \<open>Swaps\<close>
lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm" ("\<langle>_\<leftrightarrow>_\<rangle>")
is "\<lambda>a b. Fun.swap a b id"
proof
fix a b :: 'a
have "{c. Fun.swap a b id c \<noteq> c} \<subseteq> {a, b}"
by (auto simp add: Fun.swap_def)
then show "finite {c. Fun.swap a b id c \<noteq> c}"
by (rule finite_subset) simp
qed simp
lemma apply_swap_simp [simp]:
"\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> a = b"
"\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> b = a"
by (transfer; simp)+
lemma apply_swap_same [simp]:
"c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = c"
by transfer simp
lemma apply_swap_eq_iff [simp]:
"\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
"\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a"
by (transfer; auto simp add: Fun.swap_def)+
lemma swap_1 [simp]:
"\<langle>a\<leftrightarrow>a\<rangle> = 1"
by transfer simp
lemma swap_sym:
"\<langle>b\<leftrightarrow>a\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
by (transfer; auto simp add: Fun.swap_def)+
lemma swap_self [simp]:
"\<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> = 1"
by transfer (simp add: Fun.swap_def fun_eq_iff)
lemma affected_swap:
"a \<noteq> b \<Longrightarrow> affected \<langle>a\<leftrightarrow>b\<rangle> = {a, b}"
by transfer (auto simp add: Fun.swap_def)
lemma inverse_swap [simp]:
"inverse \<langle>a\<leftrightarrow>b\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
by transfer (auto intro: inv_equality simp: Fun.swap_def)
subsection \<open>Permutations specified by cycles\<close>
fun cycle :: "'a list \<Rightarrow> 'a perm" ("\<langle>_\<rangle>")
where
"\<langle>[]\<rangle> = 1"
| "\<langle>[a]\<rangle> = 1"
| "\<langle>a # b # as\<rangle> = \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
text \<open>
We do not continue and restrict ourselves to syntax from here.
See also introductory note.
\<close>
subsection \<open>Syntax\<close>
bundle no_permutation_syntax
begin
no_notation swap ("\<langle>_\<leftrightarrow>_\<rangle>")
no_notation cycle ("\<langle>_\<rangle>")
no_notation "apply" (infixl "\<langle>$\<rangle>" 999)
end
bundle permutation_syntax
begin
notation swap ("\<langle>_\<leftrightarrow>_\<rangle>")
notation cycle ("\<langle>_\<rangle>")
notation "apply" (infixl "\<langle>$\<rangle>" 999)
no_notation "apply" ("op \<langle>$\<rangle>")
end
unbundle no_permutation_syntax
end