tuned fact references
authorhaftmann
Sat Dec 17 15:22:13 2016 +0100 (2016-12-17)
changeset 64589c1932a4a227f
parent 64588 293ab573d034
child 64590 6621d91d3c8a
tuned fact references
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:13 2016 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -823,15 +823,13 @@
     1.4      |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}])
     1.5  val div_mod_ss =
     1.6    simpset_of (put_simpset HOL_basic_ss @{context}
     1.7 -    addsimps @{thms simp_thms}
     1.8 -    @ map (Thm.symmetric o mk_meta_eq) 
     1.9 -      [@{thm "dvd_eq_mod_eq_0"},
    1.10 -       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
    1.11 -       @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
    1.12 -    @ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
    1.13 -       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"},
    1.14 -       @{thm "div_by_Suc_0"}, @{thm "mod_by_Suc_0"}, @{thm "Suc_eq_plus1"}]
    1.15 -    @ @{thms ac_simps}
    1.16 +    addsimps @{thms simp_thms
    1.17 +      mod_eq_0_iff_dvd mod_add_left_eq [symmetric] mod_add_right_eq [symmetric]
    1.18 +      mod_add_eq [symmetric] div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
    1.19 +      mod_self mod_by_0 div_by_0
    1.20 +      div_0 mod_0 div_by_1 mod_by_1
    1.21 +      div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1
    1.22 +      ac_simps}
    1.23     addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
    1.24  val splits_ss =
    1.25    simpset_of (put_simpset comp_ss @{context}