add lemma swap_triple
authorhuffman
Fri Dec 18 18:48:27 2009 -0800 (2009-12-18)
changeset 34145402b7c74799d
parent 34114 f3fd41b9c017
child 34146 14595e0c27e8
add lemma swap_triple
src/HOL/Fun.thy
     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