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
apply (rule TrueI)
--"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)
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 (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))")
defer
apply (simp_all add: eqvt_at_def evals_def)[3]
sorry

(* can probably not proved by a trivial size argument *)
termination sorry