author urbanc Wed, 15 Feb 2006 19:11:10 +0100 changeset 19045 75786c2eb897 parent 19044 d4bc0ee9383a child 19046 bc5c6c9b114e
```--- 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"```