equal
deleted
inserted
replaced
43 "supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)" |
43 "supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)" |
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 kind_ty_trm_perm) |
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) |
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 kind_ty_trm_fv) |
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 |
66 |
66 |
72 "supp (TPi A x B) = supp A \<union> (supp B - {atom x})" |
72 "supp (TPi A x B) = supp A \<union> (supp B - {atom x})" |
73 "supp (Const i) = {atom i}" |
73 "supp (Const i) = {atom i}" |
74 "supp (Var x) = {atom x}" |
74 "supp (Var x) = {atom x}" |
75 "supp (App M N) = supp M \<union> supp N" |
75 "supp (App M N) = supp M \<union> supp N" |
76 "supp (Lam A x M) = supp A \<union> (supp M - {atom x})" |
76 "supp (Lam A x M) = supp A \<union> (supp M - {atom x})" |
77 apply (simp_all add: supp_fv kind_ty_trm_fv) |
77 apply (simp_all add: supp_fv) |
78 |
78 |
79 end |
79 end |
80 |
80 |
81 |
81 |
82 |
82 |