src/HOL/Lambda/WeakNorm.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28262 aa7ca36d67fd
child 32010 cb1a1c94b4cd
permissions -rw-r--r--
added lemmas
berghofe@14063
     1
(*  Title:      HOL/Lambda/WeakNorm.thy
berghofe@14063
     2
    ID:         $Id$
berghofe@14063
     3
    Author:     Stefan Berghofer
berghofe@14063
     4
    Copyright   2003 TU Muenchen
berghofe@14063
     5
*)
berghofe@14063
     6
berghofe@14063
     7
header {* Weak normalization for simply-typed lambda calculus *}
berghofe@14063
     8
haftmann@22512
     9
theory WeakNorm
haftmann@24994
    10
imports Type NormalForm Code_Integer
haftmann@22512
    11
begin
berghofe@14063
    12
berghofe@14063
    13
text {*
berghofe@14063
    14
Formalization by Stefan Berghofer. Partly based on a paper proof by
berghofe@14063
    15
Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
berghofe@14063
    16
*}
berghofe@14063
    17
berghofe@14063
    18
berghofe@14063
    19
subsection {* Main theorems *}
berghofe@14063
    20
berghofe@18331
    21
lemma norm_list:
berghofe@18331
    22
  assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
berghofe@22271
    23
  and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)"
berghofe@22271
    24
  and uNF: "NF u" and uT: "e \<turnstile> u : T"
berghofe@18331
    25
  shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow>
berghofe@18331
    26
    listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>
berghofe@22271
    27
      NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow>
berghofe@18331
    28
    \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*
berghofe@22271
    29
      Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> map f as')"
berghofe@18331
    30
  (is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'")
berghofe@18331
    31
proof (induct as rule: rev_induct)
berghofe@18331
    32
  case (Nil Us)
berghofe@18331
    33
  with Var_NF have "?ex Us [] []" by simp
berghofe@18331
    34
  thus ?case ..
berghofe@18331
    35
next
berghofe@18331
    36
  case (snoc b bs Us)
wenzelm@23464
    37
  have "e\<langle>i:T\<rangle> \<tturnstile> bs  @ [b] : Us" by fact
berghofe@18331
    38
  then obtain Vs W where Us: "Us = Vs @ [W]"
berghofe@18331
    39
    and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W"
berghofe@18331
    40
    by (rule types_snocE)
berghofe@18331
    41
  from snoc have "listall ?R bs" by simp
berghofe@18331
    42
  with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
berghofe@18331
    43
  then obtain bs' where
berghofe@18331
    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'"
berghofe@22271
    45
    and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
berghofe@18331
    46
  from snoc have "?R b" by simp
berghofe@22271
    47
  with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
berghofe@18331
    48
    by iprover
berghofe@22271
    49
  then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "NF b'"
berghofe@18331
    50
    by iprover
berghofe@22271
    51
  from bsNF [of 0] have "listall NF (map f bs')"
berghofe@18331
    52
    by (rule App_NF_D)
wenzelm@23464
    53
  moreover have "NF (f b')" using bNF by (rule f_NF)
berghofe@22271
    54
  ultimately have "listall NF (map f (bs' @ [b']))"
berghofe@18331
    55
    by simp
berghofe@22271
    56
  hence "\<And>j. NF (Var j \<degree>\<degree> map f (bs' @ [b']))" by (rule NF.App)
berghofe@18331
    57
  moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'"
berghofe@18331
    58
    by (rule f_compat)
berghofe@18331
    59
  with bsred have
berghofe@18331
    60
    "\<And>j. (Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs) \<degree> f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>*
berghofe@18331
    61
     (Var j \<degree>\<degree> map f bs') \<degree> f b'" by (rule rtrancl_beta_App)
berghofe@18331
    62
  ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
berghofe@18331
    63
  thus ?case ..
berghofe@18331
    64
qed
berghofe@18331
    65
berghofe@14063
    66
lemma subst_type_NF:
berghofe@22271
    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'"
berghofe@14063
    68
  (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
berghofe@14063
    69
proof (induct U)
berghofe@14063
    70
  fix T t
berghofe@14063
    71
  let ?R = "\<lambda>t. \<forall>e T' u i.
berghofe@22271
    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')"
berghofe@14063
    73
  assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
berghofe@14063
    74
  assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
berghofe@22271
    75
  assume "NF t"
berghofe@14063
    76
  thus "\<And>e T' u i. PROP ?Q t e T' u i T"
berghofe@14063
    77
  proof induct
berghofe@22271
    78
    fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
berghofe@14063
    79
    {
berghofe@14063
    80
      case (App ts x e_ T'_ u_ i_)
berghofe@18331
    81
      assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
berghofe@18331
    82
      then obtain Us
berghofe@18331
    83
	where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
berghofe@18331
    84
	and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"
berghofe@18331
    85
	by (rule var_app_typesE)
berghofe@22271
    86
      from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
berghofe@14063
    87
      proof
berghofe@14063
    88
	assume eq: "x = i"
berghofe@14063
    89
	show ?thesis
berghofe@14063
    90
	proof (cases ts)
berghofe@14063
    91
	  case Nil
berghofe@14063
    92
	  with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp
nipkow@17589
    93
	  with Nil and uNF show ?thesis by simp iprover
berghofe@14063
    94
	next
berghofe@14063
    95
	  case (Cons a as)
berghofe@18331
    96
          with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
wenzelm@23464
    97
	    by (cases Us) (rule FalseE, simp+, erule that)
berghofe@18331
    98
	  from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
berghofe@14063
    99
	    by simp
berghofe@14063
   100
          from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
berghofe@14063
   101
          with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
berghofe@18331
   102
	  from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp
berghofe@18331
   103
	  from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp
berghofe@14063
   104
	  from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
nipkow@17589
   105
	  from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
berghofe@18331
   106
	  with lift_preserves_beta' lift_NF uNF uT argsT'
berghofe@18331
   107
	  have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
berghofe@18331
   108
            Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>
berghofe@22271
   109
	    NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list)
berghofe@14063
   110
	  then obtain as' where
berghofe@14063
   111
	    asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
berghofe@14063
   112
	      Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
berghofe@22271
   113
	    and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover
berghofe@14063
   114
	  from App and Cons have "?R a" by simp
berghofe@22271
   115
	  with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'"
nipkow@17589
   116
	    by iprover
berghofe@22271
   117
	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover
berghofe@22271
   118
	  from uNF have "NF (lift u 0)" by (rule lift_NF)
berghofe@22271
   119
	  hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF)
berghofe@22271
   120
	  then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'"
nipkow@17589
   121
	    by iprover
berghofe@22271
   122
	  from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua"
berghofe@14063
   123
	  proof (rule MI1)
berghofe@14063
   124
	    have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
berghofe@14063
   125
	    proof (rule typing.App)
berghofe@14063
   126
	      from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type)
berghofe@14063
   127
	      show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp
berghofe@14063
   128
	    qed
berghofe@14063
   129
	    with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')
berghofe@14063
   130
	    from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
wenzelm@23464
   131
	    show "NF a'" by fact
berghofe@14063
   132
	  qed
berghofe@22271
   133
	  then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua"
nipkow@17589
   134
	    by iprover
berghofe@14063
   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]"
berghofe@14063
   136
	    by (rule subst_preserves_beta2')
berghofe@14063
   137
	  also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"
berghofe@14063
   138
	    by (rule subst_preserves_beta')
berghofe@14063
   139
	  also note uared
berghofe@14063
   140
	  finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .
berghofe@14063
   141
	  hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp
wenzelm@23464
   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"
berghofe@14063
   143
	  proof (rule MI2)
berghofe@14063
   144
	    have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'"
berghofe@14063
   145
	    proof (rule list_app_typeI)
berghofe@14063
   146
	      show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp
berghofe@18331
   147
	      from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
berghofe@14063
   148
		by (rule substs_lemma)
berghofe@14063
   149
	      hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"
berghofe@14063
   150
		by (rule lift_types)
berghofe@14063
   151
	      thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"
berghofe@14063
   152
		by (simp_all add: map_compose [symmetric] o_def)
berghofe@14063
   153
	    qed
berghofe@14063
   154
	    with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"
berghofe@14063
   155
	      by (rule subject_reduction')
berghofe@14063
   156
	    from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
berghofe@14063
   157
	    with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App)
berghofe@14063
   158
	    with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
berghofe@14063
   159
	  qed
berghofe@14063
   160
	  then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
berghofe@22271
   161
	    and rnf: "NF r" by iprover
berghofe@14063
   162
	  from asred have
berghofe@14063
   163
	    "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
berghofe@14063
   164
	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
berghofe@14063
   165
	    by (rule subst_preserves_beta')
berghofe@14063
   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>*
berghofe@14063
   167
	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2')
berghofe@14063
   168
	  also note rred
berghofe@14063
   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" .
berghofe@14063
   170
	  with rnf Cons eq show ?thesis
nipkow@17589
   171
	    by (simp add: map_compose [symmetric] o_def) iprover
berghofe@14063
   172
	qed
berghofe@14063
   173
      next
berghofe@14063
   174
	assume neq: "x \<noteq> i"
berghofe@18331
   175
	from App have "listall ?R ts" by (iprover dest: listall_conj2)
berghofe@18331
   176
	with TrueI TrueI uNF uT argsT
berghofe@18331
   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>
berghofe@22271
   178
	  NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
berghofe@18331
   179
	  by (rule norm_list [of "\<lambda>t. t", simplified])
berghofe@18331
   180
	then obtain ts' where NF: "?ex ts'" ..
berghofe@18331
   181
	from nat_le_dec show ?thesis
berghofe@18331
   182
	proof
berghofe@18331
   183
	  assume "i < x"
berghofe@18331
   184
	  with NF show ?thesis by simp iprover
berghofe@18331
   185
	next
berghofe@18331
   186
	  assume "\<not> (i < x)"
berghofe@18331
   187
	  with NF neq show ?thesis by (simp add: subst_Var) iprover
berghofe@14063
   188
	qed
berghofe@14063
   189
      qed
berghofe@14063
   190
    next
berghofe@14063
   191
      case (Abs r e_ T'_ u_ i_)
berghofe@14063
   192
      assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
berghofe@14063
   193
      then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
wenzelm@23464
   194
      moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
wenzelm@23464
   195
      moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
berghofe@22271
   196
      ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
berghofe@22271
   197
      thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
nipkow@17589
   198
	by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
berghofe@14063
   199
    }
berghofe@14063
   200
  qed
berghofe@14063
   201
qed
berghofe@14063
   202
berghofe@14063
   203
berghofe@22271
   204
-- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
berghofe@23750
   205
inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
berghofe@22271
   206
  where
berghofe@14063
   207
    Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
berghofe@22271
   208
  | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
berghofe@22271
   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"
berghofe@14063
   210
berghofe@14063
   211
lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
berghofe@14063
   212
  apply (induct set: rtyping)
berghofe@14063
   213
  apply (erule typing.Var)
berghofe@14063
   214
  apply (erule typing.Abs)
berghofe@14063
   215
  apply (erule typing.App)
berghofe@14063
   216
  apply assumption
berghofe@14063
   217
  done
berghofe@14063
   218
berghofe@14063
   219
wenzelm@18513
   220
theorem type_NF:
wenzelm@18513
   221
  assumes "e \<turnstile>\<^sub>R t : T"
wenzelm@23464
   222
  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using assms
berghofe@14063
   223
proof induct
berghofe@14063
   224
  case Var
nipkow@17589
   225
  show ?case by (iprover intro: Var_NF)
berghofe@14063
   226
next
berghofe@14063
   227
  case Abs
nipkow@17589
   228
  thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
berghofe@14063
   229
next
berghofe@22271
   230
  case (App e s T U t)
berghofe@14063
   231
  from App obtain s' t' where
wenzelm@23464
   232
    sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'"
berghofe@22271
   233
    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
berghofe@22271
   234
  have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u"
berghofe@14063
   235
  proof (rule subst_type_NF)
wenzelm@23464
   236
    have "NF (lift t' 0)" using tNF by (rule lift_NF)
berghofe@22271
   237
    hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
berghofe@22271
   238
    hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
berghofe@22271
   239
    thus "NF (Var 0 \<degree> lift t' 0)" by simp
berghofe@14063
   240
    show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
berghofe@14063
   241
    proof (rule typing.App)
berghofe@14063
   242
      show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
berghofe@14063
   243
      	by (rule typing.Var) simp
berghofe@14063
   244
      from tred have "e \<turnstile> t' : T"
wenzelm@23464
   245
      	by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
berghofe@14063
   246
      thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"
berghofe@14063
   247
      	by (rule lift_type)
berghofe@14063
   248
    qed
berghofe@14063
   249
    from sred show "e \<turnstile> s' : T \<Rightarrow> U"
wenzelm@23464
   250
      by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
wenzelm@23464
   251
    show "NF s'" by fact
berghofe@14063
   252
  qed
berghofe@22271
   253
  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
berghofe@14063
   254
  from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
berghofe@23750
   255
  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
nipkow@17589
   256
  with unf show ?case by iprover
berghofe@14063
   257
qed
berghofe@14063
   258
berghofe@14063
   259
berghofe@14063
   260
subsection {* Extracting the program *}
berghofe@14063
   261
berghofe@14063
   262
declare NF.induct [ind_realizer]
berghofe@23750
   263
declare rtranclp.induct [ind_realizer irrelevant]
berghofe@14063
   264
declare rtyping.induct [ind_realizer]
berghofe@22271
   265
lemmas [extraction_expand] = conj_assoc listall_cons_eq
berghofe@14063
   266
berghofe@14063
   267
extract type_NF
berghofe@23750
   268
lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
berghofe@14063
   269
  apply (rule iffI)
berghofe@23750
   270
  apply (erule rtranclpR.induct)
berghofe@23750
   271
  apply (rule rtranclp.rtrancl_refl)
berghofe@23750
   272
  apply (erule rtranclp.rtrancl_into_rtrancl)
berghofe@22271
   273
  apply assumption
berghofe@23750
   274
  apply (erule rtranclp.induct)
berghofe@23750
   275
  apply (rule rtranclpR.rtrancl_refl)
berghofe@23750
   276
  apply (erule rtranclpR.rtrancl_into_rtrancl)
berghofe@22271
   277
  apply assumption
berghofe@14063
   278
  done
berghofe@14063
   279
berghofe@22271
   280
lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t"
berghofe@14063
   281
  apply (erule NFR.induct)
berghofe@14063
   282
  apply (rule NF.intros)
berghofe@14063
   283
  apply (simp add: listall_def)
berghofe@14063
   284
  apply (erule NF.intros)
berghofe@14063
   285
  done
berghofe@14063
   286
berghofe@14063
   287
text_raw {*
berghofe@14063
   288
\begin{figure}
berghofe@14063
   289
\renewcommand{\isastyle}{\scriptsize\it}%
berghofe@14063
   290
@{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
berghofe@14063
   291
\renewcommand{\isastyle}{\small\it}%
berghofe@14063
   292
\caption{Program extracted from @{text subst_type_NF}}
berghofe@14063
   293
\label{fig:extr-subst-type-nf}
berghofe@14063
   294
\end{figure}
berghofe@14063
   295
berghofe@14063
   296
\begin{figure}
berghofe@14063
   297
\renewcommand{\isastyle}{\scriptsize\it}%
berghofe@14063
   298
@{thm [display,margin=100] subst_Var_NF_def}
berghofe@14063
   299
@{thm [display,margin=100] app_Var_NF_def}
berghofe@14063
   300
@{thm [display,margin=100] lift_NF_def}
berghofe@14063
   301
@{thm [display,eta_contract=false,margin=100] type_NF_def}
berghofe@14063
   302
\renewcommand{\isastyle}{\small\it}%
berghofe@14063
   303
\caption{Program extracted from lemmas and main theorem}
berghofe@14063
   304
\label{fig:extr-type-nf}
berghofe@14063
   305
\end{figure}
berghofe@14063
   306
*}
berghofe@14063
   307
berghofe@14063
   308
text {*
berghofe@14063
   309
The program corresponding to the proof of the central lemma, which
berghofe@14063
   310
performs substitution and normalization, is shown in Figure
berghofe@14063
   311
\ref{fig:extr-subst-type-nf}. The correctness
berghofe@14063
   312
theorem corresponding to the program @{text "subst_type_NF"} is
berghofe@14063
   313
@{thm [display,margin=100] subst_type_NF_correctness
berghofe@14063
   314
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
berghofe@14063
   315
where @{text NFR} is the realizability predicate corresponding to
berghofe@14063
   316
the datatype @{text NFT}, which is inductively defined by the rules
berghofe@14063
   317
\pagebreak
berghofe@14063
   318
@{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}
berghofe@14063
   319
berghofe@14063
   320
The programs corresponding to the main theorem @{text "type_NF"}, as
berghofe@14063
   321
well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
berghofe@14063
   322
The correctness statement for the main function @{text "type_NF"} is
berghofe@14063
   323
@{thm [display,margin=100] type_NF_correctness
berghofe@14063
   324
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
berghofe@14063
   325
where the realizability predicate @{text "rtypingR"} corresponding to the
berghofe@14063
   326
computationally relevant version of the typing judgement is inductively
berghofe@14063
   327
defined by the rules
berghofe@14063
   328
@{thm [display,margin=100] rtypingR.Var [no_vars]
berghofe@14063
   329
  rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
berghofe@14063
   330
*}
berghofe@14063
   331
berghofe@14063
   332
subsection {* Generating executable code *}
berghofe@14063
   333
haftmann@27982
   334
instantiation NFT :: default
haftmann@27982
   335
begin
haftmann@27982
   336
haftmann@27982
   337
definition "default = Dummy ()"
haftmann@27982
   338
haftmann@27982
   339
instance ..
haftmann@27982
   340
haftmann@27982
   341
end
haftmann@27982
   342
haftmann@27982
   343
instantiation dB :: default
haftmann@27982
   344
begin
haftmann@27982
   345
haftmann@27982
   346
definition "default = dB.Var 0"
haftmann@27982
   347
haftmann@27982
   348
instance ..
haftmann@27982
   349
haftmann@27982
   350
end
haftmann@27982
   351
haftmann@27982
   352
instantiation * :: (default, default) default
haftmann@27982
   353
begin
haftmann@27982
   354
haftmann@27982
   355
definition "default = (default, default)"
haftmann@27982
   356
haftmann@27982
   357
instance ..
haftmann@27982
   358
haftmann@27982
   359
end
haftmann@27982
   360
haftmann@27982
   361
instantiation list :: (type) default
haftmann@27982
   362
begin
haftmann@27982
   363
haftmann@27982
   364
definition "default = []"
haftmann@27982
   365
haftmann@27982
   366
instance ..
haftmann@27982
   367
haftmann@27982
   368
end
haftmann@27982
   369
haftmann@27982
   370
instantiation "fun" :: (type, default) default
haftmann@27982
   371
begin
haftmann@27982
   372
haftmann@27982
   373
definition "default = (\<lambda>x. default)"
haftmann@27982
   374
haftmann@27982
   375
instance ..
haftmann@27982
   376
haftmann@27982
   377
end
haftmann@27982
   378
haftmann@27982
   379
definition int_of_nat :: "nat \<Rightarrow> int" where
haftmann@27982
   380
  "int_of_nat = of_nat"
haftmann@27982
   381
haftmann@27982
   382
text {*
haftmann@27982
   383
  The following functions convert between Isabelle's built-in {\tt term}
haftmann@27982
   384
  datatype and the generated {\tt dB} datatype. This allows to
haftmann@27982
   385
  generate example terms using Isabelle's parser and inspect
haftmann@27982
   386
  normalized terms using Isabelle's pretty printer.
haftmann@27982
   387
*}
haftmann@27982
   388
haftmann@27982
   389
ML {*
haftmann@27982
   390
fun dBtype_of_typ (Type ("fun", [T, U])) =
haftmann@27982
   391
      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
haftmann@27982
   392
  | dBtype_of_typ (TFree (s, _)) = (case explode s of
haftmann@27982
   393
        ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
haftmann@27982
   394
      | _ => error "dBtype_of_typ: variable name")
haftmann@27982
   395
  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
haftmann@27982
   396
haftmann@27982
   397
fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i)
haftmann@27982
   398
  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
haftmann@27982
   399
  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
haftmann@27982
   400
  | dB_of_term _ = error "dB_of_term: bad term";
haftmann@27982
   401
haftmann@27982
   402
fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
haftmann@27982
   403
      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
haftmann@27982
   404
  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
haftmann@27982
   405
and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n)
haftmann@27982
   406
  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
haftmann@27982
   407
      let val t = term_of_dB' Ts dBt
haftmann@27982
   408
      in case fastype_of1 (Ts, t) of
haftmann@27982
   409
          Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
haftmann@27982
   410
        | _ => error "term_of_dB: function type expected"
haftmann@27982
   411
      end
haftmann@27982
   412
  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
haftmann@27982
   413
haftmann@27982
   414
fun typing_of_term Ts e (Bound i) =
haftmann@27982
   415
      @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i))
haftmann@27982
   416
  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
haftmann@27982
   417
        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
haftmann@27982
   418
          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
haftmann@27982
   419
          typing_of_term Ts e t, typing_of_term Ts e u)
haftmann@27982
   420
      | _ => error "typing_of_term: function type expected")
haftmann@27982
   421
  | typing_of_term Ts e (Abs (s, T, t)) =
haftmann@27982
   422
      let val dBT = dBtype_of_typ T
haftmann@27982
   423
      in @{code Abs} (e, dBT, dB_of_term t,
haftmann@27982
   424
        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
haftmann@27982
   425
        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
haftmann@27982
   426
      end
haftmann@27982
   427
  | typing_of_term _ _ _ = error "typing_of_term: bad term";
haftmann@27982
   428
haftmann@27982
   429
fun dummyf _ = error "dummy";
haftmann@27982
   430
haftmann@27982
   431
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
haftmann@27982
   432
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
wenzelm@28262
   433
val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
haftmann@27982
   434
haftmann@27982
   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)))))"};
haftmann@27982
   436
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
wenzelm@28262
   437
val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
haftmann@27982
   438
*}
haftmann@27982
   439
haftmann@27982
   440
text {*
haftmann@27982
   441
The same story again for the SML code generator.
haftmann@27982
   442
*}
haftmann@27982
   443
berghofe@14063
   444
consts_code
haftmann@27982
   445
  "default" ("(error \"default\")")
haftmann@27982
   446
  "default :: 'a \<Rightarrow> 'b::default" ("(fn '_ => error \"default\")")
berghofe@14063
   447
berghofe@17145
   448
code_module Norm
berghofe@17145
   449
contains
berghofe@14063
   450
  test = "type_NF"
berghofe@14063
   451
berghofe@14063
   452
ML {*
haftmann@20713
   453
fun nat_of_int 0 = Norm.zero
berghofe@17145
   454
  | nat_of_int n = Norm.Suc (nat_of_int (n-1));
berghofe@14063
   455
haftmann@20713
   456
fun int_of_nat Norm.zero = 0
berghofe@17145
   457
  | int_of_nat (Norm.Suc n) = 1 + int_of_nat n;
berghofe@14063
   458
berghofe@14063
   459
fun dBtype_of_typ (Type ("fun", [T, U])) =
berghofe@17145
   460
      Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
berghofe@14063
   461
  | dBtype_of_typ (TFree (s, _)) = (case explode s of
berghofe@17145
   462
        ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
berghofe@14063
   463
      | _ => error "dBtype_of_typ: variable name")
berghofe@14063
   464
  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
berghofe@14063
   465
berghofe@17145
   466
fun dB_of_term (Bound i) = Norm.dB_Var (nat_of_int i)
berghofe@17145
   467
  | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u)
berghofe@17145
   468
  | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)
berghofe@14063
   469
  | dB_of_term _ = error "dB_of_term: bad term";
berghofe@14063
   470
berghofe@17145
   471
fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =
berghofe@14063
   472
      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
berghofe@14063
   473
  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
berghofe@17145
   474
and term_of_dB' Ts (Norm.dB_Var n) = Bound (int_of_nat n)
berghofe@17145
   475
  | term_of_dB' Ts (Norm.App (dBt, dBu)) =
berghofe@14063
   476
      let val t = term_of_dB' Ts dBt
berghofe@14063
   477
      in case fastype_of1 (Ts, t) of
berghofe@14063
   478
          Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
berghofe@14063
   479
        | _ => error "term_of_dB: function type expected"
berghofe@14063
   480
      end
berghofe@14063
   481
  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
berghofe@14063
   482
berghofe@14063
   483
fun typing_of_term Ts e (Bound i) =
berghofe@17145
   484
      Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i)))
berghofe@14063
   485
  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
berghofe@17145
   486
        Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t,
berghofe@14063
   487
          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
berghofe@14063
   488
          typing_of_term Ts e t, typing_of_term Ts e u)
berghofe@14063
   489
      | _ => error "typing_of_term: function type expected")
berghofe@14063
   490
  | typing_of_term Ts e (Abs (s, T, t)) =
berghofe@14063
   491
      let val dBT = dBtype_of_typ T
berghofe@17145
   492
      in Norm.rtypingT_Abs (e, dBT, dB_of_term t,
berghofe@14063
   493
        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
haftmann@20713
   494
        typing_of_term (T :: Ts) (Norm.shift e Norm.zero dBT) t)
berghofe@14063
   495
      end
berghofe@14063
   496
  | typing_of_term _ _ _ = error "typing_of_term: bad term";
berghofe@14063
   497
berghofe@14063
   498
fun dummyf _ = error "dummy";
berghofe@14063
   499
*}
berghofe@14063
   500
berghofe@14063
   501
text {*
berghofe@14063
   502
We now try out the extracted program @{text "type_NF"} on some example terms.
berghofe@14063
   503
*}
berghofe@14063
   504
berghofe@14063
   505
ML {*
haftmann@22512
   506
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
berghofe@17145
   507
val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
wenzelm@28262
   508
val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
berghofe@14063
   509
haftmann@22512
   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)))))"};
berghofe@17145
   511
val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
wenzelm@28262
   512
val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
berghofe@14063
   513
*}
berghofe@14063
   514
berghofe@14063
   515
end