97 @{thm "mod_self"}, @{thm "zmod_self"}, |
97 @{thm "mod_self"}, @{thm "zmod_self"}, |
98 @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, |
98 @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, |
99 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
99 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
100 @{thm "Suc_plus1"}] |
100 @{thm "Suc_plus1"}] |
101 addsimps @{thms add_ac} |
101 addsimps @{thms add_ac} |
102 addsimprocs [cancel_div_mod_proc] |
102 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc] |
103 val simpset0 = HOL_basic_ss |
103 val simpset0 = HOL_basic_ss |
104 addsimps [mod_div_equality', Suc_plus1] |
104 addsimps [mod_div_equality', Suc_plus1] |
105 addsimps comp_ths |
105 addsimps comp_ths |
106 addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}] |
106 addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}] |
107 (* Simp rules for changing (n::int) to int n *) |
107 (* Simp rules for changing (n::int) to int n *) |