# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307532646 -3600
# Node ID 71382ce4d2ed2157162f8a41cff58c89d7080a83
# Parent  3503432262dc5f4aa905447880cfef4409fdc851
merged

diff -r 3503432262dc -r 71382ce4d2ed Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 08 08:44:01 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 08 12:30:46 2011 +0100
@@ -644,6 +644,25 @@
 apply(simp_all add: permute_pure)
 done
 
+(* function that evaluates a lambda term *)
+nominal_primrec
+   eval :: "lam \<Rightarrow> lam" and
+   app :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "eval (Var x) = Var x"
+| "eval (Lam [x].t) = Lam [x].(eval t)"
+| "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])"
+apply(simp add: eval_app_graph_def eqvt_def)
+apply(perm_simp)
+apply(simp)
+apply(rule TrueI)
+defer
+apply(simp_all)
+defer
+oops (* can this be defined ? *)
 
 text {* tests of functions containing if and case *}
 
@@ -751,6 +770,9 @@
 
 
 
+
+
+
 end