11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
12 |
12 |
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
14 local_theory -> local_theory |
14 local_theory -> local_theory |
15 |
15 |
16 val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> |
16 val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> |
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
18 end |
18 end |
19 |
19 |
20 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
20 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
21 struct |
21 struct |
153 if false then print_tac ("ptest: " ^ msg) else all_tac |
153 if false then print_tac ("ptest: " ^ msg) else all_tac |
154 |
154 |
155 fun q_tac msg i = |
155 fun q_tac msg i = |
156 if true then print_tac ("qtest: " ^ msg) else all_tac |
156 if true then print_tac ("qtest: " ^ msg) else all_tac |
157 |
157 |
158 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps |
158 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps |
159 fv_bn_eqvts qinduct bclausess ctxt = |
159 fv_bn_eqvts qinduct bclausess ctxt = |
160 let |
160 let |
161 val goals1 = map mk_fvs_goals fvs |
161 val goals1 = map mk_fvs_goals fvs |
162 val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns |
162 val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns |
163 |
|
164 |
|
165 |
163 |
166 fun tac ctxt = |
164 fun tac ctxt = |
167 SUBGOAL (fn (goal, i) => |
165 SUBGOAL (fn (goal, i) => |
168 let |
166 let |
169 val (fv_fun, arg) = |
167 val (fv_fun, arg) = |
188 end) |
186 end) |
189 in |
187 in |
190 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
188 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
191 end |
189 end |
192 |
190 |
193 (* |
|
194 fun fv_tac bclauses ctxt = |
|
195 SOLVED' (EVERY' [ |
|
196 (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ " with " ^ (@{make_string} bclauses))), |
|
197 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
|
198 p_tac "A", |
|
199 TRY o EVERY' (mk_supp_abs_tac ctxt bclauses), |
|
200 p_tac "B", |
|
201 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
|
202 p_tac "C", |
|
203 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
|
204 p_tac "D", |
|
205 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
|
206 p_tac "E", |
|
207 TRY o asm_full_simp_tac (add_ss thms3), |
|
208 p_tac "F", |
|
209 TRY o simp_tac (add_ss thms2), |
|
210 p_tac "G", |
|
211 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), |
|
212 p_tac "H", |
|
213 (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) |
|
214 ]) |
|
215 |
|
216 fun fv_tacs ctxt = map (fv_tac ctxt) bclausess |
|
217 (*fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps*) |
|
218 *) |
|
219 |
|
220 (* |
|
221 fun bn_tac ctxt bn_simp = |
|
222 SOLVED' (EVERY' [ |
|
223 (fn i => print_tac ("BN Goal: " ^ string_of_int i)), |
|
224 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
|
225 q_tac "A", |
|
226 TRY o mk_bn_supp_abs_tac bn_simp, |
|
227 q_tac "B", |
|
228 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
|
229 q_tac "C", |
|
230 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
|
231 q_tac "D", |
|
232 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
|
233 q_tac "E", |
|
234 TRY o asm_full_simp_tac (add_ss thms3), |
|
235 q_tac "F", |
|
236 TRY o simp_tac (add_ss thms2), |
|
237 q_tac "G", |
|
238 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), |
|
239 (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i)) |
|
240 ]) |
|
241 *) |
|
242 |
191 |
243 |
192 |
244 end (* structure *) |
193 end (* structure *) |