199 lemma supp_rkind_rty_rtrm_easy:

   199 lemma supp_eqs:

   200  "supp TYP = {}"

   200   "supp TYP = {}"

   201  "supp (TCONST i) = {atom i}"

   201   "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"

   202  "supp (TAPP A M) = supp A \<union> supp M"

   202   "supp (TCONST i) = {atom i}"

   203  "supp (CONS i) = {atom i}"

   203   "supp (TAPP A M) = supp A \<union> supp M"

   204  "supp (VAR x) = {atom x}"

   204   "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"

   205  "supp (APP M N) = supp M \<union> supp N"

   205   "supp (CONS i) = {atom i}"

   206 apply (simp_all add: supp_def permute_ktt)

   206   "supp (VAR x) = {atom x}"

   207 apply (simp_all only: kind_ty_trm_INJECT)

   207   "supp (APP M N) = supp M \<union> supp N"

   208 apply (simp_all only: supp_at_base[simplified supp_def])

   208   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"

   209 apply (simp_all add: Collect_imp_eq Collect_neg_eq)

   209   apply(simp_all (no_asm) add: supp_def)

   210 done

   210   apply(simp_all only: kind_ty_trm_INJECT Abs_eq_iff alpha_gen)

   211   apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])

   212   apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)

   213   apply(simp_all add: supp_at_base[simplified supp_def])

   214   done

   213  "supp t1 = fv_kind t1"

   217   "supp t1 = fv_kind t1"

   214  "supp t2 = fv_ty t2"

   218   "supp t2 = fv_ty t2"

   215  "supp t3 = fv_trm t3"

   219   "supp t3 = fv_trm t3"

   216 apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)

   220   apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)

   217 apply (simp_all add: supp_rkind_rty_rtrm_easy)

   221   apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm)

   218 apply (simp_all add: fv_kind_ty_trm)

   222   apply(simp_all)

   219 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")

   223   apply(subst supp_eqs)

   220 apply(simp only: supp_Abs)

   224   apply(simp_all add: supp_Abs)

   221 apply(simp (no_asm) add: supp_def)

   225   apply(subst supp_eqs)

   222 apply(simp add: kind_ty_trm_INJECT)

   226   apply(simp_all add: supp_Abs)

   223 apply(simp add: Abs_eq_iff)

   227   apply(subst supp_eqs)

   224 apply(simp add: alpha_gen)

   228   apply(simp_all add: supp_Abs)

   225 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)

   229   done

   226 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])

   227 apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)")

   228 apply(simp add: supp_Abs)

   229 apply(simp (no_asm) add: supp_def)

   230 apply(simp add: kind_ty_trm_INJECT)

   231 apply(simp add: Abs_eq_iff)

   232 apply(simp add: alpha_gen)

   233 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)

   234 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)

   235 apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)")

   236 apply(simp add: supp_Abs)

   237 apply(simp (no_asm) add: supp_def)

   238 apply(simp add: kind_ty_trm_INJECT)

   239 apply(simp add: Abs_eq_iff)

   240 apply(simp add: alpha_gen)

   241 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)

   242 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)

   243 done

   244 

   245 (* Not needed anymore *)

   246 lemma supp_kpi: "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"

   247 apply (simp add: permute_set_eq supp_def Abs_eq_iff kind_ty_trm_INJECT)

   248 apply (simp add: alpha_gen supp_fv)

   249 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)

   250 done

   253  "supp TYP = {}"

   232   "supp TYP = {}"

   254  "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"

   233   "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"

   255  "supp (TCONST i) = {atom i}"

   234   "supp (TCONST i) = {atom i}"

   256  "supp (TAPP A M) = supp A \<union> supp M"

   235   "supp (TAPP A M) = supp A \<union> supp M"

   257  "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"

   236   "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"

   258  "supp (CONS i) = {atom i}"

   237   "supp (CONS i) = {atom i}"

   259  "supp (VAR x) = {atom x}"

   238   "supp (VAR x) = {atom x}"

   260  "supp (APP M N) = supp M \<union> supp N"

   239   "supp (APP M N) = supp M \<union> supp N"

   261  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"

   240   "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"

   262 apply (simp_all only: supp_rkind_rty_rtrm_easy)

   241   by (simp_all only: supp_fv fv_kind_ty_trm)

   263 apply (simp_all only: supp_fv fv_kind_ty_trm)

   264 done