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: Abs_eq_iff) |
653 apply(simp add: Abs_eq_iff) |
654 apply(simp add: 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 insert_eqvt empty_eqvt atom_eqvt) |
656 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
656 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
657 apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)") |
657 apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)") |
658 apply(simp add: supp_Abs Set.Un_commute) |
658 apply(simp add: supp_Abs Set.Un_commute) |
659 apply(simp (no_asm) add: supp_def) |
659 apply(simp (no_asm) add: supp_def) |
660 apply(simp add: KIND_TY_TRM_INJECT) |
660 apply(simp add: KIND_TY_TRM_INJECT) |
661 apply(simp add: Abs_eq_iff) |
661 apply(simp add: Abs_eq_iff) |
662 apply(simp add: alpha_gen) |
662 apply(simp add: alpha_gen) |
663 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt) |
663 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
664 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
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)") |
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) |
666 apply(simp add: supp_Abs Set.Un_commute) |
667 apply(simp (no_asm) add: supp_def) |
667 apply(simp (no_asm) add: supp_def) |
668 apply(simp add: KIND_TY_TRM_INJECT) |
668 apply(simp add: KIND_TY_TRM_INJECT) |
669 apply(simp add: Abs_eq_iff) |
669 apply(simp add: Abs_eq_iff) |
670 apply(simp add: alpha_gen) |
670 apply(simp add: alpha_gen) |
671 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt) |
671 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
672 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
672 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
673 done |
673 done |
674 |
674 |
675 (* Not needed anymore *) |
675 (* Not needed anymore *) |
676 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" |