201 end; (* LA_Logic *) |
201 end; (* LA_Logic *) |
202 |
202 |
203 |
203 |
204 (* arith theory data *) |
204 (* arith theory data *) |
205 |
205 |
|
206 datatype arithtactic = ArithTactic of {name: string, tactic: int -> tactic, id: stamp}; |
|
207 |
|
208 fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()}; |
|
209 |
|
210 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); |
|
211 |
206 structure ArithTheoryData = TheoryDataFun |
212 structure ArithTheoryData = TheoryDataFun |
207 (struct |
213 (struct |
208 val name = "HOL/arith"; |
214 val name = "HOL/arith"; |
209 type T = {splits: thm list, |
215 type T = {splits: thm list, |
210 inj_consts: (string * typ) list, |
216 inj_consts: (string * typ) list, |
211 discrete: string list, |
217 discrete: string list, |
212 presburger: (int -> tactic) option}; |
218 tactics: arithtactic list}; |
213 val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE}; |
219 val empty = {splits = [], inj_consts = [], discrete = [], tactics = []}; |
214 val copy = I; |
220 val copy = I; |
215 val extend = I; |
221 val extend = I; |
216 fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1}, |
222 fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, |
217 {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) = |
223 {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) = |
218 {splits = Drule.merge_rules (splits1, splits2), |
224 {splits = Drule.merge_rules (splits1, splits2), |
219 inj_consts = merge_lists inj_consts1 inj_consts2, |
225 inj_consts = merge_lists inj_consts1 inj_consts2, |
220 discrete = merge_lists discrete1 discrete2, |
226 discrete = merge_lists discrete1 discrete2, |
221 presburger = (case presburger1 of NONE => presburger2 | p => p)}; |
227 tactics = gen_merge_lists eq_arith_tactic tactics1 tactics2}; |
222 fun print _ _ = (); |
228 fun print _ _ = (); |
223 end); |
229 end); |
224 |
230 |
225 val arith_split_add = Thm.declaration_attribute (fn thm => |
231 val arith_split_add = Thm.declaration_attribute (fn thm => |
226 Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => |
232 Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
227 {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}))); |
233 {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics}))); |
228 |
234 |
229 fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => |
235 fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
230 {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger}); |
236 {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, tactics= tactics}); |
231 |
237 |
232 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => |
238 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => |
233 {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger}); |
239 {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, tactics= tactics}); |
|
240 |
|
241 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]}); |
234 |
243 |
235 |
244 |
236 signature HOL_LIN_ARITH_DATA = |
245 signature HOL_LIN_ARITH_DATA = |
237 sig |
246 sig |
238 include LIN_ARITH_DATA |
247 include LIN_ARITH_DATA |
992 (* some goals that fast_arith_tac alone would fail on. *) |
1001 (* some goals that fast_arith_tac alone would fail on. *) |
993 (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st)))) |
1002 (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st)))) |
994 (fast_ex_arith_tac ex) |
1003 (fast_ex_arith_tac ex) |
995 i st; |
1004 i st; |
996 |
1005 |
997 fun presburger_tac i st = |
1006 fun arith_theory_tac i st = |
998 (case ArithTheoryData.get (Thm.theory_of_thm st) of |
1007 let |
999 {presburger = SOME tac, ...} => |
1008 val tactics = #tactics (ArithTheoryData.get (Thm.theory_of_thm st)) |
1000 (warning "Trying full Presburger arithmetic ..."; tac i st) |
1009 in |
1001 | _ => no_tac st); |
1010 FIRST' (map (fn ArithTactic {tactic, ...} => tactic) tactics) i st |
|
1011 end; |
1002 |
1012 |
1003 in |
1013 in |
1004 |
1014 |
1005 val simple_arith_tac = FIRST' [fast_arith_tac, |
1015 val simple_arith_tac = FIRST' [fast_arith_tac, |
1006 ObjectLogic.atomize_tac THEN' raw_arith_tac true]; |
1016 ObjectLogic.atomize_tac THEN' raw_arith_tac true]; |
1007 |
1017 |
1008 val arith_tac = FIRST' [fast_arith_tac, |
1018 val arith_tac = FIRST' [fast_arith_tac, |
1009 ObjectLogic.atomize_tac THEN' raw_arith_tac true, |
1019 ObjectLogic.atomize_tac THEN' raw_arith_tac true, |
1010 presburger_tac]; |
1020 arith_theory_tac]; |
1011 |
1021 |
1012 val silent_arith_tac = FIRST' [fast_arith_tac, |
1022 val silent_arith_tac = FIRST' [fast_arith_tac, |
1013 ObjectLogic.atomize_tac THEN' raw_arith_tac false, |
1023 ObjectLogic.atomize_tac THEN' raw_arith_tac false, |
1014 presburger_tac]; |
1024 arith_theory_tac]; |
1015 |
1025 |
1016 fun arith_method prems = |
1026 fun arith_method prems = |
1017 Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); |
1027 Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); |
1018 |
1028 |
1019 end; |
1029 end; |