# HG changeset patch
# User urbanc
# Date 1178062943 -7200
# Node ID f1db55c7534dd70cdb9c2790eb13a7f28c6486c7
# Parent  2064f0fd20c92b40c79a811c72c23bdedbcd2ac2
tuned some proofs and changed variable names in some definitions of Nominal.thy

diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Wed May 02 01:42:23 2007 +0200
@@ -4,15 +4,19 @@
 imports Lam_Funs
 begin
 
-text {* The Church-Rosser proof from a paper by Masako Takahashi;
-        our formalisation follows with some slight exceptions the one 
-        done by Randy Pollack and James McKinna from their 1993 
-        TLCA-paper; the proof is simpler by using an auxiliary
-        reduction relation called complete development reduction.
-      
-        Authors: Mathilde Arnaud and Christian Urban
-     *}
+text {* Authors: Mathilde Arnaud and Christian Urban
+
+        The Church-Rosser proof from a paper by Masako Takahashi.
+        This formalisation follows with some very slight exceptions 
+        the one  given by Randy Pollack in his paper:
 
+             Polishing Up the Tait-Martin Löf Proof of the 
+             Church-Rosser Theorem (1995).
+
+  *}
+
+section {* Lemmas about Capture-Avoiding Substitution *}
+ 
 lemma forget:
   assumes asm: "x\<sharp>L"
   shows "L[x::=P] = L"
@@ -43,6 +47,14 @@
 by (nominal_induct M avoiding: x y N L rule: lam.induct)
    (auto simp add: fresh_fact forget)
 
+lemma subst_rename: 
+  assumes a: "c\<sharp>t1"
+  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
+using a
+by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
+   (auto simp add: calc_atm fresh_atm abs_fresh)
+
+
 section {* Beta Reduction *}
 
 inductive2
@@ -58,10 +70,12 @@
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
+section {* Transitive Closure of Beta *}
+
 inductive2
   "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
 where
-    bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
+    bs1[intro,simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
   | bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
 
 equivariance Beta_star
@@ -103,6 +117,8 @@
 by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
    (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
 
+section {* Transitive Closure of One *}
+
 inductive2
   "One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
 where
@@ -127,33 +143,22 @@
 by (nominal_induct avoiding: a rule: One.strong_induct)
    (auto simp add: abs_fresh fresh_atm fresh_fact)
 
-lemma subst_rename: 
-  assumes a: "c\<sharp>t1"
-  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
-using a
-by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
-   (auto simp add: calc_atm fresh_atm abs_fresh)
+section {* Elimination Rules for One *}
 
 lemma one_var:
   assumes a: "Var x \<longrightarrow>\<^isub>1 t"
   shows "t = Var x"
 using a
-by - (ind_cases2 "Var x \<longrightarrow>\<^isub>1 t", simp)
+by (erule_tac One.cases) (simp_all) 
 
 lemma one_abs: 
-  fixes    t :: "lam"
-  and      t':: "lam"
-  and      a :: "name"
   assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
-  using a
-  apply -
-  apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
+using a
+  apply(erule_tac One.cases)
   apply(auto simp add: lam.inject alpha)
   apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
-  apply(rule conjI)
-  apply(perm_simp)
-  apply(simp add: fresh_left calc_atm)
+  apply(perm_simp add: fresh_left calc_atm)
   apply(simp add: One.eqvt)
   apply(simp add: one_fresh_preserv)
 done  
@@ -163,8 +168,7 @@
   shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
          (\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   using a
-  apply -
-  apply(ind_cases2 "App t1 t2 \<longrightarrow>\<^isub>1 t'")
+  apply(erule_tac One.cases)
   apply(auto simp add: lam.distinct lam.inject)
   done
 
@@ -173,8 +177,7 @@
   shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
          (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   using a
-  apply -
-  apply(ind_cases2 "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
+  apply(erule_tac One.cases)
   apply(simp_all add: lam.inject)
   apply(force)
   apply(erule conjE)
@@ -201,7 +204,7 @@
   apply(simp add: One.eqvt)
   done
 
-text {* complete development reduction *}
+text {* Complete Development Reduction *}
 
 inductive2
   cd1 :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ >c _" [80,80]80)
@@ -227,12 +230,9 @@
   obtain c::"name" where fs: "c\<sharp>(a,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp,blast)
   have eq1: "Lam [a].t1 = Lam [c].([(c,a)]\<bullet>t1)" using fs
     by (rule_tac sym, auto simp add: lam.inject alpha fresh_prod fresh_atm)
-  have "App (Lam [a].t1) s1 = App (Lam [c].([(c,a)]\<bullet>t1)) s1"
-    using eq1 by simp
-  also have "\<dots> >c  ([(c,a)]\<bullet>t2)[c::=s2]" using fs a b
-    by (rule_tac cd1r, simp_all add: cd1.eqvt)
-  also have "\<dots> = t2[a::=s2]" using fs 
-    by (rule_tac subst_rename[symmetric], simp)
+  have "App (Lam [a].t1) s1 = App (Lam [c].([(c,a)]\<bullet>t1)) s1" using eq1 by simp
+  also have "\<dots> >c  ([(c,a)]\<bullet>t2)[c::=s2]" using fs a b by (simp_all add: cd1.eqvt)
+  also have "\<dots> = t2[a::=s2]" using fs  by (rule_tac subst_rename[symmetric], simp)
   finally show "App (Lam [a].t1) s1 >c (t2[a::=s2])" by simp
 qed
 
@@ -242,19 +242,15 @@
   and     b: "s1 >c s2"
   shows "a\<sharp>s2"
 using b a
-by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
-
+ by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
   
 lemma cd1_lam:
-  fixes c::"'a::fs_name"
   assumes a: "Lam [a].t >c t'"
   shows "\<exists>s. t'=Lam [a].s \<and> t >c s"
 using a
 apply -
 apply(erule cd1.cases)
-apply(simp_all)
-apply(simp add: lam.inject)
-apply(simp add: alpha)
+apply(simp_all add: lam.inject alpha)
 apply(auto)
 apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
 apply(perm_simp add: fresh_left cd1.eqvt cd1_fresh_preserve)
@@ -289,32 +285,19 @@
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)"
   using a
-proof induct
-  case bs1 thus ?case by simp
-next
-  case (bs2 y z) 
-  thus ?case by (blast dest: b3)
-qed
+by (induct) (blast)+
 
 lemma one_app_congL: 
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
   using a
-proof induct
-  case bs1 thus ?case by simp
-next
-  case bs2 thus ?case by (blast dest: b1)
-qed
+by (induct) (blast)+
   
 lemma one_app_congR: 
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
 using a
-proof induct
-  case bs1 thus ?case by simp
-next 
-  case bs2 thus ?case by (blast dest: b2)
-qed
+by (induct) (blast)+
 
 lemma one_app_cong: 
   assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
@@ -324,7 +307,7 @@
   have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL)
   moreover
   have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR)
-  ultimately show ?thesis by (rule beta_star_trans)
+  ultimately show "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" by (rule beta_star_trans)
 qed
 
 lemma one_beta_star: 
diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Wed May 02 01:42:23 2007 +0200
@@ -1,6 +1,6 @@
 (* $Id$ *)
 
-(* A challenge suggested by Adam Chlipala *)
+(* The definitions for a challenge suggested by Adam Chlipala *)
 
 theory Compile
 imports "../Nominal"
@@ -8,51 +8,58 @@
 
 atom_decl name 
 
-nominal_datatype data = DNat
-                      | DProd "data" "data"
-                      | DSum "data" "data"
+nominal_datatype data = 
+    DNat
+  | DProd "data" "data"
+  | DSum "data" "data"
 
-nominal_datatype ty = Data "data"
-                    | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype ty = 
+    Data "data"
+  | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
 
-nominal_datatype trm = Var "name"
-                     | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
-                     | App "trm" "trm"
-                     | Const "nat"
-                     | Pr "trm" "trm"
-                     | Fst "trm"
-                     | Snd "trm"
-                     | InL "trm"
-                     | InR "trm"
-                     | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" 
-                             ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100)
+nominal_datatype trm = 
+  Var "name"
+  | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+  | App "trm" "trm"
+  | Const "nat"
+  | Pr "trm" "trm"
+  | Fst "trm"
+  | Snd "trm"
+  | InL "trm"
+  | InR "trm"
+  | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" 
+          ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100)
 
 nominal_datatype dataI = OneI | NatI
 
-nominal_datatype tyI = DataI "dataI"
-                     | ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype tyI = 
+    DataI "dataI"
+  | ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100)
 
-nominal_datatype trmI = IVar "name"
-                      | ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100)
-                      | IApp "trmI" "trmI"
-                      | IUnit
-                      | INat "nat"
-                      | ISucc "trmI"
-                      | IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100)
-                      | IRef "trmI" 
-                      | ISeq "trmI" "trmI" ("_;;_" [100,100] 100)
-                      | Iif "trmI" "trmI" "trmI"
+nominal_datatype trmI = 
+    IVar "name"
+  | ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100)
+  | IApp "trmI" "trmI"
+  | IUnit
+  | INat "nat"
+  | ISucc "trmI"
+  | IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100)
+  | IRef "trmI" 
+  | ISeq "trmI" "trmI" ("_;;_" [100,100] 100)
+  | Iif "trmI" "trmI" "trmI"
 
 text {* valid contexts *}
 
-inductive2 valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
+inductive2 
+  valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
 where
   v1[intro]: "valid []"
 | v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *)
 
 text {* typing judgements for trms *}
 
-inductive2 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+inductive2 
+  typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
 where
   t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
 | t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
@@ -69,7 +76,8 @@
 
 text {* typing judgements for Itrms *}
 
-inductive2 Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
+inductive2 
+  Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
 where
   t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
 | t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2"
@@ -159,7 +167,8 @@
 
 text {* big-step evaluation for trms *}
 
-inductive2 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
+inductive2 
+  big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
 where
   b0[intro]: "Lam [x].e \<Down> Lam [x].e"
 | b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'"
@@ -172,7 +181,8 @@
 | b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
 | b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
 
-inductive2 Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
+inductive2 
+  Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
 where
   m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
 | m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk> 
diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed May 02 01:42:23 2007 +0200
@@ -14,15 +14,17 @@
 
 atom_decl name 
 
-nominal_datatype ty = TBase 
-                    | TUnit 
-                    | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype ty = 
+    TBase 
+  | TUnit 
+  | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
 
-nominal_datatype trm = Unit
-                     | Var "name"
-                     | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
-                     | App "trm" "trm"
-                     | Const "nat"
+nominal_datatype trm = 
+    Unit
+  | Var "name"
+  | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+  | App "trm" "trm"
+  | Const "nat"
 
 types Ctxt  = "(name\<times>ty) list"
 types Subst = "(name\<times>trm) list" 
diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Wed May 02 01:42:23 2007 +0200
@@ -8,9 +8,10 @@
 
 atom_decl name
 
-nominal_datatype lam = Var "name"
-                     | App "lam" "lam"
-                     | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+nominal_datatype lam = 
+    Var "name"
+  | App "lam" "lam"
+  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
 text {* definition of the height-function on lambda-terms *} 
 
diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Wed May 02 01:42:23 2007 +0200
@@ -6,9 +6,10 @@
 
 atom_decl name
 
-nominal_datatype lam = Var "name"
-                     | App "lam" "lam"
-                     | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+nominal_datatype lam = 
+    Var "name"
+  | App "lam" "lam"
+  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
 text {* depth of a lambda-term *}
 
diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/Lambda_mu.thy
--- a/src/HOL/Nominal/Examples/Lambda_mu.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy	Wed May 02 01:42:23 2007 +0200
@@ -8,10 +8,11 @@
 
 atom_decl var mvar
 
-nominal_datatype trm = Var   "var" 
-                     | Lam  "\<guillemotleft>var\<guillemotright>trm"   ("Lam [_]._" [100,100] 100)
-                     | App  "trm" "trm" 
-                     | Pss  "mvar" "trm"
-                     | Act  "\<guillemotleft>mvar\<guillemotright>trm"  ("Act [_]._" [100,100] 100)
+nominal_datatype trm = 
+    Var   "var" 
+  | Lam  "\<guillemotleft>var\<guillemotright>trm"   ("Lam [_]._" [100,100] 100)
+  | App  "trm" "trm" 
+  | Pss  "mvar" "trm"
+  | Act  "\<guillemotleft>mvar\<guillemotright>trm"  ("Act [_]._" [100,100] 100)
 
 end
diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Wed May 02 01:42:23 2007 +0200
@@ -31,7 +31,7 @@
 
 (* permutation on sets *)
 defs (unchecked overloaded)
-  perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
+  perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>x | x. x\<in>X}"
 
 lemma empty_eqvt:
   shows "pi\<bullet>{} = {}"
@@ -50,7 +50,7 @@
   "pi\<bullet>()    = ()"
   
 primrec (unchecked perm_prod)
-  "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"
+  "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
 
 lemma fst_eqvt:
   "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
@@ -1171,7 +1171,7 @@
   and   y  :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "pi \<bullet> (x=y) = (pi\<bullet>x = pi\<bullet>y)"
+  shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)"
 using assms
 by (auto simp add: pt_bij perm_bool)
 
@@ -1309,9 +1309,18 @@
   and   pi::"'x prm"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "pi \<bullet> (X - Y) = (pi \<bullet> X) - (pi \<bullet> Y)"
+  shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
   by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
 
+lemma pt_Collect_eqvt:
+  fixes pi::"'x prm"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
+apply(auto simp add: perm_set_def  pt_rev_pi[OF pt, OF at])
+apply(rule_tac x="(rev pi)\<bullet>x" in exI)
+apply(simp add: pt_pi_rev[OF pt, OF at])
+done
 
 -- "some helper lemmas for the pt_perm_supp_ineq lemma"
 lemma Collect_permI: 
@@ -1596,15 +1605,15 @@
   and   x  :: "'y"
   assumes pt: "pt TYPE('y) TYPE('x)"
   and     at: "at TYPE('x)"
-  and     h1: "a \<sharp> pi"
-  and     h2: "a \<sharp> x"
-  shows "a \<sharp> (pi \<bullet> x)"
+  and     h1: "a\<sharp>pi"
+  and     h2: "a\<sharp>x"
+  shows "a\<sharp>(pi\<bullet>x)"
 using assms
 proof -
-  have "a \<sharp> rev pi"using h1 by (simp add: fresh_list_rev)
-  then have "(rev pi) \<bullet> a = a" by (simp add: at_prm_fresh[OF at])
-  then have "((rev pi) \<bullet> a) \<sharp> x" using h2 by simp
-  thus "a \<sharp> (pi \<bullet> x)"  by (simp add: pt_fresh_right[OF pt, OF at])
+  have "a\<sharp>(rev pi)"using h1 by (simp add: fresh_list_rev)
+  then have "(rev pi)\<bullet>a = a" by (simp add: at_prm_fresh[OF at])
+  then have "((rev pi)\<bullet>a)\<sharp>x" using h2 by simp
+  thus "a\<sharp>(pi\<bullet>x)"  by (simp add: pt_fresh_right[OF pt, OF at])
 qed
 
 lemma pt_fresh_perm_app_ineq:
@@ -2127,11 +2136,11 @@
     case goal1
     show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
       apply(auto simp add: perm_set_def)
-      apply(rule_tac x="pi\<bullet>xa" in exI)
+      apply(rule_tac x="pi\<bullet>xb" in exI)
       apply(rule conjI)
-      apply(rule_tac x="xa" in exI)
+      apply(rule_tac x="xb" in exI)
       apply(simp)
-      apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xa) = pi\<bullet>(f xa)")(*A*)
+      apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xb) = pi\<bullet>(f xb)")(*A*)
       apply(simp)
       apply(rule pt_set_bij2[OF pt_x, OF at])
       apply(assumption)
@@ -2146,7 +2155,7 @@
       apply(rule_tac x="(rev pi)\<bullet>x" in exI)
       apply(rule conjI)
       apply(simp add: pt_pi_rev[OF pt_x, OF at])
-      apply(rule_tac x="a" in bexI)
+      apply(rule_tac x="xb" in bexI)
       apply(simp add: pt_set_bij1[OF pt_x, OF at])
       apply(simp add: pt_fun_app_eq[OF pt, OF at])
       apply(assumption)
@@ -2177,7 +2186,7 @@
   apply(erule conjE)
   apply(simp add: perm_set_def)
   apply(auto)
-  apply(subgoal_tac "[(a,b)]\<bullet>aa = aa")(*A*)
+  apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
   apply(simp)
   apply(rule pt_fresh_fresh[OF pt, OF at])
   apply(force)
@@ -2351,7 +2360,7 @@
 apply(simp add: cp_def)
 apply(auto)
 apply(auto simp add: perm_set_def)
-apply(rule_tac x="pi2\<bullet>aa" in exI)
+apply(rule_tac x="pi2\<bullet>xc" in exI)
 apply(auto)
 done