equal
deleted
inserted
replaced
205 shows "xs = ys \<Longrightarrow> set xs = set ys" |
205 shows "xs = ys \<Longrightarrow> set xs = set ys" |
206 by simp |
206 by simp |
207 |
207 |
208 ML {* |
208 ML {* |
209 fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
209 fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
210 (prems, bclausess) qexhaust_thm = |
210 prems bclausess qexhaust_thm = |
211 let |
211 let |
212 fun aux_tac prem bclauses = |
212 fun aux_tac prem bclauses = |
213 case (get_all_binders bclauses) of |
213 case (get_all_binders bclauses) of |
214 [] => EVERY' [rtac prem, atac] |
214 [] => EVERY' [rtac prem, atac] |
215 | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => |
215 | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => |
274 val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm) |
274 val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm) |
275 in |
275 in |
276 rtac side_thm 1 |
276 rtac side_thm 1 |
277 end) ctxt |
277 end) ctxt |
278 in |
278 in |
279 rtac qexhaust_thm THEN' RANGE (map2 aux_tac prems bclausess) |
279 EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] |
280 end |
280 end |
281 *} |
281 *} |
282 |
282 |
283 |
283 ML {* |
284 ML {* |
284 fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns |
285 fun prove_strong_exhausts lthy exhausts qtrms bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns |
|
286 perm_bn_alphas = |
285 perm_bn_alphas = |
287 let |
286 let |
288 val ((_, exhausts'), lthy') = Variable.import true exhausts lthy |
287 val ((_, exhausts'), lthy') = Variable.import true exhausts lthy |
289 |
288 |
290 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
289 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
294 |> map prop_of |
293 |> map prop_of |
295 |> map Logic.strip_horn |
294 |> map Logic.strip_horn |
296 |> split_list |
295 |> split_list |
297 |>> (map o map) strip_params_prems_concl |
296 |>> (map o map) strip_params_prems_concl |
298 |
297 |
299 val premss = ((map2 o map2) (process_ecase lthy'' c) ecases bclausesss) |
298 val premss = (map2 o map2) (process_ecase lthy'' c) ecases bclausesss |
300 |
299 |
|
300 fun tac bclausess exhaust {prems, context} = |
|
301 case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
|
302 prems bclausess exhaust |
|
303 |
|
304 fun prove prems bclausess exhaust concl = |
|
305 Goal.prove lthy'' [] prems concl (tac bclausess exhaust) |
301 in |
306 in |
302 map2 (fn (prems, bclausess) => fn (exh, concl) => |
307 map4 prove premss bclausesss exhausts' main_concls |
303 Goal.prove lthy'' [] prems concl |
308 |> ProofContext.export lthy'' lthy |
304 (fn {prems: thm list, context} => |
|
305 HEADGOAL (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
|
306 (prems, bclausess) exh) |
|
307 ) |
|
308 ) (premss ~~ bclausesss) (exhausts' ~~ main_concls) |
|
309 |> ProofContext.export lthy'' lthy |
|
310 end |
309 end |
311 *} |
310 *} |
312 |
311 |
313 |
312 |
314 |
313 |
822 val qpermute_bn_thms = |
821 val qpermute_bn_thms = |
823 if get_STEPS lthy > 33 |
822 if get_STEPS lthy > 33 |
824 then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC |
823 then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC |
825 else [] |
824 else [] |
826 |
825 |
827 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms qeq_iffs' |
826 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
828 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
827 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
829 |
828 |
830 |
829 |
831 (* noting the theorems *) |
830 (* noting the theorems *) |
832 |
831 |