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