74 in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs))) |
74 in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs))) |
75 handle ERROR msg => |
75 handle ERROR msg => |
76 (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE) |
76 (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE) |
77 end; |
77 end; |
78 |
78 |
79 fun prep_simproc thy (name, pats, proc) = |
|
80 Simplifier.simproc_global thy name pats proc; |
|
81 |
|
82 |
79 |
83 (*** Use CancelNumerals simproc without binary numerals, |
80 (*** Use CancelNumerals simproc without binary numerals, |
84 just for cancellation ***) |
81 just for cancellation ***) |
85 |
82 |
86 val mk_times = FOLogic.mk_binop @{const_name Arith.mult}; |
83 val mk_times = FOLogic.mk_binop @{const_name Arith.mult}; |
200 |
197 |
201 structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData); |
198 structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData); |
202 |
199 |
203 |
200 |
204 val nat_cancel = |
201 val nat_cancel = |
205 map (prep_simproc @{theory}) |
202 [Simplifier.make_simproc @{context} "nateq_cancel_numerals" |
206 [("nateq_cancel_numerals", |
203 {lhss = |
207 ["l #+ m = n", "l = m #+ n", |
204 [@{term "l #+ m = n"}, @{term "l = m #+ n"}, |
208 "l #* m = n", "l = m #* n", |
205 @{term "l #* m = n"}, @{term "l = m #* n"}, |
209 "succ(m) = n", "m = succ(n)"], |
206 @{term "succ(m) = n"}, @{term "m = succ(n)"}], |
210 EqCancelNumerals.proc), |
207 proc = K EqCancelNumerals.proc, identifier = []}, |
211 ("natless_cancel_numerals", |
208 Simplifier.make_simproc @{context} "natless_cancel_numerals" |
212 ["l #+ m < n", "l < m #+ n", |
209 {lhss = |
213 "l #* m < n", "l < m #* n", |
210 [@{term "l #+ m < n"}, @{term "l < m #+ n"}, |
214 "succ(m) < n", "m < succ(n)"], |
211 @{term "l #* m < n"}, @{term "l < m #* n"}, |
215 LessCancelNumerals.proc), |
212 @{term "succ(m) < n"}, @{term "m < succ(n)"}], |
216 ("natdiff_cancel_numerals", |
213 proc = K LessCancelNumerals.proc, identifier = []}, |
217 ["(l #+ m) #- n", "l #- (m #+ n)", |
214 Simplifier.make_simproc @{context} "natdiff_cancel_numerals" |
218 "(l #* m) #- n", "l #- (m #* n)", |
215 {lhss = |
219 "succ(m) #- n", "m #- succ(n)"], |
216 [@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"}, |
220 DiffCancelNumerals.proc)]; |
217 @{term "(l #* m) #- n"}, @{term "l #- (m #* n)"}, |
|
218 @{term "succ(m) #- n"}, @{term "m #- succ(n)"}], |
|
219 proc = K DiffCancelNumerals.proc, identifier = []}]; |
221 |
220 |
222 end; |
221 end; |
223 |
222 |
224 val _ = |
223 val _ = |
225 Theory.setup (Simplifier.map_theory_simpset (fn ctxt => |
224 Theory.setup (Simplifier.map_theory_simpset (fn ctxt => |