src/HOL/Fun.thy
changeset 34145 402b7c74799d
parent 34101 d689f0b33047
child 34153 5da0f7abbe29
     1.1 --- a/src/HOL/Fun.thy	Thu Dec 17 13:51:50 2009 -0800
     1.2 +++ b/src/HOL/Fun.thy	Fri Dec 18 18:48:27 2009 -0800
     1.3 @@ -467,6 +467,11 @@
     1.4  lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
     1.5  by (rule ext, simp add: fun_upd_def swap_def)
     1.6  
     1.7 +lemma swap_triple:
     1.8 +  assumes "a \<noteq> c" and "b \<noteq> c"
     1.9 +  shows "swap a b (swap b c (swap a b f)) = swap a c f"
    1.10 +  using assms by (simp add: expand_fun_eq swap_def)
    1.11 +
    1.12  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
    1.13  by (rule ext, simp add: fun_upd_def swap_def)
    1.14