206 datatype arithtactic = ArithTactic of {name: string, tactic: int -> tactic, id: stamp}; |
206 datatype arithtactic = ArithTactic of {name: string, tactic: int -> tactic, id: stamp}; |
207 |
207 |
208 fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()}; |
208 fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()}; |
209 |
209 |
210 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); |
210 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); |
|
211 |
|
212 val merge_arith_tactics = gen_merge_lists eq_arith_tactic; |
211 |
213 |
212 structure ArithTheoryData = TheoryDataFun |
214 structure ArithTheoryData = TheoryDataFun |
213 (struct |
215 (struct |
214 val name = "HOL/arith"; |
216 val name = "HOL/arith"; |
215 type T = {splits: thm list, |
217 type T = {splits: thm list, |
222 fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, |
224 fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, |
223 {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) = |
225 {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) = |
224 {splits = Drule.merge_rules (splits1, splits2), |
226 {splits = Drule.merge_rules (splits1, splits2), |
225 inj_consts = merge_lists inj_consts1 inj_consts2, |
227 inj_consts = merge_lists inj_consts1 inj_consts2, |
226 discrete = merge_lists discrete1 discrete2, |
228 discrete = merge_lists discrete1 discrete2, |
227 tactics = gen_merge_lists eq_arith_tactic tactics1 tactics2}; |
229 tactics = merge_arith_tactics tactics1 tactics2}; |
228 fun print _ _ = (); |
230 fun print _ _ = (); |
229 end); |
231 end); |
230 |
232 |
231 val arith_split_add = Thm.declaration_attribute (fn thm => |
233 val arith_split_add = Thm.declaration_attribute (fn thm => |
232 Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
234 Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
237 |
239 |
238 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
240 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
239 {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, tactics= tactics}); |
241 {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, tactics= tactics}); |
240 |
242 |
241 fun arith_tactic_add tac = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
243 fun arith_tactic_add tac = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
242 {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics @ [tac]}); |
244 {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= merge_arith_tactics tactics [tac]}); |
243 |
245 |
244 |
246 |
245 signature HOL_LIN_ARITH_DATA = |
247 signature HOL_LIN_ARITH_DATA = |
246 sig |
248 sig |
247 include LIN_ARITH_DATA |
249 include LIN_ARITH_DATA |