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