theory Lambda_add
imports "Lambda"
begin

nominal_primrec
  addlam :: "lam \<Rightarrow> lam"
where
  "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
| "addlam (App t1 t2) = App t1 t2"
| "addlam (Lam [x]. t) = Lam [x].t"
  unfolding addlam_graph_def eqvt_def
  apply perm_simp
  apply auto
  apply (case_tac x rule: lam.exhaust)
  apply auto
  apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
  apply (simp add: fresh_at_base)
  apply (simp add: Abs1_eq_iff lam.fresh fresh_at_base)
  done

termination by lexicographic_order

end