src/HOL/Lambda/WeakNorm.thy
author wenzelm
Sun Apr 09 18:51:13 2006 +0200 (2006-04-09)
changeset 19380 b808efaa5828
parent 19363 667b5ea637dd
child 19656 09be06943252
permissions -rw-r--r--
tuned syntax/abbreviations;
     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 abbreviation (xsymbols)
   369   rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   370   "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
   371 
   372 inductive rtyping
   373   intros
   374     Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
   375     Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
   376     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"
   377 
   378 lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
   379   apply (induct set: rtyping)
   380   apply (erule typing.Var)
   381   apply (erule typing.Abs)
   382   apply (erule typing.App)
   383   apply assumption
   384   done
   385 
   386 
   387 theorem type_NF:
   388   assumes "e \<turnstile>\<^sub>R t : T"
   389   shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems
   390 proof induct
   391   case Var
   392   show ?case by (iprover intro: Var_NF)
   393 next
   394   case Abs
   395   thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
   396 next
   397   case (App T U e s t)
   398   from App obtain s' t' where
   399     sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF"
   400     and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by iprover
   401   have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF"
   402   proof (rule subst_type_NF)
   403     have "lift t' 0 \<in> NF" by (rule lift_NF)
   404     hence "listall (\<lambda>t. t \<in> NF) [lift t' 0]" by (rule listall_cons) (rule listall_nil)
   405     hence "Var 0 \<degree>\<degree> [lift t' 0] \<in> NF" by (rule NF.App)
   406     thus "Var 0 \<degree> lift t' 0 \<in> NF" by simp
   407     show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
   408     proof (rule typing.App)
   409       show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
   410       	by (rule typing.Var) simp
   411       from tred have "e \<turnstile> t' : T"
   412       	by (rule subject_reduction') (rule rtyping_imp_typing)
   413       thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"
   414       	by (rule lift_type)
   415     qed
   416     from sred show "e \<turnstile> s' : T \<Rightarrow> U"
   417       by (rule subject_reduction') (rule rtyping_imp_typing)
   418   qed
   419   then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp iprover
   420   from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
   421   hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans)
   422   with unf show ?case by iprover
   423 qed
   424 
   425 
   426 subsection {* Extracting the program *}
   427 
   428 declare NF.induct [ind_realizer]
   429 declare rtrancl.induct [ind_realizer irrelevant]
   430 declare rtyping.induct [ind_realizer]
   431 lemmas [extraction_expand] = trans_def conj_assoc listall_cons_eq
   432 
   433 extract type_NF
   434 
   435 lemma rtranclR_rtrancl_eq: "((a, b) \<in> rtranclR r) = ((a, b) \<in> rtrancl (Collect r))"
   436   apply (rule iffI)
   437   apply (erule rtranclR.induct)
   438   apply (rule rtrancl_refl)
   439   apply (erule rtrancl_into_rtrancl)
   440   apply (erule CollectI)
   441   apply (erule rtrancl.induct)
   442   apply (rule rtranclR.rtrancl_refl)
   443   apply (erule rtranclR.rtrancl_into_rtrancl)
   444   apply (erule CollectD)
   445   done
   446 
   447 lemma NFR_imp_NF: "(nf, t) \<in> NFR \<Longrightarrow> t \<in> NF"
   448   apply (erule NFR.induct)
   449   apply (rule NF.intros)
   450   apply (simp add: listall_def)
   451   apply (erule NF.intros)
   452   done
   453 
   454 text_raw {*
   455 \begin{figure}
   456 \renewcommand{\isastyle}{\scriptsize\it}%
   457 @{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
   458 \renewcommand{\isastyle}{\small\it}%
   459 \caption{Program extracted from @{text subst_type_NF}}
   460 \label{fig:extr-subst-type-nf}
   461 \end{figure}
   462 
   463 \begin{figure}
   464 \renewcommand{\isastyle}{\scriptsize\it}%
   465 @{thm [display,margin=100] subst_Var_NF_def}
   466 @{thm [display,margin=100] app_Var_NF_def}
   467 @{thm [display,margin=100] lift_NF_def}
   468 @{thm [display,eta_contract=false,margin=100] type_NF_def}
   469 \renewcommand{\isastyle}{\small\it}%
   470 \caption{Program extracted from lemmas and main theorem}
   471 \label{fig:extr-type-nf}
   472 \end{figure}
   473 *}
   474 
   475 text {*
   476 The program corresponding to the proof of the central lemma, which
   477 performs substitution and normalization, is shown in Figure
   478 \ref{fig:extr-subst-type-nf}. The correctness
   479 theorem corresponding to the program @{text "subst_type_NF"} is
   480 @{thm [display,margin=100] subst_type_NF_correctness
   481   [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
   482 where @{text NFR} is the realizability predicate corresponding to
   483 the datatype @{text NFT}, which is inductively defined by the rules
   484 \pagebreak
   485 @{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}
   486 
   487 The programs corresponding to the main theorem @{text "type_NF"}, as
   488 well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
   489 The correctness statement for the main function @{text "type_NF"} is
   490 @{thm [display,margin=100] type_NF_correctness
   491   [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
   492 where the realizability predicate @{text "rtypingR"} corresponding to the
   493 computationally relevant version of the typing judgement is inductively
   494 defined by the rules
   495 @{thm [display,margin=100] rtypingR.Var [no_vars]
   496   rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
   497 *}
   498 
   499 subsection {* Generating executable code *}
   500 
   501 consts_code
   502   arbitrary :: "'a"       ("(error \"arbitrary\")")
   503   arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
   504 
   505 code_module Norm
   506 contains
   507   test = "type_NF"
   508 
   509 text {*
   510 The following functions convert between Isabelle's built-in {\tt term}
   511 datatype and the generated {\tt dB} datatype. This allows to
   512 generate example terms using Isabelle's parser and inspect
   513 normalized terms using Isabelle's pretty printer.
   514 *}
   515 
   516 ML {*
   517 fun nat_of_int 0 = Norm.id_0
   518   | nat_of_int n = Norm.Suc (nat_of_int (n-1));
   519 
   520 fun int_of_nat Norm.id_0 = 0
   521   | int_of_nat (Norm.Suc n) = 1 + int_of_nat n;
   522 
   523 fun dBtype_of_typ (Type ("fun", [T, U])) =
   524       Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
   525   | dBtype_of_typ (TFree (s, _)) = (case explode s of
   526         ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
   527       | _ => error "dBtype_of_typ: variable name")
   528   | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
   529 
   530 fun dB_of_term (Bound i) = Norm.dB_Var (nat_of_int i)
   531   | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u)
   532   | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)
   533   | dB_of_term _ = error "dB_of_term: bad term";
   534 
   535 fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =
   536       Abs ("x", T, term_of_dB (T :: Ts) U dBt)
   537   | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
   538 and term_of_dB' Ts (Norm.dB_Var n) = Bound (int_of_nat n)
   539   | term_of_dB' Ts (Norm.App (dBt, dBu)) =
   540       let val t = term_of_dB' Ts dBt
   541       in case fastype_of1 (Ts, t) of
   542           Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
   543         | _ => error "term_of_dB: function type expected"
   544       end
   545   | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
   546 
   547 fun typing_of_term Ts e (Bound i) =
   548       Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i)))
   549   | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
   550         Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t,
   551           dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
   552           typing_of_term Ts e t, typing_of_term Ts e u)
   553       | _ => error "typing_of_term: function type expected")
   554   | typing_of_term Ts e (Abs (s, T, t)) =
   555       let val dBT = dBtype_of_typ T
   556       in Norm.rtypingT_Abs (e, dBT, dB_of_term t,
   557         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
   558         typing_of_term (T :: Ts) (Norm.shift e Norm.id_0 dBT) t)
   559       end
   560   | typing_of_term _ _ _ = error "typing_of_term: bad term";
   561 
   562 fun dummyf _ = error "dummy";
   563 *}
   564 
   565 text {*
   566 We now try out the extracted program @{text "type_NF"} on some example terms.
   567 *}
   568 
   569 ML {*
   570 val sg = sign_of (the_context());
   571 fun rd s = read_cterm sg (s, TypeInfer.logicT);
   572 
   573 val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";
   574 val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
   575 val ct1' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct1)) dB1);
   576 
   577 val ct2 = rd
   578   "%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)))))";
   579 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
   580 val ct2' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct2)) dB2);
   581 *}
   582 
   583 end