--- 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 ***
--- 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
--- 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
--- 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>
--- 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>
--- /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
--- 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)"
--- 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