1 (* Title: HOL/Lambda/Standardization.thy |
|
2 Author: Stefan Berghofer |
|
3 Copyright 2005 TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Standardization *} |
|
7 |
|
8 theory Standardization |
|
9 imports NormalForm |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Based on lecture notes by Ralph Matthes \cite{Matthes-ESSLLI2000}, |
|
14 original proof idea due to Ralph Loader \cite{Loader1998}. |
|
15 *} |
|
16 |
|
17 |
|
18 subsection {* Standard reduction relation *} |
|
19 |
|
20 declare listrel_mono [mono_set] |
|
21 |
|
22 inductive |
|
23 sred :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>s" 50) |
|
24 and sredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool" (infixl "[\<rightarrow>\<^sub>s]" 50) |
|
25 where |
|
26 "s [\<rightarrow>\<^sub>s] t \<equiv> listrelp op \<rightarrow>\<^sub>s s t" |
|
27 | Var: "rs [\<rightarrow>\<^sub>s] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> rs'" |
|
28 | Abs: "r \<rightarrow>\<^sub>s r' \<Longrightarrow> ss [\<rightarrow>\<^sub>s] ss' \<Longrightarrow> Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> ss'" |
|
29 | Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t" |
|
30 |
|
31 lemma refl_listrelp: "\<forall>x\<in>set xs. R x x \<Longrightarrow> listrelp R xs xs" |
|
32 by (induct xs) (auto intro: listrelp.intros) |
|
33 |
|
34 lemma refl_sred: "t \<rightarrow>\<^sub>s t" |
|
35 by (induct t rule: Apps_dB_induct) (auto intro: refl_listrelp sred.intros) |
|
36 |
|
37 lemma refl_sreds: "ts [\<rightarrow>\<^sub>s] ts" |
|
38 by (simp add: refl_sred refl_listrelp) |
|
39 |
|
40 lemma listrelp_conj1: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp R x y" |
|
41 by (erule listrelp.induct) (auto intro: listrelp.intros) |
|
42 |
|
43 lemma listrelp_conj2: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp S x y" |
|
44 by (erule listrelp.induct) (auto intro: listrelp.intros) |
|
45 |
|
46 lemma listrelp_app: |
|
47 assumes xsys: "listrelp R xs ys" |
|
48 shows "listrelp R xs' ys' \<Longrightarrow> listrelp R (xs @ xs') (ys @ ys')" using xsys |
|
49 by (induct arbitrary: xs' ys') (auto intro: listrelp.intros) |
|
50 |
|
51 lemma lemma1: |
|
52 assumes r: "r \<rightarrow>\<^sub>s r'" and s: "s \<rightarrow>\<^sub>s s'" |
|
53 shows "r \<degree> s \<rightarrow>\<^sub>s r' \<degree> s'" using r |
|
54 proof induct |
|
55 case (Var rs rs' x) |
|
56 then have "rs [\<rightarrow>\<^sub>s] rs'" by (rule listrelp_conj1) |
|
57 moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros) |
|
58 ultimately have "rs @ [s] [\<rightarrow>\<^sub>s] rs' @ [s']" by (rule listrelp_app) |
|
59 hence "Var x \<degree>\<degree> (rs @ [s]) \<rightarrow>\<^sub>s Var x \<degree>\<degree> (rs' @ [s'])" by (rule sred.Var) |
|
60 thus ?case by (simp only: app_last) |
|
61 next |
|
62 case (Abs r r' ss ss') |
|
63 from Abs(3) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1) |
|
64 moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros) |
|
65 ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app) |
|
66 with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])" |
|
67 by (rule sred.Abs) |
|
68 thus ?case by (simp only: app_last) |
|
69 next |
|
70 case (Beta r u ss t) |
|
71 hence "r[u/0] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last) |
|
72 hence "Abs r \<degree> u \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (rule sred.Beta) |
|
73 thus ?case by (simp only: app_last) |
|
74 qed |
|
75 |
|
76 lemma lemma1': |
|
77 assumes ts: "ts [\<rightarrow>\<^sub>s] ts'" |
|
78 shows "r \<rightarrow>\<^sub>s r' \<Longrightarrow> r \<degree>\<degree> ts \<rightarrow>\<^sub>s r' \<degree>\<degree> ts'" using ts |
|
79 by (induct arbitrary: r r') (auto intro: lemma1) |
|
80 |
|
81 lemma lemma2_1: |
|
82 assumes beta: "t \<rightarrow>\<^sub>\<beta> u" |
|
83 shows "t \<rightarrow>\<^sub>s u" using beta |
|
84 proof induct |
|
85 case (beta s t) |
|
86 have "Abs s \<degree> t \<degree>\<degree> [] \<rightarrow>\<^sub>s s[t/0] \<degree>\<degree> []" by (iprover intro: sred.Beta refl_sred) |
|
87 thus ?case by simp |
|
88 next |
|
89 case (appL s t u) |
|
90 thus ?case by (iprover intro: lemma1 refl_sred) |
|
91 next |
|
92 case (appR s t u) |
|
93 thus ?case by (iprover intro: lemma1 refl_sred) |
|
94 next |
|
95 case (abs s t) |
|
96 hence "Abs s \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs t \<degree>\<degree> []" by (iprover intro: sred.Abs listrelp.Nil) |
|
97 thus ?case by simp |
|
98 qed |
|
99 |
|
100 lemma listrelp_betas: |
|
101 assumes ts: "listrelp op \<rightarrow>\<^sub>\<beta>\<^sup>* ts ts'" |
|
102 shows "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<degree>\<degree> ts'" using ts |
|
103 by induct auto |
|
104 |
|
105 lemma lemma2_2: |
|
106 assumes t: "t \<rightarrow>\<^sub>s u" |
|
107 shows "t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using t |
|
108 by induct (auto dest: listrelp_conj2 |
|
109 intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp) |
|
110 |
|
111 lemma sred_lift: |
|
112 assumes s: "s \<rightarrow>\<^sub>s t" |
|
113 shows "lift s i \<rightarrow>\<^sub>s lift t i" using s |
|
114 proof (induct arbitrary: i) |
|
115 case (Var rs rs' x) |
|
116 hence "map (\<lambda>t. lift t i) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) rs'" |
|
117 by induct (auto intro: listrelp.intros) |
|
118 thus ?case by (cases "x < i") (auto intro: sred.Var) |
|
119 next |
|
120 case (Abs r r' ss ss') |
|
121 from Abs(3) have "map (\<lambda>t. lift t i) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) ss'" |
|
122 by induct (auto intro: listrelp.intros) |
|
123 thus ?case by (auto intro: sred.Abs Abs) |
|
124 next |
|
125 case (Beta r s ss t) |
|
126 thus ?case by (auto intro: sred.Beta) |
|
127 qed |
|
128 |
|
129 lemma lemma3: |
|
130 assumes r: "r \<rightarrow>\<^sub>s r'" |
|
131 shows "s \<rightarrow>\<^sub>s s' \<Longrightarrow> r[s/x] \<rightarrow>\<^sub>s r'[s'/x]" using r |
|
132 proof (induct arbitrary: s s' x) |
|
133 case (Var rs rs' y) |
|
134 hence "map (\<lambda>t. t[s/x]) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) rs'" |
|
135 by induct (auto intro: listrelp.intros Var) |
|
136 moreover have "Var y[s/x] \<rightarrow>\<^sub>s Var y[s'/x]" |
|
137 proof (cases "y < x") |
|
138 case True thus ?thesis by simp (rule refl_sred) |
|
139 next |
|
140 case False |
|
141 thus ?thesis |
|
142 by (cases "y = x") (auto simp add: Var intro: refl_sred) |
|
143 qed |
|
144 ultimately show ?case by simp (rule lemma1') |
|
145 next |
|
146 case (Abs r r' ss ss') |
|
147 from Abs(4) have "lift s 0 \<rightarrow>\<^sub>s lift s' 0" by (rule sred_lift) |
|
148 hence "r[lift s 0/Suc x] \<rightarrow>\<^sub>s r'[lift s' 0/Suc x]" by (fast intro: Abs.hyps) |
|
149 moreover from Abs(3) have "map (\<lambda>t. t[s/x]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) ss'" |
|
150 by induct (auto intro: listrelp.intros Abs) |
|
151 ultimately show ?case by simp (rule sred.Abs) |
|
152 next |
|
153 case (Beta r u ss t) |
|
154 thus ?case by (auto simp add: subst_subst intro: sred.Beta) |
|
155 qed |
|
156 |
|
157 lemma lemma4_aux: |
|
158 assumes rs: "listrelp (\<lambda>t u. t \<rightarrow>\<^sub>s u \<and> (\<forall>r. u \<rightarrow>\<^sub>\<beta> r \<longrightarrow> t \<rightarrow>\<^sub>s r)) rs rs'" |
|
159 shows "rs' => ss \<Longrightarrow> rs [\<rightarrow>\<^sub>s] ss" using rs |
|
160 proof (induct arbitrary: ss) |
|
161 case Nil |
|
162 thus ?case by cases (auto intro: listrelp.Nil) |
|
163 next |
|
164 case (Cons x y xs ys) |
|
165 note Cons' = Cons |
|
166 show ?case |
|
167 proof (cases ss) |
|
168 case Nil with Cons show ?thesis by simp |
|
169 next |
|
170 case (Cons y' ys') |
|
171 hence ss: "ss = y' # ys'" by simp |
|
172 from Cons Cons' have "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys \<or> y' = y \<and> ys => ys'" by simp |
|
173 hence "x # xs [\<rightarrow>\<^sub>s] y' # ys'" |
|
174 proof |
|
175 assume H: "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys" |
|
176 with Cons' have "x \<rightarrow>\<^sub>s y'" by blast |
|
177 moreover from Cons' have "xs [\<rightarrow>\<^sub>s] ys" by (iprover dest: listrelp_conj1) |
|
178 ultimately have "x # xs [\<rightarrow>\<^sub>s] y' # ys" by (rule listrelp.Cons) |
|
179 with H show ?thesis by simp |
|
180 next |
|
181 assume H: "y' = y \<and> ys => ys'" |
|
182 with Cons' have "x \<rightarrow>\<^sub>s y'" by blast |
|
183 moreover from H have "xs [\<rightarrow>\<^sub>s] ys'" by (blast intro: Cons') |
|
184 ultimately show ?thesis by (rule listrelp.Cons) |
|
185 qed |
|
186 with ss show ?thesis by simp |
|
187 qed |
|
188 qed |
|
189 |
|
190 lemma lemma4: |
|
191 assumes r: "r \<rightarrow>\<^sub>s r'" |
|
192 shows "r' \<rightarrow>\<^sub>\<beta> r'' \<Longrightarrow> r \<rightarrow>\<^sub>s r''" using r |
|
193 proof (induct arbitrary: r'') |
|
194 case (Var rs rs' x) |
|
195 then obtain ss where rs: "rs' => ss" and r'': "r'' = Var x \<degree>\<degree> ss" |
|
196 by (blast dest: head_Var_reduction) |
|
197 from Var(1) rs have "rs [\<rightarrow>\<^sub>s] ss" by (rule lemma4_aux) |
|
198 hence "Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> ss" by (rule sred.Var) |
|
199 with r'' show ?case by simp |
|
200 next |
|
201 case (Abs r r' ss ss') |
|
202 from `Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''` show ?case |
|
203 proof |
|
204 fix s |
|
205 assume r'': "r'' = s \<degree>\<degree> ss'" |
|
206 assume "Abs r' \<rightarrow>\<^sub>\<beta> s" |
|
207 then obtain r''' where s: "s = Abs r'''" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" by cases auto |
|
208 from r''' have "r \<rightarrow>\<^sub>s r'''" by (blast intro: Abs) |
|
209 moreover from Abs have "ss [\<rightarrow>\<^sub>s] ss'" by (iprover dest: listrelp_conj1) |
|
210 ultimately have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r''' \<degree>\<degree> ss'" by (rule sred.Abs) |
|
211 with r'' s show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp |
|
212 next |
|
213 fix rs' |
|
214 assume "ss' => rs'" |
|
215 with Abs(3) have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux) |
|
216 with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs) |
|
217 moreover assume "r'' = Abs r' \<degree>\<degree> rs'" |
|
218 ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp |
|
219 next |
|
220 fix t u' us' |
|
221 assume "ss' = u' # us'" |
|
222 with Abs(3) obtain u us where |
|
223 ss: "ss = u # us" and u: "u \<rightarrow>\<^sub>s u'" and us: "us [\<rightarrow>\<^sub>s] us'" |
|
224 by cases (auto dest!: listrelp_conj1) |
|
225 have "r[u/0] \<rightarrow>\<^sub>s r'[u'/0]" using Abs(1) and u by (rule lemma3) |
|
226 with us have "r[u/0] \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule lemma1') |
|
227 hence "Abs r \<degree> u \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule sred.Beta) |
|
228 moreover assume "Abs r' = Abs t" and "r'' = t[u'/0] \<degree>\<degree> us'" |
|
229 ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" using ss by simp |
|
230 qed |
|
231 next |
|
232 case (Beta r s ss t) |
|
233 show ?case |
|
234 by (rule sred.Beta) (rule Beta)+ |
|
235 qed |
|
236 |
|
237 lemma rtrancl_beta_sred: |
|
238 assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'" |
|
239 shows "r \<rightarrow>\<^sub>s r'" using r |
|
240 by induct (iprover intro: refl_sred lemma4)+ |
|
241 |
|
242 |
|
243 subsection {* Leftmost reduction and weakly normalizing terms *} |
|
244 |
|
245 inductive |
|
246 lred :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>l" 50) |
|
247 and lredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool" (infixl "[\<rightarrow>\<^sub>l]" 50) |
|
248 where |
|
249 "s [\<rightarrow>\<^sub>l] t \<equiv> listrelp op \<rightarrow>\<^sub>l s t" |
|
250 | Var: "rs [\<rightarrow>\<^sub>l] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>l Var x \<degree>\<degree> rs'" |
|
251 | Abs: "r \<rightarrow>\<^sub>l r' \<Longrightarrow> Abs r \<rightarrow>\<^sub>l Abs r'" |
|
252 | Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>l t" |
|
253 |
|
254 lemma lred_imp_sred: |
|
255 assumes lred: "s \<rightarrow>\<^sub>l t" |
|
256 shows "s \<rightarrow>\<^sub>s t" using lred |
|
257 proof induct |
|
258 case (Var rs rs' x) |
|
259 then have "rs [\<rightarrow>\<^sub>s] rs'" |
|
260 by induct (iprover intro: listrelp.intros)+ |
|
261 then show ?case by (rule sred.Var) |
|
262 next |
|
263 case (Abs r r') |
|
264 from `r \<rightarrow>\<^sub>s r'` |
|
265 have "Abs r \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> []" using listrelp.Nil |
|
266 by (rule sred.Abs) |
|
267 then show ?case by simp |
|
268 next |
|
269 case (Beta r s ss t) |
|
270 from `r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t` |
|
271 show ?case by (rule sred.Beta) |
|
272 qed |
|
273 |
|
274 inductive WN :: "dB => bool" |
|
275 where |
|
276 Var: "listsp WN rs \<Longrightarrow> WN (Var n \<degree>\<degree> rs)" |
|
277 | Lambda: "WN r \<Longrightarrow> WN (Abs r)" |
|
278 | Beta: "WN ((r[s/0]) \<degree>\<degree> ss) \<Longrightarrow> WN ((Abs r \<degree> s) \<degree>\<degree> ss)" |
|
279 |
|
280 lemma listrelp_imp_listsp1: |
|
281 assumes H: "listrelp (\<lambda>x y. P x) xs ys" |
|
282 shows "listsp P xs" using H |
|
283 by induct auto |
|
284 |
|
285 lemma listrelp_imp_listsp2: |
|
286 assumes H: "listrelp (\<lambda>x y. P y) xs ys" |
|
287 shows "listsp P ys" using H |
|
288 by induct auto |
|
289 |
|
290 lemma lemma5: |
|
291 assumes lred: "r \<rightarrow>\<^sub>l r'" |
|
292 shows "WN r" and "NF r'" using lred |
|
293 by induct |
|
294 (iprover dest: listrelp_conj1 listrelp_conj2 |
|
295 listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros |
|
296 NF.intros [simplified listall_listsp_eq])+ |
|
297 |
|
298 lemma lemma6: |
|
299 assumes wn: "WN r" |
|
300 shows "\<exists>r'. r \<rightarrow>\<^sub>l r'" using wn |
|
301 proof induct |
|
302 case (Var rs n) |
|
303 then have "\<exists>rs'. rs [\<rightarrow>\<^sub>l] rs'" |
|
304 by induct (iprover intro: listrelp.intros)+ |
|
305 then show ?case by (iprover intro: lred.Var) |
|
306 qed (iprover intro: lred.intros)+ |
|
307 |
|
308 lemma lemma7: |
|
309 assumes r: "r \<rightarrow>\<^sub>s r'" |
|
310 shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r |
|
311 proof induct |
|
312 case (Var rs rs' x) |
|
313 from `NF (Var x \<degree>\<degree> rs')` have "listall NF rs'" |
|
314 by cases simp_all |
|
315 with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'" |
|
316 proof induct |
|
317 case Nil |
|
318 show ?case by (rule listrelp.Nil) |
|
319 next |
|
320 case (Cons x y xs ys) |
|
321 hence "x \<rightarrow>\<^sub>l y" and "xs [\<rightarrow>\<^sub>l] ys" by simp_all |
|
322 thus ?case by (rule listrelp.Cons) |
|
323 qed |
|
324 thus ?case by (rule lred.Var) |
|
325 next |
|
326 case (Abs r r' ss ss') |
|
327 from `NF (Abs r' \<degree>\<degree> ss')` |
|
328 have ss': "ss' = []" by (rule Abs_NF) |
|
329 from Abs(3) have ss: "ss = []" using ss' |
|
330 by cases simp_all |
|
331 from ss' Abs have "NF (Abs r')" by simp |
|
332 hence "NF r'" by cases simp_all |
|
333 with Abs have "r \<rightarrow>\<^sub>l r'" by simp |
|
334 hence "Abs r \<rightarrow>\<^sub>l Abs r'" by (rule lred.Abs) |
|
335 with ss ss' show ?case by simp |
|
336 next |
|
337 case (Beta r s ss t) |
|
338 hence "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t" by simp |
|
339 thus ?case by (rule lred.Beta) |
|
340 qed |
|
341 |
|
342 lemma WN_eq: "WN t = (\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')" |
|
343 proof |
|
344 assume "WN t" |
|
345 then have "\<exists>t'. t \<rightarrow>\<^sub>l t'" by (rule lemma6) |
|
346 then obtain t' where t': "t \<rightarrow>\<^sub>l t'" .. |
|
347 then have NF: "NF t'" by (rule lemma5) |
|
348 from t' have "t \<rightarrow>\<^sub>s t'" by (rule lred_imp_sred) |
|
349 then have "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" by (rule lemma2_2) |
|
350 with NF show "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by iprover |
|
351 next |
|
352 assume "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
|
353 then obtain t' where t': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and NF: "NF t'" |
|
354 by iprover |
|
355 from t' have "t \<rightarrow>\<^sub>s t'" by (rule rtrancl_beta_sred) |
|
356 then have "t \<rightarrow>\<^sub>l t'" using NF by (rule lemma7) |
|
357 then show "WN t" by (rule lemma5) |
|
358 qed |
|
359 |
|
360 end |
|