89 val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT; |
89 val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT; |
90 val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"}; |
90 val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"}; |
91 end); |
91 end); |
92 |
92 |
93 val nat_cancel_sums_add = |
93 val nat_cancel_sums_add = |
94 [Simplifier.simproc @{theory} "nateq_cancel_sums" |
94 [Simplifier.simproc_global @{theory} "nateq_cancel_sums" |
95 ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"] |
95 ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"] |
96 (K EqCancelSums.proc), |
96 (K EqCancelSums.proc), |
97 Simplifier.simproc @{theory} "natless_cancel_sums" |
97 Simplifier.simproc_global @{theory} "natless_cancel_sums" |
98 ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"] |
98 ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"] |
99 (K LessCancelSums.proc), |
99 (K LessCancelSums.proc), |
100 Simplifier.simproc @{theory} "natle_cancel_sums" |
100 Simplifier.simproc_global @{theory} "natle_cancel_sums" |
101 ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"] |
101 ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"] |
102 (K LeCancelSums.proc)]; |
102 (K LeCancelSums.proc)]; |
103 |
103 |
104 val nat_cancel_sums = nat_cancel_sums_add @ |
104 val nat_cancel_sums = nat_cancel_sums_add @ |
105 [Simplifier.simproc @{theory} "natdiff_cancel_sums" |
105 [Simplifier.simproc_global @{theory} "natdiff_cancel_sums" |
106 ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"] |
106 ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"] |
107 (K DiffCancelSums.proc)]; |
107 (K DiffCancelSums.proc)]; |
108 |
108 |
109 val setup = |
109 val setup = |
110 Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); |
110 Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); |