equal
deleted
inserted
replaced
1 (* Title: HOL/Integ/presburger.ML |
1 (* Title: HOL/Integ/presburger.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Amine Chaieb and Stefan Berghofer, TU Muenchen |
3 Author: Amine Chaieb and Stefan Berghofer, TU Muenchen |
4 |
4 |
5 Tactic for solving arithmetical Goals in Presburger Arithmetic |
5 Tactic for solving arithmetical Goals in Presburger Arithmetic. |
6 *) |
6 |
7 |
7 This version of presburger deals with occurences of functional symbols |
8 (* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To enable this feature call the procedure with the parameter abs |
8 in the subgoal and abstract over them to try to prove the more general |
|
9 formula. It then resolves with the subgoal. To enable this feature |
|
10 call the procedure with the parameter abs. |
9 *) |
11 *) |
10 |
12 |
11 signature PRESBURGER = |
13 signature PRESBURGER = |
12 sig |
14 sig |
13 val presburger_tac : bool -> bool -> int -> tactic |
15 val presburger_tac : bool -> bool -> int -> tactic |
235 a = flag for abstracting over function occurences |
237 a = flag for abstracting over function occurences |
236 i = subgoal *) |
238 i = subgoal *) |
237 |
239 |
238 fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st => |
240 fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st => |
239 let |
241 let |
240 val g = BasisLibrary.List.nth (prems_of st, i - 1) |
242 val g = List.nth (prems_of st, i - 1) |
241 val sg = sign_of_thm st |
243 val sg = sign_of_thm st |
242 (* The Abstraction step *) |
244 (* The Abstraction step *) |
243 val g' = if a then abstract_pres sg g else g |
245 val g' = if a then abstract_pres sg g else g |
244 (* Transform the term*) |
246 (* Transform the term*) |
245 val (t,np,nh) = prepare_for_presburger sg q g' |
247 val (t,np,nh) = prepare_for_presburger sg q g' |