equal
deleted
inserted
replaced
92 |
92 |
93 |
93 |
94 subsection {* Lists of types *} |
94 subsection {* Lists of types *} |
95 |
95 |
96 lemma lists_typings: |
96 lemma lists_typings: |
97 "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}" |
97 "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}" |
98 apply (induct ts) |
98 apply (induct ts fixing: Ts) |
99 apply (case_tac Ts) |
99 apply (case_tac Ts) |
100 apply simp |
100 apply simp |
101 apply (rule lists.Nil) |
101 apply (rule lists.Nil) |
102 apply simp |
102 apply simp |
103 apply (case_tac Ts) |
103 apply (case_tac Ts) |
106 apply (rule lists.Cons) |
106 apply (rule lists.Cons) |
107 apply blast |
107 apply blast |
108 apply blast |
108 apply blast |
109 done |
109 done |
110 |
110 |
111 lemma types_snoc: "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]" |
111 lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]" |
112 apply (induct ts) |
112 apply (induct ts fixing: Ts) |
113 apply simp |
113 apply simp |
114 apply (case_tac Ts) |
114 apply (case_tac Ts) |
115 apply simp+ |
115 apply simp+ |
116 done |
116 done |
117 |
117 |
118 lemma types_snoc_eq: "\<And>Ts. e \<tturnstile> ts @ [t] : Ts @ [T] = |
118 lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] = |
119 (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" |
119 (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" |
120 apply (induct ts) |
120 apply (induct ts fixing: Ts) |
121 apply (case_tac Ts) |
121 apply (case_tac Ts) |
122 apply simp+ |
122 apply simp+ |
123 apply (case_tac Ts) |
123 apply (case_tac Ts) |
124 apply (case_tac "ts @ [t]") |
124 apply (case_tac "ts @ [t]") |
125 apply simp+ |
125 apply simp+ |
154 |
154 |
155 |
155 |
156 subsection {* n-ary function types *} |
156 subsection {* n-ary function types *} |
157 |
157 |
158 lemma list_app_typeD: |
158 lemma list_app_typeD: |
159 "\<And>t T. e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts" |
159 "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts" |
160 apply (induct ts) |
160 apply (induct ts fixing: t T) |
161 apply simp |
161 apply simp |
162 apply atomize |
162 apply atomize |
163 apply simp |
163 apply simp |
164 apply (erule_tac x = "t \<degree> a" in allE) |
164 apply (erule_tac x = "t \<degree> a" in allE) |
165 apply (erule_tac x = T in allE) |
165 apply (erule_tac x = T in allE) |
174 lemma list_app_typeE: |
174 lemma list_app_typeE: |
175 "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" |
175 "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" |
176 by (insert list_app_typeD) fast |
176 by (insert list_app_typeD) fast |
177 |
177 |
178 lemma list_app_typeI: |
178 lemma list_app_typeI: |
179 "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T" |
179 "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T" |
180 apply (induct ts) |
180 apply (induct ts fixing: t T Ts) |
181 apply simp |
181 apply simp |
182 apply atomize |
182 apply atomize |
183 apply (case_tac Ts) |
183 apply (case_tac Ts) |
184 apply simp |
184 apply simp |
185 apply simp |
185 apply simp |
199 without analyzing the typing derivation. This is crucial |
199 without analyzing the typing derivation. This is crucial |
200 for program extraction. |
200 for program extraction. |
201 *} |
201 *} |
202 |
202 |
203 theorem var_app_type_eq: |
203 theorem var_app_type_eq: |
204 "\<And>T U. e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U" |
204 "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U" |
205 apply (induct ts rule: rev_induct) |
205 apply (induct ts fixing: T U rule: rev_induct) |
206 apply simp |
206 apply simp |
207 apply (ind_cases "e \<turnstile> Var i : T") |
207 apply (ind_cases "e \<turnstile> Var i : T") |
208 apply (ind_cases "e \<turnstile> Var i : T") |
208 apply (ind_cases "e \<turnstile> Var i : T") |
209 apply simp |
209 apply simp |
210 apply simp |
210 apply simp |
218 apply (erule impE) |
218 apply (erule impE) |
219 apply assumption |
219 apply assumption |
220 apply simp |
220 apply simp |
221 done |
221 done |
222 |
222 |
223 lemma var_app_types: "\<And>ts Ts U. e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> |
223 lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> |
224 e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us" |
224 e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us" |
225 apply (induct us) |
225 apply (induct us fixing: ts Ts U) |
226 apply simp |
226 apply simp |
227 apply (erule var_app_type_eq) |
227 apply (erule var_app_type_eq) |
228 apply assumption |
228 apply assumption |
229 apply simp |
229 apply simp |
230 apply atomize |
230 apply atomize |
290 |
290 |
291 lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> (\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T)" |
291 lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> (\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T)" |
292 by (induct set: typing) auto |
292 by (induct set: typing) auto |
293 |
293 |
294 lemma lift_types: |
294 lemma lift_types: |
295 "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts" |
295 "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts" |
296 apply (induct ts) |
296 apply (induct ts fixing: Ts) |
297 apply simp |
297 apply simp |
298 apply (case_tac Ts) |
298 apply (case_tac Ts) |
299 apply auto |
299 apply auto |
300 done |
300 done |
301 |
301 |
309 apply auto |
309 apply auto |
310 apply blast |
310 apply blast |
311 done |
311 done |
312 |
312 |
313 lemma substs_lemma: |
313 lemma substs_lemma: |
314 "\<And>Ts. e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow> |
314 "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow> |
315 e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts" |
315 e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts" |
316 apply (induct ts) |
316 apply (induct ts fixing: Ts) |
317 apply (case_tac Ts) |
317 apply (case_tac Ts) |
318 apply simp |
318 apply simp |
319 apply simp |
319 apply simp |
320 apply atomize |
320 apply atomize |
321 apply (case_tac Ts) |
321 apply (case_tac Ts) |
350 |
350 |
351 |
351 |
352 subsection {* Alternative induction rule for types *} |
352 subsection {* Alternative induction rule for types *} |
353 |
353 |
354 lemma type_induct [induct type]: |
354 lemma type_induct [induct type]: |
|
355 assumes |
355 "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow> |
356 "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow> |
356 (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> P T" |
357 (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)" |
357 proof - |
358 shows "P T" |
358 case rule_context |
359 proof (induct T) |
359 show ?thesis |
360 case Atom |
360 proof (induct T) |
361 show ?case by (rule prems) simp_all |
361 case Atom |
362 next |
362 show ?case by (rule rule_context) simp_all |
363 case Fun |
363 next |
364 show ?case by (rule prems) (insert Fun, simp_all) |
364 case Fun |
|
365 show ?case by (rule rule_context) (insert Fun, simp_all) |
|
366 qed |
|
367 qed |
365 qed |
368 |
366 |
369 end |
367 end |