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