35 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
35 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
36 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
36 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
37 |
37 |
38 lemma supp_eqs: |
38 lemma supp_eqs: |
39 "supp Type = {}" |
39 "supp Type = {}" |
40 "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPi rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)" |
40 "supp kind = fv_kind kind \<Longrightarrow> supp (KPi ty name kind) = supp ty \<union> supp (Abs {atom name} kind)" |
41 "supp (TConst i) = {atom i}" |
41 "supp (TConst i) = {atom i}" |
42 "supp (TApp A M) = supp A \<union> supp M" |
42 "supp (TApp A M) = supp A \<union> supp M" |
43 "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPi rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)" |
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 rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
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 kind_ty_trm_perm) |
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) |
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 |
67 lemma supp_rkind_rty_rtrm: |
67 lemma supp_kind_ty_trm: |
68 "supp Type = {}" |
68 "supp Type = {}" |
69 "supp (KPi A x K) = supp A \<union> (supp K - {atom x})" |
69 "supp (KPi A x K) = supp A \<union> (supp K - {atom x})" |
70 "supp (TConst i) = {atom i}" |
70 "supp (TConst i) = {atom i}" |
71 "supp (TApp A M) = supp A \<union> supp M" |
71 "supp (TApp A M) = supp A \<union> supp M" |
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})" |