25 lemma ex_out: 

    25 thm kind_ty_trm.supp

    26   "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"

    27   "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"

    28   "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"

    29   "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"

    30 apply (blast)+

    31 done

    32 

    33 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"

    34 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])

    35 

    36 lemma supp_eqs:

    37   "supp Type = {}"

    38   "supp kind = fv_kind kind \<Longrightarrow> supp (KPi ty name kind) = supp ty \<union> supp (Abs {atom name} kind)"

    39   "supp (TConst i) = {atom i}"

    40   "supp (TApp A M) = supp A \<union> supp M"

    41   "supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)"

    42   "supp (Const i) = {atom i}"

    43   "supp (Var x) = {atom x}"

    44   "supp (App M N) = supp M \<union> supp N"

    45   "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"

    46   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt)

    47   apply(simp_all only: kind_ty_trm.eq_iff Abs_eq_iff alpha_gen)

    48   apply(simp_all only: ex_out)

    49   apply(simp_all only: eqvts[symmetric])

    50   apply(simp_all only: Collect_neg_conj)

    51   apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc)

    52   apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc)

    53   apply(simp_all add: Un_left_commute)

    54   done

    55 

    56 lemma supp_fv:

    57   "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"

    58   apply(induct rule: kind_ty_trm.induct)

    59   apply(simp_all (no_asm) only: supp_eqs)

    60   apply(simp_all)

    61   apply(simp_all add: supp_eqs)

    62   apply(simp_all add: supp_Abs)

    63   done

    64 

    65 lemma supp_kind_ty_trm:

    66   "supp Type = {}"

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

    68   "supp (TConst i) = {atom i}"

    69   "supp (TApp A M) = supp A \<union> supp M"

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

    71   "supp (Const i) = {atom i}"

    72   "supp (Var x) = {atom x}"

    73   "supp (App M N) = supp M \<union> supp N"

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

    75 apply (simp_all add: supp_fv)