Theory EtaExpansionSafe

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