equal
deleted
inserted
replaced
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 rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
47 "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
48 apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm) |
48 apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm) |
49 apply(simp_all only: kind_ty_trm_inject 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) |