# HG changeset patch
# User huffman
# Date 1261003115 28800
# Node ID d689f0b3304718575726db796aaa457875802698
# Parent  61e19e96828f1fcc6f417719f44bdd566b3cfac4
declare swap_self [simp], add lemma comp_swap

diff -r 61e19e96828f -r d689f0b33047 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Dec 16 15:15:39 2009 +0100
+++ b/src/HOL/Fun.thy	Wed Dec 16 14:38:35 2009 -0800
@@ -458,7 +458,7 @@
 where
   "swap a b f = f (a := f b, b:= f a)"
 
-lemma swap_self: "swap a a f = f"
+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"
@@ -467,6 +467,9 @@
 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
 by (rule ext, simp add: fun_upd_def 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 inj_on_imp_inj_on_swap:
   "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
 by (simp add: inj_on_def swap_def, blast)