--- a/Nominal/Ex/Lambda.thy	Fri Jun 03 22:31:44 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Sat Jun 04 09:07:50 2011 +0900
@@ -67,23 +67,28 @@
 where
   "f (Var x) = f1 x"
 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)"
-| "atom x \<sharp> (f1, f2, f3) \<Longrightarrow> f (Lam [x].t) = f3 x t (f t)"
+| "f (Lam [x].t) = f3 x t (f t)"
   apply (simp add: eqvt_def f_graph_def)
   apply (perm_simp)
   apply(simp add: eq[simplified eqvt_def])
-  apply(rule_tac y="x" and c="(f1,f2,f3)" in lam_strong_exhaust2)
+  apply(rule_tac y="x" in lam.exhaust)
   apply(auto simp add: fresh_star_def)
-  apply(rule fs)
-  apply(simp add: fresh_Pair_elim)
   apply(erule Abs1_eq_fdest)
   apply simp_all
   apply(simp add: fcb)
+  apply (rule fresh_fun_eqvt_app3[OF eq(3)])
+  apply (simp add: fresh_at_base)
+  apply assumption
+  apply (erule fresh_eqvt_at)
+  apply (simp add: finite_supp)
+  apply assumption
   apply (subgoal_tac "\<And>p y r. p \<bullet> (f3 x y r) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)")
-  apply (simp add: eqvt_at_def eqvt_def)
-  apply (simp add: permute_fun_app_eq eq[simplified eqvt_def])
-  sorry
+  apply (simp add: eqvt_at_def)
+  apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
+  done
 
-termination sorry
+termination
+  by (relation "measure size") (auto simp add: lam.size)
 
 end
 
@@ -91,6 +96,18 @@
 
 thm test_def
 
+interpretation hei: test
+  "%n. (1 :: nat)"
+  "%t1 t2 r1 r2. (r1 + r2)"
+  "%n t r. r + 1"
+  apply default
+  apply (auto simp add: pure_fresh supp_Pair)
+  apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3]
+  apply (simp_all add: eqvt_def permute_fun_def permute_pure)
+  done
+
+thm hei.f.simps
+
 
 
 inductive