25 val mod_div_equality' = @{thm mod_div_equality'}; |
25 val mod_div_equality' = @{thm mod_div_equality'}; |
26 val split_div' = @{thm split_div'}; |
26 val split_div' = @{thm split_div'}; |
27 val Suc_plus1 = @{thm Suc_plus1}; |
27 val Suc_plus1 = @{thm Suc_plus1}; |
28 val imp_le_cong = @{thm imp_le_cong}; |
28 val imp_le_cong = @{thm imp_le_cong}; |
29 val conj_le_cong = @{thm conj_le_cong}; |
29 val conj_le_cong = @{thm conj_le_cong}; |
30 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym; |
30 val mod_add_left_eq = @{thm mod_add_left_eq} RS sym; |
31 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym; |
31 val mod_add_right_eq = @{thm mod_add_right_eq} RS sym; |
32 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym; |
32 val mod_add_eq = @{thm mod_add_eq} RS sym; |
33 val int_mod_add_eq = @{thm mod_add_eq} RS sym; |
|
34 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym; |
|
35 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym; |
|
36 val nat_div_add_eq = @{thm div_add1_eq} RS sym; |
33 val nat_div_add_eq = @{thm div_add1_eq} RS sym; |
37 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; |
34 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; |
38 |
35 |
39 fun prepare_for_linz q fm = |
36 fun prepare_for_linz q fm = |
40 let |
37 let |
68 val thy = ProofContext.theory_of ctxt |
65 val thy = ProofContext.theory_of ctxt |
69 (* Transform the term*) |
66 (* Transform the term*) |
70 val (t,np,nh) = prepare_for_linz q g |
67 val (t,np,nh) = prepare_for_linz q g |
71 (* Some simpsets for dealing with mod div abs and nat*) |
68 (* Some simpsets for dealing with mod div abs and nat*) |
72 val mod_div_simpset = HOL_basic_ss |
69 val mod_div_simpset = HOL_basic_ss |
73 addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, |
70 addsimps [refl,mod_add_eq, mod_add_left_eq, |
74 nat_mod_add_right_eq, int_mod_add_eq, |
71 mod_add_right_eq, |
75 int_mod_add_right_eq, int_mod_add_left_eq, |
|
76 nat_div_add_eq, int_div_add_eq, |
72 nat_div_add_eq, int_div_add_eq, |
77 @{thm mod_self}, @{thm "zmod_self"}, |
73 @{thm mod_self}, @{thm "zmod_self"}, |
78 @{thm mod_by_0}, @{thm div_by_0}, |
74 @{thm mod_by_0}, @{thm div_by_0}, |
79 @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, |
75 @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, |
80 @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
76 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, |
81 Suc_plus1] |
77 Suc_plus1] |
82 addsimps @{thms add_ac} |
78 addsimps @{thms add_ac} |
83 addsimprocs [cancel_div_mod_proc] |
79 addsimprocs [cancel_div_mod_proc] |
84 val simpset0 = HOL_basic_ss |
80 val simpset0 = HOL_basic_ss |
85 addsimps [mod_div_equality', Suc_plus1] |
81 addsimps [mod_div_equality', Suc_plus1] |