equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 signature INT_ARITH = |
6 signature INT_ARITH = |
7 sig |
7 sig |
8 val setup: Context.generic -> Context.generic |
8 val setup: Context.generic -> Context.generic |
9 val global_setup: theory -> theory |
|
10 end |
9 end |
11 |
10 |
12 structure Int_Arith : INT_ARITH = |
11 structure Int_Arith : INT_ARITH = |
13 struct |
12 struct |
14 |
13 |
76 |
75 |
77 val zero_one_idom_simproc = |
76 val zero_one_idom_simproc = |
78 make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", |
77 make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", |
79 proc = sproc, identifier = []} |
78 proc = sproc, identifier = []} |
80 |
79 |
81 val fast_int_arith_simproc = |
|
82 Simplifier.simproc_global @{theory} "fast_int_arith" |
|
83 ["(m::'a::{linordered_idom,number_ring}) < n", |
|
84 "(m::'a::{linordered_idom,number_ring}) <= n", |
|
85 "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc); |
|
86 |
|
87 val global_setup = |
|
88 Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]); |
|
89 |
|
90 |
|
91 fun number_of thy T n = |
80 fun number_of thy T n = |
92 if not (Sign.of_sort thy (T, @{sort number})) |
81 if not (Sign.of_sort thy (T, @{sort number})) |
93 then raise CTERM ("number_of", []) |
82 then raise CTERM ("number_of", []) |
94 else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; |
83 else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; |
95 |
84 |