wenzelm@9436
|
1 |
(* Title: HOL/Integ/int_arith1.ML
|
wenzelm@9436
|
2 |
ID: $Id$
|
wenzelm@9436
|
3 |
Authors: Larry Paulson and Tobias Nipkow
|
wenzelm@9436
|
4 |
|
wenzelm@9436
|
5 |
Simprocs and decision procedure for linear arithmetic.
|
wenzelm@9436
|
6 |
*)
|
wenzelm@9436
|
7 |
|
paulson@14329
|
8 |
(** Misc ML bindings **)
|
paulson@14329
|
9 |
|
paulson@14272
|
10 |
val NCons_Pls = thm"NCons_Pls";
|
paulson@14272
|
11 |
val NCons_Min = thm"NCons_Min";
|
paulson@14272
|
12 |
val NCons_BIT = thm"NCons_BIT";
|
paulson@14272
|
13 |
val number_of_Pls = thm"number_of_Pls";
|
paulson@14272
|
14 |
val number_of_Min = thm"number_of_Min";
|
paulson@14272
|
15 |
val number_of_BIT = thm"number_of_BIT";
|
paulson@14272
|
16 |
val bin_succ_Pls = thm"bin_succ_Pls";
|
paulson@14272
|
17 |
val bin_succ_Min = thm"bin_succ_Min";
|
paulson@14272
|
18 |
val bin_succ_BIT = thm"bin_succ_BIT";
|
paulson@14272
|
19 |
val bin_pred_Pls = thm"bin_pred_Pls";
|
paulson@14272
|
20 |
val bin_pred_Min = thm"bin_pred_Min";
|
paulson@14272
|
21 |
val bin_pred_BIT = thm"bin_pred_BIT";
|
paulson@14272
|
22 |
val bin_minus_Pls = thm"bin_minus_Pls";
|
paulson@14272
|
23 |
val bin_minus_Min = thm"bin_minus_Min";
|
paulson@14272
|
24 |
val bin_minus_BIT = thm"bin_minus_BIT";
|
paulson@14272
|
25 |
val bin_add_Pls = thm"bin_add_Pls";
|
paulson@14272
|
26 |
val bin_add_Min = thm"bin_add_Min";
|
paulson@14272
|
27 |
val bin_mult_Pls = thm"bin_mult_Pls";
|
paulson@14272
|
28 |
val bin_mult_Min = thm"bin_mult_Min";
|
paulson@14272
|
29 |
val bin_mult_BIT = thm"bin_mult_BIT";
|
paulson@14271
|
30 |
|
paulson@14378
|
31 |
val neg_def = thm "neg_def";
|
paulson@14378
|
32 |
val iszero_def = thm "iszero_def";
|
paulson@14378
|
33 |
|
paulson@14272
|
34 |
val NCons_Pls_0 = thm"NCons_Pls_0";
|
paulson@14272
|
35 |
val NCons_Pls_1 = thm"NCons_Pls_1";
|
paulson@14272
|
36 |
val NCons_Min_0 = thm"NCons_Min_0";
|
paulson@14272
|
37 |
val NCons_Min_1 = thm"NCons_Min_1";
|
paulson@14272
|
38 |
val bin_succ_1 = thm"bin_succ_1";
|
paulson@14272
|
39 |
val bin_succ_0 = thm"bin_succ_0";
|
paulson@14272
|
40 |
val bin_pred_1 = thm"bin_pred_1";
|
paulson@14272
|
41 |
val bin_pred_0 = thm"bin_pred_0";
|
paulson@14272
|
42 |
val bin_minus_1 = thm"bin_minus_1";
|
paulson@14272
|
43 |
val bin_minus_0 = thm"bin_minus_0";
|
paulson@14272
|
44 |
val bin_add_BIT_11 = thm"bin_add_BIT_11";
|
paulson@14272
|
45 |
val bin_add_BIT_10 = thm"bin_add_BIT_10";
|
paulson@14272
|
46 |
val bin_add_BIT_0 = thm"bin_add_BIT_0";
|
paulson@14272
|
47 |
val bin_add_Pls_right = thm"bin_add_Pls_right";
|
paulson@14272
|
48 |
val bin_add_Min_right = thm"bin_add_Min_right";
|
paulson@14272
|
49 |
val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
|
paulson@14272
|
50 |
val bin_mult_1 = thm"bin_mult_1";
|
paulson@14272
|
51 |
val bin_mult_0 = thm"bin_mult_0";
|
paulson@14272
|
52 |
val number_of_NCons = thm"number_of_NCons";
|
paulson@14272
|
53 |
val number_of_succ = thm"number_of_succ";
|
paulson@14272
|
54 |
val number_of_pred = thm"number_of_pred";
|
paulson@14272
|
55 |
val number_of_minus = thm"number_of_minus";
|
paulson@14272
|
56 |
val number_of_add = thm"number_of_add";
|
paulson@14272
|
57 |
val diff_number_of_eq = thm"diff_number_of_eq";
|
paulson@14272
|
58 |
val number_of_mult = thm"number_of_mult";
|
paulson@14272
|
59 |
val double_number_of_BIT = thm"double_number_of_BIT";
|
paulson@14387
|
60 |
val numeral_0_eq_0 = thm"numeral_0_eq_0";
|
paulson@14387
|
61 |
val numeral_1_eq_1 = thm"numeral_1_eq_1";
|
paulson@14387
|
62 |
val numeral_m1_eq_minus_1 = thm"numeral_m1_eq_minus_1";
|
paulson@14387
|
63 |
val mult_minus1 = thm"mult_minus1";
|
paulson@14387
|
64 |
val mult_minus1_right = thm"mult_minus1_right";
|
paulson@14387
|
65 |
val minus_number_of_mult = thm"minus_number_of_mult";
|
paulson@14272
|
66 |
val zero_less_nat_eq = thm"zero_less_nat_eq";
|
paulson@14272
|
67 |
val eq_number_of_eq = thm"eq_number_of_eq";
|
paulson@14272
|
68 |
val iszero_number_of_Pls = thm"iszero_number_of_Pls";
|
paulson@14272
|
69 |
val nonzero_number_of_Min = thm"nonzero_number_of_Min";
|
paulson@14272
|
70 |
val iszero_number_of_BIT = thm"iszero_number_of_BIT";
|
paulson@14272
|
71 |
val iszero_number_of_0 = thm"iszero_number_of_0";
|
paulson@14272
|
72 |
val iszero_number_of_1 = thm"iszero_number_of_1";
|
paulson@14272
|
73 |
val less_number_of_eq_neg = thm"less_number_of_eq_neg";
|
paulson@14387
|
74 |
val le_number_of_eq = thm"le_number_of_eq";
|
paulson@14272
|
75 |
val not_neg_number_of_Pls = thm"not_neg_number_of_Pls";
|
paulson@14272
|
76 |
val neg_number_of_Min = thm"neg_number_of_Min";
|
paulson@14272
|
77 |
val neg_number_of_BIT = thm"neg_number_of_BIT";
|
paulson@14272
|
78 |
val le_number_of_eq_not_less = thm"le_number_of_eq_not_less";
|
paulson@14387
|
79 |
val abs_number_of = thm"abs_number_of";
|
paulson@14272
|
80 |
val number_of_reorient = thm"number_of_reorient";
|
paulson@14272
|
81 |
val add_number_of_left = thm"add_number_of_left";
|
paulson@14272
|
82 |
val mult_number_of_left = thm"mult_number_of_left";
|
paulson@14272
|
83 |
val add_number_of_diff1 = thm"add_number_of_diff1";
|
paulson@14272
|
84 |
val add_number_of_diff2 = thm"add_number_of_diff2";
|
paulson@14272
|
85 |
val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
|
paulson@14272
|
86 |
val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
|
paulson@14272
|
87 |
val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
|
paulson@14271
|
88 |
|
paulson@14272
|
89 |
val NCons_simps = thms"NCons_simps";
|
paulson@14272
|
90 |
val bin_arith_extra_simps = thms"bin_arith_extra_simps";
|
paulson@14272
|
91 |
val bin_arith_simps = thms"bin_arith_simps";
|
paulson@14272
|
92 |
val bin_rel_simps = thms"bin_rel_simps";
|
paulson@11868
|
93 |
|
paulson@14272
|
94 |
val zless_imp_add1_zle = thm "zless_imp_add1_zle";
|
wenzelm@9436
|
95 |
|
paulson@14272
|
96 |
val combine_common_factor = thm"combine_common_factor";
|
paulson@14272
|
97 |
val eq_add_iff1 = thm"eq_add_iff1";
|
paulson@14272
|
98 |
val eq_add_iff2 = thm"eq_add_iff2";
|
paulson@14272
|
99 |
val less_add_iff1 = thm"less_add_iff1";
|
paulson@14272
|
100 |
val less_add_iff2 = thm"less_add_iff2";
|
paulson@14272
|
101 |
val le_add_iff1 = thm"le_add_iff1";
|
paulson@14272
|
102 |
val le_add_iff2 = thm"le_add_iff2";
|
wenzelm@9436
|
103 |
|
paulson@14387
|
104 |
val arith_special = thms"arith_special";
|
wenzelm@9436
|
105 |
|
paulson@14272
|
106 |
structure Bin_Simprocs =
|
paulson@14272
|
107 |
struct
|
paulson@14272
|
108 |
fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
|
paulson@14272
|
109 |
if t aconv u then None
|
paulson@14272
|
110 |
else
|
paulson@14272
|
111 |
let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
|
paulson@14272
|
112 |
in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
|
wenzelm@9436
|
113 |
|
paulson@14272
|
114 |
fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
|
paulson@14272
|
115 |
fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
|
wenzelm@9436
|
116 |
|
paulson@14272
|
117 |
fun prep_simproc (name, pats, proc) =
|
paulson@14272
|
118 |
Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
|
wenzelm@9436
|
119 |
|
paulson@14272
|
120 |
fun is_numeral (Const("Numeral.number_of", _) $ w) = true
|
paulson@14272
|
121 |
| is_numeral _ = false
|
wenzelm@9436
|
122 |
|
paulson@14272
|
123 |
fun simplify_meta_eq f_number_of_eq f_eq =
|
paulson@14272
|
124 |
mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
|
wenzelm@9436
|
125 |
|
paulson@14272
|
126 |
(*reorientation simprules using ==, for the following simproc*)
|
paulson@14272
|
127 |
val meta_zero_reorient = zero_reorient RS eq_reflection
|
paulson@14272
|
128 |
val meta_one_reorient = one_reorient RS eq_reflection
|
paulson@14272
|
129 |
val meta_number_of_reorient = number_of_reorient RS eq_reflection
|
wenzelm@9436
|
130 |
|
paulson@14272
|
131 |
(*reorientation simplification procedure: reorients (polymorphic)
|
paulson@14272
|
132 |
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
|
paulson@14272
|
133 |
fun reorient_proc sg _ (_ $ t $ u) =
|
paulson@14272
|
134 |
case u of
|
paulson@14272
|
135 |
Const("0", _) => None
|
paulson@14272
|
136 |
| Const("1", _) => None
|
paulson@14272
|
137 |
| Const("Numeral.number_of", _) $ _ => None
|
paulson@14272
|
138 |
| _ => Some (case t of
|
paulson@14272
|
139 |
Const("0", _) => meta_zero_reorient
|
paulson@14272
|
140 |
| Const("1", _) => meta_one_reorient
|
paulson@14272
|
141 |
| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
|
wenzelm@9436
|
142 |
|
paulson@14272
|
143 |
val reorient_simproc =
|
paulson@14272
|
144 |
prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
|
wenzelm@9436
|
145 |
|
paulson@14272
|
146 |
end;
|
wenzelm@9436
|
147 |
|
paulson@14272
|
148 |
|
paulson@14387
|
149 |
Addsimps arith_special;
|
paulson@14272
|
150 |
Addsimprocs [Bin_Simprocs.reorient_simproc];
|
wenzelm@9436
|
151 |
|
wenzelm@9436
|
152 |
|
wenzelm@9436
|
153 |
structure Int_Numeral_Simprocs =
|
wenzelm@9436
|
154 |
struct
|
wenzelm@9436
|
155 |
|
paulson@11868
|
156 |
(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
|
paulson@11868
|
157 |
isn't complicated by the abstract 0 and 1.*)
|
paulson@14387
|
158 |
val numeral_syms = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym];
|
paulson@11868
|
159 |
|
paulson@14474
|
160 |
(** New term ordering so that AC-rewriting brings numerals to the front **)
|
paulson@14474
|
161 |
|
paulson@14474
|
162 |
(*Order integers by absolute value and then by sign. The standard integer
|
paulson@14474
|
163 |
ordering is not well-founded.*)
|
paulson@14474
|
164 |
fun num_ord (i,j) =
|
paulson@14474
|
165 |
(case Int.compare (abs i, abs j) of
|
paulson@14474
|
166 |
EQUAL => Int.compare (Int.sign i, Int.sign j)
|
paulson@14474
|
167 |
| ord => ord);
|
paulson@14474
|
168 |
|
paulson@14474
|
169 |
(*This resembles Term.term_ord, but it puts binary numerals before other
|
paulson@14474
|
170 |
non-atomic terms.*)
|
paulson@14474
|
171 |
local open Term
|
paulson@14474
|
172 |
in
|
paulson@14474
|
173 |
fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
|
paulson@14474
|
174 |
(case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
|
paulson@14474
|
175 |
| numterm_ord
|
paulson@14474
|
176 |
(Const("Numeral.number_of", _) $ v, Const("Numeral.number_of", _) $ w) =
|
paulson@14474
|
177 |
num_ord (HOLogic.dest_binum v, HOLogic.dest_binum w)
|
paulson@14474
|
178 |
| numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
|
paulson@14474
|
179 |
| numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
|
paulson@14474
|
180 |
| numterm_ord (t, u) =
|
paulson@14474
|
181 |
(case Int.compare (size_of_term t, size_of_term u) of
|
paulson@14474
|
182 |
EQUAL =>
|
paulson@14474
|
183 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
paulson@14474
|
184 |
(case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
|
paulson@14474
|
185 |
end
|
paulson@14474
|
186 |
| ord => ord)
|
paulson@14474
|
187 |
and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
|
paulson@14474
|
188 |
end;
|
paulson@14474
|
189 |
|
paulson@14474
|
190 |
fun numtermless tu = (numterm_ord tu = LESS);
|
paulson@14474
|
191 |
|
paulson@14474
|
192 |
(*Defined in this file, but perhaps needed only for simprocs of type nat.*)
|
paulson@14474
|
193 |
val num_ss = HOL_ss settermless numtermless;
|
paulson@14474
|
194 |
|
paulson@14474
|
195 |
|
paulson@14474
|
196 |
(** Utilities **)
|
wenzelm@9436
|
197 |
|
paulson@14387
|
198 |
fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_bin n;
|
wenzelm@9436
|
199 |
|
wenzelm@9436
|
200 |
(*Decodes a binary INTEGER*)
|
paulson@11868
|
201 |
fun dest_numeral (Const("0", _)) = 0
|
paulson@11868
|
202 |
| dest_numeral (Const("1", _)) = 1
|
wenzelm@13462
|
203 |
| dest_numeral (Const("Numeral.number_of", _) $ w) =
|
wenzelm@10890
|
204 |
(HOLogic.dest_binum w
|
wenzelm@10890
|
205 |
handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
|
wenzelm@9436
|
206 |
| dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
|
wenzelm@9436
|
207 |
|
wenzelm@9436
|
208 |
fun find_first_numeral past (t::terms) =
|
wenzelm@13462
|
209 |
((dest_numeral t, rev past @ terms)
|
wenzelm@13462
|
210 |
handle TERM _ => find_first_numeral (t::past) terms)
|
wenzelm@9436
|
211 |
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
|
wenzelm@9436
|
212 |
|
wenzelm@9436
|
213 |
val mk_plus = HOLogic.mk_binop "op +";
|
wenzelm@9436
|
214 |
|
paulson@14387
|
215 |
fun mk_minus t =
|
paulson@14387
|
216 |
let val T = Term.fastype_of t
|
paulson@14387
|
217 |
in Const ("uminus", T --> T) $ t
|
paulson@14387
|
218 |
end;
|
wenzelm@9436
|
219 |
|
paulson@11868
|
220 |
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
|
paulson@14387
|
221 |
fun mk_sum T [] = mk_numeral T 0
|
paulson@14387
|
222 |
| mk_sum T [t,u] = mk_plus (t, u)
|
paulson@14387
|
223 |
| mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
|
wenzelm@9436
|
224 |
|
wenzelm@9436
|
225 |
(*this version ALWAYS includes a trailing zero*)
|
paulson@14387
|
226 |
fun long_mk_sum T [] = mk_numeral T 0
|
paulson@14387
|
227 |
| long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
|
wenzelm@9436
|
228 |
|
paulson@14387
|
229 |
val dest_plus = HOLogic.dest_bin "op +" Term.dummyT;
|
wenzelm@9436
|
230 |
|
wenzelm@9436
|
231 |
(*decompose additions AND subtractions as a sum*)
|
wenzelm@9436
|
232 |
fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
|
wenzelm@9436
|
233 |
dest_summing (pos, t, dest_summing (pos, u, ts))
|
wenzelm@9436
|
234 |
| dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
|
wenzelm@9436
|
235 |
dest_summing (pos, t, dest_summing (not pos, u, ts))
|
wenzelm@9436
|
236 |
| dest_summing (pos, t, ts) =
|
paulson@14387
|
237 |
if pos then t::ts else mk_minus t :: ts;
|
wenzelm@9436
|
238 |
|
wenzelm@9436
|
239 |
fun dest_sum t = dest_summing (true, t, []);
|
wenzelm@9436
|
240 |
|
wenzelm@9436
|
241 |
val mk_diff = HOLogic.mk_binop "op -";
|
paulson@14387
|
242 |
val dest_diff = HOLogic.dest_bin "op -" Term.dummyT;
|
wenzelm@9436
|
243 |
|
wenzelm@9436
|
244 |
val mk_times = HOLogic.mk_binop "op *";
|
wenzelm@9436
|
245 |
|
paulson@14387
|
246 |
fun mk_prod T =
|
paulson@14387
|
247 |
let val one = mk_numeral T 1
|
paulson@14387
|
248 |
fun mk [] = one
|
paulson@14387
|
249 |
| mk [t] = t
|
paulson@14387
|
250 |
| mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
|
paulson@14387
|
251 |
in mk end;
|
wenzelm@9436
|
252 |
|
paulson@14387
|
253 |
(*This version ALWAYS includes a trailing one*)
|
paulson@14387
|
254 |
fun long_mk_prod T [] = mk_numeral T 1
|
paulson@14387
|
255 |
| long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
|
paulson@14387
|
256 |
|
paulson@14387
|
257 |
val dest_times = HOLogic.dest_bin "op *" Term.dummyT;
|
wenzelm@9436
|
258 |
|
wenzelm@9436
|
259 |
fun dest_prod t =
|
wenzelm@13462
|
260 |
let val (t,u) = dest_times t
|
wenzelm@9436
|
261 |
in dest_prod t @ dest_prod u end
|
wenzelm@9436
|
262 |
handle TERM _ => [t];
|
wenzelm@9436
|
263 |
|
wenzelm@13462
|
264 |
(*DON'T do the obvious simplifications; that would create special cases*)
|
paulson@14387
|
265 |
fun mk_coeff (k, t) = mk_times (mk_numeral (Term.fastype_of t) k, t);
|
wenzelm@9436
|
266 |
|
wenzelm@9436
|
267 |
(*Express t as a product of (possibly) a numeral with other sorted terms*)
|
wenzelm@9436
|
268 |
fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
|
wenzelm@9436
|
269 |
| dest_coeff sign t =
|
wenzelm@9436
|
270 |
let val ts = sort Term.term_ord (dest_prod t)
|
wenzelm@13462
|
271 |
val (n, ts') = find_first_numeral [] ts
|
wenzelm@9436
|
272 |
handle TERM _ => (1, ts)
|
paulson@14387
|
273 |
in (sign*n, mk_prod (Term.fastype_of t) ts') end;
|
wenzelm@9436
|
274 |
|
wenzelm@9436
|
275 |
(*Find first coefficient-term THAT MATCHES u*)
|
wenzelm@13462
|
276 |
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
|
wenzelm@9436
|
277 |
| find_first_coeff past u (t::terms) =
|
wenzelm@13462
|
278 |
let val (n,u') = dest_coeff 1 t
|
wenzelm@13462
|
279 |
in if u aconv u' then (n, rev past @ terms)
|
wenzelm@13462
|
280 |
else find_first_coeff (t::past) u terms
|
wenzelm@13462
|
281 |
end
|
wenzelm@13462
|
282 |
handle TERM _ => find_first_coeff (t::past) u terms;
|
wenzelm@9436
|
283 |
|
wenzelm@9436
|
284 |
|
paulson@11868
|
285 |
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
|
paulson@14387
|
286 |
val add_0s = thms "add_0s";
|
paulson@14387
|
287 |
val mult_1s = thms "mult_1s";
|
wenzelm@9436
|
288 |
|
paulson@11868
|
289 |
(*To perform binary arithmetic. The "left" rewriting handles patterns
|
paulson@11868
|
290 |
created by the simprocs, such as 3 * (5 * x). *)
|
paulson@14387
|
291 |
val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
|
wenzelm@13462
|
292 |
add_number_of_left, mult_number_of_left] @
|
paulson@11868
|
293 |
bin_arith_simps @ bin_rel_simps;
|
wenzelm@9436
|
294 |
|
paulson@14113
|
295 |
(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
|
paulson@14113
|
296 |
during re-arrangement*)
|
paulson@14113
|
297 |
val non_add_bin_simps =
|
paulson@14113
|
298 |
bin_simps \\ [add_number_of_left, number_of_add RS sym];
|
paulson@14113
|
299 |
|
wenzelm@9436
|
300 |
(*To evaluate binary negations of coefficients*)
|
paulson@14387
|
301 |
val minus_simps = NCons_simps @
|
paulson@14387
|
302 |
[numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
|
wenzelm@13462
|
303 |
bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
|
wenzelm@13462
|
304 |
bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
|
wenzelm@9436
|
305 |
|
wenzelm@9436
|
306 |
(*To let us treat subtraction as addition*)
|
paulson@14387
|
307 |
val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
|
wenzelm@9436
|
308 |
|
paulson@10713
|
309 |
(*push the unary minus down: - x * y = x * - y *)
|
paulson@14387
|
310 |
val minus_mult_eq_1_to_2 =
|
paulson@14387
|
311 |
[minus_mult_left RS sym, minus_mult_right] MRS trans |> standard;
|
paulson@10713
|
312 |
|
paulson@10713
|
313 |
(*to extract again any uncancelled minuses*)
|
paulson@14387
|
314 |
val minus_from_mult_simps =
|
paulson@14387
|
315 |
[minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
|
paulson@10713
|
316 |
|
paulson@10713
|
317 |
(*combine unary minus with numeric literals, however nested within a product*)
|
paulson@14387
|
318 |
val mult_minus_simps =
|
paulson@14387
|
319 |
[mult_assoc, minus_mult_left, minus_mult_eq_1_to_2];
|
paulson@10713
|
320 |
|
wenzelm@9436
|
321 |
(*Apply the given rewrite (if present) just once*)
|
wenzelm@9436
|
322 |
fun trans_tac None = all_tac
|
wenzelm@9436
|
323 |
| trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
|
wenzelm@9436
|
324 |
|
wenzelm@9436
|
325 |
fun simplify_meta_eq rules =
|
wenzelm@9436
|
326 |
simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
|
paulson@12975
|
327 |
o mk_meta_eq;
|
wenzelm@9436
|
328 |
|
wenzelm@9436
|
329 |
structure CancelNumeralsCommon =
|
wenzelm@9436
|
330 |
struct
|
wenzelm@13462
|
331 |
val mk_sum = mk_sum
|
wenzelm@13462
|
332 |
val dest_sum = dest_sum
|
wenzelm@13462
|
333 |
val mk_coeff = mk_coeff
|
wenzelm@13462
|
334 |
val dest_coeff = dest_coeff 1
|
wenzelm@13462
|
335 |
val find_first_coeff = find_first_coeff []
|
wenzelm@9436
|
336 |
val trans_tac = trans_tac
|
wenzelm@13462
|
337 |
val norm_tac =
|
paulson@11868
|
338 |
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
|
paulson@14387
|
339 |
diff_simps@minus_simps@add_ac))
|
paulson@14387
|
340 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
|
paulson@14387
|
341 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
|
paulson@14387
|
342 |
add_ac@mult_ac))
|
wenzelm@13462
|
343 |
val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
|
wenzelm@9436
|
344 |
val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
|
wenzelm@9436
|
345 |
end;
|
wenzelm@9436
|
346 |
|
wenzelm@9436
|
347 |
|
wenzelm@9436
|
348 |
structure EqCancelNumerals = CancelNumeralsFun
|
wenzelm@9436
|
349 |
(open CancelNumeralsCommon
|
wenzelm@13485
|
350 |
val prove_conv = Bin_Simprocs.prove_conv
|
wenzelm@9436
|
351 |
val mk_bal = HOLogic.mk_eq
|
paulson@14387
|
352 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
|
wenzelm@9436
|
353 |
val bal_add1 = eq_add_iff1 RS trans
|
wenzelm@9436
|
354 |
val bal_add2 = eq_add_iff2 RS trans
|
wenzelm@9436
|
355 |
);
|
wenzelm@9436
|
356 |
|
wenzelm@9436
|
357 |
structure LessCancelNumerals = CancelNumeralsFun
|
wenzelm@9436
|
358 |
(open CancelNumeralsCommon
|
wenzelm@13485
|
359 |
val prove_conv = Bin_Simprocs.prove_conv
|
wenzelm@9436
|
360 |
val mk_bal = HOLogic.mk_binrel "op <"
|
paulson@14387
|
361 |
val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
|
wenzelm@9436
|
362 |
val bal_add1 = less_add_iff1 RS trans
|
wenzelm@9436
|
363 |
val bal_add2 = less_add_iff2 RS trans
|
wenzelm@9436
|
364 |
);
|
wenzelm@9436
|
365 |
|
wenzelm@9436
|
366 |
structure LeCancelNumerals = CancelNumeralsFun
|
wenzelm@9436
|
367 |
(open CancelNumeralsCommon
|
wenzelm@13485
|
368 |
val prove_conv = Bin_Simprocs.prove_conv
|
wenzelm@9436
|
369 |
val mk_bal = HOLogic.mk_binrel "op <="
|
paulson@14387
|
370 |
val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
|
wenzelm@9436
|
371 |
val bal_add1 = le_add_iff1 RS trans
|
wenzelm@9436
|
372 |
val bal_add2 = le_add_iff2 RS trans
|
wenzelm@9436
|
373 |
);
|
wenzelm@9436
|
374 |
|
wenzelm@13462
|
375 |
val cancel_numerals =
|
paulson@11868
|
376 |
map Bin_Simprocs.prep_simproc
|
wenzelm@9436
|
377 |
[("inteq_cancel_numerals",
|
paulson@14387
|
378 |
["(l::'a::number_ring) + m = n",
|
paulson@14387
|
379 |
"(l::'a::number_ring) = m + n",
|
paulson@14387
|
380 |
"(l::'a::number_ring) - m = n",
|
paulson@14387
|
381 |
"(l::'a::number_ring) = m - n",
|
paulson@14387
|
382 |
"(l::'a::number_ring) * m = n",
|
paulson@14387
|
383 |
"(l::'a::number_ring) = m * n"],
|
wenzelm@9436
|
384 |
EqCancelNumerals.proc),
|
wenzelm@13462
|
385 |
("intless_cancel_numerals",
|
obua@14738
|
386 |
["(l::'a::{ordered_idom,number_ring}) + m < n",
|
obua@14738
|
387 |
"(l::'a::{ordered_idom,number_ring}) < m + n",
|
obua@14738
|
388 |
"(l::'a::{ordered_idom,number_ring}) - m < n",
|
obua@14738
|
389 |
"(l::'a::{ordered_idom,number_ring}) < m - n",
|
obua@14738
|
390 |
"(l::'a::{ordered_idom,number_ring}) * m < n",
|
obua@14738
|
391 |
"(l::'a::{ordered_idom,number_ring}) < m * n"],
|
wenzelm@9436
|
392 |
LessCancelNumerals.proc),
|
wenzelm@13462
|
393 |
("intle_cancel_numerals",
|
obua@14738
|
394 |
["(l::'a::{ordered_idom,number_ring}) + m <= n",
|
obua@14738
|
395 |
"(l::'a::{ordered_idom,number_ring}) <= m + n",
|
obua@14738
|
396 |
"(l::'a::{ordered_idom,number_ring}) - m <= n",
|
obua@14738
|
397 |
"(l::'a::{ordered_idom,number_ring}) <= m - n",
|
obua@14738
|
398 |
"(l::'a::{ordered_idom,number_ring}) * m <= n",
|
obua@14738
|
399 |
"(l::'a::{ordered_idom,number_ring}) <= m * n"],
|
wenzelm@9436
|
400 |
LeCancelNumerals.proc)];
|
wenzelm@9436
|
401 |
|
wenzelm@9436
|
402 |
|
wenzelm@9436
|
403 |
structure CombineNumeralsData =
|
wenzelm@9436
|
404 |
struct
|
wenzelm@13462
|
405 |
val add = op + : int*int -> int
|
wenzelm@13462
|
406 |
val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
|
wenzelm@13462
|
407 |
val dest_sum = dest_sum
|
wenzelm@13462
|
408 |
val mk_coeff = mk_coeff
|
wenzelm@13462
|
409 |
val dest_coeff = dest_coeff 1
|
paulson@14272
|
410 |
val left_distrib = combine_common_factor RS trans
|
wenzelm@13485
|
411 |
val prove_conv = Bin_Simprocs.prove_conv_nohyps
|
wenzelm@9436
|
412 |
val trans_tac = trans_tac
|
wenzelm@13462
|
413 |
val norm_tac =
|
paulson@11868
|
414 |
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
|
paulson@14387
|
415 |
diff_simps@minus_simps@add_ac))
|
paulson@14387
|
416 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
|
paulson@14387
|
417 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
|
paulson@14387
|
418 |
add_ac@mult_ac))
|
wenzelm@13462
|
419 |
val numeral_simp_tac = ALLGOALS
|
wenzelm@9436
|
420 |
(simp_tac (HOL_ss addsimps add_0s@bin_simps))
|
wenzelm@9436
|
421 |
val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
|
wenzelm@9436
|
422 |
end;
|
wenzelm@9436
|
423 |
|
wenzelm@9436
|
424 |
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
|
wenzelm@13462
|
425 |
|
wenzelm@13462
|
426 |
val combine_numerals =
|
wenzelm@13462
|
427 |
Bin_Simprocs.prep_simproc
|
paulson@14387
|
428 |
("int_combine_numerals",
|
paulson@14387
|
429 |
["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"],
|
paulson@14387
|
430 |
CombineNumerals.proc);
|
wenzelm@9436
|
431 |
|
wenzelm@9436
|
432 |
end;
|
wenzelm@9436
|
433 |
|
wenzelm@9436
|
434 |
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
|
wenzelm@9436
|
435 |
Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
|
wenzelm@9436
|
436 |
|
wenzelm@9436
|
437 |
(*examples:
|
wenzelm@9436
|
438 |
print_depth 22;
|
wenzelm@9436
|
439 |
set timing;
|
wenzelm@9436
|
440 |
set trace_simp;
|
wenzelm@13462
|
441 |
fun test s = (Goal s, by (Simp_tac 1));
|
wenzelm@9436
|
442 |
|
wenzelm@11704
|
443 |
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
|
wenzelm@9436
|
444 |
|
wenzelm@11704
|
445 |
test "2*u = (u::int)";
|
wenzelm@11704
|
446 |
test "(i + j + 12 + (k::int)) - 15 = y";
|
wenzelm@11704
|
447 |
test "(i + j + 12 + (k::int)) - 5 = y";
|
wenzelm@9436
|
448 |
|
wenzelm@9436
|
449 |
test "y - b < (b::int)";
|
wenzelm@11704
|
450 |
test "y - (3*b + c) < (b::int) - 2*c";
|
wenzelm@9436
|
451 |
|
wenzelm@11704
|
452 |
test "(2*x - (u*v) + y) - v*3*u = (w::int)";
|
wenzelm@11704
|
453 |
test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
|
wenzelm@11704
|
454 |
test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
|
wenzelm@11704
|
455 |
test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
|
wenzelm@9436
|
456 |
|
wenzelm@11704
|
457 |
test "(i + j + 12 + (k::int)) = u + 15 + y";
|
wenzelm@11704
|
458 |
test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
|
wenzelm@9436
|
459 |
|
wenzelm@11704
|
460 |
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)";
|
wenzelm@9436
|
461 |
|
wenzelm@9436
|
462 |
test "a + -(b+c) + b = (d::int)";
|
wenzelm@9436
|
463 |
test "a + -(b+c) - b = (d::int)";
|
wenzelm@9436
|
464 |
|
wenzelm@9436
|
465 |
(*negative numerals*)
|
wenzelm@11704
|
466 |
test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
|
wenzelm@11704
|
467 |
test "(i + j + -3 + (k::int)) < u + 5 + y";
|
wenzelm@11704
|
468 |
test "(i + j + 3 + (k::int)) < u + -6 + y";
|
wenzelm@11704
|
469 |
test "(i + j + -12 + (k::int)) - 15 = y";
|
wenzelm@11704
|
470 |
test "(i + j + 12 + (k::int)) - -15 = y";
|
wenzelm@11704
|
471 |
test "(i + j + -12 + (k::int)) - -15 = y";
|
wenzelm@9436
|
472 |
*)
|
wenzelm@9436
|
473 |
|
wenzelm@9436
|
474 |
|
paulson@14387
|
475 |
(** Constant folding for multiplication in semirings **)
|
wenzelm@9436
|
476 |
|
paulson@14387
|
477 |
(*We do not need folding for addition: combine_numerals does the same thing*)
|
wenzelm@9436
|
478 |
|
paulson@14387
|
479 |
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
|
wenzelm@9436
|
480 |
struct
|
wenzelm@13462
|
481 |
val ss = HOL_ss
|
wenzelm@13462
|
482 |
val eq_reflection = eq_reflection
|
wenzelm@9436
|
483 |
val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
|
wenzelm@9436
|
484 |
val add_ac = mult_ac
|
wenzelm@9436
|
485 |
end;
|
wenzelm@9436
|
486 |
|
paulson@14387
|
487 |
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
|
wenzelm@9436
|
488 |
|
paulson@14387
|
489 |
val assoc_fold_simproc =
|
paulson@14387
|
490 |
Bin_Simprocs.prep_simproc
|
obua@14738
|
491 |
("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
|
paulson@14387
|
492 |
Semiring_Times_Assoc.proc);
|
paulson@14387
|
493 |
|
paulson@14387
|
494 |
Addsimprocs [assoc_fold_simproc];
|
paulson@14387
|
495 |
|
paulson@14387
|
496 |
|
wenzelm@9436
|
497 |
|
wenzelm@9436
|
498 |
|
wenzelm@9436
|
499 |
(*** decision procedure for linear arithmetic ***)
|
wenzelm@9436
|
500 |
|
wenzelm@9436
|
501 |
(*---------------------------------------------------------------------------*)
|
wenzelm@9436
|
502 |
(* Linear arithmetic *)
|
wenzelm@9436
|
503 |
(*---------------------------------------------------------------------------*)
|
wenzelm@9436
|
504 |
|
wenzelm@9436
|
505 |
(*
|
wenzelm@9436
|
506 |
Instantiation of the generic linear arithmetic package for int.
|
wenzelm@9436
|
507 |
*)
|
wenzelm@9436
|
508 |
|
wenzelm@9436
|
509 |
(* Update parameters of arithmetic prover *)
|
wenzelm@9436
|
510 |
local
|
wenzelm@9436
|
511 |
|
wenzelm@9436
|
512 |
(* reduce contradictory <= to False *)
|
wenzelm@13462
|
513 |
val add_rules =
|
paulson@14387
|
514 |
simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
|
paulson@14390
|
515 |
[neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
|
paulson@14369
|
516 |
minus_zero, diff_minus, left_minus, right_minus,
|
paulson@14369
|
517 |
mult_zero_left, mult_zero_right, mult_1, mult_1_right,
|
paulson@14369
|
518 |
minus_mult_left RS sym, minus_mult_right RS sym,
|
paulson@14369
|
519 |
minus_add_distrib, minus_minus, mult_assoc,
|
paulson@14387
|
520 |
of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
|
paulson@14387
|
521 |
of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat,
|
paulson@14387
|
522 |
zero_neq_one, zero_less_one, zero_le_one,
|
paulson@14387
|
523 |
zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
|
wenzelm@9436
|
524 |
|
paulson@14387
|
525 |
val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
|
paulson@14387
|
526 |
Int_Numeral_Simprocs.cancel_numerals;
|
wenzelm@9436
|
527 |
|
wenzelm@9436
|
528 |
in
|
wenzelm@9436
|
529 |
|
wenzelm@9436
|
530 |
val int_arith_setup =
|
nipkow@10693
|
531 |
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
|
paulson@14368
|
532 |
{add_mono_thms = add_mono_thms,
|
nipkow@10693
|
533 |
mult_mono_thms = mult_mono_thms,
|
nipkow@10574
|
534 |
inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
|
paulson@14272
|
535 |
lessD = lessD @ [zless_imp_add1_zle],
|
wenzelm@9436
|
536 |
simpset = simpset addsimps add_rules
|
wenzelm@9436
|
537 |
addsimprocs simprocs
|
wenzelm@9436
|
538 |
addcongs [if_weak_cong]}),
|
paulson@14387
|
539 |
arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT),
|
nipkow@10834
|
540 |
arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
|
wenzelm@9436
|
541 |
arith_discrete ("IntDef.int", true)];
|
wenzelm@9436
|
542 |
|
wenzelm@9436
|
543 |
end;
|
wenzelm@9436
|
544 |
|
wenzelm@13462
|
545 |
val fast_int_arith_simproc =
|
wenzelm@13462
|
546 |
Simplifier.simproc (Theory.sign_of (the_context()))
|
paulson@14387
|
547 |
"fast_int_arith"
|
obua@14738
|
548 |
["(m::'a::{ordered_idom,number_ring}) < n",
|
obua@14738
|
549 |
"(m::'a::{ordered_idom,number_ring}) <= n",
|
obua@14738
|
550 |
"(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
|
wenzelm@9436
|
551 |
|
wenzelm@9436
|
552 |
Addsimprocs [fast_int_arith_simproc]
|
wenzelm@13462
|
553 |
|
wenzelm@9436
|
554 |
|
wenzelm@9436
|
555 |
(* Some test data
|
wenzelm@9436
|
556 |
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
|
wenzelm@9436
|
557 |
by (fast_arith_tac 1);
|
wenzelm@11704
|
558 |
Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
|
wenzelm@9436
|
559 |
by (fast_arith_tac 1);
|
paulson@11868
|
560 |
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d";
|
wenzelm@9436
|
561 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
562 |
Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
|
wenzelm@9436
|
563 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
564 |
Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
|
wenzelm@9436
|
565 |
\ ==> a+a <= j+j";
|
wenzelm@9436
|
566 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
567 |
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
|
wenzelm@11704
|
568 |
\ ==> a+a - - -1 < j+j - 3";
|
wenzelm@9436
|
569 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
570 |
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
|
wenzelm@9436
|
571 |
by (arith_tac 1);
|
wenzelm@9436
|
572 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
wenzelm@9436
|
573 |
\ ==> a <= l";
|
wenzelm@9436
|
574 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
575 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
wenzelm@9436
|
576 |
\ ==> a+a+a+a <= l+l+l+l";
|
wenzelm@9436
|
577 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
578 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
wenzelm@9436
|
579 |
\ ==> a+a+a+a+a <= l+l+l+l+i";
|
wenzelm@9436
|
580 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
581 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
wenzelm@9436
|
582 |
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
|
wenzelm@9436
|
583 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
584 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
wenzelm@11704
|
585 |
\ ==> 6*a <= 5*l+i";
|
wenzelm@9436
|
586 |
by (fast_arith_tac 1);
|
wenzelm@9436
|
587 |
*)
|