287 (* The Abstraction step *) |
287 (* The Abstraction step *) |
288 val g' = if a then abstract_pres sg g else g |
288 val g' = if a then abstract_pres sg g else g |
289 (* Transform the term*) |
289 (* Transform the term*) |
290 val (t,np,nh) = prepare_for_presburger sg q g' |
290 val (t,np,nh) = prepare_for_presburger sg q g' |
291 (* Some simpsets for dealing with mod div abs and nat*) |
291 (* Some simpsets for dealing with mod div abs and nat*) |
292 val mod_div_simpset = HOL_basic_ss |
292 val mod_div_simpset = Simplifier.theory_context sg HOL_basic_ss |
293 addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, |
293 addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, |
294 nat_mod_add_right_eq, int_mod_add_eq, |
294 nat_mod_add_right_eq, int_mod_add_eq, |
295 int_mod_add_right_eq, int_mod_add_left_eq, |
295 int_mod_add_right_eq, int_mod_add_left_eq, |
296 nat_div_add_eq, int_div_add_eq, |
296 nat_div_add_eq, int_div_add_eq, |
297 mod_self, zmod_self, |
297 mod_self, zmod_self, |