Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Combinatorics/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 87 kB

Quellcode-Bibliothek Permutations.thy Sprache: Isabelle

(*  Author:     Amine Chaieb, University of Cambridge

    With various additions by Manuel Eberl
*)

section \<open>Permutations, both general and specifically on finite sets.\<close>

theory Permutations
  imports
    "HOL-Library.Multiset"
    "HOL-Library.Disjoint_Sets"
    Transposition
begin

subsection \<open>Auxiliary\<close>

abbreviation (input) fixpoints :: \<open>('a \<Rightarrow> 'a) \<Rightarrow> 'a set\<close>
  where \<open>fixpoints f \<equiv> {x. f x = x}\<close>

lemma inj_on_fixpoints:
  \<open>inj_on f (fixpoints f)\<close>
  by (rule inj_onI) simp

lemma bij_betw_fixpoints:
  \<open>bij_betw f (fixpoints f) (fixpoints f)\<close>
  using inj_on_fixpoints by (auto simp add: bij_betw_def)

subsection \<open>Basic definition and consequences\<close>

definition permutes :: \<open>('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool\<close>  (infixr \<open>permutes\<close> 41)
  where \<open>p permutes S \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)\<close>

lemma bij_imp_permutes:
  \<open>p permutes S\<close> if \<open>bij_betw p S S\<close> and stable: \<open>\<And>x. x \<notin> S \<Longrightarrow> p x = x\<close>
proof -
  note \<open>bij_betw p S S\<close>
  moreover have \<open>bij_betw p (- S) (- S)\<close>
    by (auto simp add: stable intro!: bij_betw_imageI inj_onI)
  ultimately have \<open>bij_betw p (S \<union> - S) (S \<union> - S)\<close>
    by (rule bij_betw_combine) simp
  then have \<open>\<exists>!x. p x = y\<close> 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' \<in> S" by metis
      from inj_onD[OF i fx[folded fx'] x this]
      show "x' = x" by simp
    qed
  qed
qed

context
  fixes p :: \<open>'a \<Rightarrow> 'a\<close> and S :: \<open>'a set\<close>
  assumes perm: \<open>p permutes S\<close>
begin

lemma permutes_inj:
  \<open>inj p\<close>
  using perm by (auto simp: permutes_def inj_on_def)

lemma permutes_image:
  \<open>p ` S = S\<close>
proof (rule set_eqI)
  fix x
  show \<open>x \<in> p ` S \<longleftrightarrow> x \<in> S\<close>
  proof
    assume \<open>x \<in> p ` S\<close>
    then obtain y where \<open>y \<in> S\<close> \<open>p y = x\<close>
      by blast
    with perm show \<open>x \<in> S\<close>
      by (cases \<open>y = x\<close>) (auto simp add: permutes_def)
  next
    assume \<open>x \<in> S\<close>
    with perm obtain y where \<open>y \<in> S\<close> \<open>p y = x\<close>
      by (metis permutes_def)
    then show \<open>x \<in> p ` S\<close>
      by blast
  qed
qed

lemma permutes_not_in:
  \<open>x \<notin> S \<Longrightarrow> p x = x\<close>
  using perm by (auto simp: permutes_def)

lemma permutes_image_complement:
  \<open>p ` (- S) = - S\<close>
  by (auto simp add: permutes_not_in)

lemma permutes_in_image:
  \<open>p x \<in> S \<longleftrightarrow> x \<in> S\<close>
  using permutes_image permutes_inj by (auto dest: inj_image_mem_iff)

lemma permutes_surj:
  \<open>surj p\<close>
proof -
  have \<open>p ` (S \<union> - S) = p ` S \<union> p ` (- S)\<close>
    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:
  \<open>inv p y = x \<longleftrightarrow> p x = y\<close>
  by (auto simp add: permutes_inverses)

lemma permutes_inj_on:
  \<open>inj_on p A\<close>
  by (rule inj_on_subset [of _ UNIV]) (auto intro: permutes_inj)

lemma permutes_bij:
  \<open>bij p\<close>
  unfolding bij_def by (metis permutes_inj permutes_surj)

lemma permutes_imp_bij:
  \<open>bij_betw p S S\<close>
  by (simp add: bij_betw_def permutes_image permutes_inj_on)

lemma permutes_subset:
  \<open>p permutes T\<close> if \<open>S \<subseteq> T\<close>
proof (rule bij_imp_permutes)
  define R where \<open>R = T - S\<close>
  with that have \<open>T = R \<union> S\<close> \<open>R \<inter> S = {}\<close>
    by auto
  then have \<open>p x = x\<close> if \<open>x \<in> R\<close> for x
    using that by (auto intro: permutes_not_in)
  then have \<open>p ` R = R\<close>
    by simp
  with \<open>T = R \<union> S\<close> show \<open>bij_betw p T T\<close>
    by (simp add: bij_betw_def permutes_inj_on image_Un permutes_image)
  fix x
  assume \<open>x \<notin> T\<close>
  with \<open>T = R \<union> S\<close> show \<open>p x = x\<close>
    by (simp add: permutes_not_in)
qed

lemma permutes_imp_permutes_insert:
  \<open>p permutes insert x S\<close>
  by (rule permutes_subset) auto

end

lemma permutes_id [simp]:
  \<open>id permutes S\<close>
  by (auto intro: bij_imp_permutes)

lemma permutes_empty [simp]:
  \<open>p permutes {} \<longleftrightarrow> p = id\<close>
proof
  assume \<open>p permutes {}\<close>
  then show \<open>p = id\<close>
    by (auto simp add: fun_eq_iff permutes_not_in)
next
  assume \<open>p = id\<close>
  then show \<open>p permutes {}\<close>
    by simp
qed

lemma permutes_sing [simp]:
  \<open>p permutes {a} \<longleftrightarrow> p = id\<close>
proof
  assume perm: \<open>p permutes {a}\<close>
  show \<open>p = id\<close>
  proof
    fix x
    from perm have \<open>p ` {a} = {a}\<close>
      by (rule permutes_image)
    with perm show \<open>p x = id x\<close>
      by (cases \<open>x = a\<close>) (auto simp add: permutes_not_in)
  qed
next
  assume \<open>p = id\<close>
  then show \<open>p permutes {a}\<close>
    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:
  \<open>p permutes T\<close> if \<open>p permutes S\<close> \<open>\<And>x. x \<in> S - T \<Longrightarrow> p x = x\<close>
proof -
  define R U where \<open>R = T \<inter> S\<close> and \<open>U = S - T\<close>
  then have \<open>T = R \<union> (T - S)\<close> \<open>S = R \<union> U\<close> \<open>R \<inter> U = {}\<close>
    by auto
  from that \<open>U = S - T\<close> have \<open>p ` U = U\<close>
    by simp
  from \<open>p permutes S\<close> have \<open>bij_betw p (R \<union> U) (R \<union> U)\<close>
    by (simp add: permutes_imp_bij \<open>S = R \<union> U\<close>)
  moreover have \<open>bij_betw p U U\<close>
    using that \<open>U = S - T\<close> by (simp add: bij_betw_def permutes_inj_on)
  ultimately have \<open>bij_betw p R R\<close>
    using \<open>R \<inter> U = {}\<close> \<open>R \<inter> U = {}\<close> by (rule bij_betw_partition)
  then have \<open>p permutes R\<close>
  proof (rule bij_imp_permutes)
    fix x
    assume \<open>x \<notin> R\<close>
    with \<open>R = T \<inter> S\<close> \<open>p permutes S\<close> show \<open>p x = x\<close>
      by (cases \<open>x \<in> S\<close>) (auto simp add: permutes_not_in that(2))
  qed
  then have \<open>p permutes R \<union> (T - S)\<close>
    by (rule permutes_subset) simp
  with \<open>T = R \<union> (T - S)\<close> show ?thesis
    by simp
qed

lemma permutes_bij_inv_into: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
  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: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
  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: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
  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 \<open>Group properties\<close>

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 \<open>Restricting a permutation to a subset\<close>

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 \<open>auto intro: bij_betwI\<close>)
  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 \<open>Mapping a permutation\<close>

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 \<open>inj_on f A\<close> u(1) by (metis assms(2) inj_on_cong inv_into_f_f)
    thus ?thesis
      using u \<open>x = y\<close> \<open>A = B\<close> 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: \<open>A = B\<close>)
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 \<open>p permutes A\<close> 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 \<open>inj_on g B\<close> 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'] \<open>g x = g y\<close> 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 \<open>inj_on g B\<close> in auto)
  also have "\ = map_permutation A id p"
    by (intro map_permutation_cong assms comp_inj_on)
       (use \<open>inj_on g B\<close> assms(1,3) in \<open>auto simp: bij_betw_def\<close>)
  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 \<circ> f) p"
    by (rule map_permutation_compose[OF _ inj_on_inv_into])
       (use assms in \<open>auto simp: bij_betw_def\<close>)
  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)
             {\<pi>. \<pi> permutes A} {\<pi>. \<pi> 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 \<pi> assume "\<pi> 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)
             {\<pi>. \<pi> permutes A \<and> (\<forall>x\<in>A. \<pi> x \<noteq> x)} {\<pi>. \<pi> permutes B \<and> (\<forall>x\<in>B. \<pi> x \<noteq> 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 \<open>The number of permutations on a finite set\<close>

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)} =
  (\<lambda>(b, p). transpose a b \<circ> p) ` {(b, p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
proof -
  have "p permutes insert a S \
    (\<exists>b q. p = transpose a b \<circ> q \<and> b \<in> insert a S \<and> 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 \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have Fs: "card F = n - 1"
      by auto
    from \<open>finite F\<close> insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
      by auto
    then have "finite ?pF"
      by (auto intro: card_ge_0_finite)
    with \<open>finite F\<close> 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 \<open>x \<notin> F\<close> eq have "b = ?g (b, p) x"
          by (auto simp: permutes_def fun_upd_def fun_eq_iff)
        also from qF \<open>x \<notin> F\<close> eq have "\<dots> = ?g (c, q) x"
          by (auto simp: fun_upd_def fun_eq_iff)
        also from qF \<open>x \<notin> F\<close> have "\<dots> = 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 \<open>b = c\<close> have "(b, p) = (c, q)"
          by simp
      }
      then show ?thesis
        unfolding inj_on_def by blast
    qed
    from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have "n \<noteq> 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 \<open>finite F\<close> \<open>finite ?pF\<close>
      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 \<open>Permutations of index set for iterated operations\<close>

lemma (in comm_monoid_set) permute:
  assumes "p permutes S"
  shows "F g S = F (g \ p) S"
proof -
  from \<open>p permutes S\<close> 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 \<open>p permutes S\<close> have "p ` S = S"
    by (rule permutes_image)
  ultimately show ?thesis
    by simp
qed

subsection \<open>Permutations as transposition sequences\<close>

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 \<open>Some closure properties of the set of permutations, with lengths\<close>

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 \<open>auto simp add: comp_assoc intro: swapidseq.comp_Suc\<close>)

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 \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close>

lemma swap_id_common:" a \ c \ b \ c \
  transpose a b \<circ> transpose a c = transpose b c \<circ> transpose a b"
  by (simp add: fun_eq_iff transpose_def)

lemma swap_id_common': "a \ b \ a \ c \
  transpose a c \<circ> transpose b c = transpose b c \<circ> 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 \<circ> transpose c d = transpose c d \<circ> transpose a b"
  by (simp add: fun_eq_iff transpose_def)

subsection \<open>The identity map only has even transposition sequences\<close>

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 \<and> b = d \<or> a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d \<Longrightarrow>
      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 \
  (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
    transpose a b \<circ> transpose c d = transpose x y \<circ> 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 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = transpose a b \<circ> q \<and> swapidseq m q \<and> a \<noteq> 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 \<section>: "transpose a b \<circ> p = transpose x y \<circ> (transpose a z \<circ> 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 "**" \<section> swapidseq.simps by blast
  qed
qed

lemma swapidseq_identity_even:
  assumes "swapidseq n (id :: 'a \ 'a)"
  shows "even n"
  using \<open>swapidseq n id\<close>
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 \<open>Therefore we have a welldefined notion of parity\<close>

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 \<open>And it has the expected composition properties\<close>

lemma evenperm_id[simp]: "evenperm id = True"
  by (rule evenperm_unique[where n = 0]) simp_all

lemma evenperm_identity [simp]:
  \<open>evenperm (\<lambda>x. x)\<close>
  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 \<open>A more abstract characterization of permutations\<close>

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 \<open>a \<noteq> b\<close> have **: "{x. (transpose a b \<circ> p) x \<noteq> x} \<subseteq> ?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 \<open>bij ?r\<close> **])
  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 \<open>Relation to \<open>permutes\<close>\<close>

lemma permutes_imp_permutation:
  \<open>permutation p\<close> if \<open>finite S\<close> \<open>p permutes S\<close>
proof -
  from \<open>p permutes S\<close> have \<open>{x. p x \<noteq> x} \<subseteq> S\<close>
    by (auto dest: permutes_not_in)
  then have \<open>finite {x. p x \<noteq> x}\<close>
    using \<open>finite S\<close> by (rule finite_subset)
  moreover from \<open>p permutes S\<close> have \<open>bij p\<close>
    by (auto dest: permutes_bij)
  ultimately show ?thesis
    by (simp add: permutation)
qed

lemma permutation_permutesE:
  assumes \<open>permutation p\<close>
  obtains S where \<open>finite S\<close> \<open>p permutes S\<close>
proof -
  from assms have fin: \<open>finite {x. p x \<noteq> x}\<close>
    by (simp add: permutation)
  from assms have \<open>bij p\<close>
    by (simp add: permutation)
  also have \<open>UNIV = {x. p x \<noteq> x} \<union> {x. p x = x}\<close>
    by auto
  finally have \<open>bij_betw p {x. p x \<noteq> x} {x. p x \<noteq> x}\<close>
    by (rule bij_betw_partition) (auto simp add: bij_betw_fixpoints)
  then have \<open>p permutes {x. p x \<noteq> x}\<close>
    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 \<open>Sign of a permutation\<close>

definition sign :: \<open>('a \<Rightarrow> 'a) \<Rightarrow> int\<close> \<comment> \<open>TODO: prefer less generic name\<close>
  where \<open>sign p = (if evenperm p then 1 else - 1)\<close>

lemma sign_cases [case_names even odd]:
  obtains \<open>sign p = 1\<close> | \<open>sign p = - 1\<close>
  by (cases \<open>evenperm p\<close>) (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]:
  \<open>sign (\<lambda>x. x) = 1\<close>
  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]:
  \<open>sign p * (sign p * sign q) = sign q\<close>
  by (simp add: sign_def)

lemma abs_sign [simp]: "\sign p\ = 1"
  by (simp add: sign_def)

subsection \<open>An induction principle in terms of transpositions\<close>

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
             \<Longrightarrow> P (Transposition.transpose a b \<circ> 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 \<open>?r permutes F\<close>], 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 \<open>p permutes _\<close>, of x] False by auto
    have "P ?q"
      by (rule insert(5))
         (use \<open>P ?r\<close> \<open>p x \<in> F\<close> \<open>?r permutes F\<close> False in \<open>auto simp: o_def intro: permutes_subset\<close>)
    thus "P p"
      by (simp add: qp)
  qed (use \<open>P ?r\<close> 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
             \<Longrightarrow> P (p \<circ> 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 \<open>P id\<close> 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 \<open>finite S\<close>
      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 \<circ> 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 \<open>auto intro!: permutes_apply_transps\<close>)
  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 \<open>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 \<open>More on the sign of permutations\<close>

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 \<open>
  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.
\<close>
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 \<open>auto simp: permutes_swap_id sign_swap_id\<close>)

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 \<open>Transpositions of adjacent elements\<close>

text \<open>
  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 \<^emph>\<open>adjacent\<close> elements,
  i.e.\ transpositions of the form $i \leftrightarrow i+1$.
\<close>

function adj_transp_seq :: "nat \ nat \ nat list" where
  "adj_transp_seq a b =
     (if a \<ge> 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 (\<circ>) (f \<circ> g) (map (\<lambda>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) \<circ> Transposition.transpose (Suc a) b \<circ> 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 \<open>Transferring properties of permutations along bijections\<close>

locale permutes_bij =
  fixes p :: "'a \ 'a" and A :: "'a set" and B :: "'b set"
  fixes f :: "'a \ 'b" and f' :: "'b \<Rightarrow> 'a"
  fixes p' :: "'b \<Rightarrow> '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 \<in> A"
  using bij_f' by (auto simp: bij_betw_def)

lemma permutes_p': "p' permutes B"
proof -
  have p': "p' x = x" if "x \<notin> 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) =
             (\<lambda>y. if y \<in> 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 \<in> 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' \<longleftrightarrow> 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 \<open>Permuting a list\<close>

text \<open>This function permutes a list by applying a permutation to the indices.\<close>

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

--> --------------------

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.37Bemerkung: ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.