90 addsimps comp_arith |
90 addsimps comp_arith |
91 addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}] |
91 addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}] |
92 (* Simp rules for changing (n::int) to int n *) |
92 (* Simp rules for changing (n::int) to int n *) |
93 val simpset1 = HOL_basic_ss |
93 val simpset1 = HOL_basic_ss |
94 addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) |
94 addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) |
95 [int_int_eq, zle_int, zless_int, zadd_int, zmult_int] |
95 [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}] |
96 addsplits [zdiff_int_split] |
96 addsplits [zdiff_int_split] |
97 (*simp rules for elimination of int n*) |
97 (*simp rules for elimination of int n*) |
98 |
98 |
99 val simpset2 = HOL_basic_ss |
99 val simpset2 = HOL_basic_ss |
100 addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1] |
100 addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}] |
101 addcongs [conj_le_cong, imp_le_cong] |
101 addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}] |
102 (* simp rules for elimination of abs *) |
102 (* simp rules for elimination of abs *) |
103 val simpset3 = HOL_basic_ss addsplits [abs_split] |
103 val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}] |
104 val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
104 val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
105 (* Theorem for the nat --> int transformation *) |
105 (* Theorem for the nat --> int transformation *) |
106 val pre_thm = Seq.hd (EVERY |
106 val pre_thm = Seq.hd (EVERY |
107 [simp_tac mod_div_simpset 1, simp_tac simpset0 1, |
107 [simp_tac mod_div_simpset 1, simp_tac simpset0 1, |
108 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), |
108 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), |