theory ArityEtaExpansion imports EtaExpansion "Arity-Nominal" TransformTools begin lift_definition Aeta_expand :: "Arity ⇒ exp ⇒ exp" is "eta_expand". lemma Aeta_expand_eqvt[eqvt]: "π ∙ Aeta_expand a e = Aeta_expand (π ∙ a) (π ∙ e)" apply (cases a) apply simp apply transfer apply simp done lemma Aeta_expand_0[simp]: "Aeta_expand 0 e = e" by transfer simp lemma Aeta_expand_inc[simp]: "Aeta_expand (inc⋅n) e = (Lam [fresh_var e]. Aeta_expand n (App e (fresh_var e)))" apply (simp add: inc_def) by transfer simp lemma subst_Aeta_expand: "(Aeta_expand n e)[x::=y] = Aeta_expand n e[x::=y]" by transfer (rule subst_eta_expand) lemma isLam_Aeta_expand: "isLam e ⟹ isLam (Aeta_expand a e)" by transfer (rule isLam_eta_expand) lemma isVal_Aeta_expand: "isVal e ⟹ isVal (Aeta_expand a e)" by transfer (rule isVal_eta_expand) lemma Aeta_expand_fresh[simp]: "a ♯ Aeta_expand n e = a ♯ e" by transfer simp lemma Aeta_expand_fresh_star[simp]: "a ♯* Aeta_expand n e = a ♯* e" by (auto simp add: fresh_star_def) interpretation supp_bounded_transform Aeta_expand apply standard using Aeta_expand_fresh apply (auto simp add: fresh_def) done end