1 (* Title: HOL/Lambda/WeakNorm.thy |
|
2 Author: Stefan Berghofer |
|
3 Copyright 2003 TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Weak normalization for simply-typed lambda calculus *} |
|
7 |
|
8 theory WeakNorm |
|
9 imports Type NormalForm Code_Integer |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Formalization by Stefan Berghofer. Partly based on a paper proof by |
|
14 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |
|
15 *} |
|
16 |
|
17 |
|
18 subsection {* Main theorems *} |
|
19 |
|
20 lemma norm_list: |
|
21 assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'" |
|
22 and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)" |
|
23 and uNF: "NF u" and uT: "e \<turnstile> u : T" |
|
24 shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow> |
|
25 listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> |
|
26 NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow> |
|
27 \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
|
28 Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> map f as')" |
|
29 (is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'") |
|
30 proof (induct as rule: rev_induct) |
|
31 case (Nil Us) |
|
32 with Var_NF have "?ex Us [] []" by simp |
|
33 thus ?case .. |
|
34 next |
|
35 case (snoc b bs Us) |
|
36 have "e\<langle>i:T\<rangle> \<tturnstile> bs @ [b] : Us" by fact |
|
37 then obtain Vs W where Us: "Us = Vs @ [W]" |
|
38 and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W" |
|
39 by (rule types_snocE) |
|
40 from snoc have "listall ?R bs" by simp |
|
41 with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc) |
|
42 then obtain bs' where |
|
43 bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'" |
|
44 and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover |
|
45 from snoc have "?R b" by simp |
|
46 with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'" |
|
47 by iprover |
|
48 then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "NF b'" |
|
49 by iprover |
|
50 from bsNF [of 0] have "listall NF (map f bs')" |
|
51 by (rule App_NF_D) |
|
52 moreover have "NF (f b')" using bNF by (rule f_NF) |
|
53 ultimately have "listall NF (map f (bs' @ [b']))" |
|
54 by simp |
|
55 hence "\<And>j. NF (Var j \<degree>\<degree> map f (bs' @ [b']))" by (rule NF.App) |
|
56 moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'" |
|
57 by (rule f_compat) |
|
58 with bsred have |
|
59 "\<And>j. (Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs) \<degree> f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* |
|
60 (Var j \<degree>\<degree> map f bs') \<degree> f b'" by (rule rtrancl_beta_App) |
|
61 ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp |
|
62 thus ?case .. |
|
63 qed |
|
64 |
|
65 lemma subst_type_NF: |
|
66 "\<And>t e T u i. NF t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> NF u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
|
67 (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U") |
|
68 proof (induct U) |
|
69 fix T t |
|
70 let ?R = "\<lambda>t. \<forall>e T' u i. |
|
71 e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')" |
|
72 assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1" |
|
73 assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2" |
|
74 assume "NF t" |
|
75 thus "\<And>e T' u i. PROP ?Q t e T' u i T" |
|
76 proof induct |
|
77 fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T" |
|
78 { |
|
79 case (App ts x e_ T'_ u_ i_) |
|
80 assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'" |
|
81 then obtain Us |
|
82 where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'" |
|
83 and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us" |
|
84 by (rule var_app_typesE) |
|
85 from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
|
86 proof |
|
87 assume eq: "x = i" |
|
88 show ?thesis |
|
89 proof (cases ts) |
|
90 case Nil |
|
91 with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp |
|
92 with Nil and uNF show ?thesis by simp iprover |
|
93 next |
|
94 case (Cons a as) |
|
95 with argsT obtain T'' Ts where Us: "Us = T'' # Ts" |
|
96 by (cases Us) (rule FalseE, simp+, erule that) |
|
97 from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'" |
|
98 by simp |
|
99 from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto |
|
100 with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp |
|
101 from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp |
|
102 from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp |
|
103 from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
|
104 from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2) |
|
105 with lift_preserves_beta' lift_NF uNF uT argsT' |
|
106 have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
|
107 Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and> |
|
108 NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list) |
|
109 then obtain as' where |
|
110 asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
|
111 Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'" |
|
112 and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover |
|
113 from App and Cons have "?R a" by simp |
|
114 with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'" |
|
115 by iprover |
|
116 then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover |
|
117 from uNF have "NF (lift u 0)" by (rule lift_NF) |
|
118 hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF) |
|
119 then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'" |
|
120 by iprover |
|
121 from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua" |
|
122 proof (rule MI1) |
|
123 have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'" |
|
124 proof (rule typing.App) |
|
125 from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type) |
|
126 show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp |
|
127 qed |
|
128 with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
|
129 from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction') |
|
130 show "NF a'" by fact |
|
131 qed |
|
132 then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua" |
|
133 by iprover |
|
134 from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]" |
|
135 by (rule subst_preserves_beta2') |
|
136 also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]" |
|
137 by (rule subst_preserves_beta') |
|
138 also note uared |
|
139 finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" . |
|
140 hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp |
|
141 from T asNF _ uaNF have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r" |
|
142 proof (rule MI2) |
|
143 have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'" |
|
144 proof (rule list_app_typeI) |
|
145 show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp |
|
146 from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts" |
|
147 by (rule substs_lemma) |
|
148 hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts" |
|
149 by (rule lift_types) |
|
150 thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts" |
|
151 by (simp_all add: o_def) |
|
152 qed |
|
153 with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'" |
|
154 by (rule subject_reduction') |
|
155 from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
|
156 with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App) |
|
157 with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
|
158 qed |
|
159 then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" |
|
160 and rnf: "NF r" by iprover |
|
161 from asred have |
|
162 "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
|
163 (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]" |
|
164 by (rule subst_preserves_beta') |
|
165 also from uared' have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
|
166 (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2') |
|
167 also note rred |
|
168 finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" . |
|
169 with rnf Cons eq show ?thesis |
|
170 by (simp add: o_def) iprover |
|
171 qed |
|
172 next |
|
173 assume neq: "x \<noteq> i" |
|
174 from App have "listall ?R ts" by (iprover dest: listall_conj2) |
|
175 with TrueI TrueI uNF uT argsT |
|
176 have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and> |
|
177 NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'") |
|
178 by (rule norm_list [of "\<lambda>t. t", simplified]) |
|
179 then obtain ts' where NF: "?ex ts'" .. |
|
180 from nat_le_dec show ?thesis |
|
181 proof |
|
182 assume "i < x" |
|
183 with NF show ?thesis by simp iprover |
|
184 next |
|
185 assume "\<not> (i < x)" |
|
186 with NF neq show ?thesis by (simp add: subst_Var) iprover |
|
187 qed |
|
188 qed |
|
189 next |
|
190 case (Abs r e_ T'_ u_ i_) |
|
191 assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'" |
|
192 then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp |
|
193 moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF) |
|
194 moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type) |
|
195 ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs) |
|
196 thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
|
197 by simp (iprover intro: rtrancl_beta_Abs NF.Abs) |
|
198 } |
|
199 qed |
|
200 qed |
|
201 |
|
202 |
|
203 -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *} |
|
204 inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50) |
|
205 where |
|
206 Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T" |
|
207 | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)" |
|
208 | App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U" |
|
209 |
|
210 lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T" |
|
211 apply (induct set: rtyping) |
|
212 apply (erule typing.Var) |
|
213 apply (erule typing.Abs) |
|
214 apply (erule typing.App) |
|
215 apply assumption |
|
216 done |
|
217 |
|
218 |
|
219 theorem type_NF: |
|
220 assumes "e \<turnstile>\<^sub>R t : T" |
|
221 shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using assms |
|
222 proof induct |
|
223 case Var |
|
224 show ?case by (iprover intro: Var_NF) |
|
225 next |
|
226 case Abs |
|
227 thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs) |
|
228 next |
|
229 case (App e s T U t) |
|
230 from App obtain s' t' where |
|
231 sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'" |
|
232 and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover |
|
233 have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u" |
|
234 proof (rule subst_type_NF) |
|
235 have "NF (lift t' 0)" using tNF by (rule lift_NF) |
|
236 hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil) |
|
237 hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App) |
|
238 thus "NF (Var 0 \<degree> lift t' 0)" by simp |
|
239 show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U" |
|
240 proof (rule typing.App) |
|
241 show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U" |
|
242 by (rule typing.Var) simp |
|
243 from tred have "e \<turnstile> t' : T" |
|
244 by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps) |
|
245 thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T" |
|
246 by (rule lift_type) |
|
247 qed |
|
248 from sred show "e \<turnstile> s' : T \<Rightarrow> U" |
|
249 by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps) |
|
250 show "NF s'" by fact |
|
251 qed |
|
252 then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover |
|
253 from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App) |
|
254 hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans) |
|
255 with unf show ?case by iprover |
|
256 qed |
|
257 |
|
258 |
|
259 subsection {* Extracting the program *} |
|
260 |
|
261 declare NF.induct [ind_realizer] |
|
262 declare rtranclp.induct [ind_realizer irrelevant] |
|
263 declare rtyping.induct [ind_realizer] |
|
264 lemmas [extraction_expand] = conj_assoc listall_cons_eq |
|
265 |
|
266 extract type_NF |
|
267 |
|
268 lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b" |
|
269 apply (rule iffI) |
|
270 apply (erule rtranclpR.induct) |
|
271 apply (rule rtranclp.rtrancl_refl) |
|
272 apply (erule rtranclp.rtrancl_into_rtrancl) |
|
273 apply assumption |
|
274 apply (erule rtranclp.induct) |
|
275 apply (rule rtranclpR.rtrancl_refl) |
|
276 apply (erule rtranclpR.rtrancl_into_rtrancl) |
|
277 apply assumption |
|
278 done |
|
279 |
|
280 lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t" |
|
281 apply (erule NFR.induct) |
|
282 apply (rule NF.intros) |
|
283 apply (simp add: listall_def) |
|
284 apply (erule NF.intros) |
|
285 done |
|
286 |
|
287 text_raw {* |
|
288 \begin{figure} |
|
289 \renewcommand{\isastyle}{\scriptsize\it}% |
|
290 @{thm [display,eta_contract=false,margin=100] subst_type_NF_def} |
|
291 \renewcommand{\isastyle}{\small\it}% |
|
292 \caption{Program extracted from @{text subst_type_NF}} |
|
293 \label{fig:extr-subst-type-nf} |
|
294 \end{figure} |
|
295 |
|
296 \begin{figure} |
|
297 \renewcommand{\isastyle}{\scriptsize\it}% |
|
298 @{thm [display,margin=100] subst_Var_NF_def} |
|
299 @{thm [display,margin=100] app_Var_NF_def} |
|
300 @{thm [display,margin=100] lift_NF_def} |
|
301 @{thm [display,eta_contract=false,margin=100] type_NF_def} |
|
302 \renewcommand{\isastyle}{\small\it}% |
|
303 \caption{Program extracted from lemmas and main theorem} |
|
304 \label{fig:extr-type-nf} |
|
305 \end{figure} |
|
306 *} |
|
307 |
|
308 text {* |
|
309 The program corresponding to the proof of the central lemma, which |
|
310 performs substitution and normalization, is shown in Figure |
|
311 \ref{fig:extr-subst-type-nf}. The correctness |
|
312 theorem corresponding to the program @{text "subst_type_NF"} is |
|
313 @{thm [display,margin=100] subst_type_NF_correctness |
|
314 [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]} |
|
315 where @{text NFR} is the realizability predicate corresponding to |
|
316 the datatype @{text NFT}, which is inductively defined by the rules |
|
317 \pagebreak |
|
318 @{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]} |
|
319 |
|
320 The programs corresponding to the main theorem @{text "type_NF"}, as |
|
321 well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}. |
|
322 The correctness statement for the main function @{text "type_NF"} is |
|
323 @{thm [display,margin=100] type_NF_correctness |
|
324 [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]} |
|
325 where the realizability predicate @{text "rtypingR"} corresponding to the |
|
326 computationally relevant version of the typing judgement is inductively |
|
327 defined by the rules |
|
328 @{thm [display,margin=100] rtypingR.Var [no_vars] |
|
329 rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]} |
|
330 *} |
|
331 |
|
332 subsection {* Generating executable code *} |
|
333 |
|
334 instantiation NFT :: default |
|
335 begin |
|
336 |
|
337 definition "default = Dummy ()" |
|
338 |
|
339 instance .. |
|
340 |
|
341 end |
|
342 |
|
343 instantiation dB :: default |
|
344 begin |
|
345 |
|
346 definition "default = dB.Var 0" |
|
347 |
|
348 instance .. |
|
349 |
|
350 end |
|
351 |
|
352 instantiation prod :: (default, default) default |
|
353 begin |
|
354 |
|
355 definition "default = (default, default)" |
|
356 |
|
357 instance .. |
|
358 |
|
359 end |
|
360 |
|
361 instantiation list :: (type) default |
|
362 begin |
|
363 |
|
364 definition "default = []" |
|
365 |
|
366 instance .. |
|
367 |
|
368 end |
|
369 |
|
370 instantiation "fun" :: (type, default) default |
|
371 begin |
|
372 |
|
373 definition "default = (\<lambda>x. default)" |
|
374 |
|
375 instance .. |
|
376 |
|
377 end |
|
378 |
|
379 definition int_of_nat :: "nat \<Rightarrow> int" where |
|
380 "int_of_nat = of_nat" |
|
381 |
|
382 text {* |
|
383 The following functions convert between Isabelle's built-in {\tt term} |
|
384 datatype and the generated {\tt dB} datatype. This allows to |
|
385 generate example terms using Isabelle's parser and inspect |
|
386 normalized terms using Isabelle's pretty printer. |
|
387 *} |
|
388 |
|
389 ML {* |
|
390 fun dBtype_of_typ (Type ("fun", [T, U])) = |
|
391 @{code Fun} (dBtype_of_typ T, dBtype_of_typ U) |
|
392 | dBtype_of_typ (TFree (s, _)) = (case explode s of |
|
393 ["'", a] => @{code Atom} (@{code nat} (ord a - 97)) |
|
394 | _ => error "dBtype_of_typ: variable name") |
|
395 | dBtype_of_typ _ = error "dBtype_of_typ: bad type"; |
|
396 |
|
397 fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i) |
|
398 | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u) |
|
399 | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t) |
|
400 | dB_of_term _ = error "dB_of_term: bad term"; |
|
401 |
|
402 fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) = |
|
403 Abs ("x", T, term_of_dB (T :: Ts) U dBt) |
|
404 | term_of_dB Ts _ dBt = term_of_dB' Ts dBt |
|
405 and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n) |
|
406 | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) = |
|
407 let val t = term_of_dB' Ts dBt |
|
408 in case fastype_of1 (Ts, t) of |
|
409 Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu |
|
410 | _ => error "term_of_dB: function type expected" |
|
411 end |
|
412 | term_of_dB' _ _ = error "term_of_dB: term not in normal form"; |
|
413 |
|
414 fun typing_of_term Ts e (Bound i) = |
|
415 @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i)) |
|
416 | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of |
|
417 Type ("fun", [T, U]) => @{code App} (e, dB_of_term t, |
|
418 dBtype_of_typ T, dBtype_of_typ U, dB_of_term u, |
|
419 typing_of_term Ts e t, typing_of_term Ts e u) |
|
420 | _ => error "typing_of_term: function type expected") |
|
421 | typing_of_term Ts e (Abs (s, T, t)) = |
|
422 let val dBT = dBtype_of_typ T |
|
423 in @{code Abs} (e, dBT, dB_of_term t, |
|
424 dBtype_of_typ (fastype_of1 (T :: Ts, t)), |
|
425 typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t) |
|
426 end |
|
427 | typing_of_term _ _ _ = error "typing_of_term: bad term"; |
|
428 |
|
429 fun dummyf _ = error "dummy"; |
|
430 |
|
431 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; |
|
432 val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1)); |
|
433 val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1); |
|
434 |
|
435 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"}; |
|
436 val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2)); |
|
437 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2); |
|
438 *} |
|
439 |
|
440 text {* |
|
441 The same story again for the SML code generator. |
|
442 *} |
|
443 |
|
444 consts_code |
|
445 "default" ("(error \"default\")") |
|
446 "default :: 'a \<Rightarrow> 'b::default" ("(fn '_ => error \"default\")") |
|
447 |
|
448 code_module Norm |
|
449 contains |
|
450 test = "type_NF" |
|
451 |
|
452 ML {* |
|
453 fun nat_of_int 0 = Norm.zero |
|
454 | nat_of_int n = Norm.Suc (nat_of_int (n-1)); |
|
455 |
|
456 fun int_of_nat Norm.zero = 0 |
|
457 | int_of_nat (Norm.Suc n) = 1 + int_of_nat n; |
|
458 |
|
459 fun dBtype_of_typ (Type ("fun", [T, U])) = |
|
460 Norm.Fun (dBtype_of_typ T, dBtype_of_typ U) |
|
461 | dBtype_of_typ (TFree (s, _)) = (case explode s of |
|
462 ["'", a] => Norm.Atom (nat_of_int (ord a - 97)) |
|
463 | _ => error "dBtype_of_typ: variable name") |
|
464 | dBtype_of_typ _ = error "dBtype_of_typ: bad type"; |
|
465 |
|
466 fun dB_of_term (Bound i) = Norm.dB_Var (nat_of_int i) |
|
467 | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u) |
|
468 | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t) |
|
469 | dB_of_term _ = error "dB_of_term: bad term"; |
|
470 |
|
471 fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) = |
|
472 Abs ("x", T, term_of_dB (T :: Ts) U dBt) |
|
473 | term_of_dB Ts _ dBt = term_of_dB' Ts dBt |
|
474 and term_of_dB' Ts (Norm.dB_Var n) = Bound (int_of_nat n) |
|
475 | term_of_dB' Ts (Norm.App (dBt, dBu)) = |
|
476 let val t = term_of_dB' Ts dBt |
|
477 in case fastype_of1 (Ts, t) of |
|
478 Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu |
|
479 | _ => error "term_of_dB: function type expected" |
|
480 end |
|
481 | term_of_dB' _ _ = error "term_of_dB: term not in normal form"; |
|
482 |
|
483 fun typing_of_term Ts e (Bound i) = |
|
484 Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i))) |
|
485 | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of |
|
486 Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t, |
|
487 dBtype_of_typ T, dBtype_of_typ U, dB_of_term u, |
|
488 typing_of_term Ts e t, typing_of_term Ts e u) |
|
489 | _ => error "typing_of_term: function type expected") |
|
490 | typing_of_term Ts e (Abs (s, T, t)) = |
|
491 let val dBT = dBtype_of_typ T |
|
492 in Norm.rtypingT_Abs (e, dBT, dB_of_term t, |
|
493 dBtype_of_typ (fastype_of1 (T :: Ts, t)), |
|
494 typing_of_term (T :: Ts) (Norm.shift e Norm.zero dBT) t) |
|
495 end |
|
496 | typing_of_term _ _ _ = error "typing_of_term: bad term"; |
|
497 |
|
498 fun dummyf _ = error "dummy"; |
|
499 *} |
|
500 |
|
501 text {* |
|
502 We now try out the extracted program @{text "type_NF"} on some example terms. |
|
503 *} |
|
504 |
|
505 ML {* |
|
506 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; |
|
507 val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1)); |
|
508 val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1); |
|
509 |
|
510 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"}; |
|
511 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2)); |
|
512 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2); |
|
513 *} |
|
514 |
|
515 end |
|