# HG changeset patch
# User urbanc
# Date 1140027070 -3600
# Node ID 75786c2eb897d1d7130f1e928dd46a65a2e3f20f
# Parent  d4bc0ee9383a77ee93688a3fc5d27acf0749d411
added lemma pt_perm_compose'

diff -r d4bc0ee9383a -r 75786c2eb897 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Feb 15 19:01:09 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Feb 15 19:11:10 2006 +0100
@@ -1357,6 +1357,21 @@
   thus ?thesis by (simp add: pt2[OF pt])
 qed
 
+lemma pt_perm_compose':
+  fixes pi1 :: "'x prm"
+  and   pi2 :: "'x prm"
+  and   x  :: "'a"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "(pi2\<bullet>pi1)\<bullet>x = pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x))" 
+proof -
+  have "pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x)) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>((rev pi2)\<bullet>x))"
+    by (rule pt_perm_compose[OF pt, OF at])
+  also have "\<dots> = (pi2\<bullet>pi1)\<bullet>x" by (simp add: pt_pi_rev[OF pt, OF at])
+  finally have "pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x)) = (pi2\<bullet>pi1)\<bullet>x" by simp
+  thus ?thesis by simp
+qed
+
 lemma pt_perm_compose_rev:
   fixes pi1 :: "'x prm"
   and   pi2 :: "'x prm"
@@ -1545,7 +1560,7 @@
   by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])
 
 
---"sometimes pt_fun_app_eq does to much; this lemma 'corrects it'"
+--"sometimes pt_fun_app_eq does too much; this lemma 'corrects it'"
 lemma pt_perm:
   fixes x  :: "'a"
   and   pi1 :: "'x prm"