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