586 addsimprocs [simproc] addSolver equiv_solver |
586 addsimprocs [simproc] addSolver equiv_solver |
587 (* 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 ? *) |
588 (* can this cause loops in equiv_tac ? *) |
589 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) |
590 in |
590 in |
591 ObjectLogic.full_atomize_tac THEN' |
|
592 simp_tac simpset THEN' |
591 simp_tac simpset THEN' |
593 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
592 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
594 rtac @{thm ball_reg_right}, |
593 rtac @{thm ball_reg_right}, |
595 rtac @{thm bex_reg_left}, |
594 rtac @{thm bex_reg_left}, |
596 resolve_tac (Inductive.get_monos ctxt), |
595 resolve_tac (Inductive.get_monos ctxt), |
597 rtac @{thm ball_all_comm}, |
596 rtac @{thm ball_all_comm}, |
598 rtac @{thm bex_ex_comm}, |
597 rtac @{thm bex_ex_comm}, |
599 resolve_tac eq_eqvs, |
598 resolve_tac eq_eqvs, |
600 (* should be equivalent to the above, but causes loops: *) |
599 (* should be equivalent to the above, but causes loops: *) |
601 (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *) |
600 (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *) |
|
601 (* the culprit is aslread rtac @{thm eq_imp_rel} *) |
602 simp_tac simpset]) |
602 simp_tac simpset]) |
603 end |
603 end |
604 *} |
604 *} |
605 |
605 |
606 section {* Injections of rep and abses *} |
606 section {* Injections of rep and abses *} |