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