24 val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", |
24 val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", |
25 "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]; |
25 "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]; |
26 |
26 |
27 val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", |
27 val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", |
28 "add_Suc", "add_number_of_left", "mult_number_of_left", |
28 "add_Suc", "add_number_of_left", "mult_number_of_left", |
29 "Suc_eq_add_numeral_1"])@ |
29 "Suc_eq_plus1"])@ |
30 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"]) |
30 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"]) |
31 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} |
31 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} |
32 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, |
32 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, |
33 @{thm "real_of_nat_number_of"}, |
33 @{thm "real_of_nat_number_of"}, |
34 @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"}, |
34 @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"}, |
48 val number_of2 = @{thm "number_of2"}; |
48 val number_of2 = @{thm "number_of2"}; |
49 val split_zdiv = @{thm "split_zdiv"}; |
49 val split_zdiv = @{thm "split_zdiv"}; |
50 val split_zmod = @{thm "split_zmod"}; |
50 val split_zmod = @{thm "split_zmod"}; |
51 val mod_div_equality' = @{thm "mod_div_equality'"}; |
51 val mod_div_equality' = @{thm "mod_div_equality'"}; |
52 val split_div' = @{thm "split_div'"}; |
52 val split_div' = @{thm "split_div'"}; |
53 val Suc_plus1 = @{thm "Suc_plus1"}; |
|
54 val imp_le_cong = @{thm "imp_le_cong"}; |
53 val imp_le_cong = @{thm "imp_le_cong"}; |
55 val conj_le_cong = @{thm "conj_le_cong"}; |
54 val conj_le_cong = @{thm "conj_le_cong"}; |
56 val mod_add_eq = @{thm "mod_add_eq"} RS sym; |
55 val mod_add_eq = @{thm "mod_add_eq"} RS sym; |
57 val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym; |
56 val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym; |
58 val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym; |
57 val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym; |
102 val mod_div_simpset = HOL_basic_ss |
101 val mod_div_simpset = HOL_basic_ss |
103 addsimps [refl, mod_add_eq, |
102 addsimps [refl, mod_add_eq, |
104 @{thm "mod_self"}, @{thm "zmod_self"}, |
103 @{thm "mod_self"}, @{thm "zmod_self"}, |
105 @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, |
104 @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, |
106 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
105 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
107 @{thm "Suc_plus1"}] |
106 @{thm "Suc_eq_plus1"}] |
108 addsimps @{thms add_ac} |
107 addsimps @{thms add_ac} |
109 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc] |
108 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc] |
110 val simpset0 = HOL_basic_ss |
109 val simpset0 = HOL_basic_ss |
111 addsimps [mod_div_equality', Suc_plus1] |
110 addsimps [mod_div_equality', @{thm Suc_eq_plus1}] |
112 addsimps comp_ths |
111 addsimps comp_ths |
113 addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}] |
112 addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}] |
114 (* Simp rules for changing (n::int) to int n *) |
113 (* Simp rules for changing (n::int) to int n *) |
115 val simpset1 = HOL_basic_ss |
114 val simpset1 = HOL_basic_ss |
116 addsimps [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] @ map (fn r => r RS sym) |
115 addsimps [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] @ map (fn r => r RS sym) |