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 as |
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] |
|
407 |
406 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" |
407 apply (induct rule: KIND_TY_TRM_induct) |
409 apply (induct rule: KIND_TY_TRM_induct) |
408 apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted]) |
410 apply (simp_all) |
409 done |
411 done |
410 |
412 |
411 lemma perm_add_ok: |
413 lemma perm_add_ok: |
412 "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))" |
414 "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))" |
413 "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)" |
415 "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)" |
414 "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)" |
416 "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)" |
415 apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts) |
417 apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts) |
416 apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted]) |
418 apply (simp_all) |
417 done |
419 done |
418 |
420 |
419 instance |
421 instance |
420 apply default |
422 apply default |
421 apply (simp_all add: perm_zero_ok perm_add_ok) |
423 apply (simp_all add: perm_zero_ok perm_add_ok) |
422 done |
424 done |
423 |
425 |
424 end |
426 end |
425 |
|
426 lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted] |
|
427 |
427 |
428 lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
428 lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
429 |
429 |
430 lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
430 lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
431 |
431 |