# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1344354917 -3600
# Node ID deef21dc972f6fc14d4eb6482d92b528d29f3a0d
# Parent  6454435d689be893f5894af05b01dbba581597ba
added eqvt-lemma for function composition

diff -r 6454435d689b -r deef21dc972f Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Aug 06 13:50:19 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Aug 07 16:55:17 2012 +0100
@@ -1046,9 +1046,6 @@
   apply(simp)
   done
 
-thm eqvts_raw
-
-
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
@@ -1131,8 +1128,12 @@
 lemma fun_upd_eqvt[eqvt]:
   shows "p \<bullet> (f(x := y)) = (p \<bullet> f)((p \<bullet> x) := (p \<bullet> y))"
 unfolding fun_upd_def
-by (simp)
-
+by simp
+
+lemma comp_eqvt [eqvt]:
+  shows "p \<bullet> (f \<circ> g) = (p \<bullet> f) \<circ> (p \<bullet> g)"
+unfolding comp_def
+by simp
 
 subsubsection {* Equivariance for product operations *}