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