src/HOL/Lambda/WeakNorm.thy
author nipkow
Thu Dec 11 08:52:50 2008 +0100 (2008-12-11)
changeset 29106 25e28a4070f3
parent 28262 aa7ca36d67fd
child 32010 cb1a1c94b4cd
permissions -rw-r--r--
Testfile for Stefan's code generator
     1 (*  Title:      HOL/Lambda/WeakNorm.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     4     Copyright   2003 TU Muenchen
     5 *)
     6 
     7 header {* Weak normalization for simply-typed lambda calculus *}
     8 
     9 theory WeakNorm
    10 imports Type NormalForm Code_Integer
    11 begin
    12 
    13 text {*
    14 Formalization by Stefan Berghofer. Partly based on a paper proof by
    15 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
    16 *}
    17 
    18 
    19 subsection {* Main theorems *}
    20 
    21 lemma norm_list:
    22   assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
    23   and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)"
    24   and uNF: "NF u" and uT: "e \<turnstile> u : T"
    25   shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow>
    26     listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>
    27       NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow>
    28     \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*
    29       Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> map f as')"
    30   (is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'")
    31 proof (induct as rule: rev_induct)
    32   case (Nil Us)
    33   with Var_NF have "?ex Us [] []" by simp
    34   thus ?case ..
    35 next
    36   case (snoc b bs Us)
    37   have "e\<langle>i:T\<rangle> \<tturnstile> bs  @ [b] : Us" by fact
    38   then obtain Vs W where Us: "Us = Vs @ [W]"
    39     and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W"
    40     by (rule types_snocE)
    41   from snoc have "listall ?R bs" by simp
    42   with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
    43   then obtain bs' where
    44     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'"
    45     and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
    46   from snoc have "?R b" by simp
    47   with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
    48     by iprover
    49   then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "NF b'"
    50     by iprover
    51   from bsNF [of 0] have "listall NF (map f bs')"
    52     by (rule App_NF_D)
    53   moreover have "NF (f b')" using bNF by (rule f_NF)
    54   ultimately have "listall NF (map f (bs' @ [b']))"
    55     by simp
    56   hence "\<And>j. NF (Var j \<degree>\<degree> map f (bs' @ [b']))" by (rule NF.App)
    57   moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'"
    58     by (rule f_compat)
    59   with bsred have
    60     "\<And>j. (Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs) \<degree> f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>*
    61      (Var j \<degree>\<degree> map f bs') \<degree> f b'" by (rule rtrancl_beta_App)
    62   ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
    63   thus ?case ..
    64 qed
    65 
    66 lemma subst_type_NF:
    67   "\<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'"
    68   (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
    69 proof (induct U)
    70   fix T t
    71   let ?R = "\<lambda>t. \<forall>e T' u i.
    72     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')"
    73   assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
    74   assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
    75   assume "NF t"
    76   thus "\<And>e T' u i. PROP ?Q t e T' u i T"
    77   proof induct
    78     fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
    79     {
    80       case (App ts x e_ T'_ u_ i_)
    81       assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
    82       then obtain Us
    83 	where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
    84 	and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"
    85 	by (rule var_app_typesE)
    86       from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
    87       proof
    88 	assume eq: "x = i"
    89 	show ?thesis
    90 	proof (cases ts)
    91 	  case Nil
    92 	  with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp
    93 	  with Nil and uNF show ?thesis by simp iprover
    94 	next
    95 	  case (Cons a as)
    96           with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
    97 	    by (cases Us) (rule FalseE, simp+, erule that)
    98 	  from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
    99 	    by simp
   100           from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
   101           with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
   102 	  from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp
   103 	  from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp
   104 	  from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
   105 	  from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
   106 	  with lift_preserves_beta' lift_NF uNF uT argsT'
   107 	  have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
   108             Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>
   109 	    NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list)
   110 	  then obtain as' where
   111 	    asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
   112 	      Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
   113 	    and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover
   114 	  from App and Cons have "?R a" by simp
   115 	  with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'"
   116 	    by iprover
   117 	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover
   118 	  from uNF have "NF (lift u 0)" by (rule lift_NF)
   119 	  hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF)
   120 	  then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'"
   121 	    by iprover
   122 	  from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua"
   123 	  proof (rule MI1)
   124 	    have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
   125 	    proof (rule typing.App)
   126 	      from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type)
   127 	      show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp
   128 	    qed
   129 	    with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')
   130 	    from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
   131 	    show "NF a'" by fact
   132 	  qed
   133 	  then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua"
   134 	    by iprover
   135 	  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]"
   136 	    by (rule subst_preserves_beta2')
   137 	  also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"
   138 	    by (rule subst_preserves_beta')
   139 	  also note uared
   140 	  finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .
   141 	  hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp
   142 	  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"
   143 	  proof (rule MI2)
   144 	    have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'"
   145 	    proof (rule list_app_typeI)
   146 	      show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp
   147 	      from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
   148 		by (rule substs_lemma)
   149 	      hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"
   150 		by (rule lift_types)
   151 	      thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"
   152 		by (simp_all add: map_compose [symmetric] o_def)
   153 	    qed
   154 	    with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"
   155 	      by (rule subject_reduction')
   156 	    from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
   157 	    with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App)
   158 	    with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
   159 	  qed
   160 	  then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
   161 	    and rnf: "NF r" by iprover
   162 	  from asred have
   163 	    "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
   164 	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
   165 	    by (rule subst_preserves_beta')
   166 	  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>*
   167 	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2')
   168 	  also note rred
   169 	  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" .
   170 	  with rnf Cons eq show ?thesis
   171 	    by (simp add: map_compose [symmetric] o_def) iprover
   172 	qed
   173       next
   174 	assume neq: "x \<noteq> i"
   175 	from App have "listall ?R ts" by (iprover dest: listall_conj2)
   176 	with TrueI TrueI uNF uT argsT
   177 	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>
   178 	  NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
   179 	  by (rule norm_list [of "\<lambda>t. t", simplified])
   180 	then obtain ts' where NF: "?ex ts'" ..
   181 	from nat_le_dec show ?thesis
   182 	proof
   183 	  assume "i < x"
   184 	  with NF show ?thesis by simp iprover
   185 	next
   186 	  assume "\<not> (i < x)"
   187 	  with NF neq show ?thesis by (simp add: subst_Var) iprover
   188 	qed
   189       qed
   190     next
   191       case (Abs r e_ T'_ u_ i_)
   192       assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
   193       then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
   194       moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
   195       moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
   196       ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
   197       thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
   198 	by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
   199     }
   200   qed
   201 qed
   202 
   203 
   204 -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
   205 inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   206   where
   207     Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
   208   | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
   209   | 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"
   210 
   211 lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
   212   apply (induct set: rtyping)
   213   apply (erule typing.Var)
   214   apply (erule typing.Abs)
   215   apply (erule typing.App)
   216   apply assumption
   217   done
   218 
   219 
   220 theorem type_NF:
   221   assumes "e \<turnstile>\<^sub>R t : T"
   222   shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using assms
   223 proof induct
   224   case Var
   225   show ?case by (iprover intro: Var_NF)
   226 next
   227   case Abs
   228   thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
   229 next
   230   case (App e s T U t)
   231   from App obtain s' t' where
   232     sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'"
   233     and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
   234   have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u"
   235   proof (rule subst_type_NF)
   236     have "NF (lift t' 0)" using tNF by (rule lift_NF)
   237     hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
   238     hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
   239     thus "NF (Var 0 \<degree> lift t' 0)" by simp
   240     show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
   241     proof (rule typing.App)
   242       show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
   243       	by (rule typing.Var) simp
   244       from tred have "e \<turnstile> t' : T"
   245       	by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
   246       thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"
   247       	by (rule lift_type)
   248     qed
   249     from sred show "e \<turnstile> s' : T \<Rightarrow> U"
   250       by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
   251     show "NF s'" by fact
   252   qed
   253   then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
   254   from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
   255   hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
   256   with unf show ?case by iprover
   257 qed
   258 
   259 
   260 subsection {* Extracting the program *}
   261 
   262 declare NF.induct [ind_realizer]
   263 declare rtranclp.induct [ind_realizer irrelevant]
   264 declare rtyping.induct [ind_realizer]
   265 lemmas [extraction_expand] = conj_assoc listall_cons_eq
   266 
   267 extract type_NF
   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 * :: (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 (the_context ()) (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 (the_context ()) (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 (the_context ()) (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 (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
   513 *}
   514 
   515 end