author | wenzelm |
Wed, 31 Dec 2008 15:30:10 +0100 | |
changeset 29269 | 5c25a2012975 |
parent 28952 | 15a4b2cf8c34 |
child 30496 | 7cdcc9dd95cb |
permissions | -rw-r--r-- |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28952
diff
changeset
|
1 |
(* Title: HOL/Tools/int_arith1.ML |
23164 | 2 |
Authors: Larry Paulson and Tobias Nipkow |
3 |
||
4 |
Simprocs and decision procedure for linear arithmetic. |
|
5 |
*) |
|
6 |
||
7 |
structure Int_Numeral_Base_Simprocs = |
|
8 |
struct |
|
9 |
fun prove_conv tacs ctxt (_: thm list) (t, u) = |
|
10 |
if t aconv u then NONE |
|
11 |
else |
|
12 |
let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
|
13 |
in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end |
|
14 |
||
15 |
fun prove_conv_nohyps tacs sg = prove_conv tacs sg []; |
|
16 |
||
17 |
fun prep_simproc (name, pats, proc) = |
|
18 |
Simplifier.simproc (the_context()) name pats proc; |
|
19 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
20 |
fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true |
23164 | 21 |
| is_numeral _ = false |
22 |
||
23 |
fun simplify_meta_eq f_number_of_eq f_eq = |
|
24 |
mk_meta_eq ([f_eq, f_number_of_eq] MRS trans) |
|
25 |
||
26 |
(*reorientation simprules using ==, for the following simproc*) |
|
23881 | 27 |
val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection |
28 |
val meta_one_reorient = @{thm one_reorient} RS eq_reflection |
|
25481 | 29 |
val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection |
23164 | 30 |
|
31 |
(*reorientation simplification procedure: reorients (polymorphic) |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
32 |
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*) |
23164 | 33 |
fun reorient_proc sg _ (_ $ t $ u) = |
34 |
case u of |
|
25481 | 35 |
Const(@{const_name HOL.zero}, _) => NONE |
23164 | 36 |
| Const(@{const_name HOL.one}, _) => NONE |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
37 |
| Const(@{const_name Int.number_of}, _) $ _ => NONE |
23164 | 38 |
| _ => SOME (case t of |
25481 | 39 |
Const(@{const_name HOL.zero}, _) => meta_zero_reorient |
40 |
| Const(@{const_name HOL.one}, _) => meta_one_reorient |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
41 |
| Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient) |
23164 | 42 |
|
43 |
val reorient_simproc = |
|
44 |
prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc) |
|
45 |
||
46 |
end; |
|
47 |
||
48 |
||
49 |
Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc]; |
|
50 |
||
51 |
||
52 |
structure Int_Numeral_Simprocs = |
|
53 |
struct |
|
54 |
||
55 |
(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs |
|
56 |
isn't complicated by the abstract 0 and 1.*) |
|
25481 | 57 |
val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; |
23164 | 58 |
|
59 |
(** New term ordering so that AC-rewriting brings numerals to the front **) |
|
60 |
||
61 |
(*Order integers by absolute value and then by sign. The standard integer |
|
62 |
ordering is not well-founded.*) |
|
63 |
fun num_ord (i,j) = |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
64 |
(case int_ord (abs i, abs j) of |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
65 |
EQUAL => int_ord (Int.sign i, Int.sign j) |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
66 |
| ord => ord); |
23164 | 67 |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28952
diff
changeset
|
68 |
(*This resembles TermOrd.term_ord, but it puts binary numerals before other |
23164 | 69 |
non-atomic terms.*) |
70 |
local open Term |
|
71 |
in |
|
72 |
fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28952
diff
changeset
|
73 |
(case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) |
23164 | 74 |
| numterm_ord |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
75 |
(Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) = |
23164 | 76 |
num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
77 |
| numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
78 |
| numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER |
23164 | 79 |
| numterm_ord (t, u) = |
80 |
(case int_ord (size_of_term t, size_of_term u) of |
|
81 |
EQUAL => |
|
82 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28952
diff
changeset
|
83 |
(case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) |
23164 | 84 |
end |
85 |
| ord => ord) |
|
86 |
and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) |
|
87 |
end; |
|
88 |
||
89 |
fun numtermless tu = (numterm_ord tu = LESS); |
|
90 |
||
91 |
(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*) |
|
92 |
val num_ss = HOL_ss settermless numtermless; |
|
93 |
||
94 |
||
95 |
(** Utilities **) |
|
96 |
||
97 |
fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; |
|
98 |
||
99 |
fun find_first_numeral past (t::terms) = |
|
100 |
((snd (HOLogic.dest_number t), rev past @ terms) |
|
101 |
handle TERM _ => find_first_numeral (t::past) terms) |
|
102 |
| find_first_numeral past [] = raise TERM("find_first_numeral", []); |
|
103 |
||
104 |
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; |
|
105 |
||
106 |
fun mk_minus t = |
|
107 |
let val T = Term.fastype_of t |
|
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
108 |
in Const (@{const_name HOL.uminus}, T --> T) $ t end; |
23164 | 109 |
|
110 |
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
|
111 |
fun mk_sum T [] = mk_number T 0 |
|
112 |
| mk_sum T [t,u] = mk_plus (t, u) |
|
113 |
| mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
|
114 |
||
115 |
(*this version ALWAYS includes a trailing zero*) |
|
116 |
fun long_mk_sum T [] = mk_number T 0 |
|
117 |
| long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
|
118 |
||
119 |
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; |
|
120 |
||
121 |
(*decompose additions AND subtractions as a sum*) |
|
122 |
fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = |
|
123 |
dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
124 |
| dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = |
|
125 |
dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
126 |
| dest_summing (pos, t, ts) = |
|
127 |
if pos then t::ts else mk_minus t :: ts; |
|
128 |
||
129 |
fun dest_sum t = dest_summing (true, t, []); |
|
130 |
||
131 |
val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; |
|
132 |
val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; |
|
133 |
||
134 |
val mk_times = HOLogic.mk_binop @{const_name HOL.times}; |
|
135 |
||
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
136 |
fun one_of T = Const(@{const_name HOL.one},T); |
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
137 |
|
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
138 |
(* build product with trailing 1 rather than Numeral 1 in order to avoid the |
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
139 |
unnecessary restriction to type class number_ring |
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
140 |
which is not required for cancellation of common factors in divisions. |
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
141 |
*) |
23164 | 142 |
fun mk_prod T = |
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
143 |
let val one = one_of T |
23164 | 144 |
fun mk [] = one |
145 |
| mk [t] = t |
|
146 |
| mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) |
|
147 |
in mk end; |
|
148 |
||
149 |
(*This version ALWAYS includes a trailing one*) |
|
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
150 |
fun long_mk_prod T [] = one_of T |
23164 | 151 |
| long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); |
152 |
||
153 |
val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; |
|
154 |
||
155 |
fun dest_prod t = |
|
156 |
let val (t,u) = dest_times t |
|
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
157 |
in dest_prod t @ dest_prod u end |
23164 | 158 |
handle TERM _ => [t]; |
159 |
||
160 |
(*DON'T do the obvious simplifications; that would create special cases*) |
|
161 |
fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); |
|
162 |
||
163 |
(*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
164 |
fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t |
|
165 |
| dest_coeff sign t = |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28952
diff
changeset
|
166 |
let val ts = sort TermOrd.term_ord (dest_prod t) |
23164 | 167 |
val (n, ts') = find_first_numeral [] ts |
168 |
handle TERM _ => (1, ts) |
|
169 |
in (sign*n, mk_prod (Term.fastype_of t) ts') end; |
|
170 |
||
171 |
(*Find first coefficient-term THAT MATCHES u*) |
|
172 |
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
173 |
| find_first_coeff past u (t::terms) = |
|
174 |
let val (n,u') = dest_coeff 1 t |
|
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
175 |
in if u aconv u' then (n, rev past @ terms) |
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
176 |
else find_first_coeff (t::past) u terms |
23164 | 177 |
end |
178 |
handle TERM _ => find_first_coeff (t::past) u terms; |
|
179 |
||
180 |
(*Fractions as pairs of ints. Can't use Rat.rat because the representation |
|
181 |
needs to preserve negative values in the denominator.*) |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
182 |
fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); |
23164 | 183 |
|
184 |
(*Don't reduce fractions; sums must be proved by rule add_frac_eq. |
|
185 |
Fractions are reduced later by the cancel_numeral_factor simproc.*) |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
186 |
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); |
23164 | 187 |
|
188 |
val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; |
|
189 |
||
190 |
(*Build term (p / q) * t*) |
|
191 |
fun mk_fcoeff ((p, q), t) = |
|
192 |
let val T = Term.fastype_of t |
|
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
193 |
in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; |
23164 | 194 |
|
195 |
(*Express t as a product of a fraction with other sorted terms*) |
|
196 |
fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t |
|
197 |
| dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) = |
|
198 |
let val (p, t') = dest_coeff sign t |
|
199 |
val (q, u') = dest_coeff 1 u |
|
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
200 |
in (mk_frac (p, q), mk_divide (t', u')) end |
23164 | 201 |
| dest_fcoeff sign t = |
202 |
let val (p, t') = dest_coeff sign t |
|
203 |
val T = Term.fastype_of t |
|
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
204 |
in (mk_frac (p, 1), mk_divide (t', one_of T)) end; |
23164 | 205 |
|
206 |
||
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
207 |
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) |
23164 | 208 |
val add_0s = thms "add_0s"; |
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23365
diff
changeset
|
209 |
val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"]; |
23164 | 210 |
|
211 |
(*Simplify inverse Numeral1, a/Numeral1*) |
|
212 |
val inverse_1s = [@{thm inverse_numeral_1}]; |
|
213 |
val divide_1s = [@{thm divide_numeral_1}]; |
|
214 |
||
215 |
(*To perform binary arithmetic. The "left" rewriting handles patterns |
|
216 |
created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *) |
|
25481 | 217 |
val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym, |
218 |
@{thm add_number_of_left}, @{thm mult_number_of_left}] @ |
|
219 |
@{thms arith_simps} @ @{thms rel_simps}; |
|
23164 | 220 |
|
221 |
(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms |
|
222 |
during re-arrangement*) |
|
223 |
val non_add_simps = |
|
25481 | 224 |
subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps; |
23164 | 225 |
|
226 |
(*To evaluate binary negations of coefficients*) |
|
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
25919
diff
changeset
|
227 |
val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @ |
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
25919
diff
changeset
|
228 |
@{thms minus_bin_simps} @ @{thms pred_bin_simps}; |
23164 | 229 |
|
230 |
(*To let us treat subtraction as addition*) |
|
231 |
val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; |
|
232 |
||
233 |
(*To let us treat division as multiplication*) |
|
234 |
val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; |
|
235 |
||
236 |
(*push the unary minus down: - x * y = x * - y *) |
|
237 |
val minus_mult_eq_1_to_2 = |
|
238 |
[@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard; |
|
239 |
||
240 |
(*to extract again any uncancelled minuses*) |
|
241 |
val minus_from_mult_simps = |
|
242 |
[@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym]; |
|
243 |
||
244 |
(*combine unary minus with numeric literals, however nested within a product*) |
|
245 |
val mult_minus_simps = |
|
246 |
[@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; |
|
247 |
||
248 |
(*Apply the given rewrite (if present) just once*) |
|
249 |
fun trans_tac NONE = all_tac |
|
250 |
| trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); |
|
251 |
||
252 |
fun simplify_meta_eq rules = |
|
253 |
let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules |
|
254 |
in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end |
|
255 |
||
256 |
structure CancelNumeralsCommon = |
|
257 |
struct |
|
258 |
val mk_sum = mk_sum |
|
259 |
val dest_sum = dest_sum |
|
260 |
val mk_coeff = mk_coeff |
|
261 |
val dest_coeff = dest_coeff 1 |
|
262 |
val find_first_coeff = find_first_coeff [] |
|
263 |
val trans_tac = fn _ => trans_tac |
|
264 |
||
265 |
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ |
|
23881 | 266 |
diff_simps @ minus_simps @ @{thms add_ac} |
23164 | 267 |
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps |
23881 | 268 |
val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} |
23164 | 269 |
fun norm_tac ss = |
270 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
271 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
272 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
273 |
||
274 |
val numeral_simp_ss = HOL_ss addsimps add_0s @ simps |
|
275 |
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
276 |
val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s) |
|
277 |
end; |
|
278 |
||
279 |
||
280 |
structure EqCancelNumerals = CancelNumeralsFun |
|
281 |
(open CancelNumeralsCommon |
|
282 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
283 |
val mk_bal = HOLogic.mk_eq |
|
284 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
|
25481 | 285 |
val bal_add1 = @{thm eq_add_iff1} RS trans |
286 |
val bal_add2 = @{thm eq_add_iff2} RS trans |
|
23164 | 287 |
); |
288 |
||
289 |
structure LessCancelNumerals = CancelNumeralsFun |
|
290 |
(open CancelNumeralsCommon |
|
291 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
23881 | 292 |
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} |
293 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT |
|
25481 | 294 |
val bal_add1 = @{thm less_add_iff1} RS trans |
295 |
val bal_add2 = @{thm less_add_iff2} RS trans |
|
23164 | 296 |
); |
297 |
||
298 |
structure LeCancelNumerals = CancelNumeralsFun |
|
299 |
(open CancelNumeralsCommon |
|
300 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
23881 | 301 |
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} |
302 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT |
|
25481 | 303 |
val bal_add1 = @{thm le_add_iff1} RS trans |
304 |
val bal_add2 = @{thm le_add_iff2} RS trans |
|
23164 | 305 |
); |
306 |
||
307 |
val cancel_numerals = |
|
308 |
map Int_Numeral_Base_Simprocs.prep_simproc |
|
309 |
[("inteq_cancel_numerals", |
|
310 |
["(l::'a::number_ring) + m = n", |
|
311 |
"(l::'a::number_ring) = m + n", |
|
312 |
"(l::'a::number_ring) - m = n", |
|
313 |
"(l::'a::number_ring) = m - n", |
|
314 |
"(l::'a::number_ring) * m = n", |
|
315 |
"(l::'a::number_ring) = m * n"], |
|
316 |
K EqCancelNumerals.proc), |
|
317 |
("intless_cancel_numerals", |
|
318 |
["(l::'a::{ordered_idom,number_ring}) + m < n", |
|
319 |
"(l::'a::{ordered_idom,number_ring}) < m + n", |
|
320 |
"(l::'a::{ordered_idom,number_ring}) - m < n", |
|
321 |
"(l::'a::{ordered_idom,number_ring}) < m - n", |
|
322 |
"(l::'a::{ordered_idom,number_ring}) * m < n", |
|
323 |
"(l::'a::{ordered_idom,number_ring}) < m * n"], |
|
324 |
K LessCancelNumerals.proc), |
|
325 |
("intle_cancel_numerals", |
|
326 |
["(l::'a::{ordered_idom,number_ring}) + m <= n", |
|
327 |
"(l::'a::{ordered_idom,number_ring}) <= m + n", |
|
328 |
"(l::'a::{ordered_idom,number_ring}) - m <= n", |
|
329 |
"(l::'a::{ordered_idom,number_ring}) <= m - n", |
|
330 |
"(l::'a::{ordered_idom,number_ring}) * m <= n", |
|
331 |
"(l::'a::{ordered_idom,number_ring}) <= m * n"], |
|
332 |
K LeCancelNumerals.proc)]; |
|
333 |
||
334 |
||
335 |
structure CombineNumeralsData = |
|
336 |
struct |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
337 |
type coeff = int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
338 |
val iszero = (fn x => x = 0) |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
339 |
val add = op + |
23164 | 340 |
val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) |
341 |
val dest_sum = dest_sum |
|
342 |
val mk_coeff = mk_coeff |
|
343 |
val dest_coeff = dest_coeff 1 |
|
25481 | 344 |
val left_distrib = @{thm combine_common_factor} RS trans |
23164 | 345 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps |
346 |
val trans_tac = fn _ => trans_tac |
|
347 |
||
348 |
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ |
|
23881 | 349 |
diff_simps @ minus_simps @ @{thms add_ac} |
23164 | 350 |
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps |
23881 | 351 |
val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} |
23164 | 352 |
fun norm_tac ss = |
353 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
354 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
355 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
356 |
||
357 |
val numeral_simp_ss = HOL_ss addsimps add_0s @ simps |
|
358 |
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
359 |
val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s) |
|
360 |
end; |
|
361 |
||
362 |
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
363 |
||
364 |
(*Version for fields, where coefficients can be fractions*) |
|
365 |
structure FieldCombineNumeralsData = |
|
366 |
struct |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
367 |
type coeff = int * int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24266
diff
changeset
|
368 |
val iszero = (fn (p, q) => p = 0) |
23164 | 369 |
val add = add_frac |
370 |
val mk_sum = long_mk_sum |
|
371 |
val dest_sum = dest_sum |
|
372 |
val mk_coeff = mk_fcoeff |
|
373 |
val dest_coeff = dest_fcoeff 1 |
|
25481 | 374 |
val left_distrib = @{thm combine_common_factor} RS trans |
23164 | 375 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps |
376 |
val trans_tac = fn _ => trans_tac |
|
377 |
||
378 |
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ |
|
23881 | 379 |
inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac} |
23164 | 380 |
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps |
23881 | 381 |
val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} |
23164 | 382 |
fun norm_tac ss = |
383 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
384 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
385 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
386 |
||
387 |
val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] |
|
388 |
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
389 |
val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s @ divide_1s) |
|
390 |
end; |
|
391 |
||
392 |
structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); |
|
393 |
||
394 |
val combine_numerals = |
|
395 |
Int_Numeral_Base_Simprocs.prep_simproc |
|
396 |
("int_combine_numerals", |
|
397 |
["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], |
|
398 |
K CombineNumerals.proc); |
|
399 |
||
400 |
val field_combine_numerals = |
|
401 |
Int_Numeral_Base_Simprocs.prep_simproc |
|
402 |
("field_combine_numerals", |
|
403 |
["(i::'a::{number_ring,field,division_by_zero}) + j", |
|
404 |
"(i::'a::{number_ring,field,division_by_zero}) - j"], |
|
405 |
K FieldCombineNumerals.proc); |
|
406 |
||
407 |
end; |
|
408 |
||
409 |
Addsimprocs Int_Numeral_Simprocs.cancel_numerals; |
|
410 |
Addsimprocs [Int_Numeral_Simprocs.combine_numerals]; |
|
411 |
Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals]; |
|
412 |
||
413 |
(*examples: |
|
414 |
print_depth 22; |
|
415 |
set timing; |
|
416 |
set trace_simp; |
|
417 |
fun test s = (Goal s, by (Simp_tac 1)); |
|
418 |
||
419 |
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; |
|
420 |
||
421 |
test "2*u = (u::int)"; |
|
422 |
test "(i + j + 12 + (k::int)) - 15 = y"; |
|
423 |
test "(i + j + 12 + (k::int)) - 5 = y"; |
|
424 |
||
425 |
test "y - b < (b::int)"; |
|
426 |
test "y - (3*b + c) < (b::int) - 2*c"; |
|
427 |
||
428 |
test "(2*x - (u*v) + y) - v*3*u = (w::int)"; |
|
429 |
test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"; |
|
430 |
test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"; |
|
431 |
test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"; |
|
432 |
||
433 |
test "(i + j + 12 + (k::int)) = u + 15 + y"; |
|
434 |
test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; |
|
435 |
||
436 |
test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"; |
|
437 |
||
438 |
test "a + -(b+c) + b = (d::int)"; |
|
439 |
test "a + -(b+c) - b = (d::int)"; |
|
440 |
||
441 |
(*negative numerals*) |
|
442 |
test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"; |
|
443 |
test "(i + j + -3 + (k::int)) < u + 5 + y"; |
|
444 |
test "(i + j + 3 + (k::int)) < u + -6 + y"; |
|
445 |
test "(i + j + -12 + (k::int)) - 15 = y"; |
|
446 |
test "(i + j + 12 + (k::int)) - -15 = y"; |
|
447 |
test "(i + j + -12 + (k::int)) - -15 = y"; |
|
448 |
*) |
|
449 |
||
450 |
||
451 |
(** Constant folding for multiplication in semirings **) |
|
452 |
||
453 |
(*We do not need folding for addition: combine_numerals does the same thing*) |
|
454 |
||
455 |
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = |
|
456 |
struct |
|
23881 | 457 |
val assoc_ss = HOL_ss addsimps @{thms mult_ac} |
23164 | 458 |
val eq_reflection = eq_reflection |
459 |
end; |
|
460 |
||
461 |
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); |
|
462 |
||
463 |
val assoc_fold_simproc = |
|
464 |
Int_Numeral_Base_Simprocs.prep_simproc |
|
465 |
("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], |
|
466 |
K Semiring_Times_Assoc.proc); |
|
467 |
||
468 |
Addsimprocs [assoc_fold_simproc]; |
|
469 |
||
470 |
||
471 |
||
472 |
||
473 |
(*** decision procedure for linear arithmetic ***) |
|
474 |
||
475 |
(*---------------------------------------------------------------------------*) |
|
476 |
(* Linear arithmetic *) |
|
477 |
(*---------------------------------------------------------------------------*) |
|
478 |
||
479 |
(* |
|
480 |
Instantiation of the generic linear arithmetic package for int. |
|
481 |
*) |
|
482 |
||
483 |
(* Update parameters of arithmetic prover *) |
|
484 |
local |
|
485 |
||
24266
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
486 |
(* reduce contradictory =/</<= to False *) |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
487 |
|
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
488 |
(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<", |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
489 |
and m and n are ground terms over rings (roughly speaking). |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
490 |
That is, m and n consist only of 1s combined with "+", "-" and "*". |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
491 |
*) |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
492 |
local |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
493 |
val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0}; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
494 |
val lhss0 = [@{cpat "0::?'a::ring"}]; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
495 |
fun proc0 phi ss ct = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
496 |
let val T = ctyp_of_term ct |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
497 |
in if typ_of T = @{typ int} then NONE else |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
498 |
SOME (instantiate' [SOME T] [] zeroth) |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
499 |
end; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
500 |
val zero_to_of_int_zero_simproc = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
501 |
make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc", |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
502 |
proc = proc0, identifier = []}; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
503 |
|
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
504 |
val oneth = (symmetric o mk_meta_eq) @{thm of_int_1}; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
505 |
val lhss1 = [@{cpat "1::?'a::ring_1"}]; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
506 |
fun proc1 phi ss ct = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
507 |
let val T = ctyp_of_term ct |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
508 |
in if typ_of T = @{typ int} then NONE else |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
509 |
SOME (instantiate' [SOME T] [] oneth) |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
510 |
end; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
511 |
val one_to_of_int_one_simproc = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
512 |
make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc", |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
513 |
proc = proc1, identifier = []}; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
514 |
|
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
515 |
val allowed_consts = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
516 |
[@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
517 |
@{const_name "HOL.minus"}, @{const_name "HOL.plus"}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
518 |
@{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
519 |
@{const_name "HOL.less_eq"}]; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
520 |
|
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
521 |
fun check t = case t of |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
522 |
Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int}) |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
523 |
else s mem_string allowed_consts |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
524 |
| a$b => check a andalso check b |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
525 |
| _ => false; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
526 |
|
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
527 |
val conv = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
528 |
Simplifier.rewrite |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
529 |
(HOL_basic_ss addsimps |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
530 |
((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
531 |
@{thm of_int_diff}, @{thm of_int_minus}])@ |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
532 |
[@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}]) |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
533 |
addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]); |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
534 |
|
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
535 |
fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
536 |
val lhss' = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
537 |
[@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
538 |
@{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
539 |
@{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}] |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
540 |
in |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
541 |
val zero_one_idom_simproc = |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
542 |
make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
543 |
proc = sproc, identifier = []} |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
544 |
end; |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
545 |
|
23164 | 546 |
val add_rules = |
25481 | 547 |
simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @ |
23164 | 548 |
[@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}, |
549 |
@{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus}, |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset
|
550 |
@{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}, |
23164 | 551 |
@{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym, |
552 |
@{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc}, |
|
23365 | 553 |
@{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add}, |
554 |
@{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, |
|
555 |
@{thm of_int_mult}] |
|
23164 | 556 |
|
23365 | 557 |
val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] |
23164 | 558 |
|
24266
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
559 |
val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc |
23164 | 560 |
:: Int_Numeral_Simprocs.combine_numerals |
561 |
:: Int_Numeral_Simprocs.cancel_numerals; |
|
562 |
||
563 |
in |
|
564 |
||
565 |
val int_arith_setup = |
|
24093 | 566 |
LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
23164 | 567 |
{add_mono_thms = add_mono_thms, |
568 |
mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms, |
|
569 |
inj_thms = nat_inj_thms @ inj_thms, |
|
25481 | 570 |
lessD = lessD @ [@{thm zless_imp_add1_zle}], |
23164 | 571 |
neqE = neqE, |
572 |
simpset = simpset addsimps add_rules |
|
573 |
addsimprocs Int_Numeral_Base_Simprocs |
|
574 |
addcongs [if_weak_cong]}) #> |
|
24196 | 575 |
arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #> |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset
|
576 |
arith_discrete @{type_name Int.int} |
23164 | 577 |
|
578 |
end; |
|
579 |
||
580 |
val fast_int_arith_simproc = |
|
28262
aa7ca36d67fd
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents:
26086
diff
changeset
|
581 |
Simplifier.simproc (the_context ()) |
23164 | 582 |
"fast_int_arith" |
583 |
["(m::'a::{ordered_idom,number_ring}) < n", |
|
584 |
"(m::'a::{ordered_idom,number_ring}) <= n", |
|
24093 | 585 |
"(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc); |
23164 | 586 |
|
587 |
Addsimprocs [fast_int_arith_simproc]; |