# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1297867473 0
# Node ID fafc461bdb9eb7124eef7dad0822e5ac2cd4b52e
# Parent  e6bf6790da7d9c11ccfee1208dfa8ccba19516a7
added eqvt for length

diff -r e6bf6790da7d -r fafc461bdb9e Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Wed Feb 16 14:03:26 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Feb 16 14:44:33 2011 +0000
@@ -275,6 +275,10 @@
 apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
 done
 
+lemma length_eqvt[eqvt]:
+  shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
+by (induct xs) (simp_all add: permute_pure)
+
 
 subsection {* Equivariance Finite-Set Operations *}