# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1336852440 -3600
# Node ID c25386402f6a97596607410bde151f74e5366541
# Parent  51c475ceaf09c16d732ce2be1d2c7c764a5aa5c9
added a lemma about composition and permutations

diff -r 51c475ceaf09 -r c25386402f6a Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue May 01 12:16:04 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Sat May 12 20:54:00 2012 +0100
@@ -405,6 +405,9 @@
   shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
   unfolding permute_fun_def by simp
 
+lemma permute_fun_comp:
+  shows "p \<bullet> f  = (permute p) o f o (permute (-p))"
+by (simp add: comp_def permute_fun_def)
 
 subsection {* Permutations for booleans *}