equal
deleted
inserted
replaced
6 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} |
6 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} |
7 |
7 |
8 theory Int |
8 theory Int |
9 imports Equiv_Relations Wellfounded |
9 imports Equiv_Relations Wellfounded |
10 uses |
10 uses |
11 ("Tools/numeral.ML") |
|
12 ("Tools/int_arith.ML") |
11 ("Tools/int_arith.ML") |
13 begin |
12 begin |
14 |
13 |
15 subsection {* The equivalence relation underlying the integers *} |
14 subsection {* The equivalence relation underlying the integers *} |
16 |
15 |
833 mult_minus_left mult_minus_right |
832 mult_minus_left mult_minus_right |
834 minus_add_distrib minus_minus mult_assoc |
833 minus_add_distrib minus_minus mult_assoc |
835 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
834 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
836 of_int_0 of_int_1 of_int_add of_int_mult |
835 of_int_0 of_int_1 of_int_add of_int_mult |
837 |
836 |
838 use "Tools/numeral.ML" |
|
839 use "Tools/int_arith.ML" |
837 use "Tools/int_arith.ML" |
840 declaration {* K Int_Arith.setup *} |
838 declaration {* K Int_Arith.setup *} |
841 |
839 |
842 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | |
840 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | |
843 "(m::'a::linordered_idom) <= n" | |
841 "(m::'a::linordered_idom) <= n" | |