148 val nat_cancel_sums = nat_cancel_sums_add @ |
158 val nat_cancel_sums = nat_cancel_sums_add @ |
149 [prep_simproc ("natdiff_cancel_sums", |
159 [prep_simproc ("natdiff_cancel_sums", |
150 ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], |
160 ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], |
151 K DiffCancelSums.proc)]; |
161 K DiffCancelSums.proc)]; |
152 |
162 |
153 end; (* ArithData *) |
163 val arith_data_setup = |
154 |
164 Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); |
155 open ArithData; |
165 |
156 |
166 |
157 |
167 (* FIXME dead code *) |
158 (*---------------------------------------------------------------------------*) |
|
159 (* 2. Linear arithmetic *) |
|
160 (*---------------------------------------------------------------------------*) |
|
161 |
|
162 (* Parameters data for general linear arithmetic functor *) |
|
163 |
|
164 structure LA_Logic: LIN_ARITH_LOGIC = |
|
165 struct |
|
166 |
|
167 val ccontr = ccontr; |
|
168 val conjI = conjI; |
|
169 val notI = notI; |
|
170 val sym = sym; |
|
171 val not_lessD = @{thm linorder_not_less} RS iffD1; |
|
172 val not_leD = @{thm linorder_not_le} RS iffD1; |
|
173 val le0 = thm "le0"; |
|
174 |
|
175 fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); |
|
176 |
|
177 val mk_Trueprop = HOLogic.mk_Trueprop; |
|
178 |
|
179 fun atomize thm = case Thm.prop_of thm of |
|
180 Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) => |
|
181 atomize(thm RS conjunct1) @ atomize(thm RS conjunct2) |
|
182 | _ => [thm]; |
|
183 |
|
184 fun neg_prop ((TP as Const("Trueprop",_)) $ (Const("Not",_) $ t)) = TP $ t |
|
185 | neg_prop ((TP as Const("Trueprop",_)) $ t) = TP $ (HOLogic.Not $t) |
|
186 | neg_prop t = raise TERM ("neg_prop", [t]); |
|
187 |
|
188 fun is_False thm = |
|
189 let val _ $ t = Thm.prop_of thm |
|
190 in t = Const("False",HOLogic.boolT) end; |
|
191 |
|
192 fun is_nat(t) = fastype_of1 t = HOLogic.natT; |
|
193 |
|
194 fun mk_nat_thm sg t = |
|
195 let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) |
|
196 in instantiate ([],[(cn,ct)]) le0 end; |
|
197 |
|
198 end; (* LA_Logic *) |
|
199 |
|
200 |
|
201 (* arith theory data *) |
|
202 |
|
203 datatype arithtactic = ArithTactic of {name: string, tactic: int -> tactic, id: stamp}; |
|
204 |
|
205 fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()}; |
|
206 |
|
207 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); |
|
208 |
|
209 structure ArithContextData = GenericDataFun |
|
210 ( |
|
211 type T = {splits: thm list, |
|
212 inj_consts: (string * typ) list, |
|
213 discrete: string list, |
|
214 tactics: arithtactic list}; |
|
215 val empty = {splits = [], inj_consts = [], discrete = [], tactics = []}; |
|
216 val extend = I; |
|
217 fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, |
|
218 {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) = |
|
219 {splits = Library.merge Thm.eq_thm_prop (splits1, splits2), |
|
220 inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), |
|
221 discrete = Library.merge (op =) (discrete1, discrete2), |
|
222 tactics = Library.merge eq_arith_tactic (tactics1, tactics2)}; |
|
223 ); |
|
224 |
|
225 val get_arith_data = ArithContextData.get o Context.Proof; |
|
226 |
|
227 val arith_split_add = Thm.declaration_attribute (fn thm => |
|
228 ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => |
|
229 {splits = insert Thm.eq_thm_prop thm splits, |
|
230 inj_consts = inj_consts, discrete = discrete, tactics = tactics})); |
|
231 |
|
232 fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => |
|
233 {splits = splits, inj_consts = inj_consts, |
|
234 discrete = insert (op =) d discrete, tactics = tactics}); |
|
235 |
|
236 fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => |
|
237 {splits = splits, inj_consts = insert (op =) c inj_consts, |
|
238 discrete = discrete, tactics= tactics}); |
|
239 |
|
240 fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => |
|
241 {splits = splits, inj_consts = inj_consts, discrete = discrete, |
|
242 tactics = insert eq_arith_tactic tac tactics}); |
|
243 |
|
244 |
|
245 signature HOL_LIN_ARITH_DATA = |
|
246 sig |
|
247 include LIN_ARITH_DATA |
|
248 val fast_arith_split_limit: int ConfigOption.T |
|
249 val setup_options: theory -> theory |
|
250 end; |
|
251 |
|
252 structure LA_Data_Ref: HOL_LIN_ARITH_DATA = |
|
253 struct |
|
254 |
|
255 val (fast_arith_split_limit, setup1) = ConfigOption.int "fast_arith_split_limit" 9; |
|
256 val (fast_arith_neq_limit, setup2) = ConfigOption.int "fast_arith_neq_limit" 9; |
|
257 val setup_options = setup1 #> setup2; |
|
258 |
|
259 |
|
260 (* internal representation of linear (in-)equations *) |
|
261 type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool); |
|
262 |
|
263 (* Decomposition of terms *) |
|
264 |
|
265 fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT) |
|
266 | nT _ = false; |
|
267 |
|
268 fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) : |
|
269 (term * Rat.rat) list * Rat.rat = |
|
270 case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) |
|
271 | SOME n => (AList.update (op =) (t, Rat.add n m) p, i); |
|
272 |
|
273 exception Zero; |
|
274 |
|
275 fun rat_of_term (numt, dent) = |
|
276 let |
|
277 val num = HOLogic.dest_numeral numt |
|
278 val den = HOLogic.dest_numeral dent |
|
279 in |
|
280 if den = 0 then raise Zero else Rat.rat_of_quotient (num, den) |
|
281 end; |
|
282 |
|
283 (* Warning: in rare cases number_of encloses a non-numeral, |
|
284 in which case dest_numeral raises TERM; hence all the handles below. |
|
285 Same for Suc-terms that turn out not to be numerals - |
|
286 although the simplifier should eliminate those anyway ... |
|
287 *) |
|
288 fun number_of_Sucs (Const ("Suc", _) $ n) : int = |
|
289 number_of_Sucs n + 1 |
|
290 | number_of_Sucs t = |
|
291 if HOLogic.is_zero t then 0 else raise TERM ("number_of_Sucs", []); |
|
292 |
|
293 (* decompose nested multiplications, bracketing them to the right and combining |
|
294 all their coefficients |
|
295 *) |
|
296 fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat = |
|
297 let |
|
298 fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) = ( |
|
299 (case s of |
|
300 Const ("Numeral.number_class.number_of", _) $ n => |
|
301 demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n))) |
|
302 | Const (@{const_name HOL.uminus}, _) $ (Const ("Numeral.number_class.number_of", _) $ n) => |
|
303 demult (t, Rat.mult m (Rat.rat_of_int (~(HOLogic.dest_numeral n)))) |
|
304 | Const (@{const_name Suc}, _) $ _ => |
|
305 demult (t, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat s))) |
|
306 | Const (@{const_name HOL.times}, _) $ s1 $ s2 => |
|
307 demult (mC $ s1 $ (mC $ s2 $ t), m) |
|
308 | Const (@{const_name HOL.divide}, _) $ numt $ (Const ("Numeral.number_class.number_of", _) $ dent) => |
|
309 let |
|
310 val den = HOLogic.dest_numeral dent |
|
311 in |
|
312 if den = 0 then |
|
313 raise Zero |
|
314 else |
|
315 demult (mC $ numt $ t, Rat.mult m (Rat.inv (Rat.rat_of_int den))) |
|
316 end |
|
317 | _ => |
|
318 atomult (mC, s, t, m) |
|
319 ) handle TERM _ => atomult (mC, s, t, m) |
|
320 ) |
|
321 | demult (atom as Const(@{const_name HOL.divide}, _) $ t $ (Const ("Numeral.number_class.number_of", _) $ dent), m) = |
|
322 (let |
|
323 val den = HOLogic.dest_numeral dent |
|
324 in |
|
325 if den = 0 then |
|
326 raise Zero |
|
327 else |
|
328 demult (t, Rat.mult m (Rat.inv (Rat.rat_of_int den))) |
|
329 end |
|
330 handle TERM _ => (SOME atom, m)) |
|
331 | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero) |
|
332 | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m) |
|
333 | demult (t as Const ("Numeral.number_class.number_of", _) $ n, m) = |
|
334 ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n))) |
|
335 handle TERM _ => (SOME t, m)) |
|
336 | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m) |
|
337 | demult (t as Const f $ x, m) = |
|
338 (if member (op =) inj_consts f then SOME x else SOME t, m) |
|
339 | demult (atom, m) = (SOME atom, m) |
|
340 and |
|
341 atomult (mC, atom, t, m) = ( |
|
342 case demult (t, m) of (NONE, m') => (SOME atom, m') |
|
343 | (SOME t', m') => (SOME (mC $ atom $ t'), m') |
|
344 ) |
|
345 in demult end; |
|
346 |
|
347 fun decomp0 (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) : |
|
348 ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option = |
|
349 let |
|
350 (* Turn term into list of summand * multiplicity plus a constant *) |
|
351 fun poly (Const (@{const_name HOL.plus}, _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = |
|
352 poly (s, m, poly (t, m, pi)) |
|
353 | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) = |
|
354 if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi)) |
|
355 | poly (all as Const (@{const_name HOL.uminus}, T) $ t, m, pi) = |
|
356 if nT T then add_atom all m pi else poly (t, Rat.neg m, pi) |
|
357 | poly (Const (@{const_name HOL.zero}, _), _, pi) = |
|
358 pi |
|
359 | poly (Const (@{const_name HOL.one}, _), m, (p, i)) = |
|
360 (p, Rat.add i m) |
|
361 | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) = |
|
362 poly (t, m, (p, Rat.add i m)) |
|
363 | poly (all as Const (@{const_name HOL.times}, _) $ _ $ _, m, pi as (p, i)) = |
|
364 (case demult inj_consts (all, m) of |
|
365 (NONE, m') => (p, Rat.add i m') |
|
366 | (SOME u, m') => add_atom u m' pi) |
|
367 | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) = |
|
368 (case demult inj_consts (all, m) of |
|
369 (NONE, m') => (p, Rat.add i m') |
|
370 | (SOME u, m') => add_atom u m' pi) |
|
371 | poly (all as Const ("Numeral.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) = |
|
372 (let val k = HOLogic.dest_numeral t |
|
373 val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k |
|
374 in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end |
|
375 handle TERM _ => add_atom all m pi) |
|
376 | poly (all as Const f $ x, m, pi) = |
|
377 if f mem inj_consts then poly (x, m, pi) else add_atom all m pi |
|
378 | poly (all, m, pi) = |
|
379 add_atom all m pi |
|
380 val (p, i) = poly (lhs, Rat.one, ([], Rat.zero)) |
|
381 val (q, j) = poly (rhs, Rat.one, ([], Rat.zero)) |
|
382 in |
|
383 case rel of |
|
384 @{const_name HOL.less} => SOME (p, i, "<", q, j) |
|
385 | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j) |
|
386 | "op =" => SOME (p, i, "=", q, j) |
|
387 | _ => NONE |
|
388 end handle Zero => NONE; |
|
389 |
|
390 fun of_lin_arith_sort sg (U : typ) : bool = |
|
391 Type.of_sort (Sign.tsig_of sg) (U, ["Ring_and_Field.ordered_idom"]) |
|
392 |
|
393 fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool = |
|
394 if of_lin_arith_sort sg U then |
|
395 (true, D mem discrete) |
|
396 else (* special cases *) |
|
397 if D mem discrete then (true, true) else (false, false) |
|
398 | allows_lin_arith sg discrete U = |
|
399 (of_lin_arith_sort sg U, false); |
|
400 |
|
401 fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decompT option = |
|
402 case T of |
|
403 Type ("fun", [U, _]) => |
|
404 (case allows_lin_arith thy discrete U of |
|
405 (true, d) => |
|
406 (case decomp0 inj_consts xxx of |
|
407 NONE => NONE |
|
408 | SOME (p, i, rel, q, j) => SOME (p, i, rel, q, j, d)) |
|
409 | (false, _) => |
|
410 NONE) |
|
411 | _ => NONE; |
|
412 |
|
413 fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d) |
|
414 | negate NONE = NONE; |
|
415 |
|
416 fun decomp_negation data |
|
417 ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decompT option = |
|
418 decomp_typecheck data (T, (rel, lhs, rhs)) |
|
419 | decomp_negation data ((Const ("Trueprop", _)) $ |
|
420 (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) = |
|
421 negate (decomp_typecheck data (T, (rel, lhs, rhs))) |
|
422 | decomp_negation data _ = |
|
423 NONE; |
|
424 |
|
425 fun decomp ctxt : term -> decompT option = |
|
426 let |
|
427 val thy = ProofContext.theory_of ctxt |
|
428 val {discrete, inj_consts, ...} = get_arith_data ctxt |
|
429 in decomp_negation (thy, discrete, inj_consts) end; |
|
430 |
|
431 fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T |
|
432 | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T |
|
433 | domain_is_nat _ = false; |
|
434 |
|
435 fun number_of (n, T) = HOLogic.mk_number T n; |
|
436 |
|
437 (*---------------------------------------------------------------------------*) |
|
438 (* the following code performs splitting of certain constants (e.g. min, *) |
|
439 (* max) in a linear arithmetic problem; similar to what split_tac later does *) |
|
440 (* to the proof state *) |
|
441 (*---------------------------------------------------------------------------*) |
|
442 |
|
443 (* checks if splitting with 'thm' is implemented *) |
|
444 |
|
445 fun is_split_thm (thm : thm) : bool = |
|
446 case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => ( |
|
447 (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *) |
|
448 case head_of lhs of |
|
449 Const (a, _) => member (op =) [@{const_name Orderings.max}, |
|
450 @{const_name Orderings.min}, |
|
451 @{const_name HOL.abs}, |
|
452 @{const_name HOL.minus}, |
|
453 "IntDef.nat", |
|
454 "Divides.div_class.mod", |
|
455 "Divides.div_class.div"] a |
|
456 | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ |
|
457 Display.string_of_thm thm); |
|
458 false)) |
|
459 | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ |
|
460 Display.string_of_thm thm); |
|
461 false); |
|
462 |
|
463 (* substitute new for occurrences of old in a term, incrementing bound *) |
|
464 (* variables as needed when substituting inside an abstraction *) |
|
465 |
|
466 fun subst_term ([] : (term * term) list) (t : term) = t |
|
467 | subst_term pairs t = |
|
468 (case AList.lookup (op aconv) pairs t of |
|
469 SOME new => |
|
470 new |
|
471 | NONE => |
|
472 (case t of Abs (a, T, body) => |
|
473 let val pairs' = map (pairself (incr_boundvars 1)) pairs |
|
474 in Abs (a, T, subst_term pairs' body) end |
|
475 | t1 $ t2 => |
|
476 subst_term pairs t1 $ subst_term pairs t2 |
|
477 | _ => t)); |
|
478 |
|
479 (* approximates the effect of one application of split_tac (followed by NNF *) |
|
480 (* normalization) on the subgoal represented by '(Ts, terms)'; returns a *) |
|
481 (* list of new subgoals (each again represented by a typ list for bound *) |
|
482 (* variables and a term list for premises), or NONE if split_tac would fail *) |
|
483 (* on the subgoal *) |
|
484 |
|
485 (* FIXME: currently only the effect of certain split theorems is reproduced *) |
|
486 (* (which is why we need 'is_split_thm'). A more canonical *) |
|
487 (* implementation should analyze the right-hand side of the split *) |
|
488 (* theorem that can be applied, and modify the subgoal accordingly. *) |
|
489 (* Or even better, the splitter should be extended to provide *) |
|
490 (* splitting on terms as well as splitting on theorems (where the *) |
|
491 (* former can have a faster implementation as it does not need to be *) |
|
492 (* proof-producing). *) |
|
493 |
|
494 fun split_once_items ctxt (Ts : typ list, terms : term list) : |
|
495 (typ list * term list) list option = |
|
496 let |
|
497 val thy = ProofContext.theory_of ctxt |
|
498 (* takes a list [t1, ..., tn] to the term *) |
|
499 (* tn' --> ... --> t1' --> False , *) |
|
500 (* where ti' = HOLogic.dest_Trueprop ti *) |
|
501 fun REPEAT_DETERM_etac_rev_mp terms' = |
|
502 fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const |
|
503 val split_thms = filter is_split_thm (#splits (get_arith_data ctxt)) |
|
504 val cmap = Splitter.cmap_of_split_thms split_thms |
|
505 val splits = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms) |
|
506 val split_limit = ConfigOption.get ctxt fast_arith_split_limit |
|
507 in |
|
508 if length splits > split_limit then |
|
509 (tracing ("fast_arith_split_limit exceeded (current value is " ^ |
|
510 string_of_int split_limit ^ ")"); NONE) |
|
511 else ( |
|
512 case splits of [] => |
|
513 (* split_tac would fail: no possible split *) |
|
514 NONE |
|
515 | ((_, _, _, split_type, split_term) :: _) => ( |
|
516 (* ignore all but the first possible split *) |
|
517 case strip_comb split_term of |
|
518 (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *) |
|
519 (Const (@{const_name Orderings.max}, _), [t1, t2]) => |
|
520 let |
|
521 val rev_terms = rev terms |
|
522 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
|
523 val terms2 = map (subst_term [(split_term, t2)]) rev_terms |
|
524 val t1_leq_t2 = Const (@{const_name HOL.less_eq}, |
|
525 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 |
|
526 val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2 |
|
527 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
528 val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false] |
|
529 val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false] |
|
530 in |
|
531 SOME [(Ts, subgoal1), (Ts, subgoal2)] |
|
532 end |
|
533 (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *) |
|
534 | (Const (@{const_name Orderings.min}, _), [t1, t2]) => |
|
535 let |
|
536 val rev_terms = rev terms |
|
537 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
|
538 val terms2 = map (subst_term [(split_term, t2)]) rev_terms |
|
539 val t1_leq_t2 = Const (@{const_name HOL.less_eq}, |
|
540 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 |
|
541 val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2 |
|
542 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
543 val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false] |
|
544 val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false] |
|
545 in |
|
546 SOME [(Ts, subgoal1), (Ts, subgoal2)] |
|
547 end |
|
548 (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *) |
|
549 | (Const (@{const_name HOL.abs}, _), [t1]) => |
|
550 let |
|
551 val rev_terms = rev terms |
|
552 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
|
553 val terms2 = map (subst_term [(split_term, Const (@{const_name HOL.uminus}, |
|
554 split_type --> split_type) $ t1)]) rev_terms |
|
555 val zero = Const (@{const_name HOL.zero}, split_type) |
|
556 val zero_leq_t1 = Const (@{const_name HOL.less_eq}, |
|
557 split_type --> split_type --> HOLogic.boolT) $ zero $ t1 |
|
558 val t1_lt_zero = Const (@{const_name HOL.less}, |
|
559 split_type --> split_type --> HOLogic.boolT) $ t1 $ zero |
|
560 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
561 val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false] |
|
562 val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false] |
|
563 in |
|
564 SOME [(Ts, subgoal1), (Ts, subgoal2)] |
|
565 end |
|
566 (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *) |
|
567 | (Const (@{const_name HOL.minus}, _), [t1, t2]) => |
|
568 let |
|
569 (* "d" in the above theorem becomes a new bound variable after NNF *) |
|
570 (* transformation, therefore some adjustment of indices is necessary *) |
|
571 val rev_terms = rev terms |
|
572 val zero = Const (@{const_name HOL.zero}, split_type) |
|
573 val d = Bound 0 |
|
574 val terms1 = map (subst_term [(split_term, zero)]) rev_terms |
|
575 val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)]) |
|
576 (map (incr_boundvars 1) rev_terms) |
|
577 val t1' = incr_boundvars 1 t1 |
|
578 val t2' = incr_boundvars 1 t2 |
|
579 val t1_lt_t2 = Const (@{const_name HOL.less}, |
|
580 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 |
|
581 val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ |
|
582 (Const (@{const_name HOL.plus}, |
|
583 split_type --> split_type --> split_type) $ t2' $ d) |
|
584 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
585 val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false] |
|
586 val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false] |
|
587 in |
|
588 SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)] |
|
589 end |
|
590 (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *) |
|
591 | (Const ("IntDef.nat", _), [t1]) => |
|
592 let |
|
593 val rev_terms = rev terms |
|
594 val zero_int = Const (@{const_name HOL.zero}, HOLogic.intT) |
|
595 val zero_nat = Const (@{const_name HOL.zero}, HOLogic.natT) |
|
596 val n = Bound 0 |
|
597 val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) |
|
598 (map (incr_boundvars 1) rev_terms) |
|
599 val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms |
|
600 val t1' = incr_boundvars 1 t1 |
|
601 val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ |
|
602 (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n) |
|
603 val t1_lt_zero = Const (@{const_name HOL.less}, |
|
604 HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int |
|
605 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
606 val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false] |
|
607 val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false] |
|
608 in |
|
609 SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)] |
|
610 end |
|
611 (* "?P ((?n::nat) mod (number_of ?k)) = |
|
612 ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) --> |
|
613 (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *) |
|
614 | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) => |
|
615 let |
|
616 val rev_terms = rev terms |
|
617 val zero = Const (@{const_name HOL.zero}, split_type) |
|
618 val i = Bound 1 |
|
619 val j = Bound 0 |
|
620 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
|
621 val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) |
|
622 (map (incr_boundvars 2) rev_terms) |
|
623 val t1' = incr_boundvars 2 t1 |
|
624 val t2' = incr_boundvars 2 t2 |
|
625 val t2_eq_zero = Const ("op =", |
|
626 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
|
627 val t2_neq_zero = HOLogic.mk_not (Const ("op =", |
|
628 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) |
|
629 val j_lt_t2 = Const (@{const_name HOL.less}, |
|
630 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
|
631 val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ |
|
632 (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $ |
|
633 (Const (@{const_name HOL.times}, |
|
634 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
|
635 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
636 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
|
637 val subgoal2 = (map HOLogic.mk_Trueprop |
|
638 [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) |
|
639 @ terms2 @ [not_false] |
|
640 in |
|
641 SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)] |
|
642 end |
|
643 (* "?P ((?n::nat) div (number_of ?k)) = |
|
644 ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) --> |
|
645 (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *) |
|
646 | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) => |
|
647 let |
|
648 val rev_terms = rev terms |
|
649 val zero = Const (@{const_name HOL.zero}, split_type) |
|
650 val i = Bound 1 |
|
651 val j = Bound 0 |
|
652 val terms1 = map (subst_term [(split_term, zero)]) rev_terms |
|
653 val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) |
|
654 (map (incr_boundvars 2) rev_terms) |
|
655 val t1' = incr_boundvars 2 t1 |
|
656 val t2' = incr_boundvars 2 t2 |
|
657 val t2_eq_zero = Const ("op =", |
|
658 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
|
659 val t2_neq_zero = HOLogic.mk_not (Const ("op =", |
|
660 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) |
|
661 val j_lt_t2 = Const (@{const_name HOL.less}, |
|
662 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
|
663 val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ |
|
664 (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $ |
|
665 (Const (@{const_name HOL.times}, |
|
666 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
|
667 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
668 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
|
669 val subgoal2 = (map HOLogic.mk_Trueprop |
|
670 [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) |
|
671 @ terms2 @ [not_false] |
|
672 in |
|
673 SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)] |
|
674 end |
|
675 (* "?P ((?n::int) mod (number_of ?k)) = |
|
676 ((iszero (number_of ?k) --> ?P ?n) & |
|
677 (neg (number_of (uminus ?k)) --> |
|
678 (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) & |
|
679 (neg (number_of ?k) --> |
|
680 (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *) |
|
681 | (Const ("Divides.div_class.mod", |
|
682 Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) => |
|
683 let |
|
684 val rev_terms = rev terms |
|
685 val zero = Const (@{const_name HOL.zero}, split_type) |
|
686 val i = Bound 1 |
|
687 val j = Bound 0 |
|
688 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
|
689 val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) |
|
690 (map (incr_boundvars 2) rev_terms) |
|
691 val t1' = incr_boundvars 2 t1 |
|
692 val (t2' as (_ $ k')) = incr_boundvars 2 t2 |
|
693 val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2 |
|
694 val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ |
|
695 (number_of $ |
|
696 (Const (@{const_name HOL.uminus}, |
|
697 HOLogic.intT --> HOLogic.intT) $ k')) |
|
698 val zero_leq_j = Const (@{const_name HOL.less_eq}, |
|
699 split_type --> split_type --> HOLogic.boolT) $ zero $ j |
|
700 val j_lt_t2 = Const (@{const_name HOL.less}, |
|
701 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
|
702 val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ |
|
703 (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $ |
|
704 (Const (@{const_name HOL.times}, |
|
705 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
|
706 val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2' |
|
707 val t2_lt_j = Const (@{const_name HOL.less}, |
|
708 split_type --> split_type--> HOLogic.boolT) $ t2' $ j |
|
709 val j_leq_zero = Const (@{const_name HOL.less_eq}, |
|
710 split_type --> split_type --> HOLogic.boolT) $ j $ zero |
|
711 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
712 val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false] |
|
713 val subgoal2 = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j]) |
|
714 @ hd terms2_3 |
|
715 :: (if tl terms2_3 = [] then [not_false] else []) |
|
716 @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j]) |
|
717 @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) |
|
718 val subgoal3 = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j]) |
|
719 @ hd terms2_3 |
|
720 :: (if tl terms2_3 = [] then [not_false] else []) |
|
721 @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j]) |
|
722 @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false]) |
|
723 val Ts' = split_type :: split_type :: Ts |
|
724 in |
|
725 SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)] |
|
726 end |
|
727 (* "?P ((?n::int) div (number_of ?k)) = |
|
728 ((iszero (number_of ?k) --> ?P 0) & |
|
729 (neg (number_of (uminus ?k)) --> |
|
730 (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) & |
|
731 (neg (number_of ?k) --> |
|
732 (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *) |
|
733 | (Const ("Divides.div_class.div", |
|
734 Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) => |
|
735 let |
|
736 val rev_terms = rev terms |
|
737 val zero = Const (@{const_name HOL.zero}, split_type) |
|
738 val i = Bound 1 |
|
739 val j = Bound 0 |
|
740 val terms1 = map (subst_term [(split_term, zero)]) rev_terms |
|
741 val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) |
|
742 (map (incr_boundvars 2) rev_terms) |
|
743 val t1' = incr_boundvars 2 t1 |
|
744 val (t2' as (_ $ k')) = incr_boundvars 2 t2 |
|
745 val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2 |
|
746 val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ |
|
747 (number_of $ |
|
748 (Const (@{const_name HOL.uminus}, |
|
749 HOLogic.intT --> HOLogic.intT) $ k')) |
|
750 val zero_leq_j = Const (@{const_name HOL.less_eq}, |
|
751 split_type --> split_type --> HOLogic.boolT) $ zero $ j |
|
752 val j_lt_t2 = Const (@{const_name HOL.less}, |
|
753 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
|
754 val t1_eq_t2_times_i_plus_j = Const ("op =", |
|
755 split_type --> split_type --> HOLogic.boolT) $ t1' $ |
|
756 (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $ |
|
757 (Const (@{const_name HOL.times}, |
|
758 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
|
759 val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2' |
|
760 val t2_lt_j = Const (@{const_name HOL.less}, |
|
761 split_type --> split_type--> HOLogic.boolT) $ t2' $ j |
|
762 val j_leq_zero = Const (@{const_name HOL.less_eq}, |
|
763 split_type --> split_type --> HOLogic.boolT) $ j $ zero |
|
764 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
|
765 val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false] |
|
766 val subgoal2 = (HOLogic.mk_Trueprop neg_minus_k) |
|
767 :: terms2_3 |
|
768 @ not_false |
|
769 :: (map HOLogic.mk_Trueprop |
|
770 [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j]) |
|
771 val subgoal3 = (HOLogic.mk_Trueprop neg_t2) |
|
772 :: terms2_3 |
|
773 @ not_false |
|
774 :: (map HOLogic.mk_Trueprop |
|
775 [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j]) |
|
776 val Ts' = split_type :: split_type :: Ts |
|
777 in |
|
778 SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)] |
|
779 end |
|
780 (* this will only happen if a split theorem can be applied for which no *) |
|
781 (* code exists above -- in which case either the split theorem should be *) |
|
782 (* implemented above, or 'is_split_thm' should be modified to filter it *) |
|
783 (* out *) |
|
784 | (t, ts) => ( |
|
785 warning ("Lin. Arith.: split rule for " ^ ProofContext.string_of_term ctxt t ^ |
|
786 " (with " ^ string_of_int (length ts) ^ |
|
787 " argument(s)) not implemented; proof reconstruction is likely to fail"); |
|
788 NONE |
|
789 )) |
|
790 ) |
|
791 end; |
|
792 |
|
793 (* remove terms that do not satisfy 'p'; change the order of the remaining *) |
|
794 (* terms in the same way as filter_prems_tac does *) |
|
795 |
|
796 fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list = |
|
797 let |
|
798 fun filter_prems (t, (left, right)) = |
|
799 if p t then (left, right @ [t]) else (left @ right, []) |
|
800 val (left, right) = foldl filter_prems ([], []) terms |
|
801 in |
|
802 right @ left |
|
803 end; |
|
804 |
|
805 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *) |
|
806 (* subgoal that has 'terms' as premises *) |
|
807 |
|
808 fun negated_term_occurs_positively (terms : term list) : bool = |
|
809 List.exists |
|
810 (fn (Trueprop $ (Const ("Not", _) $ t)) => member (op aconv) terms (Trueprop $ t) |
|
811 | _ => false) |
|
812 terms; |
|
813 |
|
814 fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list = |
|
815 let |
|
816 (* repeatedly split (including newly emerging subgoals) until no further *) |
|
817 (* splitting is possible *) |
|
818 fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list) |
|
819 | split_loop (subgoal::subgoals) = ( |
|
820 case split_once_items ctxt subgoal of |
|
821 SOME new_subgoals => split_loop (new_subgoals @ subgoals) |
|
822 | NONE => subgoal :: split_loop subgoals |
|
823 ) |
|
824 fun is_relevant t = isSome (decomp ctxt t) |
|
825 (* filter_prems_tac is_relevant: *) |
|
826 val relevant_terms = filter_prems_tac_items is_relevant terms |
|
827 (* split_tac, NNF normalization: *) |
|
828 val split_goals = split_loop [(Ts, relevant_terms)] |
|
829 (* necessary because split_once_tac may normalize terms: *) |
|
830 val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals |
|
831 (* TRY (etac notE) THEN eq_assume_tac: *) |
|
832 val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm |
|
833 in |
|
834 result |
|
835 end; |
|
836 |
|
837 (* takes the i-th subgoal [| A1; ...; An |] ==> B to *) |
|
838 (* An --> ... --> A1 --> B, performs splitting with the given 'split_thms' *) |
|
839 (* (resulting in a different subgoal P), takes P to ~P ==> False, *) |
|
840 (* performs NNF-normalization of ~P, and eliminates conjunctions, *) |
|
841 (* disjunctions and existential quantifiers from the premises, possibly (in *) |
|
842 (* the case of disjunctions) resulting in several new subgoals, each of the *) |
|
843 (* general form [| Q1; ...; Qm |] ==> False. Fails if more than *) |
|
844 (* !fast_arith_split_limit splits are possible. *) |
|
845 |
|
846 local |
|
847 val nnf_simpset = |
|
848 empty_ss setmkeqTrue mk_eq_True |
|
849 setmksimps (mksimps mksimps_pairs) |
|
850 addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj, |
|
851 not_all, not_ex, not_not] |
|
852 fun prem_nnf_tac i st = |
|
853 full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st |
|
854 in |
|
855 |
|
856 fun split_once_tac ctxt split_thms = |
|
857 let |
|
858 val thy = ProofContext.theory_of ctxt |
|
859 val cond_split_tac = SUBGOAL (fn (subgoal, i) => |
|
860 let |
|
861 val Ts = rev (map snd (Logic.strip_params subgoal)) |
|
862 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal) |
|
863 val cmap = Splitter.cmap_of_split_thms split_thms |
|
864 val splits = Splitter.split_posns cmap thy Ts concl |
|
865 val split_limit = ConfigOption.get ctxt fast_arith_split_limit |
|
866 in |
|
867 if length splits > split_limit then no_tac |
|
868 else split_tac split_thms i |
|
869 end) |
|
870 in |
|
871 EVERY' [ |
|
872 REPEAT_DETERM o etac rev_mp, |
|
873 cond_split_tac, |
|
874 rtac ccontr, |
|
875 prem_nnf_tac, |
|
876 TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE)) |
|
877 ] |
|
878 end; |
|
879 |
|
880 end; (* local *) |
|
881 |
|
882 (* remove irrelevant premises, then split the i-th subgoal (and all new *) |
|
883 (* subgoals) by using 'split_once_tac' repeatedly. Beta-eta-normalize new *) |
|
884 (* subgoals and finally attempt to solve them by finding an immediate *) |
|
885 (* contradiction (i.e. a term and its negation) in their premises. *) |
|
886 |
|
887 fun pre_tac ctxt i = |
|
888 let |
|
889 val split_thms = filter is_split_thm (#splits (get_arith_data ctxt)) |
|
890 fun is_relevant t = isSome (decomp ctxt t) |
|
891 in |
|
892 DETERM ( |
|
893 TRY (filter_prems_tac is_relevant i) |
|
894 THEN ( |
|
895 (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms)) |
|
896 THEN_ALL_NEW |
|
897 (CONVERSION Drule.beta_eta_conversion |
|
898 THEN' |
|
899 (TRY o (etac notE THEN' eq_assume_tac))) |
|
900 ) i |
|
901 ) |
|
902 end; |
|
903 |
|
904 end; (* LA_Data_Ref *) |
|
905 |
|
906 |
|
907 structure Fast_Arith = |
|
908 Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); |
|
909 |
|
910 fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; |
|
911 val fast_ex_arith_tac = Fast_Arith.lin_arith_tac; |
|
912 val trace_arith = Fast_Arith.trace; |
|
913 |
|
914 (* reduce contradictory <= to False. |
|
915 Most of the work is done by the cancel tactics. *) |
|
916 |
|
917 val init_arith_data = |
|
918 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => |
|
919 {add_mono_thms = add_mono_thms @ |
|
920 @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field}, |
|
921 mult_mono_thms = mult_mono_thms, |
|
922 inj_thms = inj_thms, |
|
923 lessD = lessD @ [thm "Suc_leI"], |
|
924 neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}], |
|
925 simpset = HOL_basic_ss |
|
926 addsimps |
|
927 [@{thm "monoid_add_class.zero_plus.add_0_left"}, |
|
928 @{thm "monoid_add_class.zero_plus.add_0_right"}, |
|
929 @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"}, |
|
930 @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"}, |
|
931 @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"}, |
|
932 @{thm "not_one_less_zero"}] |
|
933 addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] |
|
934 (*abel_cancel helps it work in abstract algebraic domains*) |
|
935 addsimprocs nat_cancel_sums_add}) #> |
|
936 arith_discrete "nat"; |
|
937 |
|
938 val fast_nat_arith_simproc = |
|
939 Simplifier.simproc (the_context ()) "fast_nat_arith" |
|
940 ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K Fast_Arith.lin_arith_simproc); |
|
941 |
|
942 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only |
|
943 useful to detect inconsistencies among the premises for subgoals which are |
|
944 *not* themselves (in)equalities, because the latter activate |
|
945 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the |
|
946 solver all the time rather than add the additional check. *) |
|
947 |
|
948 |
|
949 (* arith proof method *) |
|
950 |
|
951 local |
|
952 |
|
953 fun raw_arith_tac ctxt ex = |
|
954 (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o |
|
955 decomp sg"? -- but note that the test is applied to terms already before |
|
956 they are split/normalized) to speed things up in case there are lots of |
|
957 irrelevant terms involved; elimination of min/max can be optimized: |
|
958 (max m n + k <= r) = (m+k <= r & n+k <= r) |
|
959 (l <= min m n + k) = (l <= m+k & l <= n+k) |
|
960 *) |
|
961 refute_tac (K true) |
|
962 (* Splitting is also done inside fast_arith_tac, but not completely -- *) |
|
963 (* split_tac may use split theorems that have not been implemented in *) |
|
964 (* fast_arith_tac (cf. pre_decomp and split_once_items above), and *) |
|
965 (* fast_arith_split_limit may trigger. *) |
|
966 (* Therefore splitting outside of fast_arith_tac may allow us to prove *) |
|
967 (* some goals that fast_arith_tac alone would fail on. *) |
|
968 (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt))) |
|
969 (fast_ex_arith_tac ctxt ex); |
|
970 |
|
971 fun more_arith_tacs ctxt = |
|
972 let val tactics = #tactics (get_arith_data ctxt) |
|
973 in FIRST' (map (fn ArithTactic {tactic, ...} => tactic) tactics) end; |
|
974 |
|
975 in |
|
976 |
|
977 fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, |
|
978 ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true]; |
|
979 |
|
980 fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt, |
|
981 ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true, |
|
982 more_arith_tacs ctxt]; |
|
983 |
|
984 fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, |
|
985 ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false, |
|
986 more_arith_tacs ctxt]; |
|
987 |
|
988 fun arith_method src = |
|
989 Method.syntax Args.bang_facts src |
|
990 #> (fn (prems, ctxt) => Method.METHOD (fn facts => |
|
991 HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac ctxt))); |
|
992 |
|
993 end; |
|
994 |
|
995 (* antisymmetry: |
168 (* antisymmetry: |
996 combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y |
169 combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y |
997 |
170 |
998 local |
171 local |
999 val antisym = mk_meta_eq order_antisym |
172 val antisym = mk_meta_eq order_antisym |