# HG changeset patch
# User huffman
# Date 1261190907 28800
# Node ID 402b7c74799db70a3a2e17a38d8c8e329c24d053
# Parent  f3fd41b9c017241b51ed465d58b424ada7a284b4
add lemma swap_triple

diff -r f3fd41b9c017 -r 402b7c74799d src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Dec 17 13:51:50 2009 -0800
+++ b/src/HOL/Fun.thy	Fri Dec 18 18:48:27 2009 -0800
@@ -467,6 +467,11 @@
 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
 by (rule ext, simp add: fun_upd_def swap_def)
 
+lemma swap_triple:
+  assumes "a \<noteq> c" and "b \<noteq> c"
+  shows "swap a b (swap b c (swap a b f)) = swap a c f"
+  using assms by (simp add: expand_fun_eq 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)