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