--- a/Nominal/Nominal2_Base.thy	Thu Feb 24 18:50:02 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Fri Feb 25 21:23:30 2011 +0000
@@ -146,7 +146,8 @@
 
 instance perm :: size ..
 
-subsection {* Permutations form a group *}
+subsection {* Permutations form a (multiplicative) group *}
+
 
 instantiation perm :: group_add
 begin
@@ -343,7 +344,7 @@
   "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> c = c"
   unfolding swap_atom by simp_all
 
-lemma expand_perm_eq:
+lemma perm_eq_iff:
   fixes p q :: "perm"
   shows "p = q \<longleftrightarrow> (\<forall>a::atom. p \<bullet> a = q \<bullet> a)"
   unfolding permute_atom_def
@@ -371,6 +372,11 @@
   unfolding permute_perm_def 
   by (simp add: diff_minus add_assoc)
 
+lemma pemute_minus_self:
+  shows "- p \<bullet> p = p"
+  unfolding permute_perm_def 
+  by (simp add: diff_minus add_assoc)
+
 lemma permute_eqvt:
   shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"
   unfolding permute_perm_def by simp
@@ -383,12 +389,12 @@
   fixes p p1 p2 :: perm
   shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2"
   unfolding permute_perm_def
-  by (simp add: expand_perm_eq)
+  by (simp add: perm_eq_iff)
 
 lemma swap_eqvt:
   shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)"
   unfolding permute_perm_def
-  by (auto simp add: swap_atom expand_perm_eq)
+  by (auto simp add: swap_atom perm_eq_iff)
 
 lemma uminus_eqvt:
   fixes p q::"perm"
@@ -477,7 +483,6 @@
 
 lemma permute_set_eq:
   fixes x::"'a::pt"
-  and   p::"perm"
   shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
   unfolding permute_fun_def
   unfolding permute_bool_def
@@ -767,13 +772,13 @@
 where
   "supp x = {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}}"
 
-end
-
 definition
-  fresh :: "atom \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp> _" [55, 55] 55)
+  fresh :: "atom \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [55, 55] 55)
 where   
   "a \<sharp> x \<equiv> a \<notin> supp x"
 
+end
+
 lemma supp_conv_fresh: 
   shows "supp x = {a. \<not> a \<sharp> x}"
   unfolding fresh_def by simp
@@ -881,7 +886,7 @@
   then obtain a where b1: "a \<in> supp x" and b2: "a \<notin> S" by auto
   from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" unfolding supports_def by auto
   then have "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto
-  with a2 have "finite {b. (a \<rightleftharpoons> b)\<bullet>x \<noteq> x}" by (simp add: finite_subset)
+  with a2 have "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" by (simp add: finite_subset)
   then have "a \<notin> (supp x)" unfolding supp_def by simp
   with b1 show False by simp
 qed
@@ -1026,7 +1031,7 @@
 apply (rule supports_perm)
 apply (rule finite_perm_lemma)
 apply (simp add: perm_swap_eq swap_eqvt)
-apply (auto simp add: expand_perm_eq swap_atom)
+apply (auto simp add: perm_eq_iff swap_atom)
 done
 
 lemma fresh_perm: 
@@ -1081,7 +1086,7 @@
   fixes p q::"perm"
   assumes asm: "supp p \<inter> supp q = {}"
   shows "p + q  = q + p"
-unfolding expand_perm_eq
+unfolding perm_eq_iff
 proof
   fix a::"atom"
   show "(p + q) \<bullet> a = (q + p) \<bullet> a"
@@ -1273,7 +1278,7 @@
   shows "a \<sharp> f x"
   using assms
   unfolding fresh_conv_MOST
-  unfolding permute_fun_app_eq 
+  unfolding permute_fun_app_eq
   by (elim MOST_rev_mp, simp)
 
 lemma supp_fun_app:
@@ -1282,7 +1287,8 @@
   unfolding fresh_def
   by auto
 
-text {* Equivariant Functions *}
+
+subsection {* Equivariance *}
 
 definition
   "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
@@ -1311,6 +1317,7 @@
 qed
 
 text {* equivariance of a function at a given argument *}
+
 definition
  "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
 
@@ -1771,7 +1778,7 @@
     then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
     have as: "supp p \<subseteq> S" by fact
     { assume "supp p = {}"
-      then have "p = 0" by (simp add: supp_perm expand_perm_eq)
+      then have "p = 0" by (simp add: supp_perm perm_eq_iff)
       then have "P p" using zero by simp
     }
     moreover
@@ -1790,7 +1797,7 @@
       have "supp ?q \<subseteq> S" using as a2 by simp
       ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 
       moreover 
-      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
+      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: perm_eq_iff)
       ultimately have "P p" by simp
     }
     ultimately show "P p" by blast