src/HOL/Numeral_Simprocs.thy
changeset 54249 ce00f2fef556
parent 48891 c0eafbd55de3
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Mon Nov 04 18:08:47 2013 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Mon Nov 04 20:10:06 2013 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  ML_file "~~/src/Provers/Arith/extract_common_term.ML"
     1.5  
     1.6  lemmas semiring_norm =
     1.7 -  Let_def arith_simps nat_arith rel_simps
     1.8 +  Let_def arith_simps diff_nat_numeral rel_simps
     1.9    if_False if_True
    1.10    add_0 add_Suc add_numeral_left
    1.11    add_neg_numeral_left mult_numeral_left
    1.12 @@ -278,27 +278,8 @@
    1.13    ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
    1.14    {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
    1.15  
    1.16 -(* FIXME: duplicate rule warnings for:
    1.17 -  ring_distribs
    1.18 -  numeral_plus_numeral numeral_times_numeral
    1.19 -  numeral_eq_iff numeral_less_iff numeral_le_iff
    1.20 -  numeral_neq_zero zero_neq_numeral zero_less_numeral
    1.21 -  if_True if_False *)
    1.22  declaration {* 
    1.23 -  K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}])
    1.24 -  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
    1.25 -     @{thm nat_0}, @{thm nat_1},
    1.26 -     @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral},
    1.27 -     @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff},
    1.28 -     @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
    1.29 -     @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
    1.30 -     @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
    1.31 -     @{thm mult_Suc}, @{thm mult_Suc_right},
    1.32 -     @{thm add_Suc}, @{thm add_Suc_right},
    1.33 -     @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral},
    1.34 -     @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral},
    1.35 -     @{thm if_True}, @{thm if_False}])
    1.36 -  #> Lin_Arith.add_simprocs
    1.37 +  K (Lin_Arith.add_simprocs
    1.38        [@{simproc semiring_assoc_fold},
    1.39         @{simproc int_combine_numerals},
    1.40         @{simproc inteq_cancel_numerals},