# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1309905282 -7200
# Node ID e4c2854833ad8859a6c68d7d318da3df88ee5a7b
# Parent  d75b3d8529e7691e91466b91c36a8a12adec1f07
attempt for NBE

diff -r d75b3d8529e7 -r e4c2854833ad Nominal/Ex/NBE.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/NBE.thy	Wed Jul 06 00:34:42 2011 +0200
@@ -0,0 +1,66 @@
+theory Lambda
+imports 
+  "../Nominal2"
+begin
+
+
+atom_decl name
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
+
+
+nominal_datatype sem =
+  L "env" x::"name" l::"lam" binds x in l
+| N "neu"
+and neu = 
+  V "name"
+| A "neu" "sem"
+and env =
+  ENil
+| ECons "env" "name" "sem"
+
+nominal_primrec 
+  evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
+  evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
+where
+  "evals ENil (Var x) = N (V x)"
+| "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" 
+| "evals env (Lam [x]. t) = L env x t"
+| "evals env (App t1 t2) = evals_aux (evals env t1) t2 env"
+| "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"
+| "evals_aux (N n) t2 env = N (A n (evals env t2))"
+defer
+defer
+--"completeness"
+apply(case_tac x)
+apply(simp)
+apply(case_tac a)
+apply(simp)
+apply(case_tac aa rule: sem_neu_env.exhaust(3))
+apply(simp)
+apply(case_tac b rule: lam.exhaust)
+apply(metis)+
+apply(case_tac b rule: lam.exhaust)
+apply(metis)+
+apply(simp)
+apply(case_tac b)
+apply(simp)
+apply(case_tac a rule: sem_neu_env.exhaust(1))
+apply(metis)+
+--"compatibility"
+apply(all_trivials)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+defer
+apply(simp)
+sorry
+
+(* can probably not proved by a trivial size argument *)
+termination sorry
+
+