# HG changeset patch
# User haftmann
# Date 1616410191 0
# Node ID ee1c4962671cd236648a64eff7be90856b6531f7
# Parent  1e5c1f8a35cdd79425443699d2909c6d694caed6
more lemmas

diff -r 1e5c1f8a35cd -r ee1c4962671c NEWS
--- a/NEWS	Mon Mar 22 00:07:55 2021 +0100
+++ b/NEWS	Mon Mar 22 10:49:51 2021 +0000
@@ -65,8 +65,8 @@
 specific "List_Permutation".  Note that most notions from that
 theory are already present in theory "Permutations".  INCOMPATIBILITY.
 
-* Lemma "permutes_induct" has been given named premises.
-INCOMPATIBILITY.
+* Lemma "permutes_induct" has been given stronger
+hypotheses and named premises.  INCOMPATIBILITY.
 
 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to
 "order.antisym" and "order.eq_iff", to coexist locally with "antisym"
@@ -75,6 +75,9 @@
 "order" are replaced or augmented by interpretations of locale
 "ordering".
 
+* Theorem "swap_def" now is always qualified as "Fun.swap_def".  Minor
+INCOMPATIBILITY; note that for most applications less elementary lemmas
+exists.
 
 
 *** ML ***
diff -r 1e5c1f8a35cd -r ee1c4962671c src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Mar 22 10:49:51 2021 +0000
@@ -234,11 +234,6 @@
     by auto
 qed
 
-lemma swap_image:
-  "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
-                                  else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
-  by (auto simp: swap_def cong: image_cong_simp)
-
 lemmas swap_apply1 = swap_apply(1)
 lemmas swap_apply2 = swap_apply(2)
 
@@ -2598,5 +2593,4 @@
   using derf has_derivative_continuous by blast
 qed (use assms in auto)
 
-
 end
diff -r 1e5c1f8a35cd -r ee1c4962671c src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Mon Mar 22 10:49:51 2021 +0000
@@ -1295,7 +1295,7 @@
           case False
           have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
             using False l insert.prems that
-            by (auto simp: swap_def insert split: if_split_asm)
+            by (auto simp: swap_id_eq insert split: if_split_asm)
           have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)"
             by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
           moreover
@@ -1418,7 +1418,7 @@
     have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
               (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
       for i and x :: "real^'n"
-      unfolding swap_def by (rule sum.cong) auto
+      by (rule sum.cong) (auto simp add: swap_id_eq)
     have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
       by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
     with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
diff -r 1e5c1f8a35cd -r ee1c4962671c src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Mon Mar 22 10:49:51 2021 +0000
@@ -686,8 +686,10 @@
   show ?thesis
   proof
     assume cf: "convergent_prod f"
+    with f have "\<not> (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
+      by simp
     then have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0"
-      using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce
+      using * \<open>C \<noteq> 0\<close> filterlim_cong by fastforce
     then show "convergent_prod g"
       by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)
   next
diff -r 1e5c1f8a35cd -r ee1c4962671c src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Fun.thy	Mon Mar 22 10:49:51 2021 +0000
@@ -500,6 +500,23 @@
     by (rule bijI)
 qed
 
+lemma bij_betw_partition:
+  \<open>bij_betw f A B\<close>
+  if \<open>bij_betw f (A \<union> C) (B \<union> D)\<close> \<open>bij_betw f C D\<close> \<open>A \<inter> C = {}\<close> \<open>B \<inter> D = {}\<close>
+proof -
+  from that have \<open>inj_on f (A \<union> C)\<close> \<open>inj_on f C\<close> \<open>f ` (A \<union> C) = B \<union> D\<close> \<open>f ` C = D\<close>
+    by (simp_all add: bij_betw_def)
+  then have \<open>inj_on f A\<close> and \<open>f ` (A - C) \<inter> f ` (C - A) = {}\<close>
+    by (simp_all add: inj_on_Un)
+  with \<open>A \<inter> C = {}\<close> have \<open>f ` A \<inter> f ` C = {}\<close>
+    by auto
+  with \<open>f ` (A \<union> C) = B \<union> D\<close> \<open>f ` C = D\<close>  \<open>B \<inter> D = {}\<close>
+  have \<open>f ` A = B\<close>
+    by blast
+  with \<open>inj_on f A\<close> show ?thesis
+    by (simp add: bij_betw_def)
+qed
+
 lemma surj_image_vimage_eq: "surj f \<Longrightarrow> f ` (f -` A) = A"
   by simp
 
@@ -823,8 +840,11 @@
 
 subsection \<open>\<open>swap\<close>\<close>
 
-definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
-  where "swap a b f = f (a := f b, b:= f a)"
+context
+begin
+
+qualified definition swap :: \<open>'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)\<close>
+  where \<open>swap a b f = f (a := f b, b:= f a)\<close>
 
 lemma swap_apply [simp]:
   "swap a b f a = f b"
@@ -891,19 +911,29 @@
 lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f"
   by simp
 
+lemma swap_image:
+  \<open>swap i j f ` A = f ` (A - {i, j}
+    \<union> (if i \<in> A then {j} else {}) \<union> (if j \<in> A then {i} else {}))\<close>
+  by (auto simp add: swap_def)
+
+
 subsection \<open>Transpositions\<close>
 
-lemma swap_id_idempotent [simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
-  by (rule ext) (auto simp add: Fun.swap_def)
+lemma swap_id_eq: "swap a b id x = (if x = a then b else if x = b then a else x)"
+  by (simp add: swap_def)
 
-lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
-  by (simp add: Fun.swap_def)
+lemma swap_unfold:
+  \<open>swap a b p = p \<circ> swap a b id\<close>
+  by (simp add: fun_eq_iff swap_def)
+
+lemma swap_id_idempotent [simp]: "swap a b id \<circ> swap a b id = id"
+  by (simp flip: swap_unfold)
 
 lemma bij_swap_compose_bij:
-  \<open>bij (Fun.swap a b id \<circ> p)\<close> if \<open>bij p\<close>
+  \<open>bij (swap a b id \<circ> p)\<close> if \<open>bij p\<close>
   using that by (rule bij_comp) simp
 
-hide_const (open) swap
+end
 
 
 subsection \<open>Inversion of injective functions\<close>
diff -r 1e5c1f8a35cd -r ee1c4962671c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 22 10:49:51 2021 +0000
@@ -2027,6 +2027,10 @@
     by (cases "x \<in># A") simp_all
 qed
 
+lemma mset_set_upto_eq_mset_upto:
+  \<open>mset_set {..<n} = mset [0..<n]\<close>
+  by (induction n) (auto simp: ac_simps lessThan_Suc)
+
 context linorder
 begin
 
diff -r 1e5c1f8a35cd -r ee1c4962671c src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Library/Permutations.thy	Mon Mar 22 10:49:51 2021 +0000
@@ -8,90 +8,206 @@
   imports Multiset Disjoint_Sets
 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  (infixr "permutes" 41)
-  where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
+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 permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
-  unfolding permutes_def by metis
+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 permutes_not_in: "f permutes S \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = x"
-  by (auto simp: permutes_def)
+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: "p permutes S \<Longrightarrow> p ` S = S"
-  unfolding permutes_def
-  apply (rule set_eqI)
-  apply (simp add: image_iff)
-  apply metis
-  done
+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_inj: "p permutes S \<Longrightarrow> inj p"
-  unfolding permutes_def inj_def by blast
+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_inj_on: "f permutes S \<Longrightarrow> inj_on f A"
-  by (auto simp: permutes_def inj_on_def)
+lemma permutes_inv_o:
+  shows "p \<circ> inv p = id"
+    and "inv p \<circ> 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_surj: "p permutes s \<Longrightarrow> surj p"
-  unfolding permutes_def surj_def by metis
+lemma permutes_inv_eq:
+  \<open>inv p y = x \<longleftrightarrow> p x = y\<close>
+  by (auto simp add: permutes_inverses)
 
-lemma permutes_bij: "p permutes s \<Longrightarrow> bij p"
+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: "p permutes S \<Longrightarrow> bij_betw p S S"
-  by (metis UNIV_I bij_betw_subset permutes_bij permutes_image subsetI)
-
-lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S"
-  unfolding permutes_def bij_betw_def inj_on_def
-  by auto (metis image_iff)+
+lemma permutes_imp_bij:
+  \<open>bij_betw p S S\<close>
+  by (simp add: bij_betw_def permutes_image permutes_inj_on)
 
-lemma permutes_inv_o:
-  assumes permutes: "p permutes S"
-  shows "p \<circ> inv p = id"
-    and "inv p \<circ> p = id"
-  using permutes_inj[OF permutes] permutes_surj[OF permutes]
-  unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+
-
-lemma permutes_inverses:
-  fixes p :: "'a \<Rightarrow> 'a"
-  assumes permutes: "p permutes S"
-  shows "p (inv p x) = x"
-    and "inv p (p x) = x"
-  using permutes_inv_o[OF permutes, unfolded fun_eq_iff o_def] by auto
-
-lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> p permutes T"
-  unfolding permutes_def by blast
+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> if \<open>p permutes S\<close>
-  using that by (rule permutes_subset) auto
+  \<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]: "p permutes {} \<longleftrightarrow> p = id"
-  by (auto simp add: fun_eq_iff permutes_def)
+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]: "p permutes {a} \<longleftrightarrow> p = id"
-  by (simp add: fun_eq_iff permutes_def) metis  (*somewhat slow*)
+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 \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
   by (simp add: permutes_def)
 
-lemma permutes_inv_eq: "p permutes S \<Longrightarrow> inv p y = x \<longleftrightarrow> p x = y"
-  unfolding permutes_def inv_def
-  apply auto
-  apply (erule allE[where x=y])
-  apply (erule allE[where x=y])
-  apply (rule someI_ex)
-  apply blast
-  apply (rule some1_equality)
-  apply blast
-  apply blast
-  done
+lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
+  by (rule bij_imp_permutes) (auto simp add: swap_id_eq)
 
-lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
-  unfolding permutes_def Fun.swap_def fun_upd_def by auto metis
-
-lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
-  by (simp add: Ball_def permutes_def) metis
+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"
@@ -139,9 +255,6 @@
 
 subsection \<open>Group properties\<close>
 
-lemma permutes_id: "id permutes S"
-  by (simp add: permutes_def)
-
 lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S \<Longrightarrow> q \<circ> p permutes S"
   unfolding permutes_def o_def by metis
 
@@ -346,7 +459,7 @@
         from pF \<open>x \<notin> F\<close> eq have "b = ?g (b, p) x"
           by (auto simp: permutes_def Fun.swap_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: swap_def fun_upd_def fun_eq_iff)
+          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.swap_def fun_upd_def fun_eq_iff)
         finally have "b = c" .
@@ -388,6 +501,55 @@
   using card_permutations[OF refl assms] by (auto intro: card_ge_0_finite)
 
 
+subsection \<open>Hence a sort of induction principle composing by swaps\<close>
+
+lemma permutes_induct [consumes 2, case_names id swap]:
+  \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close>
+  and id: \<open>P id\<close>
+  and swap: \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (Fun.swap a b id \<circ> p)\<close>
+using \<open>finite S\<close> \<open>p permutes S\<close> swap proof (induction S arbitrary: p)
+  case empty
+  with id show ?case
+    by (simp only: permutes_empty)
+next
+  case (insert x S p)
+  define q where \<open>q = Fun.swap x (p x) id \<circ> p\<close>
+  then have swap_q: \<open>Fun.swap x (p x) id \<circ> q = p\<close>
+    by (simp add: o_assoc)
+  from \<open>p permutes insert x S\<close> have \<open>q permutes S\<close>
+    by (simp add: q_def permutes_insert_lemma)
+  then have \<open>q permutes insert x S\<close>
+    by (simp add: permutes_imp_permutes_insert)
+  from \<open>q permutes S\<close> have \<open>P q\<close>
+    by (auto intro: insert.IH insert.prems(2) permutes_imp_permutes_insert)
+  have \<open>x \<in> insert x S\<close>
+    by simp
+  moreover from \<open>p permutes insert x S\<close> have \<open>p x \<in> insert x S\<close>
+    using permutes_in_image [of p \<open>insert x S\<close> x] by simp
+  ultimately have \<open>P (Fun.swap x (p x) id \<circ> q)\<close>
+    using \<open>q permutes insert x S\<close> \<open>P q\<close>
+    by (rule insert.prems(2))
+  then show ?case
+    by (simp add: swap_q)
+qed
+
+lemma permutes_rev_induct [consumes 2, case_names id swap]:
+  \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close>
+  and id': \<open>P id\<close>
+  and swap': \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (Fun.swap a b p)\<close>
+using \<open>p permutes S\<close> \<open>finite S\<close> proof (induction rule: permutes_induct)
+  case id
+  from id' show ?case .
+next
+  case (swap a b p)
+  have \<open>P (Fun.swap (inv p a) (inv p b) p)\<close>
+    by (rule swap') (auto simp add: swap permutes_in_image permutes_inv)
+  also have \<open>Fun.swap (inv p a) (inv p b) p = Fun.swap a b id \<circ> p\<close>
+    by (rule bij_swap_comp [symmetric]) (rule permutes_bij, rule swap)
+  finally show ?case .
+qed
+
+
 subsection \<open>Permutations of index set for iterated operations\<close>
 
 lemma (in comm_monoid_set) permute:
@@ -834,47 +996,39 @@
 
 subsection \<open>Relation to \<open>permutes\<close>\<close>
 
-lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
-  unfolding permutation permutes_def bij_iff[symmetric]
-  apply (rule iffI, clarify)
-   apply (rule exI[where x="{x. p x \<noteq> x}"])
-   apply simp
-  apply clarsimp
-  apply (rule_tac B="S" in finite_subset)
-   apply auto
-  done
-
-
-subsection \<open>Hence a sort of induction principle composing by swaps\<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 permutes_induct [consumes 2, case_names id swap]:
-  \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close>
-  and id: \<open>P id\<close>
-  and swap: \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> permutation p \<Longrightarrow> P p \<Longrightarrow> P (Fun.swap a b id \<circ> p)\<close>
-using \<open>finite S\<close> \<open>p permutes S\<close> id swap proof (induction S arbitrary: p)
-  case empty
-  then show ?case by auto
-next
-  case (insert x F p)
-  let ?r = "Fun.swap x (p x) id \<circ> p"
-  let ?q = "Fun.swap x (p x) id \<circ> ?r"
-  have qp: "?q = p"
-    by (simp add: o_assoc)
-  from permutes_insert_lemma[OF \<open>p permutes insert x F\<close>] insert have Pr: "P ?r"
-    by blast
-  from permutes_in_image[OF \<open>p permutes insert x F\<close>, of x]
-  have pxF: "p x \<in> insert x F"
-    by simp
-  have xF: "x \<in> insert x F"
-    by simp
-  have rp: "permutation ?r"
-    unfolding permutation_permutes
-    using insert.hyps(1) permutes_insert_lemma[OF \<open>p permutes insert x F\<close>]
-    by blast
-  from insert.prems(3)[OF xF pxF rp Pr] qp show ?case
-    by (simp only:)
+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 \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
+  by (auto elim: permutation_permutesE intro: permutes_imp_permutation)
+
 
 subsection \<open>Sign of a permutation as a real number\<close>
 
@@ -1084,9 +1238,6 @@
   ultimately show ?thesis ..
 qed
 
-lemma mset_set_upto_eq_mset_upto: "mset_set {..<n} = mset [0..<n]"
-  by (induct n) (auto simp: add.commute lessThan_Suc)
-
 \<comment> \<open>... and derive the existing property:\<close>
 lemma mset_eq_permutation:
   fixes xs ys :: "'a list"