# HG changeset patch
# User haftmann
# Date 1620230942 0
# Node ID 5020054b3a169782dcfc327f18d7a888140f57d1
# Parent  4dc3baf45d6a5285fef3ef9d952dc52c88e48ffb
tuned theory structure

diff -r 4dc3baf45d6a -r 5020054b3a16 NEWS
--- a/NEWS	Wed May 05 16:09:02 2021 +0000
+++ b/NEWS	Wed May 05 16:09:02 2021 +0000
@@ -94,6 +94,9 @@
 * Lemma "permutes_induct" has been given stronger
 hypotheses and named premises.  INCOMPATIBILITY.
 
+* Combinator "Fun.swap" moved into separate theory "Transposition" in
+HOL-Combinatorics.  INCOMPATIBILITY.
+
 
 *** ML ***
 
diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Wed May 05 16:09:02 2021 +0000
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed May 05 16:09:02 2021 +0000
@@ -10,7 +10,7 @@
 
 theory Cartesian_Space
   imports
-    Finite_Cartesian_Product Linear_Algebra
+    Finite_Cartesian_Product Linear_Algebra "HOL-Combinatorics.Transposition"
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> (*much of the following
diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Combinatorics/Combinatorics.thy
--- a/src/HOL/Combinatorics/Combinatorics.thy	Wed May 05 16:09:02 2021 +0000
+++ b/src/HOL/Combinatorics/Combinatorics.thy	Wed May 05 16:09:02 2021 +0000
@@ -3,6 +3,7 @@
 
 theory Combinatorics
 imports
+  Transposition
   Stirling
   Permutations
   List_Permutation
diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Combinatorics/Perm.thy
--- a/src/HOL/Combinatorics/Perm.thy	Wed May 05 16:09:02 2021 +0000
+++ b/src/HOL/Combinatorics/Perm.thy	Wed May 05 16:09:02 2021 +0000
@@ -3,7 +3,8 @@
 section \<open>Permutations as abstract type\<close>
 
 theory Perm
-imports Main
+  imports
+    Transposition
 begin
 
 text \<open>
diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Wed May 05 16:09:02 2021 +0000
+++ b/src/HOL/Combinatorics/Permutations.thy	Wed May 05 16:09:02 2021 +0000
@@ -7,6 +7,7 @@
   imports
     "HOL-Library.Multiset"
     "HOL-Library.Disjoint_Sets"
+    Transposition
 begin
 
 subsection \<open>Auxiliary\<close>
diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Combinatorics/Transposition.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Combinatorics/Transposition.thy	Wed May 05 16:09:02 2021 +0000
@@ -0,0 +1,110 @@
+section \<open>Transposition function\<close>
+
+theory Transposition
+  imports Main
+begin
+
+setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.qualified_path true \<^binding>\<open>Fun\<close>))\<close>
+
+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>
+
+setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.parent_path))\<close>
+
+lemma swap_apply [simp]:
+  "Fun.swap a b f a = f b"
+  "Fun.swap a b f b = f a"
+  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> Fun.swap a b f c = f c"
+  by (simp_all add: Fun.swap_def)
+
+lemma swap_self [simp]: "Fun.swap a a f = f"
+  by (simp add: Fun.swap_def)
+
+lemma swap_commute: "Fun.swap a b f = Fun.swap b a f"
+  by (simp add: fun_upd_def Fun.swap_def fun_eq_iff)
+
+lemma swap_nilpotent [simp]: "Fun.swap a b (Fun.swap a b f) = f"
+  by (rule ext) (simp add: fun_upd_def Fun.swap_def)
+
+lemma swap_comp_involutory [simp]: "Fun.swap a b \<circ> Fun.swap a b = id"
+  by (rule ext) simp
+
+lemma swap_triple:
+  assumes "a \<noteq> c" and "b \<noteq> c"
+  shows "Fun.swap a b (Fun.swap b c (Fun.swap a b f)) = Fun.swap a c f"
+  using assms by (simp add: fun_eq_iff Fun.swap_def)
+
+lemma comp_swap: "f \<circ> Fun.swap a b g = Fun.swap a b (f \<circ> g)"
+  by (rule ext) (simp add: fun_upd_def Fun.swap_def)
+
+lemma swap_image_eq [simp]:
+  assumes "a \<in> A" "b \<in> A"
+  shows "Fun.swap a b f ` A = f ` A"
+proof -
+  have subset: "\<And>f. Fun.swap a b f ` A \<subseteq> f ` A"
+    using assms by (auto simp: image_iff Fun.swap_def)
+  then have "Fun.swap a b (Fun.swap a b f) ` A \<subseteq> (Fun.swap a b f) ` A" .
+  with subset[of f] show ?thesis by auto
+qed
+
+lemma inj_on_imp_inj_on_swap: "inj_on f A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> inj_on (Fun.swap a b f) A"
+  by (auto simp add: inj_on_def Fun.swap_def)
+
+lemma inj_on_swap_iff [simp]:
+  assumes A: "a \<in> A" "b \<in> A"
+  shows "inj_on (Fun.swap a b f) A \<longleftrightarrow> inj_on f A"
+proof
+  assume "inj_on (Fun.swap a b f) A"
+  with A have "inj_on (Fun.swap a b (Fun.swap a b f)) A"
+    by (iprover intro: inj_on_imp_inj_on_swap)
+  then show "inj_on f A" by simp
+next
+  assume "inj_on f A"
+  with A show "inj_on (Fun.swap a b f) A"
+    by (iprover intro: inj_on_imp_inj_on_swap)
+qed
+
+lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (Fun.swap a b f)"
+  by simp
+
+lemma surj_swap_iff [simp]: "surj (Fun.swap a b f) \<longleftrightarrow> surj f"
+  by simp
+
+lemma bij_betw_swap_iff [simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> bij_betw (Fun.swap x y f) A B \<longleftrightarrow> bij_betw f A B"
+  by (auto simp: bij_betw_def)
+
+lemma bij_swap_iff [simp]: "bij (Fun.swap a b f) \<longleftrightarrow> bij f"
+  by simp
+
+lemma swap_image:
+  \<open>Fun.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: Fun.swap_def)
+
+lemma inv_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
+  by (rule inv_unique_comp) (simp_all add: fun_eq_iff Fun.swap_def)
+
+lemma bij_swap_comp:
+  assumes "bij p"
+  shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
+  using surj_f_inv_f[OF bij_is_surj[OF \<open>bij p\<close>]]
+  by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF \<open>bij p\<close>])
+
+
+subsection \<open>Transpositions\<close>
+
+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>Fun.swap a b p = p \<circ> Fun.swap a b id\<close>
+  by (simp add: fun_eq_iff Fun.swap_def)
+
+lemma swap_id_idempotent [simp]: "Fun.swap a b id \<circ> Fun.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>
+  using that by (rule bij_comp) simp
+
+end
diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed May 05 16:09:02 2021 +0000
+++ b/src/HOL/Fun.thy	Wed May 05 16:09:02 2021 +0000
@@ -855,104 +855,6 @@
   by (simp add: override_on_def fun_eq_iff)
 
 
-subsection \<open>\<open>swap\<close>\<close>
-
-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"
-  "swap a b f b = f a"
-  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> swap a b f c = f c"
-  by (simp_all add: swap_def)
-
-lemma swap_self [simp]: "swap a a f = f"
-  by (simp add: swap_def)
-
-lemma swap_commute: "swap a b f = swap b a f"
-  by (simp add: fun_upd_def swap_def fun_eq_iff)
-
-lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
-  by (rule ext) (simp add: fun_upd_def swap_def)
-
-lemma swap_comp_involutory [simp]: "swap a b \<circ> swap a b = id"
-  by (rule ext) simp
-
-lemma swap_triple:
-  assumes "a \<noteq> c" and "b \<noteq> c"
-  shows "swap a b (swap b c (swap a b f)) = swap a c f"
-  using assms by (simp add: fun_eq_iff swap_def)
-
-lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
-  by (rule ext) (simp add: fun_upd_def swap_def)
-
-lemma swap_image_eq [simp]:
-  assumes "a \<in> A" "b \<in> A"
-  shows "swap a b f ` A = f ` A"
-proof -
-  have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A"
-    using assms by (auto simp: image_iff swap_def)
-  then have "swap a b (swap a b f) ` A \<subseteq> (swap a b f) ` A" .
-  with subset[of f] show ?thesis by auto
-qed
-
-lemma inj_on_imp_inj_on_swap: "inj_on f A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> inj_on (swap a b f) A"
-  by (auto simp add: inj_on_def swap_def)
-
-lemma inj_on_swap_iff [simp]:
-  assumes A: "a \<in> A" "b \<in> A"
-  shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
-proof
-  assume "inj_on (swap a b f) A"
-  with A have "inj_on (swap a b (swap a b f)) A"
-    by (iprover intro: inj_on_imp_inj_on_swap)
-  then show "inj_on f A" by simp
-next
-  assume "inj_on f A"
-  with A show "inj_on (swap a b f) A"
-    by (iprover intro: inj_on_imp_inj_on_swap)
-qed
-
-lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
-  by simp
-
-lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
-  by simp
-
-lemma bij_betw_swap_iff [simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
-  by (auto simp: bij_betw_def)
-
-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_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_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 (swap a b id \<circ> p)\<close> if \<open>bij p\<close>
-  using that by (rule bij_comp) simp
-
-end
-
-
 subsection \<open>Inversion of injective functions\<close>
 
 definition the_inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed May 05 16:09:02 2021 +0000
+++ b/src/HOL/Hilbert_Choice.thy	Wed May 05 16:09:02 2021 +0000
@@ -636,15 +636,6 @@
   shows "inv f = g"
   using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
 
-lemma inv_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
-  by (rule inv_unique_comp) simp_all
-
-lemma bij_swap_comp:
-  assumes "bij p"
-  shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
-  using surj_f_inv_f[OF bij_is_surj[OF \<open>bij p\<close>]]
-  by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF \<open>bij p\<close>])
-
 lemma subset_image_inj:
   "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)"
 proof safe