638 apply(default) |
638 apply(default) |
639 apply(simp_all only: KIND_TY_TRM_fs) |
639 apply(simp_all only: KIND_TY_TRM_fs) |
640 done |
640 done |
641 |
641 |
642 lemma supp_fv: |
642 lemma supp_fv: |
643 "fv_kind t1 = supp t1" |
643 "supp t1 = fv_kind t1" |
644 "fv_ty t2 = supp t2" |
644 "supp t2 = fv_ty t2" |
645 "fv_trm t3 = supp t3" |
645 "supp t3 = fv_trm t3" |
646 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts) |
646 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts) |
647 apply (simp_all add: supp_kind_ty_trm_easy) |
647 apply (simp_all add: supp_kind_ty_trm_easy) |
648 apply (simp_all add: fv_kind_ty_trm) |
648 apply (simp_all add: fv_kind_ty_trm) |
649 apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)") |
649 apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)") |
650 apply(simp add: supp_Abs Set.Un_commute) |
650 apply(simp add: supp_Abs Set.Un_commute) |
651 apply(simp (no_asm) add: supp_def) |
651 apply(simp (no_asm) add: supp_def) |
652 apply(simp add: KIND_TY_TRM_INJECT) |
652 apply(simp add: KIND_TY_TRM_INJECT) |
653 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] alpha_gen) |
653 apply(simp add: Abs_eq_iff) |
654 apply(simp add: Abs_eq_iff alpha_gen) |
654 apply(simp add: alpha_gen) |
|
655 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt) |
655 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
656 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
656 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
657 apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)") |
657 apply (rule refl) |
658 apply(simp add: supp_Abs Set.Un_commute) |
658 sorry (* Stuck *) |
659 apply(simp (no_asm) add: supp_def) |
659 |
660 apply(simp add: KIND_TY_TRM_INJECT) |
|
661 apply(simp add: Abs_eq_iff) |
|
662 apply(simp add: alpha_gen) |
|
663 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt) |
|
664 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
|
665 apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)") |
|
666 apply(simp add: supp_Abs Set.Un_commute) |
|
667 apply(simp (no_asm) add: supp_def) |
|
668 apply(simp add: KIND_TY_TRM_INJECT) |
|
669 apply(simp add: Abs_eq_iff) |
|
670 apply(simp add: alpha_gen) |
|
671 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt) |
|
672 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
|
673 done |
|
674 |
|
675 (* Not needed anymore *) |
660 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A" |
676 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A" |
661 (*apply (subst supp_Pair[symmetric])*) |
677 apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT) |
662 unfolding supp_def |
678 apply (simp add: alpha_gen supp_fv) |
663 apply (simp add: permute_set_eq) |
679 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute) |
664 apply(subst Abs_eq_iff) |
|
665 apply(subst KIND_TY_TRM_INJECT) |
|
666 apply(simp only: alpha_gen supp_fv) |
|
667 apply simp |
|
668 apply (simp_all add: Collect_imp_eq Collect_neg_eq) |
|
669 apply(subst Set.Un_commute) |
|
670 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
671 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
672 apply (rule refl) |
|
673 prefer 2 |
|
674 apply (rule refl) |
|
675 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
676 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} ) |
|
677 apply (rule refl) |
|
678 apply (simp_all) |
|
679 apply (simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric]) |
|
680 sorry (* should be true... *) |
|
681 |
|
682 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
|
683 apply(subst supp_kpi_pre) |
|
684 apply(subst supp_Abs) |
|
685 apply (simp only: Set.Un_commute) |
|
686 done |
680 done |
687 |
681 |
688 lemma supp_kind_ty_trm: |
682 lemma supp_kind_ty_trm: |
689 "supp TYP = {}" |
683 "supp TYP = {}" |
690 "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
684 "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |