# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267538847 -3600
# Node ID 003c7e290a04c890e80e5d427f741a7fb7b0e413
# Parent  e965524c3301f6c66b491952d674a57082342f46# Parent  dc65319809cc460b4204f71b9493aaf91194ec47
merged

diff -r dc65319809cc -r 003c7e290a04 Nominal/Abs.thy
diff -r dc65319809cc -r 003c7e290a04 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Mar 02 14:51:40 2010 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Mar 02 15:07:27 2010 +0100
@@ -889,6 +889,37 @@
 instance perm :: fs
 by default (simp add: supp_perm finite_perm_lemma)
 
+lemma plus_perm_eq:
+  fixes p q::"perm"
+  assumes asm: "supp p \<inter>  supp q = {}"
+  shows "p + q  = q + p"
+unfolding expand_perm_eq
+proof
+  fix a::"atom"
+  show "(p + q) \<bullet> a = (q + p) \<bullet> a"
+  proof -
+    { assume "a \<notin> supp p" "a \<notin> supp q"
+      then have "(p + q) \<bullet> a = (q + p) \<bullet> a" 
+	by (simp add: supp_perm)
+    }
+    moreover
+    { assume a: "a \<in> supp p" "a \<notin> supp q"
+      then have "p \<bullet> a \<in> supp p" by (simp add: supp_perm)
+      then have "p \<bullet> a \<notin> supp q" using asm by auto
+      with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" 
+	by (simp add: supp_perm)
+    }
+    moreover
+    { assume a: "a \<notin> supp p" "a \<in> supp q"
+      then have "q \<bullet> a \<in> supp q" by (simp add: supp_perm)
+      then have "q \<bullet> a \<notin> supp p" using asm by auto 
+      with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" 
+	by (simp add: supp_perm)
+    }
+    ultimately show "(p + q) \<bullet> a = (q + p) \<bullet> a" 
+      using asm by blast
+  qed
+qed
 
 section {* Finite Support instances for other types *}