--- a/Nominal/Ex/NBE.thy	Wed Jul 06 07:42:12 2011 +0900
+++ b/Nominal/Ex/NBE.thy	Wed Jul 06 01:04:09 2011 +0200
@@ -57,17 +57,62 @@
 apply(simp)
 apply(simp)
 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva x (evals enva t2a), t)")
-apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (enva, t2a)")
-apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva x (evals enva t2a), t)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))")
 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))")
 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))")
+apply(erule conjE)+
 defer
 apply (simp_all add: eqvt_at_def evals_def)[3]
+apply(simp)
+defer
+apply(erule_tac c="(cenv, env)" in  Abs_lst1_fcb2')
+apply(rule fresh_eqvt_at)
+back
+apply(simp add: eqvt_at_def)
 sorry
 
 (* can probably not proved by a trivial size argument *)
 termination sorry
 
+nominal_primrec
+  reify :: "sem \<Rightarrow> lam" and
+  reifyn :: "neu \<Rightarrow> lam"
+where
+  "reify (L env y t) = (fresh_fun (\<lambda>x::name. Lam [x]. (reify (evals (ECons env y (N (V x))) t))))"
+| "reify (N n) = reifyn n"
+| "reifyn (V x) = Var x"
+| "reifyn (A n d) = App (reifyn n) (reify d)"
+defer
+defer
+--"completeness"
+apply(case_tac x)
+apply(simp)
+apply(case_tac a rule: sem_neu_env.exhaust(1))
+apply(metis)+
+apply(case_tac b rule: sem_neu_env.exhaust(2))
+apply(simp)
+apply(simp)
+apply(metis)
+--"compatibility"
+apply(all_trivials)
+defer
+apply(simp)
+apply(simp)
+sorry
 
+termination sorry
+
+definition
+  eval :: "lam \<Rightarrow> sem"
+where
+  "eval t = evals ENil t"
+
+definition
+  normalize :: "lam \<Rightarrow> lam"
+where
+  "normalize t = reify (eval t)"
+
+end
\ No newline at end of file