23503
|
1 |
(* ID: $Id$
|
|
2 |
Author: Klaus Aehlig, Tobias Nipkow
|
|
3 |
Work in progress
|
|
4 |
*)
|
25876
|
5 |
header {* Normalization by Evaluation *}
|
23503
|
6 |
|
23854
|
7 |
theory NBE imports Main Executable_Set begin
|
23503
|
8 |
|
25876
|
9 |
ML"Syntax.ambiguity_level := 1000000"
|
|
10 |
|
23503
|
11 |
declare Let_def[simp]
|
|
12 |
|
|
13 |
consts_code undefined ("(raise Match)")
|
|
14 |
|
|
15 |
(*typedecl const_name*)
|
|
16 |
types lam_var_name = nat
|
|
17 |
ml_var_name = nat
|
|
18 |
const_name = nat
|
|
19 |
|
25873
|
20 |
datatype ml = (* rep of universal datatype *)
|
23503
|
21 |
C const_name "ml list" | V lam_var_name "ml list"
|
|
22 |
| Fun ml "ml list" nat
|
|
23 |
| "apply" ml ml (* function 'apply' *)
|
|
24 |
(* ML *)
|
|
25 |
| V_ML ml_var_name | A_ML ml "ml list" | Lam_ML ml
|
|
26 |
| CC const_name (* ref to compiled code *)
|
|
27 |
|
25873
|
28 |
datatype tm = Ct const_name | Vt lam_var_name | Lam tm | At tm tm
|
|
29 |
| term_of ml (* function 'to_term' *)
|
|
30 |
|
25680
|
31 |
lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (list_size size vs)"
|
23503
|
32 |
by (induct vs) auto
|
25680
|
33 |
lemma [simp]:"x \<in> set vs \<Longrightarrow> size x < Suc (size v + list_size size vs)"
|
23503
|
34 |
by (induct vs) auto
|
|
35 |
|
|
36 |
locale Vars =
|
|
37 |
fixes r s t:: tm
|
|
38 |
and rs ss ts :: "tm list"
|
|
39 |
and u v w :: ml
|
|
40 |
and us vs ws :: "ml list"
|
|
41 |
and nm :: const_name
|
|
42 |
and x :: lam_var_name
|
|
43 |
and X :: ml_var_name
|
|
44 |
|
23778
|
45 |
inductive_set Pure_tms :: "tm set"
|
|
46 |
where
|
|
47 |
"Ct s : Pure_tms"
|
|
48 |
| "Vt x : Pure_tms"
|
|
49 |
| "t : Pure_tms ==> Lam t : Pure_tms"
|
|
50 |
| "s : Pure_tms ==> t : Pure_tms ==> At s t : Pure_tms"
|
23503
|
51 |
|
|
52 |
consts
|
|
53 |
R :: "(const_name * tm list * tm)set" (* reduction rules *)
|
|
54 |
compR :: "(const_name * ml list * ml)set" (* compiled reduction rules *)
|
|
55 |
|
25876
|
56 |
fun lift_ml :: "nat \<Rightarrow> ml \<Rightarrow> ml" ("lift") where
|
23503
|
57 |
"lift i (C nm vs) = C nm (map (lift i) vs)" |
|
|
58 |
"lift i (V x vs) = V (if x < i then x else x+1) (map (lift i) vs)" |
|
|
59 |
"lift i (Fun v vs n) = Fun (lift i v) (map (lift i) vs) n" |
|
|
60 |
"lift i (apply u v) = apply (lift i u) (lift i v)" |
|
|
61 |
"lift i (V_ML X) = V_ML X" |
|
|
62 |
"lift i (A_ML v vs) = A_ML (lift i v) (map (lift i) vs)" |
|
|
63 |
"lift i (Lam_ML v) = Lam_ML (lift i v)" |
|
|
64 |
"lift i (CC nm) = CC nm"
|
25876
|
65 |
|
|
66 |
lemmas ml_induct = lift_ml.induct[of "%i v. P v", standard]
|
23503
|
67 |
|
25876
|
68 |
fun lift_tm :: "nat \<Rightarrow> tm \<Rightarrow> tm" ("lift") where
|
|
69 |
"lift i (Ct nm) = Ct nm" |
|
|
70 |
"lift i (Vt x) = Vt(if x < i then x else x+1)" |
|
|
71 |
"lift i (Lam t) = Lam (lift (i+1) t)" |
|
|
72 |
"lift i (At s t) = At (lift i s) (lift i t)" |
|
|
73 |
"lift i (term_of v) = term_of (lift i v)"
|
23503
|
74 |
|
25876
|
75 |
fun lift_ml_ML :: "nat \<Rightarrow> ml \<Rightarrow> ml" ("lift\<^bsub>ML\<^esub>") where
|
23503
|
76 |
"lift\<^bsub>ML\<^esub> i (C nm vs) = C nm (map (lift\<^bsub>ML\<^esub> i) vs)" |
|
|
77 |
"lift\<^bsub>ML\<^esub> i (V x vs) = V x (map (lift\<^bsub>ML\<^esub> i) vs)" |
|
|
78 |
"lift\<^bsub>ML\<^esub> i (Fun v vs n) = Fun (lift\<^bsub>ML\<^esub> i v) (map (lift\<^bsub>ML\<^esub> i) vs) n" |
|
|
79 |
"lift\<^bsub>ML\<^esub> i (apply u v) = apply (lift\<^bsub>ML\<^esub> i u) (lift\<^bsub>ML\<^esub> i v)" |
|
|
80 |
"lift\<^bsub>ML\<^esub> i (V_ML X) = V_ML (if X < i then X else X+1)" |
|
|
81 |
"lift\<^bsub>ML\<^esub> i (A_ML v vs) = A_ML (lift\<^bsub>ML\<^esub> i v) (map (lift\<^bsub>ML\<^esub> i) vs)" |
|
|
82 |
"lift\<^bsub>ML\<^esub> i (Lam_ML v) = Lam_ML (lift\<^bsub>ML\<^esub> (i+1) v)" |
|
|
83 |
"lift\<^bsub>ML\<^esub> i (CC nm) = CC nm"
|
25876
|
84 |
|
|
85 |
fun lift_tm_ML :: "nat \<Rightarrow> tm \<Rightarrow> tm" ("lift\<^bsub>ML\<^esub>") where
|
|
86 |
"lift\<^bsub>ML\<^esub> i (Ct nm) = Ct nm" |
|
|
87 |
"lift\<^bsub>ML\<^esub> i (Vt x) = Vt x" |
|
|
88 |
"lift\<^bsub>ML\<^esub> i (Lam t) = Lam (lift\<^bsub>ML\<^esub> i t)" |
|
|
89 |
"lift\<^bsub>ML\<^esub> i (At s t) = At (lift\<^bsub>ML\<^esub> i s) (lift\<^bsub>ML\<^esub> i t)" |
|
|
90 |
"lift\<^bsub>ML\<^esub> i (term_of v) = term_of (lift\<^bsub>ML\<^esub> i v)"
|
|
91 |
|
23503
|
92 |
constdefs
|
|
93 |
cons :: "tm \<Rightarrow> (nat \<Rightarrow> tm) \<Rightarrow> (nat \<Rightarrow> tm)" (infix "##" 65)
|
|
94 |
"t##f \<equiv> \<lambda>i. case i of 0 \<Rightarrow> t | Suc j \<Rightarrow> lift 0 (f j)"
|
|
95 |
cons_ML :: "ml \<Rightarrow> (nat \<Rightarrow> ml) \<Rightarrow> (nat \<Rightarrow> ml)" (infix "##" 65)
|
|
96 |
"v##f \<equiv> \<lambda>i. case i of 0 \<Rightarrow> v::ml | Suc j \<Rightarrow> lift\<^bsub>ML\<^esub> 0 (f j)"
|
|
97 |
|
25876
|
98 |
text{* Only for pure terms! *}
|
|
99 |
primrec subst :: "(nat \<Rightarrow> tm) \<Rightarrow> tm \<Rightarrow> tm" where
|
|
100 |
"subst f (Ct nm) = Ct nm" |
|
|
101 |
"subst f (Vt x) = f x" |
|
|
102 |
"subst f (Lam t) = Lam (subst (Vt 0 ## f) t)" |
|
23503
|
103 |
"subst f (At s t) = At (subst f s) (subst f t)"
|
|
104 |
|
25680
|
105 |
lemma list_size_map [simp]: "list_size f (map g xs) = list_size (f o g) xs"
|
25876
|
106 |
by (induct xs) simp_all
|
25680
|
107 |
|
|
108 |
lemma list_size_cong [cong]:
|
|
109 |
"\<lbrakk>xs = ys; \<And>x. x \<in> set ys \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> list_size f xs = list_size g ys"
|
25876
|
110 |
by (induct xs arbitrary: ys) auto
|
25680
|
111 |
|
25876
|
112 |
lemma size_lift_ml[simp]: "size(lift i (v::ml)) = size v"
|
|
113 |
by (induct i v rule: lift_ml.induct) simp_all
|
|
114 |
lemma size_lift_tm[simp]: "size(lift i t) = size(t::tm)"
|
|
115 |
by (induct i t rule: lift_tm.induct) simp_all
|
23503
|
116 |
|
25876
|
117 |
lemma size_lift_ml_ML[simp]: "size(lift\<^bsub>ML\<^esub> i (v::ml)) = size v"
|
|
118 |
by (induct i v rule: lift_ml_ML.induct) simp_all
|
|
119 |
lemma size_lift_tm_ML[simp]: "size(lift\<^bsub>ML\<^esub> i t) = size(t::tm)"
|
|
120 |
by (induct i t rule: lift_tm_ML.induct) simp_all
|
23503
|
121 |
|
25876
|
122 |
fun subst_ml_ML :: "(nat \<Rightarrow> ml) \<Rightarrow> ml \<Rightarrow> ml" ("subst\<^bsub>ML\<^esub>") where
|
23503
|
123 |
"subst\<^bsub>ML\<^esub> f (C nm vs) = C nm (map (subst\<^bsub>ML\<^esub> f) vs)" |
|
|
124 |
"subst\<^bsub>ML\<^esub> f (V x vs) = V x (map (subst\<^bsub>ML\<^esub> f) vs)" |
|
|
125 |
"subst\<^bsub>ML\<^esub> f (Fun v vs n) = Fun (subst\<^bsub>ML\<^esub> f v) (map (subst\<^bsub>ML\<^esub> f) vs) n" |
|
|
126 |
"subst\<^bsub>ML\<^esub> f (apply u v) = apply (subst\<^bsub>ML\<^esub> f u) (subst\<^bsub>ML\<^esub> f v)" |
|
|
127 |
"subst\<^bsub>ML\<^esub> f (V_ML X) = f X" |
|
|
128 |
"subst\<^bsub>ML\<^esub> f (A_ML v vs) = A_ML (subst\<^bsub>ML\<^esub> f v) (map (subst\<^bsub>ML\<^esub> f) vs)" |
|
|
129 |
"subst\<^bsub>ML\<^esub> f (Lam_ML v) = Lam_ML (subst\<^bsub>ML\<^esub> (V_ML 0 ## f) v)" |
|
|
130 |
"subst\<^bsub>ML\<^esub> f (CC nm) = CC nm"
|
|
131 |
|
25876
|
132 |
fun subst_tm_ML :: "(nat \<Rightarrow> ml) \<Rightarrow> tm \<Rightarrow> tm" ("subst\<^bsub>ML\<^esub>") where
|
|
133 |
"subst\<^bsub>ML\<^esub> f (Ct nm) = Ct nm" |
|
|
134 |
"subst\<^bsub>ML\<^esub> f (Vt x) = Vt x" |
|
|
135 |
"subst\<^bsub>ML\<^esub> f (Lam t) = Lam (subst\<^bsub>ML\<^esub> (lift 0 o f) t)" |
|
|
136 |
"subst\<^bsub>ML\<^esub> f (At s t) = At (subst\<^bsub>ML\<^esub> f s) (subst\<^bsub>ML\<^esub> f t)" |
|
|
137 |
"subst\<^bsub>ML\<^esub> f (term_of v) = term_of (subst\<^bsub>ML\<^esub> f v)"
|
|
138 |
|
23503
|
139 |
(* FIXME currrently needed for code generator *)
|
|
140 |
lemmas [code] = lift_tm_ML.simps lift_ml_ML.simps
|
|
141 |
lemmas [code] = lift_tm.simps lift_ml.simps
|
|
142 |
lemmas [code] = subst_tm_ML.simps subst_ml_ML.simps
|
|
143 |
|
|
144 |
abbreviation
|
|
145 |
subst_decr :: "nat \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> tm" where
|
|
146 |
"subst_decr k t == %n. if n<k then Vt n else if n=k then t else Vt(n - 1)"
|
|
147 |
abbreviation
|
|
148 |
subst_decr_ML :: "nat \<Rightarrow> ml \<Rightarrow> nat \<Rightarrow> ml" where
|
|
149 |
"subst_decr_ML k v == %n. if n<k then V_ML n else if n=k then v else V_ML(n - 1)"
|
|
150 |
abbreviation
|
|
151 |
subst1 :: "tm \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> tm" ("(_/[_'/_])" [300, 0, 0] 300) where
|
|
152 |
"s[t/k] == subst (subst_decr k t) s"
|
|
153 |
abbreviation
|
|
154 |
subst1_ML :: "ml \<Rightarrow> ml \<Rightarrow> nat \<Rightarrow> ml" ("(_/[_'/_])" [300, 0, 0] 300) where
|
|
155 |
"u[v/k] == subst\<^bsub>ML\<^esub> (subst_decr_ML k v) u"
|
|
156 |
|
|
157 |
|
25876
|
158 |
lemma size_subst_ml_ML[simp]:
|
|
159 |
"(!x. size(f x) = 0) \<longrightarrow> size(subst\<^bsub>ML\<^esub> f (v::ml)) = size v"
|
|
160 |
by (induct f v rule: subst_ml_ML.induct)
|
|
161 |
(simp_all add: cons_ML_def split: nat.split)
|
|
162 |
lemma size_subst_tm_ML[simp]:
|
25680
|
163 |
"(!x. size(f x) = 0) \<longrightarrow> size(subst\<^bsub>ML\<^esub> f t) = size(t::tm)"
|
25876
|
164 |
by (induct f t rule: subst_tm_ML.induct) (simp_all add: o_def)
|
23503
|
165 |
|
25876
|
166 |
lemma lift_lift_ml: includes Vars shows
|
|
167 |
"i < k+1 \<Longrightarrow> lift (Suc k) (lift i v) = lift i (lift k v)"
|
|
168 |
by(induct i v rule:lift_ml.induct)
|
|
169 |
(simp_all add:map_compose[symmetric])
|
|
170 |
lemma lift_lift_tm: includes Vars shows
|
23503
|
171 |
"i < k+1 \<Longrightarrow> lift (Suc k) (lift i t) = lift i (lift k t)"
|
25876
|
172 |
by(induct t arbitrary: i rule:lift_tm.induct)(simp_all add:lift_lift_ml)
|
23503
|
173 |
|
|
174 |
corollary lift_o_lift: shows
|
|
175 |
"i < k+1 \<Longrightarrow> lift_tm (Suc k) o (lift_tm i) = lift_tm i o lift_tm k" and
|
|
176 |
"i < k+1 \<Longrightarrow> lift_ml (Suc k) o (lift_ml i) = lift_ml i o lift_ml k"
|
25876
|
177 |
by(rule ext, simp add:lift_lift_ml lift_lift_tm)+
|
23503
|
178 |
|
25876
|
179 |
lemma lift_lift_ml_ML: includes Vars shows
|
|
180 |
"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)"
|
|
181 |
by(induct v arbitrary: i rule:lift_ml_ML.induct)
|
|
182 |
(simp_all add:map_compose[symmetric])
|
|
183 |
lemma lift_lift_tm_ML: includes Vars shows
|
|
184 |
"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)"
|
|
185 |
by(induct t arbitrary: i rule:lift_tm_ML.induct)(simp_all add:lift_lift_ml_ML)
|
23503
|
186 |
|
|
187 |
|
25876
|
188 |
lemma lift_lift_ml_ML_comm: includes Vars shows
|
|
189 |
"lift j (lift\<^bsub>ML\<^esub> i v) = lift\<^bsub>ML\<^esub> i (lift j v)"
|
|
190 |
by(induct v arbitrary: i j rule:lift_ml_ML.induct)
|
|
191 |
(simp_all add:map_compose[symmetric])
|
|
192 |
lemma lift_lift_tm_ML_comm: includes Vars shows
|
|
193 |
"lift j (lift\<^bsub>ML\<^esub> i t) = lift\<^bsub>ML\<^esub> i (lift j t)"
|
|
194 |
by(induct t arbitrary: i j rule:lift_tm_ML.induct)
|
|
195 |
(simp_all add:lift_lift_ml_ML_comm)
|
23503
|
196 |
|
|
197 |
lemma [simp]:
|
25876
|
198 |
"V_ML 0 ## subst_decr_ML k v = subst_decr_ML (Suc k) (lift\<^bsub>ML\<^esub> 0 v)"
|
23503
|
199 |
by(rule ext)(simp add:cons_ML_def split:nat.split)
|
|
200 |
|
|
201 |
lemma [simp]: "lift 0 o subst_decr_ML k v = subst_decr_ML k (lift 0 v)"
|
|
202 |
by(rule ext)(simp add:cons_ML_def split:nat.split)
|
|
203 |
|
25876
|
204 |
lemma subst_lift_ml_id[simp]: includes Vars shows "(lift\<^bsub>ML\<^esub> k u)[v/k] = u"
|
|
205 |
apply(induct k u arbitrary: v rule: lift_ml_ML.induct)
|
23503
|
206 |
apply (simp_all add:map_idI map_compose[symmetric])
|
|
207 |
apply (simp cong:if_cong)
|
|
208 |
done
|
25876
|
209 |
lemma subst_lift_tm_id[simp]: includes Vars shows
|
|
210 |
"subst\<^bsub>ML\<^esub> (subst_decr_ML k v) (lift\<^bsub>ML\<^esub> k t) = t"
|
|
211 |
by (induct k t arbitrary: v rule: lift_tm_ML.induct) simp_all
|
23503
|
212 |
|
23778
|
213 |
inductive_set
|
25873
|
214 |
tRed :: "(tm * tm)set" (* beta red + eta exp + R reduction on pure terms *)
|
23778
|
215 |
and tred :: "[tm, tm] => bool" (infixl "\<rightarrow>" 50)
|
|
216 |
where
|
23503
|
217 |
"s \<rightarrow> t == (s, t) \<in> tRed"
|
23778
|
218 |
| "At (Lam t) s \<rightarrow> t[s/0]"
|
25873
|
219 |
| "t \<rightarrow> Lam (At (lift 0 t) (Vt 0))"
|
23778
|
220 |
| "(nm,ts,t) : R ==> foldl At (Ct nm) (map (subst rs) ts) \<rightarrow> subst rs t"
|
|
221 |
| "t \<rightarrow> t' ==> Lam t \<rightarrow> Lam t'"
|
|
222 |
| "s \<rightarrow> s' ==> At s t \<rightarrow> At s' t"
|
|
223 |
| "t \<rightarrow> t' ==> At s t \<rightarrow> At s t'"
|
|
224 |
|
23503
|
225 |
abbreviation
|
|
226 |
treds :: "[tm, tm] => bool" (infixl "\<rightarrow>*" 50) where
|
|
227 |
"s \<rightarrow>* t == (s, t) \<in> tRed^*"
|
23778
|
228 |
|
|
229 |
inductive_set
|
|
230 |
tRed_list :: "(tm list * tm list) set"
|
|
231 |
and treds_list :: "[tm list, tm list] \<Rightarrow> bool" (infixl "\<rightarrow>*" 50)
|
|
232 |
where
|
23503
|
233 |
"ss \<rightarrow>* ts == (ss, ts) \<in> tRed_list"
|
23778
|
234 |
| "[] \<rightarrow>* []"
|
|
235 |
| "ts \<rightarrow>* ts' ==> t \<rightarrow>* t' ==> t#ts \<rightarrow>* t'#ts'"
|
23503
|
236 |
|
|
237 |
declare tRed_list.intros[simp]
|
|
238 |
|
|
239 |
lemma tRed_list_refl[simp]: includes Vars shows "ts \<rightarrow>* ts"
|
|
240 |
by(induct ts) auto
|
|
241 |
|
|
242 |
|
|
243 |
fun ML_closed :: "nat \<Rightarrow> ml \<Rightarrow> bool"
|
|
244 |
and ML_closed_t :: "nat \<Rightarrow> tm \<Rightarrow> bool" where
|
|
245 |
"ML_closed i (C nm vs) = (ALL v:set vs. ML_closed i v)" |
|
|
246 |
"ML_closed i (V nm vs) = (ALL v:set vs. ML_closed i v)" |
|
|
247 |
"ML_closed i (Fun f vs n) = (ML_closed i f & (ALL v:set vs. ML_closed i v))" |
|
|
248 |
"ML_closed i (A_ML v vs) = (ML_closed i v & (ALL v:set vs. ML_closed i v))" |
|
|
249 |
"ML_closed i (apply v w) = (ML_closed i v & ML_closed i w)" |
|
|
250 |
"ML_closed i (CC nm) = True" |
|
|
251 |
"ML_closed i (V_ML X) = (X<i)" |
|
|
252 |
"ML_closed i (Lam_ML v) = ML_closed (i+1) v" |
|
|
253 |
"ML_closed_t i (term_of v) = ML_closed i v" |
|
|
254 |
"ML_closed_t i (At r s) = (ML_closed_t i r & ML_closed_t i s)" |
|
|
255 |
"ML_closed_t i (Lam t) = (ML_closed_t i t)" |
|
|
256 |
"ML_closed_t i v = True"
|
|
257 |
thm ML_closed.simps ML_closed_t.simps
|
|
258 |
|
23778
|
259 |
inductive_set
|
|
260 |
Red :: "(ml * ml)set"
|
|
261 |
and Redt :: "(tm * tm)set"
|
|
262 |
and Redl :: "(ml list * ml list)set"
|
|
263 |
and red :: "[ml, ml] => bool" (infixl "\<Rightarrow>" 50)
|
|
264 |
and redl :: "[ml list, ml list] => bool" (infixl "\<Rightarrow>" 50)
|
|
265 |
and redt :: "[tm, tm] => bool" (infixl "\<Rightarrow>" 50)
|
|
266 |
and reds :: "[ml, ml] => bool" (infixl "\<Rightarrow>*" 50)
|
|
267 |
and redts :: "[tm, tm] => bool" (infixl "\<Rightarrow>*" 50)
|
|
268 |
where
|
|
269 |
"s \<Rightarrow> t == (s, t) \<in> Red"
|
|
270 |
| "s \<Rightarrow> t == (s, t) \<in> Redl"
|
|
271 |
| "s \<Rightarrow> t == (s, t) \<in> Redt"
|
|
272 |
| "s \<Rightarrow>* t == (s, t) \<in> Red^*"
|
|
273 |
| "s \<Rightarrow>* t == (s, t) \<in> Redt^*"
|
23503
|
274 |
(* ML *)
|
23778
|
275 |
| "A_ML (Lam_ML u) [v] \<Rightarrow> u[v/0]"
|
23503
|
276 |
(* compiled rules *)
|
23778
|
277 |
| "(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"
|
23503
|
278 |
(* apply *)
|
23778
|
279 |
| apply_Fun1: "apply (Fun f vs (Suc 0)) v \<Rightarrow> A_ML f (vs @ [v])"
|
|
280 |
| apply_Fun2: "n > 0 ==>
|
23503
|
281 |
apply (Fun f vs (Suc n)) v \<Rightarrow> Fun f (vs @ [v]) n"
|
23778
|
282 |
| apply_C: "apply (C nm vs) v \<Rightarrow> C nm (vs @ [v])"
|
|
283 |
| apply_V: "apply (V x vs) v \<Rightarrow> V x (vs @ [v])"
|
23503
|
284 |
(* term_of *)
|
23778
|
285 |
| term_of_C: "term_of (C nm vs) \<Rightarrow> foldl At (Ct nm) (map term_of vs)"
|
|
286 |
| term_of_V: "term_of (V x vs) \<Rightarrow> foldl At (Vt x) (map term_of vs)"
|
|
287 |
| term_of_Fun: "term_of(Fun vf vs n) \<Rightarrow>
|
23503
|
288 |
Lam (term_of ((apply (lift 0 (Fun vf vs n)) (V_ML 0))[V 0 []/0]))"
|
|
289 |
(* Context *)
|
23778
|
290 |
| ctxt_Lam: "t \<Rightarrow> t' ==> Lam t \<Rightarrow> Lam t'"
|
|
291 |
| ctxt_At1: "s \<Rightarrow> s' ==> At s t \<Rightarrow> At s' t"
|
|
292 |
| ctxt_At2: "t \<Rightarrow> t' ==> At s t \<Rightarrow> At s t'"
|
|
293 |
| ctxt_term_of: "v \<Rightarrow> v' ==> term_of v \<Rightarrow> term_of v'"
|
|
294 |
| ctxt_C: "vs \<Rightarrow> vs' ==> C nm vs \<Rightarrow> C nm vs'"
|
|
295 |
| ctxt_V: "vs \<Rightarrow> vs' ==> V x vs \<Rightarrow> V x vs'"
|
|
296 |
| ctxt_Fun1: "f \<Rightarrow> f' ==> Fun f vs n \<Rightarrow> Fun f' vs n"
|
|
297 |
| ctxt_Fun3: "vs \<Rightarrow> vs' ==> Fun f vs n \<Rightarrow> Fun f vs' n"
|
|
298 |
| ctxt_apply1: "s \<Rightarrow> s' ==> apply s t \<Rightarrow> apply s' t"
|
|
299 |
| ctxt_apply2: "t \<Rightarrow> t' ==> apply s t \<Rightarrow> apply s t'"
|
|
300 |
| ctxt_A_ML1: "f \<Rightarrow> f' ==> A_ML f vs \<Rightarrow> A_ML f' vs"
|
|
301 |
| ctxt_A_ML2: "vs \<Rightarrow> vs' ==> A_ML f vs \<Rightarrow> A_ML f vs'"
|
|
302 |
| ctxt_list1: "v \<Rightarrow> v' ==> v#vs \<Rightarrow> v'#vs"
|
|
303 |
| ctxt_list2: "vs \<Rightarrow> vs' ==> v#vs \<Rightarrow> v#vs'"
|
23503
|
304 |
|
|
305 |
|
|
306 |
consts
|
|
307 |
ar :: "const_name \<Rightarrow> nat"
|
|
308 |
|
|
309 |
axioms
|
|
310 |
ar_pos: "ar nm > 0"
|
|
311 |
|
|
312 |
types env = "ml list"
|
|
313 |
|
|
314 |
consts eval :: "tm \<Rightarrow> env \<Rightarrow> ml"
|
|
315 |
primrec
|
|
316 |
"eval (Vt x) e = e!x"
|
|
317 |
"eval (Ct nm) e = Fun (CC nm) [] (ar nm)"
|
|
318 |
"eval (At s t) e = apply (eval s e) (eval t e)"
|
|
319 |
"eval (Lam t) e = Fun (Lam_ML (eval t ((V_ML 0) # map (lift\<^bsub>ML\<^esub> 0) e))) [] 1"
|
|
320 |
|
|
321 |
fun size' :: "ml \<Rightarrow> nat" where
|
|
322 |
"size' (C nm vs) = (\<Sum>v\<leftarrow>vs. size' v)+1" |
|
|
323 |
"size' (V nm vs) = (\<Sum>v\<leftarrow>vs. size' v)+1" |
|
|
324 |
"size' (Fun f vs n) = (size' f + (\<Sum>v\<leftarrow>vs. size' v))+1" |
|
|
325 |
"size' (A_ML v vs) = (size' v + (\<Sum>v\<leftarrow>vs. size' v))+1" |
|
|
326 |
"size' (apply v w) = (size' v + size' w)+1" |
|
|
327 |
"size' (CC nm) = 1" |
|
|
328 |
"size' (V_ML X) = 1" |
|
|
329 |
"size' (Lam_ML v) = size' v + 1"
|
|
330 |
|
|
331 |
lemma listsum_size'[simp]:
|
|
332 |
"v \<in> set vs \<Longrightarrow> size' v < Suc(listsum (map size' vs))"
|
25873
|
333 |
by(induct vs)(auto)
|
23503
|
334 |
|
|
335 |
corollary cor_listsum_size'[simp]:
|
|
336 |
"v \<in> set vs \<Longrightarrow> size' v < Suc(m + listsum (map size' vs))"
|
|
337 |
using listsum_size'[of v vs] by arith
|
|
338 |
|
25873
|
339 |
lemma size'_lift_ML: "size' (lift\<^bsub>ML\<^esub> k v) = size' v"
|
|
340 |
apply(induct v arbitrary:k rule:size'.induct)
|
|
341 |
apply(simp add:map_compose[symmetric])
|
|
342 |
apply(rule arg_cong[where f = listsum])
|
|
343 |
apply(rule map_ext)
|
|
344 |
apply simp
|
|
345 |
apply(simp add:map_compose[symmetric])
|
|
346 |
apply(rule arg_cong[where f = listsum])
|
|
347 |
apply(rule map_ext)
|
|
348 |
apply simp
|
|
349 |
apply(simp add:map_compose[symmetric])
|
|
350 |
apply(rule arg_cong[where f = listsum])
|
|
351 |
apply(rule map_ext)
|
|
352 |
apply simp
|
|
353 |
apply(simp add:map_compose[symmetric])
|
|
354 |
apply(rule arg_cong[where f = listsum])
|
|
355 |
apply(rule map_ext)
|
|
356 |
apply simp
|
|
357 |
apply(simp)
|
|
358 |
apply simp
|
|
359 |
apply simp
|
|
360 |
apply(simp)
|
|
361 |
done
|
|
362 |
|
|
363 |
(* FIXME needed? *)
|
25876
|
364 |
lemma size_subst_ml_ML[simp]: includes Vars shows
|
|
365 |
"!i. size(f i) = 0 \<Longrightarrow> size(subst\<^bsub>ML\<^esub> f v) = size(v)"
|
|
366 |
by (induct f v rule: subst_ml_ML.induct)
|
|
367 |
(simp_all add: cons_ML_def split: nat.split)
|
|
368 |
lemma size_subst_tm_ML[simp]: includes Vars shows
|
|
369 |
"!i. size(f i) = 0 \<Longrightarrow> size(subst\<^bsub>ML\<^esub> f t) = size(t)"
|
|
370 |
by (induct f t rule: subst_tm_ML.induct)(simp_all add: o_def)
|
23503
|
371 |
|
25873
|
372 |
(* FIXME name and use explicitly *)
|
23503
|
373 |
lemma [simp]:
|
25873
|
374 |
"\<forall>i j. size'(f i) = 1 \<Longrightarrow> size' (subst\<^bsub>ML\<^esub> f v) = size' v"
|
|
375 |
apply(induct v arbitrary:f rule:size'.induct)
|
|
376 |
apply(simp add:map_compose[symmetric])
|
|
377 |
apply(rule arg_cong[where f = listsum])
|
|
378 |
apply(rule map_ext)
|
|
379 |
apply simp
|
|
380 |
apply(simp add:map_compose[symmetric])
|
|
381 |
apply(rule arg_cong[where f = listsum])
|
|
382 |
apply(rule map_ext)
|
|
383 |
apply simp
|
|
384 |
apply(simp add:map_compose[symmetric])
|
|
385 |
apply(rule arg_cong[where f = listsum])
|
|
386 |
apply(rule map_ext)
|
|
387 |
apply simp
|
|
388 |
apply(simp add:map_compose[symmetric])
|
|
389 |
apply(rule arg_cong[where f = listsum])
|
|
390 |
apply(rule map_ext)
|
|
391 |
apply simp
|
|
392 |
apply(simp)
|
|
393 |
apply(simp)
|
|
394 |
apply(simp)
|
|
395 |
apply(simp)
|
|
396 |
apply(erule meta_allE)
|
|
397 |
apply(erule meta_mp)
|
|
398 |
apply(simp add:cons_ML_def size'_lift_ML split:nat.split)
|
|
399 |
done
|
23503
|
400 |
|
|
401 |
lemma [simp]: "size' (lift i v) = size' v"
|
25873
|
402 |
apply(induct v arbitrary:i rule:size'.induct)
|
|
403 |
apply(simp add:map_compose[symmetric])
|
|
404 |
apply(rule arg_cong[where f = listsum])
|
|
405 |
apply(rule map_ext)
|
|
406 |
apply simp
|
|
407 |
apply(simp add:map_compose[symmetric])
|
|
408 |
apply(rule arg_cong[where f = listsum])
|
|
409 |
apply(rule map_ext)
|
|
410 |
apply simp
|
|
411 |
apply(simp add:map_compose[symmetric])
|
|
412 |
apply(rule arg_cong[where f = listsum])
|
|
413 |
apply(rule map_ext)
|
|
414 |
apply simp
|
|
415 |
apply(simp add:map_compose[symmetric])
|
|
416 |
apply(rule arg_cong[where f = listsum])
|
|
417 |
apply(rule map_ext)
|
|
418 |
apply simp
|
|
419 |
apply simp
|
|
420 |
apply simp
|
|
421 |
apply simp
|
|
422 |
apply simp
|
|
423 |
done
|
23503
|
424 |
|
|
425 |
(* the kernel function as in Section 4.1 of "Operational aspects\<dots>" *)
|
|
426 |
|
|
427 |
function kernel :: "ml \<Rightarrow> tm" ("_!" 300) where
|
|
428 |
"(C nm vs)! = foldl At (Ct nm) (map kernel vs)" |
|
|
429 |
"(Lam_ML v)! = Lam (((lift 0 v)[V 0 []/0])!)" |
|
|
430 |
"(Fun f vs n)! = foldl At (f!) (map kernel vs)" |
|
|
431 |
"(A_ML v vs)! = foldl At (v!) (map kernel vs)" |
|
|
432 |
"(apply v w)! = At (v!) (w!)" |
|
|
433 |
"(CC nm)! = Ct nm" |
|
|
434 |
"(V x vs)! = foldl At (Vt x) (map kernel vs)" |
|
|
435 |
"(V_ML X)! = undefined"
|
|
436 |
by pat_completeness auto
|
|
437 |
termination by(relation "measure size'") auto
|
|
438 |
|
|
439 |
consts kernelt :: "tm \<Rightarrow> tm" ("_!" 300)
|
|
440 |
primrec
|
|
441 |
"(Ct nm)! = Ct nm"
|
|
442 |
"(term_of v)! = v!"
|
|
443 |
"(Vt x)! = Vt x"
|
|
444 |
"(At s t)! = At (s!) (t!)"
|
|
445 |
"(Lam t)! = Lam (t!)"
|
|
446 |
|
|
447 |
abbreviation
|
|
448 |
kernels :: "ml list \<Rightarrow> tm list" ("_!" 300) where
|
|
449 |
"vs ! == map kernel vs"
|
|
450 |
|
|
451 |
(* soundness of the code generator *)
|
|
452 |
axioms
|
|
453 |
compiler_correct:
|
|
454 |
"(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"
|
|
455 |
|
|
456 |
|
|
457 |
consts
|
|
458 |
free_vars :: "tm \<Rightarrow> lam_var_name set"
|
|
459 |
primrec
|
|
460 |
"free_vars (Ct nm) = {}"
|
|
461 |
"free_vars (Vt x) = {x}"
|
|
462 |
"free_vars (Lam t) = {i. EX j : free_vars t. j = i+1}"
|
|
463 |
"free_vars (At s t) = free_vars s \<union> free_vars t"
|
|
464 |
|
|
465 |
lemma [simp]: "t : Pure_tms \<Longrightarrow> lift\<^bsub>ML\<^esub> k t = t"
|
|
466 |
by (erule Pure_tms.induct) simp_all
|
|
467 |
|
|
468 |
lemma kernel_pure: includes Vars assumes "t : Pure_tms" shows "t! = t"
|
|
469 |
using assms by (induct) simp_all
|
|
470 |
|
|
471 |
lemma lift_eval:
|
|
472 |
"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)"
|
|
473 |
apply(induct set:Pure_tms)
|
|
474 |
apply simp_all
|
|
475 |
apply clarsimp
|
|
476 |
apply(erule_tac x = "V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in allE)
|
|
477 |
apply simp
|
|
478 |
apply(erule impE)
|
|
479 |
apply clarsimp
|
|
480 |
apply(case_tac i)apply simp
|
|
481 |
apply simp
|
|
482 |
apply (simp add: map_compose[symmetric])
|
25876
|
483 |
apply (simp add: o_def lift_lift_ml_ML_comm)
|
23503
|
484 |
done
|
|
485 |
|
|
486 |
lemma lift_ML_eval[rule_format]:
|
|
487 |
"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)"
|
|
488 |
apply(induct set:Pure_tms)
|
|
489 |
apply simp_all
|
|
490 |
apply clarsimp
|
|
491 |
apply(erule_tac x = "V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in allE)
|
|
492 |
apply simp
|
|
493 |
apply(erule impE)
|
|
494 |
apply clarsimp
|
|
495 |
apply(case_tac i)apply simp
|
|
496 |
apply simp
|
|
497 |
apply (simp add: map_compose[symmetric])
|
25876
|
498 |
apply (simp add:o_def lift_lift_ml_ML)
|
23503
|
499 |
done
|
|
500 |
|
|
501 |
lemma [simp]: includes Vars shows "(v ## f) 0 = v"
|
|
502 |
by(simp add:cons_ML_def)
|
|
503 |
|
|
504 |
lemma [simp]: includes Vars shows "(v ## f) (Suc n) = lift\<^bsub>ML\<^esub> 0 (f n)"
|
|
505 |
by(simp add:cons_ML_def)
|
|
506 |
|
|
507 |
lemma lift_o_shift: "lift k o (V_ML 0 ## f) = (V_ML 0 ## (lift k \<circ> f))"
|
|
508 |
apply(rule ext)
|
25876
|
509 |
apply (simp add:cons_ML_def lift_lift_ml_ML_comm split:nat.split)
|
23503
|
510 |
done
|
|
511 |
|
25876
|
512 |
lemma lift_subst_ML_ml:
|
|
513 |
"lift_ml k (subst\<^bsub>ML\<^esub> f v) = subst\<^bsub>ML\<^esub> (lift_ml k o f) (lift_ml k v)"
|
|
514 |
by (induct k v arbitrary: f rule: lift_ml.induct)
|
|
515 |
(simp_all add:map_compose[symmetric] o_assoc lift_o_lift lift_o_shift)
|
|
516 |
lemma lift_subst_ML_tm: shows
|
|
517 |
"lift_tm k (subst\<^bsub>ML\<^esub> f t) = subst\<^bsub>ML\<^esub> (lift_ml k o f) (lift_tm k t)"
|
|
518 |
by(induct k t arbitrary: f rule: lift_tm.induct)
|
|
519 |
(simp_all add: o_assoc lift_o_lift lift_subst_ML_ml)
|
23503
|
520 |
|
25876
|
521 |
corollary lift_subst_ML1:
|
|
522 |
"\<forall>v k. lift_ml 0 (u[v/k]) = (lift_ml 0 u)[lift 0 v/k]"
|
|
523 |
apply(induct u rule:ml_induct)
|
|
524 |
apply(simp_all add:lift_lift_ml map_compose[symmetric] lift_subst_ML_ml)
|
|
525 |
apply(subst lift_lift_ml_ML_comm)apply simp
|
|
526 |
done
|
|
527 |
(*
|
|
528 |
lemma lift_ML_lift_ML_ml: includes Vars shows
|
|
529 |
"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)"
|
|
530 |
by (induct k v arbitrary: i rule: lift_ml_ML.induct)
|
|
531 |
(simp_all add:map_compose[symmetric])
|
|
532 |
lemma lift_ML_lift_ML_tm: includes Vars shows
|
23503
|
533 |
"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)"
|
25876
|
534 |
by(induct k t arbitrary: i rule: lift_tm_ML.induct)
|
|
535 |
(simp_all add:lift_ML_lift_ML_ml)
|
|
536 |
*)
|
|
537 |
(*FIXME move up *)
|
23503
|
538 |
corollary lift_ML_o_lift_ML: shows
|
|
539 |
"i < k+1 \<Longrightarrow> lift_tm_ML (Suc k) o (lift_tm_ML i) = lift_tm_ML i o lift_tm_ML k" and
|
|
540 |
"i < k+1 \<Longrightarrow> lift_ml_ML (Suc k) o (lift_ml_ML i) = lift_ml_ML i o lift_ml_ML k"
|
25876
|
541 |
apply(rule ext, simp add: lift_lift_tm_ML)
|
|
542 |
apply(rule ext, simp add: lift_lift_ml_ML)
|
|
543 |
done
|
23503
|
544 |
|
|
545 |
abbreviation insrt where
|
25876
|
546 |
"insrt k f ==
|
|
547 |
(%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)))"
|
23503
|
548 |
|
25876
|
549 |
lemma subst_insrt_lift_ml: includes Vars shows
|
23503
|
550 |
"subst\<^bsub>ML\<^esub> (insrt k f) (lift\<^bsub>ML\<^esub> k v) = lift\<^bsub>ML\<^esub> k (subst\<^bsub>ML\<^esub> f v)"
|
25876
|
551 |
apply (induct k v arbitrary: f k rule: lift_ml_ML.induct)
|
23503
|
552 |
apply (simp_all add:map_compose[symmetric] o_assoc lift_o_lift lift_o_shift)
|
25876
|
553 |
apply(subgoal_tac "V_ML 0 ## insrt k f = insrt (Suc k) (V_ML 0 ## f)")
|
|
554 |
apply simp
|
|
555 |
apply (simp add:expand_fun_eq lift_lift_ml_ML cons_ML_def split:nat.split)
|
|
556 |
done
|
|
557 |
lemma subst_insrt_lift_tm: includes Vars shows
|
|
558 |
"subst\<^bsub>ML\<^esub> (insrt k f) (lift\<^bsub>ML\<^esub> k t) = lift\<^bsub>ML\<^esub> k (subst\<^bsub>ML\<^esub> f t)"
|
|
559 |
apply (induct k t arbitrary: f k rule: lift_tm_ML.induct)
|
|
560 |
apply (simp_all)
|
23503
|
561 |
apply(subgoal_tac "lift 0 \<circ> insrt k f = insrt k (lift 0 \<circ> f)")
|
|
562 |
apply simp
|
|
563 |
apply(rule ext)
|
25876
|
564 |
apply (simp add:lift_lift_ml_ML_comm)
|
23503
|
565 |
apply(subgoal_tac "V_ML 0 ## insrt k f = insrt (Suc k) (V_ML 0 ## f)")
|
25876
|
566 |
apply (simp add:subst_insrt_lift_ml)
|
|
567 |
apply (simp add:expand_fun_eq lift_lift_ml_ML cons_ML_def split:nat.split)
|
23503
|
568 |
done
|
|
569 |
|
|
570 |
corollary subst_cons_lift: includes Vars shows
|
|
571 |
"subst\<^bsub>ML\<^esub> (V_ML 0 ## f) o (lift_ml_ML 0) = lift_ml_ML 0 o (subst_ml_ML f)"
|
|
572 |
apply(rule ext)
|
25876
|
573 |
apply(simp add: cons_ML_def subst_insrt_lift_ml[symmetric])
|
23503
|
574 |
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)))")
|
|
575 |
apply simp
|
|
576 |
apply(rule ext, simp split:nat.split)
|
|
577 |
done
|
|
578 |
|
|
579 |
lemma subst_eval[rule_format]: "t : Pure_tms \<Longrightarrow>
|
|
580 |
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)"
|
|
581 |
apply(induct set:Pure_tms)
|
|
582 |
apply simp_all
|
|
583 |
apply clarsimp
|
|
584 |
apply(erule_tac x="V_ML 0 ## f" in allE)
|
|
585 |
apply(erule_tac x= "(V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e)" in allE)
|
|
586 |
apply(erule impE)
|
|
587 |
apply clarsimp
|
|
588 |
apply(case_tac i)apply simp
|
|
589 |
apply simp
|
|
590 |
apply (simp add:subst_cons_lift map_compose[symmetric])
|
|
591 |
done
|
|
592 |
|
|
593 |
|
|
594 |
theorem kernel_eval[rule_format]: includes Vars shows
|
|
595 |
"t : Pure_tms ==>
|
|
596 |
ALL e. (ALL i : free_vars t. i < size e) \<longrightarrow> (ALL i < size e. e!i = V i []) --> (eval t e)! = t!"
|
|
597 |
apply(induct set:Pure_tms)
|
|
598 |
apply simp_all
|
|
599 |
apply clarsimp
|
|
600 |
apply(subst lift_eval) apply simp
|
|
601 |
apply clarsimp
|
|
602 |
apply(case_tac i)apply simp
|
|
603 |
apply simp
|
|
604 |
apply(subst subst_eval) apply simp
|
|
605 |
apply clarsimp
|
|
606 |
apply(case_tac i)apply simp
|
|
607 |
apply simp
|
|
608 |
apply(erule_tac x="map (subst\<^bsub>ML\<^esub> (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)))
|
|
609 |
(map (lift 0) (V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e))" in allE)
|
|
610 |
apply(erule impE)
|
|
611 |
apply(clarsimp)
|
|
612 |
apply(case_tac i)apply simp
|
|
613 |
apply simp
|
|
614 |
apply(erule impE)
|
|
615 |
apply(clarsimp)
|
|
616 |
apply(case_tac i)apply simp
|
|
617 |
apply simp
|
|
618 |
apply simp
|
|
619 |
done
|
|
620 |
|
25876
|
621 |
lemma ML_closed_lift_ML_ml[simp]:
|
|
622 |
includes Vars shows "ML_closed k v \<Longrightarrow> lift\<^bsub>ML\<^esub> k v = v"
|
|
623 |
by(induct k v rule: lift_ml_ML.induct)(simp_all add:list_eq_iff_nth_eq)
|
|
624 |
lemma ML_closed_lift_ML_tm[simp]:
|
25873
|
625 |
includes Vars shows "ML_closed_t k t \<Longrightarrow> lift\<^bsub>ML\<^esub> k t = t"
|
25876
|
626 |
by(induct k t rule: lift_tm_ML.induct)(simp_all)
|
23503
|
627 |
|
25876
|
628 |
lemma ML_closed_subst_ML_ml[simp]: includes Vars shows
|
|
629 |
"ML_closed k v \<Longrightarrow> !i<k. f i = V_ML i \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = v"
|
|
630 |
apply (induct f v arbitrary: k rule: subst_ml_ML.induct)
|
|
631 |
apply (auto simp add: list_eq_iff_nth_eq)
|
25873
|
632 |
apply(simp add:Ball_def)
|
|
633 |
apply(erule_tac x="vs!i" in meta_allE)
|
|
634 |
apply(erule_tac x="k" in meta_allE)
|
|
635 |
apply simp
|
|
636 |
apply(erule_tac x="vs!i" in meta_allE)
|
|
637 |
apply(erule_tac x="k" in meta_allE)
|
|
638 |
apply simp
|
|
639 |
apply(erule_tac x="vs!i" in meta_allE)
|
|
640 |
apply(erule_tac x="k" in meta_allE)
|
|
641 |
apply(erule_tac x="k" in meta_allE)
|
|
642 |
apply simp
|
|
643 |
apply(erule_tac x="vs!i" in meta_allE)
|
|
644 |
apply(erule_tac x="k" in meta_allE)
|
|
645 |
apply(erule_tac x="k" in meta_allE)
|
|
646 |
apply simp
|
|
647 |
apply(erule_tac x="Suc k" in meta_allE)
|
|
648 |
apply (simp add:cons_ML_def split:nat.split)
|
|
649 |
done
|
25876
|
650 |
lemma ML_closed_subst_ML_tm[simp]: includes Vars shows
|
|
651 |
"ML_closed_t k t \<Longrightarrow> !i<k. f i = V_ML i \<Longrightarrow> subst\<^bsub>ML\<^esub> f t = t"
|
|
652 |
by (induct f t arbitrary: k rule: subst_tm_ML.induct) (auto)
|
25873
|
653 |
|
25876
|
654 |
lemma ML_closed_lift_ml[simp]:
|
|
655 |
includes Vars shows "ML_closed k v \<Longrightarrow> ML_closed k (lift m v)"
|
|
656 |
by(induct k v arbitrary: m rule: lift_ml_ML.induct)
|
|
657 |
(simp_all add:list_eq_iff_nth_eq)
|
|
658 |
lemma ML_closed_lift_tm[simp]:
|
25873
|
659 |
includes Vars shows "ML_closed_t k t \<Longrightarrow> ML_closed_t k (lift m t)"
|
25876
|
660 |
by(induct k t arbitrary: m rule: lift_tm_ML.induct)(simp_all)
|
23503
|
661 |
|
|
662 |
lemma red_Lam[simp]: includes Vars shows "t \<rightarrow>* t' ==> Lam t \<rightarrow>* Lam t'"
|
|
663 |
apply(induct rule:rtrancl_induct)
|
|
664 |
apply(simp_all)
|
|
665 |
apply(blast intro: rtrancl_into_rtrancl tRed.intros)
|
|
666 |
done
|
|
667 |
|
|
668 |
lemma red_At1[simp]: includes Vars shows "t \<rightarrow>* t' ==> At t s \<rightarrow>* At t' s"
|
|
669 |
apply(induct rule:rtrancl_induct)
|
|
670 |
apply(simp_all)
|
|
671 |
apply(blast intro: rtrancl_into_rtrancl tRed.intros)
|
|
672 |
done
|
|
673 |
|
|
674 |
lemma red_At2[simp]: includes Vars shows "t \<rightarrow>* t' ==> At s t \<rightarrow>* At s t'"
|
|
675 |
apply(induct rule:rtrancl_induct)
|
|
676 |
apply(simp_all)
|
|
677 |
apply(blast intro:rtrancl_into_rtrancl tRed.intros)
|
|
678 |
done
|
|
679 |
|
|
680 |
lemma tRed_list_foldl_At:
|
|
681 |
"ts \<rightarrow>* ts' \<Longrightarrow> s \<rightarrow>* s' \<Longrightarrow> foldl At s ts \<rightarrow>* foldl At s' ts'"
|
|
682 |
apply(induct arbitrary:s s' rule:tRed_list.induct)
|
|
683 |
apply simp
|
|
684 |
apply simp
|
|
685 |
apply(blast dest: red_At1 red_At2 intro:rtrancl_trans)
|
|
686 |
done
|
|
687 |
|
|
688 |
lemma [trans]: "s = t \<Longrightarrow> t \<rightarrow> t' \<Longrightarrow> s \<rightarrow> t'"
|
|
689 |
by simp
|
|
690 |
|
|
691 |
|
|
692 |
lemma subst_foldl[simp]:
|
|
693 |
"subst f (foldl At s ts) = foldl At (subst f s) (map (subst f) ts)"
|
|
694 |
by (induct ts arbitrary: s) auto
|
|
695 |
|
|
696 |
|
|
697 |
lemma foldl_At_size: "size ts = size ts' \<Longrightarrow>
|
|
698 |
foldl At s ts = foldl At s' ts' \<longleftrightarrow> s = s' & ts = ts'"
|
|
699 |
by (induct arbitrary: s s' rule:list_induct2) simp_all
|
|
700 |
|
|
701 |
consts depth_At :: "tm \<Rightarrow> nat"
|
|
702 |
primrec
|
|
703 |
"depth_At(Ct cn) = 0"
|
|
704 |
"depth_At(Vt x) = 0"
|
|
705 |
"depth_At(Lam t) = 0"
|
|
706 |
"depth_At(At s t) = depth_At s + 1"
|
|
707 |
"depth_At(term_of v) = 0"
|
|
708 |
|
|
709 |
lemma depth_At_foldl:
|
|
710 |
"depth_At(foldl At s ts) = depth_At s + size ts"
|
|
711 |
by (induct ts arbitrary: s) simp_all
|
|
712 |
|
|
713 |
lemma foldl_At_eq_length:
|
|
714 |
"foldl At s ts = foldl At s ts' \<Longrightarrow> length ts = length ts'"
|
|
715 |
apply(subgoal_tac "depth_At(foldl At s ts) = depth_At(foldl At s ts')")
|
|
716 |
apply(erule thin_rl)
|
|
717 |
apply (simp add:depth_At_foldl)
|
|
718 |
apply simp
|
|
719 |
done
|
|
720 |
|
|
721 |
lemma foldl_At_eq[simp]: "foldl At s ts = foldl At s ts' \<longleftrightarrow> ts = ts'"
|
|
722 |
apply(rule)
|
|
723 |
prefer 2 apply simp
|
|
724 |
apply(blast dest:foldl_At_size foldl_At_eq_length)
|
|
725 |
done
|
|
726 |
|
|
727 |
lemma [simp]: "foldl At s ts ! = foldl At (s!) (map kernelt ts)"
|
|
728 |
by (induct ts arbitrary: s) simp_all
|
|
729 |
|
|
730 |
lemma [simp]: "(kernelt \<circ> term_of) = kernel"
|
|
731 |
by(rule ext) simp
|
|
732 |
|
|
733 |
lemma shift_subst_decr:
|
|
734 |
"Vt 0 ## subst_decr k t = subst_decr (Suc k) (lift 0 t)"
|
|
735 |
apply(rule ext)
|
|
736 |
apply (simp add:cons_def split:nat.split)
|
|
737 |
done
|
|
738 |
|
25873
|
739 |
lemma lift_foldl_At[simp]:
|
|
740 |
"lift k (foldl At s ts) = foldl At (lift k s) (map (lift k) ts)"
|
23503
|
741 |
by(induct ts arbitrary:s) simp_all
|
|
742 |
|
|
743 |
subsection "Horrible detour"
|
|
744 |
|
|
745 |
definition "liftn n == lift_ml 0 ^ n"
|
|
746 |
|
|
747 |
lemma [simp]: "liftn n (C i vs) = C i (map (liftn n) vs)"
|
|
748 |
apply(unfold liftn_def)
|
|
749 |
apply(induct n)
|
|
750 |
apply (simp_all add: map_compose[symmetric])
|
|
751 |
done
|
|
752 |
|
|
753 |
lemma [simp]: "liftn n (CC nm) = CC nm"
|
|
754 |
apply(unfold liftn_def)
|
|
755 |
apply(induct n)
|
|
756 |
apply (simp_all add: map_compose[symmetric])
|
|
757 |
done
|
|
758 |
|
|
759 |
lemma [simp]: "liftn n (apply v w) = apply (liftn n v) (liftn n w)"
|
|
760 |
apply(unfold liftn_def)
|
|
761 |
apply(induct n)
|
|
762 |
apply (simp_all add: map_compose[symmetric])
|
|
763 |
done
|
|
764 |
|
|
765 |
lemma [simp]: "liftn n (A_ML v vs) = A_ML (liftn n v) (map (liftn n) vs)"
|
|
766 |
apply(unfold liftn_def)
|
|
767 |
apply(induct n)
|
|
768 |
apply (simp_all add: map_compose[symmetric])
|
|
769 |
done
|
|
770 |
|
|
771 |
lemma [simp]:
|
|
772 |
"liftn n (Fun v vs i) = Fun (liftn n v) (map (liftn n) vs) i"
|
|
773 |
apply(unfold liftn_def)
|
|
774 |
apply(induct n)
|
|
775 |
apply (simp_all add: map_compose[symmetric] id_def)
|
|
776 |
done
|
|
777 |
|
|
778 |
lemma [simp]: "liftn n (Lam_ML v) = Lam_ML (liftn n v)"
|
|
779 |
apply(unfold liftn_def)
|
|
780 |
apply(induct n)
|
|
781 |
apply (simp_all add: map_compose[symmetric] id_def)
|
|
782 |
done
|
|
783 |
|
|
784 |
lemma liftn_liftn_add: "liftn m (liftn n v) = liftn (m+n) v"
|
|
785 |
by(simp add:liftn_def funpow_add)
|
|
786 |
|
|
787 |
lemma [simp]: "liftn n (V_ML k) = V_ML k"
|
|
788 |
apply(unfold liftn_def)
|
|
789 |
apply(induct n)
|
|
790 |
apply (simp_all)
|
|
791 |
done
|
|
792 |
|
|
793 |
lemma liftn_lift_ML_comm: "liftn n (lift\<^bsub>ML\<^esub> 0 v) = lift\<^bsub>ML\<^esub> 0 (liftn n v)"
|
|
794 |
apply(unfold liftn_def)
|
|
795 |
apply(induct n)
|
25876
|
796 |
apply (simp_all add:lift_lift_ml_ML_comm)
|
23503
|
797 |
done
|
|
798 |
|
|
799 |
lemma liftn_cons: "liftn n ((V_ML 0 ## f) x) = (V_ML 0 ## (liftn n o f)) x"
|
|
800 |
apply(simp add:cons_ML_def liftn_lift_ML_comm split:nat.split)
|
|
801 |
done
|
|
802 |
|
|
803 |
text{* End of horrible detour *}
|
|
804 |
|
|
805 |
lemma includes Vars shows foldl_Pure[simp]:
|
|
806 |
"t : Pure_tms \<Longrightarrow> \<forall>t\<in>set ts. t : Pure_tms \<Longrightarrow>
|
|
807 |
(!!s t. s : Pure_tms \<Longrightarrow> t : Pure_tms \<Longrightarrow> f s t : Pure_tms) \<Longrightarrow>
|
|
808 |
foldl f t ts \<in> Pure_tms"
|
|
809 |
by(induct ts arbitrary: t) simp_all
|
|
810 |
|
|
811 |
declare Pure_tms.intros[simp]
|
|
812 |
|
25876
|
813 |
lemma ML_closed_Suc: "ML_closed n v \<Longrightarrow> ML_closed (Suc n) (lift\<^bsub>ML\<^esub> k v)"
|
|
814 |
by (induct k v arbitrary: n rule: lift_ml_ML.induct) simp_all
|
25873
|
815 |
|
25876
|
816 |
lemma subst_ml_ML_coincidence:
|
|
817 |
"ML_closed k v \<Longrightarrow> !i<k. f i = g i \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = subst\<^bsub>ML\<^esub> g v"
|
|
818 |
by (induct f v arbitrary: k g rule: subst_ml_ML.induct)
|
|
819 |
(auto simp:cons_ML_def split:nat.split)
|
|
820 |
lemma subst_tm_ML_coincidence:
|
25873
|
821 |
"ML_closed_t k t \<Longrightarrow> !i<k. f i = g i \<Longrightarrow> subst\<^bsub>ML\<^esub> f t = subst\<^bsub>ML\<^esub> g t"
|
25876
|
822 |
by (induct f t arbitrary: k g rule: subst_tm_ML.induct)
|
|
823 |
(auto simp:subst_ml_ML_coincidence)
|
25873
|
824 |
|
25876
|
825 |
lemma ML_closed_subst_ML1_ml:
|
|
826 |
"!i. ML_closed k (f i) \<Longrightarrow> ML_closed k (subst\<^bsub>ML\<^esub> f v)"
|
|
827 |
by(induct f v arbitrary: k rule: subst_ml_ML.induct)
|
|
828 |
(auto simp:cons_ML_def ML_closed_Suc split:nat.split)
|
|
829 |
lemma ML_closed_subst_ML1_tm:
|
25873
|
830 |
"!i. ML_closed k (f i) \<Longrightarrow> ML_closed_t k (subst\<^bsub>ML\<^esub> f t)"
|
25876
|
831 |
by(induct f t arbitrary: k rule: subst_tm_ML.induct)
|
|
832 |
(simp_all add:ML_closed_subst_ML1_ml)
|
25873
|
833 |
|
|
834 |
lemma ML_closed_t_foldl_At:
|
|
835 |
"ML_closed_t k (foldl At t ts) \<longleftrightarrow>
|
|
836 |
ML_closed_t k t & (ALL t:set ts. ML_closed_t k t)"
|
|
837 |
by(induct ts arbitrary: t) simp_all
|
|
838 |
|
|
839 |
lemma subst_Vt: "t : Pure_tms \<Longrightarrow> subst Vt t = t"
|
|
840 |
apply(induct set:Pure_tms)
|
23503
|
841 |
apply simp_all
|
25873
|
842 |
apply(subgoal_tac "Vt 0 ## Vt = Vt")
|
|
843 |
apply simp
|
|
844 |
apply(rule ext)
|
|
845 |
apply(simp add:cons_def split:nat.split)
|
|
846 |
done
|
|
847 |
|
|
848 |
lemma ML_closed_Pure_tms: "ML_closed 0 v \<Longrightarrow> v! : Pure_tms"
|
|
849 |
apply(induct v rule:kernel.induct)
|
|
850 |
apply auto
|
|
851 |
apply(rule Pure_tms.intros)
|
|
852 |
apply(erule meta_mp)
|
|
853 |
apply(subgoal_tac "ML_closed (Suc 0) (lift 0 v)")
|
|
854 |
apply(subgoal_tac "ML_closed 0 (subst\<^bsub>ML\<^esub> (\<lambda>n. V 0 []) (lift 0 v))")
|
25876
|
855 |
apply(drule subst_ml_ML_coincidence[of _ _ "\<lambda>n. V 0 []" "\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)"])back
|
25873
|
856 |
apply simp
|
|
857 |
apply metis
|
|
858 |
apply simp
|
25876
|
859 |
apply(rule ML_closed_subst_ML1_ml)
|
25873
|
860 |
apply simp+
|
|
861 |
done
|
|
862 |
|
|
863 |
corollary subst_Vt_kernel: "ML_closed 0 v \<Longrightarrow> subst Vt (v!) = v!"
|
|
864 |
by (metis ML_closed_Pure_tms subst_Vt)
|
|
865 |
|
25876
|
866 |
lemma ML_closed_subst_ML3_ml:
|
|
867 |
"ML_closed k v \<Longrightarrow> !i<k. ML_closed l (f i) \<Longrightarrow> ML_closed l (subst\<^bsub>ML\<^esub> f v)"
|
|
868 |
by(induct f v arbitrary: k l rule: subst_ml_ML.induct)
|
|
869 |
(auto simp:cons_ML_def ML_closed_Suc split:nat.split)
|
|
870 |
lemma ML_closed_subst_ML3_tm:
|
|
871 |
"ML_closed_t k t \<Longrightarrow> !i<k. ML_closed l (f i) \<Longrightarrow> ML_closed_t l (subst\<^bsub>ML\<^esub> f t)"
|
|
872 |
by(induct f t arbitrary: k l rule: subst_tm_ML.induct)
|
|
873 |
(auto simp:ML_closed_subst_ML3_ml)
|
25873
|
874 |
|
|
875 |
lemma kernel_lift_tm: "ML_closed 0 v \<Longrightarrow> (lift i v)! = lift i (v!)"
|
|
876 |
apply(induct v arbitrary: i rule: kernel.induct)
|
|
877 |
apply (simp_all add:list_eq_iff_nth_eq)
|
|
878 |
apply(erule_tac x="Suc i" in meta_allE)
|
|
879 |
apply(erule meta_impE)
|
|
880 |
defer
|
25876
|
881 |
apply (simp add:lift_subst_ML_ml)
|
25873
|
882 |
apply(subgoal_tac "lift (Suc i) \<circ> (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)) = (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1))")
|
25876
|
883 |
apply (simp add:lift_lift_ml)
|
25873
|
884 |
apply(rule ext)
|
|
885 |
apply(simp)
|
25876
|
886 |
apply(subst ML_closed_subst_ML3_ml[of "1"])
|
25873
|
887 |
apply(simp)
|
|
888 |
apply(simp)
|
|
889 |
apply(simp)
|
|
890 |
done
|
|
891 |
|
25876
|
892 |
lemma subst_ML_ml_comp: includes Vars shows
|
25873
|
893 |
"!i. h i = subst\<^bsub>ML\<^esub> f (g i) \<Longrightarrow> subst\<^bsub>ML\<^esub> f (subst\<^bsub>ML\<^esub> g v) = subst\<^bsub>ML\<^esub> h v"
|
25876
|
894 |
apply (induct h v arbitrary: f g rule: subst_ml_ML.induct)
|
|
895 |
apply (simp add: list_eq_iff_nth_eq)
|
25873
|
896 |
apply (simp add: list_eq_iff_nth_eq)
|
|
897 |
apply (simp add: list_eq_iff_nth_eq)
|
|
898 |
apply (simp add: list_eq_iff_nth_eq)
|
|
899 |
apply (simp)
|
|
900 |
apply (simp add: list_eq_iff_nth_eq)
|
|
901 |
apply (simp)
|
|
902 |
apply(erule meta_allE)+
|
|
903 |
apply(erule meta_mp)
|
|
904 |
apply(auto simp:cons_ML_def split:nat.split)
|
|
905 |
apply (metis cons_ML_def o_apply subst_cons_lift)
|
|
906 |
done
|
25876
|
907 |
lemma subst_ML_tm_comp: includes Vars shows
|
|
908 |
"!i. h i = subst\<^bsub>ML\<^esub> f (g i) \<Longrightarrow> subst\<^bsub>ML\<^esub> f (subst\<^bsub>ML\<^esub> g t) = subst\<^bsub>ML\<^esub> h t"
|
|
909 |
apply (induct h t arbitrary: f g rule: subst_tm_ML.induct)
|
|
910 |
apply (simp)
|
|
911 |
apply (simp)
|
|
912 |
apply (simp)
|
|
913 |
apply (metis lift_subst_ML_ml o_apply subst_ML_ml_comp subst_ml_ML.simps(5))
|
|
914 |
apply (simp)
|
|
915 |
apply simp
|
|
916 |
apply (metis subst_ML_ml_comp subst_ml_ML.simps(5))
|
|
917 |
done
|
25873
|
918 |
|
|
919 |
lemma if_cong0: "If x y z = If x y z"
|
|
920 |
by simp
|
|
921 |
|
|
922 |
corollary [simp]: "ML_closed 0 v \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = v"
|
25876
|
923 |
using ML_closed_subst_ML_ml[where k=0] by simp
|
25873
|
924 |
|
|
925 |
fun subst_ml :: "(nat \<Rightarrow> nat) \<Rightarrow> ml \<Rightarrow> ml" where
|
|
926 |
"subst_ml f (C nm vs) = C nm (map (subst_ml f) vs)" |
|
|
927 |
"subst_ml f (V x vs) = V (f x) (map (subst_ml f) vs)" |
|
|
928 |
"subst_ml f (Fun v vs n) = Fun (subst_ml f v) (map (subst_ml f) vs) n" |
|
|
929 |
"subst_ml f (apply u v) = apply (subst_ml f u) (subst_ml f v)" |
|
|
930 |
"subst_ml f (V_ML X) = V_ML X" |
|
|
931 |
"subst_ml f (A_ML v vs) = A_ML (subst_ml f v) (map (subst_ml f) vs)" |
|
|
932 |
"subst_ml f (Lam_ML v) = Lam_ML (subst_ml f v)" |
|
|
933 |
"subst_ml f (CC nm) = CC nm"
|
|
934 |
|
|
935 |
lemma lift_ML_subst_ml:
|
|
936 |
"lift\<^bsub>ML\<^esub> k (subst_ml f v) = subst_ml f (lift\<^bsub>ML\<^esub> k v)"
|
|
937 |
apply (induct f v arbitrary: k rule:subst_ml.induct)
|
|
938 |
apply (simp_all add:list_eq_iff_nth_eq)
|
|
939 |
done
|
|
940 |
|
|
941 |
lemma subst_ml_subst_ML: includes Vars shows
|
|
942 |
"subst_ml f (subst\<^bsub>ML\<^esub> g v) = subst\<^bsub>ML\<^esub> (subst_ml f o g) (subst_ml f v)"
|
25876
|
943 |
apply (induct g v arbitrary: f rule: subst_ml_ML.induct)
|
25873
|
944 |
apply(simp_all add:list_eq_iff_nth_eq)
|
|
945 |
apply(subgoal_tac "(subst_ml fa \<circ> V_ML 0 ## f) = V_ML 0 ## (subst_ml fa \<circ> f)")
|
|
946 |
apply simp
|
|
947 |
apply(rule ext)
|
|
948 |
apply(simp add:cons_ML_def lift_ML_subst_ml split:nat.split)
|
|
949 |
done
|
|
950 |
|
|
951 |
lemma lift_Pure_tms[simp]: "t : Pure_tms \<Longrightarrow> lift k t : Pure_tms"
|
|
952 |
by(induct arbitrary:k set:Pure_tms) simp_all
|
|
953 |
|
|
954 |
lemma lift_subst_aux:
|
|
955 |
"t : Pure_tms \<Longrightarrow> !i<k. g i = lift k (f i) \<Longrightarrow>
|
|
956 |
ALL i>= k. g(Suc i) = lift k (f i) \<Longrightarrow>
|
|
957 |
g k = Vt k \<Longrightarrow> lift k (subst f t) = subst g (lift k t)"
|
|
958 |
apply(induct arbitrary:f g k set:Pure_tms)
|
|
959 |
apply (simp_all add: split:nat.split)
|
|
960 |
apply(erule meta_allE)+
|
|
961 |
apply(erule meta_impE)
|
|
962 |
defer
|
|
963 |
apply(erule meta_impE)
|
|
964 |
defer
|
|
965 |
apply(erule meta_mp)
|
25876
|
966 |
apply (simp_all add: cons_def lift_lift_ml lift_lift_tm split:nat.split)
|
25873
|
967 |
done
|
|
968 |
|
|
969 |
corollary lift_subst:
|
|
970 |
"t : Pure_tms \<Longrightarrow> lift 0 (subst f t) = subst (Vt 0 ## f) (lift 0 t)"
|
25876
|
971 |
by (simp add: lift_subst_aux cons_def lift_lift_ml split:nat.split)
|
23503
|
972 |
|
25873
|
973 |
lemma subst_comp: includes Vars shows
|
|
974 |
"t : Pure_tms \<Longrightarrow> !i. g i : Pure_tms \<Longrightarrow>
|
|
975 |
h = (%i. subst f (g i)) \<Longrightarrow> subst f (subst g t) = subst h t"
|
|
976 |
apply(induct arbitrary:f g h set:Pure_tms)
|
|
977 |
apply simp
|
|
978 |
apply simp
|
|
979 |
defer
|
|
980 |
apply simp
|
|
981 |
apply (simp (no_asm))
|
|
982 |
apply(erule meta_allE)+
|
|
983 |
apply(erule meta_impE)
|
|
984 |
defer
|
|
985 |
apply(erule meta_mp)
|
|
986 |
prefer 2 apply (simp add:cons_def split:nat.split)
|
|
987 |
apply(rule ext)
|
|
988 |
apply(subst (1) cons_def)
|
|
989 |
apply(subst (2) cons_def)
|
|
990 |
apply(simp split:nat.split)
|
|
991 |
apply rule apply (simp add:cons_def)
|
|
992 |
apply(simp add:lift_subst)
|
|
993 |
done
|
|
994 |
|
|
995 |
lemma lift_is_subst_ml:"lift k v = subst_ml (%n. if n<k then n else n+1) v"
|
25876
|
996 |
by(induct k v rule:lift_ml.induct)(simp_all add:list_eq_iff_nth_eq)
|
25873
|
997 |
|
|
998 |
lemma subst_ml_comp:
|
|
999 |
"subst_ml f (subst_ml g v) = subst_ml (f o g) v"
|
25876
|
1000 |
by(induct g v rule:subst_ml.induct)(simp_all add:list_eq_iff_nth_eq)
|
25873
|
1001 |
|
|
1002 |
lemma subst_kernel:
|
|
1003 |
"ML_closed 0 v \<Longrightarrow> subst (%n. Vt (f n)) (v!) = (subst_ml f v)!"
|
|
1004 |
apply (induct v arbitrary: f rule:kernel.induct)
|
|
1005 |
apply (simp_all add:list_eq_iff_nth_eq)
|
|
1006 |
apply(erule_tac x="%n. case n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> Suc(f k)" in meta_allE)
|
|
1007 |
apply(erule_tac meta_impE)
|
25876
|
1008 |
apply(rule ML_closed_subst_ML3_ml[where k="Suc 0"])
|
|
1009 |
apply (metis ML_closed_lift_ml)
|
|
1010 |
apply simp
|
25873
|
1011 |
apply(subgoal_tac "(\<lambda>n. Vt (case n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> Suc (f k))) = (Vt 0 ## (\<lambda>n. Vt (f n)))")
|
|
1012 |
apply (simp add:subst_ml_subst_ML)
|
|
1013 |
defer
|
25876
|
1014 |
apply(simp add:expand_fun_eq cons_def split:nat.split)
|
25873
|
1015 |
apply(simp add:cons_def)
|
|
1016 |
defer
|
|
1017 |
apply(simp add:lift_is_subst_ml subst_ml_comp)
|
|
1018 |
apply(rule arg_cong[where f = kernel])
|
|
1019 |
apply(subgoal_tac "(nat_case 0 (\<lambda>k. Suc (f k)) \<circ> Suc) = Suc o f")
|
25876
|
1020 |
prefer 2 apply(simp add:expand_fun_eq split:nat.split)
|
25873
|
1021 |
apply(subgoal_tac "(subst_ml (nat_case 0 (\<lambda>k. Suc (f k))) \<circ>
|
|
1022 |
(\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)))
|
|
1023 |
= (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1))")
|
|
1024 |
apply simp
|
25876
|
1025 |
apply(simp add: expand_fun_eq split:nat.split)
|
25873
|
1026 |
done
|
23503
|
1027 |
|
25873
|
1028 |
lemma kernel_subst1:
|
|
1029 |
"ML_closed 0 v \<Longrightarrow> ML_closed (Suc 0) u \<Longrightarrow>
|
|
1030 |
kernel(u[v/0]) = (kernel((lift 0 u)[V 0 []/0]))[v!/0]"
|
|
1031 |
proof(induct u arbitrary:v rule:kernel.induct)
|
|
1032 |
case (2 w)
|
|
1033 |
show ?case (is "?L = ?R")
|
|
1034 |
proof -
|
|
1035 |
have "?L = Lam (lift 0 (w[lift\<^bsub>ML\<^esub> 0 v/Suc 0])[V 0 []/0]!)"
|
|
1036 |
by (simp cong:if_cong0)
|
|
1037 |
also have "\<dots> = Lam ((lift 0 w)[lift\<^bsub>ML\<^esub> 0 (lift 0 v)/Suc 0][V 0 []/0]!)"
|
25876
|
1038 |
by (metis kernel.simps(2) lift_lift_ml_ML_comm lift_subst_ML1)
|
25873
|
1039 |
also have "\<dots> = Lam (subst\<^bsub>ML\<^esub> (%n. if n=0 then V 0 [] else
|
|
1040 |
if n=Suc 0 then lift 0 v else V_ML (n - 2)) (lift 0 w) !)"
|
|
1041 |
apply simp
|
|
1042 |
apply(rule arg_cong[where f = kernel])
|
25876
|
1043 |
apply(rule subst_ML_ml_comp)
|
25873
|
1044 |
using 2
|
|
1045 |
apply auto
|
|
1046 |
done
|
|
1047 |
also have "\<dots> = Lam ((lift 0 w)[V 0 []/0][lift 0 v/0]!)"
|
|
1048 |
apply simp
|
|
1049 |
apply(rule arg_cong[where f = kernel])
|
25876
|
1050 |
apply(rule subst_ML_ml_comp[symmetric])
|
25873
|
1051 |
using 2
|
|
1052 |
apply auto
|
|
1053 |
done
|
|
1054 |
also have "\<dots> = Lam ((lift_ml 0 ((lift_ml 0 w)[V 0 []/0]))[V 0 []/0]![(lift 0 v)!/0])"
|
|
1055 |
apply(rule arg_cong[where f = Lam])
|
|
1056 |
apply(rule 2(1))
|
25876
|
1057 |
apply (metis ML_closed_lift_ml 2)
|
25873
|
1058 |
apply(subgoal_tac "ML_closed (Suc(Suc 0)) w")
|
|
1059 |
defer
|
|
1060 |
using 2
|
|
1061 |
apply force
|
|
1062 |
apply(subgoal_tac "ML_closed (Suc (Suc 0)) (lift 0 w)")
|
|
1063 |
defer
|
25876
|
1064 |
apply(erule ML_closed_lift_ml)
|
|
1065 |
apply(erule ML_closed_subst_ML3_ml)
|
25873
|
1066 |
apply simp
|
|
1067 |
done
|
|
1068 |
also have "\<dots> = Lam ((lift_ml 0 (lift_ml 0 w)[V 1 []/0])[V 0 []/0]![(lift 0 v)!/0])" (is "_ = ?M")
|
|
1069 |
apply(subgoal_tac "lift_ml 0 (lift_ml 0 w[V 0 []/0])[V 0 []/0] =
|
|
1070 |
lift_ml 0 (lift_ml 0 w)[V 1 []/0][V 0 []/0]")
|
|
1071 |
apply simp
|
25876
|
1072 |
apply(subst lift_subst_ML_ml)
|
25873
|
1073 |
apply(simp add:comp_def if_distrib[where f="lift_ml 0"] cong:if_cong)
|
|
1074 |
done
|
|
1075 |
finally have "?L = ?M" .
|
|
1076 |
have "?R = Lam (subst (Vt 0 ## subst_decr 0 (v!))
|
|
1077 |
(lift 0 (lift_ml 0 w[V 0 []/Suc 0])[V 0 []/0]!))"
|
|
1078 |
apply(subgoal_tac "(V_ML 0 ## (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - Suc 0))) = subst_decr_ML (Suc 0) (V 0 [])")
|
|
1079 |
apply(simp cong:if_cong)
|
|
1080 |
apply(simp add:expand_fun_eq cons_ML_def split:nat.splits)
|
|
1081 |
done
|
|
1082 |
also have "\<dots> = Lam (subst (Vt 0 ## subst_decr 0 (v!))
|
|
1083 |
((lift 0 (lift_ml 0 w))[V 1 []/Suc 0][V 0 []/0]!))"
|
|
1084 |
apply(subgoal_tac "lift 0 (lift 0 w[V 0 []/Suc 0]) = lift 0 (lift 0 w)[V 1 []/Suc 0]")
|
|
1085 |
apply simp
|
25876
|
1086 |
apply(subst lift_subst_ML_ml)
|
25873
|
1087 |
apply(simp add:comp_def if_distrib[where f="lift_ml 0"] cong:if_cong)
|
|
1088 |
done
|
|
1089 |
also have "(lift_ml 0 (lift_ml 0 w))[V 1 []/Suc 0][V 0 []/0] =
|
|
1090 |
(lift 0 (lift_ml 0 w))[V 0 []/0][V 1 []/ 0]" (is "?l = ?r")
|
|
1091 |
proof -
|
|
1092 |
have "?l = subst\<^bsub>ML\<^esub> (%n. if n= 0 then V 0 [] else if n = 1 then V 1 [] else
|
|
1093 |
V_ML (n - 2))
|
|
1094 |
(lift_ml 0 (lift_ml 0 w))"
|
25876
|
1095 |
by(auto intro!:subst_ML_ml_comp)
|
|
1096 |
also have "\<dots> = ?r" by(auto intro!:subst_ML_ml_comp[symmetric])
|
25873
|
1097 |
finally show ?thesis .
|
|
1098 |
qed
|
|
1099 |
also have "Lam (subst (Vt 0 ## subst_decr 0 (v!)) (?r !)) = ?M"
|
|
1100 |
proof-
|
|
1101 |
have "subst (subst_decr (Suc 0) (lift_tm 0 (kernel v))) (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]!) =
|
|
1102 |
subst (subst_decr 0 (kernel(lift_ml 0 v))) (lift_ml 0 (lift_ml 0 w)[V 1 []/0][V 0 []/0]!)" (is "?a = ?b")
|
|
1103 |
proof-
|
|
1104 |
def pi == "%n::nat. if n = 0 then 1 else if n = 1 then 0 else n"
|
|
1105 |
have "(\<lambda>i. Vt (pi i)[lift 0 (v!)/0]) = subst_decr (Suc 0) (lift 0 (v!))"
|
|
1106 |
by(rule ext)(simp add:pi_def)
|
|
1107 |
hence "?a =
|
|
1108 |
subst (subst_decr 0 (lift_tm 0 (kernel v))) (subst (% n. Vt (pi n)) (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]!))"
|
|
1109 |
apply(subst subst_comp[OF _ _ refl])
|
|
1110 |
prefer 3 apply simp
|
|
1111 |
using 2(3)
|
|
1112 |
apply simp
|
|
1113 |
apply(rule ML_closed_Pure_tms)
|
25876
|
1114 |
apply(rule ML_closed_subst_ML3_ml[where k="Suc 0"])
|
|
1115 |
apply(rule ML_closed_subst_ML3_ml[where k="Suc(Suc 0)"])
|
25873
|
1116 |
apply simp
|
|
1117 |
apply simp
|
|
1118 |
apply simp
|
|
1119 |
apply simp
|
|
1120 |
done
|
|
1121 |
also have "\<dots> =
|
|
1122 |
(subst_ml pi (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]))![lift_tm 0 (v!)/0]"
|
|
1123 |
apply(subst subst_kernel)
|
|
1124 |
using 2 apply auto
|
25876
|
1125 |
apply(rule ML_closed_subst_ML3_ml[where k="Suc 0"])
|
|
1126 |
apply(rule ML_closed_subst_ML3_ml[where k="Suc(Suc 0)"])
|
25873
|
1127 |
apply simp
|
|
1128 |
apply simp
|
|
1129 |
apply simp
|
|
1130 |
done
|
|
1131 |
also have "\<dots> = (subst_ml pi (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]))![lift 0 v!/0]"
|
|
1132 |
proof -
|
|
1133 |
have "lift 0 (v!) = lift 0 v!" by (metis 2(2) kernel_lift_tm)
|
|
1134 |
thus ?thesis by (simp cong:if_cong)
|
|
1135 |
qed
|
|
1136 |
also have "\<dots> = ?b"
|
|
1137 |
proof-
|
|
1138 |
have 1: "subst_ml pi (lift 0 (lift 0 w)) = lift 0 (lift 0 w)"
|
|
1139 |
apply(simp add:lift_is_subst_ml subst_ml_comp)
|
|
1140 |
apply(subgoal_tac "pi \<circ> (Suc \<circ> Suc) = (Suc \<circ> Suc)")
|
|
1141 |
apply(simp)
|
|
1142 |
apply(simp add:pi_def expand_fun_eq)
|
|
1143 |
done
|
|
1144 |
have "subst_ml pi (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]) =
|
|
1145 |
lift_ml 0 (lift_ml 0 w)[V 1 []/0][V 0 []/0]"
|
|
1146 |
apply(subst subst_ml_subst_ML)
|
|
1147 |
apply(subst subst_ml_subst_ML)
|
|
1148 |
apply(subst 1)
|
25876
|
1149 |
apply(subst subst_ML_ml_comp)
|
25873
|
1150 |
apply(rule)
|
|
1151 |
apply(rule)
|
25876
|
1152 |
apply(rule subst_ML_ml_comp[symmetric])
|
25873
|
1153 |
apply(auto simp:pi_def)
|
|
1154 |
done
|
|
1155 |
thus ?thesis by simp
|
|
1156 |
qed
|
|
1157 |
finally show ?thesis .
|
|
1158 |
qed
|
|
1159 |
thus ?thesis by(simp cong:if_cong0 add:shift_subst_decr)
|
|
1160 |
qed
|
|
1161 |
finally have "?R = ?M" .
|
|
1162 |
then show "?L = ?R" using `?L = ?M` by metis
|
|
1163 |
qed
|
|
1164 |
qed (simp_all add:list_eq_iff_nth_eq)
|
|
1165 |
|
|
1166 |
|
23503
|
1167 |
theorem Red_sound: includes Vars
|
|
1168 |
shows "v \<Rightarrow> v' \<Longrightarrow> ML_closed 0 v \<Longrightarrow> v! \<rightarrow>* v'! & ML_closed 0 v'"
|
|
1169 |
and "t \<Rightarrow> t' \<Longrightarrow> ML_closed_t 0 t \<Longrightarrow> kernelt t \<rightarrow>* kernelt t' & ML_closed_t 0 t'"
|
|
1170 |
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')"
|
|
1171 |
proof(induct rule:Red_Redt_Redl.inducts)
|
|
1172 |
fix u v
|
|
1173 |
let ?v = "A_ML (Lam_ML u) [v]"
|
|
1174 |
assume cl: "ML_closed 0 (A_ML (Lam_ML u) [v])"
|
|
1175 |
let ?u' = "(lift_ml 0 u)[V 0 []/0]"
|
|
1176 |
have "?v! = At (Lam ((?u')!)) (v !)" by simp
|
|
1177 |
also have "\<dots> \<rightarrow> (?u' !)[v!/0]" (is "_ \<rightarrow> ?R") by(rule tRed.intros)
|
|
1178 |
also have "?R = u[v/0]!" using cl
|
25873
|
1179 |
apply(cut_tac u = "u" and v = "v" in kernel_subst1)
|
|
1180 |
apply(simp_all)
|
|
1181 |
done
|
23503
|
1182 |
finally have "kernel(A_ML (Lam_ML u) [v]) \<rightarrow>* kernel(u[v/0])" (is ?A) by(rule r_into_rtrancl)
|
25873
|
1183 |
moreover have "ML_closed 0 (u[v/0])" (is "?C")
|
|
1184 |
proof -
|
|
1185 |
let ?f = "\<lambda>n. if n = 0 then v else V_ML (n - 1)"
|
|
1186 |
let ?g = "\<lambda>n. v"
|
|
1187 |
have clu: "ML_closed (Suc 0) u" and clv: "ML_closed 0 v" using cl by simp+
|
|
1188 |
have "ML_closed 0 (subst\<^bsub>ML\<^esub> ?g u)"
|
25876
|
1189 |
by (metis COMBK_def ML_closed_subst_ML1_ml clv)
|
25873
|
1190 |
hence "ML_closed 0 (subst\<^bsub>ML\<^esub> ?f u)"
|
25876
|
1191 |
using subst_ml_ML_coincidence[OF clu, of ?f ?g] by auto
|
25873
|
1192 |
thus ?thesis by simp
|
|
1193 |
qed
|
23503
|
1194 |
ultimately show "?A & ?C" ..
|
|
1195 |
next
|
25873
|
1196 |
case term_of_C thus ?case
|
|
1197 |
by (auto simp:ML_closed_t_foldl_At map_compose[symmetric])
|
23503
|
1198 |
next
|
|
1199 |
fix f :: "nat \<Rightarrow> ml" and nm vs v
|
|
1200 |
assume f: "\<forall>i. ML_closed 0 (f i)" and compR: "(nm, vs, v) \<in> compR"
|
25873
|
1201 |
have "map (subst Vt) (map (subst\<^bsub>ML\<^esub> f) vs!) = map (subst\<^bsub>ML\<^esub> f) vs!"
|
25876
|
1202 |
by(simp add:list_eq_iff_nth_eq subst_Vt_kernel ML_closed_subst_ML1_ml[OF f])
|
25873
|
1203 |
with tRed.intros(3)[OF compiler_correct[OF compR f], of Vt,simplified map_compose]
|
|
1204 |
have red: "foldl At (Ct nm) ((map (subst\<^bsub>ML\<^esub> f) vs) !) \<rightarrow>
|
|
1205 |
(subst\<^bsub>ML\<^esub> f v)!" (is "_ \<rightarrow> ?R")
|
25876
|
1206 |
by(simp add:subst_Vt_kernel ML_closed_subst_ML1_ml[OF f])
|
25873
|
1207 |
hence "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! \<rightarrow>* subst\<^bsub>ML\<^esub> f v!" (is ?A) by simp
|
|
1208 |
moreover
|
25876
|
1209 |
have "ML_closed 0 (subst\<^bsub>ML\<^esub> f v)" (is ?C) by(metis ML_closed_subst_ML1_ml f)
|
23503
|
1210 |
ultimately show "?A & ?C" ..
|
|
1211 |
next
|
25873
|
1212 |
case term_of_V thus ?case
|
|
1213 |
by (auto simp:map_compose[symmetric]ML_closed_t_foldl_At)
|
23503
|
1214 |
next
|
23778
|
1215 |
case (term_of_Fun vf vs n)
|
25873
|
1216 |
hence "foldl At (lift 0 vf!)
|
|
1217 |
(map (subst\<^bsub>ML\<^esub> (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)))
|
|
1218 |
(map (lift 0) vs)!)
|
|
1219 |
= lift 0 (foldl At (vf!) (map kernel vs))"
|
|
1220 |
by (simp add:kernel_lift_tm list_eq_iff_nth_eq)
|
23503
|
1221 |
hence "term_of (Fun vf vs n)! \<rightarrow>*
|
25873
|
1222 |
Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0]))!"
|
|
1223 |
using term_of_Fun
|
|
1224 |
apply (simp del:lift_foldl_At)
|
|
1225 |
apply (metis kernel.simps r_into_rtrancl tRed.intros(2))
|
|
1226 |
done
|
23503
|
1227 |
moreover
|
|
1228 |
have "ML_closed_t 0
|
25873
|
1229 |
(Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0])))"
|
|
1230 |
using term_of_Fun by simp
|
23503
|
1231 |
ultimately show ?case ..
|
|
1232 |
next
|
|
1233 |
case apply_Fun1 thus ?case by simp
|
|
1234 |
next
|
|
1235 |
case apply_Fun2 thus ?case by simp
|
|
1236 |
next
|
|
1237 |
case apply_C thus ?case by simp
|
|
1238 |
next
|
|
1239 |
case apply_V thus ?case by simp
|
|
1240 |
next
|
|
1241 |
case ctxt_Lam thus ?case by(auto)
|
|
1242 |
next
|
|
1243 |
case ctxt_At1 thus ?case by(auto)
|
|
1244 |
next
|
|
1245 |
case ctxt_At2 thus ?case by (auto)
|
|
1246 |
next
|
|
1247 |
case ctxt_term_of thus ?case by (auto)
|
|
1248 |
next
|
|
1249 |
case ctxt_C thus ?case by (fastsimp simp:tRed_list_foldl_At)
|
|
1250 |
next
|
|
1251 |
case ctxt_V thus ?case by (fastsimp simp:tRed_list_foldl_At)
|
|
1252 |
next
|
|
1253 |
case ctxt_Fun1 thus ?case by (fastsimp simp:tRed_list_foldl_At)
|
|
1254 |
next
|
|
1255 |
case ctxt_Fun3 thus ?case by (fastsimp simp:tRed_list_foldl_At)
|
|
1256 |
next
|
|
1257 |
case ctxt_apply1 thus ?case by auto
|
|
1258 |
next
|
|
1259 |
case ctxt_apply2 thus ?case by auto
|
|
1260 |
next
|
|
1261 |
case ctxt_A_ML1 thus ?case by (fastsimp simp:tRed_list_foldl_At)
|
|
1262 |
next
|
|
1263 |
case ctxt_A_ML2 thus ?case by (fastsimp simp:tRed_list_foldl_At)
|
|
1264 |
next
|
|
1265 |
case ctxt_list1 thus ?case by simp
|
|
1266 |
next
|
|
1267 |
case ctxt_list2 thus ?case by simp
|
|
1268 |
qed
|
|
1269 |
|
|
1270 |
|
|
1271 |
lemma [simp]: "Ct n = foldl At t ts \<longleftrightarrow> t = Ct n & ts = []"
|
|
1272 |
by (induct ts arbitrary:t) auto
|
|
1273 |
|
|
1274 |
corollary kernel_inv: includes Vars shows
|
25873
|
1275 |
"(t :: tm) \<Rightarrow>* t' ==> ML_closed_t 0 t ==> t! \<rightarrow>* t'! \<and> ML_closed_t 0 t' "
|
|
1276 |
apply(induct rule: rtrancl.induct)
|
|
1277 |
apply (metis rtrancl_eq_or_trancl)
|
|
1278 |
apply (metis Red_sound rtrancl_trans)
|
|
1279 |
done
|
|
1280 |
|
|
1281 |
lemma ML_closed_t_term_of_eval:
|
|
1282 |
"t : Pure_tms \<Longrightarrow> ALL i : free_vars t. i < size e \<Longrightarrow>
|
|
1283 |
!i<length e. ML_closed n (e!i) \<Longrightarrow> ML_closed_t n (term_of (eval t e))"
|
|
1284 |
apply(induct arbitrary:n e rule: Pure_tms.induct)
|
|
1285 |
apply simp
|
|
1286 |
apply simp
|
|
1287 |
apply simp
|
|
1288 |
prefer 2 apply simp
|
|
1289 |
apply(erule_tac x="Suc n" in meta_allE)
|
|
1290 |
apply(erule_tac x="V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in meta_allE)
|
|
1291 |
apply(subgoal_tac "\<forall>i\<in>free_vars t. i < length (V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e)")
|
|
1292 |
prefer 2
|
|
1293 |
apply simp
|
|
1294 |
apply (metis Nat.less_trans gr0_implies_Suc gr_implies_not0 linorder_neq_iff not_less_eq)
|
|
1295 |
apply(subgoal_tac " \<forall>i<length (V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e).
|
|
1296 |
ML_closed (Suc n) ((V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e) ! i)")
|
|
1297 |
apply (auto simp:nth_Cons')
|
|
1298 |
apply (metis ML_closed_Suc Nat.less_trans Suc_eq_add_numeral_1 Suc_pred' add_0_left less_add_Suc2 less_antisym)
|
|
1299 |
done
|
23503
|
1300 |
|
|
1301 |
theorem includes Vars
|
|
1302 |
assumes t: "t : Pure_tms" and t': "t' : Pure_tms" and
|
25873
|
1303 |
closed: "free_vars t = {}" and reds: "term_of (eval t []) \<Rightarrow>* t'"
|
|
1304 |
shows "t \<rightarrow>* t'"
|
23503
|
1305 |
proof -
|
25873
|
1306 |
have ML_cl: "ML_closed_t 0 (term_of (eval t []))"
|
|
1307 |
apply(rule ML_closed_t_term_of_eval[OF t])
|
|
1308 |
using closed apply auto done
|
23503
|
1309 |
have "(eval t [])! = t!"
|
|
1310 |
using kernel_eval[OF t, where e="[]"] closed by simp
|
|
1311 |
hence "(term_of (eval t []))! = t!" by simp
|
|
1312 |
moreover have "term_of (eval t [])! \<rightarrow>* t'!"
|
|
1313 |
using kernel_inv[OF reds ML_cl] by auto
|
|
1314 |
ultimately have "t! \<rightarrow>* t'!" by simp
|
|
1315 |
thus ?thesis using kernel_pure t t' by auto
|
|
1316 |
qed
|
|
1317 |
|
|
1318 |
end
|