--- a/Nominal/Ex/Lambda.thy	Thu Jun 09 15:03:58 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 09 15:34:51 2011 +0900
@@ -618,6 +618,14 @@
 apply(simp_all add: permute_pure)
 done
 
+lemma supp_subst:
+  "supp (t[x ::= s]) \<subseteq> supp t \<union> supp s"
+  by (induct t x s rule: subst.induct) (auto simp add: lam.supp)
+
+lemma var_fresh_subst:
+  "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"
+  by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base)
+
 (* function that evaluates a lambda term *)
 nominal_primrec
    eval :: "lam \<Rightarrow> lam" and
@@ -628,14 +636,45 @@
 | "eval (App t1 t2) = sub (eval t1) (eval t2)"
 | "app (Var x) t2 = App (Var x) t2"
 | "app (App t0 t1) t2 = App (App t0 t1) t2"
-| "app (Lam [x].t1) t2 = eval (t1[x::= t2])"
+| "atom x \<sharp> t2 \<Longrightarrow> app (Lam [x].t1) t2 = eval (t1[x::= t2])"
 apply(simp add: eval_app_graph_def eqvt_def)
-apply(perm_simp)
-apply(simp)
+apply(rule, perm_simp, rule)
 apply(rule TrueI)
-defer
+apply (case_tac x)
+apply (case_tac a rule: lam.exhaust)
+apply simp_all[3]
+apply blast
+apply (case_tac b)
+apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
+apply simp_all[3]
+apply blast
+apply blast
+apply (simp add: Abs1_eq_iff fresh_star_def)
 apply(simp_all)
+apply(erule Abs1_eq_fdest)
+apply (simp add: Abs_fresh_iff)
+apply (simp add: Abs_fresh_iff)
+apply (erule fresh_eqvt_at)
+apply (simp add: finite_supp)
+apply (simp add: fresh_Inl)
+apply (simp add: eqvt_at_def)
+apply simp
 defer
+apply clarify
+apply(erule Abs1_eq_fdest)
+apply (erule fresh_eqvt_at)
+apply (simp add: finite_supp)
+apply (simp add: fresh_Inl var_fresh_subst)
+apply (erule fresh_eqvt_at)
+apply (simp add: finite_supp)
+apply (simp add: fresh_Inl)
+apply (simp add: fresh_def)
+using supp_subst apply blast
+apply (simp add: eqvt_at_def subst_eqvt)
+apply (subst swap_fresh_fresh)
+apply assumption+
+apply rule
+apply simp
 oops (* can this be defined ? *)
 
 text {* tests of functions containing if and case *}