1(*  Title:      HOL/Proofs/Lambda/WeakNorm.thy
2    Author:     Stefan Berghofer
3    Copyright   2003 TU Muenchen
4*)
5
6section \<open>Weak normalization for simply-typed lambda calculus\<close>
7
8theory WeakNorm
9imports LambdaType NormalForm "HOL-Library.Realizers" "HOL-Library.Code_Target_Int"
10begin
11
12text \<open>
13Formalization by Stefan Berghofer. Partly based on a paper proof by
14Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
15\<close>
16
17
18subsection \<open>Main theorems\<close>
19
20lemma 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'")
30proof (induct as rule: rev_induct)
31  case (Nil Us)
32  with Var_NF have "?ex Us [] []" by simp
33  thus ?case ..
34next
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 bsred: "Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
43    and bsNF: "NF (Var j \<degree>\<degree> map f bs')" for j
44    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 ..
63qed
64
65lemma 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")
68proof (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 e1 T'1 u1 i1)
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)
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 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 e1 T'1 u1 i1)
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 \<open>NF u\<close> 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
200qed
201
202
203\<comment> \<open>A computationally relevant copy of @{term "e \<turnstile> t : T"}\<close>
204inductive 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
210lemma 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
219theorem 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
222proof induct
223  case Var
224  show ?case by (iprover intro: Var_NF)
225next
226  case Abs
227  thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
228next
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
256qed
257
258
259subsection \<open>Extracting the program\<close>
260
261declare NF.induct [ind_realizer]
262declare rtranclp.induct [ind_realizer irrelevant]
263declare rtyping.induct [ind_realizer]
264lemmas [extraction_expand] = conj_assoc listall_cons_eq
265
266extract type_NF
267
268lemma 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
280lemma 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
287text_raw \<open>
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 \<open>subst_type_NF\<close>}
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\<close>
307
308text \<open>
309The program corresponding to the proof of the central lemma, which
310performs substitution and normalization, is shown in Figure
311\ref{fig:extr-subst-type-nf}. The correctness
312theorem corresponding to the program \<open>subst_type_NF\<close> is
313@{thm [display,margin=100] subst_type_NF_correctness
314  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
315where \<open>NFR\<close> is the realizability predicate corresponding to
316the datatype \<open>NFT\<close>, 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
320The programs corresponding to the main theorem \<open>type_NF\<close>, as
321well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
322The correctness statement for the main function \<open>type_NF\<close> is
323@{thm [display,margin=100] type_NF_correctness
324  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
325where the realizability predicate \<open>rtypingR\<close> corresponding to the
326computationally relevant version of the typing judgement is inductively
327defined 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\<close>
331
332subsection \<open>Generating executable code\<close>
333
334instantiation NFT :: default
335begin
336
337definition "default = Dummy ()"
338
339instance ..
340
341end
342
343instantiation dB :: default
344begin
345
346definition "default = dB.Var 0"
347
348instance ..
349
350end
351
352instantiation prod :: (default, default) default
353begin
354
355definition "default = (default, default)"
356
357instance ..
358
359end
360
361instantiation list :: (type) default
362begin
363
364definition "default = []"
365
366instance ..
367
368end
369
370instantiation "fun" :: (type, default) default
371begin
372
373definition "default = (\<lambda>x. default)"
374
375instance ..
376
377end
378
379definition int_of_nat :: "nat \<Rightarrow> int" where
380  "int_of_nat = of_nat"
381
382text \<open>
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\<close>
388
389ML \<open>
390val nat_of_integer = @{code nat} o @{code int_of_integer};
391
392fun dBtype_of_typ (Type ("fun", [T, U])) =
393      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
394  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
395        ["'", a] => @{code Atom} (nat_of_integer (ord a - 97))
396      | _ => error "dBtype_of_typ: variable name")
397  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
398
399fun dB_of_term (Bound i) = @{code dB.Var} (nat_of_integer i)
400  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
401  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
402  | dB_of_term _ = error "dB_of_term: bad term";
403
404fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
405      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
406  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
407and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code integer_of_nat} n)
408  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
409      let val t = term_of_dB' Ts dBt
410      in case fastype_of1 (Ts, t) of
411          Type ("fun", [T, _]) => t $ term_of_dB Ts T dBu
412        | _ => error "term_of_dB: function type expected"
413      end
414  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
415
416fun typing_of_term Ts e (Bound i) =
417      @{code Var} (e, nat_of_integer i, dBtype_of_typ (nth Ts i))
418  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
419        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
420          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
421          typing_of_term Ts e t, typing_of_term Ts e u)
422      | _ => error "typing_of_term: function type expected")
423  | typing_of_term Ts e (Abs (_, T, t)) =
424      let val dBT = dBtype_of_typ T
425      in @{code Abs} (e, dBT, dB_of_term t,
426        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
427        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
428      end
429  | typing_of_term _ _ _ = error "typing_of_term: bad term";
430
431fun dummyf _ = error "dummy";
432
433val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
434val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
435val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
436
437val 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)))))"};
438val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
439val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
440\<close>
441
442end
443