diff -r 36798cdbc452 -r a98d03fb9d53 Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Mar 25 08:05:03 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 09:08:42 2010 +0100
@@ -30,6 +30,14 @@
 thm trm_lts.distinct
 thm trm_lts.fv[simplified trm_lts.supp]
 
+consts
+  permute_bn :: "perm \<Rightarrow> lts \<Rightarrow> lts"
+
+lemma test:
+  "permute_bn pi (Lnil) = Lnil"
+  "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)"
+  sorry
+
 lemma 
   fixes t::trm
   and   l::lts
@@ -37,7 +45,7 @@
   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     a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts 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"
@@ -69,15 +77,19 @@
     apply(simp add: fresh_def)
     apply(simp add: trm_lts.fv[simplified trm_lts.supp])
     apply(simp)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Lt (p \<bullet> lts) (p \<bullet> trm)) \<sharp>* q")
+    apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
     apply(erule exE)
+    (* HERE *)
     apply(rule_tac t="Lt (p \<bullet> lts) (p \<bullet> trm)" 
-               and s="q \<bullet> Lt (p \<bullet> lts) (p \<bullet> trm)" in subst)
-    apply(rule supp_perm_eq)
-    apply(simp)
-    apply(simp)
+               and s="Lt (permute_bn q (p \<bullet> lts)) (q \<bullet> p \<bullet> trm)" in subst)
+    defer
     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])
@@ -89,7 +101,9 @@
     apply(simp add: finite_supp)
     apply(simp add: fresh_star_def)
     apply(simp add: fresh_def)
+    thm trm_lts.fv[simplified trm_lts.supp]
     apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+    apply(simp add: alpha_bn_eq_iff)
     defer
     apply(simp)
     apply(rule a5)