299 zdiv_1,zmod_1,div_1,mod_1, |
299 zdiv_1,zmod_1,div_1,mod_1, |
300 Suc_plus1] |
300 Suc_plus1] |
301 addsimps add_ac |
301 addsimps add_ac |
302 addsimprocs [cancel_div_mod_proc] |
302 addsimprocs [cancel_div_mod_proc] |
303 val simpset0 = HOL_basic_ss |
303 val simpset0 = HOL_basic_ss |
304 addsimps [mod_div_equality', Suc_plus1] |
304 addsimps [@{thm mod_div_equality'}, @{thm Suc_plus1}] |
305 addsimps comp_arith |
305 addsimps comp_arith |
306 addsplits [split_zdiv, split_zmod, split_div', split_min, split_max] |
306 addsplits [split_zdiv, split_zmod, split_div', @{thm split_min}, @{thm split_max}] |
307 (* Simp rules for changing (n::int) to int n *) |
307 (* Simp rules for changing (n::int) to int n *) |
308 val simpset1 = HOL_basic_ss |
308 val simpset1 = HOL_basic_ss |
309 addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) |
309 addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) |
310 [int_int_eq, zle_int, zless_int, zadd_int, zmult_int] |
310 [int_int_eq, zle_int, zless_int, zadd_int, zmult_int] |
311 addsplits [zdiff_int_split] |
311 addsplits [zdiff_int_split] |