69 |
69 |
70 fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE |
70 fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE |
71 |
71 |
72 val lhss' = |
72 val lhss' = |
73 [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"}, |
73 [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"}, |
74 @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"}, |
74 @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"}, |
75 @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}] |
75 @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}] |
76 |
76 |
77 val zero_one_idom_simproc = |
77 val zero_one_idom_simproc = |
78 make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", |
78 make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", |
79 proc = sproc, identifier = []} |
79 proc = sproc, identifier = []} |
80 |
80 |
81 val fast_int_arith_simproc = |
81 val fast_int_arith_simproc = |
82 Simplifier.simproc @{theory} "fast_int_arith" |
82 Simplifier.simproc @{theory} "fast_int_arith" |
83 ["(m::'a::{ordered_idom,number_ring}) < n", |
83 ["(m::'a::{linordered_idom,number_ring}) < n", |
84 "(m::'a::{ordered_idom,number_ring}) <= n", |
84 "(m::'a::{linordered_idom,number_ring}) <= n", |
85 "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc); |
85 "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc); |
86 |
86 |
87 val global_setup = Simplifier.map_simpset |
87 val global_setup = Simplifier.map_simpset |
88 (fn simpset => simpset addsimprocs [fast_int_arith_simproc]); |
88 (fn simpset => simpset addsimprocs [fast_int_arith_simproc]); |
89 |
89 |
90 |
90 |