theory EtaExpansion imports "Terms" "Substitution" begin definition fresh_var :: "exp ⇒ var" where "fresh_var e = (SOME v. v ∉ fv e)" lemma fresh_var_not_free: "fresh_var e ∉ fv e" proof- obtain v :: var where "atom v ♯ e" by (rule obtain_fresh) hence "v ∉ fv e" by (metis fv_not_fresh) thus ?thesis unfolding fresh_var_def by (rule someI) qed lemma fresh_var_fresh[simp]: "atom (fresh_var e) ♯ e" by (metis fresh_var_not_free fv_not_fresh) lemma fresh_var_subst[simp]: "e[fresh_var e::=x] = e" by (metis fresh_var_fresh subst_fresh_noop) fun eta_expand :: "nat ⇒ exp ⇒ exp" where "eta_expand 0 e = e" | "eta_expand (Suc n) e = (Lam [fresh_var e]. eta_expand n (App e (fresh_var e)))" lemma eta_expand_eqvt[eqvt]: "π ∙ (eta_expand n e) = eta_expand (π ∙ n) (π ∙ e)" apply (induction n arbitrary: e π) apply (auto simp add: fresh_Pair permute_pure) apply (metis fresh_at_base_permI fresh_at_base_permute_iff fresh_var_fresh subst_fresh_noop subst_swap_same) done lemma fresh_eta_expand[simp]: "a ♯ eta_expand n e ⟷ a ♯ e" apply (induction n arbitrary: e) apply (simp add: fresh_Pair) apply (clarsimp simp add: fresh_Pair fresh_at_base) by (metis fresh_var_fresh) lemma subst_eta_expand: "(eta_expand n e)[x ::= y] = eta_expand n (e[x ::= y])" proof (induction n arbitrary: e) case 0 thus ?case by simp next case (Suc n) obtain z :: var where "atom z ♯ (e, fresh_var e, x, y)" by (rule obtain_fresh) have "(eta_expand (Suc n) e)[x::=y] = (Lam [fresh_var e]. eta_expand n (App e (fresh_var e)))[x::=y]" by simp also have "… = (Lam [z]. eta_expand n (App e z))[x::=y]" apply (subst change_Lam_Variable[where y' = z]) using `atom z ♯ _` by (auto simp add: fresh_Pair eta_expand_eqvt pure_fresh permute_pure flip_fresh_fresh intro!: eqvt_fresh_cong2[where f = eta_expand, OF eta_expand_eqvt]) also have "… = Lam [z]. (eta_expand n (App e z))[x::=y]" using `atom z ♯ _` by simp also have "… = Lam [z]. eta_expand n (App e z)[x::=y]" unfolding Suc.IH.. also have "… = Lam [z]. eta_expand n (App e[x::=y] z)" using `atom z ♯ _` by simp also have "… = Lam [fresh_var (e[x::=y])]. eta_expand n (App e[x::=y] (fresh_var (e[x::=y])))" apply (subst change_Lam_Variable[where y' = "fresh_var (e[x::=y])"]) using `atom z ♯ _` by (auto simp add: fresh_Pair eqvt_fresh_cong2[where f = eta_expand, OF eta_expand_eqvt] pure_fresh eta_expand_eqvt flip_fresh_fresh subst_pres_fresh simp del: exp_assn.eq_iff) also have "… = eta_expand (Suc n) e[x::=y]" by simp finally show ?case. qed lemma isLam_eta_expand: "isLam e ⟹ isLam (eta_expand n e)" and "n > 0 ⟹ isLam (eta_expand n e)" by (induction n) auto lemma isVal_eta_expand: "isVal e ⟹ isVal (eta_expand n e)" and "n > 0 ⟹ isVal (eta_expand n e)" by (induction n) auto end