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