diff -r 81276d5c7438 -r 0acb0b8f4106 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 08 07:02:52 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 08 07:06:20 2011 +0900
@@ -432,7 +432,11 @@
   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]:
+lemma supp_lookup_fresh:
+  shows "atom ` set xs \<sharp>* lookup xs n x"
+  by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin)
+
+lemma lookup_eqvt[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)
 
@@ -442,37 +446,22 @@
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "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)
+  apply (simp add: eqvt_def trans_graph_def)
+  apply (rule, perm_simp, rule)
   apply (erule trans_graph.induct)
-  apply(simp)
-  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 (auto simp add: ln.fresh)
+  apply (simp add: supp_lookup_fresh)
   apply (simp add: fresh_star_def ln.fresh)
-  apply(simp)
   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)
-apply(simp_all add: fresh_star_def)[3]
-apply(blast)
-apply(blast)
-apply(simp_all)
-apply(elim conjE)
-apply clarify
-apply (erule Abs1_eq_fdest)
-apply (simp_all add: ln.fresh)
-prefer 2
-apply(drule supp_eqvt_at)
-apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2]
-prefer 2
-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_star_def)
-done
+  apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply (auto simp add: fresh_star_def)[3]
+  apply (erule Abs1_eq_fdest)
+  apply (simp_all add: fresh_star_def)
+  apply (drule supp_eqvt_at)
+  apply (rule finite_supp)
+  apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1]
+  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  done
 
 
 termination