equal
deleted
inserted
replaced
433 (l <= min m n + k) = (l <= m+k & l <= n+k) |
433 (l <= min m n + k) = (l <= m+k & l <= n+k) |
434 *) |
434 *) |
435 local |
435 local |
436 |
436 |
437 fun raw_arith_tac ex i st = |
437 fun raw_arith_tac ex i st = |
|
438 let fun elim_neq_tac i = |
|
439 COND (K(!ignore_neq)) all_tac (REPEAT_DETERM(etac linorder_neqE i)) |
|
440 in |
438 refute_tac (K true) |
441 refute_tac (K true) |
439 (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st)))) |
442 (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st)))) |
440 ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex) |
443 (elim_neq_tac THEN' fast_ex_arith_tac ex) |
441 i st; |
444 i st |
|
445 end; |
442 |
446 |
443 fun presburger_tac i st = |
447 fun presburger_tac i st = |
444 (case ArithTheoryData.get_sg (sign_of_thm st) of |
448 (case ArithTheoryData.get_sg (sign_of_thm st) of |
445 {presburger = Some tac, ...} => |
449 {presburger = Some tac, ...} => |
446 (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st) |
450 (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st) |