# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267538735 -3600
# Node ID 61319a9af976687f7ae2ac6c4178ae7eb428eb76
# Parent  cbcd4997dac54b9adcf0930e9e97d7db607e4df9
updated (added lemma about commuting permutations)

diff -r cbcd4997dac5 -r 61319a9af976 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Mar 02 15:05:35 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 *}