|
1 (* Title: HOL/Proofs/Lambda/Type.thy |
|
2 Author: Stefan Berghofer |
|
3 Copyright 2000 TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Simply-typed lambda terms *} |
|
7 |
|
8 theory Type imports ListApplication begin |
|
9 |
|
10 |
|
11 subsection {* Environments *} |
|
12 |
|
13 definition |
|
14 shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91) where |
|
15 "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))" |
|
16 |
|
17 notation (xsymbols) |
|
18 shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) |
|
19 |
|
20 notation (HTML output) |
|
21 shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) |
|
22 |
|
23 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T" |
|
24 by (simp add: shift_def) |
|
25 |
|
26 lemma shift_gt [simp]: "j < i \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e j" |
|
27 by (simp add: shift_def) |
|
28 |
|
29 lemma shift_lt [simp]: "i < j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e (j - 1)" |
|
30 by (simp add: shift_def) |
|
31 |
|
32 lemma shift_commute [simp]: "e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>" |
|
33 apply (rule ext) |
|
34 apply (case_tac x) |
|
35 apply simp |
|
36 apply (case_tac nat) |
|
37 apply (simp_all add: shift_def) |
|
38 done |
|
39 |
|
40 |
|
41 subsection {* Types and typing rules *} |
|
42 |
|
43 datatype type = |
|
44 Atom nat |
|
45 | Fun type type (infixr "\<Rightarrow>" 200) |
|
46 |
|
47 inductive typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
|
48 where |
|
49 Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T" |
|
50 | Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)" |
|
51 | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" |
|
52 |
|
53 inductive_cases typing_elims [elim!]: |
|
54 "e \<turnstile> Var i : T" |
|
55 "e \<turnstile> t \<degree> u : T" |
|
56 "e \<turnstile> Abs t : T" |
|
57 |
|
58 primrec |
|
59 typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
|
60 where |
|
61 "typings e [] Ts = (Ts = [])" |
|
62 | "typings e (t # ts) Ts = |
|
63 (case Ts of |
|
64 [] \<Rightarrow> False |
|
65 | T # Ts \<Rightarrow> e \<turnstile> t : T \<and> typings e ts Ts)" |
|
66 |
|
67 abbreviation |
|
68 typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
|
69 ("_ ||- _ : _" [50, 50, 50] 50) where |
|
70 "env ||- ts : Ts == typings env ts Ts" |
|
71 |
|
72 notation (latex) |
|
73 typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50) |
|
74 |
|
75 abbreviation |
|
76 funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200) where |
|
77 "Ts =>> T == foldr Fun Ts T" |
|
78 |
|
79 notation (latex) |
|
80 funs (infixr "\<Rrightarrow>" 200) |
|
81 |
|
82 |
|
83 subsection {* Some examples *} |
|
84 |
|
85 schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T" |
|
86 by force |
|
87 |
|
88 schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T" |
|
89 by force |
|
90 |
|
91 |
|
92 subsection {* Lists of types *} |
|
93 |
|
94 lemma lists_typings: |
|
95 "e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts" |
|
96 apply (induct ts arbitrary: Ts) |
|
97 apply (case_tac Ts) |
|
98 apply simp |
|
99 apply (rule listsp.Nil) |
|
100 apply simp |
|
101 apply (case_tac Ts) |
|
102 apply simp |
|
103 apply simp |
|
104 apply (rule listsp.Cons) |
|
105 apply blast |
|
106 apply blast |
|
107 done |
|
108 |
|
109 lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]" |
|
110 apply (induct ts arbitrary: Ts) |
|
111 apply simp |
|
112 apply (case_tac Ts) |
|
113 apply simp+ |
|
114 done |
|
115 |
|
116 lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] = |
|
117 (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" |
|
118 apply (induct ts arbitrary: Ts) |
|
119 apply (case_tac Ts) |
|
120 apply simp+ |
|
121 apply (case_tac Ts) |
|
122 apply (case_tac "ts @ [t]") |
|
123 apply simp+ |
|
124 done |
|
125 |
|
126 lemma rev_exhaust2 [extraction_expand]: |
|
127 obtains (Nil) "xs = []" | (snoc) ys y where "xs = ys @ [y]" |
|
128 -- {* Cannot use @{text rev_exhaust} from the @{text List} |
|
129 theory, since it is not constructive *} |
|
130 apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> thesis") |
|
131 apply (erule_tac x="rev xs" in allE) |
|
132 apply simp |
|
133 apply (rule allI) |
|
134 apply (rule impI) |
|
135 apply (case_tac ys) |
|
136 apply simp |
|
137 apply simp |
|
138 apply atomize |
|
139 apply (erule allE)+ |
|
140 apply (erule mp, rule conjI) |
|
141 apply (rule refl)+ |
|
142 done |
|
143 |
|
144 lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow> |
|
145 (\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> P" |
|
146 apply (cases Ts rule: rev_exhaust2) |
|
147 apply simp |
|
148 apply (case_tac "ts @ [t]") |
|
149 apply (simp add: types_snoc_eq)+ |
|
150 apply iprover |
|
151 done |
|
152 |
|
153 |
|
154 subsection {* n-ary function types *} |
|
155 |
|
156 lemma list_app_typeD: |
|
157 "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts" |
|
158 apply (induct ts arbitrary: t T) |
|
159 apply simp |
|
160 apply atomize |
|
161 apply simp |
|
162 apply (erule_tac x = "t \<degree> a" in allE) |
|
163 apply (erule_tac x = T in allE) |
|
164 apply (erule impE) |
|
165 apply assumption |
|
166 apply (elim exE conjE) |
|
167 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
168 apply (rule_tac x = "Ta # Ts" in exI) |
|
169 apply simp |
|
170 done |
|
171 |
|
172 lemma list_app_typeE: |
|
173 "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C" |
|
174 by (insert list_app_typeD) fast |
|
175 |
|
176 lemma list_app_typeI: |
|
177 "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T" |
|
178 apply (induct ts arbitrary: t T Ts) |
|
179 apply simp |
|
180 apply atomize |
|
181 apply (case_tac Ts) |
|
182 apply simp |
|
183 apply simp |
|
184 apply (erule_tac x = "t \<degree> a" in allE) |
|
185 apply (erule_tac x = T in allE) |
|
186 apply (erule_tac x = list in allE) |
|
187 apply (erule impE) |
|
188 apply (erule conjE) |
|
189 apply (erule typing.App) |
|
190 apply assumption |
|
191 apply blast |
|
192 done |
|
193 |
|
194 text {* |
|
195 For the specific case where the head of the term is a variable, |
|
196 the following theorems allow to infer the types of the arguments |
|
197 without analyzing the typing derivation. This is crucial |
|
198 for program extraction. |
|
199 *} |
|
200 |
|
201 theorem var_app_type_eq: |
|
202 "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U" |
|
203 apply (induct ts arbitrary: T U rule: rev_induct) |
|
204 apply simp |
|
205 apply (ind_cases "e \<turnstile> Var i : T" for T) |
|
206 apply (ind_cases "e \<turnstile> Var i : T" for T) |
|
207 apply simp |
|
208 apply simp |
|
209 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
210 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
211 apply atomize |
|
212 apply (erule_tac x="Ta \<Rightarrow> T" in allE) |
|
213 apply (erule_tac x="Tb \<Rightarrow> U" in allE) |
|
214 apply (erule impE) |
|
215 apply assumption |
|
216 apply (erule impE) |
|
217 apply assumption |
|
218 apply simp |
|
219 done |
|
220 |
|
221 lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> |
|
222 e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us" |
|
223 apply (induct us arbitrary: ts Ts U) |
|
224 apply simp |
|
225 apply (erule var_app_type_eq) |
|
226 apply assumption |
|
227 apply simp |
|
228 apply atomize |
|
229 apply (case_tac U) |
|
230 apply (rule FalseE) |
|
231 apply simp |
|
232 apply (erule list_app_typeE) |
|
233 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
234 apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
|
235 apply assumption |
|
236 apply simp |
|
237 apply (erule_tac x="ts @ [a]" in allE) |
|
238 apply (erule_tac x="Ts @ [type1]" in allE) |
|
239 apply (erule_tac x="type2" in allE) |
|
240 apply simp |
|
241 apply (erule impE) |
|
242 apply (rule types_snoc) |
|
243 apply assumption |
|
244 apply (erule list_app_typeE) |
|
245 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
246 apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
|
247 apply assumption |
|
248 apply simp |
|
249 apply (erule impE) |
|
250 apply (rule typing.App) |
|
251 apply assumption |
|
252 apply (erule list_app_typeE) |
|
253 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
254 apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
|
255 apply assumption |
|
256 apply simp |
|
257 apply (erule exE) |
|
258 apply (rule_tac x="type1 # Us" in exI) |
|
259 apply simp |
|
260 apply (erule list_app_typeE) |
|
261 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
262 apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
|
263 apply assumption |
|
264 apply simp |
|
265 done |
|
266 |
|
267 lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> |
|
268 (\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P" |
|
269 apply (drule var_app_types [of _ _ "[]", simplified]) |
|
270 apply (iprover intro: typing.Var)+ |
|
271 done |
|
272 |
|
273 lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P" |
|
274 apply (cases T) |
|
275 apply (rule FalseE) |
|
276 apply (erule typing.cases) |
|
277 apply simp_all |
|
278 apply atomize |
|
279 apply (erule_tac x="type1" in allE) |
|
280 apply (erule_tac x="type2" in allE) |
|
281 apply (erule mp) |
|
282 apply (erule typing.cases) |
|
283 apply simp_all |
|
284 done |
|
285 |
|
286 |
|
287 subsection {* Lifting preserves well-typedness *} |
|
288 |
|
289 lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T" |
|
290 by (induct arbitrary: i U set: typing) auto |
|
291 |
|
292 lemma lift_types: |
|
293 "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts" |
|
294 apply (induct ts arbitrary: Ts) |
|
295 apply simp |
|
296 apply (case_tac Ts) |
|
297 apply auto |
|
298 done |
|
299 |
|
300 |
|
301 subsection {* Substitution lemmas *} |
|
302 |
|
303 lemma subst_lemma: |
|
304 "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T" |
|
305 apply (induct arbitrary: e' i U u set: typing) |
|
306 apply (rule_tac x = x and y = i in linorder_cases) |
|
307 apply auto |
|
308 apply blast |
|
309 done |
|
310 |
|
311 lemma substs_lemma: |
|
312 "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow> |
|
313 e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts" |
|
314 apply (induct ts arbitrary: Ts) |
|
315 apply (case_tac Ts) |
|
316 apply simp |
|
317 apply simp |
|
318 apply atomize |
|
319 apply (case_tac Ts) |
|
320 apply simp |
|
321 apply simp |
|
322 apply (erule conjE) |
|
323 apply (erule (1) subst_lemma) |
|
324 apply (rule refl) |
|
325 done |
|
326 |
|
327 |
|
328 subsection {* Subject reduction *} |
|
329 |
|
330 lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T" |
|
331 apply (induct arbitrary: t' set: typing) |
|
332 apply blast |
|
333 apply blast |
|
334 apply atomize |
|
335 apply (ind_cases "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t') |
|
336 apply hypsubst |
|
337 apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U) |
|
338 apply (rule subst_lemma) |
|
339 apply assumption |
|
340 apply assumption |
|
341 apply (rule ext) |
|
342 apply (case_tac x) |
|
343 apply auto |
|
344 done |
|
345 |
|
346 theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T" |
|
347 by (induct set: rtranclp) (iprover intro: subject_reduction)+ |
|
348 |
|
349 |
|
350 subsection {* Alternative induction rule for types *} |
|
351 |
|
352 lemma type_induct [induct type]: |
|
353 assumes |
|
354 "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow> |
|
355 (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)" |
|
356 shows "P T" |
|
357 proof (induct T) |
|
358 case Atom |
|
359 show ?case by (rule assms) simp_all |
|
360 next |
|
361 case Fun |
|
362 show ?case by (rule assms) (insert Fun, simp_all) |
|
363 qed |
|
364 |
|
365 end |