83 | "bv_tvtk TVTKNil = {}" |
83 | "bv_tvtk TVTKNil = {}" |
84 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
84 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
85 | "bv_tvck TVCKNil = {}" |
85 | "bv_tvck TVCKNil = {}" |
86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
87 |
87 |
88 ML {* Sign.of_sort @{theory} (@{typ tkind}, @{sort fs}) *} |
88 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15) |
89 |
89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
90 lemma helper: |
|
91 "((\<exists>p. P p) \<and> Q) = (\<exists>p. (P p \<and> Q))" |
|
92 "(Q \<and> (\<exists>p. P p)) = (\<exists>p. (Q \<and> P p))" |
|
93 by auto |
|
94 |
|
95 lemma supp: |
|
96 "fv_tkind tkind = supp tkind \<and> |
|
97 fv_ckind ckind = supp ckind \<and> |
|
98 fv_ty ty = supp ty \<and> |
|
99 fv_ty_lst ty_lst = supp ty_lst \<and> |
|
100 fv_co co = supp co \<and> |
|
101 fv_co_lst co_lst = supp co_lst \<and> |
|
102 fv_trm trm = supp trm \<and> |
|
103 fv_assoc_lst assoc_lst = supp assoc_lst \<and> |
|
104 (fv_pat pat = supp pat \<and> fv_bv pat = {a. infinite {b. \<not> alpha_bv ((a \<rightleftharpoons> b) \<bullet> pat) pat}}) \<and> |
|
105 (fv_vt_lst vt_lst = supp vt_lst \<and> |
|
106 fv_bv_vt vt_lst = {a. infinite {b. \<not> alpha_bv_vt ((a \<rightleftharpoons> b) \<bullet> vt_lst) vt_lst}}) \<and> |
|
107 (fv_tvtk_lst tvtk_lst = supp tvtk_lst \<and> |
|
108 fv_bv_tvtk tvtk_lst = {a. infinite {b. \<not> alpha_bv_tvtk ((a \<rightleftharpoons> b) \<bullet> tvtk_lst) tvtk_lst}}) \<and> |
|
109 fv_tvck_lst tvck_lst = supp tvck_lst \<and> |
|
110 fv_bv_tvck tvck_lst = {a. infinite {b. \<not> alpha_bv_tvck ((a \<rightleftharpoons> b) \<bullet> tvck_lst) tvck_lst}}" |
|
111 apply(rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
|
112 ML_prf {* |
|
113 fun supp_eq_tac fv perm eqiff ctxt = |
|
114 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
|
115 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW |
|
116 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
|
117 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
|
118 simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW |
|
119 simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW |
|
120 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
|
121 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW |
|
122 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
|
123 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
|
124 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
|
125 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
|
126 simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW |
|
127 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
|
128 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
|
129 simp_tac (HOL_basic_ss addsimps @{thms helper}) THEN_ALL_NEW |
|
130 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
|
131 *} |
|
132 apply (tactic {* ALLGOALS (TRY o SOLVED' (supp_eq_tac |
|
133 @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv} |
|
134 @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm} |
|
135 @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff} |
|
136 @{context})) *}) |
|
137 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv) |
|
138 apply (simp only: supp_Abs[symmetric]) |
|
139 apply (simp (no_asm) only: supp_def) |
|
140 apply (simp only: permute_ABS) |
|
141 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm) |
|
142 apply (simp only: Abs_eq_iff) |
|
143 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff) |
|
144 apply (simp only: alpha_gen) |
|
145 apply (simp only: eqvts[symmetric]) |
|
146 apply (simp only: eqvts) |
|
147 apply (simp only: Collect_disj_eq[symmetric]) |
|
148 apply (simp only: infinite_Un[symmetric]) |
|
149 apply (simp only: Collect_disj_eq[symmetric]) |
|
150 apply (simp only: de_Morgan_conj[symmetric]) |
|
151 apply (simp only: helper) |
|
152 |
|
153 thm supp |
|
154 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified supp] |
|
155 |
90 |
156 |
91 |
157 end |
92 end |
158 |
93 |
159 |
94 |