644 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
644 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
645 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
645 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
646 apply (rule refl) |
646 apply (rule refl) |
647 prefer 2 |
647 prefer 2 |
648 apply(simp add: eqvts supp_eqvt atom_eqvt) |
648 apply(simp add: eqvts supp_eqvt atom_eqvt) |
649 sorry |
649 sorry (* Stuck *) |
650 |
650 |
651 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" |
652 apply (subst supp_Pair[symmetric]) |
652 (*apply (subst supp_Pair[symmetric])*) |
653 unfolding supp_def |
653 unfolding supp_def |
654 apply (simp add: permute_set_eq) |
654 apply (simp add: permute_set_eq) |
655 apply(subst abs_eq) |
655 apply(subst abs_eq) |
656 apply(subst KIND_TY_TRM_INJECT) |
656 apply(subst KIND_TY_TRM_INJECT) |
657 apply(simp only: supp_fv) |
657 apply(simp only: supp_fv) |
658 apply simp |
658 apply simp |
659 apply (unfold supp_def) |
659 apply (simp_all add: Collect_imp_eq Collect_neg_eq) |
660 sorry |
660 apply(subst Set.Un_commute) |
|
661 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
662 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
663 apply (rule refl) |
|
664 prefer 2 |
|
665 apply (rule refl) |
|
666 sorry (* Stuck *) |
661 |
667 |
662 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
668 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
663 apply(subst supp_kpi_pre) |
669 apply(subst supp_kpi_pre) |
664 apply(subst supp_Abst) |
670 apply(subst supp_Abst) |
665 apply (simp only: Set.Un_commute) |
671 apply (simp only: Set.Un_commute) |
675 "supp (VAR x) = {atom x}" |
681 "supp (VAR x) = {atom x}" |
676 "supp (APP M N) = supp M \<union> supp N" |
682 "supp (APP M N) = supp M \<union> supp N" |
677 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
683 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
678 apply (simp_all only: supp_kind_ty_trm_easy) |
684 apply (simp_all only: supp_kind_ty_trm_easy) |
679 apply (simp add: supp_kpi) |
685 apply (simp add: supp_kpi) |
680 sorry |
686 sorry (* Other ones will follow similarily *) |
|
687 |
681 |
688 |
682 end |
689 end |
683 |
690 |
684 |
691 |
685 |
692 |