789 |
789 |
790 |
790 |
791 (* merge *) (*NOTE: ignores some fields of 2nd simpset*) |
791 (* merge *) (*NOTE: ignores some fields of 2nd simpset*) |
792 |
792 |
793 fun merge_ss (ss1, ss2) = |
793 fun merge_ss (ss1, ss2) = |
794 let |
794 if pointer_eq (ss1, ss2) then ss1 |
795 val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _}, |
795 else |
796 {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, |
796 let |
797 loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; |
797 val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _}, |
798 val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, |
798 {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, |
799 {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
799 loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; |
800 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; |
800 val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, |
801 |
801 {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
802 val rules' = Net.merge eq_rrule (rules1, rules2); |
802 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; |
803 val prems' = merge Thm.eq_thm_prop (prems1, prems2); |
803 |
804 val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; |
804 val rules' = Net.merge eq_rrule (rules1, rules2); |
805 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; |
805 val prems' = merge Thm.eq_thm_prop (prems1, prems2); |
806 val congs' = merge (eq_cong o pairself #2) (congs1, congs2); |
806 val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; |
807 val weak' = merge (op =) (weak1, weak2); |
807 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; |
808 val procs' = Net.merge eq_proc (procs1, procs2); |
808 val congs' = merge (eq_cong o pairself #2) (congs1, congs2); |
809 val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); |
809 val weak' = merge (op =) (weak1, weak2); |
810 val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2); |
810 val procs' = Net.merge eq_proc (procs1, procs2); |
811 val solvers' = merge eq_solver (solvers1, solvers2); |
811 val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); |
812 in |
812 val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2); |
813 make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs', |
813 val solvers' = merge eq_solver (solvers1, solvers2); |
814 mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) |
814 in |
815 end; |
815 make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs', |
|
816 mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) |
|
817 end; |
816 |
818 |
817 |
819 |
818 |
820 |
819 (** rewriting **) |
821 (** rewriting **) |
820 |
822 |