src/HOL/Proofs/Lambda/WeakNorm.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 56073 29e308b56d23
child 58382 2ee61d28c667
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 37678
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/WeakNorm.thy
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
     3
    Copyright   2003 TU Muenchen
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
     4
*)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
     5
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
     6
header {* Weak normalization for simply-typed lambda calculus *}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
     7
22512
04242efdcece fixed typing bug in generated code
haftmann
parents: 22499
diff changeset
     8
theory WeakNorm
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
     9
imports LambdaType NormalForm "~~/src/HOL/Library/Code_Target_Int"
22512
04242efdcece fixed typing bug in generated code
haftmann
parents: 22499
diff changeset
    10
begin
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    11
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    12
text {*
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    13
Formalization by Stefan Berghofer. Partly based on a paper proof by
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    14
Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    15
*}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    16
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    17
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    18
subsection {* Main theorems *}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    19
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    20
lemma norm_list:
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    21
  assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    22
  and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    23
  and uNF: "NF u" and uT: "e \<turnstile> u : T"
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    24
  shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow>
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    25
    listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    26
      NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow>
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    27
    \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    28
      Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> map f as')"
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    29
  (is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'")
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    30
proof (induct as rule: rev_induct)
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    31
  case (Nil Us)
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    32
  with Var_NF have "?ex Us [] []" by simp
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    33
  thus ?case ..
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    34
next
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    35
  case (snoc b bs Us)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
    36
  have "e\<langle>i:T\<rangle> \<tturnstile> bs  @ [b] : Us" by fact
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    37
  then obtain Vs W where Us: "Us = Vs @ [W]"
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    38
    and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W"
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    39
    by (rule types_snocE)
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    40
  from snoc have "listall ?R bs" by simp
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    41
  with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    42
  then obtain bs' where
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    43
    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'"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    44
    and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    45
  from snoc have "?R b" by simp
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    46
  with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    47
    by iprover
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    48
  then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "NF b'"
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    49
    by iprover
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    50
  from bsNF [of 0] have "listall NF (map f bs')"
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    51
    by (rule App_NF_D)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
    52
  moreover have "NF (f b')" using bNF by (rule f_NF)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    53
  ultimately have "listall NF (map f (bs' @ [b']))"
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    54
    by simp
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    55
  hence "\<And>j. NF (Var j \<degree>\<degree> map f (bs' @ [b']))" by (rule NF.App)
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    56
  moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'"
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    57
    by (rule f_compat)
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    58
  with bsred have
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    59
    "\<And>j. (Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs) \<degree> f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>*
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    60
     (Var j \<degree>\<degree> map f bs') \<degree> f b'" by (rule rtrancl_beta_App)
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    61
  ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    62
  thus ?case ..
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    63
qed
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    64
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    65
lemma subst_type_NF:
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    66
  "\<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'"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    67
  (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    68
proof (induct U)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    69
  fix T t
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    70
  let ?R = "\<lambda>t. \<forall>e T' u i.
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    71
    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')"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    72
  assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    73
  assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    74
  assume "NF t"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    75
  thus "\<And>e T' u i. PROP ?Q t e T' u i T"
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    76
  proof induct
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    77
    fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    78
    {
50241
8b0fdeeefef7 eliminated some improper identifiers;
wenzelm
parents: 45169
diff changeset
    79
      case (App ts x e1 T'1 u1 i1)
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    80
      assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    81
      then obtain Us
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    82
        where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    83
        and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    84
        by (rule var_app_typesE)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
    85
      from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    86
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    87
        assume eq: "x = i"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    88
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    89
        proof (cases ts)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    90
          case Nil
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    91
          with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    92
          with Nil and uNF show ?thesis by simp iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    93
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    94
          case (Cons a as)
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
    95
          with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
56073
29e308b56d23 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents: 51143
diff changeset
    96
            by (cases Us) (rule FalseE, simp)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    97
          from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
    98
            by simp
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
    99
          from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   100
          with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   101
          from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   102
          from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   103
          from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   104
          from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   105
          with lift_preserves_beta' lift_NF uNF uT argsT'
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   106
          have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
18331
eb3a7d3d874b Factored out proof for normalization of applications (norm_list).
berghofe
parents: 18257
diff changeset
   107
            Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   108
            NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   109
          then obtain as' where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   110
            asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   111
              Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   112
            and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   113
          from App and Cons have "?R a" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   114
          with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   115
            by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   116
          then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   117
          from uNF have "NF (lift u 0)" by (rule lift_NF)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   118
          hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   119
          then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   120
            by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   121
          from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   122
          proof (rule MI1)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   123
            have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   124
            proof (rule typing.App)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   125
              from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   126
              show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   127
            qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   128
            with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   129
            from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   130
            show "NF a'" by fact
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   131
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   132
          then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   133
            by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   134
          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]"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   135
            by (rule subst_preserves_beta2')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   136
          also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   137
            by (rule subst_preserves_beta')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   138
          also note uared
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   139
          finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   140
          hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   141
          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"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   142
          proof (rule MI2)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   143
            have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   144
            proof (rule list_app_typeI)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   145
              show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   146
              from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   147
                by (rule substs_lemma)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   148
              hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   149
                by (rule lift_types)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   150
              thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"
33640
0d82107dc07a Remove map_compose, replaced by map_map
hoelzl
parents: 32960
diff changeset
   151
                by (simp_all add: o_def)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   152
            qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   153
            with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   154
              by (rule subject_reduction')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   155
            from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   156
            with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   157
            with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   158
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   159
          then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   160
            and rnf: "NF r" by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   161
          from asred have
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   162
            "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   163
            (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   164
            by (rule subst_preserves_beta')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   165
          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>*
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   166
            (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   167
          also note rred
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   168
          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" .
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   169
          with rnf Cons eq show ?thesis
33640
0d82107dc07a Remove map_compose, replaced by map_map
hoelzl
parents: 32960
diff changeset
   170
            by (simp add: o_def) iprover
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   171
        qed
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   172
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   173
        assume neq: "x \<noteq> i"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   174
        from App have "listall ?R ts" by (iprover dest: listall_conj2)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   175
        with TrueI TrueI uNF uT argsT
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   176
        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>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   177
          NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   178
          by (rule norm_list [of "\<lambda>t. t", simplified])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   179
        then obtain ts' where NF: "?ex ts'" ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   180
        from nat_le_dec show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   181
        proof
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   182
          assume "i < x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   183
          with NF show ?thesis by simp iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   184
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   185
          assume "\<not> (i < x)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   186
          with NF neq show ?thesis by (simp add: subst_Var) iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   187
        qed
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   188
      qed
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   189
    next
50241
8b0fdeeefef7 eliminated some improper identifiers;
wenzelm
parents: 45169
diff changeset
   190
      case (Abs r e1 T'1 u1 i1)
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   191
      assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   192
      then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
   193
      moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
   194
      moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   195
      ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   196
      thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   197
        by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   198
    }
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   199
  qed
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   200
qed
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   201
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   202
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   203
-- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   204
inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   205
  where
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   206
    Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   207
  | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   208
  | 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"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   209
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   210
lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   211
  apply (induct set: rtyping)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   212
  apply (erule typing.Var)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   213
  apply (erule typing.Abs)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   214
  apply (erule typing.App)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   215
  apply assumption
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   216
  done
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   217
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   218
18513
791b53bf4073 tuned proofs;
wenzelm
parents: 18331
diff changeset
   219
theorem type_NF:
791b53bf4073 tuned proofs;
wenzelm
parents: 18331
diff changeset
   220
  assumes "e \<turnstile>\<^sub>R t : T"
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
   221
  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using assms
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   222
proof induct
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   223
  case Var
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 17145
diff changeset
   224
  show ?case by (iprover intro: Var_NF)
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   225
next
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   226
  case Abs
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 17145
diff changeset
   227
  thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   228
next
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   229
  case (App e s T U t)
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   230
  from App obtain s' t' where
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
   231
    sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   232
    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   233
  have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   234
  proof (rule subst_type_NF)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
   235
    have "NF (lift t' 0)" using tNF by (rule lift_NF)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   236
    hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   237
    hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   238
    thus "NF (Var 0 \<degree> lift t' 0)" by simp
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   239
    show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   240
    proof (rule typing.App)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   241
      show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   242
        by (rule typing.Var) simp
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   243
      from tred have "e \<turnstile> t' : T"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   244
        by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   245
      thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32359
diff changeset
   246
        by (rule lift_type)
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   247
    qed
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   248
    from sred show "e \<turnstile> s' : T \<Rightarrow> U"
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
   249
      by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 23399
diff changeset
   250
    show "NF s'" by fact
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   251
  qed
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   252
  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   253
  from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   254
  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 17145
diff changeset
   255
  with unf show ?case by iprover
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   256
qed
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   257
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   258
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   259
subsection {* Extracting the program *}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   260
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   261
declare NF.induct [ind_realizer]
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   262
declare rtranclp.induct [ind_realizer irrelevant]
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   263
declare rtyping.induct [ind_realizer]
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   264
lemmas [extraction_expand] = conj_assoc listall_cons_eq
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   265
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   266
extract type_NF
37234
berghofe
parents: 33640
diff changeset
   267
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   268
lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   269
  apply (rule iffI)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   270
  apply (erule rtranclpR.induct)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   271
  apply (rule rtranclp.rtrancl_refl)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   272
  apply (erule rtranclp.rtrancl_into_rtrancl)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   273
  apply assumption
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   274
  apply (erule rtranclp.induct)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   275
  apply (rule rtranclpR.rtrancl_refl)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   276
  apply (erule rtranclpR.rtrancl_into_rtrancl)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   277
  apply assumption
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   278
  done
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   279
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21546
diff changeset
   280
lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t"
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   281
  apply (erule NFR.induct)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   282
  apply (rule NF.intros)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   283
  apply (simp add: listall_def)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   284
  apply (erule NF.intros)
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   285
  done
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   286
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   287
text_raw {*
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   288
\begin{figure}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   289
\renewcommand{\isastyle}{\scriptsize\it}%
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   290
@{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   291
\renewcommand{\isastyle}{\small\it}%
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   292
\caption{Program extracted from @{text subst_type_NF}}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   293
\label{fig:extr-subst-type-nf}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   294
\end{figure}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   295
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   296
\begin{figure}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   297
\renewcommand{\isastyle}{\scriptsize\it}%
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   298
@{thm [display,margin=100] subst_Var_NF_def}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   299
@{thm [display,margin=100] app_Var_NF_def}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   300
@{thm [display,margin=100] lift_NF_def}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   301
@{thm [display,eta_contract=false,margin=100] type_NF_def}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   302
\renewcommand{\isastyle}{\small\it}%
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   303
\caption{Program extracted from lemmas and main theorem}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   304
\label{fig:extr-type-nf}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   305
\end{figure}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   306
*}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   307
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   308
text {*
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   309
The program corresponding to the proof of the central lemma, which
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   310
performs substitution and normalization, is shown in Figure
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   311
\ref{fig:extr-subst-type-nf}. The correctness
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   312
theorem corresponding to the program @{text "subst_type_NF"} is
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   313
@{thm [display,margin=100] subst_type_NF_correctness
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   314
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   315
where @{text NFR} is the realizability predicate corresponding to
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   316
the datatype @{text NFT}, which is inductively defined by the rules
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   317
\pagebreak
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   318
@{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   319
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   320
The programs corresponding to the main theorem @{text "type_NF"}, as
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   321
well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   322
The correctness statement for the main function @{text "type_NF"} is
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   323
@{thm [display,margin=100] type_NF_correctness
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   324
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   325
where the realizability predicate @{text "rtypingR"} corresponding to the
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   326
computationally relevant version of the typing judgement is inductively
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   327
defined by the rules
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   328
@{thm [display,margin=100] rtypingR.Var [no_vars]
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   329
  rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   330
*}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   331
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   332
subsection {* Generating executable code *}
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   333
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   334
instantiation NFT :: default
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   335
begin
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   336
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   337
definition "default = Dummy ()"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   338
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   339
instance ..
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   340
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   341
end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   342
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   343
instantiation dB :: default
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   344
begin
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   345
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   346
definition "default = dB.Var 0"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   347
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   348
instance ..
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   349
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   350
end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   351
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37234
diff changeset
   352
instantiation prod :: (default, default) default
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   353
begin
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   354
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   355
definition "default = (default, default)"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   356
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   357
instance ..
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   358
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   359
end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   360
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   361
instantiation list :: (type) default
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   362
begin
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   363
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   364
definition "default = []"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   365
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   366
instance ..
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   367
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   368
end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   369
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   370
instantiation "fun" :: (type, default) default
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   371
begin
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   372
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   373
definition "default = (\<lambda>x. default)"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   374
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   375
instance ..
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   376
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   377
end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   378
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   379
definition int_of_nat :: "nat \<Rightarrow> int" where
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   380
  "int_of_nat = of_nat"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   381
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   382
text {*
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   383
  The following functions convert between Isabelle's built-in {\tt term}
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   384
  datatype and the generated {\tt dB} datatype. This allows to
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   385
  generate example terms using Isabelle's parser and inspect
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   386
  normalized terms using Isabelle's pretty printer.
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   387
*}
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   388
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   389
ML {*
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   390
val nat_of_integer = @{code nat} o @{code int_of_integer};
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   391
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   392
fun dBtype_of_typ (Type ("fun", [T, U])) =
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   393
      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 39157
diff changeset
   394
  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   395
        ["'", a] => @{code Atom} (nat_of_integer (ord a - 97))
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   396
      | _ => error "dBtype_of_typ: variable name")
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   397
  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   398
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   399
fun dB_of_term (Bound i) = @{code dB.Var} (nat_of_integer i)
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   400
  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   401
  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   402
  | dB_of_term _ = error "dB_of_term: bad term";
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   403
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   404
fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   405
      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   406
  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   407
and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code integer_of_nat} n)
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   408
  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   409
      let val t = term_of_dB' Ts dBt
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   410
      in case fastype_of1 (Ts, t) of
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   411
          Type ("fun", [T, _]) => t $ term_of_dB Ts T dBu
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   412
        | _ => error "term_of_dB: function type expected"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   413
      end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   414
  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   415
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   416
fun typing_of_term Ts e (Bound i) =
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   417
      @{code Var} (e, nat_of_integer i, dBtype_of_typ (nth Ts i))
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   418
  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   419
        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   420
          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   421
          typing_of_term Ts e t, typing_of_term Ts e u)
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   422
      | _ => error "typing_of_term: function type expected")
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 50336
diff changeset
   423
  | typing_of_term Ts e (Abs (_, T, t)) =
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   424
      let val dBT = dBtype_of_typ T
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   425
      in @{code Abs} (e, dBT, dB_of_term t,
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   426
        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   427
        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   428
      end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   429
  | typing_of_term _ _ _ = error "typing_of_term: bad term";
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   430
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   431
fun dummyf _ = error "dummy";
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   432
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   433
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   434
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 28262
diff changeset
   435
val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   436
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   437
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)))))"};
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   438
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 28262
diff changeset
   439
val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   440
*}
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 27435
diff changeset
   441
14063
e61a310cde02 New proof of weak normalization with program extraction.
berghofe
parents:
diff changeset
   442
end