slightly more general simproc (avoids errors of linarith)
authorboehmes
Sat Mar 27 02:10:00 2010 +0100 (2010-03-27)
changeset 3598327e2fa7d4ce7
parent 35982 c7d01a43e41b
child 35984 87e6e2737aee
child 35990 5ceedb86aa9d
slightly more general simproc (avoids errors of linarith)
src/HOL/SMT/Tools/z3_proof_rules.ML
src/HOL/Tools/numeral_simprocs.ML
     1.1 --- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Sat Mar 27 00:08:39 2010 +0100
     1.2 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Sat Mar 27 02:10:00 2010 +0100
     1.3 @@ -1143,6 +1143,7 @@
     1.4    addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
     1.5    addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
     1.6    addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
     1.7 +  addsimps [@{thm mult_1_left}]
     1.8    addsimprocs [
     1.9      Simplifier.simproc @{theory} "fast_int_arith" [
    1.10        "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
     2.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Mar 27 00:08:39 2010 +0100
     2.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Mar 27 02:10:00 2010 +0100
     2.3 @@ -344,8 +344,7 @@
     2.4  struct
     2.5    val assoc_ss = HOL_ss addsimps @{thms mult_ac}
     2.6    val eq_reflection = eq_reflection
     2.7 -  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
     2.8 -    | is_numeral _ = false;
     2.9 +  val is_numeral = can HOLogic.dest_number
    2.10  end;
    2.11  
    2.12  structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);