# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1275570172 -7200
# Node ID dd3b9c046c7d17aa8acf9e37ed6b30184beb4cf7
# Parent  13f20fe02ff36da67ab600c5de8439bc003d661e
added uminus_eqvt

diff -r 13f20fe02ff3 -r dd3b9c046c7d Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Thu Jun 03 11:48:44 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Thu Jun 03 15:02:52 2010 +0200
@@ -385,6 +385,11 @@
   unfolding permute_perm_def
   by (auto simp add: swap_atom expand_perm_eq)
 
+lemma uminus_eqvt:
+  fixes p q::"perm"
+  shows "p \<bullet> (- q) = - (p \<bullet> q)"
+  unfolding permute_perm_def
+  by (simp add: diff_minus minus_add add_assoc)
 
 subsection {* Permutations for functions *}
 
diff -r 13f20fe02ff3 -r dd3b9c046c7d Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Thu Jun 03 11:48:44 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Thu Jun 03 15:02:52 2010 +0200
@@ -295,14 +295,13 @@
   shows "a \<sharp> ()"
   by (simp add: fresh_def supp_unit)
 
-
 section {* additional eqvt lemmas *}
 
 lemmas [eqvt] = 
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt
+  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
 
   (* datatypes *)
   Pair_eqvt permute_list.simps