equal
deleted
inserted
replaced
5 |
5 |
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 Quotient |
9 imports Equiv_Relations Wellfounded Quotient |
10 uses |
|
11 ("Tools/int_arith.ML") |
|
12 begin |
10 begin |
13 |
11 |
14 subsection {* Definition of integers as a quotient type *} |
12 subsection {* Definition of integers as a quotient type *} |
15 |
13 |
16 definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where |
14 definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where |
717 mult_minus_left mult_minus_right |
715 mult_minus_left mult_minus_right |
718 minus_add_distrib minus_minus mult_assoc |
716 minus_add_distrib minus_minus mult_assoc |
719 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
717 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
720 of_int_0 of_int_1 of_int_add of_int_mult |
718 of_int_0 of_int_1 of_int_add of_int_mult |
721 |
719 |
722 use "Tools/int_arith.ML" |
720 ML_file "Tools/int_arith.ML" |
723 declaration {* K Int_Arith.setup *} |
721 declaration {* K Int_Arith.setup *} |
724 |
722 |
725 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | |
723 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | |
726 "(m::'a::linordered_idom) <= n" | |
724 "(m::'a::linordered_idom) <= n" | |
727 "(m::'a::linordered_idom) = n") = |
725 "(m::'a::linordered_idom) = n") = |