821 @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"}, |
821 @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"}, |
822 @{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}] |
822 @{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}] |
823 |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]) |
823 |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]) |
824 val div_mod_ss = |
824 val div_mod_ss = |
825 simpset_of (put_simpset HOL_basic_ss @{context} |
825 simpset_of (put_simpset HOL_basic_ss @{context} |
826 addsimps @{thms simp_thms} |
826 addsimps @{thms simp_thms |
827 @ map (Thm.symmetric o mk_meta_eq) |
827 mod_eq_0_iff_dvd mod_add_left_eq [symmetric] mod_add_right_eq [symmetric] |
828 [@{thm "dvd_eq_mod_eq_0"}, |
828 mod_add_eq [symmetric] div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric] |
829 @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, |
829 mod_self mod_by_0 div_by_0 |
830 @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] |
830 div_0 mod_0 div_by_1 mod_by_1 |
831 @ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"}, |
831 div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1 |
832 @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, |
832 ac_simps} |
833 @{thm "div_by_Suc_0"}, @{thm "mod_by_Suc_0"}, @{thm "Suc_eq_plus1"}] |
|
834 @ @{thms ac_simps} |
|
835 addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]) |
833 addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]) |
836 val splits_ss = |
834 val splits_ss = |
837 simpset_of (put_simpset comp_ss @{context} |
835 simpset_of (put_simpset comp_ss @{context} |
838 addsimps [@{thm minus_div_mult_eq_mod [symmetric]}] |
836 addsimps [@{thm minus_div_mult_eq_mod [symmetric]}] |
839 |> fold Splitter.add_split |
837 |> fold Splitter.add_split |