72 val thy = ProofContext.theory_of ctxt |
72 val thy = ProofContext.theory_of ctxt |
73 (* Transform the term*) |
73 (* Transform the term*) |
74 val (t,np,nh) = prepare_for_linz q g |
74 val (t,np,nh) = prepare_for_linz q g |
75 (* Some simpsets for dealing with mod div abs and nat*) |
75 (* Some simpsets for dealing with mod div abs and nat*) |
76 val mod_div_simpset = HOL_basic_ss |
76 val mod_div_simpset = HOL_basic_ss |
77 addsimps [refl,mod_add_eq, mod_add_left_eq, |
77 addsimps [refl,mod_add_eq, mod_add_left_eq, |
78 mod_add_right_eq, |
78 mod_add_right_eq, |
79 nat_div_add_eq, int_div_add_eq, |
79 nat_div_add_eq, int_div_add_eq, |
80 @{thm mod_self}, @{thm "zmod_self"}, |
80 @{thm mod_self}, @{thm "zmod_self"}, |
81 @{thm mod_by_0}, @{thm div_by_0}, |
81 @{thm mod_by_0}, @{thm div_by_0}, |
82 @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, |
82 @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, |
83 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
83 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
84 Suc_eq_plus1] |
84 Suc_eq_plus1] |
85 addsimps @{thms add_ac} |
85 addsimps @{thms add_ac} |
86 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc] |
86 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc] |
87 val simpset0 = HOL_basic_ss |
87 val simpset0 = HOL_basic_ss |
88 addsimps [mod_div_equality', Suc_eq_plus1] |
88 addsimps [mod_div_equality', Suc_eq_plus1] |
89 addsimps comp_arith |
89 addsimps comp_arith |
90 addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}] |
90 addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}] |
91 (* Simp rules for changing (n::int) to int n *) |
91 (* Simp rules for changing (n::int) to int n *) |