1.1 --- a/src/HOL/Fun.thy	Wed Dec 16 15:15:39 2009 +0100
     1.2 +++ b/src/HOL/Fun.thy	Wed Dec 16 14:38:35 2009 -0800
     1.3 @@ -458,7 +458,7 @@
     1.4  where
     1.5    "swap a b f = f (a := f b, b:= f a)"
     1.6  
     1.7 -lemma swap_self: "swap a a f = f"
     1.8 +lemma swap_self [simp]: "swap a a f = f"
     1.9  by (simp add: swap_def)
    1.10  
    1.11  lemma swap_commute: "swap a b f = swap b a f"
    1.12 @@ -467,6 +467,9 @@
    1.13  lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
    1.14  by (rule ext, simp add: fun_upd_def swap_def)
    1.15  
    1.16 +lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
    1.17 +by (rule ext, simp add: fun_upd_def swap_def)
    1.18 +
    1.19  lemma inj_on_imp_inj_on_swap:
    1.20    "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
    1.21  by (simp add: inj_on_def swap_def, blast)