# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267539180 -3600
# Node ID b7463e5e7d871664f0cfe35a03784f5c35daa9f2
# Parent  c668d65fd98865583a7cb3f1f878aafcee209f0a# Parent  003c7e290a04c890e80e5d427f741a7fb7b0e413
merge

diff -r c668d65fd988 -r b7463e5e7d87 Nominal/Abs.thy
diff -r c668d65fd988 -r b7463e5e7d87 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Mar 02 15:12:50 2010 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Mar 02 15:13:00 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 *}