136 |
136 |
137 |
137 |
138 |
138 |
139 (** prepare nat_cancel simprocs **) |
139 (** prepare nat_cancel simprocs **) |
140 |
140 |
141 fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s; |
141 fun prep_simproc (name, pats, proc) = |
142 val prep_pats = map prep_pat; |
142 Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc; |
143 |
|
144 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; |
|
145 |
|
146 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", |
|
147 "m = Suc n"]; |
|
148 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", |
|
149 "m < Suc n"]; |
|
150 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", |
|
151 "Suc m <= n", "m <= Suc n"]; |
|
152 val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", |
|
153 "Suc m - n", "m - Suc n"]; |
|
154 |
143 |
155 val nat_cancel_sums_add = map prep_simproc |
144 val nat_cancel_sums_add = map prep_simproc |
156 [("nateq_cancel_sums", eq_pats, EqCancelSums.proc), |
145 [("nateq_cancel_sums", |
157 ("natless_cancel_sums", less_pats, LessCancelSums.proc), |
146 ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc), |
158 ("natle_cancel_sums", le_pats, LeCancelSums.proc)]; |
147 ("natless_cancel_sums", |
|
148 ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], LessCancelSums.proc), |
|
149 ("natle_cancel_sums", |
|
150 ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], LeCancelSums.proc)]; |
159 |
151 |
160 val nat_cancel_sums = nat_cancel_sums_add @ |
152 val nat_cancel_sums = nat_cancel_sums_add @ |
161 [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)]; |
153 [prep_simproc ("natdiff_cancel_sums", |
162 |
154 ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], DiffCancelSums.proc)]; |
163 |
155 |
164 end; |
156 end; |
165 |
157 |
166 open ArithData; |
158 open ArithData; |
167 |
159 |
391 simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}), |
383 simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}), |
392 ArithTheoryData.init, arith_discrete ("nat", true)]; |
384 ArithTheoryData.init, arith_discrete ("nat", true)]; |
393 |
385 |
394 end; |
386 end; |
395 |
387 |
396 |
388 val fast_nat_arith_simproc = |
397 local |
389 Simplifier.simproc (Theory.sign_of (the_context ())) "fast_nat_arith" |
398 val nat_arith_simproc_pats = |
390 ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover; |
399 map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT)) |
391 |
400 ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]; |
|
401 in |
|
402 val fast_nat_arith_simproc = mk_simproc |
|
403 "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover; |
|
404 end; |
|
405 |
392 |
406 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only |
393 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only |
407 useful to detect inconsistencies among the premises for subgoals which are |
394 useful to detect inconsistencies among the premises for subgoals which are |
408 *not* themselves (in)equalities, because the latter activate |
395 *not* themselves (in)equalities, because the latter activate |
409 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the |
396 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the |