--- a/Nominal/ExLet.thy	Thu Mar 25 10:25:33 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 10:44:14 2010 +0100
@@ -42,6 +42,10 @@
   "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
   oops
 
+lemma Lt_subst:
+  "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+  sorry
+
 lemma 
   fixes t::trm
   and   l::lts
@@ -49,7 +53,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, Lt lts trm); \<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; \<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"
@@ -81,43 +85,30 @@
     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 (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+    apply(subgoal_tac "\<exists>q. (bn (permute_bn q (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="Lt (permute_bn q (p \<bullet> lts)) (q \<bullet> p \<bullet> trm)" in subst)
-    defer
+    apply(erule conjE)
+    apply(subst Lt_subst)
+    apply assumption
     apply(rule a4)
-    defer
-    apply(simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_def fresh_def)
     apply(rotate_tac 1)
     apply(drule_tac x="q + p" in meta_spec)
     apply(simp)
+    (*apply(rule at_set_avoiding2)
+    apply(simp add: finite_supp)
+    apply(simp add: supp_Abs)
+    apply(rule finite_Diff)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_star_def fresh_def supp_Abs)*)
     defer
-    apply(simp add: test)
+    apply(simp add: eqvts 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
-    apply(simp add: finite_supp)
-    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)
-    apply(simp)
-    apply(rule a6)
-    apply(simp)
-    apply(simp)
     oops