# HG changeset patch
# User haftmann
# Date 1397677901 -7200
# Node ID 8e3c848008fa1cb03072898b04e30dcd6fcf815d
# Parent  ab7c656215f2dceae27532927600f34a356ea40b
more simp rules for Fun.swap

diff -r ab7c656215f2 -r 8e3c848008fa src/HOL/Fun.thy
--- 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
diff -r ab7c656215f2 -r 8e3c848008fa src/HOL/Hilbert_Choice.thy
--- 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:
diff -r ab7c656215f2 -r 8e3c848008fa src/HOL/Library/Permutations.thy
--- 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)