--- a/src/HOL/Fun.thy Wed Apr 16 18:28:13 2014 +0200
+++ b/src/HOL/Fun.thy Wed Apr 16 21:51:41 2014 +0200
@@ -641,17 +641,31 @@
subsection {* @{text swap} *}
-definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
+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)"
-lemma swap_self [simp]: "swap a a f = f"
-by (simp add: swap_def)
+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 (rule ext, simp add: fun_upd_def 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_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"
@@ -659,7 +673,7 @@
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)
+ 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"
@@ -701,6 +715,7 @@
hide_const (open) swap
+
subsection {* Inversion of injective functions *}
definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
--- a/src/HOL/Hilbert_Choice.thy Wed Apr 16 18:28:13 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy Wed Apr 16 21:51:41 2014 +0200
@@ -409,6 +409,13 @@
by auto
qed
+lemma inv_unique_comp:
+ assumes fg: "f \<circ> g = id"
+ and gf: "g \<circ> f = id"
+ shows "inv f = g"
+ using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
+
+
subsection {* The Cantor-Bernstein Theorem *}
lemma Cantor_Bernstein_aux:
--- a/src/HOL/Library/Permutations.thy Wed Apr 16 18:28:13 2014 +0200
+++ b/src/HOL/Library/Permutations.thy Wed Apr 16 21:51:41 2014 +0200
@@ -10,28 +10,16 @@
subsection {* Transpositions *}
-lemma swap_id_refl: "Fun.swap a a id = id"
- by (fact swap_self)
-
-lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
- by (fact swap_commute)
-
-lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
- by (fact swap_commute)
-
-lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
+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 inv_unique_comp:
- assumes fg: "f \<circ> g = id"
- and gf: "g \<circ> f = id"
- shows "inv f = g"
- using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
-
-lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
+lemma inv_swap_id:
+ "inv (Fun.swap a b id) = Fun.swap a b id"
by (rule inv_unique_comp) simp_all
-lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
+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)
@@ -439,7 +427,7 @@
apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
apply (simp_all only: swap_commute)
apply (case_tac "a = c \<and> b = d")
- apply (clarsimp simp only: swapid_sym swap_id_idempotent)
+ apply (clarsimp simp only: swap_commute swap_id_idempotent)
apply (case_tac "a = c \<and> b \<noteq> d")
apply (rule disjI2)
apply (rule_tac x="b" in exI)