767 |
767 |
768 val pre_tac = LA_Data.pre_tac; |
768 val pre_tac = LA_Data.pre_tac; |
769 |
769 |
770 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data); |
770 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data); |
771 |
771 |
772 fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = |
772 val add_inj_thms = Fast_Arith.add_inj_thms; |
773 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms, |
773 val add_lessD = Fast_Arith.add_lessD; |
774 lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of}; |
774 val add_simps = Fast_Arith.add_simps; |
775 |
775 val add_simprocs = Fast_Arith.add_simprocs; |
776 fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = |
776 val set_number_of = Fast_Arith.set_number_of; |
777 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, |
|
778 lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of}; |
|
779 |
|
780 fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = |
|
781 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, |
|
782 lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of}; |
|
783 |
|
784 fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = |
|
785 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, |
|
786 lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of}; |
|
787 |
|
788 fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms)); |
|
789 fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm])); |
|
790 fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms)); |
|
791 fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs)); |
|
792 |
|
793 fun set_number_of f = Fast_Arith.map_data (map_number_of (K (serial (), f))) |
|
794 |
|
795 |
777 |
796 fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; |
778 fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; |
797 val lin_arith_tac = Fast_Arith.lin_arith_tac; |
779 val lin_arith_tac = Fast_Arith.lin_arith_tac; |
798 val trace = Fast_Arith.trace; |
780 val trace = Fast_Arith.trace; |
799 |
781 |