--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Jun 21 10:39:25 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Jun 21 23:59:36 2011 +0900
@@ -215,25 +215,32 @@
   by lexicographic_order
 
 definition psi:: "lt => lt"
-  where "psi V == V*(\<lambda>x. x)"
+  where [simp]: "psi V == V*(\<lambda>x. x)"
 
 section {* Simple consequence of CPS *}
 
+lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)"
+  by (simp add: eqvt_def eqvt_bound eqvt_lambda)
+
 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
   apply (cases V rule: lt.exhaust)
-  apply (auto simp add: psi_def)
-  apply (subst CPS1.simps)
-  apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
-  apply rule
+  apply simp_all
   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply (subst CPS1.simps(3))
-  apply assumption+
-  apply (subst CPS1.simps(3))
-  apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
-  apply assumption
-  apply rule
+  apply simp
   done
 
+lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)"
+  apply (cases V rule: lt.exhaust)
+  apply simp_all
+  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+  apply simp
+  done
+
+lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Abs n (k (Var n))))"
+  by (cases M rule: lt.exhaust) auto
+
+
+
 end