179 ML {* |
179 ML {* |
180 fun mk_minimal_ss ctxt = |
180 fun mk_minimal_ss ctxt = |
181 Simplifier.context ctxt empty_ss |
181 Simplifier.context ctxt empty_ss |
182 setsubgoaler asm_simp_tac |
182 setsubgoaler asm_simp_tac |
183 setmksimps (mksimps []) |
183 setmksimps (mksimps []) |
|
184 *} |
|
185 |
|
186 ML {* |
|
187 (* TODO/FIXME not needed anymore? *) |
|
188 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
184 *} |
189 *} |
185 |
190 |
186 section {* atomize *} |
191 section {* atomize *} |
187 |
192 |
188 lemma atomize_eqv[atomize]: |
193 lemma atomize_eqv[atomize]: |
484 raise (LIFT_MATCH "regularize (default)") |
489 raise (LIFT_MATCH "regularize (default)") |
485 *} |
490 *} |
486 |
491 |
487 ML {* |
492 ML {* |
488 fun equiv_tac ctxt = |
493 fun equiv_tac ctxt = |
489 REPEAT_ALL_NEW (FIRST' |
494 (K (print_tac "equiv tac")) THEN' |
490 [resolve_tac (equiv_rules_get ctxt)]) |
495 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
491 *} |
496 *} |
492 |
497 |
493 ML {* |
498 ML {* |
494 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
499 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
495 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
500 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
575 val thy = ProofContext.theory_of ctxt |
580 val thy = ProofContext.theory_of ctxt |
576 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
581 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
577 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
582 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
578 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
583 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
579 val simpset = (mk_minimal_ss ctxt) |
584 val simpset = (mk_minimal_ss ctxt) |
580 addsimps @{thms ball_reg_eqv bex_reg_eqv} |
585 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv} |
581 addsimprocs [simproc] addSolver equiv_solver |
586 addsimprocs [simproc] addSolver equiv_solver |
582 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
587 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
|
588 (* can this cause loops in equiv_tac ? *) |
583 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
589 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
584 in |
590 in |
585 ObjectLogic.full_atomize_tac THEN' |
591 ObjectLogic.full_atomize_tac THEN' |
586 simp_tac simpset THEN' |
592 simp_tac simpset THEN' |
587 REPEAT_ALL_NEW (FIRST' [ |
593 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
588 rtac @{thm ball_reg_right}, |
594 rtac @{thm ball_reg_right}, |
589 rtac @{thm bex_reg_left}, |
595 rtac @{thm bex_reg_left}, |
590 resolve_tac (Inductive.get_monos ctxt), |
596 resolve_tac (Inductive.get_monos ctxt), |
591 rtac @{thm ball_all_comm}, |
597 rtac @{thm ball_all_comm}, |
592 rtac @{thm bex_ex_comm}, |
598 rtac @{thm bex_ex_comm}, |
593 resolve_tac eq_eqvs, |
599 resolve_tac eq_eqvs, |
|
600 (* should be equivalent to the above, but causes loops: *) |
|
601 (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *) |
594 simp_tac simpset]) |
602 simp_tac simpset]) |
595 end |
603 end |
596 *} |
604 *} |
597 |
605 |
598 section {* Injections of rep and abses *} |
606 section {* Injections of rep and abses *} |
845 compose_tac (false, thm, 2) 1 |
853 compose_tac (false, thm, 2) 1 |
846 end |
854 end |
847 end |
855 end |
848 handle ERROR "find_qt_asm: no pair" => no_tac) |
856 handle ERROR "find_qt_asm: no pair" => no_tac) |
849 | _ => no_tac) |
857 | _ => no_tac) |
850 *} |
|
851 ML {* |
|
852 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
|
853 *} |
858 *} |
854 |
859 |
855 ML {* |
860 ML {* |
856 fun rep_abs_rsp_tac ctxt = |
861 fun rep_abs_rsp_tac ctxt = |
857 SUBGOAL (fn (goal, i) => |
862 SUBGOAL (fn (goal, i) => |