86 [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, |
86 [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, |
87 @{thm "split_min"}, @{thm "split_max"}] |
87 @{thm "split_min"}, @{thm "split_max"}] |
88 (* Simp rules for changing (n::int) to int n *) |
88 (* Simp rules for changing (n::int) to int n *) |
89 val simpset1 = put_simpset HOL_basic_ss ctxt |
89 val simpset1 = put_simpset HOL_basic_ss ctxt |
90 addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @ |
90 addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @ |
91 map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm nat_numeral}] |
91 map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}] |
92 |> Splitter.add_split @{thm "zdiff_int_split"} |
92 |> Splitter.add_split @{thm "zdiff_int_split"} |
93 (*simp rules for elimination of int n*) |
93 (*simp rules for elimination of int n*) |
94 |
94 |
95 val simpset2 = put_simpset HOL_basic_ss ctxt |
95 val simpset2 = put_simpset HOL_basic_ss ctxt |
96 addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral}, |
96 addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral}, |
97 @{thm "int_0"}, @{thm "int_1"}] |
97 @{thm "of_nat_0"}, @{thm "of_nat_1"}] |
98 |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] |
98 |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] |
99 (* simp rules for elimination of abs *) |
99 (* simp rules for elimination of abs *) |
100 val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) |
100 val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) |
101 (* Theorem for the nat --> int transformation *) |
101 (* Theorem for the nat --> int transformation *) |
102 val pre_thm = Seq.hd (EVERY |
102 val pre_thm = Seq.hd (EVERY |