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