|
1 (* ID: $Id$ |
|
2 Author: Klaus Aehlig, Tobias Nipkow |
|
3 Work in progress |
|
4 *) |
|
5 |
|
6 theory NBE imports Main ExecutableSet begin |
|
7 |
|
8 ML"set quick_and_dirty" |
|
9 |
|
10 declare Let_def[simp] |
|
11 |
|
12 consts_code undefined ("(raise Match)") |
|
13 |
|
14 (*typedecl const_name*) |
|
15 types lam_var_name = nat |
|
16 ml_var_name = nat |
|
17 const_name = nat |
|
18 |
|
19 datatype tm = Ct const_name | Vt lam_var_name | Lam tm | At tm tm |
|
20 | term_of ml (* function 'to_term' *) |
|
21 and ml = (* rep of universal datatype *) |
|
22 C const_name "ml list" | V lam_var_name "ml list" |
|
23 | Fun ml "ml list" nat |
|
24 | "apply" ml ml (* function 'apply' *) |
|
25 (* ML *) |
|
26 | V_ML ml_var_name | A_ML ml "ml list" | Lam_ML ml |
|
27 | CC const_name (* ref to compiled code *) |
|
28 |
|
29 lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (ml_list_size1 vs)" |
|
30 by (induct vs) auto |
|
31 lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (ml_list_size2 vs)" |
|
32 by (induct vs) auto |
|
33 lemma [simp]:"x \<in> set vs \<Longrightarrow> size x < Suc (size v + ml_list_size3 vs)" |
|
34 by (induct vs) auto |
|
35 lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (size v + ml_list_size4 vs)" |
|
36 by (induct vs) auto |
|
37 |
|
38 locale Vars = |
|
39 fixes r s t:: tm |
|
40 and rs ss ts :: "tm list" |
|
41 and u v w :: ml |
|
42 and us vs ws :: "ml list" |
|
43 and nm :: const_name |
|
44 and x :: lam_var_name |
|
45 and X :: ml_var_name |
|
46 |
|
47 consts Pure_tms :: "tm set" |
|
48 inductive Pure_tms |
|
49 intros |
|
50 "Ct s : Pure_tms" |
|
51 "Vt x : Pure_tms" |
|
52 "t : Pure_tms ==> Lam t : Pure_tms" |
|
53 "s : Pure_tms ==> t : Pure_tms ==> At s t : Pure_tms" |
|
54 |
|
55 consts |
|
56 R :: "(const_name * tm list * tm)set" (* reduction rules *) |
|
57 compR :: "(const_name * ml list * ml)set" (* compiled reduction rules *) |
|
58 tRed :: "(tm * tm)set" (* beta + R reduction on pure terms *) |
|
59 tRed_list :: "(tm list * tm list) set" |
|
60 |
|
61 fun |
|
62 lift_tm :: "nat \<Rightarrow> tm \<Rightarrow> tm" ("lift") and |
|
63 lift_ml :: "nat \<Rightarrow> ml \<Rightarrow> ml" ("lift") |
|
64 where |
|
65 "lift i (Ct nm) = Ct nm" | |
|
66 "lift i (Vt x) = Vt(if x < i then x else x+1)" | |
|
67 "lift i (Lam t) = Lam (lift (i+1) t)" | |
|
68 "lift i (At s t) = At (lift i s) (lift i t)" | |
|
69 "lift i (term_of v) = term_of (lift i v)" | |
|
70 |
|
71 "lift i (C nm vs) = C nm (map (lift i) vs)" | |
|
72 "lift i (V x vs) = V (if x < i then x else x+1) (map (lift i) vs)" | |
|
73 "lift i (Fun v vs n) = Fun (lift i v) (map (lift i) vs) n" | |
|
74 "lift i (apply u v) = apply (lift i u) (lift i v)" | |
|
75 "lift i (V_ML X) = V_ML X" | |
|
76 "lift i (A_ML v vs) = A_ML (lift i v) (map (lift i) vs)" | |
|
77 "lift i (Lam_ML v) = Lam_ML (lift i v)" | |
|
78 "lift i (CC nm) = CC nm" |
|
79 (* |
|
80 termination |
|
81 apply (relation "measure (sum_case (%(i,t). size t) (%(i,v). size v))") |
|
82 apply auto |
|
83 *) |
|
84 |
|
85 fun |
|
86 lift_tm_ML :: "nat \<Rightarrow> tm \<Rightarrow> tm" ("lift\<^bsub>ML\<^esub>") and |
|
87 lift_ml_ML :: "nat \<Rightarrow> ml \<Rightarrow> ml" ("lift\<^bsub>ML\<^esub>") |
|
88 where |
|
89 "lift\<^bsub>ML\<^esub> i (Ct nm) = Ct nm" | |
|
90 "lift\<^bsub>ML\<^esub> i (Vt x) = Vt x" | |
|
91 "lift\<^bsub>ML\<^esub> i (Lam t) = Lam (lift\<^bsub>ML\<^esub> i t)" | |
|
92 "lift\<^bsub>ML\<^esub> i (At s t) = At (lift\<^bsub>ML\<^esub> i s) (lift\<^bsub>ML\<^esub> i t)" | |
|
93 "lift\<^bsub>ML\<^esub> i (term_of v) = term_of (lift\<^bsub>ML\<^esub> i v)" | |
|
94 |
|
95 "lift\<^bsub>ML\<^esub> i (C nm vs) = C nm (map (lift\<^bsub>ML\<^esub> i) vs)" | |
|
96 "lift\<^bsub>ML\<^esub> i (V x vs) = V x (map (lift\<^bsub>ML\<^esub> i) vs)" | |
|
97 "lift\<^bsub>ML\<^esub> i (Fun v vs n) = Fun (lift\<^bsub>ML\<^esub> i v) (map (lift\<^bsub>ML\<^esub> i) vs) n" | |
|
98 "lift\<^bsub>ML\<^esub> i (apply u v) = apply (lift\<^bsub>ML\<^esub> i u) (lift\<^bsub>ML\<^esub> i v)" | |
|
99 "lift\<^bsub>ML\<^esub> i (V_ML X) = V_ML (if X < i then X else X+1)" | |
|
100 "lift\<^bsub>ML\<^esub> i (A_ML v vs) = A_ML (lift\<^bsub>ML\<^esub> i v) (map (lift\<^bsub>ML\<^esub> i) vs)" | |
|
101 "lift\<^bsub>ML\<^esub> i (Lam_ML v) = Lam_ML (lift\<^bsub>ML\<^esub> (i+1) v)" | |
|
102 "lift\<^bsub>ML\<^esub> i (CC nm) = CC nm" |
|
103 (* |
|
104 termination |
|
105 by (relation "measure (sum_case (%(i,t). size t) (%(i,v). size v))") auto |
|
106 *) |
|
107 constdefs |
|
108 cons :: "tm \<Rightarrow> (nat \<Rightarrow> tm) \<Rightarrow> (nat \<Rightarrow> tm)" (infix "##" 65) |
|
109 "t##f \<equiv> \<lambda>i. case i of 0 \<Rightarrow> t | Suc j \<Rightarrow> lift 0 (f j)" |
|
110 cons_ML :: "ml \<Rightarrow> (nat \<Rightarrow> ml) \<Rightarrow> (nat \<Rightarrow> ml)" (infix "##" 65) |
|
111 "v##f \<equiv> \<lambda>i. case i of 0 \<Rightarrow> v::ml | Suc j \<Rightarrow> lift\<^bsub>ML\<^esub> 0 (f j)" |
|
112 |
|
113 (* Only for pure terms! *) |
|
114 consts subst :: "(nat \<Rightarrow> tm) \<Rightarrow> tm \<Rightarrow> tm" |
|
115 primrec |
|
116 "subst f (Ct nm) = Ct nm" |
|
117 "subst f (Vt x) = f x" |
|
118 "subst f (Lam t) = Lam (subst (Vt 0 ## f) t)" |
|
119 "subst f (At s t) = At (subst f s) (subst f t)" |
|
120 |
|
121 lemma size_lift[simp]: shows |
|
122 "size(lift i t) = size(t::tm)" and "size(lift i (v::ml)) = size v" |
|
123 and "ml_list_size1 (map (lift i) vs) = ml_list_size1 vs" |
|
124 and "ml_list_size2 (map (lift i) vs) = ml_list_size2 vs" |
|
125 and "ml_list_size3 (map (lift i) vs) = ml_list_size3 vs" |
|
126 and "ml_list_size4 (map (lift i) vs) = ml_list_size4 vs" |
|
127 by (induct arbitrary: i and i and i and i and i and i rule: tm_ml.inducts) |
|
128 simp_all |
|
129 |
|
130 lemma size_lift_ML[simp]: shows |
|
131 "size(lift\<^bsub>ML\<^esub> i t) = size(t::tm)" and "size(lift\<^bsub>ML\<^esub> i (v::ml)) = size v" |
|
132 and "ml_list_size1 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size1 vs" |
|
133 and "ml_list_size2 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size2 vs" |
|
134 and "ml_list_size3 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size3 vs" |
|
135 and "ml_list_size4 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size4 vs" |
|
136 by (induct arbitrary: i and i and i and i and i and i rule: tm_ml.inducts) |
|
137 simp_all |
|
138 |
|
139 fun |
|
140 subst_ml_ML :: "(nat \<Rightarrow> ml) \<Rightarrow> ml \<Rightarrow> ml" ("subst\<^bsub>ML\<^esub>") and |
|
141 subst_tm_ML :: "(nat \<Rightarrow> ml) \<Rightarrow> tm \<Rightarrow> tm" ("subst\<^bsub>ML\<^esub>") |
|
142 where |
|
143 "subst\<^bsub>ML\<^esub> f (Ct nm) = Ct nm" | |
|
144 "subst\<^bsub>ML\<^esub> f (Vt x) = Vt x" | |
|
145 "subst\<^bsub>ML\<^esub> f (Lam t) = Lam (subst\<^bsub>ML\<^esub> (lift 0 o f) t)" | |
|
146 "subst\<^bsub>ML\<^esub> f (At s t) = At (subst\<^bsub>ML\<^esub> f s) (subst\<^bsub>ML\<^esub> f t)" | |
|
147 "subst\<^bsub>ML\<^esub> f (term_of v) = term_of (subst\<^bsub>ML\<^esub> f v)" | |
|
148 |
|
149 "subst\<^bsub>ML\<^esub> f (C nm vs) = C nm (map (subst\<^bsub>ML\<^esub> f) vs)" | |
|
150 "subst\<^bsub>ML\<^esub> f (V x vs) = V x (map (subst\<^bsub>ML\<^esub> f) vs)" | |
|
151 "subst\<^bsub>ML\<^esub> f (Fun v vs n) = Fun (subst\<^bsub>ML\<^esub> f v) (map (subst\<^bsub>ML\<^esub> f) vs) n" | |
|
152 "subst\<^bsub>ML\<^esub> f (apply u v) = apply (subst\<^bsub>ML\<^esub> f u) (subst\<^bsub>ML\<^esub> f v)" | |
|
153 "subst\<^bsub>ML\<^esub> f (V_ML X) = f X" | |
|
154 "subst\<^bsub>ML\<^esub> f (A_ML v vs) = A_ML (subst\<^bsub>ML\<^esub> f v) (map (subst\<^bsub>ML\<^esub> f) vs)" | |
|
155 "subst\<^bsub>ML\<^esub> f (Lam_ML v) = Lam_ML (subst\<^bsub>ML\<^esub> (V_ML 0 ## f) v)" | |
|
156 "subst\<^bsub>ML\<^esub> f (CC nm) = CC nm" |
|
157 |
|
158 (* FIXME currrently needed for code generator *) |
|
159 lemmas [code] = lift_tm_ML.simps lift_ml_ML.simps |
|
160 lemmas [code] = lift_tm.simps lift_ml.simps |
|
161 lemmas [code] = subst_tm_ML.simps subst_ml_ML.simps |
|
162 |
|
163 abbreviation |
|
164 subst_decr :: "nat \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> tm" where |
|
165 "subst_decr k t == %n. if n<k then Vt n else if n=k then t else Vt(n - 1)" |
|
166 abbreviation |
|
167 subst_decr_ML :: "nat \<Rightarrow> ml \<Rightarrow> nat \<Rightarrow> ml" where |
|
168 "subst_decr_ML k v == %n. if n<k then V_ML n else if n=k then v else V_ML(n - 1)" |
|
169 abbreviation |
|
170 subst1 :: "tm \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> tm" ("(_/[_'/_])" [300, 0, 0] 300) where |
|
171 "s[t/k] == subst (subst_decr k t) s" |
|
172 abbreviation |
|
173 subst1_ML :: "ml \<Rightarrow> ml \<Rightarrow> nat \<Rightarrow> ml" ("(_/[_'/_])" [300, 0, 0] 300) where |
|
174 "u[v/k] == subst\<^bsub>ML\<^esub> (subst_decr_ML k v) u" |
|
175 |
|
176 |
|
177 lemma size_subst_ML[simp]: shows |
|
178 "(!x. size(f x) = 0) \<longrightarrow> size(subst\<^bsub>ML\<^esub> f t) = size(t::tm)" and |
|
179 "(!x. size(f x) = 0) \<longrightarrow> size(subst\<^bsub>ML\<^esub> f (v::ml)) = size v" |
|
180 and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size1 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size1 vs" |
|
181 and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size2 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size2 vs" |
|
182 and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size3 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size3 vs" |
|
183 and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size4 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size4 vs" |
|
184 apply (induct arbitrary: f and f and f and f and f and f rule: tm_ml.inducts) |
|
185 apply (simp_all add:cons_ML_def split:nat.split) |
|
186 done |
|
187 |
|
188 lemma lift_lift: includes Vars shows |
|
189 "i < k+1 \<Longrightarrow> lift (Suc k) (lift i t) = lift i (lift k t)" |
|
190 and "i < k+1 \<Longrightarrow> lift (Suc k) (lift i v) = lift i (lift k v)" |
|
191 apply(induct t and v arbitrary: i and i rule:lift_tm_lift_ml.induct) |
|
192 apply(simp_all add:map_compose[symmetric]) |
|
193 done |
|
194 |
|
195 corollary lift_o_lift: shows |
|
196 "i < k+1 \<Longrightarrow> lift_tm (Suc k) o (lift_tm i) = lift_tm i o lift_tm k" and |
|
197 "i < k+1 \<Longrightarrow> lift_ml (Suc k) o (lift_ml i) = lift_ml i o lift_ml k" |
|
198 by(rule ext, simp add:lift_lift)+ |
|
199 |
|
200 lemma lift_lift_ML: includes Vars shows |
|
201 "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i t) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k t)" |
|
202 and "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i v) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k v)" |
|
203 apply(induct t and v arbitrary: i and i rule:lift_tm_ML_lift_ml_ML.induct) |
|
204 apply(simp_all add:map_compose[symmetric]) |
|
205 done |
|
206 |
|
207 |
|
208 lemma lift_lift_ML_comm: includes Vars shows |
|
209 "lift j (lift\<^bsub>ML\<^esub> i t) = lift\<^bsub>ML\<^esub> i (lift j t)" and |
|
210 "lift j (lift\<^bsub>ML\<^esub> i v) = lift\<^bsub>ML\<^esub> i (lift j v)" |
|
211 apply(induct t and v arbitrary: i j and i j rule:lift_tm_ML_lift_ml_ML.induct) |
|
212 apply(simp_all add:map_compose[symmetric]) |
|
213 done |
|
214 |
|
215 lemma [simp]: |
|
216 "V_ML 0 ## subst_decr_ML k v = subst_decr_ML (Suc k) (lift\<^bsub>ML\<^esub> 0 v)" |
|
217 by(rule ext)(simp add:cons_ML_def split:nat.split) |
|
218 |
|
219 lemma [simp]: "lift 0 o subst_decr_ML k v = subst_decr_ML k (lift 0 v)" |
|
220 by(rule ext)(simp add:cons_ML_def split:nat.split) |
|
221 |
|
222 lemma subst_lift_id[simp]: includes Vars shows |
|
223 "subst\<^bsub>ML\<^esub> (subst_decr_ML k v) (lift\<^bsub>ML\<^esub> k t) = t" and "(lift\<^bsub>ML\<^esub> k u)[v/k] = u" |
|
224 apply(induct k t and k u arbitrary: v and v rule: lift_tm_ML_lift_ml_ML.induct) |
|
225 apply (simp_all add:map_idI map_compose[symmetric]) |
|
226 apply (simp cong:if_cong) |
|
227 done |
|
228 |
|
229 abbreviation |
|
230 tred :: "[tm, tm] => bool" (infixl "\<rightarrow>" 50) where |
|
231 "s \<rightarrow> t == (s, t) \<in> tRed" |
|
232 abbreviation |
|
233 treds :: "[tm, tm] => bool" (infixl "\<rightarrow>*" 50) where |
|
234 "s \<rightarrow>* t == (s, t) \<in> tRed^*" |
|
235 abbreviation |
|
236 treds_list :: "[tm list, tm list] \<Rightarrow> bool" (infixl "\<rightarrow>*" 50) where |
|
237 "ss \<rightarrow>* ts == (ss, ts) \<in> tRed_list" |
|
238 |
|
239 inductive tRed |
|
240 intros |
|
241 "At (Lam t) s \<rightarrow> t[s/0]" |
|
242 "(nm,ts,t) : R ==> foldl At (Ct nm) (map (subst rs) ts) \<rightarrow> subst rs t" |
|
243 "t \<rightarrow> t' ==> Lam t \<rightarrow> Lam t'" |
|
244 "s \<rightarrow> s' ==> At s t \<rightarrow> At s' t" |
|
245 "t \<rightarrow> t' ==> At s t \<rightarrow> At s t'" |
|
246 |
|
247 inductive tRed_list |
|
248 intros |
|
249 "[] \<rightarrow>* []" |
|
250 "ts \<rightarrow>* ts' ==> t \<rightarrow>* t' ==> t#ts \<rightarrow>* t'#ts'" |
|
251 |
|
252 declare tRed_list.intros[simp] |
|
253 |
|
254 lemma tRed_list_refl[simp]: includes Vars shows "ts \<rightarrow>* ts" |
|
255 by(induct ts) auto |
|
256 |
|
257 consts |
|
258 Red :: "(ml * ml)set" |
|
259 Redl :: "(ml list * ml list)set" |
|
260 Redt :: "(tm * tm)set" |
|
261 |
|
262 abbreviation |
|
263 red :: "[ml, ml] => bool" (infixl "\<Rightarrow>" 50) where |
|
264 "s \<Rightarrow> t == (s, t) \<in> Red" |
|
265 abbreviation |
|
266 redl :: "[ml list, ml list] => bool" (infixl "\<Rightarrow>" 50) where |
|
267 "s \<Rightarrow> t == (s, t) \<in> Redl" |
|
268 abbreviation |
|
269 redt :: "[tm, tm] => bool" (infixl "\<Rightarrow>" 50) where |
|
270 "s \<Rightarrow> t == (s, t) \<in> Redt" |
|
271 abbreviation |
|
272 reds :: "[ml, ml] => bool" (infixl "\<Rightarrow>*" 50) where |
|
273 "s \<Rightarrow>* t == (s, t) \<in> Red^*" |
|
274 abbreviation |
|
275 redts :: "[tm, tm] => bool" (infixl "\<Rightarrow>*" 50) where |
|
276 "s \<Rightarrow>* t == (s, t) \<in> Redt^*" |
|
277 |
|
278 |
|
279 fun ML_closed :: "nat \<Rightarrow> ml \<Rightarrow> bool" |
|
280 and ML_closed_t :: "nat \<Rightarrow> tm \<Rightarrow> bool" where |
|
281 "ML_closed i (C nm vs) = (ALL v:set vs. ML_closed i v)" | |
|
282 "ML_closed i (V nm vs) = (ALL v:set vs. ML_closed i v)" | |
|
283 "ML_closed i (Fun f vs n) = (ML_closed i f & (ALL v:set vs. ML_closed i v))" | |
|
284 "ML_closed i (A_ML v vs) = (ML_closed i v & (ALL v:set vs. ML_closed i v))" | |
|
285 "ML_closed i (apply v w) = (ML_closed i v & ML_closed i w)" | |
|
286 "ML_closed i (CC nm) = True" | |
|
287 "ML_closed i (V_ML X) = (X<i)" | |
|
288 "ML_closed i (Lam_ML v) = ML_closed (i+1) v" | |
|
289 "ML_closed_t i (term_of v) = ML_closed i v" | |
|
290 "ML_closed_t i (At r s) = (ML_closed_t i r & ML_closed_t i s)" | |
|
291 "ML_closed_t i (Lam t) = (ML_closed_t i t)" | |
|
292 "ML_closed_t i v = True" |
|
293 thm ML_closed.simps ML_closed_t.simps |
|
294 |
|
295 inductive Red Redt Redl |
|
296 intros |
|
297 (* ML *) |
|
298 "A_ML (Lam_ML u) [v] \<Rightarrow> u[v/0]" |
|
299 (* compiled rules *) |
|
300 "(nm,vs,v) : compR ==> ALL i. ML_closed 0 (f i) \<Longrightarrow> A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs) \<Rightarrow> subst\<^bsub>ML\<^esub> f v" |
|
301 (* apply *) |
|
302 apply_Fun1: "apply (Fun f vs (Suc 0)) v \<Rightarrow> A_ML f (vs @ [v])" |
|
303 apply_Fun2: "n > 0 ==> |
|
304 apply (Fun f vs (Suc n)) v \<Rightarrow> Fun f (vs @ [v]) n" |
|
305 apply_C: "apply (C nm vs) v \<Rightarrow> C nm (vs @ [v])" |
|
306 apply_V: "apply (V x vs) v \<Rightarrow> V x (vs @ [v])" |
|
307 (* term_of *) |
|
308 term_of_C: "term_of (C nm vs) \<Rightarrow> foldl At (Ct nm) (map term_of vs)" |
|
309 term_of_V: "term_of (V x vs) \<Rightarrow> foldl At (Vt x) (map term_of vs)" |
|
310 term_of_Fun: "term_of(Fun vf vs n) \<Rightarrow> |
|
311 Lam (term_of ((apply (lift 0 (Fun vf vs n)) (V_ML 0))[V 0 []/0]))" |
|
312 (* Context *) |
|
313 ctxt_Lam: "t \<Rightarrow> t' ==> Lam t \<Rightarrow> Lam t'" |
|
314 ctxt_At1: "s \<Rightarrow> s' ==> At s t \<Rightarrow> At s' t" |
|
315 ctxt_At2: "t \<Rightarrow> t' ==> At s t \<Rightarrow> At s t'" |
|
316 ctxt_term_of: "v \<Rightarrow> v' ==> term_of v \<Rightarrow> term_of v'" |
|
317 ctxt_C: "vs \<Rightarrow> vs' ==> C nm vs \<Rightarrow> C nm vs'" |
|
318 ctxt_V: "vs \<Rightarrow> vs' ==> V x vs \<Rightarrow> V x vs'" |
|
319 ctxt_Fun1: "f \<Rightarrow> f' ==> Fun f vs n \<Rightarrow> Fun f' vs n" |
|
320 ctxt_Fun3: "vs \<Rightarrow> vs' ==> Fun f vs n \<Rightarrow> Fun f vs' n" |
|
321 ctxt_apply1: "s \<Rightarrow> s' ==> apply s t \<Rightarrow> apply s' t" |
|
322 ctxt_apply2: "t \<Rightarrow> t' ==> apply s t \<Rightarrow> apply s t'" |
|
323 ctxt_A_ML1: "f \<Rightarrow> f' ==> A_ML f vs \<Rightarrow> A_ML f' vs" |
|
324 ctxt_A_ML2: "vs \<Rightarrow> vs' ==> A_ML f vs \<Rightarrow> A_ML f vs'" |
|
325 ctxt_list1: "v \<Rightarrow> v' ==> v#vs \<Rightarrow> v'#vs" |
|
326 ctxt_list2: "vs \<Rightarrow> vs' ==> v#vs \<Rightarrow> v#vs'" |
|
327 |
|
328 |
|
329 consts |
|
330 ar :: "const_name \<Rightarrow> nat" |
|
331 |
|
332 axioms |
|
333 ar_pos: "ar nm > 0" |
|
334 |
|
335 types env = "ml list" |
|
336 |
|
337 consts eval :: "tm \<Rightarrow> env \<Rightarrow> ml" |
|
338 primrec |
|
339 "eval (Vt x) e = e!x" |
|
340 "eval (Ct nm) e = Fun (CC nm) [] (ar nm)" |
|
341 "eval (At s t) e = apply (eval s e) (eval t e)" |
|
342 "eval (Lam t) e = Fun (Lam_ML (eval t ((V_ML 0) # map (lift\<^bsub>ML\<^esub> 0) e))) [] 1" |
|
343 |
|
344 fun size' :: "ml \<Rightarrow> nat" where |
|
345 "size' (C nm vs) = (\<Sum>v\<leftarrow>vs. size' v)+1" | |
|
346 "size' (V nm vs) = (\<Sum>v\<leftarrow>vs. size' v)+1" | |
|
347 "size' (Fun f vs n) = (size' f + (\<Sum>v\<leftarrow>vs. size' v))+1" | |
|
348 "size' (A_ML v vs) = (size' v + (\<Sum>v\<leftarrow>vs. size' v))+1" | |
|
349 "size' (apply v w) = (size' v + size' w)+1" | |
|
350 "size' (CC nm) = 1" | |
|
351 "size' (V_ML X) = 1" | |
|
352 "size' (Lam_ML v) = size' v + 1" |
|
353 |
|
354 lemma listsum_size'[simp]: |
|
355 "v \<in> set vs \<Longrightarrow> size' v < Suc(listsum (map size' vs))" |
|
356 sorry |
|
357 |
|
358 corollary cor_listsum_size'[simp]: |
|
359 "v \<in> set vs \<Longrightarrow> size' v < Suc(m + listsum (map size' vs))" |
|
360 using listsum_size'[of v vs] by arith |
|
361 |
|
362 lemma |
|
363 size_subst_ML[simp]: includes Vars assumes A: "!i. size(f i) = 0" |
|
364 shows "size(subst\<^bsub>ML\<^esub> f t) = size(t)" |
|
365 and "size(subst\<^bsub>ML\<^esub> f v) = size(v)" |
|
366 and "ml_list_size1 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size1 vs" |
|
367 and "ml_list_size2 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size2 vs" |
|
368 and "ml_list_size3 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size3 vs" |
|
369 and "ml_list_size4 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size4 vs" |
|
370 by (induct rule: tm_ml.inducts) (simp_all add: A cons_ML_def split:nat.split) |
|
371 |
|
372 lemma [simp]: |
|
373 "\<forall>i j. size'(f i) = size'(V_ML j) \<Longrightarrow> size' (subst\<^bsub>ML\<^esub> f v) = size' v" |
|
374 sorry |
|
375 |
|
376 lemma [simp]: "size' (lift i v) = size' v" |
|
377 sorry |
|
378 |
|
379 (* the kernel function as in Section 4.1 of "Operational aspects\<dots>" *) |
|
380 |
|
381 function kernel :: "ml \<Rightarrow> tm" ("_!" 300) where |
|
382 "(C nm vs)! = foldl At (Ct nm) (map kernel vs)" | |
|
383 "(Lam_ML v)! = Lam (((lift 0 v)[V 0 []/0])!)" | |
|
384 "(Fun f vs n)! = foldl At (f!) (map kernel vs)" | |
|
385 "(A_ML v vs)! = foldl At (v!) (map kernel vs)" | |
|
386 "(apply v w)! = At (v!) (w!)" | |
|
387 "(CC nm)! = Ct nm" | |
|
388 "(V x vs)! = foldl At (Vt x) (map kernel vs)" | |
|
389 "(V_ML X)! = undefined" |
|
390 by pat_completeness auto |
|
391 termination by(relation "measure size'") auto |
|
392 |
|
393 consts kernelt :: "tm \<Rightarrow> tm" ("_!" 300) |
|
394 primrec |
|
395 "(Ct nm)! = Ct nm" |
|
396 "(term_of v)! = v!" |
|
397 "(Vt x)! = Vt x" |
|
398 "(At s t)! = At (s!) (t!)" |
|
399 "(Lam t)! = Lam (t!)" |
|
400 |
|
401 abbreviation |
|
402 kernels :: "ml list \<Rightarrow> tm list" ("_!" 300) where |
|
403 "vs ! == map kernel vs" |
|
404 |
|
405 (* soundness of the code generator *) |
|
406 axioms |
|
407 compiler_correct: |
|
408 "(nm, vs, v) : compR ==> ALL i. ML_closed 0 (f i) \<Longrightarrow> (nm, (map (subst\<^bsub>ML\<^esub> f) vs)!, (subst\<^bsub>ML\<^esub> f v)!) : R" |
|
409 |
|
410 |
|
411 consts |
|
412 free_vars :: "tm \<Rightarrow> lam_var_name set" |
|
413 primrec |
|
414 "free_vars (Ct nm) = {}" |
|
415 "free_vars (Vt x) = {x}" |
|
416 "free_vars (Lam t) = {i. EX j : free_vars t. j = i+1}" |
|
417 "free_vars (At s t) = free_vars s \<union> free_vars t" |
|
418 |
|
419 lemma [simp]: "t : Pure_tms \<Longrightarrow> lift\<^bsub>ML\<^esub> k t = t" |
|
420 by (erule Pure_tms.induct) simp_all |
|
421 |
|
422 lemma kernel_pure: includes Vars assumes "t : Pure_tms" shows "t! = t" |
|
423 using assms by (induct) simp_all |
|
424 |
|
425 lemma lift_eval: |
|
426 "t : Pure_tms \<Longrightarrow> ALL e k. (ALL i : free_vars t. i < size e) --> lift k (eval t e) = eval t (map (lift k) e)" |
|
427 apply(induct set:Pure_tms) |
|
428 apply simp_all |
|
429 apply clarsimp |
|
430 apply(erule_tac x = "V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in allE) |
|
431 apply simp |
|
432 apply(erule impE) |
|
433 apply clarsimp |
|
434 apply(case_tac i)apply simp |
|
435 apply simp |
|
436 apply (simp add: map_compose[symmetric]) |
|
437 apply (simp add: o_def lift_lift_ML_comm) |
|
438 done |
|
439 |
|
440 lemma lift_ML_eval[rule_format]: |
|
441 "t : Pure_tms \<Longrightarrow> ALL e k. (ALL i : free_vars t. i < size e) --> lift\<^bsub>ML\<^esub> k (eval t e) = eval t (map (lift\<^bsub>ML\<^esub> k) e)" |
|
442 apply(induct set:Pure_tms) |
|
443 apply simp_all |
|
444 apply clarsimp |
|
445 apply(erule_tac x = "V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in allE) |
|
446 apply simp |
|
447 apply(erule impE) |
|
448 apply clarsimp |
|
449 apply(case_tac i)apply simp |
|
450 apply simp |
|
451 apply (simp add: map_compose[symmetric]) |
|
452 apply (simp add:o_def lift_lift_ML) |
|
453 done |
|
454 |
|
455 lemma [simp]: includes Vars shows "(v ## f) 0 = v" |
|
456 by(simp add:cons_ML_def) |
|
457 |
|
458 lemma [simp]: includes Vars shows "(v ## f) (Suc n) = lift\<^bsub>ML\<^esub> 0 (f n)" |
|
459 by(simp add:cons_ML_def) |
|
460 |
|
461 lemma lift_o_shift: "lift k o (V_ML 0 ## f) = (V_ML 0 ## (lift k \<circ> f))" |
|
462 apply(rule ext) |
|
463 apply (simp add:cons_ML_def lift_lift_ML_comm split:nat.split) |
|
464 done |
|
465 |
|
466 lemma lift_subst_ML: shows |
|
467 "lift_tm k (subst\<^bsub>ML\<^esub> f t) = subst\<^bsub>ML\<^esub> (lift_ml k o f) (lift_tm k t)" and |
|
468 "lift_ml k (subst\<^bsub>ML\<^esub> f v) = subst\<^bsub>ML\<^esub> (lift_ml k o f) (lift_ml k v)" |
|
469 apply (induct t and v arbitrary: f k and f k rule: lift_tm_lift_ml.induct) |
|
470 apply (simp_all add:map_compose[symmetric] o_assoc lift_o_lift lift_o_shift) |
|
471 done |
|
472 |
|
473 corollary lift_subst_ML1: "\<forall>v k. lift_ml 0 (u[v/k]) = (lift_ml 0 u)[lift 0 v/k]" |
|
474 apply(rule measure_induct[where f = "size" and a = u]) |
|
475 apply(case_tac x) |
|
476 apply(simp_all add:lift_lift map_compose[symmetric] lift_subst_ML) |
|
477 apply(subst lift_lift_ML_comm)apply simp |
|
478 done |
|
479 |
|
480 lemma lift_ML_lift_ML: includes Vars shows |
|
481 "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i t) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k t)" |
|
482 and "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i v) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k v)" |
|
483 apply (induct k t and k v arbitrary: i k and i k |
|
484 rule: lift_tm_ML_lift_ml_ML.induct) |
|
485 apply(simp_all add:map_compose[symmetric]) |
|
486 done |
|
487 |
|
488 corollary lift_ML_o_lift_ML: shows |
|
489 "i < k+1 \<Longrightarrow> lift_tm_ML (Suc k) o (lift_tm_ML i) = lift_tm_ML i o lift_tm_ML k" and |
|
490 "i < k+1 \<Longrightarrow> lift_ml_ML (Suc k) o (lift_ml_ML i) = lift_ml_ML i o lift_ml_ML k" |
|
491 by(rule ext, simp add:lift_ML_lift_ML)+ |
|
492 |
|
493 abbreviation insrt where |
|
494 "insrt k f == (%i. if i<k then lift_ml_ML k (f i) else if i=k then V_ML k else lift_ml_ML k (f(i - 1)))" |
|
495 |
|
496 lemma subst_insrt_lift: includes Vars shows |
|
497 "subst\<^bsub>ML\<^esub> (insrt k f) (lift\<^bsub>ML\<^esub> k t) = lift\<^bsub>ML\<^esub> k (subst\<^bsub>ML\<^esub> f t)" and |
|
498 "subst\<^bsub>ML\<^esub> (insrt k f) (lift\<^bsub>ML\<^esub> k v) = lift\<^bsub>ML\<^esub> k (subst\<^bsub>ML\<^esub> f v)" |
|
499 apply (induct k t and k v arbitrary: f k and f k rule: lift_tm_ML_lift_ml_ML.induct) |
|
500 apply (simp_all add:map_compose[symmetric] o_assoc lift_o_lift lift_o_shift) |
|
501 apply(subgoal_tac "lift 0 \<circ> insrt k f = insrt k (lift 0 \<circ> f)") |
|
502 apply simp |
|
503 apply(rule ext) |
|
504 apply (simp add:lift_lift_ML_comm) |
|
505 apply(subgoal_tac "V_ML 0 ## insrt k f = insrt (Suc k) (V_ML 0 ## f)") |
|
506 apply simp |
|
507 apply(rule ext) |
|
508 apply (simp add:lift_ML_lift_ML cons_ML_def split:nat.split) |
|
509 done |
|
510 |
|
511 corollary subst_cons_lift: includes Vars shows |
|
512 "subst\<^bsub>ML\<^esub> (V_ML 0 ## f) o (lift_ml_ML 0) = lift_ml_ML 0 o (subst_ml_ML f)" |
|
513 apply(rule ext) |
|
514 apply(simp add: cons_ML_def subst_insrt_lift[symmetric]) |
|
515 apply(subgoal_tac "nat_case (V_ML 0) (\<lambda>j. lift\<^bsub>ML\<^esub> 0 (f j)) = (\<lambda>i. if i = 0 then V_ML 0 else lift\<^bsub>ML\<^esub> 0 (f (i - 1)))") |
|
516 apply simp |
|
517 apply(rule ext, simp split:nat.split) |
|
518 done |
|
519 |
|
520 lemma subst_eval[rule_format]: "t : Pure_tms \<Longrightarrow> |
|
521 ALL f e. (ALL i : free_vars t. i < size e) \<longrightarrow> subst\<^bsub>ML\<^esub> f (eval t e) = eval t (map (subst\<^bsub>ML\<^esub> f) e)" |
|
522 apply(induct set:Pure_tms) |
|
523 apply simp_all |
|
524 apply clarsimp |
|
525 apply(erule_tac x="V_ML 0 ## f" in allE) |
|
526 apply(erule_tac x= "(V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e)" in allE) |
|
527 apply(erule impE) |
|
528 apply clarsimp |
|
529 apply(case_tac i)apply simp |
|
530 apply simp |
|
531 apply (simp add:subst_cons_lift map_compose[symmetric]) |
|
532 done |
|
533 |
|
534 |
|
535 theorem kernel_eval[rule_format]: includes Vars shows |
|
536 "t : Pure_tms ==> |
|
537 ALL e. (ALL i : free_vars t. i < size e) \<longrightarrow> (ALL i < size e. e!i = V i []) --> (eval t e)! = t!" |
|
538 apply(induct set:Pure_tms) |
|
539 apply simp_all |
|
540 apply clarsimp |
|
541 apply(subst lift_eval) apply simp |
|
542 apply clarsimp |
|
543 apply(case_tac i)apply simp |
|
544 apply simp |
|
545 apply(subst subst_eval) apply simp |
|
546 apply clarsimp |
|
547 apply(case_tac i)apply simp |
|
548 apply simp |
|
549 apply(erule_tac x="map (subst\<^bsub>ML\<^esub> (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1))) |
|
550 (map (lift 0) (V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e))" in allE) |
|
551 apply(erule impE) |
|
552 apply(clarsimp) |
|
553 apply(case_tac i)apply simp |
|
554 apply simp |
|
555 apply(erule impE) |
|
556 apply(clarsimp) |
|
557 apply(case_tac i)apply simp |
|
558 apply simp |
|
559 apply simp |
|
560 done |
|
561 |
|
562 (* |
|
563 lemma subst_ML_compose: |
|
564 "subst_ml_ML f2 (subst_ml_ML f1 v) = subst_ml_ML (%i. subst_ml_ML f2 (f1 i)) v" |
|
565 sorry |
|
566 *) |
|
567 |
|
568 lemma map_eq_iff_nth: |
|
569 "(map f xs = map g xs) = (!i<size xs. f(xs!i) = g(xs!i))" |
|
570 sorry |
|
571 |
|
572 lemma [simp]: includes Vars shows "ML_closed k v \<Longrightarrow> lift\<^bsub>ML\<^esub> k v = v" |
|
573 sorry |
|
574 lemma [simp]: includes Vars shows "ML_closed 0 v \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = v" |
|
575 sorry |
|
576 lemma [simp]: includes Vars shows "ML_closed k v \<Longrightarrow> ML_closed k (lift m v)" |
|
577 sorry |
|
578 |
|
579 lemma red_Lam[simp]: includes Vars shows "t \<rightarrow>* t' ==> Lam t \<rightarrow>* Lam t'" |
|
580 apply(induct rule:rtrancl_induct) |
|
581 apply(simp_all) |
|
582 apply(blast intro: rtrancl_into_rtrancl tRed.intros) |
|
583 done |
|
584 |
|
585 lemma red_At1[simp]: includes Vars shows "t \<rightarrow>* t' ==> At t s \<rightarrow>* At t' s" |
|
586 apply(induct rule:rtrancl_induct) |
|
587 apply(simp_all) |
|
588 apply(blast intro: rtrancl_into_rtrancl tRed.intros) |
|
589 done |
|
590 |
|
591 lemma red_At2[simp]: includes Vars shows "t \<rightarrow>* t' ==> At s t \<rightarrow>* At s t'" |
|
592 apply(induct rule:rtrancl_induct) |
|
593 apply(simp_all) |
|
594 apply(blast intro:rtrancl_into_rtrancl tRed.intros) |
|
595 done |
|
596 |
|
597 lemma tRed_list_foldl_At: |
|
598 "ts \<rightarrow>* ts' \<Longrightarrow> s \<rightarrow>* s' \<Longrightarrow> foldl At s ts \<rightarrow>* foldl At s' ts'" |
|
599 apply(induct arbitrary:s s' rule:tRed_list.induct) |
|
600 apply simp |
|
601 apply simp |
|
602 apply(blast dest: red_At1 red_At2 intro:rtrancl_trans) |
|
603 done |
|
604 |
|
605 lemma [trans]: "s = t \<Longrightarrow> t \<rightarrow> t' \<Longrightarrow> s \<rightarrow> t'" |
|
606 by simp |
|
607 |
|
608 |
|
609 lemma subst_foldl[simp]: |
|
610 "subst f (foldl At s ts) = foldl At (subst f s) (map (subst f) ts)" |
|
611 by (induct ts arbitrary: s) auto |
|
612 |
|
613 |
|
614 lemma foldl_At_size: "size ts = size ts' \<Longrightarrow> |
|
615 foldl At s ts = foldl At s' ts' \<longleftrightarrow> s = s' & ts = ts'" |
|
616 by (induct arbitrary: s s' rule:list_induct2) simp_all |
|
617 |
|
618 consts depth_At :: "tm \<Rightarrow> nat" |
|
619 primrec |
|
620 "depth_At(Ct cn) = 0" |
|
621 "depth_At(Vt x) = 0" |
|
622 "depth_At(Lam t) = 0" |
|
623 "depth_At(At s t) = depth_At s + 1" |
|
624 "depth_At(term_of v) = 0" |
|
625 |
|
626 lemma depth_At_foldl: |
|
627 "depth_At(foldl At s ts) = depth_At s + size ts" |
|
628 by (induct ts arbitrary: s) simp_all |
|
629 |
|
630 lemma foldl_At_eq_length: |
|
631 "foldl At s ts = foldl At s ts' \<Longrightarrow> length ts = length ts'" |
|
632 apply(subgoal_tac "depth_At(foldl At s ts) = depth_At(foldl At s ts')") |
|
633 apply(erule thin_rl) |
|
634 apply (simp add:depth_At_foldl) |
|
635 apply simp |
|
636 done |
|
637 |
|
638 lemma foldl_At_eq[simp]: "foldl At s ts = foldl At s ts' \<longleftrightarrow> ts = ts'" |
|
639 apply(rule) |
|
640 prefer 2 apply simp |
|
641 apply(blast dest:foldl_At_size foldl_At_eq_length) |
|
642 done |
|
643 |
|
644 lemma [simp]: "foldl At s ts ! = foldl At (s!) (map kernelt ts)" |
|
645 by (induct ts arbitrary: s) simp_all |
|
646 |
|
647 lemma [simp]: "(kernelt \<circ> term_of) = kernel" |
|
648 by(rule ext) simp |
|
649 |
|
650 lemma shift_subst_decr: |
|
651 "Vt 0 ## subst_decr k t = subst_decr (Suc k) (lift 0 t)" |
|
652 apply(rule ext) |
|
653 apply (simp add:cons_def split:nat.split) |
|
654 done |
|
655 |
|
656 lemma [simp]: "lift k (foldl At s ts) = foldl At (lift k s) (map (lift k) ts)" |
|
657 by(induct ts arbitrary:s) simp_all |
|
658 |
|
659 subsection "Horrible detour" |
|
660 |
|
661 definition "liftn n == lift_ml 0 ^ n" |
|
662 |
|
663 lemma [simp]: "liftn n (C i vs) = C i (map (liftn n) vs)" |
|
664 apply(unfold liftn_def) |
|
665 apply(induct n) |
|
666 apply (simp_all add: map_compose[symmetric]) |
|
667 done |
|
668 |
|
669 lemma [simp]: "liftn n (CC nm) = CC nm" |
|
670 apply(unfold liftn_def) |
|
671 apply(induct n) |
|
672 apply (simp_all add: map_compose[symmetric]) |
|
673 done |
|
674 |
|
675 lemma [simp]: "liftn n (apply v w) = apply (liftn n v) (liftn n w)" |
|
676 apply(unfold liftn_def) |
|
677 apply(induct n) |
|
678 apply (simp_all add: map_compose[symmetric]) |
|
679 done |
|
680 |
|
681 lemma [simp]: "liftn n (A_ML v vs) = A_ML (liftn n v) (map (liftn n) vs)" |
|
682 apply(unfold liftn_def) |
|
683 apply(induct n) |
|
684 apply (simp_all add: map_compose[symmetric]) |
|
685 done |
|
686 |
|
687 lemma [simp]: |
|
688 "liftn n (Fun v vs i) = Fun (liftn n v) (map (liftn n) vs) i" |
|
689 apply(unfold liftn_def) |
|
690 apply(induct n) |
|
691 apply (simp_all add: map_compose[symmetric] id_def) |
|
692 done |
|
693 |
|
694 lemma [simp]: "liftn n (Lam_ML v) = Lam_ML (liftn n v)" |
|
695 apply(unfold liftn_def) |
|
696 apply(induct n) |
|
697 apply (simp_all add: map_compose[symmetric] id_def) |
|
698 done |
|
699 |
|
700 lemma liftn_liftn_add: "liftn m (liftn n v) = liftn (m+n) v" |
|
701 by(simp add:liftn_def funpow_add) |
|
702 |
|
703 lemma [simp]: "liftn n (V_ML k) = V_ML k" |
|
704 apply(unfold liftn_def) |
|
705 apply(induct n) |
|
706 apply (simp_all) |
|
707 done |
|
708 |
|
709 lemma liftn_lift_ML_comm: "liftn n (lift\<^bsub>ML\<^esub> 0 v) = lift\<^bsub>ML\<^esub> 0 (liftn n v)" |
|
710 apply(unfold liftn_def) |
|
711 apply(induct n) |
|
712 apply (simp_all add:lift_lift_ML_comm) |
|
713 done |
|
714 |
|
715 lemma liftn_cons: "liftn n ((V_ML 0 ## f) x) = (V_ML 0 ## (liftn n o f)) x" |
|
716 apply(simp add:cons_ML_def liftn_lift_ML_comm split:nat.split) |
|
717 done |
|
718 |
|
719 text{* End of horrible detour *} |
|
720 |
|
721 lemma kernel_subst1: |
|
722 "ML_closed 1 u \<Longrightarrow> ML_closed 0 v \<Longrightarrow> kernel( u[v/0]) = (kernel((lift 0 u)[V 0 []/0]))[kernel v/0]" |
|
723 sorry |
|
724 |
|
725 lemma includes Vars shows foldl_Pure[simp]: |
|
726 "t : Pure_tms \<Longrightarrow> \<forall>t\<in>set ts. t : Pure_tms \<Longrightarrow> |
|
727 (!!s t. s : Pure_tms \<Longrightarrow> t : Pure_tms \<Longrightarrow> f s t : Pure_tms) \<Longrightarrow> |
|
728 foldl f t ts \<in> Pure_tms" |
|
729 by(induct ts arbitrary: t) simp_all |
|
730 |
|
731 declare Pure_tms.intros[simp] |
|
732 |
|
733 lemma includes Vars shows "ML_closed 0 v \<Longrightarrow> kernel v : Pure_tms" |
|
734 apply(induct rule:kernel.induct) |
|
735 apply simp_all |
|
736 apply(rule Pure_tms.intros); |
|
737 (* "ML_closed (Suc k) v \<Longrightarrow> ML_closed k (lift 0 v)" *) |
|
738 sorry |
|
739 |
|
740 lemma subst_Vt: includes Vars shows "subst Vt = id" |
|
741 sorry |
|
742 (* |
|
743 apply(rule ext) |
|
744 apply(induct_tac x) |
|
745 apply simp_all |
|
746 |
|
747 done |
|
748 *) |
|
749 (* klappt noch nicht ganz *) |
|
750 theorem Red_sound: includes Vars |
|
751 shows "v \<Rightarrow> v' \<Longrightarrow> ML_closed 0 v \<Longrightarrow> v! \<rightarrow>* v'! & ML_closed 0 v'" |
|
752 and "t \<Rightarrow> t' \<Longrightarrow> ML_closed_t 0 t \<Longrightarrow> kernelt t \<rightarrow>* kernelt t' & ML_closed_t 0 t'" |
|
753 and "(vs :: ml list) \<Rightarrow> vs' \<Longrightarrow> !v : set vs . ML_closed 0 v \<Longrightarrow> map kernel vs \<rightarrow>* map kernel vs' & (! v':set vs'. ML_closed 0 v')" |
|
754 proof(induct rule:Red_Redt_Redl.inducts) |
|
755 fix u v |
|
756 let ?v = "A_ML (Lam_ML u) [v]" |
|
757 assume cl: "ML_closed 0 (A_ML (Lam_ML u) [v])" |
|
758 let ?u' = "(lift_ml 0 u)[V 0 []/0]" |
|
759 have "?v! = At (Lam ((?u')!)) (v !)" by simp |
|
760 also have "\<dots> \<rightarrow> (?u' !)[v!/0]" (is "_ \<rightarrow> ?R") by(rule tRed.intros) |
|
761 also have "?R = u[v/0]!" using cl |
|
762 apply(cut_tac u = "u" and v = "v" in kernel_subst1) |
|
763 apply(simp_all) |
|
764 done |
|
765 finally have "kernel(A_ML (Lam_ML u) [v]) \<rightarrow>* kernel(u[v/0])" (is ?A) by(rule r_into_rtrancl) |
|
766 moreover have "ML_closed 0 (u[v/0])" (is "?C") using cl apply simp sorry |
|
767 ultimately show "?A & ?C" .. |
|
768 next |
|
769 case term_of_C thus ?case apply (auto simp:map_compose[symmetric])sorry |
|
770 next |
|
771 fix f :: "nat \<Rightarrow> ml" and nm vs v |
|
772 assume f: "\<forall>i. ML_closed 0 (f i)" and compR: "(nm, vs, v) \<in> compR" |
|
773 note tRed.intros(2)[OF compiler_correct[OF compR f], of Vt,simplified map_compose[symmetric]] |
|
774 hence red: "foldl At (Ct nm) (map (kernel o subst\<^bsub>ML\<^esub> f) vs) \<rightarrow> |
|
775 (subst\<^bsub>ML\<^esub> f v)!" (is "_ \<rightarrow> ?R") apply(simp add:map_compose) sorry |
|
776 have "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! = |
|
777 foldl At (Ct nm) (map (kernel o subst\<^bsub>ML\<^esub> f) vs)" by (simp add:map_compose) |
|
778 also(* have "map (kernel o subst\<^bsub>ML\<^esub> f) vs = map (subst (kernel o f)) (vs!)" |
|
779 using closed_subst_kernel(2)[OF compiled_V_free1[OF compR]] |
|
780 by (simp add:map_compose[symmetric]) |
|
781 also*) note red |
|
782 (*also have "?R = subst\<^bsub>ML\<^esub> f v!" |
|
783 using closed_subst_kernel(2)[OF compiled_V_free2[OF compR]] by simp*) |
|
784 finally have "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! \<rightarrow>* subst\<^bsub>ML\<^esub> f v!" (is "?A") |
|
785 by(rule r_into_rtrancl) (* |
|
786 also have "?l = (subst\<^bsub>ML\<^esub> fa (A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)))!" (is "_ = ?l'") sorry |
|
787 also have "?r = subst\<^bsub>ML\<^esub> fa (subst\<^bsub>ML\<^esub> f v)!" (is "_ = ?r'") sorry |
|
788 finally have "?l' \<rightarrow>* ?r'" (is ?A) . *) |
|
789 moreover have "ML_closed 0 (subst\<^bsub>ML\<^esub> f v)" (is "?C") using prems sorry |
|
790 ultimately show "?A & ?C" .. |
|
791 next |
|
792 case term_of_V thus ?case apply (auto simp:map_compose[symmetric]) sorry |
|
793 next |
|
794 case (term_of_Fun n vf vs) |
|
795 hence "term_of (Fun vf vs n)! \<rightarrow>* |
|
796 Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0]))!" sorry |
|
797 moreover |
|
798 have "ML_closed_t 0 |
|
799 (Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0])))" sorry |
|
800 ultimately show ?case .. |
|
801 next |
|
802 case apply_Fun1 thus ?case by simp |
|
803 next |
|
804 case apply_Fun2 thus ?case by simp |
|
805 next |
|
806 case apply_C thus ?case by simp |
|
807 next |
|
808 case apply_V thus ?case by simp |
|
809 next |
|
810 case ctxt_Lam thus ?case by(auto) |
|
811 next |
|
812 case ctxt_At1 thus ?case by(auto) |
|
813 next |
|
814 case ctxt_At2 thus ?case by (auto) |
|
815 next |
|
816 case ctxt_term_of thus ?case by (auto) |
|
817 next |
|
818 case ctxt_C thus ?case by (fastsimp simp:tRed_list_foldl_At) |
|
819 next |
|
820 case ctxt_V thus ?case by (fastsimp simp:tRed_list_foldl_At) |
|
821 next |
|
822 case ctxt_Fun1 thus ?case by (fastsimp simp:tRed_list_foldl_At) |
|
823 next |
|
824 case ctxt_Fun3 thus ?case by (fastsimp simp:tRed_list_foldl_At) |
|
825 next |
|
826 case ctxt_apply1 thus ?case by auto |
|
827 next |
|
828 case ctxt_apply2 thus ?case by auto |
|
829 next |
|
830 case ctxt_A_ML1 thus ?case by (fastsimp simp:tRed_list_foldl_At) |
|
831 next |
|
832 case ctxt_A_ML2 thus ?case by (fastsimp simp:tRed_list_foldl_At) |
|
833 next |
|
834 case ctxt_list1 thus ?case by simp |
|
835 next |
|
836 case ctxt_list2 thus ?case by simp |
|
837 qed |
|
838 |
|
839 |
|
840 inductive_cases tRedE: "Ct n \<rightarrow> u" |
|
841 thm tRedE |
|
842 |
|
843 lemma [simp]: "Ct n = foldl At t ts \<longleftrightarrow> t = Ct n & ts = []" |
|
844 by (induct ts arbitrary:t) auto |
|
845 |
|
846 corollary kernel_inv: includes Vars shows |
|
847 "(t :: tm) \<Rightarrow>* t' ==> ML_closed_t 0 t ==> t! \<rightarrow>* t'!" |
|
848 sorry |
|
849 |
|
850 theorem includes Vars |
|
851 assumes t: "t : Pure_tms" and t': "t' : Pure_tms" and |
|
852 closed: "free_vars t = {}" and reds: "term_of (eval t []) \<Rightarrow>* t'" |
|
853 shows "t \<rightarrow>* t' " |
|
854 proof - |
|
855 have ML_cl: "ML_closed_t 0 (term_of (eval t []))" sorry |
|
856 have "(eval t [])! = t!" |
|
857 using kernel_eval[OF t, where e="[]"] closed by simp |
|
858 hence "(term_of (eval t []))! = t!" by simp |
|
859 moreover have "term_of (eval t [])! \<rightarrow>* t'!" |
|
860 using kernel_inv[OF reds ML_cl] by auto |
|
861 ultimately have "t! \<rightarrow>* t'!" by simp |
|
862 thus ?thesis using kernel_pure t t' by auto |
|
863 qed |
|
864 |
|
865 end |