attempt for NBE
authorChristian Urban <urbanc@in.tum.de>
Wed, 06 Jul 2011 00:34:42 +0200
changeset 2952 e4c2854833ad
parent 2951 d75b3d8529e7
child 2953 80f01215d1a6
attempt for NBE
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
+
+