568 "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)" |
568 "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)" |
569 "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)" |
569 "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)" |
570 "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)" |
570 "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)" |
571 by(lifting rfv_eqvt) |
571 by(lifting rfv_eqvt) |
572 |
572 |
|
573 lemma supp_kind_ty_trm_easy: |
|
574 "supp TYP = {}" |
|
575 "supp (TCONST i) = {atom i}" |
|
576 "supp (TAPP A M) = supp A \<union> supp M" |
|
577 "supp (CONS i) = {atom i}" |
|
578 "supp (VAR x) = {atom x}" |
|
579 "supp (APP M N) = supp M \<union> supp N" |
|
580 apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT) |
|
581 apply (simp_all only: supp_at_base[simplified supp_def]) |
|
582 apply (simp_all add: Collect_imp_eq Collect_neg_eq) |
|
583 done |
|
584 |
|
585 lemma supp_bind: |
|
586 "(supp (atom na, (ty, ki))) supports (KPI ty na ki)" |
|
587 "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)" |
|
588 "(supp (atom na, (ty, trm))) supports (LAM ty na trm)" |
|
589 apply(simp_all add: supports_def) |
|
590 apply(fold fresh_def) |
|
591 apply(simp_all add: fresh_Pair swap_fresh_fresh) |
|
592 apply(clarify) |
|
593 apply(subst swap_at_base_simps(3)) |
|
594 apply(simp_all add: fresh_atom) |
|
595 apply(clarify) |
|
596 apply(subst swap_at_base_simps(3)) |
|
597 apply(simp_all add: fresh_atom) |
|
598 apply(clarify) |
|
599 apply(subst swap_at_base_simps(3)) |
|
600 apply(simp_all add: fresh_atom) |
|
601 done |
|
602 |
|
603 lemma KIND_TY_TRM_fs: |
|
604 "finite (supp (x\<Colon>KIND))" |
|
605 "finite (supp (y\<Colon>TY))" |
|
606 "finite (supp (z\<Colon>TRM))" |
|
607 apply(induct x and y and z rule: KIND_TY_TRM_inducts) |
|
608 apply(simp_all add: supp_kind_ty_trm_easy) |
|
609 apply(rule supports_finite) |
|
610 apply(rule supp_bind(1)) |
|
611 apply(simp add: supp_Pair supp_atom) |
|
612 apply(rule supports_finite) |
|
613 apply(rule supp_bind(2)) |
|
614 apply(simp add: supp_Pair supp_atom) |
|
615 apply(rule supports_finite) |
|
616 apply(rule supp_bind(3)) |
|
617 apply(simp add: supp_Pair supp_atom) |
|
618 done |
|
619 |
|
620 instance KIND and TY and TRM :: fs |
|
621 apply(default) |
|
622 apply(simp_all only: KIND_TY_TRM_fs) |
|
623 done |
|
624 |
573 lemma supp_fv: |
625 lemma supp_fv: |
574 "fv_kind t1 = supp t1" |
626 "fv_kind t1 = supp t1" |
575 "fv_ty t2 = supp t2" |
627 "fv_ty t2 = supp t2" |
576 "fv_trm t3 = supp t3" |
628 "fv_trm t3 = supp t3" |
577 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts) |
629 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts) |
|
630 apply (simp_all add: supp_kind_ty_trm_easy) |
578 apply (simp_all add: fv_kind_ty_trm) |
631 apply (simp_all add: fv_kind_ty_trm) |
579 apply (simp_all add: supp_def) |
632 apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abst {atom name} kind)") |
580 sorry |
633 apply(simp add: supp_Abst Set.Un_commute) |
581 |
634 apply(simp (no_asm) add: supp_def) |
582 lemma |
635 apply(simp add: KIND_TY_TRM_INJECT) |
583 "(supp ((a \<rightleftharpoons> b) \<bullet> (K::KIND)) - {atom ((a \<rightleftharpoons> b) \<bullet> (x::name))} = supp K - {atom x} \<longrightarrow> |
636 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
584 (a \<rightleftharpoons> b) \<bullet> A = (A::TY) \<longrightarrow> (\<forall>pi\<Colon>perm. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K \<longrightarrow> (supp K - {atom x}) \<sharp>* pi \<longrightarrow> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> x)) = |
637 apply(simp add: abs_eq alpha_gen) |
585 (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x} \<and> |
638 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
586 (\<exists>pi\<Colon>perm. (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)}) \<sharp>* pi \<and> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> A \<noteq> A)" |
639 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric]) |
587 apply (case_tac "(a \<rightleftharpoons> b) \<bullet> A = A") |
640 apply (fold supp_def) |
588 apply (case_tac "supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x}") |
641 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
589 apply simp_all |
642 apply (rule refl) |
|
643 apply(subst Set.Un_commute) |
|
644 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
645 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
646 apply (rule refl) |
|
647 prefer 2 |
|
648 apply(simp add: eqvts supp_eqvt atom_eqvt) |
590 sorry |
649 sorry |
591 |
650 |
592 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A" |
651 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A" |
593 apply (subst supp_Pair[symmetric]) |
652 apply (subst supp_Pair[symmetric]) |
594 unfolding supp_def |
653 unfolding supp_def |
598 apply(simp only: supp_fv) |
657 apply(simp only: supp_fv) |
599 apply simp |
658 apply simp |
600 apply (unfold supp_def) |
659 apply (unfold supp_def) |
601 sorry |
660 sorry |
602 |
661 |
603 lemma KIND_TY_TRM_fs: |
|
604 "finite (supp (x\<Colon>KIND))" |
|
605 "finite (supp (y\<Colon>TY))" |
|
606 "finite (supp (z\<Colon>TRM))" |
|
607 apply(induct x and y and z rule: KIND_TY_TRM_inducts) |
|
608 sorry |
|
609 |
|
610 instance KIND and TY and TRM :: fs |
|
611 apply(default) |
|
612 apply(simp_all only: KIND_TY_TRM_fs) |
|
613 done |
|
614 |
|
615 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
662 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
616 apply(subst supp_kpi_pre) |
663 apply(subst supp_kpi_pre) |
617 apply(subst supp_Abst) |
664 apply(subst supp_Abst) |
618 apply (simp only: Set.Un_commute) |
665 apply (simp only: Set.Un_commute) |
619 done |
666 done |
626 "supp (TPI A x B) = supp A \<union> (supp B - {atom x})" |
673 "supp (TPI A x B) = supp A \<union> (supp B - {atom x})" |
627 "supp (CONS i) = {atom i}" |
674 "supp (CONS i) = {atom i}" |
628 "supp (VAR x) = {atom x}" |
675 "supp (VAR x) = {atom x}" |
629 "supp (APP M N) = supp M \<union> supp N" |
676 "supp (APP M N) = supp M \<union> supp N" |
630 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
677 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
631 apply - |
678 apply (simp_all only: supp_kind_ty_trm_easy) |
632 apply (simp add: supp_def) |
|
633 apply (simp add: supp_kpi) |
679 apply (simp add: supp_kpi) |
634 apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base) |
|
635 apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq) |
|
636 defer |
|
637 apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base) |
|
638 apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base) |
|
639 apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq) |
|
640 sorry |
680 sorry |
641 |
681 |
642 |
|
643 end |
682 end |
644 |
683 |
645 |
684 |
646 |
685 |
647 |
686 |