--- a/Nominal/Ex/Lambda.thy	Tue Jun 07 23:22:58 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 07 23:38:39 2011 +0900
@@ -418,18 +418,25 @@
 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
 
 lemma supp_lookup:
-  shows "supp (lookup xs n x) \<subseteq> supp x"
+  shows "supp (lookup xs n x) \<subseteq> {atom x}"
   apply(induct arbitrary: n rule: lookup.induct)
-  apply(simp add: ln.supp)
+  apply(simp add: ln.supp supp_at_base)
   apply(simp add: ln.supp pure_supp)
   done
-  
+
+lemma supp_lookup_in:
+  shows "x \<in> set xs \<Longrightarrow> supp (lookup xs n x) = {}"
+  by (induct arbitrary: n rule: lookup.induct)(auto simp add: ln.supp pure_supp)
+
+lemma supp_lookup_notin:
+  shows "x \<notin> set xs \<Longrightarrow> supp (lookup xs n x) = {atom x}"
+  by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln.supp pure_supp supp_at_base)
 
 lemma [eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
-nominal_primrec (invariant "\<lambda>x y. supp y \<subseteq> supp x")
+nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
   "trans (Var x) xs = lookup xs 0 x"
@@ -437,7 +444,13 @@
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
 apply(simp add: eqvt_def trans_graph_def)
 apply (rule, perm_simp, rule)
-defer
+  apply (erule trans_graph.induct)
+  apply (case_tac "xa \<in> set xs")
+  apply (simp add: fresh_star_def fresh_def supp_lookup_in)
+  apply (simp add: fresh_star_def fresh_def supp_lookup_notin)
+  apply blast
+  apply (simp add: fresh_star_def ln.fresh)
+  apply (simp add: ln.fresh fresh_star_def)
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -456,14 +469,8 @@
 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
 apply (simp add: eqvt_at_def)
 apply (metis atom_name_def swap_fresh_fresh)
-apply(simp add: fresh_def)
-defer
-apply(erule trans_graph.induct)
-defer
-apply(simp add: lam.supp ln.supp)
-apply(blast)
-apply(simp add: lam.supp ln.supp)
-oops
+apply(simp add: fresh_star_def)
+done
 
 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"
   apply (case_tac "x = xa")