(* Author: Amine Chaieb, University of Cambridge
With various additions by Manuel Eberl
*)
section ‹Permutations, both general
and specifically on finite sets.
›
theory Permutations
imports
"HOL-Library.Multiset"
"HOL-Library.Disjoint_Sets"
Transposition
begin
subsection ‹Auxiliary
›
abbreviation (input) fixpoints ::
‹(
'a \ 'a)
==> 'a set\
where ‹fixpoints f
≡ {x. f x = x}
›
lemma inj_on_fixpoints:
‹inj_on f (fixpoints f)
›
by (rule inj_onI) simp
lemma bij_betw_fixpoints:
‹bij_betw f (fixpoints f) (fixpoints f)
›
using inj_on_fixpoints
by (auto simp add: bij_betw_def)
subsection ‹Basic
definition and consequences
›
definition permutes ::
‹(
'a \ 'a)
==> 'a set \ bool\ (infixr \permutes\ 41)
where ‹p permutes S
⟷ (
∀x. x
∉ S
⟶ p x = x)
∧ (
∀y.
∃!x. p x = y)
›
lemma bij_imp_permutes:
‹p permutes S
› if ‹bij_betw p S S
› and stable:
‹∧x. x
∉ S
==> p x = x
›
proof -
note ‹bij_betw p S S
›
moreover have ‹bij_betw p (- S) (- S)
›
by (auto simp add: stable intro!: bij_betw_imageI inj_onI)
ultimately have ‹bij_betw p (S
∪ - S) (S
∪ - S)
›
by (rule bij_betw_combine) simp
then have ‹∃!x. p x = y
› for y
by (simp add: bij_iff)
with stable
show ?thesis
by (simp add: permutes_def)
qed
lemma inj_imp_permutes:
assumes i:
"inj_on f S" and fin:
"finite S"
and fS:
"\x. x \ S \ f x \ S"
and f:
"\i. i \ S \ f i = i"
shows "f permutes S"
unfolding permutes_def
proof (intro conjI allI impI, rule f)
fix y
from endo_inj_surj[OF fin _ i] fS
have fs:
"f ` S = S" by auto
show "\!x. f x = y"
proof (cases
"y \ S")
case False
thus ?thesis
by (intro ex1I[of _ y], insert fS f) force+
next
case True
with fs
obtain x
where x:
"x \ S" and fx:
"f x = y" by force
show ?thesis
proof (rule ex1I, rule fx)
fix x
'
assume fx
': "f x' = y
"
with True f[of x
'] have "x' ∈ S
" by metis
from inj_onD[OF i fx[folded fx
'] x this]
show "x' = x" by simp
qed
qed
qed
context
fixes p ::
‹'a \ 'a
› and S ::
‹'a set\
assumes perm:
‹p permutes S
›
begin
lemma permutes_inj:
‹inj p
›
using perm
by (auto simp: permutes_def inj_on_def)
lemma permutes_image:
‹p ` S = S
›
proof (rule set_eqI)
fix x
show ‹x
∈ p ` S
⟷ x
∈ S
›
proof
assume ‹x
∈ p ` S
›
then obtain y
where ‹y
∈ S
› ‹p y = x
›
by blast
with perm
show ‹x
∈ S
›
by (cases
‹y = x
›) (auto simp add: permutes_def)
next
assume ‹x
∈ S
›
with perm
obtain y
where ‹y
∈ S
› ‹p y = x
›
by (metis permutes_def)
then show ‹x
∈ p ` S
›
by blast
qed
qed
lemma permutes_not_in:
‹x
∉ S
==> p x = x
›
using perm
by (auto simp: permutes_def)
lemma permutes_image_complement:
‹p ` (- S) = - S
›
by (auto simp add: permutes_not_in)
lemma permutes_in_image:
‹p x
∈ S
⟷ x
∈ S
›
using permutes_image permutes_inj
by (auto dest: inj_image_mem_iff)
lemma permutes_surj:
‹surj p
›
proof -
have ‹p ` (S
∪ - S) = p ` S
∪ p ` (- S)
›
by (rule image_Un)
then show ?thesis
by (simp add: permutes_image permutes_image_complement)
qed
lemma permutes_inv_o:
shows "p \ inv p = id"
and "inv p \ p = id"
using permutes_inj permutes_surj
unfolding inj_iff [symmetric] surj_iff [symmetric]
by auto
lemma permutes_inverses:
shows "p (inv p x) = x"
and "inv p (p x) = x"
using permutes_inv_o [unfolded fun_eq_iff o_def]
by auto
lemma permutes_inv_eq:
‹inv p y = x
⟷ p x = y
›
by (auto simp add: permutes_inverses)
lemma permutes_inj_on:
‹inj_on p A
›
by (rule inj_on_subset [of _ UNIV]) (auto intro: permutes_inj)
lemma permutes_bij:
‹bij p
›
unfolding bij_def
by (metis permutes_inj permutes_surj)
lemma permutes_imp_bij:
‹bij_betw p S S
›
by (simp add: bij_betw_def permutes_image permutes_inj_on)
lemma permutes_subset:
‹p permutes T
› if ‹S
⊆ T
›
proof (rule bij_imp_permutes)
define R
where ‹R = T - S
›
with that
have ‹T = R
∪ S
› ‹R
∩ S = {}
›
by auto
then have ‹p x = x
› if ‹x
∈ R
› for x
using that
by (auto intro: permutes_not_in)
then have ‹p ` R = R
›
by simp
with ‹T = R
∪ S
› show ‹bij_betw p T T
›
by (simp add: bij_betw_def permutes_inj_on image_Un permutes_image)
fix x
assume ‹x
∉ T
›
with ‹T = R
∪ S
› show ‹p x = x
›
by (simp add: permutes_not_in)
qed
lemma permutes_imp_permutes_insert:
‹p permutes insert x S
›
by (rule permutes_subset) auto
end
lemma permutes_id [simp]:
‹id permutes S
›
by (auto intro: bij_imp_permutes)
lemma permutes_empty [simp]:
‹p permutes {}
⟷ p = id
›
proof
assume ‹p permutes {}
›
then show ‹p = id
›
by (auto simp add: fun_eq_iff permutes_not_in)
next
assume ‹p = id
›
then show ‹p permutes {}
›
by simp
qed
lemma permutes_sing [simp]:
‹p permutes {a}
⟷ p = id
›
proof
assume perm:
‹p permutes {a}
›
show ‹p = id
›
proof
fix x
from perm
have ‹p ` {a} = {a}
›
by (rule permutes_image)
with perm
show ‹p x = id x
›
by (cases
‹x = a
›) (auto simp add: permutes_not_in)
qed
next
assume ‹p = id
›
then show ‹p permutes {a}
›
by simp
qed
lemma permutes_univ:
"p permutes UNIV \ (\y. \!x. p x = y)"
by (simp add: permutes_def)
lemma permutes_swap_id:
"a \ S \ b \ S \ transpose a b permutes S"
by (rule bij_imp_permutes) (auto intro: transpose_apply_other)
lemma permutes_altdef:
"p permutes A \ bij_betw p A A \ {x. p x \ x} \ A"
using permutes_not_in[of p A]
by (auto simp: permutes_imp_bij intro!: bij_imp_permutes)
lemma permutes_superset:
‹p permutes T
› if ‹p permutes S
› ‹∧x. x
∈ S - T
==> p x = x
›
proof -
define R U
where ‹R = T
∩ S
› and ‹U = S - T
›
then have ‹T = R
∪ (T - S)
› ‹S = R
∪ U
› ‹R
∩ U = {}
›
by auto
from that
‹U = S - T
› have ‹p ` U = U
›
by simp
from ‹p permutes S
› have ‹bij_betw p (R
∪ U) (R
∪ U)
›
by (simp add: permutes_imp_bij
‹S = R
∪ U
›)
moreover have ‹bij_betw p U U
›
using that
‹U = S - T
› by (simp add: bij_betw_def permutes_inj_on)
ultimately have ‹bij_betw p R R
›
using ‹R
∩ U = {}
› ‹R
∩ U = {}
› by (rule bij_betw_partition)
then have ‹p permutes R
›
proof (rule bij_imp_permutes)
fix x
assume ‹x
∉ R
›
with ‹R = T
∩ S
› ‹p permutes S
› show ‹p x = x
›
by (cases
‹x
∈ S
›) (auto simp add: permutes_not_in that(2))
qed
then have ‹p permutes R
∪ (T - S)
›
by (rule permutes_subset) simp
with ‹T = R
∪ (T - S)
› show ?thesis
by simp
qed
lemma permutes_bij_inv_into:
🍋‹contributor
‹Lukas Bulwahn
››
fixes A ::
"'a set"
and B ::
"'b set"
assumes "p permutes A"
and "bij_betw f A B"
shows "(\x. if x \ B then f (p (inv_into A f x)) else x) permutes B"
proof (rule bij_imp_permutes)
from assms
have "bij_betw p A A" "bij_betw f A B" "bij_betw (inv_into A f) B A"
by (auto simp add: permutes_imp_bij bij_betw_inv_into)
then have "bij_betw (f \ p \ inv_into A f) B B"
by (simp add: bij_betw_trans)
then show "bij_betw (\x. if x \ B then f (p (inv_into A f x)) else x) B B"
by (subst bij_betw_cong[
where g=
"f \ p \ inv_into A f"]) auto
next
fix x
assume "x \ B"
then show "(if x \ B then f (p (inv_into A f x)) else x) = x" by auto
qed
lemma permutes_image_mset:
🍋‹contributor
‹Lukas Bulwahn
››
assumes "p permutes A"
shows "image_mset p (mset_set A) = mset_set A"
using assms
by (metis image_mset_mset_set bij_betw_imp_inj_on permutes_imp_bij permutes
_image)
lemma permutes_implies_image_mset_eq: 🍋‹contributor ‹Lukas Bulwahn››
assumes "p permutes A" "\x. x \ A \ f x = f' (p x)"
shows "image_mset f' (mset_set A) = image_mset f (mset_set A)"
proof -
have "f x = f' (p x)" if "x \# mset_set A" for x
using assms(2)[of x] that by (cases "finite A") auto
with assms have "image_mset f (mset_set A) = image_mset (f' \ p) (mset_set A)"
by (auto intro!: image_mset_cong)
also have "\ = image_mset f' (image_mset p (mset_set A))"
by (simp add: image_mset.compositionality)
also have "\ = image_mset f' (mset_set A)"
proof -
from assms permutes_image_mset have "image_mset p (mset_set A) = mset_set A"
by blast
then show ?thesis by simp
qed
finally show ?thesis ..
qed
subsection ‹Group properties›
lemma permutes_compose: "p permutes S \ q permutes S \ q \ p permutes S"
unfolding permutes_def o_def by metis
lemma permutes_inv:
assumes "p permutes S"
shows "inv p permutes S"
using assms unfolding permutes_def permutes_inv_eq[OF assms] by metis
lemma permutes_inv_inv:
assumes "p permutes S"
shows "inv (inv p) = p"
unfolding fun_eq_iff permutes_inv_eq[OF assms] permutes_inv_eq[OF permutes_inv[OF assms]]
by blast
lemma permutes_invI:
assumes perm: "p permutes S"
and inv: "\x. x \ S \ p' (p x) = x"
and outside: "\x. x \ S \ p' x = x"
shows "inv p = p'"
proof
show "inv p x = p' x" for x
proof (cases "x \ S")
case True
from assms have "p' x = p' (p (inv p x))"
by (simp add: permutes_inverses)
also from permutes_inv[OF perm] True have "\ = inv p x"
by (subst inv) (simp_all add: permutes_in_image)
finally show ?thesis ..
next
case False
with permutes_inv[OF perm] show ?thesis
by (simp_all add: outside permutes_not_in)
qed
qed
lemma permutes_vimage: "f permutes A \ f -` A = A"
by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv])
subsection ‹Restricting a permutation to a subset›
definition restrict_id :: "('a \ 'a) \ 'a set \ 'a \ 'a"
where "restrict_id f A = (\x. if x \ A then f x else x)"
lemma restrict_id_cong [cong]:
assumes "\x. x \ A \ f x = g x" "A = B"
shows "restrict_id f A = restrict_id g B"
using assms unfolding restrict_id_def by auto
lemma restrict_id_cong':
assumes "x \ A \ f x = g x" "A = B"
shows "restrict_id f A x = restrict_id g B x"
using assms unfolding restrict_id_def by auto
lemma restrict_id_simps [simp]:
"x \ A \ restrict_id f A x = f x"
"x \ A \ restrict_id f A x = x"
by (auto simp: restrict_id_def)
lemma bij_betw_restrict_id:
assumes "bij_betw f A A" "A \ B"
shows "bij_betw (restrict_id f A) B B"
proof -
have "bij_betw (restrict_id f A) (A \ (B - A)) (A \ (B - A))"
unfolding restrict_id_def
by (rule bij_betw_disjoint_Un) (use assms in ‹auto intro: bij_betwI›)
also have "A \ (B - A) = B"
using assms(2) by blast
finally show ?thesis .
qed
lemma permutes_restrict_id:
assumes "bij_betw f A A"
shows "restrict_id f A permutes A"
by (intro bij_imp_permutes bij_betw_restrict_id assms) auto
subsection ‹Mapping a permutation›
definition map_permutation :: "'a set \ ('a \ 'b) \ ('a \ 'a) \ 'b \ 'b" where
"map_permutation A f p = restrict_id (f \ p \ inv_into A f) (f ` A)"
lemma map_permutation_cong_strong:
assumes "A = B" "\x. x \ A \ f x = g x" "\x. x \ A \ p x = q x"
assumes "p ` A \ A" "inj_on f A"
shows "map_permutation A f p = map_permutation B g q"
proof -
have fg: "f x = g y" if "x \ A" "x = y" for x y
using assms(2) that by simp
have pq: "p x = q y" if "x \ A" "x = y" for x y
using assms(3) that by simp
have p: "p x \ A" if "x \ A" for x
using assms(4) that by blast
have inv: "inv_into A f x = inv_into B g y" if "x \ f ` A" "x = y" for x y
proof -
from that obtain u where u: "u \ A" "x = f u"
by blast
have "inv_into A f (f u) = inv_into A g (f u)"
using ‹inj_on f A› u(1) by (metis assms(2) inj_on_cong inv_into_f_f)
thus ?thesis
using u ‹x = y› ‹A = B› by simp
qed
show ?thesis
unfolding map_permutation_def o_def
by (intro restrict_id_cong image_cong fg pq inv_into_into p inv) (auto simp: ‹A = B›)
qed
lemma map_permutation_cong:
assumes "inj_on f A" "p permutes A"
assumes "A = B" "\x. x \ A \ f x = g x" "\x. x \ A \ p x = q x"
shows "map_permutation A f p = map_permutation B g q"
proof (intro map_permutation_cong_strong assms)
show "p ` A \ A"
using ‹p permutes A› by (simp add: permutes_image)
qed auto
lemma inv_into_id [simp]: "x \ A \ inv_into A id x = x"
by (metis f_inv_into_f id_apply image_eqI)
lemma inv_into_ident [simp]: "x \ A \ inv_into A (\x. x) x = x"
by (metis f_inv_into_f image_eqI)
lemma map_permutation_id [simp]: "p permutes A \ map_permutation A id p = p"
by (auto simp: fun_eq_iff map_permutation_def restrict_id_def permutes_not_in)
lemma map_permutation_ident [simp]: "p permutes A \ map_permutation A (\x. x) p = p"
by (auto simp: fun_eq_iff map_permutation_def restrict_id_def permutes_not_in)
lemma map_permutation_id': "inj_on f A \ map_permutation A f id = id"
unfolding map_permutation_def by (auto simp: restrict_id_def fun_eq_iff)
lemma map_permutation_ident': "inj_on f A \ map_permutation A f (\x. x) = (\x. x)"
unfolding map_permutation_def by (auto simp: restrict_id_def fun_eq_iff)
lemma map_permutation_permutes:
assumes "bij_betw f A B" "p permutes A"
shows "map_permutation A f p permutes B"
proof (rule bij_imp_permutes)
have f_A: "f ` A = B"
using assms(1) by (auto simp: bij_betw_def)
from assms(2) have "bij_betw p A A"
by (simp add: permutes_imp_bij)
show "bij_betw (map_permutation A f p) B B"
unfolding map_permutation_def f_A
by (rule bij_betw_restrict_id bij_betw_trans bij_betw_inv_into assms(1)
permutes_imp_bij[OF assms(2)] order.refl)+
show "map_permutation A f p x = x" if "x \ B" for x
using that unfolding map_permutation_def f_A by simp
qed
lemma map_permutation_compose:
fixes f :: "'a \ 'b" and g :: "'b \ 'c"
assumes "bij_betw f A B" "inj_on g B"
shows "map_permutation B g (map_permutation A f p) = map_permutation A (g \ f) p"
proof
fix c :: 'c
have bij_g: "bij_betw g B (g ` B)"
using ‹inj_on g B› unfolding bij_betw_def by blast
have [simp]: "f x = f y \ x = y" if "x \ A" "y \ A" for x y
using assms(1) that by (auto simp: bij_betw_def inj_on_def)
have [simp]: "g x = g y \ x = y" if "x \ B" "y \ B" for x y
using assms(2) that by (auto simp: bij_betw_def inj_on_def)
show "map_permutation B g (map_permutation A f p) c = map_permutation A (g \ f) p c"
proof (cases "c \ g ` B")
case c: True
then obtain a where a: "a \ A" "c = g (f a)"
using assms(1,2) unfolding bij_betw_def by auto
have "map_permutation B g (map_permutation A f p) c = g (f (p a))"
using a assms by (auto simp: map_permutation_def restrict_id_def bij_betw_def)
also have "\ = map_permutation A (g \ f) p c"
using a bij_betw_inv_into_left[OF bij_betw_trans[OF assms(1) bij_g]]
by (auto simp: map_permutation_def restrict_id_def bij_betw_def)
finally show ?thesis .
next
case c: False
thus ?thesis using assms
by (auto simp: map_permutation_def bij_betw_def restrict_id_def)
qed
qed
lemma map_permutation_compose_inv:
assumes "bij_betw f A B" "p permutes A" "\x. x \ A \ g (f x) = x"
shows "map_permutation B g (map_permutation A f p) = p"
proof -
have "inj_on g B"
proof
fix x y assume "x \ B" "y \ B" "g x = g y"
then obtain x' y' where *: "x' \ A" "y' : A" "x = f x'" "y = f y'"
using assms(1) unfolding bij_betw_def by blast
thus "x = y"
using assms(3)[of x'] assms(3)[of y'] ‹g x = g y› by simp
qed
have "map_permutation B g (map_permutation A f p) = map_permutation A (g \ f) p"
by (rule map_permutation_compose) (use assms ‹inj_on g B› in auto)
also have "\ = map_permutation A id p"
by (intro map_permutation_cong assms comp_inj_on)
(use ‹inj_on g B› assms(1,3) in ‹auto simp: bij_betw_def›)
also have "\ = p"
by (rule map_permutation_id) fact
finally show ?thesis .
qed
lemma map_permutation_apply:
assumes "inj_on f A" "x \ A"
shows "map_permutation A f h (f x) = f (h x)"
using assms by (auto simp: map_permutation_def inj_on_def)
lemma map_permutation_compose':
fixes f :: "'a \ 'b"
assumes "inj_on f A" "q permutes A"
shows "map_permutation A f (p \ q) = map_permutation A f p \ map_permutation A f q"
proof
fix y :: 'b
show "map_permutation A f (p \ q) y = (map_permutation A f p \ map_permutation A f q) y"
proof (cases "y \ f ` A")
case True
then obtain x where x: "x \ A" "y = f x"
by blast
have "map_permutation A f (p \ q) y = f (p (q x))"
unfolding x(2) by (subst map_permutation_apply) (use assms x in auto)
also have "\ = (map_permutation A f p \ map_permutation A f q) y"
unfolding x o_apply using x(1) assms
by (simp add: map_permutation_apply permutes_in_image)
finally show ?thesis .
next
case False
thus ?thesis
using False by (simp add: map_permutation_def)
qed
qed
lemma map_permutation_transpose:
assumes "inj_on f A" "a \ A" "b \ A"
shows "map_permutation A f (Transposition.transpose a b) = Transposition.transpose (f a) (f b)"
proof
fix y :: 'b
show "map_permutation A f (Transposition.transpose a b) y = Transposition.transpose (f a) (f b) y"
proof (cases "y \ f ` A")
case False
hence "map_permutation A f (Transposition.transpose a b) y = y"
unfolding map_permutation_def by (intro restrict_id_simps)
moreover have "Transposition.transpose (f a) (f b) y = y"
using False assms by (intro transpose_apply_other) auto
ultimately show ?thesis
by simp
next
case True
then obtain x where x: "x \ A" "y = f x"
by blast
have "map_permutation A f (Transposition.transpose a b) y =
f (Transposition.transpose a b x)"
unfolding x by (subst map_permutation_apply) (use x assms in auto)
also have "\ = Transposition.transpose (f a) (f b) y"
using assms(2,3) x
by (auto simp: Transposition.transpose_def inj_on_eq_iff[OF assms(1)])
finally show ?thesis .
qed
qed
lemma map_permutation_permutes_iff:
assumes "bij_betw f A B" "p ` A \ A" "\x. x \ A \ p x = x"
shows "map_permutation A f p permutes B \ p permutes A"
proof
assume "p permutes A"
thus "map_permutation A f p permutes B"
by (intro map_permutation_permutes assms)
next
assume *: "map_permutation A f p permutes B"
hence "map_permutation B (inv_into A f) (map_permutation A f p) permutes A"
by (rule map_permutation_permutes[OF bij_betw_inv_into[OF assms(1)]])
also have "map_permutation B (inv_into A f) (map_permutation A f p) =
map_permutation A (inv_into A f ∘ f) p"
by (rule map_permutation_compose[OF _ inj_on_inv_into])
(use assms in ‹auto simp: bij_betw_def›)
also have "\ = map_permutation A id p"
unfolding o_def id_def
by (rule sym, intro map_permutation_cong_strong inv_into_f_f[symmetric]
assms(2) bij_betw_imp_inj_on[OF assms(1)]) auto
also have "\ = p"
unfolding map_permutation_def using assms(3)
by (auto simp: restrict_id_def fun_eq_iff split: if_splits)
finally show "p permutes A" .
qed
lemma bij_betw_permutations:
assumes "bij_betw f A B"
shows "bij_betw (\\ x. if x \ B then f (\ (inv_into A f x)) else x)
{π. π permutes A} {π. π permutes B}" (is "bij_betw ?f _ _")
proof -
let ?g = "(\\ x. if x \ A then inv_into A f (\ (f x)) else x)"
show ?thesis
proof (rule bij_betw_byWitness [of _ ?g], goal_cases)
case 3
show ?case using permutes_bij_inv_into[OF _ assms] by auto
next
case 4
have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms)
{
fix π assume "\ permutes B"
from permutes_bij_inv_into[OF this bij_inv] and assms
have "(\x. if x \ A then inv_into A f (\ (f x)) else x) permutes A"
by (simp add: inv_into_inv_into_eq cong: if_cong)
}
from this show ?case by (auto simp: permutes_inv)
next
case 1
thus ?case using assms
by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left
dest: bij_betwE)
next
case 2
moreover have "bij_betw (inv_into A f) B A"
by (intro bij_betw_inv_into assms)
ultimately show ?case using assms
by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right
dest: bij_betwE)
qed
qed
lemma bij_betw_derangements:
assumes "bij_betw f A B"
shows "bij_betw (\\ x. if x \ B then f (\ (inv_into A f x)) else x)
{π. π permutes A ∧ (∀x∈A. π x ≠ x)} {π. π permutes B ∧ (∀x∈B. π x ≠ x)}"
(is "bij_betw ?f _ _")
proof -
let ?g = "(\\ x. if x \ A then inv_into A f (\ (f x)) else x)"
show ?thesis
proof (rule bij_betw_byWitness [of _ ?g], goal_cases)
case 3
have "?f \ x \ x" if "\ permutes A" "\x. x \ A \ \ x \ x" "x \ B" for π x
using that and assms by (metis bij_betwE bij_betw_imp_inj_on bij_betw_imp_surj_on
inv_into_f_f inv_into_into permutes_imp_bij)
with permutes_bij_inv_into[OF _ assms] show ?case by auto
next
case 4
have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms)
have "?g \ permutes A" if "\ permutes B" for π
using permutes_bij_inv_into[OF that bij_inv] and assms
by (simp add: inv_into_inv_into_eq cong: if_cong)
moreover have "?g \ x \ x" if "\ permutes B" "\x. x \ B \ \ x \ x" "x \ A" for π x
using that and assms by (metis bij_betwE bij_betw_imp_surj_on f_inv_into_f permutes_imp_bij)
ultimately show ?case by auto
next
case 1
thus ?case using assms
by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left
dest: bij_betwE)
next
case 2
moreover have "bij_betw (inv_into A f) B A"
by (intro bij_betw_inv_into assms)
ultimately show ?case using assms
by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right
dest: bij_betwE)
qed
qed
subsection ‹The number of permutations on a finite set›
lemma permutes_insert_lemma:
assumes "p permutes (insert a S)"
shows "transpose a (p a) \ p permutes S"
proof (rule permutes_superset[where S = "insert a S"])
show "Transposition.transpose a (p a) \ p permutes insert a S"
by (meson assms insertI1 permutes_compose permutes_in_image permutes_swap_id)
qed auto
lemma permutes_insert: "{p. p permutes (insert a S)} =
(λ(b, p). transpose a b ∘ p) ` {(b, p). b ∈ insert a S ∧ p ∈ {p. p permutes S}}"
proof -
have "p permutes insert a S \
(∃b q. p = transpose a b ∘ q ∧ b ∈ insert a S ∧ q permutes S)" for p
proof -
have "\b q. p = transpose a b \ q \ b \ insert a S \ q permutes S"
if p: "p permutes insert a S"
proof -
let ?b = "p a"
let ?q = "transpose a (p a) \ p"
have *: "p = transpose a ?b \ ?q"
by (simp add: fun_eq_iff o_assoc)
have **: "?b \ insert a S"
unfolding permutes_in_image[OF p] by simp
from permutes_insert_lemma[OF p] * ** show ?thesis
by blast
qed
moreover have "p permutes insert a S"
if bq: "p = transpose a b \ q" "b \ insert a S" "q permutes S" for b q
proof -
from permutes_subset[OF bq(3), of "insert a S"] have q: "q permutes insert a S"
by auto
have a: "a \ insert a S"
by simp
from bq(1) permutes_compose[OF q permutes_swap_id[OF a bq(2)]] show ?thesis
by simp
qed
ultimately show ?thesis by blast
qed
then show ?thesis by auto
qed
lemma card_permutations:
assumes "card S = n"
and "finite S"
shows "card {p. p permutes S} = fact n"
using assms(2,1)
proof (induct arbitrary: n)
case empty
then show ?case by simp
next
case (insert x F)
{
fix n
assume card_insert: "card (insert x F) = n"
let ?xF = "{p. p permutes insert x F}"
let ?pF = "{p. p permutes F}"
let ?pF' = "{(b, p). b \ insert x F \ p \ ?pF}"
let ?g = "(\(b, p). transpose x b \ p)"
have xfgpF': "?xF = ?g ` ?pF'"
by (rule permutes_insert[of x F])
from ‹x ∉ F› ‹finite F› card_insert have Fs: "card F = n - 1"
by auto
from ‹finite F› insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
by auto
then have "finite ?pF"
by (auto intro: card_ge_0_finite)
with ‹finite F› card.insert_remove have pF'f: "finite ?pF'"
by simp
have ginj: "inj_on ?g ?pF'"
proof -
{
fix b p c q
assume bp: "(b, p) \ ?pF'"
assume cq: "(c, q) \ ?pF'"
assume eq: "?g (b, p) = ?g (c, q)"
from bp cq have pF: "p permutes F" and qF: "q permutes F"
by auto
from pF ‹x ∉ F› eq have "b = ?g (b, p) x"
by (auto simp: permutes_def fun_upd_def fun_eq_iff)
also from qF ‹x ∉ F› eq have "\ = ?g (c, q) x"
by (auto simp: fun_upd_def fun_eq_iff)
also from qF ‹x ∉ F› have "\ = c"
by (auto simp: permutes_def fun_upd_def fun_eq_iff)
finally have "b = c" .
then have "transpose x b = transpose x c"
by simp
with eq have "transpose x b \ p = transpose x b \ q"
by simp
then have "transpose x b \ (transpose x b \ p) = transpose x b \ (transpose x b \ q)"
by simp
then have "p = q"
by (simp add: o_assoc)
with ‹b = c› have "(b, p) = (c, q)"
by simp
}
then show ?thesis
unfolding inj_on_def by blast
qed
from ‹x ∉ F› ‹finite F› card_insert have "n \ 0"
by auto
then have "\m. n = Suc m"
by presburger
then obtain m where n: "n = Suc m"
by blast
from pFs card_insert have *: "card ?xF = fact n"
unfolding xfgpF' card_image[OF ginj]
using ‹finite F› ‹finite ?pF›
by (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product) (simp add: n)
from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"
by (simp add: xfgpF' n)
from * have "card ?xF = fact n"
unfolding xFf by blast
}
with insert show ?case by simp
qed
lemma finite_permutations:
assumes "finite S"
shows "finite {p. p permutes S}"
using card_permutations[OF refl assms] by (auto intro: card_ge_0_finite)
lemma permutes_doubleton_iff: "f permutes {a, b} \ f = id \ f = Transposition.transpose a b"
proof (cases "a = b")
case False
have "{id, Transposition.transpose a b} \ {f. f permutes {a, b}}"
by (auto simp: permutes_id permutes_swap_id)
moreover have "id \ Transposition.transpose a b"
using False by (auto simp: fun_eq_iff Transposition.transpose_def)
hence "card {id, Transposition.transpose a b} = card {f. f permutes {a, b}}"
using False by (simp add: card_permutations)
ultimately have "{id, Transposition.transpose a b} = {f. f permutes {a, b}}"
by (intro card_subset_eq finite_permutations) auto
thus ?thesis by auto
qed auto
subsection ‹Permutations of index set for iterated operations›
lemma (in comm_monoid_set) permute:
assumes "p permutes S"
shows "F g S = F (g \ p) S"
proof -
from ‹p permutes S› have "inj p"
by (rule permutes_inj)
then have "inj_on p S"
by (auto intro: inj_on_subset)
then have "F g (p ` S) = F (g \ p) S"
by (rule reindex)
moreover from ‹p permutes S› have "p ` S = S"
by (rule permutes_image)
ultimately show ?thesis
by simp
qed
subsection ‹Permutations as transposition sequences›
inductive swapidseq :: "nat \ ('a \ 'a) \ bool"
where
id[simp]: "swapidseq 0 id"
| comp_Suc: "swapidseq n p \ a \ b \ swapidseq (Suc n) (transpose a b \ p)"
declare id[unfolded id_def, simp]
definition "permutation p \ (\n. swapidseq n p)"
subsection ‹Some closure properties of the set of permutations, with lengths›
lemma permutation_id[simp]: "permutation id"
unfolding permutation_def by (rule exI[where x=0]) simp
declare permutation_id[unfolded id_def, simp]
lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (transpose a b)"
using swapidseq.simps by fastforce
lemma permutation_swap_id: "permutation (transpose a b)"
by (meson permutation_def swapidseq_swap)
lemma swapidseq_comp_add: "swapidseq n p \ swapidseq m q \ swapidseq (n + m) (p \ q)"
proof (induct n p arbitrary: m q rule: swapidseq.induct)
case (id m q)
then show ?case by simp
next
case (comp_Suc n p a b m q)
then show ?case
by (metis add_Suc comp_assoc swapidseq.comp_Suc)
qed
lemma permutation_compose: "permutation p \ permutation q \ permutation (p \ q)"
unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
lemma swapidseq_endswap: "swapidseq n p \ a \ b \ swapidseq (Suc n) (p \ transpose a b)"
by (induct n p rule: swapidseq.induct)
(use swapidseq_swap[of a b] in ‹auto simp add: comp_assoc intro: swapidseq.comp_Suc›)
lemma swapidseq_inverse_exists: "swapidseq n p \ \q. swapidseq n q \ p \ q = id \ q \ p = id"
proof (induct n p rule: swapidseq.induct)
case id
then show ?case
by (rule exI[where x=id]) simp
next
case (comp_Suc n p a b)
from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id"
by blast
let ?q = "q \ transpose a b"
note H = comp_Suc.hyps
from swapidseq_swap[of a b] H(3) have *: "swapidseq 1 (transpose a b)"
by simp
from swapidseq_comp_add[OF q(1) *] have **: "swapidseq (Suc n) ?q"
by simp
have "transpose a b \ p \ ?q = transpose a b \ (p \ q) \ transpose a b"
by (simp add: o_assoc)
also have "\ = id"
by (simp add: q(2))
finally have ***: "transpose a b \ p \ ?q = id" .
have "?q \ (transpose a b \ p) = q \ (transpose a b \ transpose a b) \ p"
by (simp only: o_assoc)
then have "?q \ (transpose a b \ p) = id"
by (simp add: q(3))
with ** *** show ?case
by blast
qed
lemma swapidseq_inverse:
assumes "swapidseq n p"
shows "swapidseq n (inv p)"
using swapidseq_inverse_exists[OF assms] inv_unique_comp[of p] by auto
lemma permutation_inverse: "permutation p \ permutation (inv p)"
using permutation_def swapidseq_inverse by blast
subsection ‹Various combinations of transpositions with 2, 1 and 0 common elements›
lemma swap_id_common:" a \ c \ b \ c \
transpose a b ∘ transpose a c = transpose b c ∘ transpose a b"
by (simp add: fun_eq_iff transpose_def)
lemma swap_id_common': "a \ b \ a \ c \
transpose a c ∘ transpose b c = transpose b c ∘ transpose a b"
by (simp add: fun_eq_iff transpose_def)
lemma swap_id_independent: "a \ c \ a \ d \ b \ c \ b \ d \
transpose a b ∘ transpose c d = transpose c d ∘ transpose a b"
by (simp add: fun_eq_iff transpose_def)
subsection ‹The identity map only has even transposition sequences›
lemma symmetry_lemma:
assumes "\a b c d. P a b c d \ P a b d c"
and "\a b c d. a \ b \ c \ d \
a = c ∧ b = d ∨ a = c ∧ b ≠ d ∨ a ≠ c ∧ b = d ∨ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ==>
P a b c d"
shows "\a b c d. a \ b \ c \ d \ P a b c d"
using assms by metis
lemma swap_general:
assumes "a \ b" "c \ d"
shows "transpose a b \ transpose c d = id \
(∃x y z. x ≠ a ∧ y ≠ a ∧ z ≠ a ∧ x ≠ y ∧
transpose a b ∘ transpose c d = transpose x y ∘ transpose a z)"
by (metis assms swap_id_common' swap_id_independent transpose_commute transpose_comp_involutory)
lemma swapidseq_id_iff[simp]: "swapidseq 0 p \ p = id"
using swapidseq.cases[of 0 p "p = id"] by auto
lemma swapidseq_cases: "swapidseq n p \
n = 0 ∧ p = id ∨ (∃a b q m. n = Suc m ∧ p = transpose a b ∘ q ∧ swapidseq m q ∧ a ≠ b)"
by (meson comp_Suc id swapidseq.cases)
lemma fixing_swapidseq_decrease:
assumes "swapidseq n p"
and "a \ b"
and "(transpose a b \ p) a = a"
shows "n \ 0 \ swapidseq (n - 1) (transpose a b \ p)"
using assms
proof (induct n arbitrary: p a b)
case 0
then show ?case
by (auto simp add: fun_upd_def)
next
case (Suc n p a b)
from Suc.prems(1) swapidseq_cases[of "Suc n" p]
obtain c d q m where
cdqm: "Suc n = Suc m" "p = transpose c d \ q" "swapidseq m q" "c \ d" "n = m"
by auto
consider "transpose a b \ transpose c d = id"
| x y z where "x \ a" "y \ a" "z \ a" "x \ y"
"transpose a b \ transpose c d = transpose x y \ transpose a z"
using swap_general[OF Suc.prems(2) cdqm(4)] by metis
then show ?case
proof cases
case 1
then show ?thesis
by (simp only: cdqm o_assoc) (simp add: cdqm)
next
case 2
then have az: "a \ z"
by simp
from 2 have *: "(transpose x y \ h) a = a \ h a = a" for h
by (simp add: transpose_def)
from cdqm(2) have "transpose a b \ p = transpose a b \ (transpose c d \ q)"
by simp
then have 🍋: "transpose a b \ p = transpose x y \ (transpose a z \ q)"
by (simp add: o_assoc 2)
obtain **: "swapidseq (n - 1) (transpose a z \ q)" and "n\0"
by (metis "*" "\ Suc.hyps Suc.prems(3) az cdqm(3,5))
then have "Suc n - 1 = Suc (n - 1)"
by auto
with 2 show ?thesis
using "**" 🍋 swapidseq.simps by blast
qed
qed
lemma swapidseq_identity_even:
assumes "swapidseq n (id :: 'a \ 'a)"
shows "even n"
using ‹swapidseq n id›
proof (induct n rule: nat_less_induct)
case H: (1 n)
consider "n = 0"
| a b :: 'a and q m where "n = Suc m" "id = transpose a b \ q" "swapidseq m q" "a \ b"
using H(2)[unfolded swapidseq_cases[of n id]] by auto
then show ?case
proof cases
case 1
then show ?thesis by presburger
next
case h: 2
from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]]
have m: "m \ 0" "swapidseq (m - 1) (id :: 'a \ 'a)"
by auto
from h m have mn: "m - 1 < n"
by arith
from H(1)[rule_format, OF mn m(2)] h(1) m(1) show ?thesis
by presburger
qed
qed
subsection ‹Therefore we have a welldefined notion of parity›
definition "evenperm p = even (SOME n. swapidseq n p)"
lemma swapidseq_even_even:
assumes m: "swapidseq m p"
and n: "swapidseq n p"
shows "even m \ even n"
proof -
from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id"
by blast
from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]] show ?thesis
by arith
qed
lemma evenperm_unique:
assumes "swapidseq n p" and"even n = b"
shows "evenperm p = b"
by (metis evenperm_def assms someI swapidseq_even_even)
subsection ‹And it has the expected composition properties›
lemma evenperm_id[simp]: "evenperm id = True"
by (rule evenperm_unique[where n = 0]) simp_all
lemma evenperm_identity [simp]:
‹evenperm (λx. x)›
using evenperm_id by (simp add: id_def [abs_def])
lemma evenperm_swap: "evenperm (transpose a b) = (a = b)"
by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap)
lemma evenperm_comp:
assumes "permutation p" "permutation q"
shows "evenperm (p \ q) \ evenperm p = evenperm q"
proof -
from assms obtain n m where n: "swapidseq n p" and m: "swapidseq m q"
unfolding permutation_def by blast
have "even (n + m) \ (even n \ even m)"
by arith
from evenperm_unique[OF n refl] evenperm_unique[OF m refl]
and evenperm_unique[OF swapidseq_comp_add[OF n m] this] show ?thesis
by blast
qed
lemma evenperm_inv:
assumes "permutation p"
shows "evenperm (inv p) = evenperm p"
proof -
from assms obtain n where n: "swapidseq n p"
unfolding permutation_def by blast
show ?thesis
by (rule evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]])
qed
subsection ‹A more abstract characterization of permutations›
lemma permutation_bijective:
assumes "permutation p"
shows "bij p"
by (meson assms o_bij permutation_def swapidseq_inverse_exists)
lemma permutation_finite_support:
assumes "permutation p"
shows "finite {x. p x \ x}"
proof -
from assms obtain n where "swapidseq n p"
unfolding permutation_def by blast
then show ?thesis
proof (induct n p rule: swapidseq.induct)
case id
then show ?case by simp
next
case (comp_Suc n p a b)
let ?S = "insert a (insert b {x. p x \ x})"
from comp_Suc.hyps(2) have *: "finite ?S"
by simp
from ‹a ≠ b› have **: "{x. (transpose a b \ p) x \ x} \ ?S"
by auto
show ?case
by (rule finite_subset[OF ** *])
qed
qed
lemma permutation_lemma:
assumes "finite S"
and "bij p"
and "\x. x \ S \ p x = x"
shows "permutation p"
using assms
proof (induct S arbitrary: p rule: finite_induct)
case empty
then show ?case
by simp
next
case (insert a F p)
let ?r = "transpose a (p a) \ p"
let ?q = "transpose a (p a) \ ?r"
have *: "?r a = a"
by simp
from insert * have **: "\x. x \ F \ ?r x = x"
by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3))
have "bij ?r"
using insert by (simp add: bij_comp)
have "permutation ?r"
by (rule insert(3)[OF ‹bij ?r› **])
then have "permutation ?q"
by (simp add: permutation_compose permutation_swap_id)
then show ?case
by (simp add: o_assoc)
qed
lemma permutation: "permutation p \ bij p \ finite {x. p x \ x}"
using permutation_bijective permutation_finite_support permutation_lemma by auto
lemma permutation_inverse_works:
assumes "permutation p"
shows "inv p \ p = id"
and "p \ inv p = id"
using permutation_bijective [OF assms] by (auto simp: bij_def inj_iff surj_iff)
lemma permutation_inverse_compose:
assumes p: "permutation p"
and q: "permutation q"
shows "inv (p \ q) = inv q \ inv p"
by (simp add: o_inv_distrib p permutation_bijective q)
subsection ‹Relation to ‹permutes››
lemma permutes_imp_permutation:
‹permutation p› if ‹finite S› ‹p permutes S›
proof -
from ‹p permutes S› have ‹{x. p x ≠ x} ⊆ S›
by (auto dest: permutes_not_in)
then have ‹finite {x. p x ≠ x}›
using ‹finite S› by (rule finite_subset)
moreover from ‹p permutes S› have ‹bij p›
by (auto dest: permutes_bij)
ultimately show ?thesis
by (simp add: permutation)
qed
lemma permutation_permutesE:
assumes ‹permutation p›
obtains S where ‹finite S› ‹p permutes S›
proof -
from assms have fin: ‹finite {x. p x ≠ x}›
by (simp add: permutation)
from assms have ‹bij p›
by (simp add: permutation)
also have ‹UNIV = {x. p x ≠ x} ∪ {x. p x = x}›
by auto
finally have ‹bij_betw p {x. p x ≠ x} {x. p x ≠ x}›
by (rule bij_betw_partition) (auto simp add: bij_betw_fixpoints)
then have ‹p permutes {x. p x ≠ x}›
by (auto intro: bij_imp_permutes)
with fin show thesis ..
qed
lemma permutation_permutes: "permutation p \ (\S. finite S \ p permutes S)"
by (auto elim: permutation_permutesE intro: permutes_imp_permutation)
subsection ‹Sign of a permutation›
definition sign :: ‹('a \ 'a) ==> int› 🍋 ‹TODO: prefer less generic name›
where ‹sign p = (if evenperm p then 1 else - 1)›
lemma sign_cases [case_names even odd]:
obtains ‹sign p = 1› | ‹sign p = - 1›
by (cases ‹evenperm p›) (simp_all add: sign_def)
lemma sign_nz [simp]: "sign p \ 0"
by (cases p rule: sign_cases) simp_all
lemma sign_id [simp]: "sign id = 1"
by (simp add: sign_def)
lemma sign_identity [simp]:
‹sign (λx. x) = 1›
by (simp add: sign_def)
lemma sign_inverse: "permutation p \ sign (inv p) = sign p"
by (simp add: sign_def evenperm_inv)
lemma sign_compose: "permutation p \ permutation q \ sign (p \ q) = sign p * sign q"
by (simp add: sign_def evenperm_comp)
lemma sign_swap_id: "sign (transpose a b) = (if a = b then 1 else - 1)"
by (simp add: sign_def evenperm_swap)
lemma sign_idempotent [simp]: "sign p * sign p = 1"
by (simp add: sign_def)
lemma sign_left_idempotent [simp]:
‹sign p * (sign p * sign q) = sign q›
by (simp add: sign_def)
lemma abs_sign [simp]: "\sign p\ = 1"
by (simp add: sign_def)
subsection ‹An induction principle in terms of transpositions›
definition apply_transps :: "('a \ 'a) list \ 'a \ 'a" where
"apply_transps xs = foldr (\) (map (\(a,b). Transposition.transpose a b) xs) id"
lemma apply_transps_Nil [simp]: "apply_transps [] = id"
by (simp add: apply_transps_def)
lemma apply_transps_Cons [simp]:
"apply_transps (x # xs) = Transposition.transpose (fst x) (snd x) \ apply_transps xs"
by (simp add: apply_transps_def case_prod_unfold)
lemma apply_transps_append [simp]:
"apply_transps (xs @ ys) = apply_transps xs \ apply_transps ys"
by (induction xs) auto
lemma permutation_apply_transps [simp, intro]: "permutation (apply_transps xs)"
proof (induction xs)
case (Cons x xs)
thus ?case
unfolding apply_transps_Cons by (intro permutation_compose permutation_swap_id)
qed auto
lemma permutes_apply_transps:
assumes "\(a,b)\set xs. a \ A \ b \ A"
shows "apply_transps xs permutes A"
using assms
proof (induction xs)
case (Cons x xs)
from Cons.prems show ?case
unfolding apply_transps_Cons
by (intro permutes_compose permutes_swap_id Cons) auto
qed (auto simp: permutes_id)
lemma permutes_induct [consumes 2, case_names id swap]:
assumes "p permutes S" "finite S"
assumes "P id"
assumes "\a b p. a \ S \ b \ S \ a \ b \ P p \ p permutes S
==> P (Transposition.transpose a b ∘ p)"
shows "P p"
using assms(2,1,4)
proof (induct S arbitrary: p rule: finite_induct)
case empty
then show ?case using assms by (auto simp: id_def)
next
case (insert x F p)
let ?r = "Transposition.transpose x (p x) \ p"
let ?q = "Transposition.transpose x (p x) \ ?r"
have qp: "?q = p"
by (simp add: o_assoc)
have "?r permutes F"
using permutes_insert_lemma[OF insert.prems(1)] .
have "P ?r"
by (rule insert(3)[OF ‹?r permutes F›], rule insert(5)) (auto intro: permutes_subset)
show ?case
proof (cases "x = p x")
case False
have "p x \ F"
using permutes_in_image[OF ‹p permutes _›, of x] False by auto
have "P ?q"
by (rule insert(5))
(use ‹P ?r› ‹p x ∈ F› ‹?r permutes F› False in ‹auto simp: o_def intro: permutes_subset›)
thus "P p"
by (simp add: qp)
qed (use ‹P ?r› in simp)
qed
lemma permutes_rev_induct[consumes 2, case_names id swap]:
assumes "finite S" "p permutes S"
assumes "P id"
assumes "\a b p. a \ S \ b \ S \ a \ b \ P p \ p permutes S
==> P (p ∘ Transposition.transpose a b)"
shows "P p"
proof -
have "inv_into UNIV p permutes S"
using assms by (intro permutes_inv)
from this and assms(1,2) show ?thesis
proof (induction "inv_into UNIV p" arbitrary: p rule: permutes_induct)
case id
hence "p = id"
by (metis inv_id permutes_inv_inv)
thus ?case using ‹P id› by (auto simp: id_def)
next
case (swap a b p p')
have "p = Transposition.transpose a b \ (Transposition.transpose a b \ p)"
by (simp add: o_assoc)
also have "\ = Transposition.transpose a b \ inv_into UNIV p'"
by (subst swap.hyps) auto
also have "Transposition.transpose a b = inv_into UNIV (Transposition.transpose a b)"
by (simp add: inv_swap_id)
also have "\ \ inv_into UNIV p' = inv_into UNIV (p' \ Transposition.transpose a b)"
using swap ‹finite S›
by (intro permutation_inverse_compose [symmetric] permutation_swap_id permutation_inverse)
(auto simp: permutation_permutes)
finally have "p = inv (p' \ Transposition.transpose a b)" .
moreover have "p' \ Transposition.transpose a b permutes S"
by (intro permutes_compose permutes_swap_id swap)
ultimately have *: "P (p' \ Transposition.transpose a b)"
by (rule swap(4))
have "P (p' \ Transposition.transpose a b \ Transposition.transpose a b)"
by (rule assms; intro * swap permutes_compose permutes_swap_id)
also have "p' \ Transposition.transpose a b \ Transposition.transpose a b = p'"
by (simp flip: o_assoc)
finally show ?case .
qed
qed
lemma map_permutation_apply_transps:
assumes f: "inj_on f A" and "set ts \ A \ A"
shows "map_permutation A f (apply_transps ts) = apply_transps (map (map_prod f f) ts)"
using assms(2)
proof (induction ts)
case (Cons t ts)
obtain a b where [simp]: "t = (a, b)"
by (cases t)
have "map_permutation A f (apply_transps (t # ts)) =
map_permutation A f (Transposition.transpose a b ∘ apply_transps ts)"
by simp
also have "\ = map_permutation A f (Transposition.transpose a b) \
map_permutation A f (apply_transps ts)"
by (subst map_permutation_compose')
(use f Cons.prems in ‹auto intro!: permutes_apply_transps›)
also have "map_permutation A f (Transposition.transpose a b) =
Transposition.transpose (f a) (f b)"
by (intro map_permutation_transpose f) (use Cons.prems in auto)
also have "map_permutation A f (apply_transps ts) = apply_transps (map (map_prod f f) ts)"
by (intro Cons.IH) (use Cons.prems in auto)
also have "Transposition.transpose (f a) (f b) \ apply_transps (map (map_prod f f) ts) =
apply_transps (map (map_prod f f) (t # ts))"
by simp
finally show ?case .
qed (use f in ‹auto simp: map_permutation_id'\)
lemma permutes_from_transpositions:
assumes "p permutes A" "finite A"
shows "\xs. (\(a,b)\set xs. a \ b \ a \ A \ b \ A) \ apply_transps xs = p"
using assms
proof (induction rule: permutes_induct)
case id
thus ?case by (intro exI[of _ "[]"]) auto
next
case (swap a b p)
from swap.IH obtain xs where
xs: "(\(a,b)\set xs. a \ b \ a \ A \ b \ A)" "apply_transps xs = p"
by blast
thus ?case
using swap.hyps by (intro exI[of _ "(a,b) # xs"]) auto
qed
subsection ‹More on the sign of permutations›
lemma evenperm_apply_transps_iff:
assumes "\(a,b)\set xs. a \ b"
shows "evenperm (apply_transps xs) \ even (length xs)"
using assms
by (induction xs)
(simp_all add: case_prod_unfold evenperm_comp permutation_swap_id evenperm_swap)
lemma evenperm_map_permutation:
assumes f: "inj_on f A" and "p permutes A" "finite A"
shows "evenperm (map_permutation A f p) \ evenperm p"
proof -
note [simp] = inj_on_eq_iff[OF f]
obtain ts where ts: "\(a, b)\set ts. a \ b \ a \ A \ b \ A" "apply_transps ts = p"
using permutes_from_transpositions[OF assms(2,3)] by blast
have "evenperm p \ even (length ts)"
by (subst ts(2) [symmetric], subst evenperm_apply_transps_iff) (use ts(1) in auto)
also have "\ \ even (length (map (map_prod f f) ts))"
by simp
also have "\ \ evenperm (apply_transps (map (map_prod f f) ts))"
by (subst evenperm_apply_transps_iff) (use ts(1) in auto)
also have "apply_transps (map (map_prod f f) ts) = map_permutation A f p"
unfolding ts(2)[symmetric]
by (rule map_permutation_apply_transps [symmetric]) (use f ts(1) in auto)
finally show ?thesis ..
qed
lemma sign_map_permutation:
assumes "inj_on f A" "p permutes A" "finite A"
shows "sign (map_permutation A f p) = sign p"
unfolding sign_def by (subst evenperm_map_permutation) (use assms in auto)
text ‹
Sometimes it can be useful to consider the sign of a function that is not a permutation in the
Isabelle/HOL sense, but its restriction to some finite subset is.
›
definition sign_on :: "'a set \ ('a \ 'a) \ int"
where "sign_on A f = sign (restrict_id f A)"
lemma sign_on_cong [cong]:
assumes "A = B" "\x. x \ A \ f x = g x"
shows "sign_on A f = sign_on B g"
unfolding sign_on_def using assms
by (intro arg_cong[of _ _ sign] restrict_id_cong)
lemma sign_on_permutes:
assumes "f permutes A" "A \ B"
shows "sign_on B f = sign f"
proof -
have f: "f permutes B"
using assms permutes_subset by blast
have "sign_on B f = sign (restrict_id f B)"
by (simp add: sign_on_def)
also have "restrict_id f B = f"
using f by (auto simp: fun_eq_iff permutes_not_in restrict_id_def)
finally show ?thesis .
qed
lemma sign_on_id [simp]: "sign_on A id = 1"
by (subst sign_on_permutes[of _ A]) auto
lemma sign_on_ident [simp]: "sign_on A (\x. x) = 1"
using sign_on_id[of A] unfolding id_def by simp
lemma sign_on_transpose:
assumes "a \ A" "b \ A" "a \ b"
shows "sign_on A (Transposition.transpose a b) = -1"
by (subst sign_on_permutes[of _ A])
(use assms in ‹auto simp: permutes_swap_id sign_swap_id›)
lemma sign_on_compose:
assumes "bij_betw f A A" "bij_betw g A A" "finite A"
shows "sign_on A (f \ g) = sign_on A f * sign_on A g"
proof -
define restr where "restr = (\f. restrict_id f A)"
have "sign_on A (f \ g) = sign (restr (f \ g))"
by (simp add: sign_on_def restr_def)
also have "restr (f \ g) = restr f \ restr g"
using assms(2) by (auto simp: restr_def fun_eq_iff bij_betw_def restrict_id_def)
also have "sign \ = sign (restr f) * sign (restr g)" unfolding restr_def
by (rule sign_compose) (auto intro!: permutes_imp_permutation[of A] permutes_restrict_id assms)
also have "\ = sign_on A f * sign_on A g"
by (simp add: sign_on_def restr_def)
finally show ?thesis .
qed
subsection ‹Transpositions of adjacent elements›
text ‹
We have shown above that every permutation can be written as a product of transpositions.
We will now furthermore show that any transposition of successive natural numbers
$\{m, \ldots, n\}$ can be written as a product of transpositions of 🚫‹adjacent› elements,
i.e.\ transpositions of the form $i \leftrightarrow i+1$.
›
function adj_transp_seq :: "nat \ nat \ nat list" where
"adj_transp_seq a b =
(if a ≥ b then []
else if b = a + 1 then [a]
else a # adj_transp_seq (a+1) b @ [a])"
by auto
termination by (relation "measure (\(a,b). b - a)") auto
lemmas [simp del] = adj_transp_seq.simps
lemma length_adj_transp_seq:
"a < b \ length (adj_transp_seq a b) = 2 * (b - a) - 1"
by (induction a b rule: adj_transp_seq.induct; subst adj_transp_seq.simps) auto
definition apply_adj_transps :: "nat list \ nat \ nat"
where "apply_adj_transps xs = foldl (\) id (map (\x. Transposition.transpose x (x+1)) xs)"
lemma apply_adj_transps_aux:
"f \ foldl (\) g (map (\x. Transposition.transpose x (Suc x)) xs) =
foldl (∘) (f ∘ g) (map (λx. Transposition.transpose x (Suc x)) xs)"
by (induction xs arbitrary: f g) (auto simp: o_assoc)
lemma apply_adj_transps_Nil [simp]: "apply_adj_transps [] = id"
and apply_adj_transps_Cons [simp]:
"apply_adj_transps (x # xs) = Transposition.transpose x (x+1) \ apply_adj_transps xs"
and apply_adj_transps_snoc [simp]:
"apply_adj_transps (xs @ [x]) = apply_adj_transps xs \ Transposition.transpose x (x+1)"
by (simp_all add: apply_adj_transps_def apply_adj_transps_aux)
lemma adj_transp_seq_correct:
assumes "a < b"
shows "apply_adj_transps (adj_transp_seq a b) = Transposition.transpose a b"
using assms
proof (induction a b rule: adj_transp_seq.induct)
case (1 a b)
show ?case
proof (cases "b = a + 1")
case True
thus ?thesis
by (subst adj_transp_seq.simps) (auto simp: o_def Transposition.transpose_def apply_adj_transps_def)
next
case False
hence "apply_adj_transps (adj_transp_seq a b) =
Transposition.transpose a (Suc a) ∘ Transposition.transpose (Suc a) b ∘ Transposition.transpose a (Suc a)"
using 1 by (subst adj_transp_seq.simps)
(simp add: o_assoc swap_id_common swap_id_common' id_def o_def)
also have "\ = Transposition.transpose a b"
using False 1 by (simp add: Transposition.transpose_def fun_eq_iff)
finally show ?thesis .
qed
qed
lemma permutation_apply_adj_transps: "permutation (apply_adj_transps xs)"
proof (induction xs)
case (Cons x xs)
have "permutation (Transposition.transpose x (Suc x) \ apply_adj_transps xs)"
by (intro permutation_compose permutation_swap_id Cons)
thus ?case by (simp add: o_def)
qed auto
lemma permutes_apply_adj_transps:
assumes "\x\set xs. x \ A \ Suc x \ A"
shows "apply_adj_transps xs permutes A"
using assms
by (induction xs) (auto intro!: permutes_compose permutes_swap_id permutes_id)
lemma set_adj_transp_seq:
"a < b \ set (adj_transp_seq a b) = {a..
by (induction a b rule: adj_transp_seq.induct, subst adj_transp_seq.simps) auto
subsection ‹Transferring properties of permutations along bijections›
locale permutes_bij =
fixes p :: "'a \ 'a" and A :: "'a set" and B :: "'b set"
fixes f :: "'a \ 'b" and f' :: "'b ==> 'a"
fixes p' :: "'b ==> 'b"
defines "p' \ (\x. if x \ B then f (p (f' x)) else x)"
assumes permutes_p: "p permutes A"
assumes bij_f: "bij_betw f A B"
assumes f'_f: "x \ A \ f' (f x) = x"
begin
lemma bij_f': "bij_betw f' B A"
using bij_f f'_f by (auto simp: bij_betw_def) (auto simp: inj_on_def image_image)
lemma f_f': "x \ B \ f (f' x) = x"
using f'_f bij_f by (auto simp: bij_betw_def)
lemma f_in_B: "x \ A \ f x \ B"
using bij_f by (auto simp: bij_betw_def)
lemma f'_in_A: "x \ B \ f' x ∈ A"
using bij_f' by (auto simp: bij_betw_def)
lemma permutes_p': "p' permutes B"
proof -
have p': "p' x = x" if "x ∉ B" for x
using that by (simp add: p'_def)
have bij_p: "bij_betw p A A"
using permutes_p by (simp add: permutes_imp_bij)
have "bij_betw (f \ p \ f') B B"
by (rule bij_betw_trans bij_f bij_f' bij_p)+
also have "?this \ bij_betw p' B B"
by (intro bij_betw_cong) (auto simp: p'_def)
finally show ?thesis
using p' by (rule bij_imp_permutes)
qed
lemma f_eq_iff [simp]: "f x = f y \ x = y" if "x \ A" "y \ A" for x y
using that bij_f by (auto simp: bij_betw_def inj_on_def)
lemma apply_transps_map_f_aux:
assumes "\(a,b)\set xs. a \ A \ b \ A" "y \ B"
shows "apply_transps (map (map_prod f f) xs) y = f (apply_transps xs (f' y))"
using assms
proof (induction xs arbitrary: y)
case Nil
thus ?case by (auto simp: f_f')
next
case (Cons x xs y)
from Cons.prems have "apply_transps xs permutes A"
by (intro permutes_apply_transps) auto
hence [simp]: "apply_transps xs z \ A \ z \ A" for z
by (simp add: permutes_in_image)
from Cons show ?case
by (auto simp: Transposition.transpose_def f_f' f'_f case_prod_unfold f'_in_A)
qed
lemma apply_transps_map_f:
assumes "\(a,b)\set xs. a \ A \ b \ A"
shows "apply_transps (map (map_prod f f) xs) =
(λy. if y ∈ B then f (apply_transps xs (f' y)) else y)"
proof
fix y
show "apply_transps (map (map_prod f f) xs) y =
(if y ∈ B then f (apply_transps xs (f' y)) else y)"
proof (cases "y \ B")
case True
thus ?thesis
using apply_transps_map_f_aux[OF assms] by simp
next
case False
have "apply_transps (map (map_prod f f) xs) permutes B"
using assms by (intro permutes_apply_transps) (auto simp: case_prod_unfold f_in_B)
with False have "apply_transps (map (map_prod f f) xs) y = y"
by (intro permutes_not_in)
with False show ?thesis
by simp
qed
qed
end
locale permutes_bij_finite = permutes_bij +
assumes finite_A: "finite A"
begin
lemma evenperm_p'_iff: "evenperm p' ⟷ evenperm p"
proof -
obtain xs where xs: "\(a,b)\set xs. a \ A \ b \ A \ a \ b" "apply_transps xs = p"
using permutes_from_transpositions[OF permutes_p finite_A] by blast
have "evenperm p \ evenperm (apply_transps xs)"
using xs by simp
also have "\ \ even (length xs)"
using xs by (intro evenperm_apply_transps_iff) auto
also have "\ \ even (length (map (map_prod f f) xs))"
by simp
also have "\ \ evenperm (apply_transps (map (map_prod f f) xs))" using xs
by (intro evenperm_apply_transps_iff [symmetric]) (auto simp: case_prod_unfold)
also have "apply_transps (map (map_prod f f) xs) = p'"
using xs unfolding p'_def by (subst apply_transps_map_f) auto
finally show ?thesis ..
qed
lemma sign_p': "sign p' = sign p"
by (auto simp: sign_def evenperm_p'_iff)
end
subsection ‹Permuting a list›
text ‹This function permutes a list by applying a permutation to the indices.›
definition permute_list :: "(nat \ nat) \ 'a list \ 'a list"
where "permute_list f xs = map (\i. xs ! (f i)) [0..
lemma permute_list_map:
assumes "f permutes {..
shows "permute_list f (map g xs) = map g (permute_list f xs)"
using permutes_in_image[OF assms] by (auto simp: permute_list_def)
lemma permute_list_nth:
assumes "f permutes {.. "i < length xs"
shows "permute_list f xs ! i = xs ! f i"
using permutes_in_image[OF assms(1)] assms(2)
by (simp add: permute_list_def)
lemma permute_list_Nil [simp]: "permute_list f [] = []"
by (simp add: permute_list_def)
lemma length_permute_list [simp]: "length (permute_list f xs) = length xs"
by (simp add: permute_list_def)
lemma permute_list_compose:
assumes "g permutes {..
shows "permute_list (f \ g) xs = permute_list g (permute_list f xs)"
using assms[THEN permutes_in_image] by (auto simp add: permute_list_def)
lemma permute_list_ident [simp]: "permute_list (\x. x) xs = xs"
by (simp add: permute_list_def map_nth)
lemma permute_list_id [simp]: "permute_list id xs = xs"
by (simp add: id_def)
lemma mset_permute_list [simp]:
fixes xs :: "'a list"
assumes "f permutes {..
shows "mset (permute_list f xs) = mset xs"
proof (rule multiset_eqI)
fix y :: 'a
from assms have [simp]: "f x < length xs \ x < length xs" for x
using permutes_in_image[OF assms] by auto
have "count (mset (permute_list f xs)) y = card ((\i. xs ! f i) -` {y} \ {..
by (simp add: permute_list_def count_image_mset atLeast0LessThan)
also have "(\i. xs ! f i) -` {y} \ {.. y = xs ! i}"
by auto
also from assms have "card \ = card {i. i < length xs \ y = xs ! i}"
by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj)
also have "\ = count (mset xs) y"
by (simp add: count_mset count_list_eq_length_filter length_filter_conv_card)
--> --------------------
--> maximum size reached
--> --------------------
