44 "supp (Const i) = {atom i}" |
44 "supp (Const i) = {atom i}" |
45 "supp (Var x) = {atom x}" |
45 "supp (Var x) = {atom x}" |
46 "supp (App M N) = supp M \<union> supp N" |
46 "supp (App M N) = supp M \<union> supp N" |
47 "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)" |
47 "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)" |
48 apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt) |
48 apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt) |
49 apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen) |
49 apply(simp_all only: kind_ty_trm.eq_iff Abs_eq_iff alpha_gen) |
50 apply(simp_all only: ex_out) |
50 apply(simp_all only: ex_out) |
51 apply(simp_all only: eqvts[symmetric]) |
51 apply(simp_all only: eqvts[symmetric]) |
52 apply(simp_all only: Collect_neg_conj) |
52 apply(simp_all only: Collect_neg_conj) |
53 apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc) |
53 apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc) |
54 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc) |
54 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc) |
55 apply(simp_all add: Un_left_commute) |
55 apply(simp_all add: Un_left_commute) |
56 done |
56 done |
57 |
57 |
58 lemma supp_fv: |
58 lemma supp_fv: |
59 "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3" |
59 "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3" |
60 apply(induct rule: kind_ty_trm_induct) |
60 apply(induct rule: kind_ty_trm.induct) |
61 apply(simp_all (no_asm) only: supp_eqs) |
61 apply(simp_all (no_asm) only: supp_eqs) |
62 apply(simp_all) |
62 apply(simp_all) |
63 apply(simp_all add: supp_eqs) |
63 apply(simp_all add: supp_eqs) |
64 apply(simp_all add: supp_Abs) |
64 apply(simp_all add: supp_Abs) |
65 done |
65 done |