52 val mod_add_eq = @{thm "mod_add_eq"} RS sym; |
52 val mod_add_eq = @{thm "mod_add_eq"} RS sym; |
53 val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym; |
53 val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym; |
54 val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym; |
54 val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym; |
55 val nat_div_add_eq = @{thm "div_add1_eq"} RS sym; |
55 val nat_div_add_eq = @{thm "div_add1_eq"} RS sym; |
56 val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym; |
56 val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym; |
57 val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2; |
|
58 val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1; |
|
59 |
57 |
60 fun prepare_for_mir thy q fm = |
58 fun prepare_for_mir thy q fm = |
61 let |
59 let |
62 val ps = Logic.strip_params fm |
60 val ps = Logic.strip_params fm |
63 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
61 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
94 (* Transform the term*) |
92 (* Transform the term*) |
95 val (t,np,nh) = prepare_for_mir thy q g |
93 val (t,np,nh) = prepare_for_mir thy q g |
96 (* Some simpsets for dealing with mod div abs and nat*) |
94 (* Some simpsets for dealing with mod div abs and nat*) |
97 val mod_div_simpset = HOL_basic_ss |
95 val mod_div_simpset = HOL_basic_ss |
98 addsimps [refl, mod_add_eq, |
96 addsimps [refl, mod_add_eq, |
99 @{thm "mod_self"}, @{thm "zmod_self"}, |
97 @{thm mod_self}, |
100 @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, |
98 @{thm div_0}, @{thm mod_0}, |
101 @{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"}, |
102 @{thm "Suc_eq_plus1"}] |
100 @{thm "Suc_eq_plus1"}] |
103 addsimps @{thms add_ac} |
101 addsimps @{thms add_ac} |
104 addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] |
102 addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] |
105 val simpset0 = HOL_basic_ss |
103 val simpset0 = HOL_basic_ss |