1 theory EtaExpansionSestoft
2 imports EtaExpansion Sestoft
3 begin
5 theorem eta_expansion_correct:
6   assumes "set T \<subseteq> range Arg"
7   shows "(\<Gamma>, eta_expand (length T) e, T@S) \<Rightarrow>\<^sup>* (\<Gamma>, e, T@S)"
8 using assms
9 proof(induction T arbitrary: e)
10   case Nil show ?case by simp
11 next
12   case (Cons se T)
13   from Cons(2) obtain x where "se = Arg x" by auto
15   from Cons have prem: "set T \<subseteq> range Arg" by simp
17   have "(\<Gamma>, eta_expand (Suc (length T)) e, Arg x # T @ S) = (\<Gamma>, Lam [fresh_var e]. eta_expand (length T) (App e (fresh_var e)), Arg x # T @ S)" by simp
18   also have "\<dots> \<Rightarrow> (\<Gamma>, (eta_expand (length T) (App e (fresh_var e)))[fresh_var e ::= x], T @ S)" by (rule app\<^sub>2)
19   also have "\<dots> = (\<Gamma>, (eta_expand (length T) (App e x)), T @ S)" unfolding subst_eta_expand by simp
20   also have "\<dots> \<Rightarrow>\<^sup>* (\<Gamma>, App e x, T @ S)" by (rule Cons.IH[OF prem])
21   also have "\<dots> \<Rightarrow> (\<Gamma>, e, Arg x # T @ S)"  by (rule app\<^sub>1)
22   finally show ?case using `se = _` by simp
23 qed
25 fun arg_prefix :: "stack \<Rightarrow> nat" where
26   "arg_prefix [] = 0"
27 | "arg_prefix (Arg x # S) = Suc (arg_prefix S)"
28 | "arg_prefix (Alts e1 e2 # S) = 0"
29 | "arg_prefix (Upd x # S) = 0"
30 | "arg_prefix (Dummy x # S) = 0"
32 theorem eta_expansion_correct':
33   assumes "n \<le> arg_prefix S"
34   shows "(\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)"
35 proof-
36   from assms
37   have "set (take n S) \<subseteq> range Arg" and "length (take n S) = n"
38     apply (induction S arbitrary: n rule: arg_prefix.induct)
39     apply auto
40     apply (case_tac n, auto)+
41     done
42   hence "S = take n S @ drop n S" by (metis append_take_drop_id)
43   with eta_expansion_correct[OF `_ \<subseteq> _`] `length _ = _`
44   show ?thesis by metis
45 qed
47 end