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