theory EtaExpansionSafe imports EtaExpansion Sestoft begin theorem eta_expansion_safe: assumes "set T ⊆ range Arg" shows "(Γ, eta_expand (length T) e, T@S) ⇒⇧* (Γ, e, T@S)" using assms proof(induction T arbitrary: e) case Nil show ?case by simp next case (Cons se T) from Cons(2) obtain x where "se = Arg x" by auto from Cons have prem: "set T ⊆ range Arg" by simp have "(Γ, eta_expand (Suc (length T)) e, Arg x # T @ S) = (Γ, Lam [fresh_var e]. eta_expand (length T) (App e (fresh_var e)), Arg x # T @ S)" by simp also have "… ⇒ (Γ, (eta_expand (length T) (App e (fresh_var e)))[fresh_var e ::= x], T @ S)" by (rule app⇩2) also have "… = (Γ, (eta_expand (length T) (App e x)), T @ S)" unfolding subst_eta_expand by simp also have "… ⇒⇧* (Γ, App e x, T @ S)" by (rule Cons.IH[OF prem]) also have "… ⇒ (Γ, e, Arg x # T @ S)" by (rule app⇩1) finally show ?case using `se = _` by simp qed fun arg_prefix :: "stack ⇒ nat" where "arg_prefix [] = 0" | "arg_prefix (Arg x # S) = Suc (arg_prefix S)" | "arg_prefix (Alts e1 e2 # S) = 0" | "arg_prefix (Upd x # S) = 0" | "arg_prefix (Dummy x # S) = 0" theorem eta_expansion_safe': assumes "n ≤ arg_prefix S" shows "(Γ, eta_expand n e, S) ⇒⇧* (Γ, e, S)" proof- from assms have "set (take n S) ⊆ range Arg" and "length (take n S) = n" apply (induction S arbitrary: n rule: arg_prefix.induct) apply auto apply (case_tac n, auto)+ done hence "S = take n S @ drop n S" by (metis append_take_drop_id) with eta_expansion_safe[OF `_ ⊆ _`] `length _ = _` show ?thesis by metis qed end