281 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
281 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
282 end |
282 end |
283 *} |
283 *} |
284 |
284 |
285 |
285 |
286 |
|
287 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
|
288 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
|
289 ML {* val cheat_supp_eq = Unsynchronized.ref false *} |
|
290 |
|
291 |
|
292 ML {* |
286 ML {* |
293 (* for testing porposes - to exit the procedure early *) |
287 (* for testing porposes - to exit the procedure early *) |
294 exception TEST of Proof.context |
288 exception TEST of Proof.context |
295 |
289 |
296 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10); |
290 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10); |
329 val raw_size_trms = map size_const raw_tys |
323 val raw_size_trms = map size_const raw_tys |
330 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
324 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
331 |> `(fn thms => (length thms) div 2) |
325 |> `(fn thms => (length thms) div 2) |
332 |> uncurry drop |
326 |> uncurry drop |
333 |
327 |
334 (* definitions of raw permutations *) |
328 (* definitions of raw permutations by primitive recursion *) |
335 val _ = warning "Definition of raw permutations"; |
329 val _ = warning "Definition of raw permutations"; |
336 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
330 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
337 if get_STEPS lthy0 > 1 |
331 if get_STEPS lthy0 > 1 |
338 then define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm lthy0 |
332 then define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm lthy0 |
339 else raise TEST lthy0 |
333 else raise TEST lthy0 |
565 val (bns_rsp_pre, lthy9) = fold_map ( |
559 val (bns_rsp_pre, lthy9) = fold_map ( |
566 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
560 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
567 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
561 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
568 val bns_rsp = flat (map snd bns_rsp_pre); |
562 val bns_rsp = flat (map snd bns_rsp_pre); |
569 |
563 |
570 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
564 fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; |
571 else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; |
|
572 |
565 |
573 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
566 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
574 |
567 |
575 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9; |
568 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9; |
576 val (fv_rsp_pre, lthy10) = fold_map |
569 val (fv_rsp_pre, lthy10) = fold_map |
577 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
570 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
578 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9; |
571 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9; |
579 val fv_rsp = flat (map snd fv_rsp_pre); |
572 val fv_rsp = flat (map snd fv_rsp_pre); |
580 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
573 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
581 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
574 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
582 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
575 fun alpha_bn_rsp_tac _ = let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
583 else |
|
584 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
|
585 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
576 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
586 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
577 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
587 fun const_rsp_tac _ = |
578 fun const_rsp_tac _ = |
588 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
579 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
589 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
580 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
654 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
645 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
655 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
646 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
656 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos; |
647 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_trms, qalpha_bn_trms) bn_nos; |
657 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
648 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
658 val _ = warning "Support Equations"; |
649 val _ = warning "Support Equations"; |
659 fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else |
650 fun supp_eq_tac' _ = supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1; |
660 supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1; |
|
661 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => |
651 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => |
662 let val _ = warning ("Support eqs failed") in [] end; |
652 let val _ = warning ("Support eqs failed") in [] end; |
663 val lthy23 = note_suffix "supp" q_supp lthy22; |
653 val lthy23 = note_suffix "supp" q_supp lthy22; |
664 in |
654 in |
665 (0, lthy23) |
655 (0, lthy23) |