254 TRM = trm / atrm |
254 TRM = trm / atrm |
255 by (auto intro: alpha_equivps) |
255 by (auto intro: alpha_equivps) |
256 |
256 |
257 quotient_definition |
257 quotient_definition |
258 "TYP :: KIND" |
258 "TYP :: KIND" |
259 as |
259 is |
260 "Type" |
260 "Type" |
261 |
261 |
262 quotient_definition |
262 quotient_definition |
263 "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
263 "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
264 as |
264 is |
265 "KPi" |
265 "KPi" |
266 |
266 |
267 quotient_definition |
267 quotient_definition |
268 "TCONST :: ident \<Rightarrow> TY" |
268 "TCONST :: ident \<Rightarrow> TY" |
269 as |
269 is |
270 "TConst" |
270 "TConst" |
271 |
271 |
272 quotient_definition |
272 quotient_definition |
273 "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY" |
273 "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY" |
274 as |
274 is |
275 "TApp" |
275 "TApp" |
276 |
276 |
277 quotient_definition |
277 quotient_definition |
278 "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
278 "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
279 as |
279 is |
280 "TPi" |
280 "TPi" |
281 |
281 |
282 (* FIXME: does not work with CONST *) |
282 (* FIXME: does not work with CONST *) |
283 quotient_definition |
283 quotient_definition |
284 "CONS :: ident \<Rightarrow> TRM" |
284 "CONS :: ident \<Rightarrow> TRM" |
285 as |
285 is |
286 "Const" |
286 "Const" |
287 |
287 |
288 quotient_definition |
288 quotient_definition |
289 "VAR :: name \<Rightarrow> TRM" |
289 "VAR :: name \<Rightarrow> TRM" |
290 as |
290 is |
291 "Var" |
291 "Var" |
292 |
292 |
293 quotient_definition |
293 quotient_definition |
294 "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
294 "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
295 as |
295 is |
296 "App" |
296 "App" |
297 |
297 |
298 quotient_definition |
298 quotient_definition |
299 "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
299 "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
300 as |
300 is |
301 "Lam" |
301 "Lam" |
302 |
302 |
303 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
303 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
304 quotient_definition |
304 quotient_definition |
305 "fv_kind :: KIND \<Rightarrow> atom set" |
305 "fv_kind :: KIND \<Rightarrow> atom set" |
306 as |
306 is |
307 "rfv_kind" |
307 "rfv_kind" |
308 |
308 |
309 quotient_definition |
309 quotient_definition |
310 "fv_ty :: TY \<Rightarrow> atom set" |
310 "fv_ty :: TY \<Rightarrow> atom set" |
311 as |
311 is |
312 "rfv_ty" |
312 "rfv_ty" |
313 |
313 |
314 quotient_definition |
314 quotient_definition |
315 "fv_trm :: TRM \<Rightarrow> atom set" |
315 "fv_trm :: TRM \<Rightarrow> atom set" |
316 as |
316 is |
317 "rfv_trm" |
317 "rfv_trm" |
318 |
318 |
319 lemma alpha_rfv: |
319 lemma alpha_rfv: |
320 shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and> |
320 shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and> |
321 (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and> |
321 (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and> |
388 instantiation KIND and TY and TRM :: pt |
388 instantiation KIND and TY and TRM :: pt |
389 begin |
389 begin |
390 |
390 |
391 quotient_definition |
391 quotient_definition |
392 "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND" |
392 "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND" |
393 as |
393 is |
394 "permute :: perm \<Rightarrow> kind \<Rightarrow> kind" |
394 "permute :: perm \<Rightarrow> kind \<Rightarrow> kind" |
395 |
395 |
396 quotient_definition |
396 quotient_definition |
397 "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY" |
397 "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY" |
398 as |
398 is |
399 "permute :: perm \<Rightarrow> ty \<Rightarrow> ty" |
399 "permute :: perm \<Rightarrow> ty \<Rightarrow> ty" |
400 |
400 |
401 quotient_definition |
401 quotient_definition |
402 "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM" |
402 "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM" |
403 as |
403 is |
404 "permute :: perm \<Rightarrow> trm \<Rightarrow> trm" |
404 "permute :: perm \<Rightarrow> trm \<Rightarrow> trm" |
405 |
405 |
406 lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted] |
406 lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted] |
407 |
407 |
408 lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z" |
408 lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z" |