author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 56073  29e308b56d23 
child 58382  2ee61d28c667 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs 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 simplytyped lambda calculus *} 
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset

7 

22512  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  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{MatthesJoachimskiAML}. 
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  22 
and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)" 
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  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  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  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  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  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  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  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  52 
moreover have "NF (f b')" using bNF by (rule f_NF) 
22271  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  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  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  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  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  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  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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

84 
by (rule var_app_typesE) 
22271  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 tabwidth;
wenzelm
parents:
32359
diff
changeset

87 
assume eq: "x = i" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

88 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

89 
proof (cases ts) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

90 
case Nil 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

93 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

109 
then obtain as' where 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

115 
by iprover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

120 
by iprover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

122 
proof (rule MI1) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

124 
proof (rule typing.App) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

127 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

130 
show "NF a'" by fact 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

131 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

133 
by iprover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

135 
by (rule subst_preserves_beta2') 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

137 
by (rule subst_preserves_beta') 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

138 
also note uared 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

142 
proof (rule MI2) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

144 
proof (rule list_app_typeI) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

147 
by (rule substs_lemma) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

149 
by (rule lift_types) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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  151 
by (simp_all add: o_def) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

152 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

154 
by (rule subject_reduction') 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

158 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

160 
and rnf: "NF r" by iprover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

161 
from asred have 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

164 
by (rule subst_preserves_beta') 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

167 
also note rred 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

169 
with rnf Cons eq show ?thesis 
33640  170 
by (simp add: o_def) iprover 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

173 
assume neq: "x \<noteq> i" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

175 
with TrueI TrueI uNF uT argsT 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32359
diff
changeset

179 
then obtain ts' where NF: "?ex ts'" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

180 
from nat_le_dec show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

181 
proof 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

182 
assume "i < x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

183 
with NF show ?thesis by simp iprover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

184 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32359
diff
changeset

185 
assume "\<not> (i < x)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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  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  193 
moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF) 
194 
moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type) 

22271  195 
ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs) 
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 tabwidth;
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  203 
 {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *} 
23750  204 
inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50) 
22271  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  207 
 Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)" 
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  219 
theorem type_NF: 
220 
assumes "e \<turnstile>\<^sub>R t : T" 

23464  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  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  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  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  231 
sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'" 
22271  232 
and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover 
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  235 
have "NF (lift t' 0)" using tNF by (rule lift_NF) 
22271  236 
hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil) 
237 
hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App) 

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 tabwidth;
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 tabwidth;
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 tabwidth;
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  249 
by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps) 
250 
show "NF s'" by fact 

14063
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset

251 
qed 
22271  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  254 
hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans) 
17589  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  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  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  267 

23750  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  270 
apply (erule rtranclpR.induct) 
271 
apply (rule rtranclp.rtrancl_refl) 

272 
apply (erule rtranclp.rtrancl_into_rtrancl) 

22271  273 
apply assumption 
23750  274 
apply (erule rtranclp.induct) 
275 
apply (rule rtranclpR.rtrancl_refl) 

276 
apply (erule rtranclpR.rtrancl_into_rtrancl) 

22271  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  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:extrsubsttypenf} 
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:extrtypenf} 
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:extrsubsttypenf}. 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:extrtypenf}. 
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  334 
instantiation NFT :: default 
335 
begin 

336 

337 
definition "default = Dummy ()" 

338 

339 
instance .. 

340 

341 
end 

342 

343 
instantiation dB :: default 

344 
begin 

345 

346 
definition "default = dB.Var 0" 

347 

348 
instance .. 

349 

350 
end 

351 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37234
diff
changeset

352 
instantiation prod :: (default, default) default 
27982  353 
begin 
354 

355 
definition "default = (default, default)" 

356 

357 
instance .. 

358 

359 
end 

360 

361 
instantiation list :: (type) default 

362 
begin 

363 

364 
definition "default = []" 

365 

366 
instance .. 

367 

368 
end 

369 

370 
instantiation "fun" :: (type, default) default 

371 
begin 

372 

373 
definition "default = (\<lambda>x. default)" 

374 

375 
instance .. 

376 

377 
end 

378 

379 
definition int_of_nat :: "nat \<Rightarrow> int" where 

380 
"int_of_nat = of_nat" 

381 

382 
text {* 

383 
The following functions convert between Isabelle's builtin {\tt term} 

384 
datatype and the generated {\tt dB} datatype. This allows to 

385 
generate example terms using Isabelle's parser and inspect 

386 
normalized terms using Isabelle's pretty printer. 

387 
*} 

388 

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  392 
fun dBtype_of_typ (Type ("fun", [T, U])) = 
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  396 
 _ => error "dBtype_of_typ: variable name") 
397 
 dBtype_of_typ _ = error "dBtype_of_typ: bad type"; 

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  400 
 dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u) 
401 
 dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t) 

402 
 dB_of_term _ = error "dB_of_term: bad term"; 

403 

404 
fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) = 

405 
Abs ("x", T, term_of_dB (T :: Ts) U dBt) 

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  408 
 term_of_dB' Ts (@{code dB.App} (dBt, dBu)) = 
409 
let val t = term_of_dB' Ts dBt 

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  412 
 _ => error "term_of_dB: function type expected" 
413 
end 

414 
 term_of_dB' _ _ = error "term_of_dB: term not in normal form"; 

415 

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  418 
 typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of 
419 
Type ("fun", [T, U]) => @{code App} (e, dB_of_term t, 

420 
dBtype_of_typ T, dBtype_of_typ U, dB_of_term u, 

421 
typing_of_term Ts e t, typing_of_term Ts e u) 

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  424 
let val dBT = dBtype_of_typ T 
425 
in @{code Abs} (e, dBT, dB_of_term t, 

426 
dBtype_of_typ (fastype_of1 (T :: Ts, t)), 

427 
typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t) 

428 
end 

429 
 typing_of_term _ _ _ = error "typing_of_term: bad term"; 

430 

431 
fun dummyf _ = error "dummy"; 

432 

433 
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; 

434 
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1)); 

32010  435 
val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1); 
27982  436 

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)))))"}; 

438 
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2)); 

32010  439 
val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2); 
27982  440 
*} 
441 

14063
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset

442 
end 