equal
deleted
inserted
replaced
72 done |
72 done |
73 |
73 |
74 |
74 |
75 text {* Iterated function types *} |
75 text {* Iterated function types *} |
76 |
76 |
77 lemma list_app_typeD [rulify]: |
77 lemma list_app_typeD [rulified]: |
78 "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)" |
78 "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)" |
79 apply (induct_tac ts) |
79 apply (induct_tac ts) |
80 apply simp |
80 apply simp |
81 apply (intro strip) |
81 apply (intro strip) |
82 apply simp |
82 apply simp |
88 apply (ind_cases "e |- t $ u : T") |
88 apply (ind_cases "e |- t $ u : T") |
89 apply (rule_tac x = "Ta # Ts" in exI) |
89 apply (rule_tac x = "Ta # Ts" in exI) |
90 apply simp |
90 apply simp |
91 done |
91 done |
92 |
92 |
93 lemma list_app_typeI [rulify]: |
93 lemma list_app_typeI [rulified]: |
94 "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T" |
94 "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T" |
95 apply (induct_tac ts) |
95 apply (induct_tac ts) |
96 apply (intro strip) |
96 apply (intro strip) |
97 apply simp |
97 apply simp |
98 apply (intro strip) |
98 apply (intro strip) |
107 apply (erule typing.App) |
107 apply (erule typing.App) |
108 apply assumption |
108 apply assumption |
109 apply blast |
109 apply blast |
110 done |
110 done |
111 |
111 |
112 lemma lists_types [rulify]: |
112 lemma lists_types [rulified]: |
113 "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}" |
113 "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}" |
114 apply (induct_tac ts) |
114 apply (induct_tac ts) |
115 apply (intro strip) |
115 apply (intro strip) |
116 apply (case_tac Ts) |
116 apply (case_tac Ts) |
117 apply simp |
117 apply simp |
127 done |
127 done |
128 |
128 |
129 |
129 |
130 subsection {* Lifting preserves termination and well-typedness *} |
130 subsection {* Lifting preserves termination and well-typedness *} |
131 |
131 |
132 lemma lift_map [rulify, simp]: |
132 lemma lift_map [rulified, simp]: |
133 "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts" |
133 "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts" |
134 apply (induct_tac ts) |
134 apply (induct_tac ts) |
135 apply simp_all |
135 apply simp_all |
136 done |
136 done |
137 |
137 |
138 lemma subst_map [rulify, simp]: |
138 lemma subst_map [rulified, simp]: |
139 "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts" |
139 "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts" |
140 apply (induct_tac ts) |
140 apply (induct_tac ts) |
141 apply simp_all |
141 apply simp_all |
142 done |
142 done |
143 |
143 |
144 lemma lift_IT [rulify, intro!]: |
144 lemma lift_IT [rulified, intro!]: |
145 "t \<in> IT ==> \<forall>i. lift t i \<in> IT" |
145 "t \<in> IT ==> \<forall>i. lift t i \<in> IT" |
146 apply (erule IT.induct) |
146 apply (erule IT.induct) |
147 apply (rule allI) |
147 apply (rule allI) |
148 apply (simp (no_asm)) |
148 apply (simp (no_asm)) |
149 apply (rule conjI) |
149 apply (rule conjI) |
159 blast, |
159 blast, |
160 assumption)+ |
160 assumption)+ |
161 apply auto |
161 apply auto |
162 done |
162 done |
163 |
163 |
164 lemma lifts_IT [rulify]: |
164 lemma lifts_IT [rulified]: |
165 "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT" |
165 "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT" |
166 apply (induct_tac ts) |
166 apply (induct_tac ts) |
167 apply auto |
167 apply auto |
168 done |
168 done |
169 |
169 |
178 apply simp |
178 apply simp |
179 apply (case_tac nat) |
179 apply (case_tac nat) |
180 apply simp_all |
180 apply simp_all |
181 done |
181 done |
182 |
182 |
183 lemma lift_type' [rulify]: |
183 lemma lift_type' [rulified]: |
184 "e |- t : T ==> \<forall>i U. |
184 "e |- t : T ==> \<forall>i U. |
185 (\<lambda>j. if j < i then e j |
185 (\<lambda>j. if j < i then e j |
186 else if j = i then U |
186 else if j = i then U |
187 else e (j - 1)) |- lift t i : T" |
187 else e (j - 1)) |- lift t i : T" |
188 apply (erule typing.induct) |
188 apply (erule typing.induct) |
200 apply (rule ext) |
200 apply (rule ext) |
201 apply (case_tac j) |
201 apply (case_tac j) |
202 apply simp_all |
202 apply simp_all |
203 done |
203 done |
204 |
204 |
205 lemma lift_types [rulify]: |
205 lemma lift_types [rulified]: |
206 "\<forall>Ts. types e ts Ts --> |
206 "\<forall>Ts. types e ts Ts --> |
207 types (\<lambda>j. if j < i then e j |
207 types (\<lambda>j. if j < i then e j |
208 else if j = i then U |
208 else if j = i then U |
209 else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts" |
209 else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts" |
210 apply (induct_tac ts) |
210 apply (induct_tac ts) |
217 done |
217 done |
218 |
218 |
219 |
219 |
220 subsection {* Substitution lemmas *} |
220 subsection {* Substitution lemmas *} |
221 |
221 |
222 lemma subst_lemma [rulify]: |
222 lemma subst_lemma [rulified]: |
223 "e |- t : T ==> \<forall>e' i U u. |
223 "e |- t : T ==> \<forall>e' i U u. |
224 e = (\<lambda>j. if j < i then e' j |
224 e = (\<lambda>j. if j < i then e' j |
225 else if j = i then U |
225 else if j = i then U |
226 else e' (j-1)) --> |
226 else e' (j-1)) --> |
227 e' |- u : U --> e' |- t[u/i] : T" |
227 e' |- u : U --> e' |- t[u/i] : T" |
240 apply assumption |
240 apply assumption |
241 apply fastsimp |
241 apply fastsimp |
242 apply fastsimp |
242 apply fastsimp |
243 done |
243 done |
244 |
244 |
245 lemma substs_lemma [rulify]: |
245 lemma substs_lemma [rulified]: |
246 "e |- u : T ==> |
246 "e |- u : T ==> |
247 \<forall>Ts. types (\<lambda>j. if j < i then e j |
247 \<forall>Ts. types (\<lambda>j. if j < i then e j |
248 else if j = i then T else e (j - 1)) ts Ts --> |
248 else if j = i then T else e (j - 1)) ts Ts --> |
249 types e (map (\<lambda>t. t[u/i]) ts) Ts" |
249 types e (map (\<lambda>t. t[u/i]) ts) Ts" |
250 apply (induct_tac ts) |
250 apply (induct_tac ts) |
263 done |
263 done |
264 |
264 |
265 |
265 |
266 subsection {* Subject reduction *} |
266 subsection {* Subject reduction *} |
267 |
267 |
268 lemma subject_reduction [rulify]: |
268 lemma subject_reduction [rulified]: |
269 "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T" |
269 "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T" |
270 apply (erule typing.induct) |
270 apply (erule typing.induct) |
271 apply blast |
271 apply blast |
272 apply blast |
272 apply blast |
273 apply (intro strip) |
273 apply (intro strip) |
288 |
288 |
289 lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])" |
289 lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])" |
290 apply simp |
290 apply simp |
291 done |
291 done |
292 |
292 |
293 lemma subst_Var_IT [rulify]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT" |
293 lemma subst_Var_IT [rulified]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT" |
294 apply (erule IT.induct) |
294 apply (erule IT.induct) |
295 txt {* Case @{term Var}: *} |
295 txt {* Case @{term Var}: *} |
296 apply (intro strip) |
296 apply (intro strip) |
297 apply (simp (no_asm) add: subst_Var) |
297 apply (simp (no_asm) add: subst_Var) |
298 apply |
298 apply |
332 apply (rule IT.Var) |
332 apply (rule IT.Var) |
333 apply simp |
333 apply simp |
334 apply (rule lists.Cons) |
334 apply (rule lists.Cons) |
335 apply (rule Var_IT) |
335 apply (rule Var_IT) |
336 apply (rule lists.Nil) |
336 apply (rule lists.Nil) |
337 apply (rule IT.Beta [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]]) |
337 apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]]) |
338 apply (erule subst_Var_IT) |
338 apply (erule subst_Var_IT) |
339 apply (rule Var_IT) |
339 apply (rule Var_IT) |
340 apply (subst app_last) |
340 apply (subst app_last) |
341 apply (rule IT.Beta) |
341 apply (rule IT.Beta) |
342 apply (subst app_last [symmetric]) |
342 apply (subst app_last [symmetric]) |
345 done |
345 done |
346 |
346 |
347 |
347 |
348 subsection {* Well-typed substitution preserves termination *} |
348 subsection {* Well-typed substitution preserves termination *} |
349 |
349 |
350 lemma subst_type_IT [rulify]: |
350 lemma subst_type_IT [rulified]: |
351 "\<forall>t. t \<in> IT --> (\<forall>e T u i. |
351 "\<forall>t. t \<in> IT --> (\<forall>e T u i. |
352 (\<lambda>j. if j < i then e j |
352 (\<lambda>j. if j < i then e j |
353 else if j = i then U |
353 else if j = i then U |
354 else e (j - 1)) |- t : T --> |
354 else e (j - 1)) |- t : T --> |
355 u \<in> IT --> e |- u : U --> t[u/i] \<in> IT)" |
355 u \<in> IT --> e |- u : U --> t[u/i] \<in> IT)" |
452 apply (erule IT.Lambda) |
452 apply (erule IT.Lambda) |
453 apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] \<in> IT") |
453 apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] \<in> IT") |
454 apply simp |
454 apply simp |
455 apply (rule subst_type_IT) |
455 apply (rule subst_type_IT) |
456 apply (rule lists.Nil |
456 apply (rule lists.Nil |
457 [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection] |
457 [THEN 2 lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection] |
458 foldl_Cons [THEN eq_reflection]]) |
458 foldl_Cons [THEN eq_reflection]]) |
459 apply (erule lift_IT) |
459 apply (erule lift_IT) |
460 apply (rule typing.App) |
460 apply (rule typing.App) |
461 apply (rule typing.Var) |
461 apply (rule typing.Var) |
462 apply simp |
462 apply simp |