diff -r a98d03fb9d53 -r cd5a6db05540 Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Mar 25 09:08:42 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 10:25:33 2010 +0100
@@ -38,20 +38,24 @@
   "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)"
   sorry
 
+lemma permute_bn_add:
+  "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
+  oops
+
 lemma 
   fixes t::trm
   and   l::lts
   and   c::"'a::fs"
-  assumes a1: "\<And>name c. P1 c (Vr name)" 
+  assumes a1: "\<And>name c. P1 c (Vr name)"
   and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
-  and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" 
+  and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
   and     a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* (c, Lt lts trm); \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
   and     a5: "\<And>c. P2 c Lnil"
   and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
   shows "P1 c t" and "P2 c l"
 proof -
   have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
-       "(\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> l))"
+       "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
     apply(induct rule: trm_lts.inducts)
     apply(simp)
     apply(rule a1)
@@ -86,14 +90,17 @@
     apply(rule a4)
     defer
     apply(simp add: eqvts)
-    apply(simp add: fresh_star_prod)
-    apply(simp add: fresh_star_def)
-    apply(simp add: fresh_def)
-    apply(simp add: trm_lts.fv[simplified trm_lts.supp])
-    apply(subst permute_plus[symmetric])
-    apply(blast)
-    apply(subst permute_plus[symmetric])
-    apply(blast)
+    apply(rotate_tac 1)
+    apply(drule_tac x="q + p" in meta_spec)
+    apply(simp)
+    defer
+    apply(simp add: test)
+    apply(rule a5)
+    apply(simp add: test)
+    apply(rule a6)
+    apply simp
+    apply simp
+
     apply(rule at_set_avoiding2)
     apply(simp add: finite_supp)
     defer