wenzelm@9436
|
1 |
(* Title: HOL/arith_data.ML
|
wenzelm@9436
|
2 |
ID: $Id$
|
wenzelm@9436
|
3 |
Author: Markus Wenzel, Stefan Berghofer and Tobias Nipkow
|
wenzelm@9436
|
4 |
|
wenzelm@9436
|
5 |
Various arithmetic proof procedures.
|
wenzelm@9436
|
6 |
*)
|
wenzelm@9436
|
7 |
|
wenzelm@9436
|
8 |
(*---------------------------------------------------------------------------*)
|
wenzelm@9436
|
9 |
(* 1. Cancellation of common terms *)
|
wenzelm@9436
|
10 |
(*---------------------------------------------------------------------------*)
|
wenzelm@9436
|
11 |
|
nipkow@13517
|
12 |
structure NatArithUtils =
|
wenzelm@9436
|
13 |
struct
|
wenzelm@9436
|
14 |
|
wenzelm@9436
|
15 |
(** abstract syntax of structure nat: 0, Suc, + **)
|
wenzelm@9436
|
16 |
|
wenzelm@9436
|
17 |
(* mk_sum, mk_norm_sum *)
|
wenzelm@9436
|
18 |
|
wenzelm@9436
|
19 |
val one = HOLogic.mk_nat 1;
|
wenzelm@9436
|
20 |
val mk_plus = HOLogic.mk_binop "op +";
|
wenzelm@9436
|
21 |
|
wenzelm@9436
|
22 |
fun mk_sum [] = HOLogic.zero
|
wenzelm@9436
|
23 |
| mk_sum [t] = t
|
wenzelm@9436
|
24 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
|
wenzelm@9436
|
25 |
|
wenzelm@9436
|
26 |
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
|
wenzelm@9436
|
27 |
fun mk_norm_sum ts =
|
skalberg@15570
|
28 |
let val (ones, sums) = List.partition (equal one) ts in
|
wenzelm@9436
|
29 |
funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
|
wenzelm@9436
|
30 |
end;
|
wenzelm@9436
|
31 |
|
wenzelm@9436
|
32 |
|
wenzelm@9436
|
33 |
(* dest_sum *)
|
wenzelm@9436
|
34 |
|
wenzelm@9436
|
35 |
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
|
wenzelm@9436
|
36 |
|
wenzelm@9436
|
37 |
fun dest_sum tm =
|
wenzelm@9436
|
38 |
if HOLogic.is_zero tm then []
|
wenzelm@9436
|
39 |
else
|
wenzelm@9436
|
40 |
(case try HOLogic.dest_Suc tm of
|
skalberg@15531
|
41 |
SOME t => one :: dest_sum t
|
skalberg@15531
|
42 |
| NONE =>
|
wenzelm@9436
|
43 |
(case try dest_plus tm of
|
skalberg@15531
|
44 |
SOME (t, u) => dest_sum t @ dest_sum u
|
skalberg@15531
|
45 |
| NONE => [tm]));
|
wenzelm@9436
|
46 |
|
wenzelm@9436
|
47 |
|
wenzelm@9436
|
48 |
(** generic proof tools **)
|
wenzelm@9436
|
49 |
|
wenzelm@9436
|
50 |
(* prove conversions *)
|
wenzelm@9436
|
51 |
|
wenzelm@9436
|
52 |
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
|
wenzelm@9436
|
53 |
|
wenzelm@17611
|
54 |
fun prove_conv expand_tac norm_tac sg ss tu =
|
nipkow@13517
|
55 |
mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
|
wenzelm@17611
|
56 |
(K [expand_tac, norm_tac ss]))
|
wenzelm@9436
|
57 |
handle ERROR => error ("The error(s) above occurred while trying to prove " ^
|
nipkow@13517
|
58 |
(string_of_cterm (cterm_of sg (mk_eqv tu))));
|
wenzelm@9436
|
59 |
|
wenzelm@9436
|
60 |
val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
|
wenzelm@9436
|
61 |
(fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
|
wenzelm@9436
|
62 |
|
wenzelm@9436
|
63 |
|
wenzelm@9436
|
64 |
(* rewriting *)
|
wenzelm@9436
|
65 |
|
wenzelm@17611
|
66 |
fun simp_all_tac rules ss =
|
wenzelm@17875
|
67 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules));
|
wenzelm@9436
|
68 |
|
wenzelm@9436
|
69 |
val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
|
wenzelm@9436
|
70 |
val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
|
wenzelm@9436
|
71 |
|
nipkow@13517
|
72 |
fun prep_simproc (name, pats, proc) =
|
wenzelm@16834
|
73 |
Simplifier.simproc (the_context ()) name pats proc;
|
nipkow@13517
|
74 |
|
nipkow@13517
|
75 |
end;
|
nipkow@13517
|
76 |
|
nipkow@13517
|
77 |
signature ARITH_DATA =
|
nipkow@13517
|
78 |
sig
|
nipkow@13517
|
79 |
val nat_cancel_sums_add: simproc list
|
nipkow@13517
|
80 |
val nat_cancel_sums: simproc list
|
nipkow@13517
|
81 |
end;
|
nipkow@13517
|
82 |
|
nipkow@13517
|
83 |
structure ArithData: ARITH_DATA =
|
nipkow@13517
|
84 |
struct
|
nipkow@13517
|
85 |
|
nipkow@13517
|
86 |
open NatArithUtils;
|
wenzelm@9436
|
87 |
|
wenzelm@9436
|
88 |
|
wenzelm@9436
|
89 |
(** cancel common summands **)
|
wenzelm@9436
|
90 |
|
wenzelm@9436
|
91 |
structure Sum =
|
wenzelm@9436
|
92 |
struct
|
wenzelm@9436
|
93 |
val mk_sum = mk_norm_sum;
|
wenzelm@9436
|
94 |
val dest_sum = dest_sum;
|
wenzelm@9436
|
95 |
val prove_conv = prove_conv;
|
wenzelm@17611
|
96 |
fun norm_tac ss = simp_all_tac add_rules ss THEN simp_all_tac add_ac ss;
|
wenzelm@9436
|
97 |
end;
|
wenzelm@9436
|
98 |
|
wenzelm@9436
|
99 |
fun gen_uncancel_tac rule ct =
|
skalberg@15531
|
100 |
rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
|
wenzelm@9436
|
101 |
|
wenzelm@9436
|
102 |
|
wenzelm@9436
|
103 |
(* nat eq *)
|
wenzelm@9436
|
104 |
|
wenzelm@9436
|
105 |
structure EqCancelSums = CancelSumsFun
|
wenzelm@9436
|
106 |
(struct
|
wenzelm@9436
|
107 |
open Sum;
|
wenzelm@9436
|
108 |
val mk_bal = HOLogic.mk_eq;
|
wenzelm@9436
|
109 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
|
paulson@14331
|
110 |
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
|
wenzelm@9436
|
111 |
end);
|
wenzelm@9436
|
112 |
|
wenzelm@9436
|
113 |
|
wenzelm@9436
|
114 |
(* nat less *)
|
wenzelm@9436
|
115 |
|
wenzelm@9436
|
116 |
structure LessCancelSums = CancelSumsFun
|
wenzelm@9436
|
117 |
(struct
|
wenzelm@9436
|
118 |
open Sum;
|
wenzelm@9436
|
119 |
val mk_bal = HOLogic.mk_binrel "op <";
|
wenzelm@9436
|
120 |
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
|
paulson@14331
|
121 |
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
|
wenzelm@9436
|
122 |
end);
|
wenzelm@9436
|
123 |
|
wenzelm@9436
|
124 |
|
wenzelm@9436
|
125 |
(* nat le *)
|
wenzelm@9436
|
126 |
|
wenzelm@9436
|
127 |
structure LeCancelSums = CancelSumsFun
|
wenzelm@9436
|
128 |
(struct
|
wenzelm@9436
|
129 |
open Sum;
|
wenzelm@9436
|
130 |
val mk_bal = HOLogic.mk_binrel "op <=";
|
wenzelm@9436
|
131 |
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
|
paulson@14331
|
132 |
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
|
wenzelm@9436
|
133 |
end);
|
wenzelm@9436
|
134 |
|
wenzelm@9436
|
135 |
|
wenzelm@9436
|
136 |
(* nat diff *)
|
wenzelm@9436
|
137 |
|
wenzelm@9436
|
138 |
structure DiffCancelSums = CancelSumsFun
|
wenzelm@9436
|
139 |
(struct
|
wenzelm@9436
|
140 |
open Sum;
|
wenzelm@9436
|
141 |
val mk_bal = HOLogic.mk_binop "op -";
|
wenzelm@9436
|
142 |
val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
|
wenzelm@9436
|
143 |
val uncancel_tac = gen_uncancel_tac diff_cancel;
|
wenzelm@9436
|
144 |
end);
|
wenzelm@9436
|
145 |
|
wenzelm@9436
|
146 |
|
wenzelm@9436
|
147 |
|
wenzelm@9436
|
148 |
(** prepare nat_cancel simprocs **)
|
wenzelm@9436
|
149 |
|
wenzelm@9436
|
150 |
val nat_cancel_sums_add = map prep_simproc
|
wenzelm@13462
|
151 |
[("nateq_cancel_sums",
|
wenzelm@13462
|
152 |
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc),
|
wenzelm@13462
|
153 |
("natless_cancel_sums",
|
wenzelm@13462
|
154 |
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], LessCancelSums.proc),
|
wenzelm@13462
|
155 |
("natle_cancel_sums",
|
wenzelm@13462
|
156 |
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], LeCancelSums.proc)];
|
wenzelm@9436
|
157 |
|
wenzelm@9436
|
158 |
val nat_cancel_sums = nat_cancel_sums_add @
|
wenzelm@13462
|
159 |
[prep_simproc ("natdiff_cancel_sums",
|
wenzelm@13462
|
160 |
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], DiffCancelSums.proc)];
|
wenzelm@9436
|
161 |
|
wenzelm@9436
|
162 |
end;
|
wenzelm@9436
|
163 |
|
wenzelm@9436
|
164 |
open ArithData;
|
wenzelm@9436
|
165 |
|
wenzelm@9436
|
166 |
|
wenzelm@9436
|
167 |
(*---------------------------------------------------------------------------*)
|
wenzelm@9436
|
168 |
(* 2. Linear arithmetic *)
|
wenzelm@9436
|
169 |
(*---------------------------------------------------------------------------*)
|
wenzelm@9436
|
170 |
|
wenzelm@9436
|
171 |
(* Parameters data for general linear arithmetic functor *)
|
wenzelm@9436
|
172 |
|
wenzelm@9436
|
173 |
structure LA_Logic: LIN_ARITH_LOGIC =
|
wenzelm@9436
|
174 |
struct
|
wenzelm@9436
|
175 |
val ccontr = ccontr;
|
wenzelm@9436
|
176 |
val conjI = conjI;
|
wenzelm@9436
|
177 |
val notI = notI;
|
wenzelm@9436
|
178 |
val sym = sym;
|
wenzelm@9436
|
179 |
val not_lessD = linorder_not_less RS iffD1;
|
wenzelm@9436
|
180 |
val not_leD = linorder_not_le RS iffD1;
|
wenzelm@9436
|
181 |
|
wenzelm@9436
|
182 |
|
wenzelm@9436
|
183 |
fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
|
wenzelm@9436
|
184 |
|
wenzelm@9436
|
185 |
val mk_Trueprop = HOLogic.mk_Trueprop;
|
wenzelm@9436
|
186 |
|
nipkow@16733
|
187 |
fun atomize thm = case #prop(rep_thm thm) of
|
nipkow@16733
|
188 |
Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
|
nipkow@16733
|
189 |
atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
|
nipkow@16733
|
190 |
| _ => [thm];
|
nipkow@16733
|
191 |
|
wenzelm@9436
|
192 |
fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
|
wenzelm@9436
|
193 |
| neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
|
wenzelm@9436
|
194 |
|
wenzelm@9436
|
195 |
fun is_False thm =
|
wenzelm@9436
|
196 |
let val _ $ t = #prop(rep_thm thm)
|
wenzelm@9436
|
197 |
in t = Const("False",HOLogic.boolT) end;
|
wenzelm@9436
|
198 |
|
wenzelm@9436
|
199 |
fun is_nat(t) = fastype_of1 t = HOLogic.natT;
|
wenzelm@9436
|
200 |
|
wenzelm@9436
|
201 |
fun mk_nat_thm sg t =
|
wenzelm@9436
|
202 |
let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
|
wenzelm@9436
|
203 |
in instantiate ([],[(cn,ct)]) le0 end;
|
wenzelm@9436
|
204 |
|
wenzelm@9436
|
205 |
end;
|
wenzelm@9436
|
206 |
|
wenzelm@9436
|
207 |
|
wenzelm@9436
|
208 |
(* arith theory data *)
|
wenzelm@9436
|
209 |
|
wenzelm@16424
|
210 |
structure ArithTheoryData = TheoryDataFun
|
wenzelm@16424
|
211 |
(struct
|
wenzelm@9436
|
212 |
val name = "HOL/arith";
|
nipkow@15185
|
213 |
type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string list, presburger: (int -> tactic) option};
|
wenzelm@9436
|
214 |
|
skalberg@15531
|
215 |
val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE};
|
wenzelm@9436
|
216 |
val copy = I;
|
wenzelm@16424
|
217 |
val extend = I;
|
wenzelm@16424
|
218 |
fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1},
|
berghofe@13877
|
219 |
{splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) =
|
wenzelm@9436
|
220 |
{splits = Drule.merge_rules (splits1, splits2),
|
nipkow@10574
|
221 |
inj_consts = merge_lists inj_consts1 inj_consts2,
|
nipkow@15185
|
222 |
discrete = merge_lists discrete1 discrete2,
|
skalberg@15531
|
223 |
presburger = (case presburger1 of NONE => presburger2 | p => p)};
|
wenzelm@9436
|
224 |
fun print _ _ = ();
|
wenzelm@16424
|
225 |
end);
|
wenzelm@9436
|
226 |
|
berghofe@13877
|
227 |
fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
|
berghofe@13877
|
228 |
{splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm);
|
wenzelm@9436
|
229 |
|
berghofe@13877
|
230 |
fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
|
berghofe@13877
|
231 |
{splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger});
|
nipkow@10574
|
232 |
|
berghofe@13877
|
233 |
fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
|
berghofe@13877
|
234 |
{splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
|
wenzelm@9436
|
235 |
|
wenzelm@9436
|
236 |
|
wenzelm@9436
|
237 |
structure LA_Data_Ref: LIN_ARITH_DATA =
|
wenzelm@9436
|
238 |
struct
|
wenzelm@9436
|
239 |
|
wenzelm@9436
|
240 |
(* Decomposition of terms *)
|
wenzelm@9436
|
241 |
|
wenzelm@9436
|
242 |
fun nT (Type("fun",[N,_])) = N = HOLogic.natT
|
wenzelm@9436
|
243 |
| nT _ = false;
|
wenzelm@9436
|
244 |
|
haftmann@17325
|
245 |
fun add_atom(t,m,(p,i)) = (case AList.lookup (op =) p t of NONE => ((t, m) :: p, i)
|
haftmann@17325
|
246 |
| SOME n => (AList.update (op =) (t, ratadd (n, m)) p, i));
|
nipkow@10693
|
247 |
|
nipkow@10693
|
248 |
exception Zero;
|
wenzelm@9436
|
249 |
|
nipkow@10693
|
250 |
fun rat_of_term(numt,dent) =
|
nipkow@10693
|
251 |
let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent
|
nipkow@10693
|
252 |
in if den = 0 then raise Zero else int_ratdiv(num,den) end;
|
nipkow@10718
|
253 |
|
nipkow@10718
|
254 |
(* Warning: in rare cases number_of encloses a non-numeral,
|
nipkow@10718
|
255 |
in which case dest_binum raises TERM; hence all the handles below.
|
nipkow@11334
|
256 |
Same for Suc-terms that turn out not to be numerals -
|
nipkow@11334
|
257 |
although the simplifier should eliminate those anyway...
|
nipkow@10718
|
258 |
*)
|
nipkow@10718
|
259 |
|
nipkow@11334
|
260 |
fun number_of_Sucs (Const("Suc",_) $ n) = number_of_Sucs n + 1
|
nipkow@11334
|
261 |
| number_of_Sucs t = if HOLogic.is_zero t then 0
|
nipkow@11334
|
262 |
else raise TERM("number_of_Sucs",[])
|
nipkow@11334
|
263 |
|
nipkow@10718
|
264 |
(* decompose nested multiplications, bracketing them to the right and combining all
|
nipkow@10718
|
265 |
their coefficients
|
nipkow@10718
|
266 |
*)
|
nipkow@10718
|
267 |
|
nipkow@13499
|
268 |
fun demult inj_consts =
|
nipkow@13499
|
269 |
let
|
nipkow@10718
|
270 |
fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
|
nipkow@10718
|
271 |
Const("Numeral.number_of",_)$n
|
paulson@15965
|
272 |
=> demult(t,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
|
nipkow@12480
|
273 |
| Const("uminus",_)$(Const("Numeral.number_of",_)$n)
|
paulson@15965
|
274 |
=> demult(t,ratmul(m,rat_of_intinf(~(HOLogic.dest_binum n))))
|
nipkow@11334
|
275 |
| Const("Suc",_) $ _
|
nipkow@11334
|
276 |
=> demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
|
nipkow@10718
|
277 |
| Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
|
nipkow@10718
|
278 |
| Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
|
nipkow@10718
|
279 |
let val den = HOLogic.dest_binum dent
|
nipkow@10718
|
280 |
in if den = 0 then raise Zero
|
paulson@15965
|
281 |
else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_intinf den)))
|
nipkow@10718
|
282 |
end
|
nipkow@10718
|
283 |
| _ => atomult(mC,s,t,m)
|
nipkow@10718
|
284 |
) handle TERM _ => atomult(mC,s,t,m))
|
nipkow@10718
|
285 |
| demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) =
|
nipkow@10718
|
286 |
(let val den = HOLogic.dest_binum dent
|
paulson@15965
|
287 |
in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_intinf den))) end
|
skalberg@15531
|
288 |
handle TERM _ => (SOME atom,m))
|
skalberg@15531
|
289 |
| demult(Const("0",_),m) = (NONE, rat_of_int 0)
|
skalberg@15531
|
290 |
| demult(Const("1",_),m) = (NONE, m)
|
nipkow@10718
|
291 |
| demult(t as Const("Numeral.number_of",_)$n,m) =
|
paulson@15965
|
292 |
((NONE,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
|
skalberg@15531
|
293 |
handle TERM _ => (SOME t,m))
|
nipkow@12480
|
294 |
| demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
|
nipkow@13499
|
295 |
| demult(t as Const f $ x, m) =
|
skalberg@15531
|
296 |
(if f mem inj_consts then SOME x else SOME t,m)
|
skalberg@15531
|
297 |
| demult(atom,m) = (SOME atom,m)
|
nipkow@10718
|
298 |
|
skalberg@15531
|
299 |
and atomult(mC,atom,t,m) = (case demult(t,m) of (NONE,m') => (SOME atom,m')
|
skalberg@15531
|
300 |
| (SOME t',m') => (SOME(mC $ atom $ t'),m'))
|
nipkow@13499
|
301 |
in demult end;
|
nipkow@10718
|
302 |
|
nipkow@10574
|
303 |
fun decomp2 inj_consts (rel,lhs,rhs) =
|
nipkow@10574
|
304 |
let
|
wenzelm@9436
|
305 |
(* Turn term into list of summand * multiplicity plus a constant *)
|
wenzelm@9436
|
306 |
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
|
wenzelm@9436
|
307 |
| poly(all as Const("op -",T) $ s $ t, m, pi) =
|
nipkow@15958
|
308 |
if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,ratneg m,pi))
|
nipkow@15958
|
309 |
| poly(all as Const("uminus",T) $ t, m, pi) =
|
nipkow@15958
|
310 |
if nT T then add_atom(all,m,pi) else poly(t,ratneg m,pi)
|
wenzelm@9436
|
311 |
| poly(Const("0",_), _, pi) = pi
|
nipkow@11464
|
312 |
| poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m))
|
nipkow@10693
|
313 |
| poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
|
nipkow@10718
|
314 |
| poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
|
nipkow@13499
|
315 |
(case demult inj_consts (t,m) of
|
skalberg@15531
|
316 |
(NONE,m') => (p,ratadd(i,m))
|
skalberg@15531
|
317 |
| (SOME u,m') => add_atom(u,m',pi))
|
nipkow@10718
|
318 |
| poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) =
|
nipkow@13499
|
319 |
(case demult inj_consts (t,m) of
|
skalberg@15531
|
320 |
(NONE,m') => (p,ratadd(i,m'))
|
skalberg@15531
|
321 |
| (SOME u,m') => add_atom(u,m',pi))
|
nipkow@10718
|
322 |
| poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
|
paulson@15965
|
323 |
((p,ratadd(i,ratmul(m,rat_of_intinf(HOLogic.dest_binum t))))
|
nipkow@10718
|
324 |
handle TERM _ => add_atom all)
|
nipkow@10574
|
325 |
| poly(all as Const f $ x, m, pi) =
|
nipkow@10574
|
326 |
if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
|
wenzelm@9436
|
327 |
| poly x = add_atom x;
|
wenzelm@9436
|
328 |
|
nipkow@10718
|
329 |
val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0))
|
nipkow@10718
|
330 |
and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0))
|
nipkow@10693
|
331 |
|
wenzelm@9436
|
332 |
in case rel of
|
skalberg@15531
|
333 |
"op <" => SOME(p,i,"<",q,j)
|
skalberg@15531
|
334 |
| "op <=" => SOME(p,i,"<=",q,j)
|
skalberg@15531
|
335 |
| "op =" => SOME(p,i,"=",q,j)
|
skalberg@15531
|
336 |
| _ => NONE
|
skalberg@15531
|
337 |
end handle Zero => NONE;
|
wenzelm@9436
|
338 |
|
skalberg@15531
|
339 |
fun negate(SOME(x,i,rel,y,j,d)) = SOME(x,i,"~"^rel,y,j,d)
|
skalberg@15531
|
340 |
| negate NONE = NONE;
|
wenzelm@9436
|
341 |
|
nipkow@15121
|
342 |
fun of_lin_arith_sort sg U =
|
nipkow@15121
|
343 |
Type.of_sort (Sign.tsig_of sg) (U,["Ring_and_Field.ordered_idom"])
|
nipkow@15121
|
344 |
|
nipkow@15121
|
345 |
fun allows_lin_arith sg discrete (U as Type(D,[])) =
|
nipkow@15121
|
346 |
if of_lin_arith_sort sg U
|
nipkow@15185
|
347 |
then (true, D mem discrete)
|
nipkow@15121
|
348 |
else (* special cases *)
|
nipkow@15185
|
349 |
if D mem discrete then (true,true) else (false,false)
|
nipkow@15121
|
350 |
| allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
|
nipkow@15121
|
351 |
|
nipkow@15121
|
352 |
fun decomp1 (sg,discrete,inj_consts) (T,xxx) =
|
wenzelm@9436
|
353 |
(case T of
|
nipkow@15121
|
354 |
Type("fun",[U,_]) =>
|
nipkow@15121
|
355 |
(case allows_lin_arith sg discrete U of
|
skalberg@15531
|
356 |
(true,d) => (case decomp2 inj_consts xxx of NONE => NONE
|
skalberg@15531
|
357 |
| SOME(p,i,rel,q,j) => SOME(p,i,rel,q,j,d))
|
skalberg@15531
|
358 |
| (false,_) => NONE)
|
skalberg@15531
|
359 |
| _ => NONE);
|
wenzelm@9436
|
360 |
|
nipkow@10574
|
361 |
fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs))
|
nipkow@10574
|
362 |
| decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
|
nipkow@10574
|
363 |
negate(decomp1 data (T,(rel,lhs,rhs)))
|
skalberg@15531
|
364 |
| decomp2 data _ = NONE
|
wenzelm@9436
|
365 |
|
nipkow@10574
|
366 |
fun decomp sg =
|
wenzelm@16424
|
367 |
let val {discrete, inj_consts, ...} = ArithTheoryData.get sg
|
nipkow@15121
|
368 |
in decomp2 (sg,discrete,inj_consts) end
|
wenzelm@9436
|
369 |
|
nipkow@16358
|
370 |
fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
|
nipkow@10693
|
371 |
|
wenzelm@9436
|
372 |
end;
|
wenzelm@9436
|
373 |
|
wenzelm@9436
|
374 |
|
wenzelm@9436
|
375 |
structure Fast_Arith =
|
wenzelm@9436
|
376 |
Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
|
wenzelm@9436
|
377 |
|
nipkow@13499
|
378 |
val fast_arith_tac = Fast_Arith.lin_arith_tac false
|
nipkow@13499
|
379 |
and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
|
nipkow@14517
|
380 |
and trace_arith = Fast_Arith.trace
|
nipkow@14517
|
381 |
and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
|
wenzelm@9436
|
382 |
|
wenzelm@9436
|
383 |
local
|
wenzelm@9436
|
384 |
|
nipkow@13902
|
385 |
val isolateSuc =
|
nipkow@13902
|
386 |
let val thy = theory "Nat"
|
nipkow@13902
|
387 |
in prove_goal thy "Suc(i+j) = i+j + Suc 0"
|
nipkow@13902
|
388 |
(fn _ => [simp_tac (simpset_of thy) 1])
|
nipkow@13902
|
389 |
end;
|
nipkow@13902
|
390 |
|
wenzelm@9436
|
391 |
(* reduce contradictory <= to False.
|
wenzelm@9436
|
392 |
Most of the work is done by the cancel tactics.
|
wenzelm@9436
|
393 |
*)
|
nipkow@12931
|
394 |
val add_rules =
|
paulson@14368
|
395 |
[add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
|
nipkow@15184
|
396 |
One_nat_def,isolateSuc,
|
wenzelm@17875
|
397 |
order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
|
paulson@16473
|
398 |
zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
|
wenzelm@9436
|
399 |
|
paulson@14368
|
400 |
val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
|
wenzelm@9436
|
401 |
(fn prems => [cut_facts_tac prems 1,
|
paulson@14368
|
402 |
blast_tac (claset() addIs [add_mono]) 1]))
|
nipkow@15121
|
403 |
["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
|
nipkow@15121
|
404 |
"(i = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
|
nipkow@15121
|
405 |
"(i <= j) & (k = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
|
nipkow@15121
|
406 |
"(i = j) & (k = l) ==> i + k = j + (l::'a::pordered_ab_semigroup_add)"
|
wenzelm@9436
|
407 |
];
|
wenzelm@9436
|
408 |
|
nipkow@15121
|
409 |
val mono_ss = simpset() addsimps
|
nipkow@15121
|
410 |
[add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
|
nipkow@15121
|
411 |
|
nipkow@15121
|
412 |
val add_mono_thms_ordered_field =
|
nipkow@15121
|
413 |
map (fn s => prove_goal (the_context ()) s
|
nipkow@15121
|
414 |
(fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
|
nipkow@15121
|
415 |
["(i<j) & (k=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
|
nipkow@15121
|
416 |
"(i=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
|
nipkow@15121
|
417 |
"(i<j) & (k<=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
|
nipkow@15121
|
418 |
"(i<=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
|
nipkow@15121
|
419 |
"(i<j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"];
|
nipkow@15121
|
420 |
|
wenzelm@9436
|
421 |
in
|
wenzelm@9436
|
422 |
|
wenzelm@9436
|
423 |
val init_lin_arith_data =
|
wenzelm@9436
|
424 |
Fast_Arith.setup @
|
nipkow@15921
|
425 |
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
|
nipkow@15121
|
426 |
{add_mono_thms = add_mono_thms @
|
nipkow@15121
|
427 |
add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
|
nipkow@10693
|
428 |
mult_mono_thms = mult_mono_thms,
|
nipkow@10574
|
429 |
inj_thms = inj_thms,
|
wenzelm@9436
|
430 |
lessD = lessD @ [Suc_leI],
|
nipkow@15923
|
431 |
neqE = [linorder_neqE_nat,
|
wenzelm@16485
|
432 |
get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
|
paulson@15234
|
433 |
simpset = HOL_basic_ss addsimps add_rules
|
wenzelm@17875
|
434 |
addsimprocs [ab_group_add_cancel.sum_conv,
|
paulson@15234
|
435 |
ab_group_add_cancel.rel_conv]
|
paulson@15234
|
436 |
(*abel_cancel helps it work in abstract algebraic domains*)
|
paulson@15234
|
437 |
addsimprocs nat_cancel_sums_add}),
|
nipkow@15185
|
438 |
ArithTheoryData.init, arith_discrete "nat"];
|
wenzelm@9436
|
439 |
|
wenzelm@9436
|
440 |
end;
|
wenzelm@9436
|
441 |
|
wenzelm@13462
|
442 |
val fast_nat_arith_simproc =
|
wenzelm@16834
|
443 |
Simplifier.simproc (the_context ()) "fast_nat_arith"
|
wenzelm@13462
|
444 |
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
|
wenzelm@9436
|
445 |
|
wenzelm@9436
|
446 |
|
wenzelm@9436
|
447 |
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
|
wenzelm@9436
|
448 |
useful to detect inconsistencies among the premises for subgoals which are
|
wenzelm@9436
|
449 |
*not* themselves (in)equalities, because the latter activate
|
wenzelm@9436
|
450 |
fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
|
wenzelm@9436
|
451 |
solver all the time rather than add the additional check. *)
|
wenzelm@9436
|
452 |
|
wenzelm@9436
|
453 |
|
wenzelm@9436
|
454 |
(* arith proof method *)
|
wenzelm@9436
|
455 |
|
wenzelm@9436
|
456 |
(* FIXME: K true should be replaced by a sensible test to speed things up
|
wenzelm@9436
|
457 |
in case there are lots of irrelevant terms involved;
|
wenzelm@9436
|
458 |
elimination of min/max can be optimized:
|
wenzelm@9436
|
459 |
(max m n + k <= r) = (m+k <= r & n+k <= r)
|
wenzelm@9436
|
460 |
(l <= min m n + k) = (l <= m+k & l <= n+k)
|
wenzelm@9436
|
461 |
*)
|
wenzelm@10516
|
462 |
local
|
wenzelm@10516
|
463 |
|
nipkow@13499
|
464 |
fun raw_arith_tac ex i st =
|
nipkow@13499
|
465 |
refute_tac (K true)
|
wenzelm@16834
|
466 |
(REPEAT o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
|
nipkow@14509
|
467 |
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
|
nipkow@14509
|
468 |
i st;
|
wenzelm@9436
|
469 |
|
berghofe@13877
|
470 |
fun presburger_tac i st =
|
wenzelm@16834
|
471 |
(case ArithTheoryData.get (Thm.theory_of_thm st) of
|
skalberg@15531
|
472 |
{presburger = SOME tac, ...} =>
|
wenzelm@16970
|
473 |
(warning "Trying full Presburger arithmetic ..."; tac i st)
|
berghofe@13877
|
474 |
| _ => no_tac st);
|
berghofe@13877
|
475 |
|
wenzelm@10516
|
476 |
in
|
wenzelm@10516
|
477 |
|
berghofe@13877
|
478 |
val simple_arith_tac = FIRST' [fast_arith_tac,
|
berghofe@13877
|
479 |
ObjectLogic.atomize_tac THEN' raw_arith_tac true];
|
berghofe@13877
|
480 |
|
berghofe@13877
|
481 |
val arith_tac = FIRST' [fast_arith_tac,
|
berghofe@13877
|
482 |
ObjectLogic.atomize_tac THEN' raw_arith_tac true,
|
berghofe@13877
|
483 |
presburger_tac];
|
berghofe@13877
|
484 |
|
berghofe@13877
|
485 |
val silent_arith_tac = FIRST' [fast_arith_tac,
|
berghofe@13877
|
486 |
ObjectLogic.atomize_tac THEN' raw_arith_tac false,
|
berghofe@13877
|
487 |
presburger_tac];
|
wenzelm@10516
|
488 |
|
wenzelm@9436
|
489 |
fun arith_method prems =
|
wenzelm@9436
|
490 |
Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
|
wenzelm@9436
|
491 |
|
wenzelm@10516
|
492 |
end;
|
wenzelm@10516
|
493 |
|
nipkow@15195
|
494 |
(* antisymmetry:
|
nipkow@15197
|
495 |
combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y
|
nipkow@15195
|
496 |
|
nipkow@15195
|
497 |
local
|
nipkow@15195
|
498 |
val antisym = mk_meta_eq order_antisym
|
nipkow@15195
|
499 |
val not_lessD = linorder_not_less RS iffD1
|
nipkow@15195
|
500 |
fun prp t thm = (#prop(rep_thm thm) = t)
|
nipkow@15195
|
501 |
in
|
nipkow@15195
|
502 |
fun antisym_eq prems thm =
|
nipkow@15195
|
503 |
let
|
nipkow@15195
|
504 |
val r = #prop(rep_thm thm);
|
nipkow@15195
|
505 |
in
|
nipkow@15195
|
506 |
case r of
|
nipkow@15195
|
507 |
Tr $ ((c as Const("op <=",T)) $ s $ t) =>
|
nipkow@15195
|
508 |
let val r' = Tr $ (c $ t $ s)
|
nipkow@15195
|
509 |
in
|
nipkow@15195
|
510 |
case Library.find_first (prp r') prems of
|
skalberg@15531
|
511 |
NONE =>
|
wenzelm@16834
|
512 |
let val r' = Tr $ (HOLogic.Not $ (Const("op <",T) $ s $ t))
|
nipkow@15195
|
513 |
in case Library.find_first (prp r') prems of
|
skalberg@15531
|
514 |
NONE => []
|
skalberg@15531
|
515 |
| SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
|
nipkow@15195
|
516 |
end
|
skalberg@15531
|
517 |
| SOME thm' => [thm' RS (thm RS antisym)]
|
nipkow@15195
|
518 |
end
|
nipkow@15195
|
519 |
| Tr $ (Const("Not",_) $ (Const("op <",T) $ s $ t)) =>
|
nipkow@15195
|
520 |
let val r' = Tr $ (Const("op <=",T) $ s $ t)
|
nipkow@15195
|
521 |
in
|
nipkow@15195
|
522 |
case Library.find_first (prp r') prems of
|
skalberg@15531
|
523 |
NONE =>
|
wenzelm@16834
|
524 |
let val r' = Tr $ (HOLogic.Not $ (Const("op <",T) $ t $ s))
|
nipkow@15195
|
525 |
in case Library.find_first (prp r') prems of
|
skalberg@15531
|
526 |
NONE => []
|
skalberg@15531
|
527 |
| SOME thm' =>
|
nipkow@15195
|
528 |
[(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
|
nipkow@15195
|
529 |
end
|
skalberg@15531
|
530 |
| SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
|
nipkow@15195
|
531 |
end
|
nipkow@15195
|
532 |
| _ => []
|
nipkow@15195
|
533 |
end
|
nipkow@15195
|
534 |
handle THM _ => []
|
nipkow@15195
|
535 |
end;
|
nipkow@15197
|
536 |
*)
|
wenzelm@9436
|
537 |
|
wenzelm@9436
|
538 |
(* theory setup *)
|
wenzelm@9436
|
539 |
|
wenzelm@9436
|
540 |
val arith_setup =
|
wenzelm@9436
|
541 |
init_lin_arith_data @
|
wenzelm@17875
|
542 |
[fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
|
wenzelm@17875
|
543 |
addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
|
wenzelm@17875
|
544 |
addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy),
|
paulson@15221
|
545 |
Method.add_methods
|
wenzelm@17875
|
546 |
[("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
|
wenzelm@17875
|
547 |
"decide linear arithmethic")],
|
wenzelm@9436
|
548 |
Attrib.add_attributes [("arith_split",
|
wenzelm@17875
|
549 |
(Attrib.no_args arith_split_add,
|
paulson@15221
|
550 |
Attrib.no_args Attrib.undef_local_attribute),
|
wenzelm@9893
|
551 |
"declaration of split rules for arithmetic procedure")]];
|