1922315781f5987a587d300e0234981d3e40ced1
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 definition eta_expand_heap :: "(var \<Rightarrow> nat) \<Rightarrow> heap \<Rightarrow> heap"
48   where "eta_expand_heap f \<Gamma> = map_ran (\<lambda> x e. eta_expand (f x) e) \<Gamma>"
50 lemma eta_expand_heap_Nil[simp]:
51   "eta_expand_heap exp [] = []"
52   unfolding eta_expand_heap_def by simp
53 lemma eta_expand_heap_Cons[simp]:
54   "eta_expand_heap exp ((x, e) # \<Gamma>) = (x, eta_expand (exp x) e) # eta_expand_heap exp \<Gamma>"
55   unfolding eta_expand_heap_def by simp
56 lemma eta_expand_heap_append[simp]:
57   "eta_expand_heap exp (\<Delta> @ \<Gamma>) = eta_expand_heap exp \<Delta> @ eta_expand_heap exp \<Gamma>"
58   by (induction \<Delta>) auto
60 lemma fresh_eta_expand_heap[simp]: "a \<sharp> eta_expand_heap exp \<Gamma> \<longleftrightarrow> a \<sharp> \<Gamma>"
61   by (induction \<Gamma>) (auto simp add: fresh_Cons fresh_Pair)
63 theorem bound_eta_expansion_correct:
64   fixes exp :: "var \<Rightarrow> nat"
65   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S')"
66   assumes "\<not> boring_step (\<Delta>, z, S')"
67   assumes "\<And> x e'. e = Var x \<Longrightarrow> map_of \<Gamma> x = Some e' \<Longrightarrow> (if isVal e' then exp x \<le> arg_prefix S else exp x = 0)"
68   assumes "exp ` (- domA \<Gamma>) \<subseteq> {0}"
69   shows "(eta_expand_heap exp \<Gamma>, e, S) \<Rightarrow>\<^sup>* (eta_expand_heap exp \<Delta>, z, S')"
70 using assms
71 proof(induction "(\<Gamma>, e, S)" "(\<Delta>, z, S')" arbitrary: \<Gamma> e S \<Delta> z S'  rule: step_induction)
72 case (thunk \<Gamma> x e S)
73   from thunk.prems thunk.hyps
74   have "exp x = 0" by auto
75   hence "eta_expand (exp x) e = e" by simp
77   from `map_of \<Gamma> x = Some e`
78   have "map_of (eta_expand_heap exp \<Gamma>) x = Some (eta_expand (exp x) e)"
79     unfolding eta_expand_heap_def by (metis  map_ran_conv option.simps(9))
80   hence "(eta_expand_heap exp \<Gamma>, Var x, S) \<Rightarrow> (delete x (eta_expand_heap exp \<Gamma>), e, Upd x # S)"
81     unfolding `eta_expand (exp x) e = e`
82     by (rule step.var\<^sub>1)
83   also have "delete x (eta_expand_heap exp \<Gamma>) = eta_expand_heap exp (delete x \<Gamma>)"
84     by (simp add: eta_expand_heap_def map_ran_delete)
85   finally
86   show "(eta_expand_heap exp \<Gamma>, Var x, S) \<Rightarrow>\<^sup>* (eta_expand_heap exp (delete x \<Gamma>), e, Upd x # S)"..
87 next
88 case (lamvar \<Gamma> x e S)
89   from lamvar.prems lamvar.hyps
90   have "exp x \<le> arg_prefix S" by auto
92   from `map_of \<Gamma> x = Some e`
93   have "map_of (eta_expand_heap exp \<Gamma>) x = Some (eta_expand (exp x) e)"
94     unfolding eta_expand_heap_def by (metis map_ran_conv option.simps(9))
95   hence "(eta_expand_heap exp \<Gamma>, Var x, S) \<Rightarrow> (delete x (eta_expand_heap exp \<Gamma>), eta_expand (exp x) e, Upd x # S)"
96     by (rule step.var\<^sub>1)
97   hence "(eta_expand_heap exp \<Gamma>, Var x, S) \<Rightarrow>\<^sup>* (delete x (eta_expand_heap exp \<Gamma>), eta_expand (exp x) e, Upd x # S)"..
98   also have "\<dots> \<Rightarrow> ((x, eta_expand (exp x) e) # delete x (eta_expand_heap exp \<Gamma>), eta_expand (exp x) e, S)"
99     using isVal_eta_expand(1)[OF `isVal _`] by (auto intro: var\<^sub>2)
100   also have "\<dots> \<Rightarrow>\<^sup>* ((x, eta_expand (exp x) e) # delete x (eta_expand_heap exp \<Gamma>), e, S)"
101      by (rule eta_expansion_correct') fact
102   also have "delete x (eta_expand_heap exp \<Gamma>) = eta_expand_heap exp (delete x \<Gamma>)"
103     by (simp add: eta_expand_heap_def map_ran_delete)
104   finally
105   show ?case by simp
106 next
107 case (let\<^sub>1 \<Delta> \<Gamma> S e)
108   from fresh_distinct[OF let\<^sub>1(1)] let\<^sub>1(4)
109   have "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> exp x = 0" by auto
110   hence "eta_expand_heap exp \<Delta> = \<Delta>" by (induction \<Delta>) auto
111   with let\<^sub>1
112   show ?case by (fastforce intro: step.intros simp add: fresh_star_def )
113 next
114 case refl
115   show ?case..
116 next
117 case trans
118   thus ?case
119 oops
123 end