--- /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
+
+